X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=bbc23cece60a3b7f9c154f29e1b0ea013205c276;hp=9bfa3ee70cf3a259103510eafa8fdb4b492017be;hb=2d459a9332289f9d9b702f7e02d85a07bde4d7e6;hpb=1dc1c72afe669382fd004e5193b1f57be4d7cef0

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. 
+