-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 @@ -61,15 +60,22 @@ from worlds to extensions: intransitive verb phrases like "left" now take intensional 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). +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 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. +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: @@ -83,144 +89,114 @@ 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 =

+let ann = 'a';; +let bill = 'b';; +let cam = 'c';; -We'll assume that this and the other laws always hold. +let left1 (x:e) = true;; +let saw1 (x:e) (y:e) = y < x;; -We now build up some extensional meanings: +left1 ann;; +saw1 bill ann;; (* true *) +saw1 ann bill;; (* false *) +- let left w x = match (w,x) with (2,'c') -> false | _ -> true;; +So here's our extensional system: everyone left, including Ann; +and Ann saw Bill, but Bill didn't see Ann. (Note that Ocaml word +order is VOS, verb-object-subject.) -This function says that everyone always left, except for Cam in world -2 (i.e., `left 2 'c' == false`). +Now we add intensions. Because different people leave in different +worlds, the meaning of *leave* must depend on the world in which it is +being evaluated: -Then the way to evaluate an extensional sentence is to determine the -extension of the verb phrase, and then apply that extension to the -extension of the subject: + let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;; - let extapp fn arg w = fn w (arg w);; +This new definition says that everyone always left, except that +in world 2, Cam didn't leave. - extapp left ann 1;; - # - : bool = true + let saw x y w = (w < 2) && (y < x);; + saw bill ann 1;; (* true: Ann saw Bill in world 1 *) + saw bill ann 2;; (* false: no one saw anyone in world 2 *) - extapp left cam 2;; - # - : bool = false +Along similar lines, this general version of *see* coincides with the +`saw1` function we defined above for world 1; in world 2, no one saw anyone. -`extapp` stands for "extensional function application". -So Ann left in world 1, but Cam didn't leave in world 2. +Just to keep things straight, let's get the facts of the world set: -A transitive predicate: +

+ 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 (w:s) = x;; +let bind m f (w:s) = f (m 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 prediction like *left* which is extensional in its +subject argument with a monadic 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 lift 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": +

+lift saw (unit bill) (unit ann) 1;; (* true *) +lift 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, but 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. +did: `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 will be extensional with respect to the nominal they combine with (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 - - diff --git a/week7.mdwn b/week7.mdwn index fe9bedb8..79983c3e 100644 --- a/week7.mdwn +++ b/week7.mdwn @@ -378,7 +378,9 @@ them from hurting the people that use them or themselves. The parentheses is the magic for telling OCaml that the function to be defined (in this case, the name of the function is `>>=`, pronounced "bind") is an infix operator, so we write - `u >>= f` or equivalently `( >>= ) u f` instead of `>>= u f`. Now: + `u >>= f` or equivalently `( >>= ) u f` instead of `>>= u + f`. Now, for a less trivial instance of a function from `int`s + to `int option`s: # unit 2;; - : int option = Some 2 @@ -405,7 +407,9 @@ them from hurting the people that use them or themselves. If you don't understand why the lambda form is necessary (the "fun x" part), you need to look again at the type of `bind`. - Some examples of associativity in the option monad: + Some examples of associativity in the option monad (bear in + mind that in the Ocaml implementation of integer division, 2/3 + evaluates to zero, throwing away the remainder): # Some 3 >>= unit >>= unit;; - : int option = Some 3 @@ -447,8 +451,7 @@ More details about monads If you studied algebra, you'll remember that a *monoid* is an associative operation with a left and right identity. For instance, the natural numbers along with multiplication form a monoid with 1 -serving as the left and right identity. That is, temporarily using -`*` to mean arithmetic multiplication, `1 * u == u == u * 1` for all +serving as the left and right identity. That is, `1 * u == u == u * 1` for all `u`, and `(u * v) * w == u * (v * w)` for all `u`, `v`, and `w`. As presented here, a monad is not exactly a monoid, because (unlike the arguments of a monoid operation) the two arguments of the bind are of @@ -478,7 +481,7 @@ invited talk, *19'th Symposium on Principles of Programming Languages*, ACM Pres * [Daniel Friedman. A Schemer's View of Monads](/schemersviewofmonads.ps): from