[[!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 <~~>
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 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?