From e92c8e00290bab8db328058c437b471c0f1671a4 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 09:59:59 -0300 Subject: algebraic identities of plus and times discharge symbolically --- docs/core-design-and-pipeline.org | 17 +++++++------ docs/vm.org | 7 ++++-- lib/vm.ml | 51 +++++++++++++++++++++++++++++++++++++-- test/test_vm.ml | 16 ++++++++++++ 4 files changed, 79 insertions(+), 12 deletions(-) diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org index c81b58a..eda5429 100644 --- a/docs/core-design-and-pipeline.org +++ b/docs/core-design-and-pipeline.org @@ -117,14 +117,15 @@ two of the ladder in decision 10: - interval propagation over residue: contradictions fail, finite integer ranges enumerate; - symbolic discharge, first fragment: universals over infinite - domains decided by kind inclusion and interval entailment, with - refutations backed by counterexamples. - -Not yet present: symbolic discharge beyond the interval fragment -(algebraic identities of relations, arithmetic decrease measures) -and Rocq certificates as admission evidence. Each arrives as a -strengthening of admission or planning; none changes the semantics -of what is already admitted. + domains decided by kind inclusion, interval entailment, and the + unit identities of the numeric relations, with refutations backed + by counterexamples. + +Not yet present: symbolic discharge beyond that fragment (richer +algebraic theories, arithmetic decrease measures) and Rocq +certificates as admission evidence. Each arrives as a strengthening +of admission or planning; none changes the semantics of what is +already admitted. * What embedding means diff --git a/docs/vm.org b/docs/vm.org index a51b85a..d678acd 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -106,8 +106,11 @@ engine decides entailment algebraically. Every natural is at least zero: proven. Not every integer is: refuted, and the refutation is backed by a concrete counterexample. Every integer is a rational: proven, which is decision 12's subtype inclusion decided -symbolically. A universal outside that fragment is a non total plan, -rejected, as decision 10 requires. +symbolically. The unit identities of the numeric relations discharge +too: =[Plus left: X right: 0 result: X]= holds over all integers by +the algebra of =Plus=, in the flat membership form of decision 14, +and fails over strings, which do not add. A universal outside that +fragment is a non total plan, rejected, as decision 10 requires. * Membership criteria as domains diff --git a/lib/vm.ml b/lib/vm.ml index 8a09f3f..4a11c4d 100644 --- a/lib/vm.ml +++ b/lib/vm.ml @@ -110,6 +110,7 @@ module Make (W : World.WORLD) = struct let value_l = forced_label "value" let left_l = forced_label "left" let right_l = forced_label "right" + let result_l = forced_label "result" type bound = { value : Q.t; strict : bool } @@ -249,11 +250,20 @@ module Make (W : World.WORLD) = struct is_int : bool; (** members are integers *) is_str : bool; has_domain : bool; (** some domain goal declared the kind *) + needs_num : bool; (** the body demands a numeric member *) lower : Propagate.bound option; upper : Propagate.bound option; } - let free = { is_int = false; is_str = false; has_domain = false; lower = None; upper = None } + let free = + { + is_int = false; + is_str = false; + has_domain = false; + needs_num = false; + lower = None; + upper = None; + } (* One goal read as a constraint on [var]; None = outside the fragment. Goals without variables evaluate outright. *) @@ -334,6 +344,42 @@ module Make (W : World.WORLD) = struct (with_bound (not less) { Propagate.value = Option.get (Propagate.numeric_value g); strict }) | _ -> None) + | ("Plus" | "Times"), _, Some l, Some r -> ( + (* The algebraic identities of the numeric relations: + membership statements that hold for every numeric + member, so a numeric quantifier discharges them and a + string quantifier refutes them. Anything beyond the + identities stays outside the fragment. *) + let result = Label.Map.find_opt Propagate.result_l bindings in + let is_zero = function + | Pattern.Integer z -> Z.equal z Z.zero + | _ -> false + and is_one = function + | Pattern.Integer z -> Z.equal z Z.one + | _ -> false + in + let identity = + match (name, l, r, result) with + | "Plus", v, unit_, Some v' when is_var v && is_zero unit_ && is_var v' -> + true + | "Plus", unit_, v, Some v' when is_var v && is_zero unit_ && is_var v' -> + true + | "Times", v, unit_, Some v' when is_var v && is_one unit_ && is_var v' -> + true + | "Times", unit_, v, Some v' when is_var v && is_one unit_ && is_var v' -> + true + | "Times", v, zero, Some zero' when is_var v && is_zero zero && is_zero zero' + -> + true + | "Times", zero, v, Some zero' when is_var v && is_zero zero && is_zero zero' + -> + true + | _ -> false + in + if identity then Some (`Side { side with needs_num = true }) + else if Label.Map.for_all (fun _ p -> Pattern.vars p = []) bindings then + ground_goal () + else None) | _, _, _, _ -> if Label.Map.for_all @@ -396,7 +442,8 @@ module Make (W : World.WORLD) = struct let entails q b = if q.is_str then - if b.is_int || b.lower <> None || b.upper <> None then `Fails + if b.is_int || b.needs_num || 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 diff --git a/test/test_vm.ml b/test/test_vm.ml index 16ca63c..4729841 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -292,6 +292,20 @@ let test_symbolic_interval_entailment () = (holds {| Query expression: [ForAll variable: X quantifier: ([Natural value: X] :and [GreaterEqual left: X right: 10]) body: [GreaterThan left: X right: 5]] |}) +let test_symbolic_algebraic_identity () = + (* The specification's flagship symbolic example, in the flat + membership form of decision 14. *) + Alcotest.(check bool) "adding zero is the identity, over all integers" true + (holds + {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [Plus left: X right: 0 result: X]] |}); + Alcotest.(check bool) "multiplying by one is the identity, over all rationals" + true + (holds + {| Query expression: [ForAll variable: X quantifier: [Rational value: X] body: [Times left: 1 right: X result: X]] |}); + Alcotest.(check bool) "strings do not add" false + (holds + {| Query expression: [ForAll variable: X quantifier: [String value: X] body: [Plus left: X right: 0 result: X]] |}) + let test_forall_outside_fragment_still_rejected () = match load @@ -489,6 +503,8 @@ let () = Alcotest.test_case "inclusion" `Quick test_symbolic_inclusion; Alcotest.test_case "interval entailment" `Quick test_symbolic_interval_entailment; + Alcotest.test_case "algebraic identity" `Quick + test_symbolic_algebraic_identity; Alcotest.test_case "outside fragment still rejected" `Quick test_forall_outside_fragment_still_rejected; ] ); -- cgit v1.2.3