* 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 our starting set `u` with \[[∃xPx]] as:
* 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 our starting set `u` with \[[∃xPx]] as:
(* we pass through the same truth_value that we started with *)
in let r' = fun var ->
if var = var_to_bind then new_index else r var
(* we pass through the same truth_value that we started with *)
- in (truth_value, r', h')
+ in (truth_value, r', h');;
What's going on in this representation of `u` updated with \[[∃x]]? For each `bool dpm` in `u`, we collect `dpm`s that are the result of passing through their `bool`, but extending their input `(r, h)` by allocating a new peg for entity `d`, for each `d` in our whole domain of entities, and binding the variable `x` to the index of that peg.
What's going on in this representation of `u` updated with \[[∃x]]? For each `bool dpm` in `u`, we collect `dpm`s that are the result of passing through their `bool`, but extending their input `(r, h)` by allocating a new peg for entity `d`, for each `d` in our whole domain of entities, and binding the variable `x` to the index of that peg.
Now, how would we implement quantifiers in this setting? I'll assume we have a function `exists` of type `(entity -> bool) -> bool`. That is, it accepts a predicate as argument and returns `true` if any element in the domain satisfies that predicate. We could implement the reader-monad version of that like this:
Now, how would we implement quantifiers in this setting? I'll assume we have a function `exists` of type `(entity -> bool) -> bool`. That is, it accepts a predicate as argument and returns `true` if any element in the domain satisfies that predicate. We could implement the reader-monad version of that like this:
- fun (lifted_predicate : entity reader -> bool reader) ->