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 λ x_{1}⋯λ x_{n}.F(x_{1},…, x_{n})=λ x_{1}⋯λ x_{n}F(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 L^{A}T_{E}X by H^{E}V^{E}A.