-#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
-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
-next: one choice leads to a normal form, the other choice leads to
-endless reduction:
-
- let prefac = \f n. isZero n 1 (mult n (f (pred n))) in
- let fac = Y prefac in
- fac 2
- = [(\f.(\x.f(xx))(\x.f(xx))) prefac] 2
- = [(\x.prefac(xx))(\x.prefac(xx))] 2
- = [prefac((\x.prefac(xx))(\x.prefac(xx)))] 2
- = [prefac(prefac((\x.prefac(xx))(\x.prefac(xx))))] 2
- = [(\f n. isZero n 1 (mult n (f (pred n))))
- (prefac((\x.prefac(xx))(\x.prefac(xx))))] 2
- = [\n. isZero n 1 (mult n ([prefac((\x.prefac(xx))(\x.prefac(xx)))] (pred n)))] 2
- = isZero 2 1 (mult 2 ([prefac((\x.prefac(xx))(\x.prefac(xx)))] (pred 2)))
- = mult 2 ([prefac((\x.prefac(xx))(\x.prefac(xx)))] 1)
- ...
- = mult 2 (mult 1 ([prefac((\x.prefac(xx))(\x.prefac(xx)))] 0))
- = mult 2 (mult 1 (isZero 0 1 ([prefac((\x.prefac(xx))(\x.prefac(xx)))] (pred 0))))
- = mult 2 (mult 1 1)
- = mult 2 1
- = 2
-
-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
-`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.#
-
-A. OK:
-
-<pre>
-A(m,n) =
- | when m == 0 -> n + 1
- | else when n == 0 -> A(m-1,1)
- | else -> A(m-1, A(m,n-1))
-
-let A = Y (\A m n. isZero m (succ n) (isZero n (A (pred m) 1) (A (pred m) (A m (pred n))))) in
-</pre>
-
-For instance,
-
- A 1 2
- = A 0 (A 1 1)
- = A 0 (A 0 (A 1 0))
- = A 0 (A 0 (A 0 1))
- = A 0 (A 0 2)
- = A 0 3
- = 4
-
-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 hyper-exponentiation is to exponentiation...