changes

[lambda.git] / cps.mdwn

diff --git a/cps.mdwn b/cps.mdwn
index f869b79..a3f0459 100644 (file)
--- a/cps.mdwn
+++ b/cps.mdwn
@@ -216,9 +216,9 @@ for functional types a->b, (a->b)' = ((a' -> σ) -> σ) -> (b' -> &sig
 
     Terms                            Types
 
-    [x] = \k.xk                      [a] = (a'->σ)->σ
-    [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->σ)->σ
-    [MN] = \k.[M](\m.m[N]k)          [b] = (b'->σ)->σ
+    [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
@@ -227,14 +227,14 @@ the following types:
     M:a->b
     N:a
     MN:b 
-    k:b'->σ
-    [N]:(a'->σ)->σ
-    m:((a'->σ)->σ)->(b'->σ)->σ
-    m[N]:(b'->σ)->σ
-    m[N]k:σ 
-    [M]:((a->b)'->σ)->σ = ((((a'->σ)->σ)->(b'->σ)->σ)->σ)->σ
-    [M](\m.m[N]k):σ
-    [MN]:(b'->σ)->σ
+    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