- 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:
-
- <pre><code>s >>= \[[∃x]] >>= \[[Px]]
+ 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')
+ let (a, r', h') = (obj, 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)
+
+ let eliminator = fun truth_value ->
+ if truth_value
+ then (fun (r, h) ->
+ let obj = List.nth h (r 'x')
+ in let u' = dpm_unit (q obj)
+ in u' (r, h)
+ ) else dpm_unit false
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
+ -->
+
+ 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:
+
+ <pre><code>u >>= \[[Qx]]