giles
2dd4c7d974
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 37s
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>
102 lines
3.2 KiB
Plaintext
102 lines
3.2 KiB
Plaintext
;; 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}))
|