# Proving a combinator is a fixed point

Show that the term ZZ where Z is λz.λx. x(z z x) satisfies the requirement for fixed point combinators that ZZM =β M(ZZM).

-
@Jack: What are your thoughts so far? –  Mike Spivey Nov 23 '10 at 1:48
Honestly, i'm pretty lost. I'm not too clear with Beta reductions to begin with, and this problem just seems to be way over my head. –  jack Nov 23 '10 at 2:17

Show that the term ZZ where Z is λz.λx. x(z z x) satisfies the requirement for fixed point combinators that ZZM =β M(ZZM).

You are given a term $Z^2 = ZZ$ where $Z = \lambda z . \lambda x . ~ x ~ (z ~ z ~ x)$ and asked to prove that $Z^2$ satisfies the equality $Z^2M ~ =_{\beta} ~ M(Z^2M)$. In order to demonstrate that $Z^2$ satisfies the equality, it suffices to show that $Z^2M$ $\beta$-reduces to $M(Z^2M)$ (modulo renaming of bound variables):

$Z^2M ~=_{\beta} ~ ((\lambda z .\lambda x.~x~(z~z~x))(\lambda z .\lambda x.~x~(z~z~x)))~ M$

$~~~~~~~~~~=_{\beta}~ (\lambda x.~x~((\lambda z .\lambda x.~x~(z~z~x))~(\lambda z .\lambda x.~x~(z~z~x))~x)~M$

$~~~~~~~~~~=_{\beta}~ M~((\lambda z . \lambda x . ~x~(z~z~x))~(\lambda z.\lambda x.~x(z~z~x)) ~ M)$

$~~~~~~~~~=~M~(Z^2 ~ M)$

Showing that the combinator satisfies the equality is simply a matter of $\beta$-reduction. For instance, the proof of the fixpoint theorem in $\lambda$-calculus is just the construction of such a combinator.

-

Hint: Expand ZZM using the definition of Z once (for the outer Z).

-