cps.mdwn

   1 Gaining control over order of evaluation
   2 ----------------------------------------
   3
   4 We know that evaluation order matters.  We're beginning to learn how
   5 to gain some control over order of evaluation (think of Jim's abort handler).
   6 We continue to reason about order of evaluation.
   7
   8 A superbly clear and lucid discussion can be found here:
   9 [Sestoft: Demonstrating Lambda Calculus Reduction](http://tinyurl.com/27nd3ub).
  10 Sestoft also provides a really lovely lambda evaluator,
  11 which allows you to select multiple evaluation strategies,
  12 and to see reductions happen step by step:
  13 [Sestoft's lambda reduction webpage](http://ellemose.dina.kvl.dk/~sestoft/lamreduce/lamframes.html).
  14
  15
  16 Evaluation order matters
  17 ------------------------
  18
  19 We've seen this many times.  For instance, consider the following
  20 reductions.  It will be convenient to use the abbreviation `w =
  21 \x.xx`.  I'll indicate which lambda is about to be reduced with a *
  22 underneath:
  23
  24 <pre>
  25 (\x.y)(ww)
  26  *
  27 y
  28 </pre>
  29
  30 Done!  We have a normal form.  But if we reduce using a different
  31 strategy, things go wrong:
  32
  33 <pre>
  34 (\x.y)(ww) =
  35 (\x.y)((\x.xx)w) =
  36         *
  37 (\x.y)(ww) =
  38 (\x.y)((\x.xx)w) =
  39         *
  40 (\x.y)(ww)
  41 </pre>
  42
  43 Etc.
  44
  45 As a second reminder of when evaluation order matters, consider using
  46 `Y = \f.(\h.f(hh))(\h.f(hh))` as a fixed point combinator to define a recursive function:
  47
  48 <pre>
  49 Y (\f n. blah) =
  50 (\f.(\h.f(hh))(\h.f(hh))) (\f n. blah)
  51      *
  52 (\f.f((\h.f(hh))(\h.f(hh)))) (\f n. blah)
  53        *
  54 (\f.f(f((\h.f(hh))(\h.f(hh))))) (\f n. blah)
  55          *
  56 (\f.f(f(f((\h.f(hh))(\h.f(hh)))))) (\f n. blah)
  57 </pre>
  58
  59 And we never get the recursion off the ground.
  60
  61
  62 Restricting evaluation: call by name, call by value
  63 ---------------------------------------------------
  64
  65 One way to begin to gain some control is by adjusting our notion of
  66 beta reduction.  This strategy has some of the flavor of adding types,
  67 but is actually a part of the untyped calculus.
  68
  69 In order to have a precise discussion, we'll need some vocabulary.
  70 We've been talking about normal form (lambda terms that can't be
  71 further reduced), and leftmost evaluation (the reduction strategy of
  72 always choosing the left most reducible lambda); we'll need to refine
  73 both of those concepts.
  74
  75 Kinds of normal form:
  76 ---------------------
  77
  78 Recall that there are three kinds of lambda term.  Let `a` be an
  79 arbitrary variable, and let `M` and `N` be arbitrary terms:
  80
  81 <pre>
  82 The pure untyped lambda calculus (again):
  83
  84              Form     Examples
  85 Variable     a        x, y, z
  86 Abstract     \aM      \x.x, \x.y, \x.\y.y
  87 Application  MN       (x x), ((\x.x) y), ((\x.x)(\y.y))
  88 </pre>
  89
  90 It will be helpful to define a *redex*, which is a lambda term of
  91 the form `((\aM) N)`.  That is, a redex is a form for which beta
  92 reduction is defined (ignoring, as usual, the manouvering required in
  93 order to avoid variable collision).
  94
  95 It will also be helpful to have names for the two components of an
  96 application `(M N)`: we'll call `M` the *functor*, and `N` the
  97 *argument*.  Note that functor position can be occupied by a variable,
  98 since `x` is in the functor position of the term `(x y)`.
  99
 100 Ok, with that vocabulary, we can distinguish four different types of
 101 normal form:
 102
 103
 104
 105
 106
 107
 108
 109 Take Plotkin's CBN CPS:
 110
 111 [x] ~~> x
 112 [\xM] ~~> \k.k(\x[M])
 113 [MN] ~~> \k.[M](\m.m[N]k)
 114
 115 let w = \x.xx in
 116
 117 [(\xy)(ww)] ~~>
 118 \k.[\xy](\m.m[ww]k) ~~>
 119 \k.[\xy](\m.m(\k.[w](\m.m[w]k))k) ~~>
 120 \k.[\xy](\m.m(\k.(\k.k(\x[xx]))(\m.m[w]k))k) ~~> beta*
 121 \k.[\xy](\m.m(\k.(\x[xx])[w]k)k) ~~>
 122 \k.[\xy](\m.m(\k.(\x(\k.[x](\m.m[x]k)))[w]k)k) ~~>
 123 \k.[\xy](\m.m(\k.(\x(\k.x(\m.mxk)))[w]k)k) ~~> beta
 124 \k.[\xy](\m.m(\k.[w](\m.m[w]k))k) --- same as second line!
 125