This website is out of date, please refer to the site on github.

# Bracket Abstraction: The Smallest PL You've Ever Seen

Posted on May 1, 2015

It’s well known that lambda calculus is an extremely small, Turing Complete language. In fact, most programming languages over the last 5 years have grown some (typed and or broken) embedding of lambda calculus with aptly named lambdas.

This is wonderful and everything but lambda calculus is actually a little complicated. It’s centred around binding and substituting for variables, while this is elegant it’s a little difficult to formalize mathematically. It’s natural to wonder whether we can avoid dealing with variables by building up all our lambda terms from a special privileged few.

These systems (sometimes called combinator calculi) are quite pleasant to model formally, but how do we know that our system is complete? In this post I’d like to go over translating any lambda calculus program into a particular combinator calculus, SK calculus.

## What is SK Combinator Calculus?

SK combinator calculus is a language with exactly 3 types of expressions.

1. We can apply one term to another, `e e`,
2. We have one term `s`
3. We another term `k`

Besides the obvious ones, there are two main rules for this system:

1. `s a b c` = `(a c) (b c)`
2. `k a b` = `a`

And that’s it. What makes SK calculus so remarkable is how minimal it is. We now show that it’s Turing complete by translating lambda calculus into it.

## Bracket Abstraction

First things first, let’s just define how to represent both SK calculus and lambda calculus in our Haskell program.

``````    data Lam = Var Int | Ap Lam Lam | Lam Lam
data SK  = S | K | SKAp SK SK``````

Now we begin by defining a translation from a simplified lambda calculus to SK calculus. This simplified calculus is just SK supplemented with variables. By defining this step, the actual transformation becomes remarkably crisp.

``    data SKH = Var' Int | S' | K' | SKAp' SKH SKH``

Note that while `SKH` has variables, but no way to bind them. In order to remove a variable, we have `bracket`. `bracket` has the property that replacing `Var 0` in a term, `e`, with a term, `e'`, is the same as `SKAp (bracket e) e'`.

``````    -- Remove one variable
bracket :: SKH -> SKH
bracket (Var' 0) = SKAp' (SKAp' S' K') K'
bracket (Var' i) = Var' (i - 1)
bracket (SKAp' l r) = SKAp' (SKAp' S' (bracket l)) (bracket r)
bracket x = x``````

If we’re at `Var 0` we replace the variable with the term `s k k`. This has the property that `(s k k) A = A`. It’s traditional to abbreviate `s k k` as `i` (leading to the name SKI calculus) but `i` is strictly unnecessary as we can see.

If we’re at an application, we do something really clever. We have two terms which both have a free variable, so we bracket them and use `S` to supply the free variable to both of them! Remember that

``s (bracket A) (bracket B) C = ((bracket A) C) ((bracket B) C)``

which is exactly what we require by the specification of `bracket`.

Now that we have a way to remove free variables from an `SKH` term, we can close off a term with no free variables to give back a normal `SK` term.

``````    close :: SKH -> SK
close (Var' _) = error "Not closed"
close S' = S
close K' = K
close (SKAp' l r) = SKAp (close l) (close r)``````

Now our translator can be written nicely.

``````    l2h :: Lam -> SKH
l2h (Var i) = Var' i
l2h (Ap l r) = SKAp' (l2h l) (l2h r)
l2h (Lam h) = bracket (l2h h)

translate :: Lam -> SK
translate = close . l2h``````

`l2h` is the main worker in this function. It works across `SKH`’s because it needs to deal with open terms during the translation. However, during the process we repeatedly call bracket so every time we go under a binder we call `bracket` afterwards, removing the free variable we just introduced.

This means that if we call `l2h` on a closed lambda term we get back a closed `SKH` term. This justifies using `close` after the toplevel call to `l2h` in `translate` which wraps up our conversion.

For funsies I decided to translate the Y combinator and got back this mess

``````(s ((s ((s s) ((s k) k))) ((s ((s s) ((s ((s s) k)) k))) ((s ((s s) k)) k))))
((s ((s s) ((s k) k))) ((s ((s s) ((s ((s s) k)) k))) ((s ((s s) k)) k)))``````

Completely useless, but kinda fun to look at. More interestingly, the canonical nonterminating lambda term is `λx. x x` which gives back `s i i`, much more readable.

## Wrap Up

Now that we’ve performed this translation we have a very nice proof of the turing completeness of SK calculus. This has some nice upshots, folks who study things like realizability models of constructive logics use Partial Combinatory Algebras a model of computation. This is essentially an algebraic model of SK calculus.

If nothing else, it’s really quite crazy that such a small language is possible of simulating any computable function across numbers.