diff options
Diffstat (limited to '')
| -rw-r--r-- | docs/virtual-machine-specification.org | 14 |
1 files changed, 8 insertions, 6 deletions
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 |