author Chris Barker Mon, 1 Nov 2010 19:13:01 +0000 (15:13 -0400) committer Chris Barker Mon, 1 Nov 2010 19:13:01 +0000 (15:13 -0400)
 assignment6.mdwn patch | blob | history intensionality-monad.ml patch | blob | history intensionality_monad.mdwn patch | blob | history week7.mdwn patch | blob | history

index d044c12..919ff24 100644 (file)
@@ -1,5 +1,35 @@
-1.  Test all three monad laws for the intensionality monad.  To do
-"intensionality-monad.ml";;`).  For instance, what does evaluating
-`bind (unit 'c') (swap left) 2 == swap left 'c' 2;;` show?  Please
-explain briefly but clearly what you are doing in your discussion.
+1.  **Build a state monad.** Based on the division by zero monad,
+build a system that will evaluate arithmetic expressions.  Instead of
+returning a simple integer as a result, it will deliver the correct
+answer along with a count of the number of operations performed during
+the calculuation.  That is, the desired behavior should be like this:
+
+    # lift ( + ) (lift ( / ) (unit 20) (unit 2)) (lift ( * ) (unit 2) (unit 3)) 0;;
+    - : int * int = (16, 3)
+
+Here, `lift` is the function that uses `bind` to prepare an ordinary
+arithmetic operator (such as addition `( + )`, division `( / )`, or
+multiplication `( * )`) to recieve objects from the counting monad as
+arguments.  The response of the interpreter says two things: that
+(20/2) + (2*3) = 16, and that the computation took three arithmetic
+steps.  By the way, that zero at the end provides the monadic object
+with a starting point (0 relevant computations have occurred previous
+to the current computation).
+
+Assume for the purposes of this excercise that no one ever tries to
+divide by zero (so there should be no int option types anywhere in
+your solution).
+
+You'll need to define a computation monad type, unit, bind, and lift.
+We encourage you to consider this hint: [[Assignment 6 Hint 1]].
+
+examples illustrating specific cases in which the monad laws are
+obeyed, then explain (briefly, not exhaustively) why the laws hold in
+general for your unit and bind operators.
+
+3. How would you extend your strategy if you wanted to count
+arithmetic operations, but you also wanted to be safe from division by
+zero?  This is a deep question: how should you combine two monads into
+a single system?  If you don't arrive at working code, you can still
+discuss the issues and design choices.
index 2f30f8b..d1f21d2 100644 (file)
@@ -1,57 +1,45 @@
(* This is the intensionality monad discussed in the lecture notes for week 7. *)

-type s = int;;
-type e = char;;
-type t = bool;;
+type s = int;; (* integers model possible worlds *)
+type e = char;; (* chars model individuals *)
+type t = bool;; (* booleans model 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';;
-
-let bind m f (w:s) = f (m w) w;;
-bind (unit 'a') unit 1;;
+let ann = 'a';;
+let bill = 'b';;
+let cam = 'c';;

-let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
+let left1 (x:e) = true;; (* Everyone left *)
+let saw1 (x:e) (y:e) = y < x;; (* Ann saw Bill and Cam, and Bill saw Cam *)

-let extapp fn arg w = fn w (arg w);;
+left1 ann;;
+saw1 bill ann;;
+saw1 ann bill;;

-extapp left ann 1;;
+(* Now we make the extension of "leave" sensitive to the world of evaluation *)
+let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;

-extapp left cam 2;;
+left ann 1;; (* Ann left in world 1 *)
+left cam 2;; (* Cam didn't leave in world 2 *)

-let saw w x y = (w < 2) && (y < x);;
-extapp (extapp saw bill) ann 1;; (* true *)
-extapp (extapp saw bill) ann 2;; (* false *)
+let saw x y w = (w < 2) && (y < x);;
+saw bill ann 1;; (* Ann saw Bill in world 1 *)
+saw bill ann 2;; (* Ann didn't see Bill in world 2 *)

-let intapp fn arg w = fn w arg;;
-
-let lift pred w arg = bind arg (fun x w -> pred w x) w;;
+type 'a intension = s -> 'a;;
+let unit x (w:s) = x;;
+let bind m f (w:s) = f (m w) w;;
+let lift f u v = bind u (fun x -> bind v (fun y -> f x y));;

-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 *)
+bind (unit ann) left 1;;
+bind (unit cam) left 2;;

-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 *)
+lift saw (unit bill) (unit ann) 1;;
+lift saw (unit bill) (unit ann) 2;;

-let think (w:s) (p:s->t) (x:e) =
+let thinks (p:s->t) (x:e) (w:s) =
match (x, p 2) with ('a', false) -> false | _ -> p w;;

-intapp (lift (intapp think
-                     (intapp (lift left)
-                             (unit 'b'))))
-       (unit 'a')
-1;; (* true *)
-
-intapp (lift (intapp think
-                     (intapp (lift left)
-                             (unit 'c'))))
-       (unit 'a')
-1;; (* false *)
+bind (unit ann) (thinks (bind (unit bill) left)) 1;;
+bind (unit ann) (thinks (bind (unit cam) left)) 1;;

-let swap f x y = f y x;;
-bind cam (swap left) 2;; (* false *)
index e228e24..6887487 100644 (file)
@@ -1,17 +1,29 @@
------------------------
-In the meantime, we'll look at several linguistic applications for monads, based
-on
-
-...
-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
+
+In the meantime, we'll look at several linguistic applications for
+intensional function application.
+
+First, the familiar linguistic problem:
+
+                  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.
+
+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*.  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),

@@ -22,39 +34,27 @@ To run it, download the file, start OCaml, and say

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:
+The traditional solution to the problem sketched above 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:

<pre>
-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    thought
</pre>

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.
+generalized quantifiers.

The main difference between the intensional types and the extensional
types is that in the intensional types, the arguments are functions
@@ -62,15 +62,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:

@@ -84,144 +91,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 = <fun>
-       # bind (unit 'a') unit 1;;
-       - : char = 'a'
+<pre>
+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 *)
+</pre>

-       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:
+<pre>
+     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.
+</pre>

-       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.
+<pre>
+type 'a intension = s -> 'a;;
+let unit x (w:s) = x;;
+let bind m f (w:s) = f (m w) w;;
+</pre>

-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

-Likewise for extensional transitive predicates like "saw":
+<pre>
+lift saw (unit bill) (unit ann) 1;;  (* true *)
+lift saw (unit bill) (unit ann) 2;;  (* false *)
+</pre>

-       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
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
-
-
index fe9bedb..79983c3 100644 (file)
@@ -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
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 <https://www.cs.indiana.edu/cgi-pub/c311/doku.php?id=home> but the link above is to a local copy.

-There's a long list of monad tutorials on the [[Offsite Reading]] page. Skimming the titles makes me laugh.
+There's a long list of monad tutorials on the [[Offsite Reading]] page. Skimming the titles makes us laugh.

In the presentation we gave above---which follows the functional programming conventions---we took `unit`/return and `bind` as the primitive operations. From these a number of other general monad operations can be derived. It's also possible to take some of the others as primitive. The [Monads in Category