The SKI basis — λ-calculus

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

\displaystyle \mathrm{S}

\displaystyle = \lambda x\,y\,z.\,x\,z\,(y\,z), \qquad \mathrm{K}

\displaystyle = \lambda x\,y.\,x, \qquad \mathrm{I}

\displaystyle = \lambda x.\,x

(1.28)

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

\displaystyle \mathrm{S}\,\mathrm{K}\,\mathrm{K}

\displaystyle = \mathrm{I}

(1.29)

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

\displaystyle \mathrm{S}\,\mathrm{K}\,\mathrm{K}\,z \;

\displaystyle \to_\beta\; \mathrm{K}\,z\,(\mathrm{K}\,z) \;

\displaystyle \to_\beta\; z \;

\displaystyle =\; \mathrm{I}\,z.

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$ :

\displaystyle [x]\,x

\displaystyle = \mathrm{I}, \qquad [x]\,M

\displaystyle = \mathrm{K}\,M \;\;(x \notin \mathrm{FV}(M)), \qquad [x]\,(M\,N)

\displaystyle = \mathrm{S}\,([x]\,M)\,([x]\,N)

(1.30)

$[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}$ :

\displaystyle [x]\,(f\,x\,x)

\displaystyle = \mathrm{S}\,([x]\,(f\,x))\,([x]\,x)

\displaystyle = \mathrm{S}\,\bigl(\mathrm{S}\,([x]\,f)\,([x]\,x)\bigr)\,\mathrm{I}

\displaystyle = \mathrm{S}\,(\mathrm{S}\,(\mathrm{K}\,f)\,\mathrm{I})\,\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}$ .