+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 defined:
+
+ [x] = x
+ [\xM] = \k.k(\x[M])
+ [MN] = \k.[M](\m.m[N]k)
+
+Here's the result of applying the transform to our simple example:
+
+ [(\x.y)((\x.z)u)] =
+ \k.[\x.y](\m.m[(\x.z)u]k) =
+ \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[u]k))k) =
+ \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.muk))k)
+
+Because the initial `\k` protects (i.e., takes scope over) the entire
+transformed term, we can't perform any reductions. In order to watch
+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)u)] I =
+ (\k.[\x.y](\m.m[(\x.z)u]k)) I
+ *
+ [\x.y](\m.m[(\x.z)u] I) =
+ (\k.k(\x.y))(\m.m[(\x.z)u] I)
+ * *
+ (\x.y)[(\x.z)u] I --A--
+ *
+ y I
+
+The application to `I` unlocks the leftmost functor. Because that
+functor (`\x.y`) throws away its argument (consider the reduction in the
+line marked (A)), we never need to expand the
+CPS transform of the argument. This means that we never bother to
+reduce redexes inside 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:
+
+ {(\x.y)((\x.z)u)} I =
+ (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I
+ *
+ {\x.y}(\m.{(\x.z)u}(\n.mnI)) =
+ (\k.k(\x.{y}))(\m.{(\x.z)u}(\n.mnI))
+ * *
+ {(\x.z)u}(\n.(\x.{y})nI) =
+ (\k.{\x.z}(\m.{u}(\n.mnk)))(\n.(\x.{y})nI)
+ *
+ {\x.z}(\m.{u}(\n.mn(\n.(\x.{y})nI))) =
+ (\k.k(\x.{z}))(\m.{u}(\n.mn(\n.(\x.{y})nI)))
+ * *
+ {u}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
+ (\k.ku)(\n.(\x.{z})n(\n.(\x.{y})nI))
+ * *
+ (\x.{z})u(\n.(\x.{y})nI) --A--
+ *
+ {z}(\n.(\x.{y})nI) =
+ (\k.kz)(\n.(\x.{y})nI)
+ * *
+ (\x.{y})zI
+ *
+ {y}I =
+ (\k.ky)I
+ *
+ I y
+
+In this case, the argument does get evaluated: consider the reduction
+in the line marked (A).
+
+Both xforms make the following guarantee: as long as redexes
+underneath a lambda are never evaluated, there will be at most one
+reduction available at any step in the evaluation.
+That is, all choice is removed from the evaluation process.
+
+Now let's verify that the CBN CPS avoids the infinite reduction path
+discussed above (remember that `w = \x.xx`):
+
+ [(\x.y)(ww)] I =
+ (\k.[\x.y](\m.m[ww]k)) I
+ *
+ [\x.y](\m.m[ww]I) =
+ (\k.k(\x.y))(\m.m[ww]I)
+ * *
+ (\x.y)[ww]I
+ *
+ y I
+
+
+Questions and exercises:
+
+1. Prove that {(\x.y)(ww)} does not terminate.
+
+2. Why is the CBN xform for variables `[x] = x' instead of something
+involving kappas?
+
+3. Write an Ocaml function that takes a lambda term and returns a
+CPS-xformed lambda term. You can use the following data declaration:
+
+ type form = Var of char | Abs of char * form | App of form * form;;
+
+4. The discussion above talks about the "leftmost" redex, or the
+"rightmost". But these words apply accurately only in a special set
+of terms. Characterize the order of evaluation for CBN (likewise, for
+CBV) more completely and carefully.