X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=intensionality_monad.mdwn;h=5598e42c39d1c5bb24e2cf10df6ca317e7d41c06;hp=e228e24416791a7b05b12b4afc8e2e42b80ba109;hb=89886f346dd46b9f8b35fed6094dc5b999b74354;hpb=b221494c397f7a6841b95ceeb227ac436d98440e diff --git a/intensionality_monad.mdwn b/intensionality_monad.mdwn index e228e244..5598e42c 100644 --- a/intensionality_monad.mdwn +++ b/intensionality_monad.mdwn @@ -1,15 +1,10 @@ -The intensionality monad ------------------------- -In the meantime, we'll look at several linguistic applications for monads, based -on - -what's called the *reader monad*. -... -intensional function application. In Shan (2001) [Monads for natural +Now we'll look at using monads to do intensional function application. +This really is just another application of the Reader monad, not a new monad. +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* (which -we'll see again soon). This technique was beautifully re-invented +making expressions sensitive to the world of evaluation is conceptually +the same thing as making use of the 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), @@ -22,194 +17,175 @@ To run it, download the file, start OCaml, and say Note the extra `#` attached to the directive `use`. -Here's the idea: since people can have different attitudes towards -different propositions that happen to have the same truth value, we -can't have sentences denoting simple truth values. If we did, then if John -believed that the earth was round, it would force him to believe -Fermat's last theorem holds, since both propositions are equally true. -The traditional solution 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: +First, the familiar linguistic problem: + + Bill left. + Cam left. + Ann believes [Bill left]. + Ann believes [Cam left]. + +We want an analysis on which the first three sentences can be true at +the same time that the last sentence is false. 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. + +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:
-Extensional types Intensional types Examples +Extensional types Intensional types Examples ------------------------------------------------------------------- -S s->t s->t John left -DP s->e s->e John -VP s->e->t s->(s->e)->t left -Vt s->e->e->t s->(s->e)->(s->e)->t saw -Vs s->t->e->t s->(s->t)->(s->e)->t thought +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 thoughtThis 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. If you're curious about the initial `s`'s -in the extensional types, they're there because the behavior of these -expressions depends on which world they're evaluated at. If you are -in a situation in which you can hold the evaluation world constant, -you can further simplify the extensional types. Usually, the -dependence of the extension of an expression on the evaluation world -is hidden in a superscript, or built into the lexical interpretation -function. +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 +take so-called "individual 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). - -The intenstional types are more complicated than the intensional -types. Wouldn't it be nice to keep the complicated types to just -those 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. +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 intensional types are more complicated than the extensional +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: +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: 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. - - type 'a intension = s -> 'a;; - let unit x (w:s) = x;; - - let ann = unit 'a';; - let bill = unit 'b';; - let cam = unit 'c';; - -In our monad, the intension of an extensional type `'a` is `s -> 'a`, -a function from worlds to extensions. Our unit will be the constant -function (an instance of the K combinator) that returns the same -individual at each world. - -Then `ann = unit 'a'` is a rigid designator: a constant function from -worlds to individuals that returns `'a'` no matter which world is used -as an argument. - -Let's test compliance with the left identity law: - - # let bind u f (w:s) = f (u w) w;; - val bind : (s -> 'a) -> ('a -> s -> 'b) -> s -> 'b =
+ 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. +- let saw w x y = (w < 2) && (y < x);; - extapp (extapp saw bill) ann 1;; (* true *) - extapp (extapp saw bill) ann 2;; (* false *) +Now we are ready for the intensionality monad: -In world 1, Ann saw Bill and Cam, and Bill saw Cam. No one saw anyone -in world two. +
+type 'a intension = s -> 'a;; +let unit x = fun (w:s) -> x;; +let bind u f = fun (w:s) -> f (u w) w;; +-Good. Now for intensions: +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. - let intapp fn arg w = fn w arg;; +Then combining a predicate like *left* which is extensional in its +subject argument with an intensional subject like `unit ann` is simply bind +in action: -The only difference between intensional application and extensional -application is that we don't feed the evaluation world to the argument. -(See Montague's rules of (intensional) functional application, T4 -- T10.) -In other words, instead of taking an extension as an argument, -Montague's predicates take a full-blown intension. + bind (unit ann) left 1;; (* true: Ann left in world 1 *) + bind (unit cam) left 2;; (* false: Cam didn't leave in world 2 *) -But for so-called extensional predicates like "left" and "saw", -the extra power is not used. We'd like to define intensional versions -of these predicates that depend only on their extensional essence. -Just as we used bind to define a version of addition that interacted -with the option monad, we now use bind to intensionalize an -extensional verb: +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*. - let lift pred w arg = bind arg (fun x w -> pred w x) w;; +We can arrange for an extensional transitive verb to take intensional +arguments: - intapp (lift left) ann 1;; (* true: Ann still left in world 1 *) - intapp (lift left) cam 2;; (* false: Cam still didn't leave in world 2 *) + let lift2 f u v = bind u (fun x -> bind v (fun y -> f x y));; -Because `bind` unwraps the intensionality of the argument, when the -lifted "left" receives an individual concept (e.g., `unit 'a'`) as -argument, it's the extension of the individual concept (i.e., `'a'`) -that gets fed to the basic extensional version of "left". (For those -of you who know Montague's PTQ, this use of bind captures Montague's -third meaning postulate.) +This is the exact same lift predicate we defined in order to allow +addition in our division monad example. -Likewise for extensional transitive predicates like "saw": +
+lift2 saw (unit bill) (unit ann) 1;; (* true *) +lift2 saw (unit bill) (unit ann) 2;; (* false *) +- let lift2 pred w arg1 arg2 = - bind arg1 (fun x -> bind arg2 (fun y w -> pred w x y)) w;; - intapp (intapp (lift2 saw) bill) ann 1;; (* true: Ann saw Bill in world 1 *) - intapp (intapp (lift2 saw) bill) ann 2;; (* false: No one saw anyone in world 2 *) +Ann did see bill in world 1, but Ann didn't see Bill in world 2. -Crucially, an intensional predicate does not use `bind` to consume its -arguments. Attitude verbs like "thought" are intensional with respect -to their sentential complement, but extensional with respect to their -subject (as Montague noticed, almost all verbs in English are -extensional with respect to their subject; a possible exception is "appear"): +Finally, we can define our intensional verb *thinks*. *Think* is +intensional with respect to its sentential complement, though still 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 think (w:s) (p:s->t) (x:e) = - match (x, p 2) with ('a', false) -> false | _ -> p w;; + 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. - intapp (lift (intapp think - (intapp (lift left) - (unit 'b')))) - (unit 'a') - 1;; (* true *) + 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). -The `lift` is there because "think Bill left" is extensional wrt its -subject. The important bit is that "think" takes the intension of -"Bill left" as its first argument. - - intapp (lift (intapp think - (intapp (lift left) - (unit 'c')))) - (unit 'a') - 1;; (* false *) + 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: `intapp (lift left) cam 1 == true`). Ann's thoughts are hung up -on what is happening in world 2, where Cam doesn't leave. +But in world 1, Ann doesn't believe that Cam left (even though he +did leave in world 1: `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 @@ -217,11 +193,4 @@ on what is happening in world 2, where Cam doesn't leave. (using bind), and the non-intersective adjectives will take intensional arguments. -Finally, note that within an intensional grammar, extensional funtion -application is essentially just bind: - - # let swap f x y = f y x;; - # bind cam (swap left) 2;; - - : bool = false -