From: Jim Pryor Date: Thu, 18 Nov 2010 19:09:31 +0000 (-0500) Subject: assignment7 tweaks X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=00fb05d9ee37681282813893ee69ed7441fe1273;ds=sidebyside assignment7 tweaks Signed-off-by: Jim Pryor --- diff --git a/hints/assignment_7_hint_1.mdwn b/hints/assignment_7_hint_1.mdwn index f7d5d288..6725def2 100644 --- a/hints/assignment_7_hint_1.mdwn +++ b/hints/assignment_7_hint_1.mdwn @@ -9,5 +9,7 @@ * Their function `g`, which assigns objects from the domain to pegs, corresponds to our store function, which assigns entities to indexes. +* 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. + * [More hints](/hints/assignment_7_hint_2). diff --git a/hints/assignment_7_hint_2.mdwn b/hints/assignment_7_hint_2.mdwn index 3d08c135..07d6a7ce 100644 --- a/hints/assignment_7_hint_2.mdwn +++ b/hints/assignment_7_hint_2.mdwn @@ -24,6 +24,11 @@ let bind_set (u: 'a set) (f: 'a -> 'b set) = List.concat (List.map f u);; +The following will be useful later: persuade yourself 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) + + * 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. diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn index 139597f9..c678e80b 100644 --- a/hints/assignment_7_hint_3.mdwn +++ b/hints/assignment_7_hint_3.mdwn @@ -1,2 +1,26 @@ +* In def 2.5, they say the denotation of an e-type constant α wrt a discourse possibility `(r, g, w)` is whatever object the world `w` associates with α. 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 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']]`. + +We're going to keep all of that, except dropping the worlds. And instead of talking about "\[[expression]] in discourse 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. + +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: + + let newpeg_and_bind (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 *) + in let r' = fun variable' -> + if variable' = variable then newindex else r variable' + (* the reason for returning a triple with () in first position will emerge *) + in ((), r',g') +