-* In def 2.5, they say the denotation of an e-type constant <code>α</code> wrt a discourse possibility `(r, g, w)` is whatever object the world `w` associates with <code>α</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 (value: 'a) : 'a set = [value];;
+ let bind_set (u: 'a set) (f: 'a -> 'b set) : '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.
-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.
+* 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.
-* 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:
- 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
- (* the reason for returning a triple with () in first position will emerge *)
- in ((), r',g')
+* In def 2.5, GS&V say the denotation of an e-type constant <code>α</code> wrt a discourse possibility `(r, h, w)` is whatever entity the world `w` associates with <code>α</code>. Since we don't have worlds, this will just be an entity.
-* 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 easiest for us to break \[[∃xPx]] into two pieces, \[[∃x]] and \[[Px]]. Let's consider expressions like \[[Px]] (or \[[Qx]]) first.
+ 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.
+ 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')`.
+
+* We're going to keep all of that, except dropping the worlds. And instead of talking about:
+
+ > \[[expression]] in possibility `(r, h, w)`
+
+ we'll just talk about \[[expression]] and let that be a monadic operation, implemented in part by a function that takes `(r, h)` as an argument.
+
+ In particular, the meaning of sentential clauses will be an operation that we monadically bind to an existing `bool dpm set`. Here is its type:
+
+ type clause = bool dpm -> bool dpm set;;
+
+* 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:
+
+ (* we want to return a function that we can bind to a bool dpm *)
+ let new_peg_and_assign (var_to_bind : char) (d : entity) : bool -> bool dpm =
+ fun truth_value ->
+ fun (r, h) ->
+ (* first we calculate an unused index *)
+ 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 new_index *)
+ 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');;
+
+* 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.