X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2F_assignment4_answers.mdwn;fp=exercises%2F_assignment4_answers.mdwn;h=ac1ab6eb24cb5d989381b6b82a8ee5ed05bcd6d6;hp=0000000000000000000000000000000000000000;hb=4b58f050598948e1345d1a5734257c656adb9002;hpb=ebbcaf727cfdc7d8f183a2b6af0b77262efb691f

diff --git a/exercises/_assignment4_answers.mdwn b/exercises/_assignment4_answers.mdwn
new file mode 100644
index 00000000..ac1ab6eb
--- /dev/null
+++ b/exercises/_assignment4_answers.mdwn
@@ -0,0 +1,27 @@
+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`.
+
+
+