Modular Termination of Term Rewriting Systems Revisited ^{⋆}

Maribel Fernández and Jean-Pierre Jouannaud^{1}

Laboratoire de Recherche en Informatique, Bât. 490 CNRS et Université de Paris Sud, 91405 Orsay, France

                     email: {maribel,jouannau}@lri.fr

1 Introduction

Confluent and terminating term rewriting systems are a major tool for prototyping algebraic specifications. This paper is concerned with the impact of stepwise development methodologies on prototyping.

Assume given two modules, each one specifying a set D_{i} (i = 0, 1) of defined functions with respect to a given set C_{i} of constructors by means of a set R_{i} of rewrite rules. By definition, D_{i} is the set of symbols heading the left-hand sides of rules, the other symbols being in C_{i}. The set F_{i} = C_{i}∪D_{i} is called the signature of the module. Putting these two modules together results in the union of the two rewriting systems R_{0} and R_{1}, written R_{0} ∪ R_{1}. In the unions we consider, D_{0} ∩ D_{1} = ∅. We distinguish three kinds of unions of increasing generality:

Disjoint union, denoted by R_{0} ⊕ R_{1}, if F_{0} ∩ F_{1} = ∅.

Combined union, denoted by R_{0} ⊎ R_{1}, if F_{0} ∩ F_{1} = C_{0} ∩ C_{1}, i.e. in this class of unions only constructors may be shared.

Hierarchical union, denoted by R_{0} +R_{1}, if F_{0} ∩D_{1} = ∅, but F_{1} ∩D_{0} ≠ ∅, that is, the systems may share constructors, and moreover the defined symbols of R_{0} may be constructors of R_{1}. In R_{0} + R_{1}, R_{0} is the base, and R_{1} the enrichment. There may be several successive enrichments in a hierarchical union.

Since obtaining a confluent and terminating rewriting system from a set of equations may be a hard task, it is desirable that both properties are closed under these unions. A property of term rewriting systems is modular if it is closed under union. Neither termination nor confluence is closed under arbitrary union. However, it is well known that confluence is a modular property of disjoint unions, a celebrated result of Toyama [25]. This is not true of combined union, as pointed out by Kurihara and Ohuchi [13]. In contrast, termination is not a modular property, even of disjoint unions [24]:

R_{0} = {f(0, 1, x) → f(x, x, x)}, R_{1} = {g(x, y) → x, g(x, y) → y}

Indeed, there is the following infinite reduction sequence:

f(g(0, 1), g(0, 1), g(0, 1)) → f(0, g(0, 1), g(0, 1)) → f(0, 1, g(0, 1)) → f(g(0, 1), g(0, 1), g(0, 1)) …

⋆ This work was partly supported by the ”Greco de programmation du CNRS”, and the ESPRIT Basic Research Action COMPASS.

Contradicting hopes, the above example can be refined so as to have confluent definitions for both rewrite systems [4]:

R_{0} = {f(0, 1, x) → f(x, x, x), f(x, y, z) → 2, 0 → 2, 1 → 2}
R_{1} = {g(x, y, y) → x, g(y, y, x) → x}

for which there is again an infinite reduction sequence originating from f(g(0, 2, 1), g(0, 2, 1), g(0, 2, 1)).

It however turns out that the existence of normal forms for all terms is a modular property of disjoint unions [17]. So, if two rewrite systems are both confluent and terminating, their disjoint union enjoys unique normal forms even when there are infinite reduction sequences. For example, reducing all subterms of f(g(0, 2, 1), g(0, 2, 1), g(0, 2, 1)) in the above sequence to 2 yields the normal form 2. Using implicitely a result of Rusinowitch [23] for non-duplicating disjoint unions, Kurihara and Ohuchi pointed out that a very simple strategy allows to compute this normal form: shared rewriting in which different occurrences of a same variable in a right-hand side of rule are shared. This strategy is indeed implemented in any rewriting software for efficiency reasons. So, prototyping disjoint unions operates safely. This is also true of combined unions [13], and can be generalized to even more complex situations [17].

Our goal is to work out a comprehensible theory of modularity of termination, by presenting all these results in a coherent framework^{2}. Let us call homogeneous in a union R_{0} ∪ R_{1} a term which uses function symbols of one signature only, and does not use defined symbols that belong also to the other signature. Nonhomogeneous terms can be split into a maximal homogeneous top part called cap and a multiset of pending subterms called aliens. Roughly speaking, a rewrite relation on terms is alien-decreasing if rewriting inside the cap of a term does not increase the multiset of aliens with respect to the subterm relation. This abstract property of rewrite relations is the key to modularity of disjoint and combined unions, and also plays a role for the modularity of hierarchical unions.

A key contribution of this paper is a simple proof of modularity of termination of unions of alien-decreasing rewrite relations, see section 4. This result subsumes previous results applying to disjoints unions [23], combined unions [13] and crosswise disjoint unions [19], since shared rewrite systems, non-duplicating rewrite systems and crosswise disjoint systems are alien-decreasing, as shown in section 3. It also may apply to hierarchical or even more general unions.

For hierarchical unions, we present a second modularity result that applies when the base is alien-decreasing and enrichments obey a generalised primitiverecursive schema, see section 6. This yields new modularity results, related to the recent results of Krishna Rao [20, 21], Gramlich [7] and Dershowitz [2].

The above results generalize to reductive conditional rewrite systems [10], and to rewriting modulo equations whose congruence classes are finite.

2 There are other results in this area, which do not relate directly to ours, however, and are not discussed here for lack of space.

2 Preliminaries

We assume the reader familiar with the basic concepts and notations of term rewriting systems. We refer to [3] for missing definitions and notations.

A signature F is a finite set of function symbols together with their (fixed) arity. X denotes a denumerable set of variables, T (F) denotes the set of ground terms over F and T (F, X) denotes the set of terms built up from F and X.

Terms are identified with finite labelled trees as usual. Positions are strings of positive integers. Λ denotes the empty string (root position) and ′′.′′ denotes string concatenation. We use Pos(t) for the set of positions in t, and FPos(t) for its set of non-variable positions. The prefix ordering (resp. lexicographic ordering) on positions is denoted by > (resp. >_{lex}^{N}) and the strict subterm relationship by <. The encompassment ordering, denoted by ^{•} <, is the strict part of the quasi-ordering: u ^{•} ≤v if v|_{p} = uσ for some position p and substitution σ and its equivalence corresponds to variable renaming. Subsumption is a special case of encompassment (in which u is an instance of v). We use root(t) for the variable or function symbol at the root of t. The subterm of t at position p is denoted by t|_{p} and the result of replacing t|_{p} with u at position p in t is denoted by t[u]_{p}. This notation is also used to indicate that u is a subterm of t. Var(t) denotes the set of variables appearing in t. A term is linear if variables in Var(t) occur at most once in t. If t is non-linear, it can be linearized resulting in a linear term t′ such that t = t′ξ, where ξ is a substitution from Var(t′) to Var(t).

Substitutions are written as in {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} where t_{i} is assumed different from x_{i}. We use greek letters for substitutions and postfix notation for their application.

A term rewriting system is a set of rewrite rules R = {l_{i} → r_{i}}_{i}, where l_{i} ∉ X and Var(r_{i}) ⊆ Var(l_{i}). A term t rewrites to a term u at position p with the rule l → r and the substitution σ, written t⟶_{l→r}^{p}u, or simply t →_{R} u, if t|_{p} = lσ

and u = t[rσ]_{p}. Such a term t is called reducible. Irreducible terms are said in normal form. A term t is strongly normalizable if every reduction sequence out of t is finite, hence ends in a normal form of t. A substitution γ is strongly normalizable if xγ is strongly normalizable for all x. We denote by →_{R}^{+} (resp. →_{R}^{∗}) the transitive (resp. transitive and reflexive) closure of the rewrite relation →_{R}. The subindex R will be omitted when it is clear from the context.

A term rewriting system R is

– confluent if t →^{∗} u and t →^{∗} v implies u →^{∗} s and v →^{∗} s for some s,

– terminating (or strongly normalizing) if all reduction sequences are finite,

– convergent if it is confluent and terminating,

– collapsing if it contains a rule whose right-hand side is a variable,

– conservative (also called non-duplicating) if for all l → r ∈ R and for all x ∈ Var(l), the number of occurrences of x in r is less than or equal to the number of occurrences of x in l.

3 Alien-decreasing unions

We first need some vocabulary. Given a term rewriting system R, recall that its signature F is partitioned into a set D = {f ∈ F | f = root(l), l → r ∈ R} of defined symbols and a set C = F − D of constructors. We may write D ∪ C for F.

Definition 1. Let R_{0} and R_{1} be two rewrite systems over the respective signatures F_{0} = C_{0}∪D_{0} and F_{1} = C_{1}∪D_{1} such that D_{0}∩D_{1} = ∅. Let R = R_{0}∪R_{1} be the union of the two rewrite systems, F = F_{0} ∪ F_{1} be the union of the two signatures, and S = C_{0} ∩ C_{1} the set of shared constructors. A term in T (F, X) is homogeneous if it uses function symbols of F_{0} − D_{1} or F_{1} − D_{0} exclusively (it is homogeneous with respect to the signature F_{0} in the first case, and with respect to F_{1} in the latter). A term in T (F, X) is quasi-homogeneous if it has the form s[t_{1}, …, t_{n}]_{p_{1},...,p_{n}}, where s[x_{1}, …, x_{n}]_{p_{1},...,p_{n}} ∈ T (S, X), and {t_{i} : i ∈ [1..n]} is a multiset of homogeneous terms. Derivations using rules in R are homogeneous if all terms in the sequence are homogeneous with respect to the same signature.

For combined unions, our definition of homogeneous terms corresponds to the usual definition (i.e. a term t ∈ T (F, X) is homogeneous in a combined union if t ∈ T (F_{0}, X) ∪ T (F_{1}, X)). For more general unions, note that a term built up with symbols from F_{0} (resp. F_{1}) may be non-homogeneous.

Non-homogeneous derivations may be homogenized by computing caps and aliens. The cap of a term is its maximal (with respect to subsumption) topmost quasi-homogeneous part, the subterms pending from the cap being called aliens.

Definition 2. Let ξ be a one to one correspondence between the set of terms T (F, X) and a denumerable set Y ⊇ X, such that ξ(x) = x for all x ∈ X. If t is quasi-homogeneous, then cap(t) = t and aliens(t) = ∅. Otherwise, t = sσ, where s ∈ T (F, Y) is quasi-homogeneous and maximal with respect to subsumption, and ∀y ∈ Var(s), yσ = ξ(y). We define cap(t) to be the term s and aliens(t) to be the multiset of terms {yσ | y ∈ (Y − X) ∩ Var(s)} where each term yσ appears as many times as the number of occurrences of y in s. Let c_{i} a new constructor symbol added to F_{i}, and c_{i}(s) the cap of the term c_{i}(t). We define cap(t, i), the cap of t w.r.t. R_{i} (resp. aliens(t, i), the multiset of aliens of t w.r.t. R_{i}), to be the term s (resp. the multiset of terms aliens(t)).

Example 1. Let F_{0} = {f, c}, F_{1} = {g, c}, X = {x}, Y ⊃ {x, y}. Then cap(c(f(g(x)), g(x))) = c(f(y), g(x)), and cap(c(f(g(x)), g(x)), 0) = c(f(y), y). Assume now we have the rule f(f(x)) → c(f(x), x). Then, f(f(g(x)), whose cap is homogeneous, rewrites to c(f(g(x)), g(x)), whose cap is quasi-homogeneous, but not homogeneous.

Note that the cap of a term is defined up to renaming of variables in Y − X, since the one to one correspondance ξ is arbitrary on Y − X.

Definition 3. A relation → on terms in the union is alien-decreasing if s → t in a cap position of s with a rule of R_{i} implies aliens(s, i) >_{mul} aliens(t, i), or aliens(s, i) =_{mul} aliens(t, i) and cap(s, i) →^{+} ∪ ^{•} >cap(t, i).

Note that instead of the ordering →^{+} ∪ ^{•}>, we could use any well-founded extension of →^{+} provided it is compatible with ^{•}>. The above is the only one known, but recent results of Rubio may change this situation [22].

Quasi-homogeneous terms may have symbols from both D_{0} and D_{1} provided their root is a shared constructor. Rewriting a quasi-homogeneous term amounts to rewrite one of its homogeneous subterms and results in a quasi-homogeneous term if the rules are alien-decreasing. In this sense, quasi-homogeneous terms behave like homogeneous ones for alien-decreasing rules, therefore:

Property 4. If R_{0}, R_{1} are terminating and alien-decreasing, then R_{0} ∪ R_{1} is terminating on quasi-homogeneous terms.

We now start investigating particular cases of alien-decreasing unions.

3.1 Conservative combined unions

It is rather straightforward to see that a combined union is alien-decreasing iff it is conservative. Of particular interest is the case of shared rewriting, that is, rewriting on directed acyclic graphs (dags) representing terms (see [13, 5] for details). In this way, multiple occurrences of a subterm may be simultaneously reduced to a common term. In a shared-reduction step, subterms that are covered by the same variable in the left-hand side of the rule are not copied but shared in the resulting dag, even if the right-hand side of the rule has multiple occurrences of this variable. Hence, shared-rewriting is alien-decreasing for combined unions, or more generally, when the right-hand sides of the rules are homogeneous terms. So, all results applying to conservative combined unions apply as well to combined unions with shared rewriting.

3.2 Conservative stratified unions

We can relax the hypothesis that we have a combined union, by assuming that the right-hand sides of rules are homogeneous, and that the left-hand sides may not be, yielding a stratified union. Still, we need the conservativity condition (or sharing) for those variables whose all occurrences appear immediately below the cap of the left hand side. Again, such rules are alien-decreasing.

The crosswise disjoint unions defined by D. Plump [18, 19] as unions R_{0} ∪R_{1} such that the right-hand sides of R_{i} have no common function symbol with the left-hand side of R_{1−i}, are particular cases of conservative stratified unions, in which shared constructors cannot appear in right-hand sides.

Example 2. Let {R_{1} = f(h(x), c(c(x))) → f(x, c(x))}. The right-hand side f(x, c(x)) is homogeneous in a union R_{0} ∪ R_{1} for any rewrite system R_{0} which does not have f and c as defined symbols. E.g. if we take {R_{0} = h(c(x)) → x} then we obtain a conservative stratified union, which is neither a combined union nor a crosswise disjoint union. Starting from the term f(h(h(x)), c(c(h(x)))) whose cap is f(y, c(c(z))) and multiset of aliens is {h(h(x)), h(x)}, we obtain by R_{1} f(h(x), c(h(x))) whose cap is f(z, c(z)) and multiset of aliens is {h(x), h(x)}.

3.3 Alien-decreasing hierarchical unions

In a hierarchical union R_{0} + R_{1} the rules in R_{0} are homogeneous, but the rules in R_{1} may not be (of course, not all hierarchical unions are alien-decreasing).

Since in the previous example R_{0} is homogeneous, R_{0} + R_{1} is an aliendecreasing hierarchical union, as well as a conservative stratified union. But there are hierarchical unions that are not stratified and vice-versa.

Example 3. Take {R_{1} = f(c(x), h(h(x))) → f(x, h(x))}. R_{1} is alien decreasing for any rewrite system that has h or c as defined symbol, because alien subterms decrease strictly in the subterm relationship. E.g., if {R_{0} = h(c(x)) → x}, R_{0} + R_{1} is an alien-decreasing hierarchical union which is neither a combined union nor a stratified union. Starting from the term f(c(c(x)), h(h(c(x)))) whose cap is f(c(c(x)), y) and multiset of aliens is {h(h(c(x)))}, we obtain by R_{1} f(c(x), h(c(x))) whose cap is f(c(x), y′) and multiset of aliens is {h(c(x))}. Keeping the same set R_{0}, the example {R_{1} = f(c(x), h(x)) → f(x, h(x))} is also alien-decreasing under the same hypothesis, because aliens are equal and the cap decreases strictly in the encompassment ordering.

3.4 General alien-decreasing unions

Alien-decreasing unions need not be hierarchical or stratified:

Example 4. As before, we take {R_{1} = f(c(x), h(h(x))) → f(x, h(x))}. Since R_{1} is alien decreasing for any rewrite system that has h or c as defined symbol, the union R_{0} ∪ R_{1} where {R_{0} = h(f(c(x), c(x))) → x} is an alien-decreasing union which is neither combined nor stratified nor hierarchical.

We can indeed characterize the alien-decreasing property on the rules themselves. First of all, since the rule l → r ∈ R_{0} is itself a particular rewrite, it must satisfy the alien-decreasing condition. Now, since we need stability of the condition under instanciation, we must add to the multiset of aliens, the multiset of variables of l which are not in alien(l). Let M(t) be the multiset alien(t) ∪ (cap(t) ∩ X). Then R_{0} is alien-decreasing iff for every rule l → r ∈ R_{0}, M(l) >_{mul} M(r) or M(l) =_{mul} M(r) and cap(l)(→_{R_{0}∪R_{1}}^{+} ∪ >)cap(r).

4 Termination of alien-decreasing unions

Termination is not a modular property even in the case of disjoint unions. However, it becomes modular under various hypotheses. The first result was obtained by Rusinowitch: termination is a modular property of non-duplicating disjoint unions [23]. Kurihara and Ohuchi then showed that termination of shared-rewriting is a modular property of combined unions [13], and Plump gave a proof of the modularity of termination of shared rewriting for crosswise disjoint unions [18, 19].

We give here an abstract version of these properties: termination is modular for alien-decreasing general unions. Note that systems in such unions may share constructors as well as defined operators. We derive all previous modularity results as restricted cases. Besides, our proof abstracts from useless details in [13, 19, 23] by being based on a stronger induction argument traditional in proof theory (see, e.g. [6]).

Theorem 5. Let R_{0}, R_{1} be terminating term rewriting systems over T (D_{0} ∪ C_{0}, X) and T (D_{1} ∪ C_{1}, X) respectively, where D_{0} ∩ D_{1} = ∅. If →_{R_{0}}, →_{R_{1}} are alien-decreasing then →_{R_{0}∪R_{1}} is terminating.

Proof. In order to show that any term is strongly normalizable in R_{0} ∪ R_{1}, we shall prove a stronger property: For any term t and strongly normalizable substitution γ, tγ is strongly normalizable. The theorem follows directly, by taking the identity substitution for γ.

We proceed now by noetherian induction. We interpret a term tγ by the pair I(tγ) = ⟨t, {γ}⟩, where {γ} denotes the multiset {xγ | x ∈ V ar(t)}. These pairs are compared in the ordering (^{•} >, (→_{R_{0}∪R_{1}})_{mul})_{lex}, denoted ≫ in the following. Recall that ^{•} > stands for the encompassment ordering. Besides, since →_{R_{0}∪R_{1}} is well-founded on γ by assumption, ≫ is well-founded.

We distinguish three cases in the proof, depending on the properties of tγ.

1. tγ reduces at a position p inside γ. There are two cases:

If t is not linear, let t′ be a linearized version of t, and γ′ be such that tγ = t′γ′. Clearly, γ′ is strongly normalizable since γ is, and t ^{•}>t′. Hence ⟨t, {γ}⟩ ≫ ⟨t′, {γ′}⟩, and tγ = t′γ′ is strongly normalizable by the induction hypothesis. Note how we used here the fact that the same term may be decomposed in several ways, hence have several interpretations. If t is linear, then tγ reduces to tγ′. Then ⟨t, {γ}⟩ ≫ ⟨t, {γ′}⟩, hence tγ′ is strongly normalizable by the induction hypothesis.

2. tγ reduces to t′ at a position p ≠ Λ of t. Then t ^{•}>t|_{p}, hence ⟨t, {γ}⟩ ≫ ⟨t|_{p}, {γ}⟩, hence t|_{p}γ = (tγ)|_{p} is strongly normalizable. Let z be a new variable and u = t[z]_{p}. Let γ′ = γ ∪{z ↦ (tγ)|_{p}}. γ′ is strongly normalizable, and t ^{•} >u, hence ⟨t, {γ}⟩ ≫ ⟨u, {γ′}⟩, hence uγ′ = tγ is strongly normalizable.

3. tγ reduces to t′ at p = Λ. There are two subcases:

(a) t = f(t_{1}, …, t_{n}) and t is not a variable renaming of u = f(x_{1}, …, x_{n}). Since ⟨t, {γ}⟩ ≫ ⟨t_{i}, {γ}⟩ for 1 ≤ i ≤ n, γ′ = {x_{1} ↦ t_{1}γ, …, x_{n} ↦ t_{n}γ} is strongly normalizable. Since t ^{•} >u, ⟨t, {γ}⟩ ≫ ⟨u, {γ′}⟩, hence uγ′ = tγ is strongly normalizable.

(b) t = f(x_{1}, …, x_{n}). Since γ is strongly normalizable by assumption, the subterms of the terms x_{i}γ are strongly normalizable as well. Then tγ is strongly normalizable by Lemma 6 below.

In all cases tγ is strongly normalizable or reduces to strongly normalizable terms. Hence tγ is strongly normalizable.

Lemma 6. Let R_{0}, R_{1} be terminating term rewriting systems over T (D_{0}∪C_{0}, X) and T (D_{1} ∪ C_{1}, X) respectively, where D_{0} ∩ D_{1} = ∅. If →_{R_{0}}, →_{R_{1}} are aliendecreasing then any term whose alien subterms are strongly normalizable with respect to →_{R_{0}∪R_{1}} is strongly normalizable with respect to →_{R_{0}∪R_{1}}.

Proof. We interpret a term t by the pair I(t) = ⟨aliens(t), cap(t)⟩ of the multiset of its alien subterms and its cap. Multisets of alien subterms are compared in the multiset extension of →_{R_{0}∪R_{1}} ∪ >, where < denotes the strict subterm relation, and caps are compared in the reduction ordering →_{R_{0}∪R_{1}} ∪ ^{•}>, i.e. we use ((→_{R_{0}∪R_{1}} ∪ >)_{mul}, →_{R_{0}∪R_{1}} ∪ ^{•} >)_{lex} for the ordering on interpretations. This is a well-founded ordering because →_{R_{0}∪R_{1}} is terminating on alien subterms by assumption, cap(t) is a quasi-homogeneous term and R_{0}, R_{1} are terminating, and the union of the encompassment relation (which includes >) with a terminating rewrite relation is well-founded [3].

Now, if t →_{R_{i}} t′ (i ∈ {0, 1}) there are two possibilities:

1. It is a reduction in the cap, then there are two subcases. If aliens(t) >_{mul} aliens(t′), then I(t) > I(t′). This is in particular the case if the cap shrinkes. Otherwise, aliens(t) =_{mul} aliens(t′) since R_{0} and R_{1} are alien-decreasing. We must therefore compare the caps. By assumption, cap(t) →_{R_{i}} cap(t′) or cap(t) ^{•}>cap(t′). In both cases, the cap has decreased in our ordering, hence I(t) > I(t′).

2. It is a reduction inside an alien of t, then aliens(t)(→_{R_{0}∪R_{1}} ∪ >)_{mul}aliens(t′). Then I(t) > I(t′). Note that we need to consider > since the result of reducing an alien subterm of t can be a term whose root belongs to the same signature as cap(t) (in particular, could be a constructor), and so only its strict subterms are alien subterms of t′ in this case.

In both cases the interpretation is strictly decreasing, which proves the claim.

Compare this proof structure with [23], [13] and [18], and note that lemma 6 is an interesting tool on its own: we do not use the notion of “rank” for the induction argument, which makes our proof much less technical.

Assume now that both rewrite systems R_{0} and R_{1} are simply terminating, that is, can be shown terminating by use of a simplification ordering. Let P_{f} be the rewrite system made of the projection rules f(x_{1}, …, x_{n}) → x_{i} for all 1 ≤ i ≤ n. Since a set R of rules is simply terminating iff R ∪ ⋃_{f∈F} P_{f} is terminating, it suffices to note that the obtained set of rules is alien-decreasing when the starting set R is, in order to prove that simple termination is a modular property of alien-decreasing unions.

In the case of combined unions, Kurihara and Ohuchi proved that simple termination is modular [14], without assuming the alien-decreasing property. On the other hand, rewriting becomes compatible with embedding for simply terminating systems, hence we can use embedding in our induction ordering instead of subterm or encompassement. As a consequence, we can relax the alien-decreasing assumption, but cannot get rid of it.

5 Cap-decreasing unions

Rusinowitch [23] also showed that termination of disjoint unions is modular for non-collapsing rewrite rules, and conjectured that modularity is true when one system is non-duplicating and non-collapsing, which was later proved by Middeldorp [16]. Rusinowitch second result can be proved by changing the interpretation in the proof of lemma 6, by putting the cap first, and the multiset of aliens second.

In fact, disjoint unions of non-collapsing systems are a particular case of capdecreasing general unions: a reduction in a term in the union either decreases the cap or does not change the cap but decreases the aliens. Formally:

Definition 7. A relation → on terms in a union R_{0} ∪ R_{1} where D_{0} ∩ D_{1} = ∅ is cap-decreasing if s →_{p} t implies that cap(s) and cap(t) are terms in the same signature, and if p ∈ FPos(cap(s)) then cap(s) → ∪ ^{•} >cap(t), otherwise cap(s) = cap(t).

Besides the class of non-collapsing disjoint unions, the class of non-collapsing combined unions is cap-decreasing when there are no constructor-lifting rules (i.e. when no right-hand side is rooted by a shared constructor). There are more general cap-decreasing unions: if R_{0}, R_{1} are neither collapsing nor constructorlifting and their left-hand sides are homogeneous, then R_{0} ∪R_{1} is cap-decreasing even if defined symbols of one system are used as constructors in the other.

Theorem 8. Let R_{0}, R_{1} be terminating term rewriting systems over T (D_{0} ∪ C_{0}, X) and T (D_{1} ∪ C_{1}, X) respectively, where D_{0} ∩ D_{1} = ∅. If →_{R_{0}}, →_{R_{1}} are cap-decreasing then →_{R_{0}∪R_{1}} is terminating.

Proof. The same as Theorem 5 but using Lemma 9 below instead of Lemma 6 at the end of the proof.

Lemma 9. Let R_{0}, R_{1} be terminating term rewriting systems over T (D_{0}∪C_{0}, X) and T (D_{1} ∪ C_{1}, X) respectively, where D_{0} ∩ D_{1} = ∅. If →_{R_{0}}, →_{R_{1}} are capdecreasing then any term whose alien subterms are strongly normalizable with respect to →_{R_{0}∪R_{1}} is strongly normalizable with respect to →_{R_{0}∪R_{1}}.

Proof. By noetherian induction, interpreting a term t by the pair I(t) = ⟨cap(t), aliens(t)⟩, and using the ordering (→_{R_{0}∪R_{1}} ∪ ^{•} >, (→_{R_{0}∪R_{1}})_{mul})_{lex}, which is well founded since R_{0} and R_{1} are terminating and caps are quasi-homogeneous, and →_{R_{0}∪R_{1}} is terminating on alien subterms by assumption.

As already mentioned, non-collapsing disjoint unions are cap-decreasing:

Corollary 10. [23] Termination is a modular property of non-collapsing disjoint unions.

The technique used in the proofs of the last theorems can be easily adapted to the case of combined unions where one system is both alien-decreasing and cap-decreasing:

Theorem 11. Let R_{0}, R_{1} be terminating term rewriting systems over T (D_{0} ∪ C_{0}, X) and T (D_{1} ∪ C_{1}, X) respectively, where D_{0} ∩ D_{1} = ∅. If either →_{R_{0}} or →_{R_{1}} is both cap-decreasing and alien-decreasing, then →_{R_{0}∪R_{1}} is terminating.

Proof. W.l.g. we are going to assume that →_{R_{0}} is cap-decreasing and aliendecreasing. To prove termination of R_{0} ⊎ R_{1} we use a sort of combined interpretation which will choose the appropriate order between cap and aliens:

I(t) = ⟨rank(t), aliens_{0}(t), cap(t), aliens(t)⟩

where rank(t) = 1 if t is homogeneous and rank(t) = 1+max_{s∈aliens(t)}(rank(s)) otherwise, and aliens_{0}(t) is the multiset of aliens of t if cap(t) ∈ T (F_{0}, X) and the empty multiset otherwise. The proof of the lemma is done by noetherian induction on the well-founded ordering

(>_{N}, (→_{R_{0}∪R_{1}} ∪ >)_{mul}, →_{R_{0}∪R_{1}} ∪ ^{•} >, (→_{R_{0}∪R_{1}})_{mul})_{lex}.

We get Middeldorp’s result for disjoint unions [16] as a corollary.

6 Hierarchical unions

The alien-decreasing property is not a real restriction in the case of combined unions since shared rewriting is alien-decreasing. In contrast, it is a severe restriction in the case of hierarchical unions since it applies to all systems in the hierarchy. Indeed, there are very few hierarchical systems which are aliendecreasing. For example, the system below, defining addition and multiplication is not. In this section we will prove a modularity result for a sequence of rewrite systems the base of which is alien-decreasing. Practice favours this kind of hierarchical combination, since it corresponds to the so-called incremental development methodology of algebraic specifications.

Let R_{0}, R_{1}, …, R_{n} be term rewriting systems over T (D_{0}∪C, X), T (D_{1}∪(D_{0}∪ C), X), …, T (D_{n} ∪ (D_{n−1} ∪ … ∪ D_{0} ∪ C), X) respectively. The corresponding hierarchical union R_{0} +…+R_{n} has R_{0} for basis, and R_{1}, …, R_{n} for incremental developments.

Example 5. A very simple (and well-known) hierarchical system is the following, where the basis defines the addition of natural numbers, and in the second level the product of natural numbers is defined using the addition.

C = {S, 0}, D_{0} = {+}, D_{1} = {×}, D_{2} = {!}.

R_{0} = \{ \begin{matrix}0 + x & → & x \\ S(x) + y & → & S(x + y) \end{matrix} R_{1} = \{ \begin{matrix}0 × x & → & 0 \\ S(x) × y & → & x × y + y \end{matrix}

R_{2} = \{ \begin{matrix}0! & → & 1 \\ S(x)! & → & S(x) × x! \end{matrix}

The termination of R_{0} + R_{1} + R_{2} is modular as a consequence of theorem 14 below, since it is an example of the multiset schema defined next.

6.1 Statuses and orderings

Function symbols in an incremental development will be assigned a status, that will be used to build up an ordering. We allow for a complex notion of status (e.g. the usual multiset status, or the left-to-right lexicographic status, or a term like lex(x_{2}, x_{4}, mul(x_{3}, x_{1}))), allowing us to tune up the comparison of lists according to practical needs. For example, comparing the lists of terms l_{1}, l_{2}, l_{3}, l_{4} and r_{1}, r_{2}, r_{3}, r_{4} according to the above status and the ordering > generates the comparison of l_{2} and r_{2} first, then of l_{4} and r_{4} if l_{2} and r_{2} are equivalent under variable renaming, and if this is also true of l_{4} and r_{4}, then the two multisets {l_{3}, l_{1}} and {r_{3}, r_{1}} are compared.

Definition 12. Let mul and lex be varyadic symbols. A status of arity n is a term stat ∈ T ({mul, lex}, X) such that Var(stat) = {x_{1}, …, x_{n}} and in normal form with respect to the rewrite system R_{stat}:

lex(x_{1}, …, x_{m}, lex(y_{1}, …, y_{n}), z_{1}, …, z_{p}) → lex(x_{1}, …, x_{m}, y_{1}, …, y_{n}, z_{1}, …, z_{p})
mul(x_{1}, …, x_{m}, mul(y_{1}, …, y_{n}), z_{1}, …, z_{p}) → mul(x_{1}, …, x_{m}, y_{1}, …, y_{n}, z_{1}, …, z_{p})
lex(x_{1}, …, x_{m}, mul, z_{1}, …, z_{p}) → lex(x_{1}, …, x_{m}, z_{1}, …, z_{p})
mul(x_{1}, …, x_{m}, lex, z_{1}, …, z_{p}) → mul(x_{1}, …, x_{m}, z_{1}, …, z_{p})
lex(x) → x  mul(x) → x

To each function symbol f of arity n, we associate a status (i.e. a tree) stat_{f} of the same arity. The status is called multiset (respectively lexicographic) if equal to mul(x_{1}, …, x_{n}) (respectively lex(x_{ξ(1)}, …, x_{ξ(n)}), where ξ is a permutation of [1..n]). The status of a constant symbol is therefore equal to lex or mul, while the status of a unary symbol is the variable x_{1}. Given a term t whose variables occur at positions p_{1}, …, p_{m} such that p_{i} <_{lex}^{N} p_{i+1}, its status stat_{t} is the normal form according to R_{stat}, of stat(t, Λ, {p_{1}, …, p_{m}}), where stat is defined by:

\begin{aligned}stat(f(t_{1}, …, t_{n}), p, l) & = & stat_{f}\{x_{1} ↦ stat(t_{1}, p.1, l), …, x_{n} ↦ stat(t_{n}, p.n, l)\} \\ stat(x, p, l) & = & x_{i} if p = p_{i} ∈ l \end{aligned}

Example 6. Let f, g and a have the respective statuses lex(x_{1}, x_{2}, x_{3}), mul(x_{1}, x_{2}) and lex. Then, f(x, y, g(x, y)) has the status lex(x_{1}, x_{2}, mul(x_{3}, x_{4})), while f(x, g(a, y), g(a, a)) has the status lex(x_{1}, x_{2}).

Statuses allow us to extend well-founded orderings on sets to well-founded orderings on sequences. Given a set S equipped with a well-founded ordering >, a status stat depending on n variables x_{1}, …, x_{n} and two lists of elements of S of length n, we define the ordering >_{stat} as follows:

{l_{1}, …, l_{n}} >_{stat} {r_{1}, …, r_{n}} iff
stat{x_{1} ↦ l_{1}, …, x_{n} ↦ l_{n}} >_{rpo} stat{x_{1} ↦ r_{1}, …, x_{n} ↦ r_{n}}

As a particular case of recursive path ordering, this ordering on sequences is of course well-founded if the starting ordering on S is, and is closed under instantiation [1]. Note that this ordering boils down to the usual lexicographic or multiset ordering in case the status is a term of height one.

6.2 General Recursive Schema

In this section we consider hierarchical unions in which

– R_{0} is terminating, and alien-decreasing or cap-decreasing, and

– each incremental development satisfies the general recursive schema defined below:

Definition 13. Let R be a rewrite system on T (F, X), and assume that f is a new function symbol, i.e. f ∉ F, equipped with a status stat_{f}. Then we can define f with a finite set of rewrite rules satisfying the following General (recursive) Schema:

f(l_{1}, …, l_{n}) → v

where l_{1}, …, l_{n} ∈ T (F, X), v ∈ T (F ∪ {f}, X), and for all subterms of the form f(r_{1}, …, r_{n}) in v, {l_{1}, …, l_{n}} >_{stat_{f}} {r_{1}, …, r_{n}}.

We will term the general schema the multiset schema (resp. lexicographic schema) when all statuses are multiset (resp. lexicographic). The multiset schema was first presented in [9] under the name of general schema. Note that the multiset schema is primitive recursive because terms in l⃗ may not contain any f by definition, hence the same is true of terms in r⃗ due to the multiset comparison. This is no more true in case of a lexicographic comparaison, hence embedded recursive calls become possible with the lexicographic schema, henceforth for the general schema. One could think that the hypothesis f(l_{1}, …, l_{n}) → r_{i} which is necessary for the definition of the recursive path ordering [11] is also necessary here. But this is not the case, since we require that {l_{1}, …, l_{n}} >_{stat_{f}} {r_{1}, …, r_{n}} for all subterms of the form f(r_{1}, …, r_{n}) in v. So, if a term v_{i} is not reached in the comparison, either it has no subterm headed by f, or it has some which will be compared.

There are only two restrictions in the general schema: mutually recursive definitions are forbidden, since we define a new function f each time; terms in r⃗_{i} must be smaller in a precise sense (using the subterm relationship) than terms in l⃗. The first restriction can be removed by packing mutually recursive definitions in a same tuple of definitions satisfying the general schema. The second appears to be essential to our proof, although we believe it can be relaxed.

Example 7. The following is a rewrite program to sort a list of natural numbers by inserting elements one by one into position. cons and nil are the list constructors, and s and 0 are the constructors for natural numbers. We use x and y for arbitrary natural numbers, and l for an arbitrary list of natural numbers.

\begin{aligned}max(0, x) & → & x & min(0, x) & → & 0 \\ max(x, 0) & → & x & min(x, 0) & → & 0 \\ max(s(x), s(y)) & → & s(max(x, y)) & min(s(x), s(y)) & → & s(min(x, y)) \end{aligned}

\begin{matrix}insert(x, nil) → & cons(x, nil) \\ insert(x, cons(y, l)) → & cons(max(x, y), insert(min(x, y), l)) \\ sort(nil) → & nil \\ sort(cons(x, l)) → & insert(x, sort(l)) \end{matrix}

Here, insert must have a lexicographic status, from right to left, while min, max and sort may have a multiset status (or a lexicographic one).

Note that most examples of hierarchical systems found in the literature (e.g. [15]), and the above one, are indeed constructor systems, but our result does not require this restriction. We now turn to the main result of this section:

Theorem 14. Let R = R_{0} + R_{1} + … + R_{m} be a hierarchical union such that R_{0} is terminating and alien-decreasing (resp. cap decreasing), and R_{1}, …, R_{m} are incremental developments satisfying the general recursive scheme. Then →_{R} is terminating.

Proof. We have to prove that for all t in the union, t is strongly normalizable with respect to R. As previously, we shall prove the stronger property: For all strongly normalizable substitution γ, tγ is strongly normalizable.

The proof is by noetherian induction. We interpret the term tγ by the triple < i, t, {γ} >, where i is the maximal index of the function symbols belonging to t and {γ} is the list of terms obtained from tγ by searching t depth first: {tγ|_{p_{1}}, …, tγ|_{p_{n}} : t|_{p} ∈ X iff ∃i ∈ [1..n]p = p_{i} and p_{1} <_{lex}^{N} … <_{lex}^{N} p_{n}}

Note that a term may have several interpretations, depending on how it is viewed as an instance of some term t by a strongly normalizable substitution γ. This pecularity will be heavily used in the proof.

The triples are compared in the ordering (>_{N},^{•}>, (→_{R} ∪ >)_{stat})_{lex}, denoted by ≫ in the following and by ≫_{n} when we want to indicate that the nth element of the triple has decreased but not the (n−1) first ones. Here, stat stands for the status stat_{t} of the second element t in the triple < i, t, {γ} >. Note that since triples are compared lexicographically, this status is the same in both triples when the comparison reaches {γ} (as in case (3.c) below), since both second elements of the triples must then be equal modulo variable renaming. Besides, since γ is strongly normalizable by assumption, and because the union of the strict subterm relationship with a rewrite relation is well-founded [3], the relation (→_{R} ∪ >)_{stat} is well-founded on γ. Hence, ≫ is a well-founded ordering on the triples.

For simplicity, we will abuse the notations by comparing terms, instead of their interpretations.

There are three cases in the proof, depending on the properties of w = tγ.

1. tγ reduces at a position p inside γ. There are two cases: If t is not linear, let t′ be a linearized version of t and γ′ be such that tγ = t′γ′. Clearly γ′ is strongly normalizing since γ is, and t ^{•}>t′. Hence tγ ≫_{2} t′γ′, and tγ = t′γ′ is strongly normalizable by the induction hypothesis. If t is linear, then tγ reduces to tγ′. Then tγ ≫_{3} tγ′, hence tγ′ is strongly normalizable by the induction hypothesis.

2. tγ reduces to t′ at a position p of t with p ≠ Λ.

Then t ^{•}>t|_{p}, hence tγ ≫ t|_{p}γ = (tγ)|_{p}, and (tγ)|_{p} is strongly normalizable. Let z be a new variable and u = t[z]_{p}. Let γ′ = γ ∪ {z ↦ (tγ)|_{p}}. γ′ is strongly normalizable, and t ^{•}>u, then tγ ≫ uγ′ = w, hence w is strongly normalizable.

3. tγ reduces to t′ at p = Λ. Now, there are three subcases:

(a) t = f(t_{1}, …, t_{n}) and t is not a variable renaming of u = f(x_{1}, …, x_{n}). Then tγ ≫ t_{i}γ for 1 ≤ i ≤ n, hence γ′ = {x_{1} ↦ t_{1}γ, …, x_{n} ↦ t_{n}γ} is strongly normalizable. Since t ^{•}>u, uγ′ is strongly normalizable, and uγ′ = tγ.

(b) t = f(x_{1}, …, x_{n}) and f ∈ F_{0}. Since γ is strongly normalizable by assumption, the subterms of the terms x_{i}γ are strongly normalizable as well. Then tγ is strongly normalizable by Lemma 15 below.

(c) t = f(x_{1}, …, x_{n}) and f ∉ F_{0}. Then f(x_{1}, …, x_{n})γ = f(l_{1}, …, l_{n})γ′ → vγ′ where f(l_{1}, …, l_{n}) → v is a rule defining f. As subterms of {γ}, l_{1}γ′, …, l_{n}γ′ as well as terms in {γ′} are strongly normalizable by assumption. We now prove the following property (P): for any term w and substitution θ satisfying:

(i) θ is strongly normalizable, and (ii){l_{1}γ′, …, l_{n}γ′} >_{stat_{f}} {u_{1}θ, …, u_{n}θ}, for all subterms f(u_{1}, …, u_{n}) of w, wθ is strongly normalizable. The proof is by induction on the number of recursive calls to f in w.

– Assume that f has no occurrence in w. Then the interpretation of wθ is strictly smaller than the interpretation of f(x_{1}, …, x_{n})γ, and since θ is strongly normalizable, we can conclude by the outer induction hypothesis.

– Otherwise, we eliminate an innermost recursive call by moving its instance by θ to the substitution part. Let f(u_{1}, …, u_{n}) be a recursive call at position p in w such that f does not occur in any u_{i}. Hence f(x_{1}, …, x_{n})γ ≫_{1} u_{i}θ, and u_{i}θ is strongly normalizable by the outer induction hypothesis. Hence, the substitution θ′ = {x_{1} ↦ u_{1}θ, …, x_{n} ↦ u_{n}θ} is strongly normalizable. Now, {x_{1}γ, …, x_{n}γ} = {l_{1}γ′, …, l_{n}γ′} >_{stat_{f}} {u_{1}θ, …, u_{n}θ} = {x_{1}θ′, …, x_{n}θ′} by assumption on w. Therefore f(x_{1}, …, x_{n})γ ≫_{3} f(x_{1}, …, x_{n})θ′, hence f(x_{1}, …, x_{n})θ′ = f(u_{1}θ, …, u_{n}θ) is strongly normalizable by the outer induction hypothesis. We can now move the instantiated recursive call f(u_{1}θ, …, u_{n}θ) to θ (abusing names) by adding a new variable z to its domain and letting zθ = (w|_{p})θ = f(u_{1}, …, u_{n})θ, yielding a strongly normalizable substitution θ such that wθ = w[z]_{p}θ. We now prove property (ii) for w[z]_{p}. But this follows from the fact that any recursive call to f at position q in w[z]_{p} is a recursive call to f at position q in w, hence their instances by θ are identical terms. Since the recursive call in w satisfies (ii), so does the recursive call in w[z]_{p}.

Since w[z]_{p} has one recursive call to f less than w, we can apply the inner induction hypothesis and conclude that w[z]_{p}θ = wθ is strongly normalizable, and we are done with the proof of (P). Note now that the pair (v, γ′) satisfies (i) as already noticed and (ii) by definition of the general schema, and because >_{stat_{f}} is closed under instantiation. Taking v for w and γ′ for θ finishes the proof of this case.

In each case tγ is strongly normalizable or reduces to strongly normalizable terms. Then tγ is strongly normalizable.

This proof is indeed a specialization of [9] to the case of first-order rules, but allows for a more sophisticated notion of status to the price of some complications in case 3c of the proof. But these complications arise as soon as we allow for a lexicographic status, which is crucial for practical needs.

Lemma 15. Let R = R_{0} + R_{1} + … + R_{n} be a hierarchical system such that R_{0} is terminating and alien-decreasing (resp. cap-decreasing). If f ∈ F_{0} then any instance of f(x_{1}, …, x_{n}) is strongly normalizable (with respect to R) whenever its alien subterms are strongly normalizable (with respect to R).

Proof. Straightforward adaptation of the proof of lemma 6.

7 Extensions

Our results generalize easily to other forms of rewriting: conditional rewrite systems that are reductive, and rewriting modulo a set of regular equations. Reductive rewrite systems [10] generalize the notion of simplifying rewrite systems of Kaplan [12].

7.1 Conditional rewriting

Definition 16. A conditional rewrite system R is a set {ρ_{i}}_{i} of conditional rules of the form:

ρ = l → r if u_{1} ↓ v_{1} ∧ … ∧ u_{n} ↓ v_{n}

where ↓ is interpreted as joinability with respect to R.

To the rule ρ, we associate the term rewriting system ρ̂ = {l → r, l → u_{1}, l → v_{1}, …, l → u_{n}, l → v_{n}}, and to the set R = {ρ_{i}}_{i} of rules we associate the set R̂ = ⋃_{i} ρ̂_{i} of rules.

We say that R is reductive (resp. alien-decreasing, cap-decreasing) if R̂ is terminating (resp. alien-decreasing, cap-decreasing). Reductive systems are of course terminating [10].

We say that R satisfies the general schema iff the associated rewrite system R̂ satisfies the schema.

Theorem 17. Termination is a modular property of alien-decreasing (resp. cap decreasing) unions of reductive rewrite systems. Termination is a modular property of hierarchical reductive systems having an alien-decreasing (resp. cap-decreasing) base.

Proof. We simply apply theorems 5 (resp. 8), or 14, to R̂ which shows that R is reductive.

Hierarchical unions of conditional rewrite systems have also been investigated by Middeldorp and Gramlich, with a different notion of reductive conditionnal rewriting system for which modularity results are problematic.

7.2 Rewriting modulo

Associative-commutative rewriting is very important in practice. We can also generalize easily our results for this case, actually for rewriting modulo a congruence whose equivalence classes are finite. This implies in particular that this congruence is generated by regular equations, that is equations l = r such that Var(l) = Var(r).

It is important here that the subterm and encompassment orderings are still compatible (with respect to well-foundedness) with the rewriting relation on congruence classes of terms, which in turns requires that the congruence classes are finite [8]. It is also important that equivalent terms are built up from the same set of function symbols in order for our interpretation to be compatible with the congruence, which follows from the regularity condition. The finiteness condition on congruence classes is therefore all we need.

Theorem 18. Termination is a modular property of alien-decreasing (resp. cap decreasing) unions of reductive rewrite systems modulo a congruence whose equivalence classes are finite. Termination is a modular property of hierarchical reductive systems modulo a congruence whose equivalence classes are finite, provided the base is aliendecreasing (resp. cap-decreasing).

8 Conclusion

We have identified a property of rewrite relations, the alien-decreasing property, that turns out to be a key for the modularity of termination of disjoint, combined and even hierarchical unions. We have shown a simple proof of the modularity of termination of general unions R_{1} ∪R_{2} (D_{1} ∩D_{2} = ∅) of alien-decreasing systems, and we also showed that many known sufficient conditions for the modularity of termination [23, 13, 18, 19] are in fact consequences of this result.

The modularity result of [23] for disjoint unions without collapsing rules is instead obtained as a consequence of another general result: modularity of general unions of cap-decreasing systems.

The proof technique applied to obtain the modularity of systems satisfying the abstract property of cap-decreasingness or alien-decreasigness is interesting on its own, and it yields simple proofs of other modularity results, such as [16].

For hierarchical systems with an alien-decreasing base, we have given sufficient conditions for the modularity of termination related with the form of the recursive rules in the enrichments: when these rules satisfy the general recursive scheme then the whole system terminates. Although hierarchical systems arise naturally in practice, for instance in the development of functional programs or algebraic specifications, modular aspects of hierarchical systems have deserved little attention until now. Previous results on modularity of hierarchical systems were given by Krishna Rao in [20], where sufficient conditions for modularity of convergence of a restricted class of hierchical systems are shown, and in [21], where he characterizes a class of hierarchical systems for which syntactical sufficient conditions for modularity of simple termination can be given. Another class of hierarchical systems for which termination is modular is described in [2]. The results presented in [20, 21, 2] and here are not easily comparable because there are systems whose termination can be established by one result and not by the others. In particular, we accomodate mutually recursive definitions easily, which causes difficulties to finding simplification orderings, as in [21]. We can also generalize our results to the case of conditional rewriting modulo a congruence whose equivalence classes are finite. This was done without effort, thanks to our powerful proof technique.

Acknowledgments: To Bernhard Gramlich and Ralph Matthes for their careful reading.

References

1. Nachum Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279–301, March 1982.

2. Nachum Dershowitz. Hierarchical termination. Draft, 1994.

3. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243– 309. North-Holland, 1990.

4. K. Drosten. Termerssetzungssysteme. PhD thesis, University of Passau, Germany, 1989. In german.

5. M. Fernandez and J.-P. Jouannaud. Modularity properties of term rewriting systems revisited. Technical Report 875, Laboratoire de Recherche en Informatique, November 1993.

6. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

7. B. Gramlich. A structural analysis of modular termination of term rewriting systems. Research Report SR-91-15, University Kaiserslautern, 1991.

8. Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4), November 1986.

9. Jean-Pierre Jouannaud and Mitsuhiro Okada. Executable higher-order algebraic specification languages. In Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam, pages 350–361, 1991.

10. Jean-Pierre Jouannaud and B. Waldmann. Reductive conditional term rewriting systems. In Proc. Third IFIP Working Conference on Formal Description of Programming Concepts, Ebberup, Denmark, 1986.

11. S. Kamin and Jean-Jacques Lévy. Two generalizations of the recursive path ordering. Available as a report of the department of computer science, University of Illinois at Urbana-Champaign, 1980.

12. Stephane Kaplan. Conditional rewrite rules. Theoretical Computer Science, 33:175–193, March 1984.

13. Mahahito Kurihara and Azuma Ohuchi. Non-copying term rewriting and modularity of termination. Hokkaido University.

14. Mahahito Kurihara and Azuma Ohuchi. Modularity of simple termination of term rewriting systems with shared constructors. Theoretical Computer Science, 103:273–282, 1992.

15. A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. In Proc. 4th Rewriting Techniques and Applications, LNCS 488, Como, Italy, 1991.

16. Aart Middeldorp. A sufficient condition for the termination of the direct sum of term rewriting systems. In Proc. of the 4th IEEE Symposium on Logic in Computer Science, Pacific Grove, pages 396–401, 1989.

17. Aart Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Free University of Amsterdam, Netherland, 1990.

18. Detlef Plump. Implementing term rewriting by graph reduction: Termination of combined systems. In Proc. Conditional and Typed Rewriting Systems, LNCS 516, 1991.

19. Detlef Plump. Collapsed tree rewriting: Completeness, confluence and modularity. In Proc. Conditional Term Rewriting Systems, LNCS 656, 1993.

20. M.R.K. Krishna Rao. Modular proofs for completeness of hierarchical systems. to appear, 1993.

21. M.R.K. Krishna Rao. Modular proofs for simple termination of hierarchical systems. to appear, 1993.

22. Albert Rubio. Automated deduction with constrained clauses. PhD Thesis, Univ. de Catalunya, 1994.

23. Michaël Rusinowitch. On termination of the direct sum of term rewriting systems. Information Processing Letters, 26:65–70, 1987.

24. Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, April 1987.

25. Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128–143, April 1987.

This article was processed using the LaTEX macro package with LLNCS style