From: Jim Pryor Date: Fri, 19 Nov 2010 14:25:16 +0000 (-0500) Subject: assignment7 tweaks X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=679852d7a5f67d6da3443b959acb1a41f3558c85 assignment7 tweaks Signed-off-by: Jim Pryor --- diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn index 591fd31d..07cbd648 100644 --- a/hints/assignment_7_hint_5.mdwn +++ b/hints/assignment_7_hint_5.mdwn @@ -1,5 +1,5 @@ -* How shall we handle \[[∃x]]. As we said, GS&V really tell us how to interpret \[[∃xPx]], but what they say about this breaks naturally into two pieces, such that we can represent the update of our starting set `u` with \[[∃xPx]] as: +* How shall we handle \[[∃x]]? As we said, GS&V really tell us how to interpret \[[∃xPx]], but what they say about this breaks naturally into two pieces, such that we can represent the update of our starting set `u` with \[[∃xPx]] as: 
u >>=set \[[∃x]] >>=set \[[Px]]
@@ -38,7 +38,7 @@ (* the reason for returning true as an initial element should now be apparent *) in (true, r',h') - What's going on here? For each `bool dpm` in `u` that wraps a `true`, we collect `dpm`s that are the result of 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. For `bool dpm`s in `u` that wrap `false`, we just discard them. We could if we wanted instead return `unit_set (unit_dpm false)`. + What's going on in this representation of `u` updated with \[[∃x]]? For each `bool dpm` in `u` that wraps a `true`, we collect `dpm`s that are the result of 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. For `bool dpm`s in `u` that wrap `false`, we just discard them. We could if we wanted instead return `unit_set (unit_dpm false)`. 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.