added draft of assignment4

[lambda.git] / exercises / _assignment4_answers.mdwn

diff --git a/exercises/_assignment4_answers.mdwn b/exercises/_assignment4_answers.mdwn
new file mode 100644 (file)
index 0000000..ac1ab6e
--- /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`.
+
+
+