edits

[lambda.git] / hints / assignment_7_hint_5.mdwn

<!--
I would like to propose one pedegogical suggestion (due to Ken), which
is to separate peg addition from non-determinacy by explicitly adding
a "Let" construction to GSV's logic, i.e., "Let of var * term *
clause", whose interpretation adds a peg, assigns var to it, sets the
value to the value computed by term, and evaluates the clause with the
new peg in place.  This can be added easily, especially since you have
supplied a procedure that handles the main essence of the
construction.  Once the Let is in place, adding the existential is
purely dealing with nondeterminism.
-->

*       How shall we handle \[[&exist;x]]? As we said, GS&V really tell us how to interpret \[[&exist;xPx]], but for our purposes, what they say about this can be broken naturally into two pieces, such that we represent the update of our starting set `u` with \[[&exist;xPx]] as:

        <pre><code>u >>= \[[&exist;x]] >>= \[[Px]]
        </code></pre>

        (Extra credit: how does the discussion on pp. 25-29 of GS&V bear on the possibility of this simplification?)

        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 entity has the property P will be eliminated.

        We can defer that to a later step, where we do `... >>= \[[Px]]`. GS&V continue:
 
        >       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'` as there are entities `d` which in the possible world of `i` have the property P.

        Deferring the "property P" part, this corresponds to:

        <pre><code>u updated with \[[&exist;x]] &equiv;
                let extend one_dpm (d : entity) =
                        bind_dpm one_dpm (new_peg_and_assign 'x' d)
                in bind_set u (fun one_dpm -> List.map (fun d -> extend one_dpm d) domain)
        </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) : 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');;
        
        What's going on in this proposed representation of \[[&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 where the entity `d` we did that with doesn't have property P. (Again, consult GS&V pp. 25-9 for extra credit.)

        If we call the function `(fun one_dom -> List.map ...)` defined above \[[&exist;x]], then `u` updated with \[[&exist;x]] updated with \[[Px]] is just:

        <pre><code>u >>= \[[&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 u \[[&exist;x]]) \[[Px]]
        </code></pre>

*       Let's compare this to what \[[&exist;xPx]] would look like on a non-dynamic semantics, for example, where we use a simple reader monad to implement variable binding. Reminding ourselves, we'd be working in a framework like this. (Here we implement environments or assignments as functions from variables to entities, instead of as lists of pairs of variables and entities. An assignment `r` here is what `fun c -> List.assoc c r` would have been in [week7](
/reader_monad_for_variable_binding).)
 
                type assignment = char -> entity;;
                type 'a reader = assignment -> 'a;;

                let unit_reader (value : 'a) : 'a reader = fun r -> value;;

                let bind_reader (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
                        fun r ->
                                let a = u r
                                in let u' = f a
                                in u' r;;

        Here the type of a sentential clause is:

                type clause = bool reader;;

        Here are meanings for singular terms and predicates:

                let getx : entity reader = fun r -> r 'x';;

                type lifted_unary = entity reader -> bool reader;;

                let lift (predicate : entity -> bool) : lifted_unary =
                        fun entity_reader ->
                                fun r ->
                                        let obj = entity_reader r
                                        in unit_reader (predicate obj)

        The meaning of \[[Qx]] would then be:

        <pre><code>\[[Q]] &equiv; lift q
        \[[x]] &equiv; getx
        \[[Qx]] &equiv; \[[Q]] \[[x]] &equiv;
                fun r ->
                        let obj = getx r
                        in unit_reader (q obj)
        </code></pre>

        Recall also how we defined \[[lambda x]], or as [we called it before](/reader_monad_for_variable_binding), \\[[who(x)]]:

                let shift (var_to_bind : char) (clause : clause) : lifted_unary =
                        fun entity_reader ->
                                fun r ->
                                        let new_value = entity_reader r
                                        (* remember here we're implementing assignments as functions rather than as lists of pairs *)
                                        in let r' = fun var -> if var = var_to_bind then new_value else r var
                                        in clause r'

        Now, how would we implement quantifiers in this setting? I'll assume we have a function `exists` of type `(entity -> bool) -> bool`. That is, it accepts a predicate as argument and returns `true` if any element in the domain satisfies that predicate. We could implement the reader-monad version of that like this:

                fun (lifted_predicate : lifted_unary) ->
                        fun r -> exists (fun (obj : entity) ->
                                lifted_predicate (unit_reader obj) r)
                        
        That would be the meaning of \[[&exist;]], which we'd use like this:

        <pre><code>\[[&exist;]] ( \[[Q]] )
        </code></pre>

        or this:

        <pre><code>\[[&exist;]] ( \[[lambda x]] \[[Qx]] )
        </code></pre>

        If we wanted to compose \[[&exist;]] with \[[lambda x]], we'd get:

                let shift var_to_bind clause =
                        fun entity_reader r ->
                                let new_value = entity_reader r
                                in let r' = fun var -> if var = var_to_bind then new_value else r var
                                in clause r'
                in let lifted_exists =
                        fun lifted_predicate ->
                                fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
                in fun bool_reader -> lifted_exists (shift 'x' bool_reader)

        which we can simplify to:

        <!--
                let shifted clause =
                        fun entity_reader r ->
                                let new_value = entity_reader r
                                in let r' = fun var -> if var = 'x' then new_value else r var
                                in clause r'
                in let lifted_exists =
                        fun lifted_predicate ->
                                fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
                in fun bool_reader -> lifted_exists (shifted bool_reader)

                fun bool_reader ->
                        let shifted' =
                                fun entity_reader r ->
                                        let new_value = entity_reader r
                                        in let r' = fun var -> if var = 'x' then new_value else r var
                                        in bool_reader r'
                        in fun r -> exists (fun obj -> shifted' (unit_reader obj) r)

                fun bool_reader ->
                        let shifted'' r obj =
                                        let new_value = (unit_reader obj) r
                                        in let r' = fun var -> if var = 'x' then new_value else r var
                                        in bool_reader r'
                        in fun r -> exists (fun obj -> shifted'' r obj)

                fun bool_reader ->
                        let shifted'' r obj =
                                        let new_value = obj
                                        in let r' = fun var -> if var = 'x' then new_value else r var
                                        in bool_reader r'
                        in fun r -> exists (shifted'' r)
        -->

                fun bool_reader ->
                        let shifted r new_value =
                                        let r' = fun var -> if var = 'x' then new_value else r var
                                        in bool_reader r'
                        in fun r -> exists (shifted r)

        This gives us a value for \[[&exist;x]], which we use like this:

        <pre><code>\[[&exist;x]] ( \[[Qx]] )
        </code></pre>

        Contrast the way we use \[[&exist;x]] in GS&V's system. Here we don't have a function that takes \[[Qx]] as an argument. Instead we have a operation that gets bound in a discourse chain:

        <pre><code>u >>= \[[&exist;x]] >>= \[[Qx]]
        </code></pre>

        The crucial difference in GS&V's system is that the distinctive effect of the \[[&exist;x]]---to allocate new pegs in the store and associate variable `x` with the objects stored there---doesn't last only while interpreting some clauses supplied as arguments to \[[&exist;x]]. Instead, it persists through the discourse, possibly affecting the interpretation of claims outside the logical scope of the quantifier. This is how we'll able to interpret claims like:

        >       If &exist;x (man x and &exist;y y is wife of x) then (x kisses y).

        See the discussion on pp. 24-5 of GS&V.


*       Can you figure out how to handle \[[not &phi;]] and the other connectives? If not, here are some [more hints](/hints/assignment_7_hint_6). But try to get as far as you can on your own.