Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 AC-Unification of Higher-order Patterns
AC-Unification of Higher-order Patterns
Alexandre Boudet and Evelyne Contejean
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
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. 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.