From Lambda calculus to Combinator Calculus

After yesterdays description of the Y combinator in lambda calculus, I thought it would be fun to show some fun and useful stuff that you can do using combinators.

Let's take three simple combinators:

1. S: S is a function application combinator: S = lambda x y z . (x z (y z)).
   
2. K: K generates functions that return a specific constant value: K = lambda x . (lambda y . x).
   
3. I: I is the identity function: I = lambda x . x
   

At first glance, these look like a very strange selection. In particular, S is an odd application mechanism - rather than taking two parameters, x and y, and applying x to y, it takes two functions x and y and a third value z, and applies the result of applying x to z to the result of applying y to z.

But there's a reason. Watch this: each line in the following is one step of reduction:

S K K x =
(K x) (K x) =
x

Poof! We don't need I at all. We just created the equivalent of I using nothing but S and K. But that's just the start: in fact, we can create the equivalent of any lambda calculus expression using nothing but the S and K combinators with no variables.

For example, the Y combinator is:

Y = S S K (S (K (S S (S (S S K)))) K)

Before we go any further, there's one important thing to point out. Note that above, I said that with S K K we created the equivalent of I. It does not reduce to lambda x . x.

So far in lambda calculus, we've said that "x = y" if and only if x and y are either identical, or can be made identical through alpha conversion. (So lambda x y . x + y is equal to lambda a b . a + b, but not equal to lambda x y . y + x.) This is called intensional equivalence. But it's extremely useful to have another idea of equality, which is called extensional equivalence or extensional equality. In extensional equality, an expression X equals an expression Y if/f either X is identical to Y (modulo alphas), or for all a . X a = Y a.

From now on, when we use "=", it will be for extensional equality. We can translate any lambda expression into an extensionally equivalent combinator term. We'll define a transform function C from lambda terms to combinator terms:

• (1) C{x} = x
  
• (2) C{E1 E2} = C{E1} C{E2}
  
• (3) C{lambda x . E} = K C{E} if x is not free in E.
  
• (4) C{lambda x . x} = I
  
• (5) C{lambda x. E1 E2} = (S C{lambda x.E1} C{lambda x.E2})
  
• (6) C{lambda x.(lambda y. E)} = C{lambda x. C{lambda y.E}}, if x is free in E.
  

Let's try a walkthrough:

• C{lambda x y . y x}
  
• Curry the function: C{lambda x . (lambda y . y x)}
  
• By rule 6: C{lambda x . C{lambda y . y x}}
  
• By rule 5: C{lambda x . S C{lambda y. y} C{lambda y . x}}
  
• By rule 4: C{lambda x . S I C{lambda y . x}}
  
• By rule 3: C{lambda x . S I (K C{x})}
  
• By rule 1: C{lambda x . S I (K x)}
  
• By rule 5: S C{lambda x . S I} C{lambda x . (K x)}
  
• By rule 3: S (K (S I)) C{lambda x . K x}
  
• By rule 5: S (K (S I)) (S C{lambda x . K} C{lambda x . x})
  
• By rule 1: S (K (S I)) (S C{lambda x . K} I)
  
• By rule 3: S (K (S I)) (S (K K) I)
  

Now, let's try using "x" and "y" as parameters to that combinator expression, and reduce:

• S (K (S I)) (S (K K) I) x y
  
• Let's create some aliases, to make things easier to read: A=(K (S I)), B = (S (K K) I), so our expression is now: S A B x y
  
• Expand S: (A x (B x)) y
  
• Let's unalias B: (A x ((S (K K) I) x)) y
  
• Now, let's get rid of the S: (A x ((K K) x (I x))) y
  
• And get rid of the I: (A x ((K K) x x)) y
  
• Reduce (K K) x: (A x (K x)) y
  
• Expand out the A alias: ((K (S I)) x (K x)) y
  
• Reduce (K (S I)) x, giving: ((S I) (K x)) y
  
• Reduce S: I y (K x) y
  
• Reduce I: y (K x) y
  
• And finally reduce (K x) y leaving: y x
  

And there we go. Fun, huh?