1 This discussion elaborates on the discussion of evaluation order in the
2 class notes from week 2.  It makes use of the reduction diagrams drawn
3 in class, which makes choice of evaluation strategy a choice of which
4 direction to move through a network of reduction links.
7 Some lambda terms can be reduced in different ways:
9 <pre>
10                      ((\x.x)((\y.y) z))
11                        /      \
12                       /        \
13                      /          \
14                     /            \
15                     ((\y.y) z)   ((\x.x) z)
16                       \             /
17                        \           /
18                         \         /
19                          \       /
20                           \     /
21                            \   /
22                              z
23 </pre>
25 But because the lambda calculus is confluent (has the diamond
26 property, named after the shape of the diagram above), no matter which
27 lambda you choose to target for reduction first, you end up at the
28 same place.  It's like travelling in Manhattan: if you walk uptown
29 first and then head east, you end up in the same place as if you walk
30 east and then head uptown.
32 But which lambda you target has implications for efficiency and for
33 termination.  (Later in the course, it will have implications for
34 the order in which side effects occur.)
36 First, efficiency:
38 <pre>
39                       ((\x.w)((\y.y) z))
40                         \      \
41                          \      ((\x.w) z)
42                           \       /
43                            \     /
44                             \   /
45                              \ /
46                               w
47 </pre>
49 If a function discards its argument (as `\x.w` does), it makes sense
50 to target that function for reduction, rather than wasting effort
51 reducing the argument only to have the result of all that work thrown
52 away.  So in this situation, the strategy of "always reduce the
53 leftmost reducible lambda" wins.
55 But:
57 <pre>
58                         ((\x.xx)((\y.y) z))
59                           /       \
60      (((\y.y) z)((\y.y) z)         ((\x.xx) z)
61         /         |                  /
62        /          (((\y.y)z)z)      /
63       /              |             /
64      /               |            /
65     /                |           /
66     (z ((\y.y)z))    |          /
67          \           |         /
68           -----------.---------
69                      |
70                      zz
71 </pre>
73 This time, the leftmost function `\x.xx` copies its argument.
74 If we reduce the rightmost lambda first (rightmost branch of the
75 diagram), the argument is already simplified before we do the
76 copying.  We arrive at the normal form (i.e., the form that cannot be
77 further reduced) in two steps.
79 But if we reduce the rightmost lambda first (the two leftmost branches
80 of the diagram), we copy the argument before it has been evaluated.
81 In effect, when we copy the unreduced argument, we double the amount
82 of work we need to do to deal with that argument.
84 So when the function copies its argument, the "always reduce the
85 rightmost reducible lambda" wins.
87 So evaluation strategies have a strong effect on how many reduction
88 steps it takes to arrive at a stopping point (e.g., normal form).
90 Now for termination:
92 <pre>
93 (\x.w)((\x.xxx)(\x.xxx))
94  |      \
95  |       (\x.w)((\x.xxx)(\x.xxx)(\x.xxx))
96  |        /      \
97  |       /        (\x.w)((\x.xxx)(\x.xxx)(\x.xxx)(\x.xxx))
98  |      /          /       \
99  .-----------------         etc.
100  |
101  w
102 </pre>
104 Here we have a function that discards its argument on the left, and a
105 non-terminating term on the right.  It's even more evil than Omega,
106 because it not only never reduces, it generates more and more work
107 with each so-called reduction.  If we unluckily adopt the "always
108 reduce the rightmost reducible lambda" strategy, we'll spend our days
109 relentlessly copying out new copies of \x.xxx.  But if we even once
110 reduce the leftmost reducible lambda, we'll immediately jump to the
111 normal form, `w`.
113 We can roughly associate the "leftmost always" strategy with call by
114 name (normal order), and the "rightmost always" strategy with call by
115 value (applicative order).  There are fine-grained distinctions among
116 these terms of art that we will not pause to untangle here.
118 If a term has a normal form (a reduction such that no further
119 reduction is possible), then a leftmost-always reduction will find it.
120 (That's why it's called "normal order": it's the evaluation order that
121 guarantees finding a normal form if one exists.)
123 Preview: if the evaluation of a function has side effects, then the
124 choice of an evaluation strategy will make a big difference in which
125 side effect occur and in which order.