# Deriving SKI

19 May 2022The 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.