<figure><img src="image_1.png" /></figure>

HAL
open science

# A Characterization of Basic Feasible Functionals
Through Higher-Order Rewriting and Tuple
Interpretations

Patrick Baillot, Ugo Dal Lago, Cynthia Kop, Deivid Vale

► To cite this version:

Patrick Baillot, Ugo Dal Lago, Cynthia Kop, Deivid Vale. A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations. Logical Methods in Computer Science, In press. hal-05343191

HAL Id: hal-05343191

https://hal.science/hal-05343191v1

Submitted on 3 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A CHARACTERIZATION OF BASIC FEASIBLE FUNCTIONALS THROUGH HIGHER-ORDER REWRITING AND TUPLE INTERPRETATIONS

PATRICK BAILLOT ⚫<sup>a</sup>, UGO DAL LAGO ⚫<sup>b</sup>, CYNTHIA KOP ⚫<sup>c</sup>, AND DEIVID VALE ⚫<sup>c</sup>

**ABSTRACT.** The class of type-two basic feasible functionals ($BFF_2$) is the analogue of FP (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. $BFF_2$ 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_2$ 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 tuple interpretations for higher-order term rewriting and see second order rewriting as ways of computing type-2 functionals. We then prove that the class of functionals represented by higher-order terms admitting polynomially bounded cost-size interpretations exactly corresponds to $BFF_2$.

## 1. INTRODUCTION

Computational complexity classes — and in particular those relating to polynomial time and space [HS69, Cob65] — 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 [BC92, Lei91, Oit01, DLH11, BDBRDR18] fits into this picture, and is concerned

*Key words and phrases:* Basic Feasible Functions; Higher-Order Term Rewriting; Tuple Interpretation; Implicit Computational Complexity.

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.

<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /></figure>

<footnote><sup>a</sup> Univ. Lille, CNRS, Inria, Centrale Lille, UMR 9189 CRISTAL, F-59000 Lille, France
*e-mail address:* patrick.baillot@univ-lille.fr</footnote>

<footnote><sup>b</sup> Università di Bologna, Inria
*e-mail address:* ugo.dallago@unibo.it</footnote>

<footnote><sup>c</sup> Radboud University Nijmegen
*e-mail address:* c.kop@cs.ru.nl, deividvale@cs.ru.nl</footnote>
with characterizations of complexity classes based on tools from mathematical logic and the
theory of programming languages.

One of the areas involved in this investigation is certainly that of term rewriting [Ter03],
which has proved useful as a tool for the characterization of complexity classes. In particular,
the class FP (i.e., of first-order functions computable in polynomial time) has been character-
ized through variations of techniques originally introduced for termination, e.g., the interpre-
tation method [MN70, Lan79], path orders [Der82], or dependency pairs [GTS04]. Some ex-
amples of such characterizations can be found in [BW96, BCMT01, BMM11, AM13, BDL12].

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 [Con73], Mehlhorn [Meh76],
and Kapron and Cook [KC96] 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 for instance in computable analysis [KC12], NP search problems [BCE+98], and
programming language theory [DR06].

There have been several proposals for a class of type-2 functionals that generalizes
FP. However, the most widely accepted one is the class BFF₂ of *type-two 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 [IRK01, DR06], typed imperative languages [HKMP20, HKMP22], and restricted
forms of iteration in OTMs [KS18].

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 [KvOvR93].

This paper goes precisely in this direction by showing that the interpretation method in
the form studied by Kop and Vale [KV21, KV23] provides the right tools to characterize BFF₂.
More precisely, we consider a class of higher-order rewrite 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 [BCMT01]
because BFF₂ crucially relies on some conditions both on *size* and on *time*. 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., [AMS16].

**Contributions.** We consider simply-typed term rewriting systems (STRS for short) with
partial application but no $\lambda$-abstraction. The contributions of this paper are as follows.

* We provide a compatibility theorem for cost-size interpretations of STRSs with respect to innermost reduction, whose proof is simpler than that of [KV23]; this captures the fact that cost-size interpretations provide safe upper bounds on the length of reduction sequences, and that the size interpretation of a term cannot increase.
* We propose a natural definition of computation of type-2 functionals by an STRS, which can be of more general interest than the specific characterization of the class BFF₂ that we focus on in this paper; this is purely operational in nature and revolves around the use of rewrite rules modeling calls for an “oracle”. This notion of computation is, intuitively, a rewriting counterpart for oracle Turing machines.

* We prove a soundness result, stating that any (orthogonal) STRS with a polynomially bounded cost-size interpretation computes a type-2 functional in BFF₂; this proof uses, in particular, a term-graph rewriting argument.

* Conversely, we define an encoding of polynomial time Oracle Turing Machines in an STRS which shows that any type-2 functional in BFF₂ can be computed by an STRS with a polynomially bounded cost-size interpretation.

**Related Work.** We describe here some related work about the topics addressed by this paper, namely implicit computational complexity, higher-order complexity classes, higher-order rewriting systems, and interpretations.

Implicit computational complexity refers to a line of work aiming at characterizing complexity classes without reference to machine models and explicit bounds on resources, but instead by relying on logical systems and programming language restrictions. It goes back to early work by Leivant [Lei91] and Bellantoni and Cook [BC92] and has used various methods coming in particular from recursion theory [LM94, Oit01], programming language restrictions [Jon01, KS17], linear logic [Gir98, Laf04, Bai11] and type systems [Hof03, LS16]. In the setting of term-rewriting it has taken advantage of contributions in the area of polynomial interpretations [BCMT98] and has provided a variety of characterizations for first-order complexity classes such as FP and PSPACE [MM00, BMM05, BW96, BCMT01, BMM11, AM13, BLM12].

The class of Basic Feasible Functionals BFF was introduced by Cook and Kapron [CK89] by means of bounded typed loop programs, and they showed that its type-2 restriction BFF₂ coincides with a class that had been defined by Melhorn [Meh76]. They later provided a machine characterization of type-2 BFF₂ by polynomial time Oracle Turing Machines (OTM) [KC91, KC96] which gave more confidence in the naturalness of this class. Several works then provided alternative characterizations of BFF₂, in particular by restricted recursion schemes in some functional languages [IRK01, DR06], or typed imperative languages with insights coming from non-interference analysis [HKMP20, HKMP22], or by restricted forms of iteration in OTMs [KS18].

Higher-order interpretations have been introduced and investigated in [vdP96] in relation to termination issues but not to complexity classes. In [BDL12, BL16] a notion of higher-order polynomial interpretations was proposed which allowed to provide a characterization of the (first-order) class FP of polynomial time computable functions. However, the codomain considered was the domain $\mathbb{N}$ of natural numbers, not tuples, and this approach did not consider higher-order complexity. An investigation of higher-order complexity classes employing the higher-order interpretation method in the context of a pure higher-order functional language was proposed in [HP20]. However, this paper did not provide a characterization of the standard BFF₂ class. Instead, it characterized 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 [HP20]). Another related line of work is that of [FHHP15]: the authors consider a first order functional stream language, which allows to implement second order functionals and they study (first-order) interpretations for this
language. In this way they define a subclass of $BFF_2$ but do not characterize $BFF_2$ itself. Closer to the present work, the paper [KV21] introduced the notion of tuple interpretation for higher-order rewriting systems and in particular the cost-size interpretations that we use here. Then [KV23] adapted this notion to the weak call-by-value strategy, which allowed for tighter bounds but also relaxed the approach by separating the cost and the size components.

**Publication History.** This paper is a revised and extended version of [BLKV24]. This version contains detailed proofs of the results and additional examples, which previously could not be added due to space constraints. The results in this paper appear in monograph form in the last author's PhD thesis [Val24, Chapter 6].

**Outline of the Paper.** The paper is organized as follows. We first provide some background on higher-order rewriting and simply typed term-rewriting system (STRS), and on type-two complexity (Section 2). We then recall the definition of cost-size interpretations and prove a compatibility theorem for cost-size interpretations of STRSs with respect to innermost reduction (Section 3). In Section 4 we state the main theorem of this paper, which says that the STRSs with polynomially bounded cost-size interpretations exactly characterize the $BFF_2$ functionals. Section 5 is devoted to the proof of the first direction of this theorem, the soundness result. Section 6 contains the proof of the second direction, the completeness result. In Section 7 we conclude the paper and discuss future work.

**Technical Overview.** In this paper we see $BFF_2$ (Definition 2.5) as the set of those type-2 functionals computed by an Oracle Turing Machine in polynomial time. We recall basic definitions of such theory in Section 2.2. The main result of this paper is a characterization of the class $BFF_2$ via higher-order term rewriting.

In order to formally give a statement of this result we need to first establish some important notions such as the rewriting counterpart of an oracle (see Definition 4.2) and a computability notion for higher-order rewriting (see Definition 4.3). We state the main result in Theorem 4.5. It 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_2$ (*soundness*). Conversely, we prove that all functionals in $BFF_2$ 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.

Soundness at first seems straightforward. From Kop and Vale [KV23] we know that (call-by-value) higher-order rewrite systems that admit polynomial interpretations (with certain conditions on the interpretation of data constructors) satisfy the property that their runtime complexity is polynomially bounded. We could temptingly say if a term rewrite system computes (in the sense of Definition 4.3) a type-2 functional, it must do so in a polynomial number of steps, and hence the said functional must be in $BFF_2$. However, this is not generally the case due to the size-explosion problem, i.e., in a polynomial number of steps we could iterate over copied data. We solve this issue by restricting the interpretation of data constructors in Definition 4.4 and by employing term graph rewriting (see Section 5.3). Additionally, we need to guarantee that polynomial interpretations alone are capable of controlling the size of the calls to the oracle. More precisely, such interpretations do not allow for unbounded repeated iteration of oracle calls and the size of the resulting oracle call is polynomially related to the size of its given input. This is established by the *Oracle Subterm Lemma* (see Lemma 5.4). We then prove soundness in Theorem 5.16.
To prove completeness we work on an encoding of polynomial time Oracle Turing Machines (OTMs) in STRSs. We proceed as follows: we encode machine configurations as terms and machine transitions as rewriting rules that rewrite such configuration terms. With such encoding, we can faithfully simulate transitions on an OTM as one or more rewriting steps on the corresponding rewrite system. The correctness of such simulation is the subject of Lemma 6.2. Notice however that simulating OTMs by STRSs is not enough. We need to do it in polynomially many steps. For this we provide a rewrite system that can fully simulate a run of an OTM in polynomially many steps, which is given by Theorem 6.4.

## 2. PRELIMINARIES

In this section we present a brief overview of simply typed term rewriting and the basic notions on basic feasible functionals. We assume the reader to be familiar with concepts from rewriting theory [Ter03] and basic notions of computability and complexity theory [AB09].

### 2.1. Higher-Order Rewriting.
We roughly follow the definition of a simply-typed term rewriting system (STRS) [Kus01]: types are simple, consisting of either base or functional types; terms are applicative, meaning they may be partially applied but contain no lambda abstractions. We limit our interest to second-order STRSs where all rules have base type (which in practice means the left- and right-hand side of rules are fully applied terms). Reduction follows an innermost evaluation strategy. We make this intuition precise below.

First, let us define our notion of a type. Let $\mathbb{B}$ be a nonempty set of base types which are ranged over by $\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$ with $n \ge 0$. 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))$.

Then, signatures are sets of function symbols, each of them equipped with a type. Formally, a signature $\mathbb{F}$ is a triple $(\mathbb{B}, \Sigma, \mathbf{typeOf})$ where $\mathbb{B}$ is a set of base types, $\Sigma$ is a nonempty set of symbols, and $\mathbf{typeOf}$ is a function from $\Sigma$ to $\mathbb{T}(\mathbb{B})$.

Next, we define terms. For each type $\sigma$ with $\mathrm{ord}(\sigma) \le 1$, we assume given a set $\mathbb{X}_{\sigma}$ of countably many variables and assume that $\mathbb{X}_{\sigma} \cap \mathbb{X}_{\tau} = \emptyset$ if $\sigma \ne \tau$. We let $\mathbb{X}$ denote $\cup_{\sigma} \mathbb{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}{f : \sigma} \quad \frac{\mathbf{typeOf}(f) = \sigma}{\mathbf{typeOf}(f)} \quad (\text{app}) \quad \frac{s : \sigma \Rightarrow \tau}{(s t) : \tau} \quad t : \sigma $$

As usual, application of terms is left-associative, so we write $s t u$ for $((s t) u)$. Let $\mathbf{vars}(s)$ be the set of variables occurring in $s$. A term $s$ is ground if $\mathbf{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 \ne t$. For a term $s$, $\mathbf{pos}(s)$ is the set of positions in $s$: $\mathbf{pos}(x) = \mathbf{pos}(f) = \{\#\}$ and $\mathbf{pos}(st) = \{\#\} \cup \{1 \cdot u \mid u \in \mathbf{pos}(s)\} \cup \{2 \cdot u \mid u \in \mathbf{pos}(t)\}$. For $p \in \mathbf{pos}(s)$, the subterm $s|_p$ at position $p$ is given by: $s|_p = 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}(\mathbf{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$. We
say a term *has type order k* if its type has order *k*. 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 substituting $\square$ by $s$.

Finally, we have all the ingredients needed to define rewriting rules and the dynamics they give rise to. A *rewrite rule* $\ell \to r$ is a pair of terms of the same type such that $\ell$ has a form $f \ell_1 \cdots \ell_m$ with $f \in \Sigma$, 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 pair consisting of a signature $\mathbb{F}$ and a set of rewrite rules $\mathcal{R}$ over $T(\mathbb{F}, \mathbb{X})$. In this paper, we require that all rules have *base type*: that is, for each rule $\ell \to r$, the type of $\ell$ (so also the type of $r$) is a base type. An STRS is *innermost orthogonal* if all rules are left-linear, and any two distinct rules $\ell_1 \to r_1$, $\ell_2 \to r_2$ are non-overlapping: there are no substitutions $\gamma$ and $\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$. A term is in *normal form* if none of its subterms is a redex.

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$ and $\to_R^*$ for the transitive-reflexive closure. 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 [MN98]. In this paper, we will typically drop the “innermost” adjective and simply refer to terminating/orthogonal/confluent STRSs.

**Example 2.1.** Let us consider a simple example of STRS. We start by defining the following signature $\mathbb{F}$. The base types are $\mathbb{B} = \{\mathbf{nat}\}$ and $\Sigma$ includes $\mathbf{0} : \mathbf{nat}, \mathbf{s} : \mathbf{nat} \Rightarrow \mathbf{nat}$. We add rules for basic operations such as `add`, `mult`: $\mathbf{nat} \Rightarrow \mathbf{nat} \Rightarrow \mathbf{nat}$ and a higher-order function `fnProd`: $(\mathbf{nat} \Rightarrow \mathbf{nat}) \Rightarrow \mathbf{nat} \Rightarrow \mathbf{nat} \Rightarrow \mathbf{nat}$. Finally, the set of rules $\mathcal{R}$ is given by:

$$
\begin{array}{lclcl}
\mathbf{add} \mathbf{0} \mathbf{y} & \to & \mathbf{y} & \quad & \mathbf{add} (\mathbf{s} \mathbf{x}) \mathbf{y} & \to & \mathbf{s} (\mathbf{add} \mathbf{x} \mathbf{y}) \\
\mathbf{mult} \mathbf{0} \mathbf{y} & \to & \mathbf{0} & \quad & \mathbf{mult} (\mathbf{s} \mathbf{x}) \mathbf{y} & \to & \mathbf{add} \mathbf{y} (\mathbf{mult} \mathbf{x} \mathbf{y}) \\
\mathbf{fnProd} \mathbf{F} \mathbf{0} \mathbf{y} & \to & \mathbf{y} & \quad & \mathbf{fnProd} \mathbf{F} (\mathbf{s} \mathbf{x}) \mathbf{y} & \to & \mathbf{fnProd} \mathbf{F} \mathbf{x} (\mathbf{mult} \mathbf{y} (\mathbf{F} \mathbf{x}))
\end{array}
$$

Notice that this system is left-linear and non-overlapping; hence, it is innermost orthogonal, and therefore innermost confluent.

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

**Remark 2.2.** In this paper, we have chosen to limit interest to second-order systems with base-type rules. The restriction to base-type rules is not so significant — since one may simply pad both sides of the rules with fresh variables until they have base type — but the order limitation is arguably more restrictive.

We impose this restriction because our primary goal is to identify a convenient class of term rewriting systems that characterizes $\mathbf{BFF}_2$ — not to find the most general class of term rewriting systems that may do so. Indeed, we have already derived a variation of the results in this work for call-by-value systems of unrestricted type order following the definitions of cost-size interpretation in [KV23] (see [Val24, Chapter 6]). Hence, we have every reason to believe that the type restriction could be dropped also in the current innermost setting, provided the “main” function $\mathbf{F}$ that we will identify in Definition 4.3 remains second-order, i.e., the oracle functions considered are still first-order in such an
envisioned extension. We have not done so in this work because extending the definition of "interpretation" to higher-order innermost systems would add a lot of technical burden (as it also does for call-by-value reduction), and inhibit understanding of the methodology, for arguably little expressivity gain.

We also suspect that the results will extend if lambda-abstraction and beta reduction are permitted, but we have not confirmed this as it would require a larger change, primarily in the construction of Section 5.3. This is also not a major restriction, since abstractions in the right-hand side of rules can be replaced by fresh function symbols.

## 2.2. Basic Feasible Functionals.
We assume familiarity with Turing Machines and basic notions of computability and complexity theory [AB09]. In this paper, we consider deterministic multi-tape Turing Machines. Those are, conceptually, machines consisting 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. 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 (querytapeᵢ for 1 ≤ i ≤ k) and k designated answer tapes (answertapeᵢ). It also has k distinct query states qᵢ and k answer states aᵢ.

Let $W = \{0,1\}^*$. A computation with a k-ary OTM M requires k fixed oracle functions $f_1, \dots, f_k : W \to W$. We write $M_{\bar{f}}$ to denote a run of M with these functions. A run of $M_{\bar{f}}$ on w starts with w written on the main tape. It ends when the machine halts, and yields the word that is written on 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 tape₂ᵢ and enters the query state $q_i$. Then, in one step, it transitions to the answer state $a_i$ as follows:

(a) the query value w written in querytapeᵢ, the query tape for $f_i$, is read;

(b) the contents of answertapeᵢ, are changed to $f_i(w)$;

(c) the query value w is erased from querytapeᵢ; and

(d) the head of answertapeᵢ is moved to its first symbol.

The running time of $M_{\bar{f}}$ on w is the number of steps used in the computation.

We say x is of type-0 whenever $x \in W$. 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 2.3.** 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.4.** 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 such polynomial expressions can be naturally viewed as type-2 functionals, e.g., $P(F, x) = 3 * F(x) + x$ is a type-2 functional of rank (1, 1).
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 $\mathbf{BFF}_2$ as the class of functionals computable by
OTMs with running time bounded by a second-order polynomial:

**Definition 2.5.** A type-2 functional $\Psi$ is in $\mathbf{BFF}_2$ iff there exist an OTM $M$ and a second-order polynomial $P$ such that $M$ computes $\Psi$ and for all $\vec{f}$ and $\vec{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. COST-SIZE INTERPRETATIONS

In this section we define cost-size interpretations for the syntax of types and terms in the STRS format. The interpretations we develop differ from those in [KV23] in two key aspects: here we limit ourselves to second-order systems and the rewriting strategy is innermost instead of call-by-value. As a consequence, the notion of *cost* here is explicitly expressed as a function *cost*(·) that inductively computes the total cost of reduction. Furthermore, these changes require that we prove a higher-order version of the innermost compatibility theorem.

**3.1. The Interpretation of Types and Terms.** In cost-size interpretations, each base-type term is mapped to two different components: a *size* and a *cost*. Intuitively, the size component imposes a restriction on the shape of the normal form of a term; for example, by limiting the total number of function symbols in the normal form, or a weighted total where some symbols are weighed more heavily than others. Meanwhile, the cost component is an integer that bounds the number of steps needed to reach a normal form. By separating these two notions, we can obtain a more fine-grained complexity bound compared to the classical interpretation methods that map to for instance natural numbers [BL16, BCMT01, HP20]. For non-base type terms, the cost and size interpretations are represented by *functions*.

In this paper both the cost and size components must be elements of quasi-ordered sets, which we define formally as follows.

**Size interpretation.** 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 *weakly monotonic functions*: functions that preserve the 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 g(x)$ for all $x \in S_\sigma$. So $S_{\sigma \to \tau}$ is a set of weakly monotonic functionals, using pointwise comparison.

We assume given a fixed *size interpretation function* $\mathcal{J}^s$, which maps each $f \in \Sigma$ to some $\mathcal{J}_f^s \in S_{\text{type0f}(f)}$. If we are additionally given a valuation $\alpha$ that maps each $x \in \mathcal{X}_\sigma$ to $S_\sigma$, we can map each term $s : \sigma$ to an element of $S_\sigma$ naturally as follows: (a) $[[x]]_\alpha^s = \alpha(x)$; (b) $[[f]]_\alpha^s = \mathcal{J}_f^s$; (c) $[[st]]_\alpha^s = [[s]]_\alpha^s([t]]_\alpha^s)$.

(Note that the superscript $s$ always indicates *size*, while we will use $c$ for *cost*.)
**Cost interpretation.** For every type $\sigma$ with $\mathrm{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 $\mathrm{ord}(\sigma) = 1$.

For the weak monotonicity, we again use pointwise comparison: for $f, g \in C_{\sigma \to \tau}$ we say $f \ge g$ if $f(x) \ge g(x)$ for every $x \in C_\sigma$.

We assume given a fixed cost interpretation function $\mathcal{J}^c$, which maps each $f \in \Sigma$ to some $\mathcal{J}_f^c \in C_{\mathrm{type0f}(f)}$; and for each type $\sigma$ with $\mathrm{ord}(\sigma) \le 1$, we assume given valuations $\alpha : \mathbb{X}_\sigma \to S_\sigma$ and $\zeta : \mathbb{X}_\sigma \to C_\sigma$. We then define, for terms of type order $\le 1$:

$$ \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}^s, \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) $$

This is well-defined under our assumptions that all variables have a type of order 0 or 1 (so the arguments to a variable have type order 0), and that we can write $f : (\vec{l}_1 \Rightarrow \kappa_1) \Rightarrow \cdots \Rightarrow (\vec{l}_k \Rightarrow \kappa_k) \Rightarrow \nu_1 \Rightarrow \cdots \Rightarrow \nu_l \Rightarrow \iota$ for each function symbol $f$. Observe also that $\mathcal{J}_f^c$, when fully applied, maps to a natural number. As the left- and right-hand sides of rules have base type, this definition assigns a natural number as the cost interpretation for both sides of each rule.

Intuitively, for a ground base-type term $f s_1 \cdots s_k t_1 \cdots t_n$, $\llbracket f s_1 \cdots s_k t_1 \cdots t_n \rrbracket_{\alpha, \zeta}^c$ expresses the cost of the reduction to normal form *not including* the cost of first normalising each $s_i$ and $t_i$. To compute the full reduction cost, we let

$$ \mathrm{cost}(s)_{\alpha, \zeta} = \sum \{ \llbracket t \rrbracket_{\alpha, \zeta}^c \mid s \supseteq t \text{ and } t \text{ is a non-variable term of base type} \} $$

In addition, in our proofs it is very convenient to have a second cost measure:

$$ \mathrm{cost}^*(s)_{\alpha, \zeta} = \sum \{ \llbracket t \rrbracket_{\alpha, \zeta}^c \mid s \supseteq t \text{ and } t \text{ is a non-variable base-type term not in normal form} \} $$

The difference between **cost** and **cost*** is that subterms that are already in normal form may still contribute a non-zero part to the **cost** measure of a term, but not to **cost***.

**Compatibility.** A cost-size interpretation $\mathcal{F}$ for a second order signature $\mathbb{F} = (\mathbb{B}, \Sigma, \mathrm{type0f})$ is a choice of a quasi-ordered set $S_\iota$, for each $\iota \in \mathbb{B}$, along with cost- and size-interpretation functions $\mathcal{J}^c$ and $\mathcal{J}^s$ defined as above. Let $(\mathbb{F}, \mathcal{R})$ be an STRS over $\mathbb{F}$.

**Definition 3.1.** We say $(\mathbb{F}, \mathcal{R})$ is *compatible* with a cost-size interpretation if for any valuations $\alpha$ and $\zeta$, we have (a) $\llbracket \ell \rrbracket_{\alpha, \zeta}^c > \mathrm{cost}(r)_{\alpha, \zeta}$ and (b) $\llbracket \ell \rrbracket_\alpha^s \supseteq \llbracket r \rrbracket_\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}$.

As in all notions of interpretation where the underlying domain is that of the natural numbers, the compatibility check is, in general, bound to be undecidable. This is the case even if sound but complete techniques exist. In any case, a study about the possibility of automating our technique is outside the scope of this paper and is thus left to future work.

To avoid heavy notation, we will often omit the valuations $\alpha$ and $\zeta$ from subscripts when quantifying over them, and keep the quantification implicit. For example, instead of writing

$$ \forall \alpha, \zeta. \llbracket \mathrm{fnProd} F (s \times) y \rrbracket_{\alpha, \zeta}^c > \mathrm{cost}(\mathrm{fnProd} F x (\mathrm{mult} y (F x)))_{\alpha, \zeta} $$

we will use:

$$ \llbracket \mathrm{fnProd} F (s \times) y \rrbracket^c > \mathrm{cost}(\mathrm{fnProd} F x (\mathrm{mult} y (F x))) $$
When we do this, we will also leave $\alpha$ and $\zeta$ out of concreate interpretations; for example, instead of

$$[[\text{fnProd } F x y]]_{\alpha, \zeta}^{c} = 3 * \alpha(x) * \alpha(y) * \max(\alpha(F)(\alpha(x)), 1)^{\alpha(x)+1} + \alpha(x) * \zeta(F)(\alpha(x)) + 2 * \alpha(x) + 1$$
we will use:

$$[[\text{fnProd } F x y]]_{\alpha, \zeta}^{c} = 3 * x * y * \max(F^{s}(x), 1)^{x+1} + x * F^{c}(x) + 2 * x + 1$$

Where $\alpha(x)$ is simply denoted as $x$ for type-0 variables, and as $x^s$ for type-1 variables; $\zeta(x)$ is always denoted as $x^c$ (note that, when considering the cost interpretation of rules, $\zeta(x)$ only occurs for type-1 variables).

**Example 3.2.** Let us consider the signature of the STRS given in Example 2.1. We can interpret the base type nat as the natural quasi-order set $S_{\text{nat}} = (\mathbb{N}, \geq)$. We need to give interpretations for the constructors of nat. Let us start by size.

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

This gives us $[[\Gamma \bar{n}]]^s = n$ for all $n \in \mathbb{N}$. So intuitively our interpretation is counting how many $s$ symbols there are in the unary representation of a natural number, and setting this as its size. For the cost measure we do as follows.

$$\mathcal{J}_{0}^{c} = 0 \qquad \mathcal{J}_{s}^{c} = \lambda x.0$$

This gives us $[[\Gamma \bar{n}]]^c = \text{cost}(n) = 0$, which makes sense since the base type nat is intended to represent data values, from which no computation can be started. Here we see a first contrast with the classical interpretation method. By splitting cost and size we can faithfully encode complexity information into the interpretation.

Next, we give size and cost interpretation functions for add and mult. So 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 \geq [[r]]^s$ for the first four rules of Example 2.1 (e.g., $[[\text{mult}(s x) y]]^s = (x + 1) * y \geq y + (x * y) = [[\text{add} y (\text{mult} x y)]]^s$). For the cost interpretation functions, note that both add and mult are type-1, so we must choose functions that take the sizes of their arguments as input, and return a cost. Here, we choose $\mathcal{J}_{\text{add}}^{c} = \lambda xy.x + 1$ and $\mathcal{J}_{\text{mult}}^{c} = \lambda xy.x * y + 2 * x + 1$. To see why this makes sense, consider arguments in normal form: e.g., reducing add ($s^n 0$) ($s^m 0$) to normal form takes $n + 1$ steps. We indeed have the required inequality $[[\ell]]^c > \text{cost}(r)$ for the first four rules; for example:

$$\begin{align*}
[[\text{mult}(s x) y]]^{c} &= [[s x]]^{s} * [[y]]^{s} + 2 * [[s x]]^{s} + 1 \\
&= (x + 1) * y + 2 * (x + 1) + 1 &&= x * y + 2 * x + y + 3 \\
&> \\
\text{cost}(\text{add} y (\text{mult} x y)) &= [[\text{add} y (\text{mult} x y)]]^{c} + [[\text{mult} x y]]^{c} \\
&= (y + 1) + (x * y + 2 * x + 1) = x * y + x * x + y + 2
\end{align*}$$

Regarding fnProd: note that the cost of evaluating a term $\text{fnProd } F n m$ depends not only on the sizes of the arguments $F$, $n$ and $m$, but also on the behaviour of $F$: if $F$ is a function that computes its result in linear time in the size of the input, then $\text{fnProd } F n m$ will reach a normal form much faster than if $F$ operates in exponential time. The computation time is also affected by the size of the output that $\text{fnProd}$ produces, as this is fed into mult. This is why $\mathcal{J}_{\text{fnProd}}^{c}$ takes both a cost function and a size function as argument. We can orient both rules by choosing $\mathcal{J}_{\text{fnProd}}^{s} = \lambda Fxy.y * \max(F(x), 1)^x$ and $\mathcal{J}_{\text{fnProd}}^{c} = \lambda F^{c}F^{s}xy.3 * x * y * \max(F^{s}(x), 1)^{x+1} + x * F^{c}(x) + 2 * x + 1$.

Notice that $\mathcal{J}_{\text{fnProd}}^{c}$ is not polynomial, but that is allowed in the general case.
**Example 3.3.** Consider an STRS with base types $\mathbb{B} = \{\text{nat}\}$, function symbols $0: \text{nat}, s:$
$\text{nat} \Rightarrow \text{nat}, \text{minus} : \text{nat} \Rightarrow \text{nat} \Rightarrow \text{nat}$, and rules:

$$ \text{minus} (s x) (s y) \rightarrow \text{minus} x y \qquad \text{minus} x 0 \rightarrow x $$

If we choose $\mathcal{J}_0^s$, $\mathcal{J}_s^s$, $\mathcal{J}_0^c$ and $\mathcal{J}_s^c$ like in Example 3.2, and $\mathcal{J}_{\text{minus}}^c = \lambda xy.y$, then we have $\text{cost}(\text{minus } 0 (s	ext{ }0)) = 1$, while $\text{cost}^*(\text{minus } 0 (s	ext{ }0)) = 0$. This is because $\text{minus } 0 (s	ext{ }0)$ is in normal form, even though it is not fully built from constructors.

**3.2. The Compatibility Theorem.** We now prove the Innermost Compatibility Theorem for STRSs. The proof is analogous to that in [KV23] with some adaptations to the definitions of Section 3.1 which are possible here since our terms are applicative and second-order only; we also make some adaptations to the evaluation strategy being innermost rather than call-by-value, in particular through the use of the $\text{cost}^*(\cdot)$ function.

**Theorem 3.4 (Innermost Compatibility).** Suppose $(\mathbb{F}, \mathcal{R})$ is an STRS compatible with a cost-size interpretation $\mathcal{F}$ (following Definition 3.1). 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 \mathbb{R} t$.

Hence, if we find a suitable cost-size interpretation, which orients all the rules, then we have a *bound* on the derivation height of any given term: that is, the number of reduction steps we need to take to reduce any given term to normal form. For example, suppose $s_0 \to \mathbb{R} s_1 \to \mathbb{R} \dots \to \mathbb{R} s_n$. Let $\alpha$ and $\zeta$ map all variables either to 0 or to a constant function $\lambda \vec{x}.0$. Then $\text{cost}^*(s_0)_{\alpha, \zeta} \ge \text{cost}^*(s_1)_{\alpha, \zeta} + 1 \ge \dots \ge \text{cost}^*(s_n)_{\alpha, \zeta} + n$ — and therefore, necessarily $\text{cost}^*(s_0)_{\alpha, \zeta} \ge n$. This holds whether $s_0$ has base type or not, since $\text{cost}^*(\cdot)$ always maps to a natural number. Observing that always $\text{cost}(s)_{\alpha, \zeta} \ge \text{cost}^*(s)_{\alpha, \zeta}$:

**Corollary 3.5.** Suppose $(\mathbb{F}, \mathcal{R})$ is an STRS compatible with a cost-size interpretation $\mathcal{F}$, and let $s$ be a term with derivation height $n$. Then for any valuations $\alpha$ and $\zeta$, $\text{cost}(s)_{\alpha, \zeta} \ge n$.

In order to prove Theorem 3.4, we first establish some useful lemmas. Recall that in this paper, all rules are of base type, i.e., they are fully applied. Since reduction is innermost, a rule may only be fired if the matching substitution (i.e., the substitution $\gamma$ on the base case $\ell\gamma \to r\gamma$), maps all variables to irreducible terms. So in the lemmas below, without loss of generality, we restrict ourselves to this type of substitutions and notice that $\text{cost}^*(x\gamma) = 0$ for any variable $x$.

**Lemma 3.6.** For all terms $st$ with $t$ of base type: $[[st]]_\alpha^s = [[s]]_\alpha^s([[[t]]_\alpha^s)$ and $[[st]]_{\alpha, \zeta}^c = [[s]]_{\alpha, \zeta}^c([[[t]]_\alpha^s)$ for all $\alpha, \zeta$.

*Proof.* The former statement holds by definition. The latter holds by a straightforward case analysis on the form of $s$: it holds both if $s = x s_1 \dots s_n$ and $s = f s_1 \dots s_k t_1 \dots t_n$. For the $f$ case, recall that we fixed $f: (\vec{\iota}_1 \Rightarrow \kappa_1) \Rightarrow \dots \Rightarrow (\vec{\iota}_k \Rightarrow \kappa_k) \Rightarrow \nu_1 \Rightarrow \dots \Rightarrow \nu_l \Rightarrow \iota$ as the general type for function symbols $f$, and since $t$ has base type, all higher-type arguments to $f$ are necessarily already supplied. Hence, $[[s]]_{\alpha, \zeta}^c$ is indeed well-defined. $\square$

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

**Lemma 3.7.** 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}^{s}$.

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

$$ \begin{align*} \llbracket (tu)\gamma \rrbracket^s &= \llbracket t\gamma \rrbracket^s (\llbracket u\gamma \rrbracket^s) \\ &\stackrel{IH}{=} \llbracket t \rrbracket^s_{\alpha\gamma} (\llbracket u \rrbracket^s_{\alpha\gamma}) = \llbracket t u \rrbracket^s_{\alpha\gamma} \end{align*} \quad \square $$

We can now prove the *size* part of Theorem 3.4 which is stated as the lemma below.

**Lemma 3.8.** Let $(\mathbb{F}, \mathcal{R})$ be an STRS compatible with a cost–size interpretation following Definition 3.1, and let $s, t$ be terms of the same type such that $s \to_R t$. Then $[[s]]_{\alpha}^s \supseteq [[t]]_{\alpha}^s$ holds for all $\alpha$.

*Proof.* By induction on the form of s.

In the base case, we have $s \to_R t$ by $\ell\gamma \to r\gamma$. Then we combine the substitution lemma (Lemma 3.7) with the compatibility requirement for size, i.e., $[[\ell]]_{\alpha}^s \supseteq [[r]]_{\alpha}^s$, as follows:

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

In the application case, $s = s_1 s_2$ and either $t = t_1 s_2$ with $s_1 \to_R t_1$ or $t = s_1 t_2$ with $s_2 \to_R t_2$. In the first case, $[[s_1]]_{\alpha}^s \supseteq [[t_1]]_{\alpha}^s$ by the induction hypothesis, which by definition gives $[[s]]_{\alpha}^s = [[s_1]]_{\alpha}^s ([[s_2]]_{\alpha}^s) \supseteq [[t_1]]_{\alpha}^s ([[s_2]]_{\alpha}^s) = [[t]]_{\alpha}^s$. In the second case, $[[s_2]]_{\alpha}^s \supseteq [[t_2]]_{\alpha}^s$ by the induction hypothesis and $[[s]]_{\alpha}^s = [[s_1]]_{\alpha}^s ([[s_2]]_{\alpha}^s) \supseteq [[s_1]]_{\alpha}^s ([[t_2]]_{\alpha}^s) = [[t]]_{\alpha}^s$ because by definition, $[[s_1]]_{\alpha}^s$ is a weakly monotonic function. $\square$

**Lemma 3.9.** Given cost–size valuations $\alpha, \gamma$ and a term $s$ of type order at most 1. Then $[[s\gamma]]_{\alpha,\zeta}^c = [[s]]_{\alpha^\gamma, \zeta^\gamma}^c$.

*Proof.* By induction on the size of s. We consider two cases:

* For the first case, we get $s = x s_1 \dots 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*} \llbracket (x s_1 \dots s_n)\gamma \rrbracket_{\alpha, \zeta}^c &= \llbracket (x\gamma) (s_1\gamma) \dots (s_n\gamma) \rrbracket_{\alpha, \zeta}^c \\ \text{Lemma 3.6} \quad &\stackrel{\text{Lemma 3.7}}{=} \llbracket x\gamma \rrbracket_{\alpha, \zeta}^c (\llbracket s_1\gamma \rrbracket_{\alpha}^s, \dots, \llbracket s_n\gamma \rrbracket_{\alpha}^s) \\ &= \zeta_{\alpha}^{\gamma}(x) (\llbracket s_1 \rrbracket_{\alpha}^s, \dots, \llbracket s_n \rrbracket_{\alpha}^s) \\ &= \llbracket (x s_1 \dots s_n) \rrbracket_{\alpha^\gamma, \zeta^\gamma}^c \end{align*} $$

* For the second case we have $s = f s_1 \dots s_k t_1 \dots t_n$. Recall that we fixed $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$ 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*} \llbracket (f s_1 \dots s_k t_1 \dots t_n)\gamma \rrbracket_{\alpha, \zeta}^c \\ &= \llbracket f(s_1\gamma) \dots (s_k\gamma) (t_1\gamma) \dots (t_n\gamma) \rrbracket_{\alpha, \zeta}^c \\ &= \mathcal{J}_f^c (\llbracket s_1\gamma \rrbracket_{\alpha, \zeta}^c, \llbracket s_1\gamma \rrbracket_{\alpha}^s, \dots, \llbracket s_k\gamma \rrbracket_{\alpha, \zeta}^c, \llbracket s_k\gamma \rrbracket_{\alpha}^s, \llbracket t_1\gamma \rrbracket_{\alpha}^s, \dots, \llbracket t_n\gamma \rrbracket_{\alpha}^s) \end{align*} $$
$$
\begin{align*}
\text{IH, Lemma 3.7} &\qquad \mathcal{J}_{\mathfrak{f}}^{\mathcal{C}}(\llbracket s_1 \rrbracket_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}}^{\mathcal{C}}, \llbracket s_1 \rrbracket_{\alpha^{\gamma}}^{\mathcal{S}}, \dots, \llbracket s_k \rrbracket_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}}^{\mathcal{C}}, \llbracket s_k \rrbracket_{\alpha^{\gamma}}^{\mathcal{S}}, \dots, \llbracket t_1 \rrbracket_{\alpha^{\gamma}}^{\mathcal{S}}, \dots, \llbracket t_n \rrbracket_{\alpha^{\gamma}}^{\mathcal{S}}) \\
&= \llbracket \mathfrak{f} s_1 \dots s_k t_1 \dots t_n \rrbracket_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}}^{\mathcal{C}} \tag*{\square}
\end{align*}
$$

<figure><img src="image_5.png" /></figure>

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

**Lemma 3.10.** For any term $s$ of type order 0 or 1, and any substitution $\gamma$ such that all $\gamma(x)$ are in normal form, we have that $\text{cost}(s)_{\alpha^{\gamma}, \zeta_{\alpha}^{\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_{\alpha}^{\gamma}} = 0$ by definition, and since we assumed that $\gamma(x)$ is in normal form, also $\text{cost}^*(x\gamma)_{\alpha, \zeta} = 0$. If $n > 0$ and $s$ has base type, then $\text{cost}(s)_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}} = \zeta_{\alpha}^{\gamma}(x)(\llbracket s_1 \rrbracket_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}}^{\mathcal{S}}, \dots, \llbracket s_n \rrbracket_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}}^{\mathcal{S}}) + \sum_{i=1}^{n} \text{cost}(s_i)_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}} = \llbracket \gamma(x) \rrbracket_{\alpha, \zeta}^{\mathcal{C}}(\llbracket s_1 \gamma \rrbracket_{\alpha, \zeta}^{\mathcal{S}}, \dots, \llbracket s_n \gamma \rrbracket_{\alpha, \zeta}^{\mathcal{S}}) + \sum_{i=1}^{n} \text{cost}(s_i)_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}}$ by Lemmas 3.7 and 3.9. By Lemma 3.6 and the induction hypothesis this $\ge \llbracket (x\gamma)(s_1\gamma) \dots (s_n\gamma) \rrbracket^{\mathcal{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 = \mathfrak{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_{\alpha}^{\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_{\alpha}^{\gamma}} &= \text{cost}(\mathfrak{f} s_1 \dots s_k t_1 \dots t_n)_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}} \\
&= \llbracket s \rrbracket_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}}^{\mathcal{C}} + \sum_{i=1}^{k} \text{cost}(s_i)_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}} + \sum_{j=1}^{n} \text{cost}(t_j)_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}} \\
\text{Lemma 3.9} \quad &\overset{\text{ IH }}{=} \llbracket s\gamma \rrbracket_{\alpha, \zeta}^{\mathcal{C}} + \sum_{i=1}^{k} \text{cost}(s_i)_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}} + \sum_{j=1}^{n} \text{cost}(t_j)_{\alpha^{\gamma}, \zeta_{\alpha}^{\gamma}} \\
&\overset{\text{ IH }}{\ge} \llbracket s\gamma \rrbracket_{\alpha, \zeta}^{\mathcal{C}} + \sum_{i=1}^{k} \text{cost}^*(s_i\gamma)_{\alpha, \zeta} + \sum_{j=1}^{n} \text{cost}^*(t_j\gamma)_{\alpha, \zeta} \\
&= \text{cost}^*(s\gamma)_{\alpha, \zeta}
\end{align*}
$$

<figure><img src="image_6.png" /></figure>

If not, then:

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

**Lemma 3.11.** Let $(\mathbb{F}, \mathcal{R})$ be an STRS compatible with a cost–size interpretation following Definition 3.1 and $s, t$ be type-1 terms of the same type, such that $s \to_{\mathcal{R}} t$. Then we have that $\llbracket s \rrbracket_{\alpha, \zeta}^{\mathcal{C}} \ge \llbracket t \rrbracket_{\alpha, \zeta}^{\mathcal{C}}$.
*Proof.* By induction on the size of $s$. There are two cases.

* First, $s = x s_1 \dots s_n$. We can write $x : \iota_1 \Rightarrow \dots \Rightarrow \iota_k \Rightarrow \kappa$ and, since $s$ is type-1 (so not of base type), $n < k$. Then $t = x s_1 \dots s'_i \dots s_n$ with $s_i \to_R s'_i$. Hence, by Lemma 3.8 and monotonicity of $\zeta(x)$:

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

* For the second part, $s = f s_1 \dots s_k t_1 \dots t_n$, recall that rules are of base type, and therefore reduction does not occur at head position. Hence, either $t = f s_1 \dots s'_i \dots s_k t_1 \dots t_n$ with $s_i \to_R s'_i$, or $t = f s_1 \dots s_k t_1 \dots t'_i \dots t_n$ with $t_i \to_R t'_i$.

In the first case,

$$ 
\begin{aligned}
& [f s_1 \dots s_i \dots s_k t_1 \dots t_n]_{\alpha, \zeta}^{c} \\
&= \mathcal{J}_f^{c}([s_1]_{\alpha, \zeta}^{c}, [s_1]_{\alpha, \zeta}^{s}, \dots, [s_i]_{\alpha, \zeta}^{c}, [s_i]_{\alpha}^{s}, \dots, [s_k]_{\alpha, \zeta}^{c}, [s_k]_{\alpha}^{s}, [t_1]_{\alpha}^{s}, \dots, [t_n]_{\alpha}^{s}) \\
&\geq \mathcal{J}_f^{c}([s_1]_{\alpha, \zeta}^{c}, [s_1]_{\alpha, \zeta}^{s}, \dots, [s_i]_{\alpha, \zeta}^{c}, [s_i]_{\alpha}^{s}, \dots, [s_k]_{\alpha, \zeta}^{c}, [s_k]_{\alpha}^{s}, [t_1]_{\alpha}^{s}, \dots, [t_n]_{\alpha}^{s}) \\
&= [f s_1 \dots s'_i \dots s_k t_1 \dots t_n]_{\alpha, \zeta}^{c}
\end{aligned}
$$

because $[s_i]_{\alpha}^{s} \supseteq [s'_i]_{\alpha, \zeta}^{s}$ by Lemma 3.8, $[s_i]_{\alpha, \zeta}^{c} \geq [s'_i]_{\alpha, \zeta}^{c}$ by the induction hypothesis, and $\mathcal{J}_f^{c}$ is weakly monotonic. For the second case, we only need Lemma 3.8 and monotonicity, not the induction hypothesis. $\square$

Finally, we are ready to prove the innermost compatibility theorem.

**Theorem 3.4 (Innermost Compatibility).** Suppose $(\mathbb{F}, \mathcal{R})$ is an STRS compatible with a cost-size interpretation $\mathcal{F}$ (following Definition 3.1). 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_R t$.

*Proof.* The second part of the theorem is given by Lemma 3.8. The first part follows by induction on the reduction $s \to_R t$.

* For the base case, we have by Lemmas 3.9 and 3.10 that

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

* For the application case with a variable root symbol, we have that $x t_1 \dots t_i \dots t_n \to_R x t_1 \dots t'_i \dots t_n$ with $t_i \to_R t'_i$. By induction we get $\text{cost}^*(t_i)_{\alpha, \zeta} > \text{cost}^*(t'_i)_{\alpha, \zeta}$, and by Lemma 3.8 we have $[t_i]_{\alpha}^{s} \supseteq [t'_i]_{\alpha}^{s}$. Then, if $s$ has base type:

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

If s does not have base type, we have a similar reasoning without the component $[[x t_1 \dots t_i \dots t_n]]_{\alpha, \zeta}^c$.

* 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 \dots s_k t_1 \dots t_i \dots t_n \to_R f s_1 \dots s_k t_1 \dots t'_i \dots t_n$ with $t_i \to_R t'_i$. Let us write $\vec{s}$ for $s_1 \dots s_k$ and $c(s)$ for $\sum_{j=1}^k \mathrm{cost}^*(s_j)_{\alpha, \zeta}$ below. We also abuse notation and write $[[\vec{s}]_{\alpha, \zeta}^c, [[\vec{s}]_\alpha^s]$ for $[[s_1]]_{\alpha, \zeta}^c, [[s_1]]_\alpha^s, \dots, [[s_k]]_{\alpha, \zeta}^c, [[s_k]]_\alpha^s$. If s has base type:

$$
\begin{align*}
\mathrm{cost}^*(f \vec{s} t_1 \dots t_i \dots t_n)_{\alpha, \zeta} \\
&= [[f \vec{s} t_1 \dots t_i \dots t_n]]_{\alpha, \zeta}^c + c(s) + \sum_{j=1}^n \mathrm{cost}^*(t_j)_{\alpha, \zeta} \\
&= \mathcal{J}_f^c( [[\vec{s}]_{\alpha, \zeta}^c, [[\vec{s}]_\alpha^s, [[t_1]]_\alpha^s, \dots, [[t_i]]_\alpha^s, \dots, [[t_n]]_\alpha^s) + c(s) + \sum_{j=1}^n \mathrm{cost}^*(t_j)_{\alpha, \zeta} \\
&\ge \mathcal{J}_f^c( [[\vec{s}]_{\alpha, \zeta}^c, [[\vec{s}]_\alpha^s, [[t_1]]_\alpha^s, \dots, [[t'_i]]_\alpha^s, \dots, [[t_n]]_\alpha^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)_{\alpha, \zeta}
\end{align*}
$$

where in the last step we use $\mathrm{cost}^*(t_i)_{\alpha, \zeta} > \mathrm{cost}^*(t'_i)_{\alpha, \zeta}$, given by the IH. If s does not have base type, the reasoning is similar, only omitting the component $[[f \vec{s} t_1 \dots t_i \dots t_n]]_{\alpha, \zeta}^c$.

* 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 \dots s_i \dots s_k t_1 \dots t_n \to_R f s_1 \dots s'_i \dots s_k t_1 \dots t_n$ with $s_i \to_R s'_i$. Recall that by IH we get $\mathrm{cost}^*(s_i)_{\alpha, \zeta} > \mathrm{cost}^*(s'_i)_{\alpha, \zeta}$. If s does not have base type, we conclude in a similar reasoning to the ones used above, simply counting the $\mathrm{cost}^*(\cdot)$ for all arguments. If s does have base type, note that $s_i$ and $s'_i$ are type-1 terms, so we can apply Lemma 3.11 to obtain $[[s_i]]^c \ge [[s'_i]]^c$. With this in hand we reason as follows:

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

By monotonicity of $\mathcal{J}_f^c$ and $[[s_i]]_{\alpha, \zeta}^c \ge [[s'_i]]_{\alpha, \zeta}^c, [[s_i]]_\alpha^s \supseteq [[s'_i]]_\alpha^s$, we get

$$
\begin{align*}
& \ge \mathcal{J}_f^c( [[s_1]]_{\alpha, \zeta}^c, [[s_1]]_\alpha^s, \dots, [[s'_i]]_{\alpha, \zeta}^c, [[s'_i]]_\alpha^s, \dots, [[s_k]]_{\alpha, \zeta}^c, [[s_k]]_\alpha^s, [[\vec{t}]]_\alpha^s) \\
& \quad + ( \sum_{j=1 \dots k, j \neq i} \mathrm{cost}^*(s_j)_{\alpha, \zeta} ) + \mathrm{cost}^*(s_i)_{\alpha, \zeta} + ( \sum_{j=1} \mathrm{cost}^*(t_j)_{\alpha, \zeta} ) \\
& > \mathcal{J}_f^c( [[s_1]]_{\alpha, \zeta}^c, [[s_1]]_\alpha^s, \dots, [[s'_i]]_{\alpha, \zeta}^c, [[s'_i]]_\alpha^s, \dots, [[s_k]]_{\alpha, \zeta}^c, [[s_k]]_\alpha^s, [[\vec{t}]]_\alpha^s) \\
& \quad + ( \sum_{j=1 \dots k, j \neq i} \mathrm{cost}^*(s_j)_{\alpha, \zeta} ) + \mathrm{cost}^*(s'_i)_{\alpha, \zeta} + ( \sum_{j=1} \mathrm{cost}^*(t_j)_{\alpha, \zeta} )
\end{align*}
$$

$$= \mathrm{cost}^*(f s_1 \dots s'_i \dots s_k \vec{t})_{\alpha, \zeta}$$

□
4. FROM HIGHER-ORDER REWRITING TO BFF₂ AND BACK

The main result of this paper roughly states that BFF₂ consists exactly of those type-2 functionals computed by an STRS compatible with a cost–size tuple interpretation, whose main function is polynomially bounded. 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. The challenge is that such an STRS is required to do what it is supposed to do *for every* input, and the inputs not only consist of words, but also of functions on words. We thus have to find a way to encode type-1 functions seen as inputs to a type-2 program.

Indeed, let us start by encoding words in W as terms. We let bit, word ∈ B and introduce symbols o, i : bit and [] : word, :: : bit ⇒ word ⇒ word (where :: will be used in infix notation). Then for instance 001 is encoded as the term o::(o::(i::[])). In practice, we usually employ the cleaner list-like notation [o; o; i]. Let w denote the term encoding of a word w.

**Example 4.1** (Implementing Binary Addition). Let us implement binary addition. For this purpose, we consider binary sequences written in *little-endian* format, i.e., the least significant digit is at the head of the list. So the decimal number 6 is written as 011 in little-endian notation. To start, we will need the following logical operations on bit symbols.

<figure><img src="image_7.png" /></figure>

The rules defining aux : word ⇒ word ⇒ bit ⇒ word below compute the bitwise addition of two binary numbers, given a carrying value as the third argument. This is done by recursing over the input lists.

<figure><img src="image_8.png" /></figure>

Finally, we write the addition of binary numbers as the rule $x +_B y \rightarrow \text{aux } xy o$. We can orient all rules by setting the following interpretation:

<figure><img src="image_9.png" /></figure>

This interpretation assigns cost 0 to all ground constructor terms: ground terms that are exclusively built from the constructor symbols i, o, [] and ::. The size of a binary word is its length. The cost of adding two numbers is bounded by $2 + 7 * \langle \text{the length of the longest} \rangle$: this accounts for iterating through the list, and doing 6 bit operations for each step.

Next, we encode type-1 functions as a possibly infinite set of one-step rewrite rules.
**Definition 4.2.** Consider a type-1 function $f : W \to W$ and let $S_f : \mathbf{word} \Rightarrow \mathbf{word}$ be a fresh function symbol. A set of rules $\mathcal{R}_f$ defines a function $f : \mathbb{N} \to \mathbb{N}$ by way of the symbol $S_f$ if and only if $\mathcal{R}_f$ contains exactly the rules $S_f \underline{n} \to \underline{m}$ where $n, m \in \mathbb{N}$ and $m = f(n)$.

Intuitively, this infinite set of rules is the rewriting counterpart of an oracle $f$. Indeed, in a single rewrite step $S_f \underline{x}$ rewrites to the value $f(x)$. Henceforth, we assume given that our STRS $(\mathbb{F}, \mathcal{R})$ at hand is such that $\mathbb{F}$ contains $\mathfrak{o}, \mathfrak{i}, \mathfrak{[}]$; $\mathfrak{::}$ typed as above and a distinguished symbol $\mathbf{F} : (\mathbf{word} \Rightarrow \mathbf{word})^k \Rightarrow \mathbf{word}^l \Rightarrow \mathbf{word}$. Given type-1 functions $f_1, \dots, f_k$, we write $\mathbb{F}_{\vec{f}}$ for $\mathbb{F}$ extended with function symbols $S_{f_i} : \mathbf{word} \Rightarrow \mathbf{word}$, with $1 \le i \le k$, and let $\mathcal{R}_{+\vec{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 4.3.** Let $(\mathbb{F}, \mathcal{R})$ be an STRS. We say that $\mathbf{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$, $\mathbf{F} S_{f_1} \cdots S_{f_k} \underline{w_1} \cdots \underline{w_l} \to_{\mathcal{R}_{+\vec{f}}} \mathfrak{o}$, where $u = \Psi(f_1, \dots, f_k, w_1, \dots, w_l)$.

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

**Definition 4.4.** We say that 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_{\mathbf{word}} = (\mathbb{N}, \geq)$;

* $\mathcal{J}_{\mathfrak{o}}^{\mathcal{c}} = \mathcal{J}_{\mathfrak{i}}^{\mathcal{c}} = \mathcal{J}_{\mathfrak{[}]}$ = 0, $\mathcal{J}_{\mathfrak{::}}^{\mathcal{c}} = \lambda x y . 0$, and $\mathcal{J}_{\mathfrak{::}}^{\mathcal{s}} = \lambda x y . x + y + c$ for some $c \geq 1$;

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

Note that the condition on $\mathcal{J}_{\mathfrak{::}}^{\mathcal{s}}$ corresponds to what is called *additive quasi-interpretation* in [BMM11]. Finally, we can formally state our main result.

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

Note that the polynomial bound *only* refers to the cost-size interpretation for $\mathbf{F}$. Indeed, except for $\mathfrak{o}$, $\mathfrak{i}$, $\mathfrak{[}]$, and $\mathfrak{::}$ there are no requirements on the interpretations for other symbols. We will prove this result in two parts. First, we prove soundness in Section 5 which states that every type-2 functional computed by an STRS as above is in $\mathrm{BFF}_2$. Then in Section 6 we prove completeness, which states that every functional in $\mathrm{BFF}_2$ 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 4.6.** Let us consider the type-2 functional defined by $\Psi := \lambda f x. \sum_{i<|x|} f(i)$, where $|x|$ refers to the length of the word $x$. Notice that $\Psi$ adds all $f(i)$ over each word $i \in W$ whose value (as a binary number) is smaller than the length of $x$. This functional was proved to lie in $\mathrm{BFF}_2$ in [IRK01], where the authors used an encoding of $\Psi$ as a $\mathrm{BTLP}_2$ program. We can encode $\Psi$ as an STRS as follows. We expand on the STRS from Example 4.1. Let us also include the type nat and data constructors $\mathfrak{o}$ and $\mathfrak{s}$ from Example 2.1, and consider ancillary symbols `lengthOf`: `word` $\Rightarrow$ nat and `toBin`: nat $\Rightarrow$ word, defined by the following rules:

`lengthOf []` $\to$ 0

`toBin 0` $\to$ $\mathfrak{[}]$

`lengthOf (a::as)` $\to$ `s (lengthOf as)`

`toBin (s n)` $\to$ `(toBin n) +_B (i::\mathfrak{[}])`
The former computes the length of a given word and the latter converts a number from unary to binary representation (using the binary addition symbol $+_B : word \Rightarrow word \Rightarrow word$, whose rules were given in Example 4.1). Then $\Psi$ is computed by:

$$ 
\begin{align*}
\mathcal{J}_0^s = 0 &\qquad \mathcal{J}_0^c = 0 &\qquad \mathcal{J}_s^s = \lambda x.1 + x &\qquad \mathcal{J}_s^c = \lambda x.0 \\
\mathcal{J}_{\text{lengthOf}}^s = \lambda x.x &\qquad \mathcal{J}_{\text{lengthOf}}^c = \lambda x.1 + x &\qquad \mathcal{J}_{\text{toBin}}^s = \lambda x.1 + x &\qquad \mathcal{J}_{\text{toBin}}^c = \lambda x.7 * x^2 + 3 * x + 1
\end{align*}
$$

That is, if we want to compute $\Psi(f, x)$ we simply reduce the term $\mathcal{start} S_f \underline{\underline{\phantom{x}}}$ to normal form. By Theorem 4.5, to show that this system is in $\mathbf{BFF}_2$ via our rewriting formalism we need to exhibit a cost-size tuple interpretation for it that satisfies Definition 4.4. The interpretation functions for $o$, $i$, $[]$ and $::$ from Example 4.1 satisfy the requirements (with $c = 1$); in addition let us set the following interpretations:

$$ 
\begin{align*}
\mathcal{J}_0^s = 0 &\qquad \mathcal{J}_0^c = 0 &\qquad \mathcal{J}_s^s = \lambda x.1 + x &\qquad \mathcal{J}_s^c = \lambda x.0 \\
\mathcal{J}_{\text{lengthOf}}^s = \lambda x.x &\qquad \mathcal{J}_{\text{lengthOf}}^c = \lambda x.1 + x &\qquad \mathcal{J}_{\text{toBin}}^s = \lambda x.1 + x &\qquad \mathcal{J}_{\text{toBin}}^c = \lambda x.7 * x^2 + 3 * x + 1
\end{align*}
$$

$$ \mathcal{J}_{\text{compute}}^s = \lambda F j a. j + \max(a, F(j)) $$

$$ \mathcal{J}_{\text{compute}}^c = \lambda F^c F^s j a. 4 * j^3 + 7 * j * \max(a, F^s(j)) + j * F^c(j) + 1 $$

$$ \mathcal{J}_{\text{start}}^s = \lambda F x.x + F(x) $$

$$ \mathcal{J}_{\text{start}}^c = \lambda F^c F^s x. 4 * x^3 + 7 * x * F^s(x) + x * F^c(x) + x + 3 $$

This orients all rules, and $\mathcal{J}_{\text{start}}^c$ is a polynomial.

## 5. SOUNDNESS

In order to prove soundness, let us consider a fixed finite orthogonal STRS $\mathcal{R}$ with a distinguished function symbol $F$ which admits a polynomially bounded cost-size interpretation, that computes a type-2 functional $\Psi$. We proceed to show that $\Psi$ is in $\mathbf{BFF}_2$ 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 4.3). The restriction on $\mathcal{J}_{\cdot}^s$ (Definition 4.4) implies that $[\mathcal{F} S_f \underline{\underline{w}}]^c$ is bounded by a second-order polynomial over $|f|, |w|$. We show this in Lemma 5.1. By compatibility (Corollary 3.5), we can do at most polynomially many steps when reducing $\mathcal{F} S_f \underline{\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 5.4.

(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 $\mathbf{BFF}_2$, Theorem 5.16.
5.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}^{\mathcal{s}} = \lambda xy.x + y + c$ (Definition 4.4) let $\mu := \max(\mathcal{J}_{\circ}^{\mathcal{s}}, \mathcal{J}_{i}^{\mathcal{s}}) + c$ and $\nu := \mathcal{J}_{\llbracket}^{\mathcal{s}}$. Consequently, for all $w \in W$:

$$|w| \le \llbracket \mathbf{w} \rrbracket^{\mathcal{s}} \le \mu * |w| + \nu \quad (5.1)$$

Recall that by Definition 4.2 the extended system $\mathcal{R}_{+f}$ has possibly infinitely many rules of the form $S_f \mathbf{w} \to f(\mathbf{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}^{\mathcal{c}} = \lambda x.1 \qquad \mathcal{J}_{S_f}^{\mathcal{s}} = \lambda x.\mu * |f|(x) + \nu$$

Recall that $|f|(n) = \max_{|y| \le n} |f(y)|$. Hence, $|f|$ is weakly monotonic, and therefore so is $\mathcal{J}_{S_f}^{\mathcal{s}}$. This orients the rules in $\mathcal{R}_f$ because $\llbracket S_f \mathbf{w} \rrbracket^{\mathcal{c}} = 1 > 0 = \text{cost}(f(\mathbf{w}))$, and $\llbracket S_f \mathbf{w} \rrbracket^{\mathcal{s}} = \mu * |f|(\llbracket \mathbf{w} \rrbracket^{\mathcal{s}}) + \nu \ge \mu * |f|(\lvert w \rvert) + \nu \ge \mu * |f(w)| + \nu$ by definition of $|f|$, which is superior or equal to $\llbracket f(\mathbf{w}) \rrbracket^{\mathcal{s}}$.

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

*Proof.* As $\mathcal{J}_{\cdot\cdot}^{\mathcal{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}_{\cdot\cdot}^{\mathcal{c}}(\mathcal{J}_{S_f}^{\mathcal{c}}, \mathcal{J}_{S_f}^{\mathcal{s}}, \llbracket \mathbf{w} \rrbracket^{\mathcal{s}}) = \text{cost}(FS_f \mathbf{w})$ (we omit $\alpha$ and $\zeta$ here because there are no variables in $FS_f \mathbf{w}$, and therefore the valuations are not relevant to the cost value). By Corollary 3.5, this serves as a bound on the derivation height of $FS_f \mathbf{w}$. $\square$

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. This is very much in the style of what has been done for first-order rewriting and the $\lambda$-calculus in the past [AM10, DLM12, AL16].

5.2. **Bounding The Oracle Input.** We first show that calling the oracle along a computation does not introduce an exponential overhead along the way. More precisely, 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 $FS_f \mathbf{w} \to_{\mathcal{R}} \mathbf{v}$, 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 any polynomial bounding $\mathcal{J}_{\cdot\cdot}^{\mathcal{c}}$. Since $P$ is a second-order polynomial, each occurrence of a sub-expression $F^c(E)$ in $P$ is itself a second-order polynomial, and so
is E. Let us enumerate these arguments as $E_1, \dots, E_n$. We can then construct the new polynomial $Q$ as follows:

$$Q := \sum_i E_i \quad \text{where occurrences of } F^c(E_j) \text{ inside } E_i \text{ are replaced by 1}$$

The idea here is that the polynomial $Q$ sums up all those expressions $E_i$ (with $1 \le i \le n$) given to $F^c$ as argument. We do this because intuitively, if during the computation a word $\underline{v}$ is ever given to the oracle, then the cost for the oracle computation must be accounted for in $\mathcal{J}_F^c$. Hence, $[\underline{v}]^s$ must be bounded by some $E_i$, so certainly by the sum of all $E_i$. We can safely replace occurrences of $F^c(E_j)$ that occur inside another $E_i$ by 1 because $F^c$ will be instantiated by $\mathcal{J}_{S_f}^c = \lambda x.1$ (or, in Lemma 5.3, by a function that maps specific input to 1).

Due to this replacement, $F^c$ does not occur in $Q$, so $Q$ is only parametrized by $F^s$ and some type-0 variable $x$. It is also possible for $Q$ to be a constant polynomial, or to be parametrized only by a type-0 variable. Its final shape depends on the arguments provided to the $F^c$ in $P$. We let $B(G, y) := Q(\lambda z.\mu * G(z) + \nu, \mu * y + \nu)$.

**Example 5.2.** Let us illustrate the construction of such polynomial $Q$. Consider the following polynomial $P$.

$$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$ is built by adding each of those arguments given to $F^c$. We get

$$\begin{aligned} Q &= 3 + F^s(9 * x) + 12 + 3 + x * 1 + 2 \\ &= 20 + F^s(9 * x) + x \end{aligned}$$

Finally, we construct the polynomial $B$.

$$\begin{aligned} 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 \end{aligned}$$

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 5.3.** Fix $f, w$. Let $G : \mathbb{N} \to \mathbb{N}$ with $G(z) = \mathcal{J}_{S_f}^c(z)$ if $z \le B(|f|, |w|)$. Then $P(G, \mathcal{J}_{S_f}^s, [\underline{w}]^s) = P(\mathcal{J}_{S_f}^c, \mathcal{J}_{S_f}^s, [\underline{w}]^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 5.3 is used in the following key result:

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

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

$$\begin{array}{rcl@{\quad}l} S'_f \underline{x} & \to & \underline{f(x)} & \text{if } |x| \le B(|f|, |w|) & \text{helper } \mathbf{0} y \to y \\ S'_f \underline{x} & \to & \text{helper} \upharpoonright \mathcal{N} \downharpoonright \underline{f(x)} & \text{otherwise} & \text{helper } (s x) y \to \text{helper } xy \end{array}$$
Where ⌜N⌝ is the unary number encoding of N, as introduced in Section 2.1. Notice that by definition the rules for S'f will produce f(x) in a single step if |x| ≤ B(|f|, |w|) but they will take N + 2 steps otherwise. Also observe that Sf and S'f behave the same; that is, Sf x and S'f x have the same normal form on any input x. We extend the interpretation function of the original signature with:

$$ \mathcal{J}_{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}_{S'f}^{s} = \mathcal{J}_{Sf}^{s} $$

$$ \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 5.3, $\text{cost}(\text{FS}'_f \underline{w}) \le P(\mathcal{J}_{S'_f}^c, \mathcal{J}_{S'_f}^s, [[\underline{w}]^s]) = P(\mathcal{J}_{S_f}^c, \mathcal{J}_{S_f}^s, [[\underline{w}]^s]) \le D(|f|, |w|) = N$. Yet, as we have $\text{FS}_f \underline{w} \to_{\mathcal{R}_{+f}}^*$, we also have $\text{FS}_f \underline{w} \to_{\mathcal{R}\cup\mathcal{R}'_{f,w}} C[S_f \underline{x}]$, where $C'$ is obtained from C by replacing all occurrences of $S_f$ by $S'_f$. Since $|x| > B(|f|, |w|)$ by assumption, the reduction $\text{FS}'_f \underline{w} \to_{\mathcal{R}\cup\mathcal{R}'_{f,w}}^*$, $C[S'_f \underline{w}] \to_{\mathcal{R}\cup\mathcal{R}'_{f,w}}^* C[\underline{f}(x)]$ takes strictly more than N steps, contradicting Corollary 3.5. $\square$

**5.3. Graph Rewriting.** Lemma 5.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 $\text{FS}_f \underline{w}$. However, as observed in Section 5.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 5.5.** 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.

<figure><img src="image_10.png" /><figcaption>FIGURE 1. A term graph, its simplified version, and two graphs with sharing</figcaption></figure>

Term graphs can be denoted visually in an intuitive way. For example, using $\Sigma$ from Example 2.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 Fig. 1a. We use $\perp$ to indicate unlabeled vertices and a circle for $\Lambda$. We will typically omit vertex names, as done in Fig. 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) = f \text{ if } s|_p = 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]_G$ and $[\text{add } 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 5.6.** Let $G = (V, \text{label}, \text{succ}, \Lambda)$ and $v \in V$. The **subgraph reach**($G, v$) of $G$ with root $v$ is the term graph $(V', \text{label}', \text{succ}', v)$ where $V'$ contains those nodes $v' \in V$ such that there exists a path from $v$ to $v'$ and $\text{label}', \text{succ}'$ are respectively the restrictions of $\text{label}$ and $\text{succ}$ to $V'$.

**Definition 5.7.** 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{label}_H(\phi(v))$ and $\text{succ}_H(\phi(v))$ may be anything.)

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

**Lemma 5.9.** Let $(\ell \to r, v, \phi)$ be a redex in $G$, $x \in \text{vars}(\ell)$, and let $a_x$ be the corresponding vertex in $[\ell]_G$. Then $v \neq \phi(a_x)$, nor is there a path from $\phi(a_x)$ to $v$.

*Proof.* Note that $\ell$ is not a variable, so there is a (non-empty) path from the root of $[\ell]_G$ to each $a_x$; hence, by definition of homomorphism, there is a path from $\phi(\Lambda_{[\ell]_G}) = v$ to each $\phi(a_x)$. Since $G$ is acyclic, this means that $\phi(a_x)$ cannot be $v$, nor can there be a path from $\phi(a_x)$ back to $v$. $\square$

**Definition 5.10.** Let $G$ be a term graph and $v_1, v_2$ vertices in $G$ such that no path exists from $v_2$ to $v_1$. 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$ and $\Lambda'_G$ given by:

$$ \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$, which does not introduce any cycles because there is no path from $v_2$ to $v_1$. With these definitions in hand, we can define *contraction* of term graphs:

**Definition 5.11.** Let $G$ be a term graph, and $(\rho, v, \phi)$ a redex in $G$ with $\rho \in \mathcal{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}\} \ (\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}) = f$ if $r|_p = f$ and $\text{label}_H(\bar{p}) = @$ otherwise

- $\text{succ}_H(\bar{p}) = \varepsilon$ if $r|_p = 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 \bar{\mathbb{H}}]$. Otherwise, let $I = H[v \gg \bar{\mathbb{H}}]$, so with all references to $v$ redirected to the root vertex for $r$. (Note that in the first case, there is no path from $\phi(a_x)$ to $v$ by Lemma 5.9; and in the second case, every path from $\bar{\mathbb{H}}$ into $V_G$ passes through some $\phi(a_y)$, so again by Lemma 5.9 there is no path from $\bar{\mathbb{H}}$ to $v$, and therefore the redirection is allowed.)

(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 Fig. 2a with a rule $\text{add } 0 \ 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 Fig. 2b, and the result of the garbage collection in Fig. 2c.

<figure><img src="image_11.png" /><figcaption>FIGURE 2. Reducing a graph with the rule $\text{add } 0 \ y \to y$</figcaption></figure>

Second, we consider a reduction of the graph in Fig. 3a by $\text{mult}(s \ x) \ y \to \text{add} \ y$ ($\text{mult} \ x \ y$). Unlike the previous example, this graph has sharing. Fig. 3b 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 Fig. 3c.

<figure><img src="image_12.png" /><figcaption>FIGURE 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 (that is, one in which no variable occurs more than once), clearly $[[s]_G]_G^{-1} = s$ modulo variable renaming. We make the following observation:

**Lemma 5.12.** 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_{\mathcal{R}_{+f}} [H]_G^{-1}$. Moreover, if $s \to_{\mathcal{R}_{+f}} t$ for some $t$, then there exists $H$ such that $G \rightsquigarrow H$.

Consequently, if $\to_{\mathcal{R}_{+f}}$ is terminating, then so is $\rightsquigarrow$; and if $[s]_G \rightsquigarrow^n G$ for some ground term $s$ then $s \to_{\mathcal{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 5.13.** If $[FS_f w]_G \rightsquigarrow^n G$, then $n \le D(|f|, |w|)$; and if $G$ cannot be reduced by $\rightsquigarrow$, then $[G]_G^{-1} = \Psi(f, w)$.

## 5.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.14.** 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 intermediate graph in the reduction $[G w]_G \to_{\mathcal{R}}^+ [q]_G$ is polynomially bounded by a second-order polynomial over $|f|, |w|$:

**Lemma 5.15.** 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 5.1, $a$ is the constant from Lemma 5.14, and $B$ is the polynomial from Section 5.2. This suffices, because there are at most $D(|f|, |w|)$ steps (Lemma 5.1, Corollary 5.13), each of which increases the graph size by at most $\max(a, |f|(B(|f|, |w|)))$ according to Lemmas 5.4 and 5.14. (Note that, by the Oracle Subterm lemma, $B$ takes the size $|w|$ of the original input $w$ as its second argument, not the current size of the term.) $\square$

All in all, we are finally ready to prove the soundness side of the main theorem:
**Theorem 5.16 (Soundness).** Let $\mathcal{R}$ be a finite orthogonal STRS admitting a polynomially bounded interpretation. If $\mathsf{F}$ computes a type-2 functional $\Psi$, then $\Psi \in \mathsf{BFF}$.

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

* that we can represent each graph in polynomial space in the size of the graph; simply, we can make use of an adjacency-matrix representation of the graph;

* that we simulate any rewriting step that does not call the oracle (so using a rule in $\mathcal{R}$) following the contraction algorithm we defined in Definition 5.11, which is clearly feasible to do in polynomial time in the size of the graph; of course this could in principle involve the creation of new nodes and edges, but the amount of them is statically bounded by the size of the underlying set or rewrite rules (excluding those involving the oracle).

* and that each oracle call (implemented in rewriting by a $\mathcal{R}_f$-step $S_f \xrightarrow{\mathsf{x}} \mathsf{y}$) is resolved by copying $\mathsf{x}$ to the query tape, transitioning to the query state, and from the answer state copying $\mathsf{y}$ from the answer tape to the main tape. By Lemma 5.4 this is doable in polynomial time in $|f|, |w|$ and the graph size.

By Lemma 5.15, 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 2.5, $\Psi$ is in $\mathsf{BFF}_2$. □

## 6. COMPLETENESS

Recall from Section 4 that to prove completeness we have to show the following: if a given type-2 functional $\Psi$ is in $\mathsf{BFF}_2$, then there exists an orthogonal STRS computing $\Psi$ and admitting a polynomially bounded interpretation. In this section, we prove this implication by providing an encoding of polynomial time Oracle Turing Machines as STRSs that admit a polynomially bounded interpretation.

The encoding is divided into three steps. In Section 6.1, we define the function symbols that allow us to encode any possible machine configuration as terms. In Section 6.2, we encode machine transitions as reduction rules that rewrite configuration terms. This allows us to simulate one transition in an OTM as one or more rewriting steps on the corresponding rewrite system. Lastly, we design an STRS which simulates a complete execution of an OTM in polynomially many steps. Achieving this polynomial bound is non-trivial and is done in Section 6.3 and Section 6.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, \mathsf{B}\}$.
**6.1. Encoding Machine Configurations as Terms.** Recall from Section 4 that we have o, i: bit, ::= bit ⇒ word ⇒ word and []: word, which are the basic constructors for encoding binary words as terms. To represent a (partial) tape, we also introduce b: bit for the blank symbol. Now for instance a tape with content 011B01BB... (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; 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...w_{p-1}\#w_p w_{p+1}...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...w_{p-1}$, and the *right* word $w_p...w_k$. To represent a tape configuration as a term, we introduce three symbols:

$$L: \text{word} \Rightarrow \text{left} \qquad R: \text{word} \Rightarrow \text{right} \qquad \text{split}: \text{left} \Rightarrow \text{right} \Rightarrow \text{tape}$$

Here, L, R hold the content<fnref n="1" /> of the left and right split of the tape, respectively. For convenience in rewriting transitions, later on, we encode the left side of the split in reverse order. More precisely, we encode the configuration $w_1...w_{p-1}\#w_p w_{p+1}...w_k$ as the term

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

The symbol currently being read is the first element of the list below R; in case of R[], this symbol is 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: tape ⇒ tape ⇒ tape ⇒ config. Thus, a configuration $(q, t_1, t_2, t_3)$ is represented by a term $qT_1 T_2 T_3$.

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

$$\text{initial}(w) := q_0 (\text{split}(L[])(\text{R}[w])) (\text{split}(L[])(\text{R}[\])) (\text{split}(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{align*}
\mathcal{J}_o^s &= 0 & \mathcal{J}_o^s &= 0 & \mathcal{J}_o^s &= \lambda xy.x + y + 1 \\
\mathcal{J}_i^s &= 0 & \mathcal{J}_i^s &= \lambda x.x & \mathcal{J}_{\text{split}}^s &= \lambda xy.x + y \\
\mathcal{J}_b^s &= 0 & \mathcal{J}_b^s &= \lambda x.x & \mathcal{J}_q^s &= \lambda xyz.x + y \quad (\text{for all states } q)
\end{align*}$$

Hence, we satisfy the size component of the requirements in Definition 4.4. We have $[\underline{w}]^s = |w|$; 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.

<footnote n="1">¹While we technically do not need these two constructors (we could have split: word ⇒ word ⇒ tape), they serve to make configurations more human-readable.</footnote>
6.2. **Encoding Machine Transitions as Rules.** 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[t]{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, \mathbf{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 of the machine. Let us describe such rules as follows:

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

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

Moreover, for transitions $q \xrightarrow[1]{\mathbf{B}/w, L} l$ (so where $\mathbf{B}$ is read), we add a rule:

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

These rules respectively handle the steps where a tape configuration is changed from $u_1 \dots u_{p-1} u_p \# r u_{p+2} \dots u_k$ to $u_1 \dots u_{p-1} \# u_p i u_{p+2} \dots u_k$, and where a tape configuration is changed from $u_1 \dots u_k \# \mathbf{r}$ to $u_1 \dots \# 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:

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

This is implemented by the following rules:

$$ \text{step } F(\text{query } t_1 (\text{split } x(\mathbf{R}y)) t_3) \to \text{answer } t_1 (\text{split } (\mathbf{L}[])(\mathbf{R}[])) (\text{split } (\mathbf{L}[])(\mathbf{R}(F(\text{clean } y))))) $$

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

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

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

The various **step** rules and the **clean** rules defined above are non-overlapping because we consider deterministic OTMs. Additionally, they are also left-linear. We can orient such rules as follows:

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

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

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

**Lemma 6.2.** Let $M_f$ be an OTM and $C, D$ be machine configurations of $M_f$ such that $C \rightsquigarrow D$. Then step $S_f[C] \xrightarrow{\mathbf{r}} [D]$, where $[C]$ is the term encoding of $C$.
**6.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:

$$ \begin{array}{l} \text{execute } F(\mathbf{q} x y z) \rightarrow \text{execute } F(\text{step}(\mathbf{q} x y z)) \quad \text{for } \mathbf{q} \neq \text{end} \\ \text{execute } F(\text{end}(\text{split}(\mathbf{L} x)(\mathbf{R} w)) y z) \rightarrow \text{clean } w \end{array} $$

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 [KC96, 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 6.3.** 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. $\square$

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

$$ \begin{array}{lclcl} \text{len } [] & \rightarrow & 0 & \quad & \text{len } (x::y) \rightarrow \text{s } (\text{len } y) \\ \max 0 m & \rightarrow & m & \quad & \max (\text{s } n) 0 & \rightarrow & \text{s } n \\ \text{limit } [] n & \rightarrow & [] & \quad & \text{limit } (x::y) 0 & \rightarrow & [] \\ \text{retif } [] n z & \rightarrow & z & \quad & \text{retif } (x::y) 0 z & \rightarrow & [] \end{array} \quad \begin{array}{l} \text{max } (\text{s } n) (\text{s } m) \rightarrow \text{s } (\max n m) \\ \text{limit } (x::y) (\text{s } n) \rightarrow x::(\text{limit } y n) \\ \text{retif } (x::y) (\text{s } n) z \rightarrow \text{retif } y n z \end{array} $$

$$ \begin{array}{lclcl} \text{tryapply } F a n & \rightarrow & \text{len } (\text{retif } a n (F (\text{limit } a n))) & & \\ \text{tryall } F \emptyset n & \rightarrow & 0 & \quad & \text{tryall } F (scons a tl) n \rightarrow \max (\text{tryapply } F a n) (\text{tryall } F t l n) \end{array} $$

The cost-size interpretations of these rules are as follows.

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

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| \le n$, and to $⌜0⌝$ otherwise.
Thus, it indeed returns exactly $|F|_{\{a\}}(n)$.

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

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

$$ \begin{align*} & \text{cost}(\text{len } (\text{retif } a n (F (\text{limit } a n)))) \\ &= [\text{len } (\text{retif } a n (F (\text{limit } a n))))]^c + [\text{retif } a n (F (\text{limit } a n))]^c + \\ & \quad [F (\text{limit } a n)]^c + [\text{limit } a n]^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{scons}}^{s} &= \lambda xy.y + 1 & \mathcal{J}_{\text{scons}}^{c} &= \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*} [\text{tryall } F \ (\text{scons } a \ tl) \ n]^s &= F^s(n) \\ &= \max(F^s(n), F^s(n)) \\ &= [[\max (\text{tryapply } F a n) (\text{tryall } F tl n)]^s \end{align*} $$

and

$$ \begin{align*} [\text{tryall } F \ (\text{scons } a \ tl) \ n]^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) \\ &= [\text{tryall } F \ tl \ n]^c + (F^c(n) + 2 * F^s(n) + 2 * n + 6) \\ &= [\text{tryall } F \ tl \ n]^c + [\text{tryapply } F a n]^c + F^s(n) + 2 \\ &= [\text{tryall } F \ tl \ n]^c + [\text{tryapply } F a n]^c + [[\max (\text{tryapply } F a n) (\text{tryall } F \ tl \ n)]^c + 1 \\ &> \text{cost}(\max (\text{tryapply } F a n) (\text{tryall } F \ tl \ n)) \end{align*} $$

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} \text{an.} 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 tryall and the functions add, mult from Example 2.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|$.

**6.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 n m z a 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** ⇒ **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{align*}
& F F w \rightarrow F' F (\text{len } w) (\mathbf{q}_0 (\text{split}(L [])) (R w)) (\text{split}(L [])) (R [])) (\text{split}(L [])) (R [])) \\
& F' F z c \rightarrow \begin{array}{@{}l@{}} \text{execute} F \Theta_{F;z;\emptyset}^{P_M+1} \circ z \emptyset c \\ \qquad \text{execute } F (s n) m z a (q t_1 t_2 t_3) \rightarrow \\ \qquad \text{execute } F n (n m) z (\text{step } F (q t_1 t_2 t_3)) \text{ for } q \notin \{\text{query, end}\} \\ \text{execute } F (s n) m z a (\text{query } t_1 t_2 t_3) \rightarrow \\ \qquad \text{execute'} F n (n m) z (\text{scons } (\text{extract } t_2) a) (\text{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 (\text{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 \quad \text{minus } 0 (n y) \rightarrow 0 \quad \text{minus } (s x) (n y) \rightarrow \text{minus } x y \end{array} \\
& \text{That is, an execution on } FS_f w \text{ first computes the length of } w \text{ and } P_M(|f|_{\emptyset}, |w|), \text{ and uses these as arguments to execute. Each normal transition lowers the number } n \text{ of steps we are allowed to do and increases the number } m \text{ of steps we have done. Each oracle transition updates } A, \text{ and either lowers } n \text{ by one, or updates it to the new value } P_M(|f|_A, |w|) - m, \text{ since we have already done } m \text{ steps. Once we read the final state, the answer is read off the first tape.}
\end{align*}
$$

That is, an execution on $FS_f w$ first computes the length of $w$ and $P_M(|f|_\emptyset, |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 $m$ 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. So let us provide the interpretations for the **nnat** functions symbols and the two simple rules for **extract** and **minus**, given as follows:

$$
\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

$$
\mathrm{cost}(\Theta_{F;z;a}^{P}) \leq \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:

$$
\begin{align*}
\mathcal{J}_F^s &= \lambda F n.n + P_M(F, n) + 1 \\
\mathcal{J}_{F'}^s &= \lambda F z c.c + P_M(F, z) + 1 \\
\mathcal{J}_{\text{execute}}^s &= \lambda F n m z a c.c + \theta_{F,z,n,m} \\
\mathcal{J}_{\text{execute}'}^s &= \lambda F n m z a c.c + 1 + \theta_{F,z,n,m}
\end{align*}
$$

And the cost interpretations by:

$$
\begin{align*}
\mathcal{J}_F^c &= \lambda F n.(P_M(F^s, n) + 1)* \\
&\quad (8 + 3 * P_M(F^s, n) + 2 * n + F^c(P_M(F^s, n) + n + 1) + \\
&\qquad \qquad \qquad \mathrm{POLY}_{F,z}[P_M(F^s, n) + 1]) + 6 + 2 * n + \mathrm{POLY}_{F,z}[0]
\end{align*}
$$

$$
\begin{align*}
\mathcal{J}_{F'}^c &= \lambda F z c.(P_M(F^s, z) + 1)* \\
&\quad (8 + 3 * P_M(F^s, z) + 2 * c + F^c(P_M(F^s, z) + 1 + c) + \\
&\qquad \qquad \mathrm{POLY}_{F,z}[P_M(F^s, z) + 1]) + 4 + c + \mathrm{POLY}_{F,z}[0]
\end{align*}
$$

$$
\begin{align*}
\mathcal{J}_{\text{execute}}^{c} &= \lambda F n m z a c. \theta_{F,z,n,m} * \\
&\quad (5 + 2 * (\theta_{F,z,n,m} + c) + F^c(\theta_{F,z,n,m} + c) + \\
&\qquad \qquad \mathrm{POLY}_{F,z}[\theta_{F,z,n,m} + a] + P_M(F^s, z)) + 3 + \theta_{F,z,n,m} + c
\end{align*}
$$

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

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

$$
\begin{align*}
\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{align*}
$$

Observe that this holds since $\max(a+1, b+1) = \max(a, b) + 1$. We also have the following:

$$
\begin{align*}
\theta_{F,z,n,m} &= \max(P_M(F^s, z) + 1 - m, n) \\
&\ge \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 \minus \theta_{F;z;m}^{P_M+1} \rrbracket^s} , m
\end{align*}
$$

The inequalities now follow by writing out definitions.

**Theorem 6.4.** If $\Psi \in \text{BFF}_2$, 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.

7. CONCLUSION

This paper gives the first characterization of the class of type-2 basic feasible functionals by term rewriting based on the interpretation method and in particular on polynomial cost–size interpretations. Surely, it would make sense to try to go beyond types of order 2 and try to characterize classes of basic feasible functionals of order at least 3. Such classes are less well understood than their order-2 counterparts and perhaps an analysis based on tools from rewriting could help to shed some light on their nature (see, e.g., Hugo Férée’s work on this subject [Fér17]).
REFERENCES

[AB09] Sanjeev Arora and Boaz Barak. *Computational Complexity: A Modern Approach*. Cambridge University Press, USA, 1st edition, 2009.

[AL16] Beniamino Accattoli and Ugo Dal Lago. (leftmost-outermost) beta reduction is invariant, indeed. *Log. Methods Comput. Sci.*, 12(1), 2016. doi:10.2168/LMCS-12(1:4)2016.

[AM10] Martin Avanzini and Georg Moser. Closing the gap between runtime complexity and polytime computability. In Christopher Lynch, editor, *Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scotland, UK*, volume 6 of *LIPIcs*, pages 33–48. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. doi:10.4230/LIPICS.RTA.2010.33.

[AM13] Martin Avanzini and Georg Moser. Polynomial path orders. *Log. Methods Comput. Sci.*, 9(4), 2013. doi:10.2168/LMCS-9(4:9)2013.

[AMS16] Martin Avanzini, Georg Moser, and Michael Schaper. TcT: Tyrolean complexity tool. In Marsha Chechik and Jean-François Raskin, editors, *Proceedings of TACAS 2016 conference*, volume 9636 of *Lecture Notes in Computer Science*, pages 407–423. Springer, 2016. doi:10.1007/978-3-662-49674-9\_24.

[Bai11] Patrick Baillot. Elementary linear logic revisited for polynomial time and an exponential time hierarchy. In Hongseok Yang, editor, *Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings*, volume 7078 of *Lecture Notes in Computer Science*, pages 337–352. Springer, 2011. doi:10.1007/978-3-642-25318-8\_25.

[BC92] Stephen J. Bellantoni and Stephen A. Cook. A new recursion-theoretic characterization of the polytime functions. *Comput. Complex.*, 2:97–110, 1992. doi:10.1007/BF01201998.

[BCE⁺⁹⁸] Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The relative complexity of NP search problems. *J. Comput. Syst. Sci.*, 57(1):3–19, 1998. doi:10.1006/JCSS.1998.1575.

[BCMT98] Guillaume Bonfante, Adam Cichon, Jean-Yves Marion, and Hélène Touzet. Complexity classes and rewrite systems with polynomial interpretation. In Georg Gottlob, Etienne Grandjean, and Katrin Seyr, editors, *Computer Science Logic, 12th International Workshop, CSL '98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings*, volume 1584 of *Lecture Notes in Computer Science*, pages 372–384. Springer, 1998. doi:10.1007/10703163\_25.

[BCMT01] Guillaume Bonfante, Adam Cichon, Jean-Yves Marion, and Hélène Touzet. Algorithms with polynomial interpretation termination proof. *J. Funct. Program.*, 11(1):33–53, 2001. doi:10.1017/S0956796800003877.

[BDBRDR18] Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca. Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. *Inf. Comput.*, 261:55–77, 2018. doi:10.1016/J.IC.2018.05.005.

[BDL12] Patrick Baillot and Ugo Dal Lago. Higher-order interpretations and program complexity. In *Proceedings of CSL 2012*, volume 16 of *LIPIcs*, pages 62–76. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. doi:10.4230/LIPICS.CSL.2012.62.

[BL16] Patrick Baillot and Ugo Dal Lago. Higher-order interpretations and program complexity. *Inf. Comput.*, 248:56–81, 2016. URL: https://doi.org/10.1016/j.ic.2015.12.008.

[BLKV24] Patrick Baillot, Ugo Dal Lago, Cynthia Kop, and Deivid Vale. On basic feasible functionals and the interpretation method. In Naoki Kobayashi and James Worrell, editors, *Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II*, volume 14575 of *Lecture Notes in Computer Science*, pages 70–91. Springer, 2024. doi:10.1007/978-3-031-57231-9\_4.

[BLM12] Patrick Baillot, Ugo Dal Lago, and Jean-Yves Moyen. On quasi-interpretations, blind abstractions and implicit complexity. *Math. Struct. Comput. Sci.*, 22(4):549–580, 2012. doi:10.1017/S0960129511000685.

[BMM05] Guillaume Bonfante, Jean-Yves Marion, and Jean-Yves Moyen. Quasi-interpretations and small space bounds. In Jürgen Giesl, editor, *Term Rewriting and Applications, 16th International*
Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, pages 150-164. Springer, 2005. doi:10.1007/978-3-540-32033-3\_12.

[BMM11] Guillaume Bonfante, Jean-Yves Marion, and Jean-Yves Moyen. Quasi-interpretations a way to control resources. Theor. Comput. Sci., 412(25):2776-2796, 2011. doi:10.1016/j.tcs.2011.02.007.

[BW96] Arnold Beckmann and Andreas Weiermann. A term rewriting characterization of the polytime functions and related complexity classes. Arch. Math. Log., 36(1):11-30, 1996. doi:10.1007/s001530050054.

[CK89] Stephen A. Cook and Bruce M. Kapron. Characterizations of the basic feasible functionals of finite type (extended abstract). In 30th Annual Symposium on Foundations of Computer Science, Research Triangle Park, North Carolina, USA, 30 October - 1 November 1989, pages 154-159. IEEE Computer Society, 1989. doi:10.1109/SFCS.1989.63471.

[Cob65] Alan Cobham. The intrinsic computational difficulty of functions. In Yehoshua Bar-Hillel, editor, Logic, Methodology and Philosophy of Science: Proceedings of the 1964 International Congress (Studies in Logic and the Foundations of Mathematics), pages 24-30. North-Holland Publishing, 1965.

[Con73] Robert L. Constable. Type two computational complexity. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA, pages 108-121. ACM, 1973. doi:10.1145/800125.804041.

[Der82] Nachum Dershowitz. Orderings for term-rewriting systems. Theor. Comput. Sci., 17:279-301, 1982. doi:10.1016/0304-3975(82)90026-3.

[DLH11] Ugo Dal Lago and Martin Hofmann. Realizability models and implicit complexity. Theor. Comput. Sci., 412(20):2029-2047, 2011. doi:10.1016/J.TCS.2010.12.025.

[DLM12] Ugo Dal Lago and Simone Martini. On constructor rewrite systems and the lambda calculus. Log. Methods Comput. Sci., 8(3), 2012. doi:10.2168/LMCS-8(3:12)2012.

[DR06] Norman Danner and James S. Royer. Adventures in time and space. In J. Gregory Morrisett and Simon L. Peyton Jones, editors, Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, pages 168-179. ACM, 2006. doi:10.1145/1111037.1111053.

[Fér17] Hugo Férée. Game semantics approach to higher-order complexity. J. Comput. Syst. Sci., 87:1-15, 2017. doi:10.1016/J.JCSS.2017.02.003.

[FHHP15] Hugo Férée, Emmanuel Hainry, Mathieu Hoyrup, and Romain Péchoux. Characterizing polynomial time complexity of stream programs using interpretations. Theor. Comput. Sci., 585:41-54, 2015. doi:10.1016/J.TCS.2015.03.008.

[Gir98] Jean-Yves Girard. Light linear logic. Inf. Comput., 143(2):175-204, 1998. doi:10.1006/INCO.1998.2700.

[GTS04] Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In Franz Baader and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, volume 3452 of Lecture Notes in Computer Science, pages 301-331. Springer, 2004. doi:10.1007/978-3-540-32275-7\_21.

[HKMP20] Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux. A tier-based typed programming language characterizing feasible functionals. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 535-549. ACM, 2020. doi:10.1145/3373718.3394768.

[HKMP22] Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux. Complete and tractable machine-independent characterizations of second-order polytime. In Patricia Bouyer and Lutz Schröder, editors, 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, doi:10.1007/978-3-540-32275-7\_22.
*Proceedings*, volume 13242 of *Lecture Notes in Computer Science*, pages 368–388. Springer, 2022. doi:10.1007/978-3-030-99253-8\_19.

[Hof03] Martin Hofmann. Linear types and non-size-increasing polynomial time computation. *Inf. Comput.*, 183(1):57–85, 2003. doi:10.1016/S0890-5401(03)00009-9.

[HP20] Emmanuel Hainry and Romain Péchoux. Theory of higher order interpretations and application to basic feasible functions. *Log. Methods Comput. Sci.*, 16(4), 2020. URL: https://lmcs.episciences.org/6973.

[HS69] Juris Hartmanis and Richard Edwin Stearns. Automata-based computational complexity. *Inf. Sci.*, 1(2):173–184, 1969. doi:10.1016/0020-0255(69)90014-0.

[IRK01] Robert J. Irwin, James S. Royer, and Bruce M. Kapron. On characterizations of the basic feasible functionals (part i). *J. Funct. Program.*, 11(1):117–153, 2001. doi:10.1017/S0956796800003841.

[Jon01] Neil D. Jones. The expressive power of higher-order types or, life without CONS. *J. Funct. Program.*, 11(1):5–94, 2001. URL: https://doi.org/10.1017/S0956796800003889.

[KC91] Bruce M. Kapron and Stephen A. Cook. A new characterization of Mehlhorn's polynomial time functionals (extended abstract). In *32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991*, pages 342–347. IEEE Computer Society, 1991. doi:10.1109/SFCS.1991.185389.

[KC96] Bruce M. Kapron and Stephen A. Cook. A new characterization of type-2 feasibility. *SIAM J. Comput.*, 25(1):117–132, 1996. doi:10.1137/S0097539794263452.

[KC12] Akitoshi Kawamura and Stephen A. Cook. Complexity theory for operators in analysis. *ACM Trans. Comput. Theory*, 4(2):5:1–5:24, 2012. doi:10.1145/2189778.2189780.

[KS17] Cynthia Kop and Jakob Grue Simonsen. Complexity hierarchies and higher-order cons-free term rewriting. *Log. Methods Comput. Sci.*, 13(3), 2017. doi:10.23638/LMCS-13(3:8)2017.

[KS18] Bruce M. Kapron and Florian Steinberg. Type-two polynomial-time and restricted lookahead. In Anuj Dawar and Erich Grädel, editors, *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018*, pages 579–588. ACM, 2018. doi:10.1145/3209108.3209124.

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

[KV21] Cynthia Kop and Deivid Vale. Tuple interpretations for higher-order complexity. In Naoki Kobayashi, editor, *6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)*, volume 195 of *LIPIcs*, pages 31:1–31:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.FSCD.2021.31.

[KV23] C. Kop and D. Vale. Cost-size semantics for call-by-value higher-order rewriting. In *Proc. FSCD*, volume 260 of *LIPIcs*, pages 15:1–15:19, 2023. doi:10.4230/LIPIcs.FSCD.2023.15.

[KvOvR93] Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk. Combinatory reduction systems: Introduction and survey. *Theor. Comput. Sci.*, 121(1&2):279–308, 1993. doi:10.1016/0304-3975(93)90091-7.

[Laf04] Yves Lafont. Soft linear logic and polynomial time. *Theor. Comput. Sci.*, 318(1-2):163–180, 2004. doi:10.1016/J.TCS.2003.10.018.

[Lan79] Dallas S Lankford. On proving term rewriting systems are noetherian. *Memo MTP-3*, 1979. URL: https://www.ens-lyon.fr/LIP/REWRITING/TERMINATION/Lankford_Poly_Term.pdf.

[Lei91] Daniel Leivant. 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*, pages 2–11. IEEE Computer Society, 1991. doi:10.1109/LICS.1991.151625.

[LM94] Daniel Leivant and Jean-Yves Marion. Ramified recurrence and computational complexity II: substitution and poly-space. In Leszek Pacholski and Jerzy Tiuryn, editors, *Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers*, volume 933 of *Lecture Notes in Computer Science*, pages 486–500. Springer, 1994. doi:10.1007/BFB0022277.
[LS16] Ugo Dal Lago and Ulrich Schöpp. Computation by interaction for space-bounded functional programming. *Inf. Comput.*, 248:150–194, 2016. doi:10.1016/J.IC.2015.04.006.

[Meh76] Kurt Mehlhorn. Polynomial and abstract subrecursive classes. *J. Comput. Syst. Sci.*, 12(2):147–178, 1976. doi:10.1016/S0022-0000(76)80035-9.

[MM00] Jean-Yves Marion and Jean-Yves Moyen. Efficient first order functional program interpreter with time bound certifications. In Michel Parigot and Andrei Voronkov, editors, *Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings*, volume 1955 of *Lecture Notes in Computer Science*, pages 25–42. Springer, 2000. doi:10.1007/3-540-44404-1_3.

[MN70] Zohar Manna and Steven Ness. On the termination of Markov algorithms. In *Proceedings of the Third Hawaii International Conference on System Science*, pages 789–792, 1970.

[MN98] Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. *Theor. Comput. Sci.*, 192(1):3–29, 1998. doi:10.1016/S0304-3975(97)00143-6.

[Oit01] Isabel Oitavem. Implicit characterizations of pspace. In Reinhard Kahle, Peter Schroeder-Heister, and Robert F. Stärk, editors, *Proof Theory in Computer Science, International Seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001, Proceedings*, volume 2183 of *Lecture Notes in Computer Science*, pages 170–190. Springer, 2001. doi:10.1007/3-540-45504-3_11.

[Ter03] Terese. *Term rewriting systems*, volume 55 of *Cambridge tracts in theoretical computer science*. Cambridge University Press, 2003.

[Val24] Deivid Vale. *On Semantical Methods for Higher-Order Complexity Analysis*. PhD thesis, Radboud University Nijmegen, 2024. URL: https://hdl.handle.net/2066/304473.

[vdP96] Jaco van de Pol. *Termination of Higher-order Rewrite Systems*. PhD thesis, University of Utrecht, 1996. URL: https://www.cs.au.dk/~jaco/papers/thesis.pdf.