We introduce a new bounded theory $\RS$,
and show that the functions which
are $\Sigma^b_1$-representable in it are precisely
random functions which can be computed
in polynomial time.

Concretely, we pass through the class of oracle functions
over strings $\POR$,
which is introduced in Section <ref>,
together with $\RS$.

Then, we show that functions computed by poly-time PTMs
are arithmetically characterized by a class of
probabilistic bounded formulas:

in Section <ref>,
we prove that the class of poly-time oracle functions
is equivalent to that of functions which are $\Sigma^b_1$-representable
in $\RS$, and

in Section <ref> we establish the converse.

§ OVERVIEW

Usual characterizations of poly-time (deterministic)
functions in bounded arithmetic are obtained by two “macro”
results [1, 7].

Some Cobham-style algebra for poly-time functions is
introduced and shown equivalent to (1) that
of functions computed by TMs running in polynomial time,
and (2) that of functions which are $\Sigma^b_1$-representable
in the proper bounded theory.

The global structure of our proof follows a similar path,
with an algebra of oracle recursive function,
called $\POR$, playing the role of our Cobham-style
function algebra.

In our case, functions are poly-time computable by PTMs
and the theory is randomized $\RS$.

After introducing these classes, we show

that the random functions which are
$\Sigma^b_1$-representable in $\RS$ are precisely those in
$\POR$, and

that $\POR$ is equivalent
(in a very specific sense)
to the class of functions computed by PTMs running
in polynomial time.

While the first part is established due to standard
arguments [7, 3],
the presence of randomness introduced a
delicate ingredient to be dealt with in the second part.

Indeed, functions in $\POR$ access randomness
in a rather different way
with respect to PTMs, and relating these
models requires some effort,
that involves long chains of
intermediate simulations.

[node distance=2cm]
at (0,2) (a) $\POR$;
at (-1.6,0.7) (b) $\RS$;
at (1.6,0.7) (c) $\RFP$;

[<->,thick] (a) to [bend right=20] (b);
[<->,thick] (b) to [bend right=20] (c);
[<->,thick] (c) to [bend right=20] (a);

Proof Schema

we start by defining the class of oracle functions over strings,
the new theory $\RS$, strongly inspired
by [8], but over a “probabilistic word language”,
and considering a slightly modified notion of
fitting the domain of our peculiar oracle functions.

Then, we prove that the class of
random functions computable in polynomial time, called $\RFP$,
is precisely the class of
functions which are $\Sigma^b_1$-representable in $\RS$
in three steps:

* We prove that functions in $\POR$ are $\Sigma^b_1$-representable
in $\RS$ by induction on the structure of oracle functions
(and relying on the encoding machinery presented
in [1, 7]).

* We show that all functions which are $\Sigma^b_1$-representable
in $\RS$ are in $\POR$ by realizability techniques
similar to Cook and Urquhart's one [3].

* We generalize Cobham's result to  probabilistic
showing that functions in $\POR$
are precisely those in $\RFP$.

[node distance=2cm]
at (-4,0) (a) $\RS$;
at (0,0) (b) $\POR$;
at (4,0) (c) $\RFP$;
at (-2,1) realizability [3];
at (-2,-1) induction [6];
at (2,0.3) series of simulations;

[->,thick,dotted] (a) to [bend right=30] (b);
[->,thick,dotted] (b) to [bend right=30] (a);
[<->,thick,dotted] (c) to (b);

Our Proof in a Nutshell

§ INTRODUCING $\POR$ AND $\RS$

In this section, we introduce
a Cobham-style function algebra for poly-time oracle
recursive functions $\POR$,
and a randomized bounded arithmetic $\RS$.

As Ferreira's ones [6, 7],
these classes are both associated with binary strings
rather than natural positive integer:
$\POR$ is a class of oracle functions over sequences of bits,
while $\RS$ is defined in a probabilistic word language $\rl$.

Strings support a natural notion of term-size
and make it easier to deal with bounds and time-complexity.

Observe that working with strings is not crucial
and all results below could be spelled out in terms of natural

Indeed, theories have been introduced
in both formulations – Ferreira's $\Sigma^b_1$-NIA
and Buss' $\BussS$ – and proved equivalent [8].

§.§ The Function Algebra $\POR$

We introduce a function algebra for
poly-time oracle recursive functions inspired by Ferreira's
$\PTCA$ [6, 7],
and defined over strings.

Let $\Bool=\{\zero,\one\}$,
$\Ss=\Bool^*$ be the set of binary strings
of finite length, and $\Os=\Bool^\Ss$ be the set of binary
strings of infinite length.

Metavariables $\eta',\eta'',\dots$ are used to
denote the elements of $\Os$.

Let $|\cdot |$ denote the length-map string, so that for any
string $x$, $|x|$ indicates the length of $x$.

Given two binary strings $x,y$ we use $x\ssubseteq y$
to express that $x$ is an initial
or prefix substring of $y$,
$x\cconc y$ (abbreviated as $xy$) for concatenation,
and $x\ttimes y$ obtained by self-concatenating
$x$ for $|y|$-times.

Given an infinite string of bits $\eta$,
and a finite string $x$, $\eta(x)$ denotes
one specific bit of $\eta$,
the so-called $x$-th bit of $x$.

A fundamental difference between oracle functions
and those of $\PTCA$ is that the latter ones are
of the form $f:\Ss^k \times \Os \to \Ss$,
carrying an additional argument
to be interpreted as the underlying source of random bits.

Furthermore, $\PR$ includes the basic function query,
$\queryS(x,\eta)=\eta(x)$, which can be used to
observe any bit in $\eta$.

The class $\POR$ is the smallest class
of functions $f:\Ss^k \times \Os\to \Ss$,

* The empty (string) function $\emptyS(x,\eta)=\eepsilon$

* The projection (string) functions $\projS^{n}_i(x_1,\dots, x_n,\eta) =x_i$,
for $n\in\Nat$ and $1\leq i\leq n$

* The word-successor $\successorS_{b}(x,\eta)=x\bool$,
where $b=0$ if $\bool=\one$ and $b=1$ if $\bool=\one$

* The conditional (string) function

\begin{align*}
\condS(\eepsilon, y, z_0, z_1, \eta) &= y \\
\condS(x\bool, y, z_0, z_1, \eta) &= z_{b},
\end{align*}

where $b=0$ if $\bool = \zero$ and $b=1$ if $\bool=\one$

* The query (string) function $\queryS(x,\eta) = \eta(x)$

and closed under the following schemas:

* Composition, where $f$ is defined from
$g,h_1,\dots, h_k$ as

f(\vec{x},\eta) = g(h_1(\vec{x},\eta), \dots, h_k(\vec{x},\eta),
\eta)

* Bounded recursion on notation, where $f$
is defined from $g,h_0,$ and $h_1$ as

\begin{align*}
f(\vec{x},\eepsilon,\eta) &= g(\vec{x},\eta) \\
f(\vec{x}, y\zero, \eta) &= h_0(\vec{x}, y, f(\vec{x}, y, \eta),
\eta) |_{t(\vec{x},y)} \\
f(\vec{x}, y\one, \eta) &=
h_1(\vec{x}, y, f(\vec{x},y,\eta), \eta)|_{t(\vec{x},y)}
\end{align*}

and $t$ is obtained from $\eepsilon, \one, \zero, \cconc,$
and $\ttimes$ by explicit definition,
that is $t$ can be obtained applying $\cconc$ and $\ttimes$
on the constants $\eepsilon, \zero,\one$, and
the variables $\vec{x}$ and $y$.[Notice that there is a
clear correspondence with the grammar for terms in $\rl$, Definition <ref>.]

Actually, the conditional function $\condS$
could be defined by bounded recursion.

As follows

\begin{align*}
\condS(\eepsilon, y, z_0, z_1,\eta) = y \\
\condS(x\zero, y, z_0,z_1,\eta) = \projS_3(x\zero,y,z_0,z_1,
f(x\zero,y,z_0,z_1,\eta),\eta)|_{\zero} \\
\condS(x\one, y, z_0,z_1,\eta) = \projS_4(x\one,y,z_0,z_1,\eta)|_{\zero}.
\end{align*}

We take it as a primitive function of $\POR$
to help making the realizability of Section <ref>

Neither the query function or the conditional function
appear in Ferreira's characterization [7],
which instead contains the “substring-conditional”

\successorS(x,y,\eta) = \begin{cases}
\one \ \ &\text{if } x \ssubseteq y \\
\zero \ \ &\text{otherwise,}
\end{cases}

which can be defined in $\POR$ by bounded recursion.

First, let $\tailF (x,\eta)$ be defined as follows:

\begin{align*}
\tailF (\eepsilon,\eta) &= \eepsilon \\
\tailF (x\bool,\eta) &= x.
\end{align*}

Then, let $\prF(x,\eta)$ be:

\textcolor{red}{\cdots}

and $\eqF(x,y,\eta)$ be:

\begin{align*}
\eqF(x,\eepsilon,\eta) &=
\condS(x,\one,\eepsilon,\eepsilon,\eta) \\
\eqF(x,y\zero,\eta) &=
\condS(x,\eepsilon,\eqF(\prF(x), y,\eta), \eepsilon, \eta) \\
\eqF(x,y\one,\eta) &=
\condS(x,\eepsilon,\eepsilon, \eqF(\prF(x),y,\eta),\eta).
\end{align*}

Finally, we can define $\successorS(x,y,\eta)$ as:

\begin{align*}
\successorS(x,\eepsilon,\eta) &= \condS(x,\one,\zero,\zero,\eta) \\
\successorS(x,y\zero,\eta) &=
\condS(x,\one, \condS(\eqF(x,y\zero,\eta),
\successorS(x,y\zero,\eta), \one,\one,\eta),
\successorS(x,y,\eta),\eta) \\
\successorS(x,y\one,\eta) &=
\condS(x,\one,\successorS(x,y,\eta), \condS(\eqF(x,y\one,\eta),
\successorS(x,y,\eta), \one,\one,\eta)), \eta).
\end{align*}

§.§ Randomized Bounded Arithmetics

First, we introduce a probabilistic word language for our bounded arithmetic,
together with its quantitative interpretation.

The Language $\rl$.
Following [8],
we consider a first-order signature for natural numbers
in binary notation endowed with a special predicate symbol

Consequently, formulas are interpreted over $\Ss$ rather
than $\Nat$.

Terms and formulas of $\rl$ are defined by the grammar below:

\begin{align*}
t &\df x \midd \epsilon \midd \zzero \midd \oone \midd t\conc t \midd
t \times t \\
F &\df \Flip(t) \midd t=s \midd \neg F \midd
F \wedge F \midd F \vee F \midd (\exists x)F \midd
(\forall x)F.
\end{align*}

For readability, we adopt the following abbreviations:
$ts$ for $t\conc s$,
$\oone^t$ for $\oone \times t$,
and $t\preceq s$ for $\oone^t \subseteq \oone^s$,
expressing that the length of $t$ is smaller than that of $s$.

Given three terms $t,r,$ and $s$, the abbreviation
$t|_r = s$ denotes the following formula,

(\oone^r \subseteq \oone^t \wedge s \subseteq t \wedge
\oone^r = \oone^s) \vee
(\oone^t \subseteq \oone^r \wedge s=t),

saying that $s$ is the truncation of $t$
at the length of $r$.

Every string $\str\in \Ss$ can be seen as a term of $\rl$
$\overline{\str}$, such that
$\overline{\str\bool} = \overline{\str}\bbool$,
where $\bool\in\Bool$ and $\bbool\in\{\zzero,\oone\}$,
e.g. $\overline{\zero\zero\one} = \zzero\zzero\oone$.

A central feature of bounded arithmetic is the presence of
bounded quantification.

[Bounded Quantifiers]
In $\rl$, bounded quantified expressions
are expressions of either the form
$(\forall x)(\oone^x \subseteq \oone^t \rightarrow \fone)$ or
$(\exists x)(\oone^x \subseteq \oone^t \wedge \fone)$,
usually abbreviated as $(\forall x\preceq t)\fone$ and
$(\exists x \preceq t)\fone$ respectively.

We call subword quantifications,
quantifications of the form
$(\forall x\subseteq^* t)\fone$ and
$(\exists x\subseteq^* t)\fone$,
$(\forall x)\big((\exists w \subseteq t)(wx\subseteq t)
\rightarrow \fone\big)$
$(\exists x)(\exists w\subseteq t)
(wx \subseteq t \wedge \fone)$.
we abbreviate so-called initial subword
$(\forall x)(x\subseteq t \rightarrow \fone)$
as $(\forall x\subseteq t)\fone$
$(\exists x)(x\subseteq t \wedge \fone)$
as $(\exists x\subseteq t)\fone$.

The distinction between bounded and subword
quantification is important for complexity reasons.
If $\str \in \Ss$ is a string of length $k$,
the witness of a subword existentially quantified
$(\exists x \subseteq^* \overline{\str})\fone$
is to be looked for among all possible sub-strings of $\str$,
that is within a space of size $\mathcal{O}(k)$.
On the contrary, the witness of a bounded formula
$(\exists x\preceq \overline{\str})\fone$
is to be looked for among all possible strings of
length $k$, namely within a space of size $\mathcal{O}(2^k)$.

In order to avoid misunderstanding let us briefly sum up
the different notions and symbols used for subword relations.

We uses $\ssubseteq$ to express a relation between strings,
that is $x\ssubseteq y$ expresses that $x$ is an initial or prefix substring of $y$.
We use $\subseteq$ as a relation symbol in the language $\rl$.

We use $\preceq$ as an auxiliary symbol in the language $\rl$;
in particular, as seen, $t\preceq s$ is syntactic sugar for $\oone^t\subseteq \oone^s$.

We use $\subseteq^*$ as an auxiliary symbol in the language $\rl$
to denote subword quantification.

We also use $(\exists w\subseteq t)\fone$ as an abbreviation of
$(\exists w)(w\subseteq t\wedge \fone)$
and similarly for $(\forall w\subseteq t)$.

A $\Sigma^b_0$-formula is a subword quantified
i.e. a formula belonging to the smallest class
of $\rl$ containing atomic
formulas and closed under Boolean operations
and subword quantification.

A formula is said to be a
$\Sigma^b_1$-formula, if it is of the form
$(\exists x_1\preceq t)\dots(\exists x_n\preceq t_n)
\fone$,
where the only quantifications in $\fone$ are
subword ones.

We call $\Sigma^b_1$ the class containing
all and only the $\Sigma^b_1$-formulas.

An extended $\Sigma^b_1$-formula
is any formula of $\rl$ that can be constructed
in a finite number of steps, starting with
subword quantifications and bounded existential
quantifications and bounded existential quantifications.

The Bounded Theory $\RS$.
We introduce the bounded theory $\RS$,
which can be seen as a
probabilistic version to Ferreira's
$\Sigma^b_1$-NIA [6].

It is expressed in the language $\rl$.

The theory $\RS$ is defined by axioms
belonging to two classes:

* Basic axioms:

* $x\epsilon=x$

* $x(y\bbool) = (xy)\bbool$

* $x\times \epsilon=\epsilon$

* $x\times x\bbool = (x\times y)x$

* $x\subseteq \epsilon \leftrightarrow x=\epsilon$

* $x\subseteq y\bbool \leftrightarrow
x\subseteq y \vee x=y\bbool$

* $x\bbool = y\bbool \rightarrow x=y$

* $x\zzero \neq y\oone$,

* $x\bbool\neq \epsilon$

with $\bbool\in \{\zzero,\oone\}$

* Axiom schema for induction on notation,

B(\epsilon) \wedge (\forall x)\big(B(x) \rightarrow
B(x\zzero) \wedge B(x\oone)\big)
\rightarrow (\forall x)B(x),

where $B$ is a $\Sigma^b_1$-formula in $\rl$.

Induction on notation
adapts the usual induction schema of $\PA$
to the binary representation.

Of course, as in Buss' and Ferreira's approach,
the restriction of this schema to $\Sigma^b_1$-formulas
is essential
to characterize algorithms computed with bounded resources.

Indeed, more general instances of the schema
would extend representability to random functions which
are not poly-time (probabilistic) computable.

In $\RS$ any extended $\Sigma^b_1$-formula
is logically equivalent to a
$\Sigma^b_1$-formula.[Actually, Ferreira
proved this result for the theory $\Sigma^b_1$-NIA <cit.>,
but it clearly holds for $\rl$ as well.]

Semantics for Formulas in $\rl$.
We introduce a quantitative semantics for
formulas of $\rl$,
which is strongly inspired by that for $\MQPA$.

In particular, function symbols of $\rl$ as well as the predicate
symbols “=” and “$\subseteq$” have a standard interpretation
as relations over $\Ss$
in the canonical model $\mathscr{W}=(\Ss, \cconc, \ttimes)$,
while, as we shall see,
$\Flip(t)$ can be interpreted either in a standard way
or following Definition <ref>.

Given a set of term variables $\mathcal{G}$,
an environment $\xi: \mathcal{G} \to \Ss$
is a mapping that assigns to each variable a string.

Given a term $t$ in $\rl$ and an environment $\xi$,
the interpretation of $t$ in $\xi$ is the string
$\model{t}_\xi \in \Ss$ inductively defined as follows:

\begin{align*}
\model{\epsilon}_\xi &\df \eepsilon \\
\model{\zzero}_\xi &\df \zero \\
\model{\oone}_\xi &\df \one \\
\end{align*}

\begin{align*}
\model{x}_\xi &\df \xi(x) \in \Ss \\
\model{t\conc s}_\xi &\df \model{t}_\xi \model{s}_\xi \\
\model{t \times s} _\xi &\df \model{t}_\xi \times \model{s}_\xi.
\end{align*}

As in Chapter <ref>, we extend the canonincal model $\mathscr{W}$ with the probability probability space
$\mathscr{P}_{\mathscr{W}} = (\Os, \sigma(\Cyls), \mu_{\Cyls})$,
where $\sigma(\Cyls)\subseteq \mathcal{P}(\Os)$
is the Borel $\sigma$-algebra generated by cylinders
$\cyl^\bool_\str = \{\eta \ | \ \eta(\str)=\bool\}$,
for $\bool \in \Bool$, and such that

To formally define cylinders over $\Bool^\Ss$,
we slightly modify Billingsley's notion of cylinder
of rank n.

For any countable set $S$,
finite $K\subset S$ and $H\subseteq \Bool^K$,

\cyl(H) = \{\eta \in \Bool^S \ | \ \eta |_K \in H\},

is a cylinder over $S$.

Then, $\Cyls$ and $\sigma(\Cyls)$
are defined in the standard way and
the probability measure over it is defined as follows:[For further
details, see [5].]

For any countable set $S$,
$K\subseteq S$ and $H\subseteq \Bool^K$ such
that $\cyl(H)=\{\eta \in \Bool^S \ | \ \eta|_K \in H\}$,

\mu_{\Cyls}(\cyl(H))= \frac{|H|}{2^{|K|}}.

This is a measure over $\sigma(\mathscr{C})$.

Then, formulas of $\rl$ are interpreted as sets measurable sets.

Given a term $t$, a formula $F$,
and an environment $\xi: \mathcal{G} \to \Ss$,
where $\mathcal{G}$ is the set of term variables,
the interpretation of $F$ under $\xi$
is the measurable set of sequences $\model{F}_\xi
\in \sigma(\Cyls)$ inductively defined as follows:

\begin{align*}
\\
\model{\Flip(t)}_\xi &\df
\{\eta \ | \ \eta(\model{t}_\xi) = \one\} \\
\model{t=s}_\xi &\df
\begin{cases}
\Os \ &\text{if } \model{t}_\xi = \model{s}_\xi   \\
\emptyset \ &\text{otherwise}
\end{cases} \\
\model{t\subseteq s}_\xi &\df
\begin{cases}
\Os \ &\text{if } \model{t}_\xi \ssubseteq \model{s}_\xi \\
\emptyset \ &\text{otherwise}
\end{cases}
\end{align*}

\begin{align*}
\model{\neg G}_\xi &\df \Os - \model{G}_\xi  \\
\model{G \vee H}_\xi &\df  \model{G}_\xi \cup \model{H}_\xi \\
\model{G \wedge H}_\xi &\df \model{G}_\xi \cap \model{H}_\xi \\
\model{G\rightarrow H}_\xi &\df (\Os - \model{G}_\xi) \cup
\model{H}_\xi \\
\model{(\exists x)G}_\xi &\df
\bigcup_{i\in\Ss} \model{G}_{\xi\{x\leftarrow i\}} \\
\model{(\forall x)G}_\xi &\df
\bigcap_{i\in \Ss} \model{G}_{\xi \{x\leftarrow i\}}.
\end{align*}

As anticipated, this semantics is well-defined.
Indeed, the sets $\model{\Flip(t)}_\xi$,
$\model{t=s}_\xi$ and $\model{t\subseteq s}_\xi$
are measurable and measurability is preserved
by all the logical operators.

A interpretation of the language
$\rl$ in the usual sense is given due to an environment $\xi$
plus the choice of an interpretation $\eta$ for $\Flip(x)$.

Given a $\rl$-formula $\fone$, and an interpretation
where $\xi:\mathcal{G}\to \Ss$ and
$\eta^{\mathtt{FLIP}} \subseteq \Os$,
the interpretation of $\fone$ in $\rho$ $\model{\fone}_\rho$,
is inductively defined as follows:

\begin{align*}
\model{\Flip(t)}_\rho &\df
\begin{cases}
1 \ &\text{if } \eta^{\mathtt{FLIP}}(\model{t}_\rho) =
\one \\
0 \ &\text{otherwise}
\end{cases} \\
\model{t=s}_\rho &\df
\begin{cases}
1 \ &\text{if } \model{t}_\rho = \model{s}_\rho \\
0 \ &\text{otherwise.}
\end{cases} \\
\model{t \subseteq s}_\rho &\df
\begin{cases}
1 \ &\text{if } \model{t}_\rho \ssubseteq \model{s}_\rho \\
0 \ &\text{otherwise}
\end{cases}
\end{align*}

\begin{align*}
\model{\neg G}_\rho &\df 1 - \model{G}_\rho \\
\model{G \wedge H}_\rho &\df min\{\model{G}_\rho,
\model{H}_\rho\} \\
\model{G \vee H}_\rho &\df max\{\model{G}_\rho,
\model{H}_\rho\} \\
\model{G \rightarrow H}_\rho &\df
max\{(1-\model{G}_\rho), \model{H}_\rho\} \\
\model{(\forall x)G}_\rho &\df
min\{\model{G}_{\rho\{x \leftarrow \str\}} \ | \ \str \in \Ss\} \\
\model{(\exists x)G}_\rho &\df max\{\model{G}_{\rho\{x\leftarrow \str\}}
\ | \ \str \in \Ss\}.
\end{align*}

For readability's sake,
we abbreviate $\model{\cdot}_{\rho}$ simply as
and $\model{\cdot}_\xi$ as  $\model{\cdot}$.

Observe that quantitative
and qualitative
semantics for $\rl$ are mutually related,
as can be proved by induction on the structure of formulas [5].

For any formula $F$ in $\rl$, environment $\xi$,
function $\eta \in \Os$ and $\rho=(\eta,\xi)$,

\model{F}_{\xi,\eta} = 1 \ \ \text{iff} \ \
\eta \in \model{F}_\rho.

§ $\RS$ CHARACTERIZES $\POR$

As said, our proof follows a so-to-say standard path [1, 6].

The first step consists in showing that functions in $\POR$
are precisely those which are $\Sigma^b_1$-representable in

To do so, we extend Buss' representability conditions by
adding a constraint to link the quantitative semantics
of formulas in $\RS$ with the additional functional
parameter $\eta$ of oracle recursive functions.

A function $f:\Ss^k \times \Os \to \Ss$ is
in $\RS$ if there is a
$\Sigma^b_1$-formula $\fone(\vec{x},y)$ of $\rl$ such that:

* $\RS\vdash (\forall \vec{x})(\exists y)\fone(\vec{x},y)$

* $\RS \vdash (\forall \vec{x})(\forall y)(\forall z)
\big(\fone(\vec{x},y) \wedge \fone(\vec{x},z) \rightarrow y=z\big)$

* for all $\str_1,\dots, \str_j,\strT \in \Ss$ and $\eta\in \Os$,

f(\str_1,\dots, \str_j,\eta) = \strT \ \ \ \text{iff} \ \ \
\eta \in \model{\fone
(\overline{\str_1},\dots, \overline{\str_j},\overline{\strT})}.

We recall that the language $\rl$ allows us to associate
the formula $\fone$ with both a qualitative
– namely, when dealing with 1. and 2. –
and a quantitative interpretation – namely, in 3.

Then, in  Section <ref>,
we prove the following theorem.

For any function $f:\Ss^k\times \Os \to \Ss$,
$f$ is $\Sigma^b_1$-representable in $\RS$
when $f\in\POR$.

In particular, that any function in $\POR$
is $\Sigma^b_1$-representable in
$\RS$ is proved in Section <ref>
by a straightforward induction on the structure
of probabilistic oracle functions.

The other direction is established in
Section <ref> by a realizability argument
very close to the one offered in [3].

[node distance=2cm]
[draw] at (-3,0) (a) Class $\POR$;
[draw] at (3,0) (b) $\Sigma^b_1$-Representability in $\RS$;
at (0,1.2) induction on $\POR$, Sec. <ref>;
at (0,-1.2) realizability as in [3], Sec. <ref>;

[->,dotted,thick] (-2.5,0.4) to [bend left=20] (2.5,0.4);
[->,dotted,thick] (2.5,-0.4) to [bend left=20] (-2.5,-0.4);

Relating $\POR$ and $\RS$

§.§ Functions in $\POR$ are $\Sigma^b_1$-Representable in $\RS$

We prove that any function in $\POR$ is
$\Sigma^b_1$-representable in $\RS$ by
constructing the desired formula by induction on the structure
of oracle functions.

Preliminarily notice that, for example,
the formula $(\forall \vec{x})(\exists y)G(\vec{x},y)$
occurring in condition 1. is not in
$\Sigma^b_1$, since its existential
quantifier is not bounded.

Hence, in order to prove the inductive steps of Theorem <ref>
– namely, composition
and bounded recursion on notation –
we need to adapt Parikh's theorem [10]

to $\RS$.[The
theorem is usually presented in the
context of Buss' bounded theories,
as stating that given a bounded formula
$\fone$ in $\mathcal{L}_\Nat$ such that $\BussS \vdash
(\forall \vec{x})(\exists y)\fone$,
then there is a term $t(\vec{x})$
such that also $\BussS
\vdash (\forall \vec{x})(\exists y\leq t(\vec{x}))
\fone(\vec{x},y)$ [1, 2].

Furthermore, due to [8],
Buss' syntactic proof can be adapted
to $\Sigma^b_1$-NIA in a natural way.

The same result holds for $\RS$,
which does not contain any specific rule
concerning $\Flip(\cdot)$.]

Let $\fone(\vec{x},y)$ be a bounded formula in $\rl$
such that
$\RS \vdash (\forall \vec{x})(\exists y) \fone(\vec{x},y)$.

Then, there is a term $t$ such that,

\RS \vdash (\forall \vec{x})(\exists y \preceq t(\vec{x}))\fone(\vec{x},y).

Every $f\in \POR$ is $\Sigma^b_1$-representable
in $\RS$.

The proof is by induction on the structure
of functions in $\POR$.[For further details, see Appendix <cit.>.]

Base Case. Each basic function is
$\Sigma^b_1$-representable in $\RS$.
There are five possible sub-cases:

* Empty (String) Function.
$f=\emptyS$ is $\Sigma^b_1$-represented in $\RS$ by
the formula:

F_{\emptyS}(x,y) : x=x \wedge y=\epsilon.

Existence is proved considering

For the reflexivity of identity both
$\RS\vdash x=x$ and $\RS \vdash \epsilon=\epsilon$

So, by rules for conjunction,
we obtain $\RS\vdash x=x \wedge \epsilon=\epsilon$,
and conclude:

\RS\vdash (\forall x)(\exists y)(x=x \wedge y=\epsilon).

* Uniqueness is proved assuming $\RS \vdash
x= x \wedge z=\epsilon$.

By rules for conjunction,
in particular $\RS \vdash z=\epsilon$, and since

$\RS \vdash y=\epsilon$,
by the transitivity of identity, we conclude

\RS\vdash y=z.

* Assume $\emptyS(\str, \eta^*) = \strT$.

If $\strT=\eepsilon$, then:

\begin{align*}
\model{\overline{\str} = \overline{\str}
\wedge \overline{\strT} = \epsilon}
\model{\overline{\str} = \overline{\str}}
\cap
\model{\overline{\strT} = \epsilon} \\
&= \Os \cap \Os \\
&= \Os.
\end{align*}

So, in this case, for any $\eta^*$,
$\eta^* \in \model{\overline{\str}=\overline{\str}
\wedge \overline{\strT} = \epsilon}$,
as clearly $\eta^* \in\Os$.

If $\strT\neq \eepsilon$, then

\begin{align*}
\model{\overline{\str} = \overline{\str} \wedge
\overline{\strT} = \epsilon}
\model{\overline{\str} = \overline{\str}}
\cap \model{\overline{\strT} =\epsilon} \\
&= \Os \cap \emptyset \\
&= \emptyset.
\end{align*}

So, for any $\eta^*$,
$\eta^* \not\in \model{\overline{\str}= \overline{\str}
\vee \overline{\strT} = \epsilon}$,
as clearly $\eta^* \not\in \emptyset$.

* Projection (String) Function.
$f=\projS^n_i$, for $1\leq i\leq n$,
is $\Sigma^b_1$-represented in $\RS$ by
the formula:

F_{\projS^{n}_{i}}(x,y) : \bigwedge_{j\in J}(x_j=x_j)
\wedge y= x_i,

where $J=\{1,\dots, n\}\setminus \{i\}$.

* Word-Successor Function.
$f=\successorS_b$ is $\Sigma^b_1$-represented
in $\RS$ by the formula:

F_{S_b}(x,y) : y= x\bbool

where $\bbool=\zzero$ if $b=0$
and $\bbool=\oone$ if $b=1$.

* Conditional (String) Function.
$f=\condS$ is $\Sigma^b_1$-represented
in $\RS$ by the formula:

\begin{align*}
\fone_{\condS} (x,v,z_0,z_1,y) :
(x=\epsilon \wedge y=v)
&\vee (\exists x' \preceq x)
(x=x'\zzero \wedge y=z_0) \\
(\exists x'\preceq x)
(x=x'\oone \wedge y=z_1).
\end{align*}

* Query (String) Function.
$f=\queryS$ is $\Sigma^b_1$-represented
in $\RS$ by the formula:

F_{\queryS}(x,y) :
(\Flip(x) \wedge y=\oone) \vee
(\neg \Flip(x) \wedge y=\zzero).

Notice that, in this case, the proof crucially
relies on the fact that oracle functions
invoke exactly one oracle.

* Existence is proved by cases.

If $\RS \vdash \Flip(x)$,
let $y=\oone$.
By the reflexivity of identity,
$\RS \vdash \oone = \oone$ holds,
so also $\RS \vdash \Flip(x) \wedge \oone=\oone$.

By rules for disjunction, we conclude
$\RS\vdash (\Flip(x) \wedge \oone = \oone)
\vee (\neg \Flip(x) \wedge \oone= \zzero)$
and so,

\RS \vdash (\exists y)\big((\Flip(x) \wedge y=\oone)
\vee (\neg \Flip(x) \wedge y=\zzero)\big).

If $\RS \vdash \neg \Flip(x)$,
let $y=\zzero$.
By the reflexivity of identity
$\RS \vdash \zzero=\zzero$ holds.

Thus, by the rules for conjunction,
$\RS \vdash \neg \Flip(x) \wedge \zzero=\zzero$
and for disjunction,
we conclude $\RS \vdash(\Flip(x) \wedge \zzero=\oone)
\vee (\neg \Flip(x) \wedge \zzero=\zzero)$ and so,

\RS \vdash (\exists y) \big((\Flip(x) \wedge
y= \oone) \vee
(\neg \Flip(x) \wedge y=\zzero)\big).

* Uniqueness is established
relying on the transitivity of identity.

* Finally, it is shown that for every
$\str,\strT\in \Ss$ and
$\eta^* \in \Os$,
$\queryS(\str,\eta^*)=\strT$ when
$\eta^*\in \model{F_{\queryS}

Assume $\queryS(\str,\eta^*) = \one$,
which is $\eta^*(\str)=\one$,

\begin{align*}
\model{\fone_Q(\overline{\sigma},\overline{\tau})}
\model{\Flip(\overline{\str}) \wedge
\overline{\strT}=\oone}
\cup
\model{\neg \Flip(\overline{\str})
\wedge \overline{\strT}=\zzero} \\
&= (\model{\Flip(\overline{\str})} \cap
\model{\oone=\oone}) \cup
(\model{\neg \Flip(\overline{\str})}
\cap \model{\oone=\zzero}) \\
&= (\model{\Flip(\overline{\str})} \cap \Os)
\cup
(\model{\neg \Flip(\overline{\str})} \cap
\emptyset) \\
&= \model{\Flip(\overline{\str})} \\
&= \{\eta \ | \ \eta(\str)=\one\}.
\end{align*}

Clearly, $\eta^* \in  \model{(\Flip(\overline{\str}) \wedge \overline{\strT} = \oone) \vee (\neg \Flip(\overline{\str}) \wedge \overline{\strT}=\zzero)}$.

The case $\queryS(\sigma,\eta^*)=\zero$
and the opposite direction are proved in a similar way.

Inductive Case.
If $f$ is defined by composition or bounded recursion
from $\Sigma^b_1$-representable functions,
then $f$ is $\Sigma^b_1$-representable in $\RS$:

* Composition.
Assume that $f$ is defined by composition from functions
$g,h_1,\dots, h_k$ so that

f(\vec{x},\eta) = g(h_1(\vec{x},\eta), \dots, h_k(\vec{x},\eta),
\eta)

and that $g,h_1,\dots, h_k$ are represented in $\RS$
by  the $\Sigma^b_1$-formulas
$F_g,F_{h_1},$ $\dots, F_{h_k}$, respectively.

By Proposition <ref>,
there exist suitable terms $t_{g}, t_{h_1},\dots, t_{h_k}$
such that condition 1. of Definition <ref>
can be strengthened to $\RS\vdash(\forall \vec{x})
(\exists y \preceq t_i)F_i(\vec{x},y)$ for each $i\in\{g,h_1,\dots, h_k\}$.

We conclude that $f(\vec{x},\eta)$ is $\Sigma^b_1$-represented
in $\RS$ by the following formula:

\begin{align*}
F_f(x,y) : (\exists z_1\preceq t_{h_1}(\vec{x}))
\dots
(\exists z_k \preceq t_{h_k}(\vec{x}))
\big(F_{h_1}(\vec{x},z_1) &\wedge \dots
F_{h_k}(\vec{x},z_k) \\
F_g(z_1,..., z_k,y)\big).
\end{align*}

Indeed, by IH,
$F_g,F_{h_1},\dots, F_{h_k}$ are $\Sigma^b_1$-formulas.
Then, also $F_f$ is in $\Sigma^b_1$.
Conditions 1.-3. are proved to hold by slightly modifying standard

* Bounded Recursion. Assume that $f$
is defined by bounded recursion from
$g,h_0,$ and $h_1$ so that:

\begin{align*}
f(\vec{x},\eepsilon,\eta) &= g(\vec{x},\eta) \\
f(\vec{x}, y\bool, \eta) &= h_i(\vec{x},y,f(\vec{x},y,\eta),\eta)|_{t(\vec{x},y)},
\end{align*}

where $i \in\{0,1\}$
and $\bool=\zero$ when $i=0$ while
and $\bool = \one$ when $i=1$.

Let $g,h_0, h_1$ be represented in $\RS$
by, respectively, the $\Sigma^b_1$-formulas
$F_g,F_{h_0},$ and $F_{h_1}$.

Moreover, by Proposition <ref>,
there exist suitable terms $t_g,t_{h_0},$ and $t_{h_1}$
such that condition 1. of Definition <ref>
can be strengthened to its “bounded version”.

Then, it can be proved that $f(\vec{x},y)$
is $\Sigma^b_1$-represented in $\RS$ by the formula below:

\begin{align*}
F_f(x,y) : \ &(\exists v \preceq t_g(\vec{x})
t_f(\vec{x}) (y \times t(\vec{x},y) t(\vec{x},y) \oone\oone))
\big(F_{lh}(v, \oone \times y \oone)  \\
& \wedge (\exists z\preceq t_g(\vec{x}))
(F_{eval}(v,\epsilon,z) \wedge
F_g(\vec{x},z)) \\
& \wedge (\forall u \subset y)(\exists z)
\big(\tilde{z} \preceq t(\vec{x},y))
\big(F_{eval}(v,\oone \times u, z) \wedge
F_{eval}(v,\oone \times u\oone,\tilde{z}) \\
& \wedge (u\zzero \subseteq y \rightarrow
(\exists z_0 \preceq t_{h_0}(\vec{x},u,z))
\wedge z_0|_{t(\vec{x},u)} = \tilde{z})) \\
& \wedge (u\oone \subseteq y \rightarrow
(\exists z_1 \preceq t_{h_1}(\vec{x},u,z))
(F_{h_1}(\vec{x},u,z,z_1) \wedge
z_1|_{t(\vec{x},u)} = \tilde{z}))\big)\big),
\end{align*}

where $\fone_{lh}$ and $F_{eval}$ are $\Sigma^b_1$-formulas
defined as in [7].

Intuitively, $F_{lh}(x,y)$ states that the number of $\oone$s
in the encoding of $x$ is $yy$,
while $F_{eval}(x,y,z)$ is a “decoding” formula
(strongly resembling Gödel's $\beta$-formula),
expressing that the “bit” encoded in $x$ as its $y$-th bit
is $z$.

Moreover $x\subset y$ is an abbreviation for $x\subseteq y
\wedge x \neq y$.

Then, this formula $F_f$ satisfies all the requirements to
$\Sigma^b_1$-represent in $\RS$ the function $f$,
obtained by bounded recursion from $g,h_0,$ and $h_1$.

In particular, conditions 1. and 2. concerning existence and
have already been proved to hold by Ferreira [7].

Furthermore, $F_f$ expresses that,
given the desired encoding sequence $v$:
(i.) the $\eepsilon$-th bit of $v$ is (the encoding
of) $z'$ such that $F_g(\vec{x},z')$ holds,
where (for IH) $F_g$ is the $\Sigma^b_1$-formula
representing the function $g$,
and (ii.) given that for each $u\subset y$,
$z$ denotes the “ bit” encoded in $v$ at position
$1\times u$ and, similarly, $\tilde{z}$ is the next “bit”,
encoded in $v$ at position $\oone \times u\oone$,
then if $u\bbool \subseteq y$
(that is, if we are considering the initial substring of $y$
the last bit of which corresponds to $\bbool$),
then there is a $z_b$ such that
$F_{h_b}(\vec{x},y,z,z_b)$, where $F_{h_b}$ $\Sigma^b_1$-represents
the function $f_{h_b}$ and the truncation of $z_b$
at $t(\vec{x},u)$ is precisely
$\tilde{z}$, with $b=0$ when $\bbool=\zzero$ and
$b=1$ when $\bbool=\oone$.[Otherwise said,
if $u\zzero\subseteq y$, there is a $z_0$ such that
the $\Sigma^b_1$-formula $F_{h_0}(\vec{x},
u,z,z_0)$ represents  the function $h_0$
and, in this case, $\tilde{z}$ corresponds
to the truncation of $z_0$ at $t(\vec{x},u)$,
that is the “bit” encoded by $v$ at the position
$\oone \times u\oone$ (i.e. corresponding to
$u\zzero \subseteq y$) is precisely such $\tilde{z}$.
Equally, if $u\oone\subseteq y$, there is a
$z_0$ such that the $\Sigma^b_1$-formula
$F_{h_1}(\vec{x},u,z,z_1)$ represents now the function
$h_1$ and $\tilde{z}$ corresponds to the truncation
of $z_1$ at $t(\vec{x},u)$,
that is the “bit” encoded by $v$ at position
$\oone\times u\oone$ (i.e. corresponding to $u\oone
\subseteq y)$ is precisely such $\vec{z}$. For further details, see Appendix <cit.>.]

§.§ The functions which are $\Sigma^b_1$-Representable
in $\RS$ are in $\POR$

§ RELATING $\POR$ AND POLY-TIME PTMS

[1]
S.R. Buss.
Bounded Arithmetic.
PhD thesis, Princeton University, 1986.

[2]
S.R. Buss.
First-Order Proof Theory of Arithmetic.
In Elsavier, editor, Handbook of Proof Theory. Buss, S.R.,

[3]
S. Cook and A. Urquhart.
Functional Interpretations of Feasibly Constructive Arithmetic.
Annals of Pure and Applied Logic, 63:103–200, 1993.

[4]
T. Coquand and M. Hofmann.
A New Method for Establishing Conservativity of Classical Systems
over Their Intuitionistic Version.
Mathematical Structures in Computer Science, 9(4):323–333,

[5]
D. Davoli.
Bounded Arithmetic and Randomized Computation.
Master Thesis, <http://amslaurea.unibo.it/26234/>, 2022.

[6]
F. Ferreira.
Polyonmial time computable arithmetic and conservative extesions.
Ph.D. Dissertation, December 1988.

[7]
F. Ferreira.
Polynomial-time computable arithmetic.
In W. Sieg, editor, Logic and Computation, volume 106 of Contemporary Mathematics, pages 137–156. AMS, 1990.

[8]
G. Ferreira and I. Oitavem.
An Interpretation of $S^1_2$ in $\Sigma^b_1$-NIA.
Portugaliae Mathematica, 63:427–450, 2006.

[9]
J.T. Gill.
Computational complexity of probabilistic Turing machines.
J. Comput., 6(4):675–695, 1977.

[10]
R.J. Parikh.
Language Generating Devices.
Quart. Prog. Rep., 60:199–212, 1961.

[11]
E.S. Santos.
Probabilistic Turing machines and computability.
Proceedings of the American Mathematical Society,
22(3):704–710, 1969.

[12]
G. Winskel.
The Formal Semantics of Programming Languages.
The MIT Press, 1993.

§ PROOFS FROM SECTION <REF>

§.§ Further details on Theorem <ref>

The proof is by induction on the structure
of $f\in\POR$.

Base case.
If $f$ is a basic function, then there are five possible

* $f=E$ is $\Sigma^b_1$-represented in $\RS$
by the formula
$F_E(x,y) : x=x \wedge y=\epsilon$.

The existence condition is derived as follows:

$z=z \vdash (\exists y)(z=z \wedge y=\epsilon),
$\vdash(\exists y)(z=z \wedge y=\epsilon),

$\epsilon=\epsilon \vdash (\exists y)(z=z \wedge
$\vdash(\exists y)(z=z \wedge y=\epsilon),\epsilon=\epsilon$
$\wedge R$
$\vdash (\exists y)(z=z \wedge y=\epsilon), z=z \wedge
\epsilon=\epsilon$
$\exists R$
$(\exists y) (z=z \wedge y=\epsilon)$
$\forall R$
$\vdash(\forall x)(\exists y)(x=x \wedge y=\epsilon)$

Uniqueness condition is derived below:

$x_2=x_3,x_1=x_1,x_2=\epsilon, x_3=\epsilon \vdash
$x_1=x_1,x_2=\epsilon, x_1=x_1,x_3=\epsilon
\vdash x_2 = x_3$
$\wedge L$s
$x_1=x_1\wedge x_2=\epsilon, x_1=x_1 \wedge
x_2=\epsilon \vdash x_2=x_3$
$\wedge L$
$(x_1=x_1 \wedge x_2=\epsilon)
\wedge (x_1=x_1\wedge x_2=\epsilon) \vdash
$\rightarrow R$
$\vdash (x_1=x_1 \wedge x_2=\epsilon)
\wedge (x_1=x_1 \wedge x_2=\epsilon) \rightarrow
$\forall Rs$
$\vdash (\forall x)(\forall y)(\forall z)((x=x
\wedge y=\epsilon) \wedge (x=x \wedge z=\epsilon) \rightarrow

The semantic condition is proved showing that
for all $n,m\in \Ss$ and $\eta^* \in\Os$,
$E(\str_1,\eta^*)=\str_2$ when $\eta \in \model{\overline{\str_1}=\overline{\str_1}
\wedge \overline{\str_2}=\epsilon}$.

$\Rightarrow$ Assume $\str_2=\eepsilon$.

\begin{align*}
\model{\overline{\str_1}=\overline{\str_1} \wedge \overline{\str_2}
=\epsilon} &=
\model{\overline{\str_1}=\overline{\str_1} \wedge \overline{\eepsilon}
= \epsilon} \\
&= \model{\overline{\str_1}=\overline{\str_1} \wedge
\epsilon=\epsilon} \\
&= \model{\overline{\str_1}=\overline{\str_1}} \cap
\model{\epsilon=\epsilon} \\
&= \Os \cap \Os \\
&= \Os.
\end{align*}

Clearly, for any $\eta^*$, $\eta^*\in \Os$,
that is $\eta^* \in \model{\overline{\str_1}=\overline{\str_1}
\wedge \overline{m}=\epsilon}$.

$\Leftarrow$ Assume (by contraposition) $m\neq \eepsilon$.

\begin{align*}
\model{\overline{\str_1}=\overline{\str_1} \wedge
\overline{\str_2}=\epsilon} &=
\model{\overline{\str_1} = \overline{\str_1}} \cap
\model{\overline{\str_2} =\epsilon} \\
&= \Os \cap \emptyset \\
&= \emptyset.
\end{align*}

Clearly, for any $\eta^*$, $\eta^* \not \in \emptyset$,
so $\eta^* \not\in \model{\overline{\str_1}=\overline{\str_1}
\wedge \overline{\str_2}=\emptyset}$.

* $f= P^n_i$, for $1\leq i\leq n \in \Nat$.
The function si $\Sigma^b_1$-represented in $\RS$
by the formula:
$\bigwedge_{j\in J}(x_j=x_j) \wedge y=x_i$,
where $J=\{1,\dots, n\}\setminus i$.
The proof is similar to the one above.

* $f = S_b$.
The function is $\Sigma^b_1$-represented
in $\RS$ by the formula: $y=x\bbool$,
where $\bbool\in\{\zzero,\oone\}$
and $\bbool=\zzero$ when $b=0$
and $\bbool=\oone$ when $b=1$.

The existence condition is derived as follows:

$z\bbool = z\bbool \vdash (\exists y)(y=z\bbool),
z\bbool = z\bbool$

$\vdash (\exists y)(y=z\bbool), z\bbool = z\bbool$
$\exists R$
$\vdash (\exists y)(y=z\bbool)$
$\forall R$
$\vdash (\forall x)(\exists y)(y=x\bbool)$

Uniqueness is derived below:

$x_2=x_3,x_2=x_1\bbool, x_3=x_1\bbool \vdash
$x_2=x_1\bbool, x_3 = x_1\bbool \vdash x_2=x_3$
$\wedge L$
$x_2=x_1\bbool \wedge x_3=x_1\bbool \vdash
$\rightarrow R$
$\vdash (x_2=x_1\bbool) \wedge
(x_3=x_1\bbool) \rightarrow x_2=x_3$
$\forall R$s
$\vdash (\forall x)(\forall y)(\forall z)((y=x\bbool)
\wedge (z=x\bbool) \rightarrow y=z)$

The semantic condition is proved showing that for
all $\str_1,\str_2 \in \Ss$ and $\eta^* \in \Os$,
$S_b(\str_1,\eta^*) = \str_2$
when $\eta^* \in \model{\overline{\str_2} = \overline{\str_1}\bbool}$.

Assume $b=0$.
So, $\str_2=\str_1\zero$ (and
$\bbool = \zzero$).

\begin{align*}
\model{\overline{\str_2}=\overline{\str_1}\zzero}
\model{\overline{\str_1\zero} = \overline{n}\zzero} \\
&= \model{\overline{n}\zzero = \overline{n}\zzero} \\
&= \Os.
\end{align*}

For any $\eta^*$, $\eta^* \in \Os$,
that is $\eta^* \in \model{\overline{\str_2} = \overline{\str_1}\zzero}$.

Similarly, if $b=1$ and $\str_2=\str_1\one$
(and $\bbool = \oone$).

\begin{align*}
\model{\overline{\str_2} = \overline{\str_1}\oone}
\model{\overline{n\one} = \overline{n}\oone} \\
&= \model{\overline{n}\oone = \overline{n}\oone} \\
&= \Os.
\end{align*}

$\Leftarrow$ Assume (by contraposition)
$b=0$ and $\str_2\neq \str_1 \zero$
(and $\bbool = \oone$).
Then, clearly $\model{\overline{\str_2} = \overline{\str_1}\oone}
= \emptyset$.
So, for any $\eta^*\in \Os$,
$\eta^* \not\in \emptyset$.

The case of $b=0$ and $m\neq n\oone$ (and $\bbool=\zzero$)
is equivalent.

* $f=C$.
The function is $\Sigma^b_1$-representable in $\RS$
by the formula
F_C(x,v,z_0,z_1,y) : (x=\epsilon \wedge y=v)
\vee (\exists x' \preceq x)
(x=x'\zzero \wedge y=z_0)
\vee (\exists x'\preceq x)(x=x'\one \wedge y=z_1).

* $f=Q$. The function is $\Sigma^b_1$-represented
in $\RS$ by $
F_Q : (\Flip(x) \wedge y=\oone) \vee
(\neg \Flip(x) \wedge y=\zzero).
The existence condition is proved as follows:

$\Flip(x) \vdash
(\exists y)F_Q(z,y), \Flip(z)$
$\neg R$
$\vdash (\exists y)F_Q(z,y),
\Flip(z), \neg \Flip(z)$

$\mathcal{D}_{\exists Q}$

$\vdash (\exists y)F_Q(z,y), \Flip(z),\oone=\zzero$
$\wedge R$
$\vdash (\exists y)F_Q(z,y),
\Flip(z), \neg\Flip(z) \wedge \oone=\zzero$

$\oone=\oone \vdash ..., \oone=\oone$
$\vdash ..., \oone = \oone$
$\wedge R$

$\vdash (\exists y)F_Q(z,y), (\Flip(z) \wedge \oone=\oone),
(\neg \Flip(z) \wedge \oone=\zzero)$
$\vee R$
$\vdash (\exists y)F_Q(z,y), (\Flip(z) \wedge \oone=\oone)
\vee (\neg \Flip(z) \wedge \oone=\zzero)$
$\exists R$
$\vdash (\exists y)((\Flip(z) \wedge y=\oone)
\vee (\neg \Flip(z) \wedge y=\zzero))
$\forall R$
$\vdash(\forall x)(\exists y)((\Flip(x) \wedge
y=\oone) \vee (\neg \Flip(x) \wedge

\mathcal{D}_{\exists Q}

$\Flip(z)\vdash .... , \Flip(z)$
$\neg R$
$\vdash ...\Flip(z), \neg \Flip(z)$

$\zzero=\zzero \vdash ..., \Flip(z),
\zzero=\zzero$
$\vdash ..., \Flip(z), \zzero=\zzero$

$\wedge R$
$\vdash ..., \Flip(z), \Flip(z)\wedge \zzero=\oone,
\neg \Flip(z) \wedge \zzero=\zzero$
$\vee R$
$\vdash(\exists y)F_Q(z,y), \oone = \zzero,
\Flip(z), F_Q(z,\zzero)$
$\exists R$

$\vdash (\exists y)F_Q(z,y),
\Flip(z),\oone=\zzero$

Uniqueness is shown as below:

$\mathcal{D}_{\forall Q1}$
$\Flip(x_1) \wedge x_2 = \oone,
F_Q(x_1,x_2) \vdash x_2 = x_3$

$\mathcal{D}_{\forall Q2}$
$\neg \Flip(x_1) \wedge = \zzero,
F_Q(x_1,x_3) \vdash x_2=x_3$

$\vee L$
$F_Q(x_1,x_2), F_Q(x_1,x_3)
\vdash x_2=x_3$
$\wedge L$
$F_Q(x_1,x_2)\wedge F_Q(x_1,x_3) \vdash
$\rightarrow R$
$\vdash F_Q(x_1,x_2)
\wedge F_Q(x_1,x_3) \rightarrow x_2 = x_3$
$\forall R$s
$\vdash (\forall x)(\forall y)(\forall z)(F_Q(x,y)
\wedge F_Q(x,z) \rightarrow y=z)$

\mathcal{D}_{\forall Q1}

$x_2=x_3, \Flip(x_1), x_2=\oone,
x_3=\oone \vdash x_2=x_3$
$\Flip(x_1), x_2=\oone, \Flip(x_1),
x_3=\oone \vdash x_2=x_3$
$\wedge L$
\Flip(x_1) \wedge x_3=\oone \vdash
x_2 = x_3$

$\Flip(x_1), x_2=\oone, x_3=\zzero
\vdash x_2=x_3,\Flip(x_1)$
$\neg L$
$\Flip(x_1), x_2=\oone,
\neg \Flip(x_1), x_3=\zzero \vdash x_2=x_3$
$\wedge L$
$\Flip(x_1), x_2=\oone,
\neg \Flip(x_1) \wedge x_3=\zzero \vdash

$\vee L$
$\Flip(x_1),x_2=\oone, F_Q(x_1,x-3)
\vdash x_2=x_3$
$\wedge L$
$\Flip(x_1) \wedge x_2=\oone,
F_{Q}(x_1,x_3) \vdash x_2=x_3$

\mathcal{D}_{\forall Q2}

$\Flip(x_1), x_3=\oone, y=\zzero \vdash
x_2=x_3, \Flip(x_1)$
$\neg L$
$\neg \Flip(x_1), y=\zzero, \Flip(x_1),
x_3=\oone \vdash x_2=x_3$
$\wedge L$
$\neg \Flip(x_1), y=\zzero,
\Flip(x_1) \wedge x_3=\oone \vdash x_2=x_3$

$x_2=x_3, \neg \Flip(x_1), x_2=\zzero,
x_3=\zzero \vdash x_2=x_3$
$\neg \Flip(x_1), x_2=\zzero, \neg \Flip(x_1),
x_3=\zzero \vdash x_2=x_3$
$\wedge L$
$\neg \Flip(x_1), x_2=\zzero,
\neg \Flip(x_1) \wedge x_3=\zzero \vdash x_2=x_3$

$\vee L$
$\neg \Flip(x_1), y=\zzero, F_Q(x_1,x_3)
\vdash x_2=x_3$
$\wedge L$
$\neg \Flip(x_1) \wedge y=\zzero, F_Q(x_1,x_3)
\vdash x_2=x_3$

The semantic condition is proved considering that
for all
$\str_1,\str_2$ and $\eta^* \in \Os$,
$Q(\str_1,\eta^*) = \str_2$
when $\eta^* \in \model{(\Flip(\overline{\str_1})
\wedge \overline{\str_2}=\oone)
\vee (\neg \Flip(\overline{\str_1} \wedge
\overline{\str_2}=\zzero)}$.

Assume $Q(\str_1,\eta^*) =\str_2$
and $\str_2=\one$,
that is $\eta^* (\str_1)=\one$.

\begin{align*}
\model{F_Q(\overline{\str_1},\overline{\str_2}) }
\model{(\Flip(\overline{\str_1}) \wedge \overline{\one}
=\oone) \vee (\neg \Flip(\overline{\str_1}) \wedge
\overline{\one} = \zero)} \\
&= \model{(\Flip(\overline{\str_1}) \wedge
\oone = \oone) \vee (\neg \Flip(\overline{\str_1}) \wedge
\oone =\zzero)} \\
&= \model{\Flip(\overline{\str_1}) \wedge \oone = \oone}
\cup \model{\neg \Flip(\overline{\str_1}) \wedge \oone = \zzero} \\
&= \big(\model{\Flip(\overline{\str_1})} \cap \model{\oone =\oone}\big)
\cup \big(\model{\neg \Flip(\overline{\str_1})} \cap
\model{\oone=\zzero}\big) \\
&= \big(\model{\Flip(\overline{\str_1})} \cap \Os\big)
\cup \big(\model{\neg \Flip(\overline{\str_1})} \cap
\emptyset \big) \\
&= \model{\Flip(\overline{\str_1})} \cup \emptyset \\
&= \model{\Flip(\overline{\str_1})} \\
&= \{ \eta \ | \ \eta (\str_1) = \one\}.
\end{align*}

As seen $\eta^* (\str_1)=\one$,
so $\eta^* \in \{\eta \ | \ \eta(n) = \one\}
= \model{(\Flip(\overline{\str_1}) \wedge
\overline{\one} =\oone) \vee
(\neg \Flip(\overline{\str_1}) \wedge \overline{\one}=\zzero)}$.

Assume $Q(\str_1,\eta^*)=\str_2$ and $\str_2=\zero$,
that is $\eta^* (\str_1)=\zero$.

\begin{align*}
\model{F_Q(\overline{\str_1},\overline{\str_2})} &=
\model{(\Flip(\overline{\str_1}) \wedge \overline{\one}
= \oone) \vee (\neg \Flip(\overline{\str_1}) \wedge
\overline{\one} = \zzero)} \\
&= \model{(\Flip(\overline{\str_1}) \wedge \zzero=\oone)
\vee (\neg \Flip(\overline{\str_1}) \wedge \zzero=\zzero)} \\
&= \model{\Flip(\overline{\str_1}) \wedge \zzero=\oone}
\cup \model{\neg \Flip(\overline{\str_1}) \wedge \zzero=\zzero} \\
\big(\model{\Flip(\overline{\str_1})} \cap \model{\zzero=\oone}\big)
\cup
\big(\model{\neg \Flip(\overline{\str_1})} \cap \model{\zzero=\zzero} \big) \\
&= (\model{\Flip(\overline{\str_1})} \cap \emptyset)
\cup (\model{\neg \Flip(\overline{\str_1})} \cap \Os) \\
&= \emptyset \cup \model{\neg \Flip(\overline{\str_1})} \\
&= \model{\neg \Flip(\overline{\str_1})} \\
&= \Os - \model{\Flip(\overline{\str_1})} \\\
&= \{ \eta \ | \ \eta (n) = \zero\}.
\end{align*}

As seen, $\eta^*(n)=\\zero$, so clearly
$\eta^* \in \{\eta \ | \ \eta(n) = \zero\} =
\model{(\Flip(\overline{\str_1}) \wedge \overline{\zero}
= \oone ) \vee (\neg \Flip(\overline{\str_1})
\wedge \overline{\zero} = \zzero)}$.

Assume (by contraposition) $\eta^*(\str_1)=\one$,
so $Q(\str_1,\eta^*) =\one$
and $m=\zero$.
As shown above,
in this case $\model{(\Flip(\overline{\str_1}) \wedge
\overline{\zero}=\oone) \vee (\neg \Flip(\overline{\str_1})
\wedge \overline{\zero}=\zzero)}
= \{\eta \ | \ \eta(\str_1)=\zero\}$.
For assumption, $\eta^*$ is such that $\eta^*(\str_1)=\one$,
so $\eta^* \not \in \{\eta \ | \ \eta(\str_1)=\zero\}$,
that is $\eta^* \not\in \model{(\Flip(\overline{\str_1} \wedge
\overline{\zero}=\oone) \vee
(\neg \Flip(\overline{\str_1}) \wedge
\overline{\zero}=\zzero)}$.

Assume (by contraposition) $\eta^*(\str_1)=\zero$,
so $Q(\str_1,\eta^*)=\zero$ and $m=\one$.

As shown above, in the case $\model{(\Flip(\overline{\str_1})
\wedge \overline{\one}=\oone) \vee (\neg \Flip(\overline{\str_1})
\wedge \overline{\one} = \zzero)}
= \{\eta \ | \ \eta(\str_1)= \one\}$.

For assumption, $\eta^*$ is such that $\eta^*(\str_1)=\zero$,
so $\eta^* \not\in \{\eta \ | \ \eta(\str_1) =\one\}$,
that is $\eta^* \not \in \model{(\Flip(\overline{\str_1}) \wedge
\overline{\one}=\oone) \vee
(\neg \Flip(\overline{\str_1}) \wedge \overline{\one}=\zzero)}$.

Inductive Case. If $f\in\POR$ is obtained from
$\Sigma^b_1$-representable functions by
either composition or bounded recursion, then $f$
is $\Sigma^b_1$-representable as well.

§ PROOFS FROM SECTION <REF>

§.§ Relating $\RFP$ and $\SFP$

§.§.§ On Stream Turing Machine

We define stream Turing machines in a formal

A stream Turing machine
is a quadruple $\STM= \langle \Qstates, q_0,\Sigma,
\delta\rangle$,

* $\Qstates$ is a finite set of states
ranged over by $q_1,q_2,\dots$

* $q_0\in\Qstates$ is an initial state

* $\Sigma$ is a finite set of characters ranged over
by $c_1,c_2,\dots$

* $\delta: \hat{\Sigma} \times \Qstates \times
\hat{\Sigma} \times \Bool \to \hat{\Sigma}
\times \{\mathtt{L},\mathtt{R}\}$ is a transition function describing
the new configuration reached by the machine.

$\mathtt{L}$ and $\mathtt{R}$ are two fixed and distinct symbols
(e.g. $\one$ and $\zero$),
$\hat{\Sigma}=\Sigma \cup\{\blank\}$
and $\blank\not\in\Sigma$ is the blank

The configuration of an STM
is a quadruple $\langle \str, q, \strT,\omega\rangle$,

* $\str\in\{\zero,\one,\blank\}^*$ is the portion
of the work tape
on the left of the head

* $q\in\Qstates$ is the current state of the machine

* $\strT \in\{\zero,\one,\blank\}^*$ is the portion
of the work tape on the right of the head

* $\omega\in \Bool^\Nat$ is the portion of the oracle
tape that has not been read yet.

We can now  give the definition of family of reachability
relations for an STM.

Given an STM $\STM$ with transition function $\delta$,
we use $\vdash_\delta$ to denote its standard step function
and $\{\triangleright^n_{\STM}\}_n$
the smallest family of relations such that:

\begin{align*}
\langle \str,q,\strT,\omega \rangle &\triangleright^0_{\STM}
\langle \str,q,\strT,\omega \rangle \\
\Big(\langle \str,q,\strT,\omega \rangle
\triangleright^n_{\STM} \langle \str',q,\strT',\omega'\rangle\Big)
\ \wedge  \ \ & \\
\Big(\langle \str',q',\strT',\omega'\rangle
\vdash_\delta
\langle \str'',q',\strT'', \omega''\rangle\Big)
\rightarrow \ &  \Big(
\langle \str, q,\strT,\omega\rangle
\triangleright^{n+1}_{\STM}
\langle \str'',q',\strT'', \omega''\rangle \Big)
\end{align*}

Given an STM $\STM=\langle \Qstates,
q_0,\Sigma,\delta\rangle$, oracle tape
$\omega : \Nat \to \Bool$ and a function
$g:\Nat \to \Bool$,
we say that $\STM$ computes g,
$f_{\STM}=g$, when for every string $\str\in\Ss$,
and oracle tape $\omega \in\Bool^\Nat$,
there are $n\in\Nat, \strT\in\Ss,q'\in\Qstates$,
and a function $\psi: \Nat \to \Bool$ such that

\langle \epsilon, q_0, \str, \omega\rangle
\triangleright^n_{\STM}
(\strTT, q', \strT, \psi\rangle,

and $\langle \strTT, q', \strT, \psi\rangle$
is a final configuration for $\STM$
with $f_{\STM}(\str,\omega)$ being the longest
suffix of $\strTT$ not including $\blank$.

§.§.§ Proof of Proposition <ref>

We need to extend this definition to
probability distributions over $\Ss$,
so to deal with PTMs.

Given a PTM $\PTM$,
a configuration $\langle \str, q,\strT\rangle$,
we define the following sequence of random

\begin{align*}
X^{\langle \str,q,\strT\rangle}_{\PTM,0} &\df
\omega \to \langle \str,q,\strT\rangle \\
X^{\langle \str,q,\strT\rangle}_{\PTM,n+1}
&\df \omega \to
\begin{cases}
\delta_{\bool}\big(X^{\langle \str,q,\strT\rangle}(\omega)\big)
&\text{if } \omega(n) = \bool \text{ and for some }
\langle \str',q',\strT'\rangle, \\
& \ \ \ \ \ \ \ \
\ \ \ \ \ \
\ \ \ \ \ \delta_\bool(X^{\langle \str,q,\strT\rangle}_{\PTM,n}
(\omega))= \langle \str',q',\strT'\rangle \\
X^{\langle \str,q,\strT\rangle}_{\PTM,n}(\omega)
&\text{if } \omega(n) = \bool \text{ and for no }
\langle \str',q',\strT'\rangle , \\
& \ \ \ \ \ \ \ \
\ \ \ \ \ \
\ \ \ \ \ \delta_\bool(X^{\langle \str,q,\strT\rangle}_{\PTM,n}
(\omega)) = \langle \str',q',\str'\rangle.
\end{cases}
\end{align*}

for any $\omega \in \Bool^\Nat$.

Intuitively, the variable $X^{\langle \str,q,\strT\rangle}_{\PTM,n}$
describes the configuration reached by the machine
after exactly $n$ transitions.

We say that a PTM $\PTM$ computes $Y_{\PTM,\str}$
when there is an $m\in \Nat$ such that
for any $\str\in\Ss$, $X^{\langle \str,q_0,\strT\rangle}_{\PTM,m}$
is final.

In this case, $Y_{\PTM,\str}$ is the longest suffix of
$\pi_1\Big(X^{\langle \str, q_0,\epsilon\rangle}_{\PTM,m}\Big)$,
which does not contain $\blank$.

We now prove Proposition <ref>,
which establishes the equivalence between STMs and PTMs.

[Equivalence between PTMs
and STMs]
For any poly-time STM $\STM$, there is a poly-time PTM
$\PTM^*$ such that for any strings $\str,\strT\in \Ss$,

\mu(\{\eta \ | \ \STM(\str,\omega)=\strT\}) = \Pr[\STM^*(\str)=
\strT],

and viceversa.

We show that for any $\str, \strT \in \Ss$,

\begin{align*}
\mu
\big(\{\omega \in \Bool^\Nat \ | \ \STM(\str,\omega)=\strT\}\big)
\mu
\big(\PTM(\str)^{-1} (\strT)\big) \\
\mu
\big(\{\omega \in \Bool^\Nat \ | \ \STM(\str,\omega)=\strT\}\big) &=
\mu
\big(\{\omega \in \Bool^\Nat \ | \ Y_{\STM,\str}(\omega)=\strT\}\big).
\end{align*}

We actually show a stronger result,
namely that there is a bijection $I$ : STMs $\to$
PTM such that for any $n\in\Nat$

\begin{align}
\{\omega \in \Bool^\Nat \ | \ \langle \str, q_0,\strT,\omega\rangle
\triangleright^n_\delta \langle
\strT, q,\psi,n\rangle\}
\{\omega \in \Bool^\Nat \ | \ X^{\langle \epsilon,q_0,\str\rangle}_{I(\STM),n}
(\omega) = \langle \strT,q,\psi\rangle\}.
\tag{I.}
\end{align}

This entails,

\begin{align}
\{\omega \in \Bool^\Nat \ | \ \STM(\str,\omega)=\strT\}
\{ \omega \in \Bool^\Nat
\ | \ Y_{I(\STM),\str}(\omega)=\strT\}.
\tag{II.}
\end{align}

The bijection $I$ splits the function $\delta$ of $\STM$
so that if the corresponding character on the oracle tape is $\zero$,
then the transition is defined by $\delta_0$;
if the character is $\one$, it is defined by $\delta_1$.

We prove (I.) by induction on the number of steps required by
$\STM$ to compute its input value.

§.§ From $\SFP$ to $\POR$

To prove Proposition <ref>
we show the correspondence between functions
computable by an STM and those computable by
a finite-stream STM.

For all $f\in \SFP$ with polynomial time-bound $p$

there is an $h\in\PTF$ such that,
for any $\omega \in \Bool^\Nat$ and $\str\in\Ss$,

f(\str,\eta)= h(\str,\omega_{p(|\str|)}).

Since $f\in\SFP$,
there is poly-time STM $\STM=\langle \Qstates,q_0,\Sigma,\delta\rangle$
such that $f=f_{\STM}$.

Let us consider the FSTM $\STM'$,
which is defined as $\STM$ but is finite.

Then for any $k\in\Nat$
and $\str', \strT',\strT'',\strT''' \in \Ss$,

\langle \epsilon,q_0',\str,\str'\rangle
\triangleright^k_{\STM} \langle \strT,q,\strT',\strT''\rangle \ \
\text{ iff } \ \
\langle\epsilon,q_0',\str,\str'\eta\rangle
\triangleright^k_{\STM'} \langle \strT,q,\strT'',\strT'''\eta\rangle.

Furthermore, $\STM'$ requires the same number
of steps as those required by $\STM$, so

is in $\PTF$ too.

We conclude the proof defining $h=f_{\PTM'}$.

The next step consists in showing that each function
$f\in\PTF$ corresponds to a function

which can be defined without recurring to $\query$.

For any $f\in\PTF$ and $\str\in\Ss$,
there is a $g\in\POR$ such that for any
$x,y\in \Ss$ and $\eta\in\Os$,
Furthermore, if $f$ is defined without recurring to
$g$ do not include $\query$ as well.

Let us outline the main steps of the proof:

* We define encodings using strings for configuration and
transition functions – called $e_c$ and $e_t$, respectively –
for FSTM.

Moreover, there is a function $step\in\POR$,
which satisfies the simulation schema in Figure <ref>.

Observe that $e_c,e_t$ and $step$ are correct
with respect to the given simulation.

[node distance = 8 cm]
at (-3.2,2) (c) $c = \langle \sigma, q, \tau, y\rangle$;
at (-3.2,0) (sc) $\str_c\in \Ss$;
at (3.2,2) (d) $d = \langle \sigma, q, \tau, y\rangle$;
at (3.2,0) (sd) $\str_d\in \Ss$;
at (0,2.3) $\vdash_{\delta}$;
at (-3.6,1) $e_c$;
at (3.6,1) $e_c$;
at (0,-0.3) for any $\eta\in\Os$, $step(\str_c, e_t(\delta), \eta)=\str_d$;

[->] (c) edge  (d);
[->] (sc) edge  (sd);
[->] (c) edge (sc);
[->] (d) edge (sd);

Behavior of $step$.

* For any $f\in\POR$ and $\str,\strT\in\Ss$,
if there is an $\rl$-term $t(x)$, which bounds the size
of $f(\str,\eta)$ for any possible input,
f_m=\lambda z,x,\eta^{|z|}(x,\eta)\in\POR.\footnote{Observe
that if
$f$ is defined without recurring to $\query$,
also $f_m$ can be defined without using it.}

* Given a machine $\STM$, if $\str\in\Ss$ is a correct
encoding for a configuration of $\STM$,
then for any $\eta\in\Os$ $|step(\str,\eta)|$
is $\mathcal{O}(|\str|)$.

* For any $\eta\in \Os$,
if $c=e_c(\str,q,\strT,y,\eta)$,
there is a function $dectape$ such that
is the longest suffix without occurrences of

Then, as a consequence of Lemma <ref>,
each function $f\in\SFP$ can be simulated
by a function $g\in\POR$ using
a polynomial prefix of the oracle for $f$
as an additional input.

For any $f\in\SFP$ and polynomial $p$,
there is a function $f\in\POR$, such that
for any $\omega\in \Bool^\Nat,$
$\eta\in\Os$ and $x\in\Ss$,

Assume $f\in\SFP$ and $y=\eta_{p(|x|)}$.
By Lemma <ref>,
there is a function $h\in\PTF$ such that
for any $\eta:\Nat\to \Bool$ and $x\in\Ss$,

Moreover, due to Lemma <ref>,
there is a $g\in\POR$ such that for any $x,y\in\Ss,\omega
\in \Os$,

Them $g$ is the desired function.

We now establish that there is a function $e\in\POR$,
which produces strings with the same distribution
of the prefixes of the functions in $\Ss^\Nat$.

Intuitively, this function extracts $|x|+1$ bits
from $\eta$ and concatenates them in the output.

The definition of $e$ passes through a dyadic representation of a number,
$dyad : \Nat \to \Ss$.

Therefore, the function $e$ creates
strings $\one^0,\one^1,\dots, \one^k$,
and samples the function $\eta$ on the given
coordinates –
$dy(\one^0),dy(\one^1),\dots, dy(\one^k)$ –
concatenating the result in a string.

The function $dyad : \Nat \to \Ss$ associates
each $n\in \Nat$ to the string obtained
by stripping the left-most bit from the binary representation
of $n+1$.

In order to define $dy(\cdot,\cdot)$,
some auxiliary functions are introduced,
namely $binsucc:\Ss\times \Os\to \Ss$,

\begin{align*}
binsucc(\epsilon,\eta) &\df \one \\
binsucc(x\zero,\eta) &\df x\one|_{x\zero\zero} \\
binsucc(x\one,\eta) &\df
\end{align*}

and $bin:\Ss\times \Os \to \Ss$,

\begin{align*}
bin(\epsilon,\eta) &\df \zero \\
bin(x\bool,\eta) &\df binsucc(bin(x,\eta),\eta)|_{x\bool}.
\end{align*}

The function $dy:\Ss\times \Os \to\Ss$ is defined as follows:

dy(x,\eta) \df  lrs(bin(x,\eta),\eta),

where $lrs$ is a string manipulator, which removes
the left-most bit from a string if it exists; otherwise returns
details can be found in [5].]

The function $dyad(n)$ is easily shown bijective
and the following proposition is proved by induction.

The function $dyad(n)$ is bijective.

* The function is an injection. different numbers
have different binary encodings and, for any
$n\in\Nat^+$ and $\omega\in\Os$,
$bin(n,\omega)$ has $\one$ as its left-most bit.[This is
proved by induction on $n$, leveraging the definition of $bin$.]

Given two distinct binary encodings of $n\neq m\in\Nat$,
say $\one\str$ and $\one\strT$,
then $\str\neq \strT$.[Otherwise $n=m$.
Indeed, the function associating numbers to binary representations
is itself a binjection.]

* The function is surjective.
It is computed by removing a bit, which is
always $\one$.
So, each string $\str\in\Ss$ is the image of
a number $n\in\Nat$ such that the binary encoding
of $n+1$ is $\one\str$.
This number always exists.

For any $n\in\Nat,\str\in\Ss$ and $\eta\in\Os$,
$|\str|=n+1$, then

We also introduce the function $e$ and prove its correctness
(by induction on the structure of strings).

Let $e:\Ss \times \Os \to \Ss$ be defined
as follows:

\begin{align*}
e(\epsilon,\eta) &\df \epsilon \\
e(x\bool,\eta) &\df e(x,\omega)\query(dy(x,\eta),
\eta)|_{x\bool}.
\end{align*}

For any $\str\in \Ss$ and $i\in\Nat$,
if $|\str|=i+1$,
for each $j\leq i\in \Nat$ and $\eta\in\Os$:

the length of $e(\str,\eta)$ is exactly

We also introduce a relation $\sim_{dy}$,
which is again a bijection.

We define $\sim_{dy}$ as the smallest relation
in $\Os \times \Bool^\Nat$ such that:

\eta \sim_{dy} \eta \ \ \text{iff} \ \
\text{ for any } n\in\Nat, \omega(n)=\eta(dy(\one^{n+1},
\omega)).

The relation $\sim_{dy}$ is a bijection.

By Proposition <ref>
and Lemma <ref>,
there is a $\omega\in\Os$
in relation with $\eta$.
Assume there is an $\omega'\neq \omega\in\Os$,
again in relation with $\eta$.
Then there is a $\str\in\Ss$, such that
$\omega(\str)\neq \omega'(\str)$.
By Proposition <ref>,
the value of $\omega$ does not affect the output.
Furthermore $dy$ is a bijection,
so there is an $n\in\Nat$ such that $dy(\one^{n+1},
\omega)=\str$ and
$\eta(n)=\omega_1(\str) \neq \omega_2(\str)=
\eta(n)$ is a contradiction.

The proof is the same when dealing with $\eta \in \Bool^\Nat$.

If $\omega \sim_{dy} \eta$
then, there is an $n\in\Nat$,

The proof is by contraposition.
Suppose $\omega_n\neq e(\underline{n}_\Nat,\eta)$.
As a consequence of Lemma <ref>,
there is an $m\in\Nat$ such that
$\omega(m)\neq \eta(dy(\underline{m}_\Nat,\eta))$,
which is a contradiction.

We can finally prove Proposition <ref>.

By Corollary <ref>,
there is a function $f'\in\POR$ and a polynomial
such that for any
$\str,\strT\in\Ss$, $\omega \in \Bool^\Nat$
and $\eta \in \Os$,

\begin{align}
\str= \omega_{p(x)} \rightarrow
\tag{$*$}
\end{align}

Let us fix $\overline{\omega}\in\{\omega\in\Bool^\Nat \ | \
its image with respect to $sim_{dy}$ is in
\{\eta \in \Os \ | \ f'(x,e(p'(s(x,\eta),\eta),
\eta),\eta)= \strT\},
where $s$ is the function of $\POR$ computing

By Lemma <ref>,

\overline{\omega}_{p(x)} = e(p(size(x,\eta),\eta),

where $p'\in \POR$
computes the polynomial $p$,
defined without recurring to $\query$.

Furthermore, given a fixed
$\overline{\eta} \in\{\eta \in \Os \ | \
f'(\str,e(p'(size(\str,\eta),\eta), \eta),\eta)=
\strT\}$,
its pre-image with respect to $\sim_{dy}
\in \{\omega\in\Bool^\Nat \ | \ f(\str,\omega)=\strT\}$.

The proof is analogous to the one above.

Since $\sim_{dy}$ is a bijection between

\mu(\{\omega\in\Bool^\Nat \ | \ f(\str,\omega)=\strT\})
\mu(\{\eta \in \Os | f'(x,e(p(size(x,\eta),
\eta),\eta),\eta) = \strT\}),

which concludes the proof.

§.§ From $\POR$ to $\SFP$

First, we define the imperative language
$\SIFPra$ together with its
big-step semantics,
and prove its poly-time programs equivalent
to $\POR$.

The language of programs of $\SIFPra$
$\LSra$ – i.e. the set of strings
produced by non-terminal symbol
$\prog{Stm}_{\text{RA}}$ – is defined
as follows:

\begin{align*}
\prog{Id} &\df X_i \midd Y_i \midd S_i \midd
R \midd Q \midd Z \midd T \\
\prog{Exp} &\df \epsilon \midd
\prog{Exp.0} \midd \prog{Exp.1} \midd
\prog{Id} \midd \prog{Exp} \sqsubseteq \prog{Id} \midd
\prog{Exp} \wedge \prog{Id} \midd
\neg \prog{Exp} \\
\prog{Stm}_{\text{RA}} &\df
\prog{Id} \leftarrow \prog{Exp} \midd
\prog{Stm}_{\text{RA}}; \prog{Stm}_{\text{RA}} \midd
\mathtt{while} (\prog{Exp}) \{\prog{Stm}\}_{\text{RA}} \midd
\mathtt{Flip}(\prog{Exp}),
\end{align*}

with $i\in\Nat$.

The big-step semantics associated with the language of $\SIFPra$
programs relies on the notion of store.

A store is a function
$\Sigma:\prog{Id} \rightharpoonup  \Ss$.

An empty store is a store which is total
and constant on $\progE$.

We represent such object as $[ \ ]$.
We define the updating of a store $\Sigma$
with a mapping from $y\in\prog{Id}$ to $\str\in \Ss$

\Sigma[y\leftarrow \str](x) \df \begin{cases}
\str \ &\text{if } x=y \\
\Sigma(x) \ &\text{otherwise.}
\end{cases}

The semantics of an expression $E\in\mathcal{L}(\prog{Exp})$
is the smallest relation
$\rightharpoonup : \mathcal{L}(\prog{Exp})
\times (\prog{Id} \to \Ss) \times \Os \times
\Ss$ closed under the following rules:

$\langle \progE,\Sigma\rangle
\rightharpoonup \eepsilon$

$\langle e,\Sigma\rangle \rightharpoonup
\str$
$\langle e.\prog{b},\Sigma\rangle
\rightharpoonup \str \conc \bool$

$\langle e,\Sigma\rangle
\rightharpoonup \str$
$\str\subseteq \strT$
$\langle e\sqsubseteq \prog{Id},
\Sigma\rangle \rightharpoonup \one$

$\langle e,\Sigma\rangle
\rightharpoonup \str$
$\str \not\subseteq \strT$
$\langle e\sqsubseteq \prog{Id},
\Sigma\rangle \rightharpoonup \zero$

$\langle \prog{Id},\Sigma\rangle
\rightharpoonup \str$

$\prog{Id} \not \in dom(\Sigma)$
$\langle \prog{Id},\Sigma\rangle
\rightharpoonup \eepsilon$

$\langle e,\Sigma\rangle \rightharpoonup
\progZ$
$\langle \neg e,\Sigma\rangle
\rightharpoonup \one$

$\langle e,\Sigma\rangle \rightharpoonup\str$
$\sigma \neq\zero$
$\langle \neg e,\Sigma\rangle
\rightharpoonup \zero$

$\langle e,\Sigma\rangle \rightharpoonup
\one$
$\langle e\wedge \prog{Id},\Sigma\rangle
\rightharpoonup \one$

$\langle e,\Sigma \rangle \rightharpoonup
\str$
$\str\neq \one \wedge
\strT \neq \one$
$\langle e \wedge \prog{Id},\Sigma\rangle
\rightharpoonup \zero$

where $\prog{b}\in \{\prog{0},\prog{1}\}$.[We assume that
if $\prog{b}=\prog{1}$, then $\bool =\one$,
and if $\prog{b}=\prog{0}$, then $\bool=\zero$.]

The semantics of a program $\prog{P} \in\LSra$ is the smallest
relation $\triangleright \subseteq \LSra \times
(\prog{Id} \to \Ss)
\times \Os \times (\prog{Id} \to \Ss)$
closed under the following rules:

$\langle e,\Sigma\rangle \rightharpoonup
\str$
$\langle \prog{Id} \rightharpoonup
e,\Sigma,\eta\rangle \triangleright
\Sigma[\prog{Id} \leftarrow \str]$

$\langle s,\Sigma,\eta\rangle
\triangleright \Sigma'$
$\langle t,\Sigma',\eta\rangle
\triangleright \Sigma''$
$\langle s;t,\Sigma,\eta\rangle
\triangleright \Sigma''$

$\langle e,\Sigma \rangle \rightharpoonup
\one$
$\langle s,\Sigma,\eta\rangle
\triangleright \Sigma'$
$\langle \mathtt{while}(e)\{s\},
\Sigma',\eta\rangle \triangleright \Sigma''$
$\langle \mathtt{while}(e)\{s\},
\Sigma, \eta\rangle \triangleright \Sigma''$

$\langle e,\Sigma \rangle \rightharpoonup
\str $
$\str \neq \one$
$\langle \mathtt{while}(e)\{s\},
\Sigma,\eta\rangle \triangleright \Sigma$

$\langle e,\Sigma\rangle \rightharpoonup
\str$
$\langle \mathtt{Flip}(e),\Sigma,\eta\rangle
\triangleright \Sigma[R\leftarrow \bool]$

The semantics allows us to associate each
program of $\SIFPra$ to the function
it evaluates:

Function evaluation
by a correct $\SIFPra$ program $\prog{P}$
is $\model{\cdot} : \LSra \to (\Ss^n \times \Os
\to \Ss)$ defined as below:[Instead
of the infixed notation for $\triangleright$,
we use its prefixed notation.
So, the notation express the store associated
to the $P$,
$\Sigma$ and $\omega$ by $\triangleright$.

Moreover, we employ the same function symbol
$\triangleright$ to denote two distinct functions:
the big-step operational semantics of $\SIFPra$
and the big-step operational semantics
of programs in $\SIFPla$.]

\model{\prog{P}} \df \lambda x_1,\dots, x_n,\eta
\triangleright (\langle \prog{P}, [ \ ] [X_1 \leftarrow x_1],
\dots, [X_n \leftarrow x_n],\eta\rangle )

Observe that, among the different registers,
the register $R$ is meant to contain
the value computed by the program at the
end of its execution.

Similarly, the $\{X_i\}_{i\in\Nat}$ registers
are used to store the inputs of the function.

We now establish the correspondence beteween
$\POR$ and $\SIFPra$.

For any function $f\in\POR$,
there is a poly-time $\SIFPra$ program
$\prog{P}$ such that
for all $x_1,\dots, x_n$,

\model{\prog{P}}(x_1,\dots, x_n,\omega)=f(x_1,\dots,

Moreover, if $f\in\POR$, then
$\prog{P}$ does not contain any $\mathtt{Flip}(e)$

The proof is quite simple under a technical
relying on the fact that it is possible
to associate to any function of $\POR$
an equivalent poly-time program,
and on the possibility to compose them
and implement bounded recursion on notation
in $\SIFPra$ with a polynomial overhead.

Concretely, for any function $f\in\POR$,
we define a program $\mathscr{L}_f$
such that $\model{\mathscr{L}_f}(x_1,\dots, x_n)
= f(x_1,\dots, x_n)$.

The correctness of $\mathscr{L}_f$ is given
by the following invariant properties:

* the result of the computation is stored in

* inputs are stored in the registers of the group

* the function $\mathscr{L}$ does not
the values it accesses as input.

We define $\mathscr{L}_f$
as follows:

\begin{align*}
\mathscr{L}_E &= R \leftarrow \epsilon \\
\mathscr{L}_{S_0} &= R \leftarrow X_0.\prog{0} \\
\mathscr{L}_{S_1} &= R \leftarrow X_0.\prog{1} \\
\mathscr{L}_{P^n_i} &= R \leftarrow X_i \\
\mathscr{L}_C &= R \leftarrow X_1 \sqsubseteq X_2 \\
\mathscr{L}{\query} &= \mathtt{Flip}(X_1).
\end{align*}

The correctness of base cases is trivial to prove
and the only translation containing
$\mathtt{Flip}(e)$ for some
$e\in \mathcal{L}(\prog{Exp})$ is that of $\query$.

The encoding of composition and bounded
recursion are more convoluted.[The
proof of their correctness requires a conspicuous amount of
low-level definitions and technical results.
For an extensive presentation, see [5].]

§.§.§ From $\SIFPra$ to $\SIFPla$

We now show that every program in $\SIFPra$
is equivalent to one in $\SIFPla$.

First, we need to define the language and semantics
for $\SIFPla$.

The language of $\SIFPla$ $\LSla$,
that is the set of strings produced by non-terminal
symbols $\prog{Stm}_{\text{LA}}$, is defined as follows:

\prog{Stm}_{\text{LA}} \df \prog{Id} \leftarrow \prog{Exp} \midd
\prog{Stm}_{\text{LA}} ; \prog{Stm}_{\text{LA}} \midd
\mathtt{while}(\prog{Exp})\{\prog{Stm}\}_{\text{LA}} \midd
\mathtt{RandBit}().

The semantics of a program $\prog{P}\in\LSla$ is the smallest relation
$\triangleright \subseteq (\LSla \times (\prog{Id} \to
\Ss \times \Bool^\Nat) \times
((\prog{Id} \to \Ss \times \Bool^\Nat)$
closed under the following rules:

$\langle e,\Sigma\rangle \rightharpoonup \str$
$\langle \prog{Id} \leftarrow e,\Sigma,\omega\rangle
\triangleright \langle \Sigma[\prog{Id}\leftarrow \str],\omega\rangle$

$\langle s,\Sigma,\omega\rangle \triangleright
\langle \Sigma',\omega'\rangle$
$\langle t,\Sigma',\omega\rangle \triangleright
\langle \Sigma'',\omega''\rangle$
$\langle s;t,\Sigma,\omega\rangle \triangleright
\langle \Sigma'',\omega''\rangle$

$\langle e,\Sigma\rangle \rightharpoonup
\one$
$\langle s,\Sigma,\omega\rangle \triangleright
\langle \Sigma',\omega'\rangle$
$\langle \mathtt{while}(e) \{s\}, \Sigma',\omega\rangle
\triangleright \langle \Sigma'',\omega''\rangle$
$\langle \mathtt{while}(e)\{s\},
\Sigma,\omega\rangle \triangleright \langle \Sigma',\omega''\rangle$

$\langle e,\Sigma\rangle \rightharpoonup \str$
$\str\neq \one$
$\langle \mathtt{while}(e)\{s\},\Sigma,\omega\rangle
\triangleright \langle \Sigma, \omega\rangle$

$\langle \mathtt{RandBit}(), \Sigma,
\bool \omega\rangle \triangleright
\langle\Sigma[R\leftarrow \bool],\omega\rangle$

For each total program $\prog{P}\in \SIFPra$,
there is a $\query\in \SIFPla$ such that,
for any $x,y\in \Nat$,

\mu(\{\omega \in \Os \ | \ \model{\prog{P}}(x,\eta)=y\})
= \mu(\{\omega \in \Bool^\Nat \ | \
\model{\query}(x,\eta)=y\}).

Moreover, if $\prog{P}$ is poly-time $\query$, too.

We prove Lemma <ref>
showing that $\SIFPra$ can be simulated in
$\SIFPla$ given two novel small-step semantic relations
($\toLA,\toRA$) obtained by splitting the corresponding
big-step semantics into smallest transitions,
one per each $\cdot \ ; \ \cdot$ instruction.

The intuitive idea behind this novel semantics
is to enrich big-step operational semantics with some piece
of information, which are needed to build
an induction proof of the reduction from
$\SIFPra$ to $\SIFPla$.

In particular, we employ a list $\Psi$ containing
pairs $(x,\prog{b})$,
to keep track of the previous call to the primitive
$\Flip(x)$ forv $\SIFPra$,
and to the result of the $x$-th call of
primitive $\mathtt{RandBit}()$ for $\SIFPla$.

The main issue
consists in the simulation of the access to the
random tape.

Then, we define the translation so that
it stores in a specific and fresh register
an associative table recording all queries
$\str$ within a $\Flip(\str)$ instruction and
the result b
picked from $\eta$ and returned.

The addition of the map $\Psi$ allows
to replicate the content of the associative table $\Psi$
explicitly in the semantics of program.

This simulation requires a translation of
$\Flip(e)$ into an equivalent procedure.

* at each simulated query $\Flip(e)$,
the destination program looks up the associative

* if it finds the queried coordinate $e$ within
a pair $(e,\prog{b})$, it returns $\prog{b}$.

Otherwise, (i)
it reduced $\Flip(e)$ to a call of
$\mathtt{RandBit}()$ which outputs either $\bool=\zero$
or $\bool=\one$,
(ii) it records the couple $\langle e,\bool\rangle$
in the associative table and returns $\bool$.

The construction is convoluted.
This kind of simulation preserves the distributions
of strings computed by the original program:

* we show that the big-step and small-step
semantics for $\SIFPra$ and $\SIFPla$ are
equally expressive.

* we define a relation $\Theta$ between configurations of
the small-step semantics  of $\SIFPra$
and $\SIFPla$:

$*$ first, we define a function
$\alpha:\LSra \to \LSla$ mapping the program
$\prog{P}_{\text{RA}} \in \LSra$ into the corresponding
$\prog{P}_{\text{LA}}\in\LSla$, translating
$\Flip(e)$ as described above.

$*$ we define a relation $\beta$ between a triple
$\langle \prog{P}_{\text{RA}},\Sigma,\Psi\rangle$ and a single
store $\Gamma$,
which is meat to capture the configuration-to -store
dependencies between the configuration
of $\prog{P}_{\text{RA}}$ running with store $\Sigma$
and computed associative table $\Psi$
and the store $\Gamma$ of simulating $\prog{P}_{\text{LA}}$.

So, $\Gamma$ stores a representation of $\Psi$
into a dedicated register.

$*$ a function $\gamma$ which transforms the constraints
on the oracle gathered by $\toRA$ to the information
collected by $\toLA$.
Then, $\Theta$ is so defined that $
\Theta(\langle \prog{P},\Sigma_1,\Psi\rangle, \langle \query,
\Sigma_2,\Theta\rangle)$ holds when:
(i.) $\alpha(\prog{P})=\query$, (ii.) $\beta(\langle
\prog{P},\Sigma_1,\Psi\rangle,
\Sigma_2)$,
(iii.) $\gamma(\Psi)=\Phi$,
(iv.) $\mu(\Psi)=\mu(\Phi)$.

* we show that $\Theta$ associates to
each triple $\langle \prog{P}_{\text{RA}},\Sigma, \Psi\rangle$
other triples
$\langle \prog{P}_{\text{LA}},\Gamma,\Phi\rangle$
which weakly simulate the relation $\toRA$ with respect
to $\toLA$.
This is displayed by Figure <ref>.

[node distance=5cm]
(PRA) at (-3,2) $\langle P_{\text{RA}};Q_{\text{RA}}, \Sigma, \Psi\rangle$;
(PLA) at (-3,-0) $\langle P_{\text{LA}};Q_{\text{LA}}, \Gamma, \Phi\rangle$;
(P1RA) at (3,2) $\langle Q_{\text{RA}}, \Sigma', \Psi'\rangle$;
(P1LA) at (3,0) $^*\langle Q_{\text{LA}}, \Gamma', \Phi'\rangle$;
at (-3.3,1) $\Theta$;
at (3.3,1) $\Theta$;

[->,densely dashed,thick] (PRA) to (P1RA);
[->,densely dashed,thick] (PLA) to (P1LA);
[->] (PRA) to (PLA);
[->] (P1RA) to (P1LA);

Commutation schema between $\SIFPra$ and $\SIFPla$

§.§.§ From $\SIFPla$ to $\SFP_{\text{OD}}$

We introduce $\SFP_{\text{OD}}$,
the class corresponding to $\SFP$ defined
on a variation of STMs which can read characters from the oracle
and show that $\SIFPla$ can be reduced to it.

For readability's sake, we avoid cumbersome details,
focussing on an informal (but exhaustive) description
of how to build the on-demand STM.

For every $\prog{P}\in\LSla$, there is a $\STM^{\prog{P}} \in \SFP$
such that for any $x\in\Ss$ and
$\omega \in\Bool^\Nat$,

\prog{P}(x,\omega)=\STM^{\prog{P}}(x,\omega).

Moreover, if $\prog{P}$ is poly-time, then $\STM^\prog{P}$ is also

The construction relies on the implementation of a
program in $\SIFPla$ by a multi-tape on-demand STM
which uses a tape to store the values of each register,
plus an additional tape containing the partial results
obtained during the evaluation
of the expressions and another tape containing $\omega$.

We denote the tape used for storing the
result coming from the evaluation of the expression with $e$.

The following invariant properties holds:

* on each tape, values are stored to the immediate
right of the head,

* the result of the last expression evaluated is stored
on tape $e$ to the immediate right of the head.

The value of expressions of $\SIFP$ can be computed
using the tape $e$.[In particular we prove this by induction
on the syntax of expressions. (1)

each access to the value stored in a register
consists in a copy of the content
of the corresponding tape to $e$, which is a simple operation
(due to the invariant properties above)
concatenations – namely $f.\prog{0}$ and
$f.\prog{1}$ – are implemented by the addition of a character
at the end of $e$, which contains the value of $f$.
(3) the binary expressions are non-trivial.
Since one of the two operands is a register identifier,
the machine can directly compare $e$ with the tape,
corresponding to the identifier, and to replace the content
of $e$ with the result of the comparison,
which in all cases is $\zero$ or $\one$.
Further details can be found in [5].]

All operations can be implemented without consuming any
character on the oracle tape
and with linear time with respect to the
size of the value of the expression.

We assign a sequence of machine states,
$q^I_{s_1},q_{s_i}^1,\dots, q_{s_i}^F$,
to each statement $s_i$.

* assignments consist in copies of the value in $e$
to the tape corresponding to the destination register
and delations of the value on $e$, as replaced by $\blank$.

This is implemented without consuming any character on
the oracle tape.

* The sequencing operation $s;t$ is implemented
inserting a composed transition from $q_s^F$ to $q_t^I$
in $\delta$.
This does not consume the oracle tape.

* a $\mathtt{while}()$ statement $s=\mathtt{while}(f)\{t\}$

In particular, the statement $\mathtt{RandBit}()$ is implemented consuming
a character on the tape and copying its value on the tape
which corresponds to the register $R$.

Furthermore, if we assume $\prog{P}$ to be poly-time,
after the simulation of each statement,
it holds that:

* the length of the non-blank portion of the first tapes
corresponding to the register is polynomially bounded
as their contents are precisely the the contents of
$\prog{P}$'s registers, which are polynomially bounded as a consequence
of the hypotheses of their poly-time complexity,

* the head of all the tapes corresponding to the registers
point to the left-most symbol of the string thereby contained.

It is well-known that the reduction of the number of tapes
on a poly-time TM comes with a polynomial overhead in time.
For this reason, we conclude that the poly-time multi-tape
on-demand STM can be
reduced to a poly-time canonical on-demand STM.

This concludes our proof.

It remains to show that each on-demand STM can be reduced
to an equivalent STM.

For every $\STM =\langle \Qstates, \Sigma, \delta,q_0\rangle
\in \SFP_{\text{OD}}$,
the machine $\STM'=\langle \Qstates, \Sigma, H(\delta), q_0\rangle
\in \SFP$ is such that for every $n\in\Nat$
and configuration of $\STM$ $\langle \str,q,\strT,\eta\rangle$,
and for every $\str',\strT'\in\Ss,q\in\Qstates$,
\mu(\{\omega \in \Bool^\Nat \ | \ (\exists \omega')\langle\str,q,\strT,\omega\rangle
\triangleright^n_\delta \langle \str',q',\strT',\omega'\rangle\})$
$\mu(\{\xi \in \Bool^\Nat \ | \ (\exists \xi')
\langle \str,q,\strT,\xi\rangle \triangleright^n_{H(\delta)}
\langle \str',q',\strT',\xi'\rangle \}).$

Even in this case, the proof relies on a reduction.
In particular, we show that given an on-demand STM,
it is possible to build an STM, which is equivalent
to the former.

Intuitively, the encoding from an on-demand STM to an ordinary
STM takes the transition function $\delta$ of the STM
and substitutes each transition not causing the oracle tape to shift
– i.e. tagged with $\natural$ – with two distinct transitions,
where $\natural$ is substituted by $\zero$ and $\one$, respectively.

This causes the resulting machine to produce an identical transition but
shifting the head on the oracle tape on the right.

We also define an encoding from an on-demand STM
to a canonical STM as follows:

H \df \langle \Qstates, \Sigma, \delta, q_0\rangle \to
\big\langle \Qstates, \Sigma, \bigcup \Delta_H(\delta), q_0\big\rangle.

where $\Delta_H$ is,

\begin{align*}
\Delta_H\big(\langle p, c_r,\zero,q,c_w,d\rangle\big) &\df
\{\langle p,c_r, \zero, q,c_w,d\rangle\} \\
\Delta_H\big(\langle p,c_r,\one,q,c_w,d\rangle\big) &\df
\{\langle p,c_r,\one,q,c_w,d\rangle\} \\
\Delta_H \big(\langle p,c_r,\natural, q,c_w,d\rangle\big) &\df
\{\langle p, c_r,\zero, q,c_w,d\rangle,
\langle p,c_r,\one,q,c_w,d\rangle\}.
\end{align*}

§.§.§ From $\POR$ to $\SFP$

We then conclude the proof relating $\POR$ and $\SFP$.

For any $f:\Ss^k\times \Os \to \Ss \in\POR$,
there is a function $f^\star : \Ss^k\times \Bool^\Nat \to \Ss$
such that for all $\str_1,\dots, \str_k,\strT\in \Ss$,

\mu\big(\{\omega \in \Bool^\Nat \ | \ f(\str_1,\dots, \str_k,\omega)=\strT\}\big) =
\mu\big(\{\eta \in \Os \ | \ f^\star(\str_1,\dots,\str_k,\eta)=\strT\}\big).

It is a straightforward consequence of Lemma <ref>, Lemma <ref>, Proposition <ref>,
and Lemma <ref>.