Defining the Y combinator in terms of S, K and I

Question

We know that the Y-combinator is defined as: $$\text{Y}:=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$

Wikipedia says :$$\text{Y}:=\text{S(K(SII))(S(S(KS)K)(K(SII)))}$$

Now the question is: What logical steps can we take to convert the first definition to the second?

While it is easy to show the equivalence between the two definitions, finding how the first definition can motivate and lead to the second definition is, in my opinion, a tricky task. I have added my proof as an answer, but all other ideas and suggestions are welcome.

Answer 1

Let's define $$\text{E}=\lambda\text{x. f (x x)}$$ which leads to:

$$ \begin{align*} \text{E x}&=\text{f (x x)}\\ &=\text{f (I x (I x))}\\ &=\text{f (S I I x)}\\ &=\text{(K f x) (S I I x)}\\ &=\text{S (K f) (S I I) x}\\ &=\text{(K S f) (K f) (S I I) x}\\ &=\text{S (K S) K f (S I I) x}\\ &=\text{S (K S) K f (K (S I I) f) x}\\ &=\text{S (S (K S) K)(K (S I I)) f x}\\ \therefore \text{ E}&=\text{S (S (K S) K)(K (S I I)) f}\\ &=\text{T f [Let]} \end{align*} $$

Now $\text{Y}=\lambda\text{f. E E}$, so: $$\begin{align*} \text{Y f}&=\text{E E}\\ &=\text{T f (T f)}\\ &=\text{S T T f}\\ \therefore\text{ Y}&=\text{S T T}\\ &=\text{S S I T}\\ &=\text{S S I (S (S (K S) K)(K (S I I)))}\\ &=\text{S (K (S I I)) (S (S (K S) K)(K (S I I)))} \end{align*}$$

Note: See this for why $\text{SSI}$ and $\text{S(K(SII))}$ are equivalent.

Answer 2

Define $D = S I I$, $B = S (K S) K$ and $V = S B (K D)$. Then, your definition is $Y = S (K D) V$. Since $D x = S I I x = I x (I x) = x x$, then, when applied to $f$, this is equivalent to $$S (K D) V f = K D f (V f) = D (V f) = V f (V f) = S V V f.$$ Thus, under the η-rule, $$S (K D) V = λf·S (K D) Vf = λf·S V V f = S V V.$$ Actually, if you go with strict $SKI$ abstraction, then $S V V$ is what the article should be citing, not $S (K D) V$.

First, $$f(x x) = K f x (D x) = S (K f) D x\quad⇒\quadλx·f(x x) = λx·S (K f) D x = S (K f) D.$$ Second, $$S (K f) = K S f (K f) = S (K S) K f = B f,\quad D = K D f.$$ Therefore $$S (K f) D = B f (K D f) = S B (K D) f = V f.$$ Thus, it follows that $$λf·(λx·f (x x))(λx·f (x x)) = λf·(V f)(V f) = λf·S V V f = S V V.$$

Under the combinator engine Combo, which I put up on GitHub, the abstraction algorithm uses a wider range of combinators, including $D$ and $B$. If will yield $S \_0 \_0$, where $\_0 = C B D$, since $C a b = S a (K b)$ (under the η-rule), where $C = λxλyλz·x z y$. Therefore, $\_0 = V$. If you run Combo on $V = S B (K D)$ with the extensionality axiom (the η-rule) turned on, it will give you $C B D$.

If you run it on $S (C B D) (C B D)$ with, extensionality turned on, it will block it and report it as a "cyclic term", recognizing that it reduces as $Y = λf·Y f = λf·f (Y f)$, which leads to an infinite reduction. If I get around to upgrading Combo to generate, accept and process rational infinite lambda terms, then it might eventually be able to state that $Y$ has $λf·f(f(f(⋯))$ as a normal form, establishing this result in the same finite number of steps that it currently takes to recognize it's a cyclic term in its current version.