Missing parentheses in $s(k (s I I))(s(\lambda y. s(k y))(\lambda y. s I I)$ leads to interesting error in “nLab” page. Need a double check.

Solution 1:

I totally agree that what you have noticed is the only error among the equivalences, well spotted!

A missing parenthesis leads to the completely wrong conclusion that $S(K(SII))(S(S(KS)(S(KK)I)))(K(SII))$ is a fixed point combinator! A proof that $S(K(SII))(S(S(KS)(S(KK)I)))(K(SII))$ is not a fixed point combinator is here.


To @mohottnad: Equivalence $(1)$ is$-$quite surprisingly$-$correct! Indeed,

$$Y = \lambda y. (\lambda x. y(xx)) (\lambda x. y(xx))$$ and we have that \begin{align} \lambda x. y(xx) &=_\beta S(Ky)(SII) \\ \lambda x.xx &=_\beta SII \end{align} Since $(\lambda x.xx)(\lambda x.y(xx)) =_\beta (\lambda x.y(xx))(\lambda x.y(xx))$, we can conclude that \begin{align} Y &=_\beta \lambda y.(\lambda x.xx)(\lambda x.y(xx)) \\ &=_\beta \lambda y.(SII)(S(Ky)(SII)) \end{align}

I agree that the explanation on nLab's page could be a bit more lengthy and thorough. At first sight, I was convinced that equivalence $(1)$ was wrong, too.


An emended version of the equivalences in nLab's page about partial combinatory algebra, Point 4 in section Examples of Combinators, would be the following:

\begin{align} Y & =_\beta \lambda y. (S I I)(S(K y)(S I I)) \\ & =_\beta S(\lambda y. S I I)(\lambda y. S(K y)(S I I)) \\ & =_\beta S(K(S I I)) \big(S(\lambda y. S(K y))(\lambda y. S I I)\big) \\ &=_\beta S(K(SII)) \big(S(S(KS)K)(K(SII))\big) \end{align}

where, in the last equivalence, we used the fact that \begin{align} S(S(KS)K)(K(SII)) &\to_\beta^* S (\lambda y.(KSy)(Ky)) (K(SII)) \\ &\to_\beta^* S (\lambda y. S(Ky)) (K(SII)) \\ &\to_\beta S(\lambda y. S(K y))(\lambda y. S I I) \end{align}

Therefore, $S(K(SII)) \big(S(S(KS)K)(K(SII))\big) $ is a fixed point combinator, and this is consistent with Wikipedia's page about fixed point combinators.