maude: Phase 4 conditional equations (19 tests, 138 total)

lib/maude/conditional.sx — condition-aware reducer. ceq fires only when
its guard holds: equational guards (l=r reduce to same normal form) and
boolean guards (term reduces to true), evaluated by recursing through the
same reducer. Verified on gcd, insertion sort, max, even.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

lib/maude/conditional.sx

@@ -0,0 +1,144 @@
+;; lib/maude/conditional.sx — conditional equations (Phase 4).
+;;
+;; A condition-aware superset of the Phase 3 reducer. `ceq L = R if COND` fires
+;; only when COND holds under the matching substitution. Conditions come from
+;; the parser as:
+;;   {:kind :eq :lhs L :rhs R}   — holds iff reduce(s L) =AC= reduce(s R)
+;;   {:kind :bool :term T}       — holds iff reduce(s T) =AC= true
+;; Condition evaluation recurses through the SAME reducer (mau/cnormalize), so
+;; a ceq whose guard mentions other (possibly conditional) equations Just Works
+;; — 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.
+
+(define
+  mau/ac-candidates
+  (fn
+    (theory f th eq term)
+    (let
+      ((id (get th :id))
+        (pels (mau/flatten-op theory f (get eq :lhs)))
+        (sels (mau/flatten-op theory f term)))
+      (let
+        ((matches (if (get th :comm) (mau/match-multiset theory f (mau/append2 pels (list (mau/var "$R" ""))) sels {} id) (mau/match-sequence theory f (mau/append2 (list (mau/var "$L" "")) (mau/append2 pels (list (mau/var "$R" "")))) sels {} id))))
+        (map (fn (s) {:s s :result (mau/ac-eq-result theory f th eq s)}) matches)))))
+
+(define
+  mau/eq-candidates
+  (fn
+    (theory eq term)
+    (let
+      ((lhs (get eq :lhs)))
+      (let
+        ((th (if (mau/app? lhs) (mau/th-of theory (mau/op lhs)) {:id nil :assoc false :comm false})))
+        (if
+          (and (mau/app? lhs) (get th :assoc))
+          (mau/ac-candidates theory (mau/op lhs) th eq term)
+          (map (fn (s) {:s s :result (mau/subst-apply s (get eq :rhs))}) (mau/mm theory lhs term {})))))))
+
+(define
+  mau/cond-holds?
+  (fn
+    (theory eqs cond s)
+    (if
+      (= cond nil)
+      true
+      (if
+        (= (get cond :kind) "eq")
+        (mau/ac-equal?
+          theory
+          (mau/cnormalize
+            theory
+            eqs
+            (mau/subst-apply s (get cond :lhs))
+            mau/reduce-fuel)
+          (mau/cnormalize
+            theory
+            eqs
+            (mau/subst-apply s (get cond :rhs))
+            mau/reduce-fuel))
+        (mau/ac-equal?
+          theory
+          (mau/cnormalize
+            theory
+            eqs
+            (mau/subst-apply s (get cond :term))
+            mau/reduce-fuel)
+          (mau/const "true"))))))
+
+(define
+  mau/try-candidates
+  (fn
+    (theory all-eqs cond term cands)
+    (if
+      (empty? cands)
+      nil
+      (let
+        ((c (first cands)))
+        (if
+          (and
+            (not (mau/ac-equal? theory (get c :result) term))
+            (mau/cond-holds? theory all-eqs cond (get c :s)))
+          (get c :result)
+          (mau/try-candidates theory all-eqs cond term (rest cands)))))))
+
+(define
+  mau/crewrite-loop
+  (fn
+    (theory all-eqs eqs term)
+    (if
+      (empty? eqs)
+      nil
+      (let
+        ((r (mau/try-candidates theory all-eqs (get (first eqs) :cond) term (mau/eq-candidates theory (first eqs) term))))
+        (if (= r nil) (mau/crewrite-loop theory all-eqs (rest eqs) term) r)))))
+
+(define
+  mau/crewrite-top
+  (fn (theory eqs term) (mau/crewrite-loop theory eqs eqs term)))
+
+(define
+  mau/cnormalize
+  (fn
+    (theory eqs term fuel)
+    (if
+      (<= fuel 0)
+      term
+      (cond
+        ((mau/var? term) term)
+        ((mau/app? term)
+          (let
+            ((nargs (map (fn (a) (mau/cnormalize theory eqs a fuel)) (mau/args term))))
+            (let
+              ((t2 (mau/app (mau/op term) nargs)))
+              (let
+                ((r (mau/crewrite-top theory eqs t2)))
+                (if
+                  (= r nil)
+                  t2
+                  (mau/cnormalize theory eqs r (- fuel 1)))))))
+        (else term)))))
+
+(define
+  mau/creduce
+  (fn
+    (m term)
+    (mau/cnormalize
+      (mau/build-theory m)
+      (mau/module-eqs m)
+      term
+      mau/reduce-fuel)))
+
+(define
+  mau/creduce-term
+  (fn (m src) (mau/creduce m (mau/parse-term-in m src))))
+
+(define
+  mau/creduce->str
+  (fn (m src) (mau/term->str (mau/creduce-term m src))))
+
+(define
+  mau/ccanon
+  (fn (m src) (mau/canon (mau/build-theory m) (mau/creduce-term m src))))

lib/maude/conformance.conf

@@ -10,10 +10,12 @@ PRELOADS=(
   lib/maude/parser.sx
   lib/maude/reduce.sx
   lib/maude/matching.sx
+  lib/maude/conditional.sx
 )
 
 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!)"
+  "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)"
 )

lib/maude/scoreboard.json

@@ -1,12 +1,13 @@
 {
   "lang": "maude",
-  "total_passed": 119,
+  "total_passed": 138,
   "total_failed": 0,
-  "total": 119,
+  "total": 138,
   "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":"matching","passed":28,"failed":0,"total":28},
+    {"name":"conditional","passed":19,"failed":0,"total":19}
   ],
-  "generated": "2026-06-07T15:00:34+00:00"
+  "generated": "2026-06-07T15:05:31+00:00"
 }

lib/maude/scoreboard.md

@@ -1,9 +1,10 @@
 # maude scoreboard
 
-**119 / 119 passing** (0 failure(s)).
+**138 / 138 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
 | parse | 65 | 65 | ok |
 | reduce | 26 | 26 | ok |
 | matching | 28 | 28 | ok |
+| conditional | 19 | 19 | ok |

lib/maude/tests/conditional.sx

@@ -0,0 +1,108 @@
+;; lib/maude/tests/conditional.sx — Phase 4: conditional equations.
+
+(define mct-pass 0)
+(define mct-fail 0)
+(define mct-failures (list))
+
+(define
+  mct-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mct-pass (+ mct-pass 1))
+      (do
+        (set! mct-fail (+ mct-fail 1))
+        (append!
+          mct-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; ---- gcd (equational guard, recursive) ----
+
+(define
+  mct-gcd
+  (mau/parse-module
+    "fmod GCD 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 _-_ : Nat Nat -> Nat .\n  op gcd : Nat Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 > Y = false .\n  eq s X > 0 = true .\n  eq s X > s Y = X > Y .\n  eq X - 0 = X .\n  eq 0 - Y = 0 .\n  eq s X - s Y = X - Y .\n  eq gcd(X, 0) = X .\n  eq gcd(0, Y) = Y .\n  eq gcd(X, X) = X .\n  ceq gcd(X, Y) = gcd(X - Y, Y) if X > Y = true .\n  ceq gcd(X, Y) = gcd(Y, X) if Y > X = true .\nendfm"))
+
+(mct-check!
+  "gcd-6-4"
+  (mau/creduce->str mct-gcd "gcd(s s s s s s 0, s s s s 0)")
+  "s_(s_(0))")
+(mct-check!
+  "gcd-3-6"
+  (mau/creduce->str mct-gcd "gcd(s s s 0, s s s s s s 0)")
+  "s_(s_(s_(0)))")
+(mct-check!
+  "gcd-base-zero"
+  (mau/creduce->str mct-gcd "gcd(s s 0, 0)")
+  "s_(s_(0))")
+(mct-check!
+  "gcd-equal"
+  (mau/creduce->str mct-gcd "gcd(s s 0, s s 0)")
+  "s_(s_(0))")
+(mct-check!
+  "gcd-coprime"
+  (mau/creduce->str mct-gcd "gcd(s s s 0, s s 0)")
+  "s_(0)")
+;; guard predicate reductions
+(mct-check! "gt-true" (mau/creduce->str mct-gcd "s s 0 > s 0") "true")
+(mct-check! "gt-false" (mau/creduce->str mct-gcd "s 0 > s s 0") "false")
+
+;; ---- insertion sort (true/false guards) ----
+
+(define
+  mct-sort
+  (mau/parse-module
+    "fmod SORT is\n  sorts Nat List 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 nil : -> List .\n  op _:_ : Nat List -> List .\n  op insert : Nat List -> List .\n  op sort : List -> List .\n  vars M N : Nat .\n  var L : List .\n  eq 0 <= N = true .\n  eq s M <= 0 = false .\n  eq s M <= s N = M <= N .\n  eq insert(N, nil) = N : nil .\n  ceq insert(N, M : L) = N : (M : L) if N <= M = true .\n  ceq insert(N, M : L) = M : insert(N, L) if N <= M = false .\n  eq sort(nil) = nil .\n  eq sort(N : L) = insert(N, sort(L)) .\nendfm"))
+
+(mct-check!
+  "sort-321"
+  (mau/creduce->str mct-sort "sort(s s s 0 : (s 0 : (s s 0 : nil)))")
+  "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")
+(mct-check! "sort-empty" (mau/creduce->str mct-sort "sort(nil)") "nil")
+(mct-check!
+  "sort-singleton"
+  (mau/creduce->str mct-sort "sort(s s 0 : nil)")
+  "_:_(s_(s_(0)), nil)")
+(mct-check!
+  "insert-front"
+  (mau/creduce->str mct-sort "insert(0, s 0 : (s s 0 : nil))")
+  "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))")
+(mct-check!
+  "insert-back"
+  (mau/creduce->str mct-sort "insert(s s s 0, s 0 : (s s 0 : nil))")
+  "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")
+
+;; ---- max (conditional simplification, both branches) ----
+
+(define
+  mct-max
+  (mau/parse-module
+    "fmod MAX 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 max : Nat Nat -> Nat .\n  vars M N : Nat .\n  eq 0 <= N = true .\n  eq s M <= 0 = false .\n  eq s M <= s N = M <= N .\n  ceq max(M, N) = M if N <= M = true .\n  ceq max(M, N) = N if N <= M = false .\nendfm"))
+
+(mct-check!
+  "max-left"
+  (mau/creduce->str mct-max "max(s s s 0, s 0)")
+  "s_(s_(s_(0)))")
+(mct-check!
+  "max-right"
+  (mau/creduce->str mct-max "max(s 0, s s 0)")
+  "s_(s_(0))")
+(mct-check!
+  "max-equal"
+  (mau/creduce->str mct-max "max(s s 0, s s 0)")
+  "s_(s_(0))")
+
+;; ---- boolean-kind condition (`if pred`) ----
+
+(define
+  mct-even
+  (mau/parse-module
+    "fmod EVEN is\n  sorts Nat Bool Tag .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op even : Nat -> Bool .\n  op evn : -> Tag .\n  op odd : -> Tag .\n  op tag : Nat -> Tag .\n  var N : Nat .\n  eq even(0) = true .\n  eq even(s 0) = false .\n  eq even(s s N) = even(N) .\n  ceq tag(N) = evn if even(N) .\n  ceq tag(N) = odd if even(N) = false .\nendfm"))
+
+(mct-check! "even-4" (mau/creduce->str mct-even "even(s s s s 0)") "true")
+(mct-check! "even-3" (mau/creduce->str mct-even "even(s s s 0)") "false")
+(mct-check! "tag-even-bool" (mau/creduce->str mct-even "tag(s s 0)") "evn")
+(mct-check! "tag-odd" (mau/creduce->str mct-even "tag(s s s 0)") "odd")
+
+(define mau-conditional-tests-run! (fn () {:failures mct-failures :total (+ mct-pass mct-fail) :passed mct-pass :failed mct-fail}))

plans/maude-on-sx.md

@@ -81,9 +81,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
 - [x] 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.
+- [x] `ceq L = R if Cond` — apply only when `Cond` reduces to true.
+- [x] Recursion via the same reduce engine (terminating because Cond is shorter).
+- [x] Tests: gcd, sorting, conditional simplifications.
 
 ### Phase 5 — System modules + rewrite rules
 - [ ] `mod ... endm` syntax with `rl` rules.
@@ -177,5 +177,23 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
     oracle. `$EMPTY` is a transient marker for empty rest blocks w/o id; never
     leaks past `mau/restv`.
 
+- **Phase 4 (conditional equations) — DONE, 138/138 total.**
+  `lib/maude/conditional.sx` is a condition-aware superset of the Phase 3
+  reducer. `mau/eq-candidates` enumerates (subst, result) pairs for an
+  equation (AC via rest-var extension `mau/ac-candidates`, else `mau/mm`);
+  `mau/try-candidates` commits the first candidate that both makes progress
+  (canonical form changes) AND whose guard holds. `mau/cond-holds?` evaluates
+  `{:kind :eq}` guards (reduce both sides, `ac-equal?`) and `{:kind :bool}`
+  guards (reduce, `=AC= true`), recursing through `mau/cnormalize` — same
+  reducer, so guards can mention other (conditional) equations. Public:
+  `mau/creduce` / `mau/creduce->str` / `mau/ccanon`. Verified on gcd
+  (subtractive, recursive guard), insertion sort (true/false branches), max,
+  and even (bool-kind `if pred` guard).
+  - Notes for next phases: `mau/creduce` is the canonical reducer now; Phase 5
+    rules reduce to normal form via creduce between rewrite steps. `_:_` cons
+    parses LEFT-assoc (no `gather` support yet) — write list literals
+    right-parenthesized, or add a `gather`/parse-assoc attr later if a test
+    needs bare `a : b : c`.
+
 ## Blockers
 _(none)_