giles
9dd9fb9c37
Design + ops scaffolding for the next phase of work, none of it touching
substrate or guest code.
lib-guest.md: rewrites Architectural framing as a 5-layer stack
(substrate → lib/guest → languages → shared/ → applications),
recursive dependency-direction rule, scaled two-consumer rule. Adds
Phase B (long-running stratification) with sub-layer matrix
(core/typed/relational/effects/layout/lazy/oo), language profiles, and
the long-running-discipline section. Preserves existing Phase A
progress log and rules.
ocaml-on-sx.md: scope reduced to substrate validation + HM + reference
oracle. Phases 1-5 + minimal stdlib slice + vendored testsuite slice.
Dream carved out into dream-on-sx.md; Phase 8 (ReasonML) deferred.
Records lib-guest sequencing dependency.
datalog-on-sx.md: adds Phase 4 built-in predicates + body arithmetic,
Phase 6 magic sets, safety analysis in Phase 3, Non-goals section.
New chisel plans (forward-looking, not yet launchable):
kernel-on-sx.md — first-class everything, env-as-value endgame
idris-on-sx.md — dependent types, evidence chisel
probabilistic-on-sx.md — weighted nondeterminism + traces
maude-on-sx.md — rewriting as primitive
linear-on-sx.md — resource model, artdag-relevant
Loop briefings (4 active, 1 cold):
minikanren-loop.md, ocaml-loop.md, datalog-loop.md, elm-loop.md, koka-loop.md
Restore scripts mirror the loop pattern:
restore-{minikanren,ocaml,datalog,jit-perf,lib-guest}.sh
Each captures worktree state, plan progress, MCP health, tmux status.
Includes the .mcp.json absolute-path patch instruction (fresh worktrees
have no _build/, so the relative mcp_tree path fails on first launch).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
132 lines
7.8 KiB
Markdown
132 lines
7.8 KiB
Markdown
# 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)_
|