AC matching can be implemented by enumerating the perfect matchings of the bipartite graph (P, N, E), where P is the set of subpatterns to match, N is the set of children of the node we are matching at, and there is an edge in E for every pair (p, n) ∈ P × N such that p matches n.
Associative-Commutative Rewriting on Large Terms has some interesting insights into improving best/average-case performance (slides, paper).
This one is probably the most commonly needed in practice.
[ ] Implement ACU-matching
Reducible to solving systems of inhomogeneous linear Diophantine equations.
[ ] Implement I-matching
[ ] Implement CI-matching
[ ] Implement ACI-matching
[ ] Implement matching modulo the axioms of a boolean ring
[ ] Implement matching modulo the axioms of an abelian group
[ ] Implement matching modulo arbitrary first-order equations using narrowing
We should support
Term
nodes with associativity (A), commutativity (C), unitality (U), and idempotency (I) axioms, and combinations thereof.(P, N, E)
, whereP
is the set of subpatterns to match,N
is the set of children of the node we are matching at, and there is an edge inE
for every pair(p, n) ∈ P × N
such thatp
matchesn
.Unification for all of these is known to be decidable (and algorithms are known for them), though I haven't looked into efficiency for all of them.
Other resources