From 458cadab1427b0fc0f7bc8689f1dddb18b2201e7 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Fri, 19 Nov 2010 07:54:06 -0500 Subject: [PATCH] assignment7 tweaks Signed-off-by: Jim Pryor --- hints/assignment_7_hint_3.mdwn | 6 +- hints/assignment_7_hint_4.mdwn | 203 ++++++++++++++++------------------------- hints/assignment_7_hint_5.mdwn | 47 ++++++++++ 3 files changed, 127 insertions(+), 129 deletions(-) diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn index d3e06c53..7617922b 100644 --- a/hints/assignment_7_hint_3.mdwn +++ b/hints/assignment_7_hint_3.mdwn @@ -3,7 +3,7 @@ Now some of the `dpm`s we work with will be `bool dpm`s, which are functions from discourse possibilities to `bool`s (and discourse possibilities). It's tempting to think we might just work with `bool dpm`s instead of sets of possibilities. However, I don't think this can work. The reason why is that at a crucial point in GS&Vs semantics, we have to work with not just a *single* way of mutating or "extending" a discourse possibility, but a *range* of different ways to mutate the live discourse possibilities. So we do need to work with sets, after all. - A set is just another monadic layer. We've already talked about list monads, and we can for these purposes just use list monads to represent set monads. Instead of sets of possibilities, we'll be working with sets of `dpm`s, that is, sets of discourse possibility monads, or computations on discourse possibilities. + A set is just another monadic layer. We've already talked about list monads, and we can for these purposes just use list monads to represent set monads. Instead of sets of possibilities, let's work with sets of `dpm`s, that is, sets of discourse possibility monads, or computations on discourse possibilities. As I said, for simplicity, we'll represent sets using lists: @@ -27,7 +27,7 @@ we'll just talk about \[[expression]] and let that be a monadic value, implemented in part by a function that takes `(r, h)` as an argument. - More specifically, \[[expression]] will be a set of `'a dpm`s, where `'a` is the appropriate type for *expression*. An `'a dpm` is implemented by a function that takes `(r, h)` as an argument. + More specifically, \[[expression]] will be a set of `'a dpm`s, where `'a` is the appropriate type for *expression*. Each `'a dpm` is implemented by a function that takes `(r, h)` as an argument. * In def 2.7, GS&V talk about an operation that takes an existing set of discourse possibilities, and *extends* each member in the set by (i) allocating a new location in the store, (ii) putting some entity `d` from the domain in that location, and (iii) assigning variable `x` to that location in the store. It will be useful to have a shorthand way of referring to this operation: @@ -37,7 +37,7 @@ It will be useful to have a shorthand way of referring to this operation: (* first we calculate an unused index *) let newindex = List.length h (* next we store d at h[newindex], which is at the very end of h *) - (* the following line achieves that in a simple but very inefficient way *) + (* the following line achieves that in a simple but inefficient way *) in let h' = List.append h [d] (* next we assign 'x' to location newindex *) in let r' = fun v -> diff --git a/hints/assignment_7_hint_4.mdwn b/hints/assignment_7_hint_4.mdwn index b17f83f3..d41e0f0a 100644 --- a/hints/assignment_7_hint_4.mdwn +++ b/hints/assignment_7_hint_4.mdwn @@ -5,33 +5,22 @@ 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 ascribed 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 apply a filter that only lets through those `bool dpm`s whose outputs are `(true, r, h)`, where the entity that `r` and `h` associate with variable `x` has the property P. So what we want is: +* 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. I'll assume we have some function Q to start with that maps entities to `bool`s. - let test = (fun (truth_value, r, h) -> - truth_value && (let obj = List.nth h (r 'x') in Q obj)) - in List.filter test u + Then what we want is something like this: - Persuade yourself that in general: + 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)) - List.filter (test : 'a -> bool) (u : 'a set) : 'a set + The first three seven lines here just perfom the operation we described: return a `bool dpm` computation that only yields `true` whether 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. - is the same as: - - bind_set u (fun a -> if test a then unit_set a else empty_set) - - Hence substituting in our above formula, we can derive: - - let test = (fun (truth_value, r, h) -> - truth_value && (let obj = List.nth h (r 'x') in Q obj)) - in bind_set u (fun a -> if test a then unit_set a else empty_set) - - or simplifying: - - bind_set u (fun (truth_value, r, h) -> - if truth_value && (let obj = List.nth h (r 'x') in Q obj) - then unit_set (true, r, h) else empty_set) - - We can call the `(fun (truth_value, r, h) -> ...)` part \[[Qx]] and then updating `u` with \[[Qx]] will be: + We can call the `(fun one_dpm -> ...)` part \[[Qx]] and then updating `u` with \[[Qx]] will be: bind_set u \[[Qx]] @@ -41,149 +30,111 @@ * Now our second question: how do we decompose the behavior here ascribed 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`. Except that we don't have just one `dpm` to compose it with, but a set of them. However, we'll leave that to our predicates to deal with. We'll just make \[[x]] be an operation on a single `dpm`. Let's call the `dpm` we start with `v`. Then what we want to do 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 sets of `dpm`s; we'll leave that to our predicates to interface with. We'll just make \[[x]] be a single `entity dpm`. Then what we want is: let getx = fun (r, h) -> let obj = List.nth h (r 'x') - in (obj, r, h) - in bind_dpm v (fun _ -> getx) - - What's going on here? Our starting `dpm` is a kind of monadic box. We don't care what value is inside that monadic box, which is why we're binding it to a function of the form `fun _ -> ...`. What we return is a new monadic box, which takes `(r, h)` as input and returns the entity they associate with variable `x` (together with unaltered versions of `r` and `h`). + in (obj, r, h);; -* Now what do we do with predicates? We suppose we're given a function Q that maps entities to `bool`s. We want to turn it into a function that maps `entity dpm`s to `bool dpm`s. Eventually we'll need to operate not just on single `dpm`s but on sets of them, but first things first. We'll begin by lifting Q into a function that takes `entity dpm`s as arguments and returns `bool dpm`s: +* Now what do we do with predicates? As before, we suppose we have a function Q that maps entities to `bool`s. We want to turn it into a function that maps `entity dpm`s to `bool dpm`s. Eventually we'll need to operate not just on single `dpm`s but on sets of them, but first things first. We'll begin by lifting Q into a function that takes `entity dpm`s as arguments and returns `bool dpm`s: fun entity_dpm -> bind_dpm entity_dpm (fun e -> unit_dpm (Q e)) - Now we have to transform this into a function that again takes single `entity dpm`s as arguments, but now returns a `(bool dpm) set`. This is easily done with `unit_set`: + Now we have to transform this into a function that again takes single `entity dpm`s as arguments, but now returns a `bool dpm set`. This is easily done with `unit_set`: 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. + + This is most easily done like this: + + fun entity_dpm -> + fun truth_value -> + if truth_value = false + then empty_set + else unit_set (bind dpm entity_dpm (fun e -> unit_dpm (Q e))) + + Doing things this way will discard `bool dpm`s that start out wrapping `false`, and will pass through other `bool dpm`s that start out wrapping `true` but which our current filter transforms to a wrapped `false`. You might instead aim for consistency, and always pass through wrapped `false`s, whether they started out that way or are only now being generated; or instead always discard such, and only pass through wrapped `true`s. But what we have here will work fine too. + If we let that be \[[Q]], then \[[Q]] \[[x]] would be: let getx = fun (r, h) -> let obj = List.nth h (r 'x') in (obj, r, h) in let entity_dpm = getx - in unit_set (bind_dpm entity_dpm (fun e -> unit_dpm (Q e))) + in fun truth_value -> + if truth_value = false + then empty_set + else unit_set (bind_dpm entity_dpm (fun e -> unit_dpm (Q e))) or, simplifying: let getx = fun (r, h) -> let obj = List.nth h (r 'x') in (obj, r, h) - in unit_set (bind_dpm getx (fun e -> unit_dpm (Q e))) + in fun truth_value -> + if truth_value + then unit_set (bind_dpm getx (fun e -> unit_dpm (Q e))) + else empty_set which is: let getx = fun (r, h) -> let obj = List.nth h (r 'x') in (obj, r, h) - in fun (r, h) -> - let (a, r', h') = getx (r, h) - in let u' = (fun e -> unit_dpm (Q e)) a - in unit_set (u' (r', h')) + in fun truth_value -> + if truth_value + then unit_set ( + 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 empty_set which is: - fun (r, h) -> - let obj = List.nth h (r 'x') - in let (a, r', h') = (obj, r, h) - in let u' = (fun e -> unit_dpm (Q e)) a - in unit_set (u' (r', h')) + in fun truth_value -> + if truth_value + then unit_set ( + fun (r, h) -> + let obj = List.nth h (r 'x') + let (a, r', h') = (obj, r, h) + in let u' = (fun e -> unit_dpm (Q e)) a + in u' (r', h') + ) else empty_set which is: - fun (r, h) -> - let obj = List.nth h (r 'x') - in let u' = unit_dpm (Q obj) - in unit_set (u' (r, h)) - - which is: - - fun (r, h) -> - let obj = List.nth h (r 'x') - in unit_set (unit_dpm (Q obj) (r, h)) - - which is: - - fun (r, h) -> - let obj = List.nth h (r 'x') - in unit_set ((Q obj, r, h)) - - - - - - - - -, so really \[[x]] will need to be a monadic operation on *a set of* `entity dpm`s. But one thing at a time. First, let's figure out what operation should be performed on each starting `dpm`. Let's call the `dpm` we start with `v`. Then what we want to do is: - - - So that's how \[[x]] should operate on a single `dpm`. How should it operate on a set of them? Well, we just have to take each member of the set and return a `unit_set` of the operation we perform on each of them. The `bind_set` operation takes care of joining all those `unit_set`s together. So, where `u` is the set of `dpm`s we start with, we have: - - let handle_each = fun v -> - (* as above *) - let getx = fun (r, h) -> - let obj = List.nth h (r 'x') - in (obj, r, h) - in let result = bind_dpm v (fun _ -> getx) - (* we return a unit_set of each result *) - in unit_set result - in bind_set u handle_each - - This is a computation that takes a bunch of `_ dpm`s and returns `dpm`s that return their input discourse possibilities unaltered, together with the entity those discouse possibilities associate with variable 'x'. We can take \[[x]] to be the `handle_each` function defined above. - - -* 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')`. - - - -* Now 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 `s` with \[[∃xPx]] as: - - 
s >>= \[[∃x]] >>= \[[Px]]
-
- - 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. - - We can defer that to a later step, where we do `... >>= \[[Px]]`. - - > The referent system of the remaining possibilities will be extended with a new peg, which is associated with `x`. And for each old possibility `i` in `s`, there will be just as many extensions `i[x/d]` in the new state `s'` and there are entities `d` which in the possible world of `i` have the property P. - - Deferring the "property P" part, this says: + in fun truth_value -> + if truth_value + then unit_set ( + fun (r, h) -> + let obj = List.nth h (r 'x') + in let u' = unit_dpm (Q obj) + in u' (r', h') + ) else empty_set + + This is a bit different than the \[[Qx]] we had before: - 
s updated with \[[∃x]] ≡
-		s >>= (fun (r, h) -> List.map (fun d -> newpeg_and_bind 'x' d) domain)
-
- - That is, for each pair `(r, h)` in `s`, we collect the result of extending `(r, h)` by allocating a new peg for entity `d`, for each `d` in our whole domain of entities (here designated `domain`), and binding the variable `x` to the index of that peg. + 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 (fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs)) - A later step can then filter out all the possibilities in which the entity `d` we did that with doesn't have property P. + because that one passed through every `bool dpm` that wrapped a `false`; whereas now we're discarding some of them. But these will work equally well. We can implement either behavior (or, as we said before, the behavior of never passing through a wrapped `false`). - So if we just call the function `(fun (r, h) -> ...)` above \[[∃x]], then `s` updated with \[[∃x]] updated with \[[Px]] is just: +* Reviewing: now we've determined how to define \[[Q]] and \[[x]] such that \[[Qx]] can be the result of applying the function \[[Q]] to the `entity dpm` \[[x]]. And \[[Qx]] in turn is now a function that takes a `bool dpm` as input and returns a `bool dpm set` as output. We compose this with a `bool dpm set` we already have on hand: - 
s >>= \[[∃x]] >>= \[[Px]]
-
+ bind_set u \[[Qx]] - or, being explicit about which "bind" operation we're representing here with `>>=`, that is: + or: - 
bind_set (bind_set s \[[∃x]]) \[[Px]]
+	
u >>=set \[[Qx]]
 	

 
-*	In def 3.1 on p. 14, GS&V define `s` updated with \[[not φ]] as:
-
-	>	{ i &elem; s | i does not subsist in s[φ] }
-
-	where `i` *subsists* in s[φ] if there are any `i'` that *extend* `i` in s[φ].
-
-	Here's how we can represent that:
-
-		
bind_set s (fun (r, h) ->
-			let u = unit_set (r, h)
-			in let descendents = u >>= \[[φ]]
-			in if descendents = empty_set then u else empty_set
-		

-
+*	Can you figure out how to handle \[[∃x]] on your own? If not, here are some [more hints](/hints/assignment_7_hint_5).
 
diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn
index 139597f9..46ca442d 100644
--- a/hints/assignment_7_hint_5.mdwn
+++ b/hints/assignment_7_hint_5.mdwn
@@ -1,2 +1,49 @@
 
+*	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 `s` with \[[∃xPx]] as:
+
+	
s >>= \[[∃x]] >>= \[[Px]]
+	

+
+	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.
+
+	We can defer that to a later step, where we do `... >>= \[[Px]]`.
+ 
+	>	The referent system of the remaining possibilities will be extended with a new peg, which is associated with `x`. And for each old possibility `i` in `s`, there will be just as many extensions `i[x/d]` in the new state `s'` and there are entities `d` which in the possible world of `i` have the property P.
+
+	Deferring the "property P" part, this says:
+
+	
s updated with \[[∃x]] ≡
+		s >>= (fun (r, h) -> List.map (fun d -> newpeg_and_bind 'x' d) domain)
+	

+	
+	That is, for each pair `(r, h)` in `s`, we collect the result of extending `(r, h)` by allocating a new peg for entity `d`, for each `d` in our whole domain of entities (here designated `domain`), and binding the variable `x` to the index of that peg.
+
+	A later step can then filter out all the possibilities in which the entity `d` we did that with doesn't have property P.
+
+	So if we just call the function `(fun (r, h) -> ...)` above \[[∃x]], then `s` updated with \[[∃x]] updated with \[[Px]] is just:
+
+	
s >>= \[[∃x]] >>= \[[Px]]
+	

+
+	or, being explicit about which "bind" operation we're representing here with `>>=`, that is:
+
+	
bind_set (bind_set s \[[∃x]]) \[[Px]]
+	

+
+*	In def 3.1 on p. 14, GS&V define `s` updated with \[[not φ]] as:
+
+	>	{ i &elem; s | i does not subsist in s[φ] }
+
+	where `i` *subsists* in s[φ] if there are any `i'` that *extend* `i` in s[φ].
+
+	Here's how we can represent that:
+
+		
bind_set s (fun (r, h) ->
+			let u = unit_set (r, h)
+			in let descendents = u >>= \[[φ]]
+			in if descendents = empty_set then u else empty_set
+		

+
 
-- 
2.11.0