Exercise 20
(a) Construct a λ-term $M$ such that $M=_β λxy. x M y$.
(b) Construct a λ-term $M$ such that $M xyz=_β xyzM$.
(a) To solve this equation, we first define an abstraction of the expression as follows.
$$ L := λz (λxy. x z y)$$
Which means
$$\begin{align} L M & =_β λxy. xMy \\ \\ & =_β M \end{align}$$
So if we can find an $M$ such that $LM =_β M$ then this $M$ is a solution to the given equation. The fixed point theorem guarantees such an $M$ exists.
One way to construct that $M$ is to use the Curry fixed point combinator $Y$, defined as follows.
$$Y := λy. (λx. y(xx))(λx. y(xx))$$
The key property of $Y$ is that
$$YL =_β L(YL)$$
So if we construct
$$M := YL$$
we can check this $M:= YL$ is a solution
$$\begin{align} M & =_β (YL) \\ \\ & =_β L(YL) \\ \\ & =_β LM \\ \\ & =_β λxy. xMy \qquad \Box \end{align}$$
(b) We'll start from the expression that will make use of the abstraction $L$ we'll construct.
$$ M =_β LM $$
Using the given $M xyz =_β xyz M$, we have
$$M xyz =_β LM xyz =_β xyz M$$
This means $L$ must be
$$L := λaxyz . xyza$$
The key property of the Curry fixed point combinator $Y$ is
$$YL =_β L(YL)$$
So if we set
$$ M := YL $$
then we can check this $M:=YL$ is a solution
$$\begin{align} Mxyz & =_β (YL) xyz \\ \\& =_β L(YL) xyz \\ \\ & =_β LM xyz \\ \\ & =_β xyzM \qquad \Box \end{align}$$
