X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=hints%2Fassignment_7_hint_5.mdwn;h=07cbd648c5eba86e4919784bce57c24969fe1925;hp=591fd31d9421859776cb4220a92ecb8a3076f16e;hb=679852d7a5f67d6da3443b959acb1a41f3558c85;hpb=26574827b88c32f00baaf941c4eac1aaebac839d 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.