From 0886f3c71cf8551e4f8b3726654003a4f29645f0 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 22:12:53 -0300 Subject: residuation: open membership returns residual constraints --- docs/virtual-machine-specification.org | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) (limited to 'docs/virtual-machine-specification.org') 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; -- cgit v1.2.3