About the Confluence of Equational Pattern Rewrite Systems

Alexandre 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.


A. Boudet and E. Contejean. AC-unification of higher-order patterns. pages 267–281.
G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM, 27(4):797–821, Oct. 1980.
J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4), Nov. 1986.
R. Mayr and T. Nipkow. Higher-order rewrite ststems and their confluence. To appear in TCS.

Full Paper

This document was translated from LATEX by HEVEA.