From: Chris Barker Date: Thu, 9 Jun 2011 21:27:46 +0000 (-0400) Subject: changes X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=b182d028574a85cb3bf9d8105f054c8ea6a99b03 changes --- 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
-   [MN] = \k.(\m.mk)
-    = \k.[M](\m.[N](\n.mnk))
+   [MN] = \k.{M}(\m.m{N}k)
+   {MN} = \k.[M](\m.[N](\n.mnk))
 
Thinking through the types