From: Chris Barker Date: Sat, 2 Oct 2010 19:31:54 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=550067e6cbfb3ff838997559946f958fb2eb7395;ds=sidebyside edits --- diff --git a/week4.mdwn b/week4.mdwn index edf9552d..4c8288e8 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -2,8 +2,8 @@ #These notes return to the topic of fixed point combiantors for one more return to the topic of fixed point combinators# -Q: How do you know that every term in the untyped lambda calculus has -a fixed point? +#Q: How do you know that every term in the untyped lambda calculus has +a fixed point?# 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 <~~> @@ -18,7 +18,7 @@ X = WW = (\x.T(xx))W = T(WW) = TX Please slow down and make sure that you understand what justified each of the equalities in the last line. -Q: How do you know that for any term `T`, `YT` is a fixed point of `T`? +#Q: How do you know that for any term `T`, `YT` is a fixed point of `T`?# A: Note that in the proof given in the previous answer, we chose `T` and then set `X = WW = (\x.T(xx))(\x.T(xx))`. If we abstract over @@ -26,7 +26,7 @@ and then set `X = WW = (\x.T(xx))(\x.T(xx))`. If we abstract over what argument `T` we feed Y, it returns some `X` that is a fixed point of `T`, by the reasoning in the previous answer. -Q: So if every term has a fixed point, even `Y` has fixed point. +#Q: So if every term has a fixed point, even `Y` has fixed point.# A: Right: @@ -37,7 +37,7 @@ A: Right: = Y(Y((\x.Y(xx))(\x.Y(xx)))) = Y(Y(Y(...(Y(YY))...))) -Q: Ouch! Stop hurting my brain. +#Q: Ouch! Stop hurting my brain.# A: Let's come at it from the direction of arithmetic. Recall that we claimed that even `succ`---the function that added one to any @@ -58,7 +58,7 @@ successor. Let's just check that `X = succ X`: You should see the close similarity with YY here. -Q. So `Y` applied to `succ` returns a number that is not finite! +#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: @@ -94,7 +94,7 @@ 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]]? +#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 @@ -133,11 +133,11 @@ leftmost/call-by-name/normal-order evaluation strategy, we'll always start with the `isZero` predicate, and only produce a fresh copy of `prefac` if we are forced to. -Q. You claimed that the Ackerman function couldn't be implemented +#Q. You claimed that the Ackerman function couldn't be implemented using our primitive recursion techniques (such as the techniques that allow us to define addition and multiplication). But you haven't shown that it is possible to define the Ackerman function using full -recursion. +recursion.# A. OK: