I was reading nLab’s article on fixed-point combinators and it mentions that
$$Y = S(K (S I I))(S(S (K S)(S(K K)I)))(K (S I I))$$
is a fixed-point combinator.
However, when I convert it to a lambda calculus term using SKI combinator interpreter, I get the output:
(x0->(x1->x0(x0)(x1(x1))))
Or equivalently,
$$\lambda xy.(xx)(yy)$$
which, as far as I can tell, is not a fixed-point combinator.
I also confirmed as much by doing the conversion by hand by using:
- $S = \lambda xyz.(xz)(yz)$
- $K = \lambda xy.x$
- $I = \lambda x.x$
It was tedious, but my general approach was to evaluate simple terms and build on top of that. Here’s the outline:
- $(SII) = \lambda z.zz$
- Then $A = (K\ (SII)) = \lambda yz.zz$
- $(KK) = \lambda y.K$
- Then $B = (S\ (KK)\ I) = \lambda zy.z$
- $(KS) = \lambda y.S$
- Then $C = (S\ (KS)\ B) = \lambda z.(S\ (\lambda y.z))$
- Then $D = (S\ C) = \lambda yzc.(z\ ((yz)\ c))$
- Then $Y = S\ A\ D\ A = (AA)(DA) = (\lambda z.zz)(\lambda zc.z(cc)) = \lambda cz.(cc)(zz) = \lambda xy.(xx)(yy)$
There is a similar SKI combinator that’s also quoted (in other sources) as being a fixed-point combinator:
$$Y = S(K(SII))(S(S(KS)K)(K(SII)))$$
and I have confirmed that it is a fixed-point combinator. I converted it by hand and it is equivalent to:
$$\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$
which is the $Y$-combinator, which is ofc a fixed-point combinator. (Unfortunately, the “SKI combinator interpreter” can’t help as it encounters an infinite loop: Reduction error: over 1000 steps, infinite loop? which is understandable given that there’s no $\beta$-normal form of the $Y$-combinator and if we assume that the interpreter only terminates when there are no more $\beta$-reductions to perform.
Best Answer
There is a typo in nLab's page about fixed point combinators, the term $S (K(SII)) (S(S(KS)(S(KK)I))) (K(SII))$ is not a fixed point combinator.
Indeed, the $\lambda$-term $S (K(SII)) (S(S(KS)(S(KK)I))) (K(SII))$ (where $K$, $S$ and $I$ are interpreted by the $\lambda$-terms you wrote) $\beta$-reduces in several steps to the $\beta$-normal form $\lambda xy.xx(yy)$ (in accordance with SKI interpreter, as you correctly wrote, see below for a proof). This is in contradiction with the fact that every fixed point combinator is not $\beta$-normalizable (see below for a proof).
The source of the error in nLab's page seems to be Point 4 in the example of combinators on nLab's page about partial combinatory algebra. See here for a proper discussion.
Let us show that every fixed point combinator $P$ is not $\beta$-normalizable, that is, there is no $\beta$-normal form $N$ such that $P \to_\beta^* N$ (as usual, $\to_\beta^*$ is the reflexive-transitive closure of $\beta$-reduction step $\to_\beta$: thus, $P \to_\beta^* N$ means that $P$ $\beta$-reduces to $N$ in several $\beta$-reduction steps).
Assume, for the sake of contradiction, that $P$ is $\beta$-normalizable, that is, $P \to_\beta^* N$ for some $\beta$-normal form $N$. It is easy to show that for every $\beta$-normal term $M$ and every variable $x$, $Mx$ is $\beta$-normalizable. Let $N'$ be the $\beta$-normal form of $Nx$. By definition of fixed point combinator, for every variable $x$, one has $Px =_\beta x(Px)$ ($=_\beta$ is $\beta$-equivalence, the symmetric and reflexive-transitive closure of $\to_\beta$), hence $Nx =_\beta x(Nx)$ and so $N' =_\beta xN'$. Both $N'$ and $xN'$ are $\beta$-normal, thus by confluence from $N' =_\beta xN'$ it follows that $N' = xN'$ (they are syntactically equal, up to $\alpha$-conversion), which is clearly impossible.
Let us show that $S (K(SII)) (S(S(KS)(S(KK)I))) (K(SII))$ (where $K$, $S$ and $I$ are interpreted by the $\lambda$-term you wrote) $\beta$-reduces to the $\beta$-normal form $\lambda xy.xx(yy)$.
Note that the starting term is the application of $S$ to three arguments:
first argument, $K(SII)$;
second argument, $S(S(KS)(S(KK)I))$;
third argument, $K(SII)$.
Let us see how these arguments $\beta$-reduce separately.
The first and third arguments $\beta$-reduce as follows:
\begin{align} K(SII) &\to_\beta \lambda y.(SII) \to_\beta^* \lambda yz. Iz(Iz) \to_\beta^* \lambda yz.zz \end{align}
Concerning the second argument, this is the application of $S$ to $S(KS)(S(KK)I)$. Now, \begin{align} S(KK)I &\to_\beta^* \lambda z. KKz(Iz) \to_\beta \lambda z. KKzz \to_\beta^* \lambda z. Kz \to_\beta^* \lambda z y. z = K \\ S(KS)(S(KK)I) &\to_\beta^* S(KS)K \to_\beta^* \lambda z. KSz(Kz) \to_\beta^* \lambda z. S(Kz) \to_\beta \lambda z. S (\lambda y.z) \end{align}
Therefore, \begin{align} S\big(S(KS)(S(KK)I)\big) &\to_\beta^* S \lambda z. S (\lambda y.z) \to_\beta \lambda yz. (\lambda z'.S(\lambda y'.z'))z (yz) \\&\to_\beta \lambda yz. S(\lambda y'.z)(yz) \to_\beta^* \lambda yzz'.(\lambda y'.z)z' (yzz') \\ &\to_\beta \lambda yzz'.z (yzz') \end{align}
Putting everything together, we have \begin{align} S (K(SII)) (S(S(KS)(S(KK)I))) (K(SII)) &\to_\beta^* S (\lambda yz.zz) (\lambda yzz'.z (yzz')) (\lambda yz.zz) \\ &\to_\beta^* (\lambda yz.zz) \lambda yz.zz\big((\lambda yzz'.z (yzz'))\lambda yz.zz \big) \\ &\to_\beta (\lambda yz.zz) \lambda yz.zz\big(\lambda zz'.z ((\lambda yz.zz)zz') \big) \\ &\to_\beta^* (\lambda yz.zz) \lambda yz.zz\big(\lambda zz'.z (z'z') \big) \\ &\to_\beta (\lambda z.zz) \big(\lambda zz'.z (z'z') \big) \\ &\to_\beta (\lambda zz'.z (z'z')) \lambda zz'.z (z'z') \\ &\to_\beta \lambda z'. (\lambda zx.z (xx))(z'z') \\ &\to_\beta \lambda z'x. (z'z')(xx) \end{align}