Deciding the confluence of ordered term rewrite systems.
replace me
Introduction
rewrite systems (TRS) have been applied to many problems in symbolic computa-
tion, automated theorem proving, program synthesis and verification, and logic programming
among others. Two fundamental properties of TRS are termination and confluence,
which together ensure the existence and uniqueness of normal forms and hence a decidable
word problem. Let us take a closer look at both properties.
Termination of TRS is undecidable even for left-linear one-rule systems [Dau89]. However,
a TRS R terminates if, and only if, there is some reduction ordering ? such that l ? r for
each l ! r 2 R, and there are practical general-purpose methods for defining such ?. But
standard TRS cannot deal with inherently non-orientable axioms (like the commutativity
axiom). Therefore they have been generalized to ordered TRS (E; ?), where rewriting is
The second author partially supported by the NSF grants CCR-9712396 and INT-9401087. The other
three authors are supported by the CCL ESPRIT working group 22457. An earlier verion of this work,
presented at the LICS'98 conference, included similar results limited to the LPO ordering.
done by applying equations of E in whatever direction agrees with ? [HR87]. Hence ordered
TRS can handle any set of equations E, being terminating by definition. A standard choice
in practice for ? is some of the existing general-purpose path orderings, since they are
easily defined and implemented. In Section 2 we characterize the requirements on ? that
are needed for solving word problems by ordered rewriting, and we show that they can be
obtained in a simple way for path orderings.
Confluence is undecidable in general, but for terminating TRS a decision procedure is
given in Knuth and Bendix' landmark paper [KB70]: a TRS is confluent if, and only if, all
its critical pairs are joinable. For ordered TRS, deciding confluence is more difficult. It has
been a long standing open question, listed for instance as open problem #64 in the RTA'93
list [DJK93]. The main problem is that, due to the ordering restrictions, different instances
of a critical pair may require different joinability proofs.
Here we prove the decidability of confluence if ? belongs to a class of path orderings: then
it is possible to finitely analyze the joinability of all ground instances -possibly with new
symbols- of each critical pair. Dealing with new symbols is essential for deciding arbitrary
word problems, and it is also a fundamental characteristic of the notion of confluence, since
the weaker property of ground confluence, i.e., confluence when rewriting only ground terms
over the given signature, is undecidable even for terminating standard TRS [KNO90].
Example: Let E consist of the (clearly non-orientable) single equation
y). Then there is a critical pair cp which is (z To
show confluence, we have to prove that every instance cpoe is joinable by ordered rewriting
with E. In this example, this can be done by considering a number of well-chosen ordering
relations between terms that cover all possible cases. On the one hand, one considers (i)
yoe, and, on the other, the further
possible relations with uoe. In all cases, joinability follows. Note that it is not sufficient here
to consider only relations between variables, as observed in [MN90].
In general the picture is not so simple as in the previous example. Joinability proofs may
have more than one step, and the cases of ordering relations considered must be compatible
with the ones of previous steps, and also the new equality relations may introduce additional
subterms that can be rewritten. Furthermore, one has to show that the search process of
attempted joinability proofs by such a case analysis is finite, while covering all possible cases.
In the following we do this by building for each critical pair cp an arbitrary confluence tree,
whose nodes are ordering-constrained equations, and whose root is cp. Children of a node are
obtained by three possible steps: constrained rewriting , decomposition, and instantiation.
These steps precisely generate the right ordering relations that have to be analyzed. Our
main result is finally that (E; ?) is confluent if, and only if, all leaves of the trees are
tautologies.
The whole process of building the trees importantly relies on existing results for ordering
constraint solving. This is also the case for our proof of finiteness of the trees. Here we
adapt the constraint solving algorithms of [Nie93] with extended signature semantics (i.e.,
new symbols may appear in solutions) for the recursive path ordering with status (RPOS).
In RPOS, every symbol is assigned a lexicographic or a multiset status. The lexicographic
path ordering (LPO) or the multiset path ordering (MPO) are obtained as particular cases
of RPOS by making all symbols lexicographic or multiset, respectively (see, e.g., [Der82]).
More refined path orderings like KNS [KNS85] or RDO [Les90] are included as well, since
all these orderings coincide on ground terms [Der87], and hence the same constraint solving
algorithms apply.
We emphasize that our decision procedure is not only of theoretical interest. Since Knuth
and Bendix' paper in the late 60's, a lot of work has been devoted to the completion of
standard TRS and to ordered (or unfailing) completion of ordered TRS (e.g., [BDH86,
HR87, Pet90, MN90, BD94]). Ordered completion provably yields a confluent system after
a (possibly infinite) number of iterations. It roughly amounts to a systematic closure of
the TRS under inclusion of (simplifications of) its non-joinable critical pairs. In order to
enhance the efficiency of completion and to find finite complete TRS whenever they exist,
powerful methods for proving the joinability (and hence redundancy) of a critical pair are
crucial. This is precisely what our method is able to do (automatically), making it now also
possible to decide whether the completion has finished. In fact, in [NN93] we reported on
the use of similar trees in the Saturate system [GNN95] as a successful method for proving
the redundancy of critical pairs. Furthermore, in case of non-joinability, instead of adding
the critical pair to E, one may choose to add the non-tautology leaves of the tree.
Comparing our result with the undecidability of confluence for arbitrary finite term
rewriting systems, it seems quite surprising (in favour of ordered rewriting), since extending
the notion of reduction we go from undecidability to decidability. There is an obvious clue
for this result: ordered rewriting is always terminating. However, the picture is not so
simple. For instance, we also show that for finite sets of constrained equations, confluence
is undecidable (while ordered rewriting is still terminating). This relativizes the scope of
our decidability result and also shows its significance.
Unfortunately, in completion with constraint inheritance [KKR90, NR95], constrained
equations appear even if we start with only unconstrained ones. In such an equation e j c,
the constraint c records the conditions under which e is derivable. This restricts the number
of critical pairs that have to be considered, but arbitrary simplification by rewriting is not
allowed any more. In this context, our problem is to decide joinability of the critical pairs by
rewriting with a set of constrained equations. This is not easy, because simplification with
an arbitrary constrained rule is undecidable [CT97]: given a term s and a rule l ! r j c, it
is undecidable whether or not all instances of s can be reduced.
Going further, we investigate the use of ordered rewriting in a classical application of
rewrite systems: the proof-by-consistency approach to proving inductive theorems [KM87,
JK86, Bac88]. Here again, the result is the opposite of what happens in the case of finite
rewriting systems: we show that ground reducibility is undecidable for ordered
rewriting.
The paper is organized as follows. We mainly focus on our decidability result: the decidability
of confluence. We first recall in Section 2 the basic notions of ordered rewriting, as
well as some results on ordering constraints. In Section 3, we introduce our confluence trees
and we show how to solve constraints over the set of normal forms and derive the decidability
of confluence. In Section 4 we sketch the undecidability of confluence for a finite set
of constrained equations. In Section 5, we show that ground reducibility is undecidable for
ordered rewriting. Finally, in Section 6, we state some possible extensions and implications
of our decidability result in other areas.
Ordered Rewriting and RPOS Constraints
We adopt the terminology and the notations of [DJ90]. T is the set of first-order
terms built on alphabets F of function symbols and X of variable symbols. T (F) is the set of
terms which do not contain any variables. A multiset over a set S is a function M
The union and intersection of multisets are defined as usual by M 1 [M 2
and We also use a set-like notation:
denotes a and x 6j b. A multiset M is empty
An equation is a multiset of two terms, written
s and t are in T Positions in a term are strings of positive integers, corresponding
to paths in the tree representation of the term. The set of positions of a term t is written
Pos(t). If p is a position of t, then tj p is the subterm of t at position p and t[u] p is the
term obtained by replacing tj p with u at position p in t. The topmost symbol of a term
. The size of a term t, denoted jtj, is 1 if t is a variable and
is a term f(t between two terms (identity)
will be written j in order to distinguish it from the equality symbol in equations.
If ! is a binary relation on a set S, then / is its inverse, $ its symmetric closure, !
its reflexive-transitive closure and ! + its transitive closure. We write
and there is no t 0 such that t ! t 0 . Then t is called a normal form of s. The relation !
is well-founded or terminating if there exists no infinite sequence s it is
confluent if the relation /   contained in the joinability relation !   ffi /   . It is
locally confluent if the relation / ffi ! is contained in the joinability relation !   ffi /   . A
relation ! on terms is monotonic if terms u and positions
p.
A (strict, partial) ordering is an irreflexive transitive binary relation. An ordering - on
reduction ordering if it is well-founded, monotonic, and stable under substitutions
implies soe - toe for all oe with range in T
The word problem for a set of equations E is to check, given an equation
or not it is a logical consequence of E (denoted as usual E We denote by $E
the smallest monotonic relation on terms such that soe $E toe for all substitutions oe and
t.
2.1 Ordered rewriting
An ordered term rewrite system (TRS) is a pair (E; -), where E is a set of equations, and
- is a reduction ordering. The ordered rewriting relation defined by (E; -) is the smallest
binary relation !E;- on terms such that soe !E;- toe whenever
soe - toe.
Our aim is to apply ordered rewriting with (E; -) for solving word problems E
built over T In general will be universally quantified, but it is well-known
that it suffices to consider only ground a signature with sufficiently many new
constant symbols. For our purposes, we need to go slightly beyond: we consider only one
new symbol succ. In the following, let 0 be a constant symbol in F (if there is no constant
in F , then 0 is added as usual), let succ be a new unary function symbol not in F , and let
F e denote F [ fsuccg.
Proposition 1 Let E be a set of equations and let be an equation, where s, t, and
all terms in E are built over T oe be the
substitution fx 1 7!
only if, soe
In standard rewriting, termination and confluence of !R suffice for solving word problems
in the theory of a TRS R, since then s
R t if, and only if, s !
R t, i.e., if the (unique)
normal forms of s and t by !R coincide.
In ordered rewriting this is no longer the case if the relation !E;- is restricted by a too
ordering -. For example, if - is the empty ordering, then !E;- is empty as well (and
hence confluent and terminating), but useless for our purpose. A necessary condition on
- is clearly that there should be a unique minimal element w.r.t. - in each E-congruence
class. But even this is insufficient: if E is is the smallest relation
containing a - c and b - c, then !E;- is confluent and terminating but a and c are different
E-equivalent normal forms.
Since by proposition 1 it suffices to consider word problems where the equation
be proved is built over T in the literature this problem is overcome by requiring - to
be total on ground terms.
Below we show that this can be weakened: it is sufficient that - orients all non-trivial
instances of the equations, i.e., these instances have a one-step rewrite proof using !E;- .
But in fact it suffices to consider rewrite proofs with an arbitrary number of steps. This
leads to the following precise characterization of what is needed for deciding word problems:
be an ordered term rewrite system such that !E;- is confluent and
terminating on T The the following two statements are equivalent:
1. uoe !
E;- voe for all all oe with range in T
2. For all s, t in T
hence the word problem for E is decidable).
Proof: The second statement trivially implies the first one. Conversely, for all s; t 2 T
clearly
t, and, if s
t, we have a derivation s
and the monotonicity of -, each step can be decomposed
into zero or more steps of $E;- , and, by confluence and termination of !E;- , this implies
t. 2
This lemma shows the relevance of the following:
be a set of equations built on T
Given a well-founded monotonic ordering - on T (F), the ordered rewrite system (E; -)
is ground confluent if !E;- is confluent on T (F).
Given a well-founded monotonic ordering - on T confluent if !E;- is
confluent on T
Note that in classical term rewriting confluence is defined for arbitrary extensions of
F with new symbols, but this makes no sense in ordered rewriting without extending -
accordingly. But, as said, the extension to T practice, and hence our
definition of confluence for ordered TRS is the adequate counterpart of confluence of classical
TRS.
As for classical term rewriting, in ordered rewriting there is a gap between confluence and
ground confluence: given an ordering - on T confluence implies ground confluence,
but the converse is false. An easy example if given by 0g. This
rewrite system is not confluent. However, if F only consists of 0; f , then the system is
ground confluent. This example also applies to ordered rewrite systems: introducing new
symbols in F e allows to form critical peaks that cannot be reduced. For example, with the
corresponding -, we would have f(succ(0)) !E;- succ(0) and f(succ(0)) !E;- 0, with
distinct normal forms succ(0) and 0. In the next section, the new symbol succ will also be
used to build solutions of ordering constraints, which is crucial in this respect.
2.2 The Recursive Path Ordering with Status (RPOS)
Let - be an ordering on terms and let = be a congruence relation. The lexicographic
(left to right) extension - lex of - w.r.t. = for n-tuples is defined:
for some k in is well founded, so is - lex . The extension of = to multisets,
denoted by = mul , is the smallest relation such that
The extension of - to multisets w.r.t. = is defined as the smallest ordering - mul s.t.
If - is well-founded on S, so is - mul on finite multisets over S [DM79].
Let ?F be a well-founded ordering on F (called the precedence), and let stat be the status
function stat: F ! flex,mulg. Then the RPOS ordering is defined as follows: s ? rpos x if x
is a variable that is a proper subterm of s or else s j at
least one of the following conditions hold:
t, for some
(and hence n=m) and
(and hence n=m) and
rpos and ? mul
rpos are defined w.r.t. = rpos , equality up to permutation of
arguments of function symbols with mul (multiset) status.
RPOS is a reduction ordering on terms that fulfills the subterm property (s ? rpos t if
t is a proper subterm of s). Hence it also contains the (strict) tree embedding relation, the
smallest transitive monotonic relation ? emb such that s ? emb t if t is a proper subterm of s.
LPO is the particular case of an RPOS with only lex (lexicographic) status symbols. It
is a simplification ordering that is total on T (F) if ?F is total on F . RPOS is total on
is total on F .
LPO with a total precedence is a standard choice for ordered TRS, since it fulfills the
requirements of Lemma 1 if the precedence is total on F . For RPOS these requirements
have to be ensured by making f lexicographic whenever there are "permuting" equations
(possibly with some context) where - is a permutation, thus
avoiding any non-orientable F e -instances.
Hence in the following we will assume ? rpos to be such an RPOS on T linear
precedence ?F e where 0 is the smallest constant symbol in F (if there is no constant in
F we can add one w.l.o.g.) and the unary symbol succ is the smallest function symbol.
Furthermore, we will consider ordered rewrite systems (E; ? rpos ), but all our results apply
equivalently to ordered TRS (E; -) where - is any ordering such that s - t iff s ? rpos t
for all ground terms s and t, which is in particular the case for the aforementioned path
orderings KNS and RDO. The ordering ? lpo will be used several times to denote an RPOS
where all symbols have lexicographic status.
Example 1 Let E be the set fx zg. If s j
t and hence s
t +s. We also have (succ(0)+0)+0 !E;? lpo
(0+succ(0))+0 !E;? lpo
0+(0+succ(0)), the latter term being irreducible.
Example 2 Let E be the set ff(x;
f(a; a) !E;? lpo
g(a; a), but f(a; a) also rewrites into g(a; b) or g(a; 0) or into g(a; succ(0)),
etc., since there is a choice on how to instantiate the so-called extra variable z, as long as
the step is reductive w.r.t. ? lpo
Of course, if !E;? lpo
is confluent all choices lead to the same normal form. For the equivalent
set
is confluent
and all terms of the form f(s; t) or g(s; t) have g(s; 0) as unique normal form. Clearly 0 is
the most "efficient" choice for instantiating extra variables like z; in fact, to reach a normal
form here, one is eventually forced to chose 0.
2.3 RPOS constraints
Definitions and notations of this section are consistent with [Com90, Nie93, NR95], which
refer to for more details and the main results.
Here we restrict ourselves to RPOS-constraints with extended signature semantics, which
is, as we will see, what is needed for our results on confluence. In the following, an RPOS
constraint is a Boolean combination (using the connectives -; :) of atoms
ordering constraint is interpreted on T the Boolean
connectives have their usual meaning and an assignment oe of the variables of s ? t (resp.
oe when the assignment oe satisfies the constraint c; then oe is called a solution for c. We
sometimes write chains s
and also s - t as a shorthand for s ? t.
Example 3 Let oe be the assignment fx 7! succ(0); y 7! succ(succ(0))g. Then oe
x. The constraint f(x; y) ? unsatisfiable independently of
the (lexicographic or multiset) status of f .
An interesting property of RPOS is that for non-variable terms s and t, the relation
follows from at least one conjunction of relations of the form s
are subterms of s and t respectively and jsj
rise to the so-called RPOS decomposition of a relation s ? t: if s j f(s
ffl for all are RPOS decompositions of s ? t
is an RPOS decomposition of s ? t
m) and
of the form:
i.e., all constraints implying hs are RPOS decompositions
of s ? t.
m) and
implying are RPOS decompositions of s ? t.
An RPOS constraint c without disjunctions is called RPOS-closed iff 0 ? x is not in
c and for each relation s ? t in c where s and t are non-variable terms, c contains an
RPOS-decomposition of s ? contained as well if s j t).
Example 4 Suppose f ?F e g. The RPOS decomposition of f(x; y)?g(x; z) is f(x; y)?x -
y)?z. The four RPOS decompositions of g(x; y)?f(y; z) are x?f(y; z), x=f(y; z),
z). There are six RPOS decompositions of f(x; y) ? f(y; z) if
namely x?f(y; z), y?f(y; z), x=f(y; z), y=f(y; z), x?y - f(x; y)?z
and x=y - y?z. There is one RPOS decomposition of f(x; y)?f(z; x) if
namely y?z.
A simple system S is a particular constraint of the form s n # n s
or ?, every strict subterm of an s i is some s j and i
is the least equivalence relation on fs which contains all pairs (s
such that # i is =. ? S is the least transitive relation on fs containing all pairs
and such that
In are respectively the equality and ordering constraints that can be
deduced from S.
In what follows, we will assume that all terms occurring in a simple system are written
in a sorted way, that is, such that t i occurs in S for f with
multiset status and 1 n. The equational part of a simple system S, which we write
eqpart(S), is tg. The inequational part of S, denoted ineqpart(S), is fsoe ?
oe is the most general simultaneous unifier of eqpart(S) and
if eqpart(S) is not unifiable. S is called purely inequational if S j ineqpart(S).
The satisfiability problem for RPOS constraints over extended signatures can be solved
in NP time following the methods of [Nie93]. Key steps for these results are as follows:
1. Any constraint c is (effectively) equivalent to a finite disjunction of simple systems
hence c is satisfiable if, and only if, S i is satisfiable for some
2. A simple system S is unsatisfiable if eqpart(S) is not unifiable.
3. A simple system S is equivalent to ineqpart(S) if eqpart(S) is unifiable.
4. A purely inequational simple system is satisfiable if, and only if, it is RPOS-closed.
Proof: We only sketch the proof for the last statement, since it is less obvious and the
construction will be used throughout the paper. First, note that if s ? S t and S contains
no RPOS decomposition for s ? t, then it must be unsatisfiable since S is closed under
subterms and hence S must be in contradiction with all RPOS decompositions of s ? t.
This happens for example with the constraint f(y;
For the reverse implication, if S is of the form s build a solution oe
from right to left, i.e., by induction on the index i: if s i is a variable, then let s i oe be succ(0)
To see that this oe is indeed a solution, we use the fact
that S is RPOS-closed: using an induction argument on jsj + jtj for each relation s ? S t,
it can be shown that the substitution oe satisfies S if, and only if, it satisfies all relations
s or t is a variable, which in turn holds since succ is a new smallest symbol
(see [Nie93] for details). 2
In the following, the previous kind of solution for S will be called the minimal solution
for S. Note that it is alien: for every variable x, the solution xoe is headed by the new
3 Decidability of confluence of ordered rewriting
In the following, (E; ? rpos ) will be an ordered TRS. According to the previous section, we
assume that terms of E belong to T that substitutions, and the interpretation of
constraints are in T constrained equation is a pair
is an equation and c is a constraint. It denotes all its instances: the equations
such that oe Hence it is a tautology if soe j toe for all such oe. A critical pair between
two equations of E is a constrained equation u[t]
for some position p such that uj p is not a variable. Newmann's lemma states that, for a
terminating relation, confluence is equivalent to local confluence, which for term rewriting
(resp. ordered rewriting) reduces to the joinability of critical pairs. The following result is
essentially due to J. Hsiang and M. Rusinowitch [HR87] (see also [BDH86]):
Lemma 2 !E;?rpos is confluent if, and only if, for every critical pair
equations in E all its instances are joinable, i.e., there is a term u such that
E;?rpos u /
E;?rpos toe.
A confluence tree for (E; ? rpos ) and a critical pair is a tree T where the nodes
of T are constrained equations, the root of T is and the children of a node e j c in
T are the constrained equations obtained by one of the following three kinds of steps:
1. By constrained rewriting , e j c can be rewritten with
and into the complementary equation e j c - roe - loe iff
loe ?roe is satisfiable
for every variable x in r not occurring in l
x+z-y?x?z
x+z-y?z-x
z ?y?x
z ?x

Figure

1: An example of a confluence tree
2. By decomposition, e j c can be rewritten into fe if c is satisfiable and
not a simple system and fS is an equivalent set of simple systems for c.
3. By instantiation, e j c can be rewritten into eoe j ineqpart(c), if c is a satisfiable and
not purely inequational simple system, and oe is the most general unifier of eqpart(c).
Example 5 Consider again the set E
Critical pairs are
Other pairs yield unsatisfiable constraints or renamings of the above
pairs. Then a confluence tree rooted with the first one, as it was automatically generated by
the Saturate system [NN93], is depicted in Figure 1. Note that in a constrained rewrite step
with the associativity axiom (like the one applied to the root) the complementary equation
always has an unsatisfiable constraint (and is hence not shown). The three framed nodes
are leaves. Only the leftmost one is a tautology and hence E is not confluent. The last step
for the two rightmost framed nodes is by decomposition and instantiation. The three other
nodes without descendants become leaves after one step of decomposition and instantiation
followed in some cases by one rewrite step with associativity.
Proof plan: Our decision procedure will be based on the construction of one (arbitrary)
confluence tree for each critical pair. The main result will be that !E;?rpos is confluent
if, and only if, all these trees have only tautology leaves. For this purpose, we first show
that the trees are finite (Lemma 3), and that it is easy to decide whether a leaf
is a tautology (Lemma 4). Then, in Lemma 5 we show that every instance of the critical
pair at the root can be rewritten into some leaf, and hence !E;?rpos is confluent if all
leaves are tautologies, since then all instances of the critical pairs are joinable. Finally, for
the (harder) reverse implication (Lemma 6), from every non-tautology leaf c we can
reconstruct a substitution oe (not necessarily a solution of c) such that soe and toe are distinct
and in normal form, which contradicts confluence, since E
Lemma 3 Every confluence tree is finite.
Proof: The tree is finitely branching. Hence by K-onig's lemma it suffices to show that every
path is finite. Assume the contrary. Only a finite number of instantiation steps can be
applied on a branch since they reduce the number of variables of the descendant nodes, and
no two consecutive decomposition steps can be applied to a node. Hence there must be an
infinite branch with only constrained rewriting steps (each one followed by zero or one de-
compositions). This branch has no infinite subsequence of only complementary steps, since
the number of possible applications of equations to a finite e is finite, and no complementary
steps can be applied twice at the same position (then the non-complementary constraint becomes
unsatisfiable). Hence there must be an infinite number of non-complementary steps.
By Kruskal's theorem, since all terms in the tree are built over a finite set of symbols, on
such an infinite branch there must be a node e , such that
by construction of the tree, for all oe such that oe
c be a constrained equation where c is a purely inequational simple
system. Then is a tautology if, and only if, either c is unsatisfiable or s j t.
Proof: Clearly if c is unsatisfiable or s j t then is a tautology. For the reverse
direction, suppose c is satisfiable and s 6j t. Then c has an alien solution oe (for every
variable x, the solution xoe is headed by the new symbol succ), and it is easy to see that
such alien oe cannot unify two different terms in T Hence soe 6j toe and
not a tautology. 2
Lemma 5 Let T be a confluence tree rooted by all leaves of T are tautologies,
then all instances of are joinable.
Proof: Let soe = toe be an instance of with soe and toe in T show by
induction on the depth of the tree that soe = toe is joinable. If is already a leaf, then
it must be a tautology, and all instances of tautologies are trivially joinable. Otherwise the
children of are obtained by one of the three different steps.
By constrained rewriting with some the children are s[r']
and either an instance of one of the children or it
rewrites into one of them. In each case joinability follows by induction hypothesis (each
subtree has a smaller depth).
By decomposition, the children are g. Since c is equivalent to
a disjunction of the S i , toe is an instance of one of the children and joinability follows
by the induction hypothesis.
By instantiation, the only descendant is
is still an instance of the child and joinability follows by the induction hypothesis. 2
Lemma 6 Let (E; ? rpos
) be an ordered TRS and let T be a confluence tree for some critical
pair between two equations in E. If T has some non-tautology leaf then !E;?rpos is not
confluent.
Proof: From a non-tautology leaf c we can reconstruct a substitution oe (not
necessarily a solution of c) such that soe and s 0 oe are distinct and in normal form w.r.t.
!E;?rpos , which contradicts confluence, since E
We first build a satisfiable RPOS-closed constraint G (for graph) expressing that s and
s 0 are irreducible. Let ff be an alien solution of c. Then ff can be used to totally order the
set of all = rpos -different subterms of s and s 0 , so there is a simple system s
(the spine of G) containing all subterms of s and s 0 such that ff is a solution of the spine.
This spine is the first part of G. Now we add to G all relations r' ? s i (the ribs of G)
such that l' j s i for some i and some
Hence r' does not contain any variables that are not in the spine,
and all variables of G are in the spine of G.
Since ff is a solution of c we have r'ff - rpos l'ff (otherwise would be further
reducible and would not be a leaf). But impossible because ff is alien and
l' 6= rpos r', so we have r'ff ? rpos l'ff. Hence ff satisfies G (both the spine and the ribs).
Now we can close G under RPOS while keeping ff as a solution of G. Since the spine is
already RPOS-closed, this only has to be done for the ribs r' ? s i . It only produces new
ribs of the form t ? s j since equalities are again impossible because ff is alien. Note that
here t is not a variable since all variables are already on the spine.
We now complete the proof by showing that
a) the minimal solution oe of the spine satisfies the whole G and
are distinct and irreducible w.r.t. !E;?rpos .
a) it suffices to show toe ? rpos soe for all pairs t ? s i in G where s i is in the spine and t is
not (and hence t is not a variable). We proceed by induction on the ordering on pairs (s
whose first component is i (the situation of s i in the spine) and whose second component
is the subterm ordering on t. If s i is a variable and
toe ? rpos s i oe since t contains at least one symbol g of F with g ?F e 0. If s i is a variable
and by the induction hypothesis toe ? rpos s i\Gamma1 oe and hence
since t is headed by a symbol of F . If s i is not a variable, then t ? s i follows
by the induction hypothesis from relations that are smaller under the measure since G is
RPOS-closed.
oe satisfies the spine s are distinct. Now we prove that
they are also irreducible w.r.t. !E;?rpos . We proceed by induction on the sub-indices i
in s is succ(0) which is clearly irreducible. If
s 1 is ground then it is also irreducible since s 1 is a subterm of in the leaf. For the
induction step, if s i is a variable, then s i oe is succ(s i\Gamma1 oe) which is irreducible since s i\Gamma1 oe is
irreducible by the induction hypothesis. If s i is not a variable, it is of the form f(t
and all t j are some s k with i ? k and the t j oe are irreducible by the induction hypothesis
and hence we only have to check reducibility at the topmost position.
Suppose s i oe j l' for some We show that for all such it is the case that
is alien, all variable positions
of l must be positions in s i (otherwise some non-variable position of l would be succ). This
means that s i j lae for some ae and that ' j aeae 0 for some ae 0 . If lae = rpos rae then
and we are done. If lae 6= rpos rae then rae ? lae is a relation in G and hence raeoe ? rpos laeoe
which implies r' - rpos l'. 2
Theorem 1 The confluence of ordered TRS (E; ? rpos
Let us conclude this section by an example of application: we show how completion of
associativity and commutativity axioms yields a confluent ordered rewrite system, making
use of the above algorithm to check the confluence.
Example 6 We continue Example 5: we consider the axioms of associativity and commutativity
of the binary (lexicographic status) symbol +. These axioms cannot be handled by
standard completion as commutativity cannot be oriented without loosing termination.
The confluence tree of Example 5 shows that these two axioms alone are not confluent
w.r.t. ordered rewriting since there are leaves of the confluence tree which are not tautologies.
We may however add the equations which are leaves of the tree to the original set of axioms
without modifying the original equational theory (this is a completion process) and check
again for ordered confluence.
For instance, following Figure 1, we may add the equation x
the original set of equations. Then we have a 3 equations presentation which turns out to
be confluent w.r.t. ordered rewriting. There are more than 10 critical pairs to be considered
and hence the associated confluence trees with tautology leaves cannot be depicted here (but
they can be automatically reproduced by the Saturate system).
For this example, confluence can also be proved by means of the incomplete method given
by Martin and Nipkow in [MN90]. Their method is based on the fact that every instance
with some oe of a critical pair cp orders the variables of cp in some way, and sometimes
one can prove confluence for each ordering. For example, one cp is
and if the ordering is x
information is needed to show that both sides of cpoe rewrite into x 1 oe
(In fact, normalization in this rewrite system is simply sorting and associating to the right.)
Note that in many cases (e.g., the example given in the introduction) Martin and Nipkow's
analysis is too coarse. In general, even a case analysis on all possible orderings between all
subterms of the critical pair does not suffice.
4 Undecidability of confluence of constrained equations
If we use full constraints inheritance, then ordered completion generates constrained
equations. Hence, it would be nice to be able to decide not only the confluence of an ordered
rewrite system (E; ? rpos ), but also consider the case where E may contain constrained
equations. Here, we show that this is impossible as going from unconstrained to constrained
equations, confluence becomes undecidable.
Given a constrained equation rewrites to v using e if, and
only if, u rewrites to v using an instance soe = toe such that oe t. Confluence and
ground confluence of sets of constrained equations are defined accordingly.
Theorem 2 The problem of confluence of ordered rewriting for a finite set of constrained
equations is undecidable.
Proof: The main idea is that we can express, without any reference to s; 0 that a term
cannot contain s; 0. Then we can reduce ground confluence of a terminating rewrite system
to the confluence of ordered rewriting with respect to a set of constrained equations. On
the other hand, ground confluence is undecidable, even for terminating rewrite systems.
We reduce the ground confluence problem for an lpo-terminating string rewriting to
the confluence of ordered rewriting of a finite set of constrained equations. The former is
undecidable [KNO90].
We consider the system R u;v of [KNO90], section 5. It only involves unary function
symbols. No right hand side is reduced to a variable. This system is terminating; its
termination can be proved using an lpo extending a total precedence on a finite alphabet of
unary function symbols, plus a constant $, which is the smallest constant in the signature.
Then, we extend this signature F with 3 function symbols: m ? succ ? 0 which is at the
lower end of the precedence. Let F
Our set of equations contains R u;v plus the following additional
and a copy of some rules in R u;v
Basically, the first equation expresses what we want: the solutions for y of m(f(x)) ? y ?
f(x) are the terms succ
is the resulting set of constrained
equations, we claim that for every term s 2 T
which belongs to T
According to the three last sets of rules, the only irreducible term in T (f$; m; succ; 0g) is
0 and every term in this set reduces to 0. The first set of rules eliminates all occurrences
of succ which are above a confluent since all critical pairs
are trivially joinable.
Moreover, on T
is the reduction relation with
respect to E 0 until a normal form is reached. This can be shown by induction on the
number of rewriting steps. This implies more generally that
Now, we claim that ! ?;E is confluent iff R u;v is ground confluent, which proves undecidability

First assume that R u;v is ground confluent (on T (F)). Then E 1 is ground confluent on
only have to show the local confluence. Assume
by the above commutation property,
s 2 and by ground confluence of are joinable by
, which shows the confluence.
Conversely, assume that ! ?;E is confluent. Then ! ?;E 1
is confluent on T
term in T only be rewritten by rules in E 1 . Replacing 0 with $ we get the confluence
of R u;v on T
5 Undecidability of ground reducibility
Let us recall that a term t is ground reducible w.r.t. a rewrite system R iff all instances
of t are reducible by R. This definition extends to ordered rewriting, replacing
R with !E;? when E is a finite set of (unconstrained) equations.
Ground reducibility is decidable for arbitrary finite term rewriting systems [Pla85]. We
show here that it is undecidable for finite sets of equations:
Theorem 3 The problem:
Input: A finite set of (unconstrained) equations E, a term t, a lexicographic path ordering.
Question: Is t ground reducible w.r.t. !E;? ?
is undecidable.
Proof: We reduce the halting problem for a two-counters machine. First, let us recall this
computation model.
A (deterministic) two counter machines is a tuple (q a finite set of
states, is the set of final states, q 0 is the initial state and \Delta is a transition function
from Q to a finite set of actions A, consisting of
1. couples (1;
2. couples (2;
3. triples (1; q
4. triples (2; q
We assume that \Delta is undefined on states q 2 Q f .
A configuration of the machine consists in two non-negative integers n; m and a state q 2
Q. A move of the machine from configuration (n
possible iff there is a transition \Delta(q) = a and
1. Either
1 . (Increase counter i and move to q 0 ).
2. Or
2 . (If counter i is zero, move to q 0 without
changing the counters values).
3. Or a
counter i is positive, decrement
it and move to q 0 ).
The input of such a machine is a non-negative integer n, corresponding to the initial
configuration (n; 0; q 0 ). The machine halts on the input n iff there is a finite sequence of
transitions yielding a configuration (n
The following problem is undecidable [Min67]:
Input : a two counter machine M and a non-negative integer n
Question
a
@
@
@
@
a n k a m k 0

Figure

2: Representation of a sequence of configurations
We may assume without loss of generality that q 0 6= q 00 whenever
suffices to introduce two new states q 0
1 and q 0
In order to encode two-counters machines, we consider an alphabet
where every symbol of Q (the set of states of the machine) is a ternary symbol, a; b are
unary symbols and 0 is a constant. F is ordered according to q ? a
and the states are ordered in an arbitrary way.
We let t n be the term q 0 (a n (0); 0; x) and we are going to show that t n is not ground
reducible (w.r.t. a set of equations which is defined below) iff M halts on n. Intuitively,
we are going to design E in such a way that irreducible ground instances of t n encode
(halting) sequences of successive configurations of the machine, as depicted on figure 2.
Configurations of the machine are there (n
We divide the set of equations into 2 parts: the first part is independent of \Delta and
is designed in such a way that only sequences of possible configurations (not necessarily
consecutive ones) are kept as irreducible terms. The second set (the main one) encodes the
computations of the machine.
The first set of equations
1. q(x; For every non final state q
2. q(x; for every state q
3. q(q 0 for every states q; q 0
4. for every states q; q 0
5. a(q(x; for every state q
All these equations can actually be turned into rules from left to right. Irreducible ground
terms w.r.t. these rules are the terms a k (0) and the terms of the form:
a
@
@
a n k a m k 0
is a final state. Let S 1 be this set of ground terms. In what follows, we only
have to consider the applicability of the rules on S 1 .
The second set of equations
Equation (7) simply remove configurations which cannot be consecutive because of the
successive states.
7.
Now, we have to move the counters in the right way. The following array displays the
equations in the case where summarizes the constraints which are imposed
by each rule on a the terms of S 1 .
equation condition on
the transition
constraint on
resulting from
the irreducibility
9 q(x;
(8), when applied from left to right reduces a term q(a
when a cannot be applied from right to left
on terms of S 1 since b does not occur in any term of S 1 .
when applied from left to right reduces a term q(a
when a As before, (9) cannot be applied from
right to left on terms from S 1 . (10) forces
Putting together (8), (9) and (10), if we assume that there is a rule
is irreducible (at the root) iff
Note that the role of b is twofold: each time it appears in a right member of a rule, we
have only to consider possible applications of the equation from left to right, since b does
not occur in any term of S 1 . This forces to consider a particular orientation, which we will
not recall in what follows. Then, because b is minimal in the precedence, it plays no role in
the ordering constraint, except that it prevents some equalities.
In a similar way, (11) and (12) force the second counter to be remain constant (i.e.
rules.
Now, we have similar equations as (8-12) for transitions
equation condition on
the transition
constraint on
resulting from
the irreducibility
14 q(x;
Finally, we design similar rules for the other transitions, which are displayed in the next
array.
equation condition on
the transition
constraint on
resulting from
the irreducibility
19 q(x;
22 q(0;
26 q(x;
28 q(x;
29 q(x;
34 q(x;
For instance, if equations (18) and (22) force a transition to q 0
when the first counter is 0 and a transition to q 00 when the counter is not 0. Then the new
values of the counters are forced by equations (19), (20), (21) (in case of a transition to q 0 )
and (23-26) in case of a transition to q 00 .
In the end, we get what we were looking for: irreducible terms of S 1 are those in which
every pattern q(a corresponds to a move (n
of the machine. 2
6 Conclusion
We have shown that the behaviour of ordered rewriting is exactly the opposite of classical
term rewriting for two important problems: confluence and ground reducibility. Confluence
becomes decidable (whereas it is undecidable for term rewriting) and ground reducibility
becomes undecidable (whereas it is decidable for term rewriting). These results provide
interesting insights into the theory of ordered rewriting.
Regarding our proof of confluence of ordered TRS, in fact we show that confluence is
equivalent to ground confluence over a signature with only the new symbol succ, which is
what we finally show decidable. It is not difficult to show that for terminating TRS the
same results hold. Regarding the applications to completion, apart from what has already
been mentioned in the introduction, we also remark that our decision method works as
well if, instead of building a tree for each critical pair e j c - uj p =s, we build it for eoe j ?
starting with an empty ordering constraint. However, the initial
constraint c increases the efficiency of the procedure in practice by reducing the size of the
tree.
Several questions remain open. For instance, our results heavily rely on a particular
class of path orderings. Is there any other class of orderings that is useful in the context of
ordered TRS for which confluence is also decidable?

Acknowledgment

We thank R. Treinen for his comments on an earlier version of the paper.



--R

Proof by consistency in equational theories.
Equational inference
Orderings for equational proofs.
Solving symbolic ordering constraints.
The first-order theory of lexicographic path orderings is undecidable
Simulation of Turing machines by a left-linear rewrite rule
Orderings for term-rewriting systems
Termination of rewriting.
Rewrite systems.
More problems in rewriting.
Proving termnation with multiset order- ings
The Saturate System
On word problems in equational theories.
Automatic proofs by induction in equational theories without constructors.
Simple word problems in universal algebras.
Deduction with symbolic constraints.
Proof by consistency.
On ground confluence of term rewriting systems.
A path ordering for proving termination for term rewriting systems.
On the recursive decomposition ordering with lexicographical status and other related orderings.
Ordered rewriting and confluence.

Simple LPO constraint solving methods.
Practical results on the saturation of full first-order clauses: Experiments with the saturate system
Theorem Proving with Ordering and Equality Constrained Clauses.
Complete sets of reductions with constraints.
confluence tests and completion methods.
--TR
A path ordering for proving termination of term rewriting systems
Proof by consistency
On word problems in equational theories
Termination of rewriting
Simulation of turing machines by a left-linear rewrite rule
On ground-confluence of term rewriting systems
On the recursive decomposition ordering with lexicographical status and other related orderings
Ordered rewriting and confluence
Complete sets of reductions with constraints
Simple LPO constraint solving methods
Equational inference, canonical proofs, and proof orderings
Theorem proving with ordering and equality constrained clauses
The first-order theory of lexicographic path orderings is undecidable
Proving termination with multiset orderings
More Problems in Rewriting
Saturation of First-Order (Constrained) Clauses with the Saturate System
confluence;rewrite systems;ordered rewriting;path orderings