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 838a2af..61f48a7 100644 (file)
--- a/hints/assignment_7_hint_3.mdwn
+++ b/hints/assignment_7_hint_3.mdwn
@@ -7,26 +7,50 @@
 
 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 discourse possibility `(r, g, w)`
+>      \[[expression]] in possibility `(r, g, 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, 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.
+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.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:
 
 
 *      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 (variable : char) (d : entity) =
+               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 *)
                        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 variable' ->
-                                       if variable' = variable then newindex else r variable'
+                               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')
 
                                (* the reason for returning a triple with () in first position will emerge *)
                                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 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`.
+
+       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 \[[∃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]]
+
+