diff options
Diffstat (limited to '')
| -rw-r--r-- | bin/main.ml | 20 | ||||
| -rw-r--r-- | docs/virtual-machine-specification.org | 22 | ||||
| -rw-r--r-- | docs/vm.org | 11 | ||||
| -rw-r--r-- | lib/program.ml | 14 | ||||
| -rw-r--r-- | lib/vm.ml | 143 | ||||
| -rw-r--r-- | lib/vm.mli | 25 | ||||
| -rw-r--r-- | test/test_embedding.ml | 21 | ||||
| -rw-r--r-- | test/test_vm.ml | 43 |
8 files changed, 223 insertions, 76 deletions
diff --git a/bin/main.ml b/bin/main.ml index e7df2e2..c5c329a 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -8,17 +8,17 @@ let print_solutions solutions = | [] -> print_endline "no." | solutions -> List.iter - (fun solution -> - match solution with + (fun { Sol.Vm.bindings; residue } -> + let parts = + List.map + (fun (variable, pattern) -> + Format.asprintf "%s = %a" variable Sol.Pattern.pp pattern) + bindings + @ List.map (Format.asprintf "%a" Sol.Vm.pp_residual) residue + in + match parts with | [] -> print_endline "yes." - | bindings -> - let parts = - List.map - (fun (variable, pattern) -> - Format.asprintf "%s = %a" variable Sol.Pattern.pp pattern) - bindings - in - print_endline (String.concat ", " parts ^ ".")) + | parts -> print_endline (String.concat ", " parts ^ ".")) solutions let run_statements statements = diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org index 90cc6c0..f70f459 100644 --- a/docs/virtual-machine-specification.org +++ b/docs/virtual-machine-specification.org @@ -53,14 +53,21 @@ runs any goal decidable under the current substitution: - a universal runs once its quantifier is decidable, checking the body against every quantifier solution. -Goals that are not yet decidable wait. If none can ever run, the plan -is rejected with the stuck goals named. This is the whole of the -distinction the specification demands: membership checks, constraints +Goals that are not yet decidable wait. When only waiting goals +remain, membership residuates and search rejects: if every remaining +goal is builtin membership, the answer carries them as residual +constraints; if any is a stalled search, the plan is rejected with +the stuck goals named. This is the whole of the distinction the +specification demands: membership checks or residuates, constraints wait, generation only under bounds, and non total plans do not execute. -Answers are the query's free variables resolved to canonical values. -Variables that live only under a universal are not answer variables. +Answers are the query's free variables resolved to canonical values, +plus the residual constraints the answer is conditioned on; the +common case is ground and residue free. Variables that live only +under a universal are not answer variables. Integrity criteria +accept only residue free proof: a conditioned answer admits no +fact. * Totality accounting @@ -122,8 +129,9 @@ whole or not at all. Specified, not yet implemented; each grows admission or planning without changing admitted semantics: -- residuation: a constraint store that returns residual constraints - for satisfiable but underdetermined queries instead of rejecting; +- constraint propagation: residuated constraints today wait and + return; a store that actively narrows domains and detects + unsatisfiable residue early is the next strength; - symbolic discharge: algebraic evidence for universals over infinite domains, and arithmetic decrease measures for recursion that structural containment cannot see; diff --git a/docs/vm.org b/docs/vm.org index 4253231..8d1215a 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -56,9 +56,14 @@ decidable wait. So conjunction stays commutative in fact, not just in doctrine: the page order of =:and= operands never matters, and the tests assert it. -If no remaining goal can ever run, the plan is rejected as non -total. =[Integer value: X]= alone is not an enumeration, it is an -error telling you to bind or bound =X=. Membership is not generation. +When goals remain that cannot run, two things can happen. If every +one of them is pure membership, decidable the moment its variables +ground, the answer comes back with those goals as residual +constraints: =[Integer value: X]= alone answers =X= conditioned on +=[Integer value: X]=, which is exactly what the expression means. +Constraining is not searching. If any remaining goal is a stalled +search, an unbounded recursion or an infinite universal, the plan is +rejected as non total. Membership is never generation either way. Recursive rules unfold only when their witness argument is ground, so the admission proof becomes a runtime termination measure: the diff --git a/lib/program.ml b/lib/program.ml index ac62781..b0e363b 100644 --- a/lib/program.ml +++ b/lib/program.ml @@ -21,7 +21,19 @@ let load statements = pending in match Vm.Standalone.solve world pending_body with - | Ok (_ :: _) -> admit rest + (* Membership must be proven outright: an answer that is + itself conditioned on residual constraints does not + admit a fact. *) + | Ok solutions + when List.exists (fun s -> s.Vm.residue = []) solutions -> + admit rest + | Ok (_ :: _) -> + Error + (Undecidable_criterion + { + relation = pending_relation; + label = Label.to_string pending_label; + }) | Ok [] -> Error (Integrity @@ -5,7 +5,20 @@ let pp_error fmt (Non_total_plan goals) = "non-total plan rejected: no decidable goal among %s (bind more arguments or bound the search)" (String.concat ", " goals) -type solution = (string * Pattern.t) list +type residual = string * Pattern.t Label.Map.t + +let pp_residual fmt (name, bindings) = + Format.fprintf fmt "@[<hv 1>[%s" name; + Label.Map.iter + (fun label pattern -> + Format.fprintf fmt "@ %a %a" Label.pp label Pattern.pp pattern) + bindings; + Format.fprintf fmt "]@]" + +type solution = { + bindings : (string * Pattern.t) list; + residue : residual list; +} module Make (W : World.WORLD) = struct exception Stuck of string list @@ -15,6 +28,14 @@ module Make (W : World.WORLD) = struct positively and the denial negatively. *) type goal = Positive of World.expr | Negated of World.expr + (* What attempting a goal can say: run it into branches, or wait. + A waiting goal is residuatable when it is pure membership that + decides as soon as its arguments are ground; searches are + never residuatable. *) + type attempt = + | Run of (Pattern.Subst.t * goal list) list + | Wait of { residuatable : bool } + let rec flatten = function | World.And (a, b) -> flatten a @ flatten b | World.Not (universe, denial) -> flatten universe @ [ Negated denial ] @@ -74,40 +95,57 @@ module Make (W : World.WORLD) = struct | None -> None)) goal_bindings (Some subst) - (* Executing one goal yields branches: an extended substitution - and the extra goals it owes (rule bodies, disjuncts). [None] - means not decidable yet; the planner retries it later, and - rejects the plan if nothing ever runs. *) + let proven solutions = List.exists (fun (_, residue) -> residue = []) solutions + let rec try_goal world subst goal = match goal with | Negated denial -> if unresolved_vars subst denial = [] then match search world subst (flatten denial) with - | [] -> Some [ (subst, []) ] - | _ -> Some [] - else None - | Positive (World.Or (a, b)) -> Some [ (subst, flatten a); (subst, flatten b) ] - | Positive (World.And _ | World.Not _) -> - Some [ (subst, flatten (match goal with Positive e -> e | _ -> assert false)) ] + | [] -> Run [ (subst, []) ] + | solutions -> + (* Ground denials cannot residuate in practice, but if + one somehow does, refusing to conclude is the only + sound answer. *) + if proven solutions then Run [] else Wait { residuatable = false } + else Wait { residuatable = false } + | Positive (World.Or (a, b)) -> + 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. Decidable only - when the quantifier itself is; a stuck quantifier defers - the universal, and an infinite one therefore never runs. *) + (* 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. *) match search world subst (flatten quantifier) with - | exception Stuck _ -> None + | exception Stuck _ -> Wait { residuatable = false } | quantified -> - let holds s = search world s (flatten body) <> [] in - if List.for_all holds quantified then Some [ (subst, []) ] else Some [] - ) + if List.exists (fun (_, residue) -> residue <> []) quantified then + Wait { residuatable = false } + else + let body_status (s, _) = + match search world s (flatten body) with + | exception Stuck _ -> `Unknown + | [] -> `Fails + | solutions -> if proven solutions then `Holds else `Unknown + in + let statuses = List.map body_status quantified in + if List.mem `Fails statuses then Run [] + else if List.mem `Unknown statuses then + Wait { residuatable = false } + else Run [ (subst, []) ]) | Positive (World.Apply (name, bindings)) -> ( match Builtin.run subst name bindings with | Some (Builtin.Solved substs) -> - Some (List.map (fun s -> (s, [])) substs) - | Some Builtin.Stuck -> None + Run (List.map (fun s -> (s, [])) substs) + | Some Builtin.Stuck -> + (* Pure membership waiting on bindings: the residuatable + case. Constraining is not searching. *) + Wait { residuatable = true } | None -> ( match W.find world name with | Some (World.Table { facts; _ }) -> - Some + Run (List.filter_map (fun tuple -> let target = Label.Map.map Pattern.of_term tuple in @@ -126,7 +164,7 @@ module Make (W : World.WORLD) = struct | None -> false) in if List.for_all witness_ground rules then - Some + Run (List.filter_map (fun rule -> let head, body = freshen rule in @@ -134,31 +172,44 @@ module Make (W : World.WORLD) = struct (fun s -> (s, flatten body)) (unify_bindings subst bindings head)) rules) - else None + else Wait { residuatable = false } | None -> (* Unreachable on admitted programs: the loader checks references. An embedded host that lies about its catalog surfaces here as a stuck goal rather than a crash. *) - None)) + Wait { residuatable = false })) + (* Search yields substitutions with the goals they left + residuated. A state where every remaining goal is residuatable + membership is an answer; one with a stalled search is a + non-total plan. *) and search world subst goals = match goals with - | [] -> [ subst ] + | [] -> [ (subst, []) ] | _ -> ( let rec select scanned = function | [] -> None | goal :: rest -> ( match try_goal world subst goal with - | Some branches -> Some (branches, List.rev_append scanned rest) - | None -> select (goal :: scanned) rest) + | Run branches -> Some (branches, List.rev_append scanned rest) + | Wait _ -> select (goal :: scanned) rest) in match select [] goals with | Some (branches, remaining) -> List.concat_map (fun (subst, extra) -> search world subst (extra @ remaining)) branches - | None -> raise (Stuck (List.map goal_name goals))) + | None -> + if + List.for_all + (fun goal -> + match try_goal world subst goal with + | Wait { residuatable } -> residuatable + | Run _ -> false) + goals + then [ (subst, goals) ] + else raise (Stuck (List.map goal_name goals))) (* Solution variables: the free variables of the query. Whatever occurs only under a universal is bound per quantifier solution @@ -179,22 +230,40 @@ module Make (W : World.WORLD) = struct in match search world Pattern.Subst.empty (flatten expr) with | exception Stuck goals -> Error (Non_total_plan goals) - | substs -> - let read subst = - List.map - (fun v -> (v, Pattern.Subst.resolve subst (Pattern.Var v))) - variables + | outcomes -> + let read (subst, residue_goals) = + let bindings = + List.map + (fun v -> (v, Pattern.Subst.resolve subst (Pattern.Var v))) + variables + in + let residue = + List.filter_map + (function + | Positive (World.Apply (name, goal_bindings)) -> + Some + (name, Label.Map.map (Pattern.Subst.resolve subst) goal_bindings) + | _ -> None) + residue_goals + in + { bindings; residue } + in + let equal_residual (n, b) (m, c) = + String.equal n m && Label.Map.equal Pattern.equal b c in let equal_solution a b = - List.for_all2 (fun (_, p) (_, q) -> Pattern.equal p q) a b + List.for_all2 (fun (_, p) (_, q) -> Pattern.equal p q) a.bindings + b.bindings + && List.length a.residue = List.length b.residue + && List.for_all2 equal_residual a.residue b.residue in let solutions = List.fold_left - (fun acc subst -> - let solution = read subst in + (fun acc outcome -> + let solution = read outcome in if List.exists (equal_solution solution) acc then acc else acc @ [ solution ]) - [] substs + [] outcomes in Ok solutions end @@ -15,15 +15,28 @@ type error = | Non_total_plan of string list - (** No remaining goal is decidable; the relation names of the - stuck goals, for the message. *) + (** No remaining goal is decidable or residuatable; the + relation names of the stuck goals, for the message. *) val pp_error : Format.formatter -> error -> unit -(** One answer: each free variable of the query, resolved. Ground in - the common case; open exactly when the query admits any value - there. *) -type solution = (string * Pattern.t) list +(** A residual constraint: a membership goal that stayed + underdetermined. It is decidable the moment its variables are + ground; returning it is the honest answer to a satisfiable but + open query. Only builtin membership residuates; searches never + do. *) +type residual = string * Pattern.t Label.Map.t + +val pp_residual : Format.formatter -> residual -> unit +(** Prints the constraint as the proposition it is, [[Rel l: t ...]]. *) + +(** One answer: each free variable of the query resolved, plus the + residual constraints the answer is conditioned on. Ground and + residue-free in the common case. *) +type solution = { + bindings : (string * Pattern.t) list; + residue : residual list; +} module Make (W : World.WORLD) : sig val solve : W.t -> World.expr -> (solution list, error) result diff --git a/test/test_embedding.ml b/test/test_embedding.ml index 32effc2..ea55e4f 100644 --- a/test/test_embedding.ml +++ b/test/test_embedding.ml @@ -51,9 +51,11 @@ let solve source = let show solutions = solutions - |> List.map (fun solution -> - solution - |> List.map (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p) + |> List.map (fun { Sol.Vm.bindings; residue } -> + List.map + (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p) + bindings + @ List.map (Format.asprintf "%a" Sol.Vm.pp_residual) residue |> String.concat ",") |> String.concat "; " @@ -64,10 +66,19 @@ let test_kernel_scan () = | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error let test_kernel_totality () = - match solve {| [Integer value: X] |} with + match + solve + {| [ForAll variable: X quantifier: [Integer value: X] body: [True]] |} + with | Error (Sol.Vm.Non_total_plan _) -> () | Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard" +let test_kernel_residuation () = + match solve {| [Integer value: X] |} with + | Ok [ { Sol.Vm.residue = [ ("Integer", _) ]; _ } ] -> () + | Ok _ -> Alcotest.fail "open membership must residuate in the embedding too" + | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error + let () = Alcotest.run "sol-embedding" [ @@ -76,5 +87,7 @@ let () = Alcotest.test_case "scan over host relations" `Quick test_kernel_scan; Alcotest.test_case "totality guard survives embedding" `Quick test_kernel_totality; + Alcotest.test_case "residuation survives embedding" `Quick + test_kernel_residuation; ] ); ] diff --git a/test/test_vm.ml b/test/test_vm.ml index bf7ea35..83532d6 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -19,9 +19,11 @@ let run source = let show solutions = solutions - |> List.map (fun solution -> - solution - |> List.map (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p) + |> List.map (fun { Sol.Vm.bindings; residue } -> + List.map + (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p) + bindings + @ List.map (Format.asprintf "%a" Sol.Vm.pp_residual) residue |> String.concat ",") |> String.concat "; " @@ -154,13 +156,32 @@ let test_mutual_recursion_rejected () = | Error _ -> () | Ok _ -> Alcotest.fail "mutual recursion must be rejected" -let test_unbounded_membership_is_non_total_plan () = - match load {| Query expression: [Integer value: X] |} with +let test_unbounded_membership_residuates () = + (* Membership is not generation and not an error either: the + constraint comes back as the answer's condition. *) + check_answers "open membership residuates" + {| Query expression: [Integer value: X] |} "X=X,[Integer value: X]" + +let test_residue_discharged_by_binding () = + check_answers "a later equality grounds the membership" + {| Query expression: [Natural value: X] :and [Equal left: X right: 5] |} + "X=5" + +let test_residue_accumulates () = + check_answers "several open constraints residuate together" + {| Query expression: [Natural value: X] :and [GreaterThan left: X right: 5] |} + "X=X,[Natural value: X],[GreaterThan left: X right: 5]" + +let test_unbounded_search_still_rejected () = + match + load + (length_rules ^ {| Query expression: [Length list: L result: R] |}) + with | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error | Ok (world, [ query ]) -> ( match Sol.Vm.Standalone.solve world query with | Error (Sol.Vm.Non_total_plan _) -> () - | Ok _ -> Alcotest.fail "must be rejected as a non-total plan") + | Ok _ -> Alcotest.fail "an unbounded recursion must still be rejected") | Ok _ -> Alcotest.fail "expected one query" let test_domain_constrains_when_ground () = @@ -320,8 +341,14 @@ let () = test_fresh_variable_is_no_decrease; Alcotest.test_case "mutual recursion rejected" `Quick test_mutual_recursion_rejected; - Alcotest.test_case "unbounded membership rejected" `Quick - test_unbounded_membership_is_non_total_plan; + Alcotest.test_case "open membership residuates" `Quick + test_unbounded_membership_residuates; + Alcotest.test_case "residue discharged by binding" `Quick + test_residue_discharged_by_binding; + Alcotest.test_case "residue accumulates" `Quick + test_residue_accumulates; + Alcotest.test_case "unbounded search still rejected" `Quick + test_unbounded_search_still_rejected; Alcotest.test_case "membership once ground" `Quick test_domain_constrains_when_ground; Alcotest.test_case "fact domain violation" `Quick |