diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/virtual-machine-specification.org | 7 | ||||
| -rw-r--r-- | docs/vm.org | 29 |
2 files changed, 25 insertions, 11 deletions
diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org index c44b666..828bc3c 100644 --- a/docs/virtual-machine-specification.org +++ b/docs/virtual-machine-specification.org @@ -131,9 +131,10 @@ whole or not at all. Specified, not yet implemented; each grows admission or planning without changing admitted semantics: -- constraint propagation: residuated constraints today wait and - return; a store that actively narrows domains and detects - unsatisfiable residue early is the next strength; +- richer propagation: the interval store today reads domains and + one-sided comparisons; difference constraints between variables, + arithmetic relations, and propagation through record structure + are the next strengths; - symbolic discharge: algebraic evidence for universals over infinite domains, and arithmetic decrease measures for recursion that structural containment cannot see; 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 |