|
|
2dd4c7d974
|
maude: confluence / critical-pair checking (12 tests, 274 total)
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>
|
2026-06-07 20:18:33 +00:00 |
|
