X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=reader_monad_for_intensionality.mdwn;h=4159f845c8325643ad4c355608c3e7db6ba06ec2;hp=7425be417683bf126d7841d5fd3ac08ccc94609d;hb=acdcd8024b3b3da1396069dba591a2f40f55efcc;hpb=5555d992063202b118a612862085a06291bc6f47;ds=sidebyside

diff --git a/reader_monad_for_intensionality.mdwn b/reader_monad_for_intensionality.mdwn
index 7425be41..4159f845 100644
--- a/reader_monad_for_intensionality.mdwn
+++ b/reader_monad_for_intensionality.mdwn
@@ -103,18 +103,37 @@ worlds, the meaning of *leave* must depend on the world in which it is
 being evaluated:
 
     let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;
+    left ann 1;; (* true: Ann left in world 1 *)
+    left cam 2;; (* false: Cam didn't leave in world 2 *) 
 
 This new definition says that everyone always left, except that 
 in world 2, Cam didn't leave.
 
+Note that although this general *left* is sensitive to world of
+evaluation, it does not have the fully intensionalized type given in
+the chart above, which was `(s->e)->s->t`.  This is because
+*left* does not exploit the additional resolving power provided by
+making the subject an individual concept.  In semantics jargon, we say
+that *leave* is extensional with respect to its first argument.  
+
+Therefore we will adopt the general strategy of defining predicates
+in a way that they take arguments of the lowest type that will allow
+us to make all the distinctions the predicate requires.  When it comes
+time to combine this predicate with monadic arguments, we'll have to
+make use of various lifting predicates.
+
+Likewise, although *see* depends on the world of evaluation, it is
+extensional in both of its syntactic arguments:
+
     let saw x y w = (w < 2) && (y < x);;
     saw bill ann 1;; (* true: Ann saw Bill in world 1 *)
     saw bill ann 2;; (* false: no one saw anyone in world 2 *)
 
-Along similar lines, this general version of *see* coincides with the
-`saw1` function we defined above for world 1; in world 2, no one saw anyone.
+This (again, partially) intensionalized version of *see* coincides
+with the `saw1` function we defined above for world 1; in world 2, no
+one saw anyone.
 
-Just to keep things straight, let's get the facts of the world set:
+Just to keep things straight, let's review the facts:
 
 <pre>
      World 1: Everyone left.
@@ -151,17 +170,26 @@ individual concept `unit ann`, apply it to the world of evaluation in
 order to get hold of an individual (`'a'`), then feed that individual
 to the extensional predicate *left*.
 
-We can arrange for an extensional transitive verb to take intensional
-arguments:
+We can arrange for a transitive verb that is extensional in both of
+its arguments to take intensional arguments:
 
-    let lift2 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.
+This is almost the same `lift2` predicate we defined in order to allow
+addition in our division monad example.  The difference is that this
+variant operates on verb meanings that take extensional arguments but
+returns an intensional result.  Thus the original `lift2` predicate
+has `unit (f x y)` where we have just `f x y` here.
+  
+The use of `bind` here to combine *left* with an individual concept,
+and the use of `lift2'` to combine *see* with two intensional
+arguments closely parallels the two of Montague's meaning postulates
+(in PTQ) that express the relationship between extensional verbs and
+their uses in intensional contexts.
 
 <pre>
-lift2 saw (unit bill) (unit ann) 1;;  (* true *)
-lift2 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.