An exercise on combinatory logic 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?
 A: 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} $$
A: 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)$.
