edits

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index edf9552..2fa501c 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -1,9 +1,6 @@
 [[!toc]]
 
 [[!toc]]
 

-#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 <~~>
 
 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 +15,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.
 
 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
 
 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 +23,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.
 
 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:
 
 
 A: Right:
 


@@ -37,7 +34,7 @@ A: Right:
         = Y(Y((\x.Y(xx))(\x.Y(xx))))
         = Y(Y(Y(...(Y(YY))...)))
 
         = 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
 
 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 +55,7 @@ successor.  Let's just check that `X = succ X`:
 
 You should see the close similarity with YY here.
 
 
 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:
 
 A. Yes!  Let's see why it makes sense to think of `Y succ` as a Church
 numeral:


@@ -94,7 +91,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!)
 
 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
 
 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 +130,7 @@ 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. 
 
 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
-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.
+#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.#

 
 A. OK:
   
 
 A. OK:
   


@@ -165,3 +158,16 @@ A 2 x is to A 1 x as multiplication is to addition;
 A 3 x is to A 2 x as exponentiation is to multiplication---
 so A 4 x is to A 3 x as hyper-exponentiation is to exponentiation...
 
 A 3 x is to A 2 x as exponentiation is to multiplication---
 so A 4 x is to A 3 x as hyper-exponentiation is to exponentiation...
 

+#Q. What other questions should I be asking?#
+
+*    What is it about the variant fixed-point combinators that makes
+     them compatible with a call-by-value evaluation strategy?
+
+*    How do you know that the Ackerman function can't be computed
+     using primitive recursion techniques?
+
+*    What *exactly* is primitive recursion?
+
+*    I hear that `Y` delivers the *least* fixed point.  Least
+     according to what ordering?  How do you know it's least?
+     Is leastness important?