| I don't have a reference for the theorem you mentioned, but the proof is fairly
easy. Here goes.
The set of general lambda expressions is generated as follows:
Start with a set of symbols V, consisting of variables and constants.
(1) Each symbol in V is a lambda expression.
(2) If x is a variable, and A is a lambda expression, then Lx.A is a lambda
expression.
(3) If A and B are lambda expressions, then (A B) is a lambda expression.
The set of SK-expressions is generated in the same fashion, but combinators S
and K are added to V, and rule (2) is disallowed. The definitions of S and K
are
S = Lxyz. x z (y z)
K = Lxy. x
Note that we omit extraneous parenthesis -- "x y z" is really "((x y) z)". We
also group lambdas -- "Lxyz." is really "Lx.Ly.Lz.".
THEOREM: For every lambda expression there is an equivalent SK-expression.
First we need a definition, and a lemma. Let's call a lambda expression Lx.A,
where A has no uses of rule (2), a "simple" lambda expression.
LEMMA: For every simple lambda expression, there is an equivalent
SK-expression.
Proof of Lemma:
Assume false. Of all the simple expressions that do not have SK-equivalents,
pick one (Lx.A) of minimal length. So all simple expressions shorter than Lx.A
do have SK-equivalents.
Expression A must have one of two forms: a variable v, or an application
(B C). It cannot have the form Ly.D because Lx.A is simple. Case analysis:
(1) A = v where v ~= x: Lx.A = Lx.v = Kv. So Lx.A has an SK-equivalent.
(2) A = v where v = x: Lx.A = Lx.x = I = SKK. So Lx.A has an SK-equivalent.
(3) A = BC: Lx.A = Lx. B ( C )
= Lx. (Lx.B) x ( (Lx.C) x ) since B = (Lx.B)x
= Lz. (Lx.B) z ( (Lx.C) z )
= S(Lx.B)(Lx.C)
Now, Lx.B and Lx.C are both shorter than Lx.A, so they have SK-equivalents.
Denote these by B' and C'. Lx.A = S(B')(C'). Again, Lx.A has an
SK-equivalent.
Thus, the Lemma cannot be false.
Proof of Theorem:
Given any general lambda expression E, pick an "innermost" Lx. That is, find a
contained simple lambda expression. If there is none, then E is already an
SK-expression. If you find one, replace it with an SK-equivalent. This
reduced the number of Lx. constructs by one. Repeat. Done.
------------------------------------------------------------------------
Applying the above construction (with shortcuts) we get
Lxy. x y = S (K(S(SKK))) (S(KK)(SKK))
Presumably this could be simplified, but I'm too lazy at the moment.
-- Craig
|