interval propagation: contradictions fail, finite ranges enumerate

1 files changed, 21 insertions, 8 deletions

diff --git a/docs/vm.org b/docs/vm.org
index 87c0ca0..446cee2 100644
--- a/docs/vm.org
+++ b/docs/vm.org
@@ -59,14 +59,27 @@ 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.
 
-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.
+When goals remain that cannot run, the engine first propagates over
+the waiting membership constraints as one interval store. Bounds
+with an empty intersection fail the branch outright: =X > 5= with
+=X < 3= answers no, not a conditioned maybe, and so does asking one
+value to be both an integer and a string. An integer variable
+squeezed into a finite range converts to bounded generation:
+=[Natural value: X] :and [LessThan left: X right: 4]= enumerates 0
+through 3, the same admissible enumeration =Between= performs
+explicitly, because the combination of constraints is a finite
+relation. This is Sakura's cardinality analysis working inside the
+engine.
+
+If propagation finds neither a contradiction nor a finite range, two
+things can happen. If every waiting goal 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