#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 <~~>
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
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:
= 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
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:
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
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: