1. Prove that {(\x.y)(ww)} does not terminate.
-2. Why is the CBN xform for variables `[x] = x' instead of something
-involving kappas?
+2. Why is the CBN xform for variables `[x] = x` instead of something
+involving kappas (i.e., `k`'s)?
3. Write an Ocaml function that takes a lambda term and returns a
CPS-xformed lambda term. You can use the following data declaration:
5. What happens (in terms of evaluation order) when the application
rule for CBV CPS is changed to `{MN} = \k.{N}(\n.{M}(\m.mnk))`?
+6. A term and its CPS xform are different lambda terms. Yet in some
+sense they "do" the same thing computationally. Make this sense
+precise.
+
Thinking through the types
--------------------------
Excercise: what should the function ' be for the CBV xform? Hint:
see the Meyer and Wand abstract linked above for the answer.
+
+
+Other CPS transforms
+--------------------
+
+It is easy to think that CBN and CBV are the only two CPS transforms.
+(We've already seen a variant on call-by-value one of the excercises above.)
+
+In fact, the number of distinct transforms is unbounded. For
+instance, here is a variant of CBV that uses the same types as CBN:
+
+ <x> = x
+ <\xM> = \k.k(\x<M>)
+ <MN> = \k.<M>(\m.<N>(\n.m(\k.kn)k))
+
+Try reducing `<(\x.x) ((\y.y) (\z.z))> I` to convince yourself that
+this is a version of call-by-value.
+
+Once we have two evaluation strategies that rely on the same types, we
+can mix and match:
+
+ [x] = x
+ <x> = x
+ [\xM] = \k.k(\x<M>)
+ <\xM] = \k.k(\x[M])
+ [MN] = \k.<M>(\m.m<N>k)
+ <MN> = \k.[M](\m.[N](\n.m(\k.kn)k))
+
+This xform interleaves call-by-name and call-by-value in layers,
+according to the depth of embedding.
+(Cf. page 4 of Reynold's 1974 paper ftp://ftp.cs.cmu.edu/user/jcr/reldircont.pdf (equation (4) and the
+explanation in the paragraph below.)