X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=58d6bc38204bd3bcbf4afabe6d9c4306b82735de;hp=077884cc0df70cfb962f2b03ffad70f121ca1f32;hb=b5672ffae330118100a8de0a656ee9584d0f7ee6;hpb=1bac07d66d424599f9a06d374cde4e2b904847a2 diff --git a/week4.mdwn b/week4.mdwn index 077884cc..58d6bc38 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -6,8 +6,7 @@ A: That's easy: let `T` be an arbitrary term in the lambda calculus. If `T` has a fixed point, then there exists some `X` such that `X <~~> TX` (that's what it means to *have* a fixed point). -

-let L = \x. T (x x) in
+
let L = \x. T (x x) in
let X = L L in
X ≡ L L ≡ (\x. T (x x)) L ~~> T (L L) ≡ T X

@@ -18,7 +17,7 @@ of the equalities in the last line. #Q: How do you know that for any term `T`, `Y T` is a fixed point of `T`?# A: Note that in the proof given in the previous answer, we chose `T` -and then set `X = L L = (\x. T (x x)) (\x. T (x x))`. If we abstract over +and then set X ≡ L L ≡ (\x. T (x x)) (\x. T (x x)). If we abstract over `T`, we get the Y combinator, `\T. (\x. T (x x)) (\x. T (x x))`. No matter what argument `T` we feed `Y`, it returns some `X` that is a fixed point of `T`, by the reasoning in the previous answer. @@ -28,10 +27,598 @@ 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.# + +A: Is that a question? + +Let's come at it from the direction of arithmetic. Recall that we +claimed that even `succ`---the function that added one to any +number---had a fixed point. How could there be an X such that X = X+1? +That would imply that + + X <~~> succ X <~~> succ (succ X) <~~> succ (succ (succ X)) <~~> succ (... (succ X)...) + +In other words, the fixed point of `succ` is a term that is its own +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 (succ ( (\x. succ (x x)) (\x. succ (x x)) ))
+≡   succ (succ X)
+
+ +You should see the close similarity with `Y Y` here. + + +#Q. So `Y` applied to `succ` returns a number that is not finite!# + +A. Yes! Let's see why it makes sense to think of `Y succ` as a Church +numeral: + +
[same definitions]
+succ X
+≡    (\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))
+
+ +So `succ X` looks like a numeral: it takes two arguments, `s` and `z`, +and returns a sequence of nested applications of `s`... + +You should be able to prove that `add 2 (Y succ) <~~> Y succ`, +likewise for `mul`, `sub`, `pow`. What happens if we try `sub (Y +succ) (Y succ)`? What would you expect infinity minus infinity to be? +(Hint: choose your evaluation strategy so that you add two `s`s to the +first number for every `s` that you add to the second number.) + +This is amazing, by the way: we're proving things about a term that +represents arithmetic infinity. + +It's important to bear in mind the simplest term in question is not +infinite: + + Y succ = (\f. (\x. f (x x)) (\x. f (x x))) (\n s z. s (n s z)) + +The way that infinity enters into the picture is that this term has +no normal form: no matter how many times we perform beta reduction, +there will always be an opportunity for more beta reduction. (Lather, +rinse, repeat!) + + +#Q. That reminds me, what about [[evaluation order]]?# + +A. For a recursive function that has a well-behaved base case, such as +the factorial function, evaluation order is crucial. In the following +computation, we will arrive at a normal form. Watch for the moment at +which we have to make a choice about which beta reduction to perform +next: one choice leads to a normal form, the other choice leads to +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
+~~> [(\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
+~~> [\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 (mul 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0)))))
+~~> mul 2 (mul 1 1)
+~~> mul 2 1
+~~> 2
+