From aec83f0aac21e52ca2990e597c9875f9e18705d0 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 20:20:59 +0000 Subject: [PATCH] artdag: Phase 7 consumes lib/maude mau/confluent? (no bespoke confluence checker) The CID-stability check now calls mau/confluent? / mau/non-joinable-pairs from lib/maude/confluence.sx (merged in) instead of re-implementing critical-pair analysis inside lib/artdag. Picks up confluence.sx via the architecture merge. Co-Authored-By: Claude Opus 4.8 (1M context) --- plans/artdag-on-sx.md | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/plans/artdag-on-sx.md b/plans/artdag-on-sx.md index bfee934e..a7c5d25b 100644 --- a/plans/artdag-on-sx.md +++ b/plans/artdag-on-sx.md @@ -156,13 +156,18 @@ declaratively and prove it equivalent to the hand-written `optimize.sx`. - [ ] Equivalence: assert the maude-optimised DAG == `optimize.sx`'s output on the existing fixtures (same nodes, same content ids) — the rule set must cover at least the hand-written passes. -- [ ] Confluence / CID-stability check: a syntactic critical-pair / local- - confluence checker over the optimisation `eq`s — different rewrite orders must - reach the same normal form, else the optimiser is CID-unstable. Full - AC-unification is OUT OF SCOPE; check syntactic overlaps + joinability and use - `mau/canon` as the joinability oracle for AC laws. +- [ ] Confluence / CID-stability check: **consume `mau/confluent?` from + `lib/maude/confluence.sx`** — do NOT build your own checker. Assert the + optimisation rule module is confluent (`(mau/confluent? rules-module)` is + true) so different rewrite orders reach the same normal form and the optimised + pipeline's content id is stable. On failure, `mau/non-joinable-pairs` + + `mau/cp->str` name the offending critical pair (fix the rule set, e.g. add the + joining law — see the `f(a)=b,a=c` → add `f(c)=b` pattern). It is a syntactic + critical-pair checker (exact for free/constructor ops; AC overlaps under- + approximated but joined via canonical form) — that matches what this optimiser + needs. API also: `mau/critical-pairs`, `mau/joinable?`. - [ ] `lib/artdag/tests/maude-optimize.sx` — bridge round-trip, each law, - equivalence-with-`optimize.sx`, confluence of the rule set. + equivalence-with-`optimize.sx`, `(mau/confluent? rules-module)` holds. - [ ] (later) cost-directed choice among confluent-equivalent forms; (optional) miniKanren scheduling.