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 bools 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, so we face two questions. First, how do we carry this over to our present framework, where we're working with sets of dpms 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 dpms. 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 bools.

Then what we want is something like this:

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 set_bind u (fun one_dpm -> set_unit (dpm_bind 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 set_bind operation. This works by taking each dpm in the set and returning a set_unit of a filtered dpm. The definition of set_bind takes care of collecting together all of the set_units that result for each different set element we started with.

We can call the (fun one_dpm -> ...) part [[Qx]] and then updating u with [[Qx]] will be:

set_bind 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 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 dpm sets; 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')
    in (obj, r, h);;

Now what do we do with predicates? As before, we suppose we have a function q that maps entities to bools. We want to turn it into a function that maps entity dpms to bool dpms. Eventually we'll need to operate not just on single dpms but on sets of them, but first things first. We'll begin by lifting q into a function that takes entity dpms as arguments and returns bool dpms:

fun entity_dpm -> dpm_bind entity_dpm (fun e -> dpm_unit (q e))

Now we have to transform this into a function that again takes single entity dpms as arguments, but now returns a bool dpm set. This is easily done with set_unit:

fun entity_dpm -> set_unit (dpm_bind entity_dpm (fun e -> dpm_unit (q e)))

Finally, we realize that we're going to have a set of bool dpms 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 eliminator : bool -> bool dpm =
        fun truth_value ->
            if truth_value = false
            then dpm_unit false
            else dpm_bind entity_dpm (fun e -> dpm_unit (q e))
    in fun one_dpm -> set_unit (dpm_bind 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.

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 let eliminator = fun truth_value ->
    if truth_value = false
    then dpm_unit false
    else dpm_bind entity_dpm (fun e -> dpm_unit (q e))
in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)

If we simplify and unpack the definition of dpm_bind, that's equivalent to:

let getx = fun (r, h) ->
    let obj = List.nth h (r 'x')
    in (obj, r, h)
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 -> dpm_unit (q e)) a
            in u' (r', h')
    ) else dpm_unit false
in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)

which can be further simplified to:

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 dpm_unit false
in fun one_dpm -> set_unit (dpm_bind 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 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 -> set_unit (dpm_bind one_dpm eliminator)

Can you persuade yourself that these are equivalent?)

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 monadically bind this operaration to whatever bool dpm set we already have on hand:

set_bind u [[Qx]]

or:

u >>= [[Qx]]

Can you figure out how to handle [[∃x]] on your own? If not, here are some more hints. But try to get as far as you can on your own.