X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=hints%2Fassignment_7_hint_6.mdwn;h=e513284bd51d31b5eab302b3ab669e44957bf12f;hp=d69c92e7ed4d65fc9bfef71003559acb4efed46c;hb=0feebbaaa58403d836d7ea6166cf709dd3faf1a8;hpb=04296a25e1123f3e7240727f1e10142a1afadb7e;ds=sidebyside diff --git a/hints/assignment_7_hint_6.mdwn b/hints/assignment_7_hint_6.mdwn index d69c92e7..e513284b 100644 --- a/hints/assignment_7_hint_6.mdwn +++ b/hints/assignment_7_hint_6.mdwn @@ -20,13 +20,15 @@ (* if one_dpm isn't already false at (r, h), we want to check its behavior when updated with phi bind_set (unit_set one_dpm) phi === phi one_dpm; do you remember why? *) - let (truth_value, _, _) = one_dpm (r, h) + 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 (truth_value', r', h') in unit_set 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 = @@ -36,10 +38,12 @@ * Here are `or` and `if`: + (These probably still manifest the bug Simon spotted.) + let or_op (phi : clause) (psi : clause) = fun one_dpm -> unit_set ( fun (r, h) -> - in let truth_value' = ( + 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)) @@ -47,7 +51,7 @@ let if_op (phi : clause) (psi : clause) : clause = fun one_dpm -> unit_set ( 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)