From 7aacf596d73cc74eb9af381a72723b50b4069e30 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 00:35:33 -0300 Subject: symbolic discharge: universals over infinite domains decided by intervals --- lib/vm.ml | 239 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 233 insertions(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/vm.ml b/lib/vm.ml index a518aa5..8a09f3f 100644 --- a/lib/vm.ml +++ b/lib/vm.ml @@ -236,6 +236,217 @@ module Make (W : World.WORLD) = struct | None -> Unknown end + (* Symbolic discharge (decision 10, rung three, first fragment): + universals whose quantifier is an infinite domain are decided + algebraically when quantifier and body both read as kind and + interval constraints over the one quantified variable. Holds + means every member is covered; Fails is always backed by a + concrete counterexample; anything outside the fragment stays + deferred. Subtype inclusions (a Natural is an Integer is a + Rational) are decided here, literally, per decision 12. *) + module Symbolic = struct + type side = { + is_int : bool; (** members are integers *) + is_str : bool; + has_domain : bool; (** some domain goal declared the kind *) + lower : Propagate.bound option; + upper : Propagate.bound option; + } + + let free = { is_int = false; is_str = false; has_domain = false; lower = None; upper = None } + + (* One goal read as a constraint on [var]; None = outside the + fragment. Goals without variables evaluate outright. *) + let read subst var side (name, bindings) = + let value = Label.Map.find_opt Propagate.value_l bindings + and left = Label.Map.find_opt Propagate.left_l bindings + and right = Label.Map.find_opt Propagate.right_l bindings in + let ground_goal () = + match Builtin.run subst name bindings with + | Some (Builtin.Solved []) -> Some `Contradiction + | Some (Builtin.Solved _) -> Some `Trivial + | _ -> None + in + let is_var = function + | Pattern.Var v -> String.equal v var + | _ -> false + in + match (name, value, left, right) with + | ("Integer" | "Natural"), Some v, _, _ when is_var v -> + let side = { side with is_int = true; has_domain = true } in + if String.equal name "Natural" then + Some + (`Side + { + side with + lower = + Some + (match side.lower with + | None -> { Propagate.value = Q.zero; strict = false } + | Some b -> + Propagate.stronger_lower b + { Propagate.value = Q.zero; strict = false }); + }) + else Some (`Side side) + | "Rational", Some v, _, _ when is_var v -> + Some (`Side { side with has_domain = true }) + | "String", Some v, _, _ when is_var v -> + Some (`Side { side with is_str = true; has_domain = true }) + | ( ("LessThan" | "LessThanEqual" | "GreaterThan" | "GreaterEqual"), + _, + Some l, + Some r ) -> ( + let strict = + String.equal name "LessThan" || String.equal name "GreaterThan" + in + let less = + String.equal name "LessThan" || String.equal name "LessThanEqual" + in + let with_bound upper bound = + if upper then + `Side + { + side with + upper = + Some + (match side.upper with + | None -> bound + | Some b -> Propagate.stronger_upper b bound); + } + else + `Side + { + side with + lower = + Some + (match side.lower with + | None -> bound + | Some b -> Propagate.stronger_lower b bound); + } + in + match (l, r) with + | v, g when is_var v && Option.is_some (Propagate.numeric_value g) -> + Some + (with_bound less + { Propagate.value = Option.get (Propagate.numeric_value g); strict }) + | g, v when is_var v && Option.is_some (Propagate.numeric_value g) -> + Some + (with_bound (not less) + { Propagate.value = Option.get (Propagate.numeric_value g); strict }) + | _ -> None) + | _, _, _, _ -> + if + Label.Map.for_all + (fun _ p -> Pattern.vars p = []) + bindings + then ground_goal () + else None + + let read_side subst var goals = + List.fold_left + (fun acc goal -> + match acc with + | None | Some `Contradiction -> acc + | Some (`Side side) -> ( + match read subst var side goal with + | Some (`Side _ as s) -> Some s + | Some `Trivial -> Some (`Side side) + | Some `Contradiction -> Some `Contradiction + | None -> None)) + (Some (`Side free)) goals + + (* Does the quantifier's lower bound guarantee the body's? For + integer kinds compare tightened endpoints; missing body bound + is no demand, missing quantifier bound cannot guarantee one. *) + let lower_entails ~int q b = + match b with + | None -> true + | Some b -> ( + match q with + | None -> false + | Some q -> + if int then Z.geq (Propagate.lower_int q) (Propagate.lower_int b) + else + Q.gt q.Propagate.value b.Propagate.value + || (Q.equal q.Propagate.value b.Propagate.value + && ((not b.strict) || q.strict))) + + let upper_entails ~int q b = + match b with + | None -> true + | Some b -> ( + match q with + | None -> false + | Some q -> + if int then Z.leq (Propagate.upper_int q) (Propagate.upper_int b) + else + Q.lt q.Propagate.value b.Propagate.value + || (Q.equal q.Propagate.value b.Propagate.value + && ((not b.strict) || q.strict))) + + (* A rational interval that is one integer point. *) + let single_integer_point q = + match (q.lower, q.upper) with + | Some lo, Some hi -> + (not lo.Propagate.strict) + && (not hi.Propagate.strict) + && Q.equal lo.value hi.value + && Z.equal (Q.den lo.value) Z.one + | _ -> false + + let entails q b = + if q.is_str then + if b.is_int || b.lower <> None || b.upper <> None then `Fails + else `Holds + else if b.is_str then `Fails + else if b.is_int && (not q.is_int) && not (single_integer_point q) then + `Fails + else if + lower_entails ~int:q.is_int q.lower b.lower + && upper_entails ~int:q.is_int q.upper b.upper + then `Holds + else `Fails + + let discharge subst quantifier_goals body_goals = + let apply_only goals = + List.fold_left + (fun acc goal -> + Option.bind acc (fun goals -> + match goal with + | World.Apply (name, bindings) -> + Some + ((name, Label.Map.map (Pattern.Subst.resolve subst) bindings) + :: goals) + | _ -> None)) + (Some []) goals + in + match (apply_only quantifier_goals, apply_only body_goals) with + | Some quantifier, Some body -> ( + let vars = + List.concat_map + (fun (_, bindings) -> + Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings []) + quantifier + |> List.sort_uniq String.compare + in + match vars with + | [ var ] -> ( + match (read_side subst var quantifier, read_side subst var body) with + | Some (`Side q), Some (`Side b) -> + if q.has_domain then entails q b else `Unknown + | Some (`Side q), Some `Contradiction -> + (* The body is falsified outright; any member of a + nonempty quantifier is a counterexample. *) + if q.has_domain then `Fails else `Unknown + | Some `Contradiction, _ -> + (* An empty quantifier satisfies any universal. *) + `Holds + | _ -> `Unknown) + | _ -> `Unknown) + | _ -> `Unknown + end + + let rec try_goal world subst goal = match goal with | Negated denial -> @@ -252,15 +463,31 @@ module Make (W : World.WORLD) = struct Run [ (subst, flatten a); (subst, flatten b) ] | Positive ((World.And _ | World.Not _) as expr) -> Run [ (subst, flatten expr) ] | Positive (World.Forall (quantifier, body)) -> ( - (* Universal over the quantifier's solutions. Runs only when - the quantifier is decidable and closed; an undetermined - quantifier or body defers the universal, and an infinite - one therefore never runs. *) + (* Universal over the quantifier's solutions. Runs when the + quantifier is decidable and closed; otherwise symbolic + discharge gets a chance before the universal defers, so + truths over infinite domains are proven, never + enumerated. *) + let rec conjuncts = function + | World.And (a, b) -> conjuncts a @ conjuncts b + | expr -> [ expr ] + in + let symbolically () = + match + Symbolic.discharge subst (conjuncts quantifier) (conjuncts body) + with + | `Holds -> Run [ (subst, []) ] + | `Fails -> Run [] + | `Unknown -> Wait { residuatable = false } + in match search world subst (flatten quantifier) with - | exception Stuck _ -> Wait { residuatable = false } + | exception Stuck _ -> symbolically () | quantified -> if List.exists (fun (_, residue) -> residue <> []) quantified then - Wait { residuatable = false } + (* The quantifier residuated: an infinite or + underdetermined domain. Enumeration is off the + table; proof is not. *) + symbolically () else let body_status (s, _) = match search world s (flatten body) with -- cgit v1.2.3