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=f5b1ef726e2cfa444df2b5fc50562822a90f0b03;hpb=5555d992063202b118a612862085a06291bc6f47 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:
```      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
+This is almost the same `lift2` predicate we defined in order to allow
+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.

-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.
```