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 lucid discussion of evaluation order in the
9 context of the lambda calculus can be found here:
10 [Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf).
11 Sestoft also provides a lovely on-line lambda evaluator:
12 [Sestoft: Lambda calculus reduction workbench](http://www.itu.dk/~sestoft/lamreduce/index.html),
13 which allows you to select multiple evaluation strategies,
14 and to see reductions happen step by step.
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 Using a Continuation Passing Style transform to control order of evaluation
63 ---------------------------------------------------------------------------
65 We'll present a technique for controlling evaluation order by transforming a lambda term
66 using a Continuation Passing Style transform (CPS), then we'll explore
67 what the CPS is doing, and how.
69 In order for the CPS to work, we have to adopt a new restriction on
70 beta reduction: beta reduction does not occur underneath a lambda.
71 That is, `(\x.y)z` reduces to `z`, but `\w.(\x.y)z` does not, because
72 the `\w` protects the redex in the body from reduction.
73 (A redex is a subform ...(\xM)N..., i.e., something that can be the
74 target of reduction.)
76 Start with a simple form that has two different reduction paths:
78 reducing the leftmost lambda first: `(\x.y)((\x.z)w)  ~~> y`
80 reducing the rightmost lambda first: `(\x.y)((\x.z)w)  ~~> (\x.y)z ~~> y`
82 After using the following call-by-name CPS transform---and assuming
83 that we never evaluate redexes protected by a lambda---only the first
84 reduction path will be available: we will have gained control over the
85 order in which beta reductions are allowed to be performed.
87 Here's the CPS transform defined:
89     [x] = x
90     [\xM] = \k.k(\x[M])
91     [MN] = \k.[M](\m.m[N]k)
93 Here's the result of applying the transform to our problem term:
95     [(\x.y)((\x.z)w)] =
96     \k.[\x.y](\m.m[(\x.z)w]k) =
97     \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[w]k))k) =
98     \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.mwk))k)
100 Because the initial `\k` protects the entire transformed term,
101 we can't perform any reductions.  In order to see the computation
102 unfold, we have to apply the transformed term to a trivial
103 continuation, usually the identity function `I = \x.x`.
105     [(\x.y)((\x.z)w)] I =
106     (\k.[\x.y](\m.m[(\x.z)w]k)) I
107      *
108     [\x.y](\m.m[(\x.z)w] I) =
109     (\k.k(\x.y))(\m.m[(\x.z)w] I)
110      *           *
111     (\x.y)[(\x.z)w] I
112      *
113     y I
115 The application to `I` unlocks the leftmost functor.  Because that
116 functor (`\x.y`) throws away its argument, we never need to expand the
117 CPS transform of the argument.
119 Compare with a call-by-value xform:
121     {x} = \k.kx
122     {\aM} = \k.k(\a{M})
123     {MN} = \k.{M}(\m.{N}(\n.mnk))
125 This time the reduction unfolds in a different manner:
127     {(\x.y)((\x.z)w)} I =
128     (\k.{\x.y}(\m.{(\x.z)w}(\n.mnk))) I
129      *
130     {\x.y}(\m.{(\x.z)w}(\n.mnI)) =
131     (\k.k(\x.{y}))(\m.{(\x.z)w}(\n.mnI))
132      *             *
133     {(\x.z)w}(\n.(\x.{y})nI) =
134     (\k.{\x.z}(\m.{w}(\n.mnk)))(\n.(\x.{y})nI)
135      *
136     {\x.z}(\m.{w}(\n.mn(\n.(\x.{y})nI))) =
137     (\k.k(\x.{z}))(\m.{w}(\n.mn(\n.(\x.{y})nI)))
138      *             *
139     {w}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
140     (\k.kw)(\n.(\x.{z})n(\n.(\x.{y})nI))
141      *      *
142     (\x.{z})w(\n.(\x.{y})nI)
143      *
144     {z}(\n.(\x.{y})nI) =
145     (\k.kz)(\n.(\x.{y})nI)
146      *      *
147     (\x.{y})zI
148      *
149     {y}I =
150     (\k.ky)I
151      *
152     I y
154 Both xforms make the following guarantee: as long as redexes
155 underneath a lambda are never evaluated, there will be at most one
156 reduction available at any step in the evaluation.
157 That is, all choice is removed from the evaluation process.
159 Questions and exercises:
161 1. Why is the CBN xform for variables `[x] = x' instead of something
162 involving kappas?
164 2. Write an Ocaml function that takes a lambda term and returns a
165 CPS-xformed lambda term.  You can use the following data declaration:
167     type form = Var of char | Abs of char * form | App of form * form;;
169 3. What happens (in terms of evaluation order) when the application
170 rule for CBN CPS is changed to `[MN] = \k.[N](\n.[M]nk)`?  Likewise,
171 What happens when the application rule for CBV CPS is changed to
172 `{MN} = \k.{N}(\n.{M}(\m.mnk))`?
174 4. What happens when the application rules for the CPS xforms are changed to
176 <pre>
177    [MN] = \k.{M}(\m.m{N}k)
178    {MN} = \k.[M](\m.[N](\n.mnk))
179 </pre>
181 Thinking through the types
182 --------------------------
186 Let's say we're working in the simply-typed lambda calculus.
187 Then if the original term is well-typed, the CPS xform will also be
188 well-typed.  But what will the type of the transformed term be?
190 The transformed terms all have the form `\k.blah`.  The rule for the
191 CBN xform of a variable appears to be an exception, but instead of
192 writing `[x] = x`, we can write `[x] = \k.xk`, which is
193 eta-equivalent.  The `k`'s are continuations: functions from something
194 to a result.  Let's use &sigma; as the result type.  The each `k` in
195 the transform will be a function of type &rho; --> &sigma; for some
196 choice of &rho;.
198 We'll need an ancilliary function ': for any ground type a, a' = a;
199 for functional types a->b, (a->b)' = ((a' -> o) -> o) -> (b' -> o) -> o.
201     Call by name transform
203     Terms                            Types
205     [x] = \k.xk                      [a] = (a'->o)->o
206     [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->o)->o
207     [MN] = \k.[M](\m.m[N]k)          [b] = (b'->o)->o
209 Remember that types associate to the right.  Let's work through the
210 application xform and make sure the types are consistent.  We'll have
211 the following types:
213     M:a->b
214     N:a
215     MN:b
216     k:b'->o
217     [N]:(a'->o)->o
218     m:((a'->o)->o)->(b'->o)->o
219     m[N]:(b'->o)->o
220     m[N]k:o
221     [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o
222     [M](\m.m[N]k):o
223     [MN]:(b'->o)->o
225 Note that even though the transform uses the same symbol for the
226 translation of a variable, in general it will have a different type in
227 the transformed term.