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/vm.org | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'docs/vm.org') diff --git a/docs/vm.org b/docs/vm.org index 4253231..8d1215a 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -56,9 +56,14 @@ decidable wait. So conjunction stays commutative in fact, not just in doctrine: the page order of =:and= operands never matters, and the tests assert it. -If no remaining goal can ever run, the plan is rejected as non -total. =[Integer value: X]= alone is not an enumeration, it is an -error telling you to bind or bound =X=. Membership is not generation. +When goals remain that cannot run, two things can happen. If every +one of them is pure membership, decidable the moment its variables +ground, the answer comes back with those goals as residual +constraints: =[Integer value: X]= alone answers =X= conditioned on +=[Integer value: X]=, which is exactly what the expression means. +Constraining is not searching. If any remaining goal is a stalled +search, an unbounded recursion or an infinite universal, the plan is +rejected as non total. Membership is never generation either way. Recursive rules unfold only when their witness argument is ground, so the admission proof becomes a runtime termination measure: the -- cgit v1.2.3