Search

The problem of termination of a set R of rules modulo a set E of equations, called E-termination problem, arises when trying to complete the set of rules in order to get a Church-Rosser property for the rules modulo the equations. We first show here that termination of the rewriting relation and E-termination are the same whenever the used rewriting relation is E-commuting, a property inspired from Peterson and Stickel’s E-compatibility property. More precisely, their results can be obtained by requiring termination of the rewriting relation instead of E-termination if E-commutation is used instead of E-compatibility. When the rewriting relation is not E-commuting, we show how to reduce E-termination for the starting set of rules to classical termination of the rewriting relation of an extended set of rules that has the E-commutation property. This set can be classicaly constructed by computing critical pairs or extended pairs between rules and equations, according to the used rewriting relation. In addition we show that different orderings can be used for the starting set of rules and the added critical or extended pairs. Interesting issues for further research are also discussed.

Conventional algebraic specifications are first-order. Using higher-order equations in combination with first-order ones raises several fundamental model-theoretic and proof-theoretic questions. The model theory of higher-order equations is well understood (see [20] for a survey of algebraic specifications). The proof theory of higher-order equations is equally well understood, it requires higher- order matching, and higher-order rewriting therefore providing with a simple execution model. Higher-order variables may be instantiated by functions described by λ-expressions, bringing in λ-calculus, whose execution model is again rewriting (β-redexes). Hence rewriting is at the heart of all three execution models, which makes their combination quite simple on the operational side. The main question reviewed in this paper is whether the Church-Rosser and termination properties of these three execution models are preserved within their combination. We will see that the answer is to a large extent positive.