- Here's how to do that in our framework:
-
- type clause_op = bool dpm -> bool dpm set;;
-
- let negate_op (phi : clause_op) : clause_op =
- fun one_dpm -> unit_set (
- fun (r, h) ->
- let extensions set = List.filter (fun one_dpm -> let (truth_value, _, _) = one_dpm (r, h) in truth_value) set
- in let truth_value' = extensions (phi one_dpm) = []
- in (truth_value', r, h)
- )
-
+ 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) =
+ 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) ->
+ (* 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.