week7 tweak
[lambda.git] / intensionality_monad.mdwn
1 The intensionality monad
2 ------------------------
3 In the meantime, we'll look at several linguistic applications for monads, based
4 on
5
6 what's called the *reader monad*.
7 ...
8 intensional function application.  In Shan (2001) [Monads for natural
9 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
10 making expressions sensitive to the world of evaluation is
11 conceptually the same thing as making use of a *reader monad* (which
12 we'll see again soon).  This technique was beautifully re-invented
13 by Ben-Avi and Winter (2007) in their paper [A modular
14 approach to
15 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
16 though without explicitly using monads.
17
18 All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
19 To run it, download the file, start OCaml, and say 
20
21         # #use "intensionality-monad.ml";;
22
23 Note the extra `#` attached to the directive `use`.
24
25 Here's the idea: since people can have different attitudes towards
26 different propositions that happen to have the same truth value, we
27 can't have sentences denoting simple truth values.  If we did, then if John
28 believed that the earth was round, it would force him to believe
29 Fermat's last theorem holds, since both propositions are equally true.
30 The traditional solution is to allow sentences to denote a function
31 from worlds to truth values, what Montague called an intension.  
32 So if `s` is the type of possible worlds, we have the following
33 situation:
34
35
36 <pre>
37 Extensional types                 Intensional types       Examples
38 -------------------------------------------------------------------
39
40 S         s->t                    s->t                    John left
41 DP        s->e                    s->e                    John
42 VP        s->e->t                 s->(s->e)->t            left
43 Vt        s->e->e->t              s->(s->e)->(s->e)->t    saw
44 Vs        s->t->e->t              s->(s->t)->(s->e)->t    thought
45 </pre>
46
47 This system is modeled on the way Montague arranged his grammar.
48 There are significant simplifications: for instance, determiner
49 phrases are thought of as corresponding to individuals rather than to
50 generalized quantifiers.  If you're curious about the initial `s`'s
51 in the extensional types, they're there because the behavior of these
52 expressions depends on which world they're evaluated at.  If you are
53 in a situation in which you can hold the evaluation world constant,
54 you can further simplify the extensional types.  Usually, the
55 dependence of the extension of an expression on the evaluation world
56 is hidden in a superscript, or built into the lexical interpretation
57 function.
58
59 The main difference between the intensional types and the extensional
60 types is that in the intensional types, the arguments are functions
61 from worlds to extensions: intransitive verb phrases like "left" now
62 take intensional concepts as arguments (type s->e) rather than plain
63 individuals (type e), and attitude verbs like "think" now take
64 propositions (type s->t) rather than truth values (type t).
65
66 The intenstional types are more complicated than the intensional
67 types.  Wouldn't it be nice to keep the complicated types to just
68 those attitude verbs that need to worry about intensions, and keep the
69 rest of the grammar as extensional as possible?  This desire is
70 parallel to our earlier desire to limit the concern about division by
71 zero to the division function, and let the other functions, like
72 addition or multiplication, ignore division-by-zero problems as much
73 as possible.
74
75 So here's what we do:
76
77 In OCaml, we'll use integers to model possible worlds:
78
79         type s = int;;
80         type e = char;;
81         type t = bool;;
82
83 Characters (characters in the computational sense, i.e., letters like
84 `'a'` and `'b'`, not Kaplanian characters) will model individuals, and
85 OCaml booleans will serve for truth values.
86
87         type 'a intension = s -> 'a;;
88         let unit x (w:s) = x;;
89
90         let ann = unit 'a';;
91         let bill = unit 'b';;
92         let cam = unit 'c';;
93
94 In our monad, the intension of an extensional type `'a` is `s -> 'a`,
95 a function from worlds to extensions.  Our unit will be the constant
96 function (an instance of the K combinator) that returns the same
97 individual at each world.
98
99 Then `ann = unit 'a'` is a rigid designator: a constant function from
100 worlds to individuals that returns `'a'` no matter which world is used
101 as an argument.
102
103 Let's test compliance with the left identity law:
104
105         # let bind u f (w:s) = f (u w) w;;
106         val bind : (s -> 'a) -> ('a -> s -> 'b) -> s -> 'b = <fun>
107         # bind (unit 'a') unit 1;;
108         - : char = 'a'
109
110 We'll assume that this and the other laws always hold.
111
112 We now build up some extensional meanings:
113
114         let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
115
116 This function says that everyone always left, except for Cam in world
117 2 (i.e., `left 2 'c' == false`).
118
119 Then the way to evaluate an extensional sentence is to determine the
120 extension of the verb phrase, and then apply that extension to the
121 extension of the subject:
122
123         let extapp fn arg w = fn w (arg w);;
124
125         extapp left ann 1;;
126         # - : bool = true
127
128         extapp left cam 2;;
129         # - : bool = false
130
131 `extapp` stands for "extensional function application".
132 So Ann left in world 1, but Cam didn't leave in world 2.
133
134 A transitive predicate:
135
136         let saw w x y = (w < 2) && (y < x);;
137         extapp (extapp saw bill) ann 1;; (* true *)
138         extapp (extapp saw bill) ann 2;; (* false *)
139
140 In world 1, Ann saw Bill and Cam, and Bill saw Cam.  No one saw anyone
141 in world two.
142
143 Good.  Now for intensions:
144
145         let intapp fn arg w = fn w arg;;
146
147 The only difference between intensional application and extensional
148 application is that we don't feed the evaluation world to the argument.
149 (See Montague's rules of (intensional) functional application, T4 -- T10.)
150 In other words, instead of taking an extension as an argument,
151 Montague's predicates take a full-blown intension.  
152
153 But for so-called extensional predicates like "left" and "saw", 
154 the extra power is not used.  We'd like to define intensional versions
155 of these predicates that depend only on their extensional essence.
156 Just as we used bind to define a version of addition that interacted
157 with the option monad, we now use bind to intensionalize an
158 extensional verb:
159
160         let lift pred w arg = bind arg (fun x w -> pred w x) w;;
161
162         intapp (lift left) ann 1;; (* true: Ann still left in world 1 *)
163         intapp (lift left) cam 2;; (* false: Cam still didn't leave in world 2 *)
164
165 Because `bind` unwraps the intensionality of the argument, when the
166 lifted "left" receives an individual concept (e.g., `unit 'a'`) as
167 argument, it's the extension of the individual concept (i.e., `'a'`)
168 that gets fed to the basic extensional version of "left".  (For those
169 of you who know Montague's PTQ, this use of bind captures Montague's
170 third meaning postulate.)
171
172 Likewise for extensional transitive predicates like "saw":
173
174         let lift2 pred w arg1 arg2 = 
175           bind arg1 (fun x -> bind arg2 (fun y w -> pred w x y)) w;;
176         intapp (intapp (lift2 saw) bill) ann 1;;  (* true: Ann saw Bill in world 1 *)
177         intapp (intapp (lift2 saw) bill) ann 2;;  (* false: No one saw anyone in world 2 *)
178
179 Crucially, an intensional predicate does not use `bind` to consume its
180 arguments.  Attitude verbs like "thought" are intensional with respect
181 to their sentential complement, but extensional with respect to their
182 subject (as Montague noticed, almost all verbs in English are
183 extensional with respect to their subject; a possible exception is "appear"):
184
185         let think (w:s) (p:s->t) (x:e) = 
186           match (x, p 2) with ('a', false) -> false | _ -> p w;;
187
188 Ann disbelieves any proposition that is false in world 2.  Apparently,
189 she firmly believes we're in world 2.  Everyone else believes a
190 proposition iff that proposition is true in the world of evaluation.
191
192         intapp (lift (intapp think
193                                                  (intapp (lift left)
194                                                                  (unit 'b'))))
195                    (unit 'a') 
196         1;; (* true *)
197
198 So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave).
199
200 The `lift` is there because "think Bill left" is extensional wrt its
201 subject.  The important bit is that "think" takes the intension of
202 "Bill left" as its first argument.
203
204         intapp (lift (intapp think
205                                                  (intapp (lift left)
206                                                                  (unit 'c'))))
207                    (unit 'a') 
208         1;; (* false *)
209
210 But even in world 1, Ann doesn't believe that Cam left (even though he
211 did: `intapp (lift left) cam 1 == true`).  Ann's thoughts are hung up
212 on what is happening in world 2, where Cam doesn't leave.
213
214 *Small project*: add intersective ("red") and non-intersective
215  adjectives ("good") to the fragment.  The intersective adjectives
216  will be extensional with respect to the nominal they combine with
217  (using bind), and the non-intersective adjectives will take
218  intensional arguments.
219
220 Finally, note that within an intensional grammar, extensional funtion
221 application is essentially just bind:
222
223         # let swap f x y = f y x;;
224         # bind cam (swap left) 2;;
225         - : bool = false
226
227