11institutetext: Free University of Bolzano, Italy, and University of
Innsbruck, Austria
11email: sarwinkler<EMAIL_ADDRESS>
# Runtime Complexity Analysis of Logically Constrained Rewriting

Sarah Winkler and Georg Moser

###### Abstract

Logically constrained rewrite systems (LCTRSs) are a versatile and efficient
rewriting formalism that can be used to model programs from various
programming paradigms, as well as simplification systems in compilers and SMT
solvers. In this paper, we investigate techniques to analyse the worst-case
runtime complexity of LCTRSs. For that, we exploit synergies between
previously developed decomposition techniques for standard term rewriting by
Avanzini et al. in conjunction with alternating time and size bound
approximations for integer programs by Brockschmidt et al. and adapt these
techniques suitably to LCTRSs. Furthermore, we provide novel modularization
techniques to exploit loop bounds from recurrence equations which yield
sublinear bounds. We have implemented the method in TCT to test the viability
of our method.

##  1 Introduction

Rewriting with constraints over background theories is a highly versatile
model of computation and tool for analysis. While user-defined data types are
modelled by free function symbols, arbitrary decidable theories can be
incorporated, such as integer or bit-vector arithmetic, lists, or array
theory. Constraints over these theories can be effectively handled by SMT
solvers. Different rewrite formalisms capture this idea [11, 21, 19]. Here we
use the recent notion of _logically constrained term rewrite systems_
(_LCTRSs_ for short), due to Kop et al. [28, 29, 20, 10].

LCTRSs can abstract programs in a variety of paradigms, comprising imperative,
functional, and logic languages. They also subsume integer transition systems
(ITSs), which constitute a frequently used program abstraction [19, 15, 8] but
do—in contrast to LCTRSs—not support (non-tail) recursion. On the other hand,
LCTRSs can also model simplification routines for expressions, which are
crucial procedures in compilers or SMT solvers. For all of these application
areas, LCTRSs offer a _uniform_ toolset to analyse _termination_ (or non-
termination) [27, 33], _reachability_ [10], _uniqueness_ [41], or _program
equivalence_ [20].

However, techniques for resource analysis of LCTRSs are so far lacking. This
is despite the fact that in their application domains (program analysis,
simplification systems), execution time is crucial. As a remedy, this paper
investigates methods to analyse (worst-case) innermost runtime complexity of
logically constrained rewrite systems. To this end, we unify and generalise
the complexity framework for standard rewriting by Avanzini and Moser [4] with
the approach by Brockschmidt et al. to alternate time and size bound analysis
for ITSs [8], and moreover propose processors for modularisation and sublinear
bounds.

#### Contributions.

We present a novel resource analysis framework for logically constrained
rewrite systems (Sect. 4) coached in the modular processor framework of TCT
[5]. Precisely,

  1. 1.

we present the first fully-automated runtime complexity analysis of LTCRSs;

  2. 2.

we unify the complexity framework for standard (innermost) rewriting by
Avanzini and Moser [4] and the alternating time and size bound approximations
for ITSs by Brockschmidt et al. [8],

  3. 3.

generalising this, we introduce a novel modularisation processor, the
_splitting processor_ ;

  4. 4.

we present a novel processor, dubbed _recurrence processor_ to derive
sublinear bounds based on recurrences as described by the Master Theorem;

  5. 5.

we illustrate the viability of our method by providing a prototype
implementation as a dedicated module tct-lctrs in TCT, and evaluate it on ITS
benchmarks.

In the remainder of the section, we highlight potential application areas of
LCTRSs to emphasise their versatility. In the next section (Sect. 2) we give a
high-level account of our technical achievements, providing a step-by-step
explanation how the runtime complexity of a natural representation of
mergesort can be optimally analysed in our framework. In this section, we also
discuss to what extent our results can be applied to the below given examples.
In Sect. 3 we summarise the foundations of LCTRSs, while in Sect. 4 we detail
the complexity framework used. Processors carried over from the ITS setting
are presented in Sect. 5, and the novel processors are introduced in Sect. 6.
Implementational choices and experimental results are summarized in Sect. 7.
Finally, in Sect. 8 we conclude. Due to space restrictions, some proofs were
moved to an appendix.

#### Logically Constrained Rewrite Systems.

We emphasise motivational examples from three different domains, focusing on
imperative and logic programs, as well as compiler optimisations.

###### Example 1

The following recursive ITS $\mathcal{R}_{1}$, due to Albert et al. [1],
corresponds to an imperative mergesort implementation after computing loop
summaries. It is naturally coached into the LCTRS framework, with the theory
of integers as background theory.

$\displaystyle(1)\\!\\!\\!\\!$ $\displaystyle\mathsf{init}(x,y,z)$
$\displaystyle\to\mathsf{m}(x,y,z)$ $\displaystyle(2)\\!\\!\\!\\!$
$\displaystyle\mathsf{m}_{3}(x,y,z)$ $\displaystyle\to\mathsf{merge}(y,z,z)$
$\displaystyle(3)\\!\\!\\!\\!$ $\displaystyle\mathsf{m}_{1}(x,y,z)$
$\displaystyle\to\mathsf{m}(y,y,z)$ $\displaystyle(4)\\!\\!\\!\\!$
$\displaystyle\mathsf{merge}(x,y,z)$ $\displaystyle\to\mathsf{merge}(x-1,y,z)\
[x\geqslant 1\wedge y\geqslant 1]$ $\displaystyle(5)\\!\\!\\!\\!$
$\displaystyle\mathsf{m}_{0}(x,y,z)$ $\displaystyle\to\mathsf{split}(x,y,z)$
$\displaystyle(6)\\!\\!\\!\\!$ $\displaystyle\mathsf{split}(x,y,z)$
$\displaystyle\to\mathsf{split}(x-2,y,z)\ [x\geqslant 2]$
$\displaystyle(7)\\!\\!\\!\\!$ $\displaystyle\mathsf{m}_{2}(x,y,z)$
$\displaystyle\to\mathsf{m}(z,y,z)$ $\displaystyle(8)\\!\\!\\!\\!$
$\displaystyle\mathsf{merge}(x,y,z)$ $\displaystyle\to\mathsf{merge}(x,y-1,z)\
[x\geqslant 1\wedge y\geqslant 1]$ $\displaystyle(9)\\!\\!\\!\\!$
$\displaystyle\mathsf{m}(x,y,z)$ $\displaystyle\to\hbox
to0.0pt{$\langle\mathsf{m}_{0}(x,u,v),\mathsf{m}_{1}(x,u,v),\mathsf{m}_{2}(x,u,v),\mathsf{m}_{3}(x,u,v)\rangle$\hss}$
$[x\geqslant 2\wedge u\geqslant 0\wedge v\geqslant 0\wedge x+1\geqslant
2u\wedge 2u\geqslant x\wedge x\geqslant 2v\wedge 2v+1\geqslant x]$

Here a rule of the form $\ell\to r\ [c]$ means that an instance of $\ell$ is
replaced by the respective instance of $r$ provided that the instance of $c$
is satisfied.

Similarly, (constraint) logic programs can be nicely suited to LCTRSs.

###### Example 2

Consider the following simple Prolog program from the benchmarks collected by
Mesnard and Neumerkl [31].

max_length(Ls,M,Len) | :- max1(Ls,0,M), len(Ls,Len). |
---|---|---
len([H|T],L) | :- len(T,LT), L is LT + 1. | len([],0).
max1([H|T],N,M) | :- H <= N, max1(T,N,M). | max1([],M,M).
max1([H|T],N,M) | :- H > N, max1(T,H,M). |

Assuming an instantiated list $\mathtt{Ls}$, max_length(Ls,M,Len) is
deterministic and returns the maximal list entry and the length of the list.
This function becomes representable as the following LCTRS $\mathcal{R}_{2}$
over the theory of integers and lists:

$\displaystyle\mathsf{max\\_length}(ls,m,l)$
$\displaystyle\to\langle\mathsf{max}(ls,\mathsf{0},m),\mathsf{len}(ls,l)\rangle$
$\displaystyle\mathsf{len}(xs,l)$
$\displaystyle\to\mathsf{len}(t,l-\mathsf{1})~{}[xs\approx h\mathrel{::}t]$
$\displaystyle\mathsf{len}([],\mathsf{0})$ $\displaystyle\to\langle\rangle$
$\displaystyle\mathsf{max}(xs,n,m)$
$\displaystyle\to\mathsf{max}(t,n,m)~{}[h\leqslant n\wedge xs\approx
h\mathrel{::}t]$ $\displaystyle\mathsf{max}([],m,m)$
$\displaystyle\to\langle\rangle$ $\displaystyle\mathsf{max}(xs,n,m)$
$\displaystyle\to\mathsf{max}(t,h,m)~{}[h>n\wedge xs\approx h\mathrel{::}t]$

Here, $\mathrel{::}$ denotes the cons operator and
$\langle\cdot,\cdot\rangle$, $\langle\rangle$ are additional constructor
symbols to collect the recursive calls of a rule. Conceptually LCTRSs appear
as a good fit to express _constraint_ logic programs as well, making use of
the fact that constraints are natively supported.

In order to emphasise that LCTRSs are not confined to static program analysis,
we present a final example which is concerned with program optimisation.

###### Example 3

The Instcombine pass in the LLVM compilation suite performs _peephole
optimisations_ to simplify expressions in the intermediate representation. The
current optimisation set contains over 1000 simplification rules to e.g.
replace multiplications by shifts or perform bitwidth changes. About 500 of
them have recently been translated into the domain-specific language Alive
[30], and subsequently into LCTRSs [41], resulting in rules of the following
shape:

$\displaystyle\mathsf{add}(x,x)$
$\displaystyle\to\mathsf{shift\\_left}(x,\textsf{\\#x{1}})$
$\displaystyle\mathsf{add}(\mathsf{add}(\mathsf{xor}(\mathsf{or}(x,a),y),\textsf{\\#x{1}}),w)$
$\displaystyle\to\mathsf{sub}(w,\mathsf{and}(x,b))~{}[a\approx{\sim}b]$
$\displaystyle\mathsf{add}(\mathsf{xor}(x,a),z)$
$\displaystyle\to\mathsf{sub}(a+z,x)~{}[\mathsf{isPowerOf2}(a+\textsf{\\#x{1}})\land\dots]\hbox
to0.0pt{$\;$.\hss}$

These rules are expressed over the background theory of bit-vectors.
Naturally, as a compiler pass this simplification suite is a performance-
critical routine, hence an automated complexity analysis is of great interest.

##  2 Step by Step to an Optimal Bound

Consider the rewrite system $\mathcal{R}_{1}$ from Ex. 1, and a rewrite
sequence starting with an instance of $\mathsf{init}(x_{0},y_{0},z_{0})$.
Below we sketch the steps to obtain an upper bound on the runtime complexity
of $\mathcal{R}_{1}$, expressed in $|x_{0}|$, $|y_{0}|$, and $|z_{0}|$, where
$|\cdot|$ denotes the absolute value.

An automated runtime complexity analysis of mergesort is notoriously
difficult: For this example, CoFloCo [17, 16] can only derive a quadratic
bound, while KoAT [8] (as well as AProVE [22]) even proposes an exponential
bound. PUBS [1] can produce an $\mathcal{O}(n\cdot\log(n))$ bound, using a
special _level-counting_ feature, which however negatively affects its overall
success rate. Due to the work presented in this paper, our complexity analyser
TCT can automatically prove the optimal $\mathcal{O}(n\cdot\log(n))$ upper
bound. This is obtained by the following recipe.

  1. 1.

We first compute _dependency tuples_ of all rules to focus the analysis on
recursive calls (see Def. 4). Then a _dependency graph_ approximation is
computed to estimate computation paths, where the numbers refer to the
respective dependency tuples of rules in Ex. 1:

(1)(9)(3)(7)(2)(5)(6)(4)(8)

  2. 2.

Next, we derive bounds on the _size of variables_ in left hand sides of rules,
in terms of the sizes of the variables in the initial term
$\mathsf{init}(x_{0},y_{0},z_{0})$. For example, it is easy to check that for
rule (9), $|x|$, $|y|$, and $|z|$ are bounded by $|x_{0}|$, $|y_{0}|$, and
$|z_{0}|$, respectively, and all variables in other rules are bounded by
$|x_{0}|$. This is established by the _size bounds processor_ (Lem. 3).
Formally, we adapt techniques developed for ITSs for that purpose [8].

  3. 3.

We first derive time bounds for the SCCs $\\{2,4,8\\}$ and $\\{6\\}$
separately (Lem. 2). Thus, using the size bounds from above and suitable
_interpretations_ [4] (also called polynomial ranking functions [8]) for
LCTRSs, one can derive linear runtime bounds $2|x_{0}|+1$ and $|x_{0}|$ for
these subproblems, respectively.

  4. 4.

In order to analyse the SCC $\\{3,7,9\\}$, we first apply _chaining_ to
combine rule (9) with (3) and (7), respectively (eliminating symbols
$\mathsf{m}_{1}$ and $\mathsf{m}_{2}$).

  5. 5.

With respect to the modified rule (9) and the derived subproblem bounds, we
exploit the _loop processor_ (Lem. 5) to observe that its runtime can thus be
overestimated by the following _recurrence_ equations.

$\displaystyle f(|x|,|y|,|z|)$ $\displaystyle=2\cdot
f(|x|/2,|x|/2,|x|/2)+3|x|+1$ $\displaystyle f(1,|y|,|z|)$
$\displaystyle=0\quad$ (1)

Solving the recurrences by the Master Theorem, implies an overall runtime
complexity of $\mathcal{O}(|x_{0}|\cdot\log(|x_{0}|))$ for $\mathcal{R}_{1}$,
as $|x|$ in rule (9) is bound by $|x_{0}|$.

Wrt. $\mathcal{R}_{2}$ from Ex. 2, we can fully automatically infer an
(asymptotic) optimal linear bound on the runtime complexity for the given
instantiation. Here, we take an instance of $\mathsf{max\\_length}(xs,z,l)$ as
initial term. As for comparison, note that the corresponding logic program
cannot be handled by a dedicated variant of AProVE [23] geared towards runtime
complexity analysis of logic programs. Only termination can be shown by the
most recent version of AProVE [22]. A priori, our approach is restricted to
logic programs with instantiation patterns that ensure determinism and avoid
failure, but in the conclusion we discuss how to overcome this limitation.

Finally, Ex. 3 cannot yet be handled, as a successful analysis requires the
extension of the proposed framework to _(innermost) derivational complexity_
(i.e., the setting of arbitrary starting terms that may contain nested defined
symbols). This is subject to future work. However, we conceive the work
established in this paper as a solid first step towards the automated analysis
of such systems.

##  3 Logically Constrained Term Rewriting

We assume familiarity with term rewriting [6, 37], but briefly recapitulate
the notion of logically constrained rewriting [28, 20] that our approach is
based on. We consider an infinite, sorted set of variables $\mathcal{V}$ and a
sorted signature $\mathcal{F}=\mathcal{F}_{T}\uplus\mathcal{F}_{L}$ such that
$\mathcal{T}(\mathcal{F},\mathcal{V})$ denotes the set of terms over this
disjoint signature. Symbols in $\mathcal{F}_{T}$ are called _term symbols_ ,
while symbols in $\mathcal{F}_{L}$ are _theory symbols_. A term in
$\mathcal{T}(\mathcal{F}_{L},\mathcal{V})$ is a _theory term_. For a non-
variable term $t=f({t_{1}},\dots,{t_{n}})$, we write $\mathsf{root}(t)$ to
obtain the top-most symbol $f$. A _position_ $p$ is an integer sequence used
to identify subterms, and the subterm of $t$ at position $p$ is denoted
$t|_{p}$. We write $\mathcal{P}\mathsf{os}(t)$ for the set of positions in a
term $t$, and given a set of function symbols $\mathcal{F}^{\prime}$,
$\mathcal{P}\mathsf{os}_{\mathcal{F}^{\prime}}(t)$ are those positions
$p\in\mathcal{P}\mathsf{os}(t)$ such that $t|_{p}$ is rooted by a symbol in
$\mathcal{F}^{\prime}$. A _substitution_ $\sigma$ is a mapping from variables
to terms with finite domain, and $t\sigma$ denotes the application of $\sigma$
to a term $t$.

Theory terms $\mathcal{T}(\mathcal{F}_{L},\mathcal{V})$ have a fixed
semantics: we assume a mapping $\mathcal{I}$ that assigns to every sort
$\iota$ occurring in $\mathcal{F}_{L}$ a carrier set $\mathcal{I}(\iota)$.
Moreover, we assume that for every element $a\in\mathcal{I}(\iota)$ there is
exactly one constant symbol $c_{a}\in\mathcal{F}_{L}$, called a _value_. The
set of all value symbols is denoted $\mathcal{V}\mathsf{al}$. For instance, if
the sort of integers occurs in $\mathcal{F}_{L}$ then
$\mathcal{V}\mathsf{al}\subseteq\mathcal{F}_{L}$ contains a value $c_{i}$ for
every $i\in\mathbb{Z}$.

Moreover, we assume a fixed interpretation $\mathcal{J}$ that assigns to every
theory symbol $f\in\mathcal{F}_{L}$ a function $f_{\mathcal{J}}$ of
appropriate sort, and such that $(c_{a})_{\mathcal{J}}=a$ for value symbols
$c_{a}$, i.e., value symbols are interpreted as the represented element. The
interpretation $\mathcal{J}$ naturally extends to theory terms without
variables by setting
$[f({t_{1}},\dots,{t_{n}})]_{\mathcal{J}}=f_{\mathcal{J}}([t_{1}]_{\mathcal{J}},\dots,[t_{n}]_{\mathcal{J}})$.
In particular, we assume a sort $\mathsf{{bool}}$ such that
$\mathcal{I}(\mathsf{{bool}})=\\{\top,\bot\\}$ with values
$\mathcal{V}\mathsf{al}_{\mathsf{{bool}}}=\\{\mathsf{{true}},\mathsf{{false}}\\}$
such that $\mathsf{{true}}_{\mathcal{J}}=\top$, and
$\mathsf{{false}}_{\mathcal{J}}=\bot$. We also assume that $\mathcal{F}_{L}$
contains equality symbols $\mathrel{\approx}_{\iota}$ for every theory sort
$\iota$, and a symbol $\wedge$ interpreted as logical conjunction.

Theory terms of sort $\mathsf{{bool}}$ are called _constraints_ , and a
_constrained term_ is a pair $(t,\varphi)$ of a term $t$ and a constraint
$\varphi$. A substitution $\gamma$ is a _valuation_ if its range is a subset
of $\mathcal{V}\mathsf{al}$. A constraint $\varphi$ is _valid_ , denoted
$\models\varphi$, if $[\varphi\gamma]_{\mathcal{J}}=\top$ for all valuations
$\gamma$, and _satisfiable_ if $[\varphi\gamma]_{\mathcal{J}}=\top$ for some
valuation $\gamma$. We write $\psi\models\varphi$ if all valuations that
satisfy $\psi$ also satisfy $\varphi$.

#### Logically Constrained Rewriting.

A constrained rewrite rule is a triple $\ell\to r~{}[\varphi]$ where
$\ell,r\in\mathcal{T}(\mathcal{F},\mathcal{V})$, $\ell\not\in\mathcal{V}$,
$\varphi$ is a constraint, and $\mathsf{root}(\ell)\in\mathcal{F}_{T}$. If
$\varphi=\mathsf{{true}}$ then the constraint is omitted. For a rule
$\rho\colon\ell\to r~{}[\varphi]$ we use $lhs(\rho)=\ell$ and $rhs(\rho)=r$ to
denote its left- and right-hand sides, respectively. A set of constrained
rewrite rules is called a _logically constrained term rewrite system_ (_LCTRS_
for short). For an LCTRS $\mathcal{R}$, its _defined_ symbols
$\mathcal{F}_{\mathcal{D}}$ are all root symbols of left-hand sides, that is,
$\mathcal{F}_{\mathcal{D}}=\\{\mathsf{root}(\ell)\mid\ell\to
r~{}[\varphi]\in\mathcal{R}\\}$. In the remainder we assume that LCTRSs are
left-linear, that is, all variables occur at most once in the left-hand side
$\ell$ of a rule $\ell\to r~{}[\varphi]$.111Non-left-linear rules are rare in
practice; and moreover repeated occurrences of a variable $x$ in $\ell$ can be
substituted by a fresh variable $x^{\prime}$, adding $x\approx x^{\prime}$ to
$\varphi$. Though this implies that $x$ can only be substituted by theory
terms in rewrite sequences, for innermost evaluation this is not a limitation.
An LCTRS $\mathcal{R}$ is a _transition system_ if all rules in $\mathcal{R}$
are of the form $f({\ell_{1}},\dots,{\ell_{n}})\to
g({r_{1}},\dots,{r_{m}})~{}[\varphi]$ such that $f,g\in\mathcal{F}_{T}$, all
$\ell_{i}\in\mathcal{V}$, and all $r_{j}$ are in
$\mathcal{T}(\mathcal{F}_{L},\mathcal{V})$; if moreover the background theory
associated with $\mathcal{F}_{L}$ is the theory of integers then $\mathcal{R}$
is an _integer transition system_ (ITS).

The fixed rewrite system $\mathcal{R}_{\mathsf{calc}}$ is the (infinite) set
of rules $f({\ell_{1}},\dots,{\ell_{n}})\to u$ such that
$f\in\mathcal{F}_{L}\setminus\mathcal{V}\mathsf{al}$,
$\ell_{i}\in\mathcal{V}\mathsf{al}$ for all
$1\,{\leqslant}\,i\,{\leqslant}\,n$, and $u\in\mathcal{V}\mathsf{al}$ is the
value symbol of $[f({\ell_{1}},\dots,{\ell_{n}})]_{\mathcal{J}}$. A rewrite
step using $\mathcal{R}_{\mathsf{calc}}$ is called a _calculation step_ and
denoted $\to_{\mathsf{calc}}$. A _rule step_ $s\to_{\rho}^{\sigma}t$ using a
rule $\rho\colon\ell\to r\>[\varphi]$ and substitution $\sigma$ satisfies
$s=C[\ell\sigma]$, $t=C[r\sigma]$, and $\sigma$ respects $\varphi$; where a
substitution $\sigma$ is said to _respect_ a constraint $\varphi$ if
$\varphi\sigma$ is valid and $\sigma(x)\in\mathcal{V}\mathsf{al}$ for all
$x\in\mathcal{V}ar(\varphi)$. The substitution in the notation
$\to_{\rho}^{\sigma}$ is mostly omitted, and a rule step simply denoted
$\to_{\rho}$. For an LCTRS $\mathcal{R}$, we denote the relation
${\to_{\mathsf{calc}}}\cup{\\{\to_{\rho}\\}_{\rho\in\mathcal{R}}}$ by
$\to_{\mathcal{R}}$. The above rewrite step is _innermost_ , denoted
$\smash{s\overset{\mathsf{i}}{\to}_{\rho}t}$, if all proper subterms of
$\ell\sigma$ are in normal form with respect to $\to_{\mathcal{R}}$. Given
binary relations $R$ and $S$, we write $R/S$ for $S^{*}\cdot R\cdot S^{*}$.
For LCTRSs $\mathcal{R}$ and $\SS$ we abbreviate
$\smash{\overset{\mathsf{i}}{\to}_{\mathcal{R}}/\overset{\mathsf{i}}{\to}_{\SS}}$
by $\smash{\overset{\mathsf{i}}{\to}_{\mathcal{R}/\SS}}$, and
$\smash{\overset{\mathsf{i}}{\to}_{\mathcal{R}}/\to_{\mathsf{calc}}}$ by
$\smash{\overset{\mathsf{i}}{\to}_{\mathcal{R}/\mathsf{calc}}}$.

######  Example 4 (continued from Ex. 2)

The LCTRS $\mathcal{R}_{2}$ indicated in Ex. 2, expressing the predicate
max_length/3, makes use of the sorts $\mathsf{{int}}$, $\mathsf{{list}}$ and
$\mathsf{{bool}}$. Furthermore, $\mathcal{F}_{L}$ consist of symbols
$\mathrel{::}$ and $\mathsf{[]}$ for lists, $\cdot$, $+$, $-$, $\leqslant$,
and $\geqslant$ as well as values $n$ for all $n\in\mathbb{Z}$, with the usual
interpretations on $\mathbb{Z}$ and lists of integers. Then $\mathcal{R}$
admits the following rewrite steps:

$\displaystyle\mathsf{len}([\mathsf{1},\mathsf{2}],\mathsf{2})\to\mathsf{len}([\mathsf{2}],\mathsf{2}-\mathsf{1})\to_{\mathsf{calc}}\mathsf{len}([\mathsf{2}],\mathsf{1})\to\mathsf{len}([],\mathsf{1}-\mathsf{1})\to_{\mathsf{calc}}\mathsf{len}([],\mathsf{0})$

Note that in LCTRS rewriting, calculation steps like the subtractions in Ex. 4
are explicit in the $\to_{\mathsf{calc}}$ relation, in contrast to ITSs or
related formalisms [32], where simplification is implicit. Moreover, innermost
rewriting is a rather natural restriction for LCTRSs: By the definition of a
rule step using some rule $\rho$, variables in the constraint of $\rho$ need
to be substituted by values. Hence non-innermost steps are only possible if
nested redexes occur below unconstrained variables. For instance, in a term
$\mathsf{f}(\mathsf{f}(\mathsf{2}))$ only the inner $\mathsf{f}$ call
constitutes a redex for the rule $\mathsf{f}(x)\to x~{}[x>\mathsf{0}]$.

#### Algebras.

We assume mappings $|\cdot|_{\iota}:\mathcal{I}(\iota)\to\mathbb{N}$ for every
sort $\iota$, playing the role of norms to measure size. For instance, one
might take the absolute values for integers, the size function for arrays, and
the unsigned integer value for bit-vectors. The subscript $\iota$ in
$|t|_{\iota}$ is omitted if the sort of $t$ is clear from the context.

We consider well-founded algebras $\mathcal{A}$ over the natural numbers and
the Booleans, with interpretation functions $f^{\mathcal{A}}$ for all
$f\in\mathcal{F}_{T}\cup\mathcal{F}_{L}$, cf. [6, 37]. By $t^{\mathcal{A}}$ we
denote the interpretation of a term $t$ based on $\mathcal{A}$, and by
$[\alpha]_{\mathcal{A}}(t)$ the interpretation of $t$ based on $\mathcal{A}$
and valuation $\alpha$. In order to bound complexity, we use algebras that
incorporate the given complexity measures:

###### Definition 1

A _measure interpretation_ is given by an algebra $\mathcal{M}$ with carrier
$\mathbb{N}$, and measures $|\cdot|_{\iota}$ for all sorts $\iota$. The
interpretation $t^{\mathcal{M}}$ of a term $t$ is $|t|_{\iota}$ if
$t\in\mathcal{V}$ has sort $\iota$, and
$f^{\mathcal{M}}(t_{1}^{\mathcal{M}},\dots,t_{m}^{\mathcal{M}})$ if
$t=f({t_{1}},\dots,{t_{m}})$. In addition, we demand that
$f^{\mathcal{M}}([t_{1}]_{\mathcal{J}}^{\mathcal{M}},\dots,[t_{n}]_{\mathcal{J}}^{\mathcal{M}})\geqslant[f(t_{1},\dots,t_{n})]_{\mathcal{J}}^{\mathcal{M}}$
for all values ${t_{1}},\dots,{t_{n}}$.

In the following we suit interpretations (aka ranking functions) to LCTRSs.
The ternary relation $>_{[\cdot]}^{\mathcal{M}}$ is defined as
$s>_{[\varphi]}^{\mathcal{M}}t$ if and only if
$[\alpha]_{\mathcal{M}}(s)>[\alpha]_{\mathcal{M}}(t)$ is satisfied for all
valuations $\alpha$ that respect $\varphi$. Similarly,
$s\geqslant_{[\varphi]}^{\mathcal{M}}t$ if and only if
$[\alpha]_{\mathcal{M}}(s)\geqslant[\alpha]_{\mathcal{M}}(t)$ holds for all
valuations $\alpha$ that respect $\varphi$.

###### Definition 2

We call an LCTRS $\mathcal{R}$ _weakly compatible_ with a measure
interpretation $\mathcal{M}$ if $\ell\geqslant_{[\varphi]}^{\mathcal{M}}r$ for
all $\ell\to r~{}[\varphi]\in\mathcal{R}$, and _strictly compatible_ if
$\mathcal{R}$ is weakly compatible and in addition
$\ell>_{[\varphi]}^{\mathcal{M}}r$ for some $\ell\to
r~{}[\varphi]\in\mathcal{R}$.

###### Example 5

Consider the measure interpretation $\mathcal{M}$ such that
$\mathsf{m}_{3}^{\mathcal{M}}(x,y,z)=y$,
$\mathsf{merge}^{\mathcal{M}}(x,y,z)=x$, $x+^{\mathcal{M}}y=x+_{\mathbb{N}}y$,
$x-^{\mathcal{M}}y=\max(x-_{\mathbb{N}}y,0)$, $\geqslant^{\mathcal{M}}$ is
$\geqslant^{\mathbb{N}}$, and $v^{\mathcal{M}}=\max(v,0)$ for all
$v\in\mathbb{Z}$. The LCTRS $\mathcal{R}^{\prime}$ consisting of the rules
(2), (4), and (8) from Ex. 1 is strictly compatible with $\mathcal{M}$, since
the rules (2) and (8) are weakly decreasing, while (4) is strictly decreasing.

##  4 Complexity Framework

An LCTRS $\mathcal{R}$ is _terminating_ if $\to_{\mathcal{R}}$ is well-
founded. In applications like static analysis, termination of a program is
often not enough and more precise resource guarantees are needed. In this
section we propose suitable runtime complexity notions for LCTRSs.

Following common notions in complexity analysis [4], the _derivation height_
of a term $t$ wrt. a binary relation $\to$ is defined as follows:
$\mathsf{dh}(t_{0},\to)\mathrel{:=}\sup\,\\{k\mid\exists\,t_{1},\dots,t_{k}.\
t_{0}\to\dots\to t_{k}\\}$. We assume that an LCTRS $\mathcal{R}$ is
associated with a unique _initial state_ $(t_{0},\varphi_{0})$ such that
$\varphi_{0}$ is a constraint and $t_{0}=\mathsf{init}(\overline{x})$ is the
_initial term_ , for a vector of _input variables_
$\overline{x}=({x_{1}},\dots,{x_{n}})$ and a function symbol $\mathsf{init}$
that does not occur on any right-hand side. The intention is that we consider
only rewrite sequences starting at $t_{0}\sigma$, such that $\sigma$ is a
valuation that respects $\varphi_{0}$. Sometimes $s_{0}$ will be used as a
shorthand for $(t_{0},\varphi_{0})$.

For $\overline{u},\overline{v}\in\mathbb{N}^{k}$, let
$\overline{u}\leqslant_{k}\overline{v}$ abbreviate
$\bigwedge_{i=1}^{k}u_{i}\leqslant v_{i}$. Given
$\overline{t}=({t_{1}},\dots,{t_{k}})$, $|\overline{t}|$ denotes
$(|t_{1}|,\dots,|t_{k}|)$, and $\overline{t}\sigma$ denotes
$(t_{1}\sigma,\dots,t_{k}\sigma)$ for any substitution $\sigma$. For a term
$t$, we write $\overline{\mathcal{V}ar}(t)$ for a vector containing
$\mathcal{V}ar(t)$ in a fixed order.

###### Definition 3

For an LCTRS $\mathcal{R}$ and a constrained term $(t,\varphi)$ such that
$\overline{x}=\overline{\mathcal{V}ar}(t)$, the (innermost) _runtime
complexity_
$\mathsf{rc}_{\mathcal{R}}^{(t,\varphi)}\colon\mathbb{N}^{n}\to\mathbb{N}\cup\\{\omega\\}$
is defined as

$\mathsf{rc}_{\mathcal{R}}^{(t,\varphi)}(\overline{m})=\sup\>\\{\mathsf{dh}(t\sigma,\overset{\mathsf{i}}{\to}_{\mathcal{R}/\mathsf{calc}})\mid\>|\overline{x}\sigma|\leqslant_{n}\overline{m}\text{
for some $\sigma$ that respects }\varphi\\}.$

Thus, the runtime complexity of an LCTRS is the maximal number of innermost
_rule_ steps in a rewrite sequence that starts with a size-bounded instance of
the initial state $(t,\varphi)$; calculation steps are not counted. This is
common in cost analysis, it also corresponds to the runtime complexity of a
program or ITS [8], where the number of transitions are counted but not
simplifications of expressions.

_Dependency pairs_ are commonly used in termination and complexity analysis of
rewrite systems. For termination of LCTRSs they were already used in earlier
work [27]. For complexity analysis, stronger notions were developed for
standard rewriting: _dependency tuples_ (DTs) [34], _weak_ [25], and _grouped_
dependency pairs [4]. Since we consider innermost rewriting, we can use an
LCTRS variant of dependency tuples. To that end, for every defined symbol $f$
we consider a fresh symbol $f^{\sharp}$, and for a term
$t=f({t_{1}},\dots,{t_{n}})$ write $t^{\sharp}$ to denote
$f^{\sharp}({t_{1}},\dots,{t_{n}})$.

###### Definition 4

Consider a rule $\rho\colon\ell\to r~{}[\varphi]$ such that
$\mathcal{P}\mathsf{os}_{\mathcal{F}_{\mathcal{D}}}(r)$ is sorted as
${p_{1}},\dots,{p_{k}}$ with respect to a fixed order on positions. Then the
_dependency tuple_ $\mathsf{DT}(\rho)$ of $\rho$ is the constrained rule
$\ell^{\\#}\to\langle(r|_{p_{1}})^{\\#},\dots,(r|_{p_{k}})^{\\#}\rangle_{k}~{}[\varphi]$.
For an LCTRS $\mathcal{R}$,
$\mathsf{DT}(\mathcal{R})=\bigcup_{\rho\in\mathcal{R}}\mathsf{DT}(\rho)$.

Here $\langle\dots\rangle_{k}$ is a fresh tuple symbol for every arity $k$
(but the subscript will be dropped for simplicity).

######  Definition 5 (Dependency Graph)

Let $\mathcal{R}$ be an LCTRS and
$\mathcal{D}\subseteq\mathsf{DT}(\mathcal{R})$. The _dependency graph_ (DG) is
the directed graph with node set $\mathcal{D}$ and edges from
$s^{\\#}\to\langle{t^{\\#}_{1}},\dots,{t^{\\#}_{n}}\rangle~{}[\varphi]$ to
$u^{\\#}\to v~{}[\psi]$ if there is some $t_{i}^{\\#}$ such that
$t_{i}^{\\#}\sigma\to_{\mathcal{R}}^{*}u^{\\#}\tau$, for some substitutions
$\sigma$ and $\tau$ and some $i$, $1\leqslant i\leqslant n$.

The DG is not computable in general, but approximation techniques are well-
known [27, 34, 5, 22]. For instance, the graph in Sect. 2 constitutes a
dependency graph approximation for the LCTRS from Ex. 1. Following Noschiniski
et al. [34], we assume particular interpretation functions for the tuple
operators $\langle\dots\rangle$. To this end, let a _DT-measure
interpretation_ $\mathcal{M}$ be a measure interpretation that interprets
$\langle{t_{1}},\dots,{t_{k}}\rangle^{\mathcal{M}}=t_{1}+\dots+t_{k}$, for all
$k\geqslant 0$.

Let the set of _bound expressions_ UB be inductively defined as follows: (i)
$|x|_{\iota}\in\textup{UB}$ for $x\in\mathcal{V}$ of sort $\iota$, (ii)
$\mathbb{Z}\subseteq\textup{UB}$ and $\omega\in\textup{UB}$, (iii) if
$p,q\in\textup{UB}$ then $p+q$, $pq$, and $max(p,q)$ are in UB, and (iv) if
$p\in\textup{UB}$ and $k\in\mathbb{N}$ then $k^{p}$, $p/k$, and $\log_{k}(p)$
are in UB. Given $p,q\in\textup{UB}$, we write $p\leqslant q$ if
$[\alpha]_{\mathbb{N}}(p)\leqslant[\alpha]_{\mathbb{N}}(q)$ for all
substitutions $\alpha\colon\mathcal{V}\to\mathbb{N}$. For a bound expression
$p\in\textup{UB}$ and $\overline{m}\in\mathbb{N}^{n}$ we also write
$p(\overline{m})$ to denote the substituted bound expression
$p[m_{i}/x_{i}]_{1\leqslant i\leqslant n}$, assuming
$\overline{x}\in\mathcal{V}^{n}$ are the variables in the initial term
$t_{0}=\mathsf{init}(\overline{x})$.

A triple $P=((t,\varphi),\mathcal{D},\mathcal{R})$ of a constrained term
$(t,\varphi)$, a set of DTs $\mathcal{D}$, and an LCTRS $\mathcal{R}$ is
called a _(complexity) problem_. Following Brockschmidt et al. [8], we next
define time and size bound approximations.

###### Definition 6

For a complexity problem $((t,\varphi),\mathcal{D},\mathcal{R})$ with
$\overline{x}=\overline{\mathcal{V}ar}(t)$, a function
$T\colon\mathcal{D}\to\textup{UB}$ is a _runtime approximation_ if, for all
$\rho\in\mathcal{D}$ and $\overline{m}\in\mathbb{N}^{n}$,

$T(\rho)(\overline{m})\geqslant\sup\>\\{\mathsf{dh}(t\sigma,\overset{\mathsf{i}}{\to}_{\\{\rho\\}/\mathcal{D}\cup\mathcal{R}})\mid|\overline{x}\sigma|\leqslant_{n}\overline{m}\text{
and $\sigma$ respects }\varphi\\}.$

In words, a runtime approximation $T(\rho)$ over-approximates how often a DT
$\rho\in\mathcal{D}$ can be used in a rewrite sequence starting from the
initial state, expressed in terms of the input variables. For instance,
consider Ex. 1 and let $(1^{\\#})$ be the DT corresponding to rule $(1)$. Then
the function $T$ such that $T(1^{\\#})=1$ and
$T(\rho)(|x_{0}|,|y_{0}|,|z_{0}|)=|x_{0}|^{2}$ for all other DTs
$\rho\in\mathcal{D}$ is a valid (though not optimal) runtime approximation.

For a complexity problem $((t,\varphi),\mathcal{D},\mathcal{R})$, the set of
_entry variables_ EV is the set of all tuples $(\rho,y)$ such that
$\rho\in\mathcal{D}$ and $y\in\mathcal{V}ar(lhs(\rho))$.

###### Definition 7

For a complexity problem $((t,\varphi),\mathcal{D},\mathcal{R})$ with
$\overline{x}=\overline{\mathcal{V}ar}(t)$, a function
$S\colon\textup{EV}\to\textup{UB}$ is a _size approximation_ if

$S(\rho,y)(\overline{m})\geqslant\sup\>\\{|y\tau|\mid\exists\sigma,\>u.\
t\sigma\overset{\mathsf{i}}{\to}_{\mathcal{R}\cup\mathcal{D}}^{*}\cdot\overset{\mathsf{i}}{\to}_{\rho}^{\tau}u\text{,
}|\overline{x}\sigma|\leqslant_{n}\overline{m}\\}$

for $(\rho,y)\in\textup{EV}$ such that substitution $\sigma$ respects
$\varphi$, and $\overline{m}\in\mathbb{N}^{n}$.

A size approximation over-approximates how large a variable in the left-hand
side of a rule in $\mathcal{D}$ can get in a rewrite sequence from the initial
state, again expressed in terms of the input variables. A tuple $(T,S)$ is a
_bound approximation_ for a complexity problem $P$ if $T$ and $S$ are runtime
and size approximations for $P$. We next define a complexity framework in the
spirit of Avanzini and Moser [4].

###### Definition 8

Given a complexity problem $P=(s_{0},\mathcal{D},\mathcal{R})$, a
_(complexity) judgement_ is a statement ${\vdash\,}{P}\colon{(T,S)}$, for
functions $T:\mathcal{D}\to\textup{UB}$ and $S:\textup{EV}\to\textup{UB}$. The
judgement is _valid_ if $(T,S)$ is a bound approximation for $P$. A
_complexity processor_ is an inference rule on complexity judgements of the
following form:

$\frac{{\vdash\,}{P_{1}}\colon{(T_{1},S_{1})},\dots,{\vdash\,}{P_{k}}\colon{(T_{k},S_{k})}}{{\vdash\,}{P}\colon{(T,S)}}\quad\mathsf{Proc}$

and it is _sound_ if ${\vdash\,}{P}\colon{(T,S)}$ is valid whenever all
${\vdash\,}{P_{i}}\colon{(T_{i},S_{i})}$ are valid.

For a problem $P=(s_{0},\mathcal{D},\mathcal{R})$ with initial state
$s_{0}=(\mathsf{init}(\overline{x}),\varphi)$, a DT $\ell\to
r~{}[\psi]\in\mathcal{D}$ is _initial_ if
$\mathsf{root}(\ell)=\mathsf{init}^{\\#}$. The _initial processor_ for $P$ is
given by

$\frac{}{{\vdash\,}{P}\colon{(T,S_{\omega})}}\quad\mathsf{Initial}$

where $T(\rho)=1$ if $\rho$ is initial and $T(\rho)=\omega$ otherwise; and
$S_{\omega}(\rho,x)=\omega$ for all $(\rho,x)\in\textup{EV}$. Since
$\mathsf{init}^{\\#}$ does not occur on any right-hand side by assumption, the
processor Initial is sound. For instance, the DT
$\mathsf{init}^{\\#}(x,y,z)\to\mathsf{m}^{\\#}(x,y,z)$ originating from rule
(1) in Ex. 1 is initial. For a problem $P=(s_{0},\mathcal{D},\mathcal{R})$ and
an expression $C\in\textup{UB}$, we sometimes write
${\vdash\,}{P}\colon{((C)_{\Sigma},S)}$ to express that there is a runtime
approximation $T$ such that ${\vdash\,}{P}\colon{(T,S)}$ and
$C=\sum_{\rho\in\mathcal{D}}T(\rho)$.

The next result states that valid judgements bound the runtime complexity of
LCTRSs. It can be proven in a similar way as [4, Theorem 6], using the
properties of dependency tuples for innermost rewriting.

###### Theorem 4.1

If an LCTRS $\mathcal{R}$ with initial state $(t,\varphi)$ admits the valid
judgement
${\vdash\,}{((t^{\\#},\varphi),\mathsf{DT}(\mathcal{R}),\mathcal{R}\cup\mathcal{R}_{\mathsf{calc}})}\colon{(T,S)}$
then
$\mathsf{rc}^{(t,\varphi)}_{\mathcal{R}}\leqslant\sum_{\rho\in\mathsf{DT}(\mathcal{R})}T(\rho)$
holds.

##  5 Processors

This section presents processors that implement the complexity framework from
Sect. 4, in particular showing how the respective ITS techniques [8] carry
over.

### Interpretation Processors.

Compatible interpretations are a standard tool in resource analysis, cf. [34,
4, 8]. We first present a processor using a measure interpretation that
orients _all_ rules and DTs (cf. [8, Theorem 3.6]). For $p\in\textup{UB}$, let
$[p]$ denote the bound expression obtained from $p$ by replacing all
coefficients in $p$ by their absolute values (such that the resulting
expression is weakly monotone).

###### Lemma 1

Let $P=((t_{0},\varphi_{0}),\mathcal{D},\mathcal{R})$ and $\mathcal{M}$ a
$\mathsf{DT}$-measure interpretation with which $\mathcal{R}$ is weakly, and
$\mathcal{D}$ is strictly compatible. Then the following processor is sound,
where $T^{\prime}(\rho)=[(t_{0})^{\mathcal{M}}]$ for all
$\rho\in\mathcal{D}_{>}$, and $T^{\prime}(\rho)=T(\rho)$ otherwise:

$\frac{{\vdash\,}{P}\colon{(T,S)}}{{\vdash\,}{P}\colon{(T^{\prime},S)}}\quad\mathsf{Interpretation}$

For instance, for Ex. 1 one can take the interpretation $\mathcal{M}$ such
that $\mathsf{split}^{\mathcal{M}}=0$ and $f^{\mathcal{M}}=1$ for all other
$f\in\mathcal{F}_{T}$, and symbols in $\mathcal{F}_{L}$ are interpreted as in
Ex. 5. $\mathcal{R}_{1}$ is strictly compatible since all rules are weakly and
rule (5) is strictly decreasing. This justifies a runtime approximation
setting by $T(5^{\\#})=1=\mathsf{init}^{\\#}(\overline{x})^{\mathcal{M}}$.

Next, we adapt [8, Theorem 3.6] to our setting, by which runtime bounds can be
obtained using an interpretation that orients the given LCTRS _partially_. For
a dependency graph $G$ and some $\mathcal{D}^{\prime}\subseteq\mathcal{D}$,
let $\mathsf{pre}(\mathcal{D}^{\prime})$ be the set of all edges
$(\rho_{1},\rho_{2})$ in $G$, such that
$\rho_{1}\in\mathcal{D}\setminus\mathcal{D}^{\prime}$ and
$\rho_{2}\in\mathcal{D}^{\prime}$. Moreover, for a DT $\rho$ with
$\overline{\mathcal{V}ar}(lhs(\rho))=(y_{1},\dots,y_{k})$, let
$\overline{S}_{\rho}$ denote $(S(\rho,y_{1}),\dots,S(\rho,y_{k}))$.

###### Lemma 2

Suppose $P=(s_{0},\mathcal{D},\mathcal{R})$ is a complexity problem such that
$\mathcal{D}^{\prime}\subseteq\mathcal{D}$ has no initial DTs, $\mathcal{R}$
is weakly, and $\mathcal{D}^{\prime}$ is strictly compatible with a
$\mathsf{DT}$-measure interpretation $\mathcal{M}$. Then the following
processor is sound:

$\frac{{\vdash\,}{P}\colon{(T,S)}}{{\vdash\,}{P}\colon{(\lambda\rho.\left\\{\begin{array}[]{ll}\sum_{(\gamma,\delta)\in\mathsf{pre}(\mathcal{D}^{\prime})}T(\gamma)\cdot[lhs(\delta)^{\mathcal{M}}](\overline{S}_{\delta})&\text{
if }\rho\in\mathcal{D}^{\prime}_{>}\\\ T(\rho)&\text{
otherwise}\end{array}\right\\},S)}}\quad\mathsf{TimeBounds}$

where $\mathcal{D}^{\prime}_{>}$ is the set of rules $\ell\to r~{}[\varphi]$
in $\mathcal{D}^{\prime}$ such that $\ell>_{[\varphi]}^{\mathcal{M}}r$.

Next, we define a proceessor to compute size approximations.

### Size Bounds.

Size approximations were developed for ITSs and tend to be less precise for
LCTRSs due to nested terms. However, in many practical examples, a sufficient
approximation is feasible. Next, we thus adapt the relevant notions to the
LCTRS setting. First, the _local size approximation_ overapproximates the size
of entry variables in terms of variable sizes in predecessor rules.

###### Definition 9

For $\delta,\rho\in\mathcal{D}$ and $(\rho,y)\in\textup{EV}$, let
$S_{\delta\to\rho}\colon\mathcal{V}\to\textup{UB}$ be a _local size
approximation_ if

$S_{\delta\to\rho}(y)(\overline{m})\geqslant\sup\>\\{|y\tau|\mid\exists
t,\sigma.\ \ell\sigma\to_{\delta}^{\sigma}\cdot\to_{\rho}^{\tau}t\text{ and
}\overline{z}\sigma\leqslant_{n}\overline{m}\\}$

where $\ell=lhs(\delta)$, $\overline{z}=\overline{\mathcal{V}ar}(\ell)$, and
$\sigma$ is a valuation.

The intention is that for an entry variable $(\rho,y)$, such that $y$ occurs
in the left-hand side of $\rho$, the expression $S_{\delta\to\rho}(y)$ upper-
bounds $y$ in terms of the variables in $\delta$, for the case where $\rho$ is
applied after $\delta$. While such an expression is not always computable, it
can often be over-approximated. For instance, in Ex. 1 a local size
approximation $S_{(9)\to(2)}(y)$ could be $(|x|+1)/2$ or $|x|$: the subterm
$\smash{\mathsf{m}_{3}^{\\#}(x,u,v)}$ on the right-hand side of (9) matches
the left-hand side of $(2)$, instantiating the variable $y$ by $u$, and the
side condition of (9) ensures $x+1\geqslant 2u$. We next define the _entry
variable graph_ to track the dependence of entry variables on each other. For
$f\in\textup{UB}$, let $\mathcal{V}ar(f)$ be the set of all variables
occurring in $f$.222For more precision one could restrict to _active_
variables, as done in [8].

###### Definition 10

An _entry variable graph_ $G_{\textup{EV}}$ for
$(s_{0},\mathcal{D},\mathcal{R})$ with DG $G$ has node set
$\textup{EV}(\mathcal{D})$, and there is an edge from $(\delta,z)$ to
$(\rho,y)$ labeled $S_{\delta\to\rho}(y)$ if $G$ has an edge from $\delta$ to
$\rho$ and $z\in\mathcal{V}ar(S_{\delta\to\rho}(y))$.

We illustrate the concept on our running example.

###### Example 6

Consider again Ex. 1. We first apply _chaining_ , a standard technique in
termination an complexity analysis [15, 5], to compress the cycles
$(9)-(3)-(9)$ and $(9)-(7)-(9)$ into single-step cycles, such that (9) is
replaced by

$\displaystyle\mathsf{m}(x,y,z)$
$\displaystyle\to\langle\mathsf{m}_{0}(x,u,v),\mathsf{m}(u,u,v),\mathsf{m}(v,u,v),\mathsf{m}_{3}(x,u,v)\rangle\
[\psi]$ $\displaystyle\psi$ $\displaystyle=x\geqslant 2\wedge u\geqslant
0\wedge v\geqslant 0\wedge x+1\geqslant 2u\wedge 2u\geqslant x\wedge
x\geqslant 2v\wedge 2v+1\geqslant x.$

Then we obtain the following entry variable graph:

$1,x$$1,y$$1,z$$9,x$$9,y$$9,z$$2,x$$2,y$$2,z$$5,x$$5,y$$5,z$$6,x$$6,y$$6,z$$4,x$$4,y$$4,z$$8,x$$8,y$$8,z$

where a triple arrow $a$ $b$ means that there are arrows from $(a,x)$ to
$(b,x)$, $(a,y)$ to $(b,y)$, and $(a,z)$ to $(b,z)$. For all
$(a,u)\in\textup{EV}$, all outgoing edges from $(a,u)$ can be labelled $|u|$,
though more precise approximations are possible.

Next, we use the entry variable graph $G_{\textup{EV}}$ to obtain size bound
refinements, following the approach of [8]. To that end, we define two
processors $S_{triv}$ and $S_{scc}$ that refine bounds for trivial and non-
trivial SCCs in $G_{\textup{EV}}$, respectively. Here, an SCC is _trivial_ if
it consists of a single node without an edge to itself.

###### Definition 11

For size bounds $S$, we define $S_{triv}$ as follows:  (i)
$S_{triv}(\rho,y)=|y|$if $\rho$ is initial;  (ii)
$S_{triv}(\rho,y)=\max\\{\alpha(\overline{S}_{\delta})\mid(\delta,z)\to^{\alpha}(\rho,y)\text{
in }G_{\textup{EV}}\\}$, if $(\rho,y)$ is not in any non-trivial SCC of
$G_{\textup{EV}}$;  (iii) otherwise $S_{triv}(\rho,y)=S(\rho,y)$.

We distinguish three types of edges in $G_{\textup{EV}}$, by partitioning
their labels into the three sets $E_{=}$, $E_{+}$, and $E_{\times}$: for an
edge labelled $\alpha$,  (i) $\alpha\in E_{=}$if
$\alpha=a_{\alpha}\in\mathbb{N}$ or $\alpha=|x|$ for some $x\in\mathcal{V}$;
(ii) $\alpha\in E_{+}$if $|x|+a_{\alpha}\geqslant\alpha$ for some
$x\in\mathcal{V}$ and $a_{\alpha}\in\mathbb{N}$;  (iii) $\alpha\in
E_{\times}$if $c+\sum_{x\in\mathcal{X}}a_{x}|x|\geqslant\alpha$ for
$c,a_{x}\in\mathbb{N}$ and $\mathcal{X}\subseteq\mathcal{V}$.  For an SCC $C$
in $G_{\textup{EV}}$, let $C_{\alpha}$ denote the set of edge labels $\alpha$
of edges in $C$. For an entry variable graph $G_{\textup{EV}}$, let
$\mathsf{pre}(\rho,y)$ be the set of all direct predecessors of $(\rho,y)$ in
$G_{\textup{EV}}$.

###### Definition 12

Let $(T,S)$ be a bound approximation and $C$ a non-trivial SCC in
$G_{\textup{EV}}$. Then $S_{scc}$ is defined as  (i) if $C_{\alpha}\subseteq
E_{=}$ then $S_{scc}(\rho,y)=max\\{\alpha\mid\alpha\in C_{\alpha}\\}$,  (ii)
if $C_{\alpha}\subseteq E_{+}$ then let
$\alpha_{pre}=max\\{S(\rho^{\prime},z)\mid(\rho^{\prime},z)\in\mathsf{pre}(\rho,y)\setminus
C\\}$ and
$S_{scc}(\rho,y)=max(\\{\alpha_{pre}\\}\cup\\{a_{\alpha}\mid\alpha\in
C_{\alpha}\\})+\sum_{\rho\in\mathcal{D}}T(\rho)\cdot
max\\{a_{\alpha}\mid\alpha\in C\setminus E_{=}\\}$ (iii) and
$S_{scc}(\rho,y)=S(\rho,y)$ otherwise,  for all $\rho\in C$ and
$(\rho,y)\in\textup{EV}$.

Both $S_{triv}$ and $S_{scc}$ are similar to the bounds developed in [8],
though we omitted the case for $E_{\times}$ for reasons of space. We obtain
soundness by similar proofs.

###### Lemma 3

The following processors are sound:

$\frac{\parbox{128.0374pt}{${\vdash\,}{(s_{0},\mathcal{D},\mathcal{R})}\colon{(T,S)}$}}{\parbox{128.0374pt}{${\vdash\,}{(s_{0},\mathcal{D},\mathcal{R})}\colon{(T,S_{triv})}$}}\quad\frac{\parbox{128.0374pt}{${\vdash\,}{(s_{0},\mathcal{D},\mathcal{R})}\colon{(T,S)}$}}{\parbox{128.0374pt}{${\vdash\,}{(s_{0},\mathcal{D},\mathcal{R})}\colon{(T,S_{scc})}$}}\quad\mathsf{Size\
Bounds}$

##  6 Processors for Splitting and Loop Summary

In this section we present new processors to decompose a problem into
subproblems, as well as to analyse loops based on recurrence relations.

### Splitting.

We first consider a processor that allows to decompose a problem of a certain
shape into two subproblems. To that end, let a subgraph be _forward closed_ if
it is closed under successors.

###### Definition 13

Consider a problem $P=(s_{0},\mathcal{D},\mathcal{R})$ whose DG $G$ exhibits
subgraphs $G_{0}$ and $G_{1}$ with node sets $\mathcal{D}_{0}$ and
$\mathcal{D}_{1}$, respectively, such that
$\mathcal{D}=\mathcal{D}_{0}\uplus\mathcal{D}_{1}$, all initial DTs of $P$ are
in $\mathcal{D}_{0}$, and $G_{1}$ is forward closed. Then
$(\mathcal{D}_{0},\mathcal{D}_{1})$ is a _splitting_ for $P$.

A splitting thus decomposes a problem according to the scheme illustrated in
Fig. 1(a).

$\delta_{1}$$\delta_{2}$$\delta_{m}$$\gamma_{1}$$\gamma_{2}$$\gamma_{m}$$\cdot$$\cdot$$\cdot$$\cdot$$\cdot$$\cdot$$\mathcal{D}_{0}$$\mathcal{D}_{1}$$\dots$
(a) splitting

$\delta$$\gamma_{1}$$\gamma_{2}$$\gamma_{m}$$\cdot$$\cdot$$\cdot$$\mathcal{D}^{\prime}$$\dots$$1,\dots,p$
(b) recurrence

Figure 1: Problems of special shapes.

The idea is that we first analyse the subproblems $P_{0}$ and $P_{1}$
corresponding to $\mathcal{D}_{0}$ and $\mathcal{D}_{1}$ separately,
considering as initial states for $P_{1}$ all possible entry points
$\gamma_{i}$. For DTs in $\mathcal{D}_{0}$ their time bounds in $P_{0}$
constitute overall time bounds since $G_{1}$ is forward closed; on the other
hand, for every $\rho\in\mathcal{D}_{1}$, we compute time bounds via each
entry point $\gamma_{i}$, and obtain an overall time bound by taking the sum
over all $\gamma_{i}$. To that end, given $\gamma_{i}$, the time bound for
$\rho$ in $P_{1}$ is applied to the size bound for $\gamma_{i}$, and
multiplied by the time bound for the respective $\delta_{i}$, which upper-
bounds the number of applications of $\delta_{i}$ followed by $\gamma_{i}$.

###### Lemma 4

If $(s_{0},\mathcal{D},\mathcal{R})$ is a problem with splitting
$(\mathcal{D}_{0},\mathcal{D}_{1})$ such that
$\mathsf{pre}(\mathcal{D}_{1})=\\{(\delta_{i},\gamma_{i})\mid
1\,{\leqslant}\,i\,{\leqslant}\,m\\}$ and $\gamma_{i}=(\ell_{i}\to r_{i}\
[\varphi_{i}])$, the following processor is sound:

$\frac{{\vdash\,}{P}\colon{(T,S)}\quad\
{\vdash\,}{(s_{0},\mathcal{D}_{0},\mathcal{R})}\colon{(T_{0},S_{0})}\quad\
\bigwedge_{i=1}^{m}{\vdash\,}{((\ell_{i},\varphi_{i}),\mathcal{D}_{1},\mathcal{R})}\colon{(T_{i},S_{i})}}{{\vdash\,}{P}\colon{(\lambda\rho.\left\\{\begin{array}[]{ll}T_{0}(\rho)&\text{
if }\rho\in\mathcal{D}_{0}\\\ \sum_{i=1}^{m}T_{0}(\delta_{i})\cdot
T_{i}(\rho)(\overline{S}_{\gamma_{i}})&\text{ if
}\rho\in\mathcal{D}_{1}\end{array}\right\\},S)}}\quad\mathsf{Split}$

Several improvements are conceivable, for instance the conditions of the
initial states $(\ell_{i},\varphi_{i})$ could be strengthened using
reachability analysis in the DG.

### Summarising Self-Loops.

We next propose a technique for the analysis of (sub)problems whose DG is of
the shape shown in Fig. 1(b). For vectors $\overline{a},\overline{b}$, let
$\overline{a}>_{k}\overline{b}$ be a shorthand for the expression
$\overline{a}\geqslant_{k}\overline{b}\wedge(\bigvee_{j}a_{j}>b_{j})$.

###### Definition 14

Let $P=((f(\overline{x}),\varphi),\mathcal{D},\mathcal{R})$ with DG $G$ such
that $\mathcal{D}$ can be written as
$\mathcal{D}=\\{\delta\\}\uplus\mathcal{D}^{\prime}$, the graph
$G|_{\mathcal{D}^{\prime}}$ is forward-closed in $G$, and $\delta$ is of the
form:

$f(\overline{x})\to\langle
f(\overline{r}_{1}),\dots,f(\overline{r}_{p}),lhs(\gamma_{1}),\dots,lhs(\gamma_{m})\rangle\quad[\psi]$
(2)

for $\\{\gamma_{1},\dots,\gamma_{m}\\}\subseteq\mathcal{D}^{\prime}$, such
that
$\overline{x},\overline{r}_{i}\in\mathcal{T}(\mathcal{F}_{L},\mathcal{V})^{k}$
and $\varphi\wedge\psi\models|\overline{x}|>_{k}|\overline{r}_{i}|$ for all
$1\,{\leqslant}\,i\,{\leqslant}\,p$. If there is moreover some
$\overline{b}\in(\mathbb{N}\,{\cup}\,\\{-\infty\\})^{k}$ such that
$\varphi\wedge\psi\models|\overline{x}|\geqslant_{k}\overline{b}$, then $P$ is
_cyclic_ with _termination condition_ $\overline{b}$.

###### Lemma 5

Let $P=(s_{0},\mathcal{D},\mathcal{R})$ be a cyclic complexity problem with
termination condition $\overline{b}$ and a DT $\delta$ of the form (2), and
let $\gamma_{i}=(\ell_{i}\to r_{i}\ [\varphi_{i}])$, for all $i$,
$1\,{\leqslant}\,i\,{\leqslant}\,m$. Then the following processor is sound:

$\frac{{\vdash\,}{P}\colon{(T,S)}\quad\bigwedge_{i=1}^{m}{\vdash\,}{((\ell_{i},\varphi_{i}),\mathcal{D}^{\prime},\mathcal{R})}\colon{(T_{i},S_{i})}}{{\vdash\,}{(s_{0},\mathcal{D},\mathcal{R})}\colon{(F(\overline{x})_{\Sigma},S)}}\quad\mathsf{Recurrence}$

where $F$ is a solution to a recurrence
$f(\overline{x})=f(\overline{r}_{1})+\ldots+f(\overline{r}_{p})+H(\overline{x})$,
$f(\overline{b})=0$ for some
$H(\overline{x})\geqslant\sum_{\rho\in\mathcal{D}^{\prime}}\sum_{i=1}^{m}T_{i}(\rho)(\overline{S}_{\gamma_{i}})$.

This processor is key to analyse the main loop in our running example.

###### Example 7

Consider Ex. 1 with chaining as applied in Ex. 6. For the subproblems
$P_{1}=(\mathsf{m}_{0}^{\\#}(x,u,v),\psi),\mathcal{D},\mathcal{R})$ and
$P_{2}=(\mathsf{m}_{3}^{\\#}(x,u,v),\psi),\mathcal{D},\mathcal{R})$ the
judgements ${\vdash\,}{P_{1}}\colon{((x+1)_{\Sigma},S)}$ and
${\vdash\,}{P_{2}}\colon{(u+v+1)_{\Sigma},S)}$ are valid, so we can set

$H(x,u,v)=2|x|+1\geqslant x+u+v+1$ since $u,v\leqslant x/2$. Thus, we solve
the recurrence (1) given in Sect. 2. According to one of the cases of the
Master Theorem, (1) has a solution in $\mathcal{O}(|x|\cdot\log(|x|))$ which
is a complexity approximation according to Lem. 5.

To simplify the presentation, we only considered cycles formed by a single DT,
as indicated in Fig. 1(b). The result generalizes to longer cycles, but
chaining can often reduce these cases to the simpler situation discussed here.

##  7 Evaluation

To evaluate the viability of the presented framework, we prototyped our
approach in the complexity analyser TCT [5].

#### Implementation.

We added a new module tct-lctrs to the TCT tool suite, below we call the
resulting tool TCT-LCTRS.333The code is available from
https://github.com/bytekid/tct-lctrs. It currently supports the theory of
integers, as well as some operations on lists. All processors described in
this paper are implemented, using the modular processor framework of TCT. They
are arranged in the following strategy, where the loop indicates exhaustive
repetition:

dependency
---
tuples
simpsize boundstime boundssimpchainsplitrecurrence

We mention some implementation aspects that seem noteworthy.

  * •

The simp processor combines some straightforward simplification processors:
unsatisfiable paths, unreachable rules, and unused arguments are eliminated,
and leaves in the DG obtain their time bound from their predecessors.

  * •

Suitable algebras instantiating the interpretation and time bounds processors
(Lems. 1 and 2) are searched for by means of an SMT encoding, as done in the
ITS module of TCT previously using well-known techniques [35, 7].

  * •

Before applying the recurrence processor, TCT first applies chaining to obtain
loops that involve only a single DT (see Appendix B for details).

  * •

In the recurrence processor (Lem. 5),TCT first attempts to solve subproblems
corresponding to the functions ${h_{1}},\dots,{h_{m}}$ separately, obtaining
bound approximations $(T_{i},S_{i})$ for all $i$, $1\leqslant i\leqslant m$
(see the notation of Lem. 5). Then, it is checked whether a function $H$
corresponding to one of the known recursion patterns satisfies
$H(\overline{x})\geqslant\sum_{i}\sum_{\rho\in\mathcal{D}^{\prime}}T_{i}(\rho)$
using an SMT call.

  * •

The splitting processor (Lem. 4) leaves a lot of choice to the implementation
where to split. We currently use it to enable the loop processor, which
requires a very particular problem shape.

If a subroutine requires an SMT query, TCT interfaces Yices [14] and Z3 [12].

#### Experiments.

We evaluated TCT-LCTRS on the ITS benchmarks considered by Brockschmidt et al.
[8], using a timeout of 60 seconds. Tab. 1 compares our implementation with
KoAT [8], CoFloCo [17, 16], the ITS version of TCT [5], and PUBS [1], giving
the number of problems for which a bound was derived at all, the number of
constant bounds, and the number of bounds that are at most linear, quadratic,
and cubic, respectively.

|  TCT-LCTRS | KoAT | CoFloCo |  TCT-ITS | PUBS
---|---|---|---|---|---
solved problems | 359 | 404 | 347 | 309 | 285
constant | 119 | 131 | 117 | 118 | 109
$\leqslant\mathcal{O}(n)$ | 282 | 298 | 270 | 250 | 240
$\leqslant\mathcal{O}(n^{2})$ | 345 | 376 | 336 | 300 | 270
$\leqslant\mathcal{O}(n^{3})$ | 356 | 383 | 345 | 306 | 278
Table 1: Comparison of tools on ITS benchmarks.

The new splitting and recurrence processors allow TCT-LCTRS to derive
sublinear bounds. This is the case for all problems where PUBS derives a
(precise) logarithmic bound, such as the examples divByTwo and direct_n_log_n.
(KoAT and CoFloCo do not support sublinear bounds, and hence output linear
bounds for these examples.) Moreover, we can precisely analyse subproblems
produced by a divide-and-conquer approach like divide_and_conquer, where TCT
(as well as KoAT) produces the tight linear bound, while CoFloCo fails and
PUBS gives an exponential bound. Detailled results, including a complete table
and TCT output, are available on-line.444See http://cl-
informatik.uibk.ac.at/users/swinkler/lctrs˙complexity/

We moreover tested TCT on the set of logic programs collected by Mesnard and
Neumerkl [31],555See http://www.complang.tuwien.ac.at/cti/bench/. restricted
to deterministic programs. A list of solved problems is available on-line as
well.

##  8 Conclusion

This paper presented the first complexity framework for LCTRSs. We conclude by
relating to earlier work in the area, before indicating leads for future
research.

#### Related work.

In the last decades there has been significant progress in the area of _fully
automated_ resource analysis, showing that it can be both practicable and
scalable, see e.g. [39, 1, 24, 2, 36, 40, 3, 18, 26, 32]. In the following, we
indicate related work that directly influenced our framework, or employed
similar methods.

Our framework differs from earlier work by Avanzini and Moser [4] in three
important respects: first, constraints over arbitrary background theories are
supported, second, complexity is not expressed in terms of the size of the
initial term but in terms of measure functions, and third, sublinear bounds
can be derived. While innermost rewriting is a rather natural restriction for
LCTRSs, _call by need_ strategies could be considered in the future for
LCTRSs, too.

LCTRSs generalise ITSs, the complexity analysis of which is subject to a
comprehensive line of research [8, 34]. Our approach gracefully extends the
alternating time and size bound technique by Brockschmidt et al. [8], as the
ITS case is fully covered. In addition, we can obtain sublinear bounds, and
support further modularization. Moreover, LCTRSs offer native support for full
recursion.

Sublinear bounds are beyond the scope of this earlier work, but can be
inferred by some other tools. Albert et al. [1] apply refinements to linear
ranking functions and support sufficient criteria for divide-and-conquer
patterns. This allows the tool PUBS to recognize logarithmic and
$\mathcal{O}(n\,\log(n))$ bounds for some problems. Chatterjee et al. [9] use
synthesis ranking functions extended by logarithmic and exponential terms,
making use of an insightful adaption of Farkas’ and Handelman’s lemmas. The
approach is able to handle examples such as mergesort. In contrast to our work
this amounts to a whole-program analysis. Further, extensibility to a
constraint formalism like LCTRS is unclear. Wang et al. [38] present an ML-
like language with type annotations, also using the Master Theorem to handle
divide-and-conquer-like recurrences. To estimate lower bounds for logic
programs based on divide-and-conquer, Debray et al. [13] consider non-
deterministic recurrence relations and propose a technique to obtain a closed-
form bound for some cases.

#### Future work.

We see exciting directions for future work both on a theoretical and an
application level. Various additional processors can be conceived for our
complexity framework, for instance forms of dependency pairs for non-innermost
rewriting [34, 25], knowledge propagation and narrowing [34].

Simplification systems as, for instance, employed in compiler toolchains (cf.
Ex. 3) or SMT solvers constitute a highly relevant application domain, since
these routines operate in performance-critical contexts. In order to tackle
such systems, techniques for _derivational_ complexity of LCTRSs need to be
developed.

On the application level, LCTRSs constitute a natural backend for complexity
analysis of constraint logic programs, since constraints can be natively
expressed. Our experiments with logic programs did not take backtracking into
account, but suitably adapting the transformational frameworks as established
by Giesl et al. [23] to LCTRSs, this is not a showstopper: There the authors
provide an automated complexity and termination analysis of full Prolog
programs. In particular, the aforementioned restriction to deterministic
programs can be overcome. We thus plan to support CLP as a frontend of our
analysis, possibly taking into account _labelling strategies_ that control the
instantiation of query terms. We furthermore plan to support C programs as a
frontend. C programs with integers, as considered in the Termination
Competition666http://termination-portal.org/ can be expressed as ITSs. LCTRSs
offer more flexibility and can support also strings and floats, as the
respective theories are supported by SMT solvers. Just like for the case of
CLP, this requires the development of suitable complexity-reflecting
transformations. More experiments are planned to evaluate our method on
(constrained) logic programs [31] and problems from the software
competition.777https://sv-comp.sosy-lab.org/

## References

  * [1] E. Albert, P. Arenas, S. Genaim, and G. Puebla.  Automatic inference of upper bounds for recurrence relations in cost analysis.  In Proc. 15th SAS, volume 5079 of LNCS, pages 221–237, 2008\.  10.1007/978-3-540-69166-2_15.
  * [2] E. Albert, S. Genaim, and A. N. Masud.  On the inference of resource usage upper and lower bounds.  ACM TOCL, 14(3):22, 2013.  10.1145/2499937.2499943.
  * [3] M. Avanzini, U. Dal Lago, and G. Moser.  Analysing the complexity of functional programs: Higher-order meets first-order.  In Proc. 20th ICFP, pages 152–164. ACM, 2015.  10.1145/2784731.2784753.
  * [4] M. Avanzini and G. Moser.  A combination framework for complexity.  Inf. Comput., 248:22–55, 2016.  10.1016/j.ic.2015.12.007.
  * [5] M. Avanzini, G. Moser, and M. Schaper.  TcT: Tyrolean Complexity Tool.  In Proc. 22nd TACAS, volume 9636 of LNCS, pages 407–423. Springer, 2016.  10.1007/978-3-662-49674-9_24.
  * [6] F. Baader and T. Nipkow.  Term Rewriting and All That.  Cambridge University Press, 1998.  10.1017/CBO9781139172752.
  * [7] R. Bagnara and F. Mesnard.  Eventual linear ranking functions.  In Proc. 15th PPDP, pages 229–238, 2013.  10.1145/2505879.2505884.
  * [8] M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl.  Analyzing runtime and size complexity of integer programs.  ACM Trans. Program. Lang. Syst., 38(4):13:1–13:50, 2016.  10.1145/2866575.
  * [9] K. Chatterjee, H. Fu, and A. K. Goharshady.  Non-polynomial worst-case analysis of recursive programs.  In Proc. 29th CAV, volume 10427 of LNCS, pages 41–63, 2017\.  10.1007/978-3-319-63390-9_3.
  * [10] Ş. Ciobâcă and D. Lucanu.  A coinductive approach to proving reachability properties in logically constrained term rewriting systems.  In Proc. 9th IJCAR, volume 10900, pages 295–311, 2018.  10.1007/978-3-319-94205-6_20.
  * [11] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott, editors.  All About Maude—A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of LNCS.  Springer, 2007.  10.1007/978-3-540-71999-1.
  * [12] L. de Moura and N. Bjørner.  Z3: An efficient SMT solver.  In Proc. 14th TACAS, volume 4963 of LNCS, pages 337–340, 2008.  10.1007/978-3-540-78800-3_24.
  * [13] S. K. Debray, P. López-García, M. V. Hermenegildo, and N. Lin.  Lower Bound Cost Estimation for Logic Programs.  In Proc. 14th ILPS, pages 291–305, 1997.  10.7551/mitpress/4283.003.0035.
  * [14] B. Dutertre.  Yices 2.2.  In Proc. 26th CAV, volume 8559 of LNCS, pages 737–744, 2014\.  10.1007/978-3-319-08867-9_49.
  * [15] S. Falke, D. Kapur, and C. Sinz.  Termination analysis of C programs using compiler intermediate languages.  In Proc. 22nd RTA, volume 10 of LIPIcs, pages 41–50, 2011\.  10.4230/LIPIcs.RTA.2011.41.
  * [16] A. Flores-Montoya.  Upper and lower amortized cost bounds of programs expressed as cost relations.  In Proc. 21st FM, volume 9995 of LNCS, pages 254–273, 2016\.  10.1007/978-3-319-48989-6_16.
  * [17] A. Flores-Montoya.  Cost Analysis of Programs Based on the Refinement of Cost Relations.  PhD thesis, Universität Darmstadt, 2017.
  * [18] F. Frohn and J. Giesl.  Complexity analysis for Java with AProVE.  In Proc. 13th CAV, volume 10510 of LNCS, pages 85–101, 2017\.  10.1007/978-3-319-66845-1_6.
  * [19] C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke.  Proving termination of integer term rewriting.  In Proc. 20th RTA, volume 5595 of LNCS, pages 32–47, 2009\.  10.1007/978-3-642-02348-4_3.
  * [20] C. Fuhs, C. Kop, and N. Nishida.  Verifying procedural programs via constrained rewriting induction.  ACM TOCL, 18(2):14:1–14:50, 2017.  10.1145/3060143.
  * [21] Y. Furuichi, N. Nishida, M. Sakai, K. Kusakari, and T. Sakabe.  Approach to procedural program verification based on implicit induction of constrained term rewriting systems.  IPSJ Trans. Inf. and Syst., 1(2):100–121, 2008.  In Japanese.
  * [22] J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann.  Analyzing program termination and complexity automatically with AProVE.  J. Autom. Reasoning, 58(1):3–31, 2017.  10.1007/s10817-016-9388-y.
  * [23] J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs.  Symbolic evaluation graphs and term rewriting—a general methodology for analyzing logic programs.  In Proc. 14th PPDP, pages 1–12. ACM Press, 2012.  10.1007/978-3-642-38197-3_1.
  * [24] S. Gulwani.  SPEED: Symbolic complexity bound analysis.  In Proc. 21st CAV, volume 5643 of LNCS, pages 51–62, 2009\.  10.1007/978-3-642-02658-4_7.
  * [25] N. Hirokawa and G. Moser.  Automated complexity analysis based on the dependency pair method.  In Proc. 4th IJCAR, volume 5195 of LNCS, pages 364–379, 2008\.  10.1007/978-3-540-71070-7_32.
  * [26] J. Hoffmann, A. Das, and S.-C. Weng.  Towards automatic resource bound anaysis for OCaml.  In Proc. 44th POPL, pages 359–373. ACM, 2017.  10.1145/3009837.
  * [27] C. Kop.  Termination of LCTRSs.  In Proc. 13th WST, pages 59–63, 2013.
  * [28] C. Kop and N. Nishida.  Term rewriting with logical constraints.  In Proc. 9th FroCoS, volume 8152 of LNAI, pages 343–358, 2013.  10.1007/978-3-642-40885-4_24.
  * [29] C. Kop and N. Nishida.  Constrained term rewriting tool.  In Proc. 20th LPAR, volume 9450 of LNAI, pages 549–557, 2015\.  10.1007/978-3-662-48899-7_38.
  * [30] N. Lopes, D. Menendez, S. Nagarakatte, and J. Regehr.  Practical verification of peephole optimizations with Alive.  Commun. ACM, 61(2):84–91, 2018.  10.1145/3166064.
  * [31] F. Mesnard and U. Neumerkel.  Applying static analysis techniques for inferring termination conditions of logic programs.  In Proc. 8th SAS, volume 2126 of LNCS, pages 93–110, 2001\.  10.1007/3-540-47764-0_6.
  * [32] G. Moser and M. Schaper.  From Jinja bytecode to term rewriting: A complexity reflecting transformation.  Inf. Comput., 261(Part):116–143, 2018.  10.1016/j.ic.2018.05.007.
  * [33] N. Nishida and S. Winkler.  Loop detection by logically constrained term rewriting.  In Proc. 10th VSTTE, volume 11294 of LNCS, pages 309–321, 2018.  10.1007/978-3-030-03592-1_18.
  * [34] L. Noschinski, F. Emmes, and J. Giesl.  Analyzing innermost runtime complexity of term rewriting by dependency pairs.  J. Autom. Reasoning, 51(1):27–56, 2013.  10.1007/s10817-013-9277-6.
  * [35] A. Podelski and A. Rybalchenko.  A complete method for the synthesis of linear ranking functions.  In Proc. 5th VMCAI, volume 2937 of LNCS, pages 239–251, 2004\.  10.1007/978-3-540-24622-0_20.
  * [36] A. Serrano, P. López-García, and M. Hermenegildo.  Resource usage analysis of logic programs via abstract interpretation using sized types.  TPLP, 14(4-5):739–754, 2014.  10.1017/S147106841400057X.
  * [37] TeReSe.  Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 2003.
  * [38] P. Wang, D. Wang, and A. Chlipala.  TiML: A functional language for practical complexity analysis with invariants.  Proc. ACM Program. Lang., 1(OOPSLA), 2017.  10.1145/3133903.
  * [39] R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenström.  The worst-case execution-time problem - overview of methods and survey of tools.  ACM Trans. Prog. Lang. Syst., 7(3), 2008.  10.1145/1347375.1347389.
  * [40] R. Wilhelm and D. Grund.  Computation takes time, but how much?  Commun. ACM, 57(2):94–103, 2014.  10.1145/2500886.
  * [41] S. Winkler and A. Middeldorp.  Completion for logically constrained rewriting.  In Proc. 3rd FSCD, volume 108 of LIPIcs, pages 30:1–30:18, 2018.  10.4230/LIPIcs.FSCD.2018.30.

##  Appendix 0.A Proofs

###### Lemma 1

1 Suppose $P=((t_{0},\varphi_{0}),\mathcal{D},\mathcal{R})$ is a complexity
problem and $\mathcal{M}$ a $\mathsf{DT}$-measure interpretation with which
$\mathcal{R}$ is weakly, and $\mathcal{D}$ is strictly compatible. Then the
following processor is sound:

$\frac{{\vdash\,}{P}\colon{(T,S)}}{{\vdash\,}{P}\colon{(T^{\prime},S)}}\quad\mathsf{Interpretation}$

where $T^{\prime}(\rho)=(t_{0}^{\\#})^{\mathcal{M}}$ for all
$\rho\in\mathcal{D}_{>}$, and $T^{\prime}(\rho)=T(\rho)$ otherwise.

###### Proof

By assumption, $\mathcal{R}$ has a unique initial state $(t_{0},\varphi_{0})$.
Let $\overline{x}=\overline{\mathcal{V}ar}(t_{0})$, and
$\rho\in\mathcal{D}_{>}$. We show that for
${\to_{\mathcal{T}}}={\to_{(\mathcal{D}\cup\mathcal{R}\cup\mathsf{calc})\setminus\\{\rho\\}}}$,

$(t_{0}^{\\#})^{\mathcal{M}}(\overline{m})\geqslant\sup\>\\{k\mid\exists\sigma.\
t_{0}^{\\#}\sigma\mathrel{(\to_{\mathcal{T}}^{*}\cdot\to_{\rho})^{k}}u\text{,
}|\overline{x}\sigma|\leqslant_{n}\overline{m}\text{ and $\sigma$ respects
}\varphi_{0}\\}$

for all $\overline{m}\in\mathbb{N}^{n}$. Consider a substitution $\sigma$ such
that $|\overline{x}\sigma|\leqslant_{n}\overline{m}$, and a (potentially
infinite) rewrite sequence in which $k\in\mathbb{N}\cup\\{\omega\\}$ steps
apply rule $\rho$:

$t_{0}^{\\#}\sigma=v_{0}\xrightarrow[\mathcal{T}]{*}u_{1}\xrightarrow[\rho]{}v_{1}\xrightarrow[\mathcal{T}]{*}u_{2}\xrightarrow[\rho]{}v_{2}\xrightarrow[\mathcal{T}]{*}\dots$
(3)

The goal is to verify $(t_{0}^{\\#})^{\mathcal{M}}(\overline{m})\geqslant k$.
If $k=0$ then this is obvious because the domain of $\mathcal{M}$ is
$\mathbb{N}$, so suppose $k>0$. By compatibility, we have
$v_{0}^{\mathcal{M}}\geqslant u_{1}^{\mathcal{M}}$,
$u_{i}^{\mathcal{M}}>v_{i}^{\mathcal{M}}$, and $v_{i}^{\mathcal{M}}\geqslant
u_{i+1}^{\mathcal{M}}$, for all $i\geqslant 1$. Thus $k$ must be finite, and
there can be at most $(t_{0}^{\\#})^{\mathcal{M}}(\overline{m})$ $\rho$-steps
in 3. ∎

###### Lemma 2

Suppose $P=(s_{0},\mathcal{D},\mathcal{R})$ is a complexity problem such that
$\mathcal{D}^{\prime}\subseteq\mathcal{D}$ has no initial dependency tuples
and $\mathcal{R}$ is weakly, and $\mathcal{D}^{\prime}$ is strictly compatible
with a $\mathsf{DT}$-measure interpretation $\mathcal{M}$. Then the following
processor is sound:

$\frac{{\vdash\,}{P}\colon{(T,S)}}{{\vdash\,}{P}\colon{(T^{\prime},S)}}\quad\mathsf{TimeBounds}$

such that
$T^{\prime}(\rho)=\sum_{(\gamma,\delta)\in\mathsf{pre}(\mathcal{D}^{\prime})}T(\gamma)\cdot\ell_{2}^{\mathcal{M}}(\overline{S}_{\delta})$
for all $\rho\in\mathcal{D}^{\prime}_{>}$, where $\delta:\ell_{2}\to
r_{2}~{}[\varphi_{2}]$ and $\overline{S}_{\delta}$ the vector
$S(\delta,y_{1}),\dots,S(\delta,y_{k})$ for ${y_{1}},\dots,{y_{k}}$ the
variables in $\ell_{2}$. Otherwise, for all
$\rho\in\mathcal{D}\setminus\mathcal{D}^{\prime}_{>}$ set
$T^{\prime}(\rho)=T(\rho)$.

###### Proof

It suffices to show that

$T^{\prime}(\rho)(\overline{m})\geqslant\sup\>\\{k\mid
t_{0}^{\\#}\sigma\mathrel{(\to_{\mathcal{R}}^{*}\cdot\to_{\rho})^{k}}u\text{
and }|\overline{x}\sigma|\leqslant_{n}\overline{m}\text{ and $\sigma$ respects
}\varphi_{0}\\}$

holds for all $\rho\in\mathcal{D}^{\prime}_{>}$ and
$\overline{m}\in\mathbb{N}^{n}$. Fix some $\rho\in\mathcal{D}^{\prime}_{>}$
and let
$\to_{\mathcal{T}}=\to_{(\mathcal{D}\cup\mathcal{R}\cup\mathsf{calc})\setminus\\{\rho\\}}$.
Consider a substitution $\sigma$ such that
$|\overline{x}\sigma|\leqslant_{n}\overline{m}$, and a (potentially infinite)
rewrite sequence

$t_{0}^{\\#}\sigma=v_{0}\xrightarrow[\mathcal{T}]{*}u_{1}\xrightarrow[\rho]{}v_{1}\xrightarrow[\mathcal{T}]{*}u_{2}\xrightarrow[\rho]{}v_{2}\xrightarrow[\mathcal{T}]{*}\dots$
(4)

with $k\in\mathbb{N}\cup\\{\omega\\}$ steps using $\rho$. It has to be
verified that the expression
$B:=\sum_{(\gamma,\delta)\in\mathsf{pre}(\mathcal{D}^{\prime})}T(\gamma)\cdot\ell_{2}^{\mathcal{M}}(\overline{S}_{\delta})$
satisfies $B(\overline{m})\geqslant k$. We can write sequence 4 as

$t_{0}^{\\#}\sigma=v_{0}\xrightarrow[\mathcal{U}]{*}w_{1}^{\prime}\xrightarrow[\mathcal{U}]{}w_{1}\xrightarrow[\mathcal{D}^{\prime}\cup\mathcal{R}\cup\mathsf{calc}]{*}v_{1}\xrightarrow[\mathcal{U}]{*}w_{2}^{\prime}\xrightarrow[\mathcal{U}]{}w_{2}\xrightarrow[\mathcal{D}^{\prime}\cup\mathcal{R}\cup\mathsf{calc}]{*}v_{2}\xrightarrow[\mathcal{U}]{*}\dots$
(5)

for
$\mathcal{U}=\mathcal{R}\cup\mathcal{D}\cup\mathsf{calc}\setminus\mathcal{D}^{\prime}$.
Every step $w_{i}^{\prime}\to_{\mathcal{U}}w_{i}$ before a term $w_{i}$ must
use a rule $\rho_{i}$ such that
$(\rho_{i},\delta_{i})\in\mathsf{pre}(\mathcal{D}^{\prime})$, for all $i>0$.
Fix some $(\gamma,\delta)\in\mathsf{pre}(\mathcal{D}^{\prime})$, and let $i$
be such that $(\rho_{i},\delta_{i})=(\gamma,\delta)$. Moreover, in the
subsequence
$w_{i}\to_{\mathcal{D}^{\prime}\cup\mathcal{R}\cup\mathsf{calc}}^{*}v_{i}$ the
value under the interpretation $\mathcal{M}$ is weakly decreasing, and for
every $\rho$-step there is a strict decrease as
$\rho\in\mathcal{D}_{>}^{\prime}$. Hence the number of
$\mathcal{D}^{\prime}_{>}$ steps (and in particular $\rho$-steps) in
$w_{i}\to_{\mathcal{D}^{\prime}}^{*}v_{i}$ is bounded by
$N:=lhs(\delta)^{\mathcal{M}}(\overline{S}_{\delta})$. The number of $\gamma$
steps followed by $\delta$ steps in 5 is clearly bounded by $T(\gamma)$.
Summing up the product $N\cdot T(\gamma)$ over all pairs
$(\gamma,\delta)\in\mathsf{pre}(\mathcal{D}^{\prime})$ yields
$B(\overline{m})\geqslant k$. ∎

###### Lemma 5

If $(s_{0},\mathcal{D},\mathcal{R})$ is a problem with splitting
$(\mathcal{D}_{0},\mathcal{D}_{1})$ such that
$\mathsf{pre}(\mathcal{D}_{1})=\\{(\delta_{i},\gamma_{i})\mid
1\,{\leqslant}\,i\,{\leqslant}\,m\\}$ and $\gamma_{i}=(\ell_{i}\to r_{i}\
[\varphi_{i}])$, the following processor is sound:

$\frac{{\vdash\,}{P}\colon{(T,S)}\quad\
{\vdash\,}{(s_{0},\mathcal{D}_{0},\mathcal{R})}\colon{(T_{0},S_{0})}\quad\
\bigwedge_{i=1}^{m}{\vdash\,}{((\ell_{i},\varphi_{i}),\mathcal{D}_{1},\mathcal{R})}\colon{(T_{i},S_{i})}}{{\vdash\,}{P}\colon{(\lambda\rho.\left\\{\begin{array}[]{ll}T_{0}(\rho)&\text{
if }\rho\in\mathcal{D}_{0}\\\ \sum_{i=1}^{m}T_{0}(\delta_{i})\cdot
T_{i}(\rho)(\overline{S}_{\gamma_{i}})&\text{ if
}\rho\in\mathcal{D}_{1}\end{array}\right\\},S)}}\quad\mathsf{Split}$

###### Proof

Let $s_{0}=(t_{0},\varphi_{0})$. We can represent an evaluation tree as

$\displaystyle\\{t_{0}\\}$
$\displaystyle\xrightarrow[\mathcal{D}_{0}\cup\mathcal{R}]{*}\langle\\!\langle
u_{1},\dots,u_{k}\rangle\\!\rangle\xrightarrow[\delta_{j_{1}},\dots,\delta_{j_{k}}]{*}\langle\\!\langle
v_{1},\dots,v_{k^{\prime}}\rangle\\!\rangle\xrightarrow[\mathcal{D}_{1}\cup\mathcal{R}]{*}\langle\\!\langle
w_{1},\dots,w_{l}\rangle\\!\rangle$ (6)

since the evaluation must start with $\mathcal{D}_{0}$ steps, and there are no
edges from $G_{1}$ to $G_{0}$. (Here the notation
$\langle\\!\langle\dots\rangle\\!\rangle$ indicates a flattened list of nested
$\langle\dots\rangle$ terms.) For any rule $\rho\in\mathcal{D}_{0}$, by the
shape of the evaluation tree (6), $T_{0}(\rho)$ clearly serves as an overall
time bound, since $\mathcal{D}_{0}$ rules is never applied after
$\mathcal{D}_{1}$ rules.

So let $\rho\in\mathcal{D}_{1}$. Note that for every $j$,
$1\,{\leqslant}\,j\,{\leqslant}\,k$ such that $u_{j}\to\langle v_{j_{1}},\dots
v_{j_{q}}\rangle$ and all $\hat{v}\in\\{v_{j_{1}},\dots,v_{j_{q}}\\}$ there
must be some $(\delta_{i},\gamma_{i})\in\mathsf{pre}(\mathcal{D}_{1})$ such
that the step uses $\delta_{i}\in\\{\delta_{1},\dots,\delta_{m}\\}$ and
$\hat{v}$ is an instance of $lhs(\gamma_{i})$. To obtain a time bound for
$\rho$, we can thus estimate the number of applications of $\rho$ in a subtree
starting with an application of $\delta_{i}$ followed by $\gamma_{i}$, and
take the sum over all such pairs. So let
$(\delta_{i},\gamma_{i})\in\mathsf{pre}(\mathcal{D}_{1})$. To overapproximate
the number of $\rho$-steps below $\hat{v}$, we consider
$T_{1}(lhs(\gamma_{i}))$: this yields an expression in
$\mathcal{V}ar(lhs(\gamma_{i}))$, and we obtain a respective expression in
$\mathcal{V}ar(t_{0})$ by applying $T_{1}(lhs(\gamma_{i}))$ to
$\overline{S}_{\gamma_{i}}$. In order to account for multiple occurrences of
the consecutive pair $(\delta_{i},\gamma_{i})$ in (6), this expression is
multiplied by $T_{0}(\delta_{i})$. ∎

###### Lemma 6

Let $P=(s_{0},\mathcal{D},\mathcal{R})$ be a cyclic problem with termination
condition $\overline{b}$ and a DT $\delta$ of the form (2), and let
$\gamma_{i}=(\ell_{i}\to r_{i}\ [\varphi_{i}])$, for all $i$,
$1\,{\leqslant}\,i\,{\leqslant}\,m$. Then the following processor is sound:

$\frac{{\vdash\,}{P}\colon{(T,S)}\quad{\vdash\,}{\bigwedge_{i=1}^{m}((\ell_{i},\varphi_{i}),\mathcal{D}^{\prime},\mathcal{R})}\colon{(T_{i},S_{i})}}{{\vdash\,}{(s_{0},\mathcal{D},\mathcal{R})}\colon{(F(\overline{x}),S)_{\Sigma}}}\quad\mathsf{Recurrence}$

where $F$ is a solution to a recurrence

$\displaystyle f(\overline{x})$
$\displaystyle=f(\overline{r}_{1})+\ldots+f(\overline{r}_{p})+H(\overline{x})$
$\displaystyle f(\overline{b})$ $\displaystyle=0$ (7)

for some
$H(\overline{x})\geqslant\sum_{\rho\in\mathcal{D}^{\prime}}\sum_{i=1}^{m}T_{i}(\rho)(\overline{S}_{\gamma_{i}})$.

###### Proof

As $\rho$ has no incoming edges in $G$ except from itself, $G$ is of the form
depicted in Fig. 1(b). Let
$C_{i}(\overline{x})=\sum_{\rho\in\mathcal{D}^{\prime}}T_{i}(\rho)(\overline{S}_{\gamma_{i}})$
for all $i$, $1\leqslant i\leqslant m$. So an overapproximation of a solution
to

$\displaystyle f(\overline{x})$
$\displaystyle=f(\overline{r}_{1})+\ldots+f(\overline{r}_{p})+\sum_{i=1}^{m}C_{i}(\overline{x})$
$\displaystyle f(\overline{b})$ $\displaystyle=0$ (8)

is a complexity approximation for $(s_{0},\mathcal{D},\mathcal{R})$. It
remains to show that the overapproximation of
$C(\overline{x}):=\sum_{i=1}^{p}C_{i}(\overline{x})$ by $H(\overline{x})$ is
sound. To that end, let $F(\overline{x})$ be a solution to 7 and
$F^{\prime}(\overline{x})$ a solution to 8. We show by induction on
$\overline{x}$ that $F(\overline{x})\geqslant F^{\prime}(\overline{x})$ holds
for all $\overline{x}\geqslant_{n}\overline{b}$. By the assumption that $F$
and $F^{\prime}$ solve 7 and 8, this clearly holds for the base case
$\overline{x}=\overline{b}$. For the step case, it is easy to verify that
$F(\overline{x})\geqslant F^{\prime}(\overline{x})$ holds:

$\displaystyle F(\overline{x})$
$\displaystyle=F(\overline{r}_{1})+\ldots+F^{\prime}(\overline{r}_{p})+H(\overline{x})$
($F$ solves 7) $\displaystyle\geqslant
F^{\prime}(\overline{r}_{1})+\ldots+F^{\prime}(\overline{r}_{p})+C(\overline{x})$
(IH as $\overline{r}_{i}>\overline{x}$, and $H(\overline{x})\geqslant
C(\overline{x})$) $\displaystyle=F^{\prime}(\overline{x})$ ($F^{\prime}$
solves 8)

##  Appendix 0.B Further Processors

In this section we outline how _chaining_ fits into our framework, a standard
technique from termination and complexity analysis. Its adaptation is
straightforward, hence we describe it only in the appendix for the sake of
completeness.

### Chaining.

Rule chaining is a commonly used complexity-reflecting transformation [15, 5]
that can also be used for LCTRSs. Its aim is to combine rules that are applied
subsequently, which can simplify further analysis.

###### Definition 15

Let $P$ be a problem $(s_{0},\mathcal{D},\mathcal{R})$ with DG $G$ such that
$\rho\colon t\to u~{}[\varphi]\in\mathcal{D}$ has successors
$\delta_{i}\colon\ell_{i}\to r_{i}~{}[\psi_{i}]$ in $G$, for
$1\,{\leqslant}\,i\,{\leqslant}\,k$. Then $\rho$ and
$\Delta=\\{{\delta_{1}},\dots,{\delta_{k}}\\}$ are _chainable_ if there are
positions $p_{i}$ and substitutions $\sigma_{i}$ such that
$u|_{p_{i}}=\ell_{i}\sigma_{i}$, and all $\psi_{i}\sigma_{i}$ are in
$\mathcal{T}(\mathcal{F}_{L},\mathcal{V})$.888We assume that these are all
possibilities to create a redex in $u$ wrt. rules in $\Delta$. Then
$\mathsf{chain}(\rho,\delta_{i})=t\to
u[r_{i}\sigma]_{p_{i}}~{}[\varphi\wedge\psi_{i}\sigma_{i}]$, and
$\mathsf{chain}(\rho,\Delta)=\\{\,\mathsf{chain}(\rho,\delta_{i})\,\\}_{1\leqslant
i\leqslant k}$.

###### Lemma 6

For a complexity problem $(s_{0},\mathcal{D},\mathcal{R})$, the following
processor is sound:

$\frac{{\vdash\,}{(s_{0},\mathcal{D}\cup\mathsf{chain}(\rho,\Delta)\setminus\\{\rho\\},\mathcal{R})}\colon{(T,S)}}{{\vdash\,}{(s_{0},\mathcal{D},\mathcal{R})}\colon{(T^{\prime},S^{\prime})}}\quad\mathsf{Chaining}$

where $\rho$ and $\Delta$ are chainable, the updated runtime approximation is
$T^{\prime}(\delta_{i})=T(\delta_{i})+T(\mathsf{chain}(\rho,\delta_{i}))$,
$T^{\prime}(\rho)=\sum_{i}T(\mathsf{chain}(\rho,\delta_{i}))$ and
$T^{\prime}(\gamma)=T(\gamma)$ otherwise; and
$S^{\prime}(\rho,y)=\max\\{S(\mathsf{chain}(\rho,\delta_{i}))\\}_{i}$,
$S^{\prime}(\delta_{i},y)$ is $\max(S(\delta_{i},y),y\sigma_{i})$ if
$y\sigma_{i}\in\mathcal{T}(\mathcal{F}_{L},\mathcal{V})$ and $\omega$
otherwise, and $S^{\prime}(\gamma,y)=S(\gamma,y)$ for all other
$\gamma\in\mathcal{D}$.

###### Example 8

In two chaining steps, the cycles $(9)-(3)-(9)$ and $(9)-(7)-(9)$ in Ex. 1 can
be chained to single-step cycles, such that (9) is replaced by

$\displaystyle\mathsf{m}(x,y,z)$
$\displaystyle\to\langle\mathsf{m}_{0}(x,u,v),\mathsf{m}(u,u,v),\mathsf{m}(v,u,v),\mathsf{m}_{3}(x,u,v)\rangle\
[\psi]$ $\displaystyle\psi$ $\displaystyle=x\geqslant 2\wedge u\geqslant
0\wedge v\geqslant 0\wedge x+1\geqslant 2u\wedge 2u\geqslant x\wedge
x\geqslant 2v\wedge 2v+1\geqslant x$