- Form Examples
-Variable a x, y, z
-Abstract \aM \x.x, \x.y, \x.\y.y
-Application MN (x x), ((\x.x) y), ((\x.x)(\y.y))
-</pre>
+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:
+
+ <x> => \k.kx
+ <\aM> => \k.k(\a<M>)
+ <MN> => \k.<M>(\m.<N>(\n.mnk))
+
+This time the reduction unfolds in a different manner: