8
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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... $\endgroup$ Commented Dec 12, 2021 at 23:51
  • 1
    $\begingroup$ 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. $\endgroup$
    – joseville
    Commented Dec 12, 2021 at 23:56

2 Answers 2

4
$\begingroup$

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}

$\endgroup$
8
  • $\begingroup$ Thanks! What does the $^*$ in $\rightarrow^*_{\beta}$ mean? $\endgroup$
    – joseville
    Commented Dec 12, 2021 at 17:23
  • 1
    $\begingroup$ @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$. $\endgroup$ Commented Dec 12, 2021 at 19:20
  • 1
    $\begingroup$ @joseville - I edited my answer to show what, in my opinion, is the source of the typo in nLab's page. $\endgroup$ Commented Dec 12, 2021 at 23:40
  • 1
    $\begingroup$ 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))$? $\endgroup$
    – joseville
    Commented Dec 13, 2021 at 0:01
  • 1
    $\begingroup$ @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. $\endgroup$ Commented Dec 13, 2021 at 0:06
0
$\begingroup$

As you noted, that's a mistake. So, some clarification...

Under η-equivalence, $S (K x) I = x$, so you can write $S (K S) (S (K K) I) = S (K S) K$, which is the $SKI$ definition of the $B$ combinator $$B = S (K S) K = λxλyλz·x (y z).$$ The combinator $D = S I I$ is just the "doubling" combinator $D = λx·x x$. Therefore, your expression is (up to η-equivalence): $$S (K(SII)) (S(S(KS)(S(KK)I))) (K(SII)) = S (K D) (S B) (K D).$$ This is β-equivalent to $K D (K D) (S B (K D)) = D (S B (K D))$. In general, $C x y = S x (K y)$, where $C = λxλyλz·x z y$, so this can also be written as $D (C B D)$ which is β-equivalent to $C B D (C B D) = B (C B D) D$.

For the combinator $Y = λf·(λx·f (x x))(λx·f (x x))$, you have $$ λx·f (x x) = λx·f (D x) = λx·B f D x = B f D,\\ λf·B f D = C (λf·B f) D = C B D,\\ Y = λf·B f D (B f D) = S (λf·B f D) (λf·B f D) = S (C B D) (C B D). $$

So, you can see clearly that the mistake was to forget the initial $S$ and to write $C B D (C B D)$ instead of $S (C B D) (C B D)$. Alternatively, you could write, in place of $D (C B D)$, the expression $W S (C B D)$, using the combinator $W = λxλy·x y y$. Alternatively, since $B f D (B f D) = D (B f D)$, then you could also write $$λf·B f D (B f D) = λf·D (B f D) = B D (λf·B f D) = B D (C B D).$$ So, you could just as well say that the initial $B$ was missing.

Under Combo, which I put up on GitHub, the expression above for $Y$ compiles as $S \_0 \_0$, where $\_0 = C B D$, because Combo never writes the same sub-term of any term twice. It never reduces the same term twice, so if you try to reduce $S (C B D) (C B D)$, with the extensionality axiom (a.k.a. η-rule) turned on, it will stop as soon as it see the cycle in the cyclic reduction. In effect, it goes like this: $$\begin{align} Y &= λf·(λx·f (x x)) (λx·f (x x))\\ &= λf·B f (λx·x x) (B f (λx·x x))\\ &= λf·B f D (B f D)\\ &= S (λf·B f D) (λf·B f D)\\ &= S (C (λf·B f) D) (C (λf·B f) D)\\ &= S (C B D) (C B D)\\ &→ λf·S (C B D) (C B D) f\\ &→ λf·C B D f (C B D f)\\ &→ λf·B f D (B f D)\\ &→ λf·f (D (B f D))\\ &→ λf·f (B f D (B f D))\\ &⇒ λf·f (f (f (⋯)))\\ &= U (λf·(f (f (⋯)))\\ &⇒ U (U (U (⋯))) \end{align}$$ except it only writes out the sub-term it is currently working on, not the whole thing, and does not show the compilation of the λ-terms into combinators.

It stops short of the first infinite "co-inductive" step $⋯ ⇒ ⋯$ and reports that $B f D (B f D)$ is a "cyclic term". If it had co-induction and rational infinite λ-terms built into it, then it would have proceeded onward as indicated above, with the final result involving the combinator $U = λxλy·y (x y)$. But that's something still slated for future upward revision. At the time of writing, however, it still blocks the reduction at $B f D (B f D)$ (which it actually writes as $B \#0 D (B \#0 D)$) and reports a "cyclic term", after 4 combinator reductions and 1 η-rule step.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .