X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=bc154aea1195830c5858a716055ec250c4229a3e;hp=78e2d37e8a4363b6ebe10e46baa2e0205148ab08;hb=bb7d661ae9cacbe86e730ab3eea5cf2ff864912e;hpb=0a6cb8dd4a9460b13006f75f6a5b84d434aba212
diff --git a/week4.mdwn b/week4.mdwn
index 78e2d37e..bc154aea 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -27,11 +27,13 @@ of `T`, by the reasoning in the previous answer.
A: Right:
let Y = \T. (\x. T (x x)) (\x. T (x x)) in
-Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
+Y Y
+≡ \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))...)))
+~~> Y (Y (Y (...(Y (Y Y))...)))
+
#Q: Ouch! Stop hurting my brain.#
@@ -51,9 +53,9 @@ successor. Let's just check that `X = succ X`:
let succ = \n s z. s (n s z) in
let X = (\x. succ (x x)) (\x. succ (x x)) in
succ X
-≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
+≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x)) ))
-≡ succ (succ X)
+≡ succ (succ X)
You should see the close similarity with `Y Y` here.
@@ -66,12 +68,12 @@ numeral:
[same definitions]
succ X
-≡ (\n s z. s (n s z)) X
-~~> \s z. s (X s z)
+≡ (\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
-≡ (\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))
+≡ (\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))
So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,
@@ -109,17 +111,17 @@ endless reduction:
let prefact = \f n. iszero n 1 (mul n (f (pred n))) in
let fact = Y prefact in
fact 2
-≡ [(\f. (\x. f (x x)) (\x. f (x x))) prefact] 2
+≡ [(\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
-≡ [ (\f n. iszero n 1 (mul n (f (pred n)))) (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
+≡ [ (\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))
-≡ mul 2 (mul 1 (iszero 0 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0))))
+≡ 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
@@ -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.
-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
@@ -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
-using **binary trees** (see below).
+using [binary trees](/implementing_trees).
#Aborting a search through a list#