diff options
Diffstat (limited to 'docs/core-design-and-pipeline.org')
| -rw-r--r-- | docs/core-design-and-pipeline.org | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org index 9e085f8..823a24e 100644 --- a/docs/core-design-and-pipeline.org +++ b/docs/core-design-and-pipeline.org @@ -107,15 +107,17 @@ meaning; the =WORLD= functor is the seam it plugs into. What the implementation enforces today is rung one and part of rung two of the ladder in decision 10: -- structural decrease on self recursive rules, with the witness - demanded ground at unfolding; +- lexicographic structural decrease across call graph components, + with every measure position demanded ground at unfolding; self + recursion and mutual recursion are the same check; - bounded enumeration through =Between=; -- decidable negation and universals only over decidable quantifiers. +- decidable negation and universals only over decidable quantifiers; +- residuation: open membership returns as residual constraints + instead of failing the plan. Not yet present: symbolic discharge (algebraic proof of universals -over infinite domains), Rocq certificates as admission evidence, -mutual recursion under a lexicographic measure, and a constraint -store that residuates instead of rejecting. Each arrives as a +over infinite domains), Rocq certificates as admission evidence, and +active constraint propagation over residue. Each arrives as a strengthening of admission or planning; none changes the semantics of what is already admitted. |