Simple termination of context-sensitive rewriting.
Simple termination is the (often indirect) basis of most existing automatic techniques for proving termination of rule-based programs (e.g., Knuth-Bendix, polynomial, or recursive path orderings, but also DP-simple termination, etc.). An interesting framework for such programs is context-sensitive rewriting (CSR) that provides a bridge between the abstract world of general rewriting and the (more) applied setting of declarative specification and programming languages (e.g., OBJ*, CafeOBJ, ELAN, and Maude). In these languages, certain replacement restrictions can be specified in programs by the so-called strategy annotations. They may significantly improve the computational properties of programs, especially regarding their termination behaviour. Context-sensitive rewriting techniques (in particular, the methods for proving termination of CSR) have been proved useful for analyzing the properties of these programs. This entails the need to provide implementable methods for proving termination of CSR. Simplification orderings (corresponding to the notion of simple termination) which are well-known in term rewriting (and have nice properties) are, then, natural candidates for such an attempt. In this paper we introduce and investigate a corresponding notion of simple termination of CSR. We prove that our notion actually provides a unifying framework for proving termination of CSR by using standard simplification orderings via the existing (transformational) methods, and also covers CSRPO, a very recent proposal that extends the recursive path ordering (RPO) (a well-known simplification ordering) to context-sensitive terms. We also introduce polynomial orderings for dealing with (simple) termination of CSR. Finally, we also give criteria for the modularity of simple termination, for the case of disjoint unions as well as for constructor-sharing rewrite systems.
Introduction
Well-founded orderings (i.e., orderings allowing no infinite decreasing
sequence) provide a suitable basis for proving termination
in a number of programming languages and computational systems.
For instance, in term rewriting systems (TRS's) a proof of termination
can be achieved if we are able to find a (monotone and stable)
well-founded ordering > on terms (i.e., a reduction ordering) such
that l > r for every rule l ! r of the rewrite system [10, 40]. In
practice, if we want to implement a tool for proving termination of
a TRS R , we need to make this problem decidable. It is well-known
that termination of TRSs is an undecidable problem, even for TRSs
containing only one rule [7]. Hence, we can only provide effective
approaches (which yield decidable termination criteria) for certain
classes of systems. Simplification orderings are those monotone
and stable orderings > satisfying the following subterm property:
for each term t, t > s for every proper subterm s of t [8]. If termination
of a TRS R can be proved by using a simplification ordering,
then we say that R is simply terminating. Although simple termination
is also undecidable (see [33]) it covers most usual automati-
zable orderings for proving termination of rewriting (e.g., recursive
path orderings (rpo [9]), Knuth-Bendix orderings (kbo [23]), and
polynomial orderings (poly [26]), see [37] for a survey on simplification
orderings). Moreover, simple termination has interesting
properties regarding modularity: in contrast to the general case,
simple termination is modular for disjoint, constructor-sharing, and
(some classes of) hierarchical unions of TRS's [36].
obj EXAMPLE is
sorts Nat LNat .
cons : Nat LNat -> LNat [strat (1)] .
op from : Nat -> LNat [strat (1 0)] .
first : Nat LNat -> LNat [strat (1 2 0)] .
vars

Figure

1. Strategy annotations in OBJ
Context-sensitive rewriting (CSR [28]) is a restriction of rewriting
which forbids reductions on selected arguments of functions. A replacement
for each
k-ary symbol f of the signature F discriminates, for each symbol of
the signature, the argument positions on which replacements are allowed
[28]. In this way, the termination behavior of rewriting computations
can be improved, e.g., by pruning all the infinite rewrite
sequences.
In eager programming languages such as OBJ2 [14], OBJ3 [20],
CafeOBJ [15], and Maude [6], it is possible to specify the so-called
strategy annotations for controlling the execution of pro-
grams. For instance, the OBJ3 program in Figure 1 (borrowed from
[2]) specifies an explicit strategy annotation (1) for the list constructor
cons which disables replacements on the second argument (lazy
lists, see Appendix C.5 of [20]). If we collect as -( f ) the positive
indices appearing in the strategy annotation for each symbol
f in a given OBJ program 1 , we can use CSR to provide a frame-work
for analyzing and ensuring essential computational properties
such as termination, correctness and completeness (regarding
the usual semantics: head-normalization, normalization, functional
evaluation, and infinitary normalization) of programs using strategy
annotations, see [1, 2, 29, 30, 31]. In particular, termination
of (innermost) context-sensitive rewriting has been recently related
to termination of such languages [29, 30]. For instance, we can
prove termination of the OBJ3 program in Figure 1 by using the
techniques for proving termination of CSR, see Examples 5 and 7
below.
Termination of CSR and its applications has been studied in a number
of papers [5, 13, 16, 19, 22, 27, 32, 38, 39]. In most of these
papers (e.g., [13, 16, 19, 27, 38, 39]) termination of CSR is studied
in a transformational setting, namely by transforming a given
context-sensitive rewrite system (CSRS i.e., a pair (R ; -) consisting
of a TRS R and a replacement map -) into an ordinary TRS
such that termination of the latter implies termination of the former
as CSRS. Unfortunately, such transformations typically use new
symbols and rules that introduce a loss of structure and intuition,
due to the encoding of the context-sensitive control in the original
system by such new elements. They can unnecessarily complicate
the proofs of termination and make standard techniques for easing
such proofs (e.g., modular approaches) infeasible. Only recently,
some work has been devoted to the direct analysis of termination
and related properties of CSR: regarding the definition of suitable
1 As in [20], by OBJ we mean OBJ2, OBJ3, CafeOBJ, or Maude.
orderings for proving termination of CSR [5], and concerning the
modularity of termination and related properties [22]. Moreover,
the abstract properties of termination of CSR remain almost unexplored
(with the notable exception of Zantema's work [39]). In-
deed, all these lines of work appear to be promising and suggest to
further investigate direct methods for achieving simpler proofs of
termination of CSR.
In the remainder of the paper, we first introduce the necessary background
on CSR. Then we introduce and discuss simple termination
of CSR in Section 3. In Section 4 we show that in all cases where
the transformational approaches yield simple termination, the original
CSRS is simply terminating, too. Therefore, all existing transformations
for proving termination of CSR can also be used for
proving simple termination of CSRS's. Then, in Section 5 we deal
with two direct approaches for proving termination of CSR. We
show that CSRPO-termination [5] in fact yields simple termina-
tion, and we also cover simple termination proofs via polynomial
orderings. Finally, some modularity results concerning simple termination
are presented in Section 6. 2
As a motivating example for our work consider the following.
Example 1. Consider the following one-rule TRS which is contained
in the famous example of Toyama.
It is well known that this TRS is not simply terminating. However,
by forbidding reductions on the first and second argument, i.e., by
defining we obtain a 'simply terminating' behavior (re-
garding CSR) which can be easily proved by using a polynomial
ordering for CSR, see Example 10 below.
Preliminaries
2.1 Basics
Subsequently we will assume in general some familiarity with the
basic theory of term rewriting (cf. e.g. [3], [12]). Given a set A,
denotes the set of all subsets of A. Given a binary relation R
on a set A, we denote the transitive closure by R + and its reflexive
and transitive closure by R  . We say that R is terminating iff there
is no infinite sequence a 1 R a 2 R a 3   . Throughout the paper, X
denotes a countable set of variables and F denotes a signature, i.e.,
a set of function symbols ff; each having a fixed arity given
by a mapping ar N. The set of terms built from F and
is said to be linear if it has no multiple
occurrences of a single variable. Terms are viewed as labelled trees
in the usual way. Positions are represented by chains of
positive natural numbers used to address subterms of t. We denote
the empty chain by L. The set of positions of a term t is P os(t).
Positions of non-variable symbols in t are denoted as P os F (t), and
are the positions of variables. The subterm at position p of
t is denoted as tj p and t[s] p is the term t with the subterm at position
replaced by s. The symbol labelling the root of t is denoted as
root(t).
A rewrite rule is an ordered pair (l; r), written l ! r, with l; r 2
ar(l). The left-hand side (lhs)
of the rule is l and r is the right-hand side (rhs). A TRS is a pair
is a set of rewrite rules. L(R ) denotes the set
2 For the sake of readability, some proofs have been moved to
the appendix.
of lhs's of R . An instance s(l) of a lhs l of a rule is a redex. The
set of redex positions in t is P os R (t). A TRS R is left-linear if
for all l 2 L(R ), l is a linear term. Given TRSs
be the TRS
rewrites to s (at position p), written t p
(or just t ! s), if tj
substitution s. A TRS is terminating if ! is
terminating.
2.2 Context-Sensitive Rewriting
Given a signature F , a mapping - is a replacement
map (or F -map) if for all f
(or M R if determines the considered symbols),
the set of all F -maps. For the sake of simplicity, we will apply
a replacement map - 2 M F on symbols f 2 F 0 of any signature
F 0 by assuming that -( f . The inclusion
ordering  on P (N) extends to an ordering v on
means that - considers
less positions than - 0 (for reduction). We also say that - is more
restrictive than - 0 . The least upper bound (lub), t of - are
given by (-t- 0 replacement map - specifies
the argument positions which can be reduced for each symbol in
F . Accordingly, the set of -replacing positions P os - (t) of t 2
. The set of positions of replacing redexes in t is P os -
context-sensitive rewrite system (CSRS) is
a pair (R ; -), where R is a TRS and - is a replacement map. In
context-sensitive rewriting (CSR [28]), we (only) contract replacing
redexes: t -rewrites to s, written t ,! - s (or just t ,! s), if
(R ; -) is terminating if ,! - is
terminating.
3 Simple Termination of CSR
Zantema has provided an algebraic characterization of termination
of CSR [39]. As for standard rewriting, he proves that termination
of CSR is fully captured by the so-called -reduction orderings, i.e.,
well-founded, stable orderings > such that, for all
-terminating if and only if there is a -reduction ordering
> which is compatible with the rules of R , i.e., for all l ! r 2R, l >
r ([39, Proposition 1]). He also shows that -reduction ordering can
be defined by means of (well-founded) -monotone F -algebras. An
(ordered) F -algebra, is a triple (A;F A ; >), where A is a set, F A is a
set of mappings f A : A k ! A for each f 2 F where
> is a (strict) ordering on A. Given f 2 F , we say that
is -monotone if for all a;b 2 A such that a > b, we have that
f A (a
for all a
) is -monotone if for all f 2 F A , f is -monotone. A F -
algebra well-founded if > is well-founded. For
a given valuation mapping a A, the evaluation mapping
inductively defined by
and [a]( f
only if [a](t) > [a](s)
for all a A is a reduction ordering on terms for
every well-founded -monotone F -algebra (A;F A ; >) ([39, Proposition
2]). We use these notions in the following.
Given a signature F , we consider the TRS Emb(F
simply terminating if R [Emb(F ) is terminating. Regarding CSR,
the most obvious extension of this notion (a CSRS (R ; -) is simply
terminating if (R [Emb(F ); -) is terminating) is not appropriate:
Example 2. Consider the TRS R (where a is a constant):
with ?. The CSRS (R ; -) is clearly terminating; however,
(R [Emb(F ); -) (where Emb(F ) has a single rule c(x) ! x) is
not: a ,! c(a) ,! a ,!   .
Formally, in contrast to TRS's where termination of ! R implies
termination of (! R [ > st ) (with > st being the proper subterm or-
dering), this property does not hold for CSRS's any more, i.e., termination
of ,! R in general does not imply termination of (,! R
st ).
The problem is that the projections in Emb(F ) should not
make those arguments reducible which are not reducible using
the replacement map -. Therefore, we define Emb -
propose the following

DEFINITION 1. A CSRS (R ; -) is simply terminating if (R [
Obviously, if Emb - > simple termination as
in Definition 1 and the standard notion of simple termination of
TRS's coincide (as one would expect). Furthermore, any simply
terminating TRS R , viewed as CSRS (R ; -) for arbitrary
is also simply terminating (since Emb - a subset of Emb(F )
for all -). Finally, we note that if - v - 0 , then Emb - included
in Emb - 0
simple termination of (R
termination of (R ; -) in this case.
Simplification orderings are the algebraic (indeed originating)
counterpart of simple termination. A simplification ordering is
a monotonic, stable ordering on terms which additionally satisfies
the following 'subterm' property: for all t 2 T
. It is well-known that simplification orderings
are well-founded (for terms over finite signatures). Thus,
any simplification ordering is a reduction ordering, and hence it is
suitable for (trying to) prove termination of a TRS R by just comparing
the left- and right-hand sides of its rules.
The following natural generalization of simplification orderings immediately
arises.
DEFINITION 2. Let F be a signature and - 2 M F . A -
monotonic, stable ordering > is a -simplification ordering if, for
all
Unfortunately, in (sharp) contrast with the standard case, -
simplification orderings are not well-founded any more (in general).
Example 3. Consider the signature consisting of the constant a and
the unary symbol c. If we choose -(c) =?, then the binary relation
> consisting of pairs f(c n (a);c n+1 (a)) j n  0g is a -monotone
strict ordering and has the -subterm property. However, it admits
an infinite sequence
a > c(a) >    > c n (a) >
Nevertheless, Definition 2 characterizes the notion of simple termination
of Definition 1 in the following (obvious) sense.
THEOREM 1. A CSRS (R ; -) is simply terminating if and only if
there is a well-founded -simplification ordering > such that for
every rule l ! r 2 R, l > r.
PROOF. If (R ; -) is simply terminating, then the CSRS (R [
terminating and ,! + is a -
reduction ordering which clearly satisfies the -subterm property
(due to the presence of the corresponding rules in Emb -
is a -simplification ordering. Obviously, we have
On the other hand, assume that > is a well-founded -simplification
ordering such that l > r, for every rule l ! r 2 R. Since it is a -
simplification
F . Hence, > is a -reduction ordering which is compatible with
all rules from left to right. Hence,
R is simply -terminating.
Proving Simple Termination of CSR
Termination of CSRS's (R ; -) is usually proved by demonstrating
termination of a transformed TRS R -
Q obtained from R and - by
using a transformation 3 Q [13, 16, 17, 27, 38, 39]. A transformation
Q is
1. correct (regarding (simple) termination) if (simple) termination
of R -
termination of (R ; -) for all TRS
R and replacement map - 2 M R .
2. complete (regarding (simple) termination) if (simple) termination
of (R ; -) implies (simple) termination of R -
Q for all TRS
R and replacement map - 2 M R .
The simplest (and trivial) correct transformation for proving termination
of CSRS's is the identity: if R -
(R ; -) is terminating for every replacement map -.
Here, we are interested in proving simple termination of CSRS's by
using existing transformations. According to this goal in mind, we
review the main (non-trivial) correct transformations for proving
termination of CSR regarding their suitability for proving simple
termination of CSR.
4.1 The Contractive Transformation
Let F be a signature and - 2 M F be a replacement map. With the
contractive transformation [27], the non-replacing arguments of
all symbols in F are removed and a new, -contracted signature F -
is obtained (possibly reducing the arity of symbols). The function
drops the non-replacing immediate sub-terms
of a term t 2 T constructs a '-contracted' term by
joining the (also transformed) replacing arguments below the corresponding
operator of F -
L . A CSRS (R ; -), where
-contracted into R -
for a tool, MU-TERM 1.0, that implements these transformations.
ing to this definition, it is not difficult to see that R -
(R [Emb -
L . Thus, we have the following:
THEOREM 2. Let (R ; -) be a CSRS. If R -
L is simply terminating,
then (R ; -) is simply terminating.
PROOF. If R -
L is simply terminating, then R -
(R [
L is terminating. Hence, (R [Emb -
ing, i.e., (R ; -) is simply terminating.
Example 4. Consider the following CSRS which can be used to
obtain (as first(n,terms(1))) the first n terms of the series that approximates
with other k-ary symbol
f . Then,
is use an rpo based on precedence 4
terms  F :; recip;sqr; sqr  F dbl;+  F s; and first  F []:
Hence, (R ; -) is simply terminating.
The contractive transformation only works well with -conserva-
tive TRSs, i.e., satisfying that V ar - (r)  V ar - (l) for every rule
r of R [27]; otherwise, extra variables will appear in a rule of
which thus would become non-terminating. Let
ar - (r)  V ar - (l)g
That is: CoCM R contains the replacement maps - 2 CM R that
make R -conservative [32].
THEOREM 3. [32] Let R be a left-linear TRS and - 2 CoCM R . If
(R ; -) is terminating, then R -
L is terminating.
Hence, we can use the contractive transformation to fully characterize
simple termination of CSR in restricted cases.
THEOREM 4. Let be a left-linear TRS and - 2
CoCM R . Then, (R ; -) is simply terminating if and only if R -
L is
simply terminating.
4 A precedence  F is a quasi-ordering (i.e., a reflexive and transitive
relation) on the symbols of the signature F .
PROOF. The if part is Theorem 2. For the only if part, assume that
(R ; -) is simply terminating. Then, (R [Emb - terminating
and, by Theorem 3, (R [Emb -
L is terminating. Since
(R [Emb -
L
ing, hence R -
L is simply terminating.
4.2 Zantema's Transformation
Zantema's transformation marks the non-replacing arguments of
function symbols (disregarding their positions within the term)
[39]. Given
Z consists of two parts. The first part results
from R by replacing every function symbol f occurring in a left or
right-hand side with f 0 (a fresh function symbol of the same arity
as f which, then, is included in F 0 ) if it occurs in a non-replacing
argument of the function symbol directly above it. These new function
symbols are used to block further reductions at this position. In
addition, if a variable x occurs in a non-replacing position in the lhs
l of a rewrite rule l ! r, then all occurrences of x in r are replaced
by activate(x). Here, activate is a new unary function symbol which
is used to activate blocked function symbols again.
The second part of R -
Z consists of rewrite rules that are needed for
blocking and unblocking function symbols:
for every f 0 2 F 0 , together with the rule activate(x) ! x Again,
we note that, since (Emb -
and Emb -
Z ), we have that R -
(R [
Z ). Thus, we have:
THEOREM 5. Let (R ; -) be a CSRS. If R -
Z is simply terminating,
then (R ; -) is simply terminating.
Example 5. The following CSRS
with other k-ary symbol
f corresponds to the OBJ3 program in Figure 5 (we use : and []
instead of cons and nil respectively). Then,
irst 0 (x;activate(z))
rom 0 (s(x))
rom
irst 0 (x;y)
irst
is simply terminating: use the rpo which is based on precedence
sel  F activate = F first  F from; :; first'; [] and from  F
:; from';s, and gives sel the usual lexicographic status. Hence,
(R ; -) is simply terminating.
In [13], Ferreira and Ribeiro propose a variant of Zantema's transformation
which has been proved strictly more powerful than Zan-
tema's one (see [19]). Again, R -
FR has two parts. The first part
results from the first part of R -
Z by marking all function symbols
(except activate) which occur below an already marked sym-
bol. Therefore, all function symbols of non-replacing subterms are
marked. The second part consists of the rule activate(x) ! x plus
the rules:
f
f
for every f 2 F for which f 0 appears in the first part of R -
FR , where
f
f
rules
f
f
for k-ary symbols f where f 0 does not appear in the first part of
FR . However, Giesl and Middeldorp have recently shown that
these rules are not necessary for obtaining a correct transformation
[19]. Since we also have R -
(R [Emb -
FR ), this transformation is similar to Zantema's one regarding
simple termination, i.e., we have the following:
THEOREM 6. Let (R ; -) be a CSRS. If R -
FR is simply terminating,
then (R ; -) is simply terminating.
4.3 Giesl and Middeldorp's Transformations
Giesl and Middeldorp introduced a transformation that explicitly
marks the replacing positions of a term (by using a new symbol
active). Given a TRS , the TRS R -
consists of the following rules (for all
have the following.
THEOREM 7. Let (R ; -) be a CSRS. If R -
GM is simply terminating,
then (R ; -) is simply terminating.
In [16], Giesl and Middeldorp suggest a slightly different presentation
of R -
mGM of the previous transformation. In this presentation,
symbol active is not used anymore. However, we have proved that
both transformations are equivalent regarding simple termination,
GM is simply terminating if and only if R -
mGM is [32]. Thus,
Theorem 7 also holds for R -
mGM .
Giesl and Middeldorp also introduced a transformation R -
C which
is complete, i.e., every -terminating TRS is transformed into a terminating
Given a TRS and a replacement map -, the TRS R -
consists of the following rules (see [16] for a more detailed expla-
F such that
and constants c 2 F ,
THEOREM 8. Let (R ; -) be a CSRS. If R -
C is simply terminating,
then (R ; -) is simply terminating.
We conclude this section by noticing that Toyama's CSRS of Example
1 cannot be proved to be simply terminating by using any of
the previous transformations:
a ! a 0
Note that R -
L is not even
Z (and R -
FR which, in this
case coincides with R -
Z ) is not simply terminating as it contains the
non-simply terminating TRS f (a
GM is not
simply terminating:
GM
GM
GM
Finally, R -
C is not simply terminating either:
Therefore, these examples show that, in general, Theorems 2, 5,
6, 7, and 8 cannot be used in the 'only if' direction. In other
words, this means that in certain cases simple termination cannot
be proved by (the considered) transformational techniques, i.e., all
of them are incomplete regarding simple termination of CSR. No-
tably, the transformation C, which is complete for proving termination
of CSR, becomes incomplete for proving simple termination
of CSR (if we want to use simplification orderings for proving termination
of R -
C ). In the following section, we consider a different
class of methods which are not based on applying transformations
to CSRS's; in contrast, these methods are able to directly address
termination of CSRS's without transforming them.
5 Direct Approaches to SimpleTermination of
CSR
5.1 The Context-Sensitive Recursive Path Ordering
(CSRPO)
In [5], the recursive path ordering (RPO), a well-known technique
for automatically proving (simple) termination of TRSs, has been
extended to deal with termination of CSRS's. Thus, a natural question
arises: are the CSRPO-terminating CSRS's simply terminat-
ing? In this section, we positively answer this question.
The definition of CSRPO is akin to that of RPO. First, we recall the
definition of RPO. Given a precedence  F on the set of function
symbols, which is the union of a well-founded ordering  F and a
compatible and a status function stat( f
defined recursively as
follows:
1. s i  rpo t, for some
2.
3.
or
4.
where  rpo is the union of  rpo and syntactic equality.
The first idea that comes in mind to extend RPO to context-sensitive
rewriting (CSRPO) is marking the symbols which are in blocked
positions and consider them smaller than the active ones. Therefore
terms in blocked positions become smaller.
Example 6. Consider the rule
together with f1g. In order to prove that from(x) is greater
than x:from(s(x)), we take into account the replacement restriction
comparing from(x) and x:from(s(x)) where from is
a marked version of from (and we set from  F from).
However, marking all symbols in non-replacing positions can unnecessarily
weaken the resulting ordering. Thus, in addition to the
usual precedence  F on symbols, a marking map, denoted by m,
which defines for every symbol and every blocked position the set
of symbols that should be marked is also used. By F we denote
the set of marked symbols corresponding to F . Given a symbol
f in F [F and i provides the
subset of symbols in F that should be marked, i.e. m( f ; i)  F .
Marking maps are intended to mark only blocked arguments, i.e.,
seems reasonable and is also technically
necessary, see Definition 6 below). In this way, we mark only
the necessary symbols (in blocked positions).
However, if we simply apply RPO to the terms after marking the
symbols in blocked positions the resulting ordering is not stable
under substitutions. The difficult/interesting point of CSRPO is
the treatment of variables, since variables in blocked positions are
somehow smaller than variables in active positions, which is not
taken into account in RPO (see [5] for a thorough discussion of this
issue). This is achieved by appropriately marking the variables of
terms which are compared using CSRPO. Now, by X we denote
the set of labeled variables corresponding to X . The variables in X
are labeled by subsets of F , for instance x f f ;g;hg
, and we will ambiguously
use the variables of X to denote variables labeled by the
empty set.
When using the ordering, the marking map tells us whether we have
to mark the top symbol of a term every time we go to an argument
of this symbol. Thus, the marking map does not apply to the
whole term but only to the top symbol of the arguments in the recursive
calls of the definition of CSRPO. Therefore, if we have a term
access the arguments using mt(s
which represents the result of marking the top symbol (of arguments
conditional marking of top symbols
is defined by:
We
and s ng. Note that, as said, marked
symbols can only appear at the top of a term. A ground term s is in
it is in T contains no variable.
As remarked above, the treatment of variables is crucial in the definition
of CSRPO. This is because we need to ensure that CSRPO
is a stable ordering. In order to solve this problem, given a term s,
we will provide the set of labeled variables that can be considered
smaller than (or equal to) s without risk of losing stability under
substitutions. Note that we label the variables with the symbols
that should be marked in case of applying a substitution. To ensure
that some labeled variable x W is in the set of safe (wrt. stability)
labeled variables of a term s, we need x to occur in s and to be sure
that for any substitution s we have that mt(s(x);W ) is smaller than
s(s). Therefore, assuming that x occurs in s, the important point
is what happens with the function symbols heading s(s). Due to
this we analyze which function symbols are harmless as head sym-
bols. In all cases, the symbols which are included in the label W
of x; additionally, all function symbols which do not appear in the
label when we reach some occurrence of x in s are safe. Finally,
and more importantly, the symbols g that can be proved to be safe
because the head symbol of s (or recursively using some subterm
of s containing x) is greater than or equal to g (and in the latter case
they have multiset status), and g and g have the same marking.
DEFINITION 3. ([5]) Let s be a non-variable term in T
and x W a labeled variable. Then x W 2 Stable(s) if and only if x 2
The set Sa f e(s;x) for some variable x s.t. x 2V ar(s) or
some label V ) is defined as the smallest subset of F containing
1. if
2. if
(a) the union of all Sa f e(mt(s ng
and
(b) all g 2F such that
and (m(g; i) =m(g; i)) for all ar(g)g.
(c) all g 2 F such that f  F g and (m(g;
ar(g)g.
Now we can give the definition of the context-sensitive recursive
path ordering. First we give the definition of the equality relation,
induced by the equality on function symbols, that we will use.
DEFINITION 4. Given two terms in T
follows:
x
We can enlarge the equality relation by considering permutations of
arguments of symbols with multiset status.
DEFINITION 5 (CSRPO [5]). Let s;t 2 T
1.
2. or mt(s ng
3. or
4. or
5. or
t, and  S and  S
lex are respectively
the multiset and lexicographic extension of  S wrt. = S .
The precedence  F and the marking map m have to satisfy some
conditions to ensure the appropriate properties of  S for proving
termination of CSR.
DEFINITION 6. ([5]) Let  F be a precedence, - a replacement
map and m a marking map. Then ( F ; m) is a valid marking pair
if
1.
2. f  F f 8 f 2 F
3.
obj EXAMPLE-TR is
sorts Nat LNat .
ops
ops
ops nil nil' : -> LNat .
cons : Nat LNat -> LNat [strat (1)] .
op from : Nat -> LNat [strat (1 0)] .
ops sel sel' : Nat LNat -> Nat [strat (1 2 0)] .
ops first first' : Nat LNat -> LNat [strat (1 2 0)] .
vars

Figure

2. Transformed OBJ program
When valid marking maps are used, CSRPO is a reduction -
ordering and can be used for proving termination of CSRS's ([5]):
A CSRS (R ; -), where CSRPO-terminating if there
is a precedence  F on F and a valid marking map m for F such
that l  S r for all l ! r 2 R.
Example 7. Consider the CSRS (R ; -) of Example 5. Termination
of (R ; -) can also be proved using CSRPO: use the marking
and the precedence first  F
and sel  F from  F f:;s; fromg. We use the lexicographic status
for first and sel and the multiset status for all other symbols (see
Example 7 of [5]).
Example 8. Using rewriting restrictions may cause that some normal
forms of input expressions are unreachable by restricted com-
putation. For instance, the evaluation of using
the program in Figure 1 yields
obj EXAMPLE
5 We use the version 2.0 of the OBJ3 interpreter (available at
http://www.kindsoftware.com/products/opensource).
reduce in EXAMPLE : first(s(0),from(0))
rewrites: 2
result LNat: cons(0,first(0,from(s(0))))
Note that cons(0,first(0,from(s(0)))) is not a normal form. However,
is a normal form of t which cannot
be obtained by using the OBJ3 interpreter.
This can be solved by using program transformation techniques.
For instance, by applying the program transformation from OBJ
programs to OBJ programs of [2], we obtain the program of Figure
2. In contrast to the program in Figure 1, this new program can be
used to fully evaluate expressions (see [2]). Moreover, we are also
able to prove termination of this new program by using CSRPO
[4]: use the marking
and the precedence
from  F f rom;cons;s
quote  F 0';s'
quote'  F cons'; nil'
quote'  F quote
fcons  F cons
fcons
We use the lexicographic status for all symbols.
We prove that CSRPO-termination of a CSRS implies simple termination
of the CSRS.
THEOREM 9. Let (R ; -) be a CSRS. If (R ; -) is CSRPO-
terminating, then it is simply terminating.
PROOF. If (R ; -) is CSRPO-terminating, then there exists a precedence
F and a valid marking map m with l  S r for every
rule l ! r of R . We only need to prove that l  S r also holds
for every rule l ! r in Emb -
Note that we have x 2 Stable( f
if and only if f 2 Sa f e( f . Now, since
and Sa f e((x Therefore, Sa f e( f
F and f 2 Sa f e( f which means
For instance, the OBJ3 program of Figure 2 (viewed as a CSRS) is
simply terminating. On the other hand, it is not difficult to see that
termination of the CSRS of Example 1 cannot be proved using the
CSRPO: we would need to prove that the tuple ha;b;xi containing
constant symbols a;b is greater than the tuple hx;x;xi that only contains
variables. According to the definition of CSRPO, this is not
possible.
To summarize what we have done so far, we can say that our notion
of simple termination of CSR plays (almost) the same role
regarding CSR as simple termination for ordinary rewriting. We
have proved that simply terminating TRSs R -
Q prove simple termination
of (R ; -) for all the existing transformations Q. We have
also proved that CSRPO-terminating CSRS's are simply terminat-
ing. Furthermore, we have given an example of a simply terminating
CSRS which cannot be proved to be so by using the currently
developed (automatic) techniques.
Next we will consider still another method of direct termination
proofs of CSRS's.
5.2 Polynomial Orderings
A monomial in k variables over Z is a function F : Z k !Z defined
by
k for some integer a 6= 0 and some non-negative
integers . The number a is called the coefficient
of the monomial. If r then the monomial is
called a constant. A polynomial in k variables over Z is the sum of
finitely many monomials in k variables over Z.
Given a signature F and - 2 M F , let (N;F N ; >) be a F -algebra
such that, for all f 2 F , f N 2 F N is a polynomial in ar( f ) variables
satisfying (1) f N
definedness) and (2) f N is -monotone. Then, (N;F N ; >) is a well-founded
-monotone algebra and the corresponding -reduction ordering
is denoted >
poly and said to be a polynomial -ordering. The
F -algebra A is called a polynomial -interpretation for F .
In fact, given a polynomial -interpretation (N;F N ; >), the corresponding
-reduction ordering >
poly can equivalently be defined as
follows: for t; s 2 T
poly s , 8x
(i.e., we
do not need to make explicit the evaluation mapping anymore).
A positive aspect of polynomial orderings regarding other reduction
orderings is that they ease the proofs of monotonicity. In unrestricted
rewriting, monotonicity of polynomial interpretations is
normally ensured by requiring that all coeficients of all polynomials
associated to function symbols be positive (see Proposition 10
in [40] or [3, Section 5.3]). Of course, we do not want to do this,
as this would actually mean that we are using a reduction ordering
thus making it useless for proving termination of CSR in the 'inter-
esting' cases, i.e., when the TRS is not terminating. Even though
there is no simple way to ensure -monotonicity of polynomial -
orderings by constraining the shape of coeficients of monomials, we
can still use the following result (where -F=-x i means the partial
derivative of function F w.r.t. its i-th argument).
Z be a polynomial over Z. Then,
its i-th argument if -F=-x i > 0 for all
PROOF. Let x;y 2 Z be such that y > x. Polynomials (viewed as
functions on real numbers) are obviously differentiable in all their
arguments. Then, by the intermediate value theorem, there is a real
number x < z < y such that the value of -F
-x at
coincides with
by hypothesis, this is a positive number and y > x, we have
hence the conclusion

Theorem 10 does not provide a full characterization of -monotony.
For instance, the polynomial obviously monotone,
but not positive for our result can
be used to ensure (full) monotony (i.e., -monotony) of polynomials
when more standard conditions (as the aforementioned ones) do
not hold. For instance, polynomial contains
negative coefficients (which, as mentioned before, is not allowed in
the usual polynomial interpretations); the monotonicity of F can be
ensured using Theorem 10 since
N. We can use -polynomial orderings for proving termination
of CSRS's.
Example 9. Consider the CSRS (R ; -) of Example 1 and the polynomial
interpretation given by f N
and b N = 1. Obviously, f N (x;y;z) 2 N for all x;y;z 2 N. Note also
that f N is -monotone: since - f N this follows by Theorem
10. We have:
(R ; -) is terminating.
Note that the polynomial -interpretation used in Example 9 is not
monotonic in the standard case: For instance f N
f N (0;1;0) but 1 > 0, i.e., f N is not monotone in its first argument.
Similarly, f N N is not monotone
in its second argument either.
As for the unrestricted case, polynomial -orderings are well-founded
-simplification orderings if we additionally require that
THEOREM 11. Let F be a signature containing at least a constant
and (N;F N ; >) be a polynomial -interpretation
such that for all f 2 F and
poly is a well-founded -simplification ordering

Now, we have the following immediate corollary.
COROLLARY 1. Let (R ; -) be a CSRS and >
poly be a polynomial
-simplification ordering. If l > -
poly r for all rule l ! r in R , then
(R ; -) is simply terminating.
Example 10. Continuing Example 9. Note that f N in Example 9
verifies f N (x;y;z)  z z for all x;y;z 2 N. Hence, (R ; -) is
simply terminating.
6 Modularity of Simple Termination of
CSRS's
We shall now investigate to what extent the notion of simple termination
of CSRS's introduced behaves in a modular way, i.e.,
whether simple termination of two given CSRS's implies simple
termination of their union. Such a kind of modularity analysis for
general termination of CSRS's has recently been initiated in [22]
with promising first results. Let us recall a few notions and results
from [22] that we need subsequently. For simplicity, for the rest of
the paper we assume that all considered CSRS's are finite. Some of
the results (but not all) do also hold for arbitrary (infinite) systems.
DEFINITION 7. We say that a property P of CSRS's is modular for
disjoint unions if, whenever two disjoint CSRS's have property P ,
then their (disjoint) union also does. 6
This notion of modularity can be generalized in a straightforward
way to other (more general) classes of combinations of CSRS's.
6 The reverse implication usually holds, too, but for simplicity
we don't include it in the definition here.
DEFINITION 8. A rule l ! r in a CSRS (R ; -) is non-duplicating
if for every x 2 V ar(l) the multiset of replacing occurrences of x in
r is contained in the multiset of replacing occurrences of x in l, and
duplicating otherwise. (R ; -) is non-duplicating if all its rules are,
and duplicating, otherwise. A rule l ! r is said to be collapsing, if
r is a variable, and non-collapsing otherwise. A CSRS is collapsing
if it has a collapsing rule, and non-collapsing, otherwise.
Note that for CSRS's without any replacement restrictions, collaps-
ingness and non-duplication as above just yield the corresponding
well-known notions for TRS's.
Of course, in order to sensibly combine two CSRS's, one should
require some basic compatibility condition regarding the respective
replacement restrictions.
DEFINITION 9. Two CSRS's (R are said to be compatible
if they have the same replacement restrictions for shared
function symbols, i.e., if R
. The union (R ; -) of two compatible
CSRS's (R defined componentwise, i.e.,
Disjoint CSRS's are trivially compatible.
THEOREM 12. ([22]) Let (R be two disjoint, terminating
CSRS's, and let (R ; -) be their union. Then the following
hold:
(R ; -) terminates, if both (R are non-
collapsing.
(R ; -) terminates, if both (R are non-
duplicating.
(R ; -) terminates, if one of the systems is both non-collapsing
and non-duplicating.
DEFINITION 10. A TRS R is said to be terminating under free
projections, FP-terminating for short, if the disjoint union of R
and the TRS (fGg;fG(x;y) ! x;G(x;y) ! yg) is terminating. A
(R ; -) is said to be FP-terminating, if the disjoint union of R
and the CSRS ((fGg;fG(x;y)
f1;2g, is terminating.
THEOREM 13. ([22]) Let (R be two disjoint, terminating
CSRS's, such that their union (R ; -) is non-terminating.
Then one of the systems is not FP-terminating, and the other system
is collapsing.
As already shown for TRS's, this abstract and powerful structure
result has a lot of direct and indirect consequences and corollaries.
To mention only a few:
DEFINITION 11. A CSRS is non-deterministically collapsing if
there is a term that reduces to two distinct variables (in a finite
number of context-sensitive rewrite steps).
THEOREM 14. Any non-deterministically collapsing, terminating
CSRS is FP-terminating.
THEOREM 15. ([22]) Termination is modular for non-deterministically
collapsing disjoint CSRS's.
Consequently we also get the next result.
THEOREM 16. FP-termination is modular for disjoint CSRS's.
In the case of TRS's it is well-known that simple termination is
modular for disjoint unions ([25]). This can also be shown via the
TRS version of the general Theorem 13 above (cf. [21]). In par-
ticular, we note that for TRS's we have the equivalence:
simply terminating iff Now it is
obvious that if F contains a function symbols of arity at least 2, then
(R [Emb(F ); -) is non-deterministically collapsing, and, if additionally
(R [Emb(F ); -) is terminating, then (R [Emb(F ); -) is
FP-terminating. In fact, even for the case where the TRS
has only functions symbols of arity 0 and 1, simple termination of
its FP-termination as can be easily shown (e.g., by
a minimal counterexample proof). 7
With these preparations, we are ready now to tackle modularity of
simple termination for CSRS's.
THEOREM 17. Let (R ; -) with be a CSRS with
for at least one f 2F . Then simple termination of (R ; -)
implies FP-termination of (R ; -).
PROOF. Simple termination of (R ; -) means termination of (R [
By assumption, there is an f 2 F with j-( f )j
2. Thus, f rewrites to both x i and x j (using
j. But this means that (R [
non-deterministically collapsing, hence, by Theorem
14, (R [Emb - consequently, also (R ; -) are FP-
terminating.
By combining Theorem 17 and Theorem 13 we get now the following
modularity result for simple termination.
THEOREM 18. Let (R
be two disjoint CSRS's, and let (R ; -) be their disjoint
union (with
Moreover suppose that there exists an f i 2 F i with j-( f i )j  2, for
are simply terminating, then
(R ; -) is simply terminating, too.
Interestingly, for the proof of this result via Theorem
we need the technical assumption that there exists an f i 2 F i with
Currently, we do not know whether the
statement of Theorem 17 also holds without this condition. If yes,
Theorem would immediately generalize, too, and yield in general
modularity of simple termination for CSRS's.
But note that if this condition above is not satisfied, any proof of
the corresponding statement in Theorem 17 cannot work as in the
TRS case any more, since now we may have arbitrarily complicated
terms.
Finally, let us consider the case of (some) non-disjoint unions of
CSRS's.
6.1 Extension to the Constructor-Sharing
Case
Finally, let us consider the case of (some) non-disjoint unions of
CSRS's.
7 Note that in this case the terms over F have a very simple
shape, and essentially are strings.
DEFINITION 12. For a CSRS (R ; -), where R), the set of
defined (function) symbols is its set of
constructors is
be CSRS's with F 1 denoting their respective
signatures, sets of constructors, and defined function symbols.
(R are said to be (at most) constructor
sharing if D 1 \F ?. The set of shared constructors
between them is said to be
(shared) constructor lifting if root(r) 2 C , for
to be (shared) constructor lifting if it has a constructor lifting rule
said to be shared symbol lifting if
root(r) is a variable or a shared constructor. R i is said to be shared
lifting if it is collapsing or has a constructor lifting rule. R i
is layer preserving if it is not shared symbol lifting.
DEFINITION 13. Let ((F ; R;F ); -) be a CSRS and f 2F . We say
that f is fully replacing if -( f ng where n is the arity of
f .
THEOREM 19 ([22], EXTENDS [21, THEOREM 34]).
(R be two constructor sharing, compatible, terminating
CSRS's with all shared constructors fully replacing, such
that their union (R ; -) is non-terminating. Then one of the systems,
is not FP-terminating and the other system is shared symbol lifting
(i.e., collapsing or constructor lifting). 8
PROOF. We only sketch the proof idea. Analogous to [21] one considers
a minimal counterexample, i.e., a non-terminating derivation
in the union with a minimal number of alternating layers. By using
some sophisticated abstracting transfromation such a counterexample
can be translated into a counterexample that uses only one of the
two systems plus a disjoint system with only two rules of the form
(that serve for "extracting relevant information
of the former signature by need"). Note that for this construction
to work properly, we need the assumption that the shared
constructors are fully replacing.
Without the above assumption the statement of the Theorem does
not hold in general.
Example 11. Consider the CSRS's
and
with that have a shared constructor
':' which is not fully replacing. Now, both CSRS's are obviously
terminating and also FP-terminating, but their union is not due to
the cycle
length(zeros)
As for disjoint unions, from Theorem 19 above many results can
be derived. Especially regarding simple termination, we have the
following.
THEOREM 20. Let (R
constructor-sharing CSRS's with all shared constructors
fully replacing, and let (R ; -) be their union (with
8 As for TRS's, this result holds not only for finite CSRS's, but
also for finitely branching ones. But, in contrast to the disjoint
union case, it doesn't hold any more for infinitely branching sys-
tems, cf. [35] for a counterexample.
suppose that there exists an
are simply terminating, then (R ; -) is simply terminating, too.
Note that also other "symmetric" and "asymmetric" results can be
easily obtained from Theorem 19 and also from Theorem 20, anaol-
ogously to the case of disjoint unions of CSRS's (and as for TRS's).
A simple (though somewhat artificial) application example is the
following variant of Example 1.
Example 12. The two CSRS's
and
with f3g. The systems are compat-
ible, constructor-sharing and all shared constructors are (trivially)
fully replacing. Both are simply terminating (as it is not very difficult
to show; for instance, consider the polynomial interpretation
of Example 9 together with g N hence the combined
system is also simply terminating by Theorem 20. Note that
the union includes the full version of Toyama's TRS (which is non-terminating
in absence of replacement restrictions), here proved to
be simply terminating regarding CSR (for the selected replacement
map).
7 Conclusion
We have introduced a definition of simple termination of CSR and
analyzed its suitability as a unifying notion which, similar to simple
termination of rewriting, represents a class of orderings which
are well-suited for automatization. We have proven that all existing
transformations for proving termination of CSR can also be used for
proving simple termination of CSRS's (this is in contrast to other
restricted forms of termination like, e.g., innermost termination of
CSR, see [18, 22]). We have also shown that CSRPO-termination
is actually a method for proving simple termination of CSRS's. We
have analyzed the use of polynomial orderings as a tool for analyzing
termination of CSRS's. After this analysis, our
notion of simple termination appears to be a quite natural one for
the context-sensitive setting. In contrast to the context-free case
where simplification orderings (over finite signatures) are automatically
well-founded by Kruskal's Theorem, in the context-sensitive
case termination needs to be explicitly established if such orderings
are used for termination proofs. Some possible lines for doing so
have also been mentioned. Finally, we have also obtained some
first modularity results concerning simple termination of CSRS's.
These results are quite encouraging and we expect that further similar
results can be obtained, and also be extended to more general
combinations of CSRS's, e.g., to composable ([34]) and to certain
hierarchical ([24], [11]) systems.

Acknowledgements

We thank the anonymous referees for their helpful remarks.



--R

Improving on-demand strategy annotations
Correct and complete (pos- itive) strategy annotations for OBJ
rewriting and All That.
Personal communication
Recursive path orderings can be context-sensitive
Principles of Maude.
Simulation of turing machines by a regular rewrite rule.
A note on simplification orderings.
Orderings for term rewriting systems.
Termination of rewriting.
Hierarchical termination.


Principles of OBJ2.
An overview of CAFE specification environment - an algebraic approach for creating
Transformation techniques for context-sensitive rewrite systems
Transforming context-sensitive rewrite systems
Innermost termination of context-sensitive rewriting
Transformation techniques for context-sensitive rewrite systems
Introducing OBJ.
Generalized sufficient conditions for modular termination of rewriting.
Modular termination of context-sensitive rewriting
Simple word problems in universal alge- bra
Modular proofs for completeness of hierarchical term rewriting systems.
Modularity of simple termination of term rewriting systems with shared constructors.
On proving term rewriting systems are noetherian.
Termination of context-sensitive rewriting by rewriting

Termination of on-demand rewriting and termination of OBJ programs
Termination of rewriting with strategy annotations.

Termination of (canonical) context-sensitive rewriting
Simple termination is difficult.
Modular Properties of Composable Term Rewriting Systems.
On the modularity of termination of term rewriting systems.
Advanced Topics in Term Rewriting.
Simplification orderings: History of results.

of context-sensitive rewriting
In TeReSe
--TR
Termination of rewriting
Modularity of simple termination of term rewriting systems with shared constructors
Simulation of Turing machines by a regular rewrite rule
On the modularity of termination of term rewriting systems
Modular proofs for completeness of hierarchical term rewriting systems
rewriting and all that
Principles of OBJ2
Advanced topics in term rewriting
Modular termination of context-sensitive rewriting
Context-sensitive rewriting strategies
Termination of Rewriting With Strategy Annotations
Improving On-Demand Strategy Annotations
Termination of Context-Sensitive Rewriting by Rewriting
Context-Sensitive AC-Rewriting
Transforming Context-Sensitive Rewrite Systems
Termination of (Canonical) Context-Sensitive Rewriting
Termination of Context-Sensitive Rewriting
Recursive Path Orderings Can Be Context-Sensitive
Hierachical Termination
Termination of on-demand rewriting and termination of OBJ programs
An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks

--CTR
Mirtha-Lina Fernndez, Relaxing monotonicity for innermost termination, Information Processing Letters, v.93 n.3, p.117-123, 14 February 2005
Beatriz Alarcn , Ral Gutirrez , Jos Iborra , Salvador Lucas, Proving Termination of Context-Sensitive Rewriting with MU-TERM, Electronic Notes in Theoretical Computer Science (ENTCS), 188, p.105-115, July, 2007
Nao Hirokawa , Aart Middeldorp, Tyrolean termination tool: Techniques and features, Information and Computation, v.205 n.4, p.474-511, April, 2007
Jrgen Giesl , Aart Middeldorp, Transformation techniques for context-sensitive rewrite systems, Journal of Functional Programming, v.14 n.4, p.379-427, July 2004
Salvador Lucas, Proving termination of context-sensitive rewriting by transformation, Information and Computation, v.204 n.12, p.1782-1846, December, 2006
declarative programming;context-sensitive rewriting;modular program analysis and verification;automatic proofs of termination;evaluation strategies