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