Merge branch 'pryor'

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index 5238b26..f92ea16 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -27,11 +27,13 @@ of `T`, by the reasoning in the previous answer.
 A: Right:
 
 <pre><code>let Y = \T. (\x. T (x x)) (\x. T (x x)) in
-Y Y &equiv; \T. (\x. T (x x)) (\x. T (x x)) Y
+Y Y
+&equiv;   \T. (\x. T (x x)) (\x. T (x x)) Y
 ~~> (\x. Y (x x)) (\x. Y (x x))
 ~~> Y ((\x. Y (x x)) (\x. Y (x x)))
 ~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
-~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>
+~~> Y (Y (Y (...(Y (Y Y))...)))
+</code></pre>
 
 
 #Q: Ouch!  Stop hurting my brain.#
@@ -51,9 +53,9 @@ successor.  Let's just check that `X = succ X`:
 <pre><code>let succ = \n s z. s (n s z) in
 let X = (\x. succ (x x)) (\x. succ (x x)) in
 succ X 
-&equiv; succ ( (\x. succ (x x)) (\x. succ (x x)) ) 
+&equiv;   succ ( (\x. succ (x x)) (\x. succ (x x)) ) 
 ~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x)) ))
-&equiv; succ (succ X)
+&equiv;   succ (succ X)
 </code></pre>
 
 You should see the close similarity with `Y Y` here.
@@ -66,12 +68,12 @@ numeral:
 
 <pre><code>[same definitions]
 succ X
-&equiv; (\n s z. s (n s z)) X 
-~~> \s z. s (X s z)
+&equiv;    (\n s z. s (n s z)) X 
+~~>  \s z. s (X s z)
 <~~> succ (\s z. s (X s z)) ; using fixed-point reasoning
-~~> \s z. s ([succ (\s z. s (X s z))] s z)
-~~> \s z. s ([\s z. s ([succ (\s z. s (X s z))] s z)] s z)
-~~> \s z. s (s (succ (\s z. s (X s z))))
+&equiv;    (\n s z. s (n s z)) (\s z. s (X s z))
+~~>  \s z. s ((\s z. s (X s z)) s z)
+~~>  \s z. s (s (X s z))
 </code></pre>
 
 So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,
@@ -109,17 +111,17 @@ endless reduction:
 <pre><code>let prefact = \f n. iszero n 1 (mul n (f (pred n))) in
 let fact = Y prefact in
 fact 2
-&equiv; [(\f. (\x. f (x x)) (\x. f (x x))) prefact] 2
+&equiv;   [(\f. (\x. f (x x)) (\x. f (x x))) prefact] 2
 ~~> [(\x. prefact (x x)) (\x. prefact (x x))] 2
 ~~> [prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 2
 ~~> [prefact (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
-&equiv; [ (\f n. iszero n 1 (mul n (f (pred n)))) (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
+&equiv;   [ (\f n. iszero n 1 (mul n (f (pred n)))) (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
 ~~> [\n. iszero n 1 (mul n ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred n)))] 2
 ~~> iszero 2 1 (mul 2 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 2)))
 ~~> mul 2 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 1)
 ...
 ~~> mul 2 (mul 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 0))
-&equiv; mul 2 (mul 1 (iszero 0 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0))))
+&equiv;   mul 2 (mul 1 (iszero 0 1 (mul 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0)))))
 ~~> mul 2 (mul 1 1)
 ~~> mul 2 1
 ~~> 2