From: Jim Pryor Date: Tue, 2 Nov 2010 21:51:13 +0000 (-0400) Subject: tweaks X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=89886f346dd46b9f8b35fed6094dc5b999b74354;hp=e8a135f7bc1a0aa4118703baa78ec8d2ea9db490 tweaks Signed-off-by: Jim Pryor --- diff --git a/intensionality_monad.mdwn b/intensionality_monad.mdwn index acf154cf..5598e42c 100644 --- a/intensionality_monad.mdwn +++ b/intensionality_monad.mdwn @@ -1,9 +1,9 @@ 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 -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 @@ -90,13 +90,13 @@ In OCaml, we'll use integers to model possible worlds. Characters (characters in let left1 (x:e) = true;; let saw1 (x:e) (y:e) = y < x;; - left1 ann;; + left1 ann;; (* true *) 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 @@ -128,7 +128,7 @@ Now we are ready for the intensionality monad: 
 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;;
Then the individual concept `unit ann` is a rigid designator: a @@ -136,7 +136,7 @@ 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. -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: @@ -152,14 +152,14 @@ to the extensional predicate *left*. 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. 
-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 *)
Ann did see bill in world 1, but Ann didn't see Bill in world 2. @@ -183,8 +183,8 @@ So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave). 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 diff --git a/reader_monad.mdwn b/reader_monad.mdwn index 784d0a49..2e24babb 100644 --- a/reader_monad.mdwn +++ b/reader_monad.mdwn @@ -35,7 +35,7 @@ where each argument-occurrence records the distance between that occurrence and 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 x1, x2, x3, 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 x1, 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: -
\x2. x (\x8. x8 x2)
+
\x2. x2 (\x8. x8 x2)
 

 
 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.]
@@ -44,7 +44,7 @@ Now with the environment-based semantics, instead of evaluating terms using subs
 
 	(\x. M) N ~~> M {x <- 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`.
+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.)
 
@@ -66,9 +66,9 @@ operational semantics for the lambda calculus, or the underpinnings of how Schem
 
 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`.
 
@@ -141,7 +141,7 @@ have to explicitly pass around an environment that they're not themselves making
 
 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;;
@@ -225,11 +225,11 @@ Another exception is that Heim and Kratzer have to postulate a special rule to h
 	\[[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.
 
 Getting any ideas?
 
-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.
 
 How does this work?
 
@@ -237,7 +237,7 @@ We set \[[i]] = the reader-monad value `lookup i`.
 
 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:
 
@@ -248,40 +248,40 @@ That is, it takes as arguments a clause-type reader-monad `u`, and an entity-typ
 
 	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:
 
-		= 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:
 
-		= 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:
 
-		= 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]]
-		= (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:
 
-		= 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]].
 
 What's not to like?
 
diff --git a/week7.mdwn b/week7.mdwn
index 65d528c4..c2a432ec 100644
--- a/week7.mdwn
+++ b/week7.mdwn
@@ -58,12 +58,11 @@ operations.  So we have to jack up the types of the inputs:
 
 
 let div' (u:int option) (v:int option) =
-  match v with
+  match u with
 	  None -> None
-    | 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 = 
@@ -237,7 +236,7 @@ that provides at least the following three elements:
 	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:
@@ -366,7 +365,7 @@ Just like good robots, monads must obey three laws designed to prevent
 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`:
 
@@ -379,14 +378,15 @@ them from hurting the people that use them or themselves.
 	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:
+	f`.
 
 		# 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 = 
 		# divide 6 2;;
@@ -404,8 +404,8 @@ them from hurting the people that use them or themselves.
 
 		(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
@@ -427,7 +427,7 @@ them from hurting the people that use them or themselves.
 		- : 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