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).
Proving a combinator is a fixed point
-
2@Jack: What are your thoughts so far? – 2010-11-23
-
0Honestly, 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. – 2010-11-23
2 Answers
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).