push (old version of) q&a on fixed points
[lambda.git] / exercises / _assignment4.mdwn
index 0ff4b2c..7df0605 100644 (file)
@@ -12,7 +12,7 @@ and prove that it is a fixed point.
 never gets around to noticing whether it has an argument, let alone
 doing anything with that argument.  If so, how could Ω have a
 fixed point?  That is, how could there be an `X` such that
-<code>&Omega; X <~~> &Omegea;(&Omega; X)</code>?  To answer this
+<code>&Omega; X <~~> &Omega;(&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;.
 
@@ -29,18 +29,18 @@ 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 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
+        let fac = ... in
 
-    fac 4
+        fac 4
 
 ## Arithmetic infinity? ##