From: jim <jim@web>
Date: Sat, 21 Mar 2015 16:07:26 +0000 (-0400)
Subject: removed
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=52df1b9e27d8db743ad63cc97cb1444d143e98e1

removed
---

diff --git a/exercises/_assignment4_answers.mdwn b/exercises/_assignment4_answers.mdwn
deleted file mode 100644
index 135e06ce..00000000
--- a/exercises/_assignment4_answers.mdwn
+++ /dev/null
@@ -1,56 +0,0 @@
-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