summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
e8a135f)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
Now we'll look at using monads to do intensional function application.
Now we'll look at using monads to do intensional function application.
-This really is just another application of the reader monad, not a new monad.
+This really is just another application of the Reader monad, not a new monad.
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
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 the reader monad.
+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
This technique was beautifully re-invented
by Ben-Avi and Winter (2007) in their paper [A modular
approach to
let left1 (x:e) = true;;
let saw1 (x:e) (y:e) = y < x;;
let left1 (x:e) = true;;
let saw1 (x:e) (y:e) = y < x;;
saw1 bill ann;; (* true *)
saw1 ann bill;; (* false *)
So here's our extensional system: everyone left, including Ann;
saw1 bill ann;; (* true *)
saw1 ann bill;; (* false *)
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.)
+and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word
+order we're using is VOS, verb-object-subject.)
Now we add intensions. Because different people leave in different
worlds, the meaning of *leave* must depend on the world in which it is
Now we add intensions. Because different people leave in different
worlds, the meaning of *leave* must depend on the world in which it is
<pre>
type 'a intension = s -> 'a;;
let unit x = fun (w:s) -> x;;
<pre>
type 'a intension = s -> 'a;;
let unit x = fun (w:s) -> x;;
-let bind m f = fun (w:s) -> f (m w) w;;
+let bind u f = fun (w:s) -> f (u w) w;;
</pre>
Then the individual concept `unit ann` is a rigid designator: a
</pre>
Then the individual concept `unit ann` is a rigid designator: a
matter which world is used as an argument. This is a typical kind of
thing for a monad unit to do.
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
+Then combining a predicate like *left* which is extensional in its
subject argument with an intensional subject like `unit ann` is simply bind
in action:
subject argument with an intensional subject like `unit ann` is simply bind
in action:
We can arrange for an extensional transitive verb to take intensional
arguments:
We can arrange for an extensional transitive verb to take intensional
arguments:
- let lift f u v = bind u (fun x -> bind v (fun y -> f x y));;
+ let lift2 f u v = bind u (fun x -> bind v (fun y -> f x y));;
This is the exact same lift predicate we defined in order to allow
addition in our division monad example.
<pre>
This is the exact same lift predicate we defined in order to allow
addition in our division monad example.
<pre>
-lift saw (unit bill) (unit ann) 1;; (* true *)
-lift saw (unit bill) (unit ann) 2;; (* false *)
+lift2 saw (unit bill) (unit ann) 1;; (* true *)
+lift2 saw (unit bill) (unit ann) 2;; (* false *)
</pre>
Ann did see bill in world 1, but Ann didn't see Bill in world 2.
</pre>
Ann did see bill in world 1, but Ann didn't see Bill in world 2.
bind (unit ann) (thinks (bind (unit cam) left)) 1;;
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: `bind (unit cam) left 1 == true`). Ann's thoughts are hung up on
+But in world 1, Ann doesn't believe that Cam left (even though he
+did leave in world 1: `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
what is happening in world 2, where Cam doesn't leave.
*Small project*: add intersective ("red") and non-intersective
Some students have asked: why do we need de Bruijn notation to represent environments that way? Can't we just assume our variables are of the form <code>x<sub>1</sub>, x<sub>2</sub>, x<sub>3</sub></code>, and so on? And then the values that get assigned to those variables could just be kept in a stack, with the first value understood to be assigned to <code>x<sub>1</sub></code>, and so on. Yes, we could do that. But the advantage of the de Bruijn notation is that we don't have to keep track of which variable is associated with which lambda binder. In the de Bruijn framework, the outermost binder always goes with the top-most member of the stack. In the proposed alternative, that's not so: we could have:
Some students have asked: why do we need de Bruijn notation to represent environments that way? Can't we just assume our variables are of the form <code>x<sub>1</sub>, x<sub>2</sub>, x<sub>3</sub></code>, and so on? And then the values that get assigned to those variables could just be kept in a stack, with the first value understood to be assigned to <code>x<sub>1</sub></code>, and so on. Yes, we could do that. But the advantage of the de Bruijn notation is that we don't have to keep track of which variable is associated with which lambda binder. In the de Bruijn framework, the outermost binder always goes with the top-most member of the stack. In the proposed alternative, that's not so: we could have:
-<pre><code>\x<sub>2</sub>. x (\x<sub>8</sub>. x<sub>8</sub> x<sub>2</sub>)
+<pre><code>\x<sub>2</sub>. x<sub>2</sub> (\x<sub>8</sub>. x<sub>8</sub> x<sub>2</sub>)
</code></pre>
In any event, though, we won't make use of de Bruijn notation because, though it makes the semantic algorithms more elegant, it also adds an extra level of conceptual complexity, which we don't want to do.]
</code></pre>
In any event, though, we won't make use of de Bruijn notation because, though it makes the semantic algorithms more elegant, it also adds an extra level of conceptual complexity, which we don't want to do.]
-we'll instead evaluate them by manipulating their environment. (To intepret `(\x. M) N` in environment `e`, we'll interpret `M` in an environment like `e {x:= N}` where `x` may have been changed to now be assigned to `N`.
+we'll instead evaluate them by manipulating their environment. To intepret `(\x. M) N` in environment `e`, we'll interpret `M` in an environment like `e {x:= N}` where `x` may have been changed to now be assigned to `N`.
A few comments. First, what the environment associates with the variable `x` will be expressions of the lambda calculus we're evaluating. If we understand the evaluation to be call-by-name, these expressions may be complexes of the form `N P`. If on the other hand, we understand the evaluation to be call-by-value, then these expressions will always be fully evaluated before being inserted into the environment. That means they'll never be of the form `N P`; but only of the form `y` or `\y. P`. The latter kinds of expressions are called "values." But "values" here are just certain kinds of expressions. (They *could* be the denotations of lambda expressions, if one thinks of the lambda expressions as all having normal-form lambda terms as their denotations, when possible.)
A few comments. First, what the environment associates with the variable `x` will be expressions of the lambda calculus we're evaluating. If we understand the evaluation to be call-by-name, these expressions may be complexes of the form `N P`. If on the other hand, we understand the evaluation to be call-by-value, then these expressions will always be fully evaluated before being inserted into the environment. That means they'll never be of the form `N P`; but only of the form `y` or `\y. P`. The latter kinds of expressions are called "values." But "values" here are just certain kinds of expressions. (They *could* be the denotations of lambda expressions, if one thinks of the lambda expressions as all having normal-form lambda terms as their denotations, when possible.)
With these ideas settled, then, we can present an environment-based operational semantics for the untyped lambda calculus. Here is a call-by-value version, which assumes that expressions are always fully evaluated before being inserted into the environment.
With these ideas settled, then, we can present an environment-based operational semantics for the untyped lambda calculus. Here is a call-by-value version, which assumes that expressions are always fully evaluated before being inserted into the environment.
-1. When `e` assigns some term `v` to `x`, then `x`fully (that is, terminally) reduces in environment `e` to `v`. We write that as: `(e |- x) ==> v`.
+1. When `e` assigns some term `v` to `x`, then `x` fully (that is, terminally) reduces in environment `e` to `v`. We write that as: `(e |- x) ==> v`.
-2. `(e |- \x. M) ==> closure(e, \x. M)`, where a closure is some data-structure (it might just be a pair of the data-structure `e` and the formula `\x. M`).
+2. `(e |- \x. M) ==> closure(e, \x. M)`, where a closure is some data-structure (it might just be a pair of the environment `e` and the formula `\x. M`).
3. If `(e |- M) ==> closure(e2, \x. M2)` and `(e |- N) ==> v` and `(e2 {x:=v} |- M2) ==> u`, then `(e |- M N) ==> u`. Here `e2 {x:=v}` is the environment which is just like `e2` except it assigns `v` to `x`.
3. If `(e |- M) ==> closure(e2, \x. M2)` and `(e |- N) ==> v` and `(e2 {x:=v} |- M2) ==> u`, then `(e |- M N) ==> u`. Here `e2 {x:=v}` is the environment which is just like `e2` except it assigns `v` to `x`.
Yes! You can do so with a monad, in much the same way we did with our checks for divide-by-zero failures.
Yes! You can do so with a monad, in much the same way we did with our checks for divide-by-zero failures.
-Here we'll use a different monad. It's called the **reader monad**. We define it like this:
+Here we'll use a different monad. It's called the **Reader monad**. We define it like this:
(* we assume we've settled on some implementation of the environment *)
type env = (char * int) list;;
(* we assume we've settled on some implementation of the environment *)
type env = (char * int) list;;
\[[man who(i): Alice spurned i]]
is the result of combining \[[man]], an `e->t` type predicate value, with the adjective-type value of \[[who(i): Alice spurned i]]. As I said, we'll ignore complexities about their treatment of adjectives. But how is \[[who(i): Alice spurned i]] derived? Heim and Kratzer say this is defined only relative to an
\[[man who(i): Alice spurned i]]
is the result of combining \[[man]], an `e->t` type predicate value, with the adjective-type value of \[[who(i): Alice spurned i]]. As I said, we'll ignore complexities about their treatment of adjectives. But how is \[[who(i): Alice spurned i]] derived? Heim and Kratzer say this is defined only relative to an
-assignment g, and it's defined to be a function from objects x in the domain to the value \[[Alice spurned i]] has relative to shifted assignment g {i:=x}, which is like g except for assigning object x to variable i. So this is not the result of taking some value \[[who(i)]], and some separate value \[[Alice spurned i]], and supplying one of them to the other as argument to function.
+assignment g, and it's defined to be a function from objects x in the domain to the value that \[[Alice spurned i]] has relative to shifted assignment g {i:=x}, which is like g except for assigning object x to variable i. So this is not the result of taking some value \[[who(i)]], and some separate value \[[Alice spurned i]], and supplying one of them to the other as argument to function.
-Yes! We can in fact implement this as a reader monad. And in doing so, we *will* get a value \[[who(i)]] which is a function, and another value \[[Alice spurned i]], to be its argument. So the semantics in the first place again becomes compositional, and in the second place doesn't need any special rule for how \[[who(i): Alice spurned i]] is derived. It uses the same composition rule as other complex expressions.
+Yes! We can in fact implement this as a Reader monad. And in doing so, we *will* get a value \[[who(i)]] which is a function, and another value \[[Alice spurned i]], to be its argument. So the semantics in the first place again becomes compositional, and in the second place doesn't need any special rule for how \[[who(i): Alice spurned i]] is derived. It uses the same composition rule as other complex expressions.
We set \[[Alice]] = the reader-monad value `unit Alice`.
We set \[[Alice]] = the reader-monad value `unit Alice`.
-We have to lift the semantic values of predicates into the reader-monad. So if before we were taking the semantic value of "spurned" to be a function `S` of type `e -> e -> t`, now we set \[[spurned]] = lift2 S.
+We have to lift the semantic values of predicates into the Reader monad. So if before we were taking the semantic value of "spurned" to be a function `S` of type `e -> e -> t`, now we set \[[spurned]] = `lift2 S`.
Finally, we set \[[who(i)]] to be:
Finally, we set \[[who(i)]] to be:
fun (u : bool reader) (v : entity reader) -> shift i v u
fun (u : bool reader) (v : entity reader) -> shift i v u
-You can trace through what happens then if we apply \[[who(i)]] to (\[[spurned]] applied to \[[Alice]] and \[[i]]):
+You can trace through what happens then if we apply \[[who(i)]] to \[[Alice spurned i]]:
- \[[Alice spurned i]] = \[[spurned]] \[[Alice]] \[[i]]
- = (lift2 S) (unit Alice) (lookup i)
- = bind (unit Alice) (fun x -> bind (lookup i) (fun y -> unit (S x y)))
+ \[[Alice spurned i]] = \[[spurned]] \[[i]] \[[Alice]]
+ = (lift2 S) (lookup i) (unit Alice)
+ = bind (lookup i) (fun x -> bind (unit Alice) (fun y -> unit (S x y)))
because of the left-identity rule for `unit`, this is the same as:
because of the left-identity rule for `unit`, this is the same as:
- = bind (lookup i) (fun y -> unit (S Alice y))
+ = bind (lookup i) (fun x -> unit (S x Alice))
Substituting in the definition of `bind` for the reader-monad, this is:
Substituting in the definition of `bind` for the reader-monad, this is:
- = fun e -> (fun y -> unit (S Alice y)) (lookup i e) e
- = fun e -> unit (S Alice (lookup i e)) e
+ = fun e -> (fun x -> unit (S x Alice)) (lookup i e) e
+ = fun e -> unit (S (lookup i e) Alice) e
Substituting in the definition of `unit`, this is:
Substituting in the definition of `unit`, this is:
- = fun e -> S Alice (lookup i e)
+ = fun e -> S (lookup i e) Alice
And now supplying \[[Alice spurned i]] as an argument to \[[who(i)]], we get:
\[[who(i): Alice spurned i]] = \[[who(i)]] \[[Alice spurned i]]
And now supplying \[[Alice spurned i]] as an argument to \[[who(i)]], we get:
\[[who(i): Alice spurned i]] = \[[who(i)]] \[[Alice spurned i]]
- = (fun u v -> shift i v u) (fun e -> S Alice (lookup i e))
- = fun v -> shift i v (fun e -> S Alice (lookup i e))
+ = (fun u v -> shift i v u) (fun e -> S (lookup i e) Alice)
+ = fun v -> shift i v (fun e -> S (lookup i e) Alice)
Substituting in the definition of `shift`, this is:
Substituting in the definition of `shift`, this is:
- = fun v -> (fun c v u e -> u ((c, v e) :: e)) i v (fun e -> S Alice (lookup i e))
- = fun v -> (fun u e -> u ((i, v e) :: e)) (fun e -> S Alice (lookup i e))
- = fun v -> (fun e -> (fun e -> S Alice (lookup i e)) ((i, v e) :: e))
- = fun v -> (fun e -> S Alice (lookup i ((i, v e) :: e)) )
- = fun v -> (fun e -> S Alice (v e) )
+ = fun v -> (fun c v u e -> u ((c, v e) :: e)) i v (fun e -> S (lookup i e) Alice)
+ = fun v -> (fun u e -> u ((i, v e) :: e)) (fun e -> S (lookup i e) Alice)
+ = fun v -> (fun e -> (fun e -> S (lookup i e) Alice) ((i, v e) :: e))
+ = fun v -> (fun e -> S (lookup i ((i, v e) :: e)) Alice)
+ = fun v -> (fun e -> S (v e) Alice)
-In other words, it's a function from entity reader monads to a function from assignment functions to the result of applying S to Alice and the value of that entity reader-monad under that assignment function. Essentially the same as Heim and Kratzer's final value, except here we work with monadic values, such as functions from assignments to entities, rather than bare entities. And our derivation is completely compositional and uses the same composition rules for joining \[[who(i)]] to \[[Alice spurned i]] as it uses for joining \[[spurned]] to \[[Alice]] and \[[i]].
+In other words, it's a function from entity reader monads to a function from assignment functions to the result of applying S to the value of that entity reader-monad under that assignment function, and to Alice. Essentially the same as Heim and Kratzer's final value, except here we work with monadic values, such as functions from assignments to entities, rather than bare entities. And our derivation is completely compositional and uses the same composition rules for joining \[[who(i)]] to \[[Alice spurned i]] as it uses for joining \[[spurned]] to \[[i]] and \[[Alice]].
<pre>
let div' (u:int option) (v:int option) =
<pre>
let div' (u:int option) (v:int option) =
- | Some 0 -> None
- | Some y -> (match u with
- None -> None
- | Some x -> Some (x / y));;
+ | Some x -> (match v with
+ Some 0 -> None
+ | Some y -> Some (x / y));;
(*
val div' : int option -> int option -> int option = <fun>
(*
val div' : int option -> int option -> int option = <fun>
most straightforward way to lift an ordinary value into a monadic value
of the monadic type in question.
most straightforward way to lift an ordinary value into a monadic value
of the monadic type in question.
-* Thirdly, an operation that's often called `bind`. This is another
+* Thirdly, an operation that's often called `bind`. As we said before, this is another
unfortunate name: this operation is only very loosely connected to
what linguists usually mean by "binding." In our option/maybe monad, the
bind operation is:
unfortunate name: this operation is only very loosely connected to
what linguists usually mean by "binding." In our option/maybe monad, the
bind operation is:
them from hurting the people that use them or themselves.
* **Left identity: unit is a left identity for the bind operation.**
them from hurting the people that use them or themselves.
* **Left identity: unit is a left identity for the bind operation.**
- That is, for all `f:'a -> 'a m`, where `'a m` is a monadic
+ That is, for all `f:'a -> 'b m`, where `'b m` is a monadic
type, we have `(unit x) >>= f == f x`. For instance, `unit` is itself
a function of type `'a -> 'a m`, so we can use it for `f`:
type, we have `(unit x) >>= f == f x`. For instance, `unit` is itself
a function of type `'a -> 'a m`, so we can use it for `f`:
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
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, for a less trivial instance of a function from `int`s
- to `int option`s:
# unit 2;;
- : int option = Some 2
# unit 2 >>= unit;;
- : int option = Some 2
# unit 2;;
- : int option = Some 2
# unit 2 >>= unit;;
- : int option = Some 2
+ Now, for a less trivial instance of a function from `int`s to `int option`s:
+
# let divide x y = if 0 = y then None else Some (x/y);;
val divide : int -> int -> int option = <fun>
# divide 6 2;;
# let divide x y = if 0 = y then None else Some (x/y);;
val divide : int -> int -> int option = <fun>
# divide 6 2;;
(u >>= f) >>= g == u >>= (fun x -> f x >>= g)
(u >>= f) >>= g == u >>= (fun x -> f x >>= g)
- 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`.
+ 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 (bear in
mind that in the Ocaml implementation of integer division, 2/3
Some examples of associativity in the option monad (bear in
mind that in the Ocaml implementation of integer division, 2/3
- : int option = None
Of course, associativity must hold for *arbitrary* functions of
- : int option = None
Of course, associativity must hold for *arbitrary* functions of
-type `'a -> 'a m`, where `m` is the monad type. It's easy to
+type `'a -> 'b m`, where `m` is the monad type. It's easy to
convince yourself that the `bind` operation for the option monad
obeys associativity by dividing the inputs into cases: if `u`
matches `None`, both computations will result in `None`; if
convince yourself that the `bind` operation for the option monad
obeys associativity by dividing the inputs into cases: if `u`
matches `None`, both computations will result in `None`; if