Deriving SKI19 May 2022
The SKI combinator calculus is a formal system which is one of the simpler
Turing-complete systems. Its building blocks are the three combinators
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
I is different from combining
S with the combination of
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
y, etc as placeholders for any term), you
Kxy, you can derive
y entirely). Finally,
Sxyz you can derive
S combinator is particularly interesting because, unlike the
combinators, it doesn’t result in a smaller tree. This means the
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
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.