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)
- [ ] 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).

### 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.

### 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).

### 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.

### 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.

### 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).

## Blockers
_(none)_