1 Gaining control over order of evaluation
2 ----------------------------------------
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.
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).
16 Evaluation order matters
17 ------------------------
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:
24 <pre>
25 (\x.y)(ww)
26  *
27 y
28 </pre>
30 Done!  We have a normal form.  But if we reduce using a different
31 strategy, things go wrong:
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>
43 Etc.
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:
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>
59 And we never get the recursion off the ground.
62 Restricting evaluation: call by name, call by value
63 ---------------------------------------------------
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.
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.
75 Kinds of normal form:
76 ---------------------
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:
81 <pre>
82 The pure untyped lambda calculus (again):
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>
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).
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)`.
100 Ok, with that vocabulary, we can distinguish four different types of
101 normal form:
109 Take Plotkin's CBN CPS:
111 [x] ~~> x
112 [\xM] ~~> \k.k(\x[M])
113 [MN] ~~> \k.[M](\m.m[N]k)
115 let w = \x.xx in
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!