X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=cps.mdwn;h=4c40a667f2717f9e6b3e61958ca1016672dc9718;hp=6668b48ce1bcde7c63aed5a13b113c376e4bc884;hb=27ce0d45d4ab28840605ec2130f6ba4ecd9d6213;hpb=339a5442b568742f36ddab4a44f77cfb26b609a2

diff --git a/cps.mdwn b/cps.mdwn
index 6668b48c..4c40a667 100644
--- a/cps.mdwn
+++ b/cps.mdwn
@@ -180,8 +180,8 @@ 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?  
+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:
@@ -196,6 +196,10 @@ CBV) more completely and carefully.
 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
 --------------------------
@@ -248,3 +252,34 @@ term.
 
 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.
+