diff --git a/lib/artdag/conformance.sh b/lib/artdag/conformance.sh index 0d2924c6..84b96d13 100755 --- a/lib/artdag/conformance.sh +++ b/lib/artdag/conformance.sh @@ -35,13 +35,15 @@ run_suite() { (load "lib/maude/matching.sx") (load "lib/maude/conditional.sx") (load "lib/maude/fire.sx") +(load "lib/maude/confluence.sx") (load "lib/maude/rewrite.sx") (load "lib/maude/searchpath.sx") (load "lib/maude/strategy.sx") (load "lib/maude/meta.sx") (load "lib/maude/pretty.sx") (load "lib/maude/run.sx")' - BRIDGE_LOAD='(load "lib/artdag/maude-bridge.sx")' + BRIDGE_LOAD='(load "lib/artdag/maude-bridge.sx") +(load "lib/artdag/optimize-rules.sx")' fi cat > "$TMP" << EPOCHS (epoch 1) diff --git a/lib/artdag/optimize-rules.sx b/lib/artdag/optimize-rules.sx new file mode 100644 index 00000000..7262fca0 --- /dev/null +++ b/lib/artdag/optimize-rules.sx @@ -0,0 +1,69 @@ +; lib/artdag/optimize-rules.sx — Phase 7: optimisation laws as a confluent maude module. +; The optimised effect pipeline IS the normal form of the rule set, so confluence +; (mau/confluent?) is exactly content-id stability: every rewrite order reaches the +; same normal form. Media ops (blur/bright/id/over) are the opaque-op model from +; lib/maude/tests/effects.sx — the engine reasons about the pipeline algebra, never +; pixels. The radius algebra is an AC operator with identity 0 (unary 1s): Peano +; successor rules (s M + N = s(M+N), 0 + N = N) are NOT confluent here (the symbolic +; critical pairs M + 0 and (A+B)+C vs A+(B+C) stick), whereas [assoc comm id: 0] +; joins them via canonical form. maude (lib/maude) is a READ-ONLY consumed substrate: +; mau/parse-module, mau/creduce-term, mau/creduce->str, mau/ccanon, mau/confluent?, +; mau/non-joinable-pairs, mau/cp->str. + +(define + artdag/opt-module-src + (str + "fmod ARTDAGOPT is\n" + " sorts Img Num .\n" + " op 0 : -> Num .\n" + " op 1 : -> Num .\n" + " op _+_ : Num Num -> Num [assoc comm id: 0] .\n" + " op blur : Img Num -> Img .\n" + " op bright : Img Num -> Img .\n" + " op id : Img -> Img .\n" + " op over : Img Img -> Img [comm] .\n" + " vars I J : Img .\n" + " vars M N : Num .\n" + " eq id(I) = I .\n" + " eq blur(I, 0) = I .\n" + " eq bright(I, 0) = I .\n" + " eq blur(blur(I, M), N) = blur(I, M + N) .\n" + " eq bright(bright(I, M), N) = bright(I, M + N) .\n" + " eq over(I, I) = I .\n" + "endfm")) + +(define artdag/opt-module (mau/parse-module artdag/opt-module-src)) + +; ---- reduce a surface pipeline to its optimised normal form ---- + +(define + artdag/opt-reduce-term + (fn (src) (mau/creduce-term artdag/opt-module src))) + +(define + artdag/opt-normal-form + (fn (src) (mau/creduce->str artdag/opt-module src))) + +(define artdag/opt-canon (fn (src) (mau/ccanon artdag/opt-module src))) + +; two surface pipelines optimise to the same pipeline (=> same content id) iff +; their normal forms coincide. +(define + artdag/opt-same-form? + (fn (a b) (= (artdag/opt-normal-form a) (artdag/opt-normal-form b)))) + +; ---- confluence / content-id stability (consume lib/maude/confluence.sx) ---- + +(define artdag/opt-confluent? (fn () (mau/confluent? artdag/opt-module))) + +(define + artdag/opt-non-joinable + (fn () (mau/non-joinable-pairs artdag/opt-module))) + +(define + artdag/opt-non-joinable->strs + (fn + () + (map + (fn (cp) (mau/cp->str artdag/opt-module cp)) + (artdag/opt-non-joinable)))) diff --git a/lib/artdag/scoreboard.json b/lib/artdag/scoreboard.json index ce9ab602..1ed9c3ea 100644 --- a/lib/artdag/scoreboard.json +++ b/lib/artdag/scoreboard.json @@ -10,9 +10,9 @@ "serialize": {"pass": 13, "fail": 0}, "stats": {"pass": 12, "fail": 0}, "fault": {"pass": 14, "fail": 0}, - "maude-optimize": {"pass": 14, "fail": 0} + "maude-optimize": {"pass": 25, "fail": 0} }, - "total_pass": 172, + "total_pass": 183, "total_fail": 0, - "total": 172 + "total": 183 } diff --git a/lib/artdag/scoreboard.md b/lib/artdag/scoreboard.md index 14a9652f..d45acde2 100644 --- a/lib/artdag/scoreboard.md +++ b/lib/artdag/scoreboard.md @@ -14,5 +14,5 @@ _Generated by `lib/artdag/conformance.sh`_ | serialize | 13 | 0 | 13 | | stats | 12 | 0 | 12 | | fault | 14 | 0 | 14 | -| maude-optimize | 14 | 0 | 14 | -| **Total** | **172** | **0** | **172** | +| maude-optimize | 25 | 0 | 25 | +| **Total** | **183** | **0** | **183** | diff --git a/lib/artdag/tests/maude-optimize.sx b/lib/artdag/tests/maude-optimize.sx index 2f699150..38b12c56 100644 --- a/lib/artdag/tests/maude-optimize.sx +++ b/lib/artdag/tests/maude-optimize.sx @@ -110,3 +110,60 @@ (artdag/dag-id mo-diamond "a") (keys (artdag/dag-nodes mo-diamond-rt))) true) + +; ---- optimisation laws as a confluent maude module (optimize-rules.sx) ---- +; The optimised pipeline is the normal form; confluence => stable content id. + +(artdag-test "opt module is confluent" (artdag/opt-confluent?) true) + +(artdag-test + "opt module has no non-joinable critical pairs" + (len (artdag/opt-non-joinable)) + 0) + +(artdag-test + "law: identity elimination" + (artdag/opt-normal-form "id(src)") + "src") + +(artdag-test + "law: zero-radius blur is a no-op" + (artdag/opt-normal-form "blur(src, 0)") + "src") + +(artdag-test + "law: zero-radius bright is a no-op" + (artdag/opt-normal-form "bright(src, 0)") + "src") + +(artdag-test + "law: adjacent blur fusion adds radii" + (artdag/opt-normal-form "blur(blur(src, 1), 1)") + "blur(src, _+_(1, 1))") + +(artdag-test + "fusion normal form is rewrite-order stable" + (artdag/opt-same-form? + "blur(blur(blur(src, 1), 1), 1)" + "blur(blur(src, 1 + 1), 1)") + true) + +(artdag-test + "laws compose: id + no-op + fusion" + (artdag/opt-normal-form "bright(id(blur(blur(src, 1), 1)), 0)") + "blur(src, _+_(1, 1))") + +(artdag-test + "law: idempotent over dedup (CSE)" + (artdag/opt-normal-form "over(blur(src, 1), blur(src, 1))") + "blur(src, 1)") + +(artdag-test + "distinct over operands do not dedup" + (artdag/opt-same-form? "over(blur(src, 1), blur(src, 1 + 1))" "blur(src, 1)") + false) + +(artdag-test + "distinct pipelines stay distinct" + (artdag/opt-same-form? "blur(src, 1)" "bright(src, 1)") + false) diff --git a/plans/artdag-on-sx.md b/plans/artdag-on-sx.md index a7c5d25b..b6a4727e 100644 --- a/plans/artdag-on-sx.md +++ b/plans/artdag-on-sx.md @@ -31,7 +31,7 @@ edges. ## Status (rolling) -`bash lib/artdag/conformance.sh` → **172/172** (11 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize) +`bash lib/artdag/conformance.sh` → **183/183** (11 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize) Base roadmap (Phases 1–6) COMPLETE. Now extending. @@ -156,7 +156,7 @@ 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: **consume `mau/confluent?` from +- [x] 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 @@ -184,6 +184,26 @@ be an op token. ## Progress log +- **2026-06-19 Phase 7 — optimisation laws + confluence** (maude-optimize 25/25, + total 183/183). `lib/artdag/optimize-rules.sx`: the effect-pipeline optimisation + passes as a maude module `ARTDAGOPT` — `id(I)=I`, `blur(I,0)=I`, `bright(I,0)=I`, + adjacent fusion `blur(blur(I,M),N)=blur(I,M+N)` (+bright), idempotent + `over(I,I)=I`. Key result: the radius algebra is `_+_ [assoc comm id: 0]` (unary + `1`s), NOT Peano successor rules — the Peano version is non-confluent (6 + non-joinable critical pairs: `M+0` sticks, `(A+B)+C` vs `A+(B+C)` doesn't join), + whereas AC+id makes `(mau/confluent? artdag/opt-module)` true (0 non-joinable + pairs) by joining those overlaps via canonical form. So the optimised pipeline's + normal form — and hence its content id — is stable under any rewrite order. + `artdag/opt-normal-form`/`opt-reduce-term`/`opt-canon` reduce a surface pipeline; + `opt-same-form?` decides content-id equality; `opt-confluent?`/`opt-non-joinable` + /`opt-non-joinable->strs` consume `lib/maude/confluence.sx` (loaded into the + maude-optimize suite). Tests: confluence holds, every law fires, fusion is + rewrite-order stable, laws compose, dedup vs no-dedup, distinct pipelines stay + distinct. Gotcha: compare reduced *strings* (`mau/creduce->str`) — canon term + objects compare unequal under `=` even when the printed normal form is identical. + Remaining Phase 7: bridge the maude normal form back to a runnable DAG + + equivalence-with-`optimize.sx`. + - **2026-06-07 Phase 7 — maude-bridge** (maude-optimize suite 14/14, total 172/172). `lib/artdag/maude-bridge.sx`: lossless adapter between an artdag effect DAG and a maude term. `artdag/dag->term dag id` walks from a sink, emitting `(mau/app op