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.
CITATION STYLE
Dundua, B., Kutsia, T., & Marin, M. (2019). Variadic Equational Matching. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11617 LNAI, pp. 77–92). Springer Verlag. https://doi.org/10.1007/978-3-030-23250-4_6
Mendeley helps you to discover research relevant for your work.