coop/rose-ash
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

maude: Phase 5 system modules + rewrite rules (21 tests, 159 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 48s
Details

Browse Source 
lib/maude/rewrite.sx: rl/crl transitions interleaved with eq normalisation.
mau/rewrite = default strategy (top-down, leftmost-outermost, first rule);
mau/rew bounded; mau/search = BFS reachability over all successors.

lib/maude/fire.sx: short-circuiting matcher (mau/fire-eq) — finds the first
productive match instead of enumerating the whole solution set. Fixes the
exponential blowup of AC rewriting on many identical elements (8 coins:
60s+ to <1s). Eager match-multiset kept only for match-all / search.

Verified on AC coin-change, traffic light, branching search, crl clock.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
giles
2026-06-07 15:23:06 +00:00
parent 1747bbd944
commit 858d35a68c
8 changed files with 692 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
lib/maude/conditional.sx
View File

@@ -10,8 +10,10 @@
;; — termination rests on the guard reducing on structurally smaller arguments
;; (and the global fuel guard).
;;
;; This engine subsumes mau/ac-reduce: an unconditional equation has cond nil,
;; which always holds. Phases 5+ build on the c-* entry points.
;; Single-step firing uses the short-circuiting matcher in fire.sx
;; (mau/fire-eq) so reduction is not quadratic/exponential in AC argument size.
;; The eager candidate enumeration (mau/eq-candidates) is retained for `search`
;; (rewrite.sx), which genuinely needs every successor.
(define
mau/ac-candidates
@@ -92,7 +94,7 @@
(empty? eqs)
nil
(let
((r (mau/try-candidates theory all-eqs (get (first eqs) :cond) term (mau/eq-candidates theory (first eqs) term))))
((r (mau/fire-eq theory all-eqs (first eqs) term)))
(if (= r nil) (mau/crewrite-loop theory all-eqs (rest eqs) term) r)))))
(define

3
lib/maude/conformance.conf
View File

@@ -11,6 +11,8 @@ PRELOADS=(
lib/maude/reduce.sx
lib/maude/matching.sx
lib/maude/conditional.sx
lib/maude/fire.sx
lib/maude/rewrite.sx
)
SUITES=(
@@ -18,4 +20,5 @@ SUITES=(
"reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)"
"matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)"
"conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)"
"rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)"
)

250
lib/maude/fire.sx Normal file
View File

@@ -0,0 +1,250 @@
;; lib/maude/fire.sx — short-circuiting rule/equation firing.
;;
;; The eager matcher (mau/match-multiset) enumerates EVERY substitution, which
;; is what `mau/match-all` and `search` need. But for a single rewrite step we
;; only need the FIRST usable match — and eager enumeration is exponential when
;; an AC argument has many identical elements (q ; q ; ... ; q). These
;; find-matchers thread a predicate and stop at the first complete match for
;; which it returns non-nil; the predicate builds the rewritten term and checks
;; "progresses AND condition holds", so firing short-circuits on the first
;; productive match instead of materialising the whole solution set.
;;
;; pred : subst -> result-term-or-nil (result is always a term, never nil)
(define
mau/try-list
(fn
(substs cont)
(if
(empty? substs)
nil
(let
((r (cont (first substs))))
(if (= r nil) (mau/try-list (rest substs) cont) r)))))
;; ---- multiset (assoc+comm) find ----
(define
mau/ms-find
(fn
(theory f pels sels s id pred)
(cond
((empty? pels) (if (empty? sels) (pred s) nil))
(else
(let
((p (first pels)) (prest (rest pels)))
(if
(mau/var? p)
(mau/ms-find-var
theory
f
prest
sels
s
(mau/vname p)
id
pred
(mau/var-kmin (mau/vname p) id)
(mau/all-splits sels))
(mau/ms-find-nonvar theory f p prest sels s id pred 0)))))))
(define
mau/ms-find-nonvar
(fn
(theory f p prest sels s id pred i)
(if
(>= i (len sels))
nil
(let
((others (mau/remove-at sels i)))
(let
((r (mau/try-list (mau/mm theory p (nth sels i) s) (fn (s2) (mau/ms-find theory f prest others s2 id pred)))))
(if
(not (= r nil))
r
(mau/ms-find-nonvar
theory
f
p
prest
sels
s
id
pred
(+ i 1))))))))
(define
mau/ms-find-var
(fn
(theory f prest sels s name id pred kmin splits)
(if
(empty? splits)
nil
(let
((chosen (first (first splits)))
(rests (nth (first splits) 1)))
(if
(< (len chosen) kmin)
(mau/ms-find-var
theory
f
prest
sels
s
name
id
pred
kmin
(rest splits))
(let
((s2 (mau/bind-check theory s name (mau/rebuild f chosen id))))
(let
((r (if (= s2 nil) nil (mau/ms-find theory f prest rests s2 id pred))))
(if
(not (= r nil))
r
(mau/ms-find-var
theory
f
prest
sels
s
name
id
pred
kmin
(rest splits))))))))))
;; ---- sequence (assoc, ordered) find ----
(define
mau/seq-find
(fn
(theory f pels sels s id pred)
(cond
((empty? pels) (if (empty? sels) (pred s) nil))
(else
(let
((p (first pels)) (prest (rest pels)))
(if
(mau/var? p)
(mau/seq-find-var
theory
f
prest
sels
s
(mau/vname p)
id
pred
(mau/var-kmin (mau/vname p) id))
(if
(empty? sels)
nil
(mau/try-list
(mau/mm theory p (first sels) s)
(fn
(s2)
(mau/seq-find theory f prest (rest sels) s2 id pred))))))))))
(define
mau/seq-find-var
(fn
(theory f prest sels s name id pred k)
(if
(> k (len sels))
nil
(let
((s2 (mau/bind-check theory s name (mau/rebuild f (mau/take sels k) id))))
(let
((r (if (= s2 nil) nil (mau/seq-find theory f prest (mau/drop sels k) s2 id pred))))
(if
(not (= r nil))
r
(mau/seq-find-var
theory
f
prest
sels
s
name
id
pred
(+ k 1))))))))
;; ---- firing an equation/rule (returns rewritten term or nil) ----
(define
mau/fire-plain
(fn
(theory eqs eq term cnd substs)
(if
(empty? substs)
nil
(let
((res (mau/subst-apply (first substs) (get eq :rhs))))
(if
(and
(not (mau/ac-equal? theory res term))
(mau/cond-holds? theory eqs cnd (first substs)))
res
(mau/fire-plain theory eqs eq term cnd (rest substs)))))))
(define
mau/fire-ac
(fn
(theory eqs f th eq term cnd)
(let
((id (get th :id))
(pels (mau/flatten-op theory f (get eq :lhs)))
(sels (mau/flatten-op theory f term)))
(let
((pred (fn (s) (let ((res (mau/ac-eq-result theory f th eq s))) (if (and (not (mau/ac-equal? theory res term)) (mau/cond-holds? theory eqs cnd s)) res nil)))))
(if
(get th :comm)
(mau/ms-find
theory
f
(mau/append2 pels (list (mau/var "$R" "")))
sels
{}
id
pred)
(mau/seq-find
theory
f
(mau/append2
(list (mau/var "$L" ""))
(mau/append2 pels (list (mau/var "$R" ""))))
sels
{}
id
pred))))))
(define
mau/fire-eq
(fn
(theory eqs eq term)
(let
((lhs (get eq :lhs)) (cnd (get eq :cond)))
(if
(mau/app? lhs)
(let
((th (mau/th-of theory (mau/op lhs))))
(if
(get th :assoc)
(mau/fire-ac theory eqs (mau/op lhs) th eq term cnd)
(mau/fire-plain
theory
eqs
eq
term
cnd
(mau/mm theory lhs term {}))))
(mau/fire-plain
theory
eqs
eq
term
cnd
(mau/mm theory lhs term {}))))))

284
lib/maude/rewrite.sx Normal file
View File

@@ -0,0 +1,284 @@
;; lib/maude/rewrite.sx — system modules + rewrite rules (Phase 5).
;;
;; Equations (eq/ceq) are applied to a fixpoint to NORMALISE (confluent by
;; intent). Rules (rl/crl) are TRANSITIONS: asymmetric (=>), possibly
;; nondeterministic, NOT applied to a fixpoint. Maude's `rew` interleaves
;; the two: normalise with equations, fire one rule, renormalise, repeat.
;;
;; Rule firing reuses the shared firing machinery — a rule dict carries
;; :lhs/:rhs/:cond exactly like an equation, so `mau/fire-eq` (short-circuit,
;; fire.sx) applies unchanged (matching modulo the AC theory; crl guards
;; evaluated with the equations). A rule fires only if it both progresses and
;; its condition holds.
;;
;; `mau/rewrite` follows the default strategy (top-down, leftmost-outermost,
;; first applicable rule) for one path. `mau/search` does breadth-first reach
;; over ALL one-step successors — for puzzle solvers / protocol simulators
;; where the answer is on a branch `rew` would not take.
(define mau/rew-fuel 100000)
;; ---- single-step, default strategy (first applicable, leftmost-outermost) ----
(define
mau/rules-at-top
(fn
(theory eqs rules term)
(if
(empty? rules)
nil
(let
((r (mau/fire-eq theory eqs (first rules) term)))
(if (= r nil) (mau/rules-at-top theory eqs (rest rules) term) r)))))
(define
mau/apply-rule-once
(fn
(theory eqs rules term)
(let
((top (mau/rules-at-top theory eqs rules term)))
(if
(not (= top nil))
top
(if
(mau/app? term)
(mau/apply-rule-in-args
theory
eqs
rules
(mau/op term)
(mau/args term)
(list))
nil)))))
(define
mau/apply-rule-in-args
(fn
(theory eqs rules op done todo)
(if
(empty? todo)
nil
(let
((r (mau/apply-rule-once theory eqs rules (first todo))))
(if
(= r nil)
(mau/apply-rule-in-args
theory
eqs
rules
op
(mau/append2 done (list (first todo)))
(rest todo))
(mau/app op (mau/append2 done (cons r (rest todo)))))))))
(define
mau/rewrite-steps
(fn
(theory eqs rules term steps)
(if
(<= steps 0)
(mau/cnormalize theory eqs term mau/reduce-fuel)
(let
((nf (mau/cnormalize theory eqs term mau/reduce-fuel)))
(let
((r (mau/apply-rule-once theory eqs rules nf)))
(if
(= r nil)
nf
(mau/rewrite-steps theory eqs rules r (- steps 1))))))))
(define
mau/rewrite
(fn
(m term)
(mau/rewrite-steps
(mau/build-theory m)
(mau/module-eqs m)
(mau/module-rules m)
term
mau/rew-fuel)))
(define
mau/rew
(fn
(m src n)
(mau/rewrite-steps
(mau/build-theory m)
(mau/module-eqs m)
(mau/module-rules m)
(mau/parse-term-in m src)
n)))
(define
mau/rewrite-term
(fn (m src) (mau/rewrite m (mau/parse-term-in m src))))
(define
mau/rewrite->str
(fn (m src) (mau/term->str (mau/rewrite-term m src))))
(define
mau/rewrite-canon
(fn (m src) (mau/canon (mau/build-theory m) (mau/rewrite-term m src))))
(define mau/rew->str (fn (m src n) (mau/term->str (mau/rew m src n))))
(define
mau/rew-canon
(fn (m src n) (mau/canon (mau/build-theory m) (mau/rew m src n))))
;; ---- all one-step successors (for search; eager enumeration) ----
(define
mau/cands-results
(fn
(theory eqs cond term cands)
(mau/concat-map
(fn
(c)
(if
(and
(not (mau/ac-equal? theory (get c :result) term))
(mau/cond-holds? theory eqs cond (get c :s)))
(list (mau/cnormalize theory eqs (get c :result) mau/reduce-fuel))
(list)))
cands)))
(define
mau/top-successors
(fn
(theory eqs rules term)
(mau/concat-map
(fn
(rule)
(mau/cands-results
theory
eqs
(get rule :cond)
term
(mau/eq-candidates theory rule term)))
rules)))
(define
mau/arg-successors
(fn
(theory eqs rules op done todo)
(if
(empty? todo)
(list)
(mau/append2
(map
(fn
(sub)
(mau/app op (mau/append2 done (cons sub (rest todo)))))
(mau/all-successors theory eqs rules (first todo)))
(mau/arg-successors
theory
eqs
rules
op
(mau/append2 done (list (first todo)))
(rest todo))))))
(define
mau/all-successors
(fn
(theory eqs rules term)
(mau/append2
(mau/top-successors theory eqs rules term)
(if
(mau/app? term)
(mau/arg-successors
theory
eqs
rules
(mau/op term)
(mau/args term)
(list))
(list)))))
(define
mau/successors
(fn
(m src)
(let
((theory (mau/build-theory m)) (eqs (mau/module-eqs m)))
(map
(fn (t) (mau/canon theory t))
(mau/all-successors
theory
eqs
(mau/module-rules m)
(mau/cnormalize
theory
eqs
(mau/parse-term-in m src)
mau/reduce-fuel))))))
;; ---- breadth-first reachability search ----
(define
mau/canon-list
(fn (theory ts) (map (fn (t) (mau/canon theory t)) ts)))
(define
mau/bfs-search
(fn
(theory eqs rules frontier seen goal depth)
(cond
((mau/member? goal (mau/canon-list theory frontier)) true)
((<= depth 0) false)
((empty? frontier) false)
(else
(let
((newf (list)) (newseen seen))
(for-each
(fn
(t)
(for-each
(fn
(succ)
(let
((c (mau/canon theory succ)))
(when
(not (mau/member? c newseen))
(do
(set! newseen (cons c newseen))
(append! newf succ)))))
(mau/all-successors theory eqs rules t)))
frontier)
(mau/bfs-search
theory
eqs
rules
newf
newseen
goal
(- depth 1)))))))
(define
mau/search
(fn
(m start-src goal-src max-depth)
(let
((theory (mau/build-theory m))
(eqs (mau/module-eqs m))
(rules (mau/module-rules m)))
(let
((start (mau/cnormalize theory eqs (mau/parse-term-in m start-src) mau/reduce-fuel))
(goal
(mau/canon
theory
(mau/cnormalize
theory
eqs
(mau/parse-term-in m goal-src)
mau/reduce-fuel))))
(mau/bfs-search
theory
eqs
rules
(list start)
(list (mau/canon theory start))
goal
max-depth)))))

9
lib/maude/scoreboard.json
View File

@@ -1,13 +1,14 @@
{
"lang": "maude",
"total_passed": 138,
"total_passed": 159,
"total_failed": 0,
"total": 138,
"total": 159,
"suites": [
{"name":"parse","passed":65,"failed":0,"total":65},
{"name":"reduce","passed":26,"failed":0,"total":26},
{"name":"matching","passed":28,"failed":0,"total":28},
{"name":"conditional","passed":19,"failed":0,"total":19}
{"name":"conditional","passed":19,"failed":0,"total":19},
{"name":"rewrite","passed":21,"failed":0,"total":21}
],
"generated": "2026-06-07T15:05:31+00:00"
"generated": "2026-06-07T15:22:28+00:00"
}

3
lib/maude/scoreboard.md
View File

@@ -1,6 +1,6 @@
# maude scoreboard
**138 / 138 passing** (0 failure(s)).
**159 / 159 passing** (0 failure(s)).
| Suite | Passed | Total | Status |
|-------|--------|-------|--------|
@@ -8,3 +8,4 @@
| reduce | 26 | 26 | ok |
| matching | 28 | 28 | ok |
| conditional | 19 | 19 | ok |
| rewrite | 21 | 21 | ok |

114
lib/maude/tests/rewrite.sx Normal file
View File

@@ -0,0 +1,114 @@
;; lib/maude/tests/rewrite.sx — Phase 5: system modules + rewrite rules.
(define mrw-pass 0)
(define mrw-fail 0)
(define mrw-failures (list))
(define
mrw-check!
(fn
(name got expected)
(if
(= got expected)
(set! mrw-pass (+ mrw-pass 1))
(do
(set! mrw-fail (+ mrw-fail 1))
(append!
mrw-failures
(str name " expected: " expected " got: " got))))))
;; ---- AC multiset transition (the headline: rule on a sub-multiset) ----
(define
mrw-coins
(mau/parse-module
"mod COINS is\n sort Marking .\n op nil : -> Marking .\n op q : -> Marking .\n op d : -> Marking .\n op _;_ : Marking Marking -> Marking [assoc comm id: nil] .\n rl [change] : q ; q ; q ; q => d .\nendm"))
(mrw-check! "coins-kind" (mau/module-kind mrw-coins) "mod")
(mrw-check! "coins-rules" (len (mau/module-rules mrw-coins)) 1)
(mrw-check! "coins-exact" (mau/rewrite-canon mrw-coins "q ; q ; q ; q") "d")
(mrw-check!
"coins-5"
(mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q")
"_;_(d,q)")
(mrw-check!
"coins-8"
(mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q ; q ; q ; q")
"_;_(d,d)")
(mrw-check!
"coins-3-stuck"
(mau/rewrite-canon mrw-coins "q ; q ; q")
"_;_(q,q,q)")
;; ---- cyclic state machine (bounded rew) ----
(define
mrw-traffic
(mau/parse-module
"mod TRAFFIC is\n sort Light .\n ops red green yellow : -> Light .\n rl [g] : red => green .\n rl [y] : green => yellow .\n rl [r] : yellow => red .\nendm"))
(mrw-check! "traffic-1" (mau/rew->str mrw-traffic "red" 1) "green")
(mrw-check! "traffic-2" (mau/rew->str mrw-traffic "red" 2) "yellow")
(mrw-check! "traffic-3" (mau/rew->str mrw-traffic "red" 3) "red")
(mrw-check! "traffic-0" (mau/rew->str mrw-traffic "green" 0) "green")
;; ---- nondeterministic branching: rew (one path) vs search (all paths) ----
(define
mrw-ndet
(mau/parse-module
"mod NDET is\n sort S .\n ops a b c d goal : -> S .\n rl [r1] : a => b .\n rl [r2] : a => c .\n rl [r3] : b => d .\n rl [r4] : c => goal .\nendm"))
;; rew takes the first rule each step: a -> b -> d (stuck), never reaches goal.
(mrw-check! "ndet-rew-path" (mau/rewrite->str mrw-ndet "a") "d")
(mrw-check! "ndet-succ" (mau/successors mrw-ndet "a") (list "b" "c"))
(mrw-check!
"ndet-search-goal"
(mau/search mrw-ndet "a" "goal" 5)
true)
(mrw-check!
"ndet-search-shallow"
(mau/search mrw-ndet "a" "goal" 1)
false)
(mrw-check! "ndet-search-self" (mau/search mrw-ndet "a" "a" 3) true)
(mrw-check! "ndet-search-d" (mau/search mrw-ndet "a" "d" 5) true)
;; ---- conditional rule (crl with equational guard) ----
(define
mrw-clock
(mau/parse-module
"mod CLOCK is\n sorts Nat Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<_ : Nat Nat -> Bool .\n op clk : Nat -> Nat .\n vars M N : Nat .\n eq 0 < s N = true .\n eq N < 0 = false .\n eq s M < s N = M < N .\n crl [tick] : clk(N) => clk(s N) if N < s s s 0 = true .\nendm"))
;; tick fires while N < 3, then stops at clk(3).
(mrw-check!
"clock-run"
(mau/rewrite->str mrw-clock "clk(0)")
"clk(s_(s_(s_(0))))")
(mrw-check!
"clock-from-1"
(mau/rewrite->str mrw-clock "clk(s 0)")
"clk(s_(s_(s_(0))))")
(mrw-check!
"clock-step1"
(mau/rew->str mrw-clock "clk(0)" 1)
"clk(s_(0))")
;; ---- eqs interleave with rules ----
(define
mrw-mix
(mau/parse-module
"mod MIX is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op f : Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n rl [step] : f(X) => f(X + s 0) .\nendm"))
;; each rule step adds one (via the rule), eqs normalise the sum.
(mrw-check!
"mix-step1"
(mau/rew->str mrw-mix "f(s 0)" 1)
"f(s_(s_(0)))")
(mrw-check!
"mix-step2"
(mau/rew->str mrw-mix "f(0)" 2)
"f(s_(s_(0)))")
(define mau-rewrite-tests-run! (fn () {:failures mrw-failures :total (+ mrw-pass mrw-fail) :passed mrw-pass :failed mrw-fail}))

33
plans/maude-on-sx.md
View File

@@ -86,10 +86,10 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
- [x] 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).
- [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
- [ ] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point.
@@ -195,5 +195,30 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
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.
## Blockers
_(none)_