From: Chris Barker Date: Mon, 27 Sep 2010 17:55:17 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=4e90575923350315ab60968f7ca746af5f6a101d edits --- diff --git a/evaluation_order.mdwn b/evaluation_order.mdwn new file mode 100644 index 00000000..3cd25fb5 --- /dev/null +++ b/evaluation_order.mdwn @@ -0,0 +1,125 @@ +This discussion elaborates on the discussion of evaluation order in the +class notes from week 2. It makes use of the reduction diagrams drawn +in class, which makes choice of evaluation strategy a choice of which +direction to move through a network of reduction links. + + +Some lambda terms can be reduced in different ways: + +
```+                     ((\x.x)((\y.y) z))
+                       /      \
+                      /        \
+                     /          \
+                    /            \
+                    ((\y.y) z)   ((\x.x) z)
+                      \             /
+                       \           /
+                        \         /
+                         \       /
+                          \     /
+                           \   /
+                             z
+```
+ +But because the lambda calculus is confluent (has the diamond +property, named after the shape of the diagram above), no matter which +lambda you choose to target for reduction first, you end up at the +same place. It's like travelling in Manhattan: if you walk uptown +first and then head east, you end up in the same place as if you walk +east and then head uptown. + +But which lambda you target has implications for efficiency and for +termination. (Later in the course, it will have implications for +the order in which side effects occur.) + +First, efficiency: + +
```+                      ((\x.w)((\y.y) z))
+                        \      \
+                         \      ((\x.w) z)
+                          \       /
+                           \     /
+                            \   /
+                             \ /
+                              w
+```
+ +If a function discards its argument (as `\x.w` does), it makes sense +to target that function for reduction, rather than wasting effort +reducing the argument only to have the result of all that work thrown +away. So in this situation, the strategy of "always reduce the +leftmost reducible lambda" wins. + +But: + +
```+                        ((\x.xx)((\y.y) z))
+                          /       \
+     (((\y.y) z)((\y.y) z)         ((\x.xx) z)
+        /         |                  /
+       /          (((\y.y)z)z)      /
+      /              |             /
+     /               |            /
+    /                |           /
+    (z ((\y.y)z))    |          /
+         \           |         /
+          -----------.---------
+                     |
+                     zz
+```
+ +This time, the leftmost function `\x.xx` copies its argument. +If we reduce the rightmost lambda first (rightmost branch of the +diagram), the argument is already simplified before we do the +copying. We arrive at the normal form (i.e., the form that cannot be +further reduced) in two steps. + +But if we reduce the rightmost lambda first (the two leftmost branches +of the diagram), we copy the argument before it has been evaluated. +In effect, when we copy the unreduced argument, we double the amount +of work we need to do to deal with that argument. + +So when the function copies its argument, the "always reduce the +rightmost reducible lambda" wins. + +So evaluation strategies have a strong effect on how many reduction +steps it takes to arrive at a stopping point (e.g., normal form). + +Now for termination: + +
```+(\x.w)((\x.xxx)(\x.xxx))
+ |      \
+ |       (\x.w)((\x.xxx)(\x.xxx)(\x.xxx))
+ |        /      \
+ |       /        (\x.w)((\x.xxx)(\x.xxx)(\x.xxx)(\x.xxx))
+ |      /          /       \
+ .-----------------         etc.
+ |
+ w
+```
+ +Here we have a function that discards its argument on the left, and a +non-terminating term on the right. It's even more evil than Omega, +because it not only never reduces, it generates more and more work +with each so-called reduction. If we unluckily adopt the "always +reduce the rightmost reducible lambda" strategy, we'll spend our days +relentlessly copying out new copies of \x.xxx. But if we even once +reduce the leftmost reducible lambda, we'll immediately jump to the +normal form, `w`. + +We can roughly associate the "leftmost always" strategy with call by +name (normal order), and the "rightmost always" strategy with call by +value (applicative order). There are fine-grained distinctions among +these terms of art that we will not pause to untangle here. + +If a term has a normal form (a reduction such that no further +reduction is possible), then a leftmost-always reduction will find it. +(That's why it's called "normal order": it's the evaluation order that +guarantees finding a normal form if one exists.) + +Preview: if the evaluation of a function has side effects, then the +choice of an evaluation strategy will make a big difference in which +side effect occur and in which order.