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

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

Extensions (post-roadmap, toward the end-state goal)

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

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 eqs; 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.

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

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)