About the Confluence of Equational Pattern Rewrite SystemsAlexandre Boudet and Evelyne Contejean |
Abstract: We study the confluence of higher-order pattern rewrite systems modulo an equational theory E. This problem has been investigated by Mayr and Nipkow [4], for the case of rewriting modulo a congruence à la Huet [2], (in particular, the equations of E can be applied above the position where a rewrite rule is applied). The case we address here is rewriting using matching modulo E as done in the first-order case by Jouannaud and Kirchner [3].The theory is then applied to the case of AC-theories, for which we provided a complete unification algorithm in [1]. It happens that the AC-unifiers may have to be constrained by some flexible-flexible equations of the form λ x1⋯λ xn.F(x1,…, xn)=λ x1⋯λ xnF(xσ(1),…, xσ(n)), where F is a free variable and σ a permutation. This situation requires a slight technical adaptation of the theory.
This document was translated from LATEX by HEVEA.