leafs->leaves
[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     left ann 1;; (* true: Ann left in world 1 *)
107     left cam 2;; (* false: Cam didn't leave in world 2 *) 
108
109 This new definition says that everyone always left, except that 
110 in world 2, Cam didn't leave.
111
112 Note that although this general *left* is sensitive to world of
113 evaluation, it does not have the fully intensionalized type given in
114 the chart above, which was `(s->e)->s->t`.  This is because
115 *left* does not exploit the additional resolving power provided by
116 making the subject an individual concept.  In semantics jargon, we say
117 that *leave* is extensional with respect to its first argument.  
118
119 Therefore we will adopt the general strategy of defining predicates
120 in a way that they take arguments of the lowest type that will allow
121 us to make all the distinctions the predicate requires.  When it comes
122 time to combine this predicate with monadic arguments, we'll have to
123 make use of various lifting predicates.
124
125 Likewise, although *see* depends on the world of evaluation, it is
126 extensional in both of its syntactic arguments:
127
128     let saw x y w = (w < 2) && (y < x);;
129     saw bill ann 1;; (* true: Ann saw Bill in world 1 *)
130     saw bill ann 2;; (* false: no one saw anyone in world 2 *)
131
132 This (again, partially) intensionalized version of *see* coincides
133 with the `saw1` function we defined above for world 1; in world 2, no
134 one saw anyone.
135
136 Just to keep things straight, let's review the facts:
137
138 <pre>
139      World 1: Everyone left.
140               Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.              
141      World 2: Ann left, Bill left, Cam didn't leave.
142               No one saw anyone.
143 </pre>
144
145 Now we are ready for the intensionality monad:
146
147 <pre>
148 type 'a intension = s -> 'a;;
149 let unit x = fun (w:s) -> x;;
150 (* as before, bind can be written more compactly, but having
151    it spelled out like this will be useful down the road *)
152 let bind u f = fun (w:s) -> let a = u w in let u' = f a in u' w;;
153 </pre>
154
155 Then the individual concept `unit ann` is a rigid designator: a
156 constant function from worlds to individuals that returns `'a'` no
157 matter which world is used as an argument.  This is a typical kind of
158 thing for a monad unit to do.
159
160 Then combining a predicate like *left* which is extensional in its
161 subject argument with an intensional subject like `unit ann` is simply bind
162 in action:
163
164     bind (unit ann) left 1;; (* true: Ann left in world 1 *)
165     bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *)
166
167 As usual, bind takes a monad box containing Ann, extracts Ann, and
168 feeds her to the extensional *left*.  In linguistic terms, we take the
169 individual concept `unit ann`, apply it to the world of evaluation in
170 order to get hold of an individual (`'a'`), then feed that individual
171 to the extensional predicate *left*.
172
173 We can arrange for a transitive verb that is extensional in both of
174 its arguments to take intensional arguments:
175
176     let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));;
177
178 This is almost the same `lift2` predicate we defined in order to allow
179 addition in our division monad example.  The difference is that this
180 variant operates on verb meanings that take extensional arguments but
181 returns an intensional result.  Thus the original `lift2` predicate
182 has `unit (f x y)` where we have just `f x y` here.
183   
184 The use of `bind` here to combine *left* with an individual concept,
185 and the use of `lift2'` to combine *see* with two intensional
186 arguments closely parallels the two of Montague's meaning postulates
187 (in PTQ) that express the relationship between extensional verbs and
188 their uses in intensional contexts.
189
190 <pre>
191 lift2' saw (unit bill) (unit ann) 1;;  (* true *)
192 lift2' saw (unit bill) (unit ann) 2;;  (* false *)
193 </pre>
194
195 Ann did see bill in world 1, but Ann didn't see Bill in world 2.
196
197 Finally, we can define our intensional verb *thinks*.  *Think* is
198 intensional with respect to its sentential complement, though still extensional
199 with respect to its subject.  (As Montague noticed, almost all verbs
200 in English are extensional with respect to their subject; a possible
201 exception is "appear".)
202
203     let thinks (p:s->t) (x:e) (w:s) = 
204       match (x, p 2) with ('a', false) -> false | _ -> p w;;
205
206 Ann disbelieves any proposition that is false in world 2.  Apparently,
207 she firmly believes we're in world 2.  Everyone else believes a
208 proposition iff that proposition is true in the world of evaluation.
209
210     bind (unit ann) (thinks (bind (unit bill) left)) 1;;
211
212 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
213
214     bind (unit ann) (thinks (bind (unit cam) left)) 1;;
215
216 But in world 1, Ann doesn't believe that Cam left (even though he
217 did leave in world 1: `bind (unit cam) left 1 == true`).  Ann's thoughts are hung up on
218 what is happening in world 2, where Cam doesn't leave.
219
220 *Small project*: add intersective ("red") and non-intersective
221  adjectives ("good") to the fragment.  The intersective adjectives
222  will be extensional with respect to the nominal they combine with
223  (using bind), and the non-intersective adjectives will take
224  intensional arguments.
225
226