Modular termination of context-sensitive rewriting.
Context-sensitive rewriting (CSR) has recently emerged as an interesting and flexible paradigm that provides a bridge between the abstract world of general rewriting and the (more) applied setting of declarative specification and programming languages such as OBJ*, CafeOBJ, ELAN, and Maude. A natural approach to study properties of programs written in these languages is to model them as context-sensitive rewriting systems. Here we are especially interested in proving termination of such systems, and thereby providing methods to establish termination of e.g. OBJ* programs. For proving termination of context-sensitive re-writing, there exist a few transformation methods, that reduce the problem to termination of a transformed ordinary term rewriting system (TRS). These transformations, however, have some serious drawbacks. In particular, most of them do not seem to support a modular analysis of the termination problem. In this paper we will show that a substantial part of the well-known theory of modular term rewriting can be extended to CSR, via a thorough analysis of the additional complications arising from context-sensitivity. More precisely, we will mainly concentrate on termination (properties). The obtained modularity results correspond nicely to the fact that in the above languages the modular design of programs and specifications is explicitly promoted, since it can now also be complemented by modular analysis techniques.
INTRODUCTION
Programmers usually organize the programs into components
or modules. Components of a program are easier to de-
velop, analyze, debug, and test. Eventually, the programmer
wants that interesting computational properties like termination
hold for the whole program if they could be proved for
the individual components of the program. Roughly speak-
ing, this is what being a modular property means.
Context-sensitive rewriting (CSR [26]) is a restriction of
rewriting which forbids reductions on selected arguments of
functions. In this way, the termination behavior of rewriting
computations can be improved, by pruning (all) infinite
rewrite sequences. Several methods have been developed
to formally prove termination of CSR [8, 12, 13, 25, 43,
47]. Termination of (innermost) context-sensitive rewriting
has been recently related to termination of declarative languages
such as OBJ*, CafeOBJ, and Maude [27, 28]. These
languages exhibit a strong orientation towards the modular
design of programs and specifications. In this setting,
achieving modular proofs of termination is desirable. For
instance, borrowing Appendix C.5 of [16], in Figure 1 we
show an specification of a program using lazy lists. Modules
TRUTH-VALUE and NAT introduce (sorts and) the constructors
for boolean and natural numbers. Module ID-NAT provides
an specialization of the (built-in, syntactical) identity operator
1 '===' of OBJ (see module IDENTICAL on Appendix
1 The definition of binary predicate '===' is meaningful, provided
that the rules are attempted from top to bottom. This
is quite a reasonable assumption from the (OBJ) implementation
point of view. Nevertheless, our discussion on termination
of the program does not depend on this fact in any
way.
obj TRUTH-VALUE is
obj NAT is
Nat .
obj ID-NAT is
protecting TRUTH-VALUE .
var
obj LAZYLIST is
List .
List List -> List [assoc idr: nil strat (0)] .
obj INF is
protecting LAZYLIST[Nat] .
List [strat (1 0)] .
obj TAKE is
protecting LAZYLIST[Nat] .
List -> List [strat (1 2 0)] .

Figure

1: Modular specification in OBJ3
D.3 of [16]). Module INF specifies a function inf which is
able to build an infinite object: the list of all natural numbers
following number n. Module TAKE specifies a
function take which is able to select the first n components
of a (lazy) list given as the second argument of take. Fi-
nally, module LENGTH introduces a function for computing
the length of a (finite) list. Here, the use of the strategy annotation
strat (0) for the list constructor cons (in module
LAZYLIST) is intended for both (1) allow for a real terminating
behavior of the program due to disallowing the recursive
call inf(s(n)) in the definition of inf and (2) avoiding useless
reductions on the first component of a list when computing
its length. For instance, it is possible to obtain the
value s(s(0)) of length(take(s(0),inf(s(0)))) without
any risk of nontermination 2 .
Although very simple, program of Figure 1 provides an in-
This claim can be justified by using the results in [31, 30].
teresting application of our modularity results. For instance,
whereas it is not possible to prove termination of the program
using automatic techniques for proving termination
such as Knuth-Bendix, polynomial, or recursive path orderings
(see [1, 5]), it is pretty simple to separately prove termination
of modules ID-NAT, INF, TAKE, and LENGTH. Then,
our modularity results permit a formal proof of termination
which ultimately relies on the use of purely automatic techniques
such as the recursive path ordering (see Example 9
below). Moreover, automatic tools for proving termination
such as the CiME 2.0 system 3 can also be used to prove
termination of the corresponding modules. In this way, the
user is allowed to ignore the details of termination proofs/
techniques by (only) relying on the use of software tools.
Before going into details, let us mention that there exists
already abundant literature on rewriting with context-sensitive
and other related strategies, cf. e.g. [3], [7], [9], [10],
[11], [40].
2. PRELIMINARIES
2.1 Basics
Subsequently we will assume in general some familiarity with
the basic theory of term rewriting (cf. e.g. [1], [5]). Given
a set A, P(A) denotes the set of all subsets of A. Given a
binary relation R on a set A, we denote the reflexive closure
of R by its transitive closure by R + , and its reflexive and
transitive closure by R # . An element a # A is an R-normal
form, if there exists no b such that a R b; NFR is the set of R-
normal forms. We say that b is an R-normal form of a, if b is
an R-normal form and a R # b. We say that R is terminating
i# there is no infinite sequence a1 R a2 R a3 - . We say
that R is locally confluent if, for every a, b, c # A, whenever
a R b and a R c, there exists d # A such that b R # d and
We say that R is confluent if, for every a, b, c # A,
whenever a R # b and a R # c, there exists d # A such that
d. If R is confluent and terminating, then we
say that R is complete. Throughout the paper, X denotes a
countable set of variables and F denotes a signature, i.e., a
set of function symbols {f, g, .}, each having a fixed arity
given by a mapping ar : F # N. The set of terms built
from # and X is T 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 p, q, .
are represented by chains of positive natural numbers used
to address subterms of t. Given positions p, q, we denote its
concatenation as p.q. Positions are ordered by the standard
prefix ordering #. Given a set of positions P , maximal# (P )
is the set of maximal positions of P w.r.t. If p is a
position, and Q is a set of positions,
We denote the empty chain by #. The set of positions of
a term t is Pos(t). Positions of non-variable symbols in
are denoted as PosF (t), and PosX (t) are the positions
of variables. The subterm at position p of t is denoted as
t| p and t[s] p is the term t with the subterm at position p
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 # T Var(l). The left-hand
side (lhs) of the rule is l and r is the right-hand side (rhs). A
TRS is a is a set of rewrite rules.
3 Available at http://cime.lri.fr
L(R) denotes the set of lhs's of R. An instance #(l) of a
lhs l of a rule is a redex. The set of redex positions in t is
PosR(t). A TRS R is left-linear if for all l # L(R), l is a
linear term. Given TRS's
we let R # R # be the TRS
rewrites to s (at position p), written
#R s (or just t # s), if t|
for some rule # : l # r # R, p # Pos(t) and substitution
#. A TRS is terminating if # is terminating. We say that
innermost rewrites to s, written t # i s, if t p
# s and
innermost terminating
2.2 Context-Sensitive Rewriting
Given a signature F , a mapping - : F # P(N) is a replacement
map (or F-map) if for all f # F , -(f) # {1, . , ar(f)}
[26]. Let MF (or MR if determines the considered
symbols), the set of all F-maps. For the sake of simplic-
ity, we will apply a replacement map - # MF on symbols
of any signature F # by assuming that
whenever f # F . A replacement map - specifies the argument
positions which can be reduced for each symbol in
F . Accordingly, the set of -replacing positions Pos - (t) of
. The set of positions of replacing redexes in t is
context-sensitive rewrite
system (CSRS) is a pair (R, -), where R is a TRS and -
is a replacement map. In context-sensitive rewriting (CSR
[26]), we (only) contract replacing redexes: t -rewrites to s,
#R s and p # Pos - (t).
Example 1. Consider the TRS R:
with
and 2}. The CSRS (R, -) corresponds to the
OBJ3 program of Figure 1 (with cons replaced by : here; see
[27] for further details about this correspondence). Then,
we have:
Since 2.2 # Pos - (take(s(0),0:inf(s(0)))), the redex inf(s(0))
cannot be -rewritten.
The #-normal forms are called (R, -normal forms. A
CSRS (R, -) is terminating (resp. locally confluent, conflu-
ent, complete) if #- is terminating (resp. locally confluent,
confluent, complete). Slightly abusing terminology, we shall
also sometimes say that the TRS R is -terminating if the
CSRS (R, -) is terminating. With innermost CSR, # i , we
only contract maximal positions of replacing redexes: t # i s
#R s and p # maximal# (Pos -
R (t)). We say that (R, -)
is innermost terminating if # i is terminating.
3. MODULARPROOFSOFTERMINATION
OF CSR BY TRANSFORMATION
Subsequently we assume some basic familiarity with the
usual notions, notations and terminology in modularity of
rewriting (cf. e.g. [45], [33], [17], [38, 39] 4 ). We say that
some property of CSRS's is modular (under disjoint, constructor
sharing, composable unions) if, whenever two (resp.
disjoint, constructor sharing, composable) CSRS's (R1 ,
and (R2 , -2 ) have the property, then the union (R1#R2 , -1#
property. 5 Two CSRS's (R1 , -1 ) and
are disjoint if the signatures of R1 and are dis-
joint. CSRS's (R1 , -1 ) and (R2 , -2 ) are constructor sharing
if they only share constructor symbols (see Definition 7 for
details). Finally, CSRS's (R1 , -1 ) and (R2 , -2 ) are composable
if they share defined symbols provided that they
share all of their defining rules, too (cf. [39]). Note that disjoint
TRS's are sharing constructor, and sharing constructor
TRS's are composable.
Termination of CSRS's (R, -) is usually proved by demonstrating
termination of a transformed TRS R -
obtained
from R and - by using a transformation 6 # [8, 12, 13, 25,
43, 47]. The simplest (and trivial) correct transformation for
proving termination of CSRS's is the identity: if R -
is terminating, then (R, -) is terminating for every replacement
map -.
When considering the interaction between modularity and
transformations for proving termination of a CSRS (R, -),
we can imagine two main scenarios:
. First modularize, next transform (M&T): first, given
(R, -), we look for (or have) some decomposition
for modularity (e.g., disjointness, constructor-sharing,
composability, etc. Then, we prove termination of
both S -
# and T -
# (for the same transformation #).
. First transform, next modularize (T&M): first, we transform
(R, -) into R -
we look for a suitable decomposition
such that termination of
S and T ensures termination of R -
# (hence, that of
(R, -)).
The second approach (T&M) is actually a standard problem
of (being able to achieve) a modular proof of termination of
# .
The first approach (M&T) succeeds if we have
1. (S#T
# (in this way, termination of S -
implies termination of (S # T
# which entails termination
of (S # T , -)), and
2. The transformation is 'compatible' with M, i.e.,
(possibly the
same) modularity criterion M # (in this way, termination
of S -
# and T -
would imply termination of S -
4 Further relevant works on modularity not mentioned elsewhere
include (this list is highly incomplete): [22, 23, 24],
5 Typically, the inverse implication is trivial.
6 See http://www.dsic.upv.es/users/elp/slucas/muterm
for a tool, mu-term 1.0, that implements these transformations

Indeed, the first requirement (S # T
# is satisfied
by the transformations reported in the literature, as
they have, in fact, a 'modular' definition (based on each individual
rule or symbol in the signature disregarding any
'interaction'), i.e., we actually have (S # T
# for
all these transformations. On the other hand, the second requirement
is not fulfilled by many of these transformations
(in general).
According to this, we review the main (nontrivial) correct
transformations for proving termination of CSR regarding
their suitability for modular proofs of termination.
3.1 The Contractive Transformation
Let F be a signature and - # MF be a replacement
map. With the contractive transformation [25], the non-
-replacing arguments of all symbols in F are removed and
a new, -contracted signature F -
L is obtained (possibly reducing
the arity of symbols). The function
drops the non-replacing immediate subterms of
a term t # T constructs a '-contracted' term
by joining the (also transformed) replacing arguments below
the corresponding operator of F -
L . A CSRS (R, -),
-contracted into R -
Example 2. Consider the CSRS (R, -) of Example 1.
is:
take(s,
According to this definition, it is not di#cult to see that,
given TRS's S and T , (S # T
L . It is also
clear that M(S, T ) implies M(S -
Compos}, i.e., the usual criteria for modularity are preserved
(as are) by the transformation.
3.2 Zantema's Transformation
Zantema's transformation marks the non-replacing arguments
of function symbols (disregarding their positions within
the term) [47]. Given
Z consists of two parts.
The first part results from R by replacing every function
occurring in a left or right-hand side with f # (a
fresh function symbol of the same arity as f which, then, is
included in F # ) 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 posi-
tion. 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 # F # , together with the rule activate(x) # x
The problem is that activate is a new defined symbol having
a defining rule for each new 'blocked' symbol appearing in
the signature. This means that, starting from composable
modules S and T , S -
Z and T -
Z are composable only if blocked
symbols in both S and T are the same.
Example 3. Consider the TRS's:
and
that correspond to modules INF and ID-NAT in Figure 1.
Viewed as modules, they are sharing constructor. Let - be
as in Example 1. Now we have that
and
are not composable. The problem is that S -
Z has a blocked
which is not present in T -
Z .
Note that, since the rule activate(x) # x is present in every
transformed system, composability is the best that we
can achieve after applying the transformation. For instance,
disjoint TRS's S and T lose disjointness after applying the
transformation.
In [8], Ferreira and Ribeiro propose a variant of Zantema's
transformation which has been proved strictly more powerful
than Zantema's one (see [13]). This transformation has
the same problems regarding modularity.
3.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 -
{active, mark}, R -
consists of the
following rules (for all l # r # R and f # F):
mark(f(x1 , . , xk
[12].
Unfortunately, unless R = S, this transformation will
never yield a pair of composable TRS's. Note that two di#er-
ent composable systems R and S cannot share all symbols:
if they have the same defined symbols (i.e.,
all rules must coincide too (up to renaming of variables).
Hence R #= S implies that they di#er (at least) in a constructor
symbol. However, if, e.g., f # FR - FS , then a
new rule mark(f(x1 , . , xk
is in R -
GM but not in S -
GM . Since mark is a defined
GM and S -
GM are not composable. Thus, we have proven
the following:
Theorem 1. Let (R, -) and (S, -) be di#erent composable
CSRS's. Then, R -
GM and S -
GM are not composable.
Note that, since disjoint TRS's are sharing constructor; and
sharing constructor TRS's are composable, it follows that
Giesl and Middeldorp's transformation does not provide any
possibility for a M&T-analysis of termination of CSRS's (at
least regarding the modularity criteria considered here).
In [12], Giesl and Middeldorp suggest a slightly di#erent
presentation R -
mGM of the previous transformation. In this
presentation, symbol active is not used anymore. However,
since, regarding modularity, the conflicts are due to the use
of symbol mark, this new transformation has exactly the
same problem.
Giesl and Middeldorp also introduced a transformation
which is complete, i.e., every terminating CSRS (R, -) is
transformed into a terminating TRS R -
C [12].
Given a TRS replacement map -, the
proper, top}, R -
consists of the following rules (see [12] for
a more detailed explanation): for all l # r # R, f # F such
that
active(f(x1 , . , x i , . , xk
proper(c) # ok(c)
proper(f(x1 , . , xk
Unfortunately, it is not di#cult to see that, regarding a
M&T-modular analysis of termination (and due to the rules
defining proper), we have the following.
Theorem 2. Let (R, -) and (S, -) be di#erent composable
CSRS's. Then, R -
C and S -
C are not composable.
3.4 ANon-Transformational Approach to Modularity

The previous discussion shows that only the contractive
transformation seems to be a suitable choice for performing
a modular analysis of termination of CSRS's. However,
consider again the OBJ program of Figure 1 (represented by
the CSRS (R, -) of Example 1). Note that a direct proof
of termination of (R, -) is not possible with the contractive
transformation (as shown in Example 2, R -
L is not termi-
nating). Of course, in this setting, modularity is not useful
either. On the other hand, we note that S -
Z ) in
Example 3 is not kbo-terminating (resp. rpo-terminating).
Therefore, R -
Z (which contains both S -
Z and T -
Z ) is not either
kbo- or rpo-terminating. Moreover, our attempts to
prove termination of R -
Z by using CiME failed for every
considered combination (including techniques that potentially
deal with non-simply terminating TRS's like the use
of dependency pairs together with polynomial orderings) of
proof criteria. Similarly, termination of R -
GM or R -
C cannot
be proved either using kbo or rpo (see [2] for a formal
justification of this claim). In fact, we could even prove
that they are not simply terminating (see [31]). On the
other hand, our results in this section shows that M&T or
T&M approaches are not able to provide a (simpler) proof
of termination of (R, -). Hence, termination of (R, -) remains
di#cult to (automatically) prove. The following section
shows that this situation dramatically changes using a
direct modular analysis of termination of CSR.
4. MODULAR TERMINATION OF CSR
In this main section we investigate whether, and if so, how
known modularity results from ordinary term (cf. e.g. the
early pioneering work of Toyama [45, 44] and later surveys
on the state-of-the-art about modularity in rewriting like
[33], [37], [19]) extend to context-sensitive rewriting. Since
any TRS R can be viewed as the CSRS (R, -# ), all modularity
results about TRS's cover a very specific case of CSRS's,
namely, with no replacement restrictions at all. Yet, the
interesting case, of course, arises when there are proper replacement
restrictions. In this paper we only concentrate on
termination properties. First we study how to obtain criteria
for the modularity of termination of CSRS's. Later on
we'll also consider weak termination properties, which surprisingly
may help to guarantee full termination (and con-
fluence) under some conditions. Then we generalize the setting
and consider also to some extent certain non-disjoint
combinations. As for ordinary term rewriting, a deep understanding
of the disjoint union case appears to be indispensable
for properly treating non-disjoint unions. For that
reason we mainly focus here on the case of disjoint unions.
For practical purposes it is obvious, that non-disjoint combinations
are much more interesting. Yet, the lessons learned
from (the nowadays fairly well understood) modularity analysis
in term rewriting suggest to be extremely careful with
seemingly plausible conjectures and "obvious facts".
4.1 Modularity of Termination in Disjoint
Unions
In this section, we investigate modularity of termination
of disjoint unions of CSRS's. For simplicity, as a kind of
global assumption we assume that all considered CSRS's
are finite. Most of the results (but not all) do also hold for
systems with arbitrarily many rules.
The very first positive results on modularity of termina-
tion, after the negative ones in [45, 44], were given by Rusi-
nowitch [41], who showed that the absence of collapsing rules
or the absence of duplicating rules su#ce for the termination
of the disjoint union of two terminating TRS's. Later, Middeldorp
[32] refined and generalized this criterion by showing
that it su#ces that one system doesn't have any collapsing
or duplicating rules. A careful inspection of the proofs actually
shows that these results do also for CSRS's. Even
more interestingly, there is an additional source for gener-
alization. Consider e.g. the following variant of Toyama's
basic counterexample.
Example 4. The systems
with are both terminating CSRS's, as well as
their disjoint union (the latter is a consequence of Theorem
3 below). In Toyama's original version, where the union is
non-terminating, there are no restrictions, collapsing
and duplicating.
A careful inspection of these two CSRS's and of their interaction
shows that the duplicating R-rule is not a problem
any more regarding non-termination, because the first two
occurrences of x in the rhs of the R1 -rule become blocked
after applying the rule. In particular, any further extraction
of subterms at these two positions, that is crucial for
Toyama's counterexample to work, is prohibited by
{3}. This observation naturally leads to the conjecture that
blocked/inactive variables in rhs's shouldn't count for duplication

Definition 1. A rule l # r in a CSRS (R, -) is non-
duplicating if for every x # Var(l) the multiset of replacing
occurrences of x in r is contained in the multiset of replacing
occurrences of x in l. (R, -) is non-duplicating if all its rules
are.
Of course, in order to sensibly combine two CSRS's, one
should require some basic compatibility condition regarding
the respective replacement restrictions.
Definition 2. Two CSRS's (R1 , are said
to be compatible if they have the same replacement restrictions
for shared function symbols, i.e., if
and
Disjoint CSRS's are trivially compatible.
Theorem 3. Let (R1 , be two disjoint, terminating
CSRS's, and let (R, -) be their union. Then the
following hold:
(i) (R, -) terminates, if both R1 and are non-collapsing.
(ii) (R, -) terminates, if both R1 and are non-duplica-
ting.
(iii) (R, -) terminates, if one of the systems is both non-
collapsing and non-duplicating.
Proof. We sketch the proof idea and point out the differences
to the TRS case. All three properties follow immediately
from the following observations. For any infinite
(R, -derivation D : s1 # s2 # . of minimal rank (i.e.
in any minimal counterexample) we have:
(a) There are infinitely many outer reduction steps in D.
(b) There are infinitely many inner reduction steps in D
which are destructive at level 2.
(c) There are infinitely many duplicating outer reduction
steps in D.
(a) and (b) are proved as for TRS's, cf. e.g. the minimal
counterexample approach of [17], and (c) is proved as in [38],
but with a small adaptation: Instead of the well-founded
measure there, that is shown to be decreasing, namely
(the multiset of ranks of all special
subterms of level 2), we only take
active in s], i.e., we only count special subterms at
active positions. With this modification the proof goes
through as before.
With this result, we're able to explain termination of
Example 4 without having to use any sophisticated proof
method for the combined system.
In fact, in the case of TRS's, the above syntactical conditions
(non-collapsingness and non-duplication) had turned
out to be very special cases (more precisely, consequences)
of an abstract structure theorem that characterizes minimal
counterexamples (cf. [17] 7 ). For CSRS's this powerful result
also holds. To show this, we first need another definition
(where R# S mean R # S provided that R and S are dis-
joint).
Definition 3. A TRS R is said to be terminating under
FP-terminating for short, if R#{G(x, y) #
(R, -) is said to
be FP-terminating, if (R # {G(x, y) # x, G(x, y) # y}, -),
Theorem 4 (extends [17, Theorem 7]).
Let (R1 , 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.
Proof. The quite non-trivial proof is practically the same
as for TRS's as a careful inspection of [17] reveals. All the
abstracting constructions and the resulting transformation
of a minimal counterexample in the disjoint union into a
counterexample in one of the systems extended by the free
projection rules for some fresh binary operator work as before

As already shown for TRS's, this abstract and powerful
structure result has a lot of - more or less straightforward -
direct and indirect consequences and corollaries. To mention
only two:
Corollary 1. Termination is modular for non-deterministically
collapsing 9 disjoint CSRS's.
Corollary 2. FP-termination is modular for disjoint
CSRS's.
Next we will have a look at (the modularity of) weak
termination properties.
7 For the construction in [17] the involved TRS's must be
finitely branching, which in practice is always satisfied. The
case of infinitely branching systems is handled in [38] by a
similar but more involved abstraction function, based on the
same underlying idea of extracting all relevant information
from deeper alien subterms.
8 This important property was later called CE -termination in
[38] which however isn't really telling or natural. A slightly
di#erent property in [17] had been called termination preserving
under non-deterministic collapses which is precise
but rather lengthy. Here we prefer to use FP-termination,
since it naturally expresses that a rewrite system under the
addition of the projection rules for a free (i.e., fresh) function
9 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).
4.2 Modularity of Weak Termination Proper-
ties
Weak termination properties are clearly interesting on
their own, since full termination may be unrealistic or need
not really correspond to the computational process being
modelled. Certain processes or programs are inherently non-
terminating. But still, one may wish to compute normal
forms for certain inputs (and guarantee their existence).
On the other hand, interestingly, for TRS's it has turned
out that weak termination properties can be very helpful
in order to obtain in a modular way the full termination
property under certain assumptions.
Definition 4. Let (R, -) be a CSRS. (R, -) (and #)
is said to be weakly terminating (WN), if # is weakly ter-
minating. (R, -) (and #) is weakly innermost terminating
(WIN) if the innermost context-sensitive rewrite relation # i
is weakly terminating, and (strongly) innermost terminating
(SIN) if the innermost context-sensitive rewrite relation # i
is (strongly) terminating.
For ordinary TRS's it is well-known (and not di#cult to
prove) that weak termination, weak innermost termination
and (strong) innermost termination are all modular properties
(cf. e.g. [6], [17, 18]), w.r.t. disjoint unions. Surprisingly,
this does not hold in general for CSRS's as shown by the following
counterexample.
Example 5. Consider the disjoint CSRS's
with are both innermost terminating,
in fact even terminating, but their union (R, -) is neither
terminating nor innermost terminating. We have
ever, that (R, -) is weakly innermost terminating, hence also
weakly terminating: f(a, b, G(a, b)) # i f(G(a, b), G(a, b),
the latter term is in (R, -normal form.
But even WIN and WN are not modular in general for
CSRS's as we next illustrate by a modified version of Example
5.
Example 6. Consider the disjoint CSRS's
f(b, a, x) # f(x, x, x)
with (and WN), but not
SIN. even SN. But their union (R, -)
is neither WIN nor WN.
is the (only) first innermost (R, -step issuing from
Then we can innermost reduce the first argument
of f and then the second one, or vice versa, but the
subsequent innermost step must be using one of the first
four necessarily yielding a cycle
Therefore, f(a, b, G(a, b)) doesn't have an innermost (R, -
normal form, and also no (R, -normal form at all.
A careful inspection of what goes wrong here, as well as an
inspection of the corresponding proofs for the context-free
case shows that the problem comes from (innermost) redexes
which, at some point, are blocked (inactive) because they
are below some forbidden position, but become unblocked
(active) again later on. The condition that is needed to
prevent this phenomenon is the following:
Definition 5 (conservatively blocking). A CSRS
(R, -) is said to be conservatively blocking, (CB for short),
if the following holds: For every rule l # r # R, for every
variable x occurring in l at an inactive position, all occurrences
of x in r are inactive, too. 10
Under this condition now, the properties WIN, WN, and
SIN turn out to be indeed modular for CSRS's.
Theorem 5 (modul. crit. for WIN, WN, SIN).
(a) WIN is modular for disjoint CSRS's satisfying CB.
(b) WN is modular for disjoint CSRS's satisfying CB.
(c) SIN is modular for disjoint CSRS's satisfying CB.
Proof. (a), (b) and (c) are all proved by structural induction
as in the case of TRS's, cf. e.g. [18, 19]. Condition
CB ensures that the innermost term rewrite derivation that
is constructed in these proofs in the induction step, is also
still innermost, i.e., that the proof goes through for CSRS's
as well.
4.3 Relating Innermost Termination and Ter-
mination
For TRS's a powerful criterion is known under which SIN
implies, hence is equivalent to, termination (SN). Namely,
this equivalence holds for locally confluent overlay TRS's
[18]. Via the modularity of SIN for TRS's this gave rise to
immediate new modularity results for termination (and com-
pleteness) in the case of context-free rewriting (cf. [18]). For-
tunately, the above equivalence criterion between SIN and
SN also extends to CSRS's, but not directly. The non-trivial
proof requires a careful analysis and a subtle additional assumption
(which is vacuously satisfied for TRS's). 11
Definition 6. A CSRS (R, -) is said to be a (context-
sensitive) overlay system or overlay CSRS or overlaying, if
there are no critical pairs 12
#(l1 )[#(r2 )] #(r1)# such that
# is an active non-root position in l 1 . (R, -) has left-homo-
geneous replacing variables (LHRV for short) if, for every
replacing variable x in l, all occurrences of x in both l and r
are replacing. 13
Formally: For every rule l # r # R, for every variable
x (l) #= ?, then Pos -
11 A similar claim was recently made in [14] without proof,
but it remains unclear whether this claim without our condition
LHRV is true.
are rewrite rules having no
variable in common, and # is a non-variable position in l 1
such that l 1 |# and l 2 are unifiable with most general unifier
#. Observe that by definition any overlay TRS is an overlay
CSRS, but not vice versa (when considering a CSRS (R, -)
as TRS R)!
13 Formally: For every l # r # (R, -), for every x # Var - (l)
we have Pos -
Theorem 6 (local completeness criterion).
Let (R, -) be a locally confluent overlay CSRS satisfying
LHRV and let t # T innermost terminating,
then t is terminating.
Proof. Since the proof uses essentially the same approach
and construction as the one in [18] for TRS's, we only focus
on the di#erences and problems arising due to context-
sensitivity. Basically, the proof is by minimal counterexam-
ple. Suppose, there is an infinite (R, -derivation issuing
from s. Then it is not di#cult to see that one can construct
an infinite minimal derivation of the following form (with
is non-terminating, but all proper subterms
are terminating, hence complete. Since reduction steps
strictly below p1p2 . p i in s i are only finitely often pos-
sible, eventually there must again be a root reduction step
after Now the
idea is to transform the infinite derivation D into an infinite
innermost derivation D # in such a way that the reduction
steps
are still proper (and in-
nermost) reduction steps using the same rules, whereas the
other reductions s
Technically
this was achieved for TRS's by a transformation # which
(uniquely) normalizes all complete subterms of a given term,
but doesn't touch the top parts of a given non-terminating
term. Formally: 14
such that t1 , . , tn are all maximal
terminating (hence complete) subterms of t. Now the crucial
(and subtle) issue is to make sure that #(s i
and to guarantee that the rule l i # r i applied in s #
s i+1 is still applicable to #(s # i ) at the same position p1 . p i ,
i.e., that the pattern of l i is not destroyed by #. In the
case of TRS's this was guaranteed by the overlay property
combined with completeness. In the (more general) case
of overlay CSRS's there may be (context-free) rewrite steps
in the pattern of l (strictly below the root) which would
invalidate this argument. To account for this problem, we
slightly modify the definition of # as follows:
such that t1 , . , tn are all maximal
terminating (hence complete) subterms at active positions
of t (i.e., maximal complete subterms at inactive positions
of t are left untouched!). Now we are almost done.
However, there is still a problem, namely with the "variable
parts" of the lhs l i of the rule l i # r i . In the TRS case we
did get # i (l
for CSRS's, we may have the problem, that (for non-left-
linear rules) "synchronization of normalization within variable
becomes impossible, because e.g. one occurrence
of x is active, while another one is inactive. Consequently,
the resulting transformed term # i (l i )) would not be an
instance of l i any more, and l i # r i not applicable. To avoid
this, we need the additional requirement LHRV, which also
14 Note that normalization is performed with # and not with
#.
accounts for enabling "synchronization of non-linear vari-
ables". With these adaptations and modifications the proof
finally goes through as in the TRS case. 15
Clearly, this stronger local version directly implies a global
completeness criterion as corollary.
Theorem 7 (global completeness criterion).
Let (R, -) be a locally confluent overlay CSRS satisfying
LHRV. If (R, -) is innermost terminating, then it is also
terminating (hence complete).
4.4 Modularity of Completeness
Combining previous results, we get another new criterion
for the modularity of termination of CSRS's, in fact also for
the modularity of completeness.
Theorem 8 (modularity crit. for completeness).
Let (R1 , be two disjoint, terminating CSRS's
satisfying LHRV and CB. Suppose both (R1 ,
are locally confluent and overlaying. Then their disjoint
union (R, -) is also overlaying, terminating and confluent,
hence complete.
Proof. Termination of (R i , - i ) clearly implies innermost
termination of (R 2. Theorem 5 thus yields
innermost termination of (R, -). (R, -) is an overlay CSRS,
too, by definition of this notion. Similarly, LHRV and CB
also hold for (R, -), since these syntactical properties are
purely rule-based. Now, the only assumption missing, that
we need to apply Theorem 7, is local confluence. But this is
indeed guaranteed by the critical pair lemma of [26, Theorem
4, pp. 25] for CSRS's (which in turn crucially relies
on the condition LHRV). Hence, applying Theorem 7
yields termination of (R, -), which together with local confluence
shows (via Newman's Lemma) confluence and completeness

4.5 Extensions to the Constructor-Sharing
Case
As in the case of TRS's there is justified hope that many
modularity results that hold for disjoint unions can also be
extended to more general combinations. The natural next
step are constructor sharing unions. Here we will concentrate
on the case of (at most) constructor sharing CSRS's.
The slightly more general setting of unions of composable
CSRS's is beyond the scope of the present paper and will
only be touched. But we expect our approach and analysis
also to be applicable to this setting (which, already for
TRS's, is technically rather complicated).
Definition 7. For a CSRS (R, -), where
the set of defined (function) symbols is
r # R}, its set of constructors is
Currently, we have no counterexample to the statement of
Theorem 6 without the LHRV assumption. But the current
proof doesn't seem to work without it. It remains to be
investigated whether imposing linearity restrictions would
help. Observe also, that the LHRV property plays a crucial
role in known (local and global) confluence criteria for
CSRS's. Very little is known about how to prove (local)
confluence of CSRS's without LHRV, cf. [26].
C2 , and D1 , D2 denoting their respective signatures, sets of
constructors, and defined function symbols. Then (R1 ,
and (R2 , -1 ) are said to be (at most) constructor sharing if
?. The set of shared constructors
between them is . A rule l # r # R i is said to be
(shared) constructor lifting if root(r) # C, for 2. R i is
said to be (shared) constructor lifting if it has a constructor
lifting rule (i = 1, 2). A rule l # r # R i is said to be shared
lifting if root(r) is a variable or a shared constructor.
R i is said to be shared symbol lifting if it is collapsing or
has a constructor lifting rule. R i is layer preserving if it is
not shared symbol lifting.
For TRS's the main problems in disjoint unions arise from
the additional interference between the two systems in
"mixed" terms. This interference stems from (a) non-left-
linearity, and (b) from rewrite steps that destroy the "lay-
ered structure" of mixed terms thereby potentially enabling
new rewrite steps that have not been possible before. Now,
(a) is usually not a severe problem and can be dealt with
by synchronizing steps. However, (b) is a serious issue and
the main source of (almost) all problems. In disjoint unions
such "destructive" steps are only possible via collapsing rules
(cf. e.g. Theorems 3, 4). In constructor sharing unions, interference
and fusion of previously separated layers is also
possible via (shared) constructor lifting rules. The basic example
in term rewriting is the following variant of Toyama's
counterexample.
Example 7. The two constructor sharing TRS's
are terminating, but their union admits a cycle
Observe how the application of the two constructor lifting
rules enables the application of the -rule previously not
possible.
Taking this additional source of interference into account,
namely, besides collapsing rules also constructor lifting rules,
some results for disjoint unions also extend to the constructor
sharing case.
First let us look at an illuminating example.
Example 8. Consider the two constructor sharing CSRS's
with shared constructor c and
Both systems are obviously terminating, but their union admits
a cycle
Observe that the CSRS (R1 , -) is not shared symbol lifting
and non-duplicating as TRS but duplicating (as CSRS),
whereas (R2 , -) is constructor lifting and non-duplicating
(as CSRS).
For the next general result we need an additional definition

Definition 8. Let ((F , R, F), -) be a CSRS and f # F.
We say that f is fully replacing if
n is the arity of f .
Now we are ready to generalize Theorem 4 to the constructor
sharing case (cf. [17, Theorem 34]).
Theorem 9 (Theorem 4 extended).
Let (R1 , be two constructor sharing, compat-
ible, 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).
Proof. We just sketch the proof idea. The proof is very
similar to the one in the TRS case, i.e., as for Theorem 34
in [17]. Given a minimal counterexample in the union, i.e.,
an infinite (ground) derivation D of minimal rank, let's say,
with the top layer from F1 , an abstracting transformation
# is defined, which abstracts from the concrete syntactical
from of inner parts of the terms but retains all relevant
syntactical F1-information that may eventually pop up and
fuse with the topmost F1 -layer. The only di#erence is that in
the recursive definition of this abstraction function # we use
#R instead of # as in [17]. The abstracted F1-information
is collected and brought into a unique syntactical form via a
fresh binary function symbol G with
with a fresh constant A). With these preparations it is not
very di#cult to show:
(a) D contains infinitely many outer reduction steps.
(b) Any outer step in D translates into a corresponding
outer ((R1 , -1)-)step in #(D) (using the same rule at
the same position).
(c) D contains infinitely many inner reduction steps that
are destructive at level 2 (hence must be (R2 , -2 )-
steps).
(d) Any inner step in D which is destructive at level 2
translates into a (non-empty) sequence of rewrite steps
in #(D) using (only) the projection rules for G, i.e.,
Any inner step which is not destructive at level 2 (hence
it can be an (R1 , -1 )- or an (R2 , -2)-step) translates
into a (possibly empty) sequence of rewrite steps in
#(D) using (R1 # {G(x, y) # x, G(x, y) # y}, -).
Observe that without the assumption that all shared constructors
are fully replacing, the above properties (b), (d)
and (e) need not hold any more in general. 17 Now, (c) implies
that (R2 , -2 ) is shared lifting. And from (a), (b), (d)
and (e) we obtain the infinite (R1 #{G(x, y) # x, G(x, y) #
-derivation #(D) which means that (R1 , -1 ) is not FP-
terminating.
Note that, as in the case of 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 systems, cf. [38] for a corresponding
counterexample of infinitely branching constructor
sharing TRS's.
Roughly speaking, this failure is due to the fact that, for
non-fully replacing constructors, context-sensitivity makes
the abstracting transformation interfere with reduction
steps in a "non-monotonic" way.
Without the above assumption the statement of the Theorem
does not hold in general as is witnesses by Example
above. Clearly, both CSRS's R1 and R2 in this example
are FP-terminating, but their union is not even terminating.
Note that the (only) shared constructor c here is not fully
replacing.
Next let us consider the extension of the syntactical modularity
criteria of Theorem 3 to constructor sharing unions.
Theorem 10. Let (R1 , be two constructor
sharing, compatible, terminating CSRS's, and let (R, -) be
their union. Then the following hold:
(i) (R, -) terminates, if both R1 and are layer-pre-
serving.
(ii) (R, -) terminates, if both R1 and are non-duplica-
ting.
(iii) (R, -) terminates, if one of the systems is both layer-
preserving and non-duplicating.
Proof. The proof is essentially analogous to the one of
Theorem 3 one for disjoint CSRS's.
Example 9. Now we are ready to give a modular proof
of termination of the OBJ program of Figure 1: consider
the CSRS (R, -) of Example 1 as the (constructor sharing,
compatible) union of:
and
Note that S is rpo-terminating (use the precedence === >
true, false). Hence, (S, -) is terminating. On the other hand:
take(s,
is rpo-terminating too: use precedence take > nil, :; inf > :,
and length > 0, s. Hence, (T , -) is terminating. Also, polynomial
termination
can easily be proved by
using the CiME 2.0 system. Since (S, -) is layer-preserving
and non-duplicating, by Theorem 10 we conclude termination
of (R, -). According to [27], this implies termination of
the OBJ program.
Example 10. Consider the two constructor sharing TRS's
c # a
i.e., termination by using some well-founded polynomial
ordering
together with In [12] Giesl and Middeldorp show
that termination of (R1 # cannot be proved by any
existing transformation (but the complete one, see Section
3.3). However, no proof of termination of (R1 #
been reported in the literature yet. Now, we are able to give
a very simple (modular) proof: note that R1 and are ter-
minating, hence (R1 , -) and (R2 , -) are terminating. Since
(R1 , -) is layer-preserving and non-duplicating, termination
of (R1 # Theorem 10.
As for TRS's, Theorem 9 has a whole number of direct or
indirect corollaries stating more concrete modularity criteria
for termination in the case of constructor sharing unions.
We will not detail this here, but rather focus on some other
results along the lines of Sections 4.2 and 4.4.
Of course, the negative counterexamples of Section 4.2,
Examples 5 and 6, immediately extend to the constructor
sharing case, too. Yet, the positive results regarding
modularity of the "weak termination properties" WIN, WN,
and SIN extend from disjoint CSRS's to constructor sharing
ones.
Theorem 11 (Theorem 5 extended).
(a) WIN is preserved under unions of constructor sharing
CSRS's satisfying CB.
(b) WN is preserved under unions of constructor sharing
CSRS's satisfying CB.
(c) SIN is preserved under unions of constructor sharing
CSRS's satisfying CB.
Proof. The proofs of (a), (b) and (c) are essentially the
same as for Theorem 5 above, namely by structural induction
and case analysis. The only di#erence now is that in
the case of a shared constructor at the root, we may have
both top-white and top-black principal subterms below (in
the common modularity terminology, cf. e.g. [17]) such a
constructor symbol at the root. But this doesn't disturb the
reasoning in the proofs. Again condition CB ensures that
the innermost term rewrite derivation that is constructed in
these proofs in the induction step, is also still innermost,
i.e., that the proofs go through for CSRS's as well.
Similarly we obtain
Theorem 12 (Theorem 8 extended).
Let (R1 , be two constructor sharing, compati-
ble, terminating CSRS's satisfying LHRV and CB. Suppose
both (R1 , -1) and (R2 , -2 ) are locally confluent and overlay-
ing. Then their (constructor sharing) union (R, -) is also
overlaying, terminating and confluent, hence complete.
Proof. Analogous to the proof of Theorem 8 using Theorem
11 instead of Theorem 5.
5. RELATED WORK
As far as we know our results are the first to deal with
the analysis of modular properties of CSRS's. Some properties
of CSRS's have by now been fairly well investigated,
especially regarding termination proof techniques, but also
concerning other properties and verification criteria (cf. e.g.
[25, 26, 28, 27, 29, 31, 30], [47], [8], [12, 13, 15, 14],
Recent interesting developments include in particular the
approach of Giesl & Middeldorp for proving innermost termination
of CSRS's via transformations to ordinary TRS's
along the lines of [12], as well as the rpo-style approach of
[2] for directly proving termination of CSRS's without any
intermediate transformations and without recurring to ordinary
TRS's. A comparison of our results and approach with
the latter ones mentioned remains to be done.
5.1 Perspectives and Open Problems
In this paper we have started to systematically investigate
modular aspects of context-sensitive rewriting. We have almost
exclusively focussed on termination (properties). Of
course, this is only the beginning of more research to be
done. We have shown that, taking the additional complications
arising from context-sensitivity carefully into account,
it is indeed possible to extend a couple of fundamental modularity
results for TRS's to the more general case of CSRS's.
In this sense, the obtained results are quite encouraging.
They also seem to indicate that a considerable amount of
the structural knowledge about modularity in term rewriting
can be taken over to context-sensitive rewriting. However,
it has also turned that there are a couple of new phenomena
and ugly properties that crucially interfere with the traditional
approach for TRS's. In particular, it turns out that
the syntactical restrictions CB and LHRV of the replacement
- play a crucial role. These conditions are certainly
a considerable restriction in practice, and hence should also
be more thoroughly investigated. Apart from the disjoint
union case, we have also shown that the obtained results for
disjoint unions extend nicely to the case of shared construc-
tors. On the other hand, of course, modularity results do
not always help. A simple example is the following.
Example 11. The two CSRS's
with are constructor sharing and both termi-
nating, and their union R is terminating, too! However,
none of our modularity results is applicable here as the
reader is invited to verify. Intuitively, the reason for this
non-applicability of (generic) modularity results lies in the
fact, that any termination proof of R must somehow exploit
internal (termination) arguments about . A bit more
precisely, the decrease in the first argument of the second
-rule "lexicographically dominates" what happens in the
second argument. To make this more explicit, consider also
the following, semantically meaningless, variant of
with - as before. Clearly, R3 is also terminating. However,
now the union of the constructor sharing CSRS's R1 and R3
becomes non-terminating: nth(s(x),
. Here the failure
of our modularity criteria becomes comprehensible. Namely,
and do have the same syntactical modularity structure
as combined with R3 . And in the former case we got
termination, in the latter one non-termination. Thus it is
unrealistic to expect the applicability of a general modularity
result in this particular example. Yet, if we now consider
still another system
with -(:) as above and consider the union of the terminating
composable CSRS's then we might
wish to conclude termination of the combination by some
modularity criterion. This does not seem to be hopeless.
In other words, we expect that many results that hold for
constructor sharing CSRS's also extend to unions of composable
CSRS's which, additionally, may share defined function
symbols provided they then share all their defining rules, too
(cf. [39]), and to some extent also for hierarchical combinations
of CSRS's (cf. e.g. [21], [4]). However, since modularity
is known to be a very error-prone domain, any concrete such
claim has to be carefully verified. This will be the subject
of future work.
6. CONCLUSION
We have presented some first steps of a thorough modularity
analysis in context-sensitive rewriting. In the paper we
have mainly focussed on termination properties. The results
obtained by now are very encouraging. But there remains a
lot of work to be done.
7.



--R

rewriting and All That.
Recursive path orderings can be context-sensitive
Principles of Maude.
Hierarchical termination.


rewriting with operator evaluation strategies.

Termination of rewriting with local strategies.
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 su
Abstract relations between restricted termination and confluence properties of rewrite systems.
Termination and Confluence Properties of Structured Rewrite Systems.
Modularity of confluence: A simplified proof.
Modular proofs for completeness of hierarchical term rewriting systems.
Modularity of simple termination of term rewriting systems with shared constructors.
Termination of combination of composable term rewriting systems.
Modularity in noncopying term rewriting.
Termination of context-sensitive rewriting by rewriting

Termination of on-demand rewriting and termination of OBJ programs
Termination of rewriting with strategy annotations.
Transfinite rewriting semantics for term rewriting systems.

Termination of (canonical) context-sensitive rewriting

Modular Properties of Term Rewriting Systems.
Modular properties of conditional term rewriting systems.
Completeness of combinations of conditional constructor systems.
Completeness of combinations of constructor systems.
Modular Properties of Composable Term Rewriting Systems.
On the modularity of termination of term rewriting systems.
Modular properties of composable term rewriting systems.

On termination of the direct sum of term rewriting systems.


Counterexamples to termination for the direct sum of term rewriting systems.
On the Church-Rosser property for the direct sum of term rewriting systems
Termination for direct sums of left-linear complete term rewriting systems
Termination of context-sensitive rewriting
--TR
On the Church-Rosser property for the direct sum of term rewriting systems
Counterexamples to termination for the direct sum of term rewriting systems
On termination of the direct sum of term-rewriting systems
A sufficient condition for the termination of the direct sum of term rewriting systems
Modularity of simple termination of term rewriting systems with shared constructors
Completeness of combinations of constructor systems
Modularity of confluence
Modular properties of conditional term rewriting systems
Completeness of combinations of conditional constructor systems
On the modularity of termination of term rewriting systems
Modular proofs for completeness of hierarchical term rewriting systems
Modularity in noncopying term rewriting
Modular termination of <italic>r</italic>-consistent and left-linear term rewriting systems
Modular properties of composable term rewriting systems
Termination for direct sums of left-linear complete term rewriting systems
rewriting and all that
Principles of OBJ2
Context-sensitive rewriting strategies
Termination of Rewriting With Strategy Annotations
Termination of Context-Sensitive Rewriting by Rewriting
Context-Sensitive AC-Rewriting
Transforming Context-Sensitive Rewrite Systems
Transfinite Rewriting Semantics for Term Rewriting 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
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
Bernhard Gramlich , Salvador Lucas, Simple termination of context-sensitive rewriting, Proceedings of the 2002 ACM SIGPLAN workshop on Rule-based programming, p.29-42, October 05, 2002, Pittsburgh, Pennsylvania
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, Context-sensitive rewriting strategies, Information and Computation, v.178 n.1, p.294-343, October 10, 2002
Salvador Lucas, Proving termination of context-sensitive rewriting by transformation, Information and Computation, v.204 n.12, p.1782-1846, December, 2006
modular proofs of termination;declarative programming;context-sensitive rewriting;program verification;evaluation strategies;modular analysis and construction of programs