rename topics/_coroutines_and_aborts.mdwn to topics/week13_coroutines_exceptions_and_...

[lambda.git] / topics / week10_gsv.mdwn

diff --git a/topics/week10_gsv.mdwn b/topics/week10_gsv.mdwn
index 96786ca..8afe744 100644 (file)
--- a/topics/week10_gsv.mdwn
+++ b/topics/week10_gsv.mdwn
@@ -116,15 +116,15 @@ Compute the following:
 
     1. {(w,g)}[∃x.man(x)]
 
-       = {(w,g[n->a])}[man(x)] ++ {(w,g[n->b])}[man(x)] 
-                               ++ {(w,g[n->c])}[man(x)] 
-       = {} ++ {(w,g[n->b])} ++ {(w,g[n->c])}
-       = {(w,g[n->a]),(w,g[n->b]),(w,g[n->c])}
+       = {(w,g[x->a])}[man(x)] ++ {(w,g[x->b])}[man(x)] 
+                               ++ {(w,g[x->c])}[man(x)] 
+       = {} ++ {(w,g[x->b])} ++ {(w,g[x->c])}
+       = {(w,g[x->a]),(w,g[x->b]),(w,g[x->c])}
        -- Bob and Carl are men
 
     2. {(w,g)}[∃x.woman(x)]
     3. {(w,g)}[∃x∃y.man(x) and man(y)]
-    4. {(w,n,r,g)}[∃x∃y.x=y]
+    4. {(w,g)}[∃x∃y.x=y]
 
 Running the [[code|code/gsv.ml]] gives the answers.
 
@@ -391,7 +391,7 @@ two worlds.
         ---------------  ---------------
     w:  a  true          a  false
         b  false         b  true
-        c  true          c  false
+        c  false         c  false
 
     w': a  false         a  false
         b  false         b  false
@@ -412,12 +412,10 @@ Let's see how this works out in detail.
 
          -- existential introduces new peg
 
-       = (   {(w,g[x->a])}[closet(x)]
-          ++ {(w,g[x->b])}[closet(x)]
-          ++ {(w,g[x->c])}[closet(x)]
-          ++ {(w',g[x->a])}[closet(x)]
-          ++ {(w',g[x->b])}[closet(x)]
-          ++ {(w',g[x->c])}[closet(x)])[◊guilty(x)]
+       = (   {(w,g[x->a]), (w',g[x->a])}[closet(x)]
+          ++ {(w,g[x->b]), (w',g[x->b])}[closet(x)]
+          ++ {(w,g[x->c]), (w',g[x->c])}[closet(x)]
+                                                    )[◊guilty(x)]
 
          -- only possibilities in which x is in the closet survive
          -- the first update
@@ -437,12 +435,9 @@ Now we consider the second half:
 
          {(w,g), (w',g)}[∃x(closet(x) & ◊guilty(x))]
        
-       =    {(w,g[x->a])}[closet(x)][◊guilty(x)]
-         ++ {(w,g[x->b])}[closet(x)][◊guilty(x)]
-         ++ {(w,g[x->c])}[closet(x)][◊guilty(x)]
-         ++ {(w',g[x->a])}[closet(x)][◊guilty(x)]
-         ++ {(w',g[x->b])}[closet(x)][◊guilty(x)]
-         ++ {(w',g[x->c])}[closet(x)][◊guilty(x)]
+       =    {(w,g[x->a]), (w',g[x->a])}[closet(x)][◊guilty(x)]
+         ++ {(w,g[x->b]), (w',g[x->b])}[closet(x)][◊guilty(x)]
+         ++ {(w,g[x->c]), (w',g[x->c])}[closet(x)][◊guilty(x)]
 
           -- filter out possibilities in which x is not in the closet
           -- and filter out possibilities in which x is not guilty
@@ -451,10 +446,10 @@ Now we consider the second half:
 
        = {(w',g[x->c])}
 
-The result is different.  Fewer possibilities remain.  We have one of
-the possible worlds (w is ruled out), and we have ruled out possible
-discourses (x cannot refer to Alice).  So the second formula is more
-informative.
+The result is different.  Fewer possibilities remain.  We have
+eliminated one of the possible worlds (w is ruled out), and we have
+eliminated one of the possible discourses (x cannot refer to Alice).
+So the second formula is more informative.
 
 One of main conclusions of GSV is that in the presence of modality,
 the hallmark of dynamic treatments--that existentials bind outside of