# Complete and tractable machine-independent characterizations of second-order polytime

Emmanuel Hainry, Bruce M Kapron, Jean-Yves Marion, Romain Péchoux

► To cite this version:

Emmanuel Hainry, Bruce M Kapron, Jean-Yves Marion, Romain Péchoux. Complete and tractable machine-independent characterizations of second-order polytime. Logical Methods in Computer Science, 2025, Volume 21, Issue 1, 10.46298/lmcs-21(1:5)2025 . hal-05097335

HAL Id: hal-05097335

https://inria.hal.science/hal-05097335v1

Submitted on 4 Jun 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_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
COMPLETE AND TRACTABLE MACHINE-INDEPENDENT
CHARACTERIZATIONS OF SECOND-ORDER POLYTIME

EMMANUEL HAINRY ⚫<sup>a</sup>, BRUCE M. KAPRON ⚫<sup>b</sup>, JEAN-YVES MARION ⚫<sup>a</sup>,
AND ROMAIN PÉCHOUX ⚫<sup>a</sup>

ABSTRACT. The class of Basic Feasible Functionals BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of BFF based on a typed programming language of terms. These terms may perform calls to non-recursive imperative procedures. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction and is obtained through the use of closures. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of BFF, thus solving a problem open for more than 20 years.

# 1. INTRODUCTION

1.1. Motivations. The class of second-order functions computable in polynomial time was introduced and studied by Mehlhorn [Meh76], building on an earlier proposal by Constable [Con73]. Kapron and Cook characterized this class using oracle Turing machines, giving it the name Basic Feasible Functionals (BFF):

**Definition 1.1** ([KC91]). Let the size of an oracle $f$ be the first-order function defined by $|f|(n) = \max_{|y|\le n} |f(y)|$. A functional $F$ is in **BFF**, if there are an oracle Turing machine $M$ and a second-order polynomial $P$ such that $M$ computes $F$ in time bounded by $P(|f|, |x|)$, for any oracle $f$ and any input $x$.

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

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

<footnote><sup>a</sup> Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
*e-mail address:* emmanuel.hainry@loria.fr, jean-yves.marion@loria.fr, romain.pechoux@loria.fr</footnote>

<footnote><sup>b</sup> University of Victoria, Victoria, BC, Canada
*e-mail address:* bmkapron@uvic.ca</footnote>

<footnote>*Key words and phrases:* Basic feasible functionals, Type 2, Second-order, Polynomial time, Tiering, Safe recursion.</footnote>
The above characterization, that we take as a definition of BFF, shows that functions in BFF correspond to functionals computed by oracle Turing machines running in polynomial time. The polynomial time bound has a second-order nature since it takes a first-order function, the size of the oracle, as input. Since then, BFF was by consensus considered as the natural extension to second-order of the well-known class of (first-order) polynomial time computable functions, FP. Notions of second-order polynomial time, while of intrinsic interest, have also been applied in a range of areas, including structural complexity theory [Meh76], resource-bounded topology [Tow90], complexity of total search problems [BCE+98], feasible real analysis [KC12], and verification [GAC12].

Starting with Cobham's seminal work [Cob65], there have been several attempts to provide machine-independent characterizations of complexity classes such as (P and) FP, that is, characterizations based on programming languages rather than on machines. Beyond the purely theoretical aspects, the practical interest of such characterizations is to be able to automatically guarantee that a program can be executed efficiently and in a secure environment. For these characterizations to hold, some restrictions are placed on a given programming language. They ensure that a program can be simulated by a Turing machine in polynomial time and, therefore, corresponds to a function in FP. This property is called soundness. Conversely, we would like any function in FP to be computable by a program satisfying the restrictions. This property is called extensional completeness. For automation to be possible, it is necessary that the characterizations studied be tractable; that is, decidable in polynomial time. Moreover, they should preferably not require a prior knowledge of the program complexity. One speaks then of implicit characterization insofar as the programmer does not have to know an explicit bound on the complexity of the analyzed programs.

In the first-order setting, different restrictions and techniques have been developed to characterize the complexity class FP. One can think, among others, of the safe recursion and ramified recursion techniques for function algebras [BC92, LM93], of interpretation methods for term rewrite systems [BMM11], or of light and soft linear logics typing-discipline for lambda-calculi [Gir98, BT04, BM10].

In the second-order setting, a machine-independent characterization of BFF was provided in [HKMP22b]. This characterization uses the tier-based (i.e., safe/ramified recursion-based) type discipline introduced in [Mar11] on imperative programs for characterizing FP and can be restated as follows:

$$BFF = \lambda(\llbracket ST \rrbracket)_2.$$

The notation $\llbracket ST \rrbracket$ denotes the set of functions computed by typable and terminating programs; $\lambda$ denotes the lambda closure: for a given set of functionals $S$, $\lambda(S)$ is the set of functionals denoted by simply-typed lambda-terms using constants in $S$; $S_2$ is the restriction of $S$ to second-order functionals. Type inference for $\llbracket ST \rrbracket$ is fully automatic and can be performed in time cubic in the size of the analyzed program. However the above characterization has two main weaknesses:

* It is not complete: As $\llbracket ST \rrbracket \subseteq BFF$, the typed language alone is not complete for BFF and a lambda closure (i.e., $\lambda(S)$) of functionals computed by typable and terminating programs is required to ensure completeness.

* It is not tractable: the set $\llbracket ST \rrbracket$ relies on a termination assumption and it is unclear whether the characterization still holds for a decidable or, for that matter, tractable termination technique.
Thus, providing a tractable, implicit, sound, and complete programming language for characterizing second-order polynomial time is still an open problem.

## 1.2. Contributions.
Our paper provides the first solution to this problem, open for more than 20 years ([IRK01, Chapter 9]). To this end, we introduce a higher-order programming language and design a suitable typing discipline that address the two weaknesses described above. The lambda closure requirement for completeness is removed by designing a suitable programming language that consists of a layer of simply-typed terms that can perform calls to a layer of imperative and non-recursive procedures following a tier-based type discipline. This language allows for some restricted forms of procedure composition that are handled by the simply-typed terms and also allows for some restricted forms of oracle composition that are managed through the use of *closures*, syntactic elements playing the role of first-order abstractions with free variables. The termination criterion is specified as a completeness-preserving instance, called $SCP_S$, of a variant of Size Change Termination [LJB01] introduced in [BL07] that can be checked in time quadratic in the size of the analyzed program. The main contributions of this paper are:

* A programming language in which typable (SAFE) and terminating (SN) programs capture exactly BFF (Theorem 4.5).

* A restriction to lambda-free programs, called rank-0 programs, such that typable ($SAFE_0$) and terminating (SN) programs still capture exactly BFF (Theorem 4.12); hence showing that lambda-abstraction only provides a syntactic relaxation, and corresponds to a conservative extension in terms of computable functions.

* A proof that type inference for SAFE is P-complete, and a type inference procedure running in time cubic in the program size for $SAFE_0$ (Theorem 4.15).

* A simple termination criterion, called $SCP_S$, preserving soundness and completeness of the characterizations both for SAFE and for $SAFE_0$ (Theorem 5.9) that can be checked in quadratic time.

* A complete characterization of BFF in terms of typable (SAFE) and terminating ($SCP_S$) programs (Theorem 5.11) that captures strictly more programs (Figure 1) than [HKMP22b], and is decidable in P-time.

The programming language under study comes with some usual restrictions on its expressive power, *i.e.*, the typable programs it captures. Indeed, the studied characterizations of BFF are tractable/decidable whereas knowing whether a program computes a function in BFF is at least $\Sigma_0^2$-hard [Háj79], hence not decidable. As a consequence, *false negatives* (*i.e.*, programs that are rejected by the characterizations but compute a function in BFF) are unavoidable.

## 1.3. Related work.
Several tools providing machine-independent characterizations of distinct complexity classes have been developed in the field of Implicit Computational Complexity (ICC). Most of these tools are restricted to the study of first-order complexity classes. Whereas light logic approaches can deal with programs at higher types, their applications are restricted to first-order complexity classes such as FP [Gir98, BT04, BM10]. Interpretation methods were extended to higher-order polynomials in [BDL16] to study FP and adapted in [FHHP15] and [HP20] to characterize BFF. However, these characterizations are not decidable as they require checking of second-order polynomial inequalities. [CK89] and [IRK01] study characterizations of BFF in terms of a simple imperative programming
language that enforces an explicit external bound on the size of oracle outputs within loops. The corresponding restriction is not implicit by nature and is impractical from a programming perspective as the size of oracle outputs cannot be predicted. In this paper, the bound is programmer friendly because it is implicit and it only constrains the size of the oracle input.

The contributions of the paper are extensions of existing works:

* The soundness of the characterization relies strongly on the notion of *continuation*, that fixes a given oracle (closure) for once in the imperative layer. If the oracle were allowed to be updated inside a while loop, depending on some local value, then the language would yield a class beyond BFF, by computing exponential functions. Consequently, it would not be correct to think of SAFE₀ as a simple extension of the language IMP of [Win93] to higher-order because oracles need to be fixed once and for all in a call to a given imperative procedure.

* The characterization of BFF still holds in the absence of lambda-abstraction as a basic construct of the proposed programming language, in particular that completeness does not rely on lambda-abstractions apart from closures. For that purpose, we consider an alternative characterization of BFF that was introduced in [KS19] using the second-order restriction $PV_2^\omega$ of the class $PV^\omega$ from [CU93]. Note that this characterization is not implicit as it contains explicit bounds. This is an important improvement over [HKMP22b] and [KS18], both of which required external lambda-closure.

* The type system is designed so that each procedure is typed exactly once. Types are not unique, but this does not prevent type inference from being polytime, as exhibiting one type is sufficient. The tractability of type inference is obtained by combining the tractability of type inference in the tier-based layer and in the simply-typed layer [Mai04].

* The particular choice of the termination criterion SCP<sub>S</sub> was made to show that termination can be specified as a tractable/feasible criterion while preserving completeness. This is also a new result. SCP<sub>S</sub> may include nested loops (as described in [BL07]) and can be replaced by any termination criterion capturing the programs used in the proof of completeness (Examples 4.8, 4.9, and 4.11). SCP<sub>S</sub> was chosen for its tractability, but not only: the SCP criterion of [BL07] ensures termination by using an error state which breaks the control flow. But this control-flow escape would damage the non-interference property needed for tier-based typing to guarantee time complexity bounds.

This paper is an extended and revised version of the paper [HKMP22a] presented at Foundations of Software Science and Computation Structures - 25th International Conference (FoSSaCS 2022), including complete proofs.

## 1.4. Leading example.
The program *ce*, as in counterexample, of Figure 1 will be our leading example, as it computes a function known to be in BFF – [[ST]]. This function was used by Kapron and Steinberg in [KS18] as a counterexample for showing that [[ST]] is not equal to BFF. This program will be shown to be in SAFE₀ and, consequently, in SAFE and to terminate with SCP<sub>S</sub>.

Program *ce* computes a functional over the set of words $\mathcal{W}$. When the boxed variables *x* and *y* in *box [X, y] in* are fed with the inputs $f \in \mathcal{W} \to \mathcal{W}$ and $w \in \mathcal{W}$, respectively, the term *t* calls the procedure *KS*, named after Kapron-Steinberg. In *KS*, variables $\mathbf{x}_1$ and $\mathbf{x}_2$ are substituted with closures $\{\mathbf{x} \to f \ @ \ \mathbf{x}\} \text{ i.e.},$ function *f*, and $\{\mathbf{x} \to f \ @ (f \ @ \mathbf{x})\} \text{ i.e.},$ function $f \circ f$, respectively. Variable *v* is substituted with value *w*. The binary operator
<figure><img src="image_4.png" /><figcaption>FIGURE 1. Program ce</figcaption></figure>

† truncates and pads the size of its first operand to the size of its second operand plus 1. Procedure KS computes |w| bounded iterations of f ◦ f through the execution of the assignment z := X₂(z ⊤ u). The bound on the output size of each iteration is computed by the first assignment u := X₁(ϵ ⊤ ϵ) of KS and is equal to f(1), that is, f([[ϵ ⊤ ϵ]]), with [[ϵ ⊤ ϵ]] = 1; [[e]] being the result of evaluating the expression e. In any iteration of f ◦ f, the internal call to f is not bounded. Hence, there might be up to |w| increases for the input of the outer call. Such a behavior is forbidden in [[ST]].

## 2. A SECOND-ORDER LANGUAGE WITH IMPERATIVE PROCEDURES

The syntax and semantics of the programming language designed to capture the complexity class BFF are introduced in this section. Programs of this language consist in second-order terms in which imperative procedures are declared and called. These procedures have no global variables, are not recursive, and their parameters can be of order 1 (oracles) or 0. Local variables inside a procedure can only be of order 0. Oracles are in read-only mode: they cannot be declared and, hence, modified inside a procedure. Oracles can only be composed at the term level through the use of closures, first-order abstractions that can be passed as parameters in a procedure call.

### 2.1. Syntax.
Let $\bar{e}$ denote a possibly empty tuple of $n$ elements $e_1, \dots, e_n$, where $n$ is given by the context. Let $|\bar{e}|$ denote the length of tuple $\bar{e}$, i.e., $|\bar{e}| \triangleq n$. Let $\pi_i$, $0 < i \le |\bar{e}|$, denote the projectors on tuples, i.e., $\pi_i(\bar{e}) \triangleq e_i$. Let $[e]$ denote some optional element $e$.

Let $\mathcal{V}$ be a set of variables that can be split into three disjoint sets $\mathcal{V} = \mathcal{V}_0 \uplus \mathcal{V}_1 \uplus \mathcal{V}_{\ge 2}$. The type-0 variables in $\mathcal{V}_0$ will be denoted by lower case letters $x, y, \dots$ and the type-1 variables in $\mathcal{V}_1$ will be denoted by upper case letters $X, Y, \dots$. Variables in $\mathcal{V}$ of arbitrary type will be denoted by letters $a, b, a_1, a_2, \dots$.
<figure><img src="image_5.png" /><figcaption>FIGURE 2. Syntax of type-2 programs</figcaption></figure>

Let $\mathcal{O}$ be a set of operators $op$ of fixed arity $ar(op)$ that will be used both in infix and prefix notations for notational convenience and that are always fully applied, i.e., applied to a number $ar(op)$ of operands.

The programs are defined by the grammar of Figure 2 with keywords spelled out in bold typewriter font. A program is either a term $t$, a procedure declaration `declare p in prg`, or the declaration of a boxed variable $a$, called `box`, followed by a program: `box [a] in prg`. Boxed variables will represent the program inputs.

When we refer to a *type-i* syntactic element $e$ (a variable, an expression, a term, ...), for $i \in \mathbb{N}$, we implicitly assume that the element $e$ denotes some function of order $i$ over words as basic type. For example, for a term $t$, being type-0 means that $t$ is simply-typed and its type does not contain an arrow. This notion will be formally defined in Section 3.

In Figure 2, there are three constructor/destructor pairs for abstraction and application; each of them playing a distinct rôle:

* $\lambda a.t$ and $t@t$ are the standard abstraction and application on terms.

* The application of a type-1 variable $X$ within a statement is called an *oracle call*, written $X(e_1 \upharpoonright e_2)$, where $e_1$ is called the *input data*, $e_2$ is called the *input bound*, and $e_1 \upharpoonright e_2$ is called the *input*. The corresponding abstraction is called a *closure*, a map of the shape $\{x \to t\}$, where the term $t$ may contain free variables. Closures will be restricted to be of type-1 by requiring $t$ to be of type-0.

* A procedure declaration $P(\bar{X}, \bar{x})\{[\text{var } \bar{y};] \text{ st return } x\}$ is an abstraction that computes type-2 functions taking type-1 and type-0 inputs $(\bar{X}$ and $\bar{x}$, respectively) as parameters and returning a type-0 output $x$. The *procedure calls* of the shape `call P(\bar{c}, \bar{t})` are the corresponding applications and take closures as type-1 inputs and type-0 terms as type-0 inputs.

For some syntactic element $e$ of the language, let $V(e) \subseteq V$ be the set of all variables occurring in $e$. A variable is free if it is not under the scope of an abstraction and it is not boxed. A program is *closed* if it has no free variable.

For a given procedure declaration $p = P(\bar{X}, \bar{x})\{[\text{var } \bar{y};] \text{ st return } x\}$, define the *procedure name* of $p$ as $n(p) \triangleq p \in \mathbb{P}$, with $\mathbb{P}$ being a set of procedure names. Define also `body(p) \triangleq st`, `local(p) \triangleq \{\bar{y}\}`, and `param(p) \triangleq \{\bar{X}, \bar{x}\}`. `body(p)` is called the *body* of procedure $p$. The
variables in local($\mathfrak{p}$) are called *local variables* and the variables in param($\mathfrak{p}$) are called *parameters*.

We will assume that for all programs the following well-formedness conditions hold: there are no name clashes, that is two procedures should not share the same name and, in a procedure, a local variable cannot have the same name as a parameter; there are no free variables in a given procedure, in other words, the only variables in procedures are parameters and local variables; any procedure call has a corresponding procedure declaration.

Throughout the paper, we will consider closed programs in normal form. These consist of programs with no free variable that can be written as follows

box [$\bar{X}, \bar{x}$] in declare $\bar{p}$ in t,

for some term $t$. In other words, all type-1 variables then all type-0 variables are boxed before procedures are declared.

**2.2. Operational semantics.** Let $\mathcal{W} = \Sigma^*$ be the set of words over a finite alphabet $\Sigma$ such that $\{0,1\} \subseteq \Sigma$. The symbol $\varepsilon$ denotes the empty word. The length of a word $w$ is denoted $|w|$. Given two words $w$ and $v$ in $\mathcal{W}$, let $v.w$ denote the concatenation of $v$ and $w$. For a given symbol $a \in \Sigma$, let $a^n$ be defined inductively by $a^0 = \varepsilon$ and $a^{n+1} = a.a^n$. Let $\trianglelefteq$ be the sub-word relation over $\mathcal{W}$, which is defined by $v \trianglelefteq w$, if $\exists u, u' \in \mathcal{W}, w = u.v.u'$.

For a given word $w \in \mathcal{W}$ and an integer $n$, let $w_{\upharpoonright n}$ be the word obtained by truncating $w$ to its first $\min(n, |w|)$ symbols and then padding with a word of the form $10^k$ to obtain a word of size exactly $n+1$. For example, $1001_{\upharpoonright 0} = 1$, $1001_{\upharpoonright 1} = 11$, $1001_{\upharpoonright 2} = 101$, and $1001_{\upharpoonright 6} = 1001100$. Define $\forall v, w \in \mathcal{W}, [[v]](v, w) = v_{\upharpoonright |w|}$. Padding ensures that $|[v]](v, w)| = |w| + 1$. The syntax of programs enforces that oracle calls are always performed on input data padded by the input bound and, consequently, oracle calls are always performed on input data whose size does not exceed the size of the input bound plus one.

We denote the set of total functions from set $A$ to set $B$ as $A \to B$ and the set of partial functions as $A \hookrightarrow B$. For each operator op of arity $n$, a total function $[[\text{op}]] \in \mathcal{W}^n \to \mathcal{W}$ is defined. Constants may be viewed as operators of arity zero. We define two classes of operators called neutral and positive depending on the total function they compute. This categorization of operators will be used by our type system as the admissible types for operators will depend on their category.

**Definition 2.1 (Neutral and positive operators).** For an $n$-ary operator op that computes the total function $[[\text{op}]] \in \mathcal{W}^n \to \mathcal{W}$,

* op is *neutral* if $[[\text{op}]]$ is constant (i.e., $\text{ar}(\text{op}) = 0$), $[[\text{op}]] \in \mathcal{W}^n \to \{0, 1\}$ is a predicate, or $\forall \bar{w} \in \mathcal{W}^n, \exists i \le n, [[\text{op}]](\bar{w}) \le w_i$;

* op is *positive* if $\exists c_{\text{op}} \in \mathbb{N}$ s.t.: $\forall \bar{w} \in \mathcal{W}^n, |[[\text{op}]](\bar{w})| \le \max_{1 \le i \le n} |w_i| + c_{\text{op}}$.

As neutral operators are always positive, in the sequel, we reserve the name positive for those operators that are positive but not neutral.

In what follows, let $f, g, \dots$ denote total functions from words to words. A store $\mu$ consists of the disjoint union of a finite partial map $\mu_0$ from $\mathbb{V}_0$ to $\mathcal{W}$ and a finite partial map $\mu_1$ from $\mathbb{V}_1$ to total functions in $\mathcal{W} \to \mathcal{W}$. Let $\text{dom}(\mu)$ be the domain of the store $\mu$. Let $\mu[\mathbf{x} \leftarrow w]$ denote the store $\mu'$ satisfying $\mu'(b) = \mu(b)$, for all $b \ne \mathbf{x}$, and $\mu'(\mathbf{x}) = w$. This notation is extended naturally to type-1 variables $\mu[\mathbf{x} \leftarrow f]$ and to sequences of distinct variables $\mu[\bar{\mathbf{x}} \leftarrow \bar{w}, \bar{\mathbf{x}} \leftarrow \bar{f}]$. Finally, let $\mu_\emptyset$ denote the empty store.
Let $\downarrow$ denote the standard big-step call-by-name reduction relation on terms defined by: if $t_1 \downarrow \lambda a.t$ and $t\{t_2/a\} \downarrow v$ then $t_1@t_2 \downarrow v$, where $\{t_2/a\}$ is the standard substitution and where $v$ can be a type-0 variable $x$, a lambda-abstraction $\lambda a.t$, a type-1 variable application $x@t$, or a procedure call call $P(\bar{c}, \bar{t})$.

A continuation is a map $\phi$ from $V_1$ to the set of Closures, i.e., $\phi(X) = \{x \to t\}$ for some type-1 variable $X$, some type-0 variable $x$, and some type-0 term $t$. Let $\bar{X} \mapsto \bar{c}$ with $|\bar{X}| = |\bar{c}|$, be a notation for the continuation mapping each $X_i \in V_1$ to the closure $c_i$.

Given a set of procedures $\sigma$, a store $\mu$, and a continuation $\phi$, we define three distinct kinds of judgments: $(\sigma, \mu, \phi, e) \to_{\exp} w$ for expressions, $(\sigma, \mu, \phi, st) \to_{\st} \mu'$ for statements, and $(\sigma, \mu, prg) \to_{\env} w$ for programs.

* The judgment $(\sigma, \mu, \phi, e) \to_{\exp} w$ means that the expression $e$ evaluates to the word $w \in W$ with respect to the set of procedure declarations $\sigma$, the store $\mu$ and the continuation $\phi$.

* The judgment $(\sigma, \mu, \phi, st) \to_{\st} \mu'$ expresses that, under the set of procedure declarations $\sigma$, the store $\mu$ and the continuation $\phi$, the statement $st$ terminates with resulting store $\mu'$.

* The judgment $(\sigma, \mu, prg) \to_{\env} w$ means that the tuple $(\sigma, \mu, prg)$ consisting of a set $\sigma$ of procedure declarations, a store $\mu$, and a program $prg$ maps deterministically to a word $w \in W$.

Given three sequences of words $\overline{w} = w_1, \dots, w_n$, expressions $\overline{e} = e_1, \dots, e_n$, and terms $\overline{t} = t_1, \dots, t_n$ of the same length $n$, we write $(\sigma, \mu, \phi, \overline{e}) \to_{\exp} \overline{w}$, if $\forall i \le n$, $(\sigma, \mu, \phi, e_i) \to_{\exp} w_i$ and we write $(\sigma, \mu, \overline{t}) \to_{\env} \overline{w}$, if $\forall i \le n$, $(\sigma, \mu, t_i) \to_{\env} w_i$.

The big-step operational semantics of the language is described in Figure 3. One important point to stress is that closures cannot be nested and are set once and for all in a procedure call: they cannot be modified inside a procedure body. It should also be noted that procedures do not have side effects as the modifications to the store are only overlaid and not carried over in the rest of the program. In a closed program that respects well-formedness conditions, commuting box [.] in and declare . in preserves semantics. Hence for any closed program, there exists a semantically equivalent program in normal form.

A closed program in normal form $\mathbf{prg} = \mathbf{box}[\overline{\mathbf{x}}, \overline{\mathbf{x}}]$ in declare $\overline{\mathbf{p}}$ in $\mathbf{t}$ computes the second-order partial functional $\llbracket \mathbf{prg} \rrbracket \in (W \to W)^k \to W^l \hookrightarrow W$, defined by:

$$ \llbracket \mathbf{prg} \rrbracket (f_1, \dots, f_k, w_1, \dots, w_l) = w \text{ iff } (\emptyset, \mu_0[\mathbf{x}_1 \leftarrow w_1, \dots, \mathbf{x}_l \leftarrow f_1, \dots, \mathbf{x}_l \leftarrow f_l], \mathbf{prg}) \to_{\text{env}} w. $$

In the special case where $\llbracket \mathbf{prg} \rrbracket$ is a total function, the program $\mathbf{prg}$ is said to be terminating (strongly normalizing). We will denote by $\mathbf{SN}$ the set of terminating programs. For a given set of programs $S$, let $\llbracket S \rrbracket$ denote the set of functions computed by programs in $S$. Formally, $\llbracket S \rrbracket = \{\llbracket \mathbf{prg} \rrbracket | \mathbf{prg} \in S\}$. For example, $\llbracket \mathbf{SN} \rrbracket$ is the set of total second-order functions computed by terminating programs.

**Example 2.2.** Consider the program $\mathbf{ce}$ provided in Figure 1, where:

$$ \llbracket \epsilon \rrbracket () = \epsilon \in W, \quad \llbracket != \rrbracket (w, v) = \begin{cases} 1 & \text{if } v \neq w \\ 0 & \text{otherwise} \end{cases}, \quad \llbracket \text{pred} \rrbracket (v) = \begin{cases} \epsilon & \text{if } v = \epsilon \\ u & \text{if } v = a.u, a \in \Sigma \end{cases}. $$

Program $\mathbf{ce}$ is in normal form and computes the second-order functional $F \in (W \to W) \to W \to W$ defined by: $\forall f \in W \to W, \forall w \in W, F(f)(w) = F_{|w|}(f)$, where $F_n$ is defined recursively as

$$ F_0(f) = \epsilon \\ F_{n+1}(f) = (f \circ f)(\llbracket \uparrow \rrbracket(F_n(f), f(1))) = (f \circ f)(F_n(f)_{|f(f(1))|}). $$
$$ \frac{\overline{(\sigma, \mu, \phi, \bar{x}) \to_{\exp} \mu(x)} \quad (\text{Var}) \quad \frac{(\sigma, \mu, \phi, \bar{e}) \to_{\exp} \bar{w}}{(\sigma, \mu, \phi, \text{op}(\bar{e})) \to_{\exp} [\text{op}](\bar{w})} \quad (\text{Op})}{(\sigma, \mu, \phi, \mathbf{e}_1) \to_{\exp} v \quad (\sigma, \mu, \phi, \mathbf{e}_2) \to_{\exp} u \quad \phi(\mathbf{x}) = \{\mathbf{x} \to \mathbf{t}\} \quad (\sigma, \mu[x \leftarrow \llbracket v, u \rrbracket, \mathbf{t}] \to_{\text{env}} w} \quad (\text{Or})} \quad (\sigma, \mu, \phi, \mathbf{x}(\mathbf{e}_1 \upharpoonright \mathbf{e}_2)) \to_{\exp} w $$

(A) Expressions

$$ \frac{\overline{(\sigma, \mu, \phi, \text{skip}) \to_{\text{st}} \mu} \quad (\text{Skip}) \quad \frac{(\sigma, \mu, \phi, \text{st}_1) \to_{\text{st}} \mu' \quad (\sigma, \mu', \phi, \text{st}_2) \to_{\text{st}} \mu''}{(\sigma, \mu, \phi, \text{st}_1; \text{st}_2) \to_{\text{st}} \mu''} \quad (\text{Seq}) $$

$$ \frac{\overline{(\sigma, \mu, \phi, \mathbf{e}) \to_{\exp} w}}{(\sigma, \mu, \phi, \mathbf{x} := \mathbf{e}) \to_{\text{st}} \mu[\mathbf{x} \leftarrow w]} \quad (\text{Asg}) $$

$$ \frac{\overline{(\sigma, \mu, \phi, \mathbf{e}) \to_{\exp} w \quad (\sigma, \mu, \phi, \text{st}_w) \to_{\text{st}} \mu' \quad w \in \{0, 1\}}}{(\sigma, \mu, \phi, \text{if}(\mathbf{e})\{\text{st}_1\} \text{else } \text{st}_0\}) \to_{\text{st}} \mu'} \quad (\text{Cond}) $$

$$ \frac{\overline{(\sigma, \mu, \phi, \mathbf{e}) \to_{\exp} 0}}{(\sigma, \mu, \phi, \text{while}(\mathbf{e})\{\text{st}\}) \to_{\text{st}} \mu} \quad (\text{Wh0}) $$

$$ \frac{\overline{(\sigma, \mu, \phi, \mathbf{e}) \to_{\exp} 1 \quad (\sigma, \mu, \phi, \text{st; while}(\mathbf{e})\{\text{st}\}) \to_{\text{st}} \mu' \quad (\sigma, \mu, \phi, \text{while}(\mathbf{e})\{\text{st}\}) \to_{\text{st}} \mu'}}{(\sigma, \mu, \phi, \text{while}(\mathbf{e})\{\text{st}\}) \to_{\text{st}} \mu'} \quad (\text{Wh1}) $$

(B) Statements

$$ \frac{\overline{t \downarrow x \quad x \in \text{dom}(\mu)} \quad (\text{TVar}) \quad \frac{\overline{t \downarrow X @ t_1} \quad (\sigma, \mu, t_1) \to_{\text{env}} w \quad X \in \text{dom}(\mu)}{(\sigma, \mu, t) \to_{\text{env}} \mu(X)(w)} \quad (\text{OA})} $$

$$ \frac{\overline{t \downarrow \text{call } P(\bar{c}, \bar{t}_1) \quad (\sigma, \mu, \bar{t}_1) \to_{\text{env}} \bar{w} \quad (\sigma, \mu[\bar{x} \leftarrow \bar{w}, \bar{y} \leftarrow \bar{\varepsilon}], \bar{X} \mapsto \bar{c}, \text{st}) \to_{\text{st}} \mu'}}{(\sigma \cup \{P(\bar{X}, \bar{x})\}\{\text{var } \bar{y}; \text{ st return } \bar{z}\}), \mu, \mathbf{t}) \to_{\text{env}} \mu'(\bar{z})} \quad (\text{Call}) $$

(C) Type-0 terms

$$ \frac{\overline{(\sigma \cup \{\mathbf{p}\}, \mu, \mathbf{prg}) \to_{\text{env}} w}}{(\sigma, \mu, \text{declare } \mathbf{p} \text{ in } \mathbf{prg}) \to_{\text{env}} w} \quad (\text{Dec}) \quad \frac{(\sigma, \mu, \mathbf{prg}) \to_{\text{env}} w \quad \mathbf{a} \in \text{dom}(\mu)}{(\sigma, \mu, \text{box } [\mathbf{a}] \text{ in } \mathbf{prg}) \to_{\text{env}} w} \quad (\text{Box}) $$

(D) Programs

<caption>FIGURE 3. Big step operational semantics</caption>
That is a function that composes the input function $2|w|$ times $f$ while restricting its input to a fixed size $|f(1)|$ every other iteration. Indeed, $\llbracket \epsilon \rrbracket() = \epsilon$ and $\llbracket \uparrow \rrbracket(\epsilon, \epsilon) = \epsilon_{|\epsilon|} = 1$. Consequently, the oracle bound $\mathbf{u}$ in the oracle call $\mathbf{X}_2(\mathbf{z} \mid \mathbf{u})$ is bound to value $f(1)$ in the store by the statement $\mathbf{u} := \mathbf{X}_1(\epsilon \mid \epsilon)$.

Observe that the operators $\epsilon$, $!==$ and `pred` are all neutral. An example of positive operator can be given by the successor operators defined by $\llbracket \mathbf{succ}_i \rrbracket(v) = i.v$, for $i \in \{0, 1\}$. These operators are positive since $|\llbracket \mathbf{succ}_i \rrbracket(v)| = |i.v| = |v| + 1$.

The operational semantics of `ce` is illustrated by the judgment provided in Figure 4, that represents a portion of the evaluation of the whole program on inputs $f$ and $w$.

### 3. TYPE SYSTEM

In this section, we introduce the typing discipline for our programming language.

#### 3.1. Tiers and typing environments.
Let $\mathcal{W}$ be the type of words in $\mathcal{W}$. Simple types over $\mathcal{W}$ are defined inductively by $T, T', \dots ::= \mathcal{W} \mid T \to T$. Let $\mathcal{T}_\mathcal{W}$ be the set of simple types over $\mathcal{W}$. The order of a simple type in $\mathcal{T}_\mathcal{W}$ is defined inductively by: $\text{ord}(T) = 0$, if $T = \mathcal{W}$, and $\text{ord}(T) = \max(1 + \text{ord}(T_1), \text{ord}(T_2))$, if $T = T_1 \to T_2$.

Tiers are elements of the totally ordered set $(\mathbf{N}, \leq)$, where $\mathbf{N} = \{0, 1, 2, \dots\}$ is the set of natural numbers with order $\leq$. The strict order on $\mathbf{N}$ will be denoted by $<$ and the binary min and max denote the usual operations. We use bold symbols $\mathbf{k}, \mathbf{k}', \dots, \mathbf{k}_1, \mathbf{k}_2, \dots$ to denote tier variables. For $n$ tiers $\{\mathbf{k}_1, \dots, \mathbf{k}_n\}$, we also define the $n$-ary max and min: $\max_{i=1}^n \mathbf{k}_i$ and $\min_{i=1}^n \mathbf{k}_i$. A first-order tier is of the shape $\mathbf{k}_1 \to \dots \to \mathbf{k}_n \to \mathbf{k}'$, with $\mathbf{k}_i, \mathbf{k}' \in \mathbf{N}$.

A simple typing environment $\Gamma_\mathcal{W}$ is a finite partial map from $\mathcal{V}$ to $\mathcal{T}_\mathcal{W}$, which assigns simple types to variables.

A variable typing environment $\Gamma$ is a finite partial map from $\mathcal{V}_0$ to $\mathbf{N}$, which assigns single tiers to type-0 variables.

An operator typing environment $\Delta$ is a mapping that associates to some operator `op` and some tier $\mathbf{k} \in \mathbf{N}$ a set of first-order tiers $\Delta(\mathbf{op})(\mathbf{k})$ of the shape $\mathbf{k}_1 \to \dots \to \mathbf{k}_n \to \mathbf{k}'$ where $n$ is the arity of `op`.

A procedure typing environment $\Omega$ is a mapping that associates to each procedure `p` a pair $\langle\Gamma, \bar{\mathbf{k}}\rangle$ consisting of a variable typing environment $\Gamma$ and a triplet of tiers $\bar{\mathbf{k}}$. Let $\Omega_i \triangleq \pi_i(\Omega)$, $i \in \{1, 2\}$.

Let $\text{dom}(\Gamma)$, $\text{dom}(\Gamma_\mathcal{W})$, $\text{dom}(\Delta)$, and $\text{dom}(\Omega)$ denote the sets of variables typed by $\Gamma$ and $\Gamma_\mathcal{W}$, the set of operators typed by $\Delta$, and the set of procedures typed by $\Omega$, respectively.

For a procedure typing environment $\Omega$, it will be assumed that for every $\mathbf{p} \in \text{dom}(\Omega)$, $\text{param}(\mathbf{p}) \cup \text{local}(\mathbf{p}) \subseteq \text{dom}(\Omega_1(\mathbf{p}))$.

While operator and procedure typing environments are global, i.e., defined for the whole program, variable typing environments are local, i.e., relative to the procedure under analysis. In a program typing judgment, the simple typing environment can be viewed as the typing environment for the main program.
Let $\mathbf{p}_{\text{KS}} = \text{KS}(X_1, X_2, v)\{\text{var } u, z; \text{st}; \text{st}' \text{ return } z\}$, with $\text{st} = u := X_1(\epsilon \upharpoonright \epsilon)$,
$\mu_1 = \mu_0[X \leftarrow f, y \leftarrow w, u \leftarrow \epsilon, z \leftarrow \epsilon]$,
$\mu_2(z) = F|_w(f)$,

and $\phi(X_1) = \{x \to X@x\}$, $\phi(X_2) = \{x \to X@(X@x)\}$ in:

<figure><img src="image_6.png" /><figcaption>FIGURE 4. Evaluation of the program ce of Figure 1</figcaption></figure>
### 3.2. Typing judgments and type system.
The typing discipline includes two distinct kinds of typing judgments:

* Procedure typing judgments $Γ, Δ \vdash e : (k, k_{in}, k_{out})$, with $k, k_{in}, k_{out} \in \mathbf{N}$, and $e$ an expression or a statement;

* Term typing judgments $Γ_w, Ω, Δ \vdash prg : T$, with $T \in \mathcal{T}_w$.

The meaning of the procedure typing judgment is that the *expression tier* (or *statement tier*) is $k$, the *innermost tier* is $k_{in}$, and the *outermost tier* is $k_{out}$. The innermost (resp. outermost) tier is the tier of the innermost (resp. outermost) while loop guard where the expression or statement is located. The meaning of term typing judgments is that the program $prg$ is of simple type $T$ under the operator typing environment $Δ$, the procedure typing environment $Ω$ and the simple typing environment $Γ_w$.

A program $prg$ (or term $t$) is of *type-$i$*, if $Γ_w, Ω, Δ \vdash prg : T$ ($Γ_w, Ω, Δ \vdash t : T$) can be derived for some typing environments and type $T$ s.t. $ord(T) = i$.

The type system for the considered programming language is provided in Figure 5. The typing rules for expressions and statements in Figure 5A are the same as in [HKMP22b]; The typing of procedures, terms, closures and programs in Figure 5B is new. A *well-typed program* is a program that can be given the type $(\overline{W} \to \overline{W}) \to \overline{W} \to W$, i.e., the judgment $Γ_w, Ω, Δ \vdash prg : (\overline{W} \to \overline{W}) \to \overline{W} \to W$ can be derived for the environments $Γ_w, Ω, Δ$. Consequently, a well-typed program is a *type-$i$* program, for some $i \le 2$, computing a functional.

Due to the rule (E-OP) of Figure 5A, which allows several admissible types for operators, typing derivations are, in general, not unique. However, under the assumption of existence, program types are unique for fixed typing environments. The two typing rules for while loops (S-WH) and (S-WINIT) are mutually exclusive because of the non-overlapping requirements for $k_{out}$ in Figure 5A. (S-WH) is the standard rule and updates the innermost tier with the tier of the while loop guard under consideration. (S-WINIT) is an initialization rule that allows the programmer to instantiate by default the main command with outermost tier **0** as it has no outermost while. It could be sacrificed for simplicity but at the price of a worse expressive power.

For a given typing judgment $j$, a *typing derivation* $\pi \supseteq j$ is a tree whose root is the (procedure or term) typing judgment $j$ and whose children are obtained by applications of the typing rules of Figure 5. The name $\pi$ will be used alone whenever mentioning the root of a typing derivation is not explicitly needed. A typing sub-derivation of a typing derivation $\pi$ is a subtree of $\pi$.

Notice that the type system of Figure 5 is a strict extension of the type system of [HKMP22b], which mostly consists of the typing rules in Figure 5A, for procedures.

### 3.3. Safe programs.
In this section, we restrict the set of admissible operators to prevent programs admitting exponential growth from being typable. A program satisfying such a restriction will be called *safe*. We first define a safe operator typing environment by restraining how neutral and positive operators can be used, in the same way as in [HKMP22b].

**Definition 3.1 (Safe operator typing environment).** An operator typing environment $Δ$ is *safe* if for each $op \in dom(Δ)$ with non null arity $n$, $op$ is neutral or positive, $[op]$ is a polynomial time computable function, and for each $k \in \mathbf{N}$, for each $k_1 \to \dots \to k_n \to k' \in Δ(op)(k)$, the two conditions below hold:

(1) $k' \le \min_{i=1}^n k_i \le \max_{i=1}^n k_i \le k$,

(2) if $op$ is a positive operator then $k' < k$.
$$
\frac{\Gamma(\mathbf{x}) = \mathbf{k}}{\Gamma, \Delta \vdash \mathbf{x} : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})} \quad (\text{E-VAR})
$$
$$
\frac{\mathbf{k}_1 \to \dots \to \mathbf{k}_n \to \mathbf{k} \in \Delta(\mathbf{op})(\mathbf{k}_{in}) \quad \forall i \le n, \Gamma, \Delta \vdash \mathbf{e}_i : (\mathbf{k}_i, \mathbf{k}_{in}, \mathbf{k}_{out})}{\Gamma, \Delta \vdash \mathbf{op}(\mathbf{e}_1, \dots, \mathbf{e}_n) : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})} \quad (\text{E-OP})
$$
$$
\frac{\Gamma, \Delta \vdash \mathbf{e}_1 : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out}) \quad \Gamma, \Delta \vdash \mathbf{e}_2 : (\mathbf{k}_{out}, \mathbf{k}_{in}, \mathbf{k}_{out}) \quad \mathbf{k} < \mathbf{k}_{in} \text{ and } \mathbf{k} \le \mathbf{k}_{out}}{(\text{E-OR})}
$$
$$
\frac{\Gamma, \Delta \vdash \mathbf{X}(\mathbf{e}_1 \upharpoonright \mathbf{e}_2) : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})}{\Gamma, \Delta \vdash \mathbf{X}(\mathbf{e}_1 \upharpoonright \mathbf{e}_2) : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})}
$$

$$
\frac{\Gamma, \Delta \vdash \text{st} : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})}{\Gamma, \Delta \vdash \text{skip} : (\mathbf{0}, \mathbf{k}_{in}, \mathbf{k}_{out})} \quad (\text{S-SK}) \qquad \frac{\Gamma, \Delta \vdash \text{st} : (\mathbf{k}+1, \mathbf{k}_{in}, \mathbf{k}_{out})}{\Gamma, \Delta \vdash \text{st} : (\mathbf{k}+1, \mathbf{k}_{in}, \mathbf{k}_{out})} \quad (\text{S-SUB})
$$

$$
\frac{\Gamma, \Delta \vdash \mathbf{st}_1 : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out}) \quad \Gamma, \Delta \vdash \mathbf{st}_2 : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})}{\Gamma, \Delta \vdash \mathbf{st}_1; \mathbf{st}_2 : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})} \quad (\text{S-SEQ})
$$

$$
\frac{\Gamma, \Delta \vdash \mathbf{x} : (\mathbf{k}_1, \mathbf{k}_{in}, \mathbf{k}_{out}) \quad \Gamma, \Delta \vdash \mathbf{e} : (\mathbf{k}_2, \mathbf{k}_{in}, \mathbf{k}_{out}) \quad \mathbf{k}_1 \le \mathbf{k}_2}{\Gamma, \Delta \vdash \mathbf{x} := \mathbf{e} : (\mathbf{k}_1, \mathbf{k}_{in}, \mathbf{k}_{out})} \quad (\text{S-ASG})
$$

$$
\frac{\Gamma, \Delta \vdash \mathbf{e} : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out}) \quad \Gamma, \Delta \vdash \mathbf{st}_1 : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out}) \quad \Gamma, \Delta \vdash \mathbf{st}_0 : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})}{\Gamma, \Delta \vdash \mathbf{if}(\mathbf{e})\{\mathbf{st}_1\} \quad \mathbf{else} \ \{\mathbf{st}_0\} : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})} \quad (\text{S-CND})
$$

$$
\frac{\Gamma, \Delta \vdash \mathbf{e} : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}) \quad \Gamma, \Delta \vdash \mathbf{st} : (\mathbf{k}, \mathbf{k}, \mathbf{k}) \quad \mathbf{1} \le \mathbf{k}}{\Gamma, \Delta \vdash \mathbf{while}(\mathbf{e})\{\mathbf{st}\} : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{0})} \quad (\text{S-WINIT})
$$

$$
\frac{\Gamma, \Delta \vdash \mathbf{e} : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out}) \quad \Gamma, \Delta \vdash \mathbf{st} : (\mathbf{k}, \mathbf{k}, \mathbf{k}_{out}) \quad \mathbf{1} \le \mathbf{k} \le \mathbf{k}_{out}}{\Gamma, \Delta \vdash \mathbf{while}(\mathbf{e})\{\mathbf{st}\} : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})} \quad (\text{S-WH})
$$

(A) Tier-based typing rules for expressions and statements (from [HKMP22b])

$$
\frac{\Gamma_w, \Omega, \Delta \vdash \bar{\mathbf{X}} : \overline{\mathbf{W} \to \mathbf{W}} \quad \Gamma_w, \Omega, \Delta \vdash \bar{\mathbf{x}}, \bar{\mathbf{y}} : \overline{\mathbf{W}} \quad \Gamma_w, \Omega, \Delta \vdash \mathbf{x} : \mathbf{W}}{\Gamma_w, \Omega, \Delta \vdash \mathbf{P}(\bar{\mathbf{X}}, \bar{\mathbf{x}})\{[\text{var } \bar{\mathbf{y}};] \text{ st return } \mathbf{x}\} : (\overline{\mathbf{W} \to \mathbf{W}}) \to \overline{\mathbf{W} \to \mathbf{W}}} \quad (\text{PR-DEC})
$$

$$
\frac{\Gamma_w, \Omega, \Delta \vdash \mathbf{P}(\bar{\mathbf{X}}, \bar{\mathbf{x}})\{\dots\} : (\overline{\mathbf{W} \to \overline{\mathbf{W}}}) \to \overline{\mathbf{W} \to \mathbf{W}} \quad \Gamma_w, \Omega, \Delta \vdash \bar{\mathbf{c}} : \overline{\mathbf{W} \to \overline{\mathbf{W}}} \quad \Gamma_w, \Omega, \Delta \vdash \bar{\mathbf{t}} : \overline{\mathbf{W}}}{\Gamma_w, \Omega, \Delta \vdash \mathbf{call} \ P(\bar{\mathbf{c}}, \bar{\mathbf{t}}) : \mathbf{W}} \quad (\text{P-CALL})
$$

$$
\frac{\Gamma_w(\mathbf{a}) = \mathbf{T} \quad (\text{P-VAR}) \quad \frac{\Gamma_w \upharpoonright \{\mathbf{a} : \mathbf{T}\}, \Omega, \Delta \vdash \mathbf{t} : \mathbf{T}'}{\Gamma_w, \Omega, \Delta \vdash \lambda \mathbf{a} . \mathbf{t} : \mathbf{T} \to \mathbf{T}'} \quad (\text{P-ABS})}
{\Gamma_w, \Omega, \Delta \vdash \mathbf{a} : \mathbf{T}}
$$

$$
\frac{\Gamma_w, \Omega, \Delta \vdash t_1 : T \to T' \quad \Gamma_w, \Omega, \Delta \vdash t_2 : T}{\Gamma_w, \Omega, \Delta \vdash t_1 @ t_2 : T'} \quad (\text{P-APP})
$$

$$
\frac{\Gamma_w, \Omega, \Delta \vdash \mathbf{prg} : T \quad \Gamma_w, \Delta \vdash \mathbf{body}(\mathbf{p}) : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out}) \quad \Omega(\mathbf{p}) = \langle \Gamma, (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out}) \rangle}{\Gamma_w, \Omega, \Delta \vdash \mathbf{declare} \ p \ \mathbf{in} \ \mathbf{prg} : T} \quad (\text{P-DEC})
$$

$$
\frac{\Gamma_w \upharpoonright \{x : \mathbf{W}\}, \Omega, \Delta \vdash t : \mathbf{W}}{\Gamma_w, \Omega, \Delta \vdash \{x \to t\} : \mathbf{W} \to \mathbf{W}} \quad (\text{P-CLOS})
$$

$$
\frac{\Gamma_w \upharpoonright \{\mathbf{a} : \mathbf{T}\}, \Omega, \Delta \vdash \mathbf{prg} : \mathbf{T}'}{\Gamma_w, \Omega, \Delta \vdash \mathbf{box} \ [\mathbf{a}] \ \mathbf{in} \ \mathbf{prg} : \mathbf{T} \to \mathbf{T}'} \quad (\text{P-BOX})
$$

(B) Simple typing rules for procedures, terms, closures and programs

FIGURE 5. Tier-based type system
**Example 3.2.** Consider the operators !=, pred, and sucᵢ discussed in Figure 1 and an operator typing environment Δ that is safe and such that !=, pred, sucᵢ ∈ dom(Δ). We can set Δ(!=)(1) = {1 → 1 → 1} ∪ {k → k' → 0 | k, k' ≤ 1}, as != is neutral. However 1 → 0 → 1 /∈ Δ(!=)(1) as it breaks Condition (1) above (i.e., 1 ≤ min(1, 0) is false).

We can also set Δ(pred)(2) = {2 → k | k ≤ 2} ∪ {1 → k | k ≤ 1} ∪ {0 → 0}. We also have Δ(sucᵢ)(1) = {1 → 0, 0 → 0}. 1 → 1 /∈ Δ(sucᵢ)(1) as sucᵢ is a positive operator and, due to Condition (2) above, the operator output tier has to be strictly smaller than 1.

A program prg is a *safe program* if there exist a simple typing environment Γ<sub>w</sub>, a procedure typing environment Ω, and a safe operator typing environment such that prg is well-typed for these environments, i.e., Γ<sub>w</sub>, Ω, Δ ⊢ prg : (W → W) → W → W can be derived. Let SAFE be the set of safe programs.

**Example 3.3.** We consider the program ce of Figure 1. We define the operator typing environment Δ by

$$
\begin{align*}
\Delta(!=)(2) &\triangleq \{1 \to 1 \to 1\}, \\
\Delta(pred)(1) &\triangleq \{1 \to 1\}, \\
\Delta(\epsilon)(2) &\triangleq \{0, 1\}.
\end{align*}
$$

As the three operators !=, pred, and ϵ are neutral, the environment Δ is safe.

We define the simple typing environment Γ<sub>w</sub> by Γ<sub>w</sub>(u) ≜ W, Δ(v) ≜ W, Δ(z) ≜ W, Γ<sub>w</sub>(X<sub>1</sub>) ≜ W → W, and Γ<sub>w</sub>(X<sub>2</sub>) ≜ W → W. We define the variable typing environment Γ by Γ(u) ≜ 1, Δ(v) ≜ 1, Δ(z) ≜ 0. Finally, define the procedure typing environment Ω by Ω(p<sub>KS</sub>) ≜ ⟨Γ, (1, 2, 1)⟩. Using the rules of Figure 5, the following typing judgment can be derived Γ<sub>w</sub>, Ω, Δ ⊢ ce : (W → W) → W → W.

The full typing derivation is provided in Figure 6 where we sometimes use the notation Γ<sub>w</sub>, Ω, Δ ⊢ ē : T as a shorthand notation for ∀i ≤ |ē|, Γ<sub>w</sub>, Ω, Δ ⊢ eᵢ : T under the assumption that |ē| = |T|. The operator typing environment is safe and, consequently, ce is a safe program, i.e., ce ∈ SAFE.

**3.4. Intuitions.** We now give some brief intuition to the reader on the type discipline in the particular case where exactly two tiers, 0 and 1, are involved. The type system splits program variables, expressions, and statements between the two disjoint tiers:

• 0 corresponds to a program component whose execution may result in an increase of the memory size and that cannot control the program flow (similar to safe inputs in [BC92]).

• 1 corresponds to a program component whose execution cannot result in a memory increase and that may control the program flow (similar to normal inputs in [BC92]).

The type system of Figure 5 is composed of two sub-systems. The typing rules provided in Figure 5B enforce that terms follow a standard simply-typed discipline. The typing rules of Figure 5A will implement a standard non-interference type discipline à la Volpano et al. [VIS96] on the expression (and statement) tier, preventing data flows from tier 0 to tier 1. The transition between the two sub-type-systems is performed in the rule (P-DEC) of Figure 5B that checks that the procedure body follows the tier-based type discipline once and for all in a procedure declaration.

In Figure 5A, as tier 1 data cannot grow and are the only data driving the program flow, the number of distinct memory configurations on such data for a terminating procedure is
Let $\diamondsuit_{a_1, \dots, a_n}^{T_1, \dots, T_n} \triangleq \Gamma_W \cup \{a_1 : T_1, \dots, a_n : T_n\}, \Omega, \Delta$, for $n \ge 0$, and let $\mathbf{w}^W \triangleq \mathbf{w} \to \mathbf{W}$ in:

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

$\frac{\mathbf{w}^W}{\mathbf{x}, \Omega, \Delta, \boxplus} \text{ box } [x, y] \text{ in declare pks in call } \text{KS}(\{x \to X@x\}, \{x \to X@(X@x)\}, y) : (\mathbf{w}^W) \to \mathbf{w}^W \text{ (P-BOX)}$

where $\text{pks} = \text{KS}(X_1, X_2, v)\{u := X_1(\epsilon \upharpoonright \epsilon); z := \epsilon; \text{while}(v != \epsilon)\{v := \text{pred}(v); z := X_2(z \upharpoonright u)\}, \Omega(\text{pks}) = (\Gamma, (1, 2, 1))\}$, and

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

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

$\pi_2' \triangleright \Gamma, \Delta \triangleright \text{while}(v != \epsilon)\{v := \text{pred}(v); z := X_2(z \upharpoonright u)\} : (1, 2, 1)$

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

$\pi_1' \triangleright \Gamma, \Delta \triangleright v := \text{pred}(v); z := X_2(z \upharpoonright u) : (1, 1, 1)$

<caption>FIGURE 6. Typing derivation for the program `ce` of Figure 1</caption>
polynomial in the size of the program input (i.e., number of symbols). Hence a typable and terminating procedure has a *polynomial step count* in the sense of [Coo92], i.e., on any input, the execution time of a procedure is bounded by a first-order polynomial in the size of their input and the maximal size of any answer returned by an oracle call.

The innermost tier is used to implement a declassification mechanism on operators improving the type-system's expressive power: an operator may be typed differently depending on its calling context (the statement where it is applied). This is the reason why more than 2 tiers can be used in general.

The outermost tier is used to ensure that oracles are only called on inputs of bounded size. This latter restriction on oracle calls enforces a semantic restriction, called *finite lookahead revision*, introduced in [KS17, KS18] and requiring that, during each computation, the number of calls performed by the oracle on an input of increasing size is bounded by a constant.

Let MPT be the class of second-order functionals computable by an oracle Turing machine with a polynomial step count and a finite lookahead revision. [KS18] shows that $BFF = \lambda(MPT)_2$. The type system of Figure 5 ensures that each terminating procedure of a well-typed program computes a function in MPT.

# 4. CHARACTERIZATIONS OF THE CLASS OF BASIC FEASIBLE FUNCTIONALS

## 4.1. Safe and terminating programs.
In this section, we show that typable (SAFE) and terminating (SN) programs capture exactly the class of basic feasible functionals (BFF).

For a given set $S$ of functionals having simple type over $W$, let $S_2$ be the restriction of $S$ to second-order functionals and let $\lambda(S)$ be the set of functions computed by closed simply-typed lambda terms using functions in $S$ as constants. Formally, let $\lambda(S)$ be the set of functions denoted by the set of closed simply-typed lambda terms generated inductively as follows:

* for each type $\tau$, variables $x^\tau, y^\tau, \dots$ are terms,

* each functional $F \in S$ of type $\tau$, $F^\tau$ is a term,

* for any term $t^{\tau'}$ and variable $x^\tau$, $\lambda x^\tau.t^{\tau'}$ is a term of type $\tau \to \tau'$,

* for any terms $t^{\tau \to \tau'}$ and $s^\tau$, $t^{\tau \to \tau'} s^\tau$ is a term of type $\tau'$.

Each lambda term of type $\tau$ represents a function of type $\tau$ and terms are considered up to $\beta$ and $\eta$ equivalences. $\lambda(S)_2$ is called the *second-order simply-typed lambda closure* of $S$.

The second-order simply-typed lambda closure is monotone with respect to set inclusion.

**Lemma 4.1.** For any two classes of functionals $\mathcal{X}, \mathcal{Y}$, if $\mathcal{X} \subseteq \mathcal{Y}$ then $\lambda(\mathcal{X})_2 \subseteq \lambda(\mathcal{Y})_2$.

Procedures correspond to programs from [HKMP22b], we can redefine the class ST from this paper in terms of procedures. The semantics and type system restricted to procedures are equivalent, hence, given a program $p_\phi = c \ return \ x$ belonging to the set of safe and terminating programs ST, we can write a program

$$ prg = \mathit{box}[Y, \bar{y}] \ \mathit{in} \ \mathit{declare} \ P(X, \bar{x})\{c \ return \ x\} \ \mathit{in} \ \mathit{call} \ P(Y, \bar{y}) $$

that computes the same functional as $p_\phi$ and is typable and strongly normalizing provided the procedure is typable and terminating.
**Definition 4.2 (Safe and terminating procedures).** Given $p \triangleq P(\bar{x}, \bar{x})\{\text{var } \bar{y}; \text{st return } x\}$, $p$ is safe if there exist a simple typing environment $\Gamma_w$, a safe operator typing environment and a triplet of tiers $(k, k_{in}, k_{out})$ such that $p$ is well-typed for these environments, i.e. $\Gamma_w, \Delta \vdash st : (k, k_{in}, k_{out})$ can be derived using the rules of Figure 5.

Let $\llbracket p \rrbracket$ be defined by $\llbracket p \rrbracket(\bar{f}, \bar{w}) = w$ iff $(\{p\}, \mu_0[\bar{x} \leftarrow \bar{w}, \bar{x} \leftarrow \bar{f}], \text{call } P(\bar{x}, \bar{x})) \to_{\text{env}} w$ (following Figure 3). $\llbracket p \rrbracket$ is a second order partial functional in $(W \to W)^{|\bar{x}|} \to W^{|\bar{x}|} \hookrightarrow W$. If $\llbracket p \rrbracket$ is a total function, then we say that the procedure $p$ is terminating.

Let ST be the set of safe and terminating procedures, and $\llbracket \text{ST} \rrbracket$ the set of functionals computed by those procedures.

The characterization of BFF in terms of safe and terminating procedures discussed in the introduction can be stated as follows.

**Theorem 4.3 [HKMP22b].** $\lambda(\llbracket \text{ST} \rrbracket)_2 = \text{BFF}$.

We now introduce an intermediate lemma stating that $\llbracket \text{SN} \cap \text{SAFE} \rrbracket$ is stable under second-order simply-typed lambda closure.

**Lemma 4.4.** $\lambda(\llbracket \text{SN} \cap \text{SAFE} \rrbracket)_2 = \llbracket \text{SN} \cap \text{SAFE} \rrbracket$.

*Proof.* The inclusion $\llbracket \text{SN} \cap \text{SAFE} \rrbracket \subseteq \lambda(\llbracket \text{SN} \cap \text{SAFE} \rrbracket)_2$ trivially holds by definition of the second-order simply-typed lambda closure.

We show that $\lambda(\llbracket \text{SN} \cap \text{SAFE} \rrbracket)_2 \subseteq \llbracket \text{SN} \cap \text{SAFE} \rrbracket$ holds. We first define a straightforward transformation $[\cdot]$ from lambda terms representing functions in $\lambda(\llbracket \text{SN} \cap \text{SAFE} \rrbracket)_2$ to terms in $\text{SN} \cap \text{SAFE}$ as follows:

$$ 
\begin{align*}
[x^\tau] &\triangleq a_x \\
[\lambda x^\tau . t^{\tau'}] &\triangleq \lambda[x^\tau] . [t^{\tau'}] \\
[t^{\tau \to \tau'} s^\tau] &\triangleq [t^{\tau \to \tau'}]@[s^\tau] \\
[F] &\triangleq t, \text{ with } F \in \llbracket \text{SN} \cap \text{SAFE} \rrbracket,
\end{align*}
$$

for $t$ such that $\llbracket \text{box } [\bar{Y}, \bar{y}] \text{ in declare } \bar{p} \text{ in } t \rrbracket = F$. The existence of $t$ is ensured by the definition of $\llbracket \text{SN} \cap \text{SAFE} \rrbracket$ but there is no uniqueness. For a given function $f \in \lambda(\llbracket \text{SN} \cap \text{SAFE} \rrbracket)_2$, let $t_f$ be a lambda term representing $f$. $[t_f]$ is the term obtained by applying the above transformation. Let $p_f$ be the corresponding list of procedure declarations obtained for each $F$ in the above transformation. The function $f$ is of order 2, hence its simple type must be of the shape $\underbrace{(W \to W) \to (W \to W) \cdots (W \to W)}_{k} \to \underbrace{W \to W \cdots W}_{l} \to W$. The program $\text{prg} = \text{box } [X_1, \dots, X_k, x_1, \dots, x_l] \text{ in declare } p_f \text{ in } ([t_f]@X_1@\cdots@X_k)@x_1@\cdots@x_l$ is such that $\llbracket \text{prg} \rrbracket = \lambda X_1, \dots, X_k. \lambda x_1, \dots, x_l. (f X_1 \cdots X_k x_1 \cdots x_l) = f \in \lambda(\llbracket \text{SN} \cap \text{SAFE} \rrbracket)_2$, as the second-order simply-typed lambda closure is closed under $\eta$-expansion. Moreover, the program $\text{prg}$ is safe (as each procedure can be typed independently) and terminating (as it computes a total function). Hence $\llbracket \text{prg} \rrbracket \in \llbracket \text{SN} \cap \text{SAFE} \rrbracket$. $\square$

We are now ready to state a first characterization of BFF in terms of safe (SAFE) and terminating (SN) programs, showing that the external simply-typed lambda-closure of Theorem 4.3 can be removed.

**Theorem 4.5.** $\llbracket \text{SN} \cap \text{SAFE} \rrbracket_2 = \text{BFF}$.
*Proof.* Any procedure $\mathbf{p} = \mathbf{P}(\bar{\mathbf{x}}, \bar{\mathbf{x}})\{\dots\}$ can be transformed into a program:

$$ \mathbf{prg}_p \triangleq \mathbf{box}[\bar{\mathbf{Y}}, \bar{\mathbf{y}}] \text{ in declare } \mathbf{P}(\bar{\mathbf{x}}, \bar{\mathbf{x}})\{\dots\} \text{ in call } \mathbf{P}(\bar{\mathbf{z}} \to \mathbf{Y}@\mathbf{z})\bar{\mathbf{y}}, $$

that is, programs consisting of a single procedure call and a single procedure declaration and where oracle calls are restricted to type-1 program inputs $\bar{\mathbf{Y}}$ (basically the oracles). Moreover, it is easy to check that if $\mathbf{p} \in \mathbf{ST}$ then $\mathbf{prg}_p \in \mathbf{SN} \cap \mathbf{SAFE}$, by construction. Consequently, it holds that:

$$ \mathbf{BFF} = \lambda(\llbracket \mathbf{ST} \rrbracket)_2 \qquad (\text{By Theorem 4.3}) $$

$$ \subseteq \lambda(\llbracket \mathbf{SN} \cap \mathbf{SAFE} \rrbracket)_2 \qquad (\text{By Lemma 4.1}) $$

$$ = \llbracket \mathbf{SN} \cap \mathbf{SAFE} \rrbracket \qquad (\text{By Lemma 4.4}) $$

Now we show that $\llbracket \mathbf{SN} \cap \mathbf{SAFE} \rrbracket \subseteq \lambda(\llbracket \mathbf{ST} \rrbracket)_2$. Any function $f \in \llbracket \mathbf{SN} \cap \mathbf{SAFE} \rrbracket$ is computed by a safe and terminating program $\mathbf{prg}$, i.e., $\llbracket \mathbf{prg} \rrbracket = f$. For a given simple type $\mathbf{T}$, let $[\mathbf{T}]^*$ be the type obtained as follows $[\mathbf{W}]^* = \mathcal{W}$ and $[\mathbf{T} \to \mathbf{T}']^* = [\mathbf{T}]^* \to [\mathbf{T}']^*$. We define by induction a straightforward transformation $[\cdot]^*$ that maps a program in normal form in $\mathbf{SN} \cap \mathbf{SAFE}$ to a function in $\lambda(\llbracket \mathbf{ST} \rrbracket)_2$:

$$ [\mathbf{a} : \mathbf{T}]^* \triangleq \mathbf{x}_a[\mathbf{T}]^* $$

$$ [\lambda \mathbf{a} . \mathbf{t} : \mathbf{T} \to \mathbf{T}']^* \triangleq \lambda[\mathbf{a} : \mathbf{T}]^* . [\mathbf{t} : \mathbf{T}']^* $$

$$ [\mathbf{t} @ \mathbf{t} ' : \mathbf{T}]^* \triangleq [\mathbf{t} : \mathbf{T}' \to \mathbf{T}]^* [\mathbf{t}' : \mathbf{T}']^* $$

$$ [\mathbf{call} \ \mathbf{P}(\bar{\mathbf{c}}, \bar{\mathbf{t}}) : \mathbf{W}]^* \triangleq \llbracket \mathbf{prg}_p \rrbracket [\bar{\mathbf{c}} : \mathbf{T} \to \mathbf{T}]^* [\bar{\mathbf{t}} : \mathbf{T}]^* $$

$$ [\{\mathbf{x} \to \mathbf{t}\} : \mathbf{W} \to \mathbf{W}]^* \triangleq \lambda[\mathbf{x} : \mathbf{W}]^* . [\mathbf{t} : \mathbf{W}]^* $$

$$ [\mathbf{box}[\bar{\mathbf{X}}, \bar{\mathbf{x}}] \text{ in } \dots \text{ in } \mathbf{t}]^* \triangleq \lambda[\bar{\mathbf{X}} : \overline{\mathbf{W} \to \mathbf{W}}]^* . \lambda[\bar{\mathbf{x}} : \overline{\mathbf{W}}]^* . [\mathbf{t}]^* $$

In the above definitions, we have sometimes omitted types for readability. In the box [] in rule, the declarations do not get translated as procedures will be treated as function symbols from $\llbracket \mathbf{ST} \rrbracket$ written as $\llbracket \mathbf{prg}_p \rrbracket$. Indeed, as $\mathbf{prg}_p \in \mathbf{SN} \cap \mathbf{SAFE}$ it implies that the procedure $\mathbf{p}$ is terminating and safe, hence $\mathbf{p} \in \mathbf{ST}$. In the rule for application @, the type $\mathbf{T}'$ can be guessed easily as we know that the term is simply-typed (the program is safe). $\llbracket \mathbf{prg} \rrbracket^* \in \lambda(\llbracket \mathbf{ST} \rrbracket)_2$ trivially holds as $\mathbf{prg}^*$ is a second-order functional consisting of a simply-typed lambda closure of functions $\llbracket \mathbf{prg}_p \rrbracket \in \llbracket \mathbf{ST} \rrbracket$. Moreover, one can easily check that $f = \llbracket \mathbf{prg} \rrbracket = [\mathbf{prg}]^*$ and so the result follows by applying Theorem 4.3. $\square$

We want to highlight that the characterization of Theorem 4.5 is not just “moving” the simply-typed lambda-closure inside the programming language by adding a construct for lambda-abstraction. Indeed, the soundness of this result crucially depends on some choices on the language design that we have enforced: the restricted ability to compose oracles using closures, and the read-only mode of oracles inside a procedure call, implemented through continuations.

**4.2. Safe and terminating rank-r programs.** The characterization of Theorem 4.5 allows to use lambda abstractions in terms of the language. However, we also show that this characterization is still valid in the absence of lambda-abstraction.

A safe program $\mathbf{prg}$ with respect to a typing derivation $\pi$ is a *rank-r* program, if for any typing sub-derivation $\pi' \supset \Gamma_w, \Omega, \Delta \vdash \lambda \mathbf{a} . \mathbf{t} : \mathbf{T}$ of $\pi$, it holds that $\mathbf{ord}(\mathbf{T}) \le r$. In other words, all lambda-abstractions are type-k terms, for $k \le r$. In particular, a rank-(r+1) program,
for $r \ge 1$, has variables that are at most type-$r$ variables. Rank-0 and rank-1 programs may have both type-0 and type-1 variables as these variables can still be captured by closures, procedure declarations, or boxes.

For a given set $S$ of well-typed programs, let $S_r$ be the subset of rank-$r$ programs in $S$, i.e., $S_r \triangleq \{\mathbf{prg} \in S \mid \mathbf{prg}$ is a rank-$r$ program\}$. For example, SAFE$_r$ denotes the set of safe rank-$r$ programs. It trivially holds that SAFE = $\cup_{r \in \mathbb{N}}$SAFE$_r$. The rank is clearly not uniquely determined for a given program. In particular, any rank-$r$ program is also a rank-$(r+1)$ program. Consequently, for any set $S$ of well-typed programs and any $i \le j$, it trivially holds that $S_i \subseteq S_j$.

**Example 4.6.** Program `ce` of Figure 1 is in SAFE$_0$. Indeed, `ce` ∈ SAFE, `cf`. Example 3.3, and `ce` is a rank-0 program, as it does not use any lambda-abstraction.

Now we revisit the syntax and semantics of safe rank-0 programs in SAFE$_0$. The programs are generated by the syntax of Figure 2, where the terms are all type-0, denoted by $t^0$, and redefined by:

$$ \text{Terms} \quad t^0 ::= x \mid X@t^0 \mid \text{call } P(\bar{c}, \overline{t^0}) $$

Moreover, there is no longer a need for call-by-name reduction in the big step operational semantics. As a consequence, the rules (TVar), (OA), and (Call) of Figure 3C can be replaced by the following simplified rules:

$$ \begin{array}{l@{\qquad}l} \overline{(\sigma, \mu, \mathbf{x}) \to_{\text{env}} \mu(\mathbf{x})} & (\text{TVar}^0) \qquad \frac{(\sigma, \mu, \mathbf{t}_1^0) \to_{\text{env}} w}{(\sigma, \mu, \mathbf{X}@\mathbf{t}_1^0) \to_{\text{env}} \mu(\mathbf{X})(w)} \quad (\text{OA}^0) \\[2ex] \overline{(\sigma, \mu, \overline{\mathbf{t}^0}) \to_{\text{env}} \overline{w}} & (\sigma, \mu[\overline{\mathbf{x}} \leftarrow \overline{w}, \overline{\mathbf{y}} \leftarrow \overline{\varepsilon}], \overline{\mathbf{x}} \mapsto \overline{c}, \mathbf{st}) \to_{\text{st}} \mu' \\[2ex] \multicolumn{2}{@{}l}{(\sigma \cup \{\mathbf{P}(\overline{\mathbf{x}}, \overline{\mathbf{x}})\}\{\text{var } \overline{\mathbf{y}}; \text{ st return } \mathbf{z}\}, \mu, \text{call } \mathbf{P}(\overline{c}, \overline{\mathbf{t}^0})) \to_{\text{env}} \mu'(\mathbf{z})} \quad (\text{Call}^0) \end{array} $$

We will show that any function in BFF can be computed by a program in SN ∩ SAFE$_0$. For that purpose, we consider an alternative characterization of BFF that was introduced in [KS19] inspired by $PV^ω$ from [CU93]. $PV^ω$ is defined as the set of simply-typed $\lambda$ terms defined from function symbols for each FP functions and a higher order recursor $\mathcal{R}$. Instead of this recursor, we are going to use another bounded iterator $\mathcal{I}'$ that is shown in [KS19] to be equivalent to $\mathcal{R}$. Let $\mathcal{I}': (W \to W) \to W \to W \to W \to W$ be semantically defined by $\mathcal{I}'(F, a, b, c) = (\lambda x.F(lmin(x, a)))^{|c|}(b)$, where $lmin \in W \to W \to W$ is defined by

$$ lmin(a, b) = \begin{cases} a & \text{if } |a| < |b|, \\ b & \text{otherwise.} \end{cases} $$

Let $PV_2^ω$ be the second-order restriction of $PV^ω$. [CK89] defines BFF as the set of functions denoted by $PV_2^ω$ terms and from [KS19] we have that $PV_2^ω$ terms can be written as $\lambda \overline{\mathbf{x}}. \lambda \overline{\mathbf{x}}. t$, where $t$ is an order 0 term of type $W$ in normal form that is defined inductively by:

$$ t ::= x \mid X(\overline{t}) \mid F(\overline{t}) \mid \mathcal{I}'(\lambda z.t, t, t, t) $$

where $x$ and $z$ are order 0 variable of type $W$, $X$ is an order 1 variable of type $W^n \to W$, $F \in \text{FP}$ is an order 1 function of type $W^n \to W$. Using [CU93, Theorem 5.12] extended to terms containing order 1 free variables, we know that in the normal form of those terms $t$, the only $\lambda$ appearing are the $\lambda z.t$ used as the first argument of the recursor $\mathcal{I}'$.
**Proposition 4.7.** $\lambda(\{\mathcal{I}'\} \cup \text{FP})_2 = \text{BFF}$, where FP is the class of first-order polynomial time computable functions.

*Proof.* From [CK89], we know that the set of functions denoted by closed $PV_2^\omega$ terms corresponds to BFF, that is $\text{BFF} = \lambda(\{\mathcal{R}\} \cup \text{FP})_2$. [KS19] introduces an iterator $\mathcal{I}$ and the considered iterator $\mathcal{I}'$, and proves ([KS19, Lemma 2.3]) that $\lambda(\{\mathcal{R}\} \cup \text{FP}) = \lambda(\{\mathcal{I}\} \cup \text{FP})$, then that $\lambda(\{\mathcal{I}\} \cup \text{FP}) = \lambda(\{\mathcal{I}'\} \cup \text{FP})$ ([KS19, Theorem 4.3]).

We conclude that $\lambda(\{\mathcal{I}'\} \cup \text{FP})_2 = \text{BFF}$.

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

In order to prove completeness, let us now provide three examples of programs and show they belong to $\text{SAFE}_0$. The examples are a program computing the addition, a program simulating a polynomial time Turing machine, and a program computing the second order iterator $\mathcal{I}'$.

**Example 4.8 (Addition).** The following program computes the unary addition:

```
box [x,y] in
  declare add(u,v) {
    while (u != e) {
      u := pred(u);
      v := suc1(v)
    }
    return v
  }

in call add(x,y)
```

This program is in $\text{SAFE}_0$. Indeed, it can be given the type $W \to W \to W$ for the safe operator typing environment $\Delta$ defined by

$$ 
\begin{align*}
\Delta(\text{!=})(\mathbf{1}) &\triangleq \{\mathbf{1} \to \mathbf{1} \to \mathbf{1}\} & \Delta(\epsilon)(\mathbf{1}) &\triangleq \{\mathbf{1}\} \\
\Delta(\text{pred})(\mathbf{1}) &\triangleq \{\mathbf{1} \to \mathbf{1}\} & \Delta(\text{suc1})(\mathbf{1}) &\triangleq \{\mathbf{0} \to \mathbf{0}\},
\end{align*}
$$

the procedure typing environment $\Omega$ defined by $\Omega(\text{add}(u, v)\{\dots\}) = \langle\Gamma, (\mathbf{1}, \mathbf{1}, \mathbf{0})\rangle$ with $\Gamma(u) = \mathbf{1}$ and $\Gamma(v) = \mathbf{0}$, and the simple typing environment $\Gamma_W$ such that $\Gamma_W(u) = \Gamma_W(v) = W$.

Notice that any polynomial over unary words can be encoded by a typable program in $\text{SAFE}_0$ that follows a similar programming pattern and typing discipline.

**Example 4.9 (Turing machines).** Consider a one tape (deterministic) Turing Machine on a binary word. Its tape can be encoded by variables $x$ and $y$, containing respectively the reversed part of the tape to the left of the head and the right part of the tape. The head of the tape is pointing on the first symbol of $y$, if any. States are encoded by constant words, with a special $s^0$ word for the initial state The current state is stored in the variable $z$.

The machine running in time $\text{time}$ on input $\text{input}$ can be encoded by a procedure declaration, with a unique `while` loop that will iterate $|\text{time}|$ times the code that simulates one step transition of the machine. This code consists in conditionals for testing the character under the head and the current state. In the procedure TM, of program $\text{prg}_\text{TM}$ below, we detail an example of a transition, namely the case when the state is $s$ and read symbol is 0. We assume that the transition function $\delta$ defines the next state as $s'$, that the symbol 1 is written, and that the head moves to the right. In other words, $\delta(s, 0) = (s', 1, \text{right})$ is encoded. Other cases follow the same pattern.
box [t,d] in
declare TM(time, input) {
  var x,y,z;
  x := ϵ;
  y := input;
  z := s⁰; //Initial state
  while (time != ϵ) {
    if (head(y) == 0) {
      if (z == s) { //transition (s, 0) -> (s', 1, right)
        z := s';
        x := suc₁(x);
        y := pred(y)
      }
      else {...};
      ...
    }
    ...
    time := pred(time)
  }
  return y
}
in call TM(t,d)

Procedure TM can be typed by a variable typing environment Γ and a safe operator typing environment Δ such that:

$$ \forall e \in \{x, y, s, \text{input}\}, \Gamma(e) = 0, \quad \forall \text{op} \in \{!=, \text{suc}_1, \text{pred}\}, \quad 0 \to 0 \in \Delta(1)(\text{op}), \\ \Gamma(\text{time}) = 1, \quad \forall \text{op} \in \{==, \text{pred}, \text{head}\}, \quad 1 \to 1 \in \Delta(1)(\text{op}). $$

Consequently, $\text{prg}_{\text{TM}} \in \text{SAFE}_0$.

As a consequence of Examples 4.8 and 4.9, any polynomial time TM can be simulated in $\text{SAFE}_0$.

**Lemma 4.10.** For any polynomial time Turing machine *M*, there exists a $\text{SAFE}_0$ program that computes the same function as *M*.

*Proof.* To prove this lemma, we use the procedure from Example 4.9, encoding the execution of $|\text{time}|$ steps of Turing machine *M* on input. To give a correct bounding time, we assume that this machine runs in polynomial time, that is, there exists a polynomial *P* such that on input *n*, the Turing machine halts in time bounded by *P*(*n*|*n*|). As indicated in Example 4.8, we can write a safe procedure that computes *P* in unary. In other words, there is a procedure poly that takes input as argument and returns the unary representation of *P*(|input|).

The following program hence computes the same function as *M*.

box [x] in
declare poly(input) { ... }
TM(time, input) { ... }
in call TM(call poly(x), x)

Both procedures have already been shown to be safe and the program has rank 0. ☐
**Example 4.11** (Second-order iterator). The following program computes a variant (modulo padding) of the second-order iterator $\mathcal{I}'$ using the operator $\text{lmin}$ that computes the functional $\text{lmin}$ defined in Section 4.2.

```pascal
box [X, x₁, x₂, x₃] in
  declare It(Y, x, y, z) {
    var u;
    u := y;
    while (z != ϵ) {
      u := Y(lmin(u, x)↑ x);
      z := pred(z)
    }
    return u
  }

in call It(X, x₁, x₂, x₃)
    procedure it
```

This program can be shown to be in $\text{SAFE}_0$ by setting a variable typing environment $\Gamma$ such that $\Gamma(\mathbf{u}) = \Gamma(\mathbf{x}) = \Gamma(\mathbf{y}) = \mathbf{0}$ and $\Gamma(\mathbf{z}) = \mathbf{1}$.

We are now ready to characterize BFF in terms of safe and terminating rank-0 programs.

**Theorem 4.12.** $[\text{SN} \cap \text{SAFE}_0] = \text{BFF}$.

*Proof.* Lemma 4.10 shows how polynomial time Turing machines can be simulated by a $\text{SAFE}_0$ and SN program, hence for any $F \in \text{FP}$, there exist procedures $\mathbf{p}^F$ and $\mathbf{tm}^F$ with name $\text{Poly}^F$ and $\mathbf{TM}^F$ such that call $\mathbf{TM}^F(\text{call Poly}^F(\mathbf{x}), \mathbf{x})$ computes $F(\mathbf{x})$. Example 4.11 exhibits how $\mathcal{I}'$ can be programmed in $\text{SN} \cap \text{SAFE}_0$ using a procedure it with name It. Moreover, for any procedure $\mathbf{p}$ thus defined, there exists a variable typing environment $\Gamma$, a safe operator typing environment $\Delta$, and a triplet of tiers $(\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})$ such that the judgment $\Gamma, \Delta \vdash \text{body}(\mathbf{p}) : (\mathbf{k}, \mathbf{k}_{in}, \mathbf{k}_{out})$ can be derived and calls to procedures $\mathbf{n}(\mathbf{p})$ terminate on all inputs as all the considered functions are total. For a given functional denoted by $\lambda\bar{X}.\lambda\bar{x}.t \in \text{PV}_2^\omega$ in normal form, that is where all the $\lambda$ appearing in $t$ are the first argument of an $\mathcal{I}'$, let $\mathbf{F}(t)$ be a sequence of the procedures encoding the functions in $\{\mathcal{I}'\} \cup \text{FP}$ that are applied in $t$. We use notations $\emptyset$ and $\sqcup$ to respectively denote the empty sequence and the concatenation of procedures without duplication. Now we provide a transformation $[\cdot]^\dagger$ that maps a normal form of $\text{PV}_2^\omega$ to a program:

$$ \mathbf{F}(x_i) \triangleq \emptyset \qquad [x_i]^\dagger \triangleq x_i $$
$$ \mathbf{F}(X_i) \triangleq \emptyset \qquad [X_i]^\dagger \triangleq X_i $$
$$ \mathbf{F}(X(t_1, \dots, t_k)) \triangleq \sqcup \mathbf{F}(t_i) \qquad [X(t_1, \dots, t_k)]^\dagger \triangleq (\dots([X]^\dagger \sqcup [t_1]^\dagger)\dots) \sqcup [t_k]^\dagger $$
$$ \mathbf{F}(F(\bar{t})) \triangleq \mathbf{F}(\bar{t}) \sqcup \mathbf{tm}^F \sqcup \mathbf{p}^F \qquad [F(\bar{t})]^\dagger \triangleq \text{call TM}^F(\text{call Poly}^F(\bar{t})^\dagger), [\bar{t}]^\dagger) $$
$$ \mathbf{F}(\lambda z.t) \triangleq \mathbf{F}(t) \qquad [\lambda z.t]^\dagger \triangleq \{[z]^\dagger \to [t]^\dagger\} $$
$$ \mathbf{F}(\lambda z.t_1, t_2, t_3, t_4) \triangleq \sqcup \mathbf{F}(t_i) \sqcup \text{it} \qquad [\mathcal{I}'(\lambda z.t_1, t_2, t_3, t_4)]^\dagger \triangleq \text{call It}([\lambda z.t_1]^\dagger, [t_2]^\dagger, [t_3]^\dagger, [t_4]^\dagger) $$
$$ \mathbf{F}(t_1, \dots, t_k) \triangleq \sqcup \mathbf{F}(t_i) \qquad [t_1, \dots, t_k]^\dagger \triangleq [t_1]^\dagger, \dots, [t_k]^\dagger $$
$$ [\lambda \bar{X}.\lambda \bar{x}.t]^\dagger \triangleq \text{box} [[\bar{X}, \bar{x}]^\dagger] \text{ in declare } \mathbf{F}(t) \text{ in } [t]^\dagger $$

For any $f$ denoted by normal form $\lambda\bar{X}.\lambda\bar{x}.t \in \text{PV}_2^\omega$, we have $[[\lambda\bar{X}.\lambda\bar{x}.t]^\dagger]] = f$. Moreover, $[\lambda\bar{X}.\lambda\bar{x}.t]^\dagger \in \text{SN} \cap \text{SAFE}_0$ as it is terminating and safe, and the transformation $[\cdot]^\dagger$
does not make use of any lambda-abstraction. Hence $f \in [[SN \cap SAFE_0]]$ and, consequently, BFF $\subseteq [[SN \cap SAFE_0]]$.

Conversely, $SN \cap SAFE_0 \subseteq SN \cap SAFE$. Consequently, $[[SN \cap SAFE_0]] \subseteq [[SN \cap SAFE]] = BFF$, by Theorem 4.5. $\square$

Hence the characterization of Theorem 4.5 is just a conservative extension of Theorem 4.12: lambda-abstractions, viewed as a construct of the programming language, allow for more expressive power in the programming discipline but do not capture more functions. As lambda-abstraction is fully removed from the programming language, this also shows that the simply-typed lambda closure of Theorem 4.3 can be simulated through restricted oracle compositions in our programming language using closures and continuations.

Moreover, the full hierarchy of safe and terminating rank-r programs collapses.

**Corollary 4.13.** $\forall r \in \mathbb{N}, [[SN \cap SAFE_r]] = BFF$.

**4.3. Type inference.** Let the size $|p|$ of the procedure $p$ be the total number of symbols in $p$. Type inference for procedures is already known to be cubic in their size, as demonstrated in [HKMP22b].

**Theorem 4.14** [HKMP22b]. *Given a procedure $p$ and a safe operator typing environment $\Delta$, deciding if there exists a variable typing environment $\Gamma$ and a triplet of tiers $(k, k_{in}, k_{out})$ such that $\Gamma, \Delta \vdash \mathbf{body}(p) : (k, k_{in}, k_{out})$ holds can be done in time $O(|p|^3)$.*

The proof of this result uses a reduction to 2-SAT with $O(|p| \times k^2)$ clauses, which can be solved in time linear in the number of clauses [EIS76, APT79], for some tier $k \le |p|$.

Let the size $|\mathbf{prg}|$ of the program $\mathbf{prg}$ be the total number of symbols in $\mathbf{prg}$. Type inference is tractable for safe programs.

**Theorem 4.15.** *Given a program $\mathbf{prg}$ and a safe operator typing environment $\Delta$, a deciding whether $\mathbf{prg} \in \mathbf{SAFE}$ holds is a P-complete problem.*

* deciding whether $\mathbf{prg} \in \mathbf{SAFE}$ holds is a P-complete problem.

* deciding whether $\mathbf{prg} \in \mathbf{SAFE}_0$ holds can be done in time $O(|\mathbf{prg}|^3)$.

*Proof.* Showing that $\mathbf{prg} \in \mathbf{SAFE}$ consists in finding a simple typing environment $\Gamma_W$ and a procedure typing environment $\Omega$ such that $\Gamma_W, \Omega, \Delta \vdash \mathbf{prg} : \overline{W} \rightarrow \overline{W} \rightarrow \overline{W} \rightarrow W$ can be derived. Now suppose that $\mathbf{prg} = \mathbf{box}[\overline{X}, \overline{x}]$ in $\mathbf{declare} \ \overline{p}$ in $\mathbf{t}$. After $|\overline{X}, \overline{x}|$ applications of the rule (P-BOX) of Figure 5B, we end up into the following judgment $\Gamma_W \uplus \{\overline{X} : \overline{W} \rightarrow \overline{W}, \overline{x} : \overline{W}\}, \Omega, \Delta \vdash \mathbf{declare} \ \overline{p}$ in $\mathbf{t} : W$. Deriving the above judgment consists of deriving:

$$ \pi \supset \Gamma_W \uplus \{\overline{X} : \overline{W} \rightarrow \overline{W}, \overline{x} : \overline{W}\}, \Omega, \Delta \vdash \mathbf{t} : W. $$

and deriving $|\overline{p}|$ judgments of the shape:

$$ \pi_i \supset \Omega_1(p_i), \Delta \vdash \mathbf{body}(p_i) : \Omega_2(p_i) $$

with $1 \le i \le |\overline{p}|$, $\overline{p} = p_1, \dots, p_{|\overline{p}|}$, after $|\overline{p}|$ applications of the rule (P-DEC) of Figure 5B. By Theorem 4.14, we know that type inference can be done in time $O(|p_i|^3)$, for each derivation $\pi_i$. Hence, it follows that all the judgments $\pi_i$ can be inferred in time $O(|\mathbf{prg}|^3)$.

It remains to study the type inference problem for the derivation $\pi$. By looking at Figure 5B, the typing discipline for terms follows a standard simply-typed discipline augmented with constants (the procedure calls). It is well-known that type inference in the simply-typed lambda-calculus is a P-complete problem as any instance of the Circuit Value Problem (CVP) can be encoded in the former [Mai04]. For example, true and false can be
encoded as the simple types $\lambda x.\lambda y.x : T \to T' \to T$ and $\lambda x.\lambda y.y : T \to T' \to T'$, respectively, and the Boolean disjunction can be encoded by $\lambda x.\lambda y.(x (\lambda x.\lambda y.x) y) : ((T_1 \to T_2 \to T_1) \to T_3 \to T_4) \to T_3 \to T_4$. The final type can be flatten to W by performing an arbitrary number of applications. Hence on a term encoding a circuit in such a way, type inference corresponds to circuit evaluation.

For checking that a program is in $\text{SAFE}_0$, as there are no lambda-abstraction, the only admissible types for variables are $W$ and $W \to W$ and the simple type inference of the above proof can be done in time linear in $|\text{prg}|$ as it just consists in a linear syntactical check on programs. Hence the asymptotic complexity of checking that a program is in $\text{SAFE}_0$ is the complexity of deriving the judgments $\pi_i$ for procedure bodies. $\square$

Tractability of type inference is a nice property of the type system. Showing $\text{prg} \in \text{SN}$ is at least as hard as showing the termination of a first-order program, hence $\Pi_2^0$-hard in the arithmetical hierarchy. Therefore, the characterizations of Theorems 4.3, 4.5, and 4.12 are unlikely to be decidable, let alone tractable. The purpose of the next Section will be to specify a tractable termination criterion preserving completeness of the characterizations of Theorem 4.5 and Theorem 4.12.

## 5. A COMPLETENESS-PRESERVING TERMINATION CRITERION

In this section, we show that the undecidable termination assumption (SN) can be replaced with a criterion, called SCP<sub>S</sub>, adapted from the Size-Change Termination (SCT) techniques of [LJB01], that is decidable in polynomial time and that preserves the completeness of the characterizations.

### 5.1. Some considerations on program termination.
We first show that studying the termination of a safe program can be reduced to the study of the procedure termination. For that purpose, we need to define what is meant for a procedure to terminate by looking at the program semantics of Figure 3C.

A procedure $p = P(\bar{x}, \bar{x})\{\text{var } \bar{y}; \text{st return } z\}$ is *terminating* (strongly normalizing) if for any $\bar{w} \in \bar{W}$, any $\bar{f} \in \bar{W} \to \bar{W}$, there exists $v \in W$ such that the judgment $\{p\}, \mu[\bar{Y} \leftarrow \bar{f}, \bar{y} \leftarrow \bar{w}]$, call $P(\{z \to Y@z\}, \bar{y}) \to_{\text{env}} v$ can be derived.

**Lemma 5.1.** For a given $\text{prg} \in \text{SAFE}$, if all procedures defined in $\text{prg}$ terminate, then $\text{prg}$ is terminating.

*Proof.* If all procedures of a given program are terminating then any procedure call appearing in a term is terminating. As the terms are simply-typed, they are known to be terminating, as a direct consequence of the strong normalization of the simply-typed lambda-calculus [Tai67]. $\square$

Hence, ensuring the termination of each procedure of a given safe program is a sufficient condition for the program to terminate. The converse trivially does not hold as, for example, a procedure with an infinite loop may be declared and not be called within a given safe program.
**5.2. Size-Change Termination.** SCT relies on the fact that if all infinite executions imply an infinite descent in a well-founded order, then no infinite execution exists. To apply this fact for proving termination, [LJB01] defines Size-Change Graphs (SCGs) that exhibit decreases in the parameters of function calls and then studies the infinite paths in all possible infinite sequences of calls. If all those infinite sequences have at least one strictly decreasing path, then the program must terminate for all inputs. While SCT is PSpace-complete, Ben-Amram and Lee [BL07] develop a more effective technique, called SCP, that is in P. The SCP technique is strong enough for our use case. In the literature, SCT and SCP are applied to pure functional languages. As we shall enforce termination of procedures, we will follow the approach of [Ave06] adapting SCT to imperative programs.

First, we distinguish two kinds of operators that will enforce some (strict) decrease.

**Definition 5.2.** An $n$-ary operator $\mathit{op}$ is (strictly) decreasing in $i$, for $i \le n$, if $\forall \bar{w} \in \overline{\mathcal{W}}$, $\bar{w} \ne \bar{\epsilon}$, $|\llbracket \mathit{op} \rrbracket(\bar{w})| \le |w_i| (|\llbracket \mathit{op} \rrbracket(\bar{w})| < |w_i|$, respectively) and $\llbracket \mathit{op} \rrbracket(\bar{\epsilon}) = \epsilon$.

For operators of arity greater than 2, $i$ may not be unique but will be fixed for each operator in what follows.

For simplicity, we will assume that assignments of the considered programs are *flattened*, that is for any assignment $\mathbf{x} := \mathbf{e}$, either $\mathbf{e} = \mathbf{y} \in \mathcal{V}_0$, or $\mathbf{e} = \mathbf{op}(\bar{\mathbf{x}})$, with $\bar{\mathbf{x}} \in \overline{\mathcal{V}}_0$, or $\mathbf{e} = \mathbf{X}(\mathbf{y} \upharpoonright \mathbf{z})$, with $\mathbf{y}, \mathbf{z} \in \mathcal{V}_0$ and $\mathbf{X} \in \mathcal{V}_1$. Notice that, by using extra type-0 variables, any program can be easily transformed into a program with flattened assignments, while preserving semantics and safety properties.

For each assignment of a procedure $\mathbf{p}$, we design a bipartite graph, called a SCG, whose nodes are type-0 variables in $(\mathbf{local}(\mathbf{p}) \cup \mathbf{param}(\mathbf{p})) \cap \mathcal{V}_0$ and arrows indicates decreases or stagnation from the old variable to the new. If a variable may increase, then the new variable will not have an in-arrow.

The bipartite graph is generated for any flattened assignment $\mathbf{x} := \mathbf{e}$ by:

* for each $\mathbf{y}, \mathbf{y} \ne \mathbf{x}$, we draw arrows from left $\mathbf{y}$ to right $\mathbf{y}$.

* If $\mathbf{e} = \mathbf{y}$, we draw an arrow from left $\mathbf{y}$ to right $\mathbf{x}$.

* If $\mathbf{e} = \mathbf{op}(\bar{\mathbf{x}})$, with $\mathbf{op}$ a:

- decreasing operator in $i$, we draw an arrow from $\mathbf{x}_i$ to $\mathbf{x}$.

- strictly decreasing operator in $i$, we draw a "down-arrow" from $\mathbf{x}_i$ to $\mathbf{x}$.

In all other cases (neutral and non-decreasing operators, positive operators, oracle calls), no arrow is drawn. We will name this SCG graph $G(\mathbf{x} := \mathbf{e})$. Finally, for a set $V$ of variables, $G^V$ will denote the SCG obtained as a subgraph of $G$ restricted to the variables of $V$.

**Example 5.3.** Here are the SCGs associated to simple assignments of a procedure with three type-0 variables $\mathbf{x}, \mathbf{y}, \mathbf{z}$ using a strictly decreasing operator in 1 (**pred**), a decreasing operator in 2 (**min**), a positive operator (+1), and an oracle call.

<table><thead><tr><th>y := pred(x)</th><th>y := min(x, y)</th><th>x := x + 1</th><th>x := X(y &vdash; z)</th></tr></thead><tbody><tr><td>x &larr; x<br>y &larr; y<br>z &larr; z</td><td>x &larr; x<br>y &larr; y<br>z &larr; z</td><td>x &larr; x<br>y &larr; y<br>z &larr; z</td><td>x &larr; x<br>y &larr; y<br>z &larr; z</td></tr></tbody></table>
The language $\mathcal{L}(st)$ of (potentially infinite) sequences of SCG associated with the statement st is defined inductively as an $\infty$-regular expression.

$$ \begin{aligned} \mathcal{L}(x := e) &\triangleq G(x := e) & \mathcal{L}(\mathit{if}(e)\{\mathit{st}_1\}\mathit{else}\{\mathit{st}_2\}) &\triangleq \mathcal{L}(\mathit{st}_1) + \mathcal{L}(\mathit{st}_2) \\ \mathcal{L}(\mathit{st}_1; \mathit{st}_2) &\triangleq \mathcal{L}(\mathit{st}_1) \cdot \mathcal{L}(\mathit{st}_2) & \mathcal{L}(\mathit{while}(e)\{\mathit{st}_1\}) &\triangleq \mathcal{L}(\mathit{st}_1)^{\infty} \end{aligned} $$

where, following the standard terminology for automata [NP85], $\mathcal{L}(st)^{\infty}$ is defined by $\mathcal{L}(st)^{\infty} \triangleq \mathcal{L}(st)^* + \mathcal{L}(st)^{\omega}$. In the composition of SCGs, we are interested in paths that advance through the whole concatenated graph. Such a path implies that the final value of the destination variable is of length at most equal to the initial value of the source variable. If the path contains a down-arrow, then the length of the corresponding words decreases strictly.

**Definition 5.4.** Following the terminology of [BL07], a (potentially infinite) sequence of SCGs has a *down-thread* if the associated concatenated graph contains a path spanning every SCG in the sequence and this path includes a down-arrow.

**Example 5.5.** Consider the statement

$$ \mathit{st} \triangleq y := \mathit{pred}(x); y := \mathit{min}(x, y); x := x + 1; x := X(y | z), $$

whose SCGs are described in Example 5.3. The concatenated graph obtained from the (unique and finite) sequence of SCGs in $\mathcal{L}(st)$ is provided below. It contains a *down-thread* (the path from $x$ to $y$).

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

Note however that the concatenated graph associated to st; st does not contain a *down-thread*.

A (potentially infinite) sequence of SCGs is *fan-in free* if the in-degree of nodes is at most 1. By construction, all the considered SCGs are *fan-in free*.

**5.3. Safety and Polynomial Size-Change.** Unfortunately, programs with down-threads can loop infinitely in the $\epsilon$ state. To prevent this, we restrict the analysis to cases where while loops explicitly break out when the decreasing variable reaches $\epsilon$, that is procedures with while loops of the shape $\mathit{while}(x != \epsilon)\{\mathit{st}\}$.

**Definition 5.6.** For a given set $V$ of variables, we will say that st satisfies the simple graph property for $V$ if for any while loop $\mathit{while}(x != \epsilon)\{\mathit{st}'\}$ in st all sequences of SCGs $G_1^{V} G_2^{V} \dots$ such that $G_1 G_2 \dots \in \mathcal{L}(\mathit{st}')$ are *fan-in free* and contain a *down-thread* from $x$ to $x$. A procedure is in $\mathit{SCP}_S$ if its statement satisfies the simple graph property for the set of variables in while guards. A program is in $\mathit{SCP}_S$ if all its procedures are in $\mathit{SCP}_S$.

**Example 5.7.** The program ce of Figure 1 is in $\mathit{SCP}_S$. The language $\mathcal{L}(\mathit{body}(p_{KS}))$ corresponding to the body of procedure $p_{KS}$ is equal to $G_1 \cdot G_2 \cdot (G_3 \cdot G_4)^{\infty}$, where the SCGs $G_i$ are defined as follows:
<table><thead><tr><th>G<sub>1</sub></th><th>G<sub>2</sub></th><th>G<sub>3</sub></th><th>G<sub>4</sub></th></tr><tr><th>u := X<sub>1</sub>(ε ↾ ε)</th><th>z := ε</th><th>v := pred(v)</th><th>z := X<sub>2</sub>(z ↾ u)</th></tr></thead><tbody><tr><td>v —&rarr; v</td><td>v —&rarr; v</td><td>v —&darr; v</td><td>v —&rarr; v</td></tr><tr><td>u u</td><td>u —&rarr; u</td><td>u —&rarr; u</td><td>u —&rarr; u</td></tr><tr><td>z —&rarr; z</td><td>z z</td><td>z —&rarr; z</td><td>z z</td></tr></tbody></table>

First, the procedure body satisfies the syntactic restrictions on programs (flattened expressions and restricted while guards). Moreover, the procedure body satisfies the simple graph property for {$v$} as there is always a down-thread on the path from $v$ to $v$ in ($G_3 \cdot G_4$)$^\infty$ and any corresponding sequence is fan-in free. Consequently, the program `ce` is in $\text{SCP}_S \cap \text{SAFE}_0$, by Example 4.6.

**Lemma 5.8.** $\text{SCP}_S \cap \text{SAFE} \subseteq \text{SN}$.

*Proof.* All the procedures defined in a program of $\text{SCP}_S$ have down-threads for all executions and are terminating. Hence, by Lemma 5.1, the program is terminating. □

$\text{SCP}_S$ preserves completeness on safe programs for BFF.

**Theorem 5.9.** $[[\text{SCP}_S \cap \text{SAFE}_0]] = [[\text{SCP}_S \cap \text{SAFE}]] = \text{BFF}$.

*Proof.* Examples 4.8, 4.9, and 4.11 illustrate that any function in {$\mathcal{I}'$} $\cup$ FP can be computed by a program in $\text{SAFE}_0$. The programs corresponding to these three examples are in $\text{SCP}_S$ as they mostly consist of procedures with loops of the shape `while(x != e){st; x := pred(x)}` for some variable $x$ (u, time, and z, respectively) that is not assigned to in `st`. Consequently, there is a down-thread from $x$ to $x$ and `st` satisfies the simple graph property on {$x$}. We obtain that:

$$
\begin{align*}
\text{BFF} &= \lambda({\mathcal{I}'} \cup \text{FP})_2 && \text{(By Proposition 4.7)} \\
&\subseteq \lambda([\text{SCP}_S \cap \text{SAFE}_0])_2 && \text{(By Examples 4.8, 4.9, and 4.11)} \\
&\subseteq \lambda([\text{SCP}_S \cap \text{SAFE}])_2 && \text{(By Lemma 4.1)} \\
&\subseteq \lambda([\text{SN} \cap \text{SAFE}])_2 && \text{(By Lemmata 4.1 and 5.8)} \\
&= [\text{SN} \cap \text{SAFE}] && \text{(By Lemma 4.4)} \\
&= \text{BFF} && \text{(By Theorem 4.5)}
\end{align*}
$$

Consequently, $\lambda([\text{SCP}_S \cap \text{SAFE}_0])_2 = \lambda([\text{SCP}_S \cap \text{SAFE}])_2 = \text{BFF}$. Now it remains to notice that Lemma 4.4 still holds when $\text{SCP}_S$ is substituted to SN, i.e., $\lambda([\text{SCP}_S \cap \text{SAFE}])_2 = [[\text{SCP}_S \cap \text{SAFE}]]$ and the result follows. □

While in general deciding if a program satisfies the size-change termination criterion is PSpace-complete, $\text{SCP}_S$ can be checked in quadratic time and, consequently, we obtain the following results.

**Proposition 5.10.** Given a program prg, deciding if $\text{prg} \in \text{SCP}_S$ holds can be done in time $O(|\text{prg}|^2)$.

*Proof.* Given a procedure p, deciding if $p \in \text{SCP}_S$ is a particular instance of SCP that [BL07] treats in time $O(|p|^2)$. So deciding if the whole program is in $\text{SCP}_S$ can be done in $O(|\text{prg}|^2)$ by checking that each procedure is in $\text{SCP}_S$ (the size of each procedure being bounded by $|\text{prg}|$). □
**Theorem 5.11.** Given a program prg and a safe operator typing environment,

* deciding whether $prg \in \text{SCP}_S \cap \text{SAFE}$ is a P-complete problem.

* deciding whether $prg \in \text{SCP}_S \cap \text{SAFE}_0$ can be done in time $O(|prg|^3)$.

*Proof.* By Proposition 5.10 and the proof of Theorem 4.15. □

## 6. CONCLUSION AND FUTURE WORK

We have presented a typing discipline and a termination criterion for a programming language that is sound and complete for the class of second-order polytime computable functionals, BFF. This characterization has three main advantages:

(1) it is based on a natural higher-order programming language with imperative procedures;

(2) it is pure as it does not rely on an extra semantic requirements (such as taking the lambda closure);

(3) belonging to the set $\text{SCP}_S \cap \text{SAFE}$ can be decided in polynomial time.

The benefits of tractability is that our method can be automated. However the expressive power of the captured programs is restricted. This drawback is the price to pay for tractability and we claim that the full SCT method, known to be PSpace-complete, could be adapted in a more general way to our programming language in order to capture more programs at the price of a worse complexity. Moreover, any termination criterion based on the absence of infinite data flows with respect to some well-founded order could work and preserve completeness of our characterizations. Another issue of interest is to study whether the presented approach could be extended to characterize BFF in a purely functional language.

*Acknowledgments.* Bruce M. Kapron's work was supported in part by NSERC RGPIN-2021-02481. Emmanuel Hainry and Romain Péchoux's work was supported by the Inria associate team TC(Pro)$^3$.

## REFERENCES

[APT79] Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linear-time algorithm for testing the truth of certain quantified boolean formulas. *Information Processing Letters*, 8(3):121–123, 1979. doi:10.1016/0020-0190(79)90002-4.

[Ave06] James Avery. Size-change termination and bound analysis. In Masami Hagiya and Philip Wadler, editors, *FLOPS 2006*, volume 3945 of *Lecture Notes in Computer Science*, pages 192–207. Springer, 2006. doi:10.1007/11737414_14.

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

[BCE$^{+}$98] Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The relative complexity of NP search problems. *Journal of Computer and System Sciences*, 57(1):3–19, 1998. doi:10.1006/jcss.1998.1575.

[BDL16] Patrick Baillot and Ugo Dal Lago. Higher-order interpretations and program complexity. *Information and Computation*, 248:56–81, 2016. doi:10.1016/j.ic.2015.12.008.

[BL07] Amir M. Ben-Amram and Chin Soon Lee. Program termination analysis in polynomial time. *ACM Transactions on Programming Languages and Systems*, 29(1):5:1–5:37, 2007. doi:10.1145/1180475.1180480.

[BM10] Patrick Baillot and Damiano Mazza. Linear logic by levels and bounded time complexity. *Theoretical Computer Science*, 411(2):470–503, 2010. doi:10.1016/j.tcs.2009.09.015.
[BMM11] Guillaume Bonfante, Jean-Yves Marion, and Jean-Yves Moyen. Quasi-interpretations a way to control resources. *Theoretical Computer Science*, 412(25):2776-2796, 2011. doi:10.1016/j.tcs.2011.02.007.

[BT04] Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda-calculus. In *Logic in Computer Science, LICS 2004*, pages 266-275. IEEE, 2004. doi:10.1109/LICS.2004.1319621.

[CK89] Stephen A. Cook and Bruce M. Kapron. Characterizations of the basic feasible functionals of finite type. In *30th Annual Symposium on Foundations of Computer Science (FOCS 1989)*, pages 154-159. IEEE, 1989. doi:10.1109/SFCS.1989.63471.

[Cob65] Alan Cobham. The intrinsic computational difficulty of functions. In Y. Bar-Hillel, editor, *Proceedings of the International Conference on Logic, Methodology, and Philosophy of Science*, pages 24-30. North-Holland, Amsterdam, 1965.

[Con73] Robert L. Constable. Type two computational complexity. In *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.

[Coo92] Stephen A. Cook. Computability and complexity of higher type functions. In *Logic from Computer Science*, pages 51-72. Springer, 1992. doi:10.1007/978-1-4612-2822-6_3.

[CU93] Stephen A. Cook and Alasdair Urquhart. Functional interpretations of feasibly constructive arithmetic. *Annals of Pure and Applied Logic*, 63(2):103-200, 1993. doi:10.1016/0168-0072(93)90044-E.

[EIS76] Shimon Even, Alon Itai, and Adi Shamir. On the complexity of timetable and multicommodity flow problems. *SIAM Journal on Computing*, 5(4):691-703, 1976. doi:10.1137/0205048.

[FHHP15] Hugo Férée, Emmanuel Hainry, Mathieu Hoyrup, and Romain Péchoux. Characterizing polynomial time complexity of stream programs using interpretations. *Theoretical Computer Science*, 585:41-54, 2015. doi:10.1016/j.tcs.2015.03.008.

[GAC12] Sicun Gao, Jeremy Avigad, and Edmund M. Clarke. $\delta$-complete decision procedures for satisfiability over the reals. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, *Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings*, volume 7364 of *Lecture Notes in Computer Science*, pages 286-300. Springer, 2012. doi:10.1007/978-3-642-31365-3_23.

[Gir98] Jean-Yves Girard. Light linear logic. *Information and Computation*, 143(2):175-204, 1998. doi:10.1006/inco.1998.2700.

[Háj79] Petr Hájek. Arithmetical hierarchy and complexity of computation. *Theoretical Computer Science*, 8:227-237, 1979.

[HKMP22a] Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux. Complete and tractable machine-independent characterizations of second-order polytime. In *Foundations of Software Science and Computation Structures, FOSSACS 2022*, pages 368-388, 2022. doi:10.1007/978-3-030-99253-8_19.

[HKMP22b] Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux. A tier-based typed programming language characterizing feasible functionals. *Logical Methods in Computer Science*, 18, 2022. doi:10.46298/LMCS-18(1:33)2022.

[HP20] Emmanuel Hainry and Romain Péchoux. Theory of higher order interpretations and application to basic feasible functions. *Logical Methods in Computer Science*, 16(4), 2020. doi:10.23638/LMCS-16(4:14)2020.

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

[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, 1991. doi:10.1109/SFCS.1991.185389.

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

[KS17] Akitoshi Kawamura and Florian Steinberg. Polynomial running times for polynomial-time oracle machines. In *2nd International Conference on Formal Structures for Computation and*
*Deduction, FSCD 2017*, pages 23:1–23:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. doi:10.4230/LIPIcs.FSCD.2017.23.

[KS18] Bruce M. Kapron and Florian Steinberg. Type-two polynomial-time and restricted lookahead. In *Logic in Computer Science, LICS 2018*, pages 579–588. ACM, 2018. doi:10.1145/3209108.3209124.

[KS19] Bruce M. Kapron and Florian Steinberg. Type-two iteration with bounded query revision. In *Proceedings Third Joint Workshop on Developments in Implicit Computational complExity and Foundational & Practical Aspects of Resource Analysis, DICE-FOPARA@ETAPS 2019*, EPTCS, pages 61–73, 2019. doi:10.4204/EPTCS.298.5.

[LJB01] Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In Chris Hankin and Dave Schmidt, editors, *POPL 2001*, pages 81–92. ACM, 2001. doi:10.1145/360204.360210.

[LM93] Daniel Leivant and Jean-Yves Marion. Lambda calculus characterizations of poly-time. *Fundamenta Informaticae*, 19(1/2):167–184, 1993.

[Mai04] Harry G. Mairson. Linear lambda calculus and ptime-completeness. *Journal of Functional Programming*, 14(6):623–633, 2004. doi:10.1017/S0956796804005131.

[Mar11] Jean-Yves Marion. A type system for complexity flow analysis. In *Logic in Computer Science, LICS 2011*, pages 123–132. IEEE Computer Society, 2011. doi:10.1109/LICS.2011.41.

[Meh76] Kurt Mehlhorn. Polynomial and abstract subrecursive classes. *Journal of Computer and System Sciences*, 12(2):147–178, 1976. doi:10.1016/S0022-0000(76)80035-9.

[NP85] Maurice Nivat and Dominique Perrin. *Automata on infinite words*. Springer, 1985. doi:10.1007/3-540-15641-0.

[Tai67] William W. Tait. Intensional interpretations of functionals of finite type I. *Journal of Symbolic Logic*, 32(2):198–212, 1967. doi:10.2307/2271658.

[Tow90] Mike Townsend. Complexity for type-2 relations. *Notre Dame Journal of Formal Logic*, 31(2):241–262, 1990. doi:10.1305/ndjfl/1093635419.

[VIS96] Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. A sound type system for secure flow analysis. *Journal of Computer Security*, 4(2-3):167–187, 1996. doi:10.3233/JCS-1996-42-304.

[Win93] Glynn Winskel. *The formal semantics of programming languages: an introduction*. MIT press, 1993.