Improve matching algorithm to efficiently support axioms

[taktoa]

We should support Term nodes with associativity (A), commutativity (C), unitality (U), and idempotency (I) axioms, and combinations thereof.

• Implement A-matching
  • Building-in equational theories by Plotkin
• Implement AU-matching
• Implement C-matching
  • NP-complete
• Implement AC-matching
  • NP-complete
  • 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
  • Maude Manual - Chapter 16 - Narrowing
  • Basic narrowing revisited
  • Programming with narrowing: a tutorial
  • Maybe start by shelling out to Maude or Curry?
• Implement higher-order matching

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

• Maude Manual (Version 2.5)
• Summer 2014 RISC class on Unification Theory
  • Lecture 1 - Syntactic Unification
  • Lecture 2 - Speeding Up Unification
  • Lecture 3 - Matching
  • Lecture 4 - Equational Unification
  • Lecture 5 - Solving Diophantine Systems
  • Lecture 6 - Narrowing
  • Lecture 7 - Higher-Order Unification
  • Lecture 8 - Applications of Unification
• Loop detection in term rewriting using the eliminating unfoldings
• A DPLL-based Theorem Prover for Coherent Logic
  • Rete matching can be used (see Efficient Rule-Matching for Automated Coherent Logic) for first-order theorem proving in coherent logic, so this may be relevant. Also see Efficient Rule-Matching for Hyper-Tableaux.
• Handbook of Automated Reasoning