index ed6bc36..bbdea69 100644 (file)
@@ -1,96 +1,46 @@

-*      In def 2.5, they say the denotation of an e-type constant <code>&alpha;</code> wrt a discourse possibility `(r, g, w)` is whatever object the world `w` associates with <code>&alpha;</code>. Since we don't have worlds, this will just be an object.
+*      You will notice that GS&V don't just work with discourse possibilities (or more broadly, epistemic possibilities), they work with what they call "information states," which are *sets* of possibilities.

-*      They say the denotation of a predicate is whatever extension the world `w` associates with the predicate. Since we don't have worlds, this will just be an extension.
+       Now some of the `dpm`s we work with will be `bool dpm`s, which are functions from discourse possibilities to `bool`s (and discourse possibilities). It's tempting to think we might just work with `bool dpm`s instead of sets of possibilities. However, I don't think this can work. The reason why is that at a crucial point in GS&Vs semantics, we have to work with not just a *single* way of mutating or "extending" a discourse possibility, but a *range* of different ways to mutate the live discourse possibilities. So we do need to work with sets, after all.

-*      They say the denotation of a variable is the object which the store `g` 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, g, w)` is `g[r['x']]`.
+       A set is just another monadic layer. We've already talked about list monads, and we can for these purposes just use list monads to represent set monads. Instead of sets of possibilities, let's work with sets of `dpm`s, that is, sets of discourse possibility monads, or computations on discourse possibilities.

-We're going to keep all of that, except dropping the worlds. And instead of talking about
+       As I said, for simplicity, we'll represent sets using lists:

->      \[[expression]] in possibility `(r, g, w)`
+               type 'a set = 'a list;;
+               let empty_set : 'a set = [];;
+               let unit_set (x: 'a) : 'a set = [x];;
+               let bind_set (u: 'a set) (f: 'a -> 'b set) =
+                       List.concat (List.map f u);;

-we'll just talk about \[[expression]] and let that be a monadic object, implemented in part by a function that takes `(r, g)` as an argument.
+*      Reviewing: GS&V's "information states," which they notate using `s`, are sets of what they call "possibilities," and notate using `i`. Instead of sets of possibilities, which get updated to sets of other, "extended" possibilities, we'll work with sets of discourse possibility monads, which are functions from discourse possibilities to values and possibly "extended" discourse possibilities.

-More specifically, \[[expression]] will be a set of `'a discourse_possibility` monads, where `'a` is the appropriate type for *expression*, and the discourse possibility monads are themselves state monads where `(r, g)` is the state that gets updated. Those are implemented as functions from `(r, g)` to `(a, r', g')`, where `a` is a value of type `'a`, and `r', g'` are possibly altered assignment functions and stores.
+*      In def 2.5, GS&V say the denotation of an e-type constant <code>&alpha;</code> wrt a discourse possibility `(r, h, w)` is whatever entity the world `w` associates with <code>&alpha;</code>. Since we don't have worlds, this will just be an entity.

-*      In def 2.7, GS&V talk about an operation that takes an existing set of discourse possibilities, and extends each member in the set by allocating a new location in the store, and assigning a variable `'x'` to that location, which holds some object `d` from the domain. It will be useful to have a shorthand way of referring to this operation:
+       They say the denotation of a predicate is whatever extension the world `w` associates with the predicate. Since we don't have worlds, this will just be an extension, or a function from entities to `bool`s.

-               let newpeg_and_bind (bound_variable : char) (d : entity) =
-                       fun ((r, g) : assignment * store) ->
-                               let newindex = List.length g
-                               (* first we store d at index newindex in g, which is at the very end *)
-                               (* the following line achieves that in a simple but very inefficient way *)
-                               in let g' = List.append g [d]
-                               (* next we assign 'x' to location newindex *)
-                               in let r' = fun v ->
-                                       if v = bound_variable then newindex else r v
-                               in (r',g')
-
-*      At the top of p. 13 (this is in between defs 2.8 and 2.9), GS&V give two examples, one for \[[&exist;xPx]] and the other for \[[Qx]]. In fact it will be easiest for us to break \[[&exist;xPx]] into two pieces, \[[&exist;x]] and \[[Px]]. Let's consider expressions like \[[Px]]  first.
-
-       They say that the effect of updating an information state `s` with the meaning of "Qx" should be to eliminate possibilities in which the object 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 objects to `bool`s, `s` updated with \[[Qx]] should be `s` filtered by the function `fun (r, g) -> let obj = List.nth g (r 'x') in Q obj`. When `...Q obj` evaluates to `true`, that `(r, g)` pair is retained, else it is discarded.
-
-       Recall that [we said before](/hints/assignment_7_hint_2) that `List.filter (test : 'a -> bool) (u : 'a set) : 'a set` is the same as:
-
-               bind_set u (fun a -> if test a then unit_set a else empty_set)
-
-       Hence, updating `s` with \[[Qx]] should be:
-
-               bind_set s (fun (r, g) -> if (let obj = List.nth g (r 'x') in Q obj) then unit_set (r, g) else empty_set)
-
-       We can call the `(fun (r, g) -> ...)` part \[[Qx]] and then updating `s` with \[[Qx]] will be:
-
-               bind_set s \[[Qx]]
-
-       or as it's written using Haskell's infix notation for bind:
-
-               s >>= \[[Qx]]
-
-*      Now how shall we handle \[[&exist;x]]. As we said, GS&V really tell us how to interpret \[[&exist;xPx]], but what they say about this breaks naturally into two pieces, such that we can represent the update of `s` with \[[&exist;xPx]] as:
+       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')`.

-       <pre><code>s >>= \[[&exist;x]] >>= \[[Px]]
-       </code></pre>
+*      We're going to keep all of that, except dropping the worlds. And instead of talking about:

-       What does \[[&exist;x]] need to be here? Here's what they say, on the top of p. 13:
+       >       \[[expression]] in possibility `(r, h, w)`

-       >       Suppose an information state `s` is updated with the sentence &exist;xPx. Possibilities in `s` in which no object has the property P will be eliminated.
+       we'll just talk about \[[expression]] and let that be a monadic value, implemented in part by a function that takes `(r, h)` as an argument.

-       We can defer that to a later step, where we do `... >>= \[[Px]]`.
-       >       The referent system of the remaining possibilities will be extended with a new peg, which is associated with `x`. And for each old possibility `i` in `s`, there will be just as many extensions `i[x/d]` in the new state `s'` and there are objects `d` which in the possible world of `i` have the property P.
+*      In def 2.7, GS&V talk about an operation that takes an existing set of discourse possibilities, and *extends* each member in the set by (i) allocating a new location in the store, (ii) putting some entity `d` from the domain in that location, and (iii) assigning variable `x` to that location in the store.
+It will be useful to have a shorthand way of referring to this operation:

-       Deferring the "property P" part, this says:
-
-       <pre><code>s updated with \[[&exist;x]] &equiv;
-               s >>= (fun (r, g) -> List.map (fun d -> newpeg_and_bind 'x' d) domain)
-       </code></pre>
-
-       That is, for each pair `(r, g)` in `s`, we collect the result of extending `(r, g)` by allocating a new peg for object `d`, for each `d` in our whole domain of objects (here designated `domain`), and binding the variable `x` to the index of that peg.
-
-       A later step can then filter out all the possibilities in which the object `d` we did that with doesn't have property P.
-
-       So if we just call the function `(fun (r, g) -> ...)` above \[[&exist;x]], then `s` updated with \[[&exist;x]] updated with \[[Px]] is just:
-
-       <pre><code>s >>= \[[&exist;x]] >>= \[[Px]]
-       </code></pre>
-
-       or, being explicit about which "bind" operation we're representing here with `>>=`, that is:
-
-       <pre><code>bind_set (bind_set s \[[&exist;x]]) \[[Px]]
-       </code></pre>
-
-*      In def 3.1 on p. 14, GS&V define `s` updated with \[[not &phi;]] as:
-
-       >       { i &elem; s | i does not subsist in s[&phi;] }
-
-       where `i` *subsists* in <code>s[&phi;]</code> if there are any `i'` that *extend* `i` in <code>s[&phi;]</code>.
-
-       Here's how we can represent that:
-
-               <pre><code>bind_set s (fun (r, g) ->
-                       let u = unit_set (r, g)
-                       in let descendents = u >>= \[[&phi;]]
-                       in if descendents = empty_set then u else empty_set
-               </code></pre>
+               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 *)
+                               (* 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
+                               in (r',h')

+*      Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_4).