From 2d459a9332289f9d9b702f7e02d85a07bde4d7e6 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 3 Oct 2010 13:36:49 -0400 Subject: [PATCH] week4 debugging more Signed-off-by: Jim Pryor --- week4.mdwn | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/week4.mdwn b/week4.mdwn index 9bfa3ee7..bbc23cec 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -96,3 +96,42 @@ there will always be an opportunity for more beta reduction. (Lather, rinse, repeat!) +#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. + -- 2.11.0