SKI combinator calculus of `2 = λf.λx.f(f x)`

Question

EDIT: refactored this question into a slightly different, but related one: Rules for converting lambda calculus expressions to SKI combinator calculus expression? Which rule(s) is/are incorrect?

---

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. λx.c = Kc
3. λx.(y z) = S (λx.y) (λx.z)

They mention $2 = \lambda f.\lambda x.f(fx)$, and then proceed to convert the "inner part", i.e. $\lambda x.f(fx)$, into the equivalent SKI combinator calculus as follows:

  λx.f(f x)
= S (λx.f) (λx.(f x))          (case 3) <- mistake???
= S (K f)  (S (λx.f) (λx.x))   (case 2, 3)
= S (K f)  (S (K f) I)         (case 2, 1)

Have they made a mistake? When using 3. they are taking f x, equating it to z in λx.(y z) = S (λx.y) (λx.z), and then getting S (λx.f) (λx.(f x)), but that seems off since x is now a bound variable in (λx.(f x)) when it shouldn't be?

---

Is this the correct way:

  λx.f(f x)
= S (λx.f) (λx.(f a))          (relabel x to a to avoid conflict, case 3)
= S (K f)  (S (λx.f) (λx.a))   (case 2, 3)
= S (K f)  (S (K f) (K a))     (case 2, 2)

---

Which is correct?

---

Indeed, could their 3. be elaborated on further as follows to employ the kestrel, $K$:

3'. λx.(y z) = S (λx.y) (λx.z) = S (Ky) (Kz)?

If we include a 4. as:

4. K(c d) = λx.(c d) = S (Kc) (Kd) (apply 2. then 3'.)

then the conversion of the inner part of $2$ would be simpler:

  λx.f(f x)
= S (Kf) (K(f x))          (case 3')
= S (Kf) (S (Kf) (Kx))     (case 4)

Is the above valid? Are 3'. and 4. valid? and is the subsequent conversion valid?

---

Could both be correct? I.e. are their conversion and my conversion, S (Kf) (S (Kf) I) and S (Kf) (S (Kf) (Kx)) respectively, equivalent? I put both expressions through an online SKI combinator interpreter and got slightly different things: (x0->f(f(x0))) and (x0->f(f(x))) respectively. I also applied y to both conversions and got different things, f(fy) and f(fx) respectively:

• S (Kf) (S (Kf) I) y = f(fy)

  S (Kf) (S (Kf) I) y
= (Kf) y (S (Kf) I y)
= f ((Kf) y (Iy))
= f (f y)

• S (Kf) (S (Kf) (Kx)) y = f(fx)

  S (Kf) (S (Kf) (Kx)) y
= (Kf) y (S (Kf) (Kx) y)
= f ((Kf) y ((Kx) y))
= f (f x)

I think that means I've made a mistake in:

3'. λx.(y z) = S (λx.y) (λx.z) = S (Ky) (Kz)

or

4. K(c d) = λx.(c d) = S (Kc) (Kd)

But I'm not sure where.