From 10906d4ffcb35fdc678ef215ded1ea50d951afdd Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 14:46:02 +0000 Subject: [PATCH] maude: Phase 2 syntactic equational reduction (26 tests, 91 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/reduce.sx — one-sided syntactic matching (non-linear patterns via bound-var equality), immutable substitutions, innermost fixpoint normalisation. Tested on Peano arithmetic, list ops, a propositional logic simplifier, and non-linear matching. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/reduce.sx | 143 +++++++++++++++++++++++++++++++++++++ lib/maude/scoreboard.json | 9 +-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/reduce.sx | 120 +++++++++++++++++++++++++++++++ plans/maude-on-sx.md | 17 ++++- 6 files changed, 286 insertions(+), 8 deletions(-) create mode 100644 lib/maude/reduce.sx create mode 100644 lib/maude/tests/reduce.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index 4fccc519..af3f75da 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -8,8 +8,10 @@ PRELOADS=( lib/guest/pratt.sx lib/maude/term.sx lib/maude/parser.sx + lib/maude/reduce.sx ) SUITES=( "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)" + "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)" ) diff --git a/lib/maude/reduce.sx b/lib/maude/reduce.sx new file mode 100644 index 00000000..2ae0a5cc --- /dev/null +++ b/lib/maude/reduce.sx @@ -0,0 +1,143 @@ +;; lib/maude/reduce.sx — syntactic equational reduction (Phase 2). +;; +;; Apply unconditional equations left-to-right to a fixpoint, using strict +;; one-sided syntactic matching (no theories yet — assoc/comm/id come in +;; Phase 3). Reduction is innermost: arguments are normalised before the +;; enclosing operator is rewritten. +;; +;; A substitution is a dict VAR-NAME -> term, extended immutably via `assoc`. +;; Matching is one-sided: only the pattern (equation LHS) carries variables; +;; the subject is treated structurally. + +;; ---------- matching ---------- + +(define + mau/match + (fn + (pat subj s) + (cond + ((= s nil) nil) + ((mau/var? pat) + (let + ((bound (get s (mau/vname pat)))) + (if + (= bound nil) + (assoc s (mau/vname pat) subj) + (if (mau/term=? bound subj) s nil)))) + ((and (mau/app? pat) (mau/app? subj)) + (if + (and + (= (mau/op pat) (mau/op subj)) + (= (mau/arity pat) (mau/arity subj))) + (mau/match-args (mau/args pat) (mau/args subj) s) + nil)) + (else nil)))) + +(define + mau/match-args + (fn + (ps ss s) + (cond + ((= s nil) nil) + ((and (empty? ps) (empty? ss)) s) + ((or (empty? ps) (empty? ss)) nil) + (else + (mau/match-args + (rest ps) + (rest ss) + (mau/match (first ps) (first ss) s)))))) + +;; ---------- substitution application ---------- + +(define + mau/subst-apply-list + (fn + (s args) + (if + (empty? args) + (list) + (cons + (mau/subst-apply s (first args)) + (mau/subst-apply-list s (rest args)))))) + +(define + mau/subst-apply + (fn + (s term) + (cond + ((mau/var? term) + (let ((b (get s (mau/vname term)))) (if (= b nil) term b))) + ((mau/app? term) + (mau/app (mau/op term) (mau/subst-apply-list s (mau/args term)))) + (else term)))) + +;; ---------- top-level rewrite ---------- + +;; Try each unconditional equation in order; on the first whose LHS matches +;; the term, return the instantiated RHS. nil if none apply. +(define + mau/rewrite-top + (fn + (eqs term) + (cond + ((empty? eqs) nil) + (else + (let + ((eq (first eqs))) + (if + (= (get eq :cond) nil) + (let + ((s (mau/match (get eq :lhs) term {}))) + (if + (= s nil) + (mau/rewrite-top (rest eqs) term) + (mau/subst-apply s (get eq :rhs)))) + (mau/rewrite-top (rest eqs) term))))))) + +;; ---------- normalisation (innermost to fixpoint) ---------- + +(define + mau/normalize-args + (fn + (eqs args fuel) + (if + (empty? args) + (list) + (cons + (mau/normalize eqs (first args) fuel) + (mau/normalize-args eqs (rest args) fuel))))) + +(define + mau/normalize + (fn + (eqs term fuel) + (if + (<= fuel 0) + term + (cond + ((mau/var? term) term) + ((mau/app? term) + (let + ((nargs (mau/normalize-args eqs (mau/args term) fuel))) + (let + ((t2 (mau/app (mau/op term) nargs))) + (let + ((r (mau/rewrite-top eqs t2))) + (if (= r nil) t2 (mau/normalize eqs r (- fuel 1))))))) + (else term))))) + +;; ---------- module-level API ---------- + +(define mau/reduce-fuel 1000000) + +(define + mau/reduce + (fn (m term) (mau/normalize (mau/module-eqs m) term mau/reduce-fuel))) + +(define + mau/reduce-term + (fn (m src) (mau/reduce m (mau/parse-term-in m src)))) + +(define + mau/reduce->str + (fn (m src) (mau/term->str (mau/reduce-term m src)))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 483579f1..e9ea5da0 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,10 +1,11 @@ { "lang": "maude", - "total_passed": 65, + "total_passed": 91, "total_failed": 0, - "total": 65, + "total": 91, "suites": [ - {"name":"parse","passed":65,"failed":0,"total":65} + {"name":"parse","passed":65,"failed":0,"total":65}, + {"name":"reduce","passed":26,"failed":0,"total":26} ], - "generated": "2026-06-07T14:42:29+00:00" + "generated": "2026-06-07T14:45:37+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index ca01f652..3d9e113e 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,7 +1,8 @@ # maude scoreboard -**65 / 65 passing** (0 failure(s)). +**91 / 91 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| | parse | 65 | 65 | ok | +| reduce | 26 | 26 | ok | diff --git a/lib/maude/tests/reduce.sx b/lib/maude/tests/reduce.sx new file mode 100644 index 00000000..0e09549e --- /dev/null +++ b/lib/maude/tests/reduce.sx @@ -0,0 +1,120 @@ +;; lib/maude/tests/reduce.sx — Phase 2: syntactic equational reduction. + +(define mrt-pass 0) +(define mrt-fail 0) +(define mrt-failures (list)) + +(define + mrt-check! + (fn + (name got expected) + (if + (= got expected) + (set! mrt-pass (+ mrt-pass 1)) + (do + (set! mrt-fail (+ mrt-fail 1)) + (append! + mrt-failures + (str name " expected: " expected " got: " got)))))) + +;; ---- Peano arithmetic ---- + +(define + mrt-peano + (mau/parse-module + "fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op _*_ : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n eq 0 * Y = 0 .\n eq s X * Y = Y + (X * Y) .\nendfm")) + +(mrt-check! + "add-2-1" + (mau/reduce->str mrt-peano "s s 0 + s 0") + "s_(s_(s_(0)))") +(mrt-check! "add-0-0" (mau/reduce->str mrt-peano "0 + 0") "0") +(mrt-check! "add-id-left" (mau/reduce->str mrt-peano "0 + s s 0") "s_(s_(0))") +(mrt-check! + "mul-2-2" + (mau/reduce->str mrt-peano "s s 0 * s s 0") + "s_(s_(s_(s_(0))))") +(mrt-check! "mul-zero" (mau/reduce->str mrt-peano "0 * s s s 0") "0") +(mrt-check! "mul-by-zero" (mau/reduce->str mrt-peano "s s 0 * 0") "0") +(mrt-check! + "nested" + (mau/reduce->str mrt-peano "(s 0 + s 0) * s s 0") + "s_(s_(s_(s_(0))))") + +;; ---- list manipulation ---- + +(define + mrt-list + (mau/parse-module + "fmod NATLIST is\n sorts Nat List .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op nil : -> List .\n op cons : Nat List -> List .\n op append : List List -> List .\n op length : List -> Nat .\n op rev : List -> List .\n var X : Nat .\n vars L M : List .\n eq append(nil, M) = M .\n eq append(cons(X, L), M) = cons(X, append(L, M)) .\n eq length(nil) = 0 .\n eq length(cons(X, L)) = s length(L) .\n eq rev(nil) = nil .\n eq rev(cons(X, L)) = append(rev(L), cons(X, nil)) .\nendfm")) + +(mrt-check! + "append" + (mau/reduce->str mrt-list "append(cons(0, nil), cons(s 0, nil))") + "cons(0, cons(s_(0), nil))") +(mrt-check! + "append-nil" + (mau/reduce->str mrt-list "append(nil, cons(0, nil))") + "cons(0, nil)") +(mrt-check! + "length-2" + (mau/reduce->str mrt-list "length(cons(0, cons(s 0, nil)))") + "s_(s_(0))") +(mrt-check! "length-0" (mau/reduce->str mrt-list "length(nil)") "0") +(mrt-check! + "rev" + (mau/reduce->str mrt-list "rev(cons(0, cons(s 0, nil)))") + "cons(s_(0), cons(0, nil))") +(mrt-check! "rev-empty" (mau/reduce->str mrt-list "rev(nil)") "nil") + +;; ---- propositional logic simplifier ---- + +(define + mrt-prop + (mau/parse-module + "fmod PROPLOGIC is\n sort Bool .\n op tt : -> Bool .\n op ff : -> Bool .\n op not_ : Bool -> Bool .\n op _and_ : Bool Bool -> Bool .\n op _or_ : Bool Bool -> Bool .\n op _xor_ : Bool Bool -> Bool .\n vars P Q : Bool .\n eq not tt = ff .\n eq not ff = tt .\n eq tt and P = P .\n eq ff and P = ff .\n eq tt or P = tt .\n eq ff or P = P .\n eq P xor ff = P .\n eq P xor tt = not P .\nendfm")) + +(mrt-check! "not-tt" (mau/reduce->str mrt-prop "not tt") "ff") +(mrt-check! "and-simpl" (mau/reduce->str mrt-prop "not (tt and ff)") "tt") +(mrt-check! "or-simpl" (mau/reduce->str mrt-prop "ff or (tt and tt)") "tt") +(mrt-check! "double-neg" (mau/reduce->str mrt-prop "not not tt") "tt") +(mrt-check! "xor-id" (mau/reduce->str mrt-prop "tt xor ff") "tt") +(mrt-check! "xor-tt" (mau/reduce->str mrt-prop "ff xor tt") "tt") +(mrt-check! + "deep" + (mau/reduce->str mrt-prop "(tt and tt) or (not not ff)") + "tt") + +;; ---- non-linear pattern (repeated variable) + no-match leaves term ---- + +(define + mrt-same + (mau/parse-module + "fmod SAME is\n sorts Elt Bool .\n op a : -> Elt .\n op b : -> Elt .\n op tt : -> Bool .\n op same : Elt Elt -> Bool .\n var X : Elt .\n eq same(X, X) = tt .\nendfm")) + +(mrt-check! "nonlinear-match" (mau/reduce->str mrt-same "same(a, a)") "tt") +(mrt-check! + "nonlinear-nomatch" + (mau/reduce->str mrt-same "same(a, b)") + "same(a, b)") +(mrt-check! "no-rule-stays" (mau/reduce->str mrt-same "b") "b") + +;; ---- low-level matching ---- + +(mrt-check! + "match-var-binds" + (= nil (mau/match (mau/var "X" "Nat") (mau/const "0") {})) + false) +(mrt-check! + "match-mismatch" + (mau/match (mau/const "0") (mau/const "1") {}) + nil) +(mrt-check! + "subst-apply" + (mau/term->str + (mau/subst-apply + (assoc {} "X" (mau/const "0")) + (mau/app "s_" (list (mau/var "X" "Nat"))))) + "s_(0)") + +(define mau-reduce-tests-run! (fn () {:failures mrt-failures :total (+ mrt-pass mrt-fail) :passed mrt-pass :failed mrt-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index d559af7a..57692dba 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -68,9 +68,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] 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. +- [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). @@ -142,5 +142,16 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 `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)_