diff options
Diffstat (limited to 'docs/vm.org')
| -rw-r--r-- | docs/vm.org | 11 |
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 |