An exercise on combinatory logic

Question

Can somebody help me with the following exercise?

(1) Find a combinator $X$ such that $Xy = X$; (2) Find a combinator in normal form with the same property. Rules for reduction are

• $Ix > x$
• $Kxy > x$
• $Sxyz > xz(yz)$
• $x > x$
• if $x > x'$ then $Zx > Zx'$
• if $x > x'$ then $xZ > x'Z$
• if $x > y$ and $y > z$ then $x > z$

Equality is the relation generated by reduction and inverse reduction, namely by the previous rules with $=$ in place of $>$ plus

• if $x = y$ then $y = x$.

Abstraction is defined as follows

• $[x]x$ identical with $I$
• $[x]M$ identical with $KM$ if $x$ does not occur in $M$
• $[x]Ux$ identical with $U$ if $x$ does not occur in $U$
• $[x]UV$ identical with $S([x]U)([x]V)$ if the previous cases cannot be applied.

Now, (1) has the simple solution $K(FK)$ where $F$ is a fixed-point combinator. But such a solution does not work for (2) since, if for example one takes $F$ as the Curry fixed-point combinator, $F$ stands for $SWW$ for a certain W and so $K(FK)$ stands for $K(SWWK)$, which is not normal. I can't see how to solve (2).

The author suggests to use a modified version of abstraction, where the second clause is restricted to $M$ atomic, and the third clause is either restricted to $U$ atomic or dropped out.

Any idea?

Answer 1

Hmm, it was not as straightforward as I had expected, but here is a way through. Suppose $W$ is some term in normal form and we want to find a normal form $X$ such that $Xy=(WX)y$. (For this particular exercise we can take $W=K$, of course).

As long as we're not caring about normal forms, this is fairly easy. Remembering the Y-combinator we can use $$ X \approx (\lambda f.(\lambda x.f(x x))(\lambda x.f(x x))) W $$ To rewrite that into combinator form, let's assume for simplicity that we have a combinator $D$ with reduction rule $$ D a \to a a $$ Then, simplifying a bit, we get $$ \begin{align}X &\equiv ([x] W(D(x)) ([x] W(D(x)) \\ &= D([x] W(D(x)) \\ &\equiv D(S(KW)D) \end{align}$$ This works excellently: $$ \begin{align}Xy \equiv D(S(KW)D)y &\to \big(S(KW)D\,(S(KW)D)\big) y \\ &\to (KW(S(KW)D))(D(S(KW)D)) y \\ &\equiv (KW(S(KW)D)) X y \\ &\to W X y \end{align} $$ The only trouble is that $D (S(KW)D)$ is not a normal form. But notice that the only place in the above reduction where we use the $D$ reduction is the very first reduction, when $D(S(KW)D)$ does not stand alone but is followed by a $y$! So if we change our reduction rule for $D$ to $$ D a b \to (aa)b $$ the reduction sequence above still goes through, and now $D(S(KW)D)$ is a normal form!

Unfortunately we can't just add new combinators willy-nilly. so we have to express $D$ using existing combinators. This means that we can't quite get $D M$ to be a normal form itself, but as long as we can make sure that $D M$ has a normal form whenever $M$ has, that will be good enough for us.

First, things will be slightly simpler if we let $D_0 \equiv [a]aa \equiv SII $. Then we take a deep breath, write things down with abstractions, and crank the combinatorfying handle: $$ \begin{align} D &\equiv [a][b] D_0 a b \\ &\equiv [a] S ([b] D_0 a) ([b] b) \\ &\equiv [a] S(S(K D_0)(K a)) I \\ &\equiv S(S(KS)(S(S(KS)(K(K D_0))(K K)))(KI) \end{align} $$

The important part here is to resist the temptation to write $K(D_0 a)$ instead of $S(K D_0)(K a)$ to represent $[b]D_0 a$ in the second line of this, because that would make $D_0$ meet $a$ without waiting for a $b$ to be supplied, and we would have gained nothing. Once we do resist, however, we do have $$ D(S(KW)D) \to^* S(S(K D_0)(K (S(KW)D))I $$ which is a normal form that we can use as our $X$.

---

To get a slightly shorter solution for the particular case of $Xy=X$, we can note that when $W=K$, we don't actually need to carry the $y$ through all of the reductions because it's just going to be ignored by the $K$ in the end anyway, so it should be possible instead of $D$ to work with an $E$ with the reduction rule $$ Eab \to aa $$ Indeed in that case, $X=EE$ works right out of the box in a single reduction!

We can then parallel the development of $D$ above: $$ \begin{align} E &\equiv [a][b]D_0 a \\&\equiv [a]S(K D_0)(K a) \\&\equiv S(K(S(K D_0)))K\end{align}$$ and pre-reduce $EE$ to get $$ \begin{align} EE &\equiv S(K(S(K D_0)))K E \\&\to K(S(K D_0))E (K E) \\&\to S(K D_0) (K E) \\&\equiv \fbox{S(K(SII)) (K(S(K(S(K(SII))))K))} =: X \end{align}$$

We can see this reduce in practice: $$ \begin{align} Xy &\equiv S(K D_0)(K E)y \\&\to (K D_0 y)(K E y) \\&\to^* D_0 E \\&\equiv SIIE \\&\to^* EE \\&\to^* X \qquad\text{as above} \end{align} $$

Answer 2

In an extended version of Hindley's book I am reading (I'm dealing with "Introduction to combinatory logic", while the extended version is "Lambda calculus and combinators. An introduction") I have found the following remark.

Let us re-define abstraction in the following way:

• $[x]^*x$ identical to $I$
• $[x]^*M$ identical to $KM$ if $M$ is atomic different from $x$
• $[x]^*Ux$ identical to $U$ if $U$ is atomic different from $x$
• $[x]^*UV$ identical to $S([x]U)([x]V)$ if the previous cases cannot be applied.

Then, for every $X$, $[x]^*X$ is a weak normal form. By induction on the complexity of $X$, the atomic cases being trivial and the induction step being a simple application of the induction hypothesis.

With this remark, and by bearing in mind the theorem

$([x]^*X)Y > [Y/x]X$

(which therefore also holds for this re-defined abstraction, as easily provable - actually more simply then the previous abstraction) we can choose $[y]^*F([x, y]^*x)$, with $F$ fixed-point combinator. Such a term is normal according to the remark. By the theorem

$([y]^*F([x, y]^*x))y = F([x, y]^*x)$

and

$F([x, y]^*x) = ([x, y]^*x)(F([x, y]^*x)) = [y]^*F([x, y]^*x)$.