# Cyclic Implicit Complexity

Gianluca Curzi∗ and Anupam Das∗ ∗University of Birmingham

###### Abstract.

_Circular_ (or _cyclic_) proofs have received increasing attention in recent
years, and have been proposed as an alternative setting for studying
(co)inductive reasoning. In particular, now several type systems based on
circular reasoning have been proposed. However, little is known about the
complexity theoretic aspects of circular proofs, which exhibit sophisticated
loop structures atypical of more common ‘recursion schemes’. This paper
attempts to bridge the gap between circular proofs and _implicit computational
complexity_. Namely we introduce a circular proof system based on the
Bellantoni and Cook’s famous safe-normal function algebra, and we identify
suitable proof theoretical constraints to characterise the polynomial-time and
elementary computable functions.

##  1\. Introduction

Formal proofs are traditionally seen as finite mathematical objects modelling
logical or mathematical reasoning. Non-wellfounded (but finitely branching)
proofs represent a generalization of the notion of formal proof to an
infinitary setting. In non-wellfounded proof theory, special attention is
devoted to _regular_ (or _circular_) proofs, i.e. those non-wellfounded proofs
having only finitely many distinct sub-proofs. Regular proofs can be turned
into finite structures called _cycle normal forms_ , usually given as finite
trees with additional ‘backpointers’. However, regular proofs admit fallacious
reasoning. To recover consistency, a standard solution is based on the
introduction of non-local correctness criteria, e.g.  _progressiveness_ ,
typically checked by Büchi automata on infinite words.

Regular proofs, and their corresponding cycle normal forms, have been employed
to reason about modal $\mu$-calculus and fixed-point logics [NW96, DHL06b],
induction and coinduction [BS11], Kleene algebra [DP17, DP18], linear logic
[BDS16], arithmetic [Das18], system $\mathsf{T}$ [KPP21a, Das21], and
continuous cut-elimination [Min78, FS13]. In particular, [KPP21a] and [Das21]
investigate the computational aspects of regular proofs. Due to their
coinductive nature, non-wellfounded proofs are able to define any number-
theoretic (partial) function. Definability can be then restricted by combining
regularity and progressiveness: the former rules out uncomputable functions,
while the latter recovers termination.

Little is known, however, about the complexity-theoretic aspects of regular
proofs. Kuperberg, Pinault and Pous [KPP19] introduced a circular proof system
based on Kleene algebras and seen as a computational machinery for recognising
languages. The system and its affine version capture, respectively, the
regular languages and the languages accepted in logarithmic time by random-
access Turing machines. Their work does not consider the cut rule, which
allows for a proof-theoretical description of function composition and is the
key ingredient to express recursion in a cyclic-theoretic setting.

The present paper aims at bridging the gap between regular proofs and Implicit
Computational Complexity (ICC), a branch of computational complexity studying
machine-free languages and calculi able to capture a given complexity class
without relying on explicit resource bounds. Our starting point is Bellantoni
and Cook’s function algebra $\mathsf{B}$ characterising the polynomial time
computable functions ($\mathbf{F}\mathbf{PTIME}$) using _safe recursion_.
Functions of $\mathsf{B}$ have shape $f(x_{1},...,x_{n};y_{1},...,y_{m})$,
where the semicolon separates the _normal_ arguments $x_{1},...,x_{n}$ from
the _safe_ arguments $y_{1},...,y_{m}$. The idea behind safe recursion is that
only normal arguments can be used as recursive parameters, while recursive
calls can only appear in safe position. This prevents recursive calls becoming
recursive parameters of other previously defined functions. In the spirit of
the Curry-Howard paradigm, which identifies proofs and programs, $\mathsf{B}$
can be alternatively designed as a sequent calculus proof-system where safe
recursion is introduced by a specific inference rule $\mathsf{srec}$. In this
system, a two-sorted function $f(x_{1},...,x_{n};y_{1},...,y_{m})$ is
represented by a derivation of the sequent ${{\Box
N}},\overset{n}{\ldots},{{\Box N}},{N},\overset{m}{\ldots},{N}\Rightarrow N$
where $N$ is the ground type for natural numbers and ${\Box N}$ is its modal
version.

Starting from $\mathsf{B}$ we shall consider the non-wellfounded proofs, or
_coderivations_ , generated by the rules of the subsystem
$\mathsf{B}^{-}:=\mathsf{B}\setminus\mathsf{srec}$. The circular proof system
$\mathsf{C}\mathsf{N}\mathsf{B}$ is then obtained by considering the regular
and progressing coderivations of $\mathsf{B}^{-}$ which satisfy a further
criterion, called _safety_. On the one hand, regularity and progressiveness
ensure that coderivations of $\mathsf{C}\mathsf{N}\mathsf{B}$ define total
computable functions; on the other hand, the latter criterion ensures that the
recursion mechanisms defined in this infinitary setting are safe, i.e. the
recursive call of a function is never the recursive parameter of the step
function.

Despite $\mathsf{C}\mathsf{N}\mathsf{B}$ having only ground types, it is able
to define safe recursion schemes that nest recursive calls, a property that
typically arises in higher-order recursion. This is in fact a peculiar feature
of regular proofs extensively studied by Das in [Das21], who has shown that
the number-theoretic functions definable by type level $n$ proofs of a
circular version of system $\mathsf{T}$ are exactly those ones definable by
type level $n+1$ proofs of $\mathsf{T}$.

In the setting of ICC, Hofmann [Hof97] and Leivant [Lei99] observed that the
capability of nesting recursive calls by higher-order safe recursion
mechanisms can be used to characterise the elementary time functions
($\mathbf{F}\mathbf{ELEMENTARY}$). In particular, in [Hof97] Hofmann presents
the type system $\mathsf{SLR}$ (Safe Linear Recursion) as a higher-order
version of $\mathsf{B}$. This system has been shown to capture
$\mathbf{F}\mathbf{PTIME}$ once a linearity restriction on the higher-order
‘safe’ recursion operator is imposed, which prevents duplication of the
recursive calls, and hence their nesting.

Following [Hof97], we introduce a linearity requirement for
$\mathsf{C}\mathsf{N}\mathsf{B}$ that is able to control the interplay between
loops and the cut rule, called _left-leaning criterion_. The resulting
circular proof system is called $\mathsf{C}\mathsf{B}$. Intuitively,
$\mathsf{C}\mathsf{B}$ can be seen as a circular version of $\mathsf{B}$,
while $\mathsf{C}\mathsf{N}\mathsf{B}$ can be seen as the circular version of
a new function algebra, called $\mathsf{N}\mathsf{B}$, which generalises
$\mathsf{B}$ by permitting nested versions of the safe recursion scheme. In
particular, in order to define the nesting of recursive calls, the function
algebra for $\mathsf{C}\mathsf{N}\mathsf{B}$ crucially requires the
introduction of ‘auxiliary functions’, i.e. oracles.

The main results of our paper are the following:

  * •

a function is definable in $\mathsf{C}\mathsf{N}\mathsf{B}$ iff it is
$\mathsf{N}\mathsf{B}$ iff it is in $\mathbf{F}\mathbf{ELEMENTARY}$;

  * •

a function is definable in $\mathsf{C}\mathsf{B}$ iff it is in
$\mathbf{F}\mathbf{PTIME}$;

First, we define the function algebras $\mathsf{N}\mathsf{B}^{\subset}$ and
$\mathsf{B}^{\subset}$, respectively obtained by extending
$\mathsf{N}\mathsf{B}$ and $\mathsf{B}$ with a safe recursion mechanism based
on permutation of prefixes. Then we show that $\mathsf{N}\mathsf{B}$ and
$\mathsf{N}\mathsf{B}^{\subset}$ capture precisely the elementary time
computable functions, while $\mathsf{B}^{\subset}$ captures the polytime ones.
Completeness for $\mathsf{C}\mathsf{N}\mathsf{B}$ can be achieved by showing
how to represent the functions of $\mathsf{N}\mathsf{B}$. In a similar way, we
represent the functions of $\mathsf{B}$ in $\mathsf{C}\mathsf{B}$. Soundness
is subtler, as it relies on a translation of coderivations of
$\mathsf{C}\mathsf{N}\mathsf{B}$ and $\mathsf{C}\mathsf{B}$, which are
essentially coinductive objects, into the inductively defined functions of
$\mathsf{N}\mathsf{B}^{\subset}$ and $\mathsf{B}^{\subset}$, respectively.

### Overview of results

The paper is structured as follows. Section 2 discusses $\mathsf{B}$ as a
proof system. In Section 3 we present the non-wellfounded proof system
$\mathsf{B}^{-}$ and its semantics. We then analyse some proof-theoretical
conditions able to restrict the set of definable functions of
$\mathsf{B}^{-}$. This leads us to the circular proof systems
$\mathsf{C}\mathsf{N}\mathsf{B}$ and $\mathsf{C}\mathsf{B}$. In Section 4 we
present the function algebras $\mathsf{N}\mathsf{B}$, $\mathsf{B}^{\subset}$
and $\mathsf{N}\mathsf{B}^{\subset}$, which implement various safe recursion
schemes. Section 5 shows that $\mathsf{B}^{\subset}$ captures
$\mathbf{F}\mathbf{PTIME}$ (46) and that both $\mathsf{N}\mathsf{B}$ and
$\mathsf{N}\mathsf{B}^{\subset}$ capture $\mathbf{F}\mathbf{ELEMENTARY}$
(Corollary 48). These results require a Bounding Lemma (Lemma 43) and the
encoding of the elementary time functions into $\mathsf{N}\mathsf{B}$ (Theorem
47). In Section 6 we show that any function definable in $\mathsf{B}$ is also
definable in $\mathsf{C}\mathsf{B}$ (Theorem 49), and that any function
definable in $\mathsf{N}\mathsf{B}$ is also definable in
$\mathsf{C}\mathsf{N}\mathsf{B}$ (Theorem 52). In Section 7 we present a
translation of $\mathsf{C}\mathsf{N}\mathsf{B}$ into
$\mathsf{N}\mathsf{B}^{\subset}$ that maps $\mathsf{C}\mathsf{B}$
coderivations into $\mathsf{B}^{\subset}$ functions (Lemma 57).

The main results of this section are displayed in Figure 1. Many proofs are
reported in the appendices.

${\mathbf{F}\mathbf{ELEMENTARY}}$${\mathsf{N}\mathsf{B}}$${\mathsf{C}\mathsf{N}\mathsf{B}}$${\mathsf{N}\mathsf{B}^{\subset}}$${\mathsf{B}}$${\mathsf{C}\mathsf{B}}$${\mathsf{B}^{\subset}}$${\mathbf{F}\mathbf{PTIME}}$Theorem
45Theorem 52Theorem 47Lemma 57Theorem 49[BC92]Lemma 57Theorem 45 Figure 1.
Summary of the main results of the paper, where $\rightarrow$ indicates an
inclusion ($\subseteq$) of function classes.

##  2\. Preliminaries: two-tiered ‘safe-normal’ function algebras

Bellantoni and Cook introduced in [BC92] an algebra of functions based on a
simple two-sorted structure. This idea was itself inspired by Leivant’s
impredicative characterisations, one of the founding works in Implicit
Computational Complexity (ICC) [Lei91]. The resulting ‘tiering’ of the
underlying sorts has been a recurring theme in the ICC literature since, and
so it is this structure that shall form the basis of the systems we consider
in this work.

We consider functions on the natural numbers with inputs distinguished into
two sorts: ‘safe’ and ‘normal’. We shall write functions explicitly indicating
inputs, namely writing $f(x_{1},\dots,x_{m};y_{1},\dots,y_{n})$ when $f$ takes
$m$ normal inputs $\vec{x}$ and $n$ safe inputs $\vec{y}$. Both sorts vary
over the natural numbers, but their roles will be distinguished by the closure
operations of the algebras and rules of the systems we consider.

Throughout this work, we write $|x|$ for the length of $x$ (in binary
notation), and if $\vec{x}=x_{1},\dots,x_{m}$ we write $|\vec{x}|$ for the
list $|x_{1}|,\dots,|x_{m}|$.

###  2.1. Bellantoni and Cook’s characterisation of polynomial-time functions

Let us first recall Bellantoni and Cook’s algebra in its original guise.

######  Definition 1 (Bellantoni-Cook algebra).

$\mathsf{B}$ is the smallest class of (two-sorted) functions containing,

  * •

$0(;):=0\in\mathbb{N}$.

  * •

$\pi^{m;n}_{j;}(x_{1},\dots,x_{m};y_{1},\dots,y_{n}):=x_{j}$, whenever $1\leq
j\leq m$.

  * •

$\pi^{m;n}_{;j}(x_{1},\dots,x_{m};y_{1},\dots,y_{n}):=y_{j}$, whenever $1\leq
j\leq n$.

  * •

$\mathsf{s}_{i}(;x):=2x+i$, for $i\in\\{0,1\\}$.

  * •

$\mathsf{p}(;x):=\lfloor{x/2}\rfloor$.

  * •

$\mathsf{cond}(;w,x,y,z):=\begin{cases}x&w=0\\\ y&w=0\mod 2,w\neq 0\\\
z&w=1\mod 2\end{cases}$

and closed under the following:

  * •

(Safe composition)

    * –

If $f(\vec{x},x;\vec{y})\in\mathsf{B}$ and $g(\vec{x};)\in\mathsf{B}$ then
$f(\vec{x},g(\vec{x};);\vec{y})\in\mathsf{B}$.

    * –

If $f(\vec{x};\vec{y},y)\in\mathsf{B}$ and $g(\vec{x};\vec{y})\in\mathsf{B}$
then $f(\vec{x};\vec{y},g(\vec{x};\vec{y}))\in\mathsf{B}$.

  * •

(Safe recursion on notation)111This was originally called ‘predicative
recursion on notation’ by Bellantoni and Cook in [BC92], in reference to
Parsons’ predicative higher-order characterisation of the primitive recursive
functions (à la Kleene). If $g(\vec{x};\vec{y})\in\mathsf{B}$ and
$h_{i}(x,\vec{x};\vec{y},y)\in\mathsf{B}$ for $i=0,1$ then so is
$f(x,\vec{x};\vec{y})$ given by:

$\begin{array}[]{rcll}f(0,\vec{x};\vec{y})&:=&g(\vec{x};\vec{y})\\\
f(\mathsf{s}_{0}x,\vec{x};\vec{y})&:=&h_{0}(x,\vec{x};\vec{y},f(x,\vec{x};\vec{y}))&\text{if
$x\neq 0$}\\\
f(\mathsf{s}_{1}x,\vec{x};\vec{y})&:=&h_{1}(x,\vec{x};\vec{y},f(x,\vec{x};\vec{y}))\end{array}$

Intuitively, in a function $f(\vec{x};\vec{y})\in\mathsf{B}$ only the normal
arguments $\vec{x}$ can be used as recursive parameters. The idea behind safe
recursion is that recursive calls can only appear in safe position, and hence
they can never be used as recursive parameters of other previously defined
functions. Safe composition preserves the distinction between normal and safe
arguments by requiring that, when composing along a normal parameter, the pre-
composing function has no safe parameter at all. As a result, we can move a
normal parameter to a safe position but not vice versa.

Writing $\mathbf{F}\mathbf{PTIME}$ for the class of functions computable in
polynomial-time, the main result of Bellantoni and Cook is:

######  Theorem 2 ([BC92]).

$f(\vec{x};)\in\mathsf{B}$ if and only if
$f(\vec{x})\in\mathbf{F}\mathbf{PTIME}$.

###  2.2. A type theoretic presentation of Bellantoni-Cook

In this section we recall a well-known formulation of Bellantoni and Cook’s
algebra as a type system with modalities to distinguish the two sorts (cf.,
e.g., [Hof97]). In order to facilitate the definition of the circular system
that we present later, we here work with sequent-style typing derivations.

We only consider _types_ (or _formulas_) $N$ and $\Box N$ which intuitively
vary over the natural numbers (we will give a formal semantics soon). We use
$A,B,$ etc. to vary over types. A _sequent_ is an expression
$\Gamma\Rightarrow A$, where $\Gamma$ is a list of types (called the _context_
or _antecedent_) and $A$ is a type (called the _succedent_). For a list of
types $\Gamma={N},\overset{k}{\ldots},{N}$, we write $\Box\Gamma$ for ${{\Box
N}},\overset{k}{\ldots},{{\Box N}}$.

In what follows, we shall essentially identify $\mathsf{B}$ with the
$S4$-style type system in Figure 2. The colouring of type occurrences may be
ignored for now, they will become relevant in the next section. Derivations in
this system are simply called _$\mathsf{B}$ -derivations_, and will be denoted
$\mathcal{D},\mathcal{E},\ldots$, and we write $\mathcal{D}:\Gamma\Rightarrow
A$ if the derivation $\mathcal{D}$ has end-sequent is $\Gamma\Rightarrow A$.

$\scriptstyle\mathsf{id}\;$ $N\Rightarrow N$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
B$ $\scriptstyle\mathsf{w}_{N}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\Rightarrow
B$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
B$ $\scriptstyle\mathsf{w}_{\Box}\;$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
B$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}B},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\Gamma^{\prime}}\Rightarrow
C$ $\scriptstyle\mathsf{e}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}B},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}A},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\Gamma^{\prime}}\Rightarrow
C$

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\Rightarrow
A$ $\scriptstyle\Box_{l}\;$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
A$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Box\Gamma}\Rightarrow
N$ $\scriptstyle\Box_{r}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Box\Gamma}\Rightarrow{\Box
N}$ $\scriptstyle 0\;$ $\Rightarrow N$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
A$ $\scriptstyle\mathsf{s}_{0}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
A$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
A$ $\scriptstyle\mathsf{s}_{1}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
A$

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
N$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\Rightarrow
B$ $\scriptstyle\mathsf{cut}_{N}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
B$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow{\Box
N}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
B$ $\scriptstyle\mathsf{cut}_{\Box}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
B$

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
N$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\Rightarrow
N$${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\Rightarrow
N$ $\scriptstyle\mathsf{cond}_{N}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\Rightarrow
N$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
N$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
N$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
N$ $\scriptstyle\mathsf{cond}_{\Box}\;$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
N$

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
N$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}\Rightarrow
N$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}\Rightarrow
N$ $\scriptstyle\mathsf{srec}\;$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\Rightarrow
N$

Figure 2. System $\mathsf{B}$, as a sequent-style type system.

######  Convention 3 (Left normal, right safe).

In what follows, we shall always assume that sequents have the form ${{\Box
N}},\overset{}{\ldots},{{\Box N}},{N},\overset{}{\ldots},{N}\Rightarrow A$,
i.e. in the LHS all ${\Box N}$ occurrences are placed before all $N$
occurrences. Note that this invariant is maintained by the typing rules of
Figure 2, as long as we insist that $A=B$ in the exchange rule $\mathsf{e}$.
This effectively means that exchange steps have one of the following two
forms:

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\vec{N}^{\prime}}\Rightarrow
A$ $\scriptstyle\mathsf{e}_{N}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\vec{N}^{\prime}}\Rightarrow
A$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Box\vec{N}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\Gamma^{\prime}}\Rightarrow
A$ $\scriptstyle\mathsf{e}_{\Box}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Box\vec{N}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\Gamma^{\prime}}\Rightarrow
A$

Let us point out that this convention does not change the class of definable
functions, under the semantics we are about to give, as we are about to
define, up to permutation of inputs.

We define this system as a class of safe-normal functions by construing each
rule as an operation on safe-normal functions and identifying the system with
the class of thus definable functions. Formally:

######  Definition 4 (Semantics).

Given a $\mathsf{B}$-derivation ${\mathcal{D}:{{\Box
N}},\overset{m}{\ldots},{{\Box N}},{N},\overset{n}{\ldots},{N}\Rightarrow A}$
we define a two-sorted function
$f_{\mathcal{D}}(x_{1},\dots,x_{m};y_{1},\dots,y_{n})$ by induction on the
structure of $\mathcal{D}$ as follows:

  * •

If $\mathcal{D}$ is  $\scriptstyle\mathsf{id}\;$ $N\Rightarrow N$ then
$f_{\mathcal{D}}(;y):=y$.

  * •

If $\mathcal{D}$ has the form  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma\Rightarrow A$ $\scriptstyle\mathsf{w}_{N}\;$ $\Gamma,N\Rightarrow A$
then
$f_{\mathcal{D}}(\vec{x};\vec{y},y):=f_{\mathcal{D}_{0}}(\vec{x};\vec{y})$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma\Rightarrow A$ $\scriptstyle\mathsf{w}_{\Box}\;$ ${\Box
N},\Gamma\Rightarrow A$ then
$f_{\mathcal{D}}(x,\vec{x};\vec{y}):=f_{\mathcal{D}_{0}}(\vec{x};\vec{y})$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma,N,N,\vec{N}^{\prime}\Rightarrow A$ $\scriptstyle\mathsf{e}_{N}\;$
$\Gamma,N,N,\vec{N}^{\prime}\Rightarrow A$ then
$f_{\mathcal{D}}(\vec{x};\vec{y},y,y^{\prime},\vec{y}^{\prime}):=f_{\mathcal{D}_{0}}(\vec{x};\vec{y},y^{\prime},y,\vec{y}^{\prime})$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Box\vec{N},{\Box N},{\Box N},\Delta\Rightarrow A$
$\scriptstyle\mathsf{e}_{\Box}\;$ $\Box\vec{N},{\Box N},{\Box
N},\Delta\Rightarrow A$ then
$f_{\mathcal{D}}(\vec{x},x,x^{\prime},\vec{x}^{\prime};\vec{y}):=f_{\mathcal{D}_{0}}(\vec{x},x^{\prime},x,\vec{x}^{\prime};\vec{y})$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma,N\Rightarrow A$ $\scriptstyle\Box_{l}\;$ ${\Box N},\Gamma\Rightarrow
A$ then
$f_{\mathcal{D}}(x,\vec{x};\vec{y}):=f_{\mathcal{D}_{0}}(\vec{x};\vec{y},x)$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Box\Gamma\Rightarrow N$ $\scriptstyle\Box_{r}\;$ $\Box\Gamma\Rightarrow{\Box
N}$ then $f_{\mathcal{D}}(\vec{x};):=f_{\mathcal{D}_{0}}(\vec{x};)$.

  * •

If $\mathcal{D}$ is  $\scriptstyle 0\;$ $\Rightarrow N$ then
$f_{\mathcal{D}}(;):=0$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma\Rightarrow A$ $\scriptstyle\mathsf{s}_{0}\;$ $\Gamma\Rightarrow A$
then
$f_{\mathcal{D}}(\vec{x};\vec{y}):=\mathsf{s}_{0}(;f_{\mathcal{D}_{0}}(\vec{x};\vec{y}))$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma\Rightarrow A$ $\scriptstyle\mathsf{s}_{1}\;$ $\Gamma\Rightarrow A$
then
$f_{\mathcal{D}}(\vec{x};\vec{y}):=\mathsf{s}_{1}(;f_{\mathcal{D}_{0}}(\vec{x};\vec{y}))$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma\Rightarrow N$ $\textstyle{\scriptstyle\mathcal{D}_{1}}$
$\Gamma,N\Rightarrow A$ $\scriptstyle\mathsf{cut}_{N}\;$ $\Gamma\Rightarrow A$
then
$f_{\mathcal{D}}(\vec{x};\vec{y}):=f_{\mathcal{D}_{1}}(\vec{x};\vec{y},f_{\mathcal{D}_{0}}(\vec{x};\vec{y}))$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma\Rightarrow{\Box N}$ $\textstyle{\scriptstyle\mathcal{D}_{1}}$ ${\Box
N},\Gamma\Rightarrow A$ $\scriptstyle\mathsf{cut}_{\Box}\;$ $\Gamma\Rightarrow
A$ then
$f_{\mathcal{D}}(\vec{x};\vec{y}):=f_{\mathcal{D}_{1}}(f_{\mathcal{D}_{0}}(\vec{x};\vec{y}),\vec{x};\vec{y})$.

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma\Rightarrow N$ $\textstyle{\scriptstyle\mathcal{D}_{1}}$
$\Gamma,N\Rightarrow N$ $\textstyle{\scriptstyle\mathcal{D}_{2}}$
$\Gamma,N\Rightarrow N$ $\scriptstyle\mathsf{cond}_{N}\;$ $\Gamma,N\Rightarrow
N$ then:

$\begin{array}[]{rcll}f_{\mathcal{D}}(\vec{x};\vec{y},0)&:=&f_{\mathcal{D}_{0}}(\vec{x};\vec{y})\\\
f_{\mathcal{D}}(\vec{x};\vec{y},\mathsf{s}_{0}y)&:=&f_{\mathcal{D}_{1}}(\vec{x};\vec{y},y)&\text{if
$y\neq 0$}\\\
f_{\mathcal{D}}(\vec{x};\vec{y},\mathsf{s}_{1}y)&:=&f_{\mathcal{D}_{2}}(\vec{x};\vec{y},y)\end{array}$

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma\Rightarrow N$ $\textstyle{\scriptstyle\mathcal{D}_{1}}$ ${\Box
N},\Gamma\Rightarrow N$ $\textstyle{\scriptstyle\mathcal{D}_{2}}$ ${\Box
N},\Gamma\Rightarrow N$ $\scriptstyle\mathsf{cond}_{\Box}\;$ ${\Box
N},\Gamma\Rightarrow N$ then:

$\begin{array}[]{rcll}f_{\mathcal{D}}(0,\vec{x};\vec{y})&:=&f_{\mathcal{D}_{0}}(\vec{x};\vec{y})\\\
f_{\mathcal{D}}(\mathsf{s}_{0}x,\vec{x};\vec{y})&:=&f_{\mathcal{D}_{1}}(x,\vec{x};\vec{y})&\text{if
$x\neq 0$}\\\
f_{\mathcal{D}}(\mathsf{s}_{1}x,\vec{x};\vec{y})&:=&f_{\mathcal{D}_{2}}(x,\vec{x};\vec{y})\end{array}$

  * •

If $\mathcal{D}$ is  $\textstyle{\scriptstyle\mathcal{D}_{0}}$
$\Gamma\Rightarrow N$ $\textstyle{\scriptstyle\mathcal{D}_{1}}$ ${\Box
N},\Gamma,N\Rightarrow N$ $\textstyle{\scriptstyle\mathcal{D}_{2}}$ ${\Box
N},\Gamma,N\Rightarrow N$ $\scriptstyle\mathsf{srec}_{\Box}\;$ ${\Box
N},\Gamma\Rightarrow N$ then:

$\begin{array}[]{rcll}f_{\mathcal{D}}(0,\vec{x};\vec{y})&:=&f_{\mathcal{D}_{0}}(\vec{x};\vec{y})\\\
f_{\mathcal{D}}(\mathsf{s}_{0}x,\vec{x};\vec{y})&:=&f_{\mathcal{D}_{1}}(x,\vec{x};\vec{y},f_{\mathcal{D}}(x,\vec{x};\vec{y}))&\text{if
$x\neq 0$}\\\
f_{\mathcal{D}}(\mathsf{s}_{1}x,\vec{x};\vec{y})&:=&f_{\mathcal{D}_{2}}(x,\vec{x};\vec{y},f_{\mathcal{D}}(x,\vec{x};\vec{y}))\end{array}$

The above formal semantics exposes how $\mathsf{B}$-derivations and
$\mathsf{B}$ functions relate. The rule $\mathsf{srec}$ in Figure 2
corresponds to safe recursion, and safe composition along safe parameters is
expressed by means of the rules $\mathsf{cut}_{N}$. Note, however, that the
function $f_{\mathcal{D}}$ is not quite defined according to function algebra
$\mathsf{B}$, due to the interpretation of the $\mathsf{cut}_{\Box}$ rule
apparently not satisfying the required constraint on safe composition along a
normal parameter. However, this admission turns out to be harmless, as
exposited in the following proposition:

######  Proposition 5.

Given a $\mathsf{B}$-derivation
$\mathcal{D}:\Box\Gamma,\vec{N}\Rightarrow{\Box N}$, there is a
$\mathsf{B}$-derivation $\mathcal{D}^{*}:\Box\Gamma\Rightarrow{\Box N}$ (of
smaller size) such that:

$f_{\mathcal{D}}(\vec{x};\vec{y})=f_{\mathcal{D}^{*}}(\vec{x};).$

###### Proof sketch.

The proof is by induction on $\mathcal{D}$, using the fact that
$\mathsf{cond}_{N}$, $\mathsf{cond}_{{\Box N}}$ and $\mathsf{srec}_{{\Box N}}$
have only non-modal succedents. ∎

Our overuse of the notation $\mathsf{B}$ (for a function algebra and for a
type system) is now justified by the following (folklore) result.

######  Proposition 6.

$f\in\mathsf{B}$ iff there is a $\mathsf{B}$-derivation $\mathcal{D}$ for
which $f_{\mathcal{D}}(\vec{x};\vec{y})=f(\vec{x};\vec{y})$.

###### Proof sketch.

The left-right implication is routine and we omit it. For the right-left
implication we proceed by induction on the structure of $\mathcal{D}$. In
particular, notice that the interpretation $f_{\mathcal{D}}$ of a derivation
$\mathcal{D}$ given in 4 almost induces a bona fide interpretation of typing
derivations into the function algebra, but for the case where the last rule of
$\mathcal{D}$ is $\mathsf{cut}_{\Box}$. To handle this we appeal to
Proposition 5, which allows us to infer that, if
$\mathcal{D}_{0}:\Box\Gamma,\vec{N}\Rightarrow{\Box N}$ is the sub-derivation
of the leftmost premise of $\mathsf{cut}_{\Box}$, it can be replaced by the
(smaller) subderivation $\mathcal{D}_{0}^{*}:\Box\Gamma\Rightarrow{\Box N}$
constructed in 5. From here, the interpretation from 4 induces a correct
instance of safe composition along a normal parameter. ∎

######  Convention 7.

Given 6 above, we shall henceforth freely write
$f(\vec{x};\vec{y})\in\mathsf{B}$ if there is a derivation
$\mathcal{D}:\Box\Gamma,\vec{N}\Rightarrow N$ with
$f_{\mathcal{D}}(\vec{x};\vec{y})=f(\vec{x};\vec{y})$.

##  3\. Two-tiered circular systems on notation

In this section we introduce a ‘coinductive’ version of $\mathsf{B}$, and we
study global criteria that tame its computational strength. This proof-
theoretic investigation will lead us to two relevant circular systems:
$\mathsf{C}\mathsf{N}\mathsf{B}$, which morally permits ‘nested’ versions of
safe recursion, and $\mathsf{C}\mathsf{B}$, which will turn out to be closer
to usual safe recursion.

Throughout this section we shall work with the set of typing rules
$\mathsf{B}^{-}:=\mathsf{B}\setminus\mathsf{srec}$.

###  3.1. Non-wellfounded typing derivations

To begin with, we define the notion of ‘coderivation’, which is the
fundamental formal object of this section.

######  Definition 8 (Coderivations).

A ($\mathsf{B}^{-}$-)_coderivation_ is a possibly infinite rooted tree (of
height $\leq\omega$) generated by the rules of $\mathsf{B}^{-}$. Formally, it
is a ternary tree $\mathcal{D}\subseteq\\{0,1,2\\}^{*}$ where each node of
$\mathcal{D}$ is labelled by an inference step from $\mathsf{B}^{-}$ such
that, whenever $\nu\in\mathcal{D}$ is labelled by a step
$S_{1}$$\cdots$$S_{n}$ $S$ , for $n\leq 3$, $\nu$ has $n$ children in
$\mathcal{D}$ labelled by steps with conclusions $S_{1},\dots,S_{n}$
respectively. Sub-coderivations of a coderivation $\mathcal{D}$ rooted at
position $\nu\in\\{0,1,2\\}^{*}$ will be denoted $\mathcal{D}_{\nu}$, so that
$\mathcal{D}_{\epsilon}=\mathcal{D}$. We write $\nu\sqsubseteq\mu$ (resp.
$\nu\sqsubset\mu$) if $\nu$ is a prefix (resp. a strict prefix) of $\mu$, and
in this case we say that $\mu$ is _above_ (resp.  _strictly above_) $\nu$ or
that $\nu$ is _below_ (resp.  _strictly below_) $\mu$. We extend this order
from nodes to sequents in the obvious way.

We say that a coderivation is _regular_ (or _circular_) if it has only
finitely many distinct sub-coderivations.

If we ignore modalities, the rules of $\mathsf{B}^{-}$ can be obtained by
adapting to binary notation the rules of $\mathsf{CT}_{0}$, the type level 0
fragment of $\mathsf{CT}$ from [Das21], which are in turn derivable in the
type level 0 fragment of $\mathsf{C}$ from [KPP21a]. (See 22 for further
discussion on this point.)

Note that, while usual derivations may be naturally written as finite trees or
dags, regular coderivations may be naturally written as finite directed
(possibly cyclic) graphs:

######  Convention 9 (Representing coderivations).

Henceforth, we may mark steps by $\bullet$ (or similar) in a regular
coderivation to indicate roots of identical sub-coderivations. Moreover, to
avoid ambiguities and to ease parsing of (co)derivations, we shall often
underline principal formulas of a rule instance in a given coderivation and
omit instances of $\mathsf{w}_{\Box}$ and $\mathsf{w}_{N}$ as well as certain
structural steps, e.g. during a cut step.

######  Example 10 (Regular coderivations).

The coderivations $\mathcal{I}$, $\mathcal{S}$ and $\mathcal{C}$ below are
regular:

$\scriptstyle\mathsf{id}\;$ $N\Rightarrow N$ $\scriptstyle\mathsf{s}_{1}\;$
$N\Rightarrow N$ $\scriptstyle\Box_{l}\;$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}\Rightarrow N$ $\scriptstyle\Box_{r}\;$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}\Rightarrow{\Box N}$ $\vdots$ $\scriptstyle\mathsf{cut}_{\Box}\;$
$\;\bullet$ ${\Box N}\Rightarrow N$ $\scriptstyle\mathsf{cut}_{\Box}\;$
$\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}\Rightarrow N$ $\scriptstyle 0\;$ $\Rightarrow N$
$\scriptstyle\mathsf{id}\;$ $N\Rightarrow N$ $\scriptstyle\mathsf{s}_{1}\;$
$N\Rightarrow N$ $\scriptstyle\mathsf{cut}_{N}\;$ $\Rightarrow N$
$\scriptstyle\mathsf{id}\;$ $N\Rightarrow N$ $\scriptstyle\mathsf{s}_{1}\;$
$N\Rightarrow N$ $\scriptstyle\Box_{l}\;$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}\Rightarrow N$ $\vdots$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\underline{{\Box
N}}}\Rightarrow N$ $\scriptstyle\mathsf{id}\;$ $N\Rightarrow N$
$\scriptstyle\mathsf{s}_{0}\;$ $N\Rightarrow N$
$\scriptstyle\mathsf{cut}_{N}\;$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}\Rightarrow N$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}\Rightarrow N$ $\scriptstyle\mathsf{id}\;$ $N\Rightarrow N$ $\vdots$
$\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\circ$
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}},N\Rightarrow N$ $\scriptstyle\mathsf{s}_{i}\;$ $\;{\scriptstyle{i=0,1}}$
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}},N\Rightarrow N$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\circ$
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\underline{{\Box
N}}},N\Rightarrow N$ $\vdots$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}},N\Rightarrow N$ $\scriptstyle\mathsf{s}_{i}\;$ $\;{\scriptstyle{i=0,1}}$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}},N\Rightarrow N$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\underline{{\Box
N}}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}},N\Rightarrow N$

As discussed in [Das21], and implicitly stated in [KPP21a], coderivations can
be identified with Kleene-Herbrand-Gödel style equational programs, in general
computing partial recursive functionals (see, e.g., [Kle71, §63] for further
details). We shall specialise this idea to our two-sorted setting.

######  Definition 11 (Semantics of coderivations).

To each $\mathsf{B}^{-}$-coderivation $\mathcal{D}$ we associate a ‘two-
sorted’ Kleene-Herbrand-Gödel partial function $f_{\mathcal{D}}$ obtained by
construing the semantics of 4 as a (possibly infinite) equational program.

Given a two-sorted function $f(\vec{x};\vec{y})$, we say that $f$ is _defined_
by a $\mathsf{B}^{-}$-coderivation $\mathcal{D}$ (or even, is
_$\mathsf{B}^{-}$ -codefinable_) if
$f_{\mathcal{D}}(\vec{x};\vec{y})=f(\vec{x};\vec{y})$.

Note, in particular, that from a regular coderivation $\mathcal{D}$ we obtain
a _finite_ equational program determining $f_{\mathcal{D}}$. Of course, our
overuse of the notation $f_{\mathcal{D}}$ is suggestive since it is consistent
with that of 4.

######  Example 12 (Regular coderivations, revisited).

Let us consider the semantics of the coderivations $\mathcal{I}$,
$\mathcal{S}$ and $\mathcal{C}$ from Example 10.

  * •

The partial functions $f_{\mathcal{I}\nu}$ are given by the following
equational program:

$\begin{array}[]{rcll}f_{\mathcal{I}_{\epsilon}}(x;)&=&f_{\mathcal{I}_{1}}(f_{\mathcal{I}_{0}}(x;);)\\\
f_{\mathcal{I}_{0}}(x;)&=&f_{\mathcal{I}_{00}}(x;)\\\
f_{\mathcal{I}_{00}}(x;)&=&f_{\mathcal{I}_{000}}(;x)\\\
f_{\mathcal{I}_{000}}(;x)&=&\mathsf{s}_{1}(;x)\\\
f_{\mathcal{I}_{1}}(x;)&=&f_{\mathcal{I}_{\epsilon}}(x;)\end{array}$

By purely equational reasoning, we can simplify this program to obtain:

$\begin{array}[]{rcll}f_{\mathcal{I}_{\epsilon}}(x;)&=&f_{\mathcal{I}_{\epsilon}}(\mathsf{s}_{1}x;)\end{array}$

Since the above equational program keeps increasing the input, the function
$f_{\mathcal{I}}=f_{\mathcal{I}_{\epsilon}}$ is always undefined.

  * •

The equational program associated with the coderivation $\mathcal{S}$ is as
follows:

$\begin{array}[]{rcll}f_{\mathcal{S}_{\epsilon}}(0;)&=&f_{\mathcal{S}_{0}}(;)\\\
f_{\mathcal{S}_{\epsilon}}(\mathsf{s}_{0}x;)&=&f_{\mathcal{S}_{1}}(x;)\\\
f_{\mathcal{S}_{\epsilon}}(\mathsf{s}_{1}x;)&=&f_{\mathcal{S}_{2}}(x;)\\\
f_{\mathcal{S}_{0}}(;)&=&\mathsf{s}_{1}0\\\
f_{\mathcal{S}_{1}}(x;)&=&\mathsf{s}_{1}x\\\
f_{\mathcal{S}_{2}}(x;)&=&f_{\mathcal{S}_{21}}(f_{\mathcal{S}_{20}}(x;);)\\\
f_{\mathcal{S}_{20}}(x;)&=&f_{\mathcal{S}_{\epsilon}}(x;)\\\
f_{\mathcal{S}_{21}}(x;)&=&f_{\mathcal{S}_{210}}(;x)\\\
f_{\mathcal{S}_{210}}(;x)&=&\mathsf{s}_{0}(;x)\end{array}$

By equational reasoning again we obtain:

$\begin{array}[]{rcll}f_{\mathcal{S}_{\epsilon}}(0;)&=&\mathsf{s}_{1}0\\\
f_{\mathcal{S}_{\epsilon}}(\mathsf{s}_{0}x;)&=&\mathsf{s}_{1}x&x\neq 0\\\
f_{\mathcal{S}_{\epsilon}}(\mathsf{s}_{1}x;)&=&\mathsf{s}_{0}f_{\mathcal{S}_{\epsilon}}(x;)\end{array}$

Note, therefore, that the function
$f_{\mathcal{S}}=f_{\mathcal{S}_{\epsilon}}$ computes the unary successor
function $x\mapsto x+1$.

  * •

Last, the equational program of $\mathcal{C}$ can be written as:

$\begin{array}[]{rcll}f_{\mathcal{C}_{\epsilon}}(0,0;z)&=&z\\\
f_{\mathcal{C}_{\epsilon}}(0,\mathsf{s}_{i}y;z)&=&\mathsf{s}_{i}f_{\mathcal{C}_{\epsilon}}(x,y;z)&\neq
0\\\
f_{\mathcal{C}_{\epsilon}}(\mathsf{s}_{i}x,y;z)&=&\mathsf{s}_{i}f_{\mathcal{C}_{\epsilon}}(x,y;z)&\neq
0\end{array}$

which computes concatenation of the binary representation of three natural
numbers.

Despite regular coderivations being finitely presentable, they may introduce
functions that are undefined for some arguments, as shown in the above
example. We shall adapt to our setting a well-known ‘termination criterion’
from non-wellfounded proof theory able to identify certain coderivations (even
the non-regular ones) that define total functions. First, let us recall some
standard proof theoretic concepts about (co)derivations, similar to those
occurring in [Das21, KPP21b].

######  Definition 13 (Ancestry).

Fix a coderivation $\mathcal{D}$. We say that a type occurrence $A$ is an
_immediate ancestor_ of a type occurrence $B$ in $\mathcal{D}$ if they are
types in a premiss and conclusion (respectively) of an inference step and, as
typeset in Figure 2, have the same colour. If $A$ and $B$ are in some
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}$
or
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\Gamma^{\prime}}$,
then we furthermore insist that they are in the same position in the list.

Being a binary relation, immediate ancestry forms a directed graph upon which
our correctness criterion is built.

######  Definition 14 (Progressing coderivations).

A _thread_ is a maximal path in the graph of immediate ancestry. We say that a
(infinite) thread is _progressing_ if it is eventually constant ${\Box N}$ and
infinitely often principal for a $\mathsf{cond}_{{\Box N}}$ rule.

A coderivation is _progressing_ if each of its infinite branches is
progressing.

######  Example 15 (Regular coderivations re-revisited).

In Example 10, both $\mathcal{I}$ and $\mathcal{S}$ have precisely one
infinite branch (that loops on $\bullet$). The former is not progressing
because the infinite branch contains no instances of $\mathsf{cond}_{\Box}$ at
all. By contrast, $\mathcal{S}$ is progressing, since the infinite branch has
a progressing thread on the blue formulas
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box N}}$
indicated there. Last, $\mathcal{C}$ has two simple loops, one on $\bullet$
and the other one on $\circ$. For any infinite branch $B$ we have two cases:

  * •

if $B$ crosses the bottommost conditional infinitely many times, it contains a
progressing blue thread;

  * •

otherwise, $B$ crosses the topmost conditional infinitely many times, so that
it contains a progressing red thread.

Therefore, $\mathcal{C}$ is progressing.

As shown in previous works (see e.g. [Das21] and [KPP21a]), the progressing
criterion is sufficient to guarantee that the partial function computed is, in
fact, a well-defined total function:

######  Proposition 16 (Totality).

If $\mathcal{D}$ is progressing then $f_{\mathcal{D}}$ is total.

###### Proof sketch.

We proceed by contradiction. If $f_{\mathcal{D}}$ is non-total then, since
each rule preserves totality, we must have that $f_{\mathcal{D}^{\prime}}$ is
non-total for one of $\mathcal{D}$’s immediate sub-coderivations
$\mathcal{D}^{\prime}$. Continuing this reasoning we can build an infinite
‘non-total’ branch $B=(\mathcal{D}^{i})_{i<\omega}$. Let $({\Box
N}^{i})_{i\geq k}$ be a progressing thread along $B$, and assign to each
${\Box N}^{i}$ the least natural number $n_{i}\in\mathbb{N}$ such that
$f_{\mathcal{D}^{i}}$ is non-total when $n_{i}$ is assigned to the type
occurrence ${\Box N}^{i}$.

Now, notice that:

  * •

$(n_{i})_{i\geq k}$ is monotone non-increasing, by inspection of the rules and
their interpretations from 4.

  * •

$(n_{i})_{i\geq k}$ does not converge, since $({\Box N}^{i})_{i\geq k}$ is
progressing and so is infinitely often principal for $\mathsf{cond}_{\Box}$,
where the value of $n_{i}$ must strictly decrease (cf., again, 4).

This contradicts the well-ordering property of the natural numbers. ∎

One of the most appealing features of the progressing criterion is that, while
being rather expressive and admitting many natural programs, e.g. as we will
see in the next subsections, it remains effective (for regular coderivations)
thanks to well known arguments in automaton theory:

######  Fact 17 (Folklore).

It is decidable whether a regular coderivation is progressing.

This well-known result (see, e.g., [DHL06a] for an exposition for a similar
circular system) follows from the fact that the progressing criterion is
equivalent to the universality of a Büchi automaton of size determined by the
(finite) representation of the input coderivation. This problem is decidable
in polynomial space, though the correctness of this algorithm requires
nontrivial infinitary combinatorics, as formally demonstrated in [KMPS19].

Let us finally observe that the progressiveness condition turns out to be
sufficient to restate 5 in a non-wellfounded setting:

######  Proposition 18.

Given a progressing $\mathsf{B}^{-}$-coderivation
$\mathcal{D}:\Box\Gamma,\vec{N}\Rightarrow{\Box N}$, there is a progressing
$\mathsf{B}^{-}$-coderivation $\mathcal{D}^{*}:\Box\Gamma\Rightarrow{\Box N}$
such that:

$f_{\mathcal{D}}(\vec{x};\vec{y})=f_{\mathcal{D}^{*}}(\vec{x};).$

###### Proof.

By progressiveness, any infinite branch contains a
$\mathsf{cond}_{\Box}$-step, which has non-modal succedent. Since the
conclusion has a modal succedent, by inspection on the rules of
$\mathsf{B}^{-}$ we conclude that each infinite branch contains an instance of
$\Box_{r}$. Hence, the set of the conclusions of such $\Box_{r}$-steps forms a
bar across $\mathcal{D}$. By applying weak König Lemma, the set of all nodes
of $\mathcal{D}$ below this bar, say $X_{\mathcal{D}}$, is finite. The proof
is by induction on the cardinality of $X_{\mathcal{D}}$ and is analogous to 5.
∎

Note that the above proof uniquely depends on progressiveness, and so it holds
for non-regular progressing $\mathsf{B}^{-}$-coderivations as well.

###  3.2. Computational strength of coderivations.

The sequent calculus system $\mathsf{B}$ (Figure 2) is a $S4$-style modal
calculus transplanting Bellantoni and Cook’s function algebra into a proof-
theoretical setting (as in [Hof97]). In particular, $\mathsf{B}$-derivations
locally introduce safe recursion by means of the rule $\mathsf{srec}$, and
Proposition 5 ensures that the composition schemes defined by the cut rules
are safe. A different situation arises when we move from
$\mathsf{B}$-derivations to $\mathsf{B}^{-}$-coderivations: non-
wellfoundedness can actually be used to circumvent the normal/safe distinction
and subsume more complex recursion mechanisms. The following example
illustrates the problem.

######  Example 19 (Non-safety in regular progressing coderivations).

Let $g(\vec{x};\vec{y})$ and $h_{i}(x,\vec{x},z;\vec{y})$ with $i=0,1$ be
functions definable by some (regular and progressing)
$\mathsf{B}^{-}$-coderivations $\mathcal{G}$ and $\mathcal{H}_{i}$,
respectively. Then the following _non-safe_ recursion scheme,

(1) $\begin{array}[]{rcll}f(0,\vec{x};)&=&g(\vec{x};)\\\
f(\mathsf{s}_{i}x,\vec{x};)&=&h_{i}(x,\vec{x},f(x,\vec{x};);)\end{array}$

can be defined by the following (regular and progressing)
$\mathsf{B}^{-}$-coderivation:

$\textstyle{\scriptstyle\mathcal{G}}$ $\Box\vec{N}\Rightarrow N$ $\vdots$
$\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},\Box\vec{N}\Rightarrow{N}$ $\scriptstyle\Box_{r}\;$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},\Box\vec{N}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}}$ $\textstyle{\scriptstyle\mathcal{H}_{i}}$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},\Box\vec{N},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}}\Rightarrow N$ $\scriptstyle\mathsf{cut}_{\Box}\;$
$\;{\scriptstyle{i=0,1}}$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},\Box\vec{N}\Rightarrow N$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
$\underline{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}},\Box\vec{N}\Rightarrow N$

Note in particular that we can use the scheme in Equation 1 to define all
primitive recursive functions.

We can go further and show that, without restrictions on progressing
coderivations, the distinction between modal and non-modal inputs becomes
redundant:

######  Proposition 20.

For any coderivation $\mathcal{D}:{{\Box N}},\overset{n}{\ldots},{{\Box
N}},{N},\overset{m}{\ldots},{N}\Rightarrow N$ of $\mathsf{B}^{-}$ there is a
coderivation $\mathcal{D}^{\Box}:{{\Box N}},\overset{n+m}{\ldots},{{\Box
N}}\Rightarrow N$ such that:

  * •

$f_{\mathcal{D}}(\vec{x};\vec{y})=f_{\mathcal{D}^{\Box}}(\vec{x},\vec{y};)$;

  * •

$\mathcal{D}^{\Box}$ does not contain instances of $\mathsf{w}_{N}$,
$\mathsf{e}_{N}$, $\mathsf{cut}_{N}$, $\mathsf{cond}_{N}$.

Moreover, $\mathcal{D}^{\Box}$ is regular (resp. progressing) if $\mathcal{D}$
is.

###### Proof.

We construct $\mathcal{D}^{\Box}$ coinductively. The only interesting cases
are when $\mathcal{D}$ is $\mathsf{id}$ or it is obtained from
$\mathcal{D}_{0}:\Gamma\Rightarrow N$ and $\mathcal{D}_{1}:\Gamma,N\Rightarrow
A$ by applying a $\mathsf{cut}_{N}$-step. Then, $\mathcal{D}^{\Box}$ is
constructed, respectively, as follows:

${\vbox{\hbox{\kern
3.38339pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
14.40268pt\hbox{\hbox{\hbox{$\ $}}}\kern 14.40268pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to33.80537pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$N\Rightarrow N$}\kern 0.0pt$}}}}}\kern 0.0pt}}\kern
2.50005pt}\kern 1.43518pt\hbox{\kern 6.11101pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\Box_{l}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to38.80547pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern 6.11101pt\hbox{\hbox{$\kern
0.0pt\hbox{${\Box N}\Rightarrow N$}\kern 0.0pt$}}}}}\kern
0.0pt}}}\qquad\qquad{{{{}{}{}}}{{{}{}{}}}\vbox{\hbox{\kern
9.12314pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
10.13791pt\hbox{\vbox{\offinterlineskip\hbox{\kern 2.50005pt\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern 1.8541pt\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\
$}}\kern 10.00002pt}\hbox{\hbox{$\ $}}\kern 10.00002pt}\hbox{\hbox{$\
$}}}}}\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$$}}\vbox{\hbox{$\vbox{\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern 17.50002pt\hbox{\ignorespaces\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{{}{}{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>9.55482pt\hbox{\hbox{\kern
0.0pt\raise-2.42223pt\hbox{$\textstyle{\scriptstyle\mathcal{D}_{0}^{\Box}}$}}}}}}}}}}$}}\hbox
to0.0pt{\hbox{$$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
17.50002pt\hbox{\hbox{$$}}\kern 17.50002pt}}}\kern 0.0pt}}\kern 1.8541pt}\kern
0.0pt\kern 0.0pt\hbox{\hbox to0.0pt{\hss\hbox{$$}}\vbox{}\hbox
to0.0pt{\hbox{$$}\hss}}\hbox{\hbox{\hbox{$\Box\Gamma\Rightarrow N$}}}}}\kern
0.0pt}}\kern 2.50005pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\Box_{r}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to43.70831pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Box\Gamma\Rightarrow{\Box N}$}\kern 0.0pt$}}}}}\kern 0.0pt}\kern
10.00002pt}\hbox{\kern 9.4944pt\hbox{\vbox{\offinterlineskip\hbox{\kern
1.66673pt\hbox{\hbox{\kern 0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
8.08322pt\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\
$}}\kern 10.00002pt}\hbox{\hbox{$\ $}}\kern 10.00002pt}\hbox{\hbox{$\
$}}}}}\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$$}}\vbox{\hbox{$\vbox{\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern 17.50002pt\hbox{\ignorespaces\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{{}{}{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>9.55482pt\hbox{\hbox{\kern
0.0pt\raise-2.42223pt\hbox{$\textstyle{\scriptstyle\mathcal{D}_{1}^{\Box}}$}}}}}}}}}}$}}\hbox
to0.0pt{\hbox{$$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
17.50002pt\hbox{\hbox{$$}}\kern 17.50002pt}}}\kern 0.0pt}}\kern
8.08322pt}\kern 0.0pt\kern 0.0pt\hbox{\hbox to0.0pt{\hss\hbox{$$}}\vbox{}\hbox
to0.0pt{\hbox{$$}\hss}}\hbox{\hbox{\hbox{$\Box\Gamma,N\Rightarrow N$}}}}}\kern
0.0pt}}\kern 1.66673pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\Box_{l}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to54.49995pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Box\Gamma,{\Box N}\Rightarrow N$}\kern 0.0pt$}}}}}\kern
0.0pt}}}}\kern 1.43518pt\hbox{\kern 10.13791pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle\mathsf{cut}_{\Box
N}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to117.70268pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
49.63513pt\hbox{\hbox{$\Box\Gamma\Rightarrow N$}}\kern 39.49722pt}}}\kern
0.0pt}}}\qed$

As we shall see in the next subsections, the above issues can be avoided by
imposing a further global criterion to recover safe recursion in a non-
wellfounded setting. On the other hand, Proposition 20 turns out to be
particularly useful to illustrate how regularity and progressiveness affect
the class of $\mathsf{B}^{-}$-definable functions. Indeed, thanks to the above
proposition, we can recast several of the computational results present in the
(type 0) systems from [Das21, KPP21b]:

######  Proposition 21.

We have the following:

  1. (1)

If $f(\vec{x})$ is primitive recursive then $f(\vec{x};)$ is defined by a
regular and progressing $\mathsf{B}^{-}$-coderivation.

  2. (2)

The class of regular $\mathsf{B}^{-}$-coderivations is Turing-complete, i.e.
they define every partial recursive function.

  3. (3)

Any function $f(\vec{x};)$ is defined by a progressing
$\mathsf{B}^{-}$-coderivation.

Self-contained demonstrations of these points can be found in Section B.1.

In light of the proposition above, it is natural to wonder at this point
precisely what class of functions is defined by the regular progressing
$\mathsf{B}^{-}$-coderivations. Interestingly [KPP21b] show that, in the
absence of contraction rules, _only_ the primitive recursive funtions are so
definable (even at all finite types). It is tempting, therefore, to conjecture
that the regular and progressing $\mathsf{B}^{-}$-coderivations define _just_
the primitive recursive functions.

However there is a crucial difference between our formulation of cut and that
in [KPP21b], namely that ours is context-sharing and theirs is context-
splitting. Thus the former admits a quite controlled form of contraction that,
perhaps surprisingly, is enough to simulate the type 0 fragment
$\mathsf{CT}_{0}$ from [Das21] (which has explicit contraction):

######  Theorem 22.

$f(\vec{x};)$ is defined by a regular progressing
$\mathsf{B}^{-}$-coderivation if and only if $f(\vec{x})$ is type-1-primitive-
recursive, i.e. it is in the fragment $\mathsf{T}_{1}$ of Gödel’s $\mathsf{T}$
with recursion only at type $1$.

The proof of this result is somewhat technical, relying on some results from
[Das21], and is somewhat orthogonal to the focus of this paper, so is devolved
to Section B.2.

Note however that, given the computationally equivalent system
$\mathsf{CT}_{0}$ with contraction from [Das21], we can view the above result
as a sort of ‘contraction admissibility’ for regular progressing
$\mathsf{B}^{-}$-coderivations. Let us take a moment to make this formal.

Call $\mathsf{B}^{-}+\\{\mathsf{c}_{N},\mathsf{c}_{\Box N}\\}$ the extension
of $\mathsf{B}^{-}$ with the rules $\mathsf{c}_{N}$ and $\mathsf{c}_{\Box N}$
below:

(2)
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\Rightarrow
B$ $\scriptstyle\mathsf{c}_{N}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\Rightarrow
B$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}\Rightarrow B$ $\scriptstyle\mathsf{c}_{\Box}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}\Rightarrow B$

where the semantics for the new system extends the one for $\mathsf{B}^{-}$ in
the obvious way, and the notion of (progressing) thread is induced by the
given colouring.222Note that the totality argument of 16 still applies in the
presence of these rules, cf. also [Das21, KPP21b]. We have:

######  Corollary 23.

$f(\vec{x};)$ is definable by a regular progressing
$\mathsf{B}^{-}+\\{\mathsf{c}_{N},\mathsf{c}_{\Box N}\\}$-coderivation iff it
is definable by a regular progressing $\mathsf{B}^{-}$-coderivation.

###### Proof idea.

The former system is equivalent to $\mathsf{CT}_{0}$ from [Das21], whose type
1 functions are just those of $\mathsf{T}_{1}$ by [Das21, Corollary 80], which
are all defined by regular progressing $\mathsf{B}^{-}$-coderivations by 22
above. ∎

######  Remark 24.

The reader may at this point wonder if a direct ‘contraction-admissibility’
argument exists for the rules in (2). First, notice that $\mathsf{c}_{N}$ can
be derived in $\mathsf{B}^{-}$:

$\scriptstyle\mathsf{id}\;$ $N\Rightarrow N$ $\scriptstyle\mathsf{w}_{N}\;$
$\Gamma,N\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}$
$\Gamma,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}\Rightarrow
B$ $\scriptstyle\mathsf{cut}_{N}\;$
$\Gamma,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\Rightarrow
B$

While a similar derivation exists for $\mathsf{c}_{\Box}$, note that this
crucially does not preserve the same notion of thread (cf. colours above) and
so does not, a priori, preserve progressiveness.

###  3.3. Proof-level conditions motivated by implicit complexity

Example 19 from the previous subsection motivates the introduction of a
further criterion on $\mathsf{B}^{-}$-coderivations to rule out recursion
schemes that are ‘not safe’. To this end we propose the following simple
criterion:

######  Definition 25 (Safety).

A $\mathsf{B}^{-}$-coderivation is _safe_ if each infinite branch crosses only
finitely many $\mathsf{cut}_{\Box}$-steps.

######  Example 26.

The coderivation $\mathcal{I}$ in Example 10 is not safe, as there is an
instance of $\mathsf{cut}_{\Box}$ in the loop on $\bullet$, which means that
there is an infinite branch crossing infinitely many
$\mathsf{cut}_{\Box}$-steps. By contrast, using the same reasoning, we can
infer that the coderivations $\mathcal{S}$ and $\mathcal{C}$ are safe.

By inspecting the coderivation of Example 19, we notice that the infinite
branch that loops on $\bullet$ contains infinitely many $\mathsf{cut}_{\Box}$
steps, so that it does not respect the above safety condition. Perhaps
surprisingly, however, the safety condition is not enough to restrict the set
of $\mathsf{B}^{-}$-definable functions to the polytime computable ones, as
the following example shows.

######  Example 27 (Safe exponentiation).

Consider the following coderivation $\mathcal{E}$,

$\scriptstyle\mathsf{id}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}N}\Rightarrow
N$ $\scriptstyle\mathsf{s}_{0}\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}N}\Rightarrow
N$ $\vdots$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}N}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}$
$\vdots$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}\Rightarrow
N$ $\scriptstyle\mathsf{cut}_{N}\;$ $\;\scriptstyle{i=0,1}$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}N}\Rightarrow
N$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}N}\Rightarrow
N$

where we identify the sub-coderivations above the second and the third
premises of the conditional. The coderivation is clearly progressing. Moreover
it is safe, as $\mathcal{E}$ has no instances of $\mathsf{cut}_{\Box}$. Its
associated equational program can be written as follows:

(3) $\begin{array}[]{rcll}f_{\mathcal{E}}(0;y)&=&\mathsf{s}_{0}(;y)\\\
f_{\mathcal{E}}(\mathsf{s}_{0}x;y)&=&f_{\mathcal{E}}(x;f_{\mathcal{E}}(x;y))&x\neq
0\\\
f_{\mathcal{E}}(\mathsf{s}_{1}x;y)&=&f_{\mathcal{E}}(x;f_{\mathcal{E}}(x;y))\end{array}$

The above function $f_{\mathcal{E}}$ has already appeared in [Hof97, Lei99].
It is not hard to show, by induction on $x$, that
$f_{\mathcal{E}}(x;y)=2^{2^{|{x}|}}\cdot|y|$. Thus $f_{\mathcal{E}}$ has
exponential growth rate (as long as $y\neq 0$), despite the program defining a
‘safe’ recursion scheme.

The above coderivation exemplifies a safe recursion scheme that is able to
_nest_ one recursive call inside another in order to obtain exponential growth
rate. This is in fact a peculiar feature of regular proofs, and it is worth
discussing.

As we have already seen, namely in 22, (progressing)
$\mathsf{B}^{-}$-coderivations are able to simulate some sort of higher-order
recursion, namely at type 1 (cf. also [Das21]). In this way it is not
surprising that the sort of ‘nested recursion’ in Equation 3 is definable
since type 1 recursion, in particular, allows such nesting of the recursive
calls. To make this point more apparent, consider the following higher-order
recursion operator:

$\mathsf{rec}_{A}:\Box{N}\rightarrow(\Box{N}\rightarrow A\rightarrow
A)\rightarrow A\rightarrow A$

with $A=N\rightarrow N$, and $f(x)=\mathsf{rec}_{A}(x,h,g)$ is defined as
$f(0)=g$ and $f(\mathsf{s}_{i}x)=h(x,f(x))$ for $x>0$. By setting $g:=\lambda
y:N.\mathsf{s}_{0}y$ and $h:=\lambda x:{\Box N}.\lambda u:N\rightarrow
N.(\lambda y:N.u(u\,y))$ we can easily check that
$f_{\mathcal{E}}(x;y)=\mathsf{rec}_{A}(x,h,g)(y)$, where $\mathcal{E}$ is as
in Example 27. Hence, the function $f_{\mathcal{E}}(x;y)$ can be defined by
means of a higher-order version of safe recursion.

As noticed by Hofmann [Hof97], and formally proved by Leivant [Lei99], thanks
to the capability of nesting recursive calls, higher-order safe recursion can
be used to characterise $\mathbf{F}\mathbf{ELEMENTARY}$. In particular,
Hofmann showed in [Hof97] that by introducing a linearity restriction to the
operator $\mathsf{rec}_{A}$, which prevents duplication of recursive calls, it
is possible to recover the class $\mathbf{F}\mathbf{PTIME}$. The resulting
type system, called $\mathsf{SLR}$ (‘Safe Linear Recursion’), can be then
regarded as a higher-order formulation of $\mathsf{B}$.

Following [Hof97], we shall impose a linearity criterion to rule out those
coderivations that nest recursive calls. This is achieved by observing that
the duplication of the recursive calls of $f_{\mathcal{E}}$ in Example 27 is
due to the presence in $\mathcal{E}$ of loops on $\bullet$ crossing both
premises of a $\mathsf{cut}_{N}$ step. Hence, our circular-proof-theoretic
counterpart of Hofmann’s linearity restriction can be obtained by demanding
that at most one premise of each $\mathsf{cut}_{N}$ step is crossed by such
loops. We shall actually present a slightly more general criterion which does
not depend on our intuitive notion of loop.

######  Definition 28 (Left-leaning).

A $\mathsf{B}^{-}$-coderivation is _left-leaning_ if each infinite branch goes
right at a $\mathsf{cut}_{N}$-step only finitely often.

######  Example 29.

In Example 10, $\mathcal{I}$ is trivially left-leaning, as it contains no
instances of $\mathsf{cut}_{N}$ at all. The coderivations $\mathcal{S}$ and
$\mathcal{C}$ are also left-leaning, since no infinite branch can go right at
the $\mathsf{cut}_{N}$ steps. By contrast, the coderivation $\mathcal{E}$ in
Example 27 is not left-leaning, as there is an infinite branch looping at
$\bullet$ and crossing infinitely many times the rightmost premise of the
$\mathsf{cut}_{N}$-step.

We are now ready to define our circular systems:

######  Definition 30 (Circular Implicit Systems).

We define $\mathsf{C}\mathsf{N}\mathsf{B}$ as the class of safe progressing
regular $\mathsf{B}^{-}$-coderivations. $\mathsf{C}\mathsf{B}$ is the
restriction of $\mathsf{C}\mathsf{N}\mathsf{B}$ to only left-leaning
coderivations. A function $f(\vec{x};\vec{y})$ is
_$\mathsf{C}\mathsf{N}\mathsf{B}$ -definable_ (or _$\mathsf{C}\mathsf{B}$
-definable_) if there is a coderivation
$\mathcal{D}\in\mathsf{C}\mathsf{N}\mathsf{B}$ (resp.,
$\mathcal{D}\in\mathsf{C}\mathsf{B}$) such that
$f_{\mathcal{D}}(\vec{x};\vec{y})=f(\vec{x};\vec{y})$.

Let us point out that Proposition 18 can be stated to preserve safety and
left-leaningness:

######  Proposition 31.

Given $\mathcal{D}:\Box\Gamma,\vec{N}\Rightarrow{\Box N}$ a coderivation in
$\mathsf{C}\mathsf{N}\mathsf{B}$ (or $\mathsf{C}\mathsf{B}$), there exists
$\mathsf{C}\mathsf{N}\mathsf{B}$-coderivation (resp.,
$\mathsf{C}\mathsf{B}$-coderivation)
$\mathcal{D}^{*}:\Box\Gamma\Rightarrow{\Box N}$ such that:

$f_{\mathcal{D}}(\vec{x};\vec{y})=f_{\mathcal{D}^{*}}(\vec{x};)$

###  3.4. On the complexity of proof-checking

Note that both the safety and the left-leaning conditions above are defined at
the level of arbitrary coderivations, not just regular and/or progressing
ones. Moreover, these conditions are easy to check on regular coderivations:

######  Proposition 32.

The safety and the left-leaning condition are $\mathbf{NL}$-decidable for
regular coderivations.

###### Proof.

We can represent a regular coderivation $\mathcal{D}$ as a finite directed
(possibly cyclic) graph $G_{\mathcal{D}}$ labelled with inference rules. Then,
the problem of deciding whether $\mathcal{D}$ is not safe (resp. left leaning)
comes down to the problem of deciding whether a cycle $\pi$ of
$G_{\mathcal{D}}$ exists crossing a node labelled $\mathsf{cut}_{\Box}$ (resp.
crossing the rightmost child of a node labelled $\mathsf{cut}_{N}$). W.l.o.g.
we can assume that $\pi$ is a simple cycle. Given (an encoding of)
$G_{\mathcal{D}}$ as read-only input and (an encoding of) $\pi$ as a read-only
certificate, we can easily construct a deterministic Turing machine $M$
verifying that the cycle $\pi$ crosses $\mathsf{cut}_{\Box}$ (resp. the
rightmost child of a node $\mathsf{cut}_{N}$) in $G_{\mathcal{D}}$. More
specifically:

  * •

the size of the certificate is smaller than the size of the description of
$G_{\mathcal{D}}$;

  * •

$M$ reads once from left to right the addresses of the certificate which
provide the information about where to move the pointers;

  * •

$M$ works in logspace as it only stores addresses in memory. ∎

Recall that progressiveness of regular coderivations is decidable by reduction
to universality of Büchi automata, a $\mathbf{PSPACE}$-complete problem.
Indeed progressiveness itself is $\mathbf{PSPACE}$-complete in many settings,
cf. [NST19]. It is perhaps surprising, therefore, that the safety of a regular
coderivation also allows us to decide progressiveness efficiently too, thanks
to the following reduction:

######  Proposition 33.

A safe $\mathsf{B}^{-}$-coderivation is progressing iff every infinite branch
has infinitely many $\mathsf{cond}_{\Box}$-steps.

###### Proof.

The left-right implication is trivial. For the right-left implication, let us
consider an infinite branch $B$ of a safe $\mathsf{B}^{-}$-coderivation
$\mathcal{D}$. By safety, there exists a node $\nu$ of $B$ such that any
sequent above $\nu$ in $B$ is not the conclusion of a
$\mathsf{cut}_{\Box}$-step. Now, by inspecting the rules of
$\mathsf{B}^{-}\setminus\\{\mathsf{cut}_{\Box}\\}$ we observe that:

  * •

every modal formula occurrence in $B$ has a unique thread along $B$;

  * •

any infinite thread along $B$ cannot start strictly above $\nu$.

Hence, setting $k$ to be the number of ${\Box N}$ occurrences in the
antecedent of $\nu$, $B$ has (at most) $k$ infinite threads. Moreover, since
$B$ contains infinitely many $\mathsf{cond}_{\Box}$-steps, by the Infinite
Pigeonhole Principle we conclude that one of these threads is infinitely often
principal for the $\mathsf{cond}_{\Box}$ rule. ∎

Thus, using similar reasoning to that of 32 we may conclude from 33 the
following:

######  Proposition 34.

Given a regular $\mathsf{B}^{-}$-coderivation $\mathcal{D}$, the problem of
deciding if $\mathcal{D}$ is in $\mathsf{C}\mathsf{N}\mathsf{B}$ (resp.
$\mathsf{C}\mathsf{B}$) is in $\mathbf{NL}$.

Let us point out that the reduction above is similar to and indeed generalises
an analogous one for cut-free coderivations for extensions of Kleene algebra,
cf. [DP18, Proposition 8].

######  Remark 35.

Recall that in Proposition 20 we showed by means of an indirect argument that
explicit contraction is ‘admissible’ for regular progressing
$\mathsf{B}^{-}$-coderivations, and in Remark 24 we pointed out that a more
direct proof of this result cannot easily be found. In fact, we could not
easily find such a direct contraction-admissibility even for
$\mathsf{C}\mathsf{B}$ or $\mathsf{C}\mathsf{N}\mathsf{B}$. However, let us
point out that 33 still holds when explicit contraction is added to
$\mathsf{B}^{-}$. On the one hand, this observation witnesses the robustness
of the safety criterion; on the other hand, it stresses that, whatever class
of functions $\mathsf{C}\mathsf{B}$ and $\mathsf{C}\mathsf{N}\mathsf{B}$
define in the presence explicit contraction, the resulting circular proof
systems are still $\mathbf{NL}$-checkable (cf. 34). A detailed argument for
this can be found in Section B.3.

##  4\. Some variants of safe recursion on notation

In this section we shall introduce various extensions of $\mathsf{B}$ to
classify the expressivity of the circular systems $\mathsf{C}\mathsf{B}$ and
$\mathsf{C}\mathsf{N}\mathsf{B}$. First, starting from the analysis of Example
27 and the subsequent system $\mathsf{C}\mathsf{N}\mathsf{B}$, we shall define
a version of $\mathsf{B}$ with safe _nested_ recursion, called
$\mathsf{N}\mathsf{B}$. Second, motivated by the more liberal way of defining
functions in both $\mathsf{C}\mathsf{B}$ and $\mathsf{C}\mathsf{N}\mathsf{B}$,
we shall endow the function algebras $\mathsf{B}$ and $\mathsf{N}\mathsf{B}$
with forms of safe recursion over a well-founded relation $\subset$ on lists
of normal parameters. Figure 3 summarises the function algebras considered and
their relations.

$\begin{array}[]{|c|c|c|}\hline\cr\text{{safe recursion}}&\text{\footnotesize
on notation}&\text{\footnotesize on $\subset$ }\\\
\hline\cr\text{\footnotesize
unnested}&\qquad\qquad\mathsf{B}&\qquad\qquad\mathsf{B}^{\subset}\\\
\text{\footnotesize unnested, with
compositions}&\mathsf{S}\mathsf{B}&\mathsf{S}\mathsf{B}^{\subset}\\\
\text{\footnotesize
nested}&\mathsf{N}\mathsf{B}&\mathsf{N}\mathsf{B}^{\subset}\\\
\hline\cr\end{array}$
Figure 3. The function algebras considered in Section 4. Any algebra is
included in one below it or to the right of it.

###  4.1. Function algebras with nesting and composition during recursion

One of the key features of safe recursion is that ‘nesting’ of recursive calls
is not permitted. For instance, recalling the coderivation $\mathcal{E}$ from
27, let us revisit the following equational program:

(4) $\begin{array}[]{rcl}\mathsf{ex}(0;y)&=&\mathsf{s}_{0}y\\\
\mathsf{ex}(\mathsf{s}_{i}x;y)&=&\mathsf{ex}(x;\mathsf{ex}(x;y))\end{array}$

Recall that $\mathsf{ex}(x;y)=f_{\mathcal{E}}(x;y)=2^{2^{|{x}|}}\cdot y$. The
‘recursion step’ on the second line is compatible with safe composition, in
that safe inputs only occur in hereditarily safe positions, but one of the
recursive calls takes another recursive call among its safe inputs. In Example
27 we showed how the above function $\mathsf{ex}(x;y)$ can be
$\mathsf{C}\mathsf{N}\mathsf{B}$-defined. It is thus reasonable to look for a
suitable extension of $\mathsf{B}$ able to formalise such nested recursion to
serve as a function algebraic counterpart to $\mathsf{C}\mathsf{N}\mathsf{B}$.

It will be convenient throughout this section to work with generalisations of
$\mathsf{B}$ including _oracles_. Formally speaking, these can be seen as
variables ranging over two-sorted functions, though we shall often identify
them with functions themselves.

######  Definition 36.

For all sets of oracles $\vec{a}=a_{1},\dots,a_{k}$, we define the algebra of
$\mathsf{B}^{-}$ functions _over_ $\vec{a}$ to include all the initial
functions of $\mathsf{B}^{-}$ and,

  * •

(oracles). $a_{i}(\vec{x};\vec{y})$ is a function over $\vec{a}$, for $1\leq
i\leq k$, (where $\vec{x}$,$\vec{y}$ have appropriate length for $a_{i}$).

and closed under:

  * •

(Safe Composition).

    1. (1)

from $g(\vec{x};\vec{y}),h(\vec{x};\vec{y},y)$ over $\vec{a}$ define
$f(\vec{x};\vec{y})$ over $\vec{a}$ by
$f(\vec{x};\vec{y})=h(\vec{x};\vec{y},g(\vec{x};\vec{y}))$.

    2. (2)

from $g(\vec{x};)$ over $\varnothing$ and $h(\vec{x},x;\vec{y})$ over
$\varnothing$ define $f(\vec{x};\vec{y})$ over $\vec{a}$ by
$f(\vec{x};\vec{y})=h(\vec{x},g(\vec{x};);\vec{y})$.

We write $\mathsf{B}^{-}(\vec{a})$ for the class of functions over $\vec{a}$
generated in this way.

Note that Safe Composition along normal parameters (Item 2 above) comes with
the condition that $g(\vec{x};)$ is oracle-free. This restriction prevents
oracles (and hence the recursive calls) appearing in normal position. The same
condition on $h(\vec{x},x;\vec{y})$ being oracle-free is not strictly
necessary for the complexity bounds we are after, as we shall see in the next
section when we define more expressive algebras, but is convenient in order to
facilitate the ‘grand tour’ strategy of this paper (cf. Figure 1).

We shall write, say, $\lambda\vec{v}.f(\vec{x};\vec{v})$ for the function
taking only safe arguments $\vec{v}$ with
$(\lambda\vec{v}.f(\vec{x};\vec{v}))(;\vec{y})=f(\vec{x};\vec{y})$. Nested
recursion can be formalised in the setting of algebras-with-oracles as
follows:

######  Definition 37 (Safe Nested Recursion).

We write $\mathsf{snrec}$ for the scheme:

  * •

from $g(\vec{x};\vec{y})$ over $\varnothing$ and $h(a)(x,\vec{x};\vec{y})$
over $a,\vec{a}$, define $f(x,\vec{x};\vec{y})$ over $\vec{a}$ by:

$\displaystyle f(0,\vec{x};\vec{y})$ $\displaystyle=g(\vec{x};\vec{y})$
$\displaystyle f(\mathsf{s}_{0}x,\vec{x};\vec{y})$
$\displaystyle=h_{0}(\lambda\vec{v}.f(x,\vec{x};\vec{v}))(x,\vec{x};\vec{y})$
$\displaystyle x\neq 0$ $\displaystyle f(\mathsf{s}_{1}x,\vec{x};\vec{y})$
$\displaystyle=h_{1}(\lambda\vec{v}.f(x,\vec{x};\vec{v}))(x,\vec{x};\vec{y})$

We write $\mathsf{N}\mathsf{B}(\vec{a})$ for the class of functions over
$\vec{a}$ generated from $\mathsf{B}^{-}$ under $\mathsf{snrec}$ and Safe
Composition (from 36), and write simply $\mathsf{N}\mathsf{B}$ for
$\mathsf{N}\mathsf{B}(\varnothing)$.

Note that safe nested recursion, per se, admits definitions that are not
morally ‘nested’ but rather use a form of ‘composition during recursion’. Such
a scheme might have the form:

  * •

from
$g(\vec{x};\vec{y}),\vec{g}_{1}(x,\vec{x};\vec{y}),\ldots,\vec{g}_{k}(x,\vec{x};\vec{y})$
and $h_{i}(x,\vec{x};\vec{y},z_{1},\dots,z_{k})$ define:

(5) $\displaystyle f(0,\vec{x};\vec{y})$ $\displaystyle=g(\vec{x};\vec{y})$
$\displaystyle f(\mathsf{s}_{i}x,\vec{x};\vec{y})$
$\displaystyle=h_{i}(x,\vec{x};\vec{y},f(x,\vec{x};\vec{g}_{1}(x,\vec{x};\vec{y})),\dots,f(x,\vec{x};\vec{g}_{k}(x,\vec{x};\vec{y})))$

In this case, note that we have allowed the safe inputs of $f$ to take
arbitrary values given by previously defined functions, but at the same time
$f$ never calls itself in a safe position, as in (4). Note that this safe
recursion scheme does not require the use of oracles in its statement, but is
equivalent to the following one using a notion of ‘nesting’ for Safe
Composition:

######  Definition 38 (Safe Recursion with Composition During Recursion).

An instance of Safe Composition along Safe Parameters (Item 1 from 36) is
called _unnested_ if (at least) one of $g(\vec{x};\vec{y})$ and
$h(\vec{x};\vec{y},y)$ is over $\varnothing$ (i.e. is oracle-free). We define
$\mathsf{S}\mathsf{B}(\vec{a})$ to be the restriction of
$\mathsf{N}\mathsf{B}(\vec{a})$ using only unnested Safe Composition along
Safe Parameters, Item 1 from 36, and write simply $\mathsf{S}\mathsf{B}$ for
$\mathsf{S}\mathsf{B}(\varnothing)$.

It is not hard to show that, indeed, $\mathsf{S}\mathsf{B}$ defines the same
class of functions of the extension of $\mathsf{B}^{-}$ by the scheme given in
eq. 5. On the one hand, given $h_{i}$ and $\vec{g}_{j}$, the scheme in (5) can
be defined in $\mathsf{N}\mathsf{B}(\vec{a})$ using $\mathsf{snrec}$ and only
unnested instances of safe composition. On the other hand, given
$h(a)(x,\vec{x};\vec{y})$ over oracles $a,\vec{a}$, $\mathsf{snrec}$ allows us
to define $f(\mathsf{s}_{i}x,\vec{x};\vec{y})$ by replacing the oracle $a$ in
$h$ with the recursive calls $\lambda\vec{v}.f(x,\vec{x};\vec{v})$. However,
since $h(a)$ is defined using unnested safe composition, no recursive call of
$f$ can be found along the safe parameters of another one.

It should be said that we will not actually use $\mathsf{S}\mathsf{B}$ in this
work, but rather an extension of it defined in the next section, but we have
included it for completeness of our exposition.

###  4.2. Safe recursion on well-founded relations

Function algebras in general may be readily extended by recursion on arbitrary
well-founded relations. For instance, given a well-founded preorder
$\trianglelefteq$, and writing $\vartriangleleft$ for its strict variant,333To
be precise, in this work, for a preorder $\trianglelefteq$ we write
$x\vartriangleleft y$ if $x\trianglelefteq y$ and $y\not\trianglelefteq x$. As
an abuse of terminology, we say that $\trianglelefteq$ is well-founded just
when $\vartriangleleft$ is. ‘safe recursion on $\vartriangleleft$’ is given by
the following scheme:

  * •

from $h(a)(x,\vec{x};\vec{y})$ over $a,\vec{a}$, define $f(x,\vec{x};\vec{y})$
over $\vec{a}$ by:

$f(x,\vec{x};\vec{y})=h(\lambda v\vartriangleleft
x.f(v,\vec{x};\vec{y}))(x,\vec{x};\vec{y})$

Note here that we employ the notation $\lambda v\vartriangleleft x$ for a
‘guarded abstraction’. Formally:

$(\lambda v\vartriangleleft
x.f(v,\vec{x};\vec{y}))(v):=\begin{cases}f(v,\vec{x};\vec{y})&v\vartriangleleft
y\\\ 0&\text{otherwise}\end{cases}$

It is now not hard to see that total functions (with oracles) are closed under
the recursion scheme above, by reduction to induction on the well-founded
relation $\vartriangleleft$.

Note that such schemes can be naturally extended to preorders on _tuples_ of
numbers too, by abstracting several inputs. We shall specialise this idea to a
particular well-founded preorder that will be helpful later to bound the
complexity of definable functions in our systems $\mathsf{C}\mathsf{B}$ and
$\mathsf{C}\mathsf{N}\mathsf{B}$.

Recall that we say that $x$ is a _prefix_ of $y$ if $y$ can be written
$x2^{n}+z$ for some $n\geq 0$ and some $z<2^{n}$, i.e. $y$ has the form $xz$
in binary notation. We say that $x$ is a _strict_ prefix of $y$ if $x$ is a
prefix of $y$ but $x\neq y$.

######  Definition 39 (Permutations of prefixes).

Let $[n]:=\\{0,\dots,n-1\\}$. We shall write
$(x_{0},\dots,x_{n-1})\subseteq(y_{0},\dots,y_{n-1})$ if, for some permutation
$\pi:[n]\to[n]$, we have that $x_{i}$ is a prefix of $y_{\pi i}$, for all
$i<n$. We write $\vec{x}\subset\vec{y}$ if $\vec{x}\subseteq y$ but
$\vec{y}\not\subseteq x$, i.e. there is a permutation $\pi:[n]\to[n]$ with
$x_{i}$ a prefix of $y_{i}$ for each $i<n$, and for some $i<n$ $x_{i}$ is a
strict prefix of $y_{i}$.

It is not hard to see that $\subseteq$ is a well-founded preorder, by
reduction to the fact that the prefix relation is a well-founded partial
order. As a result, we may duly devise a version of safe (nested) recursion on
$\subset$:

######  Definition 40 (Safe (nested) recursion on permutations of prefixes).

We write $\mathsf{N}\mathsf{B}^{\subset}(\vec{a})$ for the class of functions
over $\vec{a}$ generated from $\mathsf{B}^{-}$ under Safe Composition, and the
scheme $\mathsf{snrec}_{\subset}$,

  * •

from $h(a)(\vec{x};\vec{y})$ over $a,\vec{a}$ define $f(\vec{x};\vec{y})$ over
$\vec{a}$ by:

$f(\vec{x};\vec{y})=h(\lambda\vec{u}\subset\vec{x},\lambda\vec{v}.f(\vec{u};\vec{v}))(\vec{x};\vec{y})$

as well as the following generalisation of Safe Composition along a Normal
Parameter:

  * (2)′

from $g(\vec{x};)$ over $\varnothing$ and $h(\vec{x},x;\vec{y})$ over
$\vec{a}$ define $f(\vec{x};\vec{y})$ over $\vec{a}$ by
$f(\vec{x};\vec{y})=h(\vec{x},g(\vec{x};);\vec{y})$.

Recalling 38, we write $\mathsf{S}\mathsf{B}^{\subset}(\vec{a})$ to be the
restriction of $\mathsf{N}\mathsf{B}^{\subset}(\vec{a})$ using only unnested
Safe Composition along Safe Parameters. Finally we define
$\mathsf{B}^{\subset}(\vec{a})$ to be the restriction of
$\mathsf{S}\mathsf{B}^{\subset}(\vec{a})$ where every instance of
$\mathsf{snrec}_{\subset}$ has the form:

  * •

from $h(a)(\vec{x};\vec{y})$ over $a,\vec{a}$, define $f(\vec{x};\vec{y})$
over $\vec{a}$:

$f(\vec{x};\vec{y})=h(\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y}.f(\vec{u};\vec{v}))(\vec{x};\vec{y})$

We call this latter recursion scheme $\mathsf{srec}_{\subset}$, e.g. if we
need to distinguish it from $\mathsf{snrec}_{\subset}$.

Note that the version of safe composition along a normal parameter above
differs from the previous one, Item 2 from 36, since the function $h$ is
allowed to use oracles. This difference is inessential in terms of
computational complexity, as we shall see, but, again, the greater
expressivity of $\mathsf{B}^{\subset}$ and $\mathsf{N}\mathsf{B}^{\subset}$
will facilitate our overall strategy for characterising $\mathsf{C}\mathsf{B}$
and $\mathsf{C}\mathsf{N}\mathsf{B}$, respectively.

Let us take a moment to point out that
$\mathsf{N}\mathsf{B}^{\subset}(\vec{a})\supseteq\mathsf{S}\mathsf{B}^{\subset}(\vec{a})\supseteq\mathsf{B}^{\subset}(\vec{a})$
indeed contain only well-defined total functions over the oracles $\vec{a}$,
by reduction to induction on the well-founded relation $\subset$.

###  4.3. Simultaneous recursion schemes

Finally, let us establish a standard type of result, that the algebras
$\mathsf{B}^{\subset}$, $\mathsf{S}\mathsf{B}^{\subset}$ and
$\mathsf{N}\mathsf{B}^{\subset}$ are closed under simultaneous versions of
their recursion schemes.

######  Definition 41 (Simultaneous schemes).

We define schemes $\mathsf{ssrec}_{\subset}$ and $\mathsf{ssnrec}_{\subset}$,
respectively, as follows, for arbitrary $\vec{a}=a_{1},\dots,a_{k}$:

  * •

from $h_{i}(\vec{a})(\vec{x};\vec{y})$ over $\vec{a},\vec{b}$, for $1\leq
i\leq k$, define $f_{i}(\vec{x};\vec{y})$ over $\vec{b}$, for $1\leq i\leq k$,
by:

$f_{i}(\vec{x};\vec{y})=h_{i}((\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y}.f_{j}(\vec{u};\vec{v}))_{1\leq
j\leq k})(\vec{x};\vec{y})$

  * •

from $h_{i}(\vec{a})(\vec{x};\vec{y})$ over $\vec{a},\vec{b}$, for $1\leq
i\leq k$, define $f_{i}(\vec{x};\vec{y})$ over $\vec{b}$, for $1\leq i\leq k$,
by:

$f_{i}(\vec{x};\vec{y})=h_{i}((\lambda\vec{u}\subset\vec{x},\lambda\vec{v}.f_{j}(\vec{u};\vec{v}))_{1\leq
j\leq k})(\vec{x};\vec{y})$

######  Proposition 42.

We have the following:

  1. (1)

If $\vec{f}(\vec{x};\vec{y})$ over $\vec{b}$ are obtained from
$\vec{h}(\vec{a})(\vec{x};\vec{y})\in\mathsf{B}^{\subset}(\vec{a},\vec{b})$ by
$\mathsf{ssrec}_{\subset}$, then also
$\vec{f}(\vec{x};\vec{y})\in\mathsf{B}^{\subset}(\vec{b})$.

  2. (2)

If $\vec{f}(\vec{x};\vec{y})$ over $\vec{b}$ are obtained from
$\vec{h}(\vec{a})(\vec{x};\vec{y})\in\mathsf{N}\mathsf{B}^{\subset}(\vec{a},\vec{b})$
(or $\in\mathsf{S}\mathsf{B}^{\subset}(\vec{a},\vec{b})$) by
$\mathsf{ssnrec}_{\subset}$, then also
$\vec{f}(\vec{x};\vec{y})\in\mathsf{N}\mathsf{B}^{\subset}(\vec{b})$ (resp.,
$\in\mathsf{S}\mathsf{B}^{\subset}(\vec{b})$).

###### Proof.

We only prove Item 1, i.e. that $\mathsf{B}^{\subset}$ is closed under
$\mathsf{ssrec}_{\subset}$, but the same argument works for Item 2: just
ignore all guards on safe inputs in recursive calls, and our construction
preserves unnestedness of Safe Composition along Safe Parameters.

Let $f_{i}(\vec{x};\vec{y})$ and $h_{i}(a_{1},\dots,a_{k})(\vec{x};\vec{y})$
be as given in 41, and temporarily write $f_{j}^{\vec{x};\vec{y}}$ for
$\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y}.f_{j}(\vec{u};\vec{v})$,
so we have:

$f_{i}(\vec{x};\vec{y})=h_{i}(f_{1}^{\vec{x};\vec{y}},\dots,f_{k}^{\vec{x};\vec{y}})(\vec{x};\vec{y})$

For $i\in\mathbb{N}$, let us temporarily write $\underline{i}$ for $i$ in
binary notation444In fact, any notation will do, but we pick one for
concreteness., and $\vec{i}$ for the list
$\underline{i},\underline{i+1},\dots,\underline{k},\underline{1},\underline{2},\dots,\underline{i-1}$.
Note that, for all $i=1,\dots,k$, $\vec{i}$ is a permutation (in fact a
rotation) of $\underline{1},\dots,\underline{k}$.

Now, let $f(\vec{x};\vec{y},\vec{z})$ over oracles $\vec{b}$ be given as
follows:

(6)
$f(\vec{x};\vec{y},\vec{z}):=\begin{cases}h_{1}(f_{1}^{\vec{x};\vec{y}},\dots,f_{k}^{\vec{x};\vec{y}})(\vec{x};\vec{y})&\vec{z}=\vec{1}\\\
\vdots\\\
h_{k}(f_{1}^{\vec{x};\vec{y}},\dots,f_{k}^{\vec{x};\vec{y}})(\vec{x};\vec{y})&\vec{z}=\vec{k}\\\
0&\text{otherwise}\end{cases}$

Note that this really is a finite case distinction since each of the boundedly
many $\vec{i}$ has bounded size, both bounds depending only on $k$, and so is
computable in $\mathsf{B}^{-}$ over $\vec{h}$.

By definition, then, we have that
$f(\vec{x};\vec{y},\vec{i})=f_{i}(\vec{x};\vec{y})$. Moreover note that, for
each $j=1,\dots,k$, we have,

$\begin{array}[]{rcl}f_{j}^{\vec{x};\vec{y}}(\vec{u}^{\prime};\vec{v}^{\prime})&=&(\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y}.f_{j}(\vec{u};\vec{v}))(\vec{u}^{\prime};\vec{v}^{\prime})\\\
&=&(\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y}.f(\vec{u};\vec{v},\vec{j}))(\vec{u}^{\prime};\vec{v}^{\prime})\\\
&=&(\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y},\lambda\vec{w}\subseteq\vec{z}.f(\vec{u};\vec{v},\vec{w}))(\vec{u}^{\prime};\vec{v}^{\prime},\vec{j})\end{array}$

as long as $\vec{z}$ is some $\vec{i}$, so indeed (6) has the form,

$f(\vec{x};\vec{y},\vec{z})=h(\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y},\lambda\vec{w}\subseteq\vec{z}.f(\vec{u};\vec{v},\vec{w}))(\vec{x};\vec{y})$

and $f(\vec{x};\vec{y},\vec{z})\in\mathsf{B}^{\subset}(\vec{b})$ by
$\mathsf{srec}_{\subset}$. Finally, since
$f_{i}(\vec{x};\vec{y})=f(\vec{x};\vec{y},\vec{i})$, we indeed have that each
$f_{i}(\vec{x};\vec{y})\in\mathsf{B}^{\subset}(\vec{b})$. ∎

##  5\. Characterizations results for function algebras

In this section we characterise the complexities of the function algebras we
introduced in the previous section. On the one hand, despite apparently
extending $\mathsf{B}$, $\mathsf{B}^{\subset}$ still captures the polynomial-
time computable functions. On the other hand, both $\mathsf{N}\mathsf{B}$ and
$\mathsf{N}\mathsf{B}^{\subset}$ are shown to capture the elementary
functions. All such results rely on a ‘bounding lemma’ inspired by [BC92].

###  5.1. Bounding Lemma

Bellantoni and Cook showed in [BC92] that any function
$f(\vec{x};\vec{y})\in\mathsf{B}$ satisfies the ‘poly-max bounding lemma’:
there is a polynomial $p_{f}$ such that:555Recall that, for
$\vec{x}=x_{1},\dots,x_{n}$, we write $|\vec{x}|$ for $|x_{1}|,\dots,|x_{n}|$.

(7) $|f(\vec{x};\vec{y})|\leq p_{f}(|\vec{x}|)+\max|\vec{y}|$

This provided a suitable invariant for eventually proving that all
$\mathsf{B}$-functions were polynomial-time computable.

In this work, inspired by that result, we extend that bounding result to a
form suitable for the algebras from the previous section. To this end we
establish in the next result a sort of ‘elementary-max’ bounding lemma that
accounts for the usual poly-max bounding as a special case, by appealing to
the notion of (un)nested safe composition. What is more, both the statement
and the proof are quite subtle due to our algebras’ formulation using oracles;
we must assume an appropriate bound for the oracles themselves, and the
various (mutual) dependencies in the statement are quite delicate.

For us to state and prove the Bounding Lemma, it will be useful to employ the
notation $||\vec{x}||:=\sum|\vec{x}|$.

######  Lemma 43.

Suppose $f(\vec{x};\vec{y})\in\mathsf{N}\mathsf{B}^{\subset}(\vec{a})$, with
$\vec{a}=a_{1},\dots,a_{k}$. There is an elementary function $e_{f}$ and a
constant $d_{f}\geq 1$ such that if for $1\leq i\leq k$,

(8) $|a_{i}(\vec{x}_{i};\vec{y}_{i})|\leq c_{i}+d_{f}\sum_{j\neq
i}c_{j}+\max|\vec{y}_{i}|$

for some constants $\vec{c}=c_{1},\ldots,c_{k}$, then we have:

(9) $|f(\vec{x};\vec{y})|\leq
e_{f}(||\vec{x}||)+d_{f}\sum\vec{c}+\max|\vec{y}|$

Moreover, if in fact
$f(\vec{x};\vec{y})\in\mathsf{S}\mathsf{B}^{\subset}(\vec{a})$, then $d_{f}=1$
and $e_{f}(n)$ is a polynomial.

Unwinding the statement above, note that $e_{f}$ and $d_{f}$ depend _only_ on
the function $f$ itself, not on the constants $\vec{c}$ given for the (mutual)
oracle bounds in Equation 8. This is crucial and we shall exploit this in the
proof that follows, namely in the case when $f$ is defined by recursion,
substituting different values for $\vec{c}$ during an inductive argument. This
independency of $e_{f}$ and $d_{f}$ from $\vec{c}$ will be made explicit in
their definitions in the proof that follows.

While the role of the elementary bounding function $e_{f}$ is a natural
counterpart of $p_{f}$ in Bellantoni and Cook’s bounding lemma, cf. Equation
7, the role of $d_{f}$ is perhaps slightly less clear. Morally, $d_{f}$
represents the amount of ‘nesting’ in the definition of $f$, increasing
whenever oracle calls are substituted into arguments for other oracles. Hence,
if $f$ uses only unnested Safe Composition, then $d_{f}=1$ as required. In the
argument that follows, it will only be important to distinguish whether
$d_{f}=1$ or not, since $d_{f}$ will form the base of an exponent when
defining $e_{f}$ in the case when $f$ is defined by safe recursion.

Let us also point out that we may relativise the statement of the lemma to any
set of oracles including those which $f(\vec{x};\vec{y})$ is over. In
particular, if $f(\vec{x};\vec{y})$ is over no oracles, then we may realise
Equation 8 vacuously by choosing $\vec{a}=\varnothing$ and we would obtain
that $|f(\vec{x};\vec{y})|\leq e_{f}(||\vec{x}||)+\max|\vec{y}|$. More
interestingly, in the case when $f(\vec{x};\vec{y})$ is just, say,
$a_{i}(\vec{x};\vec{y})$, we may choose to set $\vec{a}=a_{i}$ or
$\vec{a}=a_{1},\dots,a_{n}$ in the above lemma, yielding different bounds in
each case. We shall exploit this in inductive hypotheses in the proof that
follows (typically when we write ‘WLoG’).

###### Proof of 43.

We will proceed by induction on the definition of $f(\vec{x};\vec{y})$, always
assuming that we have $\vec{c}$ satisfying Equation 8.

Throughout the argument we shall actually construct $e_{f}(n)$ that are
_monotone_ elementary functions (without loss of generality) and exploit this
invariant. In fact $e_{f}(n)$ will always be generated by composition from
$0,\mathsf{s},+,\times,x^{y}$ and projections. If
$f(\vec{x};\vec{y})\in\mathsf{S}\mathsf{B}^{\subset}(\vec{a})$ then $e_{f}(n)$
will be in the same algebra without exponentiation, $x^{y}$, i.e. it will be a
polynomial with only non-negative coefficients. This property will be made
clear by the given explicit definitions of $e_{f}(n)$ throughout the argument.

If $f(\vec{x};\vec{y})$ is an initial function then it suffices to set
$e_{f}(n):=1+n$ and $d_{f}:=1$.

If $f(\vec{x};\vec{y})=a_{i}(\vec{x};\vec{y})$ then it suffices to set
$e_{f}(n):=0$ and $d_{f}:=1$.

If $f(\vec{x};\vec{y})=h(\vec{x};\vec{y},g(\vec{x};\vec{y}))$, let
$e_{h},e_{g},d_{h},d_{g}$ be obtained from the inductive hypothesis. We have,

$\begin{array}[]{rcl}|f(\vec{x};\vec{y})|&=&|h(\vec{x};\vec{y},g(\vec{x};\vec{y}))|\\\
&\leq&e_{h}(||\vec{x}||)+d_{h}\sum\vec{c}+\max(|\vec{y}|,|g(\vec{x};\vec{y})|)\\\
&\leq&e_{h}(||\vec{x}||)+d_{h}\sum\vec{c}+e_{g}(||\vec{x}||)+d_{g}\sum\vec{c}+\max|\vec{y}|\end{array}$

so we may set $e_{f}(n):=e_{h}(n)+e_{g}(n)$ and $d_{f}:=d_{h}+d_{g}$.

For the ‘moreover’ clause, note that if $f(\vec{x};\vec{y})$ uses only
unnested Safe Composition, then one of $g$ or $h$ does not have oracles, and
so we can assume WLoG that either the term $d_{h}\sum\vec{c}$ or the term
$d_{g}\sum\vec{c}$ above does not occur above, and we set $d_{f}:=d_{g}$ or
$d_{f}:=d_{h}$, respectively. In either case we obtain $d_{f}=1$ by the
inductive hypothesis, as required.

If $f(\vec{x};\vec{y})=h(\vec{x},g(\vec{x};);\vec{y})$, let
$e_{h},e_{g},d_{h},d_{g}$ be obtained from the inductive hypothesis. Note
that, by definition of Safe Composition along a normal parameter, we must have
that $g$ has no oracles, and so in fact $|g(\vec{x};)|\leq
e_{g}(||\vec{x}||)$. We thus have,

$\begin{array}[]{rcl}|f(\vec{x};\vec{y})|&=&|h(\vec{x},g(\vec{x};);\vec{y})|\\\
&\leq&e_{h}(||\vec{x}||,|g(\vec{x};)|)+d_{h}\sum\vec{c}+\max|\vec{y}|\\\
&\leq&e_{h}(||\vec{x}||,e_{g}(||\vec{x}||))+d_{h}\sum\vec{c}+\max|\vec{y}|\end{array}$

so we may set $e_{f}(n):=e_{h}(n,e_{g}(n))$ and $d_{f}:=d_{h}$. For the
‘moreover’ clause, note that by the inductive hypothesis $e_{h},e_{g}$ are
polynomials and $d_{h}=1$, so indeed $e_{f}$ is a polynomial and $d_{f}=1$.

Finally, if
$f(\vec{x};\vec{y})=h(\lambda\vec{u}\subset\vec{x},\lambda\vec{v}.f(\vec{u};\vec{v}))(\vec{x};\vec{y})$,
let $e_{h},d_{h}$ be obtained from the inductive hypothesis. We claim that it
suffices to set $d_{f}:=d_{h}$ and $e_{f}(n):=nd_{h}^{n}e_{h}(n)$. Note that,
for the ‘moreover’ clause, if $d_{h}=1$ then also $d_{h}^{n}=1$ and so indeed
$e_{f}(n)$ is a polynomial if $d_{h}=1$ and $e_{h}(n)$ is a polynomial.

First, let us calculate the following invariant, for $n>0$:

(10) $\begin{array}[]{rcll}e_{f}(n)&=&nd_{h}^{n}e_{h}(n)&\\\
&=&d_{h}^{n}e_{h}(n)+(n-1)d_{h}^{n}e_{h}(n)&\\\
&=&d_{h}^{n}e_{h}(n)+d_{h}(n-1)d_{h}^{n-1}e_{h}(n)\\\
&\geq&e_{h}(n)+d_{h}(n-1)d_{h}^{n-1}e_{h}(n)&\text{since $d_{h}\geq 1$}\\\
&\geq&e_{h}(n)+d_{h}(n-1)d_{h}^{n-1}e_{h}(n-1)&\text{since $e_{h}$ is
monotone}\\\ &\geq&e_{h}(n)+d_{h}e_{f}(n-1)&\text{by definition of
$e_{f}$}\end{array}$

Now, to show that Equation 9 bounds for the $f,e_{f},d_{f}$ at hand, we
proceed by a sub-induction on $||\vec{x}||$. For the base case, when
$||\vec{x}||=0$ (and so, indeed, $\vec{x}=\vec{0}$), note simply that
$\lambda\vec{u}\subset\vec{x},\lambda\vec{v}.f(\vec{u};\vec{v})$ is the
constant function $0$, and so we may appeal to the main inductive hypothesis
for $h(a)$ setting the corresponding constant $c$ for $a$ to be $0$ to obtain,

$\begin{array}[]{rcl}|f(\vec{0};\vec{y})|&=&|h(0)(\vec{0};\vec{y})|\\\
&\leq&e_{h}(0)+d_{h}\sum\vec{c}+\max|\vec{y}|\\\
&\leq&e_{f}(0)+d_{f}\sum\vec{c}+\max|\vec{y}|\end{array}$

as required. For the sub-inductive step, let $||\vec{x}||>0$. Note that,
whenever $\vec{u}\subset\vec{x}$ we have $||\vec{u}||<||\vec{x}||$ and so, by
the sub-inductive hypothesis and monotonicity of $e_{f}$ we have:

$|f(\vec{u};\vec{v})|\leq e_{f}(||\vec{x}||-1)+d_{f}\sum\vec{c}+\max|\vec{v}|$

Now we may again appeal to the main inductive hypothesis for $h(a)$ by setting
$c=e_{f}(||\vec{x}||-1)$ to be the corresponding constant for
$a=\lambda\vec{u}\subset\vec{x},\lambda\vec{v}.f(\vec{u};\vec{v})$. We thus
obtain:

$\begin{array}[]{rcll}|f(\vec{x};\vec{y})|&=&|h(\lambda\vec{u}\subset\vec{x},\lambda\vec{v}.f(\vec{u};\vec{v}))(\vec{x};\vec{y})|\\\
&\leq&e_{h}(||\vec{x}||)+d_{h}c+d_{h}\sum\vec{c}+\max|\vec{y}|&\text{by main
IH}\\\
&\leq&(e_{h}(||\vec{x}||)+d_{h}e_{f}(||\vec{x}||-1))+d_{h}\sum\vec{c}+\max|\vec{y}|&\text{since
$c=e_{f}(||\vec{x}||-1)$}\\\
&\leq&e_{f}(||\vec{x}||)+d_{h}\sum\vec{c}+\max|\vec{y}|&\text{by
\lx@cref{creftypecap~refnum}{eq:bnd-lem-rec-fn-inv}}\\\
&\leq&e_{f}(||\vec{x}||)+d_{f}\sum\vec{c}+\max|\vec{y}|&\text{since
$d_{f}=d_{h}$}\end{array}$

This completes the proof of the Bounding Lemma. ∎

Before moving on to our soundness results, let us first present an important
consequence of the bounding lemma that will be important for characterising
$\mathsf{N}\mathsf{B}^{\subset}$.

######  Proposition 44.

Let $f(\vec{a})(\vec{x};\vec{y})\in\mathsf{N}\mathsf{B}^{\subset}(\vec{a})$
and let $e_{f}$ and $d_{f}$ be as constructed in the proof of 43 and write:

$m_{f}^{\vec{c}}(\vec{x},\vec{y})\ :=\
e_{f}(||\vec{x}||)+d_{f}\sum\vec{c}+\max|\vec{y}|$

If there are constants $\vec{c}$ such that $\vec{a}$ satisfy Equation 8,
then:666To be clear, here we write $|\vec{y}_{i}|\leq
m_{f}^{\vec{c}}(\vec{x},\vec{y})$ here as an abbreviation for $\\{|y_{ij}\leq
m_{f}^{\vec{c}}(\vec{x},\vec{y})\\}_{j}$.

(11) $f(\vec{a})(\vec{x};\vec{y})\ =\
f(\lambda\vec{x}_{i}.\lambda|\vec{y}_{i}|\leq
m_{f}^{\vec{c}}(\vec{x},\vec{y}).a_{i}(\vec{x}_{i};\vec{y}_{i}))_{i}(\vec{x};\vec{y})$

Note that the point of the above proposition is somewhat dual to that of the
bounding lemma: while the latter bounds the _output_ of a function, the former
bounds the _inputs_. Nonetheless, the argument follows essentially the same
structure as that of the Bounding 43.

###### Proof.

We proceed by induction on the definition of $f(\vec{a})(\vec{x};\vec{y})$,
always making explicit the oracles of a function.

The initial functions and oracle calls are immediate, due to the
‘$\max|\vec{y}|$’ term in Equation 11.

If
$f(\vec{a})(\vec{x};\vec{y})=h(\vec{a})(\vec{x};\vec{y},g(\vec{a})(\vec{x};\vec{y}))$
then, by the inductive hypothesis for $h(\vec{a})$, any oracle call from
$h(\vec{a})$ only take safe inputs of lengths:

$\begin{array}[]{rll}\leq&e_{h}(||\vec{x}||)+d_{h}\sum\vec{c}+\max(|\vec{y}|,|g(\vec{a})(\vec{x};\vec{y})|)\\\
\leq&e_{h}(||\vec{x}||)+d_{h}\sum\vec{c}+e_{g}(||\vec{x}||)+d_{g}\sum\vec{c}+\max|\vec{y}|&\text{by
Bounding \lx@cref{creftypecap~refnum}{lem:boundinglemma}}\\\
\leq&(e_{h}(||\vec{x}||+e_{g}(||\vec{x}||))+(d_{h}+d_{g})\sum\vec{c}+\max|\vec{y}|\\\
\leq&e_{f}(||\vec{x}||)+d_{f}\sum\vec{c}+\max|\vec{y}|\end{array}$

Note that any oracle call from $g(\vec{a})$ will still only take safe inputs
of lengths $\leq e_{g}(||\vec{x}||)+d_{g}\sum\vec{c}+\max|\vec{y}|$, by the
inductive hypothesis, and $e_{g}$ and $d_{g}$ are bounded above by $e_{f}$ and
$d_{f}$ respectively.

If
$f(\vec{a})(\vec{x};\vec{y})=h(\vec{a})(\vec{x},g(\varnothing)(\vec{x};);\vec{y})$
then, by the inductive hypothesis, any oracle call will only take safe inputs
of lengths:

$\begin{array}[]{rll}\leq&e_{h}(||\vec{x}||+|g(\varnothing)(\vec{x};)|)+d_{h}\sum\vec{c}+\max|\vec{y}|\\\
\leq&e_{h}(||\vec{x}||+e_{g}(||\vec{x}||))+d_{h}\sum\vec{c}+\max|\vec{y}|&\text{by
Bounding \lx@cref{creftypecap~refnum}{lem:boundinglemma}}\\\
\leq&e_{f}(||\vec{x}||)+d_{f}\sum\vec{c}+\max|\vec{y}|\end{array}$

Finally suppose
$f(\vec{a})(\vec{x};\vec{y})=h(\vec{a},\lambda\vec{u}\subset\vec{x},\lambda\vec{v}.f(\vec{a})(\vec{u};\vec{v}))(\vec{x};\vec{y})$.
We proceed by a sub-induction on $||\vec{x}||$. Note that, since
$\vec{u}\subset\vec{x}\implies||\vec{u}||<||\vec{x}||$, we immediately inherit
from the inductive hypothesis the appropriate bound on safe inputs for oracle
calls from
$\lambda\vec{u}\subset\vec{x},\lambda\vec{v}.f(\vec{a})(\vec{u};\vec{v})$.

Now, recall from the Bounding 43, whenever $\vec{u}\subset\vec{x}$ (and so
$||\vec{u}||<||\vec{x}||$), we have $|f(\vec{u};\vec{v})|\leq
e_{f}(||\vec{x}||-1)+d_{f}\sum\vec{c}+\max|\vec{v}|$. So by setting
$c=e_{f}(||\vec{x}||-1)$ in the inductive hypothesis for $h(\vec{a},a)$, with
$a=\lambda\vec{u}\subset\vec{x},\lambda\vec{v}.f(\vec{a})(\vec{u};\vec{v})$,
any oracle call from $h(\vec{a},a)$ will only take safe inputs of lengths:

$\begin{array}[]{rll}\leq&e_{h}(||\vec{x}||)+d_{h}e_{f}(||\vec{x}||-1)+d_{h}\sum\vec{c}+\max|\vec{y}|\\\
\leq&e_{f}(||\vec{x}||)+d_{f}\sum\vec{c}+\max|\vec{y}|&\text{by
\lx@cref{creftypecap~refnum}{eq:bnd-lem-rec-fn-inv}}\end{array}$

This completes the proof. ∎

###  5.2. Soundness results

In this subsection we show that the function algebras $\mathsf{B}^{\subset}$
and $\mathsf{N}\mathsf{B}^{\subset}$ (as well as $\mathsf{N}\mathsf{B}$)
capture precisely the classes $\mathbf{F}\mathbf{PTIME}$ and
$\mathbf{F}\mathbf{ELEMENTARY}$, respectively. We start with
$\mathsf{B}^{\subset}$:

######  Theorem 45.

Suppose $\vec{a}$ satisfies Equation 8 for some constants $\vec{c}$. We have
the following:

  1. (1)

if $f(\vec{x};\vec{y})\in\mathsf{B}^{\subset}(\vec{a})$ then
$f(\vec{x},\vec{y})\in\mathbf{F}\mathbf{PTIME}(\vec{a})$.

  2. (2)

if $f(\vec{x};\vec{y})\in\mathsf{N}\mathsf{B}^{\subset}(\vec{a})$ then
$f(\vec{x},\vec{y})\in\mathbf{F}\mathbf{ELEMENTARY}(\vec{a})$.

Before we give the proof note in particular that, for $f(\vec{x};\vec{y})$ in
$\mathsf{B}^{\subset}$ or $\mathsf{N}\mathsf{B}^{\subset}$, i.e. not using any
oracles, we immediately obtain membership in $\mathbf{F}\mathbf{PTIME}$ or
$\mathbf{F}\mathbf{ELEMENTARY}$, respectively. However, the reliance on
intermediate oracles during a function definition causes some difficulties
that we must take into account. At a high level, the idea is to use the
Bounding Lemma, namely its consequence 44, to replace certain oracle calls
with explicit appropriately bounded functions computing their graphs.

###### Proof.

We proceed by induction on the definition of $f(\vec{x};\vec{y})$.

Each initial function is polynomial-time computable, and each (relativised)
complexity class considered is under composition, so it suffices to only
consider the respective recursion schemes. We shall focus first on the case of
$\mathsf{B}^{\subset}(\vec{a})$, Item 1 above, so that $e_{f}$ is a polynomial
and $d_{f}=1$ (since, in particular,
$\mathsf{B}^{\subset}(\vec{a})\subseteq\mathsf{S}\mathsf{B}^{\subset}(\vec{a})$).

Suppose we have $h(a)(\vec{x};\vec{y})\in\mathsf{B}^{\subset}(a,\vec{a})$ and
let:

$f(\vec{x};\vec{y})=h(\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y}.f(\vec{u};\vec{v}))(\vec{x};\vec{y})$

We start by making some observations:

  1. (1)

First, note that $|f(\vec{x};\vec{y})|\leq
e_{f}(|\vec{x}|)+d_{f}\sum\vec{c}+\max|\vec{y}|$, by the Bounding 43, and so
$|f(\vec{x};\vec{y})|$ is polynomial in $|\vec{x},\vec{y}|$.

  2. (2)

Second, note that the set $[\vec{x};\vec{y}]:=\\{(\vec{u},\vec{v})\ |\
\vec{u}\subset\vec{x},\vec{v}\subseteq\vec{y}\\}$ has size polynomial in
$|\vec{x},\vec{y}|$:

     * •

write $\vec{x}=x_{1},\dots,x_{m}$ and $\vec{y}=y_{1},\dots,y_{n}$.

     * •

Each $x_{i}$ and $y_{j}$ have only linearly many prefixes, and so there are at
most
$|x_{1}|\cdot\cdots\cdot|x_{m}||y_{1}|\cdot\cdots\cdot|y_{n}|\leq||\vec{x},\vec{y}||^{m+n}$
many choices of prefixes for all the arguments $\vec{x},\vec{y}$. (This is a
polynomial since $m$ and $n$ are global constants).

     * •

Additionally, there are $m!$ permutations of the arguments $\vec{x}$ and $n!$
permutations of the arguments $\vec{y}$. Again, since $m$ and $n$ are global
constants, we indeed have $|[\vec{x};\vec{y}]|=O(||\vec{x},\vec{y}||^{m+n})$,
which is polynomial in $|\vec{x},\vec{y}|$.

We describe a polynomial-time algorithm for computing $f(\vec{x};\vec{y})$
(over oracles $\vec{a}$) by a sort of ‘course-of-values’ recursion on the
order $\subset\times\subseteq$ on $[\vec{x};\vec{y}]$.

First, for convenience, temporarily extend $\subset\times\subseteq$ to a total
well-order on $[\vec{x};\vec{y}]$, and write $S$ for the associated successor
function. Note that $S$ can be computed in polynomial-time from
$[\vec{x};\vec{y}]$.

Define $F(\vec{x},\vec{y}):=\langle
f(\vec{u};\vec{v})\rangle_{\vec{u}\subset\vec{x},\vec{v}\subseteq\vec{y}}$,
i.e. it is the graph of
$\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y}.f(\vec{u};\vec{v})$
that we shall use as a ‘lookup table’. Note that $|F(\vec{x},\vec{y})|$ is
polynomial in $|\vec{x},\vec{y}|$ by Item 1 and Item 2 above. Now, we can
write:777Here, as abuse of notation, we are now simply identifying
$F(\vec{x};\vec{y})$ with
$\lambda\vec{u}\subset\vec{x},\lambda\vec{v}\subseteq\vec{y}.f(\vec{x};\vec{y})$.

$\begin{array}[]{rcl}F(S(\vec{x},\vec{y}))&=&\langle
f(S(\vec{x},\vec{y})),F(\vec{x},\vec{y})\rangle\\\ &=&\langle
h(F(\vec{x},\vec{y}))(\vec{x};\vec{y}),F(\vec{x},\vec{y})\rangle\end{array}$

Again by Item 2 (and since $F$ is polynomially bounded), this recursion
terminates in polynomial-time. We may now simply calculate
$f(\vec{x};\vec{y})$ as $h(F(\vec{x},\vec{y}))(\vec{x};\vec{y})$.

The argument for $\mathsf{N}\mathsf{B}^{\subset}$ is similar, though we need
not be as careful about computing the size of the lookup tables ($F$ above)
for recursive calls. The key idea is to use the Bounding Lemma, namely its
consequence 44, to bound the safe inputs of recursive calls so that we can
adequately store the lookup table for previous values. ∎

###  5.3. Completeness and characterisations

Note that we have the following as an immediate consequence of the soundness
result, 45 Item 1:

######  Corollary 46.

The following statements are equivalent:

  1. (1)

$f(\vec{x};)\in\mathsf{B}$

  2. (2)

$f(\vec{x};)\in\mathsf{B}^{\subset}$

  3. (3)

$f(\vec{x})\in\mathbf{F}\mathbf{PTIME}$

###### Proof sketch.

$\eqref{item:complfp-bc}\implies\eqref{item:complfp-bcpp}$ is trivial, and
$\eqref{item:complfp-bcpp}\implies\eqref{item:complfp-fp}$ is given by 45.(1).
Finally, $\eqref{item:complfp-fp}\implies\eqref{item:complfp-bc}$ is from
[BC92], stated in 2 earlier. ∎

The remainder of this subsection is devoted to establishing a similar
equivalence for $\mathsf{N}\mathsf{B}$, $\mathsf{N}\mathsf{B}^{\subset}$ and
$\mathbf{F}\mathbf{ELEMENTARY}$. To this end, we naturally require the
following result:

######  Theorem 47.

If $f(\vec{x})\in\mathbf{F}\mathbf{ELEMENTARY}$ then
$f(\vec{x};)\in\mathsf{N}\mathsf{B}$.

The proof can be divided into three steps:

  * •

We define an equivalent formulation of the class
$\mathbf{F}\mathbf{ELEMENTARY}$ for binary notation, having an exponential
growth rate function $\varepsilon^{1}(x)$, whence one may define arbitrary
elementary growth rate by setting
$\varepsilon^{m+1}(x):=\varepsilon^{1}(\varepsilon^{m}(x))$. Now we show that
any function $f(\vec{x})\in\mathbf{F}\mathbf{ELEMENTARY}$ in binary notation
is bounded above by $\varepsilon^{m}(\max(\vec{x}))$ for some $m$.

  * •

We show that for any function $f(\vec{x})\in\mathbf{F}\mathbf{ELEMENTARY}$ in
binary notation there are a function $f^{*}(x;\vec{x})\in\mathsf{N}\mathsf{B}$
and a monotone function888Bear in mind that the function $e_{f}$ here is not
necessarily the same as that of 43 in the previous section.
$e_{f}\in\mathbf{F}\mathbf{ELEMENTARY}$ such that for all integers $\vec{x}$
and all $w\geq e_{f}(\vec{x})$ we have $f^{*}(w;\vec{x})=f(\vec{x})$.

  * •

Now, given the function $\mathsf{ex}(x;y)$ in (4), we construct the function
$\mathsf{ex}^{m}(x;)$ by induction on $m$:

$\displaystyle\mathsf{ex}^{1}(x;)$ $\displaystyle=\mathsf{ex}(x;1)$
$\displaystyle\mathsf{ex}^{m+1}(x;)$
$\displaystyle=\mathsf{ex}^{m}(\mathsf{ex}^{1}(x;);)$

so that, by increasing $m$, $\mathsf{ex}^{m}(x;)$ achieves arbitrary
elementary growth rate, just like $\varepsilon^{m}$. If
$f(\vec{x})\in\mathbf{F}\mathbf{ELEMENTARY}$, by the previous point we obtain
a function $f^{*}(w;\vec{x})\in\mathsf{N}\mathsf{B}$ and a monotone function
$e_{f}\in\mathbf{F}\mathbf{ELEMENTARY}$. By the first point, there exists
$m\geq 1$ such that
$e_{f}(\vec{x})\leq\mathsf{ex}^{m}(\max_{\sharp\vec{x}}(\vec{x};);)$, where
$\max(\vec{x};)$ in $\mathsf{N}\mathsf{B}$. Therefore,
$f(\vec{x};)=f^{*}(\mathsf{ex}^{m}(\max_{\sharp\vec{x}}(\vec{x};););\vec{x})\in\mathsf{N}\mathsf{B}$.

In particular, the first point is folklore, while the proof technique adopted
for proving the last two points is well-known since [BC92], and has been
adapted to the case of the elementary functions by [WW99].

Now, by the same argument as for 46, only using 47 above instead of appealing
to [BC92], we can give our main characterisation result for algebras for
elementary computation:

######  Corollary 48.

The following statement are equivalent:

  1. (1)

$f(\vec{x};)\in\mathsf{N}\mathsf{B}$,

  2. (2)

$f(\vec{x};)\in\mathsf{N}\mathsf{B}^{\subset}$,

  3. (3)

$f(\vec{x})\in\mathbf{F}\mathbf{ELEMENTARY}$.

##  6\. Completeness for circular systems

We now return our attention to the circular systems $\mathsf{C}\mathsf{B}$ and
$\mathsf{C}\mathsf{N}\mathsf{B}$ that we introduced in Section 3. We will
address the complexity of their definable functions by ‘sandwiching’ them
between function algebras of Section 4, given their characterisations in the
previous section.

In particular, in this section we show that $\mathsf{C}\mathsf{B}$ is
‘complete’ for $\mathbf{F}\mathbf{PTIME}$ and that
$\mathsf{C}\mathsf{N}\mathsf{B}$ is complete for
$\mathbf{F}\mathbf{ELEMENTARY}$.

###  6.1. $\mathsf{C}\mathsf{B}$ contains all polynomial-time functions

To show that $\mathsf{C}\mathsf{B}$ contains all polynomial-time functions, we
simulate Bellantoni and Cook’s algebra:

######  Theorem 49.

If $f(\vec{x};\vec{y})\in\mathsf{B}$ then
$f(\vec{x};\vec{y})\in\mathsf{C}\mathsf{B}$.

###### Proof.

By Proposition 6 it suffices to show that for any $\mathsf{B}$-derivation
$\mathcal{D}$ there is a $\mathsf{C}\mathsf{B}$-coderivation $\mathcal{D}^{*}$
such that
$f_{\mathcal{D}}(\vec{x};\vec{y})=f_{\mathcal{D}^{*}}(\vec{x},\vec{y})$. The
proof is by induction on $\mathcal{D}$. The only non-trivial case is when
$\mathcal{D}$ is the following derivation:

$\textstyle{\scriptstyle\mathcal{D}_{0}}$ $\Gamma\Rightarrow N$
$\textstyle{\scriptstyle\mathcal{D}_{1}}$ ${\Box N},\Gamma,N\Rightarrow N$
$\textstyle{\scriptstyle\mathcal{D}_{2}}$ ${\Box N},\Gamma,N\Rightarrow N$
$\scriptstyle\mathsf{srec}_{\Box}\;$ ${\Box N},\Gamma\Rightarrow N$

We define $\mathcal{D}^{*}$ as follows:

$\textstyle{\scriptstyle\mathcal{D}_{0}^{*}}$ $\Box\vec{N},\vec{N}\Rightarrow
N$ $\vdots$ $\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},\Box\vec{N},\vec{N}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}$
$\textstyle{\scriptstyle\mathcal{D}^{*}_{i}}$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},\Box\vec{N},\vec{N},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}\Rightarrow
N$ $\scriptstyle\mathsf{cut}_{N}\;$ $\;{\scriptstyle i=1,2}$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},\Box\vec{N},\vec{N}\Rightarrow N$ $\scriptstyle\mathsf{cond}_{\Box}\;$
$\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\underline{{\Box
N}}},\Box\vec{N},\vec{N}\Rightarrow N$

where we identify the coderivations corresponding to the second and the third
premise of the conditional rule, as they only differ on the sub-coderivation
$\mathcal{D}^{*}_{i}$ ($i=1$ for the former and $i=2$ for the latter). The
above coderivation is clearly safe and left-leaning, by the inductive
hypotheses for $\mathcal{D}_{0},\mathcal{D}_{1},\mathcal{D}_{2}$. To see that
it is progressing, note that any infinite branch is either eventually entirely
in $\mathcal{D}_{0}^{*}$, $\mathcal{D}_{1}^{*}$ or $\mathcal{D}_{2}^{*}$, in
which case it is progressing by the inductive hypotheses, or it simply loops
on $\bullet$ forever, in which case there is a progressing thread along the
blue ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}$.

Moreover, the equational program associated with $\mathcal{D}$ can be is
equivalent to:

$\begin{array}[]{rcll}f_{\mathcal{D}^{*}_{\epsilon}}(0,\vec{x};\vec{y})&:=&f_{\mathcal{D}^{*}_{0}}(\vec{x};\vec{y})\\\
f_{\mathcal{D}^{*}_{\epsilon}}(\mathsf{s}_{0}x,\vec{x};\vec{y})&:=&f_{\mathcal{D}^{*}_{1}}(x,\vec{x};\vec{y},f_{\mathcal{D}^{*}_{\epsilon}}(x,\vec{x};\vec{y}))&\text{if
$x\neq 0$}\\\
f_{\mathcal{D}^{*}_{\epsilon}}(\mathsf{s}_{1}x,\vec{x};\vec{y})&:=&f_{\mathcal{D}^{*}_{2}}(x,\vec{x};\vec{y},f_{\mathcal{D}_{\epsilon}}(x,\vec{x};\vec{y}))\end{array}$

so that
$f_{\mathcal{D}}(\vec{x};\vec{y})=f_{\mathcal{D}^{*}}(\vec{x},\vec{y})$. ∎

###  6.2. $\mathsf{C}\mathsf{N}\mathsf{B}$ contains all elementary functions

Similarly to the case for $\mathsf{C}\mathsf{B}$, to show that
$\mathsf{C}\mathsf{N}\mathsf{B}$ is complete for elementary functions, we
shall simulate our nested algebra $\mathsf{N}\mathsf{B}$. First, we need to
introduce the notion of _oracle_ for $\mathsf{B}^{-}$-coderivations.

######  Definition 50 (Oracles for coderivations).

Let $\vec{a}=a_{1},\ldots,a_{n}$ be a set of safe-normal functions. A
$\mathsf{B}^{-}(\vec{a})$-coderivations is just a usual
$\mathsf{B}^{-}$-coderivation that may use initial sequents of the form
$\scriptstyle a_{i}\;$ ${\Box N}^{n_{i}},N^{m_{i}}\Rightarrow N$ , when
$a_{i}$ takes $n_{i}$ normal and $m_{i}$ safe inputs. We write:

$\scriptstyle a_{i}\;$ $\;i$ ${\Box N}^{n_{i}},N^{m_{i}}\Rightarrow N$
$\textstyle{\scriptstyle\mathcal{D}(\vec{a})}$ $\Gamma\Rightarrow A$

for a coderivation $\mathcal{D}$ with initial sequents among  $\scriptstyle
a_{i}\;$ ${\Box N}^{n_{i}},N^{m_{i}}\Rightarrow N$ , with $i=1,\dots,n$. We
write $\mathsf{C}\mathsf{N}\mathsf{B}(\vec{a})$ for the set of
$\mathsf{C}\mathsf{N}\mathsf{B}$-coderivations with initial functions
$\vec{a}$. We may sometimes omit indicating some oracles $\vec{a}$ if it is
clear from context.

The semantics of such coderivations and the notion of
$\mathsf{C}\mathsf{N}\mathsf{B}(\vec{a})$-definability are as expected, with
coderivations representing functions over the oracles $\vec{a}$, and
$f_{\mathcal{D}(\vec{a})}\in\mathsf{C}\mathsf{N}\mathsf{B}(\vec{a})$ denoting
the induced interpretation of $\mathcal{D}(\vec{a})$.

Before giving our main completeness result for
$\mathsf{C}\mathsf{N}\mathsf{B}$, we need the following lemma allowing us to
‘pass’ parameters to oracle calls. It is similar to the notion
$\mathcal{D}^{\vec{\rho}}$ from [Das21, Lemma 42], only we must give a more
refined argument due to the unavailability of contraction in our system.

######  Lemma 51.

Let $\mathcal{D}(a)$ be a regular coderivation over initial sequents
$\vec{a},a$ with shape:

$\scriptstyle a\;$ $\Delta\Rightarrow N$ $\scriptstyle a_{i}\;$ $\;i$
$\Delta_{i}\Rightarrow N$ $\textstyle{\scriptstyle\mathcal{D}(a)}$ ${\Box
N},\overset{k}{\ldots},{\Box N},\Gamma\Rightarrow N$

where $\Gamma$ and $\Delta$ are lists of non-modal formulas, and the path from
the conclusion to each initial sequent $a$ does not contain
$\mathsf{cut}_{\Box}$-steps, $\Box_{l}$-steps and the leftmost premise of a
$\mathsf{cond}_{\Box}$-step. Then, there exists an $a^{*}$ and a regular
coderivation $\mathcal{D}^{*}(a^{*})$ with shape:

$\scriptstyle a^{*}\;$ ${\Box N},\overset{k}{\ldots},{\Box
N},\Delta\Rightarrow N$ $\scriptstyle a_{i}\;$ $\;i$ $\Delta_{i}\Rightarrow N$
$\textstyle{\scriptstyle\mathcal{D}^{*}(a^{*})}$ ${\Box
N},\overset{k}{\ldots},{\Box N},\Gamma\Rightarrow N$

such that:

  * •

$f_{\mathcal{D}^{*}(a^{*})}(\vec{x};\vec{y})=f_{\mathcal{D}(a(\vec{x}))}(\vec{x};\vec{y})$;

  * •

there exists a ${\Box N}$-thread from the $j$th modal formula in the context
of the conclusion to the $j$th modal formula in the context of any occurrence
of the initial sequent $a^{*}$ in $\mathcal{D}^{*}(a^{*})$, for $1\leq j\leq
k$.

Moreover, if $\mathcal{D}(a)$ is progressing, safe or left-leaning, then
$\mathcal{D}^{*}(a^{*})$ is also progressing, safe or left-leaning,
respectively.

###### Proof sketch.

Let us consider a path $B$ from the root of $\mathcal{D}(a)$ to an occurrence
of the initial sequent $a$. Since the conclusion of $\mathcal{D}(a)$ contains
$k$ modal formulas, and $B$ cannot cross $\mathsf{cut}_{\Box}$-steps, $B$
contains exactly $k$ ${\Box N}$-threads, and all such threads start from the
root. Moreover, since $a$ has only non-modal formulas and $B$ cannot cross
$\Box_{l}$-steps or the leftmost premise of a $\mathsf{cond}_{\Box}$-step, we
conclude that each of the $k$ ${\Box N}$-threads must end in the principal
formula of a $\mathsf{w}_{\Box}$-step. For each $j$ we remove the
corresponding $\mathsf{w}_{\Box}$-step in $B$ we add an extra ${\Box N}$ to
the antecedent of all higher sequents in $B$ (this operation may require us to
introduce weakening steps for other branches of the proof). By repeatedly
applying the above procedure for each possible path from the root of
$\mathcal{D}(a)$ to an initial sequent $a$ we obtain a coderivation with the
desired properties. ∎

Finally we can give our main simulation result for
$\mathsf{C}\mathsf{N}\mathsf{B}$:

######  Theorem 52.

If $f(\vec{x};\vec{y})\in\mathsf{N}\mathsf{B}$ then
$f(\vec{x};\vec{y})\in\mathsf{C}\mathsf{N}\mathsf{B}$.

###### Proof.

We show by induction on $f(\vec{x};\vec{y})\in\mathsf{N}\mathsf{B}(\vec{a})$
that there is a $\mathsf{C}\mathsf{N}\mathsf{B}(\vec{a})$-coderivation
$\mathcal{D}_{f}$ such that:

  1. (1)

$f_{\mathcal{D}_{f}}(\vec{x};\vec{y})=f(\vec{x};\vec{y})$;

  2. (2)

the path from the conclusion of $\mathcal{D}_{f}$ to each initial sequent
$a_{i}$ does not contain $\mathsf{cut}_{\Box}$-steps, $\Box_{l}$-steps and the
leftmost premise of a $\mathsf{cond}_{\Box}$-step.

When $f(\vec{x};\vec{y})$ is an initial function the definition of
$\mathcal{D}^{*}$ is straightforward, as $\vec{a}=\varnothing$. If
$f(\vec{x};\vec{y})=a_{i}(\vec{x};\vec{y})$ then $\mathcal{D}_{f}$ is the
initial sequent  $\scriptstyle a_{i}\;$ $\Box\vec{N},\vec{N}\Rightarrow N$ .

Suppose that $f(\vec{x};\vec{y})=h(\vec{x},g(\vec{x};);\vec{y})$ with
$g(\vec{x};)\in\mathsf{N}\mathsf{B}(\varnothing)$ and
$h(\vec{x},z;\vec{y})\in\mathsf{N}\mathsf{B}(\varnothing)$. Then $f$ can be
$\mathsf{N}\mathsf{B}(\varnothing)$-defined by:

$\ \ \ \varnothing\ \ \ $ $\textstyle{\scriptstyle\mathcal{D}_{g}}$
$\Box\vec{N}\Rightarrow N$ $\scriptstyle\Box_{r}\;$
$\Box\vec{N}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}}$ $\ \ \ \varnothing\ \ \ $ $\textstyle{\scriptstyle\mathcal{D}_{h}}$
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\Box
N}},\Box\vec{N},\vec{N}\Rightarrow N$ $\scriptstyle\mathsf{cut}_{\Box}\;$
$\Box\vec{N},\vec{N}\Rightarrow N$

Suppose $f(\vec{x};\vec{y})=h(\vec{x};\vec{y},g(\vec{x};\vec{y}))$. Then $f$
is $\mathsf{N}\mathsf{B}(\vec{a})$-defined by:

$\scriptstyle a_{i}\;$ $\;i$ $\Box\vec{N},\vec{N}\Rightarrow N$
$\textstyle{\scriptstyle\mathcal{D}_{g}}$
$\Box\vec{N},\vec{N}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}$
$\scriptstyle a_{i}\;$ $\;i$ $\Box\vec{N},\vec{N}\Rightarrow N$
$\textstyle{\scriptstyle\mathcal{D}_{h}}$
$\Box\vec{N},\vec{N},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}N}\Rightarrow
N$ $\scriptstyle\mathsf{cut}_{N}\;$ $\Box\vec{N},\vec{N}\Rightarrow N$

Note that, while we introduce a $\mathsf{cut}_{\Box}$ here, there crucially
remains no $\mathsf{cut}_{\Box}$ between the conclusion and an oracle sequent,
thanks to the condition that $g$ and $h$ are over no oracles.

Finally, suppose that $f(x,\vec{x};\vec{y})$ is obtained from
$g(\vec{x};\vec{y})$ over $\varnothing$, and $h(a)(x,\vec{x};\vec{y})$ over
$a,\vec{a}$ by $\mathsf{snrec}$. Then,
$f(0,\vec{x};\vec{y})=g(\vec{x};\vec{y})$ and
$f(\mathsf{s}_{i}x,\vec{x};\vec{y})=h(\lambda\vec{v}.f(x,\vec{x};\vec{v}))(x,\vec{x};\vec{y})$.
Note that $a$ has same type as $\lambda\vec{v}.f(x,\vec{x};\vec{v})$, so it is
a function taking safe arguments only. Thus by induction hypothesis,
$h(a)(x,\vec{x};\vec{y})$ is $\mathsf{N}\mathsf{B}(\vec{a},a)$-defined by:

$\scriptstyle a\;$ $\vec{N}\Rightarrow N$ $\scriptstyle a_{i}\;$ $\;i$
$\Box\vec{N},\vec{N}\Rightarrow N$
$\textstyle{\scriptstyle\mathcal{D}_{h}(a)}$ ${\Box
N},\Box\vec{N},\vec{N}\Rightarrow N$

where the path from the conclusion of $\mathcal{D}_{h}(a)$ to each initial
sequent $a_{i}$ does not contain $\mathsf{cut}_{\Box}$-steps, $\Box_{l}$-steps
and the leftmost premise of a $\mathsf{cond}_{\Box}$-step. By Lemma 51 we
obtain the following coderivation:

$\scriptstyle a^{*}\;$ ${\Box N},\Box\vec{N},\vec{N}\Rightarrow N$
$\scriptstyle a_{i}\;$ $\;i$ ${\Box N},\Box\vec{N},\vec{N}\Rightarrow N$
$\textstyle{\scriptstyle\mathcal{D}_{h}^{*}(a^{*})}$ ${\Box
N},\Box\vec{N},\vec{N}\Rightarrow N$

where
$f_{\mathcal{D}_{h}^{*}(a^{*})}(x,\vec{x};\vec{y})=f_{\mathcal{D}_{h}(a(x,\vec{x}))}(x,\vec{x};\vec{y})$
and there exists a ${\Box N}$-thread from the $j$-th modal formula in the
antecedent of the conclusion to the $j$-th modal formula in the antecedent of
any $a^{*}$ initial sequent in $\mathcal{D}^{*}(a^{*})$. We define
$\mathcal{D}_{f}$ as follows:

$\scriptsize\ \ \ \varnothing\ \ \ $ $\textstyle{\scriptstyle\mathcal{D}_{g}}$
$\Box\vec{N},\vec{N}\Rightarrow N$ $\vdots$
$\scriptstyle\mathsf{cond}_{\Box}\;$ $\;\bullet$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},\Box\vec{N},\vec{N}\Rightarrow N$ $\scriptstyle a_{i}\;$ $\;i$ ${\Box
N},\Box\vec{N},\vec{N}\Rightarrow N$
$\textstyle{\scriptstyle\mathcal{D}_{h}^{*}{(\mathcal{D}_{f})}}$
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}},\Box\vec{N},\vec{N}\Rightarrow N$ $\scriptstyle\mathsf{cond}_{\Box}\;$
$\;\bullet$
$\underline{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box
N}}},\Box\vec{N},\vec{N}\Rightarrow N$

where we identify the sub-coderivations corresponding to the second and the
third premises of the conditional rule. By construction and induction
hypothesis, the above coderivation is regular and safe. To see that it is
progressing, note that any infinite branch $B$ either hits $\bullet$
infinitely often, in which case there is a progressing thread along the blue
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Box N}}$,
by the properties of $\mathcal{D}_{h}^{*}$ inherited from 51, or $B$ shares a
tail with an infinite branch of $\mathcal{D}_{g}$ or
$\mathcal{D}_{h}^{*}(a^{*})$, which are progressing by the inductive
hypotheses.

We show that $\mathcal{D}_{f}$ $\mathsf{N}\mathsf{B}(\vec{a})$-defines $f$ by
induction on $x$. For the base case,
$f_{\mathcal{D}^{*}_{f}}(0,\vec{x};\vec{y})=f_{\mathcal{D}_{g}}(\vec{x};\vec{y})=g(\vec{x};\vec{y})=f(0,\vec{x};\vec{y})$.
For the inductive step:

$\begin{array}[]{rcl}f_{\mathcal{D}^{*}_{f}}(\mathsf{s}_{i}x,\vec{x};\vec{y})&=&f_{\mathcal{D}^{*}_{h}(\lambda\vec{v}.f_{\mathcal{D}^{*}_{f}}(x,\vec{x};\vec{v}))}(x,\vec{x};\vec{y})\\\
&=&f_{\mathcal{D}^{*}_{h}(\lambda\vec{v}.f(x,\vec{x};\vec{v}))}(x,\vec{x};\vec{y})\\\
&=&f_{\mathcal{D}_{h}(\lambda\vec{v}.f(x,\vec{x};\vec{v}))}(x,\vec{x};\vec{y})\\\
&=&h(\lambda\vec{v}.f(x,\vec{x};\vec{v}))(x,\vec{x};\vec{y})\\\
&=&f(\mathsf{s}_{i}x,\vec{x};\vec{y}).\end{array}$

This completes the proof. ∎

##  7\. Soundness for circular systems

In this section we define a translation of
$\mathsf{C}\mathsf{N}\mathsf{B}$-coderivations into functions of
$\mathsf{N}\mathsf{B}^{\subset}$ which, in particular, maps
$\mathsf{C}\mathsf{B}$-derivations into functions of $\mathsf{B}^{\subset}$,
thus concluding our characterisation of $\mathsf{C}\mathsf{B}$ and
$\mathsf{C}\mathsf{N}\mathsf{B}$ in terms of computational complexity.

###  7.1. The Translation Lemma

A regular coderivation can be naturally seen as a finite tree with
‘backpointers’, a representation known as _cycle normal form_ , cf. [Bro05,
BS11].

######  Definition 53 (Cycle normal form).

Let $\mathcal{D}$ be a regular $\mathsf{B}^{-}$-coderivation. The _cycle
normal form_ (or simply _cycle nf_) of $\mathcal{D}$ is a pair
$\langle\mathcal{D},{R}_{\mathcal{D}}\rangle$, where ${R}_{\mathcal{D}}$ is a
partial self-mapping on the nodes of $\mathcal{D}$ whose domain of definition
is denoted $\mathit{Bud}(\mathcal{D})$ and:

  1. (i)

every infinite branch of $\mathcal{D}$ contains some (unique)
$\nu\in\mathit{Bud}(\mathcal{D})$;

  2. (ii)

if $\nu\in\mathit{Bud}(\mathcal{D})$ then both
${R}_{\mathcal{D}}(\nu)\sqsubset\nu$ and
$\mathcal{D}_{{R}_{\mathcal{D}}(\nu)}=\mathcal{D}_{\nu}$;

  3. (iii)

for any two distinct nodes $\mu\sqsubset\nu$ strictly below
$\mathit{Bud}(\mathcal{D})$, $\mathcal{D}_{\mu}\neq\mathcal{D}_{\nu}$

We call any $\nu\in\mathit{Bud}(\mathcal{D})$ a _bud_ , and
${R}_{\mathcal{D}}(\nu)$ its _companion_. A _terminal_ node is either a leaf
of $\mathcal{D}$ or a bud. The set of nodes of $\mathcal{D}$ bounded above by
a terminal node is denoted $T_{\mathcal{D}}$. Given a node $\nu\in
T_{\mathcal{D}}$, we define $\mathit{Bud}_{\nu}(\mathcal{D})$ as the
restriction of buds to those above $\nu$.

######  Remark 54.

The cycle normal form of a regular coderivation $\mathcal{D}$ always exists,
as by definition any infinite branch contains a node $\nu$ such that
$\mathcal{D}_{\nu}=\mathcal{D}_{\mu}$ for some node $\mu$ below $\nu$.
$\mathit{Bud}(\mathcal{D})$ is designed to consist of just the _least_ such
nodes, so that by construction the cycle normal form is unique. Note that
$\mathit{Bud}(\mathcal{D})$ must form an antichain: if
$\mu,\nu\in\mathit{Bud}(\mathcal{D})$ with $\mu\sqsubset\nu$, then
${R}_{\mathcal{D}}(\mu)\sqsubset\mu$ are below $\mathit{Bud}(\mathcal{D})$ but
we have $\mathcal{D}_{{R}_{\mathcal{D}}(\mu)}=\mathcal{D}_{\mu}$ by (ii)
above, contradicting the (iii).

Also, notice that any branch of $\mathcal{D}$ contains a leaf of
$T_{\mathcal{D}}$. Moreover, since $\mathit{Bud}(\mathcal{D})$ is an
antichain, the leaves of $T_{\mathcal{D}}$ defines a ‘bar’ across
$\mathcal{D}$, and so $T_{\mathcal{D}}$ is a finite tree.

The following proposition allows us to reformulate progressiveness, safety and
left-leaning conditions for cycle normal forms.

######  Proposition 55.

Let $\mathcal{D}$ be a regular $\mathsf{B}^{-}$-coderivation with cycle nf
$\langle\mathcal{D},{R}_{\mathcal{D}}\rangle$. For any
$\nu\in\mathit{Bud}(\mathcal{D})$, the (finite) path $\pi$ from
${R}_{\mathcal{D}}(\nu)$ to $\nu$ satisfies:

  1. (1)

if $\mathcal{D}$ is progressing, $\pi$ must contain the conclusion of an
instance of $\mathsf{cond}_{{\Box N}}$;

  2. (2)

if $\mathcal{D}$ is a $\mathsf{C}\mathsf{N}\mathsf{B}$-coderivation, $\pi$
cannot contain the conclusion of $\mathsf{cut}_{{\Box N}}$, $\Box_{l}$,
$\mathsf{w}_{\Box}$, and the leftmost premise of $\mathsf{cond}_{\Box}$;

  3. (3)

if $\mathcal{D}$ is a $\mathsf{C}\mathsf{B}$-coderivation, $\pi$ cannot
contain the conclusion of $\mathsf{w}_{N}$, the leftmost premise of
$\mathsf{cond}_{N}$, and the rightmost premise of $\mathsf{cut}_{N}$.

In what follows we shall indicate circularities in cycle nfs explicitly by
extending both $\mathsf{C}\mathsf{N}\mathsf{B}$ and $\mathsf{C}\mathsf{B}$
with a new inference rule called $\mathsf{dis}$:

$\Gamma\Rightarrow A$ $\scriptstyle\mathsf{dis}\;$ $\;X$ $\Gamma\Rightarrow A$

where $X$ is a finite set of nodes. In this presentation, we insist that each
companion $\nu$ of the cycle nf $\langle\mathcal{D},{R}_{\mathcal{D}}\rangle$
is always the conclusion of an instance of $\mathsf{dis}$, where $X$ denotes
the set of buds $\nu^{\prime}$ such that