From 5ffb50f1092baa2b76c7140b8c388d241240fa38 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Fri, 19 Nov 2010 00:25:42 -0500 Subject: [PATCH] assignment7 tweaks Signed-off-by: Jim Pryor --- hints/assignment_7_hint_1.mdwn | 8 +- hints/assignment_7_hint_2.mdwn | 33 +++---- hints/assignment_7_hint_3.mdwn | 108 +++++++---------------- hints/assignment_7_hint_4.mdwn | 189 +++++++++++++++++++++++++++++++++++++++++ hints/assignment_7_hint_5.mdwn | 2 + 5 files changed, 239 insertions(+), 101 deletions(-) create mode 100644 hints/assignment_7_hint_4.mdwn create mode 100644 hints/assignment_7_hint_5.mdwn diff --git a/hints/assignment_7_hint_1.mdwn b/hints/assignment_7_hint_1.mdwn index 6d6b760b..b6bff27c 100644 --- a/hints/assignment_7_hint_1.mdwn +++ b/hints/assignment_7_hint_1.mdwn @@ -3,13 +3,13 @@ * Where they represent pegs as natural numbers, that corresponds to our representing locations in a store by their indexes in the store. -* Where they say "reference system," which they use the leter `r` for, that corresponds to what we've been calling "assignments", and have been using the letter `g` for. +* Where they say "reference system," which they use the letter `r` for, that corresponds to what we've been calling "assignments", and have been using the letter `g` for. * Where they say `r[x/n]`, that's our `g{x:=n}`, or in OCaml, `fun v -> if v = 'x' then n else g v`. -* Their function `g`, which assigns objects from the domain to pegs, corresponds to our store function, which assigns entities to indexes. To avoid confusion, I'll use `r` for assignments, like they do, and avoid using `g` altogether. Instead I'll use `h` for stores. (We can't use `s` because GS&V use that for something else, which they call "information states.") +* Their function `g`, which assigns entities from the domain to pegs, corresponds to our store function, which assigns entities to indexes. To avoid confusion, I'll use `r` for assignments, like they do, and avoid using `g` altogether. Instead I'll use `h` for stores. (We can't use `s` because GS&V use that for something else, which they call "information states.") -* At several places they talk about some things being *real extensions* of other things. This confused me at first, because they don't ever define a notion of "real extension." (They do define what they mean by "extensions.") At one point in the paper, it emerges that what they mean is what I'd call a *proper extension*: an extension which isn't identical to the original. +* At several places they talk about some things being *real extensions* of other things. This confused me at first, because they don't ever define a notion of "real extension." (They do define what they mean by "extensions.") Eventually, it emerges that what they mean is what I'd call a *proper extension*: an extension which isn't identical to the original. -* [More hints](/hints/assignment_7_hint_2). +* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_2). diff --git a/hints/assignment_7_hint_2.mdwn b/hints/assignment_7_hint_2.mdwn index 6047aeb8..17a3955a 100644 --- a/hints/assignment_7_hint_2.mdwn +++ b/hints/assignment_7_hint_2.mdwn @@ -1,39 +1,34 @@ -* GS&V's semantics involves elements from several different monads we've been looking at. First, they're working with (epistemic) modalities, so there are worlds playing a role like they did in [[Reader Monad for Intensionality]]. But we're going to ignore the modal element for this exercise. There's also variable binding, which is [another reader monad](/reader_monad_for_variable_binding). Next, there is a notion of a store, which some operations add new reference cells to. We implement this with a state monad (and so too do they, in effect, though they don't conceive of what they're doing in those terms). So we'll be working with a combination of both a reader monad for the variable binding and a state monad to keep track of the new "pegs" or reference cells. +* GS&V's semantics involves elements from several different monads we've been looking at. First, they're working with (epistemic) modalities, so there are worlds playing a role like they did in [[Reader Monad for Intensionality]]. But we're going to ignore the modal element for this exercise. There's also variable binding, which calls for [another reader monad](/reader_monad_for_variable_binding). Next, there is a notion of a store, which some operations add new reference cells to. We implement this with a state monad (and so too, in effect, do they---though they don't conceive of what they're doing in those terms). So we'll be working with a combination of both a reader monad for the variable binding and a state monad to keep track of the new "pegs" or reference cells. There are systematic ways to layer different monads together. If you want to read about these, a keyword is "monad transformers." Ken Shan discusses them in [his paper](http://arxiv.org/abs/cs/0205026v1) that we recommended earlier. However, since we haven't studied these, we will just combine the reader monad and the state monad in an ad hoc way. The easiest way to do this is to think of the assignment function and the store of reference cells as a combined state, which gets threaded through the computations in the same way that simple states did in your earlier homeworks. - We'll call these "discourse possibility monads," and type them as follows: + We'll call these "discourse possibility monads," or `dpm`s, and type them as follows: type entity = Bob | Carol | Ted | Alice;; let domain = [Bob; Carol; Ted; Alice];; - type var = char;; - type assignment = var -> int;; (* variables are bound to indexes into the store *) + type assignment = char -> int;; (* variables are bound to indexes into the store *) type store = entity list;; - type 'a discourse_possibility = + type 'a dpm = (* we ignore worlds *) assignment * store -> 'a * assignment * store - Although we're leaving worlds out of the picture, each of these monadic objects still represents a different discourse possibility: which entities might be being talked about, using which variables. + Although we're leaving worlds out of the picture, each of these monadic values still represents a different discourse possibility: which entities might be being talked about, using which variables. -* We notice though that GS&V don't just work with discourse possibilities (or more broadly, epistemic possibilities), they work with what they call "information states," which are *sets* of possibilities. OK, a set is just another monadic layer. For simplicity, we'll represent sets using lists: + Since `dpm`s are to be a monad, we have to define a unit and a bind. These are just modeled on the unit and bind for the state monad: - type 'a set = 'a list;; - let empty_set : 'a set = [];; - let unit_set (x: 'a) : 'a set = [x];; - let bind_set (u: 'a set) (f: 'a -> 'b set) = - List.concat (List.map f u);; + let unit_dpm (x : 'a) = fun (r, h) -> (x, r, h);; - The following will be useful later: persuade yourself that `List.filter (test : 'a -> bool) (u : 'a set) : 'a set` is the same as: + let bind_dpm (u : 'a dpm) (f : 'a -> 'b dpm) = + fun (r, h) -> + let (a, r', h') = u (r, h) + in let u' = f a + in u' (r', h') - bind_set u (fun a -> if test a then unit_set a else empty_set) +* A *possibility* for GS&V is a triple of an assignment function `r`, a store `h`, and a world `w`. We're dropping worlds so we'll call pairs `(r, h)` *discourse possibilities*. *dpm*s are monads that represent computations that may mutate---or in GS&V's terminology "extend"---discourse possibilities. An `'a dpm` is a function that takes a starting `(r, h)` and returns an `'a` and a possibly mutated `r'` and `h'`. - -* So GS&V's information states, which they notate using `s`, are set-monads, whose elements in turn are discourse possibilities, which they notate using `i`, which are state monads that keep track of which entities have been introduced as objects of discourse, and which variables are bound to them, in the discourse possibility in question. In GS&V's system, possibilities are triples of an assignment function, `r`, a store `h`, and a world `w`. We're leaving the worlds out. Also, instead of just working with pairs `(r, h)`, we're working with state monads for which those pairs constitute the states we update. - - -* [More hints](/hints/assignment_7_hint_3). +* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_3). diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn index 842d90ea..8382a9bb 100644 --- a/hints/assignment_7_hint_3.mdwn +++ b/hints/assignment_7_hint_3.mdwn @@ -1,96 +1,48 @@ -* In def 2.5, they say the denotation of an e-type constant α wrt a discourse possibility `(r, h, w)` is whatever object the world `w` associates with α. Since we don't have worlds, this will just be an object. +* You will notice that GS&V don't just work with discourse possibilities (or more broadly, epistemic possibilities), they work with what they call "information states," which are *sets* of possibilities. -* 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. + 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. -* They say the denotation of a variable is the object 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')`. + 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. -We're going to keep all of that, except dropping the worlds. And instead of talking about +As I said, for simplicity, we'll represent sets using lists: -> \[[expression]] in possibility `(r, h, w)` + type 'a set = 'a list;; + let empty_set : 'a set = [];; + let unit_set (x: 'a) : 'a set = [x];; + let bind_set (u: 'a set) (f: 'a -> 'b set) = + List.concat (List.map f u);; -we'll just talk about \[[expression]] and let that be a monadic object, implemented in part by a function that takes `(r, h)` as an argument. +* 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. -More specifically, \[[expression]] will be a set of `'a discourse_possibility` monads, where `'a` is the appropriate type for *expression*, and the discourse possibility monads are themselves state monads where `(r, h)` is the state that gets updated. Those are implemented as functions from `(r, h)` to `(a, r', h')`, where `a` is a value of type `'a`, and `r', h'` are possibly altered assignment functions and stores. +* 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.7, GS&V talk about an operation that takes an existing set of discourse possibilities, and extends each member in the set by allocating a new location in the store, and assigning a variable `'x'` to that location, which holds some object `d` from the domain. It will be useful to have a shorthand way of referring to this operation: + 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. - let newpeg_and_bind (bound_variable : char) (d : entity) = + 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')`. + +* We're going to keep all of that, except dropping the worlds. And instead of talking about: + + > \[[expression]] in possibility `(r, h, w)` + + 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. + +* 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: + + let new_peg_and_assign (var_to_bind : char) (d : entity) = fun ((r, h) : assignment * store) -> + (* first we calculate an unused index *) let newindex = List.length h - (* first we store d at index newindex in h, which is at the very end *) + (* 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 *) in let h' = List.append h [d] (* next we assign 'x' to location newindex *) in let r' = fun v -> - if v = bound_variable then newindex else r v + if v = var_to_bind then newindex else r v in (r',h') -* 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 easiest for us to break \[[∃xPx]] into two pieces, \[[∃x]] and \[[Px]]. Let's consider expressions like \[[Px]] first. - - They say that the effect of updating an information state `s` with the meaning of "Qx" should be to eliminate possibilities in which the object associated with the peg associated with the variable `x` does not have the property Q. In other words, if we let `Q` be a function from objects to `bool`s, `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. - - Recall that [we said before](/hints/assignment_7_hint_2) that `List.filter (test : 'a -> bool) (u : 'a set) : 'a set` is the same as: - - bind_set u (fun a -> if test a then unit_set a else empty_set) - - Hence, updating `s` with \[[Qx]] should be: - - bind_set s (fun (r, h) -> if (let obj = List.nth h (r 'x') in Q obj) then unit_set (r, h) else empty_set) - - We can call the `(fun (r, h) -> ...)` part \[[Qx]] and then updating `s` with \[[Qx]] will be: - - bind_set s \[[Qx]] - - or as it's written using Haskell's infix notation for bind: - - s >>= \[[Qx]] - -* 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 object 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 objects `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 object `d`, for each `d` in our whole domain of objects (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 object `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
-
- +* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_4). diff --git a/hints/assignment_7_hint_4.mdwn b/hints/assignment_7_hint_4.mdwn new file mode 100644 index 00000000..b17f83f3 --- /dev/null +++ b/hints/assignment_7_hint_4.mdwn @@ -0,0 +1,189 @@ + +* 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 \[[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 a function from entities to `bool`s, `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 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: + + let test = (fun (truth_value, r, h) -> + truth_value && (let obj = List.nth h (r 'x') in Q obj)) + in List.filter test u + + Persuade yourself that in general: + + List.filter (test : 'a -> bool) (u : 'a set) : 'a set + + 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: + + bind_set u \[[Qx]] + + or as it's written using Haskell's infix notation for bind: + + u >>= \[[Qx]] + +* 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: + + 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`). + +* 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: + + 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`: + + fun entity_dpm -> unit_set (bind_dpm entity_dpm (fun e -> unit_dpm (Q e))) + + 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))) + + 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))) + + 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')) + + 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')) + + 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: + + 
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
+
+ + diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn new file mode 100644 index 00000000..139597f9 --- /dev/null +++ b/hints/assignment_7_hint_5.mdwn @@ -0,0 +1,2 @@ + + -- 2.11.0