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.
<pre>
type 'a intension = s -> 'a;;
let unit x = fun (w:s) -> x;;
-let bind u f = fun (w:s) -> f (u w) w;;
+(* as before, bind can be written more compactly, but having
+ it spelled out like this will be useful down the road *)
+let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
</pre>
Then the individual concept `unit ann` is a rigid designator: a
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.