From: Jim Pryor Date: Mon, 1 Nov 2010 06:30:05 +0000 (-0400) Subject: split off reader, intens monads; link to week7 X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=b221494c397f7a6841b95ceeb227ac436d98440e split off reader, intens monads; link to week7 Signed-off-by: Jim Pryor --- diff --git a/index.mdwn b/index.mdwn index fd607e69..107c8031 100644 --- a/index.mdwn +++ b/index.mdwn @@ -49,9 +49,9 @@ preloaded is available at [[assignment 3 evaluator]]. > Topics: Types, Polymorphism, Unit and Bottom, Dividing by Zero/[[Towards Monads]] -(1 Nov) Lecture notes for Week7; Assignment6. +(1 Nov) Lecture notes for [[Week7]]; Assignment6. -> Topics: Monads +> Topics: Monads; [[Reader Monad]]; [[Intensionality Monad]] [[Upcoming topics]] diff --git a/intensionality_monad.mdwn b/intensionality_monad.mdwn new file mode 100644 index 00000000..e228e244 --- /dev/null +++ b/intensionality_monad.mdwn @@ -0,0 +1,227 @@ +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 +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 +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), +though without explicitly using monads. + +All of the code in the discussion below can be found here: [[intensionality-monad.ml]]. +To run it, download the file, start OCaml, and say + + # #use "intensionality-monad.ml";; + +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: + + +
+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
+
+ +This 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. + +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 +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. + +So here's what we do: + +In OCaml, we'll use integers to model possible worlds: + + 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 = + # bind (unit 'a') unit 1;; + - : char = 'a' + +We'll assume that this and the other laws always hold. + +We now build up some extensional meanings: + + let left w x = match (w,x) with (2,'c') -> false | _ -> true;; + +This function says that everyone always left, except for Cam in world +2 (i.e., `left 2 'c' == false`). + +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 extapp fn arg w = fn w (arg w);; + + extapp left ann 1;; + # - : bool = true + + extapp left cam 2;; + # - : bool = false + +`extapp` stands for "extensional function application". +So Ann left in world 1, but Cam didn't leave in world 2. + +A transitive predicate: + + let saw w x y = (w < 2) && (y < x);; + extapp (extapp saw bill) ann 1;; (* true *) + extapp (extapp saw bill) ann 2;; (* false *) + +In world 1, Ann saw Bill and Cam, and Bill saw Cam. No one saw anyone +in world two. + +Good. Now for intensions: + + let intapp fn arg w = fn w arg;; + +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. + +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: + + let lift pred w arg = bind arg (fun x w -> pred w x) w;; + + 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 *) + +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.) + +Likewise for extensional transitive predicates like "saw": + + 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 *) + +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"): + + let think (w:s) (p:s->t) (x:e) = + 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 *) + +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 *) + +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. + +*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/reader_monad.mdwn b/reader_monad.mdwn new file mode 100644 index 00000000..6702a8a7 --- /dev/null +++ b/reader_monad.mdwn @@ -0,0 +1,6 @@ +Introduce + +Heim and Kratzer's "Predicate Abstraction Rule" + + + diff --git a/week7.mdwn b/week7.mdwn index c81ff125..4e52490e 100644 --- a/week7.mdwn +++ b/week7.mdwn @@ -420,236 +420,7 @@ Continuation monad. In the meantime, we'll look at several linguistic applications for monads, based on what's called the *reader monad*. +##[[Reader monad]]## -The reader monad ----------------- - -Introduce - -Heim and Kratzer's "Predicate Abstraction Rule" - - - -The intensionality monad ------------------------- -... -intensional function application. 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 -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), -though without explicitly using monads. - -All of the code in the discussion below can be found here: [[intensionality-monad.ml]]. -To run it, download the file, start OCaml, and say - - # #use "intensionality-monad.ml";; - -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: - - -
-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
-
- -This 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. - -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 -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. - -So here's what we do: - -In OCaml, we'll use integers to model possible worlds: - - 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 = - # bind (unit 'a') unit 1;; - - : char = 'a' - -We'll assume that this and the other laws always hold. - -We now build up some extensional meanings: - - let left w x = match (w,x) with (2,'c') -> false | _ -> true;; - -This function says that everyone always left, except for Cam in world -2 (i.e., `left 2 'c' == false`). - -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 extapp fn arg w = fn w (arg w);; - - extapp left ann 1;; - # - : bool = true - - extapp left cam 2;; - # - : bool = false - -`extapp` stands for "extensional function application". -So Ann left in world 1, but Cam didn't leave in world 2. - -A transitive predicate: - - let saw w x y = (w < 2) && (y < x);; - extapp (extapp saw bill) ann 1;; (* true *) - extapp (extapp saw bill) ann 2;; (* false *) - -In world 1, Ann saw Bill and Cam, and Bill saw Cam. No one saw anyone -in world two. - -Good. Now for intensions: - - let intapp fn arg w = fn w arg;; - -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. - -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: - - let lift pred w arg = bind arg (fun x w -> pred w x) w;; - - 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 *) - -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.) - -Likewise for extensional transitive predicates like "saw": - - 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 *) - -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"): - - let think (w:s) (p:s->t) (x:e) = - 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 *) - -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 *) - -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. - -*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 - +##[[Intensionality monad]]##