``````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).

``````