# On Basic Feasible Functionals and the Interpretation Method*

Patrick Baillot<fnref n="1" />, Ugo Dal Lago<fnref n="2" />, Cynthia Kop<fnref n="3" />, and Deivid Vale<fnref n="4" />

**Abstract.** The class of basic feasible functionals (BFF) is the analog of FP (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. BFF can be defined through Oracle Turing machines with running time bounded by second-order polynomials. On the other hand, higher-order term rewriting provides an elegant formalism for expressing higher-order computation. We address the problem of characterizing BFF by higher-order term rewriting. Various kinds of interpretations for *first-order* term rewriting have been introduced in the literature for proving termination and characterizing (first-order) complexity classes. In this paper, we consider a recently introduced notion of cost-size interpretations for higher-order term rewriting and see definitions as ways of computing functionals. We then prove that the class of functionals represented by higher-order terms admitting a certain kind of cost-size interpretation is exactly BFF.

**Keywords:** Basic Feasible Functions · Higher-Order Term Rewriting · Tuple Interpretations · Computational Complexity

## 1 Introduction

Computational complexity classes, and in particular those relating to polynomial time and space [19,10] capture the concept of a feasible problem, and as such have been scrutinized with great care by the scientific community in the last fifty years. The fact that even apparently simple problems, such as nontrivial separation between those classes, remain open today has highlighted the need for a comprehensive study aimed at investigating the deep nature of computational complexity. The so-called implicit computational complexity [7,29,32,12,4] fits into this picture, and is concerned with characterizations of complexity classes

<footnote n="1">¹ Univ. Lille, CNRS, Inria, Centrale Lille, UMR 9189 CRISTAL, F-59000 Lille, France, patrick.baillot@univ-lille.fr</footnote>

<footnote n="2">² University of Bologna & INRIA Sophia Antipolis, ugo.dallago@unibo.it</footnote>

<footnote n="3">³ Radboud University Nijmegen, c.kop@cs.ru.nl</footnote>

<footnote n="4">⁴ Radboud University Nijmegen, deividvale@cs.ru.nl</footnote>

<footnote>* This work is supported by the NWO TOP project "Implicit Complexity through Higher-Order Rewriting", NWO 612.001.803/7571, the NWO VIDI project "Constrained Higher-Order Rewriting and Program Equivalence", NWO VI.Vidi.193.075, and the ERC CoG "Differential Program Semantics", GA 818616.</footnote>
based on tools from mathematical logic and the theory of programming lan-
guages.

One of the areas involved in this investigation is certainly that of term rewriting [33], which has proved useful as a tool for the characterization of complexity classes. In particular, the class FP (i.e., of polytime first-order functions) has been characterized through variations of techniques originally introduced for termination, e.g., the interpretation method [30,28], path orders [14], or dependency pairs [15]. Some examples of such characterizations can be found in [6,8,9,1,3].

After the introduction of FP, it became clear that the study of computational
complexity also applies to *higher-order functionals*, which are functions that
take not only data but also other functions as inputs. The pioneering work of
Constable [11], Mehlhorn [31], and Kapron and Cook [21] laid the foundations of
the so-called higher-order complexity, which remains a prolific research area to
this day. Some motivations for this line of work can be found e.g. in computable
analysis [23], NP search problems [5], and programming language theory [13].

There have been several proposals for a class of type-two functionals that correctly generalizes FP. However, the most widely accepted one is the class BFF of basic feasible functionals. This class can be characterized based on function algebras, similar to Cobham-style, but it can also be described using Oracle Turing machines. The class BFF was then the object of study by the research community, which over the years has introduced a variety of characterizations, e.g., in terms of programming languages with restricted recursion schemes [20,13], typed imperative languages [16,17], and restricted forms of iteration in OTMs [22]. An investigation of higher-order complexity classes employing the higher-order interpretation method (in the context of a pure higher-order functional language) was also proposed in [18]. However, this paper does not provide a characterization of the standard BFF class. Instead, it characterizes a newly proposed class SFF₂ (Safe Feasible Functionals) which is defined as the restriction of BFF to argument functions in FP (see Sect. 4.2 and the conclusion in [18]).

The studies cited above present structurally complex programming languages
and logical systems, precisely due to the presence of higher-order functions. It
is not currently known whether it is possible to give a characterization of BFF
in terms of mainstream concepts of rewriting theory, although the latter has
long been known to provide tools for the modeling and analysis of functional
programs with higher-order functions [24].

This paper goes precisely in that direction by showing that the interpretation
method in the form studied by Kop and Vale [26,25] provides the right tools to
characterize BFF. More precisely, we consider a class of higher-order rewriting
systems admitting cost-size tuple interpretations (with some mild upper-bound
conditions on their cost and size components) and show that this class contains
exactly the functionals in BFF. Such a characterization could not have been
obtained employing classical integer interpretations as e.g. in [8] because BFF
crucially relies on some conditions both on size and on time. This is the main
contribution of our paper, formally stated in Theorem 2.
We believe that a benefit of this characterization is that it opens the way to effectively handling programs or executable specifications implementing BFF functions, in full generality. For instance, we expect that such a characterization could be integrated into rewriting-based tools for complexity analysis of term rewriting systems such as e.g. [2].

Our result is proved in two parts. We first prove that if any term rewriting system in this class computes a higher-order functional, then this functional has to be in BFF (*soundness*). Conversely, we prove that all functionals in BFF are computed by this class of rewriting systems (*completeness*). We argue that the key ingredient towards achieving this characterization is the ability to split the dual notions of cost and size given by the usage of tuple interpretations.

# 2 Preliminaries

## 2.1 Higher-Order Rewriting

We roughly follow the definition of *simply-typed term rewriting system* [27] (*STRS*): terms are applicative, and we limit our interest to *second-order STRSs* where all rules have base type. Reductions follow an innermost evaluation strategy.

Let $\mathbb{B}$ be a nonempty set whose elements are called *base types* and range over $\iota, \kappa, \nu$. The set $\mathbb{T}(\mathbb{B})$ of *simple types* over $\mathbb{B}$ is defined by the grammar $\mathbb{T}(\mathbb{B}) := \mathbb{B} \mid \mathbb{T}(\mathbb{B}) \Rightarrow \mathbb{T}(\mathbb{B})$. Types from $\mathbb{T}(\mathbb{B})$ are ranged over by $\sigma, \tau, \rho$. The $\Rightarrow$ type constructor is right-associative, so we write $\sigma \Rightarrow \tau \Rightarrow \rho$ for $(\sigma \Rightarrow (\tau \Rightarrow \rho))$. Hence, every type $\sigma$ can be written as $\sigma_1 \Rightarrow \dots \Rightarrow \sigma_n \Rightarrow \iota$. We may write such types as $\vec{\sigma} \Rightarrow \iota$. The *order* of a type is: $\mathrm{ord}(\iota) = 0$ for $\iota \in \mathbb{B}$ and $\mathrm{ord}(\sigma \Rightarrow \tau) = \max(1 + \mathrm{ord}(\sigma), \mathrm{ord}(\tau))$. A *signature* $\mathbb{F}$ is a triple $(\mathbb{B}, \Sigma, \mathrm{typeOf})$ where $\mathbb{B}$ is a set of base types, $\Sigma$ is a nonempty set of symbols, and $\mathrm{typeOf} : \Sigma \to \mathbb{T}(\mathbb{B})$. For each type $\sigma$, we assume given a set $X_\sigma$ of countably many variables and assume that $X_\sigma \cap X_\tau = \emptyset$ if $\sigma \neq \tau$. We let $\mathbb{X}$ denote $\cup_\sigma X_\sigma$ and assume that $\Sigma \cap \mathbb{X} = \emptyset$.

The set $\mathbb{T}(\mathbb{F}, \mathbb{X})$ — of terms built from $\mathbb{F}$ and $\mathbb{X}$ — collects those expressions $s$ for which a judgment $s : \sigma$ can be deduced using the following rules:

$$ (\text{ax}) \quad \frac{x \in \mathbb{X}_{\sigma}}{x : \sigma} \quad (\text{f-ax}) \quad \frac{f \in \Sigma \quad \text{typeOf}(f) = \sigma}{f : \sigma} \quad (\text{app}) \quad \frac{s : \sigma \Rightarrow \tau \quad t : \sigma}{(st) : \tau} $$

As usual, application of terms is left-associative, so we write $stu$ for $((st)u)$. Let $\mathit{vars}(s)$ be the set of variables occurring in $s$. A term $s$ is *ground* if $\mathit{vars}(s) = \emptyset$. The *head symbol* of a term $f s_1 \dots s_n$ is $f$. We say $t$ is a *subterm* of $s$ (written $s \supseteq t$) if either (a) $s = t$, or (b) $s = s' s''$ and $s' \supseteq t$ or $s'' \supseteq t$. It is a *proper subterm* of $s$ if $s \neq t$. For a term $s$, $\mathit{pos}(s)$ is the set of *positions* in $s$: $\mathit{pos}(x) = \mathit{pos}(f) = \{\#\}$ and $\mathit{pos}(st) = \{\#\} \cup \{1 \cdot u \mid u \in \mathit{pos}(s)\} \cup \{2 \cdot u \mid u \in \mathit{pos}(t)\}$. For $p \in \mathit{pos}(s)$, the subterm $s|_p$ at position $p$ is given by: $s|_\# = s$ and $(s_1 s_2)|_{i \cdot p} = s_i|_p$.

In this paper, we require that for all $f \in \Sigma$, $\mathrm{ord}(\mathrm{typeOf}(f)) \le 2$, so w.l.o.g., $f: (\vec{l}_1 \Rightarrow \kappa_1) \Rightarrow \dots \Rightarrow (\vec{l}_k \Rightarrow \kappa_k) \Rightarrow \nu_1 \Rightarrow \dots \Rightarrow \nu_l \Rightarrow \iota$. Hence, in a fully applied term $f s_1 \dots s_k t_1 \dots t_l$ we say the $s_i$ are the arguments of type-1 and the $t_j$ are
the arguments of type-0 for f. A substitution $\gamma$ is a type-preserving map from variables to terms such that $\{x \in \mathbb{X} | \gamma(x) \neq x\}$ is finite. We extend $\gamma$ to terms as usual: $x\gamma = \gamma(x)$, $f\gamma = f$, and $(st)\gamma = (s\gamma)(t\gamma)$. A context $C$ is a term with a single occurrence of a variable $\square$; the term $C[s]$ is obtained by replacing $\square$ by $s$.

A rewrite rule $\ell \to r$ is a pair of terms of the same type such that $\ell = f \ell_1 \cdots \ell_m$ and $\mathbf{vars}(\ell) \supseteq \mathbf{vars}(r)$. It is left-linear if no variable occurs more than once in $\ell$. A simply-typed term rewriting system $(\mathbb{F}, \mathcal{R})$ is a set of rewrite rules $\mathcal{R}$ over $\mathbb{T}(\mathbb{F}, \mathbb{X})$. In this paper, we require that all rules have base type. An STRS is innermost orthogonal if all rules are left-linear, and for any two distinct rules $\ell_1 \to r_1$, $\ell_2 \to r_2$, there are no substitutions $\gamma, \delta$ such that $\ell_1\gamma = \ell_2\delta$. A reducible expression (redex) is a term of the form $\ell\gamma$ for a rule $\ell \to r$ and substitution $\gamma$. The innermost rewrite relation induced by $\mathcal{R}$ is defined as follows:

* $\ell\gamma \to_R r\gamma$, if $\ell \to r \in \mathcal{R}$ and $\ell\gamma$ has no proper subterm that is a redex;

* $st \to_R ut$, if $s \to_R u$ and $st \to_R su$, if $t \to_R u$.

We write $\to_R^+$ for the transitive closure of $\to_R$. An STRS $\mathcal{R}$ is innermost terminating if no infinite rewrite sequence $s \to_R t \to_R \dots$ exists. It is innermost confluent if $s \to_R^+$ $t$ and $s \to_R^+$ $u$ implies that some $v$ exists with $t \to_R^+$ $v$ and $u \to_R^+$ $v$. It is well-known that innermost orthogonality implies innermost confluence. In this paper, we will typically drop the “innermost” adjective and simply refer to terminating/orthogonal/confluent STRSs.

**Example 1.** Let $\mathbb{B} = \{\text{nat}\}$ and $0: \text{nat}, s: \text{nat} \Rightarrow \text{nat}, \text{add}, \text{mult}: \text{nat} \Rightarrow \text{nat} \Rightarrow \text{nat}$, and $\text{funcProd}: (\text{nat} \Rightarrow \text{nat}) \Rightarrow \text{nat} \Rightarrow \text{nat} \Rightarrow \text{nat}$. We then let $\mathcal{R}$ be given by:

$$ \begin{array}{l@{\qquad}l} \text{add } 0 & y \to y & \text{add } (s x) y \to s (\text{add } xy) \\ \text{mult } 0 & y \to 0 & \text{mult } (s x) y \to \text{add } y (\text{mult } xy) \\ \text{funcProd } F & 0 y \to y & \text{funcProd } F (s x) y \to \text{funcProd } F x (\text{mult } y (F x)) \end{array} $$

Hereafter, we write ⌜n⌝ for the term $s(s(\dots 0\dots))$ with n ss.

## 2.2 Cost-Size Interpretations

For sets $A$ and $B$, we write $A \to B$ for the set of functions from $A$ to $B$. A quasi-ordered set $(A, \sqsupset)$ consists of a nonempty set $A$ and a reflexive and transitive relation $\sqsupset$ on $A$. For quasi-ordered sets $(A_1, \sqsupset_1)$ and $(A_2, \sqsupset_2)$, we write $A_1 \implies A_2$ for the set of functions $f \in A_1 \to A_2$ such that $f(x) \sqsupset_2 f(y)$ whenever $x \sqsupset_1 y$, i.e., $A_1 \implies A_2$ is the space of functions that preserve quasi-ordering.

For every $\iota \in \mathbb{B}$, let a quasi-ordered set $(S_\iota, \sqsupset_\iota)$ be given. We extend this to $\mathbb{T}(\mathbb{B})$ by defining $S_{\sigma \to \tau} = (S_\sigma \implies S_\tau, \sqsupset_{\sigma \to \tau})$ where $f \sqsupset_{\sigma \to \tau} g$ iff $f(x) \sqsupset_\tau f(x)$ for any $x \in S_\sigma$. Given a function $\mathcal{J}^s$ mapping $f \in \Sigma$ to some $\mathcal{J}_f^s \in S_{\text{type0f}(f)}$ and a valuation $\alpha$ mapping $x \in \mathbb{X}_\sigma$ to $S_\sigma$, we can map each term $s: \sigma$ to an element of $S_\sigma$ naturally as follows: (a) $\llbracket x \rrbracket_\alpha^s = \alpha(x)$; (b) $\llbracket f \rrbracket_\alpha^s = \mathcal{J}_f^s$; (c) $\llbracket st \rrbracket_\alpha^s = \llbracket s \rrbracket_\alpha^s(\llbracket t \rrbracket_\alpha^s).$

For every type $\sigma$ with $\text{ord}(\sigma) \le 2$, we define $C_\sigma$ as follows: (a) $C_\kappa = \mathbb{N}$ for $\kappa \in \mathbb{B}$; (b) $C_{\iota \to \tau} = S_\iota \implies C_\tau$ for $\iota \in \mathbb{B}$; and (c) $C_{\sigma \to \tau} = C_\sigma \implies S_\sigma \implies C_\tau$ if $\text{ord}(\sigma) = 1$. We want to interpret terms $s: \sigma$ where both $\sigma$ and all variables
occurring in $s$ are of type order either 0 or 1, as is the case for the left- and
right-hand side of rules. Thus, we let $\mathcal{J}^c$ be a function mapping $f \in \Sigma$ to some
$\mathcal{J}_f^c \in \mathcal{C}_{\text{type0f}(f)}$ and assume given, for each type $\sigma$, valuations $\alpha: X_\sigma \to S_\sigma$ and
$\zeta: X_\sigma \to C_\sigma$. We then define:

$$
\llbracket x s_1 \cdots s_n \rrbracket_{\alpha, \zeta}^{c} = \zeta(x)(\llbracket s_1 \rrbracket_{\alpha}^{s}, \ldots, \llbracket s_n \rrbracket_{\alpha}^{s}) \\
\llbracket f s_1 \cdots s_k t_1 \cdots t_n \rrbracket_{\alpha, \zeta}^{c} = \mathcal{J}_f^c(\llbracket s_1 \rrbracket_{\alpha, \zeta}^{c}, \llbracket s_1 \rrbracket_{\alpha}^{s}, \ldots, \llbracket s_k \rrbracket_{\alpha, \zeta}^{c}, \llbracket s_k \rrbracket_{\alpha}^{s}, \llbracket t_1 \rrbracket_{\alpha}^{s}, \ldots, \llbracket t_n \rrbracket_{\alpha}^{s})
$$

We let $\text{cost}(s)_{\alpha, \zeta} = \sum \{[t]_{\alpha, \zeta}^c \mid s \supseteq t \text{ and } t \text{ is a non-variable term of base type}\}$. This is all well-defined under our assumptions that all variables have a type of order 0 or 1, and $f: (\vec{i}_1 \Rightarrow \kappa_1) \Rightarrow \dots \Rightarrow (\vec{i}_k \Rightarrow \kappa_k) \Rightarrow \nu_1 \Rightarrow \dots \Rightarrow \nu_l \Rightarrow l$. We also define $\text{cost}'(s)_{\alpha, \zeta} = \sum \{[t]_{\alpha, \zeta}^c \mid s \supseteq t \text{ and } t \notin X \text{ is of base type not in normal form}\}$.

A cost–size interpretation $\mathcal{F}$ for a second order signature $\mathbb{F} = (\mathbb{B}, \Sigma, \text{type0f})$ is a choice of a quasi-ordered set $\mathcal{S}_\iota$, for each $\iota \in \mathbb{B}$, along with cost- and size-interpretations $\mathcal{J}^c$ and $\mathcal{J}^s$ defined as above. Let $(\mathbb{F}, \mathcal{R})$ be an STRS over $\mathbb{F}$. We say $(\mathbb{F}, \mathcal{R})$ is *compatible* with a cost–size interpretation if for any valuations $\alpha$ and $\zeta$, we have (a) $[\ell]_{\alpha, \zeta}^c > \text{cost}(r)_{\alpha, \zeta}$ and (b) $[\ell]_{\alpha}^s \supseteq [r]_{\alpha}^s$, for all rules $\ell \to r$ in $\mathcal{R}$. In this case we say such cost–size interpretation *orients* all rules in $\mathcal{R}$.

**Theorem 1 (Innermost Compatibility).** Suppose $\mathcal{R}$ is an STRS compatible with a cost–size interpretation $\mathcal{F}$, then for any valuations $\alpha$ and $\zeta$ we have $\text{cost}'(s)_{\alpha, \zeta} > \text{cost}'(t)_{\alpha, \zeta}$ and $[s]_{\alpha}^{s} \supseteq [t]_{\alpha}^{s}$ whenever $s \to_{\mathcal{R}} t$.

From compatibility, we have that if $s_0 \to_{\mathcal{R}} \dots \to_{\mathcal{R}} s_n$, then $n \le \text{cost}'(s_0)$.
Hence, $\text{cost}'(s)$ bounds the *derivation height* of $s$. This follows from [25, Corol-
lary 34], although we significantly simplified the presentation: the limitation to
second-order fully applied rules and the lack of abstraction terms allow us to
avoid many of the complexities in [25]. We also adapted it to *innermost* rather
than *call-by-value* evaluation. A correctness proof of this version is supplied in
the Appendix A. Since $\alpha$ and $\zeta$ are universally quantified, we typically omit
them, and just write $x$ instead of $\alpha(x)$ and $F^c$ instead of $\zeta(F)$.

Example 2. We let $S_{\text{nat}} = (\mathbb{N}, \ge)$ and assign $\mathcal{J}_0^s = 0$ and $\mathcal{J}_s^s = \lambda x.x + 1$, as well as $\mathcal{J}_0^c = 0$ and $\mathcal{J}_s^c = \lambda x.0$. This gives us $[\upharpoonright n \upharpoonright]^s = n$ for all $n \in \mathbb{N}$, and $[\upharpoonright n \upharpoonright]^c = \text{cost}(n) = 0$. Now, we let $\mathcal{J}_{\text{add}}^s = \lambda xy.x + y$ and $\mathcal{J}_{\text{mult}}^s = \lambda xy.x * y$; then indeed $[\ell]^s \supseteq [r]^s$ for the first four rules of Example 1 (e.g., $[\text{mult}(s x)y]^s = (x+1) * y \ge y + (x * y) = [\text{add}y(\text{mult}xy)]^s$). Moreover, let us choose $\mathcal{J}_{\text{add}}^c = \lambda xy.x + 1$ and $\mathcal{J}_{\text{mult}}^c = \lambda xy.x * y + x + 1$. Then also $[\ell]^c > \text{cost}(r)$ for all rules; for example, $[\text{mult}(s x)y]^c = (x+1) * y + 2 * x + 3 > (y+1) + (x * y + 2 * x + 1) = [\text{add}y(\text{mult}xy)]^c + [\text{mult}xy]^c = \text{cost}(\text{add}y(\text{mult}xy))$. Regarding funcProd, we can orient both rules by choosing $\mathcal{J}_{\text{funcProd}}^s = \lambda Fxy.y * \max(F(x), 1)^x$ and $\mathcal{J}_{\text{funcProd}}^c = \lambda FGxy.2*x*y*\max(F(x), 1)^{x+1} + x*G(x) + 2*x+1$. This works due to the monotonicity assumption, which provides, e.g., $G(x+1) \ge G(x)$. (This function is not polynomial, but that is allowed in the general case.)

2.3 Basic Feasible Functionals

We assume familiarity with Turing machines. In this paper, we consider *deterministic multi-tape Turing machines*. Those are, conceptually, machines consist-
ing of a finite set of states, one or more (but a fixed number of) right-infinite tapes divided into cells. Each tape is equipped with a tape head that scans the symbols on the tape's cells and may write on it. The head can move to the left or right. Let $W = \{0,1\}^*$. A k-ary Oracle Turing Machine (OTM) is a deterministic multi-tape Turing machine with at least $2k+1$ tapes: one main tape for (input/output), $k$ designated query tapes, and $k$ designated answer tapes. It also has $k$ distinct query states $q_i$ and $k$ answer states $a_i$.

A computation with a k-ary OTM $M$ requires $k$ fixed oracle functions $f_1, \dots, f_k : W \to W$. We write $M_f$ to denote a run of $M$ with these functions. A run of $M_f$ on $w$ starts with $w$ written in the main tape. It ends when the machine halts, and yields the word that is written in the main tape as output. As usual, we only consider machines that halt on all inputs. The computation proceeds as usual for non-query states. To query the value of $f_i$ on $w$, the machine writes $w$ on the corresponding query tape and enters the query state $q_i$. Then, in one step, the machine transitions to the answer state $a_i$ as follows: (a) the query value $w$ written in the query tape for $f_i$ is read; (b) the contents of the answer tape for $f_i$ are changed to $f_i(w)$; (c) the query value $w$ is erased from the query tape; and (d) the head of the answer tape is moved to its first symbol. The running time of $M_f$ on $w$ is the number of steps used in the computation.

A type-1 function is a mapping in $W \to W$. A type-2 functional of rank $(k, l)$ is a mapping in $(W \to W)^k \to W^l \to W$.

**Definition 1.** We say an OTM $M$ computes a type-2 functional $\Psi$ of rank $(k, l)$ iff for all type-1 functions $f_1, \dots, f_k$ and $x_1, \dots, x_l \in W$, whenever $M_{f_1, \dots, f_k}$ is started with $x_1, \dots, x_l$ written on its main tape (separated by blanks), it halts with $\Psi(f_1, \dots, f_k, x_1, \dots, x_l)$ written on its main tape.

**Definition 2.** Let $\{F_1, \dots, F_k\}$ be a set of type-1 variables and $\{x_1, \dots, x_l\}$ a set of type-0 variables. The set $\text{Pol}_N^2[\{F_1, \dots, F_k; x_1, \dots, x_l\}]$ of second-order polynomials over $\mathbb{N}$ with indeterminates $F_1, \dots, F_k, x_1, \dots, x_l$ is generated by:

$$P, Q := n \mid x \mid P + Q \mid P * Q \mid F(Q)$$

where $n \in \mathbb{N}$, $x \in \{x_1, \dots, x_l\}$, and $F \in \{F_1, \dots, F_k\}$.

Notice that a polynomial expression can be viewed as a type-2 functional in the natural way, e.g., $P(F, x) = 3 * F(x) + x$ is a second-order polynomial functional. Given $w \in W$, we write $|w|$ for its length and define the length $|f|$ of $f: W \to W$ as $|f| = \lambda n \max_{|y| \le n} |f(y)|$. This allows us to define BFF as the class of functionals computable by OTMs with running time bounded by a second-order polynomial.

**Definition 3.** A type-2 functional $\Psi$ is in BFF iff there exist an OTM $M$ and a second-order polynomial $P$ such that $M$ computes $\Psi$ and for all $\tilde{f}$ and $\tilde{x}$: the running time of $M_{f_1, \dots, f_k}$ on $x_1, \dots, x_l$ is at most $P(|f_1|, \dots, |f_k|, |x_1|, \dots, |x_l|)$.
### 3 Statement of the Main Result

The main result of this paper roughly states that BFF consists exactly of those type-2 functionals computed by an STRS compatible with a polynomially bounded cost-size tuple interpretation. To formally state this result, we must first define what it means for an STRS to compute a type-2 functional and define precisely the class of cost-size interpretations we are interested in.

Indeed, let us start by encoding words in $W$ as terms. We let bit, word $\in \mathbb{B}$ and introduce symbols $o, i, []$ : bit and [] : word, :: : bit $\Rightarrow$ word $\Rightarrow$ word. Then for instance 001 is encoded as the term ::= $o$ (::: $o$ (::: $i$ [])). We use the cleaner list-like notation [$o$; $o$; $i$] in practice. Let $\underline{w}$ denote the term encoding of a word $w$. Next, we encode type-1 functions as a possibly infinite set of one-step rewrite rules.

**Definition 4.** Consider a type-1 function $f : W \to W$ and let $S_f : \text{word} \Rightarrow \text{word}$ be a fresh function symbol. A set of rules $\mathcal{R}_f$ defines $f$ by way of $S_f$ if for each $w \in W$ there is exactly one rule of the form $S_f \underline{w} \to f(\underline{w})$ in $\mathcal{R}_f$.

Henceforth, we assume given that our STRS $(\mathbb{F}, \mathcal{R})$ at hand is such that $\mathbb{F}$ contains $o, i, []$, ::= typed as above and a distinguished symbol $F : (\text{word} \Rightarrow \text{word})^k \Rightarrow \text{word}^l \Rightarrow \text{word}$. Given type-1 functions $f_1, \dots, f_k$, we write $\mathbb{F}^f$ for $\mathbb{F}$ extended with function symbols $S_{f_i} : \text{word} \Rightarrow \text{word}$, with $1 \le i \le k$, and let $\mathcal{R}_{+f} = \mathcal{R} \cup \bigcup_{i=1}^k \mathcal{R}_f$. Now we can define the notion of type-2 computability for such STRSs.

**Definition 5.** Let $(\mathbb{F}, \mathcal{R})$ be an STRS. We say that $\mathbb{F}$ computes the type-2 functional $\Psi$ in $(\mathbb{F}, \mathcal{R})$ iff for all type-1 functions $f_1, \dots, f_k$ and all $w_1, \dots, w_l \in W$, $\mathbb{F} S_{f_1} \cdots S_{f_k} \underline{w_1} \cdots \underline{w_l} \to_{\mathcal{R}_{+f}} \underline{u}$, where $u = \Psi(f_1, \dots, f_k, w_1, \dots, w_l)$.

Next, we define what we mean by polynomially bounded interpretation.

**Definition 6.** We say an STRS $(\mathbb{F}, \mathcal{R})$ admits a polynomially bounded interpretation iff $(\mathbb{F}, \mathcal{R})$ is compatible with a cost-size interpretation such that:

* $S_{\text{word}} = (\mathbb{N}, \geq)$;

* $\mathcal{J}_o^c = \mathcal{J}_i^c = \mathcal{J}_{ii}^c = 0$, $\mathcal{J}_{ii}^c = \lambda xy.0$, and $\mathcal{J}_{ii}^s = \lambda xy.x + y + c$ for some $c \geq 1$;

* $\mathcal{J}_{\mathbb{F}}^c$ is bounded by a polynomial in $\text{Pol}_2^2[F_1^c, F_1^s, \dots, F_k^c, F_k^s; x_1, \dots, x_l]$.

Finally, we can formally state our main result.

**Theorem 2.** A type-2 functional $\Psi$ is in BFF if and only if there exists a finite orthogonal STRS $(\mathbb{F}, \mathcal{R})$ such that the distinguished symbol $F$ computes $\Psi$ in $(\mathbb{F}, \mathcal{R})$ and $\mathcal{R}$ admits a polynomially bounded cost-size interpretation.

We prove this result in two parts. First, we prove soundness in Section 4 which states that every type-2 functional computed by an STRS as above is in BFF. Then in Section 5 we prove completeness which states that every functional in BFF can be computed by such an STRS. In order to simplify proofs, we only consider type-2 functions of rank (1,1). We claim that the results can be easily generalized, but the proofs become more tedious when handling multiple arguments.
*Example 3.* Let us consider the type-2 functional defined by $\Psi := \lambda f x. \sum_{i<|x|} f(i)$.

Notice that $\Psi$ adds all $f(i)$ over each word $i \in W$ whose value (as a natural number) is smaller than the length of $x$. This functional was proved to lie in BFF in [20], where the authors utilized an encoding of $\Psi$ as a BTLP$_2$ program. We can encode $\Psi$ as an STRS as follows. Let us consider ancillary symbols `lengthOf`: `word` $\Rightarrow$ `nat` and `toBin`: `nat` $\Rightarrow$ `word`. The former computes the length of a given word and the latter converts a number from unary to binary representation. We also consider rules for addition on binary words, i.e., `+B`: `word` $\Rightarrow$ `word` $\Rightarrow$ `word`, which we use in infix notation below.

$$ 
\begin{align*}
\text{compute } F \ x \ 0 \ acc &\rightarrow acc \\
\text{compute } F \ x \ (s \ i) \ acc &\rightarrow \text{compute } F \ x \ i \ (acc \ +_B \ F(\text{toBin} \ i)) \\
\text{start } F \ x &\rightarrow \text{compute } F \ x \ (\text{lengthOf} \ x) \ \llbracket
\end{align*}
$$

Now, if we want to compute $\Psi(f, x)$ we simply reduce the term $\text{start } S_f \underline{\kappa}$ to normal form. To show that this system is in BFF via our rewriting formalism, we need to exhibit a cost-size tuple interpretation for it that satisfies Definition 6.

# 4 Soundness

In order to prove soundness, let us consider a fixed finite orthogonal STRS $\mathcal{R}$ admitting a polynomially bounded cost-size interpretation such that it computes a type-2 functional $\Psi$. We proceed to show that $\Psi$ is in BFF roughly as follows:

1. Since $\mathcal{R}$ computes $\Psi$ and admits a polynomially bounded interpretation, we show that so does the extended system $\mathcal{R}_{+f}$ (Definition 5). The restriction on $\mathcal{J}_{\cdot\cdot}^s$ (Definition 6) implies that $\llbracket F S_f \underline{w} \rrbracket^c$ is bounded by a second-order polynomial over $|f|, |w|$. We show this in Lemma 1. By compatibility (Theorem 1), we can do at most polynomially many steps when reducing $F S_f \underline{w}$.

2. The cost polynomial restricts the size of any input that the function variable $F$ is applied to (e.g., a cost bound of $3+F^c(m)$ implies that $F$ is never called on a term with size interpretation $> m$). This is the subject of Lemma 3.

3. Using the observations above, we then show that by graph rewriting we can simulate $\mathcal{R}_{+f}$ and compute each $\mathcal{R}_{+f}$-reduction step in polynomial time on an OTM. This guarantees that $\Psi$ is in BFF, Theorem 3.

## 4.1 Interpreting The Extended STRS, Polynomially

Our first goal is to provide a polynomially bounded cost-size interpretation to the extended system $\mathcal{R}_{+f}$. We start with the observation that the size interpretation of words in $W$ is proportional to their length. Indeed, since $\mathcal{J}_{\cdot\cdot}^s = \lambda xy.x + y + c$ (Definition 6) let $\mu := \max(\mathcal{J}_o^s, \mathcal{J}_i^s) + c$ and $\nu := \mathcal{J}_{\cdot\cdot}^s$. Consequently, for all $w \in W$:

$$ |w| \leq \llbracket \underline{w} \rrbracket^s \leq \mu * |w| + \nu \quad (1) $$
Recall that by Definition 4 the extended system $\mathcal{R}_{+f}$ has possibly infinitely many rules of the form $S_f \underline{w} \to f(\underline{w})$. Such rules $S_f$ represent calls for an oracle to compute $f$ in a single step. Thus, we set their cost to 1. The size should be given by the length of the oracle output, taking the overhead of interpretation into account. Hence, we obtain:

$$ \mathcal{J}_{S_f}^c = \lambda x.1 \qquad \mathcal{J}_{S_f}^s = \lambda x.\mu * |f|(x) + \nu $$

This is weakly monotonic because $|f|$ is. It orients the rules in $\mathcal{R}_f$ because $\llbracket S_f \underline{w} \rrbracket^c = 1 > 0 = \text{cost}(f(\underline{w}))$, and $\llbracket S_f \underline{w} \rrbracket^s = \mu * |f|(\llbracket \underline{w} \rrbracket^s) + \nu \ge \mu * |f|(\llbracket w \rrbracket) + \nu \ge \mu * |f(w)| + \nu$ by definition of $|f|$, which is superior or equal to $\llbracket f(\underline{w}) \rrbracket^s$.

As $\mathcal{J}_F^c$ is bounded by a second-order polynomial $\lambda F^c F^s x.P$, we can let $D(F, n) := P(\lambda x.1, \lambda x.\mu * F(x) + \nu, \mu * n + \nu)$. Then $D$ is a second-order polynomial, and $D(|f|, |w|) \ge \mathcal{J}_F^c(\mathcal{J}_{S_f}^c, \mathcal{J}_{S_f}^s, \llbracket \underline{w} \rrbracket^s) = \text{cost}(F S_f \underline{w})$. By Theorem 1 we see:

**Lemma 1.** There exists a second-order polynomial $D$ so that $D(|f|, |w|)$ bounds the derivation height of $F S_f \underline{w}$ for any $f \in W \to W$ and $w \in W$.

Notice that this lemma does not imply that $\Psi$ is in BFF. It only guarantees that there is a polynomial bound to the number of rewriting steps for such systems. However, it does not immediately follow that this number is a reasonable bound for the actual computational cost of simulating a reduction on an OTM. Consider for example a rule $f(s n) t \to f n (c t t)$. Every step doubles the size of the term. A naive implementation – which copies the duplicated term in each step – would take exponential time. Moreover, a single step using the oracle can create a very large output, which is not considered part of the cost of the reduction, even though an OTM would be unable to use it without first fully reading it.

Therefore, in order to prove soundness, we show how to realize a reasonable implementation of rewriting w.r.t. OTMs. In essence, we will show that (1) oracle calls are not problematic in the presence of polynomially bounded interpretations, and (2) we can handle duplication with an appropriate representation of rewriting.

## 4.2 Bounding The Oracle Input

We first deal with the reasonability of oracle calls. We will show that there exists a second-order polynomial $B$ such that if an oracle call $S_f \underline{x}$ occurs anywhere along the reduction $F S_f \underline{w} \to_R \underline{y}$, then $|x| \le B(|f|, |w|)$. From this, we know that the growth of the overall term size during an oracle call is at most $|f|(B(|f|, |w|))$.

Let $P$ again be the polynomial bounding $\mathcal{J}_F^c$. Since $P$ is a second-order polynomial, each occurrence of a sub-expression $F^c(E)$ in $P$ is a second-order polynomial, and so is $E$. Let us enumerate these arguments as $E_1, \dots, E_n$. We can then form the new polynomial $Q$ defined as

$$ Q := \sum_i E_i \quad \text{where occurrences of } F^c(E'_j) \text{ inside } E_i \text{ are replaced by 1} $$
We let $B(G, y) := Q(\lambda z.\mu * G(z) + \nu, \mu * y + \nu)$.

**Example 4.** If $P = \lambda F^c F^s x.x * F^c(3 + F^s(9*x)) + F^c(12) * F^c(3 + x * F^c(2)) + 5$, then $Q = 3 + F^s(9 * x) + 12 + 3 + x * 1 + 2 = 20 + F^s(9 * x) + x$. We have $B(G, x) = 20 + \mu * G(9*(\mu*x+\nu)) + \nu + (\mu*x+\nu) = 20 + 2*\nu + G(9*\mu*x + 9*\nu) + \mu*x$.

Now $B$ gives an upper bound to the argument values for $F^c$ that are considered: if a function differs from $\mathcal{J}_{S_f}^c$ only on argument values greater than $B(|f|, |w|)$, then we can use it in $P$ and obtain the same result. Formally:

**Lemma 2.** Fix $f, w$. Let $G \in \mathbb{N} \to \mathbb{N}$ with $G(z) = 1$ if $z \le B(|f|, |w|)$. Then $P(G, \mathcal{J}_{S_f}^s, \llbracket \mathbf{w} \rrbracket^s) = P(\mathcal{J}_{S_f}^c, \mathcal{J}_{S_f}^s, \llbracket \mathbf{w} \rrbracket^s)$.

This is proved by induction on the form of $P$, using that $G$ is never applied on arguments larger than $B(|f|, |w|)$. Lemma 2 is used in the following key result:

**Lemma 3 (Oracle Subterm Lemma).** Let $f: W \to W$ be a type-1 function and $w \in W$. If $\mathbf{F} S_f \mathbf{w} \to_{\mathbb{R}_{+f}}^* C[S_f \underline{\times}]$ for some context $C$, then $|x| \le B(|f|, |w|)$.

*Proof.* In view of a contradiction, suppose there exist $f, w$, and $x$ such that $\mathbf{F} S_f \mathbf{w} \to_{\mathbb{R}_{+f}}^* C[S_f \underline{\times}]$ for some context $C$, and $|x| > B(|f|, |w|)$. Let us now construct an alternative oracle: let $0: \text{nat}, s: \text{nat} \Rightarrow \text{nat}, S'_f: \text{word} \Rightarrow \text{word}$ and helper: $\text{nat} \Rightarrow \text{nat} \Rightarrow \text{nat}$, and for $N := D(|f|, |w|)$, let $\mathcal{R}'_{f,w}$ be given by:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \mathcal{S}'_f \underline{\times} \to \mathbf{f}(\mathbf{x}) & \text{if } |x| \le B(|f|, |w|) & \text{helper } 0 y \to y \\ \mathcal{S}'_f \underline{\times} \to \text{helper} \lceil \text{N} \rceil \mathbf{f}(\mathbf{x}) & \text{otherwise} & \text{helper } (s \mathbf{x}) y \to \text{helper } xy \end{array} $$

Where $\lceil \text{N} \rceil$ is the unary number encoding of $N$ as introduced in Section 2.1. Notice that by definition, the rules for $\mathcal{S}'_f$ will produce $\mathbf{f}(\mathbf{x})$ in one step if $|x| \le B(|f|, |w|)$, but they will take $N + 2$ steps otherwise. Also observe that $\mathcal{S}_f$ and $\mathcal{S}'_f$ behave the same; that is, $\mathcal{S}_f \underline{\times}$ and $\mathcal{S}'_f \underline{\times}$ have the same normal form on any input $\underline{\times}$. We extend the interpretation function of the original signature with:

$$ \mathcal{J}_{\mathcal{S}'_f}^c = \lambda x. \begin{cases} 1 & \text{if } x \le B(|f|, |n|) \\ N + 2 & \text{if } x > B(|f|, |n|) \end{cases} \qquad \mathcal{J}_{\mathcal{S}'_f}^s = \mathcal{J}_{\mathcal{S}_f}^s(y) $$

$$ \mathcal{J}_{\text{helper}}^{c} = \lambda xy.x + 1 \qquad \mathcal{J}_{\text{helper}}^{s} = \lambda xy.y \qquad \mathcal{J}_{0}^{s} = 0 \qquad \mathcal{J}_{s}^{s} = \lambda x.x + 1 $$

We easily see that this orients all rules in $\mathcal{R}_{f,w}$. Then, by Lemma 2, $\text{cost}(\mathbf{F} S'_f \mathbf{w}) \le P(\mathcal{J}_{\mathcal{S}'_f}^c, \mathcal{J}_{\mathcal{S}'_f}^s, \llbracket \mathbf{w} \rrbracket^s) = P(\mathcal{J}_{\mathcal{S}_f}^c, \mathcal{J}_{\mathcal{S}_f}^s, \llbracket \mathbf{w} \rrbracket^s) \le D(|f|, |w|) = N$. Yet, as we have $\mathbf{F} S_f \mathbf{w} \to_{\mathbb{R}_{+f}}^* C[S_f \underline{\times}]$, we also have $\mathbf{F} S_f \mathbf{w} \to_{\mathbb{R} \cup \mathcal{R}'_{f,w}} C'[S'_f \underline{\times}]$, where $C'$ is obtained from $C$ by replacing all occurrences of $\mathcal{S}_f$ by $\mathcal{S}'_f$. Since $|x| > B(|f|, |w|)$ by assumption, the reduction $\mathbf{F} S'_f \mathbf{w} \to_{\mathbb{R} \cup \mathcal{R}'_{f,w}} C[S'_f \mathbf{w}] \to_{\mathbb{R} \cup \mathcal{R}_{f,w'}} C[f(\mathbf{x})]$ takes strictly more than $N$ steps, contradicting Theorem 1. $\square$
<figure><img src="image_1.png" /><figcaption>Fig. 1: A term graph, its simplified version, and two graphs with sharing</figcaption></figure>

## 4.3 Graph Rewriting

Lemma 1 guarantees that if $\mathcal{R}$ is compatible with a suitable interpretation, then at most polynomially many $\mathcal{R}_{+f}$-steps can be performed starting in $FS_f w$. However, as observed in Section 4.1, this does not yet imply that a type-2 functional computed by an STRS with such an interpretation is in BFF. To simulate a reduction on an OTM, we must find a representation whose size does not increase too much in any given step. The answer is *graph rewriting*.

**Definition 7.** A term graph for a signature $\Sigma$ is a tuple $(V, \text{label}, \text{succ}, \Lambda)$ with $V$ a finite nonempty set of vertices; $\Lambda \in V$ a designated vertex called the root; $\text{label} : V \to \Sigma \cup \{\text{@}\}$ a partial function with @ fresh; and $\text{succ} : V \to V^*$ a total function such that $\text{succ}(v) = v_1v_2$ when $\text{label}(v) = \text{@}$ and $\text{succ}(v) = \varepsilon$ otherwise. We view this as a directed graph, with an edge from $v$ to $v'$ if $v' \in \text{succ}(v)$, and require that this graph is acyclic (i.e., there is no path from any $v$ to itself). Given term graph $G$, we will often directly refer to $V_G$, $\text{label}_G$, etc.

Term graphs can be denoted visually in an intuitive way. For example, using $\Sigma$ from Example 1, the graph with $V = \{v_0, \dots, v_4\}$, $\text{label} = \{v_0, v_1 \mapsto \text{@}, v_2 \mapsto \text{add}\}$, $\text{succ} = \{v_0 \mapsto v_1v_4, v_1 \mapsto v_2v_3, v_3, v_4, v_5 \mapsto \varepsilon\}$ and $\Lambda = v_0$ is pictured in Figure 1a. We use $\perp$ to indicate unlabeled vertices and a circle for $\Lambda$. We will typically omit vertex names, as done in Figure 1b. Note that the definition allows multiple vertices to have the same vertex as successor; these successor vertices with in-degree > 1 are *shared*. Two examples are denoted in Figures 1c and 1d.

Each term has a natural representation as a tree. Formally, for a term $s$ we let $[s]_G = (\text{pos}(s), \text{label}, \text{succ}, \#)$ where $\text{label}(p) = \text{@}$ if $s|_p = s_1s_2$ and $\text{label}(p) = \text{f}$ if $s|_p = \text{f}$; $\text{label}(p)$ is not defined if $s|_p$ is a variable; and $\text{succ}(p) = (1 \cdot p)(2 \cdot p)$ if $s|_p = s_1s_2$ and $\text{succ}(p) = \varepsilon$ otherwise. Essentially, $[s]_G$ maintains the positioning structure of $s$ and forgets variable names. For example, Figure 1b denotes both $[\text{add} \ x \ y]_G$ and $[\text{add} \ x \ x]_G$.

Our next step is to *reduce* term graphs using rules. We limit interest to *left-linear* rules, which includes all rules in $\mathcal{R}_{+f}$ (as $\mathcal{R}$ is orthogonal, and the rules in $\mathcal{R}_f$ are ground). To define reduction, we will need some helper definitions.
**Definition 8.** Let $G = (V, \text{label}, \text{succ}, \Lambda), v \in V$. The **subgraph reach**($G, v$) of $G$ rooted at $v$ is the term graph $(V', \text{label}', \text{succ}', v)$ where $V'$ contains those $v' \in V$ such that a path from $v$ to $v'$ exists, and $\text{label}', \text{succ}'$ are respectively the limitations of label and succ to $V'$.

**Definition 9.** A homomorphism between two term graphs $G$ and $H$ is a function $\phi: V_G \to V_H$ with $\phi(\Lambda_G) = \Lambda_H$, and for $v \in V_G$ such that $\text{label}_G(v)$ is defined, $\text{label}_H(\phi(v)) = \text{label}_G(v)$ and $\text{succ}_H(\phi(v)) = \phi(v_1) \dots \phi(v_k)$ when $\text{succ}_G(v) = v_1 \dots v_k$. (If $\text{label}_G(v)$ is undefined, $\text{succ}_H(\phi(v))$ may be anything.)

**Definition 10.** A redex in $G$ is a triple $(\rho, v, \phi)$ consisting of some rule $\rho = \ell \to r \in \mathbb{R}_{+f}$, a vertex $v$ in $V_G$, and a homomorphism $\phi: [\ell]_G \to \text{reach}(G, v)$.

**Definition 11.** Let $G$ be a term graph and $v_1, v_2$ vertices in $G$. The redirection of $v_1$ to $v_2$ is the term graph $G[v_1 \gg v_2] = (V_G, \text{label}_G, \text{succ}_G', \Lambda'_G)$ with

$$ \text{succ}_{G'}(v)_i = \begin{cases} v_2, & \text{if } \text{succ}_G(v)_i = v_1 \\ \text{succ}_G(v)_i, & \text{otherwise} \end{cases} \qquad \Lambda'_G = \begin{cases} v_2 & \text{if } \Lambda_G = v_1 \\ \Lambda_G & \text{otherwise} \end{cases} $$

That is, we replace every reference to $v_1$ by a reference to $v_2$. With these definitions in hand, we can define contraction of term graphs:

**Definition 12.** Let $G$ be a term graph, and $(\rho, v, \phi)$ a redex in $G$ with $\rho \in \mathbb{R}_{+f}$, such that no other vertex $v'$ in $\text{reach}(G, v)$ admits a redex (so $v$ is an innermost redex position). Denote $a_x$ for the position of variable $x$ in $\ell$, and recall that $a_x$ is a vertex in $[\ell]_G$. By left-linearity, $a_x$ is unique for $x \in \text{vars}(\ell)$. The contraction of $(\rho, v, \phi)$ in $G$ is the term graph $J$ produced after the following steps: $H$ (building), $I$ (redirection), and $J$ (garbage collection).

(building) Let $H = (V_H, \text{label}_H, \text{succ}_H, \Lambda_G)$ where:

* $V_H = V_G \uplus \{\bar{p} \in \text{pos}(r) \mid r|_p \text{ is not a variable}\} \text{ (}\uplus \text{ means disjoint union)}$;

* for $v \in V_G$: $\text{label}_H(v) = \text{label}_G(v)$ and $\text{succ}_H(v) = \text{succ}_G(v)$

* for $p \in V_H$ with $r|_p$ not a variable:

* $\text{label}_H(\bar{p}) = \text{f}$ if $r|_p = \text{f}$ and $\text{label}_H(\bar{p}) = \text{@}$ otherwise

* $\text{succ}_H(\bar{p}) = \varepsilon$ if $r|_p = \text{f}$; otherwise, $\text{succ}_H(\bar{p}) = \psi(1 \cdot p)\psi(2 \cdot p)$
    Here, $\psi(q) = \bar{q}$ if $r|_q$ is not a variable; if $r|_q = x$ then $\psi(q) = \phi(a_x)$.

(redirection) If $r$ is a variable $x$ (so $H = G$), then let $I = G[v \gg \phi(a_x)]$. Otherwise, let $I = H[v \gg \bar{r}]$, so with all references to $v$ redirected to the root vertex for $r$.

(garbage collection) Let $J := \text{reach}(I, \Lambda_I)$ (so remove unreachable vertices).

We then write $G \rightsquigarrow J$ in one step, and $G \rightsquigarrow^n J$ for the n-step reduction.

We illustrate this with two examples. First, we aim to rewrite the graph of Figure 2a with a rule $\text{add0} y \to y$ at vertex $v$. Since the right-hand side is a variable, the building phase does nothing. The result of the redirection phase is given in Figure 2b, and the result of the garbage collection in Figure 2c.
<figure><img src="image_2.png" /><figcaption>Fig. 2: Reducing a graph with the rule $add \ 0 \ y \to y$</figcaption></figure>

Second, we consider a reduction by mult $(s \cdot x) y \to add \ y$ (mult $x$ $y$). Figure 3a shows the result of the building phase, with the vertices and edges added during this phase in red. Redirection sets the root to the squared node (the root of the right-hand side), and the result after garbage collection is in Figure 3b.

<figure><img src="image_3.png" /><figcaption>Fig. 3: Reducing a term graph with substantial sharing</figcaption></figure>

Note that, even when a term graph $G$ is not a tree, we can find a corresponding term: we assign a variable $var(v)$ to each unlabeled vertex $v$ in $G$, and let:

$$ \theta(v) = \begin{cases} \theta(v_1) \theta(v_2) & \text{if } \text{label}(v) = @ \text{ and } \text{succ}(v) = v_1 v_2 \\ f & \text{if } \text{label}(v) = f \\ var(v) & \text{if } \text{label}(v) \text{ is undefined} \end{cases} $$

Then we may define $[G]_G^{-1} = \theta(\Lambda_G)$. For a linear term, clearly $[[s]_G]_G^{-1} = s$ (modulo variable renaming). We make the following observation:

**Lemma 4.** Assume given a term graph $G$ such that there is a path from $\Lambda_G$ to every vertex in $V_G$, and let $[G]_G^{-1} = s$. If $G \rightsquigarrow H$ then $[G]_G^{-1} \to_{R_{+f}} [H]_G^{-1}$. Moreover, if $s \to_{R_{+f}} t$ for some $t$, then there exists $H$ such that $G \rightsquigarrow H$.

Consequently, if $\to_{R_{+f}}$ is terminating, then so is $\rightsquigarrow$; and if $[s]_G \rightsquigarrow^n G$ for some ground term $s$ then $s \to_{R_{+f}}^* [G]_G^{-1}$ in at least $n$ steps. Notice that if $G$ does not
admit any redex, then $[G]_G^{-1}$ is in normal form. Moreover, since $\mathcal{R}_{+f} = \mathcal{R} \cup \mathcal{R}_f$ is orthogonal (as $\mathcal{R}$ is orthogonal and the $\mathcal{R}_f$ rules are non-overlapping) and therefore confluent, this is the unique normal form of $s$. We conclude:

**Corollary 1.** If $[FS_f w]_G \rightsquigarrow^n G$, then $n \le D(|f|, |w|)$; and if $G$ is in normal form, then $[G]_G^{-1} = \Psi(f, w)$.

## 4.4 Bringing Everything Together

We are now ready to complete the soundness proof following the recipe at the start of the section. Towards the third bullet point, we make the following observation.

**Lemma 5.** There is a constant $a$ such that, whenever $G \rightsquigarrow H$ by a rule in $\mathcal{R}$, then $|H| \le |G| + a$, where $|G|$ denotes the total number of nodes in the graph $G$.

*Proof.* In a step using a rule $\ell \to r$, the number of nodes in the graph can be increased at most by $|[r]_G|$. As there are only finitely many rules in $\mathcal{R}$, we can let $a$ be the number of nodes in the largest graph for a right-hand side $r$. $\square$

To see that graph rewriting with $S_f$ can be implemented in an efficient way, we observe that the size of any intermediary graph in the reduction $[G w]_G \to_{\mathcal{R}}^+$ $[q]_G$ is polynomially bounded by a second-order polynomial over $|f|, |w|$:

**Lemma 6.** There is a second-order polynomial $Q$ such that if $[FS_f w]_G \rightsquigarrow^* H$, then $|H| \le Q(|f|, |w|)$.

*Proof.* Let $Q(F, x) := x + D(F, x) * (a + F(B(F, x)))$, where $D$ is the polynomial from Lemma 1, $a$ is the constant from Lemma 5, and $B$ is the polynomial from Section 4.2. This suffices, because there are at most $D(|f|, |w|)$ steps (Lemma 1, Corollary 1), each of which increases the graph size by at most $\max(a, |f|(B(|f|, |w|)))$. $\square$

All in all, we are finally ready to prove the soundness side of the main theorem:

**Theorem 3.** Let $\mathcal{R}$ be a finite orthogonal STRS admitting a polynomially bounded interpretation. If $\mathbb{F}$ computes a type-2 functional $\Psi$, then $\Psi \in \text{BFF}$.

*Proof.* Given $(\mathbb{F}, \mathcal{R})$, we can construct an OTM $M$ so that for a given $f \in W \to W$, the machine $M_f$ executed on $w \in W$ computes the normal form of $FS_f w$ under $\to_{\mathcal{R}_{+f}}$ using graph rewriting. We omit the exact construction, but observe:

* that we can represent each graph in polynomial space in the size of the graph;

* that we can do a rewriting step that does not call the oracle (so using a rule in $\mathcal{R}$) following the contraction algorithm we defined in Definition 12, which is clearly feasible to do in polynomial time in the size of the graph;
* and that each oracle call (implemented in rewriting by a $\mathcal{R}_f$-step $S_f \xrightarrow{\Sigma} \mathcal{Y}$) is resolved by copying $\Sigma$ to the query tape, transitioning to the query state, and from the answer state copying $\mathcal{Y}$ from the answer tape to the main tape. By Lemma 3 this is doable in polynomial time in $|f|, |w|$ and the graph size. By Lemma 6, graph sizes are bounded by a polynomial over $|f|, |w|$, so using the above reasoning, the same holds for the cost of each reduction step. In summary: the total cost of $M_f$ running on $w$ is bounded by a second-order polynomial in terms of $|f|$ and $|w|$. As $M_f$ simulates $\mathcal{R}_{+f}$ via graph rewriting and $\mathcal{R}_{-f}$ computes $\Psi$, $M$ also computes $\Psi$. By Definition 3, $\Psi$ is in BFF. $\square$

# 5 Completeness

Recall from Section 3 that to prove completeness we have to show the following: if a given type-2 functional $\Psi$ is in BFF, then there exists an orthogonal STRS that computes $\Psi$ and admits a polynomially bounded interpretation. We prove this by providing an encoding of OTMs as STRSs that admit a polynomially bounded interpretation.

The encoding is divided into three steps. In Section 5.1, we will define the function symbols that will allow us to encode any possible machine configuration as terms. In Section 5.2, we will encode transitions as reduction rules that rewrite configuration terms. Lastly, we will design an STRS to simulate a complete execution of an OTM in polynomially many steps. Achieving this polynomial bound is non-trivial and is done in Sections 5.3–5.4.

Henceforth, we assume given a fixed OTM $M$, and a second-order polynomial $P_M$, such that $M$ operates in time $P_M$. For simplicity, we assume the machine has only three tapes (one input/output tape, one query tape, one answer tape); that each non-oracle transition only operates on one tape (i.e., reading/writing and moving the tape head); and that we only have tape symbols $\{0, 1, \mathbf{B}\}$.

## 5.1 Representing Configurations

Following 3, we have $o, i: \text{bit}, \therefore: \text{bit} \Rightarrow \text{word} \Rightarrow \text{word}$ and $\llbracket \rrbracket: \text{word}$. To represent a (partial) tape, we also introduce $b: \text{bit}$ for the blank symbol. Now for instance a tape with content $011B01BB\cdots$ (followed by infinitely many blanks) may be represented as the list $[o; i; i; b; o; i]$ of type word. We may also add an arbitrary number of blanks at the end of the representation; e.g., $[o; i; i; b; o; i; b]$.

We can think of a *tape configuration* — the combination of a tape and the position of the tape head — as a finite word $w_1 \dots w_{p-1} \# w_p w_{p+1} \dots w_k$ (followed by infinitely many blanks). Here, the tape's head is reading the symbol $w_p$. We can split this tape into two components: the *left* word $w_1 \dots w_{p-1}$, and the *right* word $w_p \dots w_k$. To represent a tape configuration, we introduce three symbols:

$L: \text{word} \Rightarrow \text{left}$

$R: \text{word} \Rightarrow \text{right}$

$\text{split}: \text{left} \Rightarrow \text{right} \Rightarrow \text{tape}$

Here, $L, R$ hold the content of the left and right split of the tape, respectively. While we technically do not need these two constructors (we could have $\text{split}$:
word $\Rightarrow$ word $\Rightarrow$ tape), they serve to make configurations more human-readable. For convenience in rewriting transitions, later on, we will encode the left side of the split in reverse order. Specifically, we encode $w_1...w_{p-1}\#w_p w_{p+1}...w_k$ as

$$ \text{split}(\text{L}[w_{p-1}; \dots; w_2; w_1]) (\text{R}[w_p; \dots; w_{k-1}; w_k]) $$

The symbol currently being read is the first element of the list below $\mathbb{R}$; in case of $\mathbb{R}$(), this symbol is $\mathbb{B}$. For a concrete example, a tape configuration 1B0#10 is represented by: split (L [o; b; i]) (R [i; o]). Since we have assumed an OTM with three tapes, a configuration of the machine at any moment is a tuple $(q, t_1, t_2, t_3)$, with $q$ a state and $t_1, t_2, t_3$ tape configurations. To represent machine configurations, we introduce, for each state $q$, a symbol $q: \text{tape} \Rightarrow \text{tape} \Rightarrow \text{tape} \Rightarrow \text{config}$. Thus, a configuration $(q, t_1, t_2, t_3)$ is represented by a term $q T_1 T_2 T_3$.

*Example 5.* The initial configuration for a machine $M_f$ on input $w$ is a tuple $(q_0, \#w, \#\mathbb{B}, \#\mathbb{B})$. This is represented by the term

$$ \text{initial}(w) := q_0 (\text{split}(\text{L})) (\text{R}\underline{w}) (\text{split}(\text{L})) (\text{R}) (\text{split}(\text{L})) (\text{R}) $$

To interpret the symbols from this section, we let $(S_\iota, \supseteq_\iota) := (\mathbb{N}, \ge)$ for all $\iota$, let $\mathcal{J}_f^c = \lambda x_1 \dots x_m. 0$ whenever $f$ takes $m$ arguments, and for the sizes:

$$ \begin{array}{lclcl} \mathcal{J}_o^s & = & 0 & \mathcal{J}_b^s & = & 0 \\ \mathcal{J}_i^s & = & 0 & \mathcal{J}_R^s & = & \lambda x.x \\ \mathcal{J}_i^s & = & \mathcal{J}_o^s & \mathcal{J}_s^c & = & \lambda xy.x + y + 1 \\ \mathcal{J}_i^s & = & \mathcal{J}_o^s & \mathcal{J}_s^c & = & \lambda x.xyx.x + y \end{array} \quad (\text{for all states } q) $$

Hence, $[\underline{w}]^s = |w|$, which satisfies the requirements of Theorem 2; the size of a tape configuration $w_1...w_{p-1}\#w_p...w_k$ is $k$, and the size of a configuration is the size of its first and second tapes combined. We do not include the third tape, as it does not directly affect either the result yielded by the final configuration (this is read from the first tape), nor the size of a word the oracle $f$ is applied on.

## 5.2 Executing The Machine

A single step in an OTM can either be an oracle call (a transition from the query state to the answer state), or a traditional step: we assume that an OTM $M$ has a fixed set $\mathcal{T}$ of transitions $q \xrightarrow[r/i, d]{r/i, d} l$ where $q$ is the input state, $l$ the output state, $t \in \{1, 2, 3\}$ the tape considered (recall that we have assumed that a non-oracle transition only operates on one tape), $r, i \in \{0, 1, \mathbb{B}\}$ respectively the symbol being read and the symbol being written, and $d \in \{L, R\}$ the direction for the read head of tape $t$ to move. We will model the computation of $M$ as rules that simulate the small step semantics for the machine.

To encode a single transition, let step : (word $\Rightarrow$ word) $\Rightarrow$ config $\Rightarrow$ config. For any transition of the form $q \xrightarrow[r/i, L]{r/i, L} l$ (so a transition operating on tape 1, and moving left), we introduce a rule (where we write $\mathbb{0} = \mathbb{o}$, $\mathbb{1} = i$, $\mathbb{B} = \mathbb{b}$):

$$ \text{step } F(q(\text{split}(\text{L}(x::y))(\text{R}(\underline{r}::z)))uv) \to 1(\text{split}(\text{L}y)(\text{R}(x::\underline{i}::z)))uv $$
Moreover, for transitions $q \overset{B/w, L}{\rightleftharpoons} l$ (so where B is read), we add a rule:

$$ \text{step } F(\mathbf{q} (\text{split}(\mathbf{L}(x::y))(\mathbf{R}[])) uv) \to 1 (\text{split}(\mathbf{L} y)(\mathbf{R}(x::[::])))) uv $$

These rules respectively handle the steps where a tape configuration is changed from $u_1...u_{p-1}u_p \# ru_{p+2}...u_k$ to $u_1...u_{p-1} \# u_p i u_{p+2}...u_k$, and where a tape configuration is changed from $u_1...u_k \# u_1...u_k i$.

Transitions where $d = R$, or on the other two tapes, are encoded similarly.

Next, we encode oracle calls. Recall that, to query the machine for the value of $f$ at $u$, we write $u$ on the second tape, move its head to the leftmost position, and enter the query state. Then, the content of this tape is erased and the image of $f$ over $u$ is written in the third tape. Visually, this step is represented as:

$$ (\mathbf{query}, \langle \text{tape}_1 \rangle, v_1 \dots v_p \# \mathbf{u} \mathbf{B} \dots, \langle \text{tape}_3 \rangle) \rightsquigarrow (\mathbf{answer}, \langle \text{tape}_1 \rangle, \# \mathbf{B}, \# f(\mathbf{u})) $$

This is implemented by the following rules:

$$ \begin{array}{l} \text{step } F(\mathbf{query} t_1 (\text{split } \mathbf{L}(\mathbf{R} y)) t_3) \to \mathbf{answer} t_1 (\text{split } \mathbf{L}[])(\mathbf{R}[])) \\ \qquad (\text{split } \mathbf{L}[])(\mathbf{R}(F(\mathbf{clean} y)))) \end{array} $$

$$ \mathbf{clean}(o::x) \to o::(\mathbf{clean} x) \qquad \mathbf{clean}(b::x) \to [] $$

$$ \mathbf{clean}(i::x) \to i::(\mathbf{clean} x) \qquad \mathbf{clean} [] \to [] $$

Here, $\mathbf{clean} : \mathbf{word} \Rightarrow \mathbf{word}$ turns a word that may have blanks in it into a bitstring, by reading until the next blank; for instance replacing $[o; i; b; i]$ by $[o; i]$.

The various step rules, as well as the clean rules, are non-overlapping because we consider deterministic OTMs. They are also left-linear, and are oriented using:

$$ \mathcal{J}_{\text{clean}}^{s} = \lambda x.x \qquad \mathcal{J}_{\text{clean}}^{c} = \lambda x.x + 1 $$

$$ \mathcal{J}_{\text{step}}^{s} = \lambda F x.x + 1 \qquad \mathcal{J}_{\text{step}}^{c} = \lambda F^{c} F^{s} x.F^{c}(x) + x + 2 $$

(Note that $\mathcal{J}_{\text{step}}^{s}$ is so simple because the size of a configuration does not include the size of the answer tape.) From the rules, the following result is obvious:

**Lemma 7.** Let $M_f$ be an OTM and $C, C'$ be machine configurations of $M_f$ such that $C \rightsquigarrow C'$. Then step $S_f[C] \to_R^{+} [C']$, where $[C]$ is the term encoding of $C$.

## 5.3 A Bound on the Number of Steps

To generalize from performing a single step of the machine to tracing a full computation on the machine level, the natural idea would be to define rules such as:

$$ \text{execute } F(\mathbf{q} \mathbf{x} \mathbf{y} \mathbf{z}) \to \text{execute } F(\text{step}(\mathbf{q} \mathbf{x} \mathbf{y} \mathbf{z})) \text{ for } q \neq \text{end} $$

$$ \text{execute } F(\text{end}(\text{split}(\mathbf{L} x)(\mathbf{R} w)) y z) \to \text{clean } w $$

Then, reducing execute $S_f$ initial($w$) to normal form simulates a full OTM execution of $M_f$ on input $w$. Unfortunately, this rule does not admit an interpretation,
as it may be non-terminating. A solution could be to give execute an additional argument ⌜N⌝ suggesting an execution in at most *N* steps; this argument would ensure termination, and could be used to find an interpretation.

The challenge, however, is to compute a bound on the number of steps in the OTM: the obvious thought is to compute $P_M(|f|, |w|)$, but this cannot in general be done in polynomial time because the STRS does not have access to $|f|$: since $|f|(i) = \max\{x \in \mathbb{N} \mid |x| \le i\}$, there are exponentially many choices for $x$.

To solve this, and following [21, Proposition 2.3], we observe that it suffices to know a bound for $f(x)$ for only those $x$ on which the oracle is actually questioned. That is, for $A \subseteq W$, let $|f|_A = \lambda n$. $\max\{|f(x)| \mid x \in A \wedge |x| \le n\}$. Then:

**Lemma 8.** Suppose an OTM $M_f$ runs in time bounded by $P_M(|f|, |w|)$ on input $w$. If $M_f$ transitions in $N$ steps from its initial state to some configuration $C$, calling the oracle only on words in $A \subseteq W$, then $N \le P_M(|f|_A, |w|)$.

*Proof (Sketch).* We construct $f'$ with $f'(x) = 0$ if $x \notin A$ and $f'(x) = f(x)$ if $x \in A$. Then $|f'| = |f|_A$, and $M_{f'}$ runs the same on input $w$ as $M_f$ does. □

Now, for $A$ encoded as a term $A$ (using symbols $\emptyset$: set, $\text{setcons}$: word $\Rightarrow$ set $\Rightarrow$ set), we can compute $|f|_A$ using the rules below, where we use unary integers as in Example 1 (0: nat, $s$: nat $\Rightarrow$ nat), and defined symbols $\text{len}$: word $\Rightarrow$ nat, $\max$: nat $\Rightarrow$ nat $\Rightarrow$ nat, limit: word $\Rightarrow$ nat $\Rightarrow$ word, $\text{retif}$: word $\Rightarrow$ nat $\Rightarrow$ word $\Rightarrow$ word, $\text{tryapply}$: (word $\Rightarrow$ word) $\Rightarrow$ word $\Rightarrow$ nat $\Rightarrow$ nat, $\text{tryall}$: (word $\Rightarrow$ word) $\Rightarrow$ set $\Rightarrow$ nat $\Rightarrow$ nat. By design, $\text{retif}$ ⌜n⌝ $y$ reduces to $y$ if $|x| \le n$ and to [] otherwise; $\text{tryapply}$ $S_f$ ⌜n⌝ reduces to the unary encoding of $|F|_{\{x\}}(n)$ and $\text{tryall}$ a ⌜n⌝ yields $|F|_A(n)$.

$$
\begin{align*}
\text{len } [] &\to 0 & \text{len } (x::y) &\to s (\text{len } y) \\
\max 0 m &\to m & \max (s n) 0 &\to s n & \max (s n) (s m) &\to s (\max n m) \\
\text{limit } [] n &\to [] & \text{limit } (x::y) 0 &\to [] & \text{limit } (x::y) (s n) &\to x::(\text{limit } y n) \\
\text{retif } [] n z &\to z & \text{retif } (x::y) 0 z &\to [] & \text{retif } (x::y) (s n) z &\to \text{retif } y n z
\end{align*}
$$

$$
\begin{align*}
\text{tryall } F \emptyset n &\to 0 & \text{tryall } F (\text{setcons } a \text{ tl}) n &\to \max (\text{tryapply } F a n) (\text{tryall } F \text{ tl } n) \\
\text{tryapply } F a n &\to \text{len } (\text{retif } a n (F (\text{limit } a n)))
\end{align*}
$$

An interpretation is provided in Appendix B. Importantly, the limit function ensures that, in *tryall* $F n$ we never apply $F$ to a word $w$ with $|w| > n$. Therefore we can let $[[A]]^s = |A|$, the number of words in $A$, and have $\mathcal{J}_{\text{tryall}}^s = \lambda F \text{an.} F(n)$ and $\mathcal{J}_{\text{tryall}}^c = \lambda F^c F^s a n. 1 + a + F^c(n) + 2 * F^s(n) + 2 * n + 6$.

Now, for a given second-order polynomial $P$, fixed $f, n$, and a term $A$ encoding a set $A \subseteq W$, we can construct a term $\Theta_{S_f; \Gamma_n; A}^P$ that computes $P(|f|_A, n)$ using $\text{tryall}$ and the functions `add`, `mult` from Example 1. By induction on $P$, we have $[[\Theta_{S_f; \Gamma_n; A}^P]]^s = P(|f|, n)$, while its cost is bounded by a polynomial over $|f|, n, |A|$.

## 5.4 Finalising Execution

Now, we can define execution in a way that can be bounded by a polynomial interpretation. We let execute: (word $\Rightarrow$ word) $\Rightarrow$ nat $\Rightarrow$ nnat $\Rightarrow$ nat $\Rightarrow$ set $\Rightarrow$
config $\Rightarrow$ word and will define rules to reduce expressions execute $F nmza c$ where

* $F$ is the function to be used in oracle calls.

* $n-1$ is a bound on the number of steps that can be done before the next oracle call (or until the machine completes execution).

* $m$ is essentially a natural number that represents the number of steps that have been done so far. We use a new sort $nnat$ with function symbols $o:nnat$ and $n:nnat \Rightarrow nnat$ because we will let $S_{nnat} = (\mathbb{N}, \leq)$, so ordered in the other direction. This will be essential to find an interpretation for execute.

* $z$ is a unary representation of $|w|$, where $w$ is the input to the OTM.

* $c$ is the current configuration.

Using helper symbols $F'$: (word $\Rightarrow$ word) $\Rightarrow$ nat $\Rightarrow$ config $\Rightarrow$ word, execute': (word $\Rightarrow$ word) $\Rightarrow$ nat $\Rightarrow$ nnat $\Rightarrow$ nat $\Rightarrow$ set $\Rightarrow$ config $\Rightarrow$ word, extract: tape $\Rightarrow$ word and minus: nat $\Rightarrow$ nnat $\Rightarrow$ nat, we introduce the rules:

$$ 
\begin{array}{l}
F F w \rightarrow F' F (\text{len } w) (q_0 (\text{split}(L [])) (R w)) (\text{split}(L [])) (R [])) (\text{split}(L [])) (R [])) \\
F' F z c \rightarrow \begin{array}{@{}c@{}}
    \text{execute} & F \Theta_{F;z;\emptyset}^{P_M+1} \circ z \emptyset c \\
    & \\
    \text{execute} & F (sn) m z a (qt_1 t_2 t_3) \rightarrow \\
    & \qquad \text{execute} F n (nm) z (\text{step } F (qt_1 t_2 t_3)) \text{ for } q \notin \{\text{query, end}\} \\
    \text{execute} & F (sn) m z a (query t_1 t_2 t_3) \rightarrow \\
    & \qquad \text{execute}' F n (nm) z (\text{setcons} (\text{extract } t_2) a) (query t_1 t_2 t_3) \\
    \text{execute}' F n m z a c \rightarrow \text{execute} F (\text{minus} \Theta_{F;z;a}^{P_M+1} m) m z a (\text{step } F c) \\
    \text{execute} F n m z a (end t_1 t_2 t_3) \rightarrow \text{extract } t_1 \\
    \text{extract} (\text{split}(L x) (R y)) \rightarrow \text{clean } y \\
    \text{minus } x \circ \rightarrow x & \text{minus } 0 (ny) \rightarrow 0 & \text{minus} (sx) (ny) \rightarrow \text{minus } xy
\end{array}
$$

$$ \begin{array}{l} \text{execute } F (sn) m z a (qt_1 t_2 t_3) \rightarrow \\ \qquad \text{execute } F n (nm) z (\text{step } F (qt_1 t_2 t_3)) \text{ for } q \notin \{\text{query, end}\} \end{array} $$

$$ \begin{array}{l} \text{execute } F (sn) m z a (query t_1 t_2 t_3) \rightarrow \\ \qquad \text{execute}' F n (nm) z (\text{setcons} (\text{extract } t_2) a) (query t_1 t_2 t_3) \end{array} $$

$$ \text{execute}' F n m z a c \rightarrow \text{execute } F (\text{minus } \Theta_{F;z;a}^{P_M+1} m) m z a (\text{step } F c) $$

$$ \text{execute } F n m z a (end t_1 t_2 t_3) \rightarrow \text{extract } t_1 $$

$$ \text{extract} (\text{split}(L x) (R y)) \rightarrow \text{clean } y $$

$$ \text{minus } x \circ \rightarrow x \qquad \text{minus } 0 (ny) \rightarrow 0 \qquad \text{minus} (sx) (ny) \rightarrow \text{minus } xy $$

That is, an execution on $FS_f w$ starts by computing the length of $w$ and $P_M(|f|_A, |w|)$, and uses these as arguments to execute. Each normal transition lowers the number $n$ of steps we are allowed to do and increases the number $n$ of steps we have done. Each oracle transition updates $A$, and either lowers $n$ by one, or updates it to the new value $P_M(|f|_A, |w|) - m$, since we have already done $m$ steps. Once we read the final state, the answer is read off the first tape.

For the interpretation, note that the unusual size set of $nnat$ allows us to choose $\mathcal{J}_{\text{minus}}^s = \lambda xy. \max(x-y, 0)$ without losing monotonicity. Hence, in every step execute $F n m z a c$, the value $\max(P_M(\llbracket F \rrbracket^s, \llbracket z \rrbracket^s) + 1 - \llbracket m \rrbracket^s, \llbracket n \rrbracket^s)$ decreases by at least one. Since $\llbracket \Theta^{P_M+1} F; z; a \rrbracket^s = P_M(\llbracket F \rrbracket^s, \llbracket z \rrbracket^s)$ regardless of $a$, we can use this component as part of the interpretation. The full interpretation functions for execute and $F$ are long and complex, so we will not supply them here. They can be found in Appendix B. We will only conclude the other side of Theorem 2:

**Theorem 4.** If $\Psi \in \text{BFF}$, then there exists a finite orthogonal STRS $\mathcal{R}$ such that $F$ computes $\Psi$ in $\mathcal{R}$ and $\mathcal{R}$ admits a polynomially bounded interpretation.
# 6 Conclusions and Future Work

In this paper, we have shown that BFF can be characterized through second-order term rewriting systems admitting polynomially bounded cost–size interpretations. This is arguably the first characterization of the basic feasible functionals purely in terms of rewriting theoretic concepts.

For the purpose of presentation, we have imposed some mild restrictions that we believe are not essential in practice. In future extensions, we can eliminate these restrictions, such as allowing lambda-abstraction, non-base type rules, and higher-order functions (assuming that F is still second-order). We can also allow arbitrary inductive data structures as input.

Another direction we definitely wish to explore is the characterization of polynomial time complexity for functionals of order strictly higher than two. It is well known that the underlying theory in this case becomes less robust than in type-2 complexity. As such, it is not clear which of the existing proposals for complexity classes of higher-order polytime complexity we can hope to capture within our framework.

# References

1. Avanzini, M., Moser, G.: Polynomial path orders. Log. Methods Comput. Sci. 9(4) (2013). https://doi.org/10.2168/LMCS-9(4:9)2013

2. Avanzini, M., Moser, G., Schaper, M.: Tct: Tyrolean complexity tool. In: Chechik, M., Raskin, J. (eds.) Proceedings of TACAS 2016 conference. Lecture Notes in Computer Science, vol. 9636, pp. 407–423. Springer (2016). https://doi.org/10.1007/978-3-662-49674-9_24

3. Baillot, P., Dal Lago, U.: Higher-order interpretations and program complexity. In: Proceedings of CSL 2012. LIPIcs, vol. 16, pp. 62–76. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012). https://doi.org/10.4230/LIPICS.CSL.2012.62, A journal version in Information and Computation (248), 2016

4. Baillot, P., De Benedetti, E., Ronchi Della Rocca, S.: Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Inf. Comput. 261, 55–77 (2018). https://doi.org/10.1016/J.IC.2018.05.005

5. Beame, P., Cook, S.A., Edmonds, J., Impagliazzo, R., Pitassi, T.: The relative complexity of NP search problems. J. Comput. Syst. Sci. 57(1), 3–19 (1998). https://doi.org/10.1006/JCSS.1998.1575

6. Beckmann, A., Weiermann, A.: A term rewriting characterization of the polytime functions and related complexity classes. Arch. Math. Log. 36(1), 11–30 (1996). https://doi.org/10.1007/s001530050054

7. Bellantoni, S.J., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions. Comput. Complex. 2, 97–110 (1992). https://doi.org/10.1007/BF01201998

8. Bonfante, G., Cichon, A., Marion, J., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Funct. Program. 11(1), 33–53 (2001). https://doi.org/10.1017/S0956796800003877

9. Bonfante, G., Marion, J., Moyen, J.: Quasi-interpretations a way to control resources. Theor. Comput. Sci. 412(25), 2776–2796 (2011). https://doi.org/10.1016/j.tcs.2011.02.007
10. Cobham, A.: The intrinsic computational difficulty of functions. In: Bar-Hillel, Y. (ed.) Logic, Methodology and Philosophy of Science: Proceedings of the 1964 International Congress (Studies in Logic and the Foundations of Mathematics), pp. 24–30. North-Holland Publishing (1965)

11. Constable, R.L.: Type two computational complexity. In: Aho, A.V., Borodin, A., Constable, R.L., Floyd, R.W., Harrison, M.A., Karp, R.M., Strong, H.R. (eds.) Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA. pp. 108–121. ACM (1973). https://doi.org/10.1145/800125.804041

12. Dal Lago, U., Hofmann, M.: Realizability models and implicit complexity. Theor. Comput. Sci. 412(20), 2029–2047 (2011). https://doi.org/10.1016/J.TCS.2010.12.025

13. Danner, N., Royer, J.S.: Adventures in time and space. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006. pp. 168–179. ACM (2006). https://doi.org/10.1145/1111037.1111053

14. Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279–301 (1982). https://doi.org/10.1016/0304-3975(82)90026-3

15. Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3452, pp. 301–331. Springer (2004). https://doi.org/10.1007/978-3-540-32275-7_21

16. Hainry, E., Kapron, B.M., Marion, J., Péchoux, R.: A tier-based typed programming language characterizing feasible functionals. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020. pp. 535–549. ACM (2020). https://doi.org/10.1145/3373718.3394768

17. Hainry, E., Kapron, B.M., Marion, J., Péchoux, R.: Complete and tractable machine-independent characterizations of second-order polytime. In: Bouyer, P., Schröder, L. (eds.) Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13242, pp. 368–388. Springer (2022). https://doi.org/10.1007/978-3-030-99253-8_19

18. Hainry, E., Péchoux, R.: Theory of higher order interpretations and application to basic feasible functions. Log. Methods Comput. Sci. 16(4) (2020), https://lmcs.episciences.org/6973

19. Hartmanis, J., Stearns, R.E.: Automata-based computational complexity. Inf. Sci. 1(2), 173–184 (1969). https://doi.org/10.1016/0020-0255(69)90014-0

20. Irwin, R.J., Royer, J.S., Kapron, B.M.: On characterizations of the basic feasible functionals (part i). J. Funct. Program. 11(1), 117–153 (2001). https://doi.org/10.1017/S0956796800003841

21. Kapron, B.M., Cook, S.A.: A new characterization of type-2 feasibility. SIAM J. Comput. 25(1), 117–132 (1996). https://doi.org/10.1137/S0097539794263452

22. Kapron, B.M., Steinberg, F.: Type-two polynomial-time and restricted lookahead. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 579–588. ACM (2018). https://doi.org/10.1145/3209108.3209124
23. Kawamura, A., Cook, S.A.: Complexity theory for operators in analysis. ACM Trans. Comput. Theory 4(2), 5:1–5:24 (2012). https://doi.org/10.1145/2189778.2189780

24. Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey. Theor. Comput. Sci. 121(1&2), 279–308 (1993). https://doi.org/10.1016/0304-3975(93)90091-7

25. Kop, C., Vale, D.: Cost-size semantics for call-by-value higher-order rewriting. In: Proc. FSCD. LIPIcs, vol. 260, pp. 15:1–15:19 (2023). https://doi.org/10.4230/LIPIcs.FSCD.2023.15

26. Kop, C., Vale, D.: Tuple interpretations for higher-order complexity. In: Kobayashi, N. (ed.) 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference). LIPIcs, vol. 195, pp. 31:1–31:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.FSCD.2021.31

27. Kusakari, K.: On proving termination of term rewriting systems with higher-order variables. IPSJ Transactions on Programming 42(SIG 7 (PRO 11)), 35–45 (2001), http://id.nii.ac.jp/1001/00016864/

28. Lankford, D.S.: On proving term rewriting systems are noetherian. Memo MTP-3 (1979), https://www.ens-lyon.fr/LIP/REWRITING/TERMINATION/Lankford_Poly_Term.pdf

29. Leivant, D.: A foundational delineation of computational feasibility. In: Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991. pp. 2–11. IEEE Computer Society (1991). https://doi.org/10.1109/LICS.1991.151625

30. Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science. pp. 789–792 (1970)

31. Mehlhorn, K.: Polynomial and abstract subrecursive classes. J. Comput. Syst. Sci. 12(2), 147–178 (1976). https://doi.org/10.1016/S0022-0000(76)80035-9

32. Oitavem, I.: Implicit characterizations of pspace. In: Kahle, R., Schroeder-Heister, P., Stärk, R.F. (eds.) Proof Theory in Computer Science, International Seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2183, pp. 170–190. Springer (2001). https://doi.org/10.1007/3-540-45504-3_11

33. Terese: Term rewriting systems, Cambridge tracts in theoretical computer science, vol. 55. Cambridge University Press (2003)

## A Innermost Compatibility Theorem for STRSs

In this section, we prove Theorem 1. The program is the same as in [25], with some adaptations to the fact that we do not use lambdas and the cost component is explicit as a $cost'(\cdot)$ function. Recall that in this paper, all rules are of base type, i.e., they are fully applied. Since reduction is innermost, we have that for a rule to be fired, the matching substitution (i.e., the substitution $\gamma$ on the base case $\ell\gamma \to r\gamma$), does not map any variable to a term containing a redex. We restrict to this type of substitutions and notice that $cost'(x\gamma) = 0$ for any variable $x$.

We first make the following observation about our definitions:

**Lemma 9.** For all terms $s t$ with $t$ of base type: $[s t]^s_\alpha = [s]^s([t]^s_\alpha)$ and $[s t]^c_{\alpha, \zeta} = [s]^c([t]^s_\alpha)$ for all $\alpha, \zeta$.
Proof. By an easy case analysis: this holds both if $s = x s_1 \cdots s_n$ and $s = f s_1 \cdots s_k t_1 \cdots t_n$ (since $t$ has base type, all higher-type arguments to $f$ are given). □

Given a valuation $\alpha$ and substitution $\gamma$, we denote the $\gamma$-extention of $\alpha$ by $\alpha^\gamma$; the valuation defined by $\alpha^\gamma(x) = [[x\gamma]]_\alpha^s$. With that in mind we start with some substitution lemmata.

**Lemma 10.** Let $\gamma$ be a substitution mapping all variables to irreducible terms and $\alpha$ be a valuation. Then, for any term $s$, $[[s\gamma]]_\alpha^s = [[s]]_{\alpha^\gamma}^s$.

*Proof.* By induction on the structure of $s$.

* If $s$ is a variable, we have $[[x\gamma]]_\alpha^s = \alpha^\gamma(x) = [[x]]_{\alpha^\gamma}^s$.

* If $s = tu$ is an application, we have

$$ \begin{align*} [[(t u)\gamma]]_\alpha^s &= [[t\gamma]]_\alpha^s ([[u\gamma]]_\alpha^s) \\ &\stackrel{IH}{=} [[t]]_{\alpha^\gamma}^s ([[u]]_{\alpha^\gamma}^s) = [[t u]]_{\alpha^\gamma}^s \end{align*} $$

□

Let us move on to cost versions of substitution lemmata. First, notice that we cannot directly define a $\gamma$-extention for cost valuations. Indeed, $[[\cdot]]_{\alpha, \zeta}^c$ also depends on a size valuation $\alpha$. So given a size valuation $\alpha$, we write $\zeta_\alpha^\gamma$ to denote the valuation $\zeta_\alpha^\gamma = [[\cdot]]_{\alpha, \zeta}^c \circ \gamma$.

**Lemma 11.** Given cost-size valuations $\alpha, \gamma$ and a term $s$ such that both $s$ and all its variables have a type of order at most 1. Then $[[s\gamma]]_{\alpha, \zeta}^c = [[s]]_{\alpha^\gamma, \zeta^\gamma}^c$.

*Proof.* We consider two cases:

* For the first case, we get $s = x s_1 \cdots s_n$, and

* If $n = 0$, we have $[[x\gamma]]_{\alpha, \zeta}^c = \zeta_\alpha^\gamma(x) = [[x]]_{\alpha^\gamma, \zeta^\gamma}^c$ by definition.

* If $n > 0$, we have

$$ \begin{align*} [[(x s_1 \cdots s_n)\gamma]]_{\alpha, \zeta}^c &= [[(x\gamma)(s_1\gamma)\cdots(s_n\gamma)]_{\alpha, \zeta}^c \\ &\stackrel{\text{lemma 9}}{=} [[x\gamma]]_{\alpha, \zeta}^c ([[s_1\gamma]]_\alpha^s, \dots, [[s_n\gamma]]_\alpha^s) \\ &\stackrel{\text{lemma 10}}{=} [[x]]_{\alpha^\gamma, \zeta^\gamma}^c ([[s_1]]_{\alpha^\gamma}^s, \dots, [[s_n]]_{\alpha^\gamma}^s) \\ &= [[(x s_1 \cdots s_n)]_{\alpha^\gamma, \zeta^\gamma}^c \end{align*} $$

* For the second case we have $s = f s_1 \cdots s_k t_1 \cdots t_n$. Recall that we fixed $f : (\vec{\iota}_1 \Rightarrow \kappa_1) \Rightarrow \cdots \Rightarrow (\vec{\iota}_k \Rightarrow \kappa_k) \Rightarrow \nu_1 \Rightarrow \cdots \Rightarrow \nu_l \Rightarrow \iota$ as the general type for $f$. Hence, since we consider $s$ of type order at most 1, $f$ must take at least $k$ arguments, and $0 \le n \le l$.

$$ \begin{align*} [[(f s_1 \cdots s_k t_1 \cdots t_n)\gamma]]_{\alpha, \zeta}^c &= [[f(s_1\gamma)\cdots(s_k\gamma)(t_1\gamma)\cdots(t_n\gamma)]_{\alpha, \zeta}^c \\ &= \mathcal{J}_f(\llbracket [s_1\gamma]_{\alpha, \zeta}^c, [s_1\gamma]_\alpha^s, \dots, [s_k\gamma]_{\alpha, \zeta}^c, [s_k\gamma]_\alpha^s, [t_1\gamma]_\alpha^s, \dots, [t_n\gamma]_\alpha^s \rrbracket) \\ &\stackrel{IH}{=} \mathcal{J}_f(\llbracket [s_1]_{\alpha^\gamma, \zeta^\gamma}^c, [s_1]_{\alpha^\gamma}^s, \dots, [s_k]_{\alpha^\gamma, \zeta^\gamma}^c, [s_k]_{\alpha^\gamma}^s, [t_1]_{\alpha^\gamma}^s, \dots, [t_n]_{\alpha^\gamma}^s \rrbracket) \\ &= [[f s_1 \cdots s_k t_1 \cdots t_n]]_{\alpha^\gamma, \zeta^\gamma}^c \end{align*} $$
□

Next, we connect the relationship between the two cost functions we defined.

**Lemma 12.** For any term $s: \iota$ so that both $s$ and all its variables have type order 0 or 1, and any normalized substitution $\gamma$, we have that $\text{cost}(s)_{\alpha\gamma,\zeta\gamma} \ge \text{cost}'(s\gamma)_{\alpha,\zeta}$.

*Proof.* We again consider two cases:

* For the first case, let $s = x s_1 \dots s_n$. If $n = 0$ then $\text{cost}(x)_{\alpha\gamma,\zeta\gamma} = 0$ by definition, and since we assumed that $\gamma$ is normalized, also $\text{cost}'(x\gamma)_{\alpha,\zeta} = 0$. If $n > 0$ and $s$ has base type, then $\text{cost}(s)_{\alpha\gamma,\zeta\gamma} = \zeta\gamma(x)(\llbracket s_1 \rrbracket^s_{\alpha\gamma,\zeta\gamma}, \dots, \llbracket s_n \rrbracket^s_{\alpha\gamma,\zeta\gamma}) + \sum_{i=1}^n \text{cost}(s_i)_{\alpha\gamma,\zeta\gamma} = \llbracket \gamma(x) \rrbracket^c_{\alpha,\zeta}(\llbracket s_1\gamma \rrbracket^s_{\alpha}, \dots, \llbracket s_n\gamma \rrbracket^s_{\alpha}) + \sum_{i=1}^n \text{cost}(s_i)_{\alpha\gamma,\zeta\gamma}$ by Lemmas 10 and 11, which by Lemma 9 and the induction hypothesis $\ge \llbracket (x\gamma)(s_1\gamma) \dots (s_n\gamma) \rrbracket^c + \sum_{i=1}^n \text{cost}'(s_i\gamma)_{\alpha,\zeta}$. Since $x\gamma$ is in normal form, either this is exactly $\text{cost}'(s\gamma)$, or $\text{cost}'(s\gamma) = 0$ and we are done regardless. If $n > 0$ and $s$ does not have base type, we complete quickly with the induction hypothesis.

* For the second case, let $s = f s_1 \dots s_k t_1 \dots t_n$. We have two cases whether $s\gamma$ is in normal form or not. In the first case, $\text{cost}'(s\gamma)_{\alpha,\zeta} = 0$ and certainly $\text{cost}(s)_{\alpha\gamma,\zeta\gamma} \ge 0$. For the second case, $s$ is not in normal form. If $s$ has base type, then:

$$ \begin{align*} \text{cost}(s)_{\alpha\gamma,\zeta\gamma} &= \text{cost}(f s_1 \dots s_k t_1 \dots t_n)_{\alpha\gamma,\zeta\gamma} \\ &= \llbracket s \rrbracket^c_{\alpha\gamma,\zeta\gamma} + \sum_{i=1}^k \text{cost}(s_i)_{\alpha\gamma,\zeta\gamma} + \sum_{j=1}^n \text{cost}(s_j)_{\alpha\gamma,\zeta\gamma} \\ &\stackrel{\text{lemma 11}}{=} \llbracket s\gamma \rrbracket^c_{\alpha,\zeta} + \sum_{i=1}^k \text{cost}(s_i)_{\alpha\gamma,\zeta\gamma} + \sum_{j=1}^n \text{cost}(s_j)_{\alpha\gamma,\zeta\gamma} \\ &\ge \sum_{i=1}^k \text{cost}'(s_i\gamma)_{\alpha,\zeta} + \sum_{j=1}^n \text{cost}'(s_j\gamma)_{\alpha,\zeta} \\ &= \text{cost}'(s\gamma)_{\alpha,\zeta} \end{align*} $$

If not, then:

$$ \begin{align*} \text{cost}(s)_{\alpha\gamma,\zeta\gamma} &= \sum_{i=1}^{k} \text{cost}(s_i)_{\alpha\gamma,\zeta\gamma} + \sum_{j=1}^{n} \text{cost}(s_j)_{\alpha\gamma,\zeta\gamma} \\ &\ge \sum_{i=1}^{k} \text{cost}'(s_i\gamma)_{\alpha,\zeta} + \sum_{j=1}^{n} \text{cost}'(s_j\gamma)_{\alpha,\zeta} \\ &= \text{cost}'(s\gamma)_{\alpha,\zeta} \end{align*} $$

□

The lemma below is restricted to type-1 terms and we assume that size compatibility holds. This lemma is only needed in one specific step of the inductive step of Theorem 1.
**Lemma 13.** Let $(\mathbb{F}, \mathcal{R})$ be a STRS satisfying the compatibility conditions of Theorem 1 and $s, t$ be type-1 terms of the same type. Assume that $[[s]]_{\alpha}^{\mathcal{S}} \supseteq [[t]]_{\alpha}^{\mathcal{S}}$. Then $[[s]]_{\alpha, \zeta}^{\mathcal{C}} \geq [[t]]_{\alpha, \zeta}^{\mathcal{C}}$ whenever $s \to_{\mathbb{R}} t$.

*Proof.* The proof is by induction on $s \to_{\mathbb{R}} t$.

* For the base case we get:

$$ \begin{aligned} [[\ell\gamma]]_{\alpha, \zeta}^{\mathcal{C}} &= [[\ell]]_{\alpha^{\gamma}, \zeta^{\gamma}}^{\mathcal{C}} \\ &> \mathrm{cost}(r)_{\alpha^{\gamma}, \zeta^{\gamma}}, \text{ by compatibility} \\ &= [[r]]_{\alpha^{\gamma}, \zeta^{\gamma}}^{\mathcal{C}} + \sum [[t]]_{\alpha^{\gamma}, \zeta^{\gamma}}^{\mathcal{C}}, \text{ where } r \supseteq t_i \\ &\geq [[r]]_{\alpha^{\gamma}, \zeta^{\gamma}}^{\mathcal{C}} = [[r\gamma]]_{\alpha, \zeta}^{\mathcal{C}} \text{ by lemma 11} \end{aligned} $$

* For the second part, we recall that to get a type-1 term of arrow type, we need to partially apply a function symbol or a variable, and since rules are of base type, reduction does not occur at head position in $s$. Then we get two cases:

* First, $s = x s_1 \dots s_n$, and assume w.l.g that $x : t_1 \Rightarrow \dots \Rightarrow t_k \Rightarrow \kappa$ and $n < k$. So we get $x s_1 \dots s_i \dots s_n \to_{\mathbb{R}} x s_1 \dots s_i \dots s_n$ with $s_i \to_{\mathbb{R}} s'_i$.

$$ \begin{aligned} [[x s_1 \dots s_i \dots s_n]]_{\alpha, \zeta}^{\mathcal{C}} &= \zeta(x)([[s_1]]_{\alpha}^{\mathcal{S}}, \dots, [[s_i]]_{\alpha}^{\mathcal{S}}, \dots, [[s_n]]_{\alpha}^{\mathcal{S}}) \\ &\supseteq \zeta(x)([[s_1]]_{\alpha}^{\mathcal{S}}, \dots, [[s'_i]]_{\alpha}^{\mathcal{S}}, \dots, [[s_n]]_{\alpha}^{\mathcal{S}}) \\ &= [[x s_1 \dots s'_i \dots s_n]]_{\alpha, \zeta}^{\mathcal{C}} \end{aligned} $$

* The case for $f s_1 \dots s_i \dots s_n$ is similar to the variable one, with the observation that by assumption $[[s_i]]_{\alpha}^{\mathcal{S}} \supseteq [[s'_i]]_{\alpha}^{\mathcal{S}}$ holds. Then we use the monotonicity of $\mathcal{J}_f^{\mathcal{S}}$.

□

Finally, we can state and prove the innermost compatibility theorem.

**Theorem 1 (Innermost Compatibility).** Suppose $\mathcal{R}$ is an STRS compatible with a cost-size interpretation $\mathcal{F}$, then for any valuations $\alpha$ and $\zeta$ we have $\mathrm{cost}'(s)_{\alpha, \zeta} > \mathrm{cost}'(t)_{\alpha, \zeta}$ and $[[s]]_{\alpha}^{\mathcal{S}} \supseteq [[t]]_{\alpha}^{\mathcal{S}}$ whenever $s \to_{\mathbb{R}} t$.

*Proof.* The proof follows by induction on the reduction $s \to_{\mathbb{R}} t$.

**Size Case.**

* In the base case, we have $s \to_{\mathbb{R}} t$ by $\ell\gamma \to r\gamma$. Then we combine the substitution lemma with the compatibility requirement for size, i.e., $[[\ell]]_{\alpha}^{\mathcal{S}} \supseteq [[r]]_{\alpha}^{\mathcal{S}}$, as follows:

$$ [[\ell\gamma]]_{\alpha}^{\mathcal{S}} = [[\ell]]_{\alpha^{\gamma}}^{\mathcal{S}} \supseteq [[r]]_{\alpha^{\gamma}}^{\mathcal{S}} = [[r\gamma]]_{\alpha}^{\mathcal{S}} $$

* In the application case, we simply apply the induction hypothesis and the fact that in $[[s t]]^{\mathcal{S}} = [[s]]^{\mathcal{S}}([[[t]]^{\mathcal{S}}])$, the function $[[s]]^{\mathcal{S}}$ is weakly monotonic.

**Cost Case.**
* For the base case, we have that

$$ \mathrm{cost}'(\ell\gamma)_{\alpha,\zeta} = [[\ell\gamma]]_{\zeta}^{\mathrm{c}} = [[\ell]]_{\zeta}^{\mathrm{c}} > \mathrm{cost}(r)_{\alpha\gamma,\zeta} \geq \mathrm{cost}'(r\gamma)_{\alpha,\zeta} $$

* For the application case with a variable root symbol, we have that $xt_1...t_i...t_n \to_R xt_1...t'_i...t_n$ with $t_i \to_R t'_i$. By induction we get $\mathrm{cost}'(t_i) > \mathrm{cost}'(t'_i)$ and also use the size part $[[t_i]]^s \supseteq [[t'_i]]^s$. Then:

$$ \begin{aligned} \mathrm{cost}'(xt_1...t_i...t_n)_{\alpha,\zeta} &= [[xt_1...t_i...t_n]]_{\alpha,\zeta}^{\mathrm{c}} + \sum_{j=1}^{n} \mathrm{cost}'(t_j)_{\alpha,\zeta} \\ &= \zeta(x)([[s_1]]_{\alpha}^{\mathrm{s}}, [[s_i]]_{\alpha}^{\mathrm{s}}, [[s_n]]_{\alpha}^{\mathrm{s}}) + \sum_{\substack{j=1...n \\ j \neq i}} \mathrm{cost}'(t_j)_{\alpha,\zeta} + \mathrm{cost}'(t_i)_{\alpha,\zeta} \\ &\geq \zeta(x)([[s_1]]_{\alpha}^{\mathrm{s}}, [[s'_i]]_{\alpha}^{\mathrm{s}}, [[s_n]]_{\alpha}^{\mathrm{s}}) + \sum_{\substack{j=1...n \\ j \neq i}} \mathrm{cost}'(t_j)_{\alpha,\zeta} + \mathrm{cost}'(t_i)_{\alpha,\zeta}, \\ &> \zeta(x)([[s_1]]_{\alpha}^{\mathrm{s}}, [[s'_i]]_{\alpha}^{\mathrm{s}}, [[s_n]]_{\alpha}^{\mathrm{s}}) + \sum_{\substack{j=1...n \\ j \neq i}} \mathrm{cost}'(t_j)_{\alpha,\zeta} + \mathrm{cost}'(t'_i)_{\alpha,\zeta} \\ &= \mathrm{cost}'(xt_1...t'_i...t_n)_{\alpha,\zeta} \end{aligned} $$

* For the application case with a function root symbol where the reduction is done in a base-type argument, we have that $f s_1...s_k t_1...t_i...t_n \to_R f s_1...s_k t_1...t'_i...t_n$ with $t_i \to_R t'_i$. Let us write $\vec{s}$ for $s_1...s_k$ and $c(s)$ for $\sum_{j=1}^k \mathrm{cost}'(s_i)_{\alpha,\zeta}$ below. We also abuse notation and write $[[\vec{s}]]_{\alpha,\zeta}^{\mathrm{c}}$, $[[\vec{s}]]_{\alpha}^{\mathrm{s}}$ for $[[s_1]]_{\alpha,\zeta}^{\mathrm{c}}$, $[[s_1]]_{\alpha}^{\mathrm{s}}$, $[[s_k]]_{\alpha,\zeta}^{\mathrm{c}}$, $[[s_k]]_{\alpha}^{\mathrm{s}}$.

$$ \begin{aligned} \mathrm{cost}'(f \vec{s} t_1 \dots t_i \dots t_n) &= [[f \vec{s} t_1 \dots t_i \dots t_n]]_{\alpha, \zeta}^{\mathrm{c}} + c(s) + \sum_{j=1}^{n} \mathrm{cost}'(t_j)_{\alpha, \zeta} \\ &= \mathcal{J}_f^{\mathrm{c}}([[\vec{s}]]_{\alpha, \zeta}^{\mathrm{c}}, [[\vec{s}]]_{\alpha}^{\mathrm{s}}, [[t_1]]_{\alpha}^{\mathrm{s}}, \dots, [[t_i]]_{\alpha}^{\mathrm{s}}, \dots, [[t_n]]_{\alpha}^{\mathrm{s}}) + c(s) + \sum_{j=1}^{n} \mathrm{cost}'(t_j)_{\alpha, \zeta} \\ &\geq \mathcal{J}_f^{\mathrm{c}}([[\vec{s}]]_{\alpha, \zeta}^{\mathrm{c}}, [[\vec{s}]]_{\alpha}^{\mathrm{s}}, [[t_1]]_{\alpha}^{\mathrm{s}}, \dots, [[t'_i]]_{\alpha}^{\mathrm{s}}, \dots, [[t_n]]_{\alpha}^{\mathrm{s}}) + c(s) + \sum_{j=1}^{n} \mathrm{cost}'(t_j)_{\alpha, \zeta} \\ &> \mathrm{cost}'(f \vec{s} t_1 \dots t'_i \dots t_n) \end{aligned} $$

where in the last step we use $\mathrm{cost}'(t_i) > \mathrm{cost}'(t'_i)$, given by the IH.

* For the application case with a function root symbol where the reduction is done in a higher-type argument, we have that $f s_1...s_i...s_k t_1...t_n \to_R f s_1...s'_i...s'_k t_1...t_n$ with $s_i \to_R s'_i$. Recall that by IH we get $\mathrm{cost}'(s_i) > \mathrm{cost}'(t'_i)$.
cost'(s'_i). Also, s_i is a type-1 term and here we are under the compatibil-
ity conditions and [[s_i]]^s &sqsubseteq; [[s'_i]]^s is valid by the size part of the theorem.
Hence the conditions of Lemma 13 are satisfied, so we get [[s_i]]^c &ge; [[s'_i]]^c,
as well.

With this in hand we reason as follows:

$$
\begin{align*}
\operatorname{cost}'(\operatorname{f} s_1 \dots s_i \dots s_k \, \vec{t})_{\alpha, \zeta} \\
&= \mathcal{J}_{\mathrm{f}}^{\mathrm{c}}(\llbracket s_1 \rrbracket_{\alpha, \zeta}^{\mathrm{c}}, \llbracket s_1 \rrbracket_{\alpha}^{\mathrm{s}}, \dots, \llbracket s_i \rrbracket_{\alpha, \zeta}^{\mathrm{c}}, \llbracket s_i \rrbracket_{\alpha}^{\mathrm{s}}, \dots, \llbracket s_k \rrbracket_{\alpha, \zeta}^{\mathrm{c}}, \llbracket s_k \rrbracket_{\alpha}^{\mathrm{s}}, \llbracket \vec{t} \rrbracket_{\alpha}^{\mathrm{s}}) \\
&\quad + \sum_{j=1 \dots k, j \neq i} \operatorname{cost}'(s_j) + \operatorname{cost}'(s_i) + \sum_{j=1}^{n} \operatorname{cost}'(t_j)
\end{align*}
$$

$$
\begin{align*}
& \text{by monotonicity of } \mathcal{J}_{\mathrm{f}}^{\mathrm{c}} \text{ and } [[s_i]]^{\mathrm{c}} \ge [[s'_i]]^{\mathrm{c}}, [[s_i]]^{\mathrm{s}} \supseteq [[s'_i]]^{\mathrm{s}}, \text{ we get} \\
& \ge \mathcal{J}_{\mathrm{f}}^{\mathrm{c}}(\llbracket s_1 \rrbracket_{\alpha, \zeta}^{\mathrm{c}}, \llbracket s_1 \rrbracket_{\alpha}^{\mathrm{s}}, \dots, \llbracket s'_i \rrbracket_{\alpha, \zeta}^{\mathrm{c}}, \llbracket s'_i \rrbracket_{\alpha}^{\mathrm{s}}, \dots, \llbracket s_k \rrbracket_{\alpha, \zeta}^{\mathrm{c}}, \llbracket s_k \rrbracket_{\alpha}^{\mathrm{s}}, \llbracket \vec{t} \rrbracket_{\alpha}^{\mathrm{s}}) \\
& \quad + \sum_{j=1 \dots k, j \neq i} \mathrm{cost}'(s_j) + \mathrm{cost}'(s_i) + \sum_{j=1}^{n} \mathrm{cost}'(t_j) \\
& > \mathcal{J}_{\mathrm{f}}^{\mathrm{c}}(\llbracket s_1 \rrbracket_{\alpha, \zeta}^{\mathrm{c}}, \llbracket s_1 \rrbracket_{\alpha}^{\mathrm{s}}, \dots, \llbracket s'_i \rrbracket_{\alpha, \zeta}^{\mathrm{c}}, \llbracket s'_i \rrbracket_{\alpha}^{\mathrm{s}}, \dots, \llbracket s_k \rrbracket_{\alpha, \zeta}^{\mathrm{c}}, \llbracket s_k \rrbracket_{\alpha}^{\mathrm{s}}, \llbracket \vec{t} \rrbracket_{\alpha}^{\mathrm{s}}) \\
& \quad + \sum_{j=1 \dots k, j \neq i} \mathrm{cost}'(s_j) + \mathrm{cost}'(s'_i) + \sum_{j=1}^{n} \mathrm{cost}'(t_j) \\
& = \mathrm{cost}'(\operatorname{f} s_1 \dots s'_i \dots s_k \, \vec{t})_{\alpha, \zeta}
\end{align*}
$$

B Interpretations for Section 5

B.1 Interpretations for section 5.3

The omitted interpretation functions in section 5.3 are:

$$
\begin{align*}
\mathcal{J}_{\text{len}}^{\text{s}} &= \boldsymbol{\lambda} x.x & \mathcal{J}_{\text{len}}^{\text{c}} &= \boldsymbol{\lambda} x.x + 1 \\
\mathcal{J}_{\text{max}}^{\text{s}} &= \boldsymbol{\lambda} nm. \max(n, m) & \mathcal{J}_{\text{max}}^{\text{c}} &= \boldsymbol{\lambda} nm.n + 1 \\
\mathcal{J}_{\text{limit}}^{\text{s}} &= \boldsymbol{\lambda} xn.n & \mathcal{J}_{\text{limit}}^{\text{c}} &= \boldsymbol{\lambda} xn.n + 1 \\
\mathcal{J}_{\text{retif}}^{\text{s}} &= \boldsymbol{\lambda} xnz.z & \mathcal{J}_{\text{retif}}^{\text{c}} &= \boldsymbol{\lambda} xnz.n + 1
\end{align*}
$$

It is easy to see that the corresponding rules are all oriented.

For tryapply, note that tryapply F a ⌜n⌝ reduces to ⌜|F(a)|⌝ if |a| ≤ n, and to
⌝0⌝ otherwise. Thus, it indeed returns exactly |F|_{\{a\}}(n).

$$
\mathcal{J}_{\text{tryapply}}^{\text{s}} = \lambda F \text{an.} F(n) \qquad \mathcal{J}_{\text{tryapply}}^{\text{c}} = \lambda F^{\text{c}} F^{\text{s}} \text{an.} F^{\text{c}}(n) + F^{\text{s}}(n) + 2 * n + 4
$$

We easily see that [[tryapply a n]]^s = [[len (retif a n (F (limit a n))))]^s. As for the cost,
note that

$$
\begin{align*}
\operatorname{cost}(\operatorname{len}(\operatorname{retif} a n (F (\operatorname{limit} a n)))) \\
&= \llbracket \operatorname{len}(\operatorname{retif} a n (F (\operatorname{limit} a n))) \rrbracket^c + \llbracket \operatorname{retif} a n (F (\operatorname{limit} a n)) \rrbracket^c + \\
&\quad \llbracket F (\operatorname{limit} a n) \rrbracket^c + \llbracket \operatorname{limit} a n \rrbracket^c \\
&= (F^c(n) + 1) + (n + 1) + F^s(n) + (n + 1) = F^c(n) + F^s(n) + 2n + 3
\end{align*}
$$
Hence, also the tryapply rule is oriented.

To interpret sets and the apply rule, we use:

$$ 
\begin{align*}
\mathcal{J}_{\emptyset}^{s} &= 0 & \mathcal{J}_{\emptyset}^{c} &= 0 & \mathcal{J}_{\text{setcons}}^{s} &= \lambda xy.y + 1 & \mathcal{J}_{\text{setcons}}^{s} &= \lambda xy.0 \\
\mathcal{J}_{\text{tryall}}^{s} &= \lambda F \text{an.} F(n) & & & & & \\
\mathcal{J}_{\text{tryall}}^{c} &= \lambda F^{c} F^{s} \text{an.} 1 + a * (F^{c}(n) + 2 * F^{s}(n) + 2 * n + 6) & & & & &
\end{align*}
$$

To see that the rule is oriented, note:

$$ 
\begin{align*}
\llbracket \text{tryall } F \ (\text{setcons } a \ tl) \ n \rrbracket^s &= F^s(n) \\
&= \max(F^s(n), F^s(n)) \\
&= \llbracket \max(\text{tryapply } F \ an) \ (\text{tryall } F \ tl \ n) \rrbracket^s
\end{align*}
$$

and

$$ 
\begin{align*}
& \llbracket \text{tryall } F \ (\text{setcons } a \ tl) \ n \rrbracket^c \\
&= 1 + (tl + 1) * (F^c(n) + 2 * F^s(n) + 2 * n + 6) \\
&= 1 + tl * (F^c(n) + 2 * F^s(n) + 2 * n + 6) \\
&\quad + 1 * (F^c(n) + 2 * F^s(n) + 2 * n + 6) \\
&= \llbracket \text{tryall } F \ tl \ n \rrbracket^c + (F^c(n) + 2 * F^s(n) + 2 * n + 6) \\
&= \llbracket \text{tryall } F \ tl \ n \rrbracket^c + \llbracket \text{tryapply } F \ an \rrbracket^c + F^s(n) + 2 \\
&= \llbracket \text{tryall } F \ tl \ n \rrbracket^c + \llbracket \text{tryapply } F \ an \rrbracket^c + \llbracket \max(\text{tryapply } F \ an) \ (\text{tryall } F \ tl \ n) \rrbracket^c + 1 \\
&> \text{cost}(\max(\text{tryapply } F \ an) \ (\text{tryall } F \ tl \ n))
\end{align*}
$$

## B.2 Interpretations for section 5.4

We first supply the interpretation functions for the nnat symbols and the two simple rules:

$$ 
\begin{align*}
\mathcal{J}_{\text{o}}^{s} &= 0 & \mathcal{J}_{\text{o}}^{c} &= 0 \\
\mathcal{J}_{\text{n}}^{s} &= \lambda x.x + 1 & \mathcal{J}_{\text{n}}^{c} &= \lambda x.0 \\
\mathcal{J}_{\text{extract}}^{s} &= \lambda x.x & \mathcal{J}_{\text{extract}}^{c} &= \lambda x.x + 2 \\
\mathcal{J}_{\text{minus}}^{s} &= \lambda xy. \max(x - y, 0) & & & & \\
\mathcal{J}_{\text{minus}}^{c} &= \lambda xy.x & & & &
\end{align*}
$$

These functions are all monotonic, and their rules are oriented (as can easily be checked).

By induction on the polynomial $P$, we can find polynomials $A_P, B_P$ such that $\text{cost}(\Theta_{F;z;a}^P) \le \llbracket a \rrbracket^s * A_P(F^c, F^s, \llbracket z \rrbracket^s) + B_P(F^c, F^s, \llbracket z \rrbracket^s)$, assuming $F, z$ and $a$ are in normal form.

To define our remaining interpretation functions, first let:

* $\theta_{F,z,n,m} := \max(P_M(F^s, z) + 1 - m, n)$

* $\text{POLY}_{F,z}[x] := x * A_{P_M+1}(F^c, F^s, \llbracket z \rrbracket^s) + B_{P_M+1}(F^c, F^s, \llbracket z \rrbracket^s)$, so the polynomial bounding $\text{cost}(\Theta_{F;z;a}^{P_M+1})$ if $\llbracket a \rrbracket^s = x$.
Then, we can orient the size interpretations of the rewrite rules by the following interpretation:

$$ \mathcal{J}_{F}^{s} = \lambda Fn.n + P_{M}(F, n) + 1 $$

$$ \mathcal{J}_{F'}^{s} = \lambda Fzc.c + P_{M}(F, z) + 1 $$

$$ \mathcal{J}_{execute}^{s} = \lambda Fnmzac.c + \theta_{F,z,n,m} $$

$$ \mathcal{J}_{execute'}^{s} = \lambda Fnmzac.c + 1 + \theta_{F,z,n,m} $$

And the cost interpretations by:

$$ \begin{aligned} \mathcal{J}_{F}^{c} = \lambda Fn.(P_{M}(F^{s}, n) + 1) * ( & 8 + 3 * P_{M}(F^{s}, n) + 2 * n + F^{c}(P_{M}(F^{s}, n) + n + 1) + \\ & \text{POLY}_{F,z}[P_{M}(F^{s}, n) + 1] \\ & + 6 + 2 * n + \text{POLY}_{F,z}[0] \end{aligned} $$

$$ \begin{aligned} \mathcal{J}_{F'}^{c} = \lambda Fzc.(P_{M}(F^{s}, z) + 1) * ( & 8 + 3 * P_{M}(F^{s}, z) + 2 * c + F^{c}(P_{M}(F^{s}, z) + 1 + c) + \\ & \text{POLY}_{F,z}[P_{M}(F^{s}, z) + 1] \\ & + 4 + c + \text{POLY}_{F,z}[0] \end{aligned} $$

$$ \begin{aligned} \mathcal{J}_{execute}^{c} = \lambda Fnmzac.\theta_{F,z,n,m} * ( & 5 + 2 * (\theta_{F,z,n,m} + c) + F^{c}(\theta_{F,z,n,m} + c) + \\ & \text{POLY}_{F,z}[\theta_{F,z,n,m} + a] + P_{M}(F^{s}, z) \\ & + 3 + \theta_{F,z,n,m} + c \end{aligned} $$

$$ \begin{aligned} \mathcal{J}_{execute'}^{c} = \lambda Fnmzac.(\theta_{F,z,n,m} + 1) * ( & 5 + 2 * (\theta_{F,z,n,m} + c + 1) + F^{c}(\theta_{F,z,n,m} + c + 1) + \\ & \text{POLY}_{F,z}[\theta_{F,z,n,m} + a] + P_{M}(F^{s}, z) \\ & + 1 \end{aligned} $$

To see that these interpretations are correct, we first observe:

$$ \begin{aligned} \theta_{F,z,s,n,m} &= \max(P_{M}(F^{s}, z) + 1 - m, n + 1) \\ &= \max(P_{M}(F^{s}, z) + 1 - (m + 1), n) + 1 \\ &= \theta_{F,z,n,m+1} + 1 \end{aligned} $$

(Because $\max(a + 1, b + 1) = \max(a, b) + 1$.) We also have, for all a:

$$ \begin{aligned} \theta_{F,z,n,m} &= \max(P_{M}(F^{s}, z) + 1 - m, n) \\ &\geq \max(P_{M}(F^{s}, z) + 1 - m, 0) \\ &= \max(P_{M}(F^{s}, z) + 1 - m, \max(P_{M}(F^{s}, z) + 1 - m, 0)) \\ &= \theta_{F,z, \llbracket \text{minus } \theta_{F,z;m}^{P_{M}+1} \rrbracket^{s}, m} \end{aligned} $$

The inequalities now follow by writing out definitions.