diff options
Diffstat (limited to '')
| -rw-r--r-- | docs/core-design-and-pipeline.org | 17 | ||||
| -rw-r--r-- | docs/virtual-machine-specification.org | 7 | ||||
| -rw-r--r-- | docs/vm.org | 16 |
3 files changed, 27 insertions, 13 deletions
diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org index 823a24e..c81b58a 100644 --- a/docs/core-design-and-pipeline.org +++ b/docs/core-design-and-pipeline.org @@ -111,13 +111,18 @@ two of the ladder in decision 10: 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 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, and -active constraint propagation over residue. Each arrives as a + instead of failing the plan; +- interval propagation over residue: contradictions fail, finite + integer ranges enumerate; +- symbolic discharge, first fragment: universals over infinite + domains decided by kind inclusion and interval entailment, with + refutations backed by counterexamples. + +Not yet present: symbolic discharge beyond the interval fragment +(algebraic identities of relations, arithmetic decrease measures) +and Rocq certificates as admission evidence. 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 828bc3c..f84bc84 100644 --- a/docs/virtual-machine-specification.org +++ b/docs/virtual-machine-specification.org @@ -135,9 +135,10 @@ without changing admitted semantics: one-sided comparisons; difference constraints between variables, arithmetic relations, and propagation through record structure are the next strengths; -- symbolic discharge: algebraic evidence for universals over - infinite domains, and arithmetic decrease measures for recursion - that structural containment cannot see; +- symbolic discharge beyond the interval fragment: algebraic + identities of relations (universals mentioning =Plus= and kin), + and arithmetic decrease measures for recursion that structural + containment cannot see; - Rocq certificates as admission evidence, and extraction of the lexicographic search itself (the containment core is already extracted); diff --git a/docs/vm.org b/docs/vm.org index 446cee2..a51b85a 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -96,10 +96,18 @@ open goals cannot happen. =Exists= lowers to a conjunction at loading, since query variables are existential already; its =variable:= is renamed apart so the scope cannot be forged. =ForAll= runs when its quantifier is -decidable: every solution of the quantifier must satisfy the body. A -universal over an infinite domain is a non total plan, rejected, as -decision 10 requires. Variables that live only under a universal are -not answer variables. +decidable: every solution of the quantifier must satisfy the body. +Variables that live only under a universal are not answer variables. + +A universal over an infinite domain is never enumerated. It gets one +chance at symbolic discharge: when quantifier and body both read as +kind and interval constraints over the quantified variable, the +engine decides entailment algebraically. Every natural is at least +zero: proven. Not every integer is: refuted, and the refutation is +backed by a concrete counterexample. Every integer is a rational: +proven, which is decision 12's subtype inclusion decided +symbolically. A universal outside that fragment is a non total plan, +rejected, as decision 10 requires. * Membership criteria as domains |