rose-ash/plans/maude-on-sx.md

# Maude-on-SX: rewriting as primitive

Equational logic + term rewriting as the *only* computational primitive. Every other guest in the set reduces ultimately to lambda terms or stack frames; **Maude** (Clavel et al.) reduces to *rewrite rules over equational classes modulo theories* (associativity, commutativity, identity). Implementing it forces the substrate to articulate its reduction semantics — currently implicit in the CEK machine and the JIT.

**The chisel:** *reduction step*. Different from Idris's *evidence* chisel and from Probabilistic's *trace* chisel. Maude asks: "what is one step of computation?" Maude's answer (apply a rewrite rule, modulo equational theories) is more general than CEK's transition. Making both consistent is informative — either the substrate has room for them to coexist, or one is a special case of the other.

**What this exposes about the substrate:**
- Whether SX's pattern matching (lib/guest/match.sx) extends to *equational matching* — matching modulo associativity, commutativity, identity.
- Whether the substrate has a notion of "normal form" or just "result of evaluation."
- Whether term-graph sharing matters at the value-level.
- Whether confluence (different rewrite orders → same result) can be checked or just hoped for.
- Whether order-sorted signatures (subsorts, polymorphism via inheritance) fit SX's value taxonomy.

**End-state goal:** **Maude 3 functional + system modules** — sorts, subsorts, equations, conditional equations, rewrite rules, equational matching modulo `assoc`/`comm`/`id`, simple strategy language. Not the full LTL model checker; a faithful core that runs idiomatic Maude programs and proves equational identities.

## Ground rules
- Scope: `lib/maude/**` and `plans/maude-on-sx.md` only. Substrate gaps → `sx-improvements.md`.
- Consumes from `lib/guest/`: `core/lex`, `core/pratt`, `core/ast`, `core/match` (extended).
- **Will propose** a new sub-layer `lib/guest/rewriting/` — equational matching beyond syntactic match, normal-form computation, confluence checking, term-graph rewriting. Second consumer: a Pure-on-SX plan, a CafeOBJ port, or a research term-rewriting playground.
- Branch: `loops/maude`. Standard worktree pattern.

## Architecture sketch

```
Maude source text (functional / system / object modules)
    │
    ▼
lib/maude/parser.sx        — fmod ... endfm syntax, sort declarations,
    │                        equations, rewrite rules
    ▼
lib/maude/signatures.sx    — sort hierarchy, operator declarations with arities,
    │                        subsort relationships, kind inference
    ▼
lib/maude/matching.sx      — pattern matching MODULO equational theories
    │                        (assoc, comm, id) — generalises core/match.sx
    ▼
lib/maude/reduce.sx        — apply equations until normal form (confluent set)
    │
    ▼
lib/maude/rewrite.sx       — apply rewrite rules under a strategy (system modules)
    │
    ▼
lib/maude/runtime.sx       — module loading, reflection (META-LEVEL)
```

## Semantic mappings

| Maude construct | SX mapping |
|----------------|-----------|
| `sort Nat .` | declare sort: `(declare-sort Nat)` |
| `subsort Nat < Int .` | subsort relation: `(declare-subsort Nat Int)` |
| `op _+_ : Nat Nat -> Nat [assoc comm id: 0] .` | operator with equational attributes |
| `eq X + 0 = X .` | equation in the equational theory |
| `ceq X + Y = Y if foo(X, Y) .` | conditional equation |
| `rl [step] : foo(X) => bar(X) .` | rewrite rule (asymmetric, in system modules) |
| `red TERM .` | reduce term to normal form by equations |
| `rew TERM .` | apply rewrite rules under default strategy |
| `META-LEVEL` | reflection: terms representing terms |

The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 + 3` (where `+` is `assoc comm`) succeeds with multiple binding sets: `(X=1, Y=2+3)`, `(X=2, Y=1+3)`, `(X=3, Y=1+2)`, etc. The matcher must enumerate solutions, not return the first.

## Roadmap

### Phase 1 — Parser + signatures
- [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
- [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)
- [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
- [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
- [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
- [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)
- [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. 6 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).
- [ ] Extract normal-form-by-equations infrastructure.
- [ ] Extract strategy combinators.
- [ ] Wait for second consumer before extracting.

## lib/guest feedback loop

**Consumes:** `core/lex`, `core/pratt`, `core/ast`, `core/match` (with proposed extension for equational matching).

**Stresses substrate:** matching backtracking and enumeration (Maude's all-matches semantics is very different from Haskell-style first-match); whether SX values can carry sort metadata efficiently; term-graph sharing.

**May propose:** `lib/guest/rewriting/` sub-layer — equational matching (extending core/match), normal-form-by-equations machinery, strategy combinators, confluence checking.

**What it teaches:** whether the substrate's reduction model has implicit assumptions (deterministic, leftmost-outermost, etc.) that a rewriting language exposes. If `core/match.sx` cleanly extends to equational matching via a configuration toggle, that's substrate-deep validation. If extending it requires fundamental rework, the substrate's matching abstraction was leaking.

## References
- Clavel et al., "All About Maude — A High-Performance Logical Framework" (Springer, 2007).
- Maude Manual: https://maude.lcc.uma.es/
- "Term Rewriting and All That" (Baader & Nipkow, 1998) — theoretical foundation.
- Eker, "Associative-Commutative Rewriting on Large Terms" (RTA 2003) — for the matching algorithm.
- Pure language (Albrecht Gräf): https://agraef.github.io/pure-lang/ — practical functional rewriting.

## Progress log

- **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
_(none)_