(\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 present a technique for controlling evaluation order by 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. (A redex is a subform ...(\xM)N..., i.e., something that can be the target of beta 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: