Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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).

share|improve this question
1  
@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
add comment

2 Answers

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

share|improve this answer
add comment

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.