Is $S(K (S I I))(S(S (K S)(S(K K)I)))(K (S I I))$ really a fixed-point combinator or is this a typo?

Question

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.

Answer 1

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}