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