added exercises

[lambda.git] / exercises / _assignment4.mdwn

diff --git a/exercises/_assignment4.mdwn b/exercises/_assignment4.mdwn
index 6c92b54..0ff4b2c 100644 (file)
--- a/exercises/_assignment4.mdwn
+++ b/exercises/_assignment4.mdwn
@@ -7,6 +7,41 @@
 <code>&omega;</code>?  Find a fixed point for <code>&omega;</code>,
 and prove that it is a fixed point.
 
+2. Consider <code>&Omega; X</code> for an arbitrary term `X`.
+&Omega; is so busy reducing itself (the eternal solipsist) that it
+never gets around to noticing whether it has an argument, let alone
+doing anything with that argument.  If so, how could &Omega; have a
+fixed point?  That is, how could there be an `X` such that
+<code>&Omega; X <~~> &Omegea;(&Omega; X)</code>?  To answer this
+question, begin by constructing <code>Y&Omega;</code>.  Prove that 
+<code>Y&Omega;</code> is a fixed point for &Omega;.
+
+3. Find two different terms that have the same fixed point.  That is,
+find terms `F`, `G`, and `X` such that `F(X) <~~> F(F(X))` and `G(X)
+<~~> G(G(X))`.  (If you need a hint, reread the notes on fixed
+points.)
+
+## Writing recursive functions ##
+
+4. Helping yourself to the functions given just below,
+write a recursive function caled `fac` that computes the factorial.
+The factorial `n! = n * (n - 1) * (n - 2) * ... * 3 * 2 * 1`.
+For instance, `fac 0 ~~> 1`, `fac 1 ~~> 1`, `fac 2 ~~> 2`, `fac 3 ~~>
+6`, and `fac 4 ~~> 24`.
+
+    let true = \then else. then in
+    let false = \then else. else in
+    let iszero = \n. n (\x. false) true in
+    let pred = \n f z. n (\u v. v (u f)) (K z) I in
+    let succ = \n f z. f (n f z) in
+    let add = \n m .n succ m in
+    let mult = \n m.n(add m)0 in
+    let Y = \h . (\f . h (f f)) (\f . h (f f)) in
+
+    let fac = ... in
+
+    fac 4
+
 ## Arithmetic infinity? ##
 
 The next few questions involve reasoning about Church arithmetic and