JAIST Repository
https://dspace.jaist.ac.jp/

Title

Automated Complexity Analysis Based on Context‑
Sensitive Rewriting

Author(s)Hirokawa, Nao; Moser, Georg

Citation

Lecture Notes in Computer Science, 8560: 257‑271

Issue Date

2014‑07

Type

Journal Article

Text version

author

URL

http://hdl.handle.net/10119/12801

RightsThis is the author‑created version of Springer,
Nao Hirokawa and Georg Moser, Lecture Notes in
Computer Science, 8560, 2014, 257‑271. The
original publication is available atwww.springerlink.com,
http://dx.doi.org/10.1007/978‑3‑319‑08918‑8̲18

Description

Joint International Conference, RTA‑TLCA 2014,
Held as Part of the Vienna Summer of Logic, VSL
2014, Vienna, Austria, July 14‑17, 2014

Japan Advanced Institute of Science and Technology

Automated Complexity Analysis Based onContext-Sensitive Rewriting?
Nao Hirokawa1 and Georg Moser2
12School of Information Science, JAIST, Japan
hirokawa@jaist.ac.jp

Institute of Computer Science, University of Innsbruck, Austria
georg.moser@uibk.ac.at

Abstract. In this paper we present a simple technique for analysing
the runtime complexity of rewrite systems. In complexity analysis manytechniques are based on reduction orders. We show how the monotonicity condition for orders can be weakened by using the notion of contextsensitive rewriting. The presented technique is very easy to implement,even in a modular setting, and has been integrated in the Tyrolean Complexity Tool. We provide ample experimental data for assessing the viability of our method.

Keywords: term rewriting, complexity analysis, context-sensitive rewriting,automation

1

Introduction

This paper is concerned with runtime complexity analysis of term rewrite systems. In recent years the field of complexity analysis of rewrite systems has been
dramatically revived. Nowadays this area provides a wide range of different techniques to analyse the time complexity of rewrite systems, fully automatically.
Techniques range from direct methods, like polynomial interpretations, matrix interpretations of polynomial path orders (e.g. [1–3]) to transformation techniques,
like adaptions of the dependency pair method [4, 5] or modular techniques [6, 7].
See [8] for an overview of complexity analysis methods for term rewrite systems.
Furthermore the connection between (runtime) complexity analysis and implicit
computational complexity [9] is by now well-understood, cf. [10]. Despite thiswealth of results, very simple examples cannot be handled and in particular theenormous power of today’s termination provers for rewrite systems is still far
beyond the ability of today’s complexity analysers. Modern termination provers
provide termination or non-termination certificates for upto 90 % of the problems Termination Problem Database (TPDB for short), while with respect to?

This research is partly supported by JSPS KAKENHI Grant Number 25730004 andFWF (Austrian Science Fund) project I 963-N15.

automated polynomial runtime complexity analysis of rewrite systems, we see a
success rate of 38 %.3
Consider Example 1 below. The example encodes division in a natural way.
It can be analysed with the techniques mentioned above, but the optimal linear
bound on the runtime complexity is not attainable.
Example 1. Consider the following TRS Rdiv 4
1:

x−0→x

2 : s(x) − s(y) → x − y3:0 ÷ s(y) → 0

4 : s(x) ÷ s(y) → s((x − y) ÷ s(y)) .

The example also clarifies a difference between the derivational and the runtime complexity of rewrite systems. The derivational complexity function withrespect to a terminating TRS relates the maximal derivation height to the size ofthe initial term, cf. [12, 13]. On the other hand the runtime complexity function
with respect to a terminating TRS restricts the derivational complexity function
so that only basic terms are considered as starting terms. Here basic terms referto terms that contain a defined symbol only at root. This terminology was suggested in [4]. Related notions have been studied in [1, 14]. It is easy to see thatthe derivational complexity with respect to Rdiv bounded from below by an exponential function, while the runtime complexity is linear. Essentially this is dueto the fact that, in the computation of division, no contraction is ever required
below the second argument. Furthermore, dependency on the first argument islinear.
An inspection of the motivating example in the context of runtime complexity analysis reveals that direct methods are not applicable as the monotonicity
constraints are too restrictive. While monotonicity is no longer an issue for transformation techniques, neither the weak dependency pair method [4] nor the dependency tuple method [5] can deduce the linear (innermost) runtime complexity,
as essential constraints cannot be met. In this paper we extend the applicability of direct techniques for complexity results by showing how the monotonicity
constraints can be significantly weakened through the employ of usable replacement maps, which govern those argument position actually used in rewriting.
As usable replacement maps are not computable in general, we provide sufficiently expressive approximations of usable replacement maps. More generally,
we show how notions from context-sensitive rewriting can be made applicable inthe context of complexity analysis.
This paper is structured as follows. In the next section we cover basics. In
Section 3 we define usable replacement maps. In Section 4 we provide experimental data that verifies that the proposed technique makes a difference in practice.
Furthermore, in Section 5 we present related work and conclude in Section 6.
3

We base the comparison on last year’s run of TERMCOMP, where we consider the
categories TRS Standard and Runtime Complexity – Innermost Rewriting. Note thatfor termination YES and NO answers have been counted.
4This is Example 3.1 in Arts and Giesl’s collection of TRSs [11].

2Runtime Complexity Analysis Based on Matrix
Interpretations

We assume familiarity with term rewriting [13, 15] but briefly review basic concepts and notations from term rewriting, context-sensitive rewriting and recall
matrix interpretations. In particular we will adapt triangular matrix interpretations for runtime complexity analysis.
Let V denote a countably infinite set of variables and F a signature, suchthat F contains at least one constant. The set of terms over F and V is denotedby T (F, V). The set of positions Pos(t) of a term t is defined as usual. We
write PosG (t) ⊆ Pos(t) for the set of positions of subterms whose root symbol is
contained in G ⊆ F. The subterm of t at position p is denoted as t|p , and t[u]pdenotes the term that is obtained from t by replacing the subterm at p by u. The
subterm relation is denoted as E. Var(t) denotes the set of variables occurringin a term t. The size |t| of a term is defined as the number of symbols in t.
A term rewrite system (TRS ) R over T (F, V) is a finite set of rewrite rulesl → r. In the sequel, R always denotes a TRS. The rewrite relation is denoted
as →R and we use the standard notations for its transitive and reflexive closure.
We simply write → for →R if R is clear from context. Let s and t be terms. If
exactly n steps are performed to rewrite s to t, we write s →n t. With NF(R) we
denote the set of all normal forms of a term rewrite system R. The innermost
rewrite relation →−i R of a TRS R is defined on terms as follows: s →−i R t if there
exist a rewrite rule l → r ∈ R, a context C, and a substitution σ such thats = C[lσ], t = C[rσ], and all proper subterms of lσ are normal forms of R.
Defined symbols of R are symbols appearing at root in left-hand sides of R. The
set of defined function symbols is denoted as D, while the constructor symbols
F \ D are collected in C. We call a term t = f (t1 , . . . , tn ) basic or constructor
based if f ∈ D and ti ∈ T (C, V) for all 1 6 i 6 n. The set of all basic terms aredenoted by Tb . We call a TRS (innermost) terminating if no infinite (innermost)rewrite sequence exists.
A replacement map µ is a function with µ(f ) ⊆ {1, . . . , n} for all n-aryfunctions with n > 1 [16]. The set Posµ (t) of µ-replacing positions in t is defined
as follows:({}
if t is a variable ,Posµ (t) :={} ∪ {ip | i ∈ µ(f ) and p ∈ Posµ (ti )} if t = f (t1 , . . . , tn ) .
µA µ-step s −→ t is a rewrite step s → t whose rewrite position is in Posµ (s).
The set of all non-µ-replacing positions in t is denoted by Posµ (t); namely,
Posµ (t) := Pos(t) \ Posµ (t).
A monotone F-algebra is a pair (A, ) where A is an F-algebra and 
is a proper order such that for every function symbol f ∈ F, fA is strictly
monotone in all coordinates with respect to . A (monotone) F-algebra (A, ) is called well-founded if  is well-founded. Any monotone F-algebra (A, R)
induces a binary relation RA on terms: define s RA t if [α]A (s) R [α]A (t) for all
assignments α. We say A is compatible with a TRS R if R ⊆ RA . Let µ denote a

replacement map. Then we call a well-founded algebra (A, ) µ-monotone if forevery function symbol f ∈ F, fA is strictly monotone on µ(f ), i.e. fA is strictly
monotone with respect to every argument position in µ(f ). Similarly a relation
R is called µ-monotone if it is strictly monotone on µ(f ) for all f ∈ F. Let R beµa TRS compatible with a µ-monotone relation R. Then clearly any µ-step s −→timplies s R t.
We recall the concept of matrix interpretations on natural numbers (see [17]but compare also [18]). Let F denote a signature. We fix a dimension d ∈ N
and use the set Nd as the carrier of an algebra A, together with the following
extension of the natural order > on N: (x1 , x2 , . . . , xd ) > (y1 , y2 , . . . , yd ) :⇐⇒x1 > y1 ∧ x2 > y2 ∧ . . . ∧ xd > yd . Let µ be a replacement map. For each nary function symbol f , we choose as an interpretation a linear function of thefollowing shape:fA : (v 1 , . . . , v n ) 7→ F1 v 1 + · · · + Fn v n + f ,where v 1 , . . . , v n are (column) vectors of variables, F1 , . . . , Fn are matrices (eachof size d × d), and f is a vector over N. Moreover, suppose for any i ∈ µ(f ) the
top left entry (Fi )1,1 is positive. Then it is easy to see that the algebra A forms aµ-monotone well-founded algebra Let A be a matrix interpretation, let α0 denotethe assignment mapping any variable to 0, i.e. α0 (x) = 0 for all x ∈ V, and lett be a term. In the following we write [t], [t]j as an abbreviation for [α0 ]A (t), or([α0 ]A (t))j (1 6 j 6 d), respectively, if the algebra A is clear from the context.
The derivation height of a term s with respect to a well-founded, finitely
branching relation → is defined as: dh(s, →) = max{n | ∃t s →n t}.
Definition 2. We define the runtime complexity function rcR (n) and the innermost runtime complexity function rciR (n) as follows:rcR (n) := max{dh(t, →R ) | t is basic and |t| 6 n}
rciR (n) := max{dh(t, →−i R ) | t is basic and |t| 6 n} .
We may say the (innermost) runtime complexity of R is linear, quadratic,or polynomial if there exists a (linear, quadratic) polynomial p(n) such that(i)rcR (n) 6 p(n) for sufficiently large n.
Note that dh(t, ) is undefined, if the relation  is not well-founded or not
finitely branching. In fact compatibility of a constructor TRS with the polynomial path order >pop∗ ([3]) induces polynomial innermost runtime complexity,
whereas f(x) >pop∗ gn (x) >pop∗ · · · >pop∗ · · · >pop∗ g2 (x) >pop∗ g(x) >pop∗ x
holds for all n ∈ N, when precedence f > g is used. Hence dh(t, >pop∗ ) is undefined, while the order >pop∗ can still be employed in complexity analysis. Let
R be a binary relation over terms, let  be a proper order on terms, and let
G denote a mapping associating a term with a natural number. Then  is Gcollapsible on R if G(s) > G(t), whenever s R t and s  t holds. An order  iscollapsible (on R), if there is a mapping G such that  is G-collapsible (on R).

Lemma 3. Let R be a finitely branching and well-founded relation. Further,let  be a G-collapsible order with R ⊆ . Then dh(t, R) 6 G(t) holds for all
terms t.
If a TRS R and a µ-monotone matrix interpretation A are compatible, G(t)can be given by [t]1 . In order to estimate derivational or runtime complexity,
one needs to associate [t]1 to |t|. For this sake we define degrees of matrix interpretations.
Definition 4. A matrix interpretation is of (basic) degree k if there is a constant c such that [t]i 6 c · |t|k for all (basic) terms t and i, respectively.
An upper triangular complexity matrix is a matrix M in Nd×d such that wehave Mj,k = 0 for all 1 6 k < j 6 d, and Mj,j 6 1 for all 1 6 j 6 d. We say that a(µ-)monotone well-founded algebra A is a triangular matrix interpretation (TMI
for short) if A is a matrix interpretation (over N) and all matrices employed areof upper triangular complexity form. The following result can be easily distilledfrom the literature, cf. [19, 20].
Theorem 5. Let A be a TMI and let M denote the component-wise maximumof all matrices occurring in A. Further, let k denote the number of ones occurring
along the diagonal of M . Then, A is O(nk )-collapsible.
In order to cope with runtime complexity, a similar idea to restricted polynomial interpretations (see [1]) can be integrated to triangular matrix interpretations. We call A a restricted matrix interpretation (RMI for short) if A is amatrix interpretation, but for each constructor symbol f ∈ C, the interpretation fA of f employs upper triangular complexity matrices, only. The following
theorem is obtained from the combination of existing results [1, 2, 19].
Theorem 6. Let A be an RMI and let t be a basic term. Further, let M denote the component-wise maximum of all matrices used for the interpretationof constructor symbols, and let k denote the number of ones occurring along the
diagonal of M . Then A is of basic degree k. Furthermore, if M is the unit matrix
then A is of basic degree 1.
It is not difficult to see that Theorem 6 also holds for RMIs based on lower
triangular complexity matrices. We refrain from given the formal details, butrather exemplify the definition below.
Example 7. Consider the TRS Rsum 5
1:

sum(0) → 0

2 : sum(s(x)) → sum(x) + s(x)53:sum1(0) → 0

4 : sum1(s(x)) → s(sum1(x) + (x + x))

The TRS is Example 2.17 in Steinbach and Kühler’s collection of TRSs [21].

where, sum and sum1 are defined symbols, and 0, s, and + are constructor symbols. Consider the 2-dimensional RMI A (based on lower triangular complexity
matrices) with
 
 
 
0
12
0
0A =
sumA (x) =
x+
1
13
1
 
 
 
10
2
12
sA (x) =x+
sum1A (x) =
x
11
2
03
 
 
10
10
+A (x, y) =
x+
y.
00
00
The rules in Rsum are interpreted and ordered as follows.
      
2
0
2
0
1:
>
3:
>
4
1
3
1
 
        
 
32
6
22
2
32
6
32
2
2:
x+
>
x+
4:
x+
>
x+
.
43
9
00
0
33
6
32
2
Therefore, Rsum ⊆ >A holds. By an application of Theorem 6 we conclude thatthe runtime complexity is quadratic. As we see later, there is a tighter bound.

3

Usable Replacement Maps

Unfortunately, there is no RMI compatible with the TRS of our running example (Example 1). The reason is that the monotonicity requirement of matrix
interpretations is too severe for complexity analysis. Inspired by the idea of
Fernández [22], we show how context-sensitive rewriting is used in complexity
analysis. Here we briefly explain our idea. Let n denote the numeral sn (0). Consider the derivation from 4 ÷ 2:
4 ÷ 2 → s((3 − 1) ÷ 2) → s((2 − 0) ÷ 2) → s(2 ÷ 2) → · · ·where redexes are underlined. Observe that e.g. any second argument of ÷ isnever rewritten. More precisely, any derivation from a basic term consists of
only µ-steps with the replacement map µ: µ(s) = µ(÷) = {1} and µ(−) = ∅.
Recall that Posµ (t) denotes the set of µ-replacing positions in t and Posµ (t) =Pos(t) \ Posµ (t). Further, a term t is a µ-replacing term with respect to a TRS
R if p ∈ Posµ (t) implies t|p ∈ NF(R). The set of all µ-replacing terms is denotedby T (µ). Below [L](→∗ ) denotes the set {t | s →∗ t for some s ∈ L}.
The above observation is cast in the following definition, borrowed from [23].
Usable replacement maps satisfy a desired property for runtime complexity analysis, as detailed in this section.
Definition 8. Let → denote a binary relation. A replacement map µ is calleda usable replacement map with respect to → and the set of starting terms Tb if[Tb ](→∗ ) ⊆ T (µ).

The main result of this section is the definition of suitable approximationsof usable replacement maps. For that we adapt the cap-function ICAP suitably,cf. [24]. Let µ be a replacement map. Clearly the function µ is representable as
set of ordered pairs (f, i). Below we often confuse the notation of µ as a functionor as a set.
Definition 9. Let R be a TRS and let µ be a replacement map. We define theoperator Υ R as follows:Υ R (µ) := {(f, i) | l → C[f (r1 , . . . , rn )] ∈ R and CAPlµ (ri ) 6= ri } .
Here CAPsµ (t) is inductively defined on t as follows:t if t = s|p for some p ∈ Posµ (s) ,s
CAPµ (t) = u if t = f (t1 , . . . , tn ) and u and l unify for no l → r ∈ R ,y otherwise ,where, u = f (CAPsµ (t1 ), . . . , CAPsµ (tn )), y is a fresh variable, and we assume
that Var(l) ∩ Var(u) = ∅ holds.
We define the approximated innermost usable replacement map µR
i as follows
Rµi := Υ R (∅) and let the approximated usable replacement map µR
f denote theRRleast fixed point of Υ . The existence of Υ follows from the monotonicityof Υ R . If R is clear from context, we simple write µi , µf , and Υ , respectively.
In the remainder of the section we establish that µi and µf constitute usable
replacement maps for →−i and → respectively. Suppose s ∈ T (µ): observe thats
the function CAPµ (t) replaces a subterm u of t by a fresh variable if uσ is aredex for some sσ ∈ T (µ). This is exemplified below.
Example 10. Consider the TRS Rdiv . Let l → r be rule 4, namely, l = s(x)÷s(y)and r = s((x − y) ÷ s(y)). Suppose µ(f ) = ∅ for all functions f and let w and z
be fresh variables. The next table summarises CAPlµ (t) for each proper subterm t
in r. To see the computation process, we also indicate the term u in Definition 9.
t
CAPlµ (t)
u

x y
x y
– –

x−y
w
x−y

s(y) (x − y) ÷ s(y)
s(y)
z
s(y)
w ÷ s(y)By underlining proper subterms t in r such that CAPlµ (t) 6= t, we haves((x − y) ÷ s(y))
which indicates (s, 1), (÷, 1) ∈ Υ (µ).
The next lemma clarifies the rôle played by the cap function CAPsµ (t).
Lemma 11. Let s and t be terms, and σ a substitution such that sσ ∈ T (µ)
and CAPsµ (t) = t. Then tσ ∈ NF(R).

Proof. We use induction on t. Suppose sσ ∈ T (µ) and CAPsµ (t) = t. If t = s|pfor some p ∈ Posµ (s) then tσ = (sσ)|p ∈ NF follows by definition of T (µ).
We can assume that t = f (t1 , . . . , tn ). Assume otherwise that t = x ∈ V,
then CAPsµ (x) = x entails that xσ occurs at a non-µ-replacing position in sσ.
Hence xσ ∈ NF follows from sσ ∈ T (µ). Moreover, by assumption we have:
1. CAPsµ (ti ) = ti for each i, and2. there is no rule l → r ∈ R such that t and l unify.
Due to 2) lσ is not reducible at the root, and the induction hypothesis yields
ti σ ∈ NF because of 1). Therefore, we obtain tσ ∈ NF.
tu
For a smooth inductive proof of the key lemma, Lemma 14, we develop analternative characterisation of the set of µ-replacing terms T (µ).
Definition 12. The set {(f, i) | f (t1 , . . . , tn ) E t and ti 6∈ NF(R)} is denotedby υ(t).
The next lemma shows that the set of µ-replacing terms T (µ) can be characterised through the above definition.
Lemma 13. T (µ) = {t | υ(t) ⊆ µ}.
Proof. For the inclusion from left to right, let t ∈ T (µ) and let (f, i) ∈ υ(t).
We show (f, i) ∈ µ. By Definition 12 there is a position p ∈ Pos(t) with t|p =f (t1 , . . . , tn ) and t|pi 6∈ NF. Thus pi ∈ Posµ (t) and i ∈ Posµ (t|p ). Hence (f, i) ∈ µ
is concluded.
Next we consider the opposite direction {t | υ(t) ⊆ µ} ⊆ T (µ). Let t be aminimal counter-example such that υ(t) ⊆ µ and t 6∈ T (µ). One can writet = f (t1 , . . . , tn ). Then, there exists a position p ∈ Posµ (t) such that t|p 6∈ NF.
Because  6∈ Posµ (t) by definition, p = iq with i ∈ N. As iq ∈ Posµ (t) one of(f, i) 6∈ µ or q ∈ Posµ (t|i ) must hold. Consider the first alternative. Then by
Definition 12, (f, i) ∈ υ(t) ⊆ µ and we obtain a contradiction. Now, consider
the second alternative. Note that t|iq 6∈ NF implies t|i 6∈ NF. In conjunction withq ∈ Posµ (t|i ) this yields that ti is counter-example which is smaller than t. This
contradicts the definition of t.
tu
The next lemma about the operator Υ is a key for the main theorem. Notethat every subterm of a µ-replacing term is a µ-replacing term.
Lemma 14. If l → r ∈ R and lσ ∈ T (µ) then rσ ∈ T (µ ∪ Υ (µ)).
Proof. Let l → r ∈ R and suppose lσ ∈ T (µ). By Lemma 13 we haveT (µ) = {t | υ(t) ⊆ µ}

T (µ ∪ Υ (µ)) = {t | υ(t) ⊆ µ ∪ Υ (µ)} .

Hence it is sufficient to show υ(rσ) ⊆ µ ∪ Υ (µ). Let (f, i) ∈ υ(rσ). There isp ∈ Pos(rσ) with rσ|p = f (t1 , . . . , tn ) and ti 6∈ NF. If p is below some variable
position of r, rσ|p is a subterm of lσ, and thus υ(rσ|p ) ⊆ υ(lσ) ⊆ µ. Otherwise, p
is a non-variable position of r. We may write r|p = f (r1 , . . . , rn ) and ri σ = ti 6∈
NF. Due to Lemma 11 we obtain CAPlµ (ri ) 6= ri . Therefore, (f, i) ∈ Υ (µ).
tuLemma 15. For the approximated usable replacement maps T (µi ) and T (µf ),the following implications hold:
1. If s ∈ T (µi ) and s →−i t then t ∈ T (µi ).
2. If s ∈ T (µf ) and s → t then t ∈ T (µf ).
Proof. We show property 1). Suppose s ∈ T (µi ) and s →−i t is a rewrite stepat p. Due to the definition of innermost rewriting, we have s|p ∈ T (∅). Hence,t|p ∈ T (µi ) is obtained by Lemma 14. Because s ∈ T (µi ) we have p ∈ Posµi (s).
Hence due to t|p ∈ T (µi ) we conclude t = s[t|p ]p ∈ T (µi ) due to the above remark.
The proof of 2) proceeds along the same pattern and is left to the reader.
tu
We arrive at the main result of this section.
Theorem 16. The inclusions [T (∅)](→−i ∗R ) ⊆ T (µi ) and [T (∅)](→∗R ) ⊆ T (µf )hold. In particular µi and µf constitute usable replacement maps for →−i and →,respectively.
Proof. We focus on the second part of the theorem, where we have to prove thatt ∈ T (µf ), whenever there exists s ∈ T (∅) such that s →∗R t. As T (∅) ⊆ T (µf )this follows directly from Lemma 15.
Note that T (∅) is the set of all argument normalised terms. Therefore, Tb ⊆T (∅). Hence the second half of the theorem follows.
t
u
µ

µ

i
f
Given a TRS R we write −→for the µi -step relation of R, and −→for theµf -step relation. The following corollary to Theorem 16 is immediate.
µ

µ

i
f
Corollary 17. We have dh(t, →−i R ) 6 dh(t, −→)and dh(t, →R ) = dh(t, −→)forall terminating terms t ∈ Tb .

An advantage of the use of context-sensitive rewriting is that the compatibility requirement of monotone algebra in termination or complexity analysis isrelaxed to µ-monotone algebra. We illustrate its use in the next examples.
Example 18. Recall the TRS Rdiv given in Example 1 above. The usable replacement maps are as follows:µi (−) = ∅ µi (s) = µi (÷) = {1}µf (s) = µf (−) = µf (÷) = {1} .

Consider the 1-dimensional RMI A (i.e. linear polynomial interpretations) with
0A = 1, sA (x) = x + 2, −A (x, y) = x + 1, and ÷A (x, y) = 3x; A is strictlyµi -monotone and µf -monotone. The rules in Rdiv are interpreted and ordered asfollows.
1:

x+1>x

3:

3>1

2:

x+3>x+1

4:

3x + 6 > 3x + 5 .

Therefore, Rdiv ⊆ >A holds. Applying Theorem 6 in the context of usable replacement maps, we conclude that the (innermost) runtime complexity is linear,which is optimal.

Example 19. Recall the TRS Rsum of Example 7. The usable replacement map
for full rewriting is as follows:µf (s) = µf (+) = {1} .

µf (sum) = µf (sum1) = ∅Consider the 1-dimensional RMI A with
0A = 2sA (x) = x + 2+A (x, y) = x

sumA (x) = 2xsum1(x, y) = 2x .

which is strictly µf -monotone. The rules in Rdiv are interpreted and ordered asfollows.
1:

4>2

3:

4>2

2:

2x + 4 > 2x4:

2x + 4 > 2x + 2 .

Therefore, Rdiv ⊆ >A holds. By an application of Theorem 6 we conclude thatthe runtime complexity is linear, which is optimal.
We cast the observations in the example into another corollary to Theorem 16.
Corollary 20. Let R be a TRS and let A be a d-degree µi -monotone (or µf monotone) RMI compatible with R. Then the (innermost) runtime complexity(i)function rcR with respect to R is bounded by a d-degree polynomial.
Proof. It suffices to consider the case for full rewriting. Let s, t be terms suchµfthat s →R t. By the theorem, we have s −→t. Furthermore, by assumption
R ⊆ A and for any f ∈ F, fA is strictly monotone on all µf (f ). Thus s A tfollows. Finally, the corollary follows by application of Theorem 6.
tu4Experiments

The usable replacement map method has been incorporated into the Tyrolean
Complexity Tool TCT [25]. We note that the established method can easily combined with existing modular frameworks and the implementation in TCT makes(essential) use of this. In this section we present an experimental evaluationof the technique based on version 8.0.6 of the Termination Problems Database(TPDB for short). We consider TRSs without theory annotation, where the runtime complexity analysis is non-trivial, that is the set of basic terms is infinite.
This testbed comprises 1249 TRSs.
All experiments were conducted on a machine that is identical to the official
competition server (8 AMD Opteron 885 dual-core processors with 2.8GHz,
8x8 GB memory). As timeout we use 60 seconds. The complete experimental data can be found at http://cl-informatik.uibk.ac.at/software/tct/experiments/rtatlca14, where also the testbed employed is detailed.
Table 1 summarises the experimental results of the use of usable replacement
maps for full and innermost runtime complexity analysis. The tests employ one-

®

full
resultinnermost

RMI(1-3),(−) RMI(1-3), (+)

RMI(1-3), (−) RMI(1-3), (+)O(n)
O(n2 )O(nk )

103
174
183

134
209
225

104
174
183

140
226
247

timeout (60s)

113

109

113

117

Table 1. Experimental results I (one- to three-dimensional RMIs)

to three-dimensional RMIs.6 The tests clearly indicate the power of the established technique. This power is not only in the absolute number of examples, butmore importantly in the precision of the analysis. We note that our tests only
make use of the simplest notion of RMIs for runtime complexity analysis cf. [26].
This is a rather mundane method, more sophisticated methods have been reported in [2, 19]. However, to assess the power of the established technique thisrestriction is insignificant.
In Table 2 we present the overall power obtained for the automated runtime
complexity analysis. Here we test the current version of TCT using a strategy
that avoids the new method, in contrast to its standard strategy. It is to be expected that the effect of the proposed technique is smaller than in Table 1. Thisis due to the presence of transformation techniques, like the weak dependency
pair method [4] or the dependency tuple method [5] and the use of a modular
framework [7]. While the usable argument method is still effective for weak dependency pairs, as it may lighten the weight gap constraint, the dependency tuple
method allows to remove all monotonicity constraints. Note that the dependency
tuple method is only applicable for innermost runtime complexity.
Despite these theoretical facts, the method has a significant impact on fulland innermost rewriting. While the overall effect is a lot smaller than for directtechniques, we emphasise that the method allows to win some examples thatcan be handled with linear rather than with quadratic complexity. The alert
reader may wonder, why there is a positive effect at all in the innermost case,as transformation techniques do not require monotonicity. This is due to thecase that even for innermost runtime complexity analysis, direct methods are
currently not superseded by transformational techniques.

5

Related Work

Usable replacement maps Usable replacement maps were originally introduced
by Fernández [22] for proving termination of innermost rewriting. This notion
6

Note that matrix interpretations, that is the test “RMI(1-3)”, cannot discern between
innermost versus full rewriting. Hence the practical differences noted in the table arecoincidental.

full
resultTCT (−) TCT (+)

innermost
TCT (−) TCT (+)

O(1)
O(n)
O(n2 )O(n3 )O(nk )

92
408
423
424
426

100
421
428
429
431

326
500
554
564
568

325
508
555
565
569

timeout (60s)

714

711

617

615

Table 2. Experimental results II (overall effect)is already applicable for analysing innermost runtime complexity. More precisely, we link Theorem 16 to Fernández’ work. In [22] an application of contextsensitive rewriting for innermost termination has been established.
µi
Proposition 21 ([22]). A TRS R is innermost terminating if −→is terminating.

Proof. We show the contraposition. If R is not innermost terminating, there isan infinite sequence t0 →−i t1 →
−i t2 →
−i · · · , where t0 ∈ T (∅). From Theorem 16
µi
µi
µi
µi
and Lemma 15 we obtain t0 −→ t1 −→t2 −→· · · . Hence, −→is not terminating.
tu
We lifted Fernández’ notion to full rewriting, exploiting the cap function
ICAP in [24]. Realisation of a fixed point calculation of usable replacement maps
is considered as a primary result of this paper. Note that Proposition 21 does
not generalise to full termination, even if one replaces the innermost replacement
map µi , by the replacement map µf .
Example 22. Consider the famous Toyama’s example R
f(a, b, x) → f(x, x, x)g(x, y) → x

g(x, y) → y .

The replacement map µf is empty. Thus, the algebra A over N
fA (x, y, z) = max{x − y, 0}

gA (x, y) = x + y + 1

aA = 1bA = 0 .

is µf -monotone and we have R ⊆ >A . However, we should not conclude termination of R, because f(a, b, g(a, b)) is non-terminating.
Cap functions In [22] usable replacement maps for innermost rewriting are defined as {(f, i) | l → C[f (r1 , . . . , rn )] ∈ R and ri|p 6C l, for some p ∈ PosD (r)}.
This and our definition µi coincide if the following cap function is used during
the computation of Υ R :t if t C s ,s
CAPµ (t) = u if t = f (t1 , . . . , tn ) and f ∈ C ,y otherwise ,where, u = f (CAPsµ (t1 ), . . . , CAPsµ (tn )) and y is a fresh variable. In the light ofthis reformulation one can (easily) verify that the usable replacement map µi in
Section 3 is always a subset of the above set.
There exists a cap function for context-sensitive rewriting, introduced by
Alarcón et al. [27] for termination analysis. Their definition is the following:t if t is a variable ,CAPsµ (t) = u if t = f (t1 , . . . , tn ) and u and l unify for no l → r ∈ R ,y otherwise ,where, y is a fresh variable and u = f (u1 , . . . , un ). Each ui stands for CAPsµ (ti )if i ∈ µ(f ), and ti otherwise. This definition cannot be used for calculation of
usable replacement maps: It is designed for exploiting a given replacement map µ
to ignore potential rewrite positions, while our cap function is aimed at detecting
potential reducible positions to build a usable replacement map.
Dependency pairs Weak dependency pairs [4] and dependency tuples [5] aretransformational approaches that split a rewrite relation into two relations. This
split allows us to weaken the monotonicity condition. Although these approaches
exploit dependencies of defined symbols, they do not analyse how variables inrewrite rules or dependency pairs (tuples) are instantiated in rewriting.7 As aconsequence, the transformations do not resolve the problem of variable duplication addressed in the introduction. We emphasise that usable replacement maps
and dependency pairs (tuples) are complementary and the combination is beneficial, as seen in Section 4. A similar observation holds for techniques employing
modularity.

6

Conclusion

In this paper we have defined the notion of usable replacement maps. It is astraightforward observation that only usable arguments need to be considered
for monotonicity conditions. In a nutshell, we have shown how monotonicity
conditions for orders can be weakened by using the notion of context-sensitive
rewriting.
The presented technique is very easy to implement and has been integrated
in the Tyrolean Complexity Tool. Above we have provided ample experimental data for assessing the viability of our method. The positive experimental
evaluation, even in the innermost case, is somewhat surprising. One might haveassumed that transformation techniques, as for example the dependency tuple
method introduced in [5] supersede direct methods and thus refrain us fromconcerns about monotonicity. Our experiments clearly show that this is not thecase. We emphasise that the here proposed method directly extends to modular
frameworks and our implementation in TCT makes essential use of this fact.
7

Approximation techniques for dependency graphs may be considered an exception.

minus : ( nat , nat ) -> nat
minus (m , n ) = match m with| 0-> 0
| S m ’ -> match n with| 0-> m
| S n ’ -> minus (m ’ , n ’);quot : ( nat , nat ) -> nat
quot (m , n ) = match m with| 0-> 0
| S m ’ -> match n with| 0-> 0
| S n ’ ->( quot ( minus (m ’ , n ’) , n )) + 1;
Fig. 1. Division in RaML

Apart from its practical value the proposed technique allows to incorporate
features of complexity analysis of functional programs into rewrite systems. We
consider a reformulation of our motivating example in an ML-like language,cf. Figure 1. This functional program is subject to the analysis of the RaMLprototype, developed by Hoffmann et al. [28]. The prototype is based on anamortised resource analysis that employs a potential-based type system. Application of the method on the example yields the optimal linear bound on the
innermost runtime complexity. Inspection of the complexity proof reveals thatthe method assigns zero potential to the second argument of minus and div,
which is related to the fact that these arguments can be safely ignored in our
setting, cf. Example 18. However, the potential-based method depends on thepresence of types as detailed in [29]. We emphasise that the usable arguments
method allows a similar fine-grained control for the runtime complexity analysis,
even without the introduction of types.
Acknowledgments. We would like to thank the anonymous reviewers fortheir valuable comments that greatly helped in improving the presentation.

References
1. Bonfante, G., Cichon, A., Marion, J.Y., Touzet, H.: Algorithms with polynomialinterpretation termination proof. JFP 11(1) (2001) 33–53
2. Middeldorp, A., Moser, G., Neurauter, F., Waldmann, J., Zankl, H.: Joint spectral
radius theory for automated complexity analysis of rewrite systems. In: Proc. 4th
CAI. Volume 6742 of LNCS. (2011) 1–20
3. Avanzini, M., Moser, G.: Polynomial path orders. LMCS 9(4) (2013)
4. Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency
pair method. In: Proc. 4th IJCAR. Number 5195 in LNAI (2008) 364–380
5. Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity ofterm rewriting by dependency pairs. JAR 51(1) (2013) 27–56

6. Zankl, H., Korp, M.: Modular complexity analysis via relative complexity. LMCS
10(1:19) (2014) 1–33
7. Avanzini, M., Moser, G.: A combination framework for complexity. In: Proc. 24th
RTA. Volume 21 of LIPIcs. (2013) 55–70
8. Moser, G.: Proof Theory at Work: Complexity Analysis of Term Rewrite Systems.
CoRR abs/0907.5527 (2009) Habilitation Thesis.
9. Baillot, P., Marion, J.Y., Rocca, S.R.D.: Guest editorial: Special issue on implicit
computational complexity. TOCL 10(4) (2009)
10. Avanzini, M., Moser, G.: Closing the gap between runtime complexity and polytime
computability. In: Proc. 21st RTA. Volume 6 of LIPIcs. (2010) 33–48
11. Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using
dependency pairs. Technical Report AIB-2001-09, RWTH Aachen (2001)
12. Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations.
In: Proc. 3rd RTA. Number 355 in LNCS (1989) 167–177
13. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University
Press (1998)
14. Choppy, C., Kaplan, S., Soria, M.: Complexity analysis of term-rewriting systems.
TCS 67(2–3) (1989) 261–282
15. TeReSe: Term Rewriting Systems. Volume 55 of Cambridge Tracks in TheoreticalComputer Science. Cambridge University Press (2003)
16. Lucas, S.: Context-sensitive rewriting strategies. IC 178(1) (2002) 294–343
17. Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. JAR 40(3) (2008) 195–220
18. Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Proc. 17th RTA. Volume 4098 of LNCS. (2006) 328–342
19. Neurauter, F., Zankl, H., Middeldorp, A.: Revisiting matrix interpretations forpolynomial derivational complexity of term rewriting. In: Proc. the 17th LPAR.
Volume 6397 of LNCS (ARCoSS). (2010) 550–564
20. Waldmann, J.: Polynomially bounded matrix interpretations. In: Proc. 21st RTA.
Volume 6 of LIPIcs. (2010) 357–372
21. Steinbach, J., Kühler, U.: Check your ordering – termination proofs and open
problems. Technical Report SR-90-25, Universität Kaiserslautern (1990)
22. Fernández, M.L.: Relaxing monotonicity for innermost termination. Information
Processing Letters 93(1) (2005) 117–123
23. Avanzini, M.: Verifying Polytime Computability Automatically. PhD thesis, University of Innsbruck (2013)
24. Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving terminationof higher-order functions. In: Proc. 5th FROCOS. Volume 3717 of LNAI. (2005)
216–231
25. Avanzini, M., Moser, G.: Tyrolean Complexity Tool: Features and usage. In: Proc.
24th RTA. Volume 21 of LIPIcs. (2013) 71–80
26. Moser, G., Schnabl, A., Waldmann, J.: Complexity analysis of term rewriting
based on matrix and context dependent interpretations. In: Proc. 28th FSTTCS.
Volume 2 of LIPIcs. (2008) 304–315
27. Alarcón, B., Gutiérrez, R., Lucas, S.: Context-sensitive dependency pairs. IC
208(8) (2010) 922–968
28. Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. In: Proc. 24th CAV.
Volume 7358 of LNCS. (2012) 781–786
29. Hofmann, M., Moser, G.: Amortised resource analysis and typed polynomial interpretations. In: Proc. of 25th RTA & 12th TLCA. LNCS (ARCoSS) (2014) toappear.