X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=intensionality_monad.mdwn;h=5598e42c39d1c5bb24e2cf10df6ca317e7d41c06;hp=acf154cf645119be9bbc181d24859f4eb4cb58c2;hb=89886f346dd46b9f8b35fed6094dc5b999b74354;hpb=e8a135f7bc1a0aa4118703baa78ec8d2ea9db490

diff --git a/intensionality_monad.mdwn b/intensionality_monad.mdwn
index acf154cf..5598e42c 100644
--- a/intensionality_monad.mdwn
+++ b/intensionality_monad.mdwn
@@ -1,9 +1,9 @@
 Now we'll look at using monads to do intensional function application.
-This really is just another application of the reader monad, not a new monad.
+This really is just another application of the Reader monad, not a new monad.
 In Shan (2001) [Monads for natural
 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
 making expressions sensitive to the world of evaluation is conceptually
-the same thing as making use of the reader monad.
+the same thing as making use of the Reader monad.
 This technique was beautifully re-invented
 by Ben-Avi and Winter (2007) in their paper [A modular
 approach to
@@ -90,13 +90,13 @@ In OCaml, we'll use integers to model possible worlds. Characters (characters in
 	let left1 (x:e) = true;; 
 	let saw1 (x:e) (y:e) = y < x;; 
 
-	left1 ann;;
+	left1 ann;; (* true *)
 	saw1 bill ann;; (* true *)
 	saw1 ann bill;; (* false *)
 
 So here's our extensional system: everyone left, including Ann;
-and Ann saw Bill, but Bill didn't see Ann.  (Note that Ocaml word
-order is VOS, verb-object-subject.)
+and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann.  (Note that the word
+order we're using is VOS, verb-object-subject.)
 
 Now we add intensions.  Because different people leave in different
 worlds, the meaning of *leave* must depend on the world in which it is
@@ -128,7 +128,7 @@ Now we are ready for the intensionality monad:
 <pre>
 type 'a intension = s -> 'a;;
 let unit x = fun (w:s) -> x;;
-let bind m f = fun (w:s) -> f (m w) w;;
+let bind u f = fun (w:s) -> f (u w) w;;
 </pre>
 
 Then the individual concept `unit ann` is a rigid designator: a
@@ -136,7 +136,7 @@ constant function from worlds to individuals that returns `'a'` no
 matter which world is used as an argument.  This is a typical kind of
 thing for a monad unit to do.
 
-Then combining a prediction like *left* which is extensional in its
+Then combining a predicate like *left* which is extensional in its
 subject argument with an intensional subject like `unit ann` is simply bind
 in action:
 
@@ -152,14 +152,14 @@ to the extensional predicate *left*.
 We can arrange for an extensional transitive verb to take intensional
 arguments:
 
-    let lift f u v = bind u (fun x -> bind v (fun y -> f x y));;
+    let lift2 f u v = bind u (fun x -> bind v (fun y -> f x y));;
 
 This is the exact same lift predicate we defined in order to allow
 addition in our division monad example.
 
 <pre>
-lift saw (unit bill) (unit ann) 1;;  (* true *)
-lift saw (unit bill) (unit ann) 2;;  (* false *)
+lift2 saw (unit bill) (unit ann) 1;;  (* true *)
+lift2 saw (unit bill) (unit ann) 2;;  (* false *)
 </pre>
 
 Ann did see bill in world 1, but Ann didn't see Bill in world 2.
@@ -183,8 +183,8 @@ So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
 
     bind (unit ann) (thinks (bind (unit cam) left)) 1;;
 
-But even in world 1, Ann doesn't believe that Cam left (even though he
-did: `bind (unit cam) left 1 == true`).  Ann's thoughts are hung up on
+But in world 1, Ann doesn't believe that Cam left (even though he
+did leave in world 1: `bind (unit cam) left 1 == true`).  Ann's thoughts are hung up on
 what is happening in world 2, where Cam doesn't leave.
 
 *Small project*: add intersective ("red") and non-intersective