X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=hints%2Fassignment_7_hint_3.mdwn;h=4aa9180f823fce57b67cba3188915bffa82f2eea;hb=5e8eadce75352b7c2ec2ad78c8c92b89bd6ee778;hp=d3e06c530d82e60857081f56ee93c951bb39e1a9;hpb=8fb69b5fc5ded83a0b3adfef69c01f259f8432ab;p=lambda.git
diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn
index d3e06c53..4aa9180f 100644
--- a/hints/assignment_7_hint_3.mdwn
+++ b/hints/assignment_7_hint_3.mdwn
@@ -3,21 +3,23 @@
Now some of the `dpm`s we work with will be `bool dpm`s, which are functions from discourse possibilities to `bool`s (and discourse possibilities). It's tempting to think we might just work with `bool dpm`s instead of sets of possibilities. However, I don't think this can work. The reason why is that at a crucial point in GS&Vs semantics, we have to work with not just a *single* way of mutating or "extending" a discourse possibility, but a *range* of different ways to mutate the live discourse possibilities. So we do need to work with sets, after all.
- A set is just another monadic layer. We've already talked about list monads, and we can for these purposes just use list monads to represent set monads. Instead of sets of possibilities, we'll be working with sets of `dpm`s, that is, sets of discourse possibility monads, or computations on discourse possibilities.
+ A set is just another monadic layer. We've already talked about list monads, and we can for these purposes just use list monads to represent set monads. Instead of sets of possibilities, let's work with sets of `dpm`s, that is, sets of discourse possibility monads, or computations on discourse possibilities.
As I said, for simplicity, we'll represent sets using lists:
type 'a set = 'a list;;
let empty_set : 'a set = [];;
- let unit_set (x: 'a) : 'a set = [x];;
- let bind_set (u: 'a set) (f: 'a -> 'b set) =
+ let unit_set (value: 'a) : 'a set = [value];;
+ let bind_set (u: 'a set) (f: 'a -> 'b set) : '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.
-* In def 2.5, GS&V say the denotation of an e-type constant α
wrt a discourse possibility `(r, h, w)` is whatever entity the world `w` associates with α
. 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.
+* In def 2.5, GS&V say the denotation of an e-type constant α
wrt a discourse possibility `(r, h, w)` is whatever entity the world `w` associates with α
. Since we don't have worlds, this will just be an entity. (Hence, we're not representing any of the interesting phenomena about epistemic non-rigidity discussed in GS&V pp. 32ff.)
+
+ GS&V 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.
They say the denotation of a variable is the entity 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')`.
@@ -25,24 +27,29 @@
> \[[expression]] in possibility `(r, h, w)`
- we'll just talk about \[[expression]] and let that be a monadic value, implemented in part by a function that takes `(r, h)` as an argument.
+ we'll just talk about \[[expression]] and let that be a monadic operation, implemented in part by a function that takes `(r, h)` as an argument.
+
+ In particular, the meaning of sentential clauses will be an operation that we monadically bind to an existing `bool dpm set`. Here is its type:
- More specifically, \[[expression]] will be a set of `'a dpm`s, where `'a` is the appropriate type for *expression*. An `'a dpm` is implemented by a function that takes `(r, h)` as an argument.
+ type clause = bool dpm -> bool dpm set;;
* 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 (i) allocating a new location in the store, (ii) putting some entity `d` from the domain in that location, and (iii) assigning variable `x` to that location in the store.
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 newindex = List.length h
- (* next we store d at h[newindex], which is at the very end of h *)
- (* the following line achieves that in a simple but very inefficient way *)
- in let h' = List.append h [d]
- (* next we assign 'x' to location newindex *)
- in let r' = fun v ->
- if v = var_to_bind then newindex else r v
- in (r',h')
-
-* Is that enough? If not, here are some [more hints](/hints/assignment_7_hint_4).
+ (* we want to return a function that we can bind to a bool dpm *)
+ 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');;
+
+* 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.