Relative undecidability in term rewriting.
For a hierarchy of properties of term rewriting systems related to termination we prove relative undecidability: For implications X  Y in the hierarchy the property X is undecidable for term rewriting systems satisfying Y. For most implications we obtain this result for term rewriting systems consisting of a single rewrite rule.
Introduction
In this paper we consider finite term rewriting systems (TRSs) over finite signa-
tures. For these systems termination and confluence are desired properties that
are sometimes very hard to prove. Classical results ([7, 9]) state that they are
undecidable: no decision procedure exists getting an arbitrary finite TRS as input
and giving as output whether the TRS is terminating (confluent) or not. In
this paper we don't consider only termination and confluence, but also a number
of related properties. For termination they are linearly ordered by implication:
The acronyms stand for polynomial termination (PT), !-termination (!T), total
termination (TT), simple termination (ST), non-self-embeddingness (NSE),
termination (strong normalization, SN), non-loopingness (NL), and acyclicity
(AC). We call this the termination hierarchy. One motivation for the properties
stronger than termination is that they obey better decomposition theorems. For
instance, !-termination and simple termination satisfy direct sum modularity
([12]), and total termination allows distribution elimination without linearity
conditions ([20]). Termination itself does not have these properties. The properties
weaker than termination are motivated by frequently occurring shapes of
infinite reductions. An extra implication SN ) WN (weak normalization) can
be added as an independent branch in the hierarchy. The confluence hierarchy
reads as follows:
WCR
Partially supported by the Advanced Information Technology Program (AITP) of
the Information Technology Promotion Agency (IPA).
?? Email: hansz@cs.ruu.nl.
The acronyms stand for strong confluence (SCR), confluence (or the Church-Rosser
property, CR), local confluence (or weak Church-Rosser, WCR), the normal
form property (NF), unique normal forms (UN), and unique normal forms
with respect to reduction UN ! . For weakly normalizing systems the properties
CR, NF, UN, and UN ! coincide. For terminating systems also WCR and CR
coincide and are decidable.
Undecidability of confluence is well-known ([9]), for the other properties in
the confluence hierarchy it is easy to see too. Also undecidability of most of the
properties related to termination is known ([7, 17, 1, 15, 22]), sometimes even
for single rules ([2, 15, 13]). The undecidability of !-termination is a new result;
this paper includes a sketch of the proof.
In this paper we do not only provide a general framework for proving this kind
of undecidability, for all implications in the hierarchies except one-PT ) !T-
we prove the stronger result of relative undecidability : for such an implication
we prove that the property X is undecidable for TRSs satisfying Y .
As a consequence, relative undecidability of X ) Z immediately follows from
validity of the implication Y ) Z and relative undecidability of X ) Y .
All of our proofs are given by means of Post's Correspondence Problem (PCP)
in the following way: for all of the implications X ) Y and all instances of PCP
we construct a TRS that always satisfies Y , and either satisfies X if and only
if the PCP instance admits a solution, or satisfies X if and only if the PCP
instance admits no solution. Since PCP is known to be undecidable ([18]), this
proves relative undecidability of the implication X ) Y .
The main part of the paper consists of constructions of such TRSs parametrized
by PCP instances and corresponding proofs of the above mentioned properties.
In the next section this is done for the confluence hierarchy and in Sect. 3 for
the termination hierarchy. These two sections can be read independently. The
definitions of the various properties are given in the respective sections; for further
preliminaries on term rewriting we refer to [3, 10]. In the remainder of this
section we recall the formulation of PCP:
given a finite alphabet \Gamma and a finite set , is there some
natural number n ? 0 and (ff such that
The set P is called an instance of PCP, the string ff 1
a solution for P . Matiyasevich and Senizergues [14] recently showed that PCP
is undecidable even when restricted to instances consisting of seven pairs. We
assume that \Gamma is fixed throughout the paper. (One may assume that
In our TRSs we need for every a 2 \Gamma a unary symbol a (and sometimes also
unary symbols - a, - a and ~ a). For any string
we define
2 The Confluence Hierarchy
In this section we show relative undecidability of all implications in the confluence
hierarchy as presented in the introduction. Actually we show the stronger
result that relative undecidability holds for linear TRSs.
Let us first recall the definitions of the six properties properties in the
confluence hierarchy. A TRS R is called confluent (or Church-Rosser, CR) if
equivalently, every two convertible terms have a
common reduct. A TRS R is called locally confluent (or weakly Church-Rosser,
. A TRS R is called strongly confluent (or
strongly Church-Rosser, SCR) if /R \Delta !R
R \Delta /   R . A TRS R is said to
have the normal form property (NF) if every term convertible to a normal form
reduces to that normal form, or, equivalently, every term that has a normal
form is confluent. A TRS R is said to have unique normal forms (UN) if different
normal forms are not convertible. A TRS R is said to have unique normal
forms with respect to reduction (UN ! ) if every term has at most one normal
form. The above definition of strong confluence originates from Huet [8] and is
different from the one in Dershowitz and Jouannaud [3]. They call a TRS R
strongly confluent if /R \Delta !R
R . Klop [10] calls the latter property
subcommutativity (WCR
Below we use PCP to show that for each of the five implications X ) Y in
the confluence hierarchy the property X is undecidable for TRSs satisfying the
property Y . A key observation is that an arbitrary PCP instance P admits a
solution if and only if A !
for the TRS
R
To arrive at results for linear TRSs and for some technical convenience this basic
system is replaced by
Proposition 1. A !
and only if P admits a solution.
Proof. Suppose is a solution for P . So
We have the following reduction in
Conversely, suppose that A !
Beyond the last A occurring in this
reduction sequence it is of the form
for some In the underbraced part only
rewrite rules of the form g(a(x); are used. Hence ff 1
giving a solution for P . ut
Below we make frequent use of the following result of Huet [8].
Theorem 2. Every linear strongly closed TRS is strongly confluent. ut
Here a TRS R is called strongly closed if both s
for every critical pair hs; ti of R.
2.1 NF ) UN
Proposition 3. The TRS R 1 (P ) has unique normal forms for every PCP instance
Proof. Consider the TRS R 0
Bg.
The relations $
Also the normal forms of
the two TRSs are the same. The TRS R 0
linear and strongly closed hence
(strongly) confluent by Thm. 2. This implies that R 1 (P ) has unique normal
forms. ut
Proposition 4. The following statements are equivalent:
1. The TRS R 1 (P ) has the normal form property.
2. The TRS R 1 (P ) is confluent.
3. The PCP instance P admits a solution.
Proof. Since confluence implies the normal form property, according to Prop. 1
it suffices to show that (i) A !
has the normal form
property and (ii) R 1 (P ) is confluent whenever A !
that A / g(c; c) ! B in R 1 (P ) with B a normal form, hence A !
definition of the normal form property. For (ii) we consider the confluent TRS
defined in the proof of Prop. 3. From A !
obtain that the
relations
confluent too. ut
2.2 CR ) NF
Bg.
Proposition 5. The TRS R 2 (P ) has the normal form property for every PCP
instance P .
Proof. The set of normal forms of R 2 (P ) coincides with the set of weakly normalizing
terms. Hence the normal form property is trivially satisfied. ut
Proposition 6. The TRS R 2 (P ) is confluent if and only if P admits a solution.
Proof. Since the relations !
confluent if
and only if R 1 (P ) is confluent. Hence the result follows from Prop. 4. ut
2.3 SCR ) CR
Ag.
Proposition 7. The TRS R 3 (P ) is confluent for every PCP instance P .
Proof. One easily checks that the linear TRS R 0
Ag is
strongly closed hence (strongly) confluent by Thm. 2. Since the relations !
confluent. ut
Proposition 8. The TRS R 3 (P ) is strongly confluent if and only if P admits
a solution.
Proof. In a shortest R 3 (P )-reduction sequence from A to B the rewrite rules
are not used. Hence A !
and only if A !
According to Prop. 1 we have to show that R 3 (P ) is strongly confluent if and
only if A !
In R 3 (P ) we have B / g(c; c) ! A. If R 3 (P ) is strongly
confluent then A. Since any
reduction sequence from A to C must pass through B, in both cases we have
the desired A !
Conversely, if A !
one easily checks that
R 3 (P ) is strongly closed and therefore strongly confluent by Thm. 2. ut
2.4 CR ) WCR
Cg.
Proposition 9. The TRS R 4 (P ) is locally confluent for every PCP instance P .
Proof. One easily checks that all critical pairs of R 4 (P ) are joinable. ut
Proposition 10. The TRS R 4 (P ) is confluent if and only if P admits a solution

Proof. In a shortest R 4 (P )-reduction sequence from A to B the rewrite rules
are not used. Hence A !
and only if
According to Prop. 1 we have to show that R 4 (P ) is confluent if
and only if A !
In R 4 (P ) we have A / f(c; c)
confluent then A !
which is equivalent to A !
Conversely, if
we obtain confluence by considering the linear and strongly
closed TRS R 0
Cg. ut
2.5 UN
In this subsection we assume that PCP instances are presented as ordered lists
sets. This entails no loss of generality.
be the union of R 1
ng
ng
ng
c) for all a
and ff(x;
Dg. Note that n depends on the PCP instance P ; for every ng we
have a unary function symbol i.
Proposition 11. A $
and only if P admits a solution.
Proof. Abbreviate R 1
is a solution for P .
ng. Let
We have the following conversion in R 0
A / f(c; c; c;
Conversely suppose that A and B are convertible in R 5 (P ). Consider a shortest
conversion between A and B. Since the rewrite rules in R 5
contribute to a shortest conversion between A and B, it must be of the form
t such that in the conversion between
5 -steps take place at root positions. Using the fact that
linear and non-erasing one easily concludes that there are no R 1
steps in the conversion between f(c; c; c; t) and B. Hence f(c; c; c; t) and B are
convertible in R 2
Because the TRS R 2
confluent and
B is a normal form, we obtain f(c; c; c;
it easy to show that
the term t codes a solution for P . ut
The sole purpose of the rules f(x;
z) is to avoid unwanted normal forms in R 5 (P ), whose presence would
considerably complicate the proofs of Props. 12 and 13 below.
Note that the above proposition doesn't hold for (the TRSs based
because in R 1 (P ) the terms A and B may be convertible even if P admits no
solution. For instance, we have A ! f(100(c); 10(c)) / f(0(c);
Proposition 12. The TRS R 5 (P ) has unique normal forms with respect to reduction
for every PCP instance P .
Proof. By induction on the structure of terms we can easily prove that every
term has at most one normal form. ut
Proposition 13. The TRS R 5 (P ) has unique normal forms if and only if P
does not have a solution.
Proof. According to Prop. 11 we have to show that R 5 (P ) admits two different
convertible normal forms if and only if A and B are convertible. If A and B are
convertible then so are the different normal forms B and D: B
Conversely, suppose that R 5 (P ) admits two different convertible normal forms
. Then we can write t
B, D, c or a variable, for 2. Due to the shape of the rules ff 1 is not affected
in the conversion ff 1
s 2 are different. Since no non-trivial conversion is possible starting from c or a
variable, we conclude that s 1 and s 2 are D and B, or vice versa. Hence D and
are convertible, and since A / C ! D also A and B are convertible. ut
3 The Termination Hierarchy
In this section we show relative undecidability of the last six implications in the
termination hierarchy as presented in the introduction.
Before we can define the properties in the termination hierarchy, we need
a few preliminary definitions. Throughout the following we assume that F is a
finite signature containing at least one constant. A (strict partial) order ? on the
set T (F) of ground terms is called monotonic if for all f 2 F and t;
and an
order ? on T (F) are called compatible if t ? u for all rewrite steps t !R u.
For compatibility with a monotonic order it suffices to check that loe ? roe for
all rules l ! r in R and all ground substitutions oe. An F-algebra consists of
a set A and for every f 2 F a function fA : A n ! A, where n is the arity of
f . A monotone F-algebra (A; ?) is an F-algebra A for which the underlying
set is provided with an order ? such that every algebra operation is monotonic
in all of its arguments. More precisely, for all f 2 F and a; b 2 A with a ? b
we have fA called
well-founded if ? is a well-founded order. A monotone F-algebra (A; ?) is called
simple if for all n-ary f 2 F with n - 1, a an 2 A, and
have fA (a an ) - a i . Every monotone F-algebra (A; ?) induces an order
?A on the set of terms T only if [ff](t) ? [ff](u)
for all assignments ff A. Here [ff] denotes the homomorphic extension of
ff, i.e.,
the value [ff](t) does not
depend on ff and is simply written as [t]. A TRS R and a monotone algebra
are called compatible if R and ?A are compatible. The set of rewrite
rules is the
arity of f , is denoted by Emb(F), or simply by Emb when the signature F can
be inferred from the context.
The properties in the termination hierarchy are now defined as follows. A
TRS is called terminating (or strongly normalizing, SN) if it does not allow infinite
reductions, or, equivalently, it is compatible with a well-founded monotone
algebra. A TRS R is called weakly normalizing (WN) if every term reduces to at
least one normal form. A TRS R over a signature F is called simply terminating
equivalently, it is compatible with a simple
monotone F-algebra. A TRS over a signature F is called totally terminating if
it is compatible with a monotonic well-founded total order on T (F), or, equiva-
lently, it is compatible with a well-founded monotone F-algebra (A; ?) in which
the order ? is total. A TRS over a signature F is called !-terminating if it
is compatible with a well-founded monotone F-algebra (A; ?) in which A = N
and ? is the usual order on N. A TRS over a signature F is called polynomially
terminating if it is compatible with a well-founded monotone F-algebra (A; ?)
in which A = N, ? is the usual order on N, and for which all functions fA are
polynomials. A TRS R is called looping if it admits a reduction
R C[toe]
for some term t, context C, and substitution oe. A TRS R is called cyclic if it
admits a reduction
R t for some term t. A TRS R is called self-embedding if
it admits a reduction
R
Emb t for some terms t, u.
Recent investigations of these notions include [4, 5, 16, 19, 20, 23]. Validity
of most of the implications in the termination hierarchy is direct from the defini-
tions; only TT ) ST requires some well-known argument, see e.g. [20], and NSE
theorem. None of the implications are equivalences: for
all implications X ) Y in the termination hierarchy a TRS exists satisfying Y
but not X . For infinite TRSs over infinite signatures the termination hierarchy
is more complicated: if the notion of embedding is not changed then NSE ) SN
does not hold any more, if the notions of embedding and simple termination are
adjusted as motivated in [16], then the implication TT ) ST no longer holds
([16]). In this paper however we consider only finite TRSs over finite signatures.
All TRSs needed for the termination hierarchy are modifications of two
basic TRSs parameterized by an arbitrary PCP instance P . For any string
any term t we define -
an
The two basic TRSs are
ae
ae
The system R(P ) is a minor modification of the basic system from [13]; the
system S(P ) is from [22]. The next well-known proposition is the motivation for
defining these systems.
Proposition 14. The following statements are equivalent:
1. The TRS R(P ) is terminating.
2. The TRS S(P ) is terminating.
3. The PCP instance P admits no solution.
Proof. We sketch the proof of the equivalence of 1 and 3; the equivalence proof
of 2 and 3 is similar. Suppose is a solution for P . So
We have the following
cyclic reduction in R(P
Conversely, suppose that R(P ) admits an infinite reduction. It is not difficult to
see that there exists an infinite reduction in which all steps take place at the root
position and both kinds of rewrite rules are used infinitely often. (This can be
shown formally using type elimination [20].) Any such reduction must contain a
subsequence of the form
where in the underbraced part only rewrite rules of the form F (ff(x); fi(y); z) !
are used. Hence
solution for P . ut
This proves undecidability of termination. Since the constructed infinite reduction
is always cyclic, this also proves undecidability of both loopingness and
cyclicity. The advantage of S(P ) over R(P ) is that it is length-preserving, which
means that substitutions oe.
Here jtj denotes the number of function symbols in t. Since for length-preserving
TRSs termination and simple termination coincide, this proves that both simple
termination and self-embeddingness are undecidable. The main result of [22] is
that S(P ) is totally terminating if and only if P admits no solution, proving
undecidability of total termination.
3.1
Let
ae
Proposition 15. The TRS S 1 (P ) is acyclic for every PCP instance P .
Proof. For a proof by contradiction, assume a cyclic S 1 (P )-reduction
exists. Applying rules of the form F (c; c; strictly
increases the number of g symbols, while the other kind of rules does not change
the number of g symbols. Hence in a reduction only rules of the second
kind are applied. But these rules constitute a terminating system, yielding the
desired contradiction. ut
Proposition 16. The TRS S 1 (P ) is looping if and only if P admits a solution.
Proof. If is a solution for P then we have the S 1 (P )-loop
Conversely, if S 1 (P ) is looping then it admits an infinite reduction. Erasing
all occurrences of g in any infinite S 1 (P )-reduction yields an infinite R(P )-
reduction. According to Prop. 14, P admits a solution. ut
3.2 SN ) NL
Let
Proposition 17. The TRS S 2 (P ) is non-looping for every PCP instance P .
Proof. For arbitrary terms t define inductively:
For every S 2 (P )-reduction step t ! u we have
Assume S 2 (P ) admits a loop. Choose a loop which the nesting
of F symbols in t is minimal. From /(t) - /(C[toe]) we conclude that C only
consists of g and h symbols; from we conclude that C is the
trivial context. Hence consisting only of
unary symbols. Hence D[F Due to minimality
not all steps take place inside t 1 , t 2 , t 3 . Moreover, at least one of the steps must
affect the context D for otherwise we would have F
with only applications of the rules F (ff(x); fi(y); z) ! F (x; y; z) at root positions,
but then the size of the maximal topmost part of t 1 consisting entirely of symbols
in \Gamma must exceed that of t 1 oe, which is clearly impossible. Hence we obtain a
non-empty reduction in the TRS consisting of the three rules
Considering size
and observing that the first two rules are terminating yields a contradiction. ut
Proposition 18. The TRS S 2 (P ) is terminating if and only if P admits no
solution.
Proof. Let be a solution for P . Write fl(c)). For every
we have the S 2 (P )-reduction
easily extending to an infinite reduction. Conversely, assume S 2 (P ) admits an
infinite reduction. Erasing all occurrences of f , g, and h yields an infinite R(P )-
reduction. According to Prop. 14, P admits a solution. ut
3.3 NSE ) SN
Let
Proposition 19. The TRS S 3 (P ) is terminating for every PCP instance P .
Proof. We apply semantic labelling as described in [21]. As model M we choose
two elements 0, 1, with interpretations FM (x;
right-hand sides of the rules are equal to 1 in this interpretation, M is indeed
a model for S 3 (P ). Using this model we label the symbol F by the value of its
first argument, yielding the labelled system
The main result of semantic labelling states that S 3 (P ) is terminating if and
only if S 0
terminating. The latter holds by recursive path order: choose
Proposition 20. The TRS S 3 (P ) is self-embedding if and only if P admits a
solution.
Proof. Let be a solution for P . Then we have the S 3 (P )-reduction
self-embedding. Conversely,
assume S 3 (P ) is self-embedding. Let /(t) denote the maximal nesting of F and
G symbols in a term t:
Obviously,
Emb t be such
that /(t) is minimal. We may assume that the topmost symbol of t is either
(i) F or (ii) G. Since we conclude that the root
symbols of t and u coincide. Moreover, by our minimality assumption, there is
at least one reduction step in
at the root position. First we consider
case (i). The S 3 (P )-reduction from t to u must start as
for otherwise there would
be no reduction step at a root position. Since the root symbols of t and u coincide,
it further follows that G(a(t 2
Consequently, a(t 2 ) is a solution for P . Next we consider case
(ii). Write Note that the rule G(c; c; z) !
F (h(c); c; z) is not applicable at root positions in the S 3 (P )-reduction ( ) from
t to u because for no term t 0 there is an S 3 (P )-reduction from F (h(c); c; t 0 ) to u.
Hence only rules of the form G(ff(x); are applicable at root
positions in ( ) and thus the root symbol of every term in ( ) is G. For every
reduction step G(t 0
3 ) in ( ) we have either (1) t 0
the reduction took place in t 0
1 if the reduction took
place in t 0
1 , or (3) t 0
1 is a proper subterm of t 0
the reduction
took place at the root. By assumption alternative (3) occurs at least once. Using
the well-known facts that . \Delta ! . and . \Delta . it follows that
there are no reduction steps at root
positions in u !   Emb t. Hence . Combining this with t 1 !
yields
contradicting the minimality
of /(t). We conclude that case (ii) is impossible. ut
be the TRS
ae
Proposition 21. The TRS S 4 (P ) is non-self-embedding for every PCP instance
Proof. For a term t, let ktk denote the number of F , a, and - a symbols in t. Clearly
for every reduction step t ! For a proof by contradiction,
assume a self-embedding reduction
kuk, in u !   Emb t only the rule h(x) ! x is applied. Just as in the proof of
Prop. 20 we may assume that there is at least one reduction step in
at the root position. Hence we may write ( ) as
where in the underbraced parts no steps take place at root positions. (Note that
no term of the form F (h(v 1
which is a contradiction. ut
Proposition 22. The TRS S 4 (P ) is simply terminating if and only if P admits
no solution.
Proof. According to Prop. 14 it is sufficient to show that S 4 (P ) is simply terminating
if and only if S(P ) is terminating. Suppose S(P ) is non-terminating.
non-terminating and hence
simply terminating. Conversely, assume S(P ) is terminating. Since
S(P ) is length-preserving it is simply terminating and thus admits a compatible
simple monotone algebra (A; ?). By defining hA becomes
a simple monotone algebra compatible with S 4 (P ), hence S 4 (P ) is simply ter-
minating. ut
Let
Proposition 23. The TRS S 5 (P ) is simply terminating for every PCP instance
Proof. Since S 5 (P ) is length-preserving it suffices to prove termination. We apply
semantic labelling. As model M we choose two elements 0, 1, with interpretations
right-hand sides of the rules are
equal to 0 in this interpretation, M is indeed a model for S 5 (P ). Using this
model we label the symbol F as follows: it is labelled by 1 if the interpretations
of the first and the third argument are equal, and by 0 otherwise. This yields
the labelled system
From [21] we know that S 5 (P ) is terminating if and only if S 0
The latter holds by lexicographic path order: choose
for all a 2 \Gamma and compare the arguments of F 1 from left to right. ut
Proposition 24. The TRS S 5 (P ) is totally terminating if and only if P admits
no solution.
Proof. Assume P admits no solution. According to [22] the TRS S(P ) is totally
hence admits a compatible well-founded monotone algebra (A; ?)
with ? a total order on A. We define the well-founded monotone algebra (B; -)
by
interpretations
One easily verifies that (B; -) is a well-founded monotone algebra compatible
with S 5 (P ). Since - is a total order on B, S 5 (P ) is totally terminating. Con-
versely, assume that is a solution for P . For a proof by contradiction,
suppose that S 5 (P ) is totally terminating. Then S 5 (P ) admits a compatible
monotonic well-founded total order ? on ground terms. Let t, u be arbitrary
ground terms (remember that a constant c 2 F is assumed) and a 2 \Gamma . If
otherwise ~
a(t) and
Hence for all ground terms t, u and all a
F (a(t); u; a(t); u). Using this result and the compatibility of S 5 (P ) and ? yields
where fl is written as fl 1 a, contradicting the irreflexivity of ?. ut
be the TRS? ? !
Proposition 25 [6]. The TRS S 6 (P ) is totally terminating for every PCP instance
Proof. We use the Knuth-Bendix order ([11]) where h is assigned weight 0, and
every other function symbol weight 1. For the precedence we choose h ? F ?
a ? c for all a 2 \Gamma . Note that h satisfies the constraint the Knuth-Bendix
order requires, namely that every function symbol of weight 0 is unary
and greatest in precedence. We take lexicographic status for each function sym-
left-to-right and G right-to-left. The induced Knuth-Bendix order orients
each rule from left to right. By a result of Ferreira [4, Thm. 4.47] the TRS S 6 (P )
is not only terminating, but even totally terminating. ut
Proposition 26 [6]. The TRS S 6 (P ) is !-terminating if and only if P admits
no solution.
Proof. Let be a solution for P . Then we have for all ground terms t an
S 6 (P )-reduction
For a proof by contradiction, assume that S 6 (P ) is !-terminating, with compatible
well-founded monotone algebra (A; ?) where
t). The above reduction proves !-termination of the single
rule contradicting [20, Prop. 11]. Hence S 6 (P ) is not
!-terminating.
This leaves to prove that S 6 (P ) is !-terminating if P has no solution. Here
we sketch the proof, for more details we refer to [6]. For a ground term t, let
ktk denote the number of barred and unbarred letters in t not below an F ,
G, or h symbol. An analysis of reduction patterns shows that any reduction
starting from a term of the shape h k (G(p; q; with at
least 3 kskg steps at the topmost F or G symbol, gives
rise to a solution for P . We define len F (p; q; s) to be the maximum number
of reduction steps at the topmost F or G symbol, starting from a term of the
shape h k Similarly we define len G (p; q; starting terms of
the shape h k (G(p; q; We define auxiliary functions on N+ as follows:
digits
Next an auxiliary function defined recursively as follows:
c if
h(c) otherwise
Now we define the well-founded monotone algebra (A; ?) with
GA (x;
w)). The definition of -
expresses the fact that from [t] one can reconstruct the sequence of barred and
unbarred letters of t. This information is essential to determine the estimated
maximal topmost reduction length of F and G terms. Formally, structural induction
on i shows:
for all strings i of barred and unbarred letters and for all ground terms
equivalent to the existence of a ground term t 00
such that
Structural induction on ff proves that
for Now one can show that [loe] ? [roe] for
any ground instance loe ! roe of a rule in S 6 (P ). The central step in this proof
is 156 for the first type of rules. The functions 0A , 1A ,
and hA are trivially monotonic. Observing that conc and revc are monotonic,
and that bound is weakly monotonic, in every argument, one obtains that - 0A ,
- 1A are monotonic as well. To establish that FA and GA are monotonic in all
arguments, one proves first that if P has no solution then for all x;
len F (-(x); -(y); -(z);
and
len G (-(x); -(y); -(z);
Obviously FA and GA are monotonic in their last argument. For the other argu-
ments, let x where at least one of these inequalities
is strict, and prove that log 156 b FA (x;y;z;w;u)
10u c. So indeed
we arrive at a compatible well-founded monotone algebra corresponding
to the positive integers N+ , which is order isomorphic to N, hence S 6 (P ) is !-
terminating. This completes the proof. ut
3.7 WN and CR
None of the TRSs R(P ), S(P confluent for arbitrary PCP
instances. This can be repaired by adding appropriate rewrite rules of the shape
F (x;
affecting any of our propositions. This has the additional benefit of making the
normalizing. (Note that S 3 (P ) to S 6 (P ) are
always terminating.) Consequently all of our results hold for confluent weakly
normalizing TRSs.
In particular, the union of R(P ) and the rule F (x; easily seen to
be weakly normalizing while it is terminating if and only if P admits no solution
as in Prop. 14. This proves relative undecidability of the implication SN ) WN.
Conclusions
For most of the implications in the confluence and termination hierarchies we
proved relative undecidability; only for polynomial termination the question of
(relative) undecidability is still open.
One can wonder whether similar results hold for TRSs consisting of single
rules. Undecidability of termination ([2]), and non-self-embeddingness and
simple termination ([15]) of single rules was already known. For the lower four
implications in the termination hierarchy indeed relative undecidability for single
(even orthogonal) rules can be proved; this work is still in progress.



--R

Linear Bounded Automata and Rewrite Systems: Influence of Initial Configuration on Decision Properties
Simulation of Turing Machines by a Regular Rewrite Rule
Rewrite Systems
Termination of Term Rewriting: Well-foundedness
Total Termination of Term Rewriting

On the Uniform Halting Problem for Term Rewriting Systems
Abstract Properties ans Applications to Term Rewriting Systems
Equations and Rewrite Rules: A Survey
Rewriting Systems
Simple Word Problems in Universal Algebras
Modularity of Simple Termination of Term Rewriting Systems
On Termination of One Rule Rewrite Systems
Decision Problems for Semi-Thue Systems with a Few Rules
Simple Termination is Difficult

The Undecidability of Self-Embedding for Term Rewriting Systems
A Variant of a Recursively Unsolvable Problem

Termination of Term Rewriting: Interpretation and Type Elimination
Termination of Term Rewriting by Semantic Labelling
Total Termination of Term Rewriting is Undecidable
Utrecht University
--TR
Rewrite systems
Simulation of Turing machines by a regular rewrite rule
rewriting systems
Termination of term rewriting
On termination of one rule rewrite systems
Total termination of term rewriting is undecidable
Omega-termination is undecidable for totally terminating term rewriting systems
Simple termination of rewrite systems
rewriting and all that
Relative undecidability in term rewriting
A Complex Example of a Simplifying Rewrite System
Relative Undecidability in the Termination Hierarchy of Single Rewrite Rules
Problems in Rewriting III
Relative Undecidability in Term Rewriting
Transforming Termination by Self-Labelling
Complexity Classes and Rewrite Systems with Polynomial Interpretation
Decision Problems for Semi-Thue Systems with a Few Rules

--CTR
Alfons Geser , Aart Middeldorp , Enno Ohlebusch , Hans Zantema, Relative undecidability in term rewriting: II. the confluence hierarchy, Information and Computation, v.178 n.1, p.132-148, October 10, 2002
Matiyasevich , Graud Snizergues, Decision problems for semi-Thue systems with a few rules, Theoretical Computer Science, v.330 n.1, p.145-169, 31 January 2005
undecidability;term rewriting;termination