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