AC-Unification of Higher-order Patterns

Abstract: We present a complete algorithm for the unification of higher-order patterns modulo the associative-commutative theory of some constants +₁,…, +_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.

References

[1]

J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT-Press, 1991.

[2]

Z. Qian and K. Wang. Modular AC-Unification of Higher-Order Patterns. pages 105–120.

This document was translated from L^AT_EX by H^EV^EA.