[lambda.git] / intensionality_monad.mdwn

The intensionality monad
------------------------

In the meantime, we'll look at several linguistic applications for
monads, based on what's called the *reader monad*, starting with
intensional function application.  

First, the familiar linguistic problem:

           Bill left.  
           Cam left.
           Ann believes [Bill left].
           Ann believes [Cam left].

We want an analysis on which all four of these sentences can be true
simultaneously.  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.

In Shan (2001) [Monads for natural language
semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that making
expressions sensitive to the world of evaluation is conceptually the
same thing as making use of a *reader monad*.  This technique was
beautifully re-invented by Ben-Avi and Winter (2007) in their paper [A
modular approach to
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 

        # #use "intensionality-monad.ml";;

Note the extra `#` attached to the directive `use`.

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>
Extensional types              Intensional types       Examples
-------------------------------------------------------------------

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
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
take intensional 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).
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
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:

In OCaml, we'll use integers to model possible worlds:

        type s = int;;
        type e = char;;
        type t = bool;;

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.

<pre>
let ann = 'a';;
let bill = 'b';;
let cam = 'c';;

let left1 (x:e) = true;; 
let saw1 (x:e) (y:e) = y < x;; 

left1 ann;;
saw1 bill ann;; (* true *)
saw1 ann bill;; (* false *)
</pre>

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

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:

    let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;

This new definition says that everyone always left, except that 
in world 2, Cam didn't leave.

    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.

Just to keep things straight, let's get the facts of the world set:

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

Now we are ready for the intensionality monad:

<pre>
type 'a intension = s -> 'a;;
let unit x (w:s) = x;;
let bind m f (w:s) = f (m w) w;;
</pre>

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.

Then combining a prediction like *left* which is extensional in its
subject argument with a monadic subject like `unit ann` is simply bind
in action:

    bind (unit ann) left 1;; (* true: Ann left in world 1 *)
    bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)

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

We can arrange for an extensional transitive verb to take intensional
arguments:

    let lift 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.

<pre>
lift saw (unit bill) (unit ann) 1;;  (* true *)
lift saw (unit bill) (unit ann) 2;;  (* false *)
</pre>

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

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

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

    bind (unit ann) (thinks (bind (unit cam) left)) 1;;

But even in world 1, Ann doesn't believe that Cam left (even though he
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.