X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=intensionality_monad.mdwn;h=5b0ec3a2461646ab3875f664ab4bc1aa79126083;hp=3b69ef9fb8101a91a19b3cc57889bc642b455048;hb=fdbafe49575c982a8583e256c16c721756bcc13c;hpb=01979f60c8474ffe20e4a1a20d59bfff5d3950c6 diff --git a/intensionality_monad.mdwn b/intensionality_monad.mdwn index 3b69ef9f..5b0ec3a2 100644 --- a/intensionality_monad.mdwn +++ b/intensionality_monad.mdwn @@ -7,11 +7,9 @@ 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 ->>>>>>> f879a647e289a67b992caaafd497910259a81040 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 @@ -21,16 +19,16 @@ Note the extra `#` attached to the directive `use`. First, the familiar linguistic problem: - Bill left. + Bill left. Cam left. Ann believes [Bill left]. Ann believes [Cam left]. -We want an analysis on which all four of these sentences can be true -simultaneously. 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. +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 @@ -57,16 +55,16 @@ 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 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). 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 +(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. +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 make the complicated types available @@ -145,7 +143,7 @@ matter which world is used as an argument. This is a typical kind of thing for a monad unit to do. Then combining a prediction like *left* which is extensional in its -subject argument with a monadic subject like `unit ann` is simply bind +subject argument with an intensional subject like `unit ann` is simply bind in action: bind (unit ann) left 1;; (* true: Ann left in world 1 *)