Fun with SKI calculus

SKI calculus is a pretty simple programming languages with the following grammar:

Expr = S | K | I | Expr Expr

And the following rewrite rules:

I x = x (identity)

K x y = x (constant)

S x y z  = (x z) (y z) (substitution)

Things associate to the left (which is evident from the grammar), so that:

(*) x y z t u v w = ((((((x y) z) t) u) v) w)

The Expr Expr is simply an application. In other hand-wavy words, somebody gave us a way to apply functions (Expr Expr) as well as 3 predefined functions (S, K, and I) and asked us what we can do with it. All the functions here take 1 argument and are curried as seen in (*), so that S x y z = (((S x) y) z).

You can define cool things like Booleans:

T x y = x (true; notice the analogy with if-else if branch)

F x y = y (false; notice the analogy with if-else else branch)

Along with things like:


AND B1 B2 = B1 (B2 T F) F = B1 B2 F

OR B1 B2 = B1 T (B2 T F) = B1 T B2

Where each B is a boolean (T or F; Apologize for the unwanted collision with the B,C,K,W system). One can reasonably guess that T = K and F = S K. Again, notice how OR mimics branching:

// please don't write your code like this
function or(b1: boolean, b2: boolean) {
    if (b1) {
   		return true;
    } else if (b2) {
        return true;
    } else {
     	return false;   

Interestingly, the following identity holds:

B T F = B

Which basically means that SKI calculus itself is telling you not to write things like if (condition) { return true; } else { return false; } and instead simply write return condition. When a combinator calculus developed in 1920s telling you how to refactor things, things must be going in the right direction...

One can introduce natural numbers using Church numerals (each number is a function applied n times):

0 -> 0 f x = x by definition (f applied 0 times), we can guess this is 0 = S K = F and, inductively, by definition of iterative function application:

Succ n f x = f (n f x)

In other words, we map natural numbers to function application. Zero is equivalent to 0 function applications (in other words, a constant), one is 1 function application, and n returns a function that applies a function n times.

Now, can you guess the successor function Succ? Not as easy anymore. However, we can use the following. Imagine a chain of rewrite rules that takes us from Succ n f x to f (n f x). Since the expression on the right is not reducible, the outcome of that derivation is precisely f (n f x). This means that if we find a reverse path starting from f (n f x) that can take us back to Succ n f x we can figure out what that successor function. Now how do we find that path?

First, notice that if we reverse the rewrite rules from the SKI calculus definition we get something like

x -> I x | K x a

a (b x) -> S c b x, where a = c x

Moreover since SKI calculus functions are all curried, we can cancel out rightmost expressions that are the same. In other words, a x = b x implies a = b. We're in some sorta right-cancellative magma now. Or, you know, some people call f x = g x => f = g being injective, because they're not careful. Just kidding. I'm guilty too. Jokes aside, if you treat f and g as functions, it's obvious that two functions are the same if and only if they return the same output for every input. Or is it?

Let's see how we can now apply these reverse rules in order to make a more educated guess of what the successor function might look like:

Succ n f x = f (n f x)

Our first goal is to expand (n f x) into something that has a dangling x on the right, which will allow us to cancel it out. Then, we proceed to factor out f, then, n, and whatever expression we will be left with will be our Succ function. Remember that S combinator is our best friend.

f (n f x) = f ((n f) x) = S a (n f) x, where a x = f

Notice that we have introduced a new variable expression a. In this case, it's easy to guess that a = K f. However, let's be more pedantic and apply our strategy – factor out x on the other side. Our reverse derivation rules that apply here are either f -> I f and f -> K f x and it is pretty clear which one we want to be able to factor out x. Finally, a x = f = K f x, therefore a = K f. Putting that a back into our derivation yields:

Succ n f x = f (n f x) = S (K f) (n f) x

We can cancel out x and all we left with is:

Succ n f = S (K f) (n f)

We continue the process to factor out f using the same strategy:

(1) S (K f) (n f) = S b n f, where b f = S (K f)

(2) b f = S (K f) = S c K f, where c f = S

c f = S = K S f therefore c = K S

Substituting c = K S back into our (2) yields:

b f = S (K f) = S (K S) K f, therefore b = S (K S) K

Putting b back into (1) yields:

S (K f) (n f) = S (S (K S) K) n f

We got lucky there – both free variables n and f lined up nicely for us to cancel them out. After doing so, we get our final answer:

Succ n f = S (K f) (n f) = S (S (K S) K) n f

Succ = S (S (K S) K)

Pretty neat.