- [(\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
+ [(\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
+ *