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:
But there's a reason. Watch this: each line in the following is one step of reduction:
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:
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
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
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:
Let's take three simple combinators:
 S: S is a function application combinator:
S = lambda x y z . (x z (y z))
.  K: K generates functions that return a specific constant value:
K = lambda x . (lambda y . x)
.  I: I is the identity function:
I = lambda x . x
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.

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)

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
0 Comments:
Post a Comment
<< Home