The SKI basis

The λ-calculus itself can be built on just three of them — S, K and I. In combinatory logic they are taken as primitives:

And I is not even needed as a primitive — it is expressible through S and K:

Let us substitute and prove the formula — expand $\mathrm{S}\,\mathrm{K}\,\mathrm{K}$ on an arbitrary argument $z$ using the definitions (1.28):

For any $z$ we get $z$ — exactly what $\mathrm{I}$ does, so $\mathrm{S}\,\mathrm{K}\,\mathrm{K}$​${} = \mathrm{I}$.

Any λ-term is translated into combinators mechanically. A term is built in three ways — a variable, an application and an abstraction; variables and applications already exist in combinatory logic, but abstraction has to be eliminated. This is done by bracket abstraction — the operation $[x]\,M$, “pull the variable $x$ out of the term $M$”. Its result is a combinator term in which $x$ no longer occurs but which, if given $x$ back, reduces to $M$ again. It is defined by the shape of the body $M$:

• $[x]\,x$​${} = \mathrm{I}$: the body is $x$ itself; returning the argument unchanged is exactly what $\mathrm{I}$ does.
• $[x]\,M$​${} = \mathrm{K}\,M$ when $x$​${} \notin \mathrm{FV}(M)$: the body does not depend on $x$, so the given argument is simply discarded.
• $[x]\,(M\,N)$​${} = \mathrm{S}\,([x]\,M)\,([x]\,N)$: in an application $x$ may hide in both $M$ and $N$, so the argument must be handed to both — which is exactly what $\mathrm{S}$ does.

If the body is itself an abstraction $\lambda y.\,M$, the inner variable is removed first and the outer one after: $[x]\,(\lambda y.\,M)$​${} = [x]\,([y]\,M)$; thus nested $\lambda$ are stripped from the inside out until only variables and applications remain.

Take $\lambda x.\,f\,x\,x$. The body $f\,x\,x$ is an application $(f\,x)\,x$, so we unwind it with the application rule, reducing everything to $\mathrm{S}$, $\mathrm{K}$, $\mathrm{I}$:

There are no variables in the result — only $\mathrm{S}$, $\mathrm{K}$, $\mathrm{I}$ and the free $f$: $\lambda x.\,f\,x\,x \;$​${} \rightsquigarrow\; \mathrm{S}\,(\mathrm{S}\,(\mathrm{K}\,f)\,\mathrm{I})\,\mathrm{I}$.