Deriving SKI

The SKI combinator calculus is a formal system which is one of the simpler Turing-complete systems. Its building blocks are the three combinators S, K, and I. These are the atomic terms; other terms can be built by joining two terms together. One thing that confused me at first is that the order in which these combinations is made is significant: combining S and then K and finally appening I is different from combining S with the combination of K and I. That is, terms in the SKI calculus aren’t just flat sequences, they are binary trees, where each internal node represents the combination of two terms.

Given a term, you can then derive other terms based on specific rules for each combinator. From Ix (using x, y, etc as placeholders for any term), you can derive x; from Kxy, you can derive x (dropping y entirely). Finally, from Sxyz you can derive xz(yz):

The S combinator is particularly interesting because, unlike the I and K combinators, it doesn’t result in a smaller tree. This means the S combinator can be used to build up further terms with more interesting derivations (maybe I’ll write another post about some of these interesting derivations at some point).

A neat thing about the tree representation of SKI terms is that it makes it straightforward to implement the derivationg process. All you need to do is traverse the tree, and when you find a structure of nodes that matches one of the combinator structures, replace it with the derived structure.

In tribute to Haskell Curry, one of the inventors of the SKI combinator calculus (with Moses Schönfinkel), here’s an implementation in haskell:

data Term = S | K | I | Placeholder Char | Cat Term Term

derive :: Term -> Term
derive (Cat I t) = t
derive (Cat (Cat K alpha) _) = alpha
derive (Cat (Cat (Cat S alpha) beta) gamma) = 
  (Cat (Cat alpha gamma) (Cat beta gamma))
derive (Cat l r) = if (derive l) /= l then 
    Cat (derive l) r 
  else 
    Cat l (derive r)
derive t = t

There’s also an implementation in PureScript (along with some functions to output SKI terms in GraphViz format, which I used to create the diagrams in this post) on GitHub.