Learning the Lambda Calculus, lambda -> ski

We have seen both SKI and the lambda calculus, and the fact that they are the same. I want to go deeper into this connection between them because I'm doing a project for my Artificial Intelligence 2 class where I've decided to prove their equivalence with a proof assistant called Coq.

Before going over the proof (which is very easy), notice that there are many combinators besides S, K, and I. We have seen Y, but other cool ones are B = (\f.\g.\x.f(gx)), which composes two functions called f and g here (this is called "." in Haskell to mimic the notation in math of a small unfilled circle), and C = (\f.\x.\y.fyx) which swaps two arguments of a function (called flip in Haskell). These are cool because they give nice little transformations and show how combinators (and the lambda calculus in general) express control flow. Concatenative languages can be considered the composition of combinators in a cool way. Also, combinators appear in the compilers for functional languages. Very cool things, them.

So, the proof. The lambda calculus is a system of universal computation, so it can compute anything that can be computed (by definition). If we can turn any term of the LC into a term of the SKI combinatory calculus that is equivalent. There is some difficulty with the notion of equality here- the translation is not a simple bijection as a lambda term translated into SKI can be translated back, but it will not always be the same term. We may take an intensional notion of equality (an intentional equality considers terms to be equal if they are exactly the same syntactically) but this will not work in general. Remember that not all reduction terminate in the lambda calculus- that is one of the reasons type systems exist. To test if two terms are exactly the same syntactically we could want to reduce then to their normal form (as all normal forms are unique and therefore are a sort if "identity" for a term). This computation of the normal form may not terminate, and therefore we can't use this notion of equality. On the other hand, we can use an extensional notion of equality- terms are equal if they work the same in all possible uses. While intensional equality is concerned with the "internal" representation of the term, extensional equality is concerned with the "external" behavior of a term. The translation that we will be looking at may not get us back where we started, but it will get us somewhere equal to where we started if we consider terms equal if they behave the same way.

The actual translation is by cases. This is very easy to express in Haskell, so I've just now written a translator from SKI to lambda calculus and back, as well as a function to reduce an SKI and a function to reduce a lambda term, both by only one reduction (again, if we keep reducing until we are done we may never terminate as in the case of the term (\x.xx)(\x.xx)).

In code we have:
data SKI = S | K | I | App SKI SKI | Var Id deriving (Show, Eq)
data Lambda = LVar Id | LApp Lambda Lambda | Abs Id Lambda deriving (Show, Eq)
As data, and for the translation:
fv (Var id) = [id]
fv (App e1 e2) = fv e1 ++ fv e2
fv _ = []

freeIn id term = id `elem` fv term

lambda2ski :: Lambda -> SKI
lambda2ski (LVar id) = Var id
lambda2ski (LApp e1 e2) = App (lambda2ski e1) (lambda2ski e2)
lambda2ski (Abs id term) = lamb id $ lambda2ski term

lamb id term | not (id `freeIn` term) = App K term
lamb id (Var id') | id == id' = I
lamb id (App e1 e2) = App (App S (lamb id e1)) (lamb id e2)

This is the code only to translate one way, the other way is even easier. The function fv gets the list of free variables in a term, and the function freeIn tests if an identifier (a String) is a free variable in a term. Of course, lambda2ski does the translation, and lamb is a helper function to take care of lambda abstractions.

For those who do not know Haskell, the translation from Wikipedia is this:
1. T[x] => x
2. T[(E₁ E₂)] => (T[E₁] T[E₂])
3. T[λx.E] => (K T[E]) (if x does not occur free in E)
4. T[λx.x] => I
5. T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)
6. T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])

Where T[term] is the translation function applied to the term "term". Having embedded the lambda calculus in SKI we have proven it as a system of universal computation, assuming the extensional equality of the translated term with the original.

It is interesting that the reverse translation, also given on the wikipedia page for combinatory logic, will make the resulting lambda term longer than the original. For the terms I have played with, it seems like translating from the LC into SKI and back always makes the term larger, although I'm not making an attempt to do reductions at the moment.

Well, that was fun. Hopefully this works out nicely in Coq as well, and I can make the project a computer verified proof of this translation.