You should see the close similarity with `Y Y` 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. Well, if it makes sense to think of it as a number at all. It doesn't have the same structure as our encodings of finite Church numbers. But let's see if it behaves like they do:
+A: Well, if it makes sense to think of it as a number at all. It doesn't have the same structure as our encodings of finite Church numbers. But let's see if it behaves like they do:
; assume same definitions as before
succ ξ
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
+A: For a recursive function that has a well-behaved base case, such as
the factorial function, evaluation order is crucial. In the following
computation, we will arrive at a normal form. Watch for the moment at
which we have to make a choice about which beta reduction to perform
`prefact` if we are forced to.
-## Q. You claimed that the Ackermann 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 Ackermann function using full recursion. ##
+## Q: You claimed that the Ackermann 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 Ackermann function using full recursion. ##
-A. OK:
+A: OK:
A(m,n) =
| when m == 0 -> n + 1
`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? ##
+## 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?