Merge branch 'master' of main.jimpryor.net:/srv/lambda/lambda
[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 Solutions to the factorial problem and the mutual recursion problem:
28
29     let true = \y n. y in    
30     let false = \y n. n in    
31     let pair = \a b. \v. v a b in    
32     let fst = \a b. a in   ; aka true    
33     let snd = \a b. b in   ; aka false    
34     let zero = \s z. z in    
35     let succ = \n s z. s (n s z) in    
36     let zero? = \n. n (\p. false) true in    
37     let pred = \n. n (\p. p (\a b. pair (succ a) a)) (pair zero zero) snd in    
38     let add = \l r. r succ l in    
39     let mult = \l r. r (add l) 0 in    
40     let Y = \h. (\u. h (u u)) (\u. h (u u)) in    
41         
42     let fact = Y (\f n . zero? n 1 (mult n (f (pred n)))) in    
43         
44     let Y1 = \f g . (\u v . f(u u v)(v v u))    
45                     (\u v . f(u u v)(v v u))    
46                     (\v u . g(v v u)(u u v)) in    
47         
48     let Y2 = \f g . Y1 g f in    
49         
50     let proto_even = \e o n. zero? n true (o (pred n)) in    
51     let proto_odd = \o e n. zero? n false (e (pred n)) in    
52         
53     let even = Y1 proto_even proto_odd in    
54     let odd = Y2 proto_even proto_odd in    
55         
56     odd 3