“Syntactic” AC-Unification

Abstract: The rules for unification in a simple syntactic theory, using Kirchner’s mutation [1, 2] do not terminate in the case of associative-commutative theories. We show that in the case of a linear equation, these rules terminate, yielding a complete set of solved forms, each variable introduced by the unifiers corresponding to a (trivial) minimal solution of the (trivial) Diophantine equation where all coefficients are 1. A non-linear problem can be first treated as a linear one, that is considering two occurrences of a same variable as two different variables. After this step, one has to solve the equations between the different values that have been obtained for the different occurrences of a same variable. We show that one can restrict the search of the solutions of these latter equations to linear substitutions. This result is based on the analysis of how the minimal solutions of a linear Diophantine equation can be built-up using the solutions of the trivial Diophantine equation associated with the linearized AC-equation. This provides a new AC-unification algorithm which does not make an explicit use of the solving of linear Diophantine equations.

References

[1]

C. Kirchner. Méthodes et outils de conception systématique d’algorithmes d’unification dans les théories equationnelles. Thèse d’Etat, Univ. Nancy, France, 1985.

[2]

C. Kirchner. Computing unification algorithms. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., pages 206–216, 1986.

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