From 2dd4c7d97495b039c248edf491f51440b1159036 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 20:18:33 +0000 Subject: [PATCH] maude: confluence / critical-pair checking (12 tests, 274 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/confluence.sx — two-sided syntactic unification (occurs-checked) → critical pairs from LHS overlaps → joinability via AC-canonical normal forms. mau/confluent? / mau/non-joinable-pairs / mau/critical-pairs / mau/cp->str. Catches f(a)=b,a=c (b f(c)); peano/idempotent/AC confirmed confluent. Syntactic overlaps (AC under-approximated, joinability uses canon). This is the CID-stability oracle for the artdag optimiser. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/confluence.sx | 268 ++++++++++++++++++++++++++++++++++ lib/maude/conformance.conf | 2 + lib/maude/scoreboard.json | 7 +- lib/maude/scoreboard.md | 3 +- lib/maude/tests/confluence.sx | 101 +++++++++++++ plans/maude-on-sx.md | 13 ++ 6 files changed, 390 insertions(+), 4 deletions(-) create mode 100644 lib/maude/confluence.sx create mode 100644 lib/maude/tests/confluence.sx diff --git a/lib/maude/confluence.sx b/lib/maude/confluence.sx new file mode 100644 index 00000000..4c4b930b --- /dev/null +++ b/lib/maude/confluence.sx @@ -0,0 +1,268 @@ +;; lib/maude/confluence.sx — critical-pair / local-confluence checking. +;; +;; A terminating equation set is confluent iff every critical pair is joinable +;; (Knuth-Bendix / Newman). A critical pair arises when two oriented equations +;; overlap: a non-variable subterm of one LHS unifies with the other LHS, giving +;; two ways to rewrite the overlap; they must reduce to the same normal form. +;; +;; This needs TWO-SIDED unification (variables on both sides), not the one-sided +;; matching the reducer uses — so this file carries its own syntactic unifier. +;; +;; SCOPE / honesty: the unifier is SYNTACTIC. For free/constructor operators the +;; check is exact. For assoc/comm (AC) operators it sees only syntactic overlaps +;; (full AC-unification is NP/infinitary — out of scope), but joinability is +;; tested with `mau/ac-equal?` (canonical form modulo the theory), so AC laws are +;; joined correctly even though their overlaps are under-approximated. Conditional +;; and `owise` equations are not oriented (skipped). + +;; ---------- syntactic unification (vars on both sides) ---------- + +(define + mau/u-walk + (fn + (t s) + (if + (mau/var? t) + (let + ((b (get s (mau/vname t)))) + (if (= b nil) t (mau/u-walk b s))) + t))) + +(define + mau/u-occurs? + (fn + (name t s) + (let + ((w (mau/u-walk t s))) + (cond + ((mau/var? w) (= (mau/vname w) name)) + ((mau/app? w) (mau/u-occurs-any? name (mau/args w) s)) + (else false))))) + +(define + mau/u-occurs-any? + (fn + (name args s) + (cond + ((empty? args) false) + ((mau/u-occurs? name (first args) s) true) + (else (mau/u-occurs-any? name (rest args) s))))) + +(define + mau/u-unify-args + (fn + (as bs s) + (cond + ((= s nil) nil) + ((and (empty? as) (empty? bs)) s) + ((or (empty? as) (empty? bs)) nil) + (else + (mau/u-unify-args + (rest as) + (rest bs) + (mau/u-unify (first as) (first bs) s)))))) + +(define + mau/u-unify + (fn + (t1 t2 s) + (if + (= s nil) + nil + (let + ((a (mau/u-walk t1 s)) (b (mau/u-walk t2 s))) + (cond + ((and (mau/var? a) (mau/var? b) (= (mau/vname a) (mau/vname b))) + s) + ((mau/var? a) + (if + (mau/u-occurs? (mau/vname a) b s) + nil + (assoc s (mau/vname a) b))) + ((mau/var? b) + (if + (mau/u-occurs? (mau/vname b) a s) + nil + (assoc s (mau/vname b) a))) + ((and (mau/app? a) (mau/app? b)) + (if + (and + (= (mau/op a) (mau/op b)) + (= (mau/arity a) (mau/arity b))) + (mau/u-unify-args (mau/args a) (mau/args b) s) + nil)) + (else nil)))))) + +(define + mau/u-apply + (fn + (t s) + (let + ((w (mau/u-walk t s))) + (if + (mau/app? w) + (mau/app + (mau/op w) + (map (fn (a) (mau/u-apply a s)) (mau/args w))) + w)))) + +(define + mau/u-rename + (fn + (t suffix) + (cond + ((mau/var? t) (mau/var (str (mau/vname t) suffix) (mau/vsort t))) + ((mau/app? t) + (mau/app + (mau/op t) + (map (fn (a) (mau/u-rename a suffix)) (mau/args t)))) + (else t)))) + +;; ---------- positions ---------- + +(define + mau/positions-args + (fn + (args i) + (if + (empty? args) + (list) + (mau/append2 + (map (fn (p) (cons i p)) (mau/nv-positions (first args))) + (mau/positions-args (rest args) (+ i 1)))))) + +;; non-variable positions (paths) of a term; root = empty path +(define + mau/nv-positions + (fn + (t) + (if + (mau/app? t) + (cons (list) (mau/positions-args (mau/args t) 0)) + (list)))) + +(define + mau/at-path + (fn + (t path) + (if + (empty? path) + t + (mau/at-path (nth (mau/args t) (first path)) (rest path))))) + +(define + mau/replace-nth + (fn + (xs i v) + (if + (= i 0) + (cons v (rest xs)) + (cons (first xs) (mau/replace-nth (rest xs) (- i 1) v))))) + +(define + mau/replace-at + (fn + (t path new) + (if + (empty? path) + new + (mau/app + (mau/op t) + (mau/replace-nth + (mau/args t) + (first path) + (mau/replace-at (nth (mau/args t) (first path)) (rest path) new)))))) + +;; ---------- critical pairs ---------- + +(define + mau/eq-same? + (fn + (e1 e2) + (and + (mau/term=? (get e1 :lhs) (get e2 :lhs)) + (mau/term=? (get e1 :rhs) (get e2 :rhs))))) + +(define + mau/cps-at + (fn + (l1 r1 l2 r2 same? paths) + (if + (empty? paths) + (list) + (let + ((p (first paths))) + (if + (and same? (empty? p)) + (mau/cps-at l1 r1 l2 r2 same? (rest paths)) + (let + ((s (mau/u-unify (mau/at-path l1 p) l2 {}))) + (if + (= s nil) + (mau/cps-at l1 r1 l2 r2 same? (rest paths)) + (cons {:right (mau/u-apply (mau/replace-at l1 p r2) s) :left (mau/u-apply r1 s)} (mau/cps-at l1 r1 l2 r2 same? (rest paths)))))))))) + +(define + mau/cps-of + (fn + (e1 e2) + (let + ((l1 (mau/u-rename (get e1 :lhs) "#1")) + (r1 (mau/u-rename (get e1 :rhs) "#1")) + (l2 (mau/u-rename (get e2 :lhs) "#2")) + (r2 (mau/u-rename (get e2 :rhs) "#2"))) + (mau/cps-at l1 r1 l2 r2 (mau/eq-same? e1 e2) (mau/nv-positions l1))))) + +(define + mau/all-cps + (fn + (eqs) + (mau/concat-map + (fn (e1) (mau/concat-map (fn (e2) (mau/cps-of e1 e2)) eqs)) + eqs))) + +;; ---------- public API ---------- + +(define + mau/orientable-eqs + (fn + (m) + (filter + (fn (e) (and (= (get e :cond) nil) (not (= (get e :owise) true)))) + (mau/module-eqs m)))) + +(define + mau/joinable? + (fn + (theory eqs t1 t2) + (mau/ac-equal? + theory + (mau/cnormalize theory eqs t1 mau/reduce-fuel) + (mau/cnormalize theory eqs t2 mau/reduce-fuel)))) + +(define mau/critical-pairs (fn (m) (mau/all-cps (mau/orientable-eqs m)))) + +(define + mau/non-joinable-pairs + (fn + (m) + (let + ((theory (mau/build-theory m)) (eqs (mau/module-eqs m))) + (filter + (fn + (cp) + (not (mau/joinable? theory eqs (get cp :left) (get cp :right)))) + (mau/all-cps (mau/orientable-eqs m)))))) + +(define mau/confluent? (fn (m) (empty? (mau/non-joinable-pairs m)))) + +(define + mau/cp->str + (fn + (m cp) + (let + ((theory (mau/build-theory m))) + (str + (mau/canon theory (get cp :left)) + " " + (mau/canon theory (get cp :right)))))) diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index 5286e343..d904c0b0 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -13,6 +13,7 @@ PRELOADS=( lib/maude/matching.sx lib/maude/conditional.sx lib/maude/fire.sx + lib/maude/confluence.sx lib/maude/rewrite.sx lib/maude/searchpath.sx lib/maude/strategy.sx @@ -25,6 +26,7 @@ SUITES=( "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)" "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)" "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)" + "confluence:lib/maude/tests/confluence.sx:(mau-confluence-tests-run!)" "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" "owise:lib/maude/tests/owise.sx:(mau-owise-tests-run!)" "gather:lib/maude/tests/gather.sx:(mau-gather-tests-run!)" diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 886b34b1..4381ebd6 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,12 +1,13 @@ { "lang": "maude", - "total_passed": 262, + "total_passed": 274, "total_failed": 0, - "total": 262, + "total": 274, "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":"confluence","passed":12,"failed":0,"total":12}, {"name":"conditional","passed":19,"failed":0,"total":19}, {"name":"owise","passed":8,"failed":0,"total":8}, {"name":"gather","passed":7,"failed":0,"total":7}, @@ -19,5 +20,5 @@ {"name":"run","passed":10,"failed":0,"total":10}, {"name":"effects","passed":8,"failed":0,"total":8} ], - "generated": "2026-06-07T19:38:27+00:00" + "generated": "2026-06-07T20:18:07+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index cfb8c57d..975bd91e 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,12 +1,13 @@ # maude scoreboard -**262 / 262 passing** (0 failure(s)). +**274 / 274 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| | parse | 65 | 65 | ok | | reduce | 26 | 26 | ok | | matching | 28 | 28 | ok | +| confluence | 12 | 12 | ok | | conditional | 19 | 19 | ok | | owise | 8 | 8 | ok | | gather | 7 | 7 | ok | diff --git a/lib/maude/tests/confluence.sx b/lib/maude/tests/confluence.sx new file mode 100644 index 00000000..e507cdc4 --- /dev/null +++ b/lib/maude/tests/confluence.sx @@ -0,0 +1,101 @@ +;; lib/maude/tests/confluence.sx — critical-pair / local-confluence checking. + +(define mcf-pass 0) +(define mcf-fail 0) +(define mcf-failures (list)) + +(define + mcf-check! + (fn + (name got expected) + (if + (= got expected) + (set! mcf-pass (+ mcf-pass 1)) + (do + (set! mcf-fail (+ mcf-fail 1)) + (append! + mcf-failures + (str name " expected: " expected " got: " got)))))) + +;; peano addition: no LHS overlaps -> confluent +(define + mcf-peano + (mau/parse-module + "fmod P is\n sort Nat .\n op 0 : -> Nat .\n op s_ : 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) .\nendfm")) + +(mcf-check! "peano-confluent" (mau/confluent? mcf-peano) true) +(mcf-check! + "peano-no-bad-pairs" + (len (mau/non-joinable-pairs mcf-peano)) + 0) + +;; f(a)=b, a=c : the inner `a` overlaps -> critical pair b vs f(c), NOT joinable +(define + mcf-bad + (mau/parse-module + "fmod B is\n sort T .\n op a : -> T .\n op b : -> T .\n op c : -> T .\n op f : T -> T .\n eq f(a) = b .\n eq a = c .\nendfm")) + +(mcf-check! "bad-not-confluent" (mau/confluent? mcf-bad) false) +(mcf-check! "bad-one-pair" (len (mau/non-joinable-pairs mcf-bad)) 1) +(mcf-check! + "bad-pair-shape" + (mau/cp->str mcf-bad (first (mau/non-joinable-pairs mcf-bad))) + "b f(c)") +(mcf-check! + "bad-has-cps" + (> (len (mau/critical-pairs mcf-bad)) 0) + true) + +;; adding f(c)=b joins the pair -> confluent +(define + mcf-fixed + (mau/parse-module + "fmod F is\n sort T .\n op a : -> T .\n op b : -> T .\n op c : -> T .\n op f : T -> T .\n eq f(a) = b .\n eq a = c .\n eq f(c) = b .\nendfm")) + +(mcf-check! "fixed-confluent" (mau/confluent? mcf-fixed) true) + +;; self-overlap that is joinable: idempotent d(d(X)) = d(X) +(define + mcf-idem + (mau/parse-module + "fmod I is\n sort T .\n op d : T -> T .\n op x : -> T .\n var X : T .\n eq d(d(X)) = d(X) .\nendfm")) + +(mcf-check! "idem-confluent" (mau/confluent? mcf-idem) true) + +;; a free-op overlap that joins: g(h(X)) over h(a) +(define + mcf-join + (mau/parse-module + "fmod J is\n sort T .\n op a : -> T .\n op k : -> T .\n op h : T -> T .\n op g : T -> T .\n op r : T -> T .\n var X : T .\n eq g(h(X)) = r(X) .\n eq h(a) = k .\nendfm")) + +;; g(h(a)) -> r(a) (rule1) or g(k) (rule2 inside). Not joinable unless g(k) reduces. +(mcf-check! "join-not-confluent" (mau/confluent? mcf-join) false) + +;; AC operator, genuinely confluent; joinability uses canonical form +(define + mcf-ac + (mau/parse-module + "fmod AC is\n sort S .\n op a : -> S .\n op b : -> S .\n op _+_ : S S -> S [assoc comm] .\n eq a + a = b .\nendfm")) + +(mcf-check! "ac-confluent" (mau/confluent? mcf-ac) true) + +;; unifier sanity (two-sided): f(X, b) unifies with f(a, Y) +(mcf-check! + "unify-twosided" + (= + nil + (mau/u-unify + (mau/app "f" (list (mau/var "X" "T") (mau/const "b"))) + (mau/app "f" (list (mau/const "a") (mau/var "Y" "T"))) + {})) + false) +;; occurs check: X vs f(X) fails +(mcf-check! + "unify-occurs" + (mau/u-unify + (mau/var "X" "T") + (mau/app "f" (list (mau/var "X" "T"))) + {}) + nil) + +(define mau-confluence-tests-run! (fn () {:failures mcf-failures :total (+ mcf-pass mcf-fail) :passed mcf-pass :failed mcf-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 447049f9..3f20931a 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -162,6 +162,19 @@ spike: it justifies a maude-driven optimiser in `lib/artdag` and the eventual 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. +**Confluence / critical-pair checking (lib/maude/confluence.sx, 12 tests):** +`mau/confluent?` answers the plan's substrate question "can confluence be +checked." Two-sided syntactic unification (`mau/u-unify`, with occurs check) → +critical pairs from LHS overlaps (`mau/critical-pairs`) → joinability via +`mau/ac-equal?` of the normal forms (`mau/non-joinable-pairs` gives the +diagnostics, `mau/cp->str` renders `left right`). Caught `f(a)=b, a=c` as +non-confluent (`b f(c)`); confirmed peano/idempotent/AC examples confluent. +SCOPE: unification is SYNTACTIC — exact for free/constructor ops, an +under-approximation for AC overlaps (full AC-unification is NP/infinitary, out +of scope), but joinability uses the AC-canonical form so AC laws still join +correctly. This is the CID-stability oracle for the artdag optimiser: an +optimisation rule set is content-id-stable iff `mau/confluent?` holds. + Pacing down to hardening. Possible niche future work: membership axioms (`mb`/`cmb`), critical-pair / confluence checking, meta-search, full mixfix (multi-`_` ops, juxtaposition `__`).