-1. Find a fixed point `X` for the succ function:
-
- H := \f.succ(ff)
- X := HH
- == (\f.succ(ff)) H
- ~~> succ(HH)
-
-So `succ(HH) <~~> succ(succ(HH))`.
-
-2. Prove that `add 1 X <~~> X`:
-
- add 1 X == (\mn.m succ n) 1 X
- ~~> 1 succ X
- == (\fz.fz) succ X
- ~~> succ X
-
-What about `add 2 X`?
-
- add 2 X == (\mn.m succ n) 2 X
- ~~> 2 succ X
- == (\fz.f(fz)) succ X
- ~~> succ (succ X)
-
-So `add n X <~~> X` for all (finite) natural numbers `n`.
-
-
-Solutions to the factorial problem and the mutual recursion problem:
-
- let true = \y n. y in
- let false = \y n. n in
- let pair = \a b. \v. v a b in
- let fst = \a b. a in ; aka true
- let snd = \a b. b in ; aka false
- let zero = \s z. z in
- let succ = \n s z. s (n s z) in
- let zero? = \n. n (\p. false) true in
- let pred = \n. n (\p. p (\a b. pair (succ a) a)) (pair zero zero) snd in
- let add = \l r. r succ l in
- let mult = \l r. r (add l) 0 in
- let Y = \h. (\u. h (u u)) (\u. h (u u)) in
-
- let fact = Y (\f n . zero? n 1 (mult n (f (pred n)))) in
-
- let Y1 = \f g . (\u v . f(u u v)(v v u))
- (\u v . f(u u v)(v v u))
- (\v u . g(v v u)(u u v)) in
-
- let Y2 = \f g . Y1 g f in
-
- let proto_even = \e o n. zero? n true (o (pred n)) in
- let proto_odd = \o e n. zero? n false (e (pred n)) in
-
- let even = Y1 proto_even proto_odd in
- let odd = Y2 proto_even proto_odd in
-
- odd 3