About the Confluence of Equational Pattern Rewrite Systems

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₁⋯λ x_n.F(x₁,…, x_n)=λ x₁⋯λ x_nF(x_σ(1),…, x_σ(n)), where F is a free variable and σ a permutation. This situation requires a slight technical adaptation of the theory.

References

[1]

A. Boudet and E. Contejean. AC-unification of higher-order patterns. pages 267–281.

[2]

G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM, 27(4):797–821, Oct. 1980.

[3]

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.

[4]

R. Mayr and T. Nipkow. Higher-order rewrite ststems and their confluence. To appear in TCS.

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