11institutetext: LIP (UMR CNRS/ENS Lyon/UCB Lyon1/INRIA), Lyon, France
22institutetext: Birkbeck, University of London, United Kingdom
33institutetext: LCIS (UGA/Grenoble INP/Ésisar), Valence, France

# Analysing Parallel Complexity of Term Rewriting††thanks:  This work was
partially funded by the French National Agency of Research in the CODAS
Project (ANR-17-CE23-0004-01).

Thaïs Baudon 11 Carsten Fuhs 22 Laure Gonnord 3311

###### Abstract

We revisit parallel-innermost term rewriting as a model of parallel
computation on inductive data structures and provide a corresponding notion of
runtime complexity parametric in the size of the start term. We propose
automatic techniques to derive both upper and lower bounds on parallel
complexity of rewriting that enable a direct reuse of existing techniques for
sequential complexity. The applicability and the precision of the method are
demonstrated by the relatively light effort in extending the program analysis
tool AProVE and by experiments on numerous benchmarks from the literature.

##  1 Introduction

Automated inference of complexity bounds for parallel computation has seen a
surge of attention in recent years [12, 13, 32, 5, 31, 18]. While techniques
and tools for a variety of computational models have been introduced, so far
there does not seem to be any paper in this area for complexity of _term
rewriting_ with parallel evaluation strategies. This paper addresses this gap
in the

⬇

fn size(&self) -> int {

match self {

&Tree::Node { v, ref left, ref right }

=> left.size() + right.size() + 1,

&Tree::Empty => 0 , } }

Figure 1: Tree size computation in Rust

literature. We consider term rewrite systems (TRSs) as _intermediate
representation_ for programs with _pattern-matching_ operating on _algebraic
data types_ like the one depicted in Figure 1.

In this particular example, the recursive calls to left.size() and
right.size() can be done in parallel. Building on previous work on parallel-
innermost rewriting [41, 20], and first ideas about parallel complexity [6],
we propose a new notion of Parallel Dependency Tuples that captures such a
behaviour, and methods to compute both upper and lower _parallel complexity
bounds_.

Bounds on parallel complexity can provide insights about the potentiality of
parallelisation: if sequential and parallel complexity of a function
(asymptotically) coincide, this information can be useful for a parallelising
compiler to refrain from parallelising the evaluation of this function.
Moreover, evaluation of TRSs (as a simple functional programming language) in
massively parallel settings such as GPUs is currently a topic of active
research [19]. In this context, a static analysis of parallel complexity can
be helpful to determine whether to rewrite on a (fast, but not very parallel)
CPU or on a (slower, but massively parallel) GPU.

A preliminary version of this work with an initial notion of parallel
complexity was presented in an informal extended abstract [14]. We now propose
a more formal version accompanied by extensions, proofs, implementation,
experiments, and related work. Sect. 2 recalls term rewriting and Dependency
Tuples [38] as the basis of our approach. In Sect. 3, we introduce a notion of
runtime complexity for parallel-innermost rewriting, and we harness the
existing Dependency Tuple framework to compute asymptotic upper bounds on this
complexity. In Sect. 4, we provide a transformation to innermost term
rewriting that lets any tool for (sequential) innermost runtime complexity be
reused to find upper bounds for parallel-innermost runtime complexity and, for
confluent parallel-innermost rewriting, also lower bounds. Sect. 5 gives
experimental evidence of the practicality of our method on a large standard
benchmark set. We discuss related work in Sect. 6. This technical report
provides full proofs in the appendix. It is an extended authors’ accepted
manuscript for our LOPSTR 2022 paper [15].

##  2 Term Rewriting and Innermost Runtime Complexity

We assume basic familiarity with term rewriting (see, e.g., [11]) and recall
standard definitions to fix notation. As customary for analysis of runtime
complexity of rewriting, we consider terms as _tree-shaped_ objects, without
sharing of subtrees.

We first define _Term Rewrite Systems_ and _Innermost Rewriting_.
$\mathcal{T}(\Sigma,\mathcal{V})$ denotes the set of _terms_ over a finite
signature $\Sigma$ and the set of variables $\mathcal{V}$. For a term $t$, its
_size_ $\lvert t\rvert$ is defined by: (a) if $t\in\mathcal{V}$, $\lvert
t\rvert=1$; (b) if $t=f(t_{1},\ldots,t_{n})$, then $\lvert
t\rvert=1+\sum_{i=1}^{n}\lvert t_{i}\rvert$. The set
$\mathcal{P}\\!\mathit{os}(t)$ of the _positions_ of $t$ is defined by: (a) if
$t\in\mathcal{V}$, then $\mathcal{P}\\!\mathit{os}(t)=\\{\varepsilon\\}$, and
(b) if $t=f(t_{1},\ldots,t_{n})$, then
$\mathcal{P}\\!\mathit{os}(t)=\\{\varepsilon\\}\cup\bigcup_{1\leq i\leq
n}\\{i\pi\mid\pi\in\mathcal{P}\\!\mathit{os}(t_{i})\\}$. The position
$\varepsilon$ is the _root position_ of term $t$. If
$t=f(t_{1},\ldots,t_{n})$, $\mathrm{root}(t)=f$ is the _root symbol_ of $t$.
The _(strict) prefix order_ $>$ on positions is the strict partial order given
by: $\tau>\pi$ iff there exists $\pi^{\prime}\neq\varepsilon$ such that
$\pi\pi^{\prime}=\tau$. Two positions $\pi$ and $\tau$ are _parallel_ iff
neither $\pi>\tau$ nor $\pi=\tau$ nor $\tau>\pi$ hold. For
$\pi\in\mathcal{P}\\!\mathit{os}(t)$, $t|_{\pi}$ is the subterm of $t$ at
position $\pi$, and we write $t[s]_{\pi}$ for the term that results from $t$
by replacing the subterm $t|_{\pi}$ at position $\pi$ by the term $s$.

A substitution $\sigma$ is a mapping from $\mathcal{V}$ to
$\mathcal{T}(\Sigma,\mathcal{V})$ with finite domain
$\mathit{Dom}(\sigma)=\\{x\in\mathcal{V}\mid\sigma(x)\neq x\\}$. We write
$\\{x_{1}\mapsto t_{1};\ldots;x_{n}\mapsto t_{n}\\}$ for a substitution
$\sigma$ with $\sigma(x_{i})=t_{i}$ for $1\leq i\leq n$ and $\sigma(x)=x$ for
all other $x\in\mathcal{V}$. We extend substitutions to terms by
$\sigma(f(t_{1},\ldots,f_{n}))=f(\sigma(t_{1}),\ldots,\sigma(t_{n}))$. We may
write $t\sigma$ for $\sigma(t)$.

For a term $t$, $\mathcal{V}(t)$ is the set of variables in $t$. A _term
rewrite system (TRS)_ $\mathcal{R}$ is a set of rules $\\{\ell_{1}\to
r_{1},\ldots,\ell_{n}\to r_{n}\\}$ with
$\ell_{i},r_{i}\in\mathcal{T}(\Sigma,\mathcal{V})$,
$\ell_{i}\not\in\mathcal{V}$, and
$\mathcal{V}(r_{i})\subseteq\mathcal{V}(\ell_{i})$ for all $1\leq i\leq n$.
The _rewrite relation_ of $\mathcal{R}$ is $s\to_{\mathcal{R}}t$ iff there are
a rule $\ell\to r\in\mathcal{R}$, a position
$\pi\in\mathcal{P}\\!\mathit{os}(s)$, and a substitution $\sigma$ such that
$s=s[\ell\sigma]_{\pi}$ and $t=s[r\sigma]_{\pi}$. Here, $\sigma$ is called the
_matcher_ and the term $\ell\sigma$ the _redex_ of the rewrite step. If no
proper subterm of $\ell\sigma$ is a possible redex, $\ell\sigma$ is an
_innermost redex_ , and the rewrite step is an _innermost rewrite step_ ,
denoted by
$s\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}t$.

$\Sigma_{d}^{\mathcal{R}}=\\{f\mid f(\ell_{1},\ldots,\ell_{n})\to
r\in\mathcal{R}\\}$ and
$\Sigma_{c}^{\mathcal{R}}=\Sigma\setminus\Sigma_{d}^{\mathcal{R}}$ are the
_defined_ and _constructor_ symbols of $\mathcal{R}$. We may also just write
$\Sigma_{d}$ and $\Sigma_{c}$. The set of positions with defined symbols of
$t$ is
$\mathcal{P}\\!\mathit{os}_{d}(t)=\\{\pi\mid\pi\in\mathcal{P}\\!\mathit{os}(t),\mathrm{root}(t|_{\pi})\in\Sigma_{d}\\}$.

For a relation $\to$, $\to^{+}$ is its transitive closure and $\to^{*}$ its
reflexive-transitive closure. An object $o$ is a _normal form_ wrt a relation
$\to$ iff there is no $o^{\prime}$ with $o\to o^{\prime}$. A relation $\to$ is
_confluent_ iff $s\to^{*}t$ and $s\to^{*}u$ implies that there exists an
object $v$ with $t\to^{*}v$ and $u\to^{*}v$. A relation $\to$ is _terminating_
iff there is no infinite sequence $t_{0}\to t_{1}\to t_{2}\to\cdots$.

######  Example 1 ($\mathsf{size}$)

Consider the TRS $\mathcal{R}$ with the following rules modelling the code of
Figure 1.

$\begin{array}[]{rcl@{\hspace*{5ex}}|@{\hspace*{5ex}}rcl}\mathsf{plus}(\mathsf{Zero},y)&\to&y\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{size}(\mathsf{Nil})&\to&\mathsf{Zero}\\\
\mathsf{plus}(\mathsf{S}(x),y)&\to&\mathsf{S}(\mathsf{plus}(x,y))\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{size}(\mathsf{Tree}(v,l,r))&\to&\mathsf{S}(\mathsf{plus}(\mathsf{size}(l),\mathsf{size}(r)))\end{array}$

Here $\Sigma_{d}^{\mathcal{R}}=\\{\mathsf{plus},\mathsf{size}\\}$ and
$\Sigma_{c}^{\mathcal{R}}=\\{\mathsf{Zero},\mathsf{S},\mathsf{Nil},\mathsf{Tree}\\}$.
We have the following innermost rewrite sequence, where the used innermost
redexes are underlined:

$\begin{array}[]{rl}&\underline{\mathsf{size}(\mathsf{Tree}(\mathsf{Zero},\mathsf{Nil},\mathsf{Tree}(\mathsf{Zero},\mathsf{Nil},\mathsf{Nil})))}\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{plus}(\underline{\mathsf{size}(\mathsf{Nil})},\mathsf{size}(\mathsf{Tree}(\mathsf{Zero},\mathsf{Nil},\mathsf{Nil}))))\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{plus}(\mathsf{Zero},\underline{\mathsf{size}(\mathsf{Tree}(\mathsf{Zero},\mathsf{Nil},\mathsf{Nil}))}))\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{plus}(\mathsf{Zero},\mathsf{S}(\mathsf{plus}(\underline{\mathsf{size}(\mathsf{Nil})},\mathsf{size}(\mathsf{Nil})))))\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{plus}(\mathsf{Zero},\mathsf{S}(\mathsf{plus}(\mathsf{Zero},\underline{\mathsf{size}(\mathsf{Nil})}))))\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{plus}(\mathsf{Zero},\mathsf{S}(\underline{\mathsf{plus}(\mathsf{Zero},\mathsf{Zero})})))\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}&\mathsf{S}(\underline{\mathsf{plus}(\mathsf{Zero},\mathsf{S}(\mathsf{Zero}))})\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{S}(\mathsf{Zero}))\end{array}$

This rewrite sequence uses 7 steps to reach a normal form.

We wish to provide static bounds on the length of the longest rewrite sequence
from terms of a specific size. Here we use innermost evaluation strategies,
which closely correspond to call-by-value strategies used in many programming
languages. We focus on rewrite sequences that start with _basic terms_ ,
corresponding to function calls where a function is applied to data objects.
The resulting notion of complexity for term rewriting is known as _innermost
runtime complexity_.

######  Definition 1 (Innermost Runtime Complexity $\mathrm{irc}$ [27, 38])

The _derivation height_ of a term $t$ wrt a relation $\to$ is the length of
the longest sequence of $\to$-steps from $t$:
$\operatorname{dh}(t,\to)=\sup\\{e\mid\exists\,t^{\prime}\in\mathcal{T}(\Sigma,\mathcal{V}).\;t\to^{e}t^{\prime}\\}$
where $\to^{e}$ is the $e^{\textrm{th}}$ iterate of $\to$. If $t$ starts an
infinite $\to$-sequence, we write $\operatorname{dh}(t,\to)=\omega$. Here,
$\omega$ is the smallest infinite ordinal, i.e., $\omega>n$ holds for all
$n\in\mathbb{N}$.

A term $f(t_{1},\ldots,t_{k})$ is _basic (for a TRS $\mathcal{R}$)_ iff
$f\in\Sigma_{d}^{\mathcal{R}}$ and
$t_{1},\dots,t_{k}\in\mathcal{T}(\Sigma_{c}^{\mathcal{R}},\mathcal{V})$.
$\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}}$ is the set of basic terms for a
TRS $\mathcal{R}$. For $n\in\mathbb{N}$, the _innermost runtime complexity_
function is
$\mathrm{irc}_{\mathcal{R}}(n)=\sup\\{\operatorname{dh}(t,{\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}})\mid
t\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}},\lvert t\rvert\leq n\\}$. For
all $P\subseteq\mathbb{N}\cup\\{\omega\\}$, $\sup\,P$ is the least upper bound
of $P$, where $\sup\,\emptyset=0$.

Many automated techniques are available [27, 38, 28, 8, 37, 36] to analyse
$\mathrm{irc}_{\mathcal{R}}$. We build on Dependency Tuples [38], originally
designed to find upper bounds for(sequential) innermost runtime complexity. A
central idea is to group all function calls by a rewrite rule _together_
rather than to separate them (as with DPs for proving termination [7]). We use
_sharp terms_ to represent these function calls.

######  Definition 2 (Sharp Terms $\mathcal{T}^{\sharp}$)

For every $f\in\Sigma_{d}$, we introduce a fresh symbol $f^{\sharp}$ of the
same arity, called a _sharp symbol_. For a term $t=f(t_{1},\ldots,t_{n})$ with
$f\in\Sigma_{d}$, we define $t^{\sharp}=f^{\sharp}(t_{1},\ldots,t_{n})$. For
all other terms $t$, we define $t^{\sharp}=t$.
$\mathcal{T}^{\sharp}=\\{t^{\sharp}\mid
t\in\mathcal{T}(\Sigma,\mathcal{V}),\mathrm{root}(t)\in\Sigma_{d}\\}$ denotes
the set of _sharp terms_.

To get an upper bound for sequential complexity, we “count” how often each
rewrite rule is used. The idea is that when a rule $\ell\to r$ is used, the
cost (i.e., number of rewrite steps for the evaluation) of the function call
to the instance of $\ell$ is 1 + the sum of the costs of all the function
calls in the resulting instance of $r$, counted separately in some fixed
order. To group $k$ function calls together, we use “compound symbols”
$\mathsf{Com}_{k}$ of arity $k$, which intuitively represent the sum of the
runtimes of their arguments.

######  Definition 3 (Dependency Tuple, DT [38])

A _dependency tuple (DT)_ is a rule of the form
$s^{\sharp}\to\mathsf{Com}_{n}(t^{\sharp}_{1},\ldots,t^{\sharp}_{n})$ where
$s^{\sharp},t^{\sharp}_{1},\ldots,t^{\sharp}_{n}\in\mathcal{T}^{\sharp}$. Let
$\ell\to r$ be a rule with
$\mathcal{P}\\!\mathit{os}_{d}(r)=\\{\pi_{1},\ldots,\pi_{n}\\}$ and
$\pi_{1}\gtrdot\ldots\gtrdot\pi_{n}$ for a total order $\gtrdot$ (e.g.,
lexicographic order) on positions. Then $\mathit{DT}(\ell\to
r)=\ell^{\sharp}\to\mathsf{Com}_{n}(r|^{\sharp}_{\pi_{1}},\ldots,r|^{\sharp}_{\pi_{n}})$.111The
order $\gtrdot$ must be total to ensure that the function $\mathit{DT}$ is
well defined wrt the order of the arguments of $\mathsf{Com}_{n}$. The
(partial!) prefix order $>$ is not sufficient here.  For a TRS $\mathcal{R}$,
let $\mathit{DT}(\mathcal{R})=\\{\mathit{DT}(\ell\to r)\mid\ell\to
r\in\mathcal{R}\\}$.

###### Example 2

For $\mathcal{R}$ from Ex. 1, $\mathit{DT}(\mathcal{R})$ consists of the
following DTs:

$\begin{array}[]{rcl}\mathsf{plus}^{\sharp}(\mathsf{Zero},y)&\to&\mathsf{Com}_{0}\\\
\mathsf{plus}^{\sharp}(\mathsf{S}(x),y)&\to&\mathsf{Com}_{1}(\mathsf{plus}^{\sharp}(x,y))\\\
\mathsf{size}^{\sharp}(\mathsf{Nil})&\to&\mathsf{Com}_{0}\\\
\mathsf{size}^{\sharp}(\mathsf{Tree}(v,l,r))&\to&\mathsf{Com}_{3}(\mathsf{size}^{\sharp}(l),\mathsf{size}^{\sharp}(r),\mathsf{plus}^{\sharp}(\mathsf{size}(l),\mathsf{size}(r)))\end{array}$

To represent the complexity of a sharp term for a set of DTs and a TRS
$\mathcal{R}$, _chain trees_ are used [38]. Intuitively, a chain tree for some
sharp term is a dependency tree of the computations involved in evaluating
this term. Each node represents a computation (the DT) on some arguments
(defined by the substitution).

######  Definition 4 (Chain Tree, $\mathit{Cplx}$ [38])

Let $\mathcal{D}$ be a set of DTs and $\mathcal{R}$ be a TRS. Let $T$ be a
(possibly infinite) tree where each node is labelled with a DT
$q^{\sharp}\to\mathsf{Com}_{n}(w^{\sharp}_{1},\ldots,w^{\sharp}_{n})$ from
$\mathcal{D}$ and a substitution $\nu$, written
$(q^{\sharp}\to\mathsf{Com}_{n}(w^{\sharp}_{1},\ldots,w^{\sharp}_{n})\mid\nu)$.
Let the root node be labelled with
$(s^{\sharp}\to\mathsf{Com}_{e}(r^{\sharp}_{1},\ldots,r^{\sharp}_{e})\mid\sigma)$.
Then $T$ is a _$(\mathcal{D},\mathcal{R})$ -chain tree for $s^{\sharp}\sigma$_
iff the following conditions hold for any node of $T$, where
$(u^{\sharp}\to\mathsf{Com}_{m}(v^{\sharp}_{1},\ldots,v^{\sharp}_{m})\mid\mu)$
is the label of the node:

  * •

$u^{\sharp}\mu$ is in normal form wrt $\mathcal{R}$;

  * •

if this node has the children
$(p^{\sharp}_{1}\to\mathsf{Com}_{m_{1}}(\ldots)\mid\delta_{1}),\ldots,(p^{\sharp}_{k}\to\mathsf{Com}_{m_{k}}(\ldots)\mid\delta_{k})$,
then there are pairwise different $i_{1},\ldots,i_{k}\in\\{1,\ldots,m\\}$ with
$v^{\sharp}_{i_{j}}\mu\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}^{*}}p^{\sharp}_{j}\delta_{j}$
for all $j\in\\{1,\ldots,k\\}$.

Let $\mathcal{S}\subseteq\mathcal{D}$ and $s^{\sharp}\in\mathcal{T}^{\sharp}$.
For a chain tree $T$, $|T|_{\mathcal{S}}\in\mathbb{N}\cup\\{\omega\\}$ is the
number of nodes in $T$ labelled with a DT from $\mathcal{S}$. We define
$\mathit{Cplx}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(s^{\sharp})=\sup\\{|T|_{\mathcal{S}}\mid
T\text{ is a }(\mathcal{D},\mathcal{R})\text{-chain tree for }s^{\sharp}\\}$.
For terms $s^{\sharp}$ without a $(\mathcal{D},\mathcal{R})$-chain tree, we
define
$\mathit{Cplx}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(s^{\sharp})=0$.

###### Example 3

For $\mathcal{R}$ from Ex. 1 and $\mathcal{D}=\mathit{DT}(\mathcal{R})$ from
Ex. 2, the following is a chain tree for the term
$\mathsf{size}^{\sharp}(\mathsf{Tree}(\mathsf{Zero},\mathsf{Nil},\mathsf{Nil}))$:

$(\mathsf{size}^{\sharp}(\mathsf{Tree}(v,l,r))\to\mathsf{Com}_{3}(\mathsf{size}^{\sharp}(l),\mathsf{size}^{\sharp}(r),\mathsf{plus}^{\sharp}(\mathsf{size}(l),\mathsf{size}(r)))$$|~{}\\{v\mapsto\mathsf{Zero};l\mapsto\mathsf{Nil};r\mapsto\mathsf{Nil}\\})$$(\mathsf{size}^{\sharp}(\mathsf{Nil})\to\mathsf{Com}_{0}\mid\\{\\})$$(\mathsf{size}^{\sharp}(\mathsf{Nil})\to\mathsf{Com}_{0}\mid\\{\\})$$(\mathsf{plus}^{\sharp}(\mathsf{Zero},y)\to\mathsf{Com}_{0}\mid\\{y\mapsto\mathsf{Zero}\\})$pt$\mathsf{size}(\mathsf{Nil})\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}^{*}}\mathsf{Zero}$

The main correctness statement in the sequential case is the following:

######  Theorem 2.1 ($\mathit{Cplx}$ bounds Derivation Height for
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$
[38])

Let $\mathcal{R}$ be a TRS, let
$t=f(t_{1},\ldots,t_{n})\in\mathcal{T}(\Sigma,\mathcal{V})$ such that all
$t_{i}$ are in normal form (this includes all
$t\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}}$). Then we have
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}})\leq\mathit{Cplx}_{\langle\mathit{DT}(\mathcal{R}),\mathit{DT}(\mathcal{R}),\mathcal{R}\rangle}(t^{\sharp})$.
If
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$
is confluent, then
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}})=\mathit{Cplx}_{\langle\mathit{DT}(\mathcal{R}),\mathit{DT}(\mathcal{R}),\mathcal{R}\rangle}(t^{\sharp})$.

For automated complexity analysis with DTs, the following notion of _DT
problems_ is used as a characterisation of DTs that we reduce in incremental
proof steps to a trivially solved problem.

######  Definition 5 (DT Problem, Complexity of DT Problem [38])

Let $\mathcal{R}$ be a TRS, $\mathcal{D}$ be a set of DTs,
$\mathcal{S}\subseteq\mathcal{D}$. Then
$\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$ is a DT problem. Its
complexity function is
$\mathrm{irc}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(n)=\sup\\{\mathit{Cplx}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(t^{\sharp})\mid
t\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}},|t|\leq n\\}$. The DT problem
$\langle\mathit{DT}(\mathcal{R}),\mathit{DT}(\mathcal{R}),\mathcal{R}\rangle$
is called the _canonical DT problem_ for $\mathcal{R}$.

For a DT problem $\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$, the set
$\mathcal{D}$ contains all DTs that can be used in chain trees. $\mathcal{S}$
contains the DTs whose complexity remains to be analysed. $\mathcal{R}$
contains the rewrite rules for evaluating the arguments of DTs. Here we focus
on simplifying $\mathcal{S}$ (thus $\mathcal{D}$ and $\mathcal{R}$ are fixed
during the process) but techniques to simplify $\mathcal{D}$ and $\mathcal{R}$
are available as well [38, 8].

Thm. 2.1 implies the following link between $\mathrm{irc}_{\mathcal{R}}$ and
$\mathrm{irc}_{\langle\mathit{DT}(\mathcal{R}),\mathit{DT}(\mathcal{R}),\mathcal{R}\rangle}$:

######  Theorem 2.2 (Complexity Bounds for TRSs via Canonical DT Problems
[38])

Let $\mathcal{R}$ be a TRS with canonical DT problem
$\langle\mathit{DT}(\mathcal{R}),\mathit{DT}(\mathcal{R}),\mathcal{R}\rangle$.
Then we have
$\mathrm{irc}_{\mathcal{R}}(n)\leq\mathrm{irc}_{\langle\mathit{DT}(\mathcal{R}),\mathit{DT}(\mathcal{R}),\mathcal{R}\rangle}(n)$.
If
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$
is confluent, we have
$\mathrm{irc}_{\mathcal{R}}(n)=\mathrm{irc}_{\langle\mathit{DT}(\mathcal{R}),\mathit{DT}(\mathcal{R}),\mathcal{R}\rangle}(n)$.

In practice, the focus is on finding asymptotic bounds for
$\mathrm{irc}_{\mathcal{R}}$. For example, Ex. 4 will show that for our TRS
$\mathcal{R}$ from Ex. 1 we have
$\mathrm{irc}_{\mathcal{R}}(n)\in\mathcal{O}(n^{2})$.

A DT problem $\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$ is said to be
_solved_ iff $\mathcal{S}=\emptyset$: we always have
$\mathrm{irc}_{\langle\mathcal{D},\emptyset,\mathcal{R}\rangle}(n)=0$. To
simplify and finally solve DT problems in an incremental fashion, complexity
analysis techniques called _DT processors_ are used. A DT processor takes a DT
problem as input and returns a (hopefully simpler) DT problem as well as an
asymptotic complexity bound as an output. The largest asymptotic complexity
bound returned over this incremental process is then also an upper bound for
$\mathrm{irc}_{\mathcal{R}}(n)$ [38, Corollary 21].

The reduction pair processor using polynomial interpretations [38] applies a
restriction of polynomial interpretations to $\mathbb{N}$ [35] to infer upper
bounds on the number of times that DTs can occur in a chain tree for terms of
size at most $n$.

######  Definition 6 (Polynomial Interpretation, CPI)

A _polynomial interpretation_ ${\mathcal{P}ol}$ maps every $n$-ary function
symbol to a polynomial with variables $x_{1},\ldots,x_{n}$ and coefficients
from $\mathbb{N}$. ${\mathcal{P}ol}$ extends to terms via
${\mathcal{P}ol}(x)=x$ for $x\in\mathcal{V}$ and
${\mathcal{P}ol}(f(t_{1},\ldots,t_{n}))={\mathcal{P}ol}(f)({\mathcal{P}ol}(t_{1}),\ldots,{\mathcal{P}ol}(t_{n}))$.
${\mathcal{P}ol}$ induces an order $\succ_{\mathcal{P}ol}$and a quasi-order
$\succsim_{\mathcal{P}ol}$ over terms where $s\succ_{\mathcal{P}ol}t$ iff
${\mathcal{P}ol}(s)>{\mathcal{P}ol}(t)$ and $s\succsim_{\mathcal{P}ol}t$ iff
${\mathcal{P}ol}(s)\geq{\mathcal{P}ol}(t)$ for all instantiations of variables
with natural numbers.

A _complexity polynomial interpretation (CPI)_ ${\mathcal{P}ol}$ is a
polynomial interpretation where:
${\mathcal{P}ol}(\mathsf{Com}_{n}(x_{1},\ldots,x_{n}))=x_{1}+\dots+x_{n}$, and
for all $f\in\Sigma_{c}$, ${\mathcal{P}ol}(f(x_{1},\ldots,x_{n}))=a_{1}\cdot
x_{1}+\dots+a_{n}\cdot x_{n}+b$ for some $a_{i}\in\\{0,1\\}$ and
$b\in\mathbb{N}$.

The restriction for CPIs regarding constructor symbols enforces that the
interpretation of a constructor term $t$ (as an argument of a term for which a
chain tree is constructed) can exceed its size $\lvert t\rvert$ only by at
most a constant factor. This is crucial for soundness. Using a CPI, we can now
define and state correctness of the corresponding reduction pair processor
[38, Theorem 27].

######  Theorem 2.3 (Reduction Pair Processor with CPIs [38])

Let $\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$ be a DT problem, let
$\succsim$ and $\succ$ be induced by a CPI ${\mathcal{P}ol}$. Let
$k\in\mathbb{N}$ be the maximal degree of all polynomials
${\mathcal{P}ol}(f^{\sharp})$ for all $f\in\Sigma_{d}$. Let
$\mathcal{D}\cup\mathcal{R}\subseteq{\succsim}$. If
$\mathcal{S}\cap{\succ}\neq\emptyset$, the reduction pair processor returns
the DT problem
$\langle\mathcal{D},\mathcal{S}\setminus{\succ},\mathcal{R}\rangle$ and the
complexity $\mathcal{O}(n^{k})$. Then the reduction pair processor is sound.

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

For our running example, consider the CPI ${\mathcal{P}ol}$ with:
${\mathcal{P}ol}(\mathsf{plus}^{\sharp}(x_{1},x_{2}))={\mathcal{P}ol}(\mathsf{size}(x_{1}))=x_{1},\;{\mathcal{P}ol}(\mathsf{size}^{\sharp}(x_{1}))=2x_{1}+x_{1}^{2},\linebreak{\mathcal{P}ol}(\mathsf{plus}(x_{1},x_{2}))=x_{1}+x_{2},{\mathcal{P}ol}(\mathsf{Tree}(x_{1},x_{2},x_{3}))=1+x_{2}+x_{3},{\mathcal{P}ol}(\mathsf{S}(x_{1}))=1+x_{1},{\mathcal{P}ol}(\mathsf{Zero})={\mathcal{P}ol}(\mathsf{Nil})=1$.
${\mathcal{P}ol}$ orients all DTs in $\mathcal{S}=\mathit{DT}(\mathcal{R})$
with $\succ$ and all rules in $\mathcal{R}$ with $\succsim$. This proves
$\mathrm{irc}_{\mathcal{R}}(n)\in\mathcal{O}(n^{2})$: since the maximal degree
of the CPI for a symbol $f^{\sharp}$ is 2, the upper bound of
$\mathcal{O}(n^{2})$ follows by Thm. 2.3.

##  3 Finding Upper Bounds for Parallel Complexity

In this section we present our main contribution: an application of the DT
framework from innermost runtime complexity to _parallel-innermost rewriting_.

The notion of parallel-innermost rewriting dates back at least to [41].
Informally, in a parallel-innermost rewrite step, all innermost redexes are
rewritten simultaneously. This corresponds to executing all function calls in
parallel using a call-by-value strategy on a machine with unbounded
parallelism [16]. In the literature [40], this strategy is also known as “max-
parallel-innermost rewriting”.

######  Definition 7 (Parallel-Innermost Rewriting [20])

A term $s$ _rewrites innermost in parallel_ to $t$ with a TRS $\mathcal{R}$,
written
$s\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}t$, iff
$s\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}^{+}}t$,
and either (a)
$s\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}t$
with $s$ an innermost redex, or (b) $s=f(s_{1},\ldots,s_{n})$,
$t=f(t_{1},\ldots,t_{n})$, and for all $1\leq k\leq n$ either
$s_{k}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}t_{k}$ or $s_{k}=t_{k}$ is a normal form.

######  Example 5 (Ex. 1 continued)

The TRS $\mathcal{R}$ from Ex. 1 allows the following parallel-innermost
rewrite sequence, where innermost redexes are underlined:

$\begin{array}[]{rl}&\underline{\mathsf{size}(\mathsf{Tree}(\mathsf{Zero},\mathsf{Nil},\mathsf{Tree}(\mathsf{Zero},\mathsf{Nil},\mathsf{Nil})))}\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{plus}(\underline{\mathsf{size}(\mathsf{Nil})},\underline{\mathsf{size}(\mathsf{Tree}(\mathsf{Zero},\mathsf{Nil},\mathsf{Nil}))}))\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{plus}(\mathsf{Zero},\mathsf{S}(\mathsf{plus}(\underline{\mathsf{size}(\mathsf{Nil})},\underline{\mathsf{size}(\mathsf{Nil})}))))\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{plus}(\mathsf{Zero},\mathsf{S}(\underline{\mathsf{plus}(\mathsf{Zero},\mathsf{Zero})})))\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}&\mathsf{S}(\underline{\mathsf{plus}(\mathsf{Zero},\mathsf{S}(\mathsf{Zero}))})\\\
\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}&\mathsf{S}(\mathsf{S}(\mathsf{Zero}))\end{array}$

In the second and in the third step, two innermost steps each happen in
parallel (which is not possible with standard innermost rewriting:
$\mathrel{\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}}\ \not\subseteq\
\mathrel{\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}}$).
An innermost rewrite sequence without parallel evaluation necessarily needs
two more steps to a normal form from this start term, as in Ex. 1.

Note that for all TRSs $\mathcal{R}$,
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ is terminating iff
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$
is terminating [20]. Ex. 5 shows that such an equivalence does _not_ hold for
the derivation height of a term. The question now is: given a TRS
$\mathcal{R}$, how much of a speed-up might we get by a switch from innermost
to parallel-innermost rewriting? To investigate, we extend the notion of
innermost runtime complexity to parallel-innermost rewriting.

######  Definition 8 (Parallel-Innermost Runtime Complexity $\mathrm{pirc}$)

For $n\in\mathbb{N}$, we define the _parallel-innermost runtime complexity_
function as
$\mathrm{pirc}_{\mathcal{R}}(n)=\sup\\{\operatorname{dh}(t,{\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}})\mid
t\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}},\lvert t\rvert\leq n\\}$.

In the literature on parallel computing [16, 31, 12], the terms _depth_ or
_span_ are commonly used for the concept of the runtime of a function on a
machine with unbounded parallelism (“wall time”), corresponding to the
complexity measure of $\mathrm{pirc}_{\mathcal{R}}$. In contrast,
$\mathrm{irc}_{\mathcal{R}}$ would describe the _work_ of a function (“CPU
time”).

In the following, given a TRS $\mathcal{R}$, our goal shall be to infer
(asymptotic) upper bounds for $\mathrm{pirc}_{\mathcal{R}}$ fully
automatically. Of course, an upper bound for (sequential)
$\mathrm{irc}_{\mathcal{R}}$ is also an upper bound for
$\mathrm{pirc}_{\mathcal{R}}$. We will now introduce techniques to find upper
bounds for $\mathrm{pirc}_{\mathcal{R}}$ that are strictly tighter than these
trivial bounds.

To find upper bounds for runtime complexity of parallel-innermost rewriting,
we can _reuse_ the notion of DTs from Def. 3 for sequential innermost
rewriting along with existing techniques [38] as illustrated in the following
example.

###### Example 6

In the recursive $\mathsf{size}$-rule, the two calls to $\mathsf{size}(l)$ and
$\mathsf{size}(r)$ happen _in parallel_ (they are _structurally independent_)
and take place at _parallel positions_ in the term. Thus, the cost (number of
rewrite steps with
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ until a normal form is reached) for these two calls
is not the _sum_ , but the _maximum_ of their individual costs. Regardless of
which of these two calls has the higher cost, we still need to add the cost
for the call to $\mathsf{plus}$ on the results of the two calls:
$\mathsf{plus}$ starts evaluating only after both calls to $\mathsf{size}$
have finished. With $\sigma$ as the used matcher for the rule and with
$t\downarrow$ as the (here unique) normal form resulting from repeatedly
rewriting a term $t$ with
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ (the “result” of evaluating $t$), we have:

$\begin{array}[]{rl}&\operatorname{dh}(\mathsf{size}(\mathsf{Tree}(v,l,r))\sigma,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\\\
=&1+\max(\operatorname{dh}(\mathsf{size}(l)\sigma,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}),\operatorname{dh}(\mathsf{size}(r)\sigma,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}))\\\ &\hskip
163.6106pt{}+\operatorname{dh}(\mathsf{plus}(\mathsf{size}(l)\sigma\\!\downarrow,\mathsf{size}(r)\sigma\\!\downarrow),\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\end{array}$

In the DT setting, we could introduce a new symbol $\mathsf{ComPar}_{k}$ that
explicitly expresses that its arguments are evaluated in parallel. This symbol
would then be interpreted as the maximum of its arguments in an extension of
Thm. 2.3:

$\displaystyle\mathsf{size}^{\sharp}(\mathsf{Tree}(v,l,r))$
$\displaystyle\to\mathsf{Com}_{2}(\mathsf{ComPar}_{2}(\mathsf{size}^{\sharp}(l),\mathsf{size}^{\sharp}(r)),\mathsf{plus}^{\sharp}(\mathsf{size}(l),\mathsf{size}(r)))$

Although automation of the search for polynomial interpretations extended by
the maximum function is readily available [24], we would still have to extend
the notion of Dependency Tuples and also adapt all existing techniques in the
Dependency Tuple framework to work with $\mathsf{ComPar}_{k}$.

This is why we have chosen the following alternative approach, which is
equally powerful on theoretical level and enables immediate reuse of existing
techniques in the DT framework. Equivalently to the above, we can “factor in”
the cost of calling $\mathsf{plus}$ into the maximum function:

$\begin{array}[]{rl}&\operatorname{dh}(\mathsf{size}(\mathsf{Tree}(v,l,r))\sigma,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\\\
=&\max(1+\operatorname{dh}(\mathsf{size}(l)\sigma,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})+\operatorname{dh}(\mathsf{plus}(\mathsf{size}(l)\sigma\\!\downarrow,\mathsf{size}(r)\sigma\\!\downarrow),\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}),\\\ &\hskip
22.3888pt1+\operatorname{dh}(\mathsf{size}(r)\sigma,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})+\operatorname{dh}(\mathsf{plus}(\mathsf{size}(l)\sigma\\!\downarrow,\mathsf{size}(r)\sigma\\!\downarrow),\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}))\end{array}$

Intuitively, this would correspond to evaluating
$\mathsf{plus}(\ldots,\ldots)$ twice, in two parallel threads of execution,
which costs the same amount of (wall) time as evaluating
$\mathsf{plus}(\ldots,\ldots)$ once. We can represent this maximum of the
execution times of two threads by introducing _two_ DTs for our recursive
$\mathsf{size}$-rule:

$\begin{array}[]{rcl}\mathsf{size}^{\sharp}(\mathsf{Tree}(v,l,r))&\to&\mathsf{Com}_{2}(\mathsf{size}^{\sharp}(l),\mathsf{plus}^{\sharp}(\mathsf{size}(l),\mathsf{size}(r)))\\\
\mathsf{size}^{\sharp}(\mathsf{Tree}(v,l,r))&\to&\mathsf{Com}_{2}(\mathsf{size}^{\sharp}(r),\mathsf{plus}^{\sharp}(\mathsf{size}(l),\mathsf{size}(r)))\end{array}$

To express the cost of a concrete rewrite sequence, we would non-
deterministically choose the DT that corresponds to the “slower thread”.

In other words, when a rule $\ell\to r$ is used, the cost of the function call
to the instance of $\ell$ is 1 + the sum of the costs of the function calls in
the resulting instance of $r$ _that are in structural dependency with each
other_. The actual cost of the function call to the instance of $\ell$ in a
concrete rewrite sequence is the _maximum_ of all the possible costs caused by
such _chains_ of structural dependency (based on the prefix order $>$ on
positions of defined function symbols in $r$). Thus, _structurally
independent_ function calls are considered in separate DTs, whose non-
determinism models the parallelism of these function calls.

The notion of _structural dependency_ of function calls is captured by Def. 9.
Basically, it comes from the fact that a term cannot be evaluated before all
its subterms have been reduced to normal forms (innermost rewriting/_call by
value_). This induces a “happens-before” relation for the computation [34].

######  Definition 9 (Structural Dependency, $\mathit{MSDC}$)

For positions $\pi_{1},\ldots,\pi_{k}$, we call
$\langle\pi_{1},\dots,\pi_{k}\rangle$ a _structural dependency chain_ for a
term $t$ iff $\pi_{1},\ldots,\pi_{k}\in\mathcal{P}\\!\mathit{os}_{d}(t)$ and
$\pi_{1}>\ldots>\pi_{k}$. Here $\pi_{i}$ _structurally depends on_ $\pi_{j}$
in $t$ iff $j<i$. A structural dependency chain
$\langle\pi_{1},\dots,\pi_{k}\rangle$ for a term $t$ is _maximal_ iff $k=0$
and $\mathcal{P}\\!\mathit{os}_{d}(t)=\emptyset$, or $k>0$ and
$\forall\pi\in\mathcal{P}\\!\mathit{os}_{d}(t)\,.\,\pi\ngtr\pi_{1}\wedge(\pi_{1}>\pi\Rightarrow\pi\in\\{\pi_{2},\ldots,\pi_{k}\\})$.
We write $\mathit{MSDC}(t)$ for the set of all maximal structural dependency
chains for $t$.

Note that $\mathit{MSDC}(t)\neq\emptyset$ always holds: if
$\mathcal{P}\\!\mathit{os}_{d}(t)=\emptyset$, then
$\mathit{MSDC}(t)=\\{\langle\rangle\\}$.

###### Example 7

Let
$t=\mathsf{S}(\mathsf{plus}(\mathsf{size}(\mathsf{Nil}),\mathsf{plus}(\mathsf{size}(x),\mathsf{Zero})))$.
In our running example, $t$ has the following structural dependencies:
$\mathit{MSDC}(t)=\\{\langle 11,1\rangle,\langle 121,12,1\rangle\\}$. The
chain $\langle 11,1\rangle$ corresponds to the nesting of
$t|_{11}=\mathsf{size}(\mathsf{Nil})$ below
$t|_{1}=\mathsf{plus}(\mathsf{size}(\mathsf{Nil}),\mathsf{plus}(\mathsf{size}(x),\mathsf{Zero}))$,
so the evaluation of $t|_{1}$ will have to wait at least until $t|_{11}$ has
been fully evaluated.

If $\pi$ structurally depends on $\tau$ in a term $t$, neither $t|_{\tau}$ nor
$t|_{\pi}$ need to _be_ a redex.Rather, $t|_{\tau}$ could be _instantiated_ to
a redex and an instance of $t|_{\pi}$ could become a redex after its subterms,
including the instance of $t|_{\tau}$, have been evaluated.

We thus revisit the notion of DTs, which now embed structural dependencies in
addition to the algorithmic dependencies already captured in DTs.

######  Definition 10 (Parallel Dependency Tuples $\mathit{PDT}$, Canonical
Parallel DT Problem)

For a rewrite rule $\ell\to r$, we define the set of its _Parallel Dependency
Tuples (PDTs)_ $\mathit{PDT}(\ell\to r)$: $\mathit{PDT}(\ell\to
r)=\\{\ell^{\sharp}\to\mathsf{Com}_{k}(r|^{\sharp}_{\pi_{1}},\ldots,r|^{\sharp}_{\pi_{k}})\mid\langle\pi_{1},\ldots,\pi_{k}\rangle\in\mathit{MSDC}(r)\\}$.
For a TRS $\mathcal{R}$, let $\mathit{PDT}(\mathcal{R})=\bigcup_{\ell\to
r\in\mathcal{R}}\mathit{PDT}(\ell\to r)$. The _canonical parallel DT problem_
for $\mathcal{R}$ is
$\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle$.

###### Example 8

For our recursive $\mathsf{size}$-rule $\ell\to r$, we have
$\mathcal{P}\\!\mathit{os}_{d}(r)=\\{1,11,12\\}$ and
$\mathit{MSDC}(r)=\\{\langle 11,1\rangle,\langle 12,1\rangle\\}$. With
$\mathit{r}|_{1}=\mathsf{plus}(\mathsf{size}(l),\mathsf{size}(r))$,
$\mathit{r}|_{11}=\mathsf{size}(l)$, and $\mathit{r}|_{12}=\mathsf{size}(r)$,
we get the PDTs from Ex. 6. For the rule
$\mathsf{size}(\mathsf{Nil})\to\mathsf{Zero}$, we have
$\mathit{MSDC}(\mathsf{Zero})=\\{\langle\rangle\\}$, so we get
$\mathit{PDT}(\mathsf{size}(\mathsf{Nil})\to\mathsf{Zero})=\\{\mathsf{size}^{\sharp}(\mathsf{Nil})\to\mathsf{Com}_{0}\\}$.

We can now make our main correctness statement:

######  Theorem 3.1 ($\mathit{Cplx}$ bounds Derivation Height for
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$)

Let $\mathcal{R}$ be a TRS, let
$t=f(t_{1},\ldots,t_{n})\in\mathcal{T}(\Sigma,\mathcal{V})$ such that all
$t_{i}$ are in normal form (e.g., when
$t\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}}$). Then we have
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\leq\mathit{Cplx}_{\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle}(t^{\sharp})$.
If
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ is confluent, then
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=\mathit{Cplx}_{\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle}(t^{\sharp})$.222
The proof uses the confluence of $\mathcal{R}$ as a sufficient criterion for
_unique normal forms_.

From Thm. 3.1, the soundness of our approach to parallel complexity analysis
via the DT framework follows analogously to [38]:

######  Theorem 3.2 (Parallel Complexity Bounds for TRSs via Canonical
Parallel DT Problems)

Let $\mathcal{R}$ be a TRS with canonical parallel DT problem
$\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle$.
Then we have
$\mathrm{pirc}_{\mathcal{R}}(n)\leq\mathrm{irc}_{\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle}(n)$.
If
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ is confluent, we have
$\mathrm{pirc}_{\mathcal{R}}(n)=\mathrm{irc}_{\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle}(n)$.

This theorem implies that we can reuse arbitrary techniques to find upper
bounds for _sequential_ complexity in the DT framework also to find upper
bounds for _parallel_ complexity, without requiring any modification to the
framework.

Thus, via Thm. 2.3, in particular we can use polynomial interpretations in the
DT framework for our PDTs to get upper bounds for
$\mathrm{pirc}_{\mathcal{R}}$.

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

For our TRS $\mathcal{R}$ computing the $\mathsf{size}$ function on trees, we
get the set $\mathit{PDT}(\mathcal{R})$ with the following PDTs:

$\begin{array}[]{rcl}\mathsf{plus}^{\sharp}(\mathsf{Zero},y)&\to&\mathsf{Com}_{0}\\\
\mathsf{plus}^{\sharp}(\mathsf{S}(x),y)&\to&\mathsf{Com}_{1}(\mathsf{plus}^{\sharp}(x,y))\\\
\mathsf{size}^{\sharp}(\mathsf{Nil})&\to&\mathsf{Com}_{0}\\\
\mathsf{size}^{\sharp}(\mathsf{Tree}(v,l,r))&\to&\mathsf{Com}_{2}(\mathsf{size}^{\sharp}(l),\mathsf{plus}^{\sharp}(\mathsf{size}(l),\mathsf{size}(r)))\\\
\mathsf{size}^{\sharp}(\mathsf{Tree}(v,l,r))&\to&\mathsf{Com}_{2}(\mathsf{size}^{\sharp}(r),\mathsf{plus}^{\sharp}(\mathsf{size}(l),\mathsf{size}(r)))\end{array}$

The interpretation ${\mathcal{P}ol}$ from Ex. 4 implies
$\mathrm{pirc}_{\mathcal{R}}(n)\in\mathcal{O}(n^{2})$. This bound is tight:
consider $\mathsf{size}(t)$ for a comb-shaped tree $t$ where the first
argument of $\mathsf{Tree}$ is always $\mathsf{Zero}$ and the third is always
$\mathsf{Nil}$. The function $\mathsf{plus}$, which needs time linear in its
first argument, is called linearly often on data linear in the size of the
start term. Due to the structural dependencies, these calls do not happen in
parallel (so call $k+1$ to $\mathsf{plus}$ must wait for call $k$).

###### Example 10

Note that $\mathrm{pirc}_{\mathcal{R}}(n)$ can be asymptotically lower than
$\mathrm{irc}_{\mathcal{R}}(n)$, for instance for the TRS $\mathcal{R}$ with
the following rules:

$\begin{array}[]{rcl@{\hspace*{5ex}}|@{\hspace*{5ex}}rcl}\mathsf{doubles}(\mathsf{Zero})&\to&\mathsf{Nil}\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{d}(\mathsf{Zero})&\to&\mathsf{Zero}\\\
\mathsf{doubles}(\mathsf{S}(x))&\to&\mathsf{Cons}(\mathsf{d}(\mathsf{S}(x)),\mathsf{doubles}(x))\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{d}(\mathsf{S}(x))&\to&\mathsf{S}(\mathsf{S}(\mathsf{d}(x)))\end{array}$

The upper bound $\mathrm{irc}_{\mathcal{R}}(n)\in\mathcal{O}(n^{2})$ is tight:
from
$\mathsf{doubles}(\mathsf{S}(\mathsf{S}(\ldots\mathsf{S}(\mathsf{Zero})\ldots)))$,
we get linearly many calls to the linear-time function $\mathsf{d}$ on
arguments of size linear in the start term. However, the Parallel Dependency
Tuples in this example are:

$\begin{array}[]{rcl@{\hspace*{5ex}}|@{\hspace*{5ex}}rcl}\mathsf{doubles}^{\sharp}(\mathsf{Zero})&\to&\mathsf{Com}_{0}\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{d}^{\sharp}(\mathsf{Zero})&\to&\mathsf{Com}_{0}\\\
\mathsf{doubles}^{\sharp}(\mathsf{S}(x))&\to&\mathsf{Com}_{1}(\mathsf{d}^{\sharp}(\mathsf{S}(x)))\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{d}^{\sharp}(\mathsf{S}(x))&\to&\mathsf{Com}_{1}(\mathsf{d}^{\sharp}(x))\\\
\mathsf{doubles}^{\sharp}(\mathsf{S}(x))&\to&\mathsf{Com}_{1}(\mathsf{doubles}^{\sharp}(x))\hfil\hskip
21.52771pt\vrule\hskip 21.52771pt\end{array}$

Then the following polynomial interpretation, which orients all DTs with
$\succ$ and all rules from $\mathcal{R}$ with $\succsim$, proves
$\mathrm{pirc}_{\mathcal{R}}(n)\in\mathcal{O}(n)$:
${\mathcal{P}ol}(\mathsf{doubles}^{\sharp}(x_{1}))={\mathcal{P}ol}(\mathsf{d}(x_{1}))=2x_{1},{\mathcal{P}ol}(\mathsf{d}^{\sharp}(x_{1}))=x_{1},{\mathcal{P}ol}(\mathsf{doubles}(x_{1}))={\mathcal{P}ol}(\mathsf{Cons}(x_{1},x_{2}))={\mathcal{P}ol}(\mathsf{Zero})={\mathcal{P}ol}(\mathsf{Nil})=1,{\mathcal{P}ol}(\mathsf{S}(x_{1}))=1+x_{1}$.

Interestingly enough, Parallel Dependency Tuples also allow us to identify
TRSs that have _no_ potential for parallelisation by parallel-innermost
rewriting.

######  Theorem 3.3 (Absence of Parallelism by PDTs)

Let $\mathcal{R}$ be a TRS such that for all rules $\ell\to r\in\mathcal{R}$,
$|\mathit{MSDC}(r)|=1$. Then: (a)
$\mathit{PDT}(\mathcal{R})=\mathit{DT}(\mathcal{R})$; (b) for all basic terms
$t_{0}$ and rewrite sequences
$t_{0}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}t_{1}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}t_{2}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\dots$, also
$t_{0}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}t_{1}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}t_{2}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}\dots$
holds (i.e., from basic terms,
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ and
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$
coincide); (c) $\mathrm{pirc}_{\mathcal{R}}(n)=\mathrm{irc}_{\mathcal{R}}(n)$.

Thus, for TRSs $\mathcal{R}$ where Thm. 3.3 applies, no rewrite rule can
introduce parallel redexes, and specific analysis techniques for
$\mathrm{pirc}_{\mathcal{R}}$ are not needed.

##  4 From Parallel DTs to Innermost Rewriting

As we have seen in the previous section, we can transform a TRS $\mathcal{R}$
with parallel-innermost rewrite relation to a DT problem whose complexity
provides an upper bound of $\mathrm{pirc}_{\mathcal{R}}$ (or, for confluent
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$, corresponds exactly to
$\mathrm{pirc}_{\mathcal{R}}$). However, DTs are only one of many available
techniques to find bounds for $\mathrm{irc}_{\mathcal{R}}$. Other techniques
include, e.g., Weak Dependency Pairs [27], usable replacement maps [28], the
Combination Framework [8], a transformation to complexity problems for integer
transition systems [37], amortised complexity analysis [36], or techniques for
finding _lower_ bounds [23]. Thus, can we benefit also from other techniques
for (sequential) innermost complexity to analyse parallel complexity?

In this section, we answer the question in the affirmative, via a generic
transformation from Dependency Tuple problems back to rewrite systems whose
innermost complexity can then be analysed using arbitrary existing techniques.

We use _relative rewriting_ , which allows for labelling some of the rewrite
rules such that their use does not contribute to the derivation height of a
term. In other words, rewrite steps with these rewrite rules are “for free”
from the perspective of complexity. Existing state-of-the-art tools like
AProVE [25] and TcT [9] are able to find bounds on (innermost) runtime
complexity of such rewrite systems.

######  Definition 11 (Relative Rewriting)

For two TRSs ${\mathcal{R}_{1}}$ and ${\mathcal{R}_{2}}$,
${\mathcal{R}_{1}}/{\mathcal{R}_{2}}$ is a _relative TRS_. Its _rewrite
relation_ $\to_{{\mathcal{R}_{1}}/{\mathcal{R}_{2}}}$ is
$\to^{*}_{{\mathcal{R}_{2}}}\circ\to_{{\mathcal{R}_{1}}}\circ\to^{*}_{{\mathcal{R}_{2}}}$,
i.e., rewriting with ${\mathcal{R}_{2}}$ is allowed before and after each
${\mathcal{R}_{1}}$-step. We define the _innermost_ rewrite relation by
$s\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{{\mathcal{R}_{1}}/{\mathcal{R}_{2}}}}t$
iff
$s\to^{*}_{{\mathcal{R}_{2}}}s^{\prime}\to_{{\mathcal{R}_{1}}}s^{\prime\prime}\to^{*}_{{\mathcal{R}_{2}}}t$
for some terms $s^{\prime},s^{\prime\prime}$ such that the proper subterms of
the redexes of each step with $\to_{\mathcal{R}_{2}}$ or
$\to_{\mathcal{R}_{1}}$ are in normal form wrt
${\mathcal{R}_{1}}\cup{\mathcal{R}_{2}}$.

The set $\mathcal{T}_{\mathrm{basic}}^{{\mathcal{R}_{1}}/{\mathcal{R}_{2}}}$
of basic terms for a relative TRS ${\mathcal{R}_{1}}/{\mathcal{R}_{2}}$ is
$\mathcal{T}_{\mathrm{basic}}^{{\mathcal{R}_{1}}/{\mathcal{R}_{2}}}=\mathcal{T}_{\mathrm{basic}}^{{\mathcal{R}_{1}}\cup{\mathcal{R}_{2}}}$.
The notion of innermost runtime complexity extends to relative TRSs in the
natural way:
$\mathrm{irc}_{{\mathcal{R}_{1}}/{\mathcal{R}_{2}}}(n)=\sup\\{\operatorname{dh}(t,{\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{{\mathcal{R}_{1}}/{\mathcal{R}_{2}}}}})\mid
t\in\mathcal{T}_{\mathrm{basic}}^{{\mathcal{R}_{1}}/{\mathcal{R}_{2}}},\lvert
t\rvert\leq n\\}$

The rewrite relation
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{{\mathcal{R}_{1}}/{\mathcal{R}_{2}}}}$
is essentially the same as
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{{\mathcal{R}_{1}}\cup{\mathcal{R}_{2}}}}$,
but only steps using rules from ${\mathcal{R}_{1}}$ count towards the
complexity; steps using rules from ${\mathcal{R}_{2}}$ have no cost. This can
be useful, e.g., for representing that built-in functions from programming
languages modelled as recursive functions have constant cost.

###### Example 11

Consider a variant of Ex. 1 where
$\mathsf{plus}(\mathsf{S}(x),y)\to\mathsf{S}(\mathsf{plus}(x,y))$ is moved to
${\mathcal{R}_{2}}$, but all other rules are elements of ${\mathcal{R}_{1}}$.
Then ${\mathcal{R}_{1}}/{\mathcal{R}_{2}}$ would provide a modelling of the
$\mathsf{size}$ function that is closer to the Rust function from Sect. 1. Let
$\mathsf{S}^{n}(\mathsf{Zero})$ denote the term obtained by $n$-fold
application of $\mathsf{S}$ to $\mathsf{Zero}$ (e.g.,
$\mathsf{S}^{2}(\mathsf{Zero})=\mathsf{S}(\mathsf{S}(\mathsf{Zero}))$).
Although
$\operatorname{dh}(\mathsf{plus}(\mathsf{S}^{n}(\mathsf{Zero}),\mathsf{S}^{m}(\mathsf{Zero})),\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{{\mathcal{R}_{1}}\cup{\mathcal{R}_{2}}}})=n+1$,
we would then get
$\operatorname{dh}(\mathsf{plus}(\mathsf{S}^{n}(\mathsf{Zero}),\mathsf{S}^{m}(\mathsf{Zero})),\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{{\mathcal{R}_{1}}/{\mathcal{R}_{2}}}})=1$,
corresponding to a machine model where the time of evaluating addition for
integers is constant.

Note the similarity of a relative TRS and a Dependency Tuple problem: only
certain rewrite steps count towards the analysed complexity. We make use of
this observation for the following transformation.

######  Definition 12 (Relative TRS for a Dependency Tuple Problem, $\delta$)

Let $\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$ be a Dependency Tuple
problem. We define the corresponding relative TRS
$\delta(\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle)=\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})$.

In other words, we omit the information that steps with our dependency tuples
can happen only on top level (possibly below constructors $\mathsf{Com}_{n}$,
but above $\mathrel{\smash{\rightarrow}_{\mathcal{R}}}$ steps). (As we shall
see in Thm. 4.2, this information can be recovered.)

The following example is taken from the _Termination Problem Data Base (TPDB)_
[43], a collection of examples used at the annual _Termination and Complexity
Competition (termCOMP)_ [26, 42] (see also Sect. 5):

######  Example 12 (TPDB, HirokawaMiddeldorp_04/t002)

Consider the following TRS $\mathcal{R}$ from category
Innermost_Runtime_Complexity of the TPDB:

$\begin{array}[]{rcl@{\hspace*{5ex}}|@{\hspace*{5ex}}rcl}\mathsf{leq}(\mathsf{0},y)&\to&\mathsf{true}\hfil\hskip
21.52771pt\vrule\hskip 21.52771pt&\mathsf{if}(\mathsf{true},x,y)&\to&x\\\
\mathsf{leq}(\mathsf{s}(x),\mathsf{0})&\to&\mathsf{false}\hfil\hskip
21.52771pt\vrule\hskip 21.52771pt&\mathsf{if}(\mathsf{false},x,y)&\to&y\\\
\mathsf{leq}(\mathsf{s}(x),\mathsf{s}(y))&\to&\mathsf{leq}(x,y)\hfil\hskip
21.52771pt\vrule\hskip 21.52771pt&\mathsf{-}(x,\mathsf{0})&\to&x\\\
\mathsf{mod}(\mathsf{0},y)&\to&\mathsf{0}\hfil\hskip 21.52771pt\vrule\hskip
21.52771pt&\mathsf{-}(\mathsf{s}(x),\mathsf{s}(y))&\to&\mathsf{-}(x,y)\\\
\mathsf{mod}(\mathsf{s}(x),\mathsf{0})&\to&\mathsf{0}\hfil\hskip
21.52771pt\vrule\hskip 21.52771pt\\\
\mathsf{mod}(\mathsf{s}(x),\mathsf{s}(y))&\to&\lx@intercol\mathsf{if}(\mathsf{leq}(y,x),\mathsf{mod}(\mathsf{-}(\mathsf{s}(x),\mathsf{s}(y)),\mathsf{s}(y)),\mathsf{s}(x))\hfil\lx@intercol\end{array}$

This TRS has the following PDTs $\mathit{PDT}(\mathcal{R})$:

$\begin{array}[]{rcl@{\hspace*{5ex}}|@{\hspace*{5ex}}rcl}\mathsf{leq}^{\sharp}(\mathsf{0},y)&\to&\mathsf{Com}_{0}\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{if}^{\sharp}(\mathsf{true},x,y)&\to&\mathsf{Com}_{0}\\\
\mathsf{leq}^{\sharp}(\mathsf{s}(x),\mathsf{0})&\to&\mathsf{Com}_{0}\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{if}^{\sharp}(\mathsf{false},x,y)&\to&\mathsf{Com}_{0}\\\
\mathsf{leq}^{\sharp}(\mathsf{s}(x),\mathsf{s}(y))&\to&\mathsf{Com}_{1}(\mathsf{leq}^{\sharp}(x,y))\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{-}^{\sharp}(x,\mathsf{0})&\to&\mathsf{Com}_{0}\\\
\mathsf{mod}^{\sharp}(\mathsf{0},y)&\to&\mathsf{Com}_{0}\hfil\hskip
21.52771pt\vrule\hskip
21.52771pt&\mathsf{-}^{\sharp}(\mathsf{s}(x),\mathsf{s}(y))&\to&\mathsf{Com}_{1}(\mathsf{-}^{\sharp}(x,y))\\\
\mathsf{mod}^{\sharp}(\mathsf{s}(x),\mathsf{0})&\to&\mathsf{Com}_{0}\hfil\hskip
21.52771pt\vrule\hskip 21.52771pt\\\
\mathsf{mod}^{\sharp}(\mathsf{s}(x),\mathsf{s}(y))&\to&\lx@intercol\mathsf{Com}_{2}(\mathsf{leq}^{\sharp}(y,x),\mathsf{if}^{\sharp}(\mathsf{leq}(y,x),\mathsf{mod}(\mathsf{-}(\mathsf{s}(x),\mathsf{s}(y)),\mathsf{s}(y)),\mathsf{s}(x)))\hfil\lx@intercol\\\
\mathsf{mod}^{\sharp}(\mathsf{s}(x),\mathsf{s}(y))&\to&\lx@intercol\mathsf{Com}_{3}(\mathsf{-}^{\sharp}(\mathsf{s}(x),\mathsf{s}(y)),\mathsf{mod}^{\sharp}(\mathsf{-}(\mathsf{s}(x),\mathsf{s}(y)),\mathsf{s}(y)),\hfil\lx@intercol\\\
&&\lx@intercol\hfil\mathsf{if}^{\sharp}(\mathsf{leq}(y,x),\mathsf{mod}(\mathsf{-}(\mathsf{s}(x),\mathsf{s}(y)),\mathsf{s}(y)),\mathsf{s}(x)))\lx@intercol\end{array}$

The canonical parallel DT problem is
$\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle$.
We get the relative TRS
$\delta(\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle)=\mathit{PDT}(\mathcal{R})/\mathcal{R}$.

######  Theorem 4.1 (Upper Complexity Bounds for
$\delta(\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle)$ from
$\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$)

Let $\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$ be a DT problem. Then
(a) for all $t^{\sharp}\in\mathcal{T}^{\sharp}$ with
$t\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}}$, we have
$\mathit{Cplx}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(t^{\sharp})\,{\leq}\operatorname{dh}(t^{\sharp},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})$,
and (b)
$\mathrm{irc}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(n)\,{\leq}\,\mathrm{irc}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}(n)$.

######  Example 13 (Ex. 12 continued)

For the relative TRS $\mathit{PDT}(\mathcal{R})/\mathcal{R}$ from Ex. 12, the
tool AProVE uses a transformation to integer transition systems [37] followed
by an application of the complexity analysis tool CoFloCo [22, 21] to find a
bound
$\mathrm{irc}_{\mathit{PDT}(\mathcal{R})/\mathcal{R}}(n)\in\mathcal{O}(n)$ and
to deduce the bound $\mathrm{pirc}_{\mathcal{R}}(n)\in\mathcal{O}(n)$ for the
original TRS $\mathcal{R}$ from the TPDB. In contrast, using the techniques of
Sect. 3 without the transformation to a relative TRS from Def. 12, AProVE
finds only a bound $\mathrm{pirc}_{\mathcal{R}}(n)\in\mathcal{O}(n^{2})$.

Intriguingly, we can use our transformation from Def. 12 not only for finding
upper bounds, but also for _lower_ bounds on $\mathrm{pirc}_{\mathcal{R}}$.

######  Theorem 4.2 (Lower Complexity Bounds for
$\delta(\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle)$ from
$\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$)

Let $\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$ be a DT problem. Then
(a) there is a type assignment s.t. for all$\ell\to
r\in\mathcal{D}\cup\mathcal{R}$, $\ell$ and $r$ get the same type, and for all
well-typed $t\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{D}\cup\mathcal{R}}$,
$\mathit{Cplx}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(t^{\sharp})\geq\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})$,
and (b)
$\mathrm{irc}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(n)\geq\mathrm{irc}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}(n)$.

Thm. 4.1 and Thm. 4.2 hold regardless of whether the original DT problem was
obtained from a TRS with sequential or with parallel evaluation. So while this
kind of connection between DT (or DP) problems and relative rewriting may be
folklore in the community, its application to convert a TRS whose _parallel_
complexity is sought to a TRS with the same _sequential_ complexity is new.

Note that Thm. 3.2 requires confluence of
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ to derive lower bounds for
$\mathrm{pirc}_{\mathcal{R}}$ from lower complexity bounds of the canonical
parallel DT problem. So to use Thm. 4.2 to search for _lower_ complexity
bounds with existing techniques [23], we need a criterion for confluence of
parallel-innermost rewriting.

######  Example 14 (Confluence of
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$
does not Imply Confluence of
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$)

To see that we cannot prove confluence of
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ just by using a standard off-the-shelf tool for
confluence analysis of innermost or full rewriting [17], consider the TRS
$\mathcal{R}=\\{\mathsf{a}\to\mathsf{f}(\mathsf{b},\mathsf{b}),\mathsf{a}\to\mathsf{f}(\mathsf{b},\mathsf{c}),\mathsf{b}\to\mathsf{c},\mathsf{c}\to\mathsf{b}\\}$.
For this TRS, both
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$
and $\mathrel{\smash{\rightarrow}_{\mathcal{R}}}$ are confluent. However,
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ is not confluent: we can rewrite both
$\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\mathsf{f}(\mathsf{b},\mathsf{b})$ and
$\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\mathsf{f}(\mathsf{b},\mathsf{c})$, yet there is no
term $v$ such that
$\mathsf{f}(\mathsf{b},\mathsf{b})\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}^{*}_{\mathcal{R}}}v$ and
$\mathsf{f}(\mathsf{b},\mathsf{c})\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}^{*}_{\mathcal{R}}}v$. The reason is that the only possible rewrite
sequences with
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ from these terms are
$\mathsf{f}(\mathsf{b},\mathsf{b})\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\mathsf{f}(\mathsf{c},\mathsf{c})\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\mathsf{f}(\mathsf{b},\mathsf{b})\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\dots$ and
$\mathsf{f}(\mathsf{b},\mathsf{c})\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\mathsf{f}(\mathsf{c},\mathsf{b})\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\mathsf{f}(\mathsf{b},\mathsf{c})\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\dots$, with no terms in common.

###### Conjecture 1

If
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ is confluent, then
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$
is confluent.

Confluence means: if a term $s$ can be rewritten to two different terms
$t_{1}$ and $t_{2}$ in 0 or more steps, it is always possible to rewrite
$t_{1}$ and $t_{2}$ in 0 or more steps to a term $u$. For
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$, the redexes that get rewritten are fixed: all
innermost redexes simultaneously. Thus, $s$ can rewrite to two _different_
terms $t_{1}$ and $t_{2}$ only if at least one of these redexes can be
rewritten in two different ways using
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$.

Towards a sufficient criterion for confluence of parallel-innermost rewriting,
we introduce the following standard definition:

######  Definition 13 (Non-Overlapping)

A TRS $\mathcal{R}$ is _non-overlapping_ iff for any two rules $\ell\to r,u\to
v\in\mathcal{R}$ where variables have been renamed apart between the rules,
there is no position $\pi$ in $\ell$ such that $\ell|_{\pi}\notin\mathcal{V}$
and the terms $\ell|_{\pi}$ and $u$ unify.

A sufficient criterion that a given redex has a unique result from a rewrite
step is given in the following.

######  Lemma 1 ([11], Lemma 6.3.9)

If a TRS $\mathcal{R}$ is non-overlapping,
$s\mathrel{\smash{\rightarrow}_{\mathcal{R}}}t_{1}$ and
$s\mathrel{\smash{\rightarrow}_{\mathcal{R}}}t_{2}$ with the redex of both
rewrite steps at the same position, then $t_{1}=t_{2}$.

With the above reasoning, this lemma directly gives us a sufficient criterion
for confluence of _parallel-innermost_ rewriting.

######  Corollary 1 (Confluence of Parallel-Innermost Rewriting)

If a TRS $\mathcal{R}$ is non-overlapping, then
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ is confluent.

So, in those cases we can actually use this sequence of transformations from a
parallel-innermost TRS via a DT problem to an innermost (relative) TRS to
analyse both upper and lower bounds for the original. Conveniently, these
cases correspond to deterministic programs, our motivation for this work!

######  Example 15 (Ex. 13 continued)

Cor. 1 and Thm. 4.2 imply that a lower bound for
$\mathrm{irc}_{\mathit{PDT}(\mathcal{R})/\mathcal{R}}(n)$ of the relative TRS
$\mathit{PDT}(\mathcal{R})/\mathcal{R}$ from Ex. 12 carries over to
$\mathrm{pirc}_{\mathcal{R}}(n)$ of the original TRS $\mathcal{R}$ from the
TPDB. AProVE uses rewrite lemmas [23] to find the lower bound
$\mathrm{irc}_{\mathit{PDT}(\mathcal{R})/\mathcal{R}}(n)\in\Omega(n)$.
Together with Ex. 13, we have automatically inferred that this complexity
bound is _tight_ : $\mathrm{pirc}_{\mathcal{R}}(n)\in\Theta(n)$.

##  5 Implementation and Experiments

We have implemented the contributions of this paper in the automated
termination and complexity analysis tool AProVE [25]. We added or modified 620
lines of Java code, including  1. the framework of parallel-innermost
rewriting;  2. the generation of parallel DTs (Thm. 3.2);  3. a processor to
convert them to TRSs with the same complexity (Thm. 4.1, Thm. 4.2);  4. the
confluence test of Cor. 1.  As far as we are aware, this is the first
implementation of a fully automated inference of complexity bounds for
parallel-innermost rewriting. To demonstrate the effectiveness of our
implementation, we have considered the 663 TRSs from category
Runtime_Complexity_Innermost_Rewriting of the TPDB, version 11.2 [43]. This
category of the TPDB is the benchmark collection used at termCOMP to compare
tools that infer complexity bounds for runtime complexity of innermost
rewriting, $\mathrm{irc}_{\mathcal{R}}$. To get meaningful results, we first
applied Thm. 3.3 to exclude TRSs $\mathcal{R}$ where
$\mathrm{pirc}_{\mathcal{R}}(n)=\mathrm{irc}_{\mathcal{R}}(n)$ trivially
holds. We obtained 294 TRSs with potential for parallelism as our benchmark
set. We conducted our experiments on the StarExec compute cluster [39] in the
all.q queue. The timeout per example and tool configuration was set to 300
seconds. Our experimental data with analysis times and all examples are
available online [1].

As remarked earlier, we always have
$\mathrm{pirc}_{\mathcal{R}}(n)\leq\mathrm{irc}_{\mathcal{R}}(n)$, so an upper
bound for $\mathrm{irc}_{\mathcal{R}}(n)$ is always a legitimate upper bound
for $\mathrm{pirc}_{\mathcal{R}}(n)$. Thus, we include upper bounds for
$\mathrm{irc}_{\mathcal{R}}$ found by the state-of-the-art tools AProVE and
TcT [2, 9]. from termCOMP 2021 as a “baseline” in our evaluation. We compare
with several configurations of AProVE and TcT that use the techniques of this
paper for $\mathrm{pirc}_{\mathcal{R}}$: “AProVE $\mathrm{pirc}_{\mathcal{R}}$
Section 3” also uses Thm. 3.2 to produce canonical parallel DT problems as
input for the DT framework. “AProVE $\mathrm{pirc}_{\mathcal{R}}$ Sections 3 &
4” additionally uses the transformation from Def. 12 to convert a TRS
$\mathcal{R}$ to a relative TRS $\mathit{PDT}(\mathcal{R})/\mathcal{R}$ and
then to analyse $\mathrm{irc}_{\mathit{PDT}(\mathcal{R})/\mathcal{R}}(n)$ (for
lower bounds only together with a confluence proof via Cor. 1). We also
extracted each of the TRSs $\mathit{PDT}(\mathcal{R})/\mathcal{R}$ and used
the files as inputs for AProVE and TcT from termCOMP 2021. “AProVE
$\mathrm{pirc}_{\mathcal{R}}$ Section 4” and “TcT
$\mathrm{pirc}_{\mathcal{R}}$ Section 4” provide the results for
$\mathrm{irc}_{\mathit{PDT}(\mathcal{R})/\mathcal{R}}$ (for lower bounds, only
where
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ had been proved confluent).

Tool | $\mathcal{O}(1)$ | $\leq\mathcal{O}(n)$ | $\leq\mathcal{O}(n^{2})$ | $\leq\mathcal{O}(n^{3})$ | $\leq\mathcal{O}(n^{\geq 4})$
---|---|---|---|---|---
TcT $\mathrm{irc}_{\mathcal{R}}$ | 4 | 28 | 39 | 44 | 44
AProVE $\mathrm{irc}_{\mathcal{R}}$ | 5 | 50 | 110 | 123 | 127
AProVE $\mathrm{pirc}_{\mathcal{R}}$ Section 3 | 5 | 65 | 125 | 140 | 142
AProVE $\mathrm{pirc}_{\mathcal{R}}$ Sections 3 & 4 | 5 | 69 | 125 | 139 | 141
TcT $\mathrm{pirc}_{\mathcal{R}}$ Section 4 | 3 | 39 | 52 | 56 | 57
AProVE $\mathrm{pirc}_{\mathcal{R}}$ Section 4 | 5 | 62 | 96 | 105 | 105

Table 1: Upper bounds for runtime complexity of (parallel-)innermost rewriting

Tool | confluent | $\geq\Omega(n)$ | $\geq\Omega(n^{2})$ | $\geq\Omega(n^{3})$ | $\geq\Omega(n^{\geq 4})$
---|---|---|---|---|---
AProVE $\mathrm{pirc}_{\mathcal{R}}$ Sections 3 & 4 | 186 | 133 | 23 | 5 | 1
TcT $\mathrm{pirc}_{\mathcal{R}}$ Section 4 | 186 | 59 | 0 | 0 | 0
AProVE $\mathrm{pirc}_{\mathcal{R}}$ Section 4 | 186 | 155 | 22 | 5 | 1

Table 2: Lower bounds for runtime complexity of parallel-innermost rewriting

Tool | $\Theta(1)$ | $\Theta(n)$ | $\Theta(n^{2})$ | $\Theta(n^{3})$ | Total
---|---|---|---|---|---
AProVE $\mathrm{pirc}_{\mathcal{R}}$ Sections 3 & 4 | 5 | 32 | 1 | 3 | 41
TcT $\mathrm{pirc}_{\mathcal{R}}$ Section 4 | 3 | 21 | 0 | 0 | 24
AProVE $\mathrm{pirc}_{\mathcal{R}}$ Section 4 | 5 | 37 | 1 | 3 | 46

Table 3: Tight bounds for runtime complexity of parallel-innermost rewriting

Table 3 gives an overview over our experimental results for upper bounds. For
each configuration, we state the number of examples for which the
corresponding asymptotic complexity bound was inferred. A column
“$\leq\mathcal{O}(n^{k})$” means that the corresponding tools proved a bound
$\leq\mathcal{O}(n^{k})$ (e.g., the configuration “AProVE
$\mathrm{irc}_{\mathcal{R}}$” proved constant or linear upper bounds in 50
cases). Maximum values in a column are highlighted in bold. We observe that
upper complexity bounds improve in a noticeable number of cases, e.g., linear
bounds on $\mathrm{pirc}_{\mathcal{R}}$ can now be inferred for 69 TRSs rather
than for 50 TRSs (using upper bounds on $\mathrm{irc}_{\mathcal{R}}$ as an
over-approximation), an improvement by 38%. Note that this does _not_ indicate
deficiencies in the existing tools for $\mathrm{irc}_{\mathcal{R}}$, which had
not been designed with analysis of $\mathrm{pirc}_{\mathcal{R}}$ in mind –
rather, it shows that specialised techniques for analysing
$\mathrm{pirc}_{\mathcal{R}}$ are a worthwhile subject of investigation. Note
also that Ex. 4 and Ex. 9 show that even for TRSs with potential for
parallelism, the actual parallel and sequential complexity may still be
asymptotically identical, which further highlights the need for dedicated
analysis techniques for $\mathrm{pirc}_{\mathcal{R}}$.

The improvement from $\mathrm{irc}_{\mathcal{R}}$ to
$\mathrm{pirc}_{\mathcal{R}}$ can be drastic: for example, for the TRS
TCT_12/recursion_10, the bounds found by AProVE change from an upper bound of
sequential complexity of $\mathcal{O}(n^{10})$ to a (tight) upper bound for
parallel complexity of $\mathcal{O}(n)$. (This TRS models a specific recursion
structure, with rules
$\\{\mathsf{f}_{0}(x)\to\mathsf{a}\\}\cup\\{\mathsf{f}_{i}(x)\to\mathsf{g}_{i}(x,x),\;\mathsf{g}_{i}(\mathsf{s}(x),y)\to\mathsf{b}(\mathsf{f}_{i-1}(y),\mathsf{g}_{i}(x,y))\mid
1\leq i\leq 10\\}$, and is highly amenable to parallelisation.) We observe
that adding the techniques from Sect. 4 to the techniques from Sect. 3 leads
to only few examples for which better upper bounds can be found (one of them
is Ex. 13).

Table 3 shows our results for lower bounds on $\mathrm{pirc}_{\mathcal{R}}$.
Here we evaluated only configurations including Def. 12 to make inference
techniques for lower bounds of $\mathrm{irc}_{\mathcal{R}}$ applicable to
$\mathrm{pirc}_{\mathcal{R}}$. The reason is that a lower bound on
$\mathrm{irc}_{\mathcal{R}}$ is not necessarily also a lower bound for
$\mathrm{pirc}_{\mathcal{R}}$ (the whole _point_ of performing innermost
rewriting in parallel is to reduce the asymptotic complexity!), so using
results by tools that compute lower bounds on $\mathrm{irc}_{\mathcal{R}}$ for
comparison would not make sense. We observe that non-trivial lower bounds can
be inferred for 155 out of the 186 examples proved confluent via Cor. 1. This
shows that our transformation from Sect. 4 has practical value since it
produces relative TRSs that are generally amenable to analysis by existing
program analysis tools. Finally, Table 3 shows that for overall 46 TRSs, the
bounds that were found are asymptotically _precise_.

##  6 Related Work, Conclusion, and Future Work

_Related work._ We provide pointers to work on automated analysis of
(sequential) innermost runtime complexity of TRSs at the start of Sect. 4. We
now focus on automated techniques for complexity analysis of
parallel/concurrent computation.

Our notion of parallel complexity follows a large tradition of static _cost
analysis_ , notably for concurrent programming. The two notable works [4, 5]
address async/finish programs where tasks are explicitly launched. The authors
propose several metrics such as the total number of spawned tasks (in any
execution of the program) and a notion of parallel complexity that is roughly
the same as ours. They provide static analyses that build on techniques for
estimating costs of imperative languages with functions calls [3], and/or
recurrence equations. Recent approaches for the Pi Calculus [12, 13] compute
the _span_ (our parallel complexity) through a new typing system. Another
type-based calculus for the same purpose has been proposed with session types
[18].

For logic programs, which – like TRSs – express an implicit parallelism,
parallel complexity can be inferred using recurrence solving [32].

The tool RAML [30] derives bounds on the worst-case evaluation cost of first-
order functional programs with list and pair constructors as well as pattern
matching and both sequential and parallel composition [31]. They use two
typing derivations with specially annotated types, one for the _work_ and one
for the _depth_ (parallel complexity). Our setting is more flexible wrt the
shape of user-defined data structures (we allow for tree constructors of
arbitrary arity), and our analysis deals with both data structure and control
in an integrated manner.

_Conclusion and future work._ We have defined parallel-innermost runtime
complexity for TRSs and proposed an approach to its automated analysis. Our
approach allows for finding both upper and lower bounds and builds on existing
techniques and tools. Our experiments on the TPDB indicate that our approach
is practically usable, and we are confident that it captures the potential
parallelism of programs with pattern matching.

Parallel rewriting is a topic of active research, e.g., for GPU-based
massively parallel rewrite engines [19]. Here our work could be useful to
determine which functions to evaluate on the GPU. More generally,
parallelising compilers which need to determine which function calls should be
compiled into parallel code may benefit from an analysis of parallel-innermost
runtime complexity such as ours.

DTs have been used [44] in runtime complexity analysis of _Logically
Constrained TRSs (LCTRSs)_ [33], an extension of TRSs by built-in data types
from SMT theories (integers, arrays, …). This work could be extended to
parallel rewriting. Moreover, analysis of _derivational complexity_ [29] of
parallel-innermost term rewriting can be a promising direction. Derivational
complexity considers the length of rewrite sequences from arbitrary start
terms,
e.g.,$\mathsf{d}(\mathsf{d}(\dots(\mathsf{d}(\mathsf{S}(\mathsf{Zero})))\dots))$
in Ex. 10, which can have longer derivations than basic terms of the same
size. Finally, towards automated parallelisation we aim to infer complexity
bounds wrt term _height_ (terms = trees!), as suggested in [6].

_Acknowledgements._ We thank the anonymous reviewers for helpful comments.

## References

  * [1] https://www.dcs.bbk.ac.uk/~carsten/eval/parallel_complexity/
  * [2] https://www.starexec.org/starexec/secure/details/solver.jsp?id=29575
  * [3] Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413(1), 142–159 (2012), https://doi.org/10.1016/j.tcs.2011.07.009
  * [4] Albert, E., Arenas, P., Genaim, S., Zanardini, D.: Task-level analysis for a language with async/finish parallelism. In: Vitek, J., Sutter, B.D. (eds.) Proceedings of the ACM SIGPLAN/SIGBED 2011 conference on Languages, compilers, and tools for embedded systems, LCTES 2011, Chicago, IL, USA, April 11-14, 2011. pp. 21–30. ACM (2011), https://doi.org/10.1145/1967677.1967681
  * [5] Albert, E., Correas, J., Johnsen, E.B., Pun, V.K.I., Román-Díez, G.: Parallel cost analysis. ACM Trans. Comput. Log. 19(4), 31:1–31:37 (2018), https://doi.org/10.1145/3274278
  * [6] Alias, C., Fuhs, C., Gonnord, L.: Estimation of Parallel Complexity with Rewriting Techniques. In: Proceedings of the 15th Workshop on Termination (WST 2016). pp. 2:1–2:5 (2016), https://hal.archives-ouvertes.fr/hal-01345914
  * [7] Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
  * [8] Avanzini, M., Moser, G.: A combination framework for complexity. Information and Computation 248, 22–55 (2016), https://doi.org/10.1016/j.ic.2015.12.007
  * [9] Avanzini, M., Moser, G., Schaper, M.: TcT: Tyrolean Complexity Tool. In: Chechik, M., Raskin, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9636, pp. 407–423. Springer (2016), https://doi.org/10.1007/978-3-662-49674-9_24
  * [10] Avanzini, M., Felgenhauer, B.: Type introduction for runtime complexity analysis. In: WST ’14. pp. 1–5 (2014), available from http://www.easychair.org/smart-program/VSL2014/WST-proceedings.pdf
  * [11] Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge Univ. Press (1998)
  * [12] Baillot, P., Ghyselen, A.: Types for complexity of parallel computation in pi-calculus. In: Yoshida, N. (ed.) Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12648, pp. 59–86. Springer (2021), https://doi.org/10.1007/978-3-030-72019-3_3
  * [13] Baillot, P., Ghyselen, A., Kobayashi, N.: Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference. LIPIcs, vol. 203, pp. 34:1–34:22. Schloss Dagstuhl \- Leibniz-Zentrum für Informatik (2021), https://doi.org/10.4230/LIPIcs.CONCUR.2021.34
  * [14] Baudon, T., Fuhs, C., Gonnord, L.: Parallel complexity of term rewriting systems. In: 17th International Workshop on Termination (WST 2021). pp. 45–50 (2021), https://hal.archives-ouvertes.fr/hal-03418400/document
  * [15] Baudon, T., Fuhs, C., Gonnord, L.: Analysing parallel complexity of term rewriting. In: 32nd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2022). Lecture Notes in Computer Science, Springer (2022), To appear.
  * [16] Blelloch, G.E., Greiner, J.: Parallelism in sequential functional languages. In: Williams, J. (ed.) Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995. pp. 226–237. ACM (1995), https://doi.org/10.1145/224164.224210
  * [17] Community: The international Confluence Competition (CoCo), http://project-coco.uibk.ac.at/
  * [18] Das, A., Hoffmann, J., Pfenning, F.: Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang. 2(ICFP), 91:1–91:30 (2018), https://doi.org/10.1145/3236786
  * [19] van Eerd, J., Groote, J.F., Hijma, P., Martens, J., Wijs, A.: Term rewriting on GPUs. In: Hojjat, H., Massink, M. (eds.) Fundamentals of Software Engineering - 9th International Conference, FSEN 2021, Virtual Event, May 19-21, 2021, Revised Selected Papers. Lecture Notes in Computer Science, vol. 12818, pp. 175–189. Springer (2021), https://doi.org/10.1007/978-3-030-89247-0_12
  * [20] Fernández, M., Godoy, G., Rubio, A.: Orderings for innermost termination. In: Giesl, J. (ed.) Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3467, pp. 17–31. Springer (2005), https://doi.org/10.1007/978-3-540-32033-3_3
  * [21] Flores-Montoya, A.: Upper and lower amortized cost bounds of programs expressed as cost relations. In: Fitzgerald, J.S., Heitmeyer, C.L., Gnesi, S., Philippou, A. (eds.) FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9995, pp. 254–273 (2016), https://doi.org/10.1007/978-3-319-48989-6_16
  * [22] Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) Programming Languages and Systems \- 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8858, pp. 275–295. Springer (2014), https://doi.org/10.1007/978-3-319-12736-1_15
  * [23] Frohn, F., Giesl, J., Hensel, J., Aschermann, C., Ströder, T.: Lower bounds for runtime complexity of term rewriting. J. Autom. Reason. 59(1), 121–163 (2017), https://doi.org/10.1007/s10817-016-9397-x
  * [24] Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: Voronkov, A. (ed.) Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5117, pp. 110–125. Springer (2008), https://doi.org/10.1007/978-3-540-70590-1_8
  * [25] Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58(1), 3–31 (2017), https://doi.org/10.1007/s10817-016-9388-y
  * [26] Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III. Lecture Notes in Computer Science, vol. 11429, pp. 156–166. Springer (2019), https://doi.org/10.1007/978-3-030-17502-3_10
  * [27] Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5195, pp. 364–379. Springer (2008), https://doi.org/10.1007/978-3-540-71070-7_32
  * [28] Hirokawa, N., Moser, G.: Automated complexity analysis based on context-sensitive rewriting. In: Dowek, G. (ed.) Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8560, pp. 257–271. Springer (2014), https://doi.org/10.1007/978-3-319-08918-8_18
  * [29] Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, April 3-5, 1989, Proceedings. Lecture Notes in Computer Science, vol. 355, pp. 167–177. Springer (1989). https://doi.org/10.1007/3-540-51081-8_107, https://doi.org/10.1007/3-540-51081-8_107
  * [30] Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science, vol. 7358, pp. 781–786. Springer (2012), https://doi.org/10.1007/978-3-642-31424-7_64
  * [31] Hoffmann, J., Shao, Z.: Automatic static cost analysis for parallel programs. In: Vitek, J. (ed.) Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9032, pp. 132–157. Springer (2015), https://doi.org/10.1007/978-3-662-46669-8_6
  * [32] Klemen, M., López-García, P., Gallagher, J.P., Morales, J.F., Hermenegildo, M.V.: A general framework for static cost analysis of parallel logic programs. In: Gabbrielli, M. (ed.) Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Porto, Portugal, October 8-10, 2019, Revised Selected Papers. Lecture Notes in Computer Science, vol. 12042, pp. 19–35. Springer (2019), https://doi.org/10.1007/978-3-030-45260-5_2
  * [33] Kop, C., Nishida, N.: Term rewriting with logical constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8152, pp. 343–358. Springer (2013), https://doi.org/10.1007/978-3-642-40885-4_24
  * [34] Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978), https://doi.org/10.1145/359545.359563
  * [35] Lankford, D.S.: Canonical algebraic simplification in computational logic. Tech. Rep. ATP-25, University of Texas (1975)
  * [36] Moser, G., Schneckenreither, M.: Automated amortised resource analysis for term rewrite systems. Sci. Comput. Program. 185 (2020), https://doi.org/10.1016/j.scico.2019.102306
  * [37] Naaf, M., Frohn, F., Brockschmidt, M., Fuhs, C., Giesl, J.: Complexity analysis for term rewriting by integer transition systems. In: Dixon, C., Finger, M. (eds.) Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10483, pp. 132–150. Springer (2017), https://doi.org/10.1007/978-3-319-66167-4_8
  * [38] Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reason. 51(1), 27–56 (2013), https://doi.org/10.1007/s10817-013-9277-6
  * [39] Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: A cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8562, pp. 367–373. Springer (2014), https://doi.org/10.1007/978-3-319-08587-6_28, https://www.starexec.org/
  * [40] Thiemann, R., Sternagel, C., Giesl, J., Schneider-Kamp, P.: Loops under strategies … continued. In: Kirchner, H., Muñoz, C.A. (eds.) Proceedings International Workshop on Strategies in Rewriting, Proving, and Programming, IWS 2010, Edinburgh, UK, 9th July 2010. EPTCS, vol. 44, pp. 51–65 (2010). https://doi.org/10.4204/EPTCS.44.4, https://doi.org/10.4204/EPTCS.44.4
  * [41] Vuillemin, J.: Correct and optimal implementations of recursion in a simple programming language. J. Comput. Syst. Sci. 9(3), 332–354 (1974), https://doi.org/10.1016/S0022-0000(74)80048-6
  * [42] Wiki: The International Termination Competition (TermComp), http://termination-portal.org/wiki/Termination_Competition
  * [43] Wiki: Termination Problems DataBase (TPDB), http://termination-portal.org/wiki/TPDB
  * [44] Winkler, S., Moser, G.: Runtime complexity analysis of logically constrained rewriting. In: Fernández, M. (ed.) Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7-9, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12561, pp. 37–55. Springer (2020), https://doi.org/10.1007/978-3-030-68446-4_2

##  Appendix 0.A Proofs

###  0.A.1 Proof of Thm. 3.1

To prove Thm. 3.1, we need some further definitions and lemmas.

######  Definition 14 (Argument Normal Form [38], Maximal Parallel Argument
Normal Form)

A term $t$ is an _argument normal form_ iff $t\in\mathcal{V}$ or
$t=f(t_{1},\ldots,t_{n})$ and all $t_{i}$ are in normal form. A term
$t\\!\Downarrow$ is a _maximal parallel argument normal form_ of a term $t$
iff $t\\!\Downarrow$ is an argument normal form such that
$t\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}^{*}_{\mathcal{R},>\varepsilon}}t\\!\Downarrow$ and for all argument
normal forms $t^{\prime}$ with
$t\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}^{*}_{\mathcal{R},>\varepsilon}}t^{\prime}$, we have
$\operatorname{dh}(t^{\prime},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\leq\operatorname{dh}(t\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$. Here
$u\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}^{*}_{\mathcal{R},>\varepsilon}}v$ denotes a rewrite sequence with
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ where all steps are at positions $>\varepsilon$.

The following lemma is adapted to the parallel setting from [38].

######  Lemma 2 (Parallel Derivation Heights of Nested Subterms)

Let $t$ be a term, let $\mathcal{R}$ be a TRS such that all reductions of $t$
with
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}}$
are finite. Then

$\displaystyle\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$ $\displaystyle\leq\max\\{\sum_{1\leq i\leq
k}\operatorname{dh}(t|_{\pi_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\mid\langle\pi_{1},\dots,\pi_{k}\rangle\in\mathit{MSDC}(t)\\}$

If
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ is confluent, then we additionally have:

$\displaystyle\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$ $\displaystyle=\max\\{\sum_{1\leq i\leq
k}\operatorname{dh}(t|_{\pi_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\mid\langle\pi_{1},\dots,\pi_{k}\rangle\in\mathit{MSDC}(t)\\}$

######  Proof (of 2)

By induction on the term size $|t|$. If $|t|=1$, the statement follows
immediately since $t\\!\Downarrow\ =t$. Now consider the case $|t|>1$. Let $n$
be the arity of the root symbol of $t$. In (parallel-)innermost rewriting, a
rewrite step at the root of $t$ requires that the arguments of $t$ have been
rewritten to normal forms. Since rewriting of arguments takes place in
parallel (case (b) of Def. 7 applies), we have

$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\leq\operatorname{dh}(t\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})+\max\\{\quad\operatorname{dh}(t|_{j},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\quad\mid 1\leq j\leq n\\}$

If
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ is confluent, we additionally have equality in the
previous as well as in the next (in)equalities since $t\\!\Downarrow$ is
uniquely determined.

As $|t_{j}|<|t|$, we can apply the induction hypothesis:

$\displaystyle\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$
$\displaystyle\leq\operatorname{dh}(t\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})+\max\\{$ $\displaystyle\max\\{\sum_{1\leq i\leq
m}\operatorname{dh}(t|_{j.\tau_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\mid\langle\tau_{1},\dots,\tau_{m}\rangle\in\mathit{MSDC}(t|_{j})\\}\hskip
8.61108pt\mid 1\leq j\leq n\\}$

Equivalently:

$\displaystyle\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$
$\displaystyle\leq\max\\{\operatorname{dh}(t\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})+\sum_{1\leq i\leq
m}\operatorname{dh}(t|_{j.\tau_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\mid 1\leq j\leq n,$ $\displaystyle\hskip
180.83276pt\langle\tau_{1},\dots,\tau_{m}\rangle\in\mathit{MSDC}(t|_{j})\\}$
$\displaystyle=\max\\{\sum_{1\leq i\leq
k}\operatorname{dh}(t|_{\pi_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\mid\langle\pi_{1},\dots,\pi_{k}\rangle\in\mathit{MSDC}(t)\\}$

For the last equality, consider that the maximal structural dependency chains
$\pi_{1},\dots,\pi_{k}$ of $t$ can have two forms. If the root of $t$ is a
defined symbol, we have $\langle
j.\tau_{1},\dots,j.\tau_{m},\varepsilon\rangle\in\mathit{MSDC}(t)$. Otherwise
$\operatorname{dh}(t\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=0$ and thus $\langle
j.\tau_{1},\dots,j.\tau_{m}\rangle\in\mathit{MSDC}(t)$. ∎

We now can proceed with the proof of Thm. 3.1.

######  Proof (of Thm. 3.1)

As the first case, consider
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=\omega$. Since $t$ is in argument normal form, the
first rewrite step from $t$ must occur at the root. Thus, there are
$\ell_{1}\to r_{1}\in\mathcal{R}$ and a substitution $\sigma_{1}$ such that
$t=\ell_{1}\sigma_{1}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}r_{1}\sigma_{1}$ and
$\operatorname{dh}(r_{1}\sigma_{1},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=\omega$. Hence, there is a minimal subterm
$r_{1}\sigma_{1}|_{\pi_{1}}$ of $r_{1}\sigma_{1}$ such that
$\operatorname{dh}(r_{1}\sigma_{1}|_{\pi_{1}},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=\omega$ and all proper subterms of
$r_{1}\sigma_{1}|_{\pi_{1}}$ terminate wrt
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$. As $\sigma_{1}$ must instantiate all variables with
normal forms, we have $\pi_{1}\in\mathcal{P}\\!\mathit{os}_{d}(r_{1})$, i.e.,
$r_{1}\sigma_{1}|_{\pi_{1}}=r_{1}|_{\pi_{1}}\sigma_{1}$. In the infinite
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$-reduction of $r_{1}|_{\pi_{1}}\sigma_{1}$, all
arguments are again reduced to normal forms first, and we get a term
$t^{\prime}$ with
$\operatorname{dh}(t^{\prime},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=\omega$. Since $t^{\prime}$ is in argument normal
form, the first rewrite step from $t^{\prime}$ must occur at the root. Thus,
there are $\ell_{2}\to r_{2}\in\mathcal{R}$ and a substitution $\sigma_{2}$
such that
$t=\ell_{2}\sigma_{2}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}r_{2}\sigma_{2}$ and
$\operatorname{dh}(r_{2}\sigma_{2},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=\omega$. This argument can be continued _ad
infinitum_ , giving rise to an infinite path in the chain tree

$(\ell^{\sharp}_{1}\to\mathsf{Com}_{n_{1}}(\ldots,r_{1}|^{\sharp}_{\pi_{1}},\ldots)\mid\sigma_{1}),\qquad(\ell^{\sharp}_{2}\to\mathsf{Com}_{n_{2}}(\ldots,r_{2}|^{\sharp}_{\pi_{2}},\ldots)\mid\sigma_{2}),\qquad\dots$

Thus, $\ell^{\sharp}_{1}\sigma_{1}=t^{\sharp}$ has an infinite chain tree, and
$\mathit{Cplx}_{\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle}(t^{\sharp})=\omega$.

Now consider the case that
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\in\mathbb{N}$. We use induction on
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$. If
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=0$, the term $t$ is in normal form wrt
$\mathcal{R}$. Thus, $t^{\sharp}$ is in normal form wrt
$\mathit{PDT}(\mathcal{R})\cup\mathcal{R}$, and
$\mathit{Cplx}_{\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle}(t^{\sharp})=0$.

If
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})>0$, since $t$ is in argument normal form, there are
$\ell\to r\in\mathcal{R}$ and a substitution $\sigma$ such that
$t=\ell\sigma\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}r\sigma=u$ and

$\displaystyle\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$
$\displaystyle=1+\operatorname{dh}(u,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$ (1)

As $\sigma$ must instantiate all variables with normal forms, we have that
$u|_{\pi}=r\sigma|_{\pi}$ is in normal form for all
$\pi\in\mathcal{P}\\!\mathit{os}_{d}(u)\setminus\mathcal{P}\\!\mathit{os}_{d}(r)$.
For these positions $\pi$, $u|_{\pi}\\!\Downarrow=u|_{\pi}$ and
$\operatorname{dh}(u|_{\pi},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=0$. From 2, we get:

$\displaystyle\quad\>\operatorname{dh}(u,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$ $\displaystyle\leq\max\\{\sum_{1\leq i\leq
k}\operatorname{dh}(u|_{\pi_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\mid\langle\pi_{1},\dots,\pi_{k}\rangle\in\mathit{MSDC}(u)\\}$
$\displaystyle=\max\\{\sum_{1\leq i\leq
j}\operatorname{dh}(u|_{\pi_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})+\sum_{j+1\leq i\leq
k}\operatorname{dh}(u|_{\pi_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\mid\langle\pi_{1},\dots,\pi_{k}\rangle\in\mathit{MSDC}(u),$
$\displaystyle\hskip
107.63855pt\pi_{1},\dots,\pi_{j}\in\mathcal{P}\\!\mathit{os}_{d}(u)\setminus\mathcal{P}\\!\mathit{os}_{d}(r),\pi_{j+1},\dots,\pi_{k}\in\mathcal{P}\\!\mathit{os}_{d}(r)\\}$
$\displaystyle=\max\\{\sum_{1\leq i\leq
j}\operatorname{dh}(u|_{\pi_{i}},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\,\>\;+\sum_{j+1\leq i\leq
k}\operatorname{dh}(u|_{\pi_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\mid\langle\pi_{1},\dots,\pi_{k}\rangle\in\mathit{MSDC}(u),$
$\displaystyle\hskip
107.63855pt\pi_{1},\dots,\pi_{j}\in\mathcal{P}\\!\mathit{os}_{d}(u)\setminus\mathcal{P}\\!\mathit{os}_{d}(r),\pi_{j+1},\dots,\pi_{k}\in\mathcal{P}\\!\mathit{os}_{d}(r)\\}$
$\displaystyle=\max\\{\hskip 17.22217pt\sum_{j+1\leq i\leq
k}\operatorname{dh}(u|_{\pi_{i}}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\mid\langle\pi_{1},\dots,\pi_{k}\rangle\in\mathit{MSDC}(u),$
(2) $\displaystyle\hskip
107.63855pt\pi_{1},\dots,\pi_{j}\in\mathcal{P}\\!\mathit{os}_{d}(u)\setminus\mathcal{P}\\!\mathit{os}_{d}(r),\pi_{j+1},\dots,\pi_{k}\in\mathcal{P}\\!\mathit{os}_{d}(r)\\}$

Note that
$\operatorname{dh}(u|_{\pi}\\!\Downarrow,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\leq\operatorname{dh}(u|_{\pi},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})<\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$ holds for all
$\pi\in\mathcal{P}\\!\mathit{os}_{d}(r)$. Thus, with the induction hypothesis,
(1) and (2), we get:

$\displaystyle\quad\>\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$
$\displaystyle=1+\operatorname{dh}(u,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})$ $\displaystyle\leq 1+\max\\{\sum_{j+1\leq i\leq
k}\mathit{Cplx}_{\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle}(u|_{\pi_{i}}\\!\Downarrow^{\sharp})\mid\langle\pi_{1},\dots,\pi_{k}\rangle\in\mathit{MSDC}(u),$
(3) $\displaystyle\hskip
77.49976pt\pi_{1},\dots,\pi_{j}\in\mathcal{P}\\!\mathit{os}_{d}(u)\setminus\mathcal{P}\\!\mathit{os}_{d}(r),\pi_{j+1},\dots,\pi_{k}\in\mathcal{P}\\!\mathit{os}_{d}(r)\\}$

Let $\langle\pi_{1},\ldots,\pi_{k}\rangle$ be an arbitrary maximal structural
dependency chain for $r$. Then there exists a corresponding chain tree for
$t^{\sharp}$ whose root node is
$(\ell^{\sharp}\to\mathsf{Com}_{k}(r_{1}|_{\pi_{1}}\\!\Downarrow^{\sharp},\ldots,r_{k}|_{\pi_{k}}\\!\Downarrow^{\sharp})\mid\sigma)$
and where the children of the root node are maximal chain trees for
$u|_{\pi_{1}}\\!\Downarrow^{\sharp},\ldots,u|_{\pi_{k}}\\!\Downarrow^{\sharp}$.
This follows because for all $1\leq i\leq k$, we have
$r|_{\pi_{i}}\sigma=u|_{\pi_{i}}$ and so
$r|_{\pi_{i}}^{\sharp}\sigma\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}^{*}}u|_{\pi_{i}}\\!\Downarrow^{\sharp}$.
Together with (3), this gives
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})\leq\mathit{Cplx}_{\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle}(t^{\sharp})$,
and for confluent
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}$ we also get
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}})=\mathit{Cplx}_{\langle\mathit{PDT}(\mathcal{R}),\mathit{PDT}(\mathcal{R}),\mathcal{R}\rangle}(t^{\sharp})$.
∎

###  0.A.2 Proof of Thm. 3.3

######  Proof (of Thm. 3.3)

Let $\mathcal{R}$ be a TRS such that for all rules $\ell\to r\in\mathcal{R}$,
$|\mathit{MSDC}(r)|=1$.

We prove part (a). By construction of $\mathit{PDT}$, for $\ell\to
r\in\mathcal{R}$ we get from $|\mathit{MSDC}(r)|=1$ that
$|\mathit{PDT}(\ell\to r)|=1$. We show that for all rules $\ell\to
r\in\mathcal{R}$, $\mathit{PDT}(\ell\to r)=\\{\mathit{DT}(\ell\to r)\\}$ and
fix $\ell\to r\in\mathcal{R}$. $|\mathit{MSDC}(r)|=1$ implies that
$\mathcal{P}\\!\mathit{os}_{d}(r)$ is ordered by the prefix order $>$ on
positions. Thus, by using an arbitrary total extension of $>$ as the total
order $\gtrdot$ used as an ingredient for the construction of
$\mathit{DT}(\ell\to r)$, we obtain the result for part (a).

We now prove part (b). Let $t_{0}$ be a basic term for $\mathcal{R}$ with a
rewrite sequence
$t_{0}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}t_{1}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}t_{2}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}\dots$. We show by induction over $i$ that for all
$t_{i}$, $t_{i}$ contains at most one innermost redex.

For the base case, consider that the basic term $t_{0}$ contains only a single
occurrence of a defined symbol, at the root. Thus, if $t_{0}$ is a redex, it
is also the unique innermost redex in $t_{0}$.

For the induction step, assume that $t_{i}$ has at most one innermost redex.
If $t_{i}$ has no redex, it is a normal form, and we are done. Otherwise,
$t_{i}$ has exactly one innermost redex at position $\tau$, and in the
parallel-innermost rewrite step
$t_{i}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}t_{i+1}$ a rule $\ell\to r$ with matcher $\sigma$
replaces $t_{i}|_{\tau}=\sigma(\ell)$ by $\sigma(r)$. The premise
$|\mathit{MSDC}(r)|=1$ implies that there is exactly one (empty or non-empty)
maximal structural dependency chain
$\langle\pi_{1},\ldots,\pi_{k}\rangle\in\mathit{MSDC}(r)$.

Since the rewrite step
$t_{i}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\>\>\mathsf{i}\>$}}}{{\smash{\longrightarrow{\parallel}\hskip
8.0pt}}}}_{\mathcal{R}}}t_{i+1}$ uses (parallel-)_innermost_ rewriting,
$\sigma(x)$ is in normal form for all variables $x$. Thus, potential redexes
in term $t_{i+1}$ can only be at positions $\tau\pi_{1},\ldots,\tau\pi_{k}$.
As $\langle\pi_{1},\ldots,\pi_{k}\rangle$ is a structural dependency chain, we
have $\pi_{1}>\dots>\pi_{k}$, which implies $\tau\pi_{1}>\dots>\tau\pi_{k}$.
Thus, the term $t_{i+1}$ has at most one innermost redex $\tau\pi_{i}$. This
concludes part (b).

Part (c) follows directly from part (b) and the definitions of
$\mathrm{pirc}_{\mathcal{R}}(n)$ and $\mathrm{irc}_{\mathcal{R}}(n)$.

###  0.A.3 Proof of Thm. 4.1

For the proof of Thm. 4.1, we need the following standard definition of a
_context_.

######  Definition 15 (Context)

A _context_ $C[]$ is a term that contains exactly one occurrence of a special
symbol $\Box$. We write $C[t]$ for the term obtained from replacing $\Box$ by
the term $t$.

######  Proof (of Thm. 4.1)

We first show part (a) of the statement. For a DT Problem
$\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle$ and a term
$t^{\sharp}\in\mathcal{T}^{\sharp}$, consider an arbitrary chain tree $T$. We
will show that if $|T|_{\mathcal{S}}=n$, then also
$\operatorname{dh}(t^{\sharp},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})\geq
n$. We consider two cases. First, $n=\omega$. Since $T$ is finitely branching,
there must be an infinite path with infinitely many nodes
$(u^{\sharp}_{1}\to\mathsf{Com}_{n_{1}}(\ldots,v_{1}^{\sharp},\ldots)\mid\sigma_{1}),(u^{\sharp}_{2}\to\mathsf{Com}_{n_{2}}(\ldots,v_{2}^{\sharp},\ldots)\mid\sigma_{2}),\dots$
such that
$u^{\sharp}_{1}\to\mathsf{Com}_{n_{1}}(\ldots,v_{1}^{\sharp},\ldots),u^{\sharp}_{2}\to\mathsf{Com}_{n_{2}}(\ldots,v_{2}^{\sharp},\ldots),\ldots\in\mathcal{D}$,
for infinitely many $i_{1}<i_{2}<i_{3}<\dots$, we also have
$u^{\sharp}_{i}\to\mathsf{Com}_{n_{i}}(\ldots,t_{i}^{\sharp},\ldots)\in\mathcal{S}$,
and for all $i$, we have
$v^{\sharp}_{i}\sigma_{i}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}^{*}}u^{\sharp}_{i+1}\sigma_{i+1}$.
Then we also have a corresponding infinite rewrite sequence

$\displaystyle t^{\sharp}=u^{\sharp}_{1}\sigma_{1}$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}^{*}}C_{1}[u^{\sharp}_{i_{1}}\sigma_{i_{1}}]\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}}}C_{1}[\mathsf{Com}_{n_{i_{1}}}(\ldots,v^{\sharp}_{i_{1}},\ldots)\sigma_{i_{1}}]$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{(\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R}}^{*}}\quad\;\;C_{2}[u^{\sharp}_{i_{2}}\sigma_{i_{2}}]\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}}}C_{2}[\mathsf{Com}_{n_{i_{2}}}(\ldots,v^{\sharp}_{i_{2}},\ldots)\sigma_{i_{2}}]$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{(\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R}}^{*}}\quad\;\;\dots$

for some contexts $C_{1},C_{2},\ldots$ (which result from rewrite steps with
rules from $\mathcal{D}$).

Now consider the case $n\in\mathbb{N}$. We use induction. For $n=0$, the
statement trivially holds. For the induction step, let $n>0$.

The (potentially infinite) chain tree $T$ has $m$ subtrees $T^{\prime}_{i}$
with roots
$(u^{\sharp}_{i}\to\mathsf{Com}_{q_{i}}(v^{\sharp}_{i,1},\ldots,v^{\sharp}_{i,q_{i}})\mid\sigma_{i})$
such that
$u^{\sharp}_{i}\to\mathsf{Com}_{q_{i}}(v^{\sharp}_{i,1},\ldots,v^{\sharp}_{i,q_{i}})\in\mathcal{S}$
and the path in the chain tree from the root to
$(u^{\sharp}_{i}\to\mathsf{Com}_{q_{i}}(v^{\sharp}_{i,1},\ldots,v^{\sharp}_{i,q_{i}})\mid\sigma_{i})$
has no outgoing edges from a node with a DT in $\mathcal{S}$.

We show two separate statements in the induction step:

For each $T_{i}$, the term $u^{\sharp}_{i}\sigma_{i}$ has
$\operatorname{dh}(u^{\sharp}_{i}\sigma_{i},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})\geq|T^{\prime}_{i}|_{\mathcal{S}}$.
(4) $\displaystyle\begin{split}\text{There are contexts $C_{1},\ldots,C_{m}$
such that\qquad}\\\\[-3.0pt]
t^{\sharp}\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}^{*}}\mathsf{Com}_{m}(C_{1}[u_{1}^{\sharp}\sigma_{1}],\ldots,C_{m}[u_{m}^{\sharp}\sigma_{m}]).\end{split}$
(5)

Statements (4) and (5) together imply
$\operatorname{dh}(t^{\sharp},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})\geq|T^{\prime}_{1}|_{\mathcal{S}}+\dots+|T^{\prime}_{m}|_{\mathcal{S}}=n$.

On (4): Let $i\in\\{1,\ldots,m\\}$ be arbitrary and fixed, let $u=u_{i}$, let
$\sigma=\sigma_{i}$, let $T^{\prime}=T^{\prime}_{i}$ (to ease notation). So
the root of $T^{\prime}$ is
$(u^{\sharp}\to\mathsf{Com}_{q}(v^{\sharp}_{1},\ldots,v^{\sharp}_{q})\mid\sigma)$.
Let this node have children
$N_{1}=(w^{\sharp}_{1}\to\mathsf{Com}_{r_{1}}(\ldots)\mid\mu_{1})$, $\ldots$,
$N_{q}=(w^{\sharp}_{q}\to\mathsf{Com}_{r_{q}}(\ldots)\mid\mu_{q})$. For the
corresponding trees $T^{\prime\prime}_{j}$ with $N_{j}$ at the root, we have
$|T^{\prime\prime}_{j}|_{\mathcal{S}}<|T^{\prime}|_{\mathcal{S}}\leq n$ by
construction, so the induction hypothesis is applicable to the terms
$w^{\sharp}_{j}\mu_{j}$, and we get
$\operatorname{dh}(w^{\sharp}_{j}\mu_{j},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})\geq|T^{\prime\prime}_{j}|_{\mathcal{S}}$
for all $1\leq j\leq q$. We construct a rewrite sequence with
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}}$
using at least
$1+|T^{\prime\prime}_{1}|_{\mathcal{S}}+\dots+|T^{\prime\prime}_{q}|_{\mathcal{S}}=|T^{\prime}|_{\mathcal{S}}$
steps with a rule from $\mathcal{S}$ as follows:

$\displaystyle u^{\sharp}\sigma$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}}}\mathsf{Com}_{q}(v^{\sharp}_{1}\sigma,\ldots,v^{\sharp}_{q}\sigma)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}^{*}}\mathsf{Com}_{q}(w^{\sharp}_{1}\mu_{1},\ldots,v^{\sharp}_{q}\sigma)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}^{*}}\dots$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{R}}^{*}}\mathsf{Com}_{q}(w^{\sharp}_{1}\mu_{1},\ldots,w^{\sharp}_{q}\mu_{q})$

With this rewrite sequence, we obtain (4) using the induction hypothesis:

$\displaystyle\quad\;\operatorname{dh}(u^{\sharp}\sigma,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})$
$\displaystyle\geq
1+\operatorname{dh}(w^{\sharp}_{1}\mu_{1},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})+\dots+\operatorname{dh}(w^{\sharp}_{q}\mu_{q},\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})$
$\displaystyle\geq
1+|T^{\prime\prime}_{1}|_{\mathcal{S}}+\dots+|T^{\prime\prime}_{q}|_{\mathcal{S}}$
$\displaystyle=|T^{\prime}|_{\mathcal{S}}$

On (5): Let the root of $T$ be
$(\ell^{\sharp}\to\mathsf{Com}_{p}(r^{\sharp}_{1},\ldots,r^{\sharp}_{p})\mid\nu)$.
With a construction similar to the one used in the case $n=\omega$, we get:

$\displaystyle t^{\sharp}=\ell^{\sharp}\nu$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{D}}}\qquad\;\;\;\mathsf{Com}_{p}(r^{\sharp}_{1}\nu,\ldots,r^{\sharp}_{p}\nu)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{(\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R}}^{*}}\mathsf{Com}_{p}(C_{1}[u_{1}^{\sharp}\sigma_{1}],\ldots,r^{\sharp}_{p}\nu)$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{(\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R}}^{*}}\dots$
$\displaystyle\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{(\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R}}^{*}}\mathsf{Com}_{p}(C_{1}[u_{1}^{\sharp}\sigma_{1}],\ldots,C_{m}[u_{m}^{\sharp}\sigma_{m}])$

for some contexts $C_{1},\ldots,C_{m}$ (which result from rewrite steps with
rules from $\mathcal{D}$). Note that here it suffices to reduce only in those
subterms with a symbol $f^{\sharp}$ at their root that are on a path to one of
the $C_{i}[u_{i}^{\sharp}\sigma_{i}]$, and depending on the tree structure,
each $r^{\sharp}_{j}\nu$ may yield 0 or more of these $m$ terms (note that $p$
and $m$ are not necessarily equal).

This concludes the induction step and hence the overall proof of part (a).

Part (b) follows from part (a), as shown in the following:

$\displaystyle\mathrm{irc}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(n)$
$\displaystyle=\sup\\{\mathit{Cplx}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(t^{\sharp})\mid
t\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}},\lvert t\rvert\leq n\\}$ by
Def. 5
$\displaystyle\leq\sup\\{\operatorname{dh}(t^{\sharp},{\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}}})\mid
t\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}},\lvert t\rvert\leq n\\}$ by
part (a)
$\displaystyle\leq\sup\\{\operatorname{dh}(s,{\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}}})\mid
s\in\mathcal{T}_{\mathrm{basic}}^{\mathcal{R}\cup\mathcal{D}},\lvert
s\rvert\leq n\\}$
$\displaystyle=\mathrm{irc}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}(n)$

∎

###  0.A.4 Proof of Thm. 4.2

######  Proof (of Thm. 4.2)

We first consider the proof for part (a).

We use the following (many-sorted first-order monomorphic) type assignment
$\Theta$ with two sorts $\alpha$ and $\beta$, where the arities of the symbols
are respected (note that here all arguments of a given symbol have the same
type):

$\displaystyle\Theta(f)$
$\displaystyle=\alpha\times\dots\times\alpha\to\alpha\text{ for $f$ in
$\Sigma^{\mathcal{R}}$}$ $\displaystyle\Theta(f^{\sharp})$
$\displaystyle=\alpha\times\dots\times\alpha\to\beta\text{ for $f^{\sharp}$ a
sharp symbol}$ $\displaystyle\Theta(\mathsf{Com}_{k})$
$\displaystyle=\beta\times\dots\times\beta\to\beta$

With this type assignment, for all rules $\ell\to
r\in\mathcal{D}\cup\mathcal{R}$, $\ell$ and $r$ are well typed and have the
same type: if $\ell\to r\in\mathcal{R}$, then all occurring symbols have the
same result type $\alpha$, which carries over to $\ell$ and $r$. And if
$\ell\to r\in\mathcal{D}$, then $\ell$ and $r$ have type $\beta$. To see that
$\ell$ and $r$ are well typed, consider that every term $\ell$ has the shape
$f^{\sharp}(s_{1},\ldots,s_{n})$, where $f^{\sharp}$ has result type $\beta$
and expects all arguments to have type $\alpha$, while all $s_{i}$ contain
only subterms of type $\alpha$. Similarly, $r$ has the shape
$\mathsf{Com}_{k}(f^{\sharp}_{1}(t_{1,1},\ldots,t_{1,n_{1}}),\ldots,f^{\sharp}_{k}(t_{k,1},\ldots,t_{k,n_{k}}))$.
$\mathsf{Com}_{k}$ has result type $\beta$ and expects all arguments to have
type $\beta$. This is the case since all $f_{i}^{\sharp}$ have result type
$\beta$. An all $f_{i}^{\sharp}$, which are right below the root, expect their
arguments $t_{i,j}$ to have result type $\alpha$. This is the case by
construction.

In the following, we consider basic terms that are well typed according to
$\Theta$ as start terms. For our relative TRS
$\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})$, we have the
following two kinds of well-typed basic terms that we need to consider:

Case 1:

$t=f(t_{1},\ldots,t_{n})$ with $f\in\Sigma_{d}$ and
$t_{1},\ldots,t_{n}\in\mathcal{T}(\Sigma_{c},\mathcal{V})$. This term and all
its subterms are of type $\alpha$. Thus, this term can be rewritten by rules
from $\mathcal{R}$, but not by rules from $\mathcal{D}$ (and $\mathcal{S}$),
which all have type $\beta$. As rewriting preserves the type of terms, $t$ is
a normal form wrt the relations
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\Theta(\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R}))}}$
and
$\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}}$,
and
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})=0$.
Since
$\mathit{Cplx}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(s)\geq 0$
regardless of $s$, the claim follows for this case.

Case 2:

$t=f^{\sharp}(t_{1},\ldots,t_{n})$ with $f\in\Sigma_{d}$ and
$t_{1},\ldots,t_{n}\in\mathcal{T}(\Sigma_{c},\mathcal{V})$. If $t$ is a normal
form, there is no tree, and
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})=0=\mathit{Cplx}_{\langle\mathcal{D},\mathcal{S},\mathcal{R}\rangle}(t)$.

Otherwise, we can convert any
${\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}\cup((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}}}={\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{D}\cup\mathcal{R}}}}$
rewrite sequence to a $(\mathcal{D},\mathcal{R})$-chain tree $T$ for $t$ such
that
$\operatorname{dh}(t,\mathrel{\smash{\stackrel{{\scriptstyle\raisebox{2.0pt}{\scriptsize$\mathsf{i}\>$}}}{{\smash{\rightarrow}}}}_{\mathcal{S}/((\mathcal{D}\setminus\mathcal{S})\cup\mathcal{R})}})=|T|_{\mathcal{S}}$,
including any rewrite sequence that witnesses