Variadic Equational Matching

摘要

In this paper we study matching in equational theories that specify counterparts of associativity and commutativity for variadic function symbols. We design a procedure to solve a system of matching equations and prove its soundness and completeness. The complete set of incomparable matchers for such a system can be infinite. From the practical side, we identify two finitary cases and impose restrictions on the procedure to get an incomplete terminating algorithm, which, in our opinion, describes the semantics for associative and commutative matching implemented in the symbolic computation system Mathematica.