maude: confluence / critical-pair checking (12 tests, 274 total)

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) <noreply@anthropic.com>

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

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!)"

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"
 }

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 |

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

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