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
--------------------------