diff options
| -rw-r--r-- | docs/core-design-and-pipeline.org | 14 | ||||
| -rw-r--r-- | docs/virtual-machine-specification.org | 14 | ||||
| -rw-r--r-- | docs/vm.org | 15 | ||||
| -rw-r--r-- | lib/vm.ml | 6 | ||||
| -rw-r--r-- | lib/world.ml | 216 | ||||
| -rw-r--r-- | lib/world.mli | 12 | ||||
| -rw-r--r-- | test/test_vm.ml | 48 |
7 files changed, 228 insertions, 97 deletions
diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org index 9e085f8..823a24e 100644 --- a/docs/core-design-and-pipeline.org +++ b/docs/core-design-and-pipeline.org @@ -107,15 +107,17 @@ meaning; the =WORLD= functor is the seam it plugs into. What the implementation enforces today is rung one and part of rung two of the ladder in decision 10: -- structural decrease on self recursive rules, with the witness - demanded ground at unfolding; +- lexicographic structural decrease across call graph components, + with every measure position demanded ground at unfolding; self + recursion and mutual recursion are the same check; - bounded enumeration through =Between=; -- decidable negation and universals only over decidable quantifiers. +- decidable negation and universals only over decidable quantifiers; +- residuation: open membership returns as residual constraints + instead of failing the plan. Not yet present: symbolic discharge (algebraic proof of universals -over infinite domains), Rocq certificates as admission evidence, -mutual recursion under a lexicographic measure, and a constraint -store that residuates instead of rejecting. Each arrives as a +over infinite domains), Rocq certificates as admission evidence, and +active constraint propagation over residue. Each arrives as a strengthening of admission or planning; none changes the semantics of what is already admitted. diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org index f70f459..c44b666 100644 --- a/docs/virtual-machine-specification.org +++ b/docs/virtual-machine-specification.org @@ -74,10 +74,12 @@ fact. The engine terminates on every admitted program. The argument, each piece machine checkable and one piece machine checked today: -1. every rule that unfolds recursively has a witness whose argument - is ground and strictly contained in the head's at each unfolding; -2. strict containment decreases a natural measure, and the induced - order is well founded: proven in =theories/Decrease.v=; +1. every rule that unfolds recursively carries its component's + lexicographic measure, all positions ground at unfolding, and + every call cycle through the component strictly decreases it; +2. strict containment decreases a natural measure, the induced + order is well founded (proven in =theories/Decrease.v=), and the + lexicographic product of well founded orders is well founded; 3. tables are finite, builtins decide or defer without search, and bounded generators enumerate finite ranges; 4. disjunction and rule choice branch finitely. @@ -136,8 +138,8 @@ without changing admitted semantics: infinite domains, and arithmetic decrease measures for recursion that structural containment cannot see; - Rocq certificates as admission evidence, and extraction of the - checker itself; -- mutual recursion under lexicographic measures; + lexicographic search itself (the containment core is already + extracted); - lowering of finite first order subplans to RNT's =Plan.t= algebra with Sakura's cardinality tags, per decision 9; - tabling for shared subderivations, an optimization the pure diff --git a/docs/vm.org b/docs/vm.org index 8d1215a..87c0ca0 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -36,12 +36,15 @@ A program only becomes a world if everything in it is admitted: attribute domain. This is integrity control at load time, the same membership check it always is. A Natural is an Integer and an Integer is a Rational, literally. -- a recursive rule must exhibit a structurally decreasing argument: - some label whose call argument sits strictly inside the head - argument, like =T= inside =#(H | T)=. The label is kept as the - rule's witness. No witness, no world. -- mutual recursion between relations is rejected for now. Self - recursion with a witness is the admitted form. +- recursion must exhibit a lexicographic structural decrease. + Admission groups rule defined relations into strongly connected + components of the call graph and searches for an ordered list of + labels such that every call inside the component strictly shrinks + at some position, all earlier positions staying equal. Self + recursion is the one label case, like =T= inside =#(H | T)=; + mutual recursion like Even and Odd passing a shrinking list back + and forth is admitted the same way. The measure is stamped on the + recursive rules as their witness. No measure, no world. - every referenced relation must exist, either builtin or declared. This is rung one of the evidence ladder in decision 10. Bounded @@ -155,13 +155,13 @@ module Make (W : World.WORLD) = struct facts) | Some (World.Rules rules) -> let witness_ground rule = - match rule.World.witness with - | None -> true - | Some label -> ( + List.for_all + (fun label -> match Label.Map.find_opt label bindings with | Some pattern -> Pattern.is_ground (Pattern.Subst.resolve subst pattern) | None -> false) + rule.World.witness in if List.for_all witness_ground rules then Run diff --git a/lib/world.ml b/lib/world.ml index 6e1e883..8ade9da 100644 --- a/lib/world.ml +++ b/lib/world.ml @@ -9,7 +9,7 @@ type rule = { rule_name : string; head : Pattern.t Label.Map.t; body : expr; - witness : Label.t option; + witness : Label.t list; } type primitive = D_integer | D_natural | D_rational | D_string @@ -42,8 +42,7 @@ type error = | Fact_not_ground of string | Schema_mismatch of { relation : string; detail : string } | Domain_violation of { relation : string; label : string } - | Non_total_rule of string - | Mutual_recursion of string list + | Non_total_component of string list | Criterion_arity of { relation : string; label : string } type pending = { @@ -69,13 +68,10 @@ let pp_error fmt = function Format.fprintf fmt "schema mismatch on %s: %s" relation detail | Domain_violation { relation; label } -> Format.fprintf fmt "domain violation on %s at %s:" relation label - | Non_total_rule name -> + | Non_total_component relations -> Format.fprintf fmt - "rule %S rejected: no structurally decreasing argument in its recursive call" - name - | Mutual_recursion cycle -> - Format.fprintf fmt "mutual recursion rejected: %s" - (String.concat " -> " cycle) + "recursion among %s rejected: no lexicographic structural decrease covers every call" + (String.concat ", " relations) | Criterion_arity { relation; label } -> Format.fprintf fmt "criterion on %s at %s: must have exactly one free variable, the subject" @@ -268,37 +264,55 @@ module Standalone = struct |> Result.map List.rev | _ -> Error (Malformed_directive "schema: takes #( ... ) of entries") - (* The structural decrease check of decision 10, rung one. Every - self-recursive application must have an argument strictly - contained in the head's argument at the same label; that label - is kept as the runtime witness. *) - let admit_rule ~relation rule_name head body = - let recursive = - applications body |> List.filter (fun (name, _) -> String.equal name relation) - in - match recursive with - | [] -> Ok { rule_name; head; body; witness = None } + (* The structural decrease check of decision 10, rung one, + generalized to call-graph components. For every strongly + connected component of the call graph among rule-defined + relations, a lexicographic measure of shared labels must + decrease on every intra-component call: at some position the + call argument sits strictly inside the head's, and at every + earlier position they are syntactically equal. The measure is + stored on each recursive rule and its positions must be ground + at unfolding, which turns the proof into a runtime termination + measure. *) + + type call = { head : Pattern.t Label.Map.t; args : Pattern.t Label.Map.t } + + let decreases c label = + match (Label.Map.find_opt label c.head, Label.Map.find_opt label c.args) with + | Some head_arg, Some call_arg -> + Pattern.strictly_contains head_arg ~sub:call_arg + | _ -> false + + let stays_equal c label = + match (Label.Map.find_opt label c.head, Label.Map.find_opt label c.args) with + | Some head_arg, Some call_arg -> Pattern.equal head_arg call_arg + | _ -> false + + (* Greedy lexicographic search with backtracking: pick a label + that decreases or stays equal on every remaining call and + decreases on at least one; the calls it covers drop out, the + rest must be covered by later positions. *) + let rec lex_measure calls candidates = + match calls with + | [] -> Some [] | _ -> - let witness_for (_, call_bindings) = - Label.Map.fold - (fun label head_arg found -> - match found with - | Some _ -> found - | None -> ( - match Label.Map.find_opt label call_bindings with - | Some call_arg - when Pattern.strictly_contains head_arg ~sub:call_arg -> - Some label - | _ -> None)) - head None - in - let witnesses = List.map witness_for recursive in - if List.for_all Option.is_some witnesses then - (* All recursive calls decrease; any common witness works - at runtime, and per-call witnesses agree by label here - because they are all drawn from the same head. *) - Ok { rule_name; head; body; witness = List.nth witnesses 0 } - else Error (Non_total_rule rule_name) + List.find_map + (fun label -> + if + List.for_all + (fun c -> decreases c label || stays_equal c label) + calls + && List.exists (fun c -> decreases c label) calls + then + let remaining = + List.filter (fun c -> not (decreases c label)) calls + in + Option.map + (fun rest -> label :: rest) + (lex_measure remaining + (List.filter (fun l -> not (Label.equal l label)) candidates)) + else None) + candidates let load statements = (* First pass: declare tables, collect raw material. *) @@ -350,7 +364,7 @@ module Standalone = struct | _ -> Error (Malformed_directive "a rule head is a single [...] block") in let* body = expr_of_node body_node in - let* rule = admit_rule ~relation rule_name head body in + let rule = { rule_name; head; body; witness = [] } in let existing = Option.value ~default:[] (String_map.find_opt relation grouped) in @@ -484,40 +498,108 @@ module Standalone = struct (Ok ()) rules) world (Ok ()) in - let dependencies relation = + (* Component analysis: group rule-defined relations into + strongly connected components of the call graph, find a + lexicographic measure for each recursive component, and stamp + it on the recursive rules as their runtime witness. *) + let rule_defined name = + match String_map.find_opt name world with + | Some (Rules _) -> true + | _ -> false + in + let edges relation = match String_map.find_opt relation world with | Some (Rules rules) -> List.concat_map - (fun rule -> - applications rule.body - |> List.filter_map (fun (name, _) -> - if - (not (String.equal name relation)) - && (match String_map.find_opt name world with - | Some (Rules _) -> true - | _ -> false) - then Some name - else None)) + (fun rule -> List.map fst (applications rule.body)) rules + |> List.filter rule_defined + |> List.sort_uniq String.compare | _ -> [] in - let* () = - let rec visit path relation = - if List.mem relation path then - Error (Mutual_recursion (List.rev (relation :: path))) - else - List.fold_left - (fun acc dep -> - let* () = acc in - visit (relation :: path) dep) - (Ok ()) - (dependencies relation) + let reachable start = + let rec go seen frontier = + match frontier with + | [] -> seen + | name :: rest -> + if List.mem name seen then go seen rest + else go (name :: seen) (edges name @ rest) in - String_map.fold - (fun relation def acc -> - let* () = acc in - match def with Rules _ -> visit [] relation | Table _ -> Ok ()) - world (Ok ()) + go [] (edges start) + in + let* world = + let relations = + String_map.fold + (fun name def acc -> + match def with Rules _ -> name :: acc | Table _ -> acc) + world [] + in + let component relation = + let reach = reachable relation in + relation + :: List.filter + (fun other -> + (not (String.equal other relation)) + && List.mem other reach + && List.mem relation (reachable other)) + relations + in + List.fold_left + (fun acc relation -> + let* world = acc in + let members = component relation in + (* Process each component once, from its least member. *) + if not (String.equal relation (List.fold_left min relation members)) + then Ok world + else + let member name = List.mem name members in + let calls_of (rule : rule) = + applications rule.body + |> List.filter_map (fun (target, args) -> + if member target then Some { head = rule.head; args } + else None) + in + let rules_of name = + match String_map.find_opt name world with + | Some (Rules rules) -> rules + | _ -> [] + in + let calls = List.concat_map calls_of (List.concat_map rules_of members) in + if calls = [] then Ok world + else + let candidates = + match calls with + | [] -> [] + | first :: rest -> + Label.Map.fold + (fun label _ acc -> + if + List.for_all + (fun c -> + Label.Map.mem label c.head + && Label.Map.mem label c.args) + rest + && Label.Map.mem label first.args + then label :: acc + else acc) + first.head [] + in + match lex_measure calls candidates with + | None -> Error (Non_total_component members) + | Some measure -> + Ok + (List.fold_left + (fun world name -> + let stamped = + List.map + (fun rule -> + if calls_of rule = [] then rule + else { rule with witness = measure }) + (rules_of name) + in + String_map.add name (Rules stamped) world) + world members)) + (Ok world) relations in (* Queries compile last, against the full catalog. *) let* queries = diff --git a/lib/world.mli b/lib/world.mli index 51ee078..14f82d3 100644 --- a/lib/world.mli +++ b/lib/world.mli @@ -29,11 +29,13 @@ type rule = { rule_name : string; head : Pattern.t Label.Map.t; body : expr; - witness : Label.t option; - (** For a recursive rule, the label whose argument strictly - decreases. The VM requires it ground before unfolding, - which is what turns the admission proof into runtime - termination. [None] on non-recursive rules. *) + witness : Label.t list; + (** For a recursive rule, the lexicographic measure of its + call-graph component: at some position the recursive + argument strictly decreases, all earlier positions staying + equal. The VM requires every position ground before + unfolding, which is what turns the admission proof into + runtime termination. Empty on non-recursive rules. *) } (** The primitive host-checked domains. *) diff --git a/test/test_vm.ml b/test/test_vm.ml index 0ae62e1..ad58720 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -113,6 +113,42 @@ let test_deep_recursion () = items) "R=1000" +(* Mutual recursion under a shared measure. *) + +let even_odd = + {| + Rule name: "even nil" head: [Even list: #()] body: [True] + Rule name: "even step" head: [Even list: #(H | T)] body: [Odd list: T] + Rule name: "odd step" head: [Odd list: #(H | T)] body: [Even list: T] + |} + +let count_solutions source = + match run source with + | [ solutions ] -> List.length solutions + | _ -> Alcotest.fail "expected one query" + +let test_mutual_recursion_admitted () = + Alcotest.(check int) + "four elements are even" 1 + (count_solutions (even_odd ^ {| Query expression: [Even list: #(1 2 3 4)] |})); + Alcotest.(check int) + "three elements are not even" 0 + (count_solutions (even_odd ^ {| Query expression: [Even list: #(1 2 3)] |})) + +let test_lexicographic_measure () = + (* One rule decreases b keeping a equal; the other decreases a + while b grows back. Only the order (a, b) covers both calls. *) + let walk = + {| + Rule name: "done" head: [Walk a: #() b: #()] body: [True] + Rule name: "b step" head: [Walk a: A b: #(H | T)] body: [Walk a: A b: T] + Rule name: "a step" head: [Walk a: #(H | T) b: #()] body: [Walk a: T b: #(1 1)] + |} + in + Alcotest.(check int) + "the walk terminates" 1 + (count_solutions (walk ^ {| Query expression: [Walk a: #(1 2) b: #(9)] |})) + (* Bounded generation is the only enumeration. *) let test_between_generates () = @@ -145,7 +181,7 @@ let test_fresh_variable_is_no_decrease () = | Error _ -> () | Ok _ -> Alcotest.fail "a fresh variable is not a structural decrease" -let test_mutual_recursion_rejected () = +let test_undecreasing_mutual_recursion_rejected () = match load {| @@ -154,7 +190,7 @@ let test_mutual_recursion_rejected () = |} with | Error _ -> () - | Ok _ -> Alcotest.fail "mutual recursion must be rejected" + | Ok _ -> Alcotest.fail "mutual recursion without decrease must be rejected" let test_unbounded_membership_residuates () = (* Membership is not generation and not an error either: the @@ -334,6 +370,10 @@ let () = Alcotest.test_case "length" `Quick test_length; Alcotest.test_case "length over strings" `Quick test_length_of_strings; Alcotest.test_case "deep recursion" `Quick test_deep_recursion; + Alcotest.test_case "mutual recursion admitted" `Quick + test_mutual_recursion_admitted; + Alcotest.test_case "lexicographic measure" `Quick + test_lexicographic_measure; ] ); ( "search", [ @@ -345,8 +385,8 @@ let () = Alcotest.test_case "loop rejected" `Quick test_loop_rule_rejected; Alcotest.test_case "fresh variable is no decrease" `Quick test_fresh_variable_is_no_decrease; - Alcotest.test_case "mutual recursion rejected" `Quick - test_mutual_recursion_rejected; + Alcotest.test_case "undecreasing mutual recursion rejected" `Quick + test_undecreasing_mutual_recursion_rejected; Alcotest.test_case "open membership residuates" `Quick test_unbounded_membership_residuates; Alcotest.test_case "residue discharged by binding" `Quick |