index edf9552..2fa501c 100644 (file)
@@ -1,9 +1,6 @@
[[!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 <~~>
@@ -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.

-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 +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.

-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 +34,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 +55,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 +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!)

-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 +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.

-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:

@@ -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...

+#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?