1em1em

# Dependency Pairs and Polynomial Path Orders††thanks: This research is
partially supported by FWF (Austrian Science Fund) projects P20133.

Martin Avanzini and Georg Moser
{martin.avanzini<EMAIL_ADDRESS>
(March 2009)

###### Abstract

We show how polynomial path orders can be employed efficiently in conjunction
with weak innermost dependency pairs to automatically certify polynomial
runtime complexity of term rewrite systems and the polytime computability of
the functions computed. The established techniques have been implemented and
we provide ample experimental data to assess the new method.

###### Contents

  1. 1 Introduction
  2. 2 The Polynomial Path Order on Sequences
  3. 3 Complexity Analysis Based on the Dependency Pair Method
  4. 4 The Polynomial Path Order over Quasi-Precedences
  5. 5 Dependency Pairs and Polynomial Path Orders
  6. 6 Experimental Results
  7. 7 Conclusion
  8. A Appendix
    1. A.1 Proof of Theorem 5.11
    2. A.2 Proof of Theorem 5.14

##  1 Introduction

In order to measure the complexity of a (terminating) term rewrite system (TRS
for short) it is natural to look at the maximal length of derivation
sequences—the _derivation length_ —as suggested by Hofbauer and Lautemann in
Hofbauer and Lautemann (1989). More precisely, the _runtime complexity
function_ with respect to a (finite and terminating) TRS $\mathcal{R}$ relates
the maximal derivation length to the size of the initial term, whenever the
set of initial terms is restricted to constructor based terms, also called
_basic_ terms. The restriction to basic terms allows us to accurately express
the complexity of a program through the runtime complexity of TRSs. In this
paper we study and combine recent efforts for the _automatic_ analysis of
runtime complexities of TRSs. In Avanzini and Moser (2008) we introduced a
restriction of the multiset path order, called _polynomial path order_
(_$\textsc{POP}^{\ast}$_ for short) that induces polynomial runtime complexity
if restricted to innermost rewriting. The definition of $\textsc{POP}^{\ast}$
employs the idea of _tiered recursion_ Simmons (1988). Syntactically this
amounts to a separation of arguments into _normal_ and _safe_ arguments, cf.
Bellantoni and Cook (1992). Furthermore, Hirokawa and the second author
introduced a variant of dependency pairs, dubbed _weak dependency pairs_ ,
that makes the dependency pair method applicable in the context of complexity
analysis, cf. Hirokawa and Moser (2008b, a).

We show how weak innermost dependency pairs can be successfully applied in
conjunction with $\textsc{POP}^{\ast}$. The following example (see Fuhs et al.
(2007)) motivates this study. Consider the TRS $\mathcal{R}_{\textsf{bin}}$
encoding the function $\lambda x.\lceil{\log(x+1)}\rceil$ for natural numbers
given as tally sequences:

$\displaystyle 1\colon$ $\displaystyle\mathsf{half}(\mathsf{0})$
$\displaystyle\to\mathsf{0}$ $\displaystyle 4\colon$
$\displaystyle\mathsf{bits}(\mathsf{0})$ $\displaystyle\to\mathsf{0}$
$\displaystyle 2\colon$ $\displaystyle\mathsf{half}(\mathsf{s}(\mathsf{0}))$
$\displaystyle\to\mathsf{0}$ $\displaystyle 5\colon$
$\displaystyle\mathsf{bits}(\mathsf{s}(\mathsf{0}))$
$\displaystyle\to\mathsf{s}(\mathsf{0})$ $\displaystyle 3\colon$
$\displaystyle\mathsf{half}(\mathsf{s}(\mathsf{s}(x)))$
$\displaystyle\to\mathsf{s}(\mathsf{half}(x))$ $\displaystyle\hskip
8.61108pt6\colon$ $\displaystyle\mathsf{bits}(\mathsf{s}(\mathsf{s}(x)))$
$\displaystyle\to\mathsf{s}(\mathsf{bits}(\mathsf{s}(\mathsf{half}(x))))$

It is easy to see that the TRS $\mathcal{R}_{\textsf{bin}}$ is not compatible
with $\textsc{POP}^{\ast}$, even if we allow quasi-precedences, see Section 4.
On the other hand, employing (weak innermost) dependency pairs, argument
filtering, and the usable rules criteria in conjunction with
$\textsc{POP}^{\ast}$, polynomial innermost runtime complexity of
$\mathcal{R}_{\textsf{bin}}$ can be shown fully automatically.

The combination of dependency pairs and polynomial path orders, while
conceptually quite clear, turns out to be technical involved. One of the first
obstacles one encounters is that the pair
$(\mathrel{\text{\raisebox{0.0pt}{${\not{>}}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}},\mathrel{{>}_{\mathsf{pop*}}})$
cannot be used as a reduction pair in the spirit of Hirokawa and Moser
(2008b), as
$\mathrel{\text{\raisebox{0.0pt}{${\not{>}}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}$
fails to be closed under contexts. Conclusively, we start from scratch and
study polynomial path orders in the context of _relative rewriting_ Geser
(1990). Based on this study an incorporation of argument filterings becomes
possible so that we can employ the pair
$(\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}},\mathrel{{>}^{\pi}_{\mathsf{pop*}}})$
in conjunction with dependency pairs successfully. Here,
$\mathrel{{>}^{\pi}_{\mathsf{pop*}}}$ refers to the order obtained by
combining $\mathrel{{>}_{\mathsf{pop*}}}$ with the argument filtering $\pi$ as
expected, and
$\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}$
denotes the extension of $\mathrel{{>}^{\pi}_{\mathsf{pop*}}}$ by term
equivalence, preserving the separation of safe and normal argument positions.
Note that for polynomial path orders, the integration of argument filterings
is not only non-trivial, but indeed a challenging task. This is mainly due to
the embodiment of tiered recursion in $\textsc{POP}^{\ast}$. Thus we establish
a combination of two syntactic techniques in complexity analysis. The
experimental evidence given below indicates the power and in particular the
efficiency of the provided results.

Our next contribution is concerned with _implicit complexity theory_ , see for
example Bonfante et al. (2009). A careful analyis of our main result shows
that polynomial path orders in conjunction with (weak innermost) dependency
pairs even induce polytime computability of the functions defined by the TRS
studied. This result fits well with recent results by Marion and Péchoux on
the use of restricted forms of the dependency pair method to charcterise
complexity classes like PTIME or PSPACE, cf. Marion and Péchoux (2008). Note
that both results allow to conclude, based on different restrictions, polytime
computability of the functions defined by constructor TRSs, whose termination
can be shown by the dependency pair method. Note that the results in Marion
and Péchoux (2008) also capture programs admitting infeasible runtime
complexities but define functions that are computable in polytime if suitable
(and non-trivial) program transformations are used. Such programs are outside
the scope of our results. Thus it seems that our results more directly assess
the complexity of the given programs. Note that our tool provides (for the
first time) a fully automatic application of the dependency pair method in the
context of implicit complexity theory.111In this context it is perhaps
interesting to note that for a variant of the TRS
$\mathcal{R}_{\textsf{bin}}$, studied in Marion and Péchoux (2008), our tool
verifies polytime computability fully automatically. See also Avanzini et al.
(2008) for the description of a small tool that implements related
characterisations of of the class of polynomial time computable functions.

The rest of the paper is organised as follows. In Section 2 we present basic
notions and recall (briefly) the _path order for FP_ from Arai and Moser
(2005). We then briefly recall dependency pairs in the context of complexity
analysis from Hirokawa and Moser (2008b, a), cf. Section 3. In Section 4 we
present polynomial path orders over quasi-precedences. Our main results are
presented in Section 5. We continue with experimental results in Section 6,
and conclude in Section 7.

##  2 The Polynomial Path Order on Sequences

We assume familiarity with the basics of term rewriting, see Baader and Nipkow
(1998); Terese (2003). Let $\mathcal{V}$ denote a countably infinite set of
variables and $\mathcal{F}$ a signature, containing at least one constant. The
set of terms over $\mathcal{F}$ and $\mathcal{V}$ is denoted as
$\mathcal{T}(\mathcal{F},\mathcal{V})$ and the set of ground terms as
$\mathcal{T}(\mathcal{F})$. We write $\operatorname{\mathsf{Fun}}(t)$ and
$\operatorname{\mathsf{Var}}(t)$ for the set of function symbols and variables
appearing in $t$, respectively. The root symbol
$\operatorname{\mathsf{rt}}(t)$ of a term $t$ is defined as usual and the
(proper) subterm relation is denoted as $\mathrel{\unlhd}$ ($\mathrel{\lhd}$).
We write $s|_{p}$ for the _subterm_ of $s$ at position $p$. The _size_
$\lvert{t}\rvert$ of a term $t$ is defined as usual and the _width_ of $t$ is
defined as
$\operatorname{\mathsf{width}}(t)\mathrel{:=}\max\\{{n,{\operatorname{\mathsf{width}}}({t}_{1}),\ldots,{\operatorname{\mathsf{width}}}({t}_{n})}\\}$
if $t=f({t}_{1},\ldots,{t}_{n})$ and $n>0$ or
$\operatorname{\mathsf{width}}(t)=1$ else. Let $\succsim$ be a preorder on the
signature $\mathcal{F}$, called _quasi-precedence_ or simply _precedence_.
Based on $\succsim$ we define an equivalence $\approx$ on terms: $s\approx t$
if either (i) $s=t$ or (ii) $s=f({s}_{1},\ldots,{s}_{n})$,
$t=g({t}_{1},\ldots,{t}_{n})$, $f\approx g$ and there exists a permutation
$\pi$ such that $s_{i}\approx t_{\pi(i)}$. For a preorder $\succsim$, we use
$\mathrel{\succsim}^{\mathsf{mul}}$ for the multiset extension of $\succsim$,
which is again a preorder. The proper order (equivalence) induced by
$\mathrel{\succsim}^{\mathsf{mul}}$ is written as
$\mathrel{\succ}^{\mathsf{mul}}$ ($\mathrel{\approx}^{\mathsf{mul}}$).

A _term rewrite system_ (_TRS_ for short) $\mathcal{R}$ over
$\mathcal{T}(\mathcal{F},\mathcal{V})$ is a _finite_ set of rewrite rules
$l\to r$, such that $l\notin\mathcal{V}$ and
$\operatorname{\mathsf{Var}}(l)\supseteq\operatorname{\mathsf{Var}}(r)$. We
write
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$$}}}_{\mathcal{R}}}$
($\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}$)
for the induced (innermost) rewrite relation. The set of defined function
symbols is denoted as $\mathcal{D}$, while the constructor symbols are
collected in $\mathcal{C}$, clearly $\mathcal{F}=\mathcal{D}\cup\mathcal{C}$.
We use $\operatorname{\mathsf{NF}}(\mathcal{R})$ to denote the set of normal
forms of $\mathcal{R}$ and set
$\mathsf{Val}\mathrel{:=}\mathcal{T}(\mathcal{C},\mathcal{V})$, the elements
of $\mathsf{Val}$ are called _values_. A TRS is called _completely defined_ if
normal forms coincide with values. We define
$\mathcal{T}_{\mathsf{b}}\mathrel{:=}\\{f({v}_{1},\ldots,{v}_{n})\mid
f\in\mathcal{D}\text{ and }v_{i}\in\mathsf{Val}\\}$ as the set of _basic
terms_. A TRS $\mathcal{R}$ is a _constructor TRS_ if
$l\in\mathcal{T}_{\mathsf{b}}$ for all ${l\to r}\in\mathcal{R}$. Let
$\mathcal{Q}$ denote a TRS. The _generalised restricted rewrite relation
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{Q}$}}}_{\mathcal{R}}}$_
is the restriction of
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$$}}}_{\mathcal{R}}}$
where all arguments of the redex are in normal form with respect to the TRS
$\mathcal{Q}$ (see Thiemann (2007)). We define the (innermost) relative
rewriting relation (denoted as
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}/\mathcal{S}}}$)
as follows:

${\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}/\mathcal{S}}}}\mathrel{:=}{{\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{R}\cup\mathcal{S}$}}}^{\ast}_{\mathcal{S}}}}\cdot{\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{R}\cup\mathcal{S}$}}}_{\mathcal{R}}}}\cdot{\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{R}\cup\mathcal{S}$}}}^{\ast}_{\mathcal{S}}}}}\hbox
to0.0pt{$\;$.\hss}$

Similarly, we set
${\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}}}\mathrel{:=}{{\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{R}\cup\mathcal{S}$}}}^{\ast}_{\mathcal{S}}}}\cdot{\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{R}\cup\mathcal{S}$}}}^{\varepsilon}_{\mathcal{R}}}}\cdot{\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{R}\cup\mathcal{S}$}}}^{\ast}_{\mathcal{S}}}}}$,
to define an _(innermost) relative root-step_.

A _polynomial interpretation_ is a well-founded and monotone algebra
$(\mathcal{A},>)$ with carrier $\mathbb{N}$ such that $>$ is the usual order
on natural numbers and all interpretation functions $f_{\mathcal{A}}$ are
polynomials. Let $\alpha\colon\mathcal{V}\to\mathcal{A}$ denote an
_assignment_ , then we write $[\alpha]_{\mathcal{A}}(t)$ for the evaluation of
term $t$ with respect to $\mathcal{A}$ and $\alpha$. A polynomial
interpretation is called a _strongly linear interpretation_ (_SLI_ for short)
if all function symbols are interpreted by _weight functions_
$f_{\mathcal{A}}({x}_{1},\ldots,{x}_{n})=\sum_{i=1}^{n}x_{i}+c$ with
$c\in\mathbb{N}$. The _derivation length_ of a terminating term $s$ with
respect to $\to$ is defined as
$\operatorname{dl}(s,\to)\mathrel{:=}\max\\{{n\mid\exists t.\;s\to^{n}t}\\}$,
where $\to^{n}$ denotes the $n$-fold application of $\to$. The _innermost
runtime complexity function_
$\operatorname{rc}^{\text{\scriptsize$\operatorname{\mathsf{i}}$}}_{\mathcal{R}}$
with respect to a TRS $\mathcal{R}$ is defined as
$\operatorname{rc}^{\text{\scriptsize$\operatorname{\mathsf{i}}$}}_{\mathcal{R}}(n)\mathrel{:=}\max\\{\operatorname{dl}(t,\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}})\mid\text{$t\in\mathcal{T}_{\mathsf{b}}$
and $\lvert{t}\rvert\leqslant n$}\\}$. If no confusion can arise
$\operatorname{rc}^{\text{\scriptsize$\operatorname{\mathsf{i}}$}}_{\mathcal{R}}$
is simply called _runtime complexity function_.

Below we recall the bare essentials of the polynomial path order
$\mathrel{\blacktriangleright}$ on sequences (POP for short) as put forward in
Arai and Moser (2005). We kindly refer the reader to Arai and Moser (2005);
Avanzini and Moser (2008) for motivation and examples. We recall the
definition of _finite approximations $\mathrel{\blacktriangleright}_{k}^{l}$_
of $\mathrel{\blacktriangleright}$. The latter is conceived as the _limit_ of
these approximations. The domain of this order are so called _sequences_
$\operatorname{\mathcal{S}eq}(\mathcal{F},\mathcal{V})\mathrel{:=}\mathcal{T}(\mathcal{F}\cup\\{\circ\\},\mathcal{V})$.
Here $\mathcal{F}$ is a finite signature and $\circ\not\in\mathcal{F}$ a fresh
variadic function symbol, used to form sequences. We denote sequences
$\circ({s}_{1},\ldots,{s}_{n})$ by $[{s}_{1}\cdots{s}_{n}]$ and write
$a\mathrel{::}[{b}_{1}\cdots{b}_{n}]$ for the sequence $[a\leavevmode\nobreak\
{b}_{1}\cdots{b}_{n}]$.

Let $\succsim$ denote a precedence. The order
$\mathrel{\blacktriangleright}_{k}^{l}$ is based on an auxiliary order
$\mathrel{\gtrdot}_{k}^{l}$ (and the equivalence $\approx$ on terms defined
above). Below we set
${\mathrel{\not{\gtrsim}}_{k}^{l}}\mathrel{:=}{\mathrel{\gtrdot}_{k}^{l}}\cup{\approx}$.
We write ${\not{\\{}}t_{1},\dots,t_{n}{\not{\\}}}$ to denote multisets and
$\uplus$ for the multiset sum.

######  Definition 2.1.

Let $k,l\geqslant 1$. The order $\mathrel{\gtrdot}_{k}^{l}$ induced by
$\succsim$ is inductively defined as follows: $s\mathrel{\gtrdot}_{k}^{l}t$
for $s=f({s}_{1},\ldots,{s}_{n})$ or $s=[{s}_{1}\cdots{s}_{n}]$ if either

  1. (i)

$s_{i}\leavevmode\nobreak\ \mathrel{\not{\gtrsim}}_{k}^{l}\leavevmode\nobreak\
t$ for some $i\in\\{{1,\dots,n}\\}$, or

  2. (ii)

$s=f({s}_{1},\ldots,{s}_{n})$, $t=g({t}_{1},\ldots,{t}_{m})$ with $f\succ g$
or $t=[{t}_{1}\cdots{t}_{m}]$, $s\mathrel{\gtrdot}_{k}^{l-1}t_{j}$ for all
$j\in\\{{1,\dots,m}\\}$, and $m<k+\operatorname{\mathsf{width}}(s)$,

  3. (iii)

$s=[{s}_{1}\cdots{s}_{n}]$, $t=[{t}_{1}\cdots{t}_{m}]$ and the following
properties hold:

     * –

${\not{\\{}}{t}_{1},\ldots,{t}_{m}{\not{\\}}}=N_{1}\uplus\cdots\uplus N_{n}$
for some multisets $N_{1},\dots,N_{n}$, and

     * –

there exists $i\in\\{{1,\dots,n}\\}$ such that
${\not{\\{}}s_{i}{\not{\\}}}\not\approx^{\mathsf{mul}}N_{i}$, and

     * –

for all $1\leqslant i\leqslant n$ such that
${\not{\\{}}s_{i}{\not{\\}}}\not\approx^{\mathsf{mul}}N_{i}$ we have
$s_{i}\mathrel{\gtrdot}_{k}^{l}r$ for all $r\in N_{i}$, and
$m<k+\operatorname{\mathsf{width}}(s)$.

######  Definition 2.2.

Let $k,l\geqslant 1$. The _approximation
$\mathrel{\blacktriangleright}_{k}^{l}$ of the polynomial path order on
sequences_ induced by $\succsim$ is inductively defined as follows:
$s\mathrel{\blacktriangleright}_{k}^{l}t$ for $s=f({s}_{1},\ldots,{s}_{n})$ or
$s=[{s}_{1}\cdots{s}_{n}]$ if either $s\mathrel{\gtrdot}_{k}^{l}t$ or

  1. (i)

$s_{i}\mathrel{\not{\gtrsim}}_{k}^{l}t$ for some $i\in\\{{1,\dots,n}\\}$,

  2. (ii)

$s=f({s}_{1},\ldots,{s}_{n})$, $t=[{t}_{1}\cdots{t}_{m}]$, and the following
properties hold:

     * –

$s\mathrel{\blacktriangleright}_{k}^{l-1}t_{j_{0}}$ for some
$j_{0}\in\\{{1,\dots,m}\\}$,

     * –

$s\mathrel{\gtrdot}_{k}^{l-1}t_{j}$ for all $j\neq j_{0}$, and
$m<k+\operatorname{\mathsf{width}}(s)$,

  3. (iii)

$s=f({s}_{1},\ldots,{s}_{n})$, $t=g({t}_{1},\ldots,{t}_{m})$, $f\sim g$ and
$[{s}_{1}\cdots{s}_{n}]\mathrel{\blacktriangleright}_{k}^{l}[{t}_{1}\cdots{t}_{m}]$,
or

  4. (iv)

$s=[{s}_{1}\cdots{s}_{n}]$, $t=[{t}_{1}\cdots{t}_{m}]$ and the following
properties hold:

     * –

${\not{\\{}}{t}_{1},\ldots,{t}_{m}{\not{\\}}}=N_{1}\uplus\cdots\uplus N_{n}$
for some multisets $N_{1},\dots,N_{n}$, and

     * –

there exists $i\in\\{{1,\dots,n}\\}$ such that
${\not{\\{}}s_{i}{\not{\\}}}\not\approx^{\mathsf{mul}}N_{i}$, and

     * –

for all $1\leqslant i\leqslant n$ such that
${\not{\\{}}s_{i}{\not{\\}}}\not\approx^{\mathsf{mul}}N_{i}$ we have
$s_{i}\mathrel{\blacktriangleright}_{k}^{l}r$ for all $r\in N_{i}$, and
$m<k+\operatorname{\mathsf{width}}(s)$.

Above we set
${\mathrel{\not{\gtrsim}}_{k}^{l}}\mathrel{:=}{\mathrel{\blacktriangleright}_{k}^{l}}\cup{\approx}$
and abbreviate $\mathrel{\blacktriangleright}_{k}^{k}$ as
$\mathrel{\blacktriangleright}_{k}$ in the following. Note that the empty
sequence is minimal with respect to both orders. It is easy to see that for
$k\leqslant l$, we have
${\mathrel{\gtrdot}_{k}}\subseteq{\mathrel{\gtrdot}_{l}}$ and
${\mathrel{\blacktriangleright}_{k}}\subseteq{\mathrel{\blacktriangleright}_{l}}$.
Note that $s\mathrel{\blacktriangleright}_{k}t$ implies that
$\operatorname{\mathsf{width}}(t)<\operatorname{\mathsf{width}}(s)+k$. For a
fixed approximation $\mathrel{\blacktriangleright}_{k}$, we define the length
of its longest decent as follows: $\mathsf{G}_{k}(t)\mathrel{:=}\max\\{{n\mid
t=t_{0}\mathrel{\blacktriangleright}_{k}t_{1}\mathrel{\blacktriangleright}_{k}\dots\mathrel{\blacktriangleright}_{k}t_{n}}\\}$.
The following proposition is a reformulation of (Arai and Moser, 2005, Lemma
6).

######  Proposition 2.3.

Let $k\in\mathbb{N}$. There exists a polynomial interpretation $\mathcal{A}$
such that $\mathsf{G}_{k}(t)\leqslant[\alpha]_{\mathcal{A}}(t)$ for all
assignments $\alpha\,\colon\,\mathcal{V}\to\mathbb{N}$. As a consequence, for
all terms $f({t}_{1},\ldots,{t}_{n})$ with
$[\alpha]_{\mathcal{A}}(t_{i})=\operatorname{\mathsf{O}}(\lvert{t_{i}}\rvert)$,
$\mathsf{G}_{k}(f({t}_{1},\ldots,{t}_{n}))$ is bounded by a polynomial $p$ in
the size of $t$, where $p$ depends on $k$ only.

Observe that the polynomial interpretation $\mathcal{A}$ as employed in the
proposition fulfils:
$\circ_{\mathcal{A}}({m}_{1},\ldots,{m}_{n})=\sum_{i=1}^{n}m_{i}+n$. In
particular, we have $[\alpha]_{\mathcal{A}}([])=0$.

##  3 Complexity Analysis Based on the Dependency Pair Method

In this section, we briefly recall the central definitions and results
established in Hirokawa and Moser (2008b, a). We kindly refer the reader to
Hirokawa and Moser (2008b, a) for further examples and underlying intuitions.
Let $\mathcal{X}$ be a set of symbols. We write
$C\langle{t}_{1},\ldots,{t}_{n}\rangle_{\mathcal{X}}$ to denote
$C[{t}_{1},\ldots,{t}_{n}]$, whenever
$\operatorname{\mathsf{rt}}(t_{i})\in\mathcal{X}$ for all
$i\in\\{{1,\dots,n}\\}$ and $C$ is a $n$-hole context containing no symbols
from $\mathcal{X}$. We set
$\mathcal{D}^{\sharp}\mathrel{:=}\mathcal{D}\cup\\{{f^{\sharp}\mid
f\in\mathcal{D}}\\}$ with each $f^{\sharp}$ a fresh function symbol. Further,
for $t=f({t}_{1},\ldots,{t}_{n})$ with $f\in\mathcal{D}$, we set
$t^{\sharp}\mathrel{:=}f^{\sharp}({t}_{1},\ldots,{t}_{n})$.

######  Definition 3.1.

Let $\mathcal{R}$ be a TRS. If $l\to r\in\mathcal{R}$ and
$r=C\langle{u}_{1},\ldots,{u}_{n}\rangle_{\mathcal{D}}$ then
$l^{\sharp}\to\operatorname{COM}(u_{1}^{\sharp},\ldots,u_{n}^{\sharp})$ is
called a _weak innermost dependency pair_ of $\mathcal{R}$. Here
$\operatorname{COM}(t)=t$ and
$\operatorname{COM}({t}_{1},\ldots,{t}_{n})=\mathsf{c}(t_{1},\ldots,t_{n})$,
$n\not=1$, for a fresh constructor symbol $\mathsf{c}$, the _compound symbol_.
The set of all weak innermost dependency pairs is denoted by
$\mathsf{WIDP}(\mathcal{R})$.

######  Example 3.2.

Reconsider the example $\mathcal{R}_{\textsf{bits}}$ from the introduction.
The set of weak innermost dependency pairs
$\mathsf{WIDP}(\mathcal{R}_{\textsf{bits}})$ is given by

$\displaystyle 7\colon$ $\displaystyle\mathsf{half}^{\sharp}(\mathsf{0})$
$\displaystyle\to\mathsf{c_{1}}$ $\displaystyle 10\colon$
$\displaystyle\mathsf{bits}^{\sharp}(\mathsf{0})$
$\displaystyle\to\mathsf{c_{3}}$ $\displaystyle 8\colon$
$\displaystyle\mathsf{half}^{\sharp}(\mathsf{s}(\mathsf{0}))$
$\displaystyle\to\mathsf{c_{2}}$ $\displaystyle 11\colon$
$\displaystyle\mathsf{bits}^{\sharp}(\mathsf{s}(\mathsf{0}))$
$\displaystyle\to\mathsf{c_{4}}$ $\displaystyle 9\colon$
$\displaystyle\mathsf{half}^{\sharp}(\mathsf{s}(\mathsf{s}(x)))$
$\displaystyle\to\mathsf{half}^{\sharp}(x)$ $\displaystyle\hskip
12.91663pt12\colon$
$\displaystyle\mathsf{bits}^{\sharp}(\mathsf{s}(\mathsf{s}(x)))$
$\displaystyle\to\mathsf{bits}^{\sharp}(\mathsf{s}(\mathsf{half}(x)))$

We write $f\rhd_{\mathrm{d}}g$ if there exists a rewrite rule $l\to
r\in\mathcal{R}$ such that $f=\operatorname{\mathsf{rt}}(l)$ and $g$ is a
defined symbol in $\operatorname{\mathsf{Fun}}(r)$. For a set $\mathcal{G}$ of
defined symbols we denote by $\mathcal{R}{\restriction}\mathcal{G}$ the set of
rewrite rules $l\to r\in\mathcal{R}$ with
$\operatorname{\mathsf{rt}}(l)\in\mathcal{G}$. The set $\mathcal{U}(t)$ of
usable rules of a term $t$ is defined as
$\mathcal{R}{\restriction}\\{{g\mid\text{$f\rhd_{\mathrm{d}}^{*}g$ for some
$f\in\operatorname{\mathsf{Fun}}(t)$}}\\}$. Finally, we define
$\mathcal{U}(\mathcal{P})=\bigcup_{l\to r\in\mathcal{P}}\mathcal{U}(r)$.

######  Example 3.3 (Example 3.2 continued).

The usable rules of $\mathsf{WIDP}(\mathcal{R}_{\textsf{bits}})$ consist of
the following rules: $1\colon\mathsf{half}(\mathsf{0})\to\mathsf{0}$,
$2\colon\mathsf{half}(\mathsf{s}(\mathsf{0}))\to\mathsf{0}$, and
$3\colon\mathsf{half}(\mathsf{s}(\mathsf{s}(x)))\to\mathsf{half}(x)$.

The following proposition allows the analysis of the (innermost) runtime
complexity through the study of (innermost) relative rewriting, see Hirokawa
and Moser (2008b) for the proof.

######  Proposition 3.4.

Let $\mathcal{R}$ be a TRS, let $t$ be a basic terminating term, and let
$\mathcal{P}=\mathsf{WIDP}(\mathcal{R})$. Then
$\operatorname{dl}(t,\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}})\leqslant\operatorname{dl}(t^{\sharp},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{U}(\mathcal{P})\,\cup\,\mathcal{P}}})$.
Moreover, if $\mathcal{P}$ is non-duplicating and
${\mathcal{U}(\mathcal{P})}\subseteq{>_{\mathcal{A}}}$ for some SLI
$\mathcal{A}$. Then there exist constants $K,L\geqslant 0$ (depending on
$\mathcal{P}$ and $\mathcal{A}$ only) such that
$\operatorname{dl}(t,\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}})\leqslant
K\cdot\operatorname{dl}(t^{\sharp},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{P}/\mathcal{U}(\mathcal{P})}})+L\cdot\lvert{t^{\sharp}}\rvert$.

This approach admits also an integration of _dependency graphs_ Arts and Giesl
(2000) in the context of complexity analysis. The nodes of the _weak innermost
dependency graph_ $\mathsf{WIDG}(\mathcal{R})$ are the elements of
$\mathcal{P}$ and there is an arrow from $s\to t$ to $u\to v$ if there exist a
context $C$ and substitutions $\sigma$, $\tau$ such that
$t\sigma\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{R}}}C[u\tau]$.
Let $\mathcal{G}=\mathsf{WIDG}(\mathcal{R})$; a _strongly connected component_
(_SCC_ for short) in $\mathcal{G}$ is a maximal _strongly connected subgraph_.
We write ${\mathcal{G}}/_{\\!\equiv}$ for the _congruence graph_ , where
$\equiv$ is the equivalence relation induced by SCCs.

######  Example 3.5 (Example 3.2 continued).

$\mathcal{G}=\mathsf{WIDG}(\mathcal{R}_{\textsf{bits}})$ consists of the nodes
(7)–(12) as mentioned in Example 3.2 and has the following shape:

798101211

The only non-trivial SCCs in $\mathcal{G}$ are $\\{9\\}$ and $\\{12\\}$. Hence
${\mathcal{G}}/_{\\!\equiv}$ consists of the nodes
$[7]_{\equiv}$–$[12]_{\equiv}$, and edges $([a]_{\equiv},[b]_{\equiv})$ for
edges $(a,b)$ in $\mathcal{G}$. Here $[a]_{\equiv}$ denotes the equivalence
class of $a$.

We set
$\operatorname{\mathsf{L}}(t)\mathrel{:=}\max\\{{\operatorname{dl}(t,\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{P}_{m}/\mathcal{S}}})\mid\text{$(\mathcal{P}_{1},\ldots,\mathcal{P}_{m})$
a path in ${\mathcal{G}}/_{\\!\equiv}$,
$\mathcal{P}_{1}\in\mathsf{Src}$}}\\}$, where $\mathsf{Src}$ denote the set o
f source nodes from ${\mathcal{G}}/_{\\!\equiv}$ and
$\mathcal{S}=\mathcal{P}_{1}\cup\cdots\cup\mathcal{P}_{m-1}\cup\mathcal{U}(\mathcal{P}_{1}\cup\cdots\cup\mathcal{P}_{m})$.
The proposition allows the use of different techniques to analyse polynomial
runtime complexity on separate paths, cf. Hirokawa and Moser (2008a).

######  Proposition 3.6.

Let $\mathcal{R}$, $\mathcal{P}$, and $t$ be as above. Then there exists a
polynomial $p$ (depending only on $\mathcal{R}$) such that
$\operatorname{dl}(t^{\sharp},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{P}/\mathcal{U}(\mathcal{P})}})\leqslant
p(\operatorname{\mathsf{L}}(t^{\sharp}))$.

##  4 The Polynomial Path Order over Quasi-Precedences

In this section, we briefly recall the central definitions and results
established in Avanzini and Moser (2008); Avanzini et al. (2008) on the
_polynomial path order_. We employ the variant of $\textsc{POP}^{\ast}$ based
on quasi-precendences, cf. Avanzini et al. (2008).

As mentioned in the introduction, $\textsc{POP}^{\ast}$ relies on tiered
recursion, which is captured by the notion of _safe mapping_. A _safe mapping_
$\operatorname{\mathsf{safe}}$ is a function that associates with every
$n$-ary function symbol $f$ the set of _safe argument positions_. If
$f\in\mathcal{D}$ then
$\operatorname{\mathsf{safe}}(f)\subseteq\\{{1,\dots,n}\\}$, for
$f\in\mathcal{C}$ we fix $\operatorname{\mathsf{safe}}(f)=\\{{1,\dots,n}\\}$.
The argument positions not included in $\operatorname{\mathsf{safe}}(f)$ are
called _normal_ and denoted by $\operatorname{\mathsf{nrm}}(f)$. We extend
$\operatorname{\mathsf{safe}}$ to terms $t\not\in\mathcal{V}$ as follows: we
define
$\operatorname{\mathsf{safe}}(f({t}_{1},\ldots,{t}_{n}))\mathrel{:=}\\{{t_{i_{1}},\dots,t_{i_{p}}}\\}$
where $\operatorname{\mathsf{safe}}(f)=\\{{{i}_{1},\ldots,{i}_{p}}\\}$,
likewise we define
$\operatorname{\mathsf{nrm}}(f({t}_{1},\ldots,{t}_{n}))\mathrel{:=}\\{{t_{j_{1}},\dots,t_{j_{q}}}\\}$
where $\operatorname{\mathsf{nrm}}(f)=\\{{{j}_{1},\ldots,{j}_{q}}\\}$. Not
every precedence is suitable for $\mathrel{{>}_{\mathsf{pop*}}}$, in
particular we need to assert that constructors are minimal.

We say that a precedence $\succsim$ is _admissible_ for $\textsc{POP}^{\ast}$
if the following is satisfied: (i) $f\succ g$ with $g\in\mathcal{D}$ implies
$f\in\mathcal{D}$, and (ii) if $f\approx g$ then $f\in\mathcal{D}$ if and only
if $g\in\mathcal{D}$. In the sequel we assume any precedence is admissible. We
extend the equivalence $\approx$ to the context of safe mapping:
$s\mathrel{\text{\raisebox{-1.00006pt}{$\stackrel{{\scriptstyle\text{{\raisebox{-0.70004pt}{\tiny{$\operatorname{\mathsf{safe}}$}}}}}}{{\approx}}$}}}t$,
if (i) $s=t$, or (ii) $s=f({s}_{1},\ldots,{s}_{n})$,
$t=g({t}_{1},\ldots,{t}_{n})$, $f\approx g$ and there exists a permutation
$\pi$ so that
$s_{i}\mathrel{\text{\raisebox{-1.00006pt}{$\stackrel{{\scriptstyle\text{{\raisebox{-0.70004pt}{\tiny{$\operatorname{\mathsf{safe}}$}}}}}}{{\approx}}$}}}t_{\pi(i)}$,
where $i\in\operatorname{\mathsf{safe}}(f)$ if and only if
$\pi(i)\in\operatorname{\mathsf{safe}}(g)$ for all $i\in\\{{1,\dots,n}\\}$.
Similar to POP, the definition of the polynomial path order
$\mathrel{{>}_{\mathsf{pop*}}}$ makes use of an auxiliary order
$\mathrel{{>}_{\mathsf{pop}}}$.

######  Definition 4.1.

The auxiliary order $\mathrel{{>}_{\mathsf{pop}}}$ induced by $\succsim$ and
$\operatorname{\mathsf{safe}}$ is inductively defined as follows:
$s=f({s}_{1},\ldots,{s}_{n})\mathrel{{>}_{\mathsf{pop}}}t$ if either

  1. (i)

$s_{i}\mathrel{\text{\raisebox{0.0pt}{${\not{>}}_{\text{\raisebox{2.0pt}{$\mathsf{pop}$}}}$}}}t$
for some $i\in\\{{1,\dots,n}\\}$, and if $f\in\mathcal{D}$ then
$i\in\operatorname{\mathsf{nrm}}(f)$, or

  2. (ii)

$t=g({t}_{1},\ldots,{t}_{m})$, $f\succ g$, $f\in\mathcal{D}$ and
$s\mathrel{{>}_{\mathsf{pop}}}t_{j}$ for all $j\in\\{{1,\dots,m}\\}$.

######  Definition 4.2.

The _polynomial path order_ $\mathrel{{>}_{\mathsf{pop*}}}$ induced by
$\succsim$ and $\operatorname{\mathsf{safe}}$ is inductively defined as
follows: $s=f({s}_{1},\ldots,{s}_{n})\mathrel{{>}_{\mathsf{pop*}}}t$ if either
$s\mathrel{{>}_{\mathsf{pop}}}t$ or

  1. (i)

$s_{i}\mathrel{\text{\raisebox{0.0pt}{${\not{>}}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}t$
for some $i\in\\{{1,\dots,n}\\}$, or

  2. (ii)

$t=g({t}_{1},\ldots,{t}_{m})$, $f\succ g$, $f\in\mathcal{D}$, and

     * –

$s\mathrel{{>}_{\mathsf{pop*}}}t_{j_{0}}$ for some
$j_{0}\in\operatorname{\mathsf{safe}}(g)$, and

     * –

for all $j\neq j_{0}$ either $s\mathrel{{>}_{\mathsf{pop}}}t_{j}$, or $s\rhd
t_{j}$ and $j\in\operatorname{\mathsf{safe}}(g)$, or

  3. (iii)

$t=g({t}_{1},\ldots,{t}_{m})$, $f\approx g$,
$\operatorname{\mathsf{nrm}}(s)\mathrel{>_{\mathsf{pop*}}^{\mathsf{mul}}}\operatorname{\mathsf{nrm}}(t)$
and
$\operatorname{\mathsf{safe}}(s)\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\mathsf{mul}}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}\operatorname{\mathsf{safe}}(t)$.

Above we set
${\mathrel{\text{\raisebox{0.0pt}{${\not{>}}_{\text{\raisebox{2.0pt}{$\mathsf{pop}$}}}$}}}}\mathrel{:=}{\mathrel{{>}_{\mathsf{pop}}}}\cup{\mathrel{\text{\raisebox{-1.00006pt}{$\stackrel{{\scriptstyle\text{{\raisebox{-0.70004pt}{\tiny{$\operatorname{\mathsf{safe}}$}}}}}}{{\approx}}$}}}}$
and
${\mathrel{\text{\raisebox{0.0pt}{${\not{>}}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}\mathrel{:=}{\mathrel{{>}_{\mathsf{pop*}}}}\cup{\mathrel{\text{\raisebox{-1.00006pt}{$\stackrel{{\scriptstyle\text{{\raisebox{-0.70004pt}{\tiny{$\operatorname{\mathsf{safe}}$}}}}}}{{\approx}}$}}}}$
below. Here $\mathrel{>_{\mathsf{pop*}}^{\mathsf{mul}}}$ and
$\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\mathsf{mul}}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}$
refer to the strict and weak multiset extension of
$\mathrel{\text{\raisebox{0.0pt}{${\not{>}}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}$
respectively.

The intuition of $\mathrel{{>}_{\mathsf{pop}}}$ is to deny any recursive call,
whereas $\mathrel{{>}_{\mathsf{pop*}}}$ allows predicative recursion: by the
restrictions imposed by $\operatorname{\mathsf{safe}}$, recursion needs to be
performed on normal arguments, while a recursively computed result must only
be used in a safe argument position, compare Bellantoni and Cook (1992). Note
that the alternative $s\rhd t_{j}$ for $j\in\operatorname{\mathsf{safe}}(g)$
in Definition 4.2(ii) guarantees that $\textsc{POP}^{\ast}$ characterises the
class of polytime computable functions, cf. Avanzini and Moser (2008). The
proof of the next theorem follows the pattern of the proof of main theorem in
Avanzini and Moser (2008), but the result is stronger due to the extension to
quasi-precedences.

######  Theorem 4.3.

Let $\mathcal{R}$ be a constructor TRS. If $\mathcal{R}$ is compatible with
$\mathrel{{>}_{\mathsf{pop*}}}$, i.e.,
${\mathcal{R}}\subseteq{\mathrel{{>}_{\mathsf{pop*}}}}$, then the innermost
runtime complexity
$\operatorname{rc}^{\text{\scriptsize$\operatorname{\mathsf{i}}$}}_{\mathcal{R}}$
induced is polynomially bounded.

Note that Theorem 4.3 is too weak to handle the TRS
$\mathcal{R}_{\textsf{bits}}$ as the (necessary) restriction to an admissible
precedence is too strong. To rectify this, we suit $\textsc{POP}^{\ast}$ so
that it can be used in conjunction with weak (innermost) dependency pairs.

An argument filtering (for a signature $\mathcal{F}$) is a mapping $\pi$ that
assigns to every $n$-ary function symbol $f\in\mathcal{F}$ an argument
position $i\in\\{1,\dots,n\\}$ or a (possibly empty) list
$\\{{i}_{1},\ldots,{i}_{m}\\}$ of argument positions with $1\leqslant
i_{1}<\cdots<i_{m}\leqslant n$. The signature $\mathcal{F}_{\pi}$ consists of
all function symbols $f$ such that $\pi(f)$ is some list
$\\{{i}_{1},\ldots,{i}_{m}\\}$, where in $\mathcal{F}_{\pi}$ the arity of $f$
is $m$. Every argument filtering $\pi$ induces a mapping from
$\mathcal{T}(\mathcal{F},\mathcal{V})$ to
$\mathcal{T}(\mathcal{F}_{\pi},\mathcal{V})$, also denoted by $\pi$:

$\pi(t)=\begin{cases}t&\text{if $t$ is a variable}\\\ \pi(t_{i})&\text{if
$t=f({t}_{1},\ldots,{t}_{n})$ and $\pi(f)=i$}\\\
f(\pi(t_{k_{1}}),\dots,\pi(t_{k_{m}}))&\text{if $t=f({t}_{1},\ldots,{t}_{n})$
and $\pi(f)=\\{{i}_{1},\ldots,{i}_{m}\\}$}\hbox to0.0pt{$\;$.\hss}\end{cases}$

######  Definition 4.4.

Let $\pi$ denote an argument filtering, and $\mathrel{{>}_{\mathsf{pop*}}}$ a
polynomial path order. We define $s\mathrel{{>}^{\pi}_{\mathsf{pop*}}}t$ if
and only if $\pi(s)\mathrel{{>}_{\mathsf{pop*}}}\pi(t)$, and likewise
$s\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}t$
if and only if
$\pi(s)\mathrel{\text{\raisebox{0.0pt}{${\not{>}}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}\pi(t)$.

######  Example 4.5 (Example 3.2 continued).

Let $\pi$ be defined as follows: $\pi(\mathsf{half})=1$ and
$\pi(f)=\\{1,\dots,n\\}$ for each $n$-ary function symbol other than
$\mathsf{half}$. Compatibility of $\mathsf{WIDP}(\mathcal{R}_{\textsf{bits}})$
with $\mathrel{{>}^{\pi}_{\mathsf{pop*}}}$ amounts to the following set of
order constraints:

$\displaystyle\mathsf{half}^{\sharp}(0)$
$\displaystyle\mathrel{{>}_{\mathsf{pop*}}}\mathsf{c_{1}}$
$\displaystyle\mathsf{bits}^{\sharp}(0)$
$\displaystyle\mathrel{{>}_{\mathsf{pop*}}}\mathsf{c_{3}}$
$\displaystyle\mathsf{half}^{\sharp}(\mathsf{s}(\mathsf{s}(x)))$
$\displaystyle\mathrel{{>}_{\mathsf{pop*}}}\mathsf{half}^{\sharp}(x)$
$\displaystyle\mathsf{half}^{\sharp}(\mathsf{s}(0))$
$\displaystyle\mathrel{{>}_{\mathsf{pop*}}}\mathsf{c_{2}}$
$\displaystyle\mathsf{bits}^{\sharp}(\mathsf{s}(0))$
$\displaystyle\mathrel{{>}_{\mathsf{pop*}}}\mathsf{c_{4}}$
$\displaystyle\mathsf{bits}^{\sharp}(\mathsf{s}(\mathsf{s}(x)))$
$\displaystyle\mathrel{{>}_{\mathsf{pop*}}}\mathsf{bits}^{\sharp}(\mathsf{s}(x))$

In order to define a $\textsc{POP}^{\ast}$ instance
$\mathrel{{>}_{\mathsf{pop*}}}$, we set
$\operatorname{\mathsf{safe}}(\mathsf{bits}^{\sharp})=\operatorname{\mathsf{safe}}(\mathsf{half})=\operatorname{\mathsf{safe}}(\mathsf{half}^{\sharp})=\varnothing$
and $\operatorname{\mathsf{safe}}(\mathsf{s})=\\{{1}\\}$. Furthermore, we
define an (admissible) precedence:
$0\approx\mathsf{c_{1}}\approx\mathsf{c_{2}}\approx\mathsf{c_{3}}\approx\mathsf{c_{4}}$.
The easy verification of
$\mathsf{WIDP}(\mathcal{R}_{\textsf{bits}})\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$
is left to the reader.

##  5 Dependency Pairs and Polynomial Path Orders

Motivated by Example 4.5, we show in this section that the pair
($\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}},\mathrel{{>}^{\pi}_{\mathsf{pop*}}}$)
can play the role of a _safe_ reduction pair, cf. Hirokawa and Moser (2008b,
a). Let $\mathcal{R}$ be a TRS over a signature $\mathcal{F}$ that is
innermost terminating. In the sequel $\mathcal{R}$ is kept fixed. Moreover, we
fix some safe mapping $\operatorname{\mathsf{safe}}$, an admissible precedence
$\succsim$, and an argument filtering $\pi$. We refer to the induced
$\textsc{POP}^{\ast}$ instance by $\mathrel{{>}^{\pi}_{\mathsf{pop*}}}$.

We adapt $\operatorname{\mathsf{safe}}$ to $\mathcal{F}_{\pi}$ in the obvious
way: for each $f_{\pi}\in\mathcal{F}_{\pi}$ with corresponding
$f\in\mathcal{F}$, we define
$\operatorname{\mathsf{safe}}(f_{\pi})\mathrel{:=}\operatorname{\mathsf{safe}}(f)\cap\pi(f)$,
and likewise
$\operatorname{\mathsf{nrm}}(f_{\pi})\mathrel{:=}\operatorname{\mathsf{nrm}}(f)\cap\pi(f)$.
Set
${\mathsf{Val}}_{\pi}\mathrel{:=}\mathcal{T}({\mathcal{C}}_{\pi},\mathcal{V})$.
Based on $\mathcal{F}_{\pi}$ we define the _normalised signature_
$\mathcal{F}^{\operatorname{\mathsf{n}}}_{\pi}\mathrel{:=}\\{{f^{\operatorname{\mathsf{n}}}\mid
f\in\mathcal{F}_{\pi}}\\}$ where the arity of $f^{\operatorname{\mathsf{n}}}$
is $\lvert{\operatorname{\mathsf{nrm}}(f)}\rvert$. We extend $\succsim$ to
$\mathcal{F}^{\operatorname{\mathsf{n}}}_{\pi}$ by
$f^{\operatorname{\mathsf{n}}}\succsim g^{\operatorname{\mathsf{n}}}$ if and
only if $f\succsim g$. Let $\mathsf{s}$ be a fresh constant that is minimal
with respect to $\succsim$. We introduce the _Buchholz norm_ of $t$ (denoted
as $\lVert{t}\rVert$) a term complexity measure that fits well with the
definition of $\textsc{POP}^{\ast}$. Set
$\lVert{t}\rVert\mathrel{:=}1+\max\\{{n,\lVert{t_{1}}\rVert,\dots,\lVert{t_{n}}\rVert}\\}$
for $t=f({t}_{1},\ldots,{t}_{n})$ and $\lVert{t}\rVert\mathrel{:=}1$,
otherwise. In the following we define an embedding from the relative rewriting
relation
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}}$
into $\mathrel{\blacktriangleright}_{k}$, such that $k$ depends only on TRSs
$\mathcal{R}$ and $\mathcal{S}$. This embedding provides the technical tool to
measure the number of root steps in a given derivation through the number of
descent in $\mathrel{\blacktriangleright}_{k}$. Hence Proposition 2.3 becomes
applicable to establishing our main result. This intuition is cast into the
next definition.

######  Definition 5.1.

A _predicative interpretation_ is a pair of mappings
$(\mathsf{S}_{\pi},\mathsf{N}_{\pi})$ from terms to sequences
$\operatorname{\mathcal{S}eq}(\mathcal{F}^{\operatorname{\mathsf{n}}}_{\pi}\cup\\{{\mathsf{s}}\\},\mathcal{V})$
defined as follows. We assume for $\pi(t)=f(\pi(t_{1}),\dots,\pi(t_{n}))$ that
$\operatorname{\mathsf{safe}}(f)=\\{{i_{1},\dots,i_{p}}\\}$ and
$\operatorname{\mathsf{nrm}}(f)=\\{{j_{1},\dots,j_{q}}\\}$.

$\displaystyle\mathsf{S}_{\pi}(t)$
$\displaystyle\mathrel{:=}\begin{cases}[\,]&\text{if
$\pi(t)\in{\mathsf{Val}}_{\pi}$},\\\
[f^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(t_{j_{1}}),\dots,\mathsf{N}_{\pi}(t_{j_{q}}))\leavevmode\nobreak\
\mathsf{S}_{\pi}(t_{i_{1}})\leavevmode\nobreak\ \cdots\leavevmode\nobreak\
\mathsf{S}_{\pi}(t_{i_{p}})]&\text{if
$\pi(t)\not\in{\mathsf{Val}}_{\pi}$.}\end{cases}$
$\displaystyle\mathsf{N}_{\pi}(t)$
$\displaystyle\mathrel{:=}\mathsf{S}_{\pi}(t)\mathrel{::}\operatorname{\mathsf{BN_{\pi}}}(t)$

Here the function $\operatorname{\mathsf{BN_{\pi}}}$ maps a term $t$ to the
sequence $[\mathsf{s}\cdots\mathsf{s}]$ with $\lVert{\pi(t)}\rVert$
occurrences of the constant $\mathsf{s}$.

Note that as a direct consequence of the definitions we obtain
$\operatorname{\mathsf{width}}(\mathsf{N}_{\pi}(t))=\lVert{\pi(t)}\rVert+1$
for all terms $t$.

######  Lemma 5.2.

There exists a polynomial $p$ such that
$\mathsf{G}_{k}(\mathsf{N}_{\pi}(t))\leqslant p(\lvert{t}\rvert)$ for every
basic term $t$. The polynomial $p$ depends only on $k$.

###### Proof.

Suppose $t=f({v}_{1},\ldots,{v}_{n})$ is a basic term with
$\operatorname{\mathsf{safe}}(f)=\\{{{i}_{1},\ldots,{i}_{p}}\\}$ and
$\operatorname{\mathsf{nrm}}(f)=\\{{{j}_{1},\ldots,{j}_{q}}\\}$. The only non-
trivial case is when $\pi(t)\not\in{\mathsf{Val}}_{\pi}$. Then

$\mathsf{N}_{\pi}(t)=[u\leavevmode\nobreak\
\mathsf{S}_{\pi}(v_{i_{1}})\cdots\mathsf{S}_{\pi}(v_{i_{p}})]\mathrel{::}\operatorname{\mathsf{BN_{\pi}}}(t)$

where
$u=f^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(v_{j_{1}}),\dots,\mathsf{N}_{\pi}(v_{j_{q}}))$.
Note that $\mathsf{S}_{\pi}(v_{i})=[\,]$ for
$i\in\\{{{i}_{1},\ldots,{i}_{q}}\\}$. Let $\mathcal{A}$ denote a polynomial
interpretation fulfilling Proposition 2.3. Using the assumption
$\circ_{\mathcal{A}}({m}_{1},\ldots,{m}_{n})=\sum_{i=1}^{n}m_{i}+n$, it is
easy to see that $\mathsf{G}_{k}(\mathsf{N}_{\pi}(t))$ is bounded linear in
$\lVert{\pi(t)}\rVert\leqslant\lvert{t}\rvert$ and
$[\alpha]_{\mathcal{A}}(u)$. As
$\mathsf{N}_{\pi}(v_{j})=[[]\leavevmode\nobreak\ \mathsf{s}\cdots\mathsf{s}]$
with $\lVert{\pi(v_{j})}\rVert\leqslant\lvert{t}\rvert$ occurrences of
$\mathsf{s}$, $\mathsf{G}_{k}(\mathsf{N}_{\pi}(v_{j}))$ is linear in
$\lvert{t}\rvert$. Hence from Proposition 2.3 we conclude that
$\mathsf{G}_{k}(\mathsf{N}_{\pi}(t))$ is polynomially bounded in
$\lvert{t}\rvert$. ∎

The next sequence of lemmas shows that the relative rewriting relation
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}}$
is embeddable into $\mathrel{\blacktriangleright}_{k}$.

######  Lemma 5.3.

Suppose $s\mathrel{{>}^{\pi}_{\mathsf{pop*}}}t$ such that
$\pi(s\sigma)\in{\mathsf{Val}}_{\pi}$. Then
$\mathsf{S}_{\pi}(s\sigma)=[\,]=\mathsf{S}_{\pi}(t\sigma)$ and
$\mathsf{N}_{\pi}(s\sigma)\mathrel{\blacktriangleright}_{1}\mathsf{N}_{\pi}(t\sigma)$.

###### Proof.

Let $\pi(s\sigma)\in{\mathsf{Val}}_{\pi}$, and suppose
$s\mathrel{{>}^{\pi}_{\mathsf{pop*}}}t$, i.e.,
$\pi(s)\mathrel{{>}_{\mathsf{pop*}}}\pi(t)$ holds. Observe that since
$\pi(s)\in{\mathsf{Val}}_{\pi}$ and due to our assumptions on safe mappings,
only clause $(1)$ from the definition of $\mathrel{{>}_{\mathsf{pop*}}}$ (or
respectively $\mathrel{{>}_{\mathsf{pop}}}$) is applicable. And thus $\pi(t)$
is a subterm of $\pi(s)$ modulo the equivalence $\approx$. We conclude
$\pi(t\sigma)\in{\mathsf{Val}}_{\pi}$, and hence
$\mathsf{S}_{\pi}(s\sigma)=[\,]=\mathsf{S}_{\pi}(t\sigma)$. Finally, notice
that $\lVert{\pi(s\sigma)}\rVert>\lVert{\pi(t\sigma)}\rVert$ as $\pi(t\sigma)$
is a subterm of $\pi(s\sigma)$. Thus
$\mathsf{N}_{\pi}(s\sigma)\mathrel{\blacktriangleright}_{1}\mathsf{N}_{\pi}(t\sigma)$
follows as well. ∎

To improve the clarity of the exposition, we concentrate on the curcial cases
in the proofs of the following lemma. The interested reader is kindly referred
to Avanzini (2009) for the full proof.

######  Lemma 5.4.

Suppose $s\mathrel{{>}^{\pi}_{\mathsf{pop}}}t$ such that
$\pi(s\sigma)=f(\pi(s_{1}\sigma),\dots,\pi(s_{n}\sigma))$ with
$\pi(s_{i}\sigma)\in{\mathsf{Val}}_{\pi}$ for $i\in\\{{1,\dots,n}\\}$.
Moreover suppose $\operatorname{\mathsf{nrm}}(f)=\\{{j_{1},\dots,j_{q}}\\}$.
Then

$f^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(s_{j_{1}}\sigma),\dots,\mathsf{N}_{\pi}(s_{j_{q}}\sigma))\mathrel{\gtrdot}_{3\cdot\lVert{\pi(t)}\rVert}\mathsf{N}_{\pi}(t\sigma)$

holds.

###### Proof.

Note that the assumption implies that the argument filtering $\pi$ does not
collapse $f$. We show the lemma by induction on
$\mathrel{{>}^{\pi}_{\mathsf{pop}}}$. We consider the subcase that
$s\mathrel{{>}^{\pi}_{\mathsf{pop}}}t$ follows as
$t=g({t}_{1},\ldots,{t}_{m})$, $\pi$ does not collapse on $g$, $f\succ g$, and
$s\mathrel{{>}^{\pi}_{\mathsf{pop}}}t_{j}$ for all $j\in\pi(g)$, cf.
Definition 4.1(ii). We set
$u\mathrel{:=}f^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(s_{j_{1}}\sigma),\dots,\mathsf{N}_{\pi}(s_{j_{q}}\sigma))$
and $k\mathrel{:=}3\cdot\lVert{\pi(t)}\rVert$ and first prove
$u\mathrel{\gtrdot}_{k-1}\mathsf{S}_{\pi}(t\sigma)$.

If $\pi(t\sigma)\in{\mathsf{Val}}_{\pi}$, then
$\mathsf{S}_{\pi}(t\sigma)=[\,]$ is minimal with respect to
$\mathrel{\gtrdot}_{k-1}$. Thus we are done. Hence suppose
$\operatorname{\mathsf{nrm}}(g)=\\{{j^{\prime}_{1},\dots,j^{\prime}_{q}}\\}$,
$\operatorname{\mathsf{safe}}(g)=\\{{i^{\prime}_{1},\dots,i^{\prime}_{p}}\\}$
and let

$\mathsf{S}_{\pi}(t\sigma)=[g^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(t_{j^{\prime}_{1}}\sigma),\dots,\mathsf{N}_{\pi}(t_{j^{\prime}_{q}}\sigma))\leavevmode\nobreak\
\mathsf{S}_{\pi}(t_{i^{\prime}_{1}}\sigma)\cdots\mathsf{S}_{\pi}(t_{i^{\prime}_{p}}\sigma)]\hbox
to0.0pt{$\;$.\hss}$

We set
$v\mathrel{:=}g^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(t_{j^{\prime}_{1}}\sigma),\dots,\mathsf{N}_{\pi}(t_{j^{\prime}_{q}}\sigma))$.
It suffices to show $u\mathrel{\gtrdot}_{k-2}v$ and
$u\mathrel{\gtrdot}_{k-2}\mathsf{S}_{\pi}(t_{j}\sigma)$ for
$j\in\operatorname{\mathsf{safe}}(g)$. Both assertions follow from the
induction hypothesis.

Now consider
$\mathsf{N}_{\pi}(t\sigma)=[\mathsf{S}_{\pi}(t\sigma)\leavevmode\nobreak\
\mathsf{s}\cdots\mathsf{s}]$ with $\lVert{\pi(t\sigma)}\rVert$ occurrences of
the constant $\mathsf{s}$. Recall that
$\operatorname{\mathsf{width}}(\mathsf{N}_{\pi}(t\sigma))=\lVert{\pi(t\sigma)}\rVert+1$.
Observe that $f^{\operatorname{\mathsf{n}}}\succ\mathsf{s}$. Hence to prove
$u\mathrel{\gtrdot}_{k}\mathsf{S}_{\pi}(t\sigma)$ it suffices to observe that
$\operatorname{\mathsf{width}}(u)+k>\lVert{\pi(t\sigma)}\rVert+1$ holds. For
that note that $\lVert{\pi(t\sigma)}\rVert$ is either
$\lVert{\pi(t_{j}\sigma)}\rVert+1$ for some $j\in\pi(g)$ or less than $k$. In
the latter case, we are done. Otherwise
$\lVert{\pi(t\sigma)}\rVert=\lVert{\pi(t_{j}\sigma)}\rVert+1$. Then from the
definition of $\mathrel{\gtrdot}_{k}$ and the induction hypothesis
$u\mathrel{\gtrdot}_{3\cdot\lVert{\pi(t_{j})}\rVert}\mathsf{N}_{\pi}(t_{j}\sigma)$
we can conclude
$\operatorname{\mathsf{width}}(u)+3\cdot\lVert{\pi(t_{j})}\rVert>\operatorname{\mathsf{width}}(\mathsf{N}_{\pi}(t_{j}\sigma))=\lVert{\pi(t_{j}\sigma)}\rVert+1$.
Since $k\geqslant 3\cdot(\lVert{\pi(t_{j})}\rVert+1)$,
$\operatorname{\mathsf{width}}(u)+k>\lVert{\pi(t\sigma)}\rVert+1$ follows. ∎

######  Lemma 5.5.

Suppose $s\mathrel{{>}^{\pi}_{\mathsf{pop*}}}t$ such that
$\pi(s\sigma)=f(\pi(s_{1}\sigma),\dots,\pi(s_{n}\sigma))$ with
$\pi(s_{i}\sigma)\in{\mathsf{Val}}_{\pi}$ for $i\in\\{{1,\dots,n}\\}$. Then
for $\operatorname{\mathsf{nrm}}(f)=\\{{j_{1},\dots,j_{q}}\\}$,

  1. (i)

$f^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(s_{j_{1}}\sigma),\dots,\mathsf{N}_{\pi}(s_{j_{q}}\sigma))\mathrel{\blacktriangleright}_{3\cdot\lVert{\pi(t)}\rVert}\mathsf{S}_{\pi}(t\sigma)$,
and

  2. (ii)

$f^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(s_{j_{1}}\sigma),\dots,\mathsf{N}_{\pi}(s_{j_{q}}\sigma))\mathrel{::}\operatorname{\mathsf{BN_{\pi}}}(s\sigma)\mathrel{\blacktriangleright}_{3\cdot\lVert{\pi(t)}\rVert}\mathsf{N}_{\pi}(t\sigma)$.

###### Proof.

The lemma is shown by induction on the definition of
$\mathrel{{>}^{\pi}_{\mathsf{pop*}}}$. For the following, we set
$u=f^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(s_{j_{1}}\sigma),\dots,\mathsf{N}_{\pi}(s_{j_{q}}\sigma))$.
Suppose $s\mathrel{{>}^{\pi}_{\mathsf{pop*}}}t$ follows due to Definition
4.2(ii). We set $k\mathrel{:=}3\cdot\lVert{\pi(t)}\rVert$. Let
$\operatorname{\mathsf{nrm}}(g)=\\{{j^{\prime}_{1},\dots,j^{\prime}_{q}}\\}$
and let
$\operatorname{\mathsf{safe}}(g)=\\{{i^{\prime}_{1},\dots,i^{\prime}_{p}}\\}$.

Property $(\ref{en:embed:hlp:a})$ is immediate for
$\pi(t\sigma)\in{\mathsf{Val}}_{\pi}$, so assume otherwise. We see that
$s\mathrel{{>}^{\pi}_{\mathsf{pop}}}t_{j}$ for all
$j\in\operatorname{\mathsf{nrm}}(g)$ and obtain
$u\mathrel{\gtrdot}_{k-1}g^{\operatorname{\mathsf{n}}}(\mathsf{N}_{\pi}(t_{j^{\prime}_{1}}\sigma),\dots,\mathsf{N}_{\pi}(t_{j^{\prime}_{q}}\sigma))$
as in Lemma 5.4. Furthermore, $s\mathrel{{>}^{\pi}_{\mathsf{pop*}}}t_{j_{0}}$
for some $j_{0}\in\operatorname{\mathsf{safe}}(g)$ and by induction
hypothesis:
$u\mathrel{\blacktriangleright}_{k-1}\mathsf{S}_{\pi}(t_{j_{0}}\sigma)$. To
conclude property $(\ref{en:embed:hlp:a})$, it remains to verify
$u\mathrel{\gtrdot}_{k-1}\mathsf{S}_{\pi}(t_{j}\sigma)$ for the remaining
$j\in\operatorname{\mathsf{safe}}(g)$. We either have
$s\mathrel{{>}^{\pi}_{\mathsf{pop}}}t_{j}$ or
$\pi(s_{i})\mathrel{\unrhd}\pi(t_{j})$ (for some $i$). In the former subcase
we proceed as in the claim, and for the latter we observe
$\pi(t_{j}\sigma)\in{\mathsf{Val}}_{\pi}$, and thus
$\mathsf{S}_{\pi}(t_{j}\sigma)=[\,]$ follows. This establishes property
$(\ref{en:embed:hlp:a})$.

To conclude property $(\ref{en:embed:hlp:b})$, it suffices to show
$\operatorname{\mathsf{width}}(u\mathrel{::}\operatorname{\mathsf{BN_{\pi}}}(s\sigma))+k>\operatorname{\mathsf{width}}(\mathsf{N}_{\pi}(t\sigma))$,
or equivalently $\lVert{\pi(s\sigma)}\rVert+1+k>\lVert{\pi(t\sigma)}\rVert$.
The latter can be shown, if we proceed similar as in the claim. ∎

Recall the definition of
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{Q}$}}}_{\mathcal{R}}}$
from Section 2 and define
$\mathcal{Q}\mathrel{:=}\\{f({x}_{1},\ldots,{x}_{n})\to\bot\mid
f\in\mathcal{D}\\}$, and set
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{R}}}\mathrel{:=}{\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{Q}$}}}_{\mathcal{R}}}}$.
As the normal forms of $\mathcal{Q}$ coincide with $\mathsf{Val}$,
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{R}}}$
is the restriction of
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}$,
where arguments need to be values instead of normal forms of $\mathcal{R}$.
From Lemma 5.3 and 5.5 we derive an embedding of root steps
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\varepsilon}_{\mathcal{R}}}$.

Suppose the step
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{R}}}t$
takes place below the root. Observe that $\pi(s)\not=\pi(t)$ need not hold in
general. Thus we cannot hope to prove
$\mathsf{N}_{\pi}(s)\mathrel{\blacktriangleright}_{k}\mathsf{N}_{\pi}(t)$.
However, we have the following stronger result.

######  Lemma 5.6.

There exists a uniform $k\in\mathbb{N}$ (depending only on $\mathcal{R}$) such
that if $\mathcal{R}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ holds then
${s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\varepsilon}_{\mathcal{R}}}t}$
implies
${\mathsf{N}_{\pi}(s)\mathrel{\blacktriangleright}_{k}\mathsf{N}_{\pi}(t)}$.
Moreover, if
$\mathcal{R}\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
holds then
${s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{R}}}t}$
implies ${\mathsf{N}_{\pi}(s)\mathrel{\not{\gtrsim}}_{k}\mathsf{N}_{\pi}(t)}$.

###### Proof.

We consider the first half of the assertion. Suppose
$\mathcal{R}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ and
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\varepsilon}_{\mathcal{R}}}t$,
that is for some rule ${f({l}_{1},\ldots,{l}_{n})\to r}\in\mathcal{R}$ and
substitution $\sigma\,\colon\,\mathcal{V}\to\mathsf{Val}$ we have
$s=f(l_{1}\sigma,\dots,l_{n}\sigma)$ and $t=r\sigma$. Depending on whether
$\pi$ collapses $f$, the property either directly follows from Lemma 5.3 or is
a consequence of Lemma $\ref{l:embed:hlp}(\ref{en:embed:hlp:b})$.

In order to conclude the second half of the assertion, one performs induction
on the rewrite context. In addition, one shows that for the special case
$\mathsf{S}_{\pi}(s)\approx\mathsf{S}_{\pi}(t)$, still
$\lVert{\pi(s)}\rVert\geqslant\lVert{\pi(t)}\rVert$ holds. From this the lemma
follows. ∎

For constructor TRSs, we can simulate
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}$
using
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{R}}}$.
We extend $\mathcal{R}$ with suitable rules $\Phi(\mathcal{R})$, which replace
normal forms that are not values by some constructor symbol. To simplfy the
argument we re-use the symbol $\bot$ from above. We define the TRS
$\Phi(\mathcal{R})$ as

$\Phi(\mathcal{R})\mathrel{:=}\\{{f({t}_{1},\ldots,{t}_{n})\to\bot\mid
f({t}_{1},\ldots,{t}_{n})\in{\operatorname{\mathsf{NF}}(\mathcal{R})\cap\mathcal{T}(\mathcal{F})}\text{
and }f\in\mathcal{D}}\\}\hbox to0.0pt{$\;$.\hss}$

Moreover, we define
$\phi_{\mathcal{R}}(t)\mathrel{:=}t{\downarrow}_{\Phi(\mathcal{R})}$. Observe
that $\phi_{\mathcal{R}}(\cdot)$ is well-defined since $\Phi(\mathcal{R})$ is
confluent and terminating.

######  Lemma 5.7.

Let $\mathcal{R}\cup\mathcal{S}$ be a constructor TRS. Define
$\mathcal{S}^{\prime}\mathrel{:=}\mathcal{S}\cup\Phi(\mathcal{R}\cup\mathcal{S})$.
For $s\in\mathcal{T}(\mathcal{F})$,

${s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}}t}\quad\text{implies}\quad{\phi_{\mathcal{R}\cup\mathcal{S}}(s)\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}^{\prime}}}\phi_{\mathcal{R}\cup\mathcal{S}}(t)}\hbox
to0.0pt{$\;$,\hss}$

where
${\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{R}/\mathcal{S}^{\prime}}}}$
abbreviates
${\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{S}^{\prime}}}\cdot\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{R}}}\cdot\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{S}^{\prime}}}}$.

###### Proof.

It is easy to see that
${s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}t}$
implies
$\phi_{\mathcal{R}}(s)\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{R}}}\cdot\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{!}_{\Phi(\mathcal{R})}}\phi_{\mathcal{R}}(t)$.
Suppose
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}}t$,
then there exist ground terms $u$ and $v$ such that
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{S}}}u\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}}}v\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{S}}}t$.
Let $\phi(t)\mathrel{:=}\phi_{\mathcal{R}\cup\mathcal{S}}(t)$. From the above,
$\phi(s)\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{S}^{\prime}}}\phi(u)\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\varepsilon}_{\mathcal{R}}}\cdot\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{S}^{\prime}}}\phi(v)\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{S}^{\prime}}}\phi(t)$
follows as desired. ∎

Suppose $\mathcal{R}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ and
$\mathcal{S}\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
holds. Together with Lemma 5.6, the above simulation establishes the promised
embedding of
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}}$
into $\mathrel{\blacktriangleright}_{k}$.

######  Lemma 5.8.

Let $\mathcal{R}\cup\mathcal{S}$ be a constructor TRS, and suppose
$\mathcal{R}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ and
${\mathcal{S}}\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
hold. Then for $k$ depending only on $\mathcal{R}$ and $\mathcal{S}$ and
$s\in\mathcal{T}(\mathcal{F})$, we have

${s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}}t}\quad\text{implies}\quad{\mathsf{N}_{\pi}(\phi(s))\mathrel{\blacktriangleright}_{k}^{+}\mathsf{N}_{\pi}(\phi(t))}\hbox
to0.0pt{$\;$.\hss}$

###### Proof.

Consider a step
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}}t$
and set $\phi(t)\mathrel{:=}\phi_{\mathcal{R}\cup\mathcal{S}}(t)$. By Lemma
5.7 there exist terms $u$ and $v$ such that
$\phi(s)\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{S}\cup\Phi(\mathcal{R}\cup\mathcal{S})}}u\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\varepsilon}_{\mathcal{R}}}v\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{S}\cup\Phi(\mathcal{R}\cup\mathcal{S})}}\phi(t)$.
Since $\mathcal{R}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ holds, by
Lemma 5.6
$\mathsf{N}_{\pi}(u)\mathrel{\blacktriangleright}_{k_{1}}\mathsf{N}_{\pi}(v)$
follows. Moreover from
$\mathcal{S}\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
together with Lemma 5.6 we conclude that
$r_{1}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{S}\cup\Phi(\mathcal{R}\cup\mathcal{S})}}r_{2}$
implies
$\mathsf{N}_{\pi}(r_{1})\mathrel{\not{\gtrsim}}_{k_{2}}\mathsf{N}_{\pi}(r_{2})$.
Here it suffices to see that steps from
$\mathcal{V}(\mathcal{R}\cup\mathcal{S})$ are easy to embed into
$\mathrel{\not{\gtrsim}}_{k_{2}}$ using the predicative interpretation
$\mathsf{N}_{\pi}$ independent of $k_{2}$. In both cases $k_{1}$ and $k_{2}$
depend only on $\mathcal{R}$ and $\mathcal{S}$ respectively; set
$k\mathrel{:=}\max\\{{k_{1},k_{2}}\\}$. In sum we have
$\mathsf{N}_{\pi}(\phi(s))\mathrel{\not{\gtrsim}}_{k}^{*}\mathsf{N}_{\pi}(u)\mathrel{\blacktriangleright}_{k}\mathsf{N}_{\pi}(v)\mathrel{\not{\gtrsim}}_{k}^{*}\mathsf{N}_{\pi}(\phi(t))$,
employing
${\mathrel{\blacktriangleright}_{l_{1}}}\subseteq{\mathrel{\blacktriangleright}_{l_{2}}}$
for $l_{1}\leqslant l_{2}$. It is an easy exercise to show that
${{\mathrel{\blacktriangleright}_{k}}\cdot{\approx}}\subseteq{\mathrel{\blacktriangleright}_{k}}$
and likewise
${{\approx}\cdot{\mathrel{\blacktriangleright}_{k}}}\subseteq{\mathrel{\blacktriangleright}_{k}}$
holds. Hence the lemma follows. ∎

######  Theorem 5.9.

Let $\mathcal{R}\cup\mathcal{S}$ be a constructor TRS, and suppose
$\mathcal{R}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ and
${\mathcal{S}}\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
holds. Then there exists a polynomial $p$ depending only on
$\mathcal{R}\cup\mathcal{S}$ such that for any basic and ground term $t$,
$\operatorname{dl}(t,\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}})\leqslant
p(\lvert{t}\rvert)$.

###### Proof.

Assume $t\not\in\operatorname{\mathsf{NF}}(\mathcal{R}\cup\mathcal{S})$,
otherwise
$\operatorname{dl}(t,\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}})$
is trivially bounded. Moreover $t$ is a basic term, hence
$\phi_{\mathcal{R}\cup\mathcal{S}}(t)=t$. From Lemma 5.8 we infer that
$\operatorname{dl}(t,\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}/\mathcal{S}}})\leqslant\mathsf{G}_{k}(\mathsf{N}_{\pi}(\phi_{\mathcal{R}\cup\mathcal{S}}(t)))=\mathsf{G}_{k}(\mathsf{N}_{\pi}({t}))$
for some $k$, where the latter is polynomially bounded in $\lvert{t}\rvert$
and the polynomial only depends on $k$, cf. Lemma 5.2. Finally $k$ depends
only on $\mathcal{R}\cup\mathcal{S}$. ∎

Suppose $\mathcal{R}$ is a constructor TRS, and let $\mathcal{P}$ denote the
set of weak innermost dependency pairs. For the moment, suppose that all
compound symbols of $\mathcal{P}$ are nullary. Provided that $\mathcal{P}$ is
non-duplicating and compatible with some SLI, as a consequence of the above
theorem paired with Proposition 3.4, the inclusions
$\mathcal{P}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ and
$\mathcal{U}(\mathcal{P})\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
certify that
$\operatorname{rc}^{\text{\scriptsize$\operatorname{\mathsf{i}}$}}_{\mathcal{R}}$
is polynomially bounded. Observe that for the application of
$\mathrel{{>}^{\pi}_{\mathsf{pop*}}}$ and
$\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}$
in the context of $\mathcal{P}$ and $\mathcal{U}(\mathcal{P})$, we alter
Definitions 4.1 and 4.2 such that $f\in\mathcal{D}^{\sharp}$ is demanded.

######  Example 5.10 (Example 4.5 continued).

Reconsider the TRS $\mathcal{R}_{\textsf{bits}}$, and let $\mathcal{P}$ denote
$\mathsf{WIDP}(\mathcal{R}_{\textsf{bits}})$ as drawn in Example 3.2. By
taking the SLI $\mathcal{A}$ with $0_{\mathcal{A}}=0$,
$\mathsf{s}_{\mathcal{A}}(x)=x+1$ and $\mathsf{half}_{\mathcal{A}}(x)=x+1$ we
obtain $\mathcal{U}(\mathcal{P})\subseteq{\mathrel{>_{\mathcal{A}}}}$ and
moreover, observe that $\mathcal{P}$ is both non-duplicating and contains only
nullary compound symbols. In Example 4.5 we have seen that
$\mathcal{P}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ holds. Similar,
$\mathcal{U}(\mathsf{WIDP}(\mathcal{R}_{\textsf{bits}}))\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
can easily be shown. From the above observation we thus conclude a polynomial
runtime-complexity of $\mathcal{R}_{\textsf{bits}}$.

The assumption that all compound symbols from $\mathcal{P}$ need to be nullary
is straightforward to lift, but technical. Hence, we do not provide a complete
proof here, but only indicate the necessary changes. The formal construction
can be found in the Appendix.

Note that in the general case, it does not suffice to embed root steps of
$\mathcal{P}$ into $\mathrel{\blacktriangleright}_{k}$, rather we have to
embed steps of form
$C[s_{1}^{\sharp},\dots,s_{i}^{\sharp},\dots,s_{n}^{\sharp}]\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{P}}}C[s_{1}^{\sharp},\dots,t_{i}^{\sharp},\dots,s_{n}^{\sharp}]$
with $C$ being a context built from compound symbols. As first measure we
require that the argument filtering $\pi$ is _safe_ Hirokawa and Moser
(2008b), that is $\pi(c)=[1,\dots,n]$ for each compound symbol $\mathsf{c}$ of
arity $n$. Secondly, we adapt the predicative interpretation
$\mathsf{N}_{\pi}$ in such a way that compound symbols are interpreted as
sequences, and their arguments by the interpretation $\mathsf{N}_{\pi}$. This
way, a proper embedding using $\mathsf{N}_{\pi}$ requires
$\mathsf{N}_{\pi}(s_{i}^{\sharp})\mathrel{\blacktriangleright}_{k}\mathsf{N}_{\pi}(t_{i}^{\sharp})$
instead of
$\mathsf{S}_{\pi}(s_{i}^{\sharp})\mathrel{\blacktriangleright}_{k}\mathsf{S}_{\pi}(t_{i}^{\sharp})$.

######  Theorem 5.11.

Let $\mathcal{R}$ be a constructor TRS, and let $\mathcal{P}$ denote the set
of weak innermost dependency pairs. Assume $\mathcal{P}$ is non-duplicating,
and suppose ${\mathcal{U}(\mathcal{P})}\subseteq{>_{\mathcal{A}}}$ for some
SLI $\mathcal{A}$. Let $\pi$ be a safe argument filtering. If
$\mathcal{P}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ and
$\mathcal{U}(\mathcal{P})\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
then
$\operatorname{rc}^{\text{\scriptsize$\operatorname{\mathsf{i}}$}}_{\mathcal{R}}$
is polynomially bounded.

Above it is essential that $\mathcal{R}$ is a constructor TRS. This even holds
when $\textsc{POP}^{\ast}$ is applied directly.

######  Example 5.12.

Consider the TRS $\mathcal{R}_{\operatorname{\mathsf{exp}}}$ below:

$\begin{array}[]{c}\operatorname{\mathsf{exp}}(x)\to\mathsf{e}(\mathsf{g}(x))\qquad\mathsf{e}(\mathsf{g}(\mathsf{s}(x)))\to\operatorname{\mathsf{dp}}_{1}(\mathsf{g}(x))\qquad\mathsf{g}(\mathsf{0})\to\mathsf{0}\rule[-7.74998pt]{0.0pt}{0.0pt}\\\
\operatorname{\mathsf{dp}}_{1}(x)\to\operatorname{\mathsf{dp}}_{2}(\mathsf{e}(x),x)\qquad\qquad\operatorname{\mathsf{dp}}_{2}(x,y)\to\operatorname{\mathsf{pr}}(x,\mathsf{e}(y))\end{array}$

The above rules are oriented (directly) by $\mathrel{{>}_{\mathsf{pop*}}}$
induced by $\operatorname{\mathsf{safe}}$ and $\succsim$ such that: (i) the
argument position of $\mathsf{g}$ and $\operatorname{\mathsf{exp}}$ are
normal, the remaining argument positions are safe, and (ii)
$\operatorname{\mathsf{exp}}\succ\mathsf{g}\succ\operatorname{\mathsf{dp}}_{1}\succ\operatorname{\mathsf{dp}}_{2}\succ\mathsf{e}\succ\operatorname{\mathsf{pr}}\succ\mathsf{0}$.
On the other hand, $\mathcal{R}_{\operatorname{\mathsf{exp}}}$ admits at least
exponential innermost runtime-complexity, as for instance
$\operatorname{\mathsf{exp}}(s^{n}(\mathsf{0}))$ normalizes in exponentially
(in $n$) many innermost rewrite steps.

To overcome this obstacle, we adapt the definition of
$\mathrel{{>}_{\mathsf{pop*}}}$ in the sense that we refine the notion of
defined function symbols as follows. Let $\mathcal{G}_{\mathcal{C}}$ denote
the least set containing $\mathcal{C}$ and all symbols appearing in arguments
to left-hand sides in $\mathcal{R}$. Moreover, set
$\mathcal{G}_{\mathcal{D}}\mathrel{:=}\mathcal{F}\setminus\mathcal{G}_{\mathcal{C}}$
and set
$\mathsf{Val}\mathrel{:=}\mathcal{T}(\mathcal{G}_{\mathcal{C}},\mathcal{V})$.
Then in order to extend Theorem 5.11 to non-constructor TRS it suffices to
replace $\mathcal{D}$ by $\mathcal{G}_{\mathcal{D}}$ and $\mathcal{C}$ by
$\mathcal{G}_{\mathcal{C}}$ in all above given definitions and arguments (see
Avanzini (2009) for the formal construction). Thus the next theorem follows
easily from combining Proposition 3.6 and Theorem 5.11. Note that this theorem
can be easily extended so that in each path different termination techniques
(inducing polynomial runtime complexity) are employed, see Hirokawa and Moser
(2008a) and Section 6.

######  Theorem 5.13.

Let $\mathcal{R}$ be a TRS. Let $\mathcal{G}$ denote the weak innermost
dependency graph, and let
$\mathcal{F}=\mathcal{G}_{\mathcal{D}}\uplus\mathcal{G}_{\mathcal{C}}$ be
separated as above. Suppose for every path
$(\mathcal{P}_{1},\ldots,\mathcal{P}_{n})$ in ${\mathcal{G}}/_{\\!\equiv}$
there exists an SLI $\mathcal{A}$ and a pair
$(\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}},\mathrel{{>}^{\pi}_{\mathsf{pop*}}})$
based on a safe argument filtering $\pi$ such that (i)
$\mathcal{U}(\mathcal{P}_{1}\cup\cdots\cup\mathcal{P}_{n})\subseteq{>_{\mathcal{A}}}$
(ii)
$\mathcal{P}_{1}\cup\cdots\cup\mathcal{P}_{n-1}\cup\mathcal{U}(\mathcal{P}_{1}\cup\cdots\cup\mathcal{P}_{n})\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$,
and (iii) $\mathcal{P}_{n}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$
holds. Then
$\operatorname{rc}^{\text{\scriptsize$\operatorname{\mathsf{i}}$}}_{\mathcal{R}}$
is polynomially bounded.

The next theorem establishes that $\textsc{POP}^{\ast}$ in conjunction with
(weak innermost) dependency pairs induces polytime computability of the
function described through the analysed TRS. We kindly refer the reader to the
Appendix for the proof.

######  Theorem 5.14.

Let $\mathcal{R}$ be an orthogonal, $S$-sorted and completely defined
constructor TRS such that the underlying signature is simple. Let
$\mathcal{P}$ denote the set of weak innermost dependency pairs. Assume
$\mathcal{P}$ is non-duplicating, and suppose
${\mathcal{U}(\mathcal{P})}\subseteq{>_{\mathcal{A}}}$ for some SLI
$\mathcal{A}$. If $\mathcal{P}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$
and
$\mathcal{U}(\mathcal{P})\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
then the functions computed by $\mathcal{R}$ are computable in polynomial
time.

Here _simple_ signature Marion (2003) essentially means that the size of any
constructor term depends polynomially on its depth. Such a restriction is
always necessary in this context. A detailed account is given in the Appendix
(see alo Marion (2003)). This restriction is also responsible for the
introduction of sorts.

##  6 Experimental Results

All described techniques have been incorporated into the _Tyrolean Complexity
Tool_ TCT, an open source complexity analyser222Available at http://cl-
informatik.uibk.ac.at/software/tct.. We performed tests on two testbeds: T
constitutes of the $1394$ examples from the Termination Problem Database
Version 5.0.2 that were used in the runtime-complexity category of the
termination competition 2008333See http://termcomp.uibk.ac.at.. Moreover,
testbed C is the restriction of testbed T to constructor TRSs ($638$ in
total). All experiments were conducted on a machine that is identical to the
official competition server ($8$ AMD Opteron${}^{\text{\textregistered}}$ 885
dual-core processors with 2.8GHz, $8\text{x}8$ GB memory). As timeout we use 5
seconds. We orient TRSs using $\mathrel{{>}^{\pi}_{\mathsf{pop*}}}$ by
encoding the constraints on precedence and so forth in _propositional logic_
(cf. Avanzini (2009) for details), employing $\mathsf{MiniSat}$ Eén and
Sörensson (2003) for finding satisfying assignments. In a similar spirit, we
check compatibility with SLIs via translations to SAT. In order to derive an
estimated dependency graph, we use the function $\mathsf{ICAP}$ (cf. Giesl et
al. (2005)).

Experimental findings are summarised in Table 1.444See http://cl-
informatik.uibk.ac.at/~zini/rta09 for extended results. In each column, we
highlight the total on yes-, maybe- and timeout-instances. Furthermore, we
annotate average times in seconds. In the first three columns we contrast
$\textsc{POP}^{\ast}$ as direct technique to $\textsc{POP}^{\ast}$ as base to
(weak innermost) dependency pairs. I.e., the columns WIDP and WIDG show
results concerning Proposition 3.4 together with Theorem 5.11 or Theorem 5.13
respectively.

In the remaining four columns we assess the power of Proposition 3.4 and 3.6
in conjunction with different base orders, thus verifying that the use of
$\textsc{POP}^{\ast}$ in this context is independent to existing techniques.
Column P asserts that the different paths are handled by _linear and quadratic
restricted interpretations_ Hirokawa and Moser (2008b). In column PP, in
addition $\textsc{POP}^{\ast}$ is employed. Similar, in column M  _restricted
matrix interpretations_ (that is matrix interpretations Endrullis et al.
(2008), where constructors are interpreted by triangular matrices) are used to
handle different paths. Again column MP extends column M with
$\textsc{POP}^{\ast}$. Note that all methods induce polynomial innermost
runtime complexity.

| polynomial path orders | dependency graphs mixed
---|---|---
| DIRECT | WIDP | WIDG | P | PP | M | MP
T | Yes  | 46 | /0.03 | 69 | /0.09 | 80 | /0.07 | 198 | /0.54 | 198 | /0.51 | 200 | /0.63 | 207 | /0.48
| Maybe | 1348 | /0.04 | 1322 | /0.10 | 1302 | /0.14 | 167 | /0.77 | 170 | /0.82 | 142 | /0.61 | 142 | /0.63
| Timeout  | 0 |  | 3 |  | 12 |  | 1029 |  | 1026 |  | 1052 |  | 1045 |
C | Yes  | 40 | /0.03 | 48 | /0.08 | 55 | /0.05 | 99 | /0.40 | 100 | /0.38 | 98 | /0.26 | 105 | /0.23
| Maybe | 598 | /0.05 | 587 | /0.10 | 576 | /0.13 | 143 | /0.72 | 146 | /0.77 | 119 | /0.51 | 119 | /0.54
| Timeout  | 0 |  | 3 |  | 7 |  | 396 |  | 392 |  | 421 |  | 414 |
Table 1: Experimental Results

Table 1 reflects that the integration of $\textsc{POP}^{\ast}$ in the context
of (weak) dependency pairs, significantly extends the direct approach. Worthy
of note, the extension of Avanzini and Moser (2008) with quasi-precedences
alone gives 5 additional examples. As advertised, $\textsc{POP}^{\ast}$ is
incredibly fast in all settings. Consequently, as evident from the table,
polynomial path orders team well with existing techniques, without affecting
overall performance: notice that due to the additional of
$\textsc{POP}^{\ast}$ the number of timeouts is reduced.

##  7 Conclusion

In this paper we study the runtime complexity of rewrite systems. We combine
two recently developed techniques in the context of complexity analysis: weak
innermost dependency pairs and polynomial path orders. If the conditions of
our main result are met, we can conclude the innermost polynomial runtime
complexity of the studied term rewrite system. And we obtain that the function
defined are _polytime computable_. We have implemented the technique and
experimental evidence clearly indicates the power and in particular the
efficiency of the new method.

##  Appendix A Appendix

Below we present the missing proofs of Theorem 5.11 and Theorem 5.14
respectively.

As mentioned in Section 5, we now introduce an _extended predicative
interpretation_ whose purpose is to interpret compound symbols as sequences,
and their arguments via the interpretation $\mathsf{N}_{\pi}$.

######  Definition A.1.

The _extended predicative interpretation_ $\mathsf{N}_{\pi}^{\mathsf{s}}$ from
terms $\mathcal{T}(\mathcal{F},\mathcal{V})$ to sequences
$\operatorname{\mathcal{S}eq}(\mathcal{F}^{\operatorname{\mathsf{n}}}_{\pi}\cup\\{{\mathsf{s}}\\},\mathcal{V})$
is defined as follows: if $t=\mathsf{c}({t}_{1},\ldots,{t}_{n})$ and
$\mathsf{c}\in{\mathcal{C}}_{\text{\tiny{$com$}}}$ then
$\mathsf{N}_{\pi}^{\mathsf{s}}(t)\mathrel{:=}[\mathsf{N}_{\pi}^{\mathsf{s}}(t_{1})\leavevmode\nobreak\
\cdots\leavevmode\nobreak\ \mathsf{N}_{\pi}^{\mathsf{s}}(t_{n})]$, and
otherwise $\mathsf{N}_{\pi}^{\mathsf{s}}(t)\mathrel{:=}[\mathsf{N}_{\pi}(t)]$.

Following (Terese, 2003, Section 6.5), we briefly recall _typed rewriting_.
Let $S$ be a finite set representing the set of _types_ or _sorts_. An _$S$
-sorted set $A$_ is a family of sets $\\{{A_{s}\mid s\in S}\\}$ such that all
sets $A_{s}$ are pairwise disjoint. In the following, we suppose that
$\mathcal{V}$ denotes an $S$-sorted set of variables. An _$S$ -sorted
signature $\mathcal{F}$_ is like a signature, but the _arity_ of
$f\in\mathcal{F}$ is defined by
$\operatorname{\mathsf{ar}}(f)=(s_{1},\dots,s_{n})$ for $s_{1},\dots,s_{n}\in
S$. Additionally, each symbol $f\in\mathcal{F}$ is associated with a sort
$s\in S$, called the _type of $f$_ and denoted by
$\operatorname{\mathsf{st}}(f)$. We adopt the usual notion and write
$f\,\colon\,(s_{1},\dots,s_{n})\to s$ when
$\operatorname{\mathsf{ar}}(f)=(s_{1},\dots,s_{n})$ and
$\operatorname{\mathsf{st}}(f)=s$. The _$S$ -sorted set of terms
$\mathcal{T}(\mathcal{F},\mathcal{V})_{S}$_ consists of the sets
$\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$ for $s\in S$, where
$\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$ is inductively defined by (i)
$\mathcal{V}_{s}\subseteq\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$, and (ii)
$f({t}_{1},\ldots,{t}_{n})\in\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$ for all
function symbols $f\in\mathcal{F}$, $f\,\colon\,(s_{1},\dots,s_{n})\to s$ and
terms $t_{i}\in\mathcal{T}(\mathcal{F},\mathcal{V})_{s_{i}}$ for
$i\in\\{{1,\dots,n}\\}$. We say that a term $t$ is _well-typed_ if
$t\in\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$ for some sort $s$. An
$S$-sorted term rewrite system $\mathcal{R}$ is a TRS such that for ${l\to
r}\in\mathcal{R}$, it holds that
$l,r\in\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$ for some sort $s\in S$. As a
consequence, for $s\in\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$ and
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$$}}}_{\mathcal{R}}}t$,
we have that $t\in\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$.

######  Example A.2.

Let $S=\\{{\mathsf{Bool},\mathsf{List},\mathsf{Nat},\mathsf{Pair}}\\}$. The
$S$-sorted rewrite system $\mathcal{R}_{\mathsf{Lst}}$ is given by the
following rules:

$\displaystyle\mathsf{f}(\mathsf{s}(x))$
$\displaystyle\to\mathsf{cons}(\mathsf{pair}(x,\mathsf{g}(x)),\mathsf{f}(x))$
$\displaystyle\hskip 12.91663pt\mathsf{g}(\mathsf{s}(x))$
$\displaystyle\to\mathsf{g}(x)$ $\displaystyle\mathsf{f}(0)$
$\displaystyle\to\mathsf{nil}$ $\displaystyle\mathsf{g}(0)$
$\displaystyle\to\mathsf{tt}$

Here we assign arities and sorts as follows: for the constructors we set
$0\,\colon\,\mathsf{Nat}$, $\mathsf{s}\,\colon\,\mathsf{Nat}\to\mathsf{Nat}$,
$\mathsf{pair}\,\colon\,(\mathsf{Nat},\mathsf{Bool})\to\mathsf{Pair}$,
$\mathsf{tt}\,\colon\,\mathsf{Bool}$, $\mathsf{nil}\,\colon\,\mathsf{List}$,
$\mathsf{cons}\,\colon\,(\mathsf{Pair},\mathsf{List})\to\mathsf{List}$; for
the defined symbols we set $\mathsf{f}\,\colon\,\mathsf{Nat}\to\mathsf{List}$
and $\mathsf{g}\,\colon\,\mathsf{Nat}\to\mathsf{Bool}$.

A _simple_ signature Marion (2003) is a sorted signature such that each sort
has a finite _rank_ $r$ in the following sense: the sort $s$ has rank $r$ if
for every constructor $c\,\colon\,({s}_{1},\ldots,{s}_{n})\to s$, the rank of
each sort $s_{i}$ is less than the rank of $s$, except for at most one sort
which can be of rank $r$. Simple signatures allow the definition of enumerated
datatypes and inductive datatypes like words and lists but prohibit for
instance the definition of tree structures. Observe that the signature
underlying $\mathcal{R}_{\mathsf{Lst}}$ from Example A.2 is simple. A crucial
insight is that sizes of values formed from a simple signature can be
estimated polynomially in their depth. The easy proof of the following
proposition can be found in (Marion, 2003, Proposition 17).

######  Proposition A.3.

Let $\mathcal{C}$ be a set of constructors from a simple signature
$\mathcal{F}$. There exists a constant $d\in\mathbb{N}$ such that for each
term $t\in\mathcal{T}(\mathcal{C},\mathcal{V})_{S}$ whose rank is $r$,
$\lvert{t}\rvert\leqslant d^{r}\cdot\operatorname{\mathsf{dp}}(t)^{r+1}$.

In order to give a polytime algorithm for the functions computed by a TRS, it
is essential that sizes of reducts do not exceed a polynomial bound with
respect to the size of the start term. Recall that approximations
$\mathrel{\blacktriangleright}_{k}$ tightly control the size growth of terms.
For simple signatures, we can exploit this property for a space-complexity
analysis. Although predicative interpretations remove values, by the above
proposition sizes of those can be estimated based on the Buchholz-norm record
in $\mathsf{N}_{\pi}$. And so we derive the following Lemma, essential for the
proof of Theorem 5.14.

######  Lemma A.4.

Let $\mathcal{F}$ be a simple signature. There exists a (monotone) polynomial
$p$ depending only on $\mathcal{F}$ such that for each well-typed term
$t\in\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$, $\lvert{t}\rvert\leqslant
p(\mathsf{G}_{k}(\mathsf{N}^{\mathsf{s}}(t)))$.

###### Proof.

The Lemma follows as: (i) for all sequences
$s\in\operatorname{\mathcal{S}eq}$,
$\lvert{s}\rvert\leqslant\mathsf{G}_{k}(s)+1$, and (ii) for all terms
$t\in\mathcal{T}(\mathcal{F},\mathcal{V})_{s}$, $\lvert{t}\rvert\leqslant
c\cdot\lvert{\mathsf{N}^{\mathsf{s}}(t)}\rvert^{d}$ for some uniform constants
$0<c,d\in\mathbb{N}$. These properties are simple to verify: property (i)
follows from induction on $s$ where we employ for the inductive step that
$f({s}_{1},\ldots,{s}_{n})\mathrel{\blacktriangleright}_{k}[{s}_{1}\cdots{s}_{n}]$
and
$\mathsf{G}_{k}([{s}_{1}\cdots{s}_{n}])=\sum_{i=1}^{n}\mathsf{G}_{k}(s_{i})+n$.
For property (ii), set $d=r+2$ where $r$ is the maximal rank of a symbol in
$\mathcal{C}$, and set $c=e^{r}$ where $e$ is as given from Proposition A.3.
First one shows by a straight forward induction on $t$ that
$\lvert{t}\rvert\leqslant
c\cdot(\lvert{\mathsf{S}(t)}\rvert\cdot\lVert{t}\rVert^{r+1})$ (employing
Proposition A.3 and $\operatorname{\mathsf{dp}}(t)\leqslant\lVert{t}\rVert$).
As $\lvert{\mathsf{S}(t)}\rvert<\lvert{\mathsf{N}(t)}\rvert$ and
$\lVert{t}\rVert<\lvert{\mathsf{N}(t)}\rvert$, we derive
$\lvert{t}\rvert<c\cdot\lvert{\mathsf{N}(t)}\rvert^{d}$. By induction on the
definition of $\mathsf{N}^{\mathsf{s}}$ we finally obtain property (ii). ∎

Let $\mathcal{R}$ be a (not necessarily $S$-sorted) TRS that is innermost
terminating. In the sequel, we keep $\mathcal{R}$ fixed. In order to exploit
Lemma A.4 for an analysis by means of weak innermost dependency pairs, we
introduce the notion of _type preserving weak innermost dependency pairs_.

######  Definition A.5.

If $l\to r\in\mathcal{R}$ and
$r=C\langle{u}_{1},\ldots,{u}_{n}\rangle_{\mathcal{D}}$ then
$l^{\sharp}\to\mathsf{c}(u_{1}^{\sharp},\ldots,u_{n}^{\sharp})$ is called a
_type preserving weak innermost dependency pair_ of $\mathcal{R}$. Here, the
_compound symbol_ $\mathsf{c}$ is supposed to be fresh. We set
$\mathsf{repr}(\mathsf{c})\mathrel{:=}C$ and say that $\mathsf{c}$
_represents_ the context $C$. The set of all type preserving weak innermost
dependency pairs is denoted by $\mathsf{WIDP}(\mathcal{R})$.

We collect all compound symbols appearing in $\mathsf{TPWIDP}(\mathcal{R})$ in
the set ${\mathcal{C}}_{\text{\tiny{$com$}}}$.

######  Example A.6 (Example A.2 continued).

Reconsider the rewrite system $\mathcal{R}_{\mathsf{Lst}}$ given in Example
A.2. The set $\mathsf{TPWIDP}(\mathcal{R}_{\mathsf{Lst}})$ is given by

$\displaystyle\mathsf{f}^{\sharp}(\mathsf{s}(x))$
$\displaystyle\to\mathsf{c}_{1}(\mathsf{g}^{\sharp}(x),\mathsf{f}^{\sharp}(x))$
$\displaystyle\hskip 12.91663pt\mathsf{g}^{\sharp}(\mathsf{s}(x))$
$\displaystyle\to\mathsf{c}_{3}(\mathsf{g}^{\sharp}(x))$
$\displaystyle\mathsf{f}^{\sharp}(0)$ $\displaystyle\to\mathsf{c}_{2}$
$\displaystyle\mathsf{g}^{\sharp}(0)$ $\displaystyle\to\mathsf{c}_{4}$

The constant $\mathsf{c}_{3}$ represents for instance the empty context, and
the constant $\mathsf{c}_{1}$ represents the context
$\mathsf{repr}(\mathsf{c}_{1})=\mathsf{cons}(\mathsf{pair}(x,\Box),\Box)$.

######  Lemma A.7.

Let $\mathcal{R}$ be an $S$-sorted TRS such that the underlying signature
$\mathcal{F}$ is simple. Then
$\mathsf{TPWIDP}(\mathcal{R})\cup\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))$ is
an $S$-sorted TRS, and the underlying signature
$\mathcal{F}^{\sharp}\cup{\mathcal{C}}_{\text{\tiny{$com$}}}$ a simple
signature.

###### Proof.

To conclude the claim, it suffices to type the marked and compound symbols
appropriately. For each rule
${f^{\sharp}({l}_{1},\ldots,{l}_{n})\to\mathsf{c}(r_{1}^{\sharp},\dots,r_{n}^{\sharp})}\in\mathsf{TPWIDP}(\mathcal{R})$
we proceed as follows: we set
$\operatorname{\mathsf{ar}}(f^{\sharp})\mathrel{:=}\operatorname{\mathsf{ar}}(f)$
and
$\operatorname{\mathsf{st}}(f^{\sharp})\mathrel{:=}\operatorname{\mathsf{st}}(f)$.
Moreover, we set
$\operatorname{\mathsf{ar}}(\mathsf{c})\mathrel{:=}({\operatorname{\mathsf{st}}}({r}_{1}),\ldots,{\operatorname{\mathsf{st}}}({r}_{m}))$
and
$\operatorname{\mathsf{st}}(\mathsf{c})\mathrel{:=}\operatorname{\mathsf{st}}(f)$.
It is easy to see that since $\mathcal{R}$ is $S$-sorted,
$\mathsf{TPWIDP}(\mathcal{R})\cup\mathcal{U}(\mathsf{TPWIDP}(\mathcal{R}))$ is
$S$-sorted too. ∎

Note that the above lemma fails for weak innermost dependency pairs: consider
the rule $\mathsf{f}(x)\to\mathsf{d}(\mathsf{g}(x))$, where $\mathsf{f}$ and
$\mathsf{g}$ are defined symbols and $\mathsf{d}$ is a constructor. Moreover,
suppose $\mathsf{f}\,\colon\,\mathsf{s_{2}}\to\mathsf{s_{1}}$,
$\mathsf{g}\,\colon\,\mathsf{s_{2}}\to\mathsf{s_{3}}$ and
$\mathsf{d}\,\colon\,\mathsf{s_{3}}\to\mathsf{s_{1}}$. Then we cannot type the
corresponding weak innermost dependency pair
$\mathsf{f}^{\sharp}(x)\to\mathsf{g}^{\sharp}(x)$ as above because
(return-)types of $\mathsf{f}^{\sharp}$ and $\mathsf{g}^{\sharp}$ differ.

As for practical all termination techniques, compatibility of weak innermost
dependency pairs with polynomial path orders also yield compatibility of type
preserving weak innermost dependency pairs. Moreover, from the definition we
immediately see that
$\operatorname{dl}(t^{\sharp},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathsf{TPWIDP}(\mathcal{R})/\mathcal{U}}})=\operatorname{dl}(t^{\sharp},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathsf{WIDP}(\mathcal{R})/\mathcal{U}}})$
with $\mathcal{U}=\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))$ and basic term $t$.
And so it is clear that in order to proof Theorem 5.11 and Theorem 5.14,
$\mathsf{WIDP}(\mathcal{R})$ can safely be replaced by
$\mathsf{TPWIDP}(\mathcal{R})$. We continue with the proof of Theorem 5.11.

###  A.1 Proof of Theorem 5.11

Let $\mathsf{ComCtx}$ abbreviate the set of contexts
$\mathcal{T}({\mathcal{C}}_{\text{\tiny{$com$}}}\cup\\{{\Box}\\},\mathcal{V})$
build from compound symbols. Set $\mathcal{P}=\mathsf{TPWIDP}(\mathcal{R})$
and $\mathcal{U}=\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))$. In order to
highlight the correspondence between
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}$
and
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{P}/\mathcal{U}}}$,
we extend the notion of _representatives_.

######  Definition A.8.

Let $C\in\mathsf{ComCtx}$. We define $\mathsf{reprs}(C)$ as the least set of
(ground) contexts such that (i) if $C=\Box$ then $\Box\in\mathsf{reprs}(C)$,
and (ii) if $C=\mathsf{c}({C}_{1},\ldots,{C}_{n})$,
$C^{\prime}_{i}\in\mathsf{reprs}(C_{i})$ and $\sigma$ is a substitution from
all variables in $\mathsf{repr}(\mathsf{c})$ to ground normal forms of
$\mathcal{R}$ then
$(\mathsf{repr}(\mathsf{c})\sigma)[C^{\prime}_{1},\dots,C^{\prime}_{n}]\in\mathsf{reprs}(C)$.

######  Example A.9 (Example A.6 continued).

Reconsider the TRS $\mathcal{R}_{\mathsf{Lst}}$ from Example A.2, together
with $\mathsf{TPWIDP}(\mathcal{R}_{\mathsf{Lst}})$ as given in Example A.6.
Consider the step
$\mathsf{f}(\mathsf{s}(0))\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$$}}}_{\mathcal{R}_{\mathsf{Lst}}}}\mathsf{cons}(\mathsf{pair}(0,\mathsf{g}(0)),\mathsf{f}(0))$
and the corresponding dependency pair step

$\mathsf{f}^{\sharp}(\mathsf{s}(0))\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$$}}}_{\mathsf{TPWIDP}(\mathcal{R}_{\mathsf{Lst}})}}\mathsf{c}_{1}(\mathsf{g}^{\sharp}(0),\mathsf{f}^{\sharp}(0))\hbox
to0.0pt{$\;$.\hss}$

Let $C=\mathsf{c}_{1}(\Box,\Box)$, remember that
$\mathsf{repr}(\mathsf{c}_{1})=\mathsf{cons}(\mathsf{pair}(x,\Box),\Box)$,
$\mathsf{reprs}(\Box)=\Box$ and observe that
$C^{\prime}=\mathsf{cons}(\mathsf{pair}(0,\Box),\Box)\in\mathsf{reprs}(C)$ by
taking the substitution $\sigma=\\{{x\mapsto 0}\\}$. And hence we can
reformulate the above two steps as
$\mathsf{f}(\mathsf{s}(0))\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$$}}}_{\mathcal{R}_{\mathsf{Lst}}}}C^{\prime}[\mathsf{g}(0),\mathsf{f}(0)]$
and likewise
$\mathsf{f}^{\sharp}(\mathsf{s}(0))\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$$}}}_{\mathsf{TPWIDP}(\mathcal{R}_{\mathsf{Lst}})}}C[\mathsf{g}^{\sharp}(0),\mathsf{f}^{\sharp}(0)]$.

We manifest the above observation in the following lemma.

######  Lemma A.10.

Let $s\in\mathcal{T}_{\mathsf{b}}$ be a ground and basic term. Suppose
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{R}}}t$.
Let $\mathcal{P}=\mathsf{TPWIDP}(\mathcal{R})$ and let
$\mathcal{U}=\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))$. Then there exists
contexts $C^{\prime}\in\mathsf{ComCtx}$, $C\in\mathsf{reprs}(C^{\prime})$ and
terms ${t}_{1},\ldots,{t}_{n}$ such that $t=C[{t}_{1},\ldots,{t}_{n}]$ and
moreover,
$s^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{P}\cup\mathcal{U}}}C^{\prime}[t_{1}^{\sharp},\dots,t_{n}^{\sharp}]$.

###### Proof.

We proof the lemma by induction on the length of the rewrite sequence
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{n}_{\mathcal{R}}}t$.
The base case $n=0$ is trivial, we set $C=C^{\prime}=\Box$. So suppose
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{n}_{\mathcal{R}}}t\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}u$
and the property holds for $n$. And thus we can find contexts
$C^{\prime}_{t}\in\mathsf{ComCtx}$, $C_{t}\in\mathsf{reprs}(C^{\prime}_{t})$
and terms ${t}_{1},\ldots,{t}_{n}$ such that $t=C_{t}[{t}_{1},\ldots,{t}_{n}]$
and moreover,
$s^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{P}\cup\mathcal{U}}}C^{\prime}_{t}[t_{1}^{\sharp},\dots,t_{n}^{\sharp}]$.
Without loss of generality we can assume
$u=C_{t}[t_{1},\dots,u_{i},\dots,t_{n}]$ with
$t_{i}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}u_{i}$,
as the context $C_{t}$ is solely build from constructors and normal forms of
$\mathcal{R}$.

First, suppose
$t_{i}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\varepsilon}_{\mathcal{R}}}u_{i}$,
and hence $t_{i}={l\sigma}$ for ${l\to r}\in\mathcal{R}$ and substitution
$\sigma\,\colon\,\mathcal{V}\to\operatorname{\mathsf{NF}}(\mathcal{R})\cap\mathcal{T}(\mathcal{F})$.
Moreover
${l^{\sharp}\to\mathsf{c}(r_{1}^{\sharp},\dots,r_{m}^{\sharp})}\in\mathcal{P}$
such that
$u_{i}=(\mathsf{repr}(\mathsf{c})\sigma)[r_{1}\sigma,\dots,r_{m}\sigma]$. We
set $C^{\prime}$ as the context obtained from replacing the $i$-th hole of
$C^{\prime}_{t}$ by $\mathsf{c}(\Box,\dots,\Box)$, likewise we set $C$ as the
context obtained from replacing the $i$-th hole of $C_{t}$ by
$\mathsf{repr}(\mathsf{c})\sigma$. Note that $C\in\mathsf{reprs}(C^{\prime})$.
We conclude
$s^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{P}\cup\mathcal{U}}}C^{\prime}[t_{1}^{\sharp},\dots,{r_{1}^{\sharp}\sigma,\dots,r_{m}^{\sharp}\sigma},\dots,t_{n}^{\sharp}]$
and $u=C[t_{1},\dots,r_{1}\sigma,\dots,r_{m}\sigma,\dots,t_{n}]$ which
establishes the lemma for this case.

Now suppose
$t_{i}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}u_{i}$
is a step below the root. Thus we have also
$t_{i}^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}u_{i}^{\sharp}$.
As shown in (Hirokawa and Moser, 2008b, Lemma 16), the latter can be
strengthened to
$t_{i}^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\mathcal{P}\cup\mathcal{U}$}}}_{\mathcal{U}}}u_{i}^{\sharp}$.
We conclude
$s^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{P}\cup\mathcal{U}}}C^{\prime}_{t}[t_{1}^{\sharp},\dots,u_{i}^{\sharp},\dots,t_{n}^{\sharp}]$,
and the lemma follows by setting $C^{\prime}=C^{\prime}_{t}$ and $C=C_{t}$. ∎

Suppose $\mathsf{WIDP}(\mathcal{R})$ contains non-nullary compound symbols. In
order to establish an embedding in the sense of Lemma 5.6 for that case, by
the above lemma we see that it suffices to consider only terms of shape
$s=C[{s_{1}^{\sharp},\dots,s_{n}^{\sharp}}]$ with $C\in\mathsf{ComCtx}$. With
this insight, we adjust Lemma 5.6 as below. Observe that due to the definition
of $\mathsf{N}_{\pi}^{\mathsf{s}}$, we cannot simply apply Lemma 5.6 together
with closure under context of $\mathrel{\blacktriangleright}_{k}$ here.

######  Lemma A.11.

Let $s=C[s_{1}^{\sharp},\dots,s_{n}^{\sharp}]$ for $C\in\mathsf{ComCtx}$ and
${s}_{1},\ldots,{s}_{n}\in\mathcal{T}(\mathcal{F},\mathcal{V})$. Let
$\mathcal{P}=\mathsf{TPWIDP}(\mathcal{R})$ and
$\mathcal{U}=\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))$. There exists a uniform
constant $k\in\mathbb{N}$ depending only on $\mathcal{R}$ such that if
$\mathcal{P}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ holds then
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{P}}}t$
implies
$\mathsf{N}_{\pi}^{\mathsf{s}}(s)\mathrel{\blacktriangleright}_{k}\mathsf{N}_{\pi}^{\mathsf{s}}(t)$.
Moreover, if
${\mathcal{U}}\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
holds then
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{U}}}t$
implies
$\mathsf{N}_{\pi}^{\mathsf{s}}(s)\mathrel{\not{\gtrsim}}_{k}\mathsf{N}_{\pi}^{\mathsf{s}}(t)$.

###### Proof.

We proof the lemma for $k\mathrel{:=}\max\\{{3\cdot\lVert{r}\rVert\mid{l\to
r}\in\mathcal{P}\cup\mathcal{U}}\\}$. Suppose
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{P}}}t$
or
$s\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{U}}}t$
respectively, and thus $t=C[s_{1}^{\sharp},\dots,t_{i},\dots,s_{n}^{\sharp}]$
for some term $t_{i}$. There exists a context $C^{\prime}$ (over sequences)
such that
$\mathsf{N}_{\pi}^{\mathsf{s}}(s)=C^{\prime}[\mathsf{N}_{\pi}^{\mathsf{s}}(s_{i}^{\sharp})]$
and
$\mathsf{N}_{\pi}^{\mathsf{s}}(t)=C^{\prime}[\mathsf{N}_{\pi}^{\mathsf{s}}(t_{i}^{\sharp})]$.
First assume
$s_{i}^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{P}}}t_{i}$,
and thus
$\mathsf{N}_{\pi}^{\mathsf{s}}(s_{i}^{\sharp})=[\mathsf{N}_{\pi}(l^{\sharp}\sigma)]$
and
$\mathsf{N}_{\pi}^{\mathsf{s}}(t_{i})=[[\mathsf{N}_{\pi}(r_{1}^{\sharp}\sigma)],\dots,[\mathsf{N}_{\pi}(r_{m}^{\sharp}\sigma)]]$
for ${l\to\mathsf{c}(r_{1}^{\sharp},\dots,r_{m}^{\sharp})}\in\mathcal{P}$. To
verify
$\mathsf{N}_{\pi}^{\mathsf{s}}(s)\mathrel{\blacktriangleright}_{k}\mathsf{N}_{\pi}^{\mathsf{s}}(t)$,
by Definition 2.2(ii) and Definition 2.2(iv), it suffices to verify
$\mathsf{N}_{\pi}(l^{\sharp}\sigma)\mathrel{\blacktriangleright}_{k-1}\mathsf{N}_{\pi}(r_{j}^{\sharp}\sigma)$
for all $j\in\\{{1,\dots,m}\\}$. The latter is an easy consequence of Lemma
5.6, where we employ that (i)
$l^{\sharp}\mathrel{{>}^{\pi}_{\mathsf{pop*}}}r_{j}^{\sharp}$ follows from the
assumption $\mathcal{P}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$, and
(ii) $\lVert{\pi(r)}\rVert>\lVert{\pi(r_{j})}\rVert$. Both properties are
straight forward to verify since $\pi$ is safe. For
$s_{i}^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{U}}}t$
we have
$\mathsf{N}_{\pi}^{\mathsf{s}}(s_{i}^{\sharp})=[\mathsf{N}_{\pi}(s_{i}^{\sharp})]$
and
$\mathsf{N}_{\pi}^{\mathsf{s}}(t_{i}^{\sharp})=[\mathsf{N}_{\pi}(t_{i}^{\sharp})]$
for ${l\to r}\in\mathcal{U}$. From Lemma 5.6 we obtain
$\mathsf{N}_{\pi}(s_{i}^{\sharp})\mathrel{\not{\gtrsim}}_{k}\mathsf{N}_{\pi}(t_{i}^{\sharp})$
which establishes the lemma. ∎

The proof of Theorem 5.11 is now easily obtained by incorporating the above
lemma into Theorem 5.9.

######  Theorem.

Let $\mathcal{R}$ be a constructor TRS, and let $\mathcal{P}$ denote the set
of weak innermost dependency pairs. Assume $\mathcal{P}$ is non-duplicating,
and suppose ${\mathcal{U}(\mathcal{P})}\subseteq{>_{\mathcal{A}}}$ for some
SLI $\mathcal{A}$. Let $\pi$ be a safe argument filtering. If
$\mathcal{P}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ and
$\mathcal{U}(\mathcal{P})\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
then
$\operatorname{rc}^{\text{\scriptsize$\operatorname{\mathsf{i}}$}}_{\mathcal{R}}$
is polynomially bounded.

###### Proof.

According to Proposition 3.4 we need to find a polynomial $p$ such that

$\operatorname{dl}(t^{\sharp},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathsf{WIDP}(\mathcal{R})/\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))}})\leqslant
p(\lvert{t^{\sharp}}\rvert)\hbox to0.0pt{$\;$.\hss}$

We set $\mathcal{P}=\mathsf{TPWIDP}(\mathcal{R})$ and likewise
$\mathcal{U}=\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))$. Clearly, it suffices to
show
$\operatorname{dl}(t^{\sharp},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathsf{TPWIDP}(\mathcal{R})/\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))}})\leqslant
p(\lvert{t^{\sharp}}\rvert)$ for that. Consider a sequence

$t^{\sharp}=t_{0}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{P}/\mathcal{U}}}t_{1}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{P}/\mathcal{U}}}\dots\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{P}/\mathcal{U}}}t_{\ell}\hbox
to0.0pt{$\;$,\hss}$

and pick a relative step
$t_{i}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{P}/\mathcal{U}}}t_{i+1}$.
Define
$\mathcal{U}^{\prime}=\mathcal{U}\cup\mathcal{V}(\mathcal{P}\cup\mathcal{U})$
and $\phi(t)=\phi_{\mathcal{P}\cup\mathcal{U}}(t)$. Clearly Lemma 5.7 can be
extended to account for steps of $\mathcal{P}$ below the root, and thus
$\phi(t_{i})\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{P}/\mathcal{U}^{\prime}}}\phi(t_{i+1})$
follows. Hence for some terms $u$ and $v$,
$\phi(t_{i})\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{U}^{\prime}}}u\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}_{\mathcal{P}}}v\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{U}^{\prime}}}\phi(t_{i+1})$.
As shown in Lemma A.10, all involved terms in the above sequence have the
shape $C[s_{1}^{\sharp},\dots,s_{n}^{\sharp}]$, $C\in\mathsf{ComCtx}$. As
$\mathsf{WIDP}(\mathcal{R})\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$,
and since $\pi$ is safe, it is easy to infer that
$\mathcal{P}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$ holds (we just set
every compound symbol from $\mathcal{P}$ minimal in the precedence). And hence
Lemma A.11 translates the above relative step to
$\mathsf{N}_{\pi}^{\mathsf{s}}(\phi(s))\mathrel{\blacktriangleright}^{+}_{k}\mathsf{N}_{\pi}^{\mathsf{s}}(\phi(t))$
for some uniform constant $k$. As a consequence,
$\operatorname{dl}(t,\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathsf{WIDP}(\mathcal{R})/\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))}})\leqslant\mathsf{G}_{k}(\mathsf{N}_{\pi}^{\mathsf{s}}(\phi(t)))$
for all terms $t$. Fix some reducible and basic term
$t\in\mathcal{T}_{\mathsf{b}}$. Observe
$\mathsf{N}_{\pi}^{\mathsf{s}}(\phi(t^{\sharp}))=[\mathsf{N}_{\pi}(t^{\sharp})]$
and so from Lemma 5.1 we see that
$\mathsf{G}_{k}(\mathsf{N}_{\pi}^{\mathsf{s}}(\phi(t^{\sharp})))$ is bounded
polynomially in the size of $t$. The polynomial depends only on $k$. We
conclude the theorem. ∎

###  A.2 Proof of Theorem 5.14

We now proceed with the proof Theorem 5.14, which is essentially an extension
to Theorem 5.11.

We first precisely state what it means that a TRS _computes_ some function.
For this, let
$\ulcorner{\cdot}\urcorner\,\colon\,\Sigma^{\ast}\to\mathcal{T}(\mathcal{C})$
denote an _encoding function_ that represents words over the alphabet $\Sigma$
as ground values. We call an encoding $\ulcorner{\cdot}\urcorner$ _reasonable_
if it is bijective and there exists a constant $c$ such that
$\lvert{u}\rvert\leqslant\lvert{\ulcorner{u}\urcorner}\rvert\leqslant
c\cdot\lvert{u}\rvert$ for every $u\in\Sigma^{*}$. Let
$\ulcorner{\cdot}\urcorner$ denote a reasonable encoding function, and let
$\mathcal{R}$ be a completely defined, orthogonal and terminating TRS. We say
that an $n$-ary function $f\colon(\Sigma^{\ast})^{n}\to\Sigma^{*}$ is
_computable_ by $\mathcal{R}$ if there exists a defined function symbol
$\mathsf{f}$ such that for all $w_{1},\dots,w_{n},v\in\Sigma^{\ast}$
$\mathsf{f}(\ulcorner{w_{1}}\urcorner,\dots,\ulcorner{w_{n}}\urcorner)\to^{!}\ulcorner{v}\urcorner\Longleftrightarrow
f(w_{1},\dots,w_{n})=v$. On the other hand the TRS $\mathcal{R}$ _computes_
$f$, if the function $f\colon(\Sigma^{\ast})^{n}\to\Sigma^{*}$ is defined by
the above equation.

Below we abbreviate $\mathsf{Q}_{\pi}$ as $\mathsf{Q}$ for predicative
interpretation
$\mathsf{Q}\in\\{{\mathsf{S},\mathsf{N},\mathsf{N}^{\mathsf{s}}}\\}$ and the
particular argument filtering $\pi$ that induces the identity function on
terms. Consider the following lemma.

######  Lemma A.12.

Let $\mathcal{R}$ be an $S$-sorted and completely defined constructor TRS such
that the underlying signature is simple. If
${\mathsf{TPWIDP}(\mathcal{R})\cup\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))}\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
then there exists a polynomial $p$ such that for all ground and well-typed
basic terms $t\in\mathcal{T}_{\mathsf{b}}$,
$t^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathsf{TPWIDP}(\mathcal{R})\cup\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))}}s$
implies $\lvert{s}\rvert\leqslant p(\lvert{t}\rvert)$.

###### Proof.

Let
$\mathcal{S}=\mathsf{TPWIDP}(\mathcal{R})\cup\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))$.
Suppose
$t^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{S}}}s$,
or equivalently
$t^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{v}}$}}}^{\ast}_{\mathcal{S}}}s$
since $\mathcal{R}$ is completely defined. By Lemma A.11 we derive
$\mathsf{N}^{\mathsf{s}}(t^{\sharp})\mathrel{\not{\gtrsim}}_{k}^{*}\mathsf{N}^{\mathsf{s}}(s)$
for some uniform $k\in\mathbb{N}$. And thus
$\mathsf{G}_{k}(\mathsf{N}^{\mathsf{s}}(s))\leqslant\mathsf{G}_{k}(\mathsf{N}^{\mathsf{s}}(t^{\sharp}))$.
As
$\mathsf{G}_{k}(\mathsf{N}^{\mathsf{s}}(t^{\sharp}))=\mathsf{G}_{k}([\mathsf{N}(t^{\sharp})])$
is bounded polynomially in the size of $t$ according to Lemma 5.2, we see that
there exists a polynomial $p$ such that
$\mathsf{G}_{k}(\mathsf{N}^{\mathsf{s}}(s))\leqslant\mathsf{G}_{k}(\mathsf{N}^{\mathsf{s}}(t^{\sharp}))\leqslant
p(\lvert{t}\rvert)$. Since $\mathcal{R}$ is and $S$-sorted TRS over a simple
signature, the same holds for $\mathcal{S}$ due to Lemma A.7. And thus since
$t^{\sharp}$ is well-typed and
$t^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{S}}}s$
holds, also $s$ is well-typed. Let $q$ be the polynomial as given from Lemma
A.4 with $\lvert{s}\rvert\leqslant
q(\mathsf{G}_{k}(\mathsf{N}^{\mathsf{s}}(s)))$. Summing up, we derive
$\lvert{s}\rvert\leqslant
q(\mathsf{G}_{k}(\mathsf{N}^{\mathsf{s}}(s)))\leqslant q(p(\lvert{t}\rvert))$
as desired. ∎

The above lemma has established that sizes of reducts with respect to the
relation
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathsf{TPWIDP}(\mathcal{R})\cup\mathcal{U}(\mathsf{WIDP}(\mathcal{R}))}}$
are bounded polynomially in the size of the start term, provided we can orient
dependency pairs and usable rules. It remains to verify that this is indeed
sufficient to appropriately estimate sizes of reducts with respect to
$\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}$.
The fact is established in the final Theorem.

######  Theorem.

Let $\mathcal{R}$ be an orthogonal $S$-sorted and completely defined
constructor TRS such that the underlying signature is simple. Let
$\mathcal{P}$ denote the set of weak innermost dependency pairs. Assume
$\mathcal{P}$ is non-duplicating, and suppose
${\mathcal{U}(\mathcal{P})}\subseteq{>_{\mathcal{A}}}$ for some SLI
$\mathcal{A}$. If $\mathcal{P}\subseteq{\mathrel{{>}^{\pi}_{\mathsf{pop*}}}}$
and
$\mathcal{U}(\mathcal{P})\subseteq{\mathrel{\text{\raisebox{0.0pt}{${\not{>}}^{\pi}_{\text{\raisebox{2.0pt}{$\mathsf{pop*}$}}}$}}}}$
then the functions computed by $\mathcal{R}$ are computable in polynomial-
time.

###### Proof.

We single out one of the defined symbols $\mathsf{f}\in\mathcal{D}$ and
consider the corresponding function
$f\colon(\Sigma^{\ast})^{n}\to\Sigma^{\ast}$ computed by $\mathcal{R}$. Under
the assumptions, $\mathcal{R}$ is terminating, but moreover
$\operatorname{rc}^{\text{\scriptsize$\operatorname{\mathsf{i}}$}}_{\mathcal{R}}$
is polynomially bounded according to Theorem 5.11. Additionally, from
orthogonality (and hence confluence) of $\mathcal{R}$, normal forms are unique
and so the function $f$ is well-defined. Suppose
$\mathsf{f}(\ulcorner{w_{1}}\urcorner,\dots,\ulcorner{w_{n}}\urcorner)\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$$}}}^{!}_{\mathcal{R}}}\ulcorner{v}\urcorner$
for words $w_{1},\dots,w_{n},v$. In particular, from confluence we see that

$\mathsf{f}(\ulcorner{w_{1}}\urcorner,\dots,\ulcorner{w_{n}}\urcorner)\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}t_{1}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}\cdots\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}t_{\ell}=\ulcorner{v}\urcorner\hbox
to0.0pt{$\;$.\hss}$

It is folklore that there exists a polytime algorithm performing one rewrite
step. Hence to conclude the existence of a polytime algorithm for $f$ it
suffices to bound the size of terms $t_{i}$ for $1\leqslant i\leqslant\ell$
polynomially in $\sum_{i}\lvert{w_{i}}\rvert$. And as we suppose that the
encoding $\ulcorner{\cdot}\urcorner$ is reasonable, it thus suffice to bound
the sizes of $t_{i}$ for $i\in\\{{1,\dots,\ell}\\}$ polynomially in the size
of
$t_{0}=\mathsf{f}(\ulcorner{w_{1}}\urcorner,\dots,\ulcorner{w_{n}}\urcorner)$.

Consider a term $t_{i}$. Without loss of generality, we can assume $t_{i}$ is
ground. According to Lemma A.10 there exists contexts
$C^{\prime}_{i}\in\mathsf{ComCtx}$, $C_{i}\in\mathsf{reprs}(C^{\prime}_{i})$
and terms ${u}_{1},\ldots,{u}_{n}$ such that
$t_{i}=C_{i}[{u}_{1},\ldots,{u}_{n}]$ and moreover,
$t_{0}^{\sharp}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{P}\cup\mathcal{U}}}C^{\prime}_{i}[u_{1}^{\sharp},\dots,u_{n}^{\sharp}]$
for all $i\in\\{{1,\dots,\ell}\\}$. From the assumption
$\mathsf{WIDP}(\mathcal{R})\subseteq{\mathrel{{>}_{\mathsf{pop*}}}}$ we see
$\mathsf{TPWIDP}(\mathcal{R})\subseteq{\mathrel{{>}_{\mathsf{pop*}}}}$. Thus
by Lemma A.12 there exists a polynomial $p$ such that
$\lvert{C^{\prime}_{i}[u_{1}^{\sharp},\dots,u_{n}^{\sharp}]}\rvert\leqslant
p(\lvert{t_{0}}\rvert)$. And so, clearly
$\sum_{j=0}^{n}\lvert{u_{j}}\rvert\leqslant p(\lvert{t_{0}}\rvert)$. It
remains to bound the sizes of contexts $C_{i}$ polynomially in
$\lvert{t_{0}}\rvert$.

Recall Definition A.8, and recall that
$C_{i}\in\mathsf{reprs}(C^{\prime}_{i})$. Thus $C_{i}$ is a context build from
constructors and variables, where the latter are replaced by normal forms of
$\mathcal{R}$. Since $\mathcal{R}$ is completely defined,
$\operatorname{\mathsf{NF}}(\mathcal{R})$ coincides with values. We conclude
that $C_{i}\in\mathcal{T}(\mathcal{C}\cup\\{{\Box_{s}\mid s\in S}\\})$. Here
$\Box_{s}$ denotes the hole of sort $s$. Moreover since $\mathcal{R}$ is
$S$-sorted, and
$t_{0}\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}^{\ast}_{\mathcal{R}}}C_{i}[{u}_{1},\ldots,{u}_{n}]$,
we see that $C_{i}$ is well-typed. We define
$\triangle_{\mathcal{R}}=\max\\{{\operatorname{\mathsf{dp}}(r)\mid{l\to
r}\in\mathcal{R}}\\}$. By a straight forward induction it follows that
$\operatorname{\mathsf{dp}}(t_{i})\leqslant\operatorname{\mathsf{dp}}(t_{0})+\triangle_{\mathcal{R}}\cdot
i\leqslant\lvert{t_{0}}\rvert+\triangle_{\mathcal{R}}\cdot\operatorname{dl}(t_{0},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}})$.
As a consequence,
$\operatorname{\mathsf{dp}}({C_{i}})\leqslant\lvert{t_{0}}\rvert+\triangle_{\mathcal{R}}\cdot\operatorname{dl}(t_{0},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}})$,
and thus by Proposition A.3 there exists constants $c,d\in\mathbb{N}$ such
that $\lvert{C_{i}}\rvert\leqslant
c\cdot\operatorname{\mathsf{dp}}(C_{i})^{d}\leqslant
c\cdot(\lvert{t_{0}}\rvert+\triangle_{\mathcal{R}}\cdot\operatorname{dl}(t_{0},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}}))^{d}$.
As we have that
$\operatorname{dl}(t_{0},\mathrel{\xrightarrow{\raisebox{-2.0pt}[0.0pt][0.0pt]{\text{\scriptsize$\operatorname{\mathsf{i}}$}}}_{\mathcal{R}}})$
is polynomially bounded in the size of $t_{0}$, it follows that
$\lvert{C_{i}}\rvert\leqslant q(\lvert{t_{0}}\rvert)$ for some polynomial $q$.

Summing up, we conclude that for all $i\in\\{{1,\dots,\ell}\\}$,
$\lvert{t_{i}}\rvert\leqslant p(\lvert{t_{0}}\rvert)+q(\lvert{t_{0}}\rvert)$
for the polynomials $p$ and $q$ from above. This concludes the theorem. ∎

## References

  * Arai and Moser (2005) Toshiyasu Arai and Georg Moser.  Proofs of termination of rewrite systems for polytime functions.  In _Proc. 25th FSTTCS_ , volume 3821 of _LNCS_ , pages 529–540, 2005.
  * Arts and Giesl (2000) Thomas Arts and Jürgen Giesl.  Termination of term rewriting using dependency pairs.  _TCS_ , 236(1–2):133–178, 2000.
  * Avanzini (2009) Martin Avanzini.  Automation of polynomial path orders.  Master’s thesis, University of Innsbruck, Faculty for Computer Science., 2009.  Available at http://cl-informatik.uibk.ac.at/~zini/MT.pdf.
  * Avanzini and Moser (2008) Martin Avanzini and Georg Moser.  Complexity analysis by rewriting.  In _Proc. 9th FLOPS_ , volume 4989 of _LNCS_ , pages 130–146, 2008.
  * Avanzini et al. (2008) Martin Avanzini, Georg Moser, and Andreas Schnabl.  Automated implicit computational complexity analysis (system description).  In _Proc. 4th IJCAR_ , volume 5195 of _LNCS_ , pages 132–138, 2008.
  * Baader and Nipkow (1998) Franz Baader and Tobias Nipkow.  _Term Rewriting and All That_.  Cambridge University Press, 1998.
  * Bellantoni and Cook (1992) Stephen Bellantoni and Stephen Cook.  A new recursion-theoretic characterization of the polytime functions.  _CC_ , 2(2):97–110, 1992.
  * Bonfante et al. (2009) G. Bonfante, J.-Y. Marion, and J.-Y. Moyen.  Quasi-interpretations: A way to control resources.  _TCS_ , 2009.  To appear.
  * Eén and Sörensson (2003) Niklas Eén and Niklas Sörensson.  An extensible SAT-solver.  In _Proc. 6th SAT_ , volume 2919 of _LNCS_ , pages 502–518, 2003\.
  * Endrullis et al. (2008) Jörg Endrullis, Johannes Waldmann, and Hans Zantema.  Matrix interpretations for proving termination of term rewriting.  _JAR_ , 40(2–3):195–220, 2008.
  * Fuhs et al. (2007) Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl.  SAT solving for termination analysis with polynomial interpretations.  In _Proc. 10th SAT_ , volume 4501 of _LNCS_ , pages 340–354, 2007\.
  * Geser (1990) Alfons Geser.  _Relative Termination_.  PhD thesis, University of Passau, Faculty for Mathematics and Computer Science, 1990.
  * Giesl et al. (2005) Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp.  Proving and disproving termination of higher-order functions.  In _Proc. 5th FroCoS_ , volume 4501 of _LNCS_ , pages 340–354, 2005.
  * Hirokawa and Moser (2008a) Nao Hirokawa and Georg Moser.  Complexity, graphs, and the dependency pair method.  In _Proc. 15th LPAR_ , volume 5330 of _LNCS_ , pages 667–681, 2008a.
  * Hirokawa and Moser (2008b) Nao Hirokawa and Georg Moser.  Automated complexity analysis based on the dependency pair method.  In _Proc. 4th IJCAR_ , volume 5195 of _LNCS_ , pages 364–380, 2008b.
  * Hofbauer and Lautemann (1989) D. Hofbauer and C. Lautemann.  Termination proofs and the length of derivations.  In _Proc. 3rd RTA_ , volume 355 of _LNCS_ , pages 167–177, 1989\.
  * Marion and Péchoux (2008) J.-Y. Marion and R. Péchoux.  Characterizations of polynomial complexity classes with a better intensionality.  In _Proc. 10th PPDP_ , pages 79–88. ACM, 2008.
  * Marion (2003) Jean-Yves Marion.  Analysing the implicit complexity of programs.  _IC_ , 183:2–18, 2003.
  * Simmons (1988) Harold Simmons.  The realm of primitive recursion.  _ARCH_ , 27:177–188, 1988.
  * Terese (2003) Terese.  _Term Rewriting Systems_ , volume 55 of _Cambridge Tracts in Theoretical Computer Science_.  Cambridge University Press, 2003.
  * Thiemann (2007) René Thiemann.  _The DP Framework for Proving Termination of Term Rewriting_.  PhD thesis, University of Aachen, Department of Computer Science, 2007\.