Merge branch 'pryor'
[lambda.git] / week4.mdwn
index 5238b26..bc154ae 100644 (file)
@@ -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
 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))))
 ~~> (\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.#
 
 
 #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 
 <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)) ))
 ~~> 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.
 </code></pre>
 
 You should see the close similarity with `Y Y` here.
@@ -66,12 +68,12 @@ numeral:
 
 <pre><code>[same definitions]
 succ X
 
 <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
 <~~> 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`,
 </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
 <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
 ~~> [(\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))
 ~~> [\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
 ~~> mul 2 (mul 1 1)
 ~~> mul 2 1
 ~~> 2
@@ -248,7 +250,7 @@ So, if we were searching the list that implements some set to see if the number
 we can stop. If we haven't found `5` already, we know it's not in the rest of the
 list either.
 
 we can stop. If we haven't found `5` already, we know it's not in the rest of the
 list either.
 
-This is an improvement, but it's still a "linear" search through the list.
+*Comment*: This is an improvement, but it's still a "linear" search through the list.
 There are even more efficient methods, which employ "binary" searching. They'd
 represent the set in such a way that you could quickly determine whether some
 element fell in one half, call it the left half, of the structure that
 There are even more efficient methods, which employ "binary" searching. They'd
 represent the set in such a way that you could quickly determine whether some
 element fell in one half, call it the left half, of the structure that
@@ -258,7 +260,7 @@ determination could be made for whichever half you were directed to. And then
 for whichever quarter you were directed to next. And so on. Until you either
 found the element or exhausted the structure and could then conclude that the
 element in question was not part of the set. These sorts of structures are done
 for whichever quarter you were directed to next. And so on. Until you either
 found the element or exhausted the structure and could then conclude that the
 element in question was not part of the set. These sorts of structures are done
-using **binary trees** (see below).
+using [binary trees](/implementing_trees).
 
 
 #Aborting a search through a list#
 
 
 #Aborting a search through a list#