author Chris Barker Fri, 10 Jun 2011 18:53:34 +0000 (14:53 -0400) committer Chris Barker Fri, 10 Jun 2011 18:53:34 +0000 (14:53 -0400)
 cps.mdwn patch | blob | history

index f869b79..a3f0459 100644 (file)
--- a/cps.mdwn
+++ b/cps.mdwn
@@ -216,9 +216,9 @@ for functional types a->b, (a->b)' = ((a' -> &sigma;) -> &sigma;) -> (b' -> &sig

Terms                            Types

Terms                            Types

-    [x] = \k.xk                      [a] = (a'->&sigma;)->&sigma;
-    [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->&sigma;)->&sigma;
-    [MN] = \k.[M](\m.m[N]k)          [b] = (b'->&sigma;)->&sigma;
+    [x] = \k.xk                      [a] = (a'->o)->o
+    [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->o)->o
+    [MN] = \k.[M](\m.m[N]k)          [b] = (b'->o)->o

Remember that types associate to the right.  Let's work through the
application xform and make sure the types are consistent.  We'll have

Remember that types associate to the right.  Let's work through the
application xform and make sure the types are consistent.  We'll have
@@ -227,14 +227,14 @@ the following types:
M:a->b
N:a
MN:b
M:a->b
N:a
MN:b
-    k:b'->&sigma;
-    [N]:(a'->&sigma;)->&sigma;
-    m:((a'->&sigma;)->&sigma;)->(b'->&sigma;)->&sigma;
-    m[N]:(b'->&sigma;)->&sigma;
-    m[N]k:&sigma;
-    [M]:((a->b)'->&sigma;)->&sigma; = ((((a'->&sigma;)->&sigma;)->(b'->&sigma;)->&sigma;)->&sigma;)->&sigma;
-    [M](\m.m[N]k):&sigma;
-    [MN]:(b'->&sigma;)->&sigma;
+    k:b'->o
+    [N]:(a'->o)->o
+    m:((a'->o)->o)->(b'->o)->o
+    m[N]:(b'->o)->o
+    m[N]k:o
+    [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o
+    [M](\m.m[N]k):o
+    [MN]:(b'->o)->o

Be aware that even though the transform uses the same symbol for the
translation of a variable (i.e., `[x] = x`), in general the variable

Be aware that even though the transform uses the same symbol for the
translation of a variable (i.e., `[x] = x`), in general the variable