The Union of Rewrite Systems

Karl Stroetmann ^{∗}

January 26, 1995

Abstract

The purpose of this paper is to investigate two questions, which arise naturally when rewrite systems are combined. The first question adresses the termination of the union of two terminating rewrite systems. We give a non–trivial, sufficient and decidable criterion ensuring the termination of the union of two rewrite systems.

The second question asks whether normal forms computed with a first rewrite system remain in normal form when reduced by reductions from a second rewrite system. It turns out that this question is efficiently decidable.

1 Introduction

In industrial applications one often has to combine different rewrite systems to solve complex tasks. We had to do this when we used rewriting as a method for theorem proving of open first order formulas which, in our application, were generated in Hoare–style by a tool called MUNITY. We have developed this tool for the verification of UNITY [3] programs. We have seen that it is very helpful to have a criterion which ensures that normal forms computed with one rewrite system are preserved by reductions with another rewrite system. For, if the structure of a normal form of a certain rewrite system is well understood, then it may be possible to obtain this normal form by other more efficient techniques than by rewriting. One only has to be sure that this normal form is preserved under reductions of a second rewrite system, which is to be combined with the first system. In the last section we will give an example how this can be achieved.

It turns out that the above problem is strongly connected with the question under what circumstances the union of two terminating rewrite systems is also terminating. Bachmair and Dershowitz [2] have shown that the union of two terminating rewrite systems is terminating if one rewrite system quasi–commutes over the other rewrite system. They also give a sufficient criterion for quasi–commutation. We are able to strengthen their result by showing that quasi–commutation is decidable.

In the more recent literature, Toyama has investigated the union of rewrite systems. There he is concerned with Church–Rosser properties [9, 10], or considers the union of rewrite systems with disjoint sets of function symbols [11]; However, the questions we will adress in this paper remain open there.

The outline of this paper is as follows. In Section 2 we investigate abstract properties of binary relations. After investigating the properties of quasi–commuting relations we develop a criterion guaranteeing the conservation of normal forms with respect to one binary relation under another binary relation. These considerations are then applied in Section 3 to rewrite systems, where we are able to show that quasi–commutation of one rewrite system over another rewrite system is decidable under the provision of some linearity requirements. In a final section we illustrate our ideas with algebraic examples.

∗Address correspondence to Karl Stroetmann, Siemens AG, ZFE BT SE 11, Otto–Hahn–Ring 6, D-8000 München 83, Germany.

It turns out that in the cases of real interest one does not deal with ordinary rewriting but rather with ordered rewriting [6]. Therefore we sketch in Section 4 how to lift our results to ordered rewrite systems. One could of course ask the question, why we have not developed the whole theory from the beginning for ordered rewrite sytems since ordinary rewrite systems are just a special case of ordered rewrite systems. The reasons for our approach are twofold. First the presentation would have been technically more involved and thereby obscured the underlying ideas. Secondly rewrite systems are much better known than ordered rewrite system. So by proving our theorems for this case we hope to adress a broader audience.

2 Quasi–Commuting Relations

In this section we take an abstract look at binary relations. We start with some definitions. A binary relation R on a set X is terminating iff there is no infinite sequence (x_{n})_{n∈N}, x_{n} ∈ X such that we have

x_{n} R x_{n+1} for all n ∈ N.

We say that x ∈ X is R–irreducible or in R–normal form iff there is no y ∈ X such that x R y holds.

Definition 1 (Conservation of Normal Forms) If R_{1} and R_{2} are two relations on a set X, we say that R_{1}–normal forms are conserved under R_{2}, iff the following holds for all x, y ∈ X:

x is in R_{1}–normal form & x R_{2} y ⇒ y is in R_{1}–normal form.

The relation R_{1} is said to commute over the relation R_{2}, iff R_{2} ∘ R_{1} ⊆ R_{1} ∘ R_{2} holds. Here, ∘ denotes relational composition, i. e. R_{1} ∘ R_{2} = {(x, z) : ∃y ∈ X(x R_{1} y ∧ y R_{2} z)}. The transitive reflexive closure of a relation R is written as R^{∗}, the transitive closure of R is written as R^{+} and the reflexive closure of R is written as R^{=}. If n ∈ N we write R^{n} for the n–th power of R:

R^{n} = \underbrace{R ∘ R ∘ … ∘ R}_{n times} .

R^{≥n} is short for R^{n} ∪ R^{n+1} ∪ R^{n+2} ∪ . . ..

Now suppose we have two binary relations R_{1} and R_{2} on X, which are both known to be terminating. The purpose of this section is to develop a sufficient criterion guaranteeing that the relation R := R_{1} ∪ R_{2} is also terminating. Of course there is one well–known criterion saying R is terminating if R_{1} commutes over R_{2} (Compare for example Dershowitz and Jouannaud [5]). But this requirement is much to restrictive for our later applications. We therefore need a much weaker requirement ensuring termination of R. Bachmair and Dershowitz [2] suggested the notion of “quasi–commutativity” as such a weaker requirement. Due to the fact that they only sketch the proof that quasi–commutativity is a sufficient criterion to ensure the termination of R we think it is worthwhile to elaborate their proof.

Definition 2 (Quasi–Commuting Relations) Assume that R_{1} and R_{2} are two binary relations on the set X. Then R_{1} quasi–commutes over R_{2}, iff R_{2} ∘ R_{1} ⊆ R_{1} ∘ (R_{1} ∪ R_{2})^{∗}. This means that for all x_{1}, y_{1}, y_{2} ∈ X such that

x_{1} R_{2} y_{1} and y_{1} R_{1} y_{2}

holds, there exists an x_{2} ∈ X satisfying

x_{1} R_{1} x_{2} and x_{2} (R_{1} ∪ R_{2})^{∗} y_{2}.

For the rest of this section we assume that R_{1} and R_{2} are two relations on the set X. The relation R is defined as their union: R := R_{1} ∪ R_{2}. Therefore, if we have x R^{∗} y, then either x R_{2}^{∗} y or there are finite sequences x_{1}, ⋯, x_{n} and y_{1}, ⋯, y_{n} such that

x R_{2}^{∗} x_{1} R_{1} y_{1} R_{2}^{∗} x_{2} R_{1} ⋯ R_{2}^{∗} x_{n} R_{1} y_{n} R_{2}^{∗} y

holds. Then we call the sequence x, x_{1}, y_{1}, x_{1}, ⋯, x_{n}, y_{n}, y a reduction sequence establishing x R y and say that it contains n R_{1}–reductions.

If R_{1} quasi–commutes over R_{2} and is moreover terminating, then any reduction sequence establishing x R^{∗} z can be transformed into a “standardized” reduction sequence of the form

x R_{1}^{∗} y R_{2}^{∗}z.  (∗)

This observation is the key ingredient for the proof that quasi–commutation of R_{1} over R_{2} is a sufficient criterion to guarantee termination of R under the provision that R_{1} and R_{2} are separately terminating. In order to prove (∗) we first need the following lemma.

Lemma 3 Let R_{1} and R_{2} be two binary relations on the set X such that R_{1} quasi–commutes over R_{2} and let R := R_{1} ∪ R_{2}. If there are x_{1}, y_{1}, y_{2} ∈ X and n ∈ N such that

x_{1} R_{2}^{n} y_{1} and y_{1} R_{1} y_{2}

holds, then there is an x_{2} ∈ X satisfying

x_{1} R_{1} x_{2} and x_{2} R^{∗} y_{2}.

Proof: This lemma is proved by a simple induction on n ∈ N. In the case n = 0 we can just define x_{2} := y_{2} and then nothing remains to be proved.

If we have x_{1}R_{2}^{n+1}y_{1}, then by the definition of R_{2}^{n+1} there is an z_{1} ∈ X such that

x_{1} R_{2}^{n} z_{1} R_{2} y_{1}

holds. Because R_{1} quasi–commutes over R_{2}, there exists an z_{2} ∈ X such that

z_{1} R_{1} z_{2} and z_{2} R^{∗} y_{2}.

Now the induction hypothesis can be applied to x_{1}, z_{1} and z_{2} to find an x_{2} ∈ X satisfying

x_{1} R_{1} x_{2} and x_{2} R^{∗} z_{2}.

Because of z_{2} R^{∗} y_{2} we are able to conclude

x_{1} R_{1} x_{2} and x_{2} R^{∗} y_{2}. _{□}

Lemma 4 (Standardization Lemma) Assume R_{1} and R_{2} to be two binary relations on the set X such that R_{1} is terminating and quasi–commutes over R_{2}. Then if there are x_{1} and z_{2} in X such that

x_{1} R^{∗} z_{2}

holds and the reduction sequence establishing this fact contains n R_{1} reductions, then there is an x_{2} ∈ X satisfying

x_{1} R_{1}^{≥n} x_{2} R_{2}^{∗} z_{2}.

Proof: The proof is by transfinite induction on the relation R_{1}. We make a case distinction according to the nature of the first reduction in the reduction sequence establishing x_{1} R^{∗} z_{2}.

Case 1 : x_{1} R_{2}^{∗} z_{2}.

In this case we can define x_{2} := x_{1} and are obviously done.

Case 2 : x_{1} R_{2}^{∗} v R_{1} w R^{∗} z_{2}.

We can apply Lemma 3 to x_{1} R_{2}^{∗} v R_{1} w to find a u ∈ X such that

x_{1} R_{1} u R^{∗} w

holds. Therefore we have u R^{∗} z_{2} and because of x_{1} R_{1} u we can apply the induction hypothesis to u R^{∗} z_{2}. If the reduction sequence establishing u R^{∗}z_{2} contains n R_{1} reductions, we find an x_{2} ∈ X such that

u R_{1}^{≥n} x_{2} R_{2}^{∗} z_{2}

holds. But then we can conclude

x_{1} R_{1}^{≥n+1} x_{2} R_{2}^{∗} z_{2}

and the proof is finished. _{□}

We have to reformulate the last Lemma.

Corollary 5 Let R_{1} and R_{2} be two binary relations on the set X such that R_{1} is terminating and quasi– commutes over R_{2}. Then if

x_{1} R_{2}^{∗} y_{1} R_{1}^{+} y_{2}

holds, then there is an x_{2} ∈ X satisfying

x_{1} R_{1}^{+} x_{2} and x_{2} R_{2}^{∗} y_{2}.

This last Corollary enables us to prove the following theorem.

Theorem 6 If R_{1} and R_{2} are two binary relations on the set X such that

• R_{1} and R_{2} are terminating and

• R_{1} quasi–commutes over R_{2},

then R := R_{1} ∪ R_{2} is terminating.

Proof: We assume that R is not terminating. Because R_{1} and R_{2} separately are terminating, there must be an infinite sequence (x_{n})_{n} such that we have

x_{2∗n} R_{2}^{+} x_{2∗n+1} and x_{2∗n+1} R_{1}^{+} x_{2∗n+2}

for all n ∈ N. With the last Corollary we will be able to construct an infinite sequence (y_{n})_{n} such that the following is true for all n ∈ N:

y_{n} R_{1}^{+} y_{n+1} and y_{n} R_{2}^{∗} x_{2∗n}.

The construction is by induction on n ∈ N.

Induction start : n = 0.

In this case we define y_{0} := x_{0}. We only have to show y_{0} R_{2}^{∗} x_{0}, but this is trivial.

Induction step : n → n + 1.

By induction hypothesis we know y_{n} R_{2}^{∗} x_{2∗n}. Our assumption is that we have

x_{2∗n} R_{2}^{+} x_{2∗n+1} and x_{2∗n+1} R_{1}^{+} x_{2∗n+2}.

From y_{n} R_{2}^{∗} x_{2∗n} and x_{2∗n} R_{2}^{+} x_{2∗n+1} we have y_{n} R_{2}^{+} x_{2∗n+1}, which together with x_{2∗n+1} R_{1}^{+} x_{2∗n+2} implies by the last Corollary that there is an y_{n+1} such that

y_{n} R_{1}^{+} y_{n+1} and y_{n+1} R_{2}^{∗} x_{2∗n+2}.

Now the existence of the sequence (y_{n})_{n} contradicts the fact that R_{1} is terminating. _{□} The next theorem is new.

Theorem 7 (Conservation of Normal Forms) If R_{1} and R_{2} are two binary relations on the set X such that R_{1} quasi–commutes over R_{2}, then R_{1}–normal forms are conserved under R_{2}.

Proof: If x_{1} ∈ X is in R_{1}–normal form and x_{1} R_{2} y_{1}, we have to prove that y_{1} is also in R_{1}–normal form. Suppose this is not the case. Then there is an y_{2} ∈ X such that y_{1} R_{1} y_{2}. By Corollary 5 we find an x_{2} ∈ X such that

x_{1} R_{1}^{+} x_{2} and x_{2} R_{2}^{∗} y_{2}

holds. But then x_{1} cannot have been in R_{1}–normal form. _{□}

Observation: For the last Theorem to hold it is not really required that R_{1} is quasi– commuting over R_{2}. What is required is the following property: If

x_{1} R_{2} y_{1} and y_{1} R_{1} y_{2}

holds, then x_{1} is R_{1}–reducible. Observe that this is just a reformulation of Definition 1.

3 Quasi–Commuting Rewrite Systems

In this section we want to apply our abstract considerations of quasi–commuting relations of the last section to rewrite systems. Our main goal is to find analogies of Theorem 6 and Theorem 7 for rewrite systems. If R_{1} and R_{2} are two rewrite systems, it will turn out that it is decidable

• whether R_{1} quasi–commutes over R_{2} and

• whether R_{1}–normal forms are preserved under R_{2} reductions.

This is a considerable improvement of the work of Bachmair and Dershowitz [2].

3.1 Basic Definitions

Most of our definitions are as in Dershowitz & Jouannaud [5] or in Bachmair [1]. Terms are built from a set F of function symbols and a set V of variables. The set of all terms is denoted by T (F, V). Terms containing no variables are called ground terms. The set of all ground terms is denoted by T (F). If t is a term, then F V (t) denotes the set of all variables appearing in t.

The positions (or occurrences) in a term are defined in the usual inductive way. The set of all positions in a term t is written as O(t). If u is a position in t, then t/u denotes the subterm of t at the position u. If s and t are terms and u ∈ O(t) is a position in t, then t[u ← s] is the term which we get by replacing the subterm at position u in t by s.

A position u ∈ O(t) is below a position v ∈ O(t), if there is a position w ∈ O(t/v) such that u = vw. Two positions u, v ∈ O(t) are called disjoint if neither u is below v nor v is below u.

A non–variable position in a term t is a position u in t, such that t/u is not a variable. The set of all non–variable positions in t is denoted by O^{∘} (t). Therefore O^{∘} (t) is defined as

O^{∘} (t) := {u ∈ O(t) : t/u ∉ V}.

An ordering on a set X is any binary relation on X which is irreflexive and transitive. A simplification ordering is an ordering on T (F, V) which is monotonic (s < t implies f(… s …) < f(… t …)), stable (s < t implies sσ < tσ for all substitutions σ) and has the subterm property (s < f(… s …)). It is well–known [5] that every simplification ordering is well–founded.

A (terminating) rewrite system is a pair (E, <) where E is a set of equations in T (F, V) and < is a simplification ordering such that we have l < r for all equations l = r ∈ E. (With this definition we restrict our attention to terminating rewrite systems.) Usually the equations l = r in E will be written as l → r and will be called rules.

A rewrite system (E, <) induces a binary relation →_{E} on T (F, V), which is defined as s →_{E} t iff there exists a position u ∈ O(t), a rule l → r ∈ E and a substitution σ such that

s/u ≡ lσ and t ≡ s[u ← rσ]

holds. It can easily be seen that the relation →_{E} is stable, therefore we have

s →_{E} t ⇒ sσ →_{E} tσ

for all substitutions σ. Another important property of the relation →_{E} is its compatibility. By this we mean that

s →_{E} t ⇒ r[u ← s] →_{E} r[u ← t]

holds for all terms r and all positions u ∈ O(r).

A rule l → r is called left–linear, iff every variable occurs at most once in l. It is called right–linear, iff every variable occurs at most once in r. (Note that if a rewrite system is terminating, then every variable appearing on the right–hand side of a rule must also appear on the left–hand side.) A rule is linear iff it is both left–linear and right–linear. A rewrite system (E, <) is linear, iff every rule l → r ∈ E is linear. Left–linear and right–linear rewrite systems are defined analogously.

3.2 Standard Reductions

In the following we assume that (R_{1}, <_{1}) and (R_{2}, <_{2}) are two rewrite systems, which give rise to two binary relations →_{R_{1}} and →_{R_{2}} on T (F, V). They give also rise to a third binary relation →_{R} which is defined as

s →_{R} t iff s →_{R_{1}} t or s →_{R_{2}} t.

Definition 8 (Standard Reduction) A term s is standard reducible to a term t, iff there is a term r such that the following holds:

s →_{R_{1}}^{∗} r and r →_{R_{2}}^{∗} t.

If s is standard reducible to t this is written as s →_{s} t.

We are going to investigate under which conditions the relation →_{R} is contained in the relation →_{s}. The typical non–standard reduction of a term s to a term t looks like

s →_{R_{2}} r →_{R_{1}} t.

It turns out that there are only finitely many non–standard reductions which have to be investigated. They will be termed principal non–standard reductions. We will define them next.

Definition 9 (Principal Non–Standard Reductions) Non–standard reductions come in two forms. Assume that

• l_{1} → r_{1} ∈ R_{1} and l_{2} → r_{2} ∈ R_{2} and

• u ∈O^{∘} (r_{2}) and l_{1} and r_{2}/u are unifyable with most general unifier μ.

Then we call the reduction sequence

l_{2}μ →_{R_{2}} r_{2}μ ≡ r_{2}[u ← l_{1}]μ →_{R_{1}} r_{2}[u ← r_{1}]μ

a principal non–standard reduction of the first kind.

To define the principal non–standard reductions of the second kind we assume

• l_{1} → r_{1} ∈ R_{1} and l_{2} → r_{2} ∈ R_{2} and

• u ∈O^{∘} (l_{1}) and l_{1}/u and r_{2} are unifyable with most general unifier μ.

Then we call the reduction sequence

l_{1}[u ← l_{2}]μ →_{R_{2}} l_{1}[u ← r_{2}]μ ≡ l_{1}μ →_{R_{1}} r_{1}μ

a principal non–standard reduction of the second kind.

Now a non–standard reduction is a non–standard reduction of the first or second kind.

Lemma 10 (Principal Non–Standard Reduction Lemma) If (R_{1}, <_{1}) and (R_{2}, <_{2}) are rewrite systems such that R_{1} is left–linear and R_{2} is right– linear, then the relation →_{R_{1}} quasi–commutes over →_{R_{2}} if and only if for every principal non–standard reduction

s_{1} →_{R_{2}} t_{1} →_{R_{1}} t_{2}

there is a term s_{2} such that we have

s_{1} →_{R_{1}} s_{2} →_{R}^{∗} t_{2}.

Proof: One direction is trivial. If →_{R_{1}} quasi–commutes over →_{R_{2}} and

s_{1} →_{R_{2}} t_{1} →_{R_{1}} t_{2}

is a principal non–standard reduction, then by the definition of quasi–commuting relations there has to be a term s_{2} satisfying

s_{1} →_{R_{1}} s_{2} and s_{2} →_{R}^{∗} t_{2}.

For the other direction we suppose that there are terms s_{1}, t_{1} and t_{2} such that we have

(1)  s_{1} →_{R_{2}} t_{1} and t_{1} →_{R_{1}} t_{2}.

We have to show that there is a term s_{2} satisfying

(2)  s_{1} →_{R_{1}} s_{2} and s_{2} →_{R}^{∗} t_{2}.

Because of (1) we find positions u_{1} ∈ O(t_{1}), u_{2} ∈ O(s_{1}), rules l_{1} → r_{1} ∈ R_{1}, l_{2} → r_{2} ∈ R_{2} and substitutions σ_{1}, σ_{2} such that the following holds:

(3)  t_{1}/u_{1} ≡ l_{1}σ_{1} and t_{2} ≡ t_{1}[u_{1} ← r_{1}σ_{1}],
(4)  s_{1}/u_{2} ≡ l_{2}σ_{2} and t_{1} ≡ s_{1}[u_{2} ← r_{2}σ_{2}].

Without loss of generality we may assume that the variables appearing in l_{1} → r_{1} are different from the variables in l_{2} → r_{2}. Then we can define a new substitution σ as

σ(x) := \{ \begin{matrix}σ_{1}(x) & for all x ∈ F V (l_{1} → r_{1}); \\ σ_{2}(x) & else. \end{matrix}

This definition enables us to replace both σ_{1} in (3) and σ_{2} in (4) by σ. From (4) we can conclude

t_{1}/u_{2} ≡ r_{2}σ and s_{1} ≡ t_{1}[u_{2} ← l_{2}σ].

The remaining considerations depend on the relative positions of u_{1} and u_{2}.

Case 1: u_{1} and u_{2} are disjoint.

Then we know that

s_{1}/u_{1} ≡ t_{1}[u_{2} ← l_{2}σ]/u_{1} ≡ t_{1}/u_{1} ≡ l_{1}σ

holds. Therefore we can define

s_{2} := s_{1}[u_{1} ← r_{1}σ].

From this definition we get immediately s_{1} →_{R_{1}} s_{2} and because of s_{2}/u_{2} ≡ l_{2}σ and

t_{2} ≡ t_{1}[u_{1} ← r_{1}σ] ≡ s_{1}[u_{2} ← r_{2}σ][u_{1} ← r_{1}σ] ≡ s_{2}[u_{2} ← r_{2}σ]

we find s_{2} →_{R_{2}} t_{2}, so that we have shown (2).

Case 2: u_{2} is below u_{1}.

Then there is a position v such that u_{2} = u_{1}v. To make the proof more perspicuous we define

ŝ_{1} := s_{1}/u_{1}, t̂_{1} := t_{1}/u_{1} and t̂_{2} := t_{2}/u_{1}.

With this definition we get

(5)  s_{1} ≡ t_{1}[u_{1} ← ŝ_{1}], t_{1} ≡ t_{1}[u_{1} ← t̂_{1}] and t_{2} ≡ t_{1}[u_{1} ← t̂_{2}].

(The first of these equalities is because of the identity t_{1} ≡ s_{1}[u_{2} ← r_{2}σ] equivalent to s_{1} ≡ s_{1}[u_{2} ← r_{2}σ][u_{1} ← ŝ_{1}], which follows from the fact that u_{2} is below u_{1} and the definition of ŝ_{1}, the second follows directly from the definition of t̂_{1} and the third is due to t_{2} ≡ t_{1}[u_{1} ← r_{1}σ].)

If we are now able to find a term ŝ_{2} such that

(6)  ŝ_{1} →_{R_{1}} ŝ_{2} and ŝ_{2} →_{R}^{∗} t̂_{2}

holds, we can define s_{2} := t_{1}[u_{1} ← ŝ_{2}], because then (5) and the compatibility of reductions show (2). The formulas (3) and (4) now have the form

(7)  t̂_{1} ≡ l_{1}σ and t̂_{2} ≡ r_{1}σ,

(8)  ŝ_{1}/v ≡ l_{2}σ and t̂_{1} ≡ ŝ_{1}[v ← r_{2}σ].

From this we get immediately

l_{1}σ/v ≡ r_{2}σ and ŝ_{1} ≡ t̂_{1}[v ← l_{2}σ].

Now there are again two cases depending on whether v ∈O^{∘} (l_{1}) or not. We make a case distinction accordingly.

Case 2.1: v ∈O^{∘} (l_{1}).

Then we have (l_{1}/v)σ ≡ r_{2}σ, so that l_{1}/v and r_{2} are unifyable. If μ is their most general unifier, then there is a substitution ρ such that σ = μρ. The definition shows that

l_{1}[v ← l_{2}]μ →_{R_{2}} l_{1}[v ← r_{2}]μ ≡ l_{1}μ →_{R_{1}} r_{1}μ

is a principal non–standard reduction of the second kind. By assumption there is a s̃_{2} such that

l_{1}[v ← l_{2}]μ →_{R_{1}} s̃_{2} →_{R}^{∗} r_{1}μ

holds. Multiplying this reduction sequence with ρ and defining ŝ_{2} := s̃_{2}ρ we arrive at

(9)  l_{1}[v ← l_{2}]σ →_{R_{1}} ŝ_{2} →_{R}^{∗} r_{1}σ.

Now we only have to observe that

(10)  ŝ_{1} ≡ l_{1}[v ← l_{2}]σ and t̂_{2} ≡ r_{1}σ

holds. The first equation in (10) can be seen as follows: From (8) we can conclude ŝ_{1} ≡ t̂_{1}[v ← l_{2}σ] and because of t̂_{1} ≡ l_{1}σ we get ŝ_{1} ≡ l_{1}[v ← l_{2}]σ. The second equation in (10) is already present in (7). Therefore (9) could be written as

ŝ_{1} →_{R_{1}} ŝ_{2} →_{R}^{∗} t̂_{2}

and this is just (6), which had to be proved.

Case 2.2: v ∉O^{∘} (l_{1}).

Then v can be written as v = v_{1}v_{2} with v_{1} ∈ O(l_{1}) and l_{1}/v_{1} ≡ z ∈ V. We define a substitution τ as

τ(x) := \{ \begin{matrix}σ(z)[v_{2} ← l_{2}σ] & for x ≡ z; \\ σ(x) & else. \end{matrix}

We want to show ŝ_{1} ≡ l_{1}τ. This can be seen as follows:

ŝ_{1} ≡ t̂_{1}[v ← l_{2}σ] ≡ l_{1}σ[v ← l_{2}σ] ≡ l_{1}σ[v_{1} ← (l_{1}σ)/v_{1}][v_{1}v_{2} ← l_{2}σ]
≡ l_{1}σ[v_{1} ← σ(z)[v_{2} ← l_{2}σ]] ≡ l_{1}σ[v_{1} ← τ(z)] ≡ l_{1}τ.

The last equation is valid since l_{1} → r_{1} is left–linear. Defining ŝ_{2} = r_{1}τ we get ŝ_{1} →_{R_{1}} ŝ_{2}. We want to show that ŝ_{2} →_{R_{2}}^{∗} t̂_{2} holds too. To this end we define the set

{w_{1}, ⋯, w_{n}} := {w ∈ O(r_{1}) : r_{1}/w ≡ z}

as the set of all the positions w in r_{1} such that r_{1}/w ≡ z. Because σ and τ differ only in their value on z we find

ŝ_{2} ≡ r_{1}τ ≡ r_{1}τ[w_{1} ← τ(z), ⋯, w_{n} ← τ(z)]

→_{R_{2}}^{n} r_{1}τ[w_{1} ← σ(z), ⋯, w_{n} ← σ(z)] ≡ r_{1}σ ≡ t̂_{2}.

Therefore we have

ŝ_{1} →_{R_{1}} ŝ_{2} →_{R}^{∗} t̂_{2}

as was required.

Case 3: u_{1} is below u_{2}. Then there is a position v such that u_{1} = u_{2}v. To make the proof more perspicuous we define

ŝ_{1} := s_{1}/u_{2}, t̂_{1} := t_{1}/u_{2} and t̂_{2} := t_{2}/u_{2}.

With this definition we get

(11)  s_{1} ≡ t_{1}[u_{2} ← ŝ_{1}], t_{1} ≡ t_{1}[u_{2} ← t̂_{1}] and t_{2} ≡ t_{1}[u_{2} ← t̂_{2}].

(The first of these equalitions follows from t_{1} ≡ s_{1}[u_{2} ← r_{2}σ], the second stems from the definition of t̂_{1} and the third is because of t_{1} ≡ t_{2}[u_{2}v ← l_{1}σ] equivalent to t_{2} ≡ t_{2}[u_{2}v ← l_{1}σ][u_{2} ← t̂_{2}], which can be simplified to t_{2} ≡ t_{2}[u_{2} ← t̂_{2}], which in turn follows from the definition of t̂_{2}.)

If we are now able to find a term ŝ_{2} such that

(12)  ŝ_{1} →_{R_{1}} ŝ_{2} and ŝ_{2} →_{R}^{∗} t̂_{2}

holds, we can define s_{2} := t_{1}[u_{2} ← ŝ_{2}], because then (11) and the compatibility of reductions show (2). The formulas (3) and (4) now take the form

(13)  t̂_{1}/v ≡ l_{1}σ and t̂_{2} ≡ t̂_{1}[v ← r_{1}σ],

(14)  ŝ_{1} ≡ l_{2}σ and t̂_{1} ≡ r_{2}σ.

From this we get immediately

r_{2}σ/v ≡ l_{1}σ and t̂_{1} ≡ t̂_{2}[v ← l_{1}σ].

Now there are again two cases depending on whether v ∈O^{∘} (r_{2}) or not. We make a case distinction accordingly.

Case 3.1: v ∈O^{∘} (r_{2}).

Then we have (r_{2}/v)σ ≡ l_{1}σ, so that r_{2}/v and l_{1} are unifyable. If μ is their most general unifier, then there is a substitution ρ such that σ = μρ. The definition shows that

l_{2}μ →_{R_{2}} r_{2}μ ≡ r_{2}[v ← l_{1}]μ →_{R_{1}} r_{2}[v ← r_{1}]μ

is a principal non–standard reduction of the second kind. By assumption there is a s̃_{2} such that

l_{2}μ →_{R_{1}} s̃_{2} →_{R}^{∗} r_{2}[v ← r_{1}]μ

holds. Multiplying this reduction sequence with ρ and defining ŝ_{2} := s̃_{2}ρ we arrive at

(15)  l_{2}σ →_{R_{1}} ŝ_{2} →_{R}^{∗} r_{2}[v ← r_{1}]σ.

Now we only have to observe that

(16)  ŝ_{1} ≡ l_{2}σ and t̂_{2} ≡ r_{2}[v ← r_{1}]σ

holds. The first equation in (16) is contained in (14) and the second follows from

t̂_{2} ≡ t̂_{1}[v ← r_{1}σ] ≡ r_{2}σ[v ← r_{1}σ] ≡ r_{2}[v ← r_{1}]σ.

Therefore (15) could be written as

ŝ_{1} →_{R_{1}} ŝ_{2} →_{R}^{∗} t̂_{2}

and this is just (12), which had to be proved.

Case 3.2: v ∉O^{∘} (r_{2}).

Then v can be written as v = v_{1}v_{2} with v_{1} ∈ O(r_{2}) and r_{2}/v_{1} ≡ z ∈ V. We define a substitution τ as

τ(x) := \{ \begin{matrix}σ(z)[v_{2} ← r_{1}σ] & for x ≡ z; \\ σ(x) & else. \end{matrix}

We want to show t̂_{2} ≡ r_{2}τ. This can be seen as follows:

t̂_{2} ≡ t̂_{1}[v ← r_{1}σ] ≡ r_{2}σ[v_{1}v_{2} ← r_{1}σ] ≡ r_{2}σ[v_{1} ← σ(z)][v_{1}v_{2} ← r_{1}σ]
≡ r_{2}σ[v_{1} ← σ(z)[v_{2} ← r_{1}σ]] ≡ r_{2}σ[v_{1} ← τ(z)] ≡ r_{2}τ.

The last equation is valid since l_{2} → r_{2} is right–linear. Defining r̂ = l_{2}τ we get r̂ →_{R_{2}} t̂_{2}, since t̂_{2} ≡ r_{2}τ. We also have ŝ_{1} →_{R_{1}}^{+} r̂, which can be seen as follows: Define the set

{w_{1}, ⋯, w_{n}} := {w ∈ O(l_{2}) : l_{2}/w ≡ z}

as the set of all the positions w in l_{2} such that l_{2}/w ≡ z. This set is not empty, because every variable occurring on the right–hand side of a rule has to occur also on the left–hand side. Because σ and τ differ only in their value on z we find

ŝ_{1} ≡ l_{2}σ ≡ l_{2}σ[w_{1} ← σ(z), ⋯, w_{n} ← σ(z)]
→_{R_{1}} l_{2}σ[w_{1} ← τ(z), w_{2} ← σ(z), ⋯, w_{n} ← σ(z)]
→_{R_{1}}^{∗} l_{2}σ ≡ l_{2}σ[w_{1} ← τ(z), ⋯, w_{n} ← τ(z)] ≡ l_{2}τ ≡ r̂.

Defining ŝ_{2} := l_{2}σ[w_{1} ← τ(z), w_{2} ← σ(z), ⋯, w_{n} ← σ(z)] we immediately get

ŝ_{1} →_{R_{1}} ŝ_{2} →_{R_{1}}^{∗} r̂ →_{R_{2}} t̂_{2}

which shows (12) in this case and therefore the proof is now complete. _{□}

As an immediate corollary to the Principal Non–Standard Reduction Lemma and the Standardization Lemma we get our main result.

Theorem 11 (Decidability of Quasi–Commutation) If (R_{1}, <_{1}) and (R_{2}, <_{2}) are terminating rewrite systems such that R_{1} is left–linear and R_{2} is right–linear, then →_{R_{1}} quasi–commutes over →_{R_{2}} if and only if for every principal non– standard reduction

s_{1} →_{R_{2}} t_{1} →_{R_{1}} t_{2}

there is a term s_{2} such that

(1)  s_{1} →_{R_{1}}^{+} s_{2} →_{R_{2}}^{∗} t_{2}.

Therefore the question, whether →_{R_{1}} quasi–commutes over →_{R_{2}} is decidable.

Proof: The Lemma would have been immediate if we had only demanded that for every principal nonstandard reduction s_{1} →_{R_{2}} t_{1} →_{R_{1}} t_{2} there exists a term s′_{2} satifying

(2)  s_{1} →_{R_{1}} s′_{2} →_{R}^{∗} t_{2}.

There are two cases. If →_{R_{1}} quasi–commutes over →_{R_{2}} the Standardization Lemma tells us that the existence of a term s_{2} satisfying (1) is equivalent to the existence of a term s′_{2} satisfying (2). If, one the other hand, →_{R_{1}} is not quasi–commuting over →_{R_{2}} there has to be a principal non–standard reduction sequence s_{1} →_{R_{2}} t_{1} →_{R_{1}} t_{2} such that there is no term s′_{2} satisfying (2). But then there is also no term s_{2} satisfying (1), because (1) is just a special case of (2).

We tacitly assume R_{1} and R_{2} to be finite. Then there are only finitely many principal non– standard reductions. The question whether →_{R_{1}} quasi–commutes over →_{R_{2}} is now reduced to the problem of finding for every principal non–standard reduction s_{1} →_{R_{2}} t_{1} →_{R_{1}} t_{2} a term s_{2} satisfying (1). Since we have assumed R_{1} and R_{2} to be terminating this problem is decidable. _{□}

Because of Theorem (6) we now have a non–trivial, decidable and sufficient condition for the union of two terminating rewrite systems to be terminating.

If we are only interested in the question whether normal forms computed with a rewrite system R_{1} are conserved under rewriting with another rewrite system R_{2}, we need the following weaker version of Lemma 10.

Lemma 12 If (R_{1}, <_{1}) and (R_{2}, <_{2}) are rewrite systems such that R_{1} is left–linear, then the relation →_{R_{1}}–normal forms are conserved under →_{R_{2}}–reductions if and only if for every principal non–standard reduction

s_{1} →_{R_{2}} t_{1} →_{R_{1}} t_{2}

the term s_{1} is R_{1}–reducible.

Since the proof of this Lemma is completely analogous to the proof of the Principal Non– Standard Reduction Lemma, it will not be given here. Note however the weaker conditions of this Lemma concerning linearity. Now only R_{1} has to satisfy a linearity requirement. The last Lemma enables us to decide whether the normal forms of a rewrite system →_{R_{1}} are conserved under →_{R_{2}}–reductions, because there are only finitely many principal non–standard reductions. In the next section we will make use of this observation.

4 Algebraic Examples

We now give some algebraic examples illustrating the concepts we have developed. We start with group theory.

4.1 Group Theory

The following rewrite system is known to be convergent and implements group theory [1]:

\begin{matrix}(1) e ∗ x → x & (2) x ∗ e → x \\ (3) x^{−} ∗ x → e & (4) x ∗ x^{−} → e \\ (5) x ∗ (x^{−} ∗ y) → y & (6) x^{−} ∗ (x ∗ y) → y \\ (7) (x ∗ y) ∗ z → x ∗ (y ∗ z) & (8) e^{−} → e \\ (9) (x^{−})^{−} → x & (10) (x ∗ y)^{−} → y^{−} ∗ x^{−} \end{matrix}

This rewrite system can be split up in the following way: R_{1} consists of the rules (8), (9) and (10), all the other rules belong to R_{2}. One can then check (we have done this with a computer implementation of the ideas described so far) that there are no principal non– standard reductions of the first kind, while there are three non–standard reductions of the second kind:

\begin{aligned}(x^{−} ∗ x)^{−} & →_{R_{2}} & e^{−} & →_{R_{1}} & e, \\ (x ∗ x^{−})^{−} & →_{R_{2}} & e^{−} & →_{R_{1}} & e, \\ ((x ∗ y) ∗ z)^{−} & →_{R_{2}} & (x ∗ (y ∗ z))^{−} & →_{R_{1}} & (y ∗ z)^{−} ∗ x^{−}. \end{aligned}

Now it can easily be seen that the first term of all these principal non–standard reductions is →_{R_{1}}–reducible. Therefore we can conclude by Lemma 12 that →_{R_{1}}–normal forms are conserved by →_{R_{2}} reductions. However, →_{R_{1}} is not quasi–commuting over →_{R_{2}}. This can be seen by investigating the last principal non–standard reduction. If →_{R_{1}} was quasi–commuting over →_{R_{2}}, then there would have to be a term t such that

((x ∗ y) ∗ z)^{−} →_{R_{1}} t →_{R} (y ∗ z)^{−} ∗ x^{−}

would hold. Then t would have to be z^{−} ∗ (x ∗ y)^{−}. But there is only one reduction which can be applied to this term and this reduction leads to the term z^{−} ∗ (y^{−} ∗ x^{−}), which is in normal form and not identical to (y ∗ z)^{−} ∗ x^{−}.

4.2 Ordered Rewriting

To be able to present some more interesting examples, we have to extend the concepts developed so far to ordered rewrite systems [6]. An ordered rewrite system is a pair (E, <), where E is a set of equations and < is a simplification ordering. Note that there is only one difference between rewrite systems and ordered rewrite systems. We postulated for a rewrite system (E, <), that we have r < l for all equations l = r ∈ E, this requirement is dropped for ordered rewrite systems.

An ordered rewrite system (E, <) induces a binary relation →_{E} on T (F, V), which is defined as s →_{E} t iff there exists a position u ∈ O(t), a rule l → r ∈ E and a substitution σ such that

s/u ≡ lσ t ≡ s[u ← rσ] and rσ < lσ

holds. Here the only difference between the relation →_{R} generated by a rewrite system (R, <) and the relation →_{E} generated by an ordered rewrite system is the test whether rσ < lσ holds for the instance of the equation which is used for rewriting the term under inspection. (Note that this test is superfluous for a rewrite system, because we already have r < l and the stability of the simplification ordering then ensures rσ < lσ for all substitutions σ.)

Ordered rewrite systems can not be confluent if they contain an equation s = t, whose sides can not be compared. Therefore the notion of confluence has to be replaced by the weaker notion of ground confluence. A rewrite system (E, <) is ground confluent if for all closed terms s, t_{1} and t_{2} such that s →_{E} t_{1} and s →_{E} t_{2} holds, there exists a term t_{3} satisfying t_{1} →_{E} t_{3} and t_{2} →_{E} t_{3}.

It turns out that all of the concepts we have given so far for rewrite systems can also be given for ordered rewrite systems with only some minor self–evident adjustments. The same is true for all of the theorems we have proved so far. We will just give the definition of principal non–standard reductions for ordered rewrite systems and reformulate Lemma 12 for this case, the rest is left to the reader. Again we assume that (R_{1}, <_{1}) and (R_{2}, <_{2}) are two ordered rewrite systems.

Definition 13 (Principal Non–Standard Reductions) Non–standard reductions come in two forms. Assume that

• l_{1} → r_{1} ∈ R_{1} and l_{2} → r_{2} ∈ R_{2}, • u ∈O^{∘} (r_{2}) and l_{1} and r_{2}/u are unifyable with most general unifier μ and

• l_{1}μ ≰ r_{1}μ and l_{2}μ ≰ r_{2}μ.

Then we call the reduction sequence

l_{2}μ →_{R_{2}} r_{2}μ ≡ r_{2}[u ← l_{1}]μ →_{R_{1}} r_{2}[u ← r_{1}]μ

a principal non–standard reduction of the first kind.

To define the principal non–standard reductions of the second kind we assume

• l_{1} → r_{1} ∈ R_{1} and l_{2} → r_{2} ∈ R_{2},

• u ∈O^{∘} (l_{1}) and l_{1}/u and r_{2} are unifyable with most general unifier μ,

• l_{1}μ ≰ r_{1}μ and l_{2}μ ≰ r_{2}μ and

• r_{2} is not a variable.

Then we call the reduction sequence

l_{1}[u ← l_{2}]μ →_{R_{2}} l_{1}[u ← r_{2}]μ ≡ l_{1}μ →_{R_{1}} r_{1}μ

a principal non–standard reduction of the second kind.

Now a non–standard reduction is a non–standard reduction of the first or second kind.

If s_{1} →_{R_{2}} t_{1} →_{R_{1}} t_{2} is a principal non–standard reduction, then we do not know whether the reductions s_{1} →_{R_{2}} t_{1} and t_{1} →_{R_{1}} t_{2} are actually valid as ordered reductions, because we do not know whether t_{1} <_{2} s_{1} and t_{2} <_{1} t_{1} holds. We only know t_{1} ≰_{1} t_{2} and s_{1} ≰_{2} t_{1}. Therefore there might be a substitution σ such that t_{1} <_{2} s_{1} and t_{2} <_{1} t_{1} hold and then s_{1}σ →_{R_{2}} t_{1}σ →_{R_{1}} t_{2}σ really is a sequence of valid ordered reductions.

These considerations show that the notion of a rewrite system has to be refined a little bit more. Therefore we define the concept of rewriting under a constraint, which was introduced by Peterson [8]. We will not give a formal definition, but just an example to clarify the basic idea. If our ordered rewrite system (E, <) contains the axiom of commutativity and the ordering < is the lexicographic path ordering, then we have

(∗)  x ∗ y →_{E} y ∗ x if x < y.

Here the formula x < y is called the constraint of the reduction (∗). We also say that the constraint x < y enables the reduction x ∗ y → y ∗ x. Now we can state the lemma which is needed for our examples.

Lemma 14 If (R_{1}, <_{1}) and (R_{2}, <_{2}) are ordered rewrite systems such that R_{1} is left–linear, then the relation →_{R_{2}} is →_{R_{1}} conserving if for every principal non–standard reduction

s_{1} →_{R_{2}} t_{1} →_{R_{1}} t_{2}

and for every constraint C enabling this reduction there is a term s_{2}, such that the reduction s_{1} →_{R_{1}} s_{2} is enabled by C.

Now we have developed enough theory to give another example.

4.3 Rings of Characteristic 2

For rings of characteristic 2 there is an ordered rewrite system, which can be shown to be ground confluent with the methods of Martin and Nipkow [7]. We have done this with an implementation of the ideas of Martin and Nipkow together with some ideas of our own. The system is as follows:

\begin{matrix}(1) X ∗ (Y + Z) = X ∗ Y + X ∗ Z & (2) (Y + Z) ∗ X = Y ∗ X + Z ∗ X \\ (3) (X + Y) + Z = X + (Y + Z) & (4) X + Y = Y + X \\ (5) 0 + X = X & (6) X + X = 0 \\ (7) Y + (X + Z) = X + (Y + Z) & (8) X + 0 = X \\ (9) X + (X + Y) = Y & (10) X ∗ Y = Y ∗ X \\ (11) (X ∗ Y) ∗ Z = X ∗ (Y ∗ Z) & (12) Y ∗ (X ∗ Z) = X ∗ (Y ∗ Z) \\ (13) 0 ∗ X = 0 & (14) X ∗ 0 = 0 \end{matrix}

For later reference we will denote this system as R. In order to have an ordered rewrite system we have to specify the ordering. We have taken the lexicographic path ordering, defining the precedence of the function symbols as 0 < 1 < + < ∗. If we now define R_{1} as the system consisting of the distributivity laws (1) and (2), while all the other rules are contained in R_{2}, our computer implementation shows that →_{R_{1}}–normal forms are conserved under →_{R_{2}}–reductions. But we can go further than this. All together we have found four ways to split the system. They are listed below:

\begin{matrix}1. & R_{1} = \{(1), (2)\} & R_{2} = \{(3), ⋯, (14)\} \\ 2. & R_{1} = \{(1), (2), (13), (14)\} & R_{2} = \{(3), ⋯, (12)\} \\ 3. & R_{1} = \{(1), (2), (10), ⋯, (14)\} & R_{2} = \{(3), ⋯, (9)\} \\ 4. & R_{1} = \{(1), ⋯, (4), (7), (10), ⋯, (14)\} & R_{2} = \{(5), (6), (8), (9)\} \end{matrix}

In the cases listed above it is always true that →_{R_{1}}–normal forms are conserved under →_{R_{2}}– reductions. Therefore we can split the original system into five parts. We define

\begin{matrix}R̂_{1} := \{(1), (2)\}, & R̂_{2} := \{(13), (14)\}, & R̂_{3} := \{(10), (11), (12)\}, \\ R̂_{4} := \{(3), (4), (7)\}, & R̂_{5} := \{(5), (6), (8), (9)\}. \end{matrix}

The idea behind this split is that the computation of R–normal forms can now proceed in five stages. To compute the R–normal form of a term s, we first build the normal form with respect to R̂_{1}, then this normal form is normalized with respect to R̂_{2} and so on, until we finally arrive at a term t in R̂_{5}–normal form. This term is not only in R̂_{5}–normal form, but also in R̂_{1}, R̂_{2}, R̂_{3} and R̂_{4}–normal form. To see this, we just have to notice that for instance R̂_{1} ∪ R̂_{2}–normal forms are conserved under R̂_{3} ∪ R̂_{4} ∪ R̂_{5}–reductions. Therefore in particular R̂_{1}–normal forms and R̂_{2}–normal forms are conserved under R̂_{3}–reductions. Because R = R̂_{1} ∪ ⋯ ∪ R̂_{5} the term t is then also in R–normal form. If we take a closer look at the effect of the ordered rewrite system R̂_{3}, we see that it amounts to grouping the parantheses in every product to the right and then sorting the product by an algorithm which is essentially the Bubble–Sort algorithm. Now there are other algorithms (for instance Quick–Sort) which are known to be much more efficient than Bubble–Sort. We can take one of these algorithms to achieve the same effect the ordered rewrite system R̂_{3} would achieve otherwise. Thereby, the efficiency of the computation of normal forms can be considerably increased.

References

[1] Bachmair, L., “Canonical Equational Proofs”, (Birkhäuser, Boston, 1991).

[2] Bachmair, L. and N. Dershowitz, “Commutation, Transformation, and Termination”, Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, Lecture Notes in Computer Science 230, (Springer, Berlin, 1986), pp. 5–20.

[3] Chandy, K. M. and J. Misra, “Parallel Program Design”, (Addison–Wesley, Reading, 1988).

[4] Dershowitz, N., “Termination of Rewriting” Journal of Symbolic Computation 3(1&2) (1987), pp. 69–115.

[5] Dershowitz, N. and Jouannaud, J.–P., “Rewrite Systems” Handbook of Theoretical Computer Science (Vol. B: Formal Models and Semantics), North–Holland, Amsterdam, 1990, pp. 243–320.

[6] Hsiang, J and M. Rusinowitch, “On word problems in equational theories”, Proc. Fourteenth International Colloquium on Automata, Languages and Programming, Karlsruhe, West Germany, Lecture Notes in Computer Science 267 (Springer, Berlin, 1987) pp. 54–71.

[7] Martin, U. and T. Nipkow, “Ordered Rewriting and Confluence”, 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 1990, Lecture Notes in Computer Science 449 (Springer, Berlin, 1990) pp. 366–380.

[8] Peterson, G. E., “Complete Sets of Reductions with Constraints”, 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 1990, Lecture Notes in Computer Science 449 (Springer, Berlin, 1990) pp. 366–380.

[9] Toyama, Y., “On the Church–Rosser Property for the Direct Sum of Term Rewriting System”, J. Assoc. Comput. Mach. 34(1) (1987) pp. 128–143.

[10] Toyama, Y., “Commutativity of Term Rewriting Systems”, in: K. Fuchi and L. Kott, eds., Programming of Future Generation Computer II (North Holland, Amsterdam, 1988) pp. 393–407.

[11] Toyama, Y., J. W. Klop and H. P. Barendregt, “Termination for the Direct Sum of Left–Linear Term Rewriting Systems, Proc. Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, Lecture Notes in Computer Science 355 (Springer, Berlin, 1989) pp. 477–491.