X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week7.mdwn;h=4e52490e7eaf242958a88a548aec65b4b2c3b1c1;hp=c81ff1253ceca9ee8cb724163cee5e139bcfe234;hb=b221494c397f7a6841b95ceeb227ac436d98440e;hpb=1713e01a3a0982e0f8fc68ed93035cea6ca8f46e 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 =