assignment7 tweaks

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn
index be018de..ad6d7ea 100644 (file)
--- a/hints/assignment_7_hint_3.mdwn
+++ b/hints/assignment_7_hint_3.mdwn
@@ -13,8 +13,10 @@
                let bind_set (u: 'a set) (f: 'a -> 'b set) =
                        List.concat (List.map f u);;
 
                let bind_set (u: 'a set) (f: 'a -> 'b set) =
                        List.concat (List.map f u);;
 

+

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


@@ -31,17 +33,19 @@
 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) =
 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 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
-                               (* the reason for returning true as an initial element will emerge later *)
-                               in (true, r', h')
+                       (* we want to return not a function that we can bind to a bool dpm *)
+                       fun (truth_value : bool) : bool dpm ->
+                               fun ((r, h) : assignment * store) ->
+                                       (* 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.
 
 
 *      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 3e3961e..5cf19d6 100644 (file)
--- 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]]. 
 
 
 *      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 the function from entities to `bool`s that gives the extension of "Q", then `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"?
 
 
        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. As above, I'll assume Q's extension is given by a function `q` from entities to `bool`s.

 
        Then what we want is something like this:
 
 
        Then what we want is something like this:
 


@@ -30,13 +30,13 @@
 
 *      Now our second question: how do we decompose the behavior here ascribed to \[[Qx]] into some meaning for "Q" and a different meaning for "x"?
 
 
 *      Now our second question: how do we decompose the behavior here ascribed to \[[Qx]] into some meaning for "Q" and a different meaning for "x"?
 

-       Well, we already know that \[[x]] will be a kind of computation that takes an assignment function `r` and store `h` as input. It will look up the entity that those two together associate with the variable `x`. So we can treat \[[x]] as an `entity dpm`. We don't worry here about sets of `dpm`s; we'll leave that to our predicates to interface with. We'll just make \[[x]] be a single `entity dpm`. Then what we want is:
+       Well, we already know that \[[x]] will be a kind of computation that takes an assignment function `r` and store `h` as input. It will look up the entity that those two together associate with the variable `x`. So we can treat \[[x]] as an `entity dpm`. We don't worry here about sets of `dpm`s; we'll leave that to our predicates to interface with. We'll just make \[[x]] be a single `entity dpm`. So what we want is:

 
                let getx = fun (r, h) ->
                        let obj = List.nth h (r 'x')
                        in (obj, r, h);;
 
 
                let getx = fun (r, h) ->
                        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))
 

diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn
index 1b801d1..1b2ee6a 100644 (file)
--- a/hints/assignment_7_hint_5.mdwn
+++ b/hints/assignment_7_hint_5.mdwn
@@ -15,33 +15,31 @@
        Deferring the "property P" part, this corresponds to:
 
        <pre><code>u updated with \[[&exist;x]] &equiv;
        Deferring the "property P" part, this corresponds to:
 
        <pre><code>u updated with \[[&exist;x]] &equiv;

-               let extend_one = fun one_dpm ->
-                       fun truth_value ->
-                               if truth_value = false
-                               then empty_set
-                               else List.map (fun d -> new_peg_and_assign 'x' d) domain
+               let extend_one = fun (one_dpm : bool dpm) ->
+                       List.map (fun d -> bind_dpm one_dpm (new_peg_and_assign 'x' d)) domain

                in bind_set u extend_one
        </code></pre>
 
        where `new_peg_and_assign` is the operation we defined in [hint 3](/hints/assignment_7_hint_3):
 
                let new_peg_and_assign (var_to_bind : char) (d : entity) =
                in bind_set u extend_one
        </code></pre>
 
        where `new_peg_and_assign` is the operation we defined in [hint 3](/hints/assignment_7_hint_3):
 
                let new_peg_and_assign (var_to_bind : char) (d : entity) =

-                       fun ((r, h) : assignment * store) ->
-                               (* 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
-                               (* the reason for returning true as an initial element should now be apparent *)
-                               in (true, r', h')
+                       (* we want to return not a function that we can bind to a bool dpm *)
+                       fun (truth_value : bool) : bool dpm ->
+                               fun ((r, h) : assignment * store) ->
+                                       (* 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')

        
        

-       What's going on in this representation of `u` updated with \[[&exist;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)`.
+       What's going on in this representation of `u` updated with \[[&exist;x]]? For each `bool dpm` in `u`, we collect `dpm`s that are the result of passing through their `bool`, but 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.

 
 

-       A later step can then filter out all the `dpm`s according to which the 
-entity `d` we did that with doesn't have property P.
+       A later step can then filter out all the `dpm`s according to which the entity `d` we did that with doesn't have property P.

 
        So if we just call the function `extend_one` defined above \[[&exist;x]], then `u` updated with \[[&exist;x]] updated with \[[Px]] is just:
 
 
        So if we just call the function `extend_one` defined above \[[&exist;x]], then `u` updated with \[[&exist;x]] updated with \[[Px]] is just:
 


@@ -152,9 +150,4 @@ entity `d` we did that with doesn't have property P.
                        in fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
 
 
                        in fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
 
 

-
-
-               
-       
-

 *      Can you figure out how to handle \[[not &phi;]] 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.
 *      Can you figure out how to handle \[[not &phi;]] 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.