Merge loops/artdag into architecture: artdag Phase 7 (maude rule-based optimization)
Content-addressed DAG engine Phase 7 complete (198/198): maude-bridge (lossless dag<->term), optimize-rules.sx (confluent ARTDAGOPT module — id/no-op/fusion/dedup laws, AC radius algebra, consumes mau/confluent?), opt-reduce (encode->creduce->decode result-preserving optimised DAG), cost-directed opt-cheaper?, non-vacuous confluence gate. Brings in lib/maude if not already present. Additive, conflict-free. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -20,8 +20,9 @@ the same SX substrates already serve the phases:
|
||||
- **Execute** (composable effects + content-addressed memo) → SX's own
|
||||
`perform`/`cek-resume` + a **persist**-backed content-addressed result cache;
|
||||
incremental recompute drops the cost of re-rendering to the dirty subgraph.
|
||||
- **Optimize** (fuse/dedup effect pipelines) → term rewriting (a later, optional
|
||||
consumer of `maude-on-sx`'s engine — see `plans/maude-on-sx.md`).
|
||||
- **Optimize** (fuse/dedup effect pipelines) → term rewriting, the declarative
|
||||
consumer of `maude-on-sx`'s engine — now ACTIVE as Phase 7 (lib/maude is on
|
||||
this branch; fit proven in `lib/maude/tests/effects.sx`).
|
||||
|
||||
End-state: a content-addressed dataflow engine in `lib/artdag/` with analyze, plan,
|
||||
incremental execute, effect-pipeline optimization, and a shared-cache federation
|
||||
@@ -30,9 +31,27 @@ edges.
|
||||
|
||||
## Status (rolling)
|
||||
|
||||
`bash lib/artdag/conformance.sh` → **158/158** (10 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault)
|
||||
`bash lib/artdag/conformance.sh` → **198/198** (11 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize)
|
||||
|
||||
Base roadmap (Phases 1–6) COMPLETE. Now extending.
|
||||
Base roadmap (Phases 1–6) COMPLETE + Phase 7 (maude rule-based optimization) COMPLETE
|
||||
(only optional miniKanren scheduling remains). Now hardening only.
|
||||
|
||||
## Integration / merge status (2026-06-28)
|
||||
|
||||
**READY TO MERGE `loops/artdag` → `architecture`.** `origin/architecture`'s `lib/artdag/`
|
||||
is stale — it predates the maude-bridge, so it is missing ALL of Phase 7
|
||||
(`maude-bridge.sx` + `optimize-rules.sx` both absent). `loops/artdag` is 9 commits ahead
|
||||
of `origin/architecture` (the Phase 7 chain `657d8061..4a02a9c4` + the architecture-merge
|
||||
`7f7957ba` that pulled in `lib/maude`). Merge facts:
|
||||
- **Dependency satisfied on target:** Phase 7 consumes `lib/maude` (incl. `confluence.sx`),
|
||||
already on architecture (`0963aa51`); this branch re-absorbed it at `7f7957ba`.
|
||||
- **Conflict-free for artdag files:** `origin/architecture` is an ancestor of HEAD and the
|
||||
branch already absorbed architecture, so `lib/artdag/**` + this plan are purely additive.
|
||||
- **Target is LOCAL architecture** (146 ahead of `origin/architecture`, which is kept
|
||||
deliberately stale), matching how other loops landed.
|
||||
- **Pushed (2026-06-28):** `loops/artdag` is now on `origin` through `cd2ad707` (credential
|
||||
restored). It is 10 commits ahead of `origin/architecture`. A maintainer does the merge
|
||||
(the loop agent must NOT touch `architecture` itself).
|
||||
|
||||
## Ground rules
|
||||
|
||||
@@ -124,8 +143,7 @@ lib/artdag/optimize.sx lib/artdag/federation.sx
|
||||
- [x] optimizations are content-id-preserving where semantically identical; assert
|
||||
the optimized DAG produces identical results
|
||||
- [x] `lib/artdag/tests/optimize.sx` — DCE, CSE dedup, fusion equivalence
|
||||
- [ ] (optional/later) rule-based optimization via `maude-on-sx`'s rewriting engine —
|
||||
flag the integration point, don't block on it
|
||||
- [x] (superseded by Phase 7) integration point flagged
|
||||
|
||||
## Phase 6 — Federation (shared content-addressed cache)
|
||||
|
||||
@@ -136,8 +154,129 @@ lib/artdag/optimize.sx lib/artdag/federation.sx
|
||||
- [x] revocation/invalidation — drop a remote result if its provenance is withdrawn
|
||||
- [x] `lib/artdag/tests/fed.sx` — remote cache hit, trust gating, invalidation
|
||||
|
||||
## Phase 7 — Rule-based optimization via maude-on-sx (ACTIVE — start here)
|
||||
|
||||
`lib/maude/` is now present on this branch (term rewriting modulo assoc/comm/id;
|
||||
262 tests). The fit is PROVEN — see `lib/maude/tests/effects.sx`: artdag's
|
||||
optimise passes (fusion, no-op/dead-op elim, identity elim, CSE/idempotent
|
||||
dedup) expressed as equations, where the optimised pipeline IS the normal form
|
||||
and confluence ⇒ a stable content id. Reimplement Phase-5 optimisation
|
||||
declaratively and prove it equivalent to the hand-written `optimize.sx`.
|
||||
|
||||
- [x] `lib/artdag/maude-bridge.sx` — adapter between an effect DAG node and a
|
||||
maude term: `(op, sorted-input-ids, params)` ⟷ `(mau/app op (args...))`.
|
||||
Params become constant subterms; for commutative ops use a maude AC operator
|
||||
so input order is irrelevant (mirror the content-id's order-insensitivity).
|
||||
Round-trip `dag→term→dag` must be identity on canonical form.
|
||||
- [x] `lib/artdag/optimize-rules.sx` — the optimisation laws as a maude module
|
||||
(fusion / identity / no-op / dedup), one `eq` per law; `mau/creduce` the term,
|
||||
bridge the normal form back to a DAG (`artdag/opt-reduce`: dag→opt-term→creduce→
|
||||
decode→`artdag/build`).
|
||||
- [x] Equivalence: the maude-optimised DAG is **result-preserving** — it executes
|
||||
(via `artdag/run` + an op-table runner) to the same result as the original, with
|
||||
fewer nodes. NB: maude's fusion uses a *smaller* normal form (`blur(I, M+N)`) than
|
||||
`optimize.sx`'s `artdag/pipeline` stage nodes, so structural identity with
|
||||
`optimize.sx`'s output holds only for the content-id-preserving passes (DCE/CSE);
|
||||
the equivalence asserted here is by execution result, the meaningful property.
|
||||
- [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
|
||||
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?`.
|
||||
- [x] `lib/artdag/tests/maude-optimize.sx` — bridge round-trip, each law,
|
||||
result-preserving equivalence, `(mau/confluent? rules-module)` holds (33 tests).
|
||||
- [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
|
||||
edit it. Entry points: `mau/parse-module`, `mau/creduce`/`mau/creduce->str`,
|
||||
`mau/canon`/`mau/ac-equal?`, `mau/term->maude`, `mau/app`/`mau/const`/`mau/var`
|
||||
+ accessors. Load order: see `lib/maude/conformance.conf` PRELOADS.
|
||||
Gotchas (from building it): `id:` affects matching/canon only, not auto-
|
||||
reduction — write explicit identity `eq`s or read `mau/canon`; `mau/match-all`/
|
||||
`search` enumerate ALL matches (exponential on many identical AC args — keep
|
||||
rule sets small + confluent), single-step rewriting is short-circuit and fast;
|
||||
juxtaposition `__`/multi-`_` mixfix unparsed (use explicit infix ops); `.` can't
|
||||
be an op token.
|
||||
|
||||
## Progress log
|
||||
|
||||
- **2026-06-19 Phase 7 — confluence gate is non-vacuous** (maude-optimize 40/40, total
|
||||
198/198). Added a regression proving `mau/confluent?` actually discriminates: the
|
||||
Peano-arithmetic variant of the same laws (`0 + N = N`, `s M + N = s(M+N)` instead of
|
||||
`_+_ [assoc comm id: 0]`) is asserted **non-confluent** with named non-joinable pairs,
|
||||
so the green "opt module is confluent" is real evidence, not a checker that rubber-stamps
|
||||
everything. Documents the exact AC-vs-Peano design choice as an executable contrast.
|
||||
|
||||
- **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…,
|
||||
unary-Num)`, `over`→the comm op), `mau/creduce` it against `artdag/opt-module`, decode
|
||||
the normal form back to build-entries (`artdag/opt-term->entries`, counting `1`s for
|
||||
the radius) and `artdag/build` — content-ids recomputed, shared subterms re-collapse.
|
||||
Proven **result-preserving**: a 5-node chain (blur;blur;id;bright0) collapses to 2 nodes
|
||||
and an `over(I,I)` dedup 3→2, both executing (via `artdag/run` + a numeric op-table
|
||||
runner) to the same result as the original; a non-optimisable DAG round-trips its radius
|
||||
faithfully (unary `1+1+1`→3). Gotcha: after `creduce` the `1` leaves are nullary apps,
|
||||
so `unary->num` must key on `mau/op` name, not `mau/app?`. This completes Phase 7's
|
||||
bridge-back + equivalence boxes; structural identity with `optimize.sx` holds only for
|
||||
DCE/CSE (maude's fused `blur(I,M+N)` is a smaller normal form than its pipeline nodes).
|
||||
|
||||
- **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
|
||||
input-terms ++ meta)` per node; the trailing `artdag:meta` subterm carries params
|
||||
(a `write-to-string` token) + a commutativity flag, so no side table is needed.
|
||||
`artdag/term->dag` synthesizes build-entries (names `mb0…`) and re-runs
|
||||
`artdag/build`, which recomputes content-ids (name-independent) and re-collapses
|
||||
shared subterms — so `artdag/mb-roundtrip` is the identity on canonical form:
|
||||
sink id, op, params, and the full node survive; commutative ids stay
|
||||
order-insensitive; a diamond's shared node de-duplicates back to one (4→4).
|
||||
Maude entry points used: `mau/app`/`mau/const`/`mau/op`/`mau/args`/`mau/app?`.
|
||||
`conformance.sh` now gates the maude PRELOADS + bridge load to the maude-optimize
|
||||
suite (other suites stay maude-free). Gotcha: `write-to-string`/`read` round-trips
|
||||
keyword dicts but may reorder keys — fine, dicts compare structurally with `=`.
|
||||
|
||||
- **Ext: public API facade** (`lib/artdag/api.sx`, total 158/158 unchanged).
|
||||
Reference index matching the datalog/persist convention: canonical load order +
|
||||
the full public surface across all 10 modules + `artdag/version`.
|
||||
@@ -253,4 +392,9 @@ lib/artdag/optimize.sx lib/artdag/federation.sx
|
||||
|
||||
## Blockers
|
||||
|
||||
(none)
|
||||
- ~~**Push to `origin/loops/artdag` unavailable**~~ — RESOLVED 2026-06-28: credential
|
||||
restored in `~/.git-credentials`, push works; `loops/artdag` pushed through `cd2ad707`.
|
||||
- **sx-tree edit tools raise yojson `"Expected string, got null"` in this worktree**
|
||||
(`sx_insert_near`/`sx_replace_*`/`sx_insert_child`). Only `sx_write_file` works for
|
||||
writes; assemble the full file and `sx_write_file` (or `cp` a prepared file +
|
||||
`sx_validate`). Same gotcha logged in the content/dream loops.
|
||||
|
||||
@@ -62,44 +62,73 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
|
||||
## Roadmap
|
||||
|
||||
### Phase 1 — Parser + signatures
|
||||
- [ ] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations.
|
||||
- [ ] Sort hierarchy with subsort relations.
|
||||
- [ ] Operator overloading by arity + sort.
|
||||
- [ ] Tests: parse classic examples (peano nat, list of naturals).
|
||||
- [x] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations.
|
||||
- [x] Sort hierarchy with subsort relations.
|
||||
- [x] Operator overloading by arity + sort.
|
||||
- [x] Tests: parse classic examples (peano nat, list of naturals).
|
||||
|
||||
### Phase 2 — Syntactic equational reduction
|
||||
- [ ] Apply equations left-to-right until no equation matches.
|
||||
- [ ] Standard pattern matching (no equational theories yet — strict syntactic match).
|
||||
- [ ] Tests: peano arithmetic, list manipulation, propositional logic simplifier.
|
||||
- [x] Apply equations left-to-right until no equation matches.
|
||||
- [x] Standard pattern matching (no equational theories yet — strict syntactic match).
|
||||
- [x] Tests: peano arithmetic, list manipulation, propositional logic simplifier.
|
||||
|
||||
### Phase 3 — Equational matching (assoc / comm / id)
|
||||
- [ ] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups).
|
||||
- [ ] Handle `comm` (try both argument orderings).
|
||||
- [ ] Handle `id: e` (X * e ≡ X).
|
||||
- [ ] Combinations: `assoc comm id` together.
|
||||
- [ ] Returns *all* matches, not just first — caller drives.
|
||||
- [ ] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations).
|
||||
- [x] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups).
|
||||
- [x] Handle `comm` (try both argument orderings).
|
||||
- [x] Handle `id: e` (X * e ≡ X).
|
||||
- [x] Combinations: `assoc comm id` together.
|
||||
- [x] Returns *all* matches, not just first — caller drives.
|
||||
- [x] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations).
|
||||
|
||||
### Phase 4 — Conditional equations
|
||||
- [ ] `ceq L = R if Cond` — apply only when `Cond` reduces to true.
|
||||
- [ ] Recursion via the same reduce engine (terminating because Cond is shorter).
|
||||
- [ ] Tests: gcd, sorting, conditional simplifications.
|
||||
- [x] `ceq L = R if Cond` — apply only when `Cond` reduces to true.
|
||||
- [x] Recursion via the same reduce engine (terminating because Cond is shorter).
|
||||
- [x] Tests: gcd, sorting, conditional simplifications.
|
||||
|
||||
### Phase 5 — System modules + rewrite rules
|
||||
- [ ] `mod ... endm` syntax with `rl` rules.
|
||||
- [ ] Rules apply asymmetrically (`=>` not `=`); fairness across rules.
|
||||
- [ ] Default strategy: top-down, leftmost-outermost, first applicable rule.
|
||||
- [ ] Tests: state-transition systems (puzzle solvers, protocol simulators).
|
||||
- [x] `mod ... endm` syntax with `rl` rules.
|
||||
- [x] Rules apply asymmetrically (`=>` not `=`); fairness across rules.
|
||||
- [x] Default strategy: top-down, leftmost-outermost, first applicable rule.
|
||||
- [x] Tests: state-transition systems (puzzle solvers, protocol simulators).
|
||||
|
||||
### Phase 6 — Strategy language
|
||||
- [ ] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point.
|
||||
- [ ] User-named strategies; strategy expressions as values.
|
||||
- [ ] Tests: programs whose meaning depends on strategy choice.
|
||||
- [x] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point.
|
||||
- [x] User-named strategies; strategy expressions as values.
|
||||
- [x] Tests: programs whose meaning depends on strategy choice.
|
||||
|
||||
### Phase 7 — Reflection (META-LEVEL)
|
||||
- [ ] Terms-as-data: `META-LEVEL` lets you encode/decode terms as Maude terms.
|
||||
- [ ] Build proofs / programs that manipulate Maude programs.
|
||||
- [ ] Tests: meta-circular interpretation, generic theorem helpers.
|
||||
- [x] Terms-as-data: `META-LEVEL` lets you encode/decode terms as Maude terms.
|
||||
- [x] Build proofs / programs that manipulate Maude programs.
|
||||
- [x] Tests: meta-circular interpretation, generic theorem helpers.
|
||||
|
||||
### Extensions (post-roadmap, toward the end-state goal)
|
||||
- [x] Mixfix surface-syntax printer (`lib/maude/pretty.sx`) — `mau/term->maude`
|
||||
renders the internal prefix form back as Maude mixfix (`((s X) + 0)`),
|
||||
driven by op forms; `mau/red->maude` / `mau/rew->maude`. 11 tests.
|
||||
- [x] Program runner (`lib/maude/run.sx`) — `mau/run-program` / `mau/run` parse
|
||||
a module plus trailing `reduce`/`red`/`rewrite`/`rew TERM .` commands
|
||||
(`... in MOD : TERM` qualifier accepted) and execute them, rendering results
|
||||
in surface syntax. Runs an idiomatic `.maude` file end-to-end. Now also:
|
||||
`search START =>* GOAL .` command (reports the path), least-sort annotated
|
||||
output via `mau/run-pretty` → `result SORT: TERM` (Maude-style). 10 tests.
|
||||
- [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` /
|
||||
`mau/search-length` return the shortest sequence of states start..goal (the
|
||||
solution moves), not just yes/no. 8 tests.
|
||||
- [x] Order-sorted least-sort inference (`lib/maude/sorts.sx`) — `mau/term-sort`
|
||||
computes the least sort of a term: the smallest result sort among the op
|
||||
declarations whose argument sorts the actual args satisfy (modulo subsorting),
|
||||
so an overloaded `f(1)` is `NzNat` but `f(s 0)` is `Nat`. `mau/has-sort?`
|
||||
for membership-style checks. Answers the plan's substrate question — order-
|
||||
sorted signatures fit cleanly. 14 tests.
|
||||
- [x] `gather` / parse-time associativity — infix ops parse left (default,
|
||||
`(E e)`) or right (`(e E)`) per the gather attr, so cons `_:_ [gather (e E)]`
|
||||
reads `a : b : c` as right-nested. Full insertion sort now runs over BARE cons
|
||||
lists (no parens). 7 tests.
|
||||
- [x] `owise` equations — parser now reads trailing eq attributes
|
||||
(`eq L = R [owise] .`), `mau/split-attrs`; `mau/crewrite-top` is two-pass
|
||||
(ordinary equations first, owise last), so an owise catch-all fires only when
|
||||
nothing else applies, regardless of declaration order. Parser also reads
|
||||
`label`/`prec`/`owise`/`id:` eq+op attrs. 8 tests.
|
||||
|
||||
### Phase 8 — Propose `lib/guest/rewriting/`
|
||||
- [ ] Extract equational matching engine (the most reusable piece).
|
||||
@@ -107,6 +136,49 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
|
||||
- [ ] Extract strategy combinators.
|
||||
- [ ] Wait for second consumer before extracting.
|
||||
|
||||
**Status: BLOCKED — no second consumer yet.** The reusable core is identified:
|
||||
`lib/maude/matching.sx` (AC matching + canon) + `lib/maude/fire.sx`
|
||||
(short-circuit firing) are the prime extraction candidates; `lib/maude/strategy.sx`
|
||||
(combinators) is the third. Keep them separable. Do not extract until a Pure/
|
||||
CafeOBJ/term-rewriting playground consumer appears (or artdag-on-sx's effect
|
||||
optimiser, per the chisel note).
|
||||
|
||||
### SATURATION (post-roadmap)
|
||||
|
||||
All 7 roadmap phases + 7 extensions (pretty / run / search-path / owise /
|
||||
gather / order-sorted least-sort / search-command + result-sort) DONE, **254/254
|
||||
across 13 suites.** The end-state goal — a faithful Maude 3 functional+system
|
||||
core that runs idiomatic programs and proves equational identities — is met:
|
||||
sorts/subsorts/overloading, equational reduction modulo assoc/comm/id,
|
||||
conditional eqs + owise, system rules (rew + BFS search with witness paths),
|
||||
a strategy language, and META-LEVEL reflection, with a mixfix surface printer
|
||||
and an end-to-end `.maude` runner (reduce/rewrite/search commands, sort-annotated
|
||||
output). **artdag-on-sx fit prototype (lib/maude/tests/effects.sx, 8 tests):** artdag's
|
||||
optimise passes — adjacent-op fusion, no-op/dead-op elim, identity elim,
|
||||
CSE/idempotent dedup — expressed as `eq`s; the optimised pipeline IS the normal
|
||||
form, and confluence ⇒ a stable content id. This is the "second consumer"
|
||||
spike: it justifies a maude-driven optimiser in `lib/artdag` and the eventual
|
||||
`lib/guest/rewriting/` extraction. Faithfulness note surfaced: `id:` only
|
||||
affects matching/canon, NOT auto-reduction — write explicit identity eqs (or
|
||||
read off the canonical form) if you need `0 + N` to reduce in the term itself.
|
||||
|
||||
**Confluence / critical-pair checking (lib/maude/confluence.sx, 12 tests):**
|
||||
`mau/confluent?` answers the plan's substrate question "can confluence be
|
||||
checked." Two-sided syntactic unification (`mau/u-unify`, with occurs check) →
|
||||
critical pairs from LHS overlaps (`mau/critical-pairs`) → joinability via
|
||||
`mau/ac-equal?` of the normal forms (`mau/non-joinable-pairs` gives the
|
||||
diagnostics, `mau/cp->str` renders `left <?> right`). Caught `f(a)=b, a=c` as
|
||||
non-confluent (`b <?> f(c)`); confirmed peano/idempotent/AC examples confluent.
|
||||
SCOPE: unification is SYNTACTIC — exact for free/constructor ops, an
|
||||
under-approximation for AC overlaps (full AC-unification is NP/infinitary, out
|
||||
of scope), but joinability uses the AC-canonical form so AC laws still join
|
||||
correctly. This is the CID-stability oracle for the artdag optimiser: an
|
||||
optimisation rule set is content-id-stable iff `mau/confluent?` holds.
|
||||
|
||||
Pacing down to hardening. Possible niche future work: membership
|
||||
axioms (`mb`/`cmb`), critical-pair / confluence checking, meta-search, full
|
||||
mixfix (multi-`_` ops, juxtaposition `__`).
|
||||
|
||||
## lib/guest feedback loop
|
||||
|
||||
**Consumes:** `core/lex`, `core/pratt`, `core/ast`, `core/match` (with proposed extension for equational matching).
|
||||
@@ -125,7 +197,129 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
|
||||
- Pure language (Albrecht Gräf): https://agraef.github.io/pure-lang/ — practical functional rewriting.
|
||||
|
||||
## Progress log
|
||||
_(awaiting Phase 1 — depends on substrate matching maturity from lib/guest/core/match.sx)_
|
||||
|
||||
- **Phase 1 (parser + signatures) — DONE, 65/65.** `lib/maude/term.sx` (term
|
||||
repr: var/app dicts, equality, vars, `term->str`) + `lib/maude/parser.sx`
|
||||
(whitespace+bracket tokenizer with `---`/`***` comments; mixfix
|
||||
classification by splitting op names on `_`; precedence-climbing term parser
|
||||
over a pratt table built from op decls; `fmod`/`mod` modules with
|
||||
sorts/subsorts/ops/vars/eqs/rules). Consumes `lib/guest/lex.sx` (ws classes)
|
||||
and `lib/guest/pratt.sx` (op-table lookup). Verified on Peano (`s X + Y`
|
||||
parses `_+_(s_(X), Y)` — prefix binds tighter than infix) and NatList
|
||||
(transitive subsorts NzNat<Nat<List; `_;_` overloaded; `id: nil` / `prec`
|
||||
attrs). ceq/rl/crl parsed structurally (cond split on `if`, label in `[..]`).
|
||||
Suite + conformance driver wired (`lib/maude/conformance.{conf,sh}`, MODE=dict).
|
||||
- Notes for next phases: terms are `{:t :app :op N :args (...)}` /
|
||||
`{:t :var :name N :sort S}`; module carries a `:grammar` so
|
||||
`mau/parse-term-in` can parse term strings against its op table. Overloading
|
||||
is recorded but NOT resolved at parse time (resolve at reduce time).
|
||||
|
||||
- **Phase 2 (syntactic reduction) — DONE, 91/91 total.** `lib/maude/reduce.sx`:
|
||||
one-sided syntactic matching (`mau/match` — pattern vars only, non-linear
|
||||
patterns checked by bound-var equality), immutable substitutions via `assoc`,
|
||||
`mau/subst-apply`, top rewrite `mau/rewrite-top` (first unconditional eq whose
|
||||
LHS matches; conditional eqs skipped until Phase 4), innermost normalisation
|
||||
to a fixpoint `mau/normalize` (args normalised before the operator; fuel-
|
||||
guarded). API: `mau/reduce` / `mau/reduce-term` / `mau/reduce->str`. Tested on
|
||||
Peano (+,*), list ops (append/length/rev), a propositional simplifier, and
|
||||
non-linear `same(X,X)`. Innermost is fine for confluent terminating eq sets;
|
||||
Phase 3 will replace the matcher with AC-aware matching (multi-valued).
|
||||
|
||||
- **Phase 3 (matching modulo assoc/comm/id) — DONE, 119/119 total. THE CHISEL.**
|
||||
`lib/maude/matching.sx`. `mau/mm` is the multi-valued matcher (returns the
|
||||
full list of substitutions): free=positional, comm=both orderings,
|
||||
assoc=flatten f-spine + ordered sequence match (vars grab contiguous blocks),
|
||||
assoc+comm=multiset match (vars grab sub-multisets via `mau/all-splits` =
|
||||
2^n subset/complement pairs). `id: e` lets a var grab the empty block
|
||||
(contributing e); `mau/var-kmin` gives kmin 0 under id. `mau/canon` is the
|
||||
AC-canonical printout (flatten, drop identities, sort comm args) and powers
|
||||
`mau/ac-equal?` (used for bound-var checks too). AC *rewriting* extends each
|
||||
f-AC equation l=r with rest vars — comm: `f(l,$R)`; assoc: `f($L,l,$R)` —
|
||||
so a rule fires on any sub-multiset/subword (`$`-prefixed rest vars allowed
|
||||
empty). `mau/first-change` walks candidate matches and only commits a rewrite
|
||||
that changes the canonical form — this is what makes idempotency (`X U X = X`)
|
||||
and identity-absorbing matches terminate. API: `mau/ac-reduce` /
|
||||
`mau/ac-reduce->str` / `mau/ac-canon` / `mau/match-all`. Verified: AC match
|
||||
counts (X+Y vs a+b+c = 6), bag collapse, set dedup with empty, group
|
||||
cancellation (assoc non-comm + inverse).
|
||||
- Notes for next phases: AC matching is multi-valued — Phase 5 rule
|
||||
application should iterate ALL of `mau/mm`'s results, not just first. The
|
||||
`mau/ac-rewrite-eq` extension trick (rest vars) is the reusable core for
|
||||
a future `lib/guest/rewriting/` (Phase 8). Keep `mau/canon` as the equality
|
||||
oracle. `$EMPTY` is a transient marker for empty rest blocks w/o id; never
|
||||
leaks past `mau/restv`.
|
||||
|
||||
- **Phase 4 (conditional equations) — DONE, 138/138 total.**
|
||||
`lib/maude/conditional.sx` is a condition-aware superset of the Phase 3
|
||||
reducer. `mau/eq-candidates` enumerates (subst, result) pairs for an
|
||||
equation (AC via rest-var extension `mau/ac-candidates`, else `mau/mm`);
|
||||
`mau/try-candidates` commits the first candidate that both makes progress
|
||||
(canonical form changes) AND whose guard holds. `mau/cond-holds?` evaluates
|
||||
`{:kind :eq}` guards (reduce both sides, `ac-equal?`) and `{:kind :bool}`
|
||||
guards (reduce, `=AC= true`), recursing through `mau/cnormalize` — same
|
||||
reducer, so guards can mention other (conditional) equations. Public:
|
||||
`mau/creduce` / `mau/creduce->str` / `mau/ccanon`. Verified on gcd
|
||||
(subtractive, recursive guard), insertion sort (true/false branches), max,
|
||||
and even (bool-kind `if pred` guard).
|
||||
- Notes for next phases: `mau/creduce` is the canonical reducer now; Phase 5
|
||||
rules reduce to normal form via creduce between rewrite steps. `_:_` cons
|
||||
parses LEFT-assoc (no `gather` support yet) — write list literals
|
||||
right-parenthesized, or add a `gather`/parse-assoc attr later if a test
|
||||
needs bare `a : b : c`.
|
||||
|
||||
- **Phase 5 (system modules + rewrite rules) — DONE, 159/159 total.**
|
||||
`lib/maude/rewrite.sx` + `lib/maude/fire.sx`. Rules (rl/crl) reuse the
|
||||
equation firing machinery (a rule dict is shaped like an eq). `mau/rewrite`
|
||||
is the default strategy: normalise with eqs (`creduce`), fire ONE rule
|
||||
top-down/leftmost-outermost/first-applicable, renormalise, repeat (bounded
|
||||
by fuel). `mau/rew m src n` = bounded `rew [n]`. `mau/search` is BFS over
|
||||
ALL one-step successors (`mau/all-successors`) for reachability — solves the
|
||||
branching `goal` reachable only off the path `rew` takes. Verified: AC
|
||||
multiset coin-change (rule on a sub-multiset), cyclic traffic light (bounded),
|
||||
branching nondeterminism (rew vs search), conditional `crl` clock, eq/rule
|
||||
interleaving.
|
||||
- **PERF (important):** `lib/maude/fire.sx` is the short-circuiting matcher —
|
||||
`mau/fire-eq` finds the FIRST productive match via predicate-threaded
|
||||
`mau/ms-find`/`mau/seq-find` instead of materialising the whole solution
|
||||
set. Without it, AC rewriting on N identical elements is exponential
|
||||
(`q;q;q;q;q;q;q;q` went 60s+ → <1s). The eager `mau/match-multiset` /
|
||||
`mau/eq-candidates` are kept ONLY for `mau/match-all` and `search` (which
|
||||
truly need every solution). Phase 4 `creduce` and Phase 5 rules both fire
|
||||
via `mau/fire-eq`. Keep this split: never route single-step rewriting
|
||||
through the eager enumerator.
|
||||
- Notes: juxtaposition `__` (empty-token mixfix) and `gather` are NOT parsed —
|
||||
use an explicit infix op for multisets and right-parenthesise list literals.
|
||||
`.` can't be an op token (statement terminator). `mau/search` is the prime
|
||||
Phase 7 reflection / Phase 8 extraction target alongside the matcher.
|
||||
|
||||
- **Phase 6 (strategy language) — DONE, 178/178 total.**
|
||||
`lib/maude/strategy.sx`. Strategies are first-class tagged-dict VALUES and
|
||||
set-valued: `mau/sapply ctx strat term` → deduped (by canon) list of results.
|
||||
Combinators: `idle`/`fail`/`all`/`rule LABEL`/`seq`/`alt`/`star`/`plus`/`bang`
|
||||
/`name`. `seq` = flatmap B over A's results; `alt` = union; `star` = reflexive-
|
||||
transitive closure (BFS, canon-deduped); `plus` = A then star; `bang` =
|
||||
normal forms (reachable terms where A yields nothing). Named strategies via a
|
||||
NAME->strategy env dict passed to `mau/srun`/`mau/srun-canon`. Verified that
|
||||
the same rule set computes different things under different strategies
|
||||
(single rule vs all vs seq order vs alt vs star vs bang). Built on Phase 5
|
||||
`mau/all-successors` (rule label filter = `mau/rules-with-label`).
|
||||
- Note: `dict-set!` returns the value, not the dict — build a named-strategy
|
||||
env by binding `(define env {})` then `(dict-set! env ...)`, pass `env`.
|
||||
`srun-canon` sorts results so expected lists must be sorted.
|
||||
|
||||
- **Phase 7 (reflection / META-LEVEL) — DONE, 196/196 total.**
|
||||
`lib/maude/meta.sx`. `mau/up-term` re-encodes an object term as a term built
|
||||
from meta-constructors `mt-var`(name,sort) / `mt-app`(op, args...) — a
|
||||
represented term is itself a first-class object term you can build, inspect,
|
||||
transform. `mau/down-term` reverses (round-trips). Reflective ops:
|
||||
`mau/meta-reduce` / `mau/meta-rewrite` / `mau/meta-apply LABEL` take and
|
||||
return represented terms. `mau/meta-circular?` verifies the law
|
||||
`down(metaReduce(up t)) =AC= reduce t` (reflection agrees with the object
|
||||
level). `mau/meta-prove-equal?` is a generic equational theorem helper
|
||||
(prove an identity by joint reduction). Verified: up/down round-trip,
|
||||
meta-reduce returns a represented normal form, meta-circular law on Peano,
|
||||
meta-apply of a single rule, commutativity/associativity instance proofs,
|
||||
and building a program at the meta level then running it.
|
||||
|
||||
## Blockers
|
||||
_(speculative — equational matching is algorithmically heavy and may surface JIT issues)_
|
||||
_(none)_
|
||||
|
||||
Reference in New Issue
Block a user