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)
                      \             /
                       \           /
                        \         /
                         \       /
                          \     /
                           \   /

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)
                          \       /
                           \     /
                            \   /
                             \ /

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.


                        ((\x.xx)((\y.y) z))
                          /       \
     (((\y.y) z)((\y.y) z)         ((\x.xx) z)
        /         |                  /
       /          (((\y.y)z)z)      /
      /              |             / 
     /               |            /
    /                |           /
    (z ((\y.y)z))    |          / 
         \           |         /

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.w)((\\\\
 |      /          /       \
 .-----------------         etc.

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