residuation: open membership returns residual constraints

1 files changed, 8 insertions, 3 deletions

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