From: Jim Pryor Date: Sat, 20 Nov 2010 04:28:08 +0000 (-0500) Subject: assignment7 tweaks X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=85784b8965db9b0daf0c03f043bc68bd9b41a18c assignment7 tweaks Signed-off-by: Jim Pryor --- diff --git a/hints/assignment_7_hint_4.mdwn b/hints/assignment_7_hint_4.mdwn index 253ee96f..cef57737 100644 --- a/hints/assignment_7_hint_4.mdwn +++ b/hints/assignment_7_hint_4.mdwn @@ -1,9 +1,9 @@ * 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 most natural to break \[[∃xPx]] into two pieces, \[[∃x]] and \[[Px]]. But first we need to get clear on expressions like \[[Qx]]. -* GS&V say that the effect of updating an information state `s` with the meaning of "Qx" should be to eliminate possibilities in which the entity associated with the peg associated with the variable `x` does not have the property Q. In other words, if we let `q` be the function from entities to `bool`s that gives the extension of "Q", then `s` updated with \[[Qx]] should be `s` filtered by the function `fun (r, h) -> let obj = List.nth h (r 'x') in q obj`. When `... q obj` evaluates to `true`, that `(r, h)` pair is retained, else it is discarded. +* GS&V say that the effect of updating an information state `s` with the meaning of "Qx" should be to eliminate possibilities in which the entity associated with the peg associated with the variable `x` does not have the property Q. In other words, if we let `q` be the function from entities to `bool`s that gives the extension of Q, then `s` updated with \[[Qx]] should be `s` filtered by the function `fun (r, h) -> let obj = List.nth h (r 'x') in q obj`. When `... q obj` evaluates to `true`, that `(r, h)` pair is retained, else it is discarded. - OK, we face two questions then. First, how do we carry this over to our present framework, where we're working with sets of `dpm`s instead of sets of discourse possibilities? And second, how do we decompose the behavior here ascribed to \[[Qx]] into some meaning for "Q" and a different meaning for "x"? + OK, we face two questions then. First, how do we carry this over to our present framework, where we're working with sets of `dpm`s instead of sets of discourse possibilities? And second, how do we decompose the behavior here attributed to \[[Qx]] into some meaning for "Q" and a different meaning for "x"? * Answering the first question: we assume we've got some `bool dpm set` to start with. I won't call this `s` because that's what GS&V use for sets of discourse possibilities, and we don't want to confuse discourse possibilities with `dpm`s. Instead I'll call it `u`. Now what we want to do with `u` is to map each `dpm` it gives us to one that results in `(true, r, h)` only when the entity that `r` and `h` associate with variable `x` has the property Q. As above, I'll assume Q's extension is given by a function `q` from entities to `bool`s. @@ -28,7 +28,7 @@ u >>= \[[Qx]] -* Now our second question: how do we decompose the behavior here ascribed to \[[Qx]] into some meaning for "Q" and a different meaning for "x"? +* Now our second question: how do we decompose the behavior here attributed to \[[Qx]] into some meaning for "Q" and a different meaning for "x"? Well, we already know that \[[x]] will be a kind of computation that takes an assignment function `r` and store `h` as input. It will look up the entity that those two together associate with the variable `x`. So we can treat \[[x]] as an `entity dpm`. We don't worry here about sets of `dpm`s; we'll leave that to our predicates to interface with. We'll just make \[[x]] be a single `entity dpm`. So what we want is: @@ -138,7 +138,7 @@ Can you persuade yourself that these are equivalent?) -* Reviewing: now we've determined how to define \[[Q]] and \[[x]] such that \[[Qx]] can be the result of applying the function \[[Q]] to the `entity dpm` \[[x]]. And \[[Qx]] in turn is now a function that takes a `bool dpm` as input and returns a `bool dpm set` as output. We compose this with a `bool dpm set` we already have on hand: +* Reviewing: now we've determined how to define \[[Q]] and \[[x]] such that \[[Qx]] can be the result of applying the function \[[Q]] to the `entity dpm` \[[x]]. And \[[Qx]] in turn is now a function that takes a `bool dpm` as input and returns a `bool dpm set` as output. We monadically bind this operaration to whatever `bool dpm set` we already have on hand: bind_set u \[[Qx]] diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn index 882a6232..a0ac32a3 100644 --- a/hints/assignment_7_hint_5.mdwn +++ b/hints/assignment_7_hint_5.mdwn @@ -39,7 +39,7 @@ What's going on in this representation of `u` updated with \[[∃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 according to which the entity `d` we did that with doesn't have property P. + A later step can then filter out all the `dpm`s where the entity `d` we did that with doesn't have property P. So if we just call the function `extend_one` defined above \[[∃x]], then `u` updated with \[[∃x]] updated with \[[Px]] is just: @@ -97,7 +97,8 @@ 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 : entity reader -> bool reader) -> - fun r -> exists (fun (obj : entity) -> lifted_predicate (unit_reader obj) r) + fun r -> exists (fun (obj : entity) -> + lifted_predicate (unit_reader obj) r) That would be the meaning of \[[∃]], which we'd use like this: @@ -163,7 +164,7 @@ This gives us a value for \[[∃x]], which we use like this: - 
\[[∃x]]reader ( \[[Qx]] )
+	
\[[∃x]] ( \[[Qx]] )
 	

 
 	Contrast the way we use \[[∃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:
@@ -171,9 +172,9 @@
 	
u >>= \[[∃x]] >>= \[[Qx]]
 	

 
-	The crucial difference in GS&V's system is that the distinctive effect of the \[[∃x]]---to allocate new pegs in the store and associate variable `x` with the objects stored there---doesn't last only while interpreting clauses supplied as arguments to \[[∃x]]. Instead, it persists through the discourse, possibly affecting the interpretation of claims outside the logical scope of the quantifier. This is how we're able to interpret claims like:
+	The crucial difference in GS&V's system is that the distinctive effect of the \[[∃x]]---to allocate new pegs in the store and associate variable `x` with the objects stored there---doesn't last only while interpreting clauses supplied as arguments to \[[∃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 ∃y (farmer y and ∃x y owns x) then (y beats x).
+	>	If ∃x (man x and ∃y y is wife of x) then (x kisses y).
 
 
 *	Can you figure out how to handle \[[not φ]] 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.
diff --git a/hints/assignment_7_hint_6.mdwn b/hints/assignment_7_hint_6.mdwn
index ed3828b7..0859706b 100644
--- a/hints/assignment_7_hint_6.mdwn
+++ b/hints/assignment_7_hint_6.mdwn
@@ -116,10 +116,10 @@
 		let antecedent = fun one_dpm -> exists 'x' one_dpm >>= lift_predicate male getx >>= exists 'y' >>= lift_predicate2 wife_of getx gety;;
 		
 		(* "if a man x has a wife y, x kisses y" *)
-		run (initial_set >>= if_op antecedent lift_predicate2 kisses getx gety);;
+		run (initial_set >>= if_op antecedent (lift_predicate2 kisses getx gety));;
 		(* Bob has wife Carol, and kisses her; and Ted has wife Alice and kisses her; so this is true! *)
 
 		(* "if a man x has a wife y, x misses y" *)
-		run (initial_set >>= if_op antecedent lift_predicate2 misses getx gety);;
+		run (initial_set >>= if_op antecedent (lift_predicate2 misses getx gety));;
 		(* Bob has wife Carol, and misses her; but Ted misses only Carol, not his wife Alice; so this is false! *)