* 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`.
+* Where they say `r[x/n]`, that's our `g{x:=n}`, or in OCaml, `fun var -> if var = 'x' then n else g var`.
* 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.") Eventually, it emerges that what they mean is what I'd call a *proper extension*: an extension which isn't identical to the original.
-* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_2).
+* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_2). But try to get as far as you can on your own.
* 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'`.
-* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_3).
+* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_3). But try to get as far as you can on your own.
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
- (* next we store d at h[newindex], which is at the very end of h *)
+ let new_index = List.length h
+ (* next we store d at h[new_index], which is at the very end of h *)
(* the following line achieves that in a simple but inefficient way *)
in let h' = List.append h [d]
- (* next we assign 'x' to location newindex *)
- in let r' = fun v ->
- if v = var_to_bind then newindex else r v
+ (* next we assign 'x' to location new_index *)
+ in let r' = fun var ->
+ if var = var_to_bind then new_index else r var
(* the reason for returning true as an initial element will emerge later *)
- in (true, r',h')
+ in (true, r', h')
-* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_4).
+* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_4). But try to get as far as you can on your own.
* 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.
+* 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 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. I'll assume we have some function Q to start with that maps entities to `bool`s.
+* 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 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. I'll assume we have some function q to start with that maps entities to `bool`s.
Then what we want is something like this:
fun (r, h) ->
let truth_value' =
if truth_value
- then let obj = List.nth h (r 'x') in Q obj
+ then let obj = List.nth h (r 'x') in q obj
else false
in (truth_value', r, h))
in bind_set u (fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs))
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 `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:
+* Now what do we do with predicates? As before, we suppose we have 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))
+ 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)))
+ fun entity_dpm -> unit_set (bind_dpm entity_dpm (fun e -> unit_dpm (q e)))
Finally, we realize that we're going to have a set of `bool dpm`s to start with, and we need to compose \[[Qx]] with 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.
fun entity_dpm ->
let eliminate_non_Qxs = fun truth_value ->
if truth_value = false
- then empty_set
- else unit_set (bind_dpm entity_dpm (fun e -> unit_dpm (Q e)))
- in fun one_dpm -> (bind_dpm one_dpm eliminate_non_Qxs)
+ then unit_dpm false
+ else bind_dpm entity_dpm (fun e -> unit_dpm (q e))
+ in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs)
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`.
- Doing things this way will discard `bool dpm`s from the set that started out wrapping `false`, and will pass through other `bool dpm`s that start out wrapping `true` but which our current filter transforms to a wrapped `false`. You might instead aim for consistency, and always pass through wrapped `false`s, whether they started out that way or are only now being generated; or instead always discard such, and only pass through wrapped `true`s. But what we have here will work fine too.
-
If we let that be \[[Q]], then \[[Q]] \[[x]] would be:
let getx = fun (r, h) ->
in let entity_dpm = getx
in let eliminate_non_Qxs = fun truth_value ->
if truth_value = false
- then empty_set
- else unit_set (bind_dpm entity_dpm (fun e -> unit_dpm (Q e)))
- in fun one_dpm -> (bind_dpm one_dpm eliminate_non_Qxs)
+ then unit_dpm false
+ else bind_dpm entity_dpm (fun e -> unit_dpm (q e))
+ in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs)
or, simplifying:
in (obj, r, h)
in let eliminate_non_Qxs = fun truth_value ->
if truth_value
- then unit_set (bind_dpm getx (fun e -> unit_dpm (Q e)))
- else empty_set
- in fun one_dpm -> (bind_dpm one_dpm eliminate_non_Qxs)
+ then bind_dpm getx (fun e -> unit_dpm (q e))
+ else unit_dpm false
+ in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs)
unpacking the definition of `bind_dpm`, that is:
in (obj, r, h)
in let eliminate_non_Qxs = fun truth_value ->
if truth_value
- then unit_set (
- fun (r, h) ->
+ then (fun (r, h) ->
let (a, r', h') = getx (r, h)
- in let u' = (fun e -> unit_dpm (Q e)) a
+ in let u' = (fun e -> unit_dpm (q e)) a
in u' (r', h')
- ) else empty_set
- in fun one_dpm -> (bind_dpm one_dpm eliminate_non_Qxs)
+ ) else unit_dpm false
+ in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs)
- which is:
+ continuing to simplify:
let eliminate_non_Qxs = fun truth_value ->
if truth_value
- then unit_set (
- fun (r, h) ->
+ then (fun (r, h) ->
let obj = List.nth h (r 'x')
let (a, r', h') = (obj, r, h)
- in let u' = (fun e -> unit_dpm (Q e)) a
+ in let u' = (fun e -> unit_dpm (q e)) a
in u' (r', h')
- ) else empty_set
- in fun one_dpm -> (bind_dpm one_dpm eliminate_non_Qxs)
-
- which is:
+ ) else unit_dpm false
+ in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs)
let eliminate_non_Qxs = fun truth_value ->
if truth_value
- then unit_set (
- fun (r, h) ->
+ then (fun (r, h) ->
let obj = List.nth h (r 'x')
- in let u' = unit_dpm (Q obj)
+ in let u' = unit_dpm (q obj)
in u' (r, h)
- ) else empty_set
- in fun one_dpm -> (bind_dpm one_dpm eliminate_non_Qxs)
+ ) else unit_dpm false
+ in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs)
+
+ let eliminate_non_Qxs = fun truth_value ->
+ if truth_value
+ then (fun (r, h) ->
+ let obj = List.nth h (r 'x')
+ in (q obj, r, h)
+ ) else unit_dpm false
+ in fun one_dpm -> unit_set (bind_dpm one_dpm eliminate_non_Qxs)
This is a function that takes a `bool dpm` as input and returns a `bool dpm set` as output.
- This is a bit different than the \[[Qx]] we had before:
+ (Compare to the \[[Qx]] we had before:
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
+ 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)
- 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 returning any wrapped `false`s).
+ 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 compose this with a `bool dpm set` we already have on hand:
<pre><code>u >>=<sub>set</sub> \[[Qx]]
</code></pre>
-* Can you figure out how to handle \[[∃x]] on your own? If not, here are some [more hints](/hints/assignment_7_hint_5).
+* Can you figure out how to handle \[[∃x]] on your own? If not, here are some [more hints](/hints/assignment_7_hint_5). But try to get as far as you can on your own.
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
- (* next we store d at h[newindex], which is at the very end of h *)
+ let new_index = List.length h
+ (* next we store d at h[new_index], which is at the very end of h *)
(* the following line achieves that in a simple but inefficient way *)
in let h' = List.append h [d]
- (* next we assign 'x' to location newindex *)
- in let r' = fun v ->
- if v = var_to_bind then newindex else r v
+ (* next we assign 'x' to location new_index *)
+ in let r' = fun var ->
+ if var = var_to_bind then new_index else r var
(* the reason for returning true as an initial element should now be apparent *)
- in (true, r',h')
+ in (true, r', h')
What's going on in this representation of `u` updated with \[[∃x]]? For each `bool dpm` in `u` that wraps a `true`, we collect `dpm`s that are the result of 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. For `bool dpm`s in `u` that wrap `false`, we just discard them. We could if we wanted instead return `unit_set (unit_dpm false)`.
<pre><code>bind_set (bind_set u \[[∃x]]) \[[Px]]
</code></pre>
-* Can you figure out how to handle \[[not φ]] on your own? If not, here are some [more hints](/hints/assignment_7_hint_6).
+* Let's compare this to what \[[∃xPx]] would look like on a non-dynamic semantics, for example, where we use a simple reader monad to implement variable binding. Reminding ourselves, we'd be working in a framework like this. (Here we implement environments or assignments as functions from variables to entities, instead of as lists of pairs of variables and entities. An assignment `r` here is what `fun c -> List.assoc c r` would have been in [week6](
+/reader_monad_for_variable_binding).)
+
+ type assignment = char -> entity;;
+ type 'a reader = assignment -> 'a;;
+
+ let unit_reader (x : 'a) = fun r -> x;;
+
+ let bind_reader (u : 'a reader) (f : 'a -> 'b reader) =
+ fun r ->
+ let a = u r
+ in let u' = f a
+ in u' r;;
+
+ let getx = fun r -> r 'x';;
+
+ let lift (predicate : entity -> bool) =
+ fun entity_reader ->
+ fun r ->
+ let obj = entity_reader r
+ in unit_reader (predicate obj)
+
+ `lift predicate` converts a function of type `entity -> bool` into one of type `entity reader -> bool reader`. The meaning of \[[Qx]] would then be:
+
+ <pre><code>\[[Q]] ≡ lift q
+ \[[x]] & equiv; getx
+ \[[Qx]] ≡ \[[Q]] \[[x]] ≡
+ fun r ->
+ let obj = getx r
+ in unit_reader (q obj)
+ </code></pre>
+
+ Recall also how we defined \[[lambda x]], or as [we called it before](/reader_monad_for_variable_binding), \\[[who(x)]]:
+
+ let shift (var_to_bind : char) entity_reader (v : 'a reader) =
+ fun (r : assignment) ->
+ let new_value = entity_reader r
+ (* remember here we're implementing assignments as functions rather than as lists of pairs *)
+ in let r' = fun var -> if var = var_to_bind then new_value else r var
+ in v r'
+
+ 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) : bool reader ->
+ fun r -> exists (fun (obj : entity) -> lifted_predicate (unit_reader obj) r)
+
+ That would be the meaning of \[[∃]], which we'd use like this:
+
+ <pre><code>\[[∃]] \[[Q]]
+ </code></pre>
+
+ or this:
+
+ <pre><code>\[[∃]] ( \[[lambda x]] \[[Qx]] )
+ </code></pre>
+
+ If we wanted to compose \[[∃]] with \[[lambda x]], we'd get:
+
+ let shift var_to_bind entity_reader v =
+ fun r ->
+ let new_value = entity_reader r
+ in let r' = fun var -> if var = var_to_bind then new_value else r var
+ in v r'
+ in let lifted_exists =
+ fun lifted_predicate ->
+ fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
+ in fun bool_reader -> lifted_exists (shift 'x' getx bool_reader)
+
+ which we can simplify to:
+
+ let shifted v =
+ fun r ->
+ let new_value = r 'x'
+ in let r' = fun var -> if var = 'x' then new_value else r var
+ in v r'
+ in let lifted_exists =
+ fun lifted_predicate ->
+ fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
+ in fun bool_reader -> lifted_exists (shifted bool_reader)
+
+ and simplifying further:
+
+ fun bool_reader ->
+ let shifted v =
+ fun r ->
+ let new_value = r 'x'
+ in let r' = fun var -> if var = 'x' then new_value else r var
+ in v r'
+ let lifted_predicate = shifted bool_reader
+ in fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
+
+ fun bool_reader ->
+ let lifted_predicate = fun r ->
+ let new_value = r 'x'
+ in let r' = fun var -> if var = 'x' then new_value else r var
+ in bool_reader r'
+ in fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
+
+
+
+
+
+
+
+* Can you figure out how to handle \[[not φ]] on your own? If not, here are some [more hints](/hints/assignment_7_hint_6). But try to get as far as you can on your own.