Gaining control over order of evaluation ---------------------------------------- We know that evaluation order matters. We're beginning to learn how to gain some control over order of evaluation (think of Jim's abort handler). We continue to reason about order of evaluation. A lucid discussion of evaluation order in the context of the lambda calculus can be found here: [Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf). Sestoft also provides a lovely on-line lambda evaluator: [Sestoft: Lambda calculus reduction workbench] (http://www.itu.dk/~sestoft/lamreduce/index.html), which allows you to select multiple evaluation strategies, and to see reductions happen step by step. Evaluation order matters ------------------------ We've seen this many times. For instance, consider the following reductions. It will be convenient to use the abbreviation `w = \x.xx`. I'll indicate which lambda is about to be reduced with a * underneath:
(\x.y)(ww) * yDone! We have a normal form. But if we reduce using a different strategy, things go wrong:
(\x.y)(ww) = (\x.y)((\x.xx)w) = * (\x.y)(ww) = (\x.y)((\x.xx)w) = * (\x.y)(ww)Etc. As a second reminder of when evaluation order matters, consider using `Y = \f.(\h.f(hh))(\h.f(hh))` as a fixed point combinator to define a recursive function:
Y (\f n. blah) = (\f.(\h.f(hh))(\h.f(hh))) (\f n. blah) * (\f.f((\h.f(hh))(\h.f(hh)))) (\f n. blah) * (\f.f(f((\h.f(hh))(\h.f(hh))))) (\f n. blah) * (\f.f(f(f((\h.f(hh))(\h.f(hh)))))) (\f n. blah)And we never get the recursion off the ground. Using a Continuation Passing Style transform to control order of evaluation --------------------------------------------------------------------------- We'll exhibit and explore the technique of transforming a lambda term using a Continuation Passing Style transform (CPS), then we'll explore what the CPS is doing, and how. In order for the CPS to work, we have to adopt a new restriction on beta reduction: beta reduction does not occur underneath a lambda. That is, `(\x.y)z` reduces to `z`, but `\w.(\x.y)z` does not, because the `\w` protects the redex in the body from reduction. Start with a simple form that has two different reduction paths: reducing the leftmost lambda first: `(\x.y)((\x.z)w) ~~> y' reducing the rightmost lambda first: `(\x.y)((\x.z)w) ~~> (x.y)z ~~> y' After using the following call-by-name CPS transform---and assuming that we never evaluate redexes protected by a lambda---only the first reduction path will be available: we will have gained control over the order in which beta reductions are allowed to be performed. Here's the CPS transform: [x] => x [\xM] => \k.k(\x[M]) [MN] => \k.[M](\m.m[N]k) Here's the result of applying the transform to our problem term: [(\x.y)((\x.z)w)] \k.[\x.y](\m.m[(\x.z)w]k) \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[w]k))k) \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.mwk))k) Because the initial `\k` protects the entire transformed term, we can't perform any reductions. In order to see the computation unfold, we have to apply the transformed term to a trivial continuation, usually the identity function `I = \x.x`. [(\x.y)((\x.z)w)] I \k.[\x.y](\m.m[(\x.z)w]k) I [\x.y](\m.m[(\x.z)w] I) (\k.k(\x.y))(\m.m[(\x.z)w] I) (\x.y)[(\x.z)w] I y I The application to `I` unlocks the leftmost functor. Because that functor (`\x.y`) throws away its argument, we never need to expand the CPS transform of the argument. Compare with a call-by-value xform: