X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=evaluation_order.mdwn;fp=evaluation_order.mdwn;h=3cd25fb5e3b8dff65c0a9172a84308e25d62d3f0;hp=0000000000000000000000000000000000000000;hb=4e90575923350315ab60968f7ca746af5f6a101d;hpb=652f9c0e705be97390dbde28a4e6d62cc9219b48 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.