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

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.

• The first definition "motivates" the second because it is what you get if you apply the standard translation of the $\lambda$-calculus into combinatory logic. So I don't really understand what you are asking. Feb 29 at 20:50
• @RobArthan actually I have only started learning about lambda calculus for a few months. I was unaware of a "standard translation". But thanks for your insight, I will surely try to read further about the topic. Mar 1 at 8:13
• Sorry if I sounded a bit harsh. You might like to look at the original work of Schönfinkel who invented combinatory logic. I think the motivation was to introduce combinators to remove the need for bound variables in logic along the same lines as the introduction of functionals (like the integration and differentiation operators) that remove the need for bound variables in analysis. Mar 1 at 20:36
• There's really no need to say sorry. I know that I am inexperienced in this field, but I would like to study further. My current understanding is that the functional structure allows us to think about what is being done on a variable in a general scale, not only on a particular variable, and also allows us to pass functions as arguments. Is this idea correct? @RobArthan Mar 2 at 5:29
• Not having bound variables makes substitution of terms for free variables completely unproblematic, whereas if you are substituting inside the scope of a $\lambda$, you need to take special measures to avoid variable capture problems. I admit that the reduction to combinatory logic can make things harder to understand (your example with $Y$ becomes even worse if you remove $I$ using $I = SKK$). I don't think either of the two formalisms is better or worse than the other: they are just two interesting ways of approaching the concept of an abstract function. Mar 2 at 21:20

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.

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.

• +1. Thanks for having spent time on this question. Mar 10 at 15:06