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