coop/rose-ash
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

artdag: Phase 7 cost-directed opt-improvement/opt-cheaper? + 5 tests

Browse Source 
artdag/opt-improvement compares the original output cone (dce to id) vs the
maude-reduced DAG under an injected cost-fn, returning before/after total-work and
critical-path. opt-cheaper? asserts optimisation never increases cost: the 5-node
chain drops to 2 (work 5->2, path 5->2) and stays cheaper under radius-weighted cost
(5->3); over dedup and untouched DAGs are never pessimised. Consumes cost.sx. Phase 7
base + (later) cost box done. maude-optimize 38/38, total 196/196.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
giles
2026-06-19 13:57:13 +00:00
parent 81cba2cb52
commit d7bb3303f8
5 changed files with 80 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
plans/artdag-on-sx.md
View File

@@ -31,7 +31,7 @@ edges.
## Status (rolling)
`bash lib/artdag/conformance.sh` → **191/191** (11 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize)
`bash lib/artdag/conformance.sh` → **196/196** (11 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize)
Base roadmap (Phases 1–6) COMPLETE. Now extending.
@@ -172,7 +172,10 @@ declaratively and prove it equivalent to the hand-written `optimize.sx`.
needs. API also: `mau/critical-pairs`, `mau/joinable?`.
- [x] `lib/artdag/tests/maude-optimize.sx` — bridge round-trip, each law,
result-preserving equivalence, `(mau/confluent? rules-module)` holds (33 tests).
- [ ] (later) cost-directed choice among confluent-equivalent forms; (optional)
- [x] cost-directed: `artdag/opt-improvement`/`opt-cheaper?` compare the optimised
cone vs the original cone under an injected `cost-fn` — optimisation is never a
pessimisation (fewer nodes + fused ops ⇒ total-work and critical-path never
increase, under const and radius-weighted costs). (optional, not pursued)
miniKanren scheduling.
maude is a READ-ONLY consumed substrate (like datalog/persist) — load it, don't
@@ -188,6 +191,18 @@ be an op token.
## Progress log
- **2026-06-19 Phase 7 — cost-directed: optimisation is never a pessimisation**
(maude-optimize 38/38, total 196/196). `artdag/opt-improvement dag id cost-fn` compares
the original output cone (`artdag/dce` to `id`) against the maude-reduced DAG under an
injected `cost-fn (op params)` — returns `{:before :after :before-path :after-path
:optimized}` (total-work + critical-path each side). `artdag/opt-cheaper?` asserts
`after <= before`. Under monotone per-node costs the optimised DAG never costs more:
the 5-node chain drops to 2 (const work 5→2, critical path 5→2) and stays cheaper under
a radius-weighted cost (5→3 — one `blur(M+N)` costs the same as the two it replaces);
the `over` dedup and an untouched DAG are both `opt-cheaper?`. Consumes `cost.sx`'s
`total-work`/`critical-path`. Phase 7 base + the "(later)" cost box now done; only the
optional miniKanren scheduling remains.
- **2026-06-19 Phase 7 — opt-reduce: bridge normal form back to a DAG** (maude-optimize
33/33, total 191/191). `artdag/opt-reduce dag id`: encode the DAG cone at `id` into an
opt-term (`artdag/dag->opt-term` — leaves→nullary const, `:radius` nodes→`op(inputs…,