Fast matching in combinations of regular equational theories

S. Eker

We consider the problem of efficient term matching, modulo combinations of regular equational theories. Our general approach to the problem consists of three phases: compilation, matching and subproblem solving. We describe a technique for dealing with non-linear variables in a pattern and show how this technique is specialized to several specific equational theories. For matching in an order-sorted setting we discuss an important optimization for theories involving the associativity equation. Finally we sketch a new method of combining matching algorithms for regular collapse theories and give examples that involve the identity and idempotence equations.

(BibTeX entry)    (gzip'ed Postscript)   

back   home   Formal Methods and Declarative Languages Laboratory   Computer Science Laboratory, SRI International