Its really amazing that 3 basic functions could actually simulate all of the computing that we could possibly do with lambda calculus. But most of the times we dont understand how its possible.

When we say equivalence of SKI combinator calculus and lambda calculus, we mean two things. First that any SKI expression can be turned into a lambda expression. Second that any lambda expression can be turned into a SKI expression.

SKI to Lambda

The first part of equivalence is easy to establish. We just replace $S$, $K$ and $I$ with appropriate lambda expressions

For example: The equivalent expression for \((SKK)K\) is simple \(((\lambda x. \lambda y. \lambda z. (xz)(yz))(\lambda x. \lambda y. x)(\lambda x. \lambda y. x))(\lambda x. \lambda y. x)\)

Lambda to SKI

This side of the equivalence is bit tricky. The primary problem with SKI is that it doesnt allow unbound occurences of variables, the expressions in SKI have to be expressions like in programming languages. Infact the final expression we build would have no variables at all. This restriction not necessarily reduce the expressibility in any way.

We will do a step by step procedure with induction on the structure of lambda expression. Lets call that procedure convert

To verify that such a conversion is correct, we just have to do the reverse of it ie., replace $S$, $K$ and $I$ with their lambda forms in each case and find that we get back the same expression or an expression with same normal form.



To keep things simple, especially to handle the last case, we consider $S$, $K$ and $I$ to be part of lambda calculus itself. The complete code for such conversion is here