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:
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
number---had a fixed point. How could there be an X such that X = X+1?
-Then
+That would imply that
X = succ X = succ (succ X) = succ (succ (succ (X))) = succ (... (succ X)...)
You should see the close similarity with YY here.
-Q. So `Y` applied to `succ` returns infinity!
+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:
first number for every `s` that you add to the second number.)
This is amazing, by the way: we're proving things about a term that
-represents arithmetic infinity. It's important to bear in mind the
-simplest term in question is not infinite:
+represents arithmetic infinity.
+
+It's important to bear in mind the simplest term in question is not
+infinite:
Y succ = (\f.(\x.f(xx))(\x.f(xx)))(\n s z. s (n s z))
The crucial step is the third from the last. We have our choice of
either evaluating the test `isZero 0 1 ...`, which evaluates to `1`,
+no matter what the ... contains;
or we can evaluate the `Y` pump, `(\x.prefac(xx))(\x.prefac(xx))`, to
produce another copy of `prefac`. If we postpone evaluting the
`isZero` test, we'll pump out copy after copy of `prefac`, and never
realize that we've bottomed out in the recursion. But if we adopt a
-leftmost/call by name/normal order evaluation strategy, we'll always
-start with the isZero predicate, and only produce a fresh copy of
+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
A 1 x is to A 0 x as addition is to the successor function;
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 super-exponentiation is to exponentiation...
+so A 4 x is to A 3 x as hyper-exponentiation is to exponentiation...