# 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?

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.

• Your questions seems to be answered below, but I have a question for you: why are you studying S,K,I combinators? What can they do, etc... Dec 12, 2021 at 23:51
• Re: why I’m studying them: I went down a rabbit hole. I was originally studying $\lambda$-calculus, then fixed-point combinators, then … I noticed errors, but wanted another set of eyes to check my work so.I asked this question. Re: the second question: “What can they do?”. I’m not sure — I’m not the best person to answer that. Dec 12, 2021 at 23:56

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}

• Thanks! What does the $^*$ in $\rightarrow^*_{\beta}$ mean? Dec 12, 2021 at 17:23
• @joseville - The symbol $\to_\beta^*$ stands for the reflexive-transitive closure of $\to_\beta$. Concretely, it means an arbitrary number (possibly $0$) of $\to_\beta$ steps. For instance, $(\lambda x. xx) \lambda y.y \to_\beta^* \lambda y.y$ because $(\lambda x. xx) \lambda y.y \to_\beta (\lambda y.y)\lambda y.y \to_\beta \lambda y.y$. Dec 12, 2021 at 19:20
• @joseville - I edited my answer to show what, in my opinion, is the source of the typo in nLab's page. Dec 12, 2021 at 23:40
• Thanks for the edit! Doesn’t $\lambda y.(\lambda x.xx)(\lambda x.y(xx))$ $\beta$-reduce to $Y$ when you apply $(\lambda x.xx)(\lambda x.y(xx))$? Dec 13, 2021 at 0:01
• @joseville - You're right! Sorry, I misread the parentheses that I wrote myself! I re-edited that part of my answer, pointing to your new question about the source of the error in nLab. When I'll have time to check it, I'll answer your new question, if it will still be open. Dec 13, 2021 at 0:06