X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=hints%2Fassignment_7_hint_3.mdwn;h=4aa9180f823fce57b67cba3188915bffa82f2eea;hp=be018dede8da5794f671a64e938faaaec1409115;hb=193823d816ee0b6ed88532df8ab2d9f43f66daca;hpb=1b40bc7e0915e247ecaa6ea9d583b26790c31a74
diff --git a/hints/assignment_7_hint_3.mdwn b/hints/assignment_7_hint_3.mdwn
index be018ded..4aa9180f 100644
--- a/hints/assignment_7_hint_3.mdwn
+++ b/hints/assignment_7_hint_3.mdwn
@@ -9,15 +9,17 @@
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, or a function from entities to `bool`s.
+* 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,23 +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:
+
+ 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 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 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.