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/virtual-machine-specification.org | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'docs/virtual-machine-specification.org') 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 -- cgit v1.2.3