create page
[lambda.git] / exercises / _assignment4_answers.mdwn
1 1. Find a fixed point `X` for the succ function:
2
3     H := \f.succ(ff)
4     X := HH 
5       == (\f.succ(ff)) H
6       ~~> succ(HH)
7
8 So `succ(HH) <~~> succ(succ(HH))`.
9
10 2. Prove that `add 1 X <~~> X`:
11
12     add 1 X == (\mn.m succ n) 1 X
13             ~~> 1 succ X
14             == (\fz.fz) succ X
15             ~~> succ X
16
17 What about `add 2 X`?
18
19     add 2 X == (\mn.m succ n) 2 X
20             ~~> 2 succ X
21             == (\fz.f(fz)) succ X
22             ~~> succ (succ X)
23
24 So `add n X <~~> X` for all (finite) natural numbers `n`.
25
26
27