tweak week12: caps

[lambda.git] / reader_monad_for_intensionality.mdwn

diff --git a/reader_monad_for_intensionality.mdwn b/reader_monad_for_intensionality.mdwn
index 7425be4..4159f84 100644 (file)
--- 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;;
 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.
 
 
 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 *)
 
     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.
 
 <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*.
 
 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>
 
 <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.
 </pre>
 
 Ann did see bill in world 1, but Ann didn't see Bill in world 2.