AC-Unification of Higher-order PatternsAlexandre Boudet and Evelyne Contejean |
Abstract: We present a complete algorithm for the unification of higher-order patterns modulo the associative-commutative theory of some constants +_{1},…, +_{n}. Given an AC-unification problem over higher-order patterns, the output of the algorithm is a finite set DAG solved forms [1], constrained by some flexible-flexible equations with the same head on both sides. Indeed, in the presence of AC constants, such equations are always solvable, but they have no minimal complete set of unifiers [2]. We prove that the algorithm terminates, is sound, and that any solution of the original unification problem is an instance of one of the computed solutions which satisfies the constraints.
This document was translated from L^{A}T_{E}X by H^{E}V^{E}A.