Rules for converting lambda calculus expressions to SKI combinator calculus expression? Which rule(s) is/are incorrect?

Question

learnxinyminutes.com defines $I$, $K$, and $S$ as follows:

I x = x
K x y = x
S x y z = x z (y z)

Then they give the following correspondences to aid in the conversion between lambda calculus and SKI combinator calculus:

1. λx.x = I
2. EDIT: λx.c = Kc provided that x does not occur free in c (see Mark's answer)
3. λx.(y z) = S (λx.y) (λx.z)

I tried to expand on these correspondences as follows:

3'. λx.(y z) = S (λx.y) (λx.z) = S (Ky) (Kz) (apply 2. to λx.y and to λx.y)

4. λx.(y z) = K(y z) (apply 2. with c = yz)

But that lead to incorrect results when I used 3'. and 4. to convert the number $2$ from its lambda calculus representation $λf.λx.f(f x)$ to its SKI combinator calculus representation (see my previous question for the incorrect result). So that means that 3'. and/or 4. are incorrect. Which step or steps in 3.' and/or 4. are incorrect?

Answer 1

The rules are phrased imprecisely.

To be precise, consider the language of the $\lambda$ calculus extended with $S, K,$ and $I$. The rules provide an algorithm for taking a term $\lambda x . M$ in this language, where $M$ has no $\lambda$ abstractions in it, and outputting an equivalent term with no abstractions at all in it, where the free variables in the resulting term all occur free in $\lambda x . M$.

Rule 2 says that when $x$ and $c$ are distinct variables or when $c$ is either $S, K$ or $I$, we should rewrite $\lambda x . c$ as $Kc$. The equality in rule 2 only holds when $x$ does not occur free in $c$, so applying this rule out of context can lead to an incorrect result.

To simplify $2 \equiv \lambda f . \lambda x . f(fx)$, we would first simplify $\lambda x . f(fx)$. We would write this according to rule 3 as $S (\lambda x . f) (\lambda x . fx)$, which we would then rewrite as $S (Kf) (S (\lambda x . f)(\lambda x . x))$, which we would then rewrite as $S (Kf)(S (Kf) I)$. Note that we have eliminated the variable $x$ and all instances of $\lambda$ abstraction.

We then apply the rules to $\lambda f . S (Kf) (S (Kf) I)$, which would produce a lengthy but correct term. We would convert to $S (\lambda f . S (Kf)) (\lambda f . S (Kf) I)$. Note that $\lambda f . S (Kf)$ becomes $S (\lambda f . S) (\lambda f . Kf)$, which becomes $S (K S) (S (KK) I)$. And $\lambda f . S (Kf) I$ becomes $S (\lambda f . S (Kf)) (\lambda f . I) = S (S (K S) (S (KK) I)) (KI)$. So the final result should be $S (S (K S) (S (KK) I)) (S (S (K S) (S (KK) I)) (KI))$ unless I've messed something up (which is very plausible).

Edit: this is definitely not the most efficient algorithm for taking a closed term in the $\lambda$ calculus and producing an equivalent term in the SKI calculus, either in running time or in the size of the output. One optimisation which reduces output size is looking for opportunities to use $\eta$-reduction, such as with the term $\lambda x . fx$, which can be rewritten as $f$. Our algorithm instead rewrites it as $S (Kf) I$. But this technique is limited.

If you want to use SKI as a step in compiling a language which will be used in real-world software, it's critical that the translation not blow up the size of the code super-linearly. So it's a good thing that there is a linear time and linear space algorithm for doing this translation.

The trick is to add new combinators. The idea is this: First, extend the SKI combinators to a new, larger finite set $J$ of combinators. Then, come up with a linear time and linear space algorithm for taking $\lambda$ closed terms and turning them into $J$ closed terms. Then, substitute each term in $J$ for an equivalent term in the SKI calculus. Since there are only finitely many terms in $J$, the substitution step is also linear time and linear space.

In fact, this technique means that once we have found one complete set of combinators $J$ and a good technique for writing $\lambda$-terms as $J$-terms, we can use this technique to get the representation in terms of any other finite, complete set of combinators.