From c6f572fd09dbe53dff30a91cd07b318b3e5edfd6 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sat, 20 Nov 2010 12:41:39 -0500 Subject: [PATCH] assignment7 tweaks Signed-off-by: Jim Pryor --- assignment7.mdwn | 4 +-- hints/assignment_7_hint_3.mdwn | 4 +-- hints/assignment_7_hint_4.mdwn | 74 +++++++++++++++++++++++------------------- hints/assignment_7_hint_5.mdwn | 28 +++++++++------- hints/assignment_7_hint_6.mdwn | 42 +++++++++++++++--------- 5 files changed, 87 insertions(+), 65 deletions(-) diff --git a/assignment7.mdwn b/assignment7.mdwn index 9f83b009..337249c0 100644 --- a/assignment7.mdwn +++ b/assignment7.mdwn @@ -1,4 +1,4 @@ -**The hints for problem 2 were being actively developed until early Saturday morning. They're pretty stable now. Remember you have a grace period until Sunday Nov. 28 to complete this homework.** +**The hints for problem 2 were being actively developed until Saturday morning. They're stable now. Remember you have a grace period until Sunday Nov. 28 to complete this homework.** 1. Make sure that your operation-counting monad from [[assignment6]] is working. Modify it so that instead of counting operations, it keeps track of the last remainder of any integer division. You can help yourself to the functions: @@ -7,7 +7,7 @@ Write a monadic operation that enables you to retrieve the last-saved remainder, at any arbitrary later point in the computation. -2. For the next assignment, read the paper [Coreference and Modality](/coreference-and-modality.pdf). Your task will be to re-express the semantics they offer in the terms we're now working with. You'll probably want to review the lecture notes from this week's meeting, which we haven't yet been able to post. We will do that soon. In the meantime, you can get started reading the paper. +2. For the next assignment, read the paper [Coreference and Modality](/coreference-and-modality.pdf). Your task will be to re-express the semantics they offer up to the middle of p. 16, in the terms we're now working with. You'll probably want to review the lecture notes from this week's meeting, which we haven't yet been able to post. We will do that soon. In the meantime, you can get started reading the paper. Some advice: diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn index cbcc5a0b..4aa9180f 100644 --- a/hints/assignment_7_hint_3.mdwn +++ b/hints/assignment_7_hint_3.mdwn @@ -17,9 +17,9 @@ * Reviewing: GS&V's "information states," which they notate using `s`, are sets of what they call "possibilities," and notate using `i`. Instead of sets of possibilities, which get updated to sets of other, "extended" possibilities, we'll work with sets of discourse possibility monads, which are functions from discourse possibilities to values and possibly "extended" discourse possibilities. -* In def 2.5, GS&V say the denotation of an e-type constant α wrt a discourse possibility `(r, h, w)` is whatever entity the world `w` associates with α. Since we don't have worlds, this will just be an entity. +* In def 2.5, GS&V say the denotation of an e-type constant α wrt a discourse possibility `(r, h, w)` is whatever entity the world `w` associates with α. Since we don't have worlds, this will just be an entity. (Hence, we're not representing any of the interesting phenomena about epistemic non-rigidity discussed in GS&V pp. 32ff.) - They say the denotation of a predicate is whatever extension the world `w` associates with the predicate. Since we don't have worlds, this will just be an extension, or a function from entities to `bool`s. + GS&V say the denotation of a predicate is whatever extension the world `w` associates with the predicate. Since we don't have worlds, this will just be an extension, or a function from entities to `bool`s. They say the denotation of a variable is the entity which the store `h` assigns to the index that the assignment function `r` assigns to the variable. In other words, if the variable is `'x'`, its denotation wrt `(r, h, w)` is `h[r['x']]`. In our OCaml implementation, that will be `List.nth h (r 'x')`. diff --git a/hints/assignment_7_hint_4.mdwn b/hints/assignment_7_hint_4.mdwn index c6a5995f..6b33b7a5 100644 --- a/hints/assignment_7_hint_4.mdwn +++ b/hints/assignment_7_hint_4.mdwn @@ -1,22 +1,23 @@ -* At the top of p. 13 (this is in between defs 2.8 and 2.9), GS&V give two examples, one for \[[∃xPx]] and the other for \[[Qx]]. In fact it will be most natural to break \[[∃xPx]] into two pieces, \[[∃x]] and \[[Px]]. But first we need to get clear on expressions like \[[Qx]]. +* At the top of p. 13, GS&V give two examples, one for \[[∃xPx]] and the other for \[[Qx]]. For our purposes, it will be most natural to break \[[∃xPx]] into two pieces, \[[∃x]] and \[[Px]]. But first we need to get clear on expressions like \[[Qx]] and \[[Px]]. * GS&V say that the effect of updating an information state `s` with the meaning of "Qx" should be to eliminate possibilities in which the entity associated with the peg associated with the variable `x` does not have the property Q. In other words, if we let `q` be the function from entities to `bool`s that gives the extension of Q, then `s` updated with \[[Qx]] should be `s` filtered by the function `fun (r, h) -> let obj = List.nth h (r 'x') in q obj`. When `... q obj` evaluates to `true`, that `(r, h)` pair is retained, else it is discarded. - OK, we face two questions then. First, how do we carry this over to our present framework, where we're working with sets of `dpm`s instead of sets of discourse possibilities? And second, how do we decompose the behavior here attributed to \[[Qx]] into some meaning for "Q" and a different meaning for "x"? + OK, so we face two questions. First, how do we carry this over to our present framework, where we're working with sets of `dpm`s instead of sets of discourse possibilities? And second, how do we decompose the behavior here attributed to \[[Qx]] into some meaning for "Q" and a different meaning for "x"? * Answering the first question: we assume we've got some `bool dpm set` to start with. I won't call this `s` because that's what GS&V use for sets of discourse possibilities, and we don't want to confuse discourse possibilities with `dpm`s. Instead I'll call it `u`. Now what we want to do with `u` is to map each `dpm` it gives us to one that results in `(true, r, h)` only when the entity that `r` and `h` associate with variable `x` has the property Q. As above, I'll assume Q's extension is given by a function `q` from entities to `bool`s. Then what we want is something like this: - let eliminate_non_Qxs = (fun truth_value -> - fun (r, h) -> - let truth_value' = - if truth_value - then let obj = List.nth h (r 'x') in q obj - else false - in (truth_value', r, h)) - in bind_set u (fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs)) + let eliminator : bool -> bool dpm = + fun truth_value -> + fun (r, h) -> + let truth_value' = + if truth_value + then let obj = List.nth h (r 'x') in q obj + else false + in (truth_value', r, h) + in bind_set u (fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)) The first seven lines here just perfom the operation we described: return a `bool dpm` computation that only yields `true` when its input `(r, h)` associates variable `x` with the right sort of entity. The last line performs the `bind_set` operation. This works by taking each `dpm` in the set and returning a `unit_set` of a filtered `dpm`. The definition of `bind_set` takes care of collecting together all of the `unit_set`s that result for each different set element we started with. @@ -30,7 +31,7 @@ * Now our second question: how do we decompose the behavior here attributed to \[[Qx]] into some meaning for "Q" and a different meaning for "x"? - Well, we already know that \[[x]] will be a kind of computation that takes an assignment function `r` and store `h` as input. It will look up the entity that those two together associate with the variable `x`. So we can treat \[[x]] as an `entity dpm`. We don't worry here about sets of `dpm`s; we'll leave that to our predicates to interface with. We'll just make \[[x]] be a single `entity dpm`. So what we want is: + Well, we already know that \[[x]] will be a kind of computation that takes an assignment function `r` and store `h` as input. It will look up the entity that those two together associate with the variable `x`. So we can treat \[[x]] as an `entity dpm`. We don't worry here about `dpm set`s; we'll leave them to our predicates to interface with. We'll just make \[[x]] be a single `entity dpm`. So what we want is: let getx : entity dpm = fun (r, h) -> let obj = List.nth h (r 'x') @@ -44,16 +45,17 @@ fun entity_dpm -> unit_set (bind_dpm entity_dpm (fun e -> unit_dpm (q e))) - Finally, we realize that we're going to have a set of `bool dpm`s to start with, and we need to compose \[[Qx]] with them. We don't want any of the monadic values in the set that wrap `false` to become `true`; instead, we want to apply a filter that checks whether values that formerly wrapped `true` should still continue to do so. + Finally, we realize that we're going to have a set of `bool dpm`s to start with, and we need to monadically bind \[[Qx]] to them. We don't want any of the monadic values in the set that wrap `false` to become `true`; instead, we want to apply a filter that checks whether values that formerly wrapped `true` should still continue to do so. This could be handled like this: fun entity_dpm -> - let eliminate_non_Qxs = fun truth_value -> - if truth_value = false - then unit_dpm false - else bind_dpm entity_dpm (fun e -> unit_dpm (q e)) - in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs) + let eliminator : bool -> bool dpm = + fun truth_value -> + if truth_value = false + then unit_dpm false + else bind_dpm entity_dpm (fun e -> unit_dpm (q e)) + in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator) Applied to an `entity_dpm`, that yields a function that we can bind to a `bool dpm set` and that will transform the doubly-wrapped `bool` into a new `bool dpm set`. @@ -63,40 +65,43 @@ let obj = List.nth h (r 'x') in (obj, r, h) in let entity_dpm = getx - in let eliminate_non_Qxs = fun truth_value -> + in let eliminator = fun truth_value -> if truth_value = false then unit_dpm false else bind_dpm entity_dpm (fun e -> unit_dpm (q e)) - in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs) + in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator) + - unpacking the definition of `bind_dpm`, that is: + If we simplify and unpack the definition of `bind_dpm`, that's equivalent to: let getx = fun (r, h) -> let obj = List.nth h (r 'x') in (obj, r, h) - in let eliminate_non_Qxs = fun truth_value -> + in let eliminator = fun truth_value -> if truth_value then (fun (r, h) -> let (a, r', h') = getx (r, h) in let u' = (fun e -> unit_dpm (q e)) a in u' (r', h') ) else unit_dpm false - in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs) + in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator) - continuing to simplify: + which can be further simplified to: - let eliminate_non_Qxs = fun truth_value -> + - let eliminate_non_Qxs = fun truth_value -> + let eliminator = fun truth_value -> if truth_value then (fun (r, h) -> let obj = List.nth h (r 'x') in (q obj, r, h) ) else unit_dpm false - in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs) + in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator) This is a function that takes a `bool dpm` as input and returns a `bool dpm set` as output. (Compare to the \[[Qx]] we had before: - let eliminate_non_Qxs = (fun truth_value -> + let eliminator = (fun truth_value -> fun (r, h) -> let truth_value' = if truth_value then let obj = List.nth h (r 'x') in q obj else false in (truth_value', r, h)) - in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs) + in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator) Can you persuade yourself that these are equivalent?) @@ -144,7 +150,7 @@ or: - 
u >>=set \[[Qx]]
+	
u >>= \[[Qx]]
 	

 
 *	Can you figure out how to handle \[[∃x]] on your own? If not, here are some [more hints](/hints/assignment_7_hint_5). But try to get as far as you can on your own.
diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn
index 120c1fdb..2e7808a1 100644
--- a/hints/assignment_7_hint_5.mdwn
+++ b/hints/assignment_7_hint_5.mdwn
@@ -1,9 +1,11 @@
 
-*	How shall we handle \[[∃x]]? As we said, GS&V really tell us how to interpret \[[∃xPx]], but what they say about this breaks naturally into two pieces, such that we can represent the update of our starting set `u` with \[[∃xPx]] as:
+*	How shall we handle \[[∃x]]? As we said, GS&V really tell us how to interpret \[[∃xPx]], but for our purposes, what they say about this can be broken naturally into two pieces, such that we represent the update of our starting set `u` with \[[∃xPx]] as:
 
 	
u >>= \[[∃x]] >>= \[[Px]]
 	

 
+	(Extra credit: how does the discussion on pp. 25-29 of GS&V bear on the possibility of this simplification?)
+
 	What does \[[∃x]] need to be here? Here's what they say, on the top of p. 13:
 
 	>	Suppose an information state `s` is updated with the sentence ∃xPx. Possibilities in `s` in which no entity has the property P will be eliminated.
@@ -15,9 +17,9 @@
 	Deferring the "property P" part, this corresponds to:
 
 	
u updated with \[[∃x]] ≡
-		let extend_one : clause = fun one_dpm ->
-			List.map (fun d -> bind_dpm one_dpm (new_peg_and_assign 'x' d)) domain
-		in bind_set u extend_one
+		let extend one_dpm (d : entity) =
+			bind_dpm one_dpm (new_peg_and_assign 'x' d)
+		in bind_set u (fun one_dpm -> List.map (fun d -> extend one_dpm d) domain)
 	

 
 	where `new_peg_and_assign` is the operation we defined in [hint 3](/hints/assignment_7_hint_3):
@@ -36,11 +38,9 @@
 					(* we pass through the same truth_value that we started with *)
 					in (truth_value, r', h');;
 	
-	What's going on in this representation of `u` updated with \[[∃x]]? For each `bool dpm` in `u`, we collect `dpm`s that are the result of passing through their `bool`, but extending their input `(r, h)` by allocating a new peg for entity `d`, for each `d` in our whole domain of entities, and binding the variable `x` to the index of that peg.
-
-	A later step can then filter out all the `dpm`s where the entity `d` we did that with doesn't have property P.
+	What's going on in this proposed representation of \[[∃x]]? For each `bool dpm` in `u`, we collect `dpm`s that are the result of passing through their `bool`, but extending their input `(r, h)` by allocating a new peg for entity `d`, for each `d` in our whole domain of entities, and binding the variable `x` to the index of that peg. A later step can then filter out all the `dpm`s where the entity `d` we did that with doesn't have property P. (Again, consult GS&V pp. 25-9 for extra credit.)
 
-	So if we just call the function `extend_one` defined above \[[∃x]], then `u` updated with \[[∃x]] updated with \[[Px]] is just:
+	If we call the function `(fun one_dom -> List.map ...)` defined above \[[∃x]], then `u` updated with \[[∃x]] updated with \[[Px]] is just:
 
 	
u >>= \[[∃x]] >>= \[[Px]]
 	

@@ -128,8 +128,9 @@
 				fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
 		in fun bool_reader -> lifted_exists (shift 'x' bool_reader)
 
-	which we can simplify as:
+	which we can simplify to:
 
+	
 
 		fun bool_reader ->
-			let shifted'' r new_value =
+			let shifted r new_value =
 					let r' = fun var -> if var = 'x' then new_value else r var
 					in bool_reader r'
-			in fun r -> exists (shifted'' r)
+			in fun r -> exists (shifted r)
 
 	This gives us a value for \[[∃x]], which we use like this:
 
@@ -178,10 +180,12 @@
 	
u >>= \[[∃x]] >>= \[[Qx]]
 	

 
-	The crucial difference in GS&V's system is that the distinctive effect of the \[[∃x]]---to allocate new pegs in the store and associate variable `x` with the objects stored there---doesn't last only while interpreting clauses supplied as arguments to \[[∃x]]. Instead, it persists through the discourse, possibly affecting the interpretation of claims outside the logical scope of the quantifier. This is how we'll able to interpret claims like:
+	The crucial difference in GS&V's system is that the distinctive effect of the \[[∃x]]---to allocate new pegs in the store and associate variable `x` with the objects stored there---doesn't last only while interpreting some clauses supplied as arguments to \[[∃x]]. Instead, it persists through the discourse, possibly affecting the interpretation of claims outside the logical scope of the quantifier. This is how we'll able to interpret claims like:
 
 	>	If ∃x (man x and ∃y y is wife of x) then (x kisses y).
 
+	See the discussion on pp. 24-5 of GS&V.
+
 
 *	Can you figure out how to handle \[[not φ]] and the other connectives? If not, here are some [more hints](/hints/assignment_7_hint_6). But try to get as far as you can on your own.
 
diff --git a/hints/assignment_7_hint_6.mdwn b/hints/assignment_7_hint_6.mdwn
index a371b21c..0d9f02e8 100644
--- a/hints/assignment_7_hint_6.mdwn
+++ b/hints/assignment_7_hint_6.mdwn
@@ -5,38 +5,46 @@
 
 	where `i` *subsists* in s[φ] if there are any `i'` that *extend* `i` in s[φ].
 
-	Here's how to do that in our framework. Instead of a possibility subsisting in an updated set of possibilities, we ask what is returned by extensions of a `dpm` when they're given a particular (r, h) as input.
+	Here's how to do that in our framework. Instead of asking whether a possibility subsists in an updated set of possibilities, we ask what is returned by extensions of a `dpm` when they're given a particular (r, h) as input.
 
 		(* filter out which bool dpms in a set are true when receiving (r, h) as input *)
-		let truths set (r, h) = List.filter (fun one_dpm -> let (truth_value, _, _) = one_dpm (r, h) in truth_value) set;;
+		let truths set (r, h) =
+			let test one_dpm =
+				let (truth_value, _, _) = one_dpm (r, h)
+				in truth_value
+			in List.filter test set;;
 
 		let negate_op (phi : clause) : clause =
 			fun one_dpm ->
                 let new_dpm = fun (r, h) ->
-					(* we want to check the behavior of one_dpm when updated with the operation phi *)
-					(* bind_set (unit_set one_dpm) phi === phi one_dpm; do you remember why? *)
-					let truth_value' = truths (phi one_dpm) (r, h) = []
-					(* we return a (bool, r, h) so as to constitute a dpm *)
+					(* if one_dpm isn't already false at (r, h),
+					   we want to check its behavior when updated with phi
+					   bind_set (unit_set one_dpm) phi === phi one_dpm; do you remember why? *)
+				    let (truth_value, _, _) = one_dpm (r, h)
+					in let truth_value' = truth_value && (truths (phi one_dpm) (r, h) = [])
+					(* new_dpm must return a (bool, r, h) *)
                     in (truth_value', r, h)
-				in unit_set new_dpm
+				in unit_set new_dpm;;
 
 
 *	Representing \[[and φ ψ]] is simple:
 
 		let and_op (phi : clause) (psi : clause) : clause =
 			fun one_dpm -> bind_set (phi one_dpm) psi;;
+		(* now u >>= and_op phi psi === u >>= phi >>= psi; do you remember why? *)
+		
 
 *	Here are `or` and `if`:
 
 		let or_op (phi : clause) (psi : clause) =
-			(* NOT: negate_op (and_op (negate_op phi) (negate_op psi)) *)
             fun one_dpm -> unit_set (
                 fun (r, h) ->
-					in let truth_value' = truths (phi one_dpm) (r, h) <> [] || truths (bind_set (negate_op phi one_dpm) psi) (r, h) <> []
-                    in (truth_value', r, h))
+					in let truth_value' = (
+						truths (phi one_dpm) (r, h) <> [] ||
+						truths (bind_set (negate_op phi one_dpm) psi) (r, h) <> []
+					) in (truth_value', r, h))
 
 		let if_op (phi : clause) (psi : clause) : clause =
-			(* NOT: negate_op (and_op phi (negate_op psi)) *)
             fun one_dpm -> unit_set (
               fun (r, h) ->
 					in let truth_value' = List.for_all (fun one_dpm ->
@@ -77,7 +85,7 @@
 		(* this generalizes the proposal for \[[Q]] from hint 4 *)
 		let lift_predicate (f : entity -> bool) : entity dpm -> clause =
 			fun entity_dpm ->
-				let eliminator = fun (truth_value : bool) ->
+				let eliminator = fun truth_value ->
 					if truth_value = false
 					then unit_dpm false
 					else bind_dpm entity_dpm (fun e -> unit_dpm (f e))
@@ -86,12 +94,14 @@
 		(* doing the same thing for binary predicates *)
 		let lift_predicate2 (f : entity -> entity -> bool) : entity dpm -> entity dpm -> clause =
 			fun entity1_dpm entity2_dpm ->
-				let eliminator = fun (truth_value : bool) ->
+				let eliminator = fun truth_value ->
 					if truth_value = false
 					then unit_dpm false
 					else bind_dpm entity1_dpm (fun e1 -> bind_dpm entity2_dpm (fun e2 -> unit_dpm (f e1 e2)))
 				in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator);;
 
+ 
+
 		let new_peg_and_assign (var_to_bind : char) (d : entity) : bool -> bool dpm =
 		  fun truth_value ->
 			  fun (r, h) ->
@@ -102,8 +112,10 @@
 				in (truth_value, r', h')
 
 		(* from hint 5 *)
-		let exists var : clause = fun one_dpm ->
-			List.map (fun d -> bind_dpm one_dpm (new_peg_and_assign var d)) domain
+		let exists var : clause =
+			let extend one_dpm (d : entity) =
+				bind_dpm one_dpm (new_peg_and_assign var d)
+			in fun one_dpm -> List.map (fun d -> extend one_dpm d) domain
 
 		(* include negate_op, and_op, or_op, and if_op as above *)
 
-- 
2.11.0