Variadic equational matching in associative and commutative theories. (September 2021)

• Record Type: Journal Article
• Authors: Dundua, Besik; Kutsia, Temur; Marin, Mircea
• Is Part Of: Journal of symbolic computation. Volume 106(2021)
• Page Start: 78
• Page End: 109
• Publication Date: 2021-09
• Subjects: 03B70 -- 68Q42 -- 68N15 -- 33F10; Pattern matching -- Equational theories -- Variadic symbols -- Mathematica; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2021.01.001
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: 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 termination, soundness, completeness, and minimality. The minimal complete set of matchers for such a system can be infinite, but our algorithm computes its finite representation in the form of solved set. From the practical side, we identify two finitary cases and impose restrictions on the procedure to get an incomplete algorithm, which, based on our experiments, describes the input-output behavior and properties of Mathematica's flat and orderless pattern matching.