X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=hints%2Fassignment_7_hint_6.mdwn;h=fd8f55d4ff6a160aea1b75693e22634993abe579;hp=a371b21c71280a29614f516895747a76fc4f0bba;hb=6f77f31cdd1687494ce1f52277e5486ff4293540;hpb=60fde0202775a36c5b20c370374649d2a90c6af8 diff --git a/hints/assignment_7_hint_6.mdwn b/hints/assignment_7_hint_6.mdwn index a371b21c..fd8f55d4 100644 --- a/hints/assignment_7_hint_6.mdwn +++ b/hints/assignment_7_hint_6.mdwn @@ -5,41 +5,53 @@ where `i` *subsists* in `s[φ]` if there are any `i'` that *extend* `i` in `s[φ]`. - Here's how to do that in our framework. Instead of a possibility subsisting in an updated set of possibilities, we ask what is returned by extensions of a `dpm` when they're given a particular (r, h) as input. + Here's how to do that in our framework. Instead of asking whether a possibility subsists in an updated set of possibilities, we ask what is returned by extensions of a `dpm` when they're given a particular (r, h) as input. (* filter out which bool dpms in a set are true when receiving (r, h) as input *) - let truths set (r, h) = List.filter (fun one_dpm -> let (truth_value, _, _) = one_dpm (r, h) in truth_value) set;; + let truths set (r, h) = + let test one_dpm = + let (truth_value, _, _) = one_dpm (r, h) + in truth_value + in List.filter test set;; let negate_op (phi : clause) : clause = fun one_dpm -> let new_dpm = fun (r, h) -> - (* we want to check the behavior of one_dpm when updated with the operation phi *) - (* bind_set (unit_set one_dpm) phi === phi one_dpm; do you remember why? *) - let truth_value' = truths (phi one_dpm) (r, h) = [] - (* we return a (bool, r, h) so as to constitute a dpm *) - in (truth_value', r, h) - in unit_set new_dpm + (* if one_dpm isn't already false at (r, h), + we want to check its behavior when updated with phi + set_bind (set_unit one_dpm) phi === phi one_dpm; do you remember why? *) + let (truth_value, r', h') = one_dpm (r, h) + in let truth_value' = truth_value && (truths (phi one_dpm) (r, h) = []) + (* new_dpm must return a (bool, r, h) *) + in (truth_value', r', h') + in set_unit new_dpm;; + **Thanks to Simon Charlow** for catching a subtle error in previous versions of this function. Fixed 1 Dec. + * Representing \[[and φ ψ]] is simple: let and_op (phi : clause) (psi : clause) : clause = - fun one_dpm -> bind_set (phi one_dpm) psi;; + fun one_dpm -> set_bind (phi one_dpm) psi;; + (* now u >>= and_op phi psi === u >>= phi >>= psi; do you remember why? *) + * Here are `or` and `if`: + (These probably still manifest the bug Simon spotted.) + let or_op (phi : clause) (psi : clause) = - (* NOT: negate_op (and_op (negate_op phi) (negate_op psi)) *) - fun one_dpm -> unit_set ( + fun one_dpm -> set_unit ( fun (r, h) -> - in let truth_value' = truths (phi one_dpm) (r, h) <> [] || truths (bind_set (negate_op phi one_dpm) psi) (r, h) <> [] - in (truth_value', r, h)) + let truth_value' = ( + truths (phi one_dpm) (r, h) <> [] || + truths (set_bind (negate_op phi one_dpm) psi) (r, h) <> [] + ) in (truth_value', r, h)) let if_op (phi : clause) (psi : clause) : clause = - (* NOT: negate_op (and_op phi (negate_op psi)) *) - fun one_dpm -> unit_set ( + fun one_dpm -> set_unit ( fun (r, h) -> - in let truth_value' = List.for_all (fun one_dpm -> + let truth_value' = List.for_all (fun one_dpm -> let (truth_value, _, _) = one_dpm (r, h) in truth_value = false || truths (psi one_dpm) (r, h) <> [] ) (phi one_dpm) @@ -53,21 +65,23 @@ type assignment = char -> int;; type store = entity list;; type 'a dpm = assignment * store -> 'a * assignment * store;; - let unit_dpm (x : 'a) : 'a dpm = fun (r, h) -> (x, r, h);; - let bind_dpm (u: 'a dpm) (f : 'a -> 'b dpm) : 'b dpm = + let dpm_unit (x : 'a) : 'a dpm = fun (r, h) -> (x, r, h);; + let dpm_bind (u: 'a dpm) (f : 'a -> 'b dpm) : 'b dpm = fun (r, h) -> let (a, r', h') = u (r, h) in let u' = f a in u' (r', h') 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) : 'b set = + let set_empty : 'a set = [];; + let set_unit (x : 'a) : 'a set = [x];; + let set_bind (u : 'a set) (f : 'a -> 'b set) : 'b set = List.concat (List.map f u);; type clause = bool dpm -> bool dpm set;; +* More: + (* this generalizes the getx function from hint 4 *) let get (var : char) : entity dpm = fun (r, h) -> @@ -77,20 +91,20 @@ (* this generalizes the proposal for \[[Q]] from hint 4 *) let lift_predicate (f : entity -> bool) : entity dpm -> clause = fun entity_dpm -> - let eliminator = fun (truth_value : bool) -> + let eliminator = fun truth_value -> if truth_value = false - then unit_dpm false - else bind_dpm entity_dpm (fun e -> unit_dpm (f e)) - in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator);; + then dpm_unit false + else dpm_bind entity_dpm (fun e -> dpm_unit (f e)) + in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator);; (* doing the same thing for binary predicates *) let lift_predicate2 (f : entity -> entity -> bool) : entity dpm -> entity dpm -> clause = fun entity1_dpm entity2_dpm -> - let eliminator = fun (truth_value : bool) -> + let eliminator = fun truth_value -> if truth_value = false - then unit_dpm false - else bind_dpm entity1_dpm (fun e1 -> bind_dpm entity2_dpm (fun e2 -> unit_dpm (f e1 e2))) - in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator);; + then dpm_unit false + else dpm_bind entity1_dpm (fun e1 -> dpm_bind entity2_dpm (fun e2 -> dpm_unit (f e1 e2))) + in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator);; let new_peg_and_assign (var_to_bind : char) (d : entity) : bool -> bool dpm = fun truth_value -> @@ -102,13 +116,17 @@ in (truth_value, r', h') (* from hint 5 *) - let exists var : clause = fun one_dpm -> - List.map (fun d -> bind_dpm one_dpm (new_peg_and_assign var d)) domain + let exists var : clause = + let extend one_dpm (d : entity) = + dpm_bind one_dpm (new_peg_and_assign var d) + in fun one_dpm -> List.map (fun d -> extend one_dpm d) domain (* include negate_op, and_op, or_op, and if_op as above *) +* More: + (* some handy utilities *) - let (>>=) = bind_set;; + let (>>=) = set_bind;; let getx = get 'x';; let gety = get 'y';; let initial_set = [fun (r,h) -> (true,r,h)];;