evaluation_order.mdwn

   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.
   5
   6
   7 Some lambda terms can be reduced in different ways:
   8
   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>
  24
  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.
  31
  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.)
  35
  36 First, efficiency:
  37
  38 <pre>
  39                       ((\x.w)((\y.y) z))
  40                         \      \
  41                          \      ((\x.w) z)
  42                           \       /
  43                            \     /
  44                             \   /
  45                              \ /
  46                               w
  47 </pre>
  48
  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.
  54
  55 But:
  56
  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>
  72
  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.
  78
  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.
  83
  84 So when the function copies its argument, the "always reduce the
  85 rightmost reducible lambda" wins.
  86
  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).
  89
  90 Now for termination:
  91
  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>
 103
 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`.
 112
 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.
 117
 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.)
 122
 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.