# Good Math/Bad Math

## Friday, May 19, 2006

### 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?