cat theory ready

[lambda.git] / intensionality_monad.mdwn

diff --git a/intensionality_monad.mdwn b/intensionality_monad.mdwn
index 36a0cdd..5b0ec3a 100644 (file)
--- a/intensionality_monad.mdwn
+++ b/intensionality_monad.mdwn
@@ -1,6 +1,3 @@
-The "intensionality" monad
---------------------------
-

 Now we'll look at using monads to do intensional function application.
 This really is just another application of the reader monad, not a new monad.
 In Shan (2001) [Monads for natural
 Now we'll look at using monads to do intensional function application.
 This really is just another application of the reader monad, not a new monad.
 In Shan (2001) [Monads for natural


@@ -13,7 +10,6 @@ approach to
 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
 though without explicitly using monads.
 
 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
 though without explicitly using monads.
 

-

 All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
 To run it, download the file, start OCaml, and say 
 
 All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
 To run it, download the file, start OCaml, and say 
 


@@ -21,55 +17,63 @@ To run it, download the file, start OCaml, and say
 
 Note the extra `#` attached to the directive `use`.
 
 
 Note the extra `#` attached to the directive `use`.
 

-Here's the idea: since people can have different attitudes towards
-different propositions that happen to have the same truth value, we
-can't have sentences denoting simple truth values.  If we did, then if John
-believed that the earth was round, it would force him to believe
-Fermat's last theorem holds, since both propositions are equally true.
-The traditional solution is to allow sentences to denote a function
-from worlds to truth values, what Montague called an intension.  
-So if `s` is the type of possible worlds, we have the following
-situation:
+First, the familiar linguistic problem:
+
+       Bill left.  
+          Cam left.
+          Ann believes [Bill left].
+          Ann believes [Cam left].
+
+We want an analysis on which the first three sentences can be true at
+the same time that the last sentence is false.  If sentences denoted
+simple truth values or booleans, we have a problem: if the sentences
+*Bill left* and *Cam left* are both true, they denote the same object,
+and Ann's beliefs can't distinguish between them.
+
+The traditional solution to the problem sketched above is to allow
+sentences to denote a function from worlds to truth values, what
+Montague called an intension.  So if `s` is the type of possible
+worlds, we have the following situation:

 
 
 <pre>
 
 
 <pre>

-Extensional types                 Intensional types       Examples
+Extensional types              Intensional types       Examples

 -------------------------------------------------------------------
 
 -------------------------------------------------------------------
 

-S         s->t                    s->t                    John left
-DP        s->e                    s->e                    John
-VP        s->e->t                 s->(s->e)->t            left
-Vt        s->e->e->t              s->(s->e)->(s->e)->t    saw
-Vs        s->t->e->t              s->(s->t)->(s->e)->t    thought
+S         t                    s->t                    John left
+DP        e                    s->e                    John
+VP        e->t                 (s->e)->s->t            left
+Vt        e->e->t              (s->e)->(s->e)->s->t    saw
+Vs        t->e->t              (s->t)->(s->e)->s->t    thought

 </pre>
 
 This system is modeled on the way Montague arranged his grammar.
 There are significant simplifications: for instance, determiner
 phrases are thought of as corresponding to individuals rather than to
 </pre>
 
 This system is modeled on the way Montague arranged his grammar.
 There are significant simplifications: for instance, determiner
 phrases are thought of as corresponding to individuals rather than to

-generalized quantifiers.  If you're curious about the initial `s`'s
-in the extensional types, they're there because the behavior of these
-expressions depends on which world they're evaluated at.  If you are
-in a situation in which you can hold the evaluation world constant,
-you can further simplify the extensional types.  Usually, the
-dependence of the extension of an expression on the evaluation world
-is hidden in a superscript, or built into the lexical interpretation
-function.
+generalized quantifiers.  

 
 The main difference between the intensional types and the extensional
 types is that in the intensional types, the arguments are functions
 from worlds to extensions: intransitive verb phrases like "left" now
 
 The main difference between the intensional types and the extensional
 types is that in the intensional types, the arguments are functions
 from worlds to extensions: intransitive verb phrases like "left" now

-take intensional concepts as arguments (type s->e) rather than plain
+take individual concepts as arguments (type s->e) rather than plain

 individuals (type e), and attitude verbs like "think" now take
 propositions (type s->t) rather than truth values (type t).
 individuals (type e), and attitude verbs like "think" now take
 propositions (type s->t) rather than truth values (type t).

+In addition, the result of each predicate is an intension.
+This expresses the fact that the set of people who left in one world
+may be different than the set of people who left in a different world.
+(Normally, the dependence of the extension of a predicate to the world
+of evaluation is hidden inside of an evaluation coordinate, or built
+into the the lexical meaning function, but we've made it explicit here
+in the way that the intensionality monad makes most natural.)

 
 The intenstional types are more complicated than the intensional
 
 The intenstional types are more complicated than the intensional

-types.  Wouldn't it be nice to keep the complicated types to just
-those attitude verbs that need to worry about intensions, and keep the
-rest of the grammar as extensional as possible?  This desire is
-parallel to our earlier desire to limit the concern about division by
-zero to the division function, and let the other functions, like
-addition or multiplication, ignore division-by-zero problems as much
-as possible.
+types.  Wouldn't it be nice to make the complicated types available
+for those expressions like attitude verbs that need to worry about
+intensions, and keep the rest of the grammar as extensional as
+possible?  This desire is parallel to our earlier desire to limit the
+concern about division by zero to the division function, and let the
+other functions, like addition or multiplication, ignore
+division-by-zero problems as much as possible.

 
 So here's what we do:
 
 
 So here's what we do:
 


@@ -83,144 +87,114 @@ Characters (characters in the computational sense, i.e., letters like
 `'a'` and `'b'`, not Kaplanian characters) will model individuals, and
 OCaml booleans will serve for truth values.
 
 `'a'` and `'b'`, not Kaplanian characters) will model individuals, and
 OCaml booleans will serve for truth values.
 

-       type 'a intension = s -> 'a;;
-       let unit x (w:s) = x;;
-
-       let ann = unit 'a';;
-       let bill = unit 'b';;
-       let cam = unit 'c';;
-
-In our monad, the intension of an extensional type `'a` is `s -> 'a`,
-a function from worlds to extensions.  Our unit will be the constant
-function (an instance of the K combinator) that returns the same
-individual at each world.
-
-Then `ann = unit 'a'` is a rigid designator: a constant function from
-worlds to individuals that returns `'a'` no matter which world is used
-as an argument.
-
-Let's test compliance with the left identity law:
-
-       # let bind u f (w:s) = f (u w) w;;
-       val bind : (s -> 'a) -> ('a -> s -> 'b) -> s -> 'b = <fun>
-       # bind (unit 'a') unit 1;;
-       - : char = 'a'
+<pre>
+let ann = 'a';;
+let bill = 'b';;
+let cam = 'c';;

 
 

-We'll assume that this and the other laws always hold.
+let left1 (x:e) = true;; 
+let saw1 (x:e) (y:e) = y < x;; 

 
 

-We now build up some extensional meanings:
+left1 ann;;
+saw1 bill ann;; (* true *)
+saw1 ann bill;; (* false *)
+</pre>

 
 

-       let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
+So here's our extensional system: everyone left, including Ann;
+and Ann saw Bill, but Bill didn't see Ann.  (Note that Ocaml word
+order is VOS, verb-object-subject.)

 
 

-This function says that everyone always left, except for Cam in world
-2 (i.e., `left 2 'c' == false`).
+Now we add intensions.  Because different people leave in different
+worlds, the meaning of *leave* must depend on the world in which it is
+being evaluated:

 
 

-Then the way to evaluate an extensional sentence is to determine the
-extension of the verb phrase, and then apply that extension to the
-extension of the subject:
+    let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;

 
 

-       let extapp fn arg w = fn w (arg w);;
+This new definition says that everyone always left, except that 
+in world 2, Cam didn't leave.

 
 

-       extapp left ann 1;;
-       # - : bool = true
+    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 *)

 
 

-       extapp left cam 2;;
-       # - : bool = false
+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.

 
 

-`extapp` stands for "extensional function application".
-So Ann left in world 1, but Cam didn't leave in world 2.
+Just to keep things straight, let's get the facts of the world set:

 
 

-A transitive predicate:
+<pre>
+     World 1: Everyone left.
+              Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.              
+     World 2: Ann left, Bill left, Cam didn't leave.
+              No one saw anyone.
+</pre>

 
 

-       let saw w x y = (w < 2) && (y < x);;
-       extapp (extapp saw bill) ann 1;; (* true *)
-       extapp (extapp saw bill) ann 2;; (* false *)
+Now we are ready for the intensionality monad:

 
 

-In world 1, Ann saw Bill and Cam, and Bill saw Cam.  No one saw anyone
-in world two.
+<pre>
+type 'a intension = s -> 'a;;
+let unit x (w:s) = x;;
+let bind m f (w:s) = f (m w) w;;
+</pre>

 
 

-Good.  Now for intensions:
+Then the individual concept `unit ann` is a rigid designator: a
+constant function from worlds to individuals that returns `'a'` no
+matter which world is used as an argument.  This is a typical kind of
+thing for a monad unit to do.

 
 

-       let intapp fn arg w = fn w arg;;
+Then combining a prediction like *left* which is extensional in its
+subject argument with an intensional subject like `unit ann` is simply bind
+in action:

 
 

-The only difference between intensional application and extensional
-application is that we don't feed the evaluation world to the argument.
-(See Montague's rules of (intensional) functional application, T4 -- T10.)
-In other words, instead of taking an extension as an argument,
-Montague's predicates take a full-blown intension.  
+    bind (unit ann) left 1;; (* true: Ann left in world 1 *)
+    bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)

 
 

-But for so-called extensional predicates like "left" and "saw", 
-the extra power is not used.  We'd like to define intensional versions
-of these predicates that depend only on their extensional essence.
-Just as we used bind to define a version of addition that interacted
-with the option monad, we now use bind to intensionalize an
-extensional verb:
+As usual, bind takes a monad box containing Ann, extracts Ann, and
+feeds her to the extensional *left*.  In linguistic terms, we take the
+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*.

 
 

-       let lift pred w arg = bind arg (fun x w -> pred w x) w;;
+We can arrange for an extensional transitive verb to take intensional
+arguments:

 
 

-       intapp (lift left) ann 1;; (* true: Ann still left in world 1 *)
-       intapp (lift left) cam 2;; (* false: Cam still didn't leave in world 2 *)
+    let lift f u v = bind u (fun x -> bind v (fun y -> f x y));;

 
 

-Because `bind` unwraps the intensionality of the argument, when the
-lifted "left" receives an individual concept (e.g., `unit 'a'`) as
-argument, it's the extension of the individual concept (i.e., `'a'`)
-that gets fed to the basic extensional version of "left".  (For those
-of you who know Montague's PTQ, this use of bind captures Montague's
-third meaning postulate.)
+This is the exact same lift predicate we defined in order to allow
+addition in our division monad example.

 
 

-Likewise for extensional transitive predicates like "saw":
+<pre>
+lift saw (unit bill) (unit ann) 1;;  (* true *)
+lift saw (unit bill) (unit ann) 2;;  (* false *)
+</pre>

 
 

-       let lift2 pred w arg1 arg2 = 
-         bind arg1 (fun x -> bind arg2 (fun y w -> pred w x y)) w;;
-       intapp (intapp (lift2 saw) bill) ann 1;;  (* true: Ann saw Bill in world 1 *)
-       intapp (intapp (lift2 saw) bill) ann 2;;  (* false: No one saw anyone in world 2 *)
+Ann did see bill in world 1, but Ann didn't see Bill in world 2.

 
 

-Crucially, an intensional predicate does not use `bind` to consume its
-arguments.  Attitude verbs like "thought" are intensional with respect
-to their sentential complement, but extensional with respect to their
-subject (as Montague noticed, almost all verbs in English are
-extensional with respect to their subject; a possible exception is "appear"):
+Finally, we can define our intensional verb *thinks*.  *Think* is
+intensional with respect to its sentential complement, but extensional
+with respect to its subject.  (As Montague noticed, almost all verbs
+in English are extensional with respect to their subject; a possible
+exception is "appear".)

 
 

-       let think (w:s) (p:s->t) (x:e) = 
-         match (x, p 2) with ('a', false) -> false | _ -> p w;;
+    let thinks (p:s->t) (x:e) (w:s) = 
+      match (x, p 2) with ('a', false) -> false | _ -> p w;;

 
 Ann disbelieves any proposition that is false in world 2.  Apparently,
 she firmly believes we're in world 2.  Everyone else believes a
 proposition iff that proposition is true in the world of evaluation.
 
 
 Ann disbelieves any proposition that is false in world 2.  Apparently,
 she firmly believes we're in world 2.  Everyone else believes a
 proposition iff that proposition is true in the world of evaluation.
 

-       intapp (lift (intapp think
-                                                (intapp (lift left)
-                                                                (unit 'b'))))
-                  (unit 'a') 
-       1;; (* true *)
+    bind (unit ann) (thinks (bind (unit bill) left)) 1;;

 
 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
 
 
 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
 

-The `lift` is there because "think Bill left" is extensional wrt its
-subject.  The important bit is that "think" takes the intension of
-"Bill left" as its first argument.
-
-       intapp (lift (intapp think
-                                                (intapp (lift left)
-                                                                (unit 'c'))))
-                  (unit 'a') 
-       1;; (* false *)
+    bind (unit ann) (thinks (bind (unit cam) left)) 1;;

 
 But even in world 1, Ann doesn't believe that Cam left (even though he
 
 But even in world 1, Ann doesn't believe that Cam left (even though he

-did: `intapp (lift left) cam 1 == true`).  Ann's thoughts are hung up
-on what is happening in world 2, where Cam doesn't leave.
+did: `bind (unit cam) left 1 == true`).  Ann's thoughts are hung up on
+what is happening in world 2, where Cam doesn't leave.

 
 *Small project*: add intersective ("red") and non-intersective
  adjectives ("good") to the fragment.  The intersective adjectives
  will be extensional with respect to the nominal they combine with
  (using bind), and the non-intersective adjectives will take
  intensional arguments.
 
 *Small project*: add intersective ("red") and non-intersective
  adjectives ("good") to the fragment.  The intersective adjectives
  will be extensional with respect to the nominal they combine with
  (using bind), and the non-intersective adjectives will take
  intensional arguments.

-
-Finally, note that within an intensional grammar, extensional funtion
-application is essentially just bind:
-
-       # let swap f x y = f y x;;
-       # bind cam (swap left) 2;;
-       - : bool = false
-
-