assignment7 tweaks

[lambda.git] / hints / assignment_7_hint_3.mdwn

diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn
index 4a159e9..4951100 100644 (file)
--- a/hints/assignment_7_hint_3.mdwn
+++ b/hints/assignment_7_hint_3.mdwn
@@ -3,7 +3,7 @@
 
 *      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.
 
 
 *      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.
 

-*      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']]`.
+*      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']]`. In our OCaml implementation, that will be `List.nth g (r 'x')`.

 
 We're going to keep all of that, except dropping the worlds. And instead of talking about
 
 
 We're going to keep all of that, except dropping the worlds. And instead of talking about
 


@@ -24,12 +24,11 @@ More specifically, \[[expression]] will be a set of `'a discourse_possibility` m
                                (* next we assign 'x' to location newindex *)
                                in let r' = fun v ->
                                        if v = bound_variable then newindex else r v
                                (* 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 (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 \[[∃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.
+*      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]]  first.

 
 

-       They say that the effect of updating an information state `s` with the formula `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`.
+       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:
 
 
        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:
 


@@ -41,16 +40,57 @@ More specifically, \[[expression]] will be a set of `'a discourse_possibility` m
 
        We can call the `(fun (r, g) -> ...)` part \[[Qx]] and then updating `s` with \[[Qx]] will be:
 
 
        We can call the `(fun (r, g) -> ...)` part \[[Qx]] and then updating `s` with \[[Qx]] will be:
 

-               bind_set s [[Qx]]
+               bind_set s \[[Qx]]

 
        or as it's written using Haskell's infix notation for bind:
 
 
        or as it's written using Haskell's infix notation for bind:
 

-               s >>= [[Qx]]
+               s >>= \[[Qx]]

 
 *      Now 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 `s` with \[[∃xPx]] as:
 
 
 *      Now 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 `s` with \[[∃xPx]] as:
 

-               s >>= [[∃x]] >>= [[Px]]
+       <pre><code>s >>= \[[&exist;x]] >>= \[[Px]]
+       </code></pre>

 
 

+       What does \[[&exist;x]] need to be here? Here's what they say, on the top of p. 13:

 
 

+       >       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 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.
+
+       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>