From 726f3dfb116ec9265041e642000612831633fe3c Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 23:39:40 -0300 Subject: mutual recursion admitted under lexicographic measures --- docs/core-design-and-pipeline.org | 14 ++++++++------ docs/virtual-machine-specification.org | 14 ++++++++------ docs/vm.org | 15 +++++++++------ 3 files changed, 25 insertions(+), 18 deletions(-) (limited to 'docs') 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 -- cgit v1.2.3