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

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

### 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
_(awaiting Phase 1 — depends on substrate matching maturity from lib/guest/core/match.sx)_

## Blockers
_(speculative — equational matching is algorithmically heavy and may surface JIT issues)_