Associative Commutative Pattern Matching

Abstract

Plotkin [10] has opened the way to the design of unification alRorithm i ncorporating equality axioms and their use in complete proof systems. In particular he gives ~omplete unificati 0n algorithms for terms containing associative function s~hols and for an arithmetic theor y . Huet gives in [18] a unification algorithm for ~-conversion and discusses in [19] Reneral prop ~ rties of complete set of unifiers. A complete and finite alRorithm for unification with associative commutative function symbols is given in Stickel [14] and Lanyford shows in [22] how to ex tend it to abelian group theory. Various other specific unification problems are d i scussed in [ 9,15, 23], In the case of equational theories which possess a complete set of reductions as de f ined in Knuth-Bendix [7], Fay has given in [20,21] a general unification algorithm, We are interested in this paper in the special case of commutative associative fun~tion symbols, We first study the equivalence problem which is reduced to regognizing the equal i ty of two multiset representations. In the same way, matching reduces to generating ordered partit i ons of a multiset, This generation is carried out by two processe~ operating on tree data structure s spanning the lattice of partitions. Cardinality conditions inherited from the matching pr 0 blem are used to cut the search drastically : our processes operate bidirectionnally in a cor o ut i ne mauner, each one trimming sub-structures from both search spaces. The two processes are formally defined by a unique recursive definition, and their computations correspond to a call- ~ y need interpretation of this definition. The correctness of the method is proved formally. This basic organization is used to derive a new algorithm for associative commutative unification improving over Stickel [14]. 1 '~e have programmed in LISP all these algorithms, using 11niversity of Vincennes's V-LISP system [3], We have applied them to the Stickel-Peterson's generali:!:ation of the Knuth and Bendix extension algorithm [7,8,16], Their alp.orithm relies on associativecommutative unification for the computation of critical pairs, hut also most critically O il associative-commutative match, in order to reduce terms to their normal forms. ~tickel and Peterson proposed to use unification for matching, hut this leads to unnecessary inefficienc i es that preclude the practical use of their method, Fe give in the Appendix running times on a DEC KLIO using the VLISP system, correspondinp, to some of their examples, Most proofs are omitted in this version, the full paper is available as a techn i cal report [24],