(no commit message)
[lambda.git] / reader_monad_for_intensionality.mdwn
1 Now we'll look at using monads to do intensional function application.
2 This is just another application of the Reader monad, not a new monad.
3 In Shan (2001) [Monads for natural
4 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
5 making expressions sensitive to the world of evaluation is conceptually
6 the same thing as making use of the Reader monad.
7 This technique was beautifully re-invented
8 by Ben-Avi and Winter (2007) in their paper [A modular
9 approach to
10 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
11 though without explicitly using monads.
12
13 All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
14 To run it, download the file, start OCaml, and say 
15
16         # #use "intensionality-monad.ml";;
17
18 Note the extra `#` attached to the directive `use`.
19
20 First, the familiar linguistic problem:
21
22        Bill left.  
23            Cam left.
24            Ann believes [Bill left].
25            Ann believes [Cam left].
26
27 We want an analysis on which the first three sentences can be true at
28 the same time that the last sentence is false.  If sentences denoted
29 simple truth values or booleans, we have a problem: if the sentences
30 *Bill left* and *Cam left* are both true, they denote the same object,
31 and Ann's beliefs can't distinguish between them.
32
33 The traditional solution to the problem sketched above is to allow
34 sentences to denote a function from worlds to truth values, what
35 Montague called an intension.  So if `s` is the type of possible
36 worlds, we have the following situation:
37
38
39 <pre>
40 Extensional types              Intensional types       Examples
41 -------------------------------------------------------------------
42
43 S         t                    s->t                    John left
44 DP        e                    s->e                    John
45 VP        e->t                 (s->e)->s->t            left
46 Vt        e->e->t              (s->e)->(s->e)->s->t    saw
47 Vs        t->e->t              (s->t)->(s->e)->s->t    thought
48 </pre>
49
50 This system is modeled on the way Montague arranged his grammar.
51 There are significant simplifications: for instance, determiner
52 phrases are thought of as corresponding to individuals rather than to
53 generalized quantifiers.  
54
55 The main difference between the intensional types and the extensional
56 types is that in the intensional types, the arguments are functions
57 from worlds to extensions: intransitive verb phrases like "left" now
58 take so-called "individual concepts" as arguments (type s->e) rather than plain
59 individuals (type e), and attitude verbs like "think" now take
60 propositions (type s->t) rather than truth values (type t).
61 In addition, the result of each predicate is an intension.
62 This expresses the fact that the set of people who left in one world
63 may be different than the set of people who left in a different world.
64 (Normally, the dependence of the extension of a predicate to the world
65 of evaluation is hidden inside of an evaluation coordinate, or built
66 into the the lexical meaning function, but we've made it explicit here
67 in the way that the intensionality monad makes most natural.)
68
69 The intensional types are more complicated than the extensional
70 types.  Wouldn't it be nice to make the complicated types available
71 for those expressions like attitude verbs that need to worry about
72 intensions, and keep the rest of the grammar as extensional as
73 possible?  This desire is parallel to our earlier desire to limit the
74 concern about division by zero to the division function, and let the
75 other functions, like addition or multiplication, ignore
76 division-by-zero problems as much as possible.
77
78 So here's what we do:
79
80 In OCaml, we'll use integers to model possible worlds. 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:
81
82         type s = int;;
83         type e = char;;
84         type t = bool;;
85
86         let ann = 'a';;
87         let bill = 'b';;
88         let cam = 'c';;
89
90         let left1 (x:e) = true;; 
91         let saw1 (x:e) (y:e) = y < x;; 
92
93         left1 ann;; (* true *)
94         saw1 bill ann;; (* true *)
95         saw1 ann bill;; (* false *)
96
97 So here's our extensional system: everyone left, including Ann;
98 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann.  (Note that the word
99 order we're using is VOS, verb-object-subject.)
100
101 Now we add intensions.  Because different people leave in different
102 worlds, the meaning of *leave* must depend on the world in which it is
103 being evaluated:
104
105     let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;
106
107 This new definition says that everyone always left, except that 
108 in world 2, Cam didn't leave.
109
110     let saw x y w = (w < 2) && (y < x);;
111     saw bill ann 1;; (* true: Ann saw Bill in world 1 *)
112     saw bill ann 2;; (* false: no one saw anyone in world 2 *)
113
114 Along similar lines, this general version of *see* coincides with the
115 `saw1` function we defined above for world 1; in world 2, no one saw anyone.
116
117 Just to keep things straight, let's get the facts of the world set:
118
119 <pre>
120      World 1: Everyone left.
121               Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.              
122      World 2: Ann left, Bill left, Cam didn't leave.
123               No one saw anyone.
124 </pre>
125
126 Now we are ready for the intensionality monad:
127
128 <pre>
129 type 'a intension = s -> 'a;;
130 let unit x = fun (w:s) -> x;;
131 (* as before, bind can be written more compactly, but having
132    it spelled out like this will be useful down the road *)
133 let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
134 </pre>
135
136 Then the individual concept `unit ann` is a rigid designator: a
137 constant function from worlds to individuals that returns `'a'` no
138 matter which world is used as an argument.  This is a typical kind of
139 thing for a monad unit to do.
140
141 Then combining a predicate like *left* which is extensional in its
142 subject argument with an intensional subject like `unit ann` is simply bind
143 in action:
144
145     bind (unit ann) left 1;; (* true: Ann left in world 1 *)
146     bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)
147
148 As usual, bind takes a monad box containing Ann, extracts Ann, and
149 feeds her to the extensional *left*.  In linguistic terms, we take the
150 individual concept `unit ann`, apply it to the world of evaluation in
151 order to get hold of an individual (`'a'`), then feed that individual
152 to the extensional predicate *left*.
153
154 We can arrange for an extensional transitive verb to take intensional
155 arguments:
156
157     let lift2 f u v = bind u (fun x -> bind v (fun y -> f x y));;
158
159 This is the exact same lift predicate we defined in order to allow
160 addition in our division monad example.
161
162 <pre>
163 lift2 saw (unit bill) (unit ann) 1;;  (* true *)
164 lift2 saw (unit bill) (unit ann) 2;;  (* false *)
165 </pre>
166
167 Ann did see bill in world 1, but Ann didn't see Bill in world 2.
168
169 Finally, we can define our intensional verb *thinks*.  *Think* is
170 intensional with respect to its sentential complement, though still extensional
171 with respect to its subject.  (As Montague noticed, almost all verbs
172 in English are extensional with respect to their subject; a possible
173 exception is "appear".)
174
175     let thinks (p:s->t) (x:e) (w:s) = 
176       match (x, p 2) with ('a', false) -> false | _ -> p w;;
177
178 Ann disbelieves any proposition that is false in world 2.  Apparently,
179 she firmly believes we're in world 2.  Everyone else believes a
180 proposition iff that proposition is true in the world of evaluation.
181
182     bind (unit ann) (thinks (bind (unit bill) left)) 1;;
183
184 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
185
186     bind (unit ann) (thinks (bind (unit cam) left)) 1;;
187
188 But in world 1, Ann doesn't believe that Cam left (even though he
189 did leave in world 1: `bind (unit cam) left 1 == true`).  Ann's thoughts are hung up on
190 what is happening in world 2, where Cam doesn't leave.
191
192 *Small project*: add intersective ("red") and non-intersective
193  adjectives ("good") to the fragment.  The intersective adjectives
194  will be extensional with respect to the nominal they combine with
195  (using bind), and the non-intersective adjectives will take
196  intensional arguments.
197
198