assignment7 tweaks
authorJim Pryor <profjim@jimpryor.net>
Thu, 18 Nov 2010 23:40:49 +0000 (18:40 -0500)
committerJim Pryor <profjim@jimpryor.net>
Thu, 18 Nov 2010 23:40:49 +0000 (18:40 -0500)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
hints/assignment_7_hint_1.mdwn
hints/assignment_7_hint_2.mdwn
hints/assignment_7_hint_3.mdwn

index effe6ba..6d6b760 100644 (file)
@@ -7,9 +7,9 @@
 
 *      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 v -> if v = 'x' then n else g v`.
 
-*      Their function `g`, which assigns objects from the domain to pegs, corresponds to our store function, which assigns entities to indexes.
+*      Their function `g`, which assigns objects 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 "an extension.") At one point in the paper, it emerges that what they mean is what I'd call a *proper extension*: an extension which isn't identical to the original.
+*      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.") At one point in the paper, it emerges that what they mean is what I'd call a *proper extension*: an extension which isn't identical to the original.
 
 *      [More hints](/hints/assignment_7_hint_2).
 
 
 *      [More hints](/hints/assignment_7_hint_2).
 
index 0b1c59f..6047aeb 100644 (file)
@@ -32,7 +32,7 @@
                bind_set u (fun a -> if test a then unit_set a else empty_set)
 
 
                bind_set u (fun a -> if test a then unit_set a else empty_set)
 
 
-*      So GS&V's information states, which they notate using `s`, are set-monads, whose elements in turn are discourse possibilities, which they notate using `i`, which are state monads that keep track of which entities have been introduced as objects of discourse, and which variables are bound to them, in the discourse possibility in question. In GS&V's system, possibilities are triples of an assignment function, `r`, a store `g`, and a world `w`. We're leaving the worlds out. Also, instead of just working with pairs `(r, g)`, we're working with state monads for which those pairs constitute the states we update.
+*      So GS&V's information states, which they notate using `s`, are set-monads, whose elements in turn are discourse possibilities, which they notate using `i`, which are state monads that keep track of which entities have been introduced as objects of discourse, and which variables are bound to them, in the discourse possibility in question. In GS&V's system, possibilities are triples of an assignment function, `r`, a store `h`, and a world `w`. We're leaving the worlds out. Also, instead of just working with pairs `(r, h)`, we're working with state monads for which those pairs constitute the states we update.
 
 
 *      [More hints](/hints/assignment_7_hint_3).
 
 
 *      [More hints](/hints/assignment_7_hint_3).
index 4951100..842d90e 100644 (file)
@@ -1,34 +1,34 @@
 
 
-*      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.
+*      In def 2.5, they say the denotation of an e-type constant <code>&alpha;</code> wrt a discourse possibility `(r, h, w)` is whatever object the world `w` associates with <code>&alpha;</code>. Since we don't have worlds, this will just be an object.
 
 *      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']]`. In our OCaml implementation, that will be `List.nth g (r 'x')`.
+*      They say the denotation of a variable is the object 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
 
 
 We're going to keep all of that, except dropping the worlds. And instead of talking about
 
->      \[[expression]] in possibility `(r, g, w)`
+>      \[[expression]] in possibility `(r, h, w)`
 
 
-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.
+we'll just talk about \[[expression]] and let that be a monadic object, implemented in part by a function that takes `(r, h)` 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.
+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, h)` is the state that gets updated. Those are implemented as functions from `(r, h)` to `(a, r', h')`, where `a` is a value of type `'a`, and `r', h'` are possibly altered assignment functions and stores.
 
 *      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) =
 
 *      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 *)
+                       fun ((r, h) : assignment * store) ->
+                               let newindex = List.length h
+                               (* first we store d at index newindex in h, which is at the very end *)
                                (* the following line achieves that in a simple but very inefficient way *)
                                (* the following line achieves that in a simple but very inefficient way *)
-                               in let g' = List.append g [d]
+                               in let h' = List.append h [d]
                                (* 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
-                               in (r',g')
+                               in (r',h')
 
 *      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.
 
 
 *      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.
+       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, 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.
 
        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:
 
@@ -36,9 +36,9 @@ More specifically, \[[expression]] will be a set of `'a discourse_possibility` m
 
        Hence, updating `s` with \[[Qx]] should be:
 
 
        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)
+               bind_set s (fun (r, h) -> if (let obj = List.nth h (r 'x') in Q obj) then unit_set (r, h) else empty_set)
 
 
-       We can call the `(fun (r, g) -> ...)` part \[[Qx]] and then updating `s` with \[[Qx]] will be:
+       We can call the `(fun (r, h) -> ...)` part \[[Qx]] and then updating `s` with \[[Qx]] will be:
 
                bind_set s \[[Qx]]
 
 
                bind_set s \[[Qx]]
 
@@ -62,14 +62,14 @@ More specifically, \[[expression]] will be a set of `'a discourse_possibility` m
        Deferring the "property P" part, this says:
 
        <pre><code>s updated with \[[&exist;x]] &equiv;
        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)
+               s >>= (fun (r, h) -> List.map (fun d -> newpeg_and_bind 'x' d) domain)
        </code></pre>
        
        </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.
+       That is, for each pair `(r, h)` in `s`, we collect the result of extending `(r, h)` 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.
 
 
        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:
+       So if we just call the function `(fun (r, h) -> ...)` above \[[&exist;x]], then `s` updated with \[[&exist;x]] updated with \[[Px]] is just:
 
        <pre><code>s >>= \[[&exist;x]] >>= \[[Px]]
        </code></pre>
 
        <pre><code>s >>= \[[&exist;x]] >>= \[[Px]]
        </code></pre>
@@ -87,8 +87,8 @@ More specifically, \[[expression]] will be a set of `'a discourse_possibility` m
 
        Here's how we can represent that:
 
 
        Here's how we can represent that:
 
-               <pre><code>bind_set s (fun (r, g) ->
-                       let u = unit_set (r, g)
+               <pre><code>bind_set s (fun (r, h) ->
+                       let u = unit_set (r, h)
                        in let descendents = u >>= \[[&phi;]]
                        in if descendents = empty_set then u else empty_set
                </code></pre>
                        in let descendents = u >>= \[[&phi;]]
                        in if descendents = empty_set then u else empty_set
                </code></pre>