From: Jim Pryor <profjim@jimpryor.net>
Date: Sun, 3 Oct 2010 19:42:26 +0000 (-0400)
Subject: week4 tweaking
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=d6f2385162de2e0c3c29758d90ef0ec89ae9f776;hp=-c

week4 tweaking

Signed-off-by: Jim Pryor <profjim@jimpryor.net>
---

d6f2385162de2e0c3c29758d90ef0ec89ae9f776
diff --git a/week4.mdwn b/week4.mdwn
index 4bddeaa6..fb843462 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -51,9 +51,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 +66,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
-&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))
+&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 +109,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 (mul 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