From b30e75e7f0899f35323b4ded6495b834cff74a91 Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Wed, 10 Nov 2010 11:09:27 -0500 Subject: [PATCH] fixed discussion of lift in intensionality monad --- intensionality-monad.ml | 6 ++--- reader_monad_for_intensionality.mdwn | 47 ++++++++++++++++++++++++++++-------- 2 files changed, 40 insertions(+), 13 deletions(-) diff --git a/intensionality-monad.ml b/intensionality-monad.ml index d1f21d2d..eebe5ee1 100644 --- a/intensionality-monad.ml +++ b/intensionality-monad.ml @@ -29,13 +29,13 @@ saw bill ann 2;; (* Ann didn't see Bill in world 2 *) type 'a intension = s -> 'a;; let unit x (w:s) = x;; let bind m f (w:s) = f (m w) w;; -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));; bind (unit ann) left 1;; bind (unit cam) left 2;; -lift saw (unit bill) (unit ann) 1;; -lift saw (unit bill) (unit ann) 2;; +lift2' saw (unit bill) (unit ann) 1;; +lift2' saw (unit bill) (unit ann) 2;; let thinks (p:s->t) (x:e) (w:s) = match (x, p 2) with ('a', false) -> false | _ -> p w;; diff --git a/reader_monad_for_intensionality.mdwn b/reader_monad_for_intensionality.mdwn index 7425be41..d10d7477 100644 --- a/reader_monad_for_intensionality.mdwn +++ b/reader_monad_for_intensionality.mdwn @@ -103,18 +103,36 @@ 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 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: 
      World 1: Everyone left.
@@ -151,17 +169,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.  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.
 
 
-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 *)
 

 
 Ann did see bill in world 1, but Ann didn't see Bill in world 2.
-- 
2.11.0