From b182d028574a85cb3bf9d8105f054c8ea6a99b03 Mon Sep 17 00:00:00 2001
From: Chris Barker
Date: Thu, 9 Jun 2011 17:27:46 -0400
Subject: [PATCH] changes
---
cps.mdwn | 42 +++++++++++++++++++++---------------------
1 file changed, 21 insertions(+), 21 deletions(-)
diff --git a/cps.mdwn b/cps.mdwn
index a9842d12..bb478c65 100644
--- a/cps.mdwn
+++ b/cps.mdwn
@@ -115,27 +115,27 @@ CPS transform of the argument.
Compare with a call-by-value xform:
- => \k.kx
- <\aM> => \k.k(\a)
- => \k.(\m.(\n.mnk))
+ {x} => \k.kx
+ {\aM} => \k.k(\a{M})
+ {MN} => \k.{M}(\m.{N}(\n.mnk))
This time the reduction unfolds in a different manner:
- <(\x.y)((\x.z)w)> I
- (\k.<\x.y>(\m.<(\x.z)w>(\n.mnk))) I
- <\x.y>(\m.<(\x.z)w>(\n.mnI))
- (\k.k(\x.))(\m.<(\x.z)w>(\n.mnI))
- <(\x.z)w>(\n.(\x.)nI)
- (\k.<\x.z>(\m.(\n.mnk)))(\n.(\x.)nI)
- <\x.z>(\m.(\n.mn(\n.(\x.)nI)))
- (\k.k(\x.))(\m.(\n.mn(\n.(\x.)nI)))
- (\n.(\x.)n(\n.(\x.)nI))
- (\k.kw)(\n.(\x.)n(\n.(\x.)nI))
- (\x.)w(\n.(\x.)nI)
- (\n.(\x.)nI)
- (\k.kz)(\n.(\x.)nI)
- (\x.)zI
- I
+ {(\x.y)((\x.z)w)} I
+ (\k.{\x.y}(\m.{(\x.z)w}(\n.mnk))) I
+ {\x.y}(\m.{(\x.z)w}(\n.mnI))
+ (\k.k(\x.{y}))(\m.{(\x.z)w}(\n.mnI))
+ {(\x.z)w}(\n.(\x.{y})nI)
+ (\k.{\x.z}(\m.{w}(\n.mnk)))(\n.(\x.{y})nI)
+ {\x.z}(\m.{w}(\n.mn(\n.(\x.{y})nI)))
+ (\k.k(\x.{z}))(\m.{w}(\n.mn(\n.(\x.{y})nI)))
+ {w}(\n.(\x.{z})n(\n.(\x.{y})nI))
+ (\k.kw)(\n.(\x.{z})n(\n.(\x.{y})nI))
+ (\x.{z})w(\n.(\x.{y})nI)
+ {z}(\n.(\x.{y})nI)
+ (\k.kz)(\n.(\x.{y})nI)
+ (\x.{y})zI
+ {y}I
(\k.ky)I
I y
@@ -157,13 +157,13 @@ CPS-xformed lambda term. You can use the following data declaration:
3. What happens (in terms of evaluation order) when the application
rule for CBN CPS is changed to `[MN] = \k.[N](\n.[M]nk)`? Likewise,
What happens when the application rule for CBV CPS is changed to
-` = \k.(\n.(\m.mnk))`?
+`{MN} = \k.{N}(\n.{M}(\m.mnk))`?
4. What happens when the application rules for the CPS xforms are changed to