From 1b40bc7e0915e247ecaa6ea9d583b26790c31a74 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Fri, 19 Nov 2010 18:47:07 -0500 Subject: [PATCH 1/1] assignment7 tweaks Signed-off-by: Jim Pryor --- hints/assignment_7_hint_1.mdwn | 4 +- hints/assignment_7_hint_2.mdwn | 2 +- hints/assignment_7_hint_3.mdwn | 14 ++--- hints/assignment_7_hint_4.mdwn | 79 +++++++++++++-------------- hints/assignment_7_hint_5.mdwn | 118 ++++++++++++++++++++++++++++++++++++++--- 5 files changed, 161 insertions(+), 56 deletions(-) diff --git a/hints/assignment_7_hint_1.mdwn b/hints/assignment_7_hint_1.mdwn index b6bff27c..ac15e19b 100644 --- a/hints/assignment_7_hint_1.mdwn +++ b/hints/assignment_7_hint_1.mdwn @@ -5,11 +5,11 @@ * 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. diff --git a/hints/assignment_7_hint_2.mdwn b/hints/assignment_7_hint_2.mdwn index 96e47410..02f3b158 100644 --- a/hints/assignment_7_hint_2.mdwn +++ b/hints/assignment_7_hint_2.mdwn @@ -30,5 +30,5 @@ * 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. diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn index 0914b79d..be018ded 100644 --- a/hints/assignment_7_hint_3.mdwn +++ b/hints/assignment_7_hint_3.mdwn @@ -33,15 +33,15 @@ It will be useful to have a shorthand way of referring to this operation: 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. diff --git a/hints/assignment_7_hint_4.mdwn b/hints/assignment_7_hint_4.mdwn index ae17ce1d..3e3961e5 100644 --- a/hints/assignment_7_hint_4.mdwn +++ b/hints/assignment_7_hint_4.mdwn @@ -1,11 +1,11 @@ * 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: @@ -13,7 +13,7 @@ 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)) @@ -36,13 +36,13 @@ 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. @@ -51,14 +51,12 @@ 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) -> @@ -67,9 +65,9 @@ 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: @@ -78,9 +76,9 @@ 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: @@ -89,53 +87,56 @@ 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: @@ -146,5 +147,5 @@ 
u >>=set \[[Qx]]
-* 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. diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn index 07cbd648..1b801d19 100644 --- a/hints/assignment_7_hint_5.mdwn +++ b/hints/assignment_7_hint_5.mdwn @@ -28,15 +28,15 @@ 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)`. @@ -53,4 +53,108 @@ entity `d` we did that with doesn't have property P. 
bind_set (bind_set u \[[∃x]]) \[[Px]]
-* 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: + + 
\[[Q]] ≡ lift q
+	\[[x]] & equiv; getx
+	\[[Qx]] ≡ \[[Q]] \[[x]] ≡
+		fun r ->
+			let obj = getx r
+			in unit_reader (q obj)
+
+ + 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: + + 
\[[∃]] \[[Q]]
+
+ + or this: + + 
\[[∃]] ( \[[lambda x]] \[[Qx]] )
+
+ + 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. -- 2.11.0