# On Higher-Order Probabilistic Subrecursion
(Long Version)††thanks: The authors are partially supported by ANR project
14CE250005 ELICA and ANR project 12IS02001 PACE.

Flavien Breuvart  Ugo Dal Lago  Agathe Herrou

###### Abstract

We study the expressive power of subrecursive probabilistic higher-order
calculi. More specifically, we show that endowing a very expressive
deterministic calculus like Gödel’s $\mathbb{T}$ with various forms of
probabilistic choice operators may result in calculi which are not equivalent
as for the class of distributions they give rise to, although they all
guarantee _almost-sure_ termination. Along the way, we introduce a
probabilistic variation of the classic reducibility technique, and we prove
that the simplest form of probabilistic choice leaves the expressive power of
$\mathbb{T}$ essentially unaltered. The paper ends with some observations
about functional expressivity: expectedly, all the considered calculi
represent precisely the functions which $\mathbb{T}$ itself represents.

##  1 Introduction

Probabilistic models are more and more pervasive in computer science and are
among the most powerful modeling tools in many areas like computer vision
[20], machine learning [19] and natural language processing [17]. Since the
early times of computation theory [8], the very concept of an algorithm has
been itself generalised from a purely deterministic process to one in which
certain elementary computation steps can have a probabilistic outcome. This
has further stimulated research in computation and complexity theory [11], but
also in programming languages [21].

Endowing programs with probabilistic primitives (e.g. an operator which models
sampling from a distribution) poses a challenge to programming language
semantics. Already for a minimal, imperative probabilistic programming
language, giving a denotational semantics is nontrivial [16]. When languages
also have higher-order constructs, everything becomes even harder [14] to the
point of disrupting much of the beautiful theory known in the deterministic
case [1]. This has stimulated research on denotational semantics of higher-
order probabilistic programming languages, with some surprising positive
results coming out recently [9, 4].

Not much is known about the expressive power of _probabilistic_ higher-order
calculi, as opposed to the extensive literature on the same subject about
_deterministic_ calculi (see, e.g. [24, 23]). What happens to the class of
representable functions if one enrich, say, a deterministic $\lambda$-calculus
$\mathbb{X}$ with certain probabilistic choice primitives? Are the expressive
power or the good properties of $\mathbb{X}$ somehow preserved? These
questions have been given answers in the case in which $\mathbb{X}$ is the
pure, untyped, $\lambda$-calculus [6]: in that case, univesality continues to
hold, mimicking what happens in Turing machines [22]. But what if $\mathbb{X}$
is one of the many typed $\lambda$-calculi ensuring strong normalisation for
typed terms [12]?

But let us do a step back, first: when should a higher-order probabilistic
program be considered terminating? The question can be given a satisfactory
answer being inspired by, e.g., recent works on probabilistic termination in
imperative languages and term rewrite systems [18, 2]: one could ask the
probability of divergence to be $0$, called _almost sure termination_
property, or the stronger _positive almost sure termination_ , in which one
requires the average number of evaluation steps to be finite. That termination
is desirable property, even in a probabilistic setting can be seen, e.g. in
the field of languages like Church and Anglican, in which programs are often
assumed to be almost surely terminating, e.g. when doing inference by MH
algorithms [13].

In this paper, we initiate a study on the expressive power of terminating
higher-order calculi, in particular those obtained by endowing Gödel’s
$\mathbb{T}$ with various forms of probabilistic choice operators. In
particular, three operators will be analyzed in this paper:

  * •

A binary probabilistic operator $\oplus$ such that for every pair of terms
$M,N$, the term $M\oplus N$ evaluates to either $M$ or $N$, each with
probability $\frac{1}{2}$. This is a rather minimal option, which, however,
guarantees universality if applied to the untyped $\lambda$-calculus [6] (and,
more generally, to universal models of computation [22]).

  * •

A combinator ${\mathtt{R}}$, which evaluates to any natural number $n\geq 0$
with probability $\frac{1}{2^{n+1}}$. This is the natural generalization of
$\oplus$ to sampling from a distribution having _countable_ rather than
_finite_ support. This apparently harmless generalization (which is absolutely
non-problematic in a universal setting) has dramatic consequences in a
subrecursive scenario, as we will discover soon.

  * •

A combinator ${\mathtt{X}}$ such that for every pair of values $V,W$, the term
${\mathtt{X}}\,V\,W$ evaluates to either $W$ or $V({\mathtt{X}}\,V\,W)$, each
with probability $\frac{1}{2}$. The operator ${\mathtt{X}}$ can be seen as a
probabilistic variation on $\mathbb{PCF}$’s fixpoint combinator. As such,
${\mathtt{X}}$ is potentially problematic to termination, giving rise to
infinite trees.

This way, various calculi can be obtained, like $\mathbb{T}^{\oplus}$, namely
a minimal extension of $\mathbb{T}$, or the full calculus
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$, in which the three operators
are all available. In principle, the only obvious fact about the expressive
power of the above mentioned operators is that both ${\mathtt{R}}$ and
${\mathtt{X}}$ are at least as expressive as $\oplus$: binary choice can be
easily expressed by either ${\mathtt{R}}$ or ${\mathtt{X}}$. Less obvious but
still easy to prove is the equivalence between ${\mathtt{R}}$ and
${\mathtt{X}}$ in presence of a recursive operator (see Section 3.4). But how
about, say, $\mathbb{T}^{\oplus}$ vs. $\mathbb{T}^{{\mathtt{R}}}$?

Traditionally, the expressivities of such languages are compared by looking at
the set of functions $f:\mathbb{N}\rightarrow\mathbb{N}$ defined by typable
programs $M:\mathtt{NAT}\rightarrow\mathtt{NAT}$. However, in probabilistic
setting, programs $M:\mathtt{NAT}\rightarrow\mathtt{NAT}$ computes functions
from natural numbers into _distributions_ of natural numbers. In order to fit
usual criterions, we need to fix a notion of observation. There are at least
two relevant notions of observations, corresponding to two randomised
programming paradigms, namely _Las Vegas_ and _Monte Carlo_ observations. The
main question, then, consists in understanding how the obtained classes relate
to each other, and to the class of $\mathbb{T}$-representable functions. Along
the way, however, we manage to understand how to capture the expressive power
of probabilistic calculi _per se_. This paper’s contributions can be
summarised as follows:

  * •

We first take a look at the full calculus
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$, and prove that it enforces
almost-sure termination, namely that the probability of termination of any
typable term is $1$. This is done by appropriately adapting the well-known
reducibility technique [12] to a probabilistic operational semantics. We then
observe that while $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ cannot be
_positively_ almost surely terminating, $\mathbb{T}^{\oplus}$ indeed is. This
already shows that there must be a gap in expressivity. This is done in
Section 3.

  * •

In Section 4, we look more precisely at the expressive power of
$\mathbb{T}^{\oplus}$, proving that the mere presence of probabilistic choice
does not add much to the expressive power of $\mathbb{T}$: in a sense,
probabilistic choice can be “lifted up” to the ambient deterministic calculus.

  * •

We look at other fragments of $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$
and at their expressivity. More specifically, we will prove that (the
equiexpressive) $\mathbb{T}^{{\mathtt{R}}}$ and $\mathbb{T}^{{\mathtt{X}}}$
represent precisely what $\mathbb{T}^{\oplus}$ can do _at the limit_ , in a
sense which will be made precise in Section 3. This part, which is the most
challenging, is done in Section 5.

  * •

Section 6 is devoted to proving that both for _Monte Carlo_ and for _Las
Vegas_ observations, the class of representable functions of
$\mathbb{T}^{{\mathtt{R}}}$ coincides with the $\mathbb{T}$-representable
ones.

##  2 Probabilistic Choice Operators, Informally

Any term of Gödel’s $\mathbb{T}$ can be seen as a purely deterministic
computational object whose dynamics is finitary, due to the well-known strong
normalization theorem (see, e.g., [12]). In particular, the apparent non-
determinism due to multiple redex occurrences is completely harmless because
of confluence. In this paper, indeed, we even neglect this problem, and work
with a reduction strategy, namely weak call-by-value reduction (keeping in
mind that all what we will say also holds in call-by-name). Evaluation of a
$\mathbb{T}$-term $M$ of type $\mathtt{NAT}$ can be seen as a finite sequence
of terms ending in the normal form $\boldsymbol{n}$ of $M$ (see Figure 4).
More generally, the unique normal form of any term $\mathbb{T}$ term $M$ will
be denoted as $\left\llbracket M\right\rrbracket$. Noticeably, $\mathbb{T}$ is
computationally very powerful. In particular, the $\mathbb{T}$-representable
functions from $\mathbb{N}$ to $\mathbb{N}$ coincide with the functions which
are provably total in Peano’s arithmetic [12].

As we already mentioned, the most natural way to enrich deterministic calculi
and turn them into probabilistic ones consists in endowing their syntax with
one or more probabilistic choice operators. Operationally, each of them models
the essentially stochastic process of sampling from a distribution and
proceeding depending on the outcome. Of course, one has many options here as
for _which_ of the various operators to grab. The aim of this work is
precisely to study to which extend this choice have consequences on the
overall expressive power of the underlying calculus.

Suppose, for example, that $\mathbb{T}$ is endowed with the binary
probabilistic choice operator $\oplus$ described in the Introduction, whose
evaluation corresponds to tossing a fair coin and choosing one of the two
arguments accordingly. The presence of $\oplus$ has indeed an impact on the
dynamics of the underlying calculus: the evaluation of any term $M$ is not
deterministic anymore, but can be modeled as a finitely branching tree (see,
e.g. Figure 4 for such a tree when $M$ is
$(\boldsymbol{3}\oplus\boldsymbol{4})\oplus\boldsymbol{2}\>$). The fact that
all branches of this tree have finite height (and the tree is thus finite) is
intuitive, and a proof of it can be given by adapting the well-known
reducibility proof of termination for $\mathbb{T}$. In this paper, we in fact
prove much more, and establish that $\mathbb{T}^{\oplus}$ can be embedded into
$\mathbb{T}$.

If $\oplus$ is replaced by ${\mathtt{R}}$, the underlying tree is not finitely
branching anymore, but, again, there is not (at least apparently) any
infinitely long branch, since each of them can somehow be seen as a
$\mathbb{T}$ computation (see Figure 4 for an example). What happens to the
expressive power of the obtained calculus? Intuition tells us that the
calculus should not be too expressive viz. $\mathbb{T}^{\oplus}$. If $\oplus$
is replaced by ${\mathtt{X}}$, on the other hand, the underlying tree _is_
finitely branching, but its height can well be infinite. Actually,
${\mathtt{X}}$ and ${\mathtt{R}}$ are easily shown to be equiexpressive in
presence of higher-order recursion, as we show in Section 3.4. On the other
hand, for ${\mathtt{R}}$ and $\oplus$, no such encoding is available.
Nonetheless, $\mathbb{T}^{{\mathtt{R}}}$ can still be somehow encoded embedded
into $\mathbb{T}$ (just that we need an infinite structure) as we will detail
in Section 5. From this embeding, we can show that applying Monte Carlo or Las
Vegas algorithm on $\mathbb{T}^{\oplus,{\mathtt{X}},{\mathtt{R}}}$ results do
not add any expressive power to $\mathbb{T}$, This is done in Section 6.

$M\rightarrow\cdots\rightarrow\boldsymbol{n}$
${\mathtt{R}}$$\boldsymbol{0}$$\boldsymbol{1}$$\boldsymbol{2}$$\boldsymbol{3}$$\boldsymbol{4}$$\frac{1}{2}\
\ \ \phantom{.}$$\frac{1}{4_{\vphantom{1}}}$$\frac{1}{8}\phantom{.}$$\
\frac{1}{16}$ Figure 1: A Reduction in $\mathbb{T}$ Figure 2:
A Reduction in $\mathbb{T}^{{\mathtt{R}}}$
$(\boldsymbol{3}\oplus\boldsymbol{4})\oplus\boldsymbol{2}$$\boldsymbol{3}\oplus\boldsymbol{4}$$\boldsymbol{2}$$\boldsymbol{3}$$\boldsymbol{4}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$
Figure 3:
A Reduction in $\mathbb{T}^{\oplus}$ ${\mathtt{X}}\ {\mathtt{S}}\
\boldsymbol{3}$$\boldsymbol{3}$${\mathtt{S}}({\mathtt{X}}\ {\mathtt{S}}\
\boldsymbol{3})$$\boldsymbol{4}$${\mathtt{S}}{\mathtt{S}}({\mathtt{X}}\
{\mathtt{S}}\
\boldsymbol{3})$$\boldsymbol{5}$$\ddots$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$
Figure 4:
A Reduction in $\mathbb{T}^{{\mathtt{X}}}$

##  3 The Full Calculus $\mathbb{T}^{\oplus,\mathtt{R},\mathtt{X}}$

All along this paper, we work with a calculus
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ whose _terms_ are the ones
generated by the following grammar:

$\displaystyle M,N,L\ ::=\ $ $\displaystyle
x\;\;\mbox{\Large{$\mid$}}\;\;\lambda x.M\;\;\mbox{\Large{$\mid$}}\;\;M\
N\;\;\mbox{\Large{$\mid$}}\;\;\langle
M,N\rangle\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{\pi}}_{1}\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{\pi}}_{2}\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{rec}}\;\;\mbox{\Large{$\mid$}}\;\;\boldsymbol{0}\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{S}}\;\;\mbox{\Large{$\mid$}}\;\;M\oplus
N\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{R}}\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{X}}.$

Please observe the presence of the usual constructs from the untyped
$\lambda$-calculus, but also of primitive recursion, constants for natural
numbers, pairs, and the three choice operators we have described in the
previous sections.

As usual, terms are taken modulo $\alpha$-equivalence. Terms in which no
variable occurs free are, as usual, dubbed _closed_ , and are collected in the
set $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{C}$. A _value_ is simply a
closed term from the following grammar

$\displaystyle U,V\ ::=\ $ $\displaystyle\lambda
x.M\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{\pi}}_{1}\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{\pi}}_{2}\;\;\mbox{\Large{$\mid$}}\;\;\langle
U,V\rangle\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{rec}}\;\;\mbox{\Large{$\mid$}}\;\;\boldsymbol{0}\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{S}}\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{S}}\
V\;\;\mbox{\Large{$\mid$}}\;\;{\mathtt{X}},$

and the set of values is $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V}$.
_Extended values_ are (not necessarily closed) terms generated by the same
grammar as values with the addition of variables. Closed terms that are not
values are called _reducible_ and their set is denoted
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{R}$. A _context_ is a term
with a unique hole:

$C:=\llparenthesis\cdot\rrparenthesis\;\;\mbox{\Large{$\mid$}}\;\;\lambda
x.C\;\;\mbox{\Large{$\mid$}}\;\;C\ M\;\;\mbox{\Large{$\mid$}}\;\;M\
C\;\;\mbox{\Large{$\mid$}}\;\;\langle
C,M\rangle\;\;\mbox{\Large{$\mid$}}\;\;\langle
M,C\rangle\;\;\mbox{\Large{$\mid$}}\;\;C\oplus
M\;\;\mbox{\Large{$\mid$}}\;\;M\oplus C$

We write
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{\llparenthesis\cdot\rrparenthesis}$
for the set of all such contexts.

Termination of Gödel’s $\mathbb{T}$ is guaranteed by the presence of types,
which we also need here. _Types_ are expressions generated by the following
grammar

$A,B::=\mathtt{NAT}\;\;\mbox{\Large{$\mid$}}\;\;A\rightarrow
B\;\;\mbox{\Large{$\mid$}}\;\;A\times B.$

_Environmental contexts_ are expressions of the form
$\Gamma=x_{1}\mathop{:}A_{1},\ldots,x_{n}\mathop{:}A_{n}$, while _typing
judgments_ are of the form $\Gamma\vdash M\mathop{:}A$. _Typing rules_ are
given in Figure 5. From now on, only typable terms will be considered. We
denote by $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}(A)$ the set of terms
of type $A$, and similarly for
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{C}(A)$ and
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V}(A)$.

$\Gamma,x\mathop{:}A\vdash x\mathop{:}A$ $\Gamma,x\mathop{:}A\vdash M:B$
$\Gamma\vdash\lambda x.M:A\rightarrow B$ $\Gamma\vdash M:A\rightarrow B$
$\Gamma\vdash N:A$ $\Gamma\vdash M\ N:B$
$\Gamma\vdash\boldsymbol{0}:\mathtt{NAT}$
$\Gamma\vdash{\mathtt{S}}:\mathtt{NAT}\rightarrow\mathtt{NAT}$
$\Gamma\vdash{\mathtt{rec}}:(A\times(\mathtt{NAT}\rightarrow A\rightarrow
A)\times\mathtt{NAT})\rightarrow A$ $\Gamma\vdash M:A$ $\Gamma\vdash N:B$
$\Gamma\vdash\langle M,N\rangle:A\times B$
$\Gamma\vdash{\mathtt{\pi}}_{1}:(A\times B)\rightarrow A$
$\Gamma\vdash{\mathtt{\pi}}_{2}:(A\times B)\rightarrow B$ $\Gamma\vdash M:A$
$\Gamma\vdash N:A$ $\Gamma\vdash M\oplus N:A$
$\Gamma\vdash{\mathtt{R}}:\mathtt{NAT}$
$\Gamma\vdash{\mathtt{X}}:(A\rightarrow A)\times A\rightarrow A$ Figure 5:
Typing Rules.

We use the shortcut $\boldsymbol{n}$ for values of type $\mathtt{NAT}$:
$\boldsymbol{0}$ is already part of the language of terms, while
$\boldsymbol{n+1}$ is simply ${\mathtt{S}}\ \boldsymbol{n}$. For simplicity of
notations, we also denote ${\mathtt{S}}{\mathtt{S}}$ for $\lambda
x.{\mathtt{S}}({\mathtt{S}}\ x)$; we do the same for
${\mathtt{S}}{\mathtt{S}}{\mathtt{S}}$…

###  3.1 Operational Semantics

While evaluating terms in a deterministic calculus ends up in a _value_ , the
same process leads to a _distribution_ of values when performed on terms in a
probabilistic calculus. Keep in mind that despite speaking of distribution, we
are only treating countable distributions and not continuous one, which is
much simpler. Formalizing all this requires some care, but can be done
following one of the many definitions from the literature (e.g., [6]).

Given a countable set $X$, a _distribution $\mathcal{L}$ on $X$_ is a
probabilistic (sub)distribution over elements of $X$:

$\mathcal{L},\mathcal{M},\mathcal{N}\in\mathfrak{D}(X)=\Bigl{\\{}f:X\rightarrow[0,1]\Bigm{|}\sum_{x\in
X}f(x)\leq 1\Bigr{\\}}$

We are especially concerned with distributions over terms here. In particular,
a _distribution of type $A$_ is simply an element of
$\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}(A))$. The set
$\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V})$ is ranged
over by metavariables like $\mathcal{U},\mathcal{V},\mathcal{W}$. We will use
the pointwise order $\leq$ on distributions, which turns them into an
$\omega\boldsymbol{CPO}$. Moreover, we use the following notation for Dirac’s
distributions over terms: $\\{M\\}:=\left\\{\begin{matrix}M\mapsto
1\phantom{\text{ if }M\neq N}\\\ N\mapsto 0\text{ if }M\neq
N\end{matrix}\right\\}$. The support of a distribution is indicated as
$\left|\mathcal{M}\right|$; we also define the reducible and value supports
fragments as
$\left|\mathcal{M}\right|_{R}:=\left|\mathcal{M}\right|\cap\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{R}$
and
$\left|\mathcal{M}\right|_{V}:=\left|\mathcal{M}\right|\cap\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V}$.
Notions like $\mathcal{M}^{R}$ and $\mathcal{M}^{V}$ have an obvious and
natural meaning: for any $\mathcal{M}\in\mathfrak{D}(X)$ and $Y\subseteq X$,
then $\mathcal{M}^{Y}(x)=\mathcal{M}(x)$ if $x\in Y$ and
$\mathcal{M}^{Y}(x)=0$ otherwise.

As syntactic sugar, we use integral notations to manipulate distributions,
i.e., for any family of distributions
$(\mathcal{N}_{M})_{M\in\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}}:\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}})^{\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}}$,
the expression $\int_{\mathcal{M}}\mathcal{N}_{M}.dM$ stands for

$\int_{\mathcal{M}}\mathcal{N}_{M}.dM\ :=\
\sum_{M\in\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}}\mathcal{M}(M)\cdot\mathcal{N}_{M}.$

y abuse of notation, we may define $\mathcal{N}_{M}$ only for
$M\in|\mathcal{M}|$, since the others are not used anyway.

######  Example 1.

Suppose that $\mathcal{M}=\\{\boldsymbol{n}\mapsto\frac{1}{2^{n+1}}\mid
n\in\mathbb{N}\\}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}(\mathtt{NAT}))$
is the exponential distribution over the natural numbers. Suppose, moreover
that for any $n$,
$\mathcal{N}_{\boldsymbol{n}}=\left\\{\begin{matrix}\boldsymbol{n+1}&\mapsto\frac{1}{2}\\\
\boldsymbol{0}&\mapsto\frac{1}{2}\end{matrix}\right\\}$ gives as value either
$n+1$ or $0$ with uniform probability. Then

$\displaystyle\int_{\mathcal{M}}\mathcal{N}_{M}.dM$
$\displaystyle=\sum_{n}\frac{1}{2^{n+1}}\cdot\left\\{\begin{matrix}\boldsymbol{n+1}&\mapsto\frac{1}{2}\\\\[1.00006pt]
\boldsymbol{0}&\mapsto\frac{1}{2}\end{matrix}\right\\}$
$\displaystyle=\left\\{\begin{matrix}\boldsymbol{n+1}&\mapsto&\frac{1}{2^{n+1}}\cdot\frac{1}{2}&\text{
for }n\in\mathbb{N}\\\\[1.00006pt]
\boldsymbol{0}&\mapsto&\sum_{m}\frac{1}{2^{m+1}}\end{matrix}\right\\}$
$\displaystyle=\\{\boldsymbol{n}\mapsto\frac{1}{2^{n+1}}\mid
n\in\mathbb{N}\\}$

which is exactly the same as $\mathcal{M}$.

The notation can be easily adapted, e.g., to families of real numbers
$(p_{M})_{M\in\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}}$ and to other
kinds of distributions. We indicate as
$C\llparenthesis\mathcal{M}\rrparenthesis$ the push-forward distribution
$\int_{\mathcal{M}}\\{C\llparenthesis M\rrparenthesis\\}dM$ induced by a
context $C$, and as $||\mathcal{M}||$ the norm $\int_{\mathcal{M}}1dM$ of
$\mathcal{M}$. Remark, finally, that we have the useful equality
$\mathcal{M}=\int_{\mathcal{M}}\\{M\\}dM$. The integral can be manipulated as
usual integrals which respect the less usual equation:

$\displaystyle\int_{\left(\int_{\mathcal{M}}\mathcal{N}_{M}dM\right)}\mathcal{L}_{N}dN$
$\displaystyle=$
$\displaystyle\int_{\mathcal{M}}\left(\int_{\mathcal{N}_{M}}\mathcal{L}_{N}dN\right)dM$
(1)

Reduction rules of $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ are given
by Figure 6.

M $(r\text{-}\beta)$ $(\lambda x.M)\ V\rightarrow\Bigl{\\{}M[V/x]\Bigr{\\}}$
$M\rightarrow\mathcal{M}$ $(r\text{-}@L)$ $M\ V\rightarrow\mathcal{M}\
V\vphantom{\Bigl{\\{}}$ $N\rightarrow\mathcal{N}$ $(r\text{-}@R)$ $M\
N\rightarrow M\ \mathcal{N}\vphantom{\Bigl{\\{}}$ $M\rightarrow\mathcal{M}$
$(r\text{-}\langle\cdot\rangle L)$ $\langle
M,N\rangle\rightarrow\langle\mathcal{M},N\rangle\vphantom{\Bigl{\\{}}$
$M\rightarrow\mathcal{M}$ $(r\text{-}\langle\cdot\rangle R)$ $\langle
V,M\rangle\rightarrow\langle V,\mathcal{M}\rangle\vphantom{\Bigl{\\{}}$
$(r\text{-}{\mathtt{rec}}\boldsymbol{0})$ ${\mathtt{rec}}\langle
U,V,\boldsymbol{0}\rangle\rightarrow\Bigl{\\{}U\Bigr{\\}}$
$(r\text{-}{\mathtt{rec}}{\mathtt{S}})$ ${\mathtt{rec}}\langle
U,V,{\mathtt{S}}\ \boldsymbol{n}\rangle\rightarrow\Bigl{\\{}V\ \boldsymbol{n}\
({\mathtt{rec}}\langle U,V,\boldsymbol{n}\rangle)\Bigr{\\}}$
$(r\text{-}{\mathtt{\pi}}_{1}$) ${\mathtt{\pi}}_{1}\ \langle
V,U\rangle\rightarrow\Bigl{\\{}V\Bigr{\\}}$ ($r\text{-}{\mathtt{\pi}}_{2})$
${\mathtt{\pi}}_{2}\ \langle V,U\rangle\rightarrow\Bigl{\\{}U\Bigr{\\}}$
$(r\text{-}{\mathtt{R}})$
${\mathtt{R}}\rightarrow\Bigl{\\{}\boldsymbol{n}\mapsto\frac{1}{2^{n+1}}\Bigr{\\}}_{n\in\mathbb{N}}\\!\\!\\!\\!\\!$
$(r\text{-}\oplus)$ $M\oplus
N\rightarrow\left\\{\begin{matrix}M&\mapsto&\frac{1}{2}\\\
N&\mapsto&\frac{1}{2}\end{matrix}\right\\}$ $(r\text{-}{\mathtt{X}})$
${\mathtt{X}}\langle V,W\rangle\rightarrow\left\\{\begin{matrix}V\
({\mathtt{X}}\;\langle V,W\rangle)&\mapsto&\frac{1}{2}\\\
W&\mapsto&\frac{1}{2}\end{matrix}\right\\}$ $\forall
M\in\left|\mathcal{M}\right|_{R},\ M\rightarrow\mathcal{N}_{M}$ $\forall
V\in\left|\mathcal{M}\right|_{V},\ \mathcal{N}_{V}=\\{V\\}$ $(r\text{-}{\in})$
$\mathcal{M}\rightarrow\int_{\mathcal{M}}\mathcal{N}_{M}.dM$ Figure 6:
Operational Semantics.

For simplicity, we use the notation $M\rightarrow^{?}\mathcal{M}$ for
$\\{M\\}\rightarrow\mathcal{M}$, i.e., $M\rightarrow\mathcal{M}$ whenever $M$
is reducible and $\mathcal{M}=\\{M\\}$ whenever $M$ is a value. The notation
permit to rewrite rule $(r\text{-}{\in})$ as a monadic lifting:

$\forall M\in\left|\mathcal{M}\right|,\ M\rightarrow^{?}\mathcal{N}_{M}$
$(r\text{-}{\in})$
$\mathcal{M}\rightarrow\int_{\mathcal{M}}\mathcal{N}_{M}.dM$

######  Example 2.

First, notice that we can simulate any reduction of the usual system
$\mathbb{T}$. For example, take the following term:

$\boldsymbol{\mathtt{Expo}}\ :=\ \lambda n.{\mathtt{rec}}\
\langle\boldsymbol{2}\>,\>\lambda xy.{\mathtt{rec}}\
\langle\boldsymbol{0},\lambda
x.{\mathtt{S}}{\mathtt{S}},y\rangle\>,\>{\mathtt{S}}n\rangle\quad:\
\mathtt{NAT}\rightarrow\mathtt{NAT}$

This term is computing the function $n\mapsto 2^{n+1}$ in time $\sim 2^{n+1}$.
Indeed, when applied to a natural number $\boldsymbol{n}$, it will get the
following reduction where we denote $E_{k}:={\mathtt{rec}}\
\langle\boldsymbol{1}\>,\>\lambda xy.{\mathtt{rec}}\
\langle\boldsymbol{0},\lambda
x.{\mathtt{S}}{\mathtt{S}},y\rangle\>,\>\boldsymbol{k}\rangle$:

$\displaystyle\left(\lambda n.{\mathtt{rec}}\
\langle\boldsymbol{1}\>,\>\lambda xy.{\mathtt{rec}}\
\langle\boldsymbol{0},\lambda
x.{\mathtt{S}}{\mathtt{S}},y\rangle\>,\>{\mathtt{S}}n\rangle\right)\
\boldsymbol{n}$ $\displaystyle\rightarrow\ $
$\displaystyle\Bigl{\\{}E_{n+1}\Bigr{\\}}$ $\displaystyle\rightarrow\ $
$\displaystyle\Bigl{\\{}(\lambda xy.{\mathtt{rec}}\
\langle\boldsymbol{0},\lambda x.{\mathtt{S}}{\mathtt{S}},y\rangle)\
\boldsymbol{n}\ E_{n}\Bigr{\\}}$ $\displaystyle\rightarrow\ $
$\displaystyle\Bigl{\\{}(\lambda y.{\mathtt{rec}}\
\langle\boldsymbol{0},\lambda x.{\mathtt{S}}{\mathtt{S}},y\rangle)\
E_{n}\Bigr{\\}}$ $\displaystyle\rightarrow\ $
$\displaystyle\Bigl{\\{}{\mathtt{rec}}\ \langle\boldsymbol{0},\lambda
x.{\mathtt{S}}{\mathtt{S}},E_{n}\rangle\Bigr{\\}}$ $\displaystyle\cdots$
$\displaystyle\rightarrow\ $ $\displaystyle\Bigl{\\{}{\mathtt{rec}}\
\langle\boldsymbol{0},\lambda
x.{\mathtt{S}}{\mathtt{S}},\boldsymbol{2^{n}}\rangle\Bigr{\\}}$
$\displaystyle\rightarrow\ $ $\displaystyle\Bigl{\\{}(\lambda
x.{\mathtt{S}}{\mathtt{S}})\ (\boldsymbol{2^{n}{-}1})({\mathtt{rec}}\
\langle\boldsymbol{0},\lambda
x.{\mathtt{S}}{\mathtt{S}},\boldsymbol{2^{n}{-}1}\rangle)\Bigr{\\}}$
$\displaystyle\rightarrow\ $
$\displaystyle\Bigl{\\{}{\mathtt{S}}{\mathtt{S}}({\mathtt{rec}}\
\langle\boldsymbol{0},\lambda
x.{\mathtt{S}}{\mathtt{S}},\boldsymbol{2^{n}{-}1}\rangle)\Bigr{\\}}$
$\displaystyle\cdots$ $\displaystyle\rightarrow\ $
$\displaystyle\Bigl{\\{}\boldsymbol{2^{n+1}}\Bigr{\\}}$

Remark that we are only considering Diracs here; this is because the reduction
is completely determinist: there is no probabilistic choice involved.

######  Example 3.

As a second example, we are presenting the term
${\mathtt{X}}\langle{\mathtt{S}},\boldsymbol{0}\rangle$ that is essentially
reduced by probabilistic derivations:

$\displaystyle{\mathtt{X}}\langle{\mathtt{S}},\boldsymbol{0}\rangle$
$\displaystyle\rightarrow\left\\{\begin{matrix}{\mathtt{S}}\
({\mathtt{X}}\;\langle{\mathtt{S}},\boldsymbol{0}\rangle)&\mapsto&\frac{1}{2}\\\\[1.00006pt]
\boldsymbol{0}&\mapsto&\frac{1}{2}\end{matrix}\right\\}$
$\displaystyle\rightarrow\left\\{\begin{matrix}{\mathtt{S}}{\mathtt{S}}\
({\mathtt{X}}\;\langle{\mathtt{S}},\boldsymbol{0}\rangle)&\mapsto&\frac{1}{4}\\\\[1.00006pt]
\boldsymbol{1}&\mapsto&\frac{1}{4}\\\
\boldsymbol{0}&\mapsto&\frac{1}{2}\end{matrix}\right\\}$
$\displaystyle\rightarrow\left\\{\begin{matrix}{\mathtt{S}}{\mathtt{S}}{\mathtt{S}}\
({\mathtt{X}}\;\langle{\mathtt{S}},\boldsymbol{0}\rangle)&\mapsto&\frac{1}{8}\\\\[1.00006pt]
\boldsymbol{2}&\mapsto&\frac{1}{8}\\\ \boldsymbol{1}&\mapsto&\frac{1}{4}\\\
\boldsymbol{0}&\mapsto&\frac{1}{2}\end{matrix}\right\\}$
$\displaystyle\rightarrow\cdots$

Notice that the reduction $\rightarrow$ (resp. $\rightarrow^{?}$) is
deterministic. We can easily define $\rightarrow^{n}$ (resp.
$\rightarrow^{\leq n}$) as the $n^{th}$ exponentiation of $\rightarrow$ (resp.
$\rightarrow^{?}$) and $\rightarrow^{*}$ as the reflexive and transitive
closure of $\rightarrow$ (and $\rightarrow^{?}$). In probabilistic systems, we
might want to consider infinite reductions such as the ones induced by
${\mathtt{X}}\ (\lambda x.x)\ \boldsymbol{0}$ which reduces to
$\\{\boldsymbol{0}\\}$, but in an infinite number of steps. Remark that for
any value $V$, and whenever $\mathcal{M}\rightarrow\mathcal{N}$, it holds that
$\mathcal{M}(V)\leq\mathcal{N}(V)$. As a consequence, we can proceed as
follows:

######  Definition 4.

Let $M$ be a term and let $(\mathcal{M}_{n})_{n\in\mathbb{N}}$ be the unique
distribution family such that $M\rightarrow^{\leq n}\mathcal{M}_{n}$. The
_evaluation_ of $M$ is the value distribution

$\left\llbracket
M\right\rrbracket:=\\{V\mapsto\lim_{n\rightarrow\infty}\mathcal{M}_{n}(V)\\}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V}).$

The _success_ of $\mathcal{M}$ is its probability of normalization, which is
formally defined as the norm of its evaluation, i.e.,
$Succ(M):=||\left\llbracket M\right\rrbracket||$. $\mathcal{M}^{\Delta V}_{n}$
stands for $\\{V\mapsto\mathcal{M}_{n}(V)-\mathcal{M}_{n-1}(V)\\}$, the
distributions of values reachable in exactly $n$ steps. The _average reduction
length_ from $M$ is then

$[M]\ :=\ \sum_{n}\left(n\cdot||\mathcal{M}^{\Delta V}_{n}||\right)\quad\in\
\mathbb{N}\cup\\{+\infty\\}$

######  Example 5.

Take as example the term
${\mathtt{X}}\langle{\mathtt{S}},\boldsymbol{0}\rangle$ of example 3. We have,
for all $n$:

${\mathtt{X}}\langle{\mathtt{S}},\boldsymbol{0}\rangle\rightarrow^{n}\mathcal{M}_{n}=\left\\{\begin{matrix}{\mathtt{S}}^{n}\
({\mathtt{X}}\;\langle{\mathtt{S}},\boldsymbol{0}\rangle)&\mapsto&\frac{1}{2^{n}}\\\\[1.00006pt]
\boldsymbol{i}&\mapsto&\frac{1}{2^{i+1}}&\text{for }i<n\end{matrix}\right\\}\
,$

so that $\mathcal{M}_{n}(\boldsymbol{i})=\boldsymbol{0}$ if $i\geq n$ and
$\mathcal{M}_{n}(\boldsymbol{i})=\frac{1}{2^{i+1}}$ otherwise. Thus:

$\displaystyle\left\llbracket{\mathtt{X}}\langle{\mathtt{S}},\boldsymbol{0}\rangle\right\rrbracket$
$\displaystyle=\left\\{\boldsymbol{n}\mapsto\lim_{n\rightarrow\infty}\mathcal{M}_{n}(\boldsymbol{n})\
\middle|\ n\in\mathbb{N}\right\\}$
$\displaystyle=\left\\{\boldsymbol{n}\mapsto\frac{1}{2^{n+1}}\ \middle|\
n\in\mathbb{N}\right\\}$

Notice that, by Rule $(r\text{-}\in)$, the evaluation is continuous:

$\left\llbracket\mathcal{M}\right\rrbracket=\int_{\mathcal{M}}\left\llbracket
M\right\rrbracket dM.$

Any term $M$ of type $\mathtt{NAT}\rightarrow\mathtt{NAT}$ _represents_ a
function $g:\mathbb{N}\rightarrow\mathfrak{D}(\mathbb{N})$ iff for every $m,n$
it holds that $g(n)(m)=\left\llbracket
M\;\boldsymbol{n}\right\rrbracket(\boldsymbol{m})$.

###  3.2 Technical Properties Of The Operational Semantics

Before giving the main results, some auxiliary lemmas are necessary. In
particular, we are looking for Lemma 10 which is a fundamental continuity
lemma stating that it is equivalent to apply a call by value strategy at the
level of distributions, provided that we allow infinite reductions.

The first lemma is stating that the (one step) reduction of a sum (or an
integral) is the sum (or the integral) of all the addends. Of course, the
different reductions of the addends can have interpolations which makes the
decomposition nontrivial:

######  Lemma 6.

If it exist, the reduction $\mathcal{L}$ of any integral
$\int_{\mathcal{M}}\mathcal{N}_{M}dM\rightarrow\mathcal{L}$, is the integral
$\int_{\mathcal{M}}\mathcal{L}_{M}dM$ such that
$\mathcal{N}_{M}\rightarrow\mathcal{L}_{M}$ for any
$M\in\left|\mathcal{M}\right|$.

###### Proof.

  * •

Let $(\mathcal{L}_{M})_{M\in\left|\mathcal{M}\right|}$ such that
$\mathcal{N}_{M}\rightarrow\mathcal{L}_{M}$ for any
$M\in\left|\mathcal{M}\right|$. Then in order to derive
$\mathcal{N}_{M}\rightarrow\mathcal{L}_{M}$, the only rule we can apply is
$(r\text{-}{\in})$ so that there is
$(\mathcal{L}^{\prime}_{M,N})_{M\in\left|\mathcal{M}\right|,N\in\left|\mathcal{N}_{M}\right|}$
such that $\mathcal{L}_{M}=\int_{\mathcal{N}_{M}}\mathcal{L}^{\prime}_{M,N}dN$
and $N\rightarrow^{?}\mathcal{L}^{\prime}_{M,N}$. Notice that for
$N\in\left|\mathcal{N}_{M}\right|\cap\left|\mathcal{N}_{M^{\prime}}\right|$,
the determinism of $\rightarrow^{?}$ gives that
$\mathcal{L}^{\prime}_{M,N}=\mathcal{L}^{\prime}_{M^{\prime},N}$, thus we can
define $\mathcal{L}^{\prime}_{N}$ without ambiguity for any
$N\in\bigcup_{M\in\left|\mathcal{M}\right|}\left|\mathcal{N}_{M}\right|=\left|\int_{\mathcal{M}}\mathcal{N}_{M}dM\right|$.
Then we have $N\rightarrow^{?}\mathcal{L}^{\prime}_{N}$ and
$\int_{\int_{\mathcal{M}}\mathcal{N}_{M}dM}\mathcal{L}^{\prime}_{N}dN=\int_{\mathcal{M}}\left(\int_{\mathcal{N}_{M}}\mathcal{L}^{\prime}_{N}dN\right)dM=\int_{\mathcal{M}}\mathcal{L}_{M}dM$
(we use Eq (1)). Thus, by applying rule $(r\text{-}{\in})$ we get
$\int_{\mathcal{M}}\mathcal{N}_{M}dM\rightarrow\int_{\mathcal{M}}\mathcal{L}_{M}dM$.

  * •

Conversely, we assume that
$\int_{\mathcal{M}}\mathcal{N}_{M}dM\rightarrow\mathcal{L}$. In order to
derive it, the only rule we can apply is $(r\text{-}{\in})$ so that there is
$(\mathcal{L}^{\prime}_{N})_{N\in\left|\int_{\mathcal{M}}\mathcal{N}_{M}dM\right|}$
such that
$\mathcal{L}=\int_{\left(\int_{\mathcal{M}}\mathcal{N}_{M}dM\right)}\mathcal{L}^{\prime}_{N}dN=\int_{\mathcal{M}}\left(\int_{\mathcal{N}_{M}}\mathcal{L}^{\prime}_{N}dN\right)dM$
and $N\rightarrow^{?}\mathcal{L}^{\prime}_{N}$. We conclude by setting
$\mathcal{L}_{M}:=\int_{\mathcal{N}_{M}}\mathcal{L}^{\prime}_{N}dN$.

∎

This decomposition is off course iterable to any lengths of reduction:

######  Lemma 7.

The $n^{th}$ reductions $\mathcal{L}$ of any integral
$\int_{\mathcal{M}}\mathcal{N}_{M}dM\rightarrow^{n}\mathcal{L}$, is (if it
exists) the integral $\int_{\mathcal{M}}\mathcal{L}_{M}dM$ such that
$\mathcal{N}_{M}\rightarrow^{n}\mathcal{L}_{M}$ for any
$M\in\left|\mathcal{M}\right|$.

###### Proof.

By induction on $n$:

  * •

If $n=0$ then $\mathcal{L}_{M}=\mathcal{N}$.

  * •

Otherwise,
$\int_{\mathcal{M}}\mathcal{N}_{M}dM\rightarrow\mathcal{L}^{\prime}\rightarrow^{n-1}\mathcal{L}$.
By Lemma 6, the first step is possible iff
$\mathcal{L}^{\prime}=\int_{\mathcal{M}}\mathcal{L}^{\prime}_{M}dM$ with
$\mathcal{N}_{M}\rightarrow\mathcal{L}^{\prime}_{M}$ for any
$M\in\left|\mathcal{M}\right|$. By IH, the remaining steps are then possible
iff $\mathcal{L}=\int_{\mathcal{M}}\mathcal{L}_{M}dM$ such that
$\mathcal{L}^{\prime}_{M}\rightarrow^{n-1}\mathcal{L}_{M}$ for any
$M\in\left|\mathcal{M}\right|$.

∎

Conversely, it is possible to track back values obtained from an application
as an application of values obtained from reducing both applicants.

######  Lemma 8.

If $(M\ N)\rightarrow^{n}\mathcal{L}\geq\mathcal{W}$ for some
$\mathcal{W}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V})$,
then there is
$\mathcal{U},\mathcal{V}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V})$
such that

$\displaystyle M$ $\displaystyle\rightarrow^{*}\mathcal{M}\geq\mathcal{U},$
$\displaystyle N$ $\displaystyle\rightarrow^{*}\mathcal{N}\geq\mathcal{V},$
$\displaystyle(\mathcal{U}\ \mathcal{V})$
$\displaystyle\rightarrow^{*}\mathcal{L}^{\prime}\geq\mathcal{W}.$

###### Proof.

By induction on $n$.
Trivial if $n=0$.
If $n\geq 1$, we proceed differently depending whether $M$ and $N$ are values
or not.

  * •

If $N$ is not a value then $N\rightarrow\mathcal{N}^{\prime}$ and $(M\
N)\rightarrow(M\
\mathcal{N}^{\prime})\rightarrow^{n-1}\mathcal{L}\geq\mathcal{W}$.
Notice that $(M\ \mathcal{N}^{\prime}):=\int_{\mathcal{N}^{\prime}}\\{M\
N^{\prime}\\}dN^{\prime}$. Using Lemma 7, we can decompose
$\mathcal{W}=\int_{\mathcal{N}^{\prime}}\mathcal{W}_{N^{\prime}}dN^{\prime}$
and
$\mathcal{L}=\int_{\mathcal{N}^{\prime}}\mathcal{L}_{N^{\prime}}dN^{\prime}$
in such a way that for any $N^{\prime}\in\left|\mathcal{N}^{\prime}\right|$,
$(M\ N^{\prime})\rightarrow^{\leq
n-1}\mathcal{L}_{N^{\prime}}\geq\mathcal{W}_{N^{\prime}}$. By induction we
have
$N^{\prime}\rightarrow^{*}\mathcal{N}_{N^{\prime}}\geq\mathcal{V}_{N^{\prime}}$
and $M\rightarrow^{*}\mathcal{M}_{N^{\prime}}\geq\mathcal{U}_{N^{\prime}}$
with $(\mathcal{U}_{N^{\prime}}\
\mathcal{V}_{N^{\prime}})\rightarrow^{*}\mathcal{L}^{\prime}_{N^{\prime}}\geq\mathcal{W}_{N^{\prime}}$
for all $N^{\prime}\in\left|\mathcal{N}^{\prime}\right|$. Summing up we have
$\mathcal{M}:=\int_{\mathcal{N}^{\prime}}\mathcal{M}_{N^{\prime}}dN^{\prime}$,
$\mathcal{U}:=\int_{\mathcal{N}^{\prime}}\mathcal{U}_{N^{\prime}}dN^{\prime}$,
$\mathcal{N}:=\int_{\mathcal{N}^{\prime}}\mathcal{N}_{N^{\prime}}dN^{\prime}$
and
$\mathcal{V}:=\int_{\mathcal{N}^{\prime}}\mathcal{V}_{N^{\prime}}dN^{\prime}$.

  * •

If $N$ is a value and $M\rightarrow\mathcal{M}^{\prime}$ then $(M\
N)\rightarrow(\mathcal{M}^{\prime}\
N)\rightarrow^{n-1}\mathcal{L}\geq\mathcal{W}$. Thus we can decompose the
equation similarly along $\mathcal{M}^{\prime}$ and apply our IH.

  * •

If both $M$ and $N$ are values it is trivial since $\mathcal{U}=\\{M\\}$ and
$\mathcal{V}=\\{N\\}$.

∎

######  Lemma 9.

For every $m,n\in\mathbb{N}$ and every
$\mathcal{M},\mathcal{N}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}})$,
whenever $M\rightarrow^{m}\mathcal{M}$ and
$N\rightarrow^{n}\mathcal{N}\geq\mathcal{V}$, we have $\left\llbracket M\
N\right\rrbracket\geq\left\llbracket\mathcal{M}\ \mathcal{V}\right\rrbracket$.
In particular, if moreover $\mathcal{M}\geq\mathcal{U}$, then $\left\llbracket
M\ N\right\rrbracket\geq\left\llbracket\mathcal{U}\
\mathcal{V}\right\rrbracket$.

###### Proof.

By induction on $m+n$.
Trivial if $m+n=0$.
If $n\geq 1$, we proceed differently depending whether $M$ and $N$ are values
or not.

  * •

If $N\rightarrow\mathcal{L}\rightarrow^{n-1}\mathcal{N}\geq\mathcal{V}$ then
$N$ is not a value.
Using Lemma 7, we can decompose
$\mathcal{N}=\int_{\mathcal{L}}\mathcal{N}_{L}dL$ and
$\mathcal{V}=\int_{\mathcal{L}}\mathcal{V}_{L}dL$ in such a way that for any
$L\in\left|\mathcal{L}\right|$, $L\rightarrow^{\leq
n-1}\mathcal{N}_{L}\geq\mathcal{V}_{L}$ (with $\rightarrow^{\leq n-1}$ dubbing
either $=$ or $\rightarrow^{n-1}$ depending whether $L$ is a value or not).
Then we get

$\left\llbracket M\ N\right\rrbracket=\left\llbracket M\
\mathcal{L}\right\rrbracket=\int_{\mathcal{L}}\left\llbracket M\
L\right\rrbracket dL\geq\int_{\mathcal{L}}\left\llbracket\mathcal{M}\
\mathcal{V}_{L}\right\rrbracket dL=\left\llbracket\mathcal{M}\
\left(\int_{\mathcal{L}}\mathcal{V}_{L}dL\right)\right\rrbracket=\left\llbracket\mathcal{M}\
\mathcal{V}\right\rrbracket\ .$

  * •

If $\mathcal{V}$ is the empty (sub)distribution, this is trivial.

  * •

If $n=0$ and $\mathcal{V}$ is not empty, then $\mathcal{V}=\\{N\\}$, thus $N$
is a value and $M\rightarrow\mathcal{L}\rightarrow^{m-1}\mathcal{M}$, then we
can decompose the equation similarly along $\mathcal{L}$ and apply our IH.

∎

The following is a crucial intermediate step towards Theorem 12, the main
result of this section.

######  Lemma 10.

For any $M,N$: $\left\llbracket M\
N\right\rrbracket=\left\llbracket\left\llbracket M\right\rrbracket\
\left\llbracket N\right\rrbracket\right\rrbracket$. In particular, if the
application $M\ N$ is almost-surely terminating, so are $M$ and $N$.

###### Proof.

$(\leq)\ $ There is $(\mathcal{L}_{n},\mathcal{W}_{n})_{n\geq 1}$ such that
$(M\ N)\rightarrow^{n}\mathcal{L}_{n}\geq\mathcal{W}_{n}$ for all $n$ and such
that $\left\llbracket M\ N\right\rrbracket=\lim_{n}(\mathcal{W}_{n})$.
Applying Lemma 8 gives
$\mathcal{M}_{n},\>\mathcal{N}_{n},\>\mathcal{L}^{\prime}_{n}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}})$
and
$\mathcal{U}_{n},\mathcal{V}_{n}\>{\in}\>\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V})$
such that $M\rightarrow^{*}\mathcal{M}_{n}\geq\mathcal{U}_{n}$,
$N\rightarrow^{*}\mathcal{N}_{n}\geq\mathcal{V}_{n}$ and $(\mathcal{U}_{n}\
\mathcal{V}_{n})\rightarrow^{*}\mathcal{L}^{\prime}_{n}\geq\mathcal{W}_{n}$.
Thus $\lim_{n}\mathcal{U}_{n}\leq\left\llbracket M\right\rrbracket$ and
$\lim_{n}\mathcal{V}_{n}\leq\left\llbracket N\right\rrbracket$ with
$\mathcal{W}_{n}\leq\left\llbracket\mathcal{U}_{n}\
\mathcal{V}_{n}\right\rrbracket$ leading to the required inequality:

$\left\llbracket M\
N\right\rrbracket=\lim_{n}\mathcal{W}_{n}\leq\lim_{n}\left\llbracket\mathcal{U}_{n}\
\mathcal{V}_{n}\right\rrbracket\leq\left\llbracket\lim_{n}\left(\mathcal{U}_{n}\
\mathcal{V}_{n}\right)\right\rrbracket\leq\left\llbracket\left(\lim_{n}\mathcal{U}_{n}\right)\
\left(\lim_{n}\mathcal{V}_{n}\right)\right\rrbracket\leq\left\llbracket\left\llbracket
M\right\rrbracket\ \left\llbracket N\right\rrbracket\right\rrbracket\ .$

$(\geq)\ $ There is
$(\mathcal{M}_{n},\mathcal{N}_{n},\mathcal{U}_{n},\mathcal{V}_{n})_{n\geq 1}$
such that $M\rightarrow^{n}\mathcal{M}_{n}\geq\mathcal{U}_{n}$ and
$N\rightarrow^{n}\mathcal{N}_{n}\geq\mathcal{V}_{n}$ for all $n$ and such that
$\left\llbracket M\right\rrbracket=\lim_{n}(\mathcal{U}_{n})$ and
$\left\llbracket N\right\rrbracket=\lim_{n}(\mathcal{V}_{n})$. This leads to
the equality $\left\llbracket\left\llbracket M\right\rrbracket\
\left\llbracket
N\right\rrbracket\right\rrbracket\>{=}\>\lim_{m,n}\left\llbracket\mathcal{U}_{m}\
\mathcal{V}_{n}\right\rrbracket$. Finally, by Lemma 9, for any $m,n$, each
approximant of $\left\llbracket\mathcal{U}_{m}\
\mathcal{V}_{n}\right\rrbracket$ is below $\left\llbracket M\
N\right\rrbracket$, so is their sup. ∎

###  3.3 Almost-Sure Termination

We now have all the necessary ingredients to specify a quite powerful notion
of probabilistic computation. When, precisely, should such a process be
considered _terminating_? Do all probabilistic branches (see figures 4-4) need
to be finite? Or should we stay more liberal? The literature on the subject is
unanimously pointing to the notion of _almost-sure termination_ : a
probabilistic computation should be considered terminating if the set of
infinite computation branches, although not necessarily empty, has null
probability [18, 10, 15]. This has the following incarnation in our setting:

######  Definition 11.

A term $M$ is said to be _almost-surely terminating_ (AST) iff $Succ(M)=1$.

This section is concerned with proving that
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ indeed guarantees almost-sure
termination. This will be done by adapting Girard-Tait’s reducibility
technique.

######  Theorem 12.

The full system $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ is almost-
surely terminating (AST), i.e.,

$\forall M\in\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}},\quad Succ(M)=1.$

###### Proof.

The proof is is based on the the notion of a _reducible_ term, which is given
as follows by induction on the structure of types:

$\displaystyle Red_{\mathtt{NAT}}$ $\displaystyle:=\
\left\\{M\in\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}(\mathtt{NAT})\mid
M\text{ is AST}\right\\}$ $\displaystyle Red_{A\rightarrow B}$
$\displaystyle:=\ \\{M\mid\forall V\in
Red_{A}\cap\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V},\ (M\ V)\in
Red_{B}\\}$ $\displaystyle Red_{A\times B}$ $\displaystyle:=\
\\{M\mid({\mathtt{\pi}}_{1}\ M)\in Red_{A},\ ({\mathtt{\pi}}_{2}\ M)\in
Red_{B}\\}$

Then we can observe that:

  1. 1.

The reducibility candidates over $Red_{A}$ are $\rightarrow$-saturated:
by induction on $A$ we can indeed show that if $M\rightarrow\mathcal{M}$ then
$\left|\mathcal{M}\right|\subseteq Red_{A}$ iff $M\in Red_{A}$.

     * •

Trivial for $A=\mathtt{NAT}$.

     * •

If $A={B\rightarrow C}$: then for all value $V\in Red_{B}$, $(M\
V)\rightarrow(\mathcal{M}\ V)$, thus by IH $(M\ V)\in Red_{C}$ iff
$\left|\mathcal{M}\ V\right|=\\{M^{\prime}\ V\mid
M^{\prime}\in\left|\mathcal{M}\right|\\}\subseteq Red_{C}$; which exactly
means that $\left|\mathcal{M}\right|\subseteq Red_{B\rightarrow C}$ iff $M\in
Red_{B\rightarrow C}$.

     * •

If $A={A_{1}\times A_{2}}$: then for $i\in\\{1,2\\}$, $({\mathtt{\pi}}_{i}\
M)\rightarrow({\mathtt{\pi}}_{i}\ \mathcal{M})$ so that by IH,
$({\mathtt{\pi}}_{i}\ M)\in Red_{A_{i}}$ iff $({\mathtt{\pi}}_{i}\
\mathcal{M})\subseteq Red_{A_{i}}$; which exactly means that
$\left|\mathcal{M}\right|\subseteq Red_{A_{1}\times A_{2}}$ iff $M\in
Red_{A_{1}\times A_{2}}$.

  2. 2.

The reducibility candidates over $Red_{A}$ are precisely the AST terms $M$
such that $\left\llbracket M\right\rrbracket\subseteq Red_{A}$:
this goes by induction on $A$.

     * •

Trivial for $A=\mathtt{NAT}$.

     * •

For $A=B\rightarrow C$:

Let $M\in Red_{B\rightarrow C}$. Remark that there is a value $V\in Red_{B}$,
thus $(M\ V)\in Red_{C}$ and $(M\ V)$ is AST by IH; using Lemma 10 we get $M$
AST and it is easy to see that if $U\in\left|\left\llbracket
M\right\rrbracket\right|$ then $U\in\left|\mathcal{M}\right|$ for some
$M\rightarrow^{*}\mathcal{M}$ so that $U\in Red_{B\rightarrow C}$ by
saturation.

Conversely, let $M$ be AST with $\left|\left\llbracket
M\right\rrbracket\right|\subseteq Red_{B\rightarrow C}$ and let $V\in Red_{B}$
be a value. By IH, for any $U\in\left|\left\llbracket
M\right\rrbracket\right|\subseteq Red_{B\rightarrow C}$ we have $(U\ V)$ AST
with an evaluation supported by elements of $Red_{C}$; by Lemma 10
$\left\llbracket M\ V\right\rrbracket=\left\llbracket\left\llbracket
M\right\rrbracket\ V\right\rrbracket$ meaning that $(M\ V)$ is AST and has an
evaluation supported by elements of $Red_{C}$, so that we can conclude by IH.

     * •

For $A=A_{1}\times A_{2}$:

Let $M\in Red_{A_{1}\times A_{2}}$. then $({\mathtt{\pi}}_{1}\ M)\in
Red_{A_{1}}$ and $({\mathtt{\pi}}_{1}\ M)$ is AST by IH; using Lemma 10 we get
$M$ AST and it is easy to see that if $U\in\left|\left\llbracket
M\right\rrbracket\right|$ then $U\in\left|\mathcal{M}\right|$ for some
$M\rightarrow^{*}\mathcal{M}$ so that $U\in Red_{A_{1}\rightarrow A_{2}}$ by
saturation.

Conversely, let $M$ be AST with $\left|\left\llbracket
M\right\rrbracket\right|\subseteq Red_{A_{1}\rightarrow A_{2}}$ and let
$i\in\\{1,\\}2$. By IH, for any $U\in\left|\left\llbracket
M\right\rrbracket\right|\subseteq Red_{A_{1}\rightarrow A_{2}}$ we have
$({\mathtt{\pi}}_{i}U)$ AST with an evaluation supported by elements of
$Red_{A_{i}}$; by Lemma 10 $\left\llbracket{\mathtt{\pi}}_{i}\
M\right\rrbracket=\left\llbracket{\mathtt{\pi}}_{i}\ \left\llbracket
M\right\rrbracket\right\rrbracket$ meaning that $({\mathtt{\pi}}_{i}\ M)$ is
AST and has an evaluation supported by elements of $Red_{A_{i}}$, so that we
can conclude by IH.

  3. 3.

Every term $M$ such that $x_{1}:A_{1},\ldots,x_{n}:A_{n}\vdash M:B$ is a
candidate in the sense that if $V_{i}\in Red_{A_{i}}$ for every $1\leq i\leq
n$, then $M[V_{1}/x_{1},\ldots,V_{n}/x_{n}]\in Red_{B}$:
by induction on the type derivation. The only difficult cases are the
recursion, the application, the binary choice $\oplus$ and the denumerable
choice ${\mathtt{X}}$:

     * •

For the operator ${\mathtt{rec}}$: We have to show that if $U\in Red_{A}$ and
$V\in Red_{\mathtt{NAT}\rightarrow A\rightarrow A}$ then for all
$n\in\mathbb{N}$, $({\mathtt{rec}}\ \langle U,V,\boldsymbol{n}\rangle)\in
Red_{A}$. We proceed by induction on $n$:

       * •

If $n=0$: ${\mathtt{rec}}\ \langle
U,V,\boldsymbol{0}\rangle\rightarrow\\{U\\}\subseteq Red_{A}$ and we conclude
by saturation.

       * •

Otherwise: ${\mathtt{rec}}\ \langle U,V,\boldsymbol{(n+1)}\rangle\rightarrow
V\ \boldsymbol{n}\ ({\mathtt{rec}}\ \langle U,V,\boldsymbol{n}\rangle)\in
Red_{A}$ since $({\mathtt{rec}}\ \langle U,V,\boldsymbol{n}\rangle)\in
Red_{A}$ by IH and since $\boldsymbol{n}\in Red_{\mathbb{N}}$ and $V\in
Red_{\mathbb{N}\rightarrow A\rightarrow A}$, we conclude by saturation.

     * •

For the application: we have to show that if $M\in Red_{A\rightarrow B}$ and
$N\in Red_{A}$ then $(M\ N)\in Red_{B}$. But since $N\in Red_{A}$, this means
that it is AST and for every $V\in\left|\left\llbracket
N\right\rrbracket\right|$, $(M\ V)\in Red_{B}$. In particular, by Lemma 10, we
have $\left\llbracket M\ N\right\rrbracket=\left\llbracket M\ \left\llbracket
N\right\rrbracket\right\rrbracket$ so that $(M\ N)$ is AST and
$\left|\left\llbracket M\
N\right\rrbracket\right|\subseteq\bigcup_{V\in\left|\left\llbracket
N\right\rrbracket\right|}\left|\left\llbracket M\
V\right\rrbracket\right|\subseteq Red_{B}$.

     * •

For the operator $\oplus$: If $M,N\in Red_{A}$ then
$\left|\left\\{\begin{matrix}M\mapsto\frac{1}{2}\\\\[1.99997pt]
N\mapsto\frac{1}{2}\end{matrix}\right\\}\right|\subseteq Red_{A}$, and, by
$\rightarrow$-saturation, $(M\oplus N)\in Red_{A}$.

     * •

For the operator ${\mathtt{X}}$: we have to show that for any value
$U{\in}Red_{A\rightarrow A}$ and $V{\in}Red_{A}$ if holds that $({\mathtt{X}}\
U\ V)\in Red_{A}$.
By an easy induction on $n$, $(U^{n}\ V)\in Red_{A}$ since $U^{0}\ V=V\in
Red_{B}$ and $U^{n+1}\ V=U\ (U^{n}\ V)\in Red_{B}$ whenever $U^{n}\ V\in
Red_{B}$ and $U\in Red_{B\rightarrow B}$.
Moreover, by an easy induction on $n$ we have

$\left\llbracket{\mathtt{X}}\ U\
V\right\rrbracket=\frac{1}{2^{n+1}}\left\llbracket U^{n}\ ({\mathtt{X}}\ U\
V)\right\rrbracket+\sum_{i\leq n}\frac{1}{2^{i+1}}\left\llbracket U^{i}\
V\right\rrbracket\ .$

       * •

trivial for $n=0$,

       * •

we know that $\left\llbracket{\mathtt{X}}\ U\
V\right\rrbracket=\frac{1}{2}\left\llbracket
V\right\rrbracket+\frac{1}{2}\left\llbracket V({\mathtt{X}}\ U\
V)\right\rrbracket$ and we get $\left\llbracket V({\mathtt{X}}\ U\
V)\right\rrbracket=\left\llbracket V\left\llbracket{\mathtt{X}}\ U\
V\right\rrbracket\right\rrbracket=\frac{1}{2^{n+1}}\left\llbracket
U^{n+1}({\mathtt{X}}\ U\ V)\right\rrbracket+\sum_{i\leq
n}\frac{1}{2^{i+1}}\left\llbracket U^{i+1}V\right\rrbracket$ by Lemma 10 and
IH, which is sufficient to conclude.

At the limit, we get $\left\llbracket{\mathtt{X}}\ U\
V\right\rrbracket=\sum_{i\in\mathbb{N}}\frac{1}{2^{i+1}}\left\llbracket U^{i}\
V\right\rrbracket$. We can then conclude that $({\mathtt{X}}\ U\ V)$ is AST
(since each of the $(U^{i}\ V)\in Red_{B}$ are AST and
$\sum_{i}\frac{1}{2^{i+1}}=1$) and that $\left|\left\llbracket M\
N\right\rrbracket\right|=\bigcup_{i}\left|\left\llbracket U^{i}\
V\right\rrbracket\right|\subseteq Red_{A}$.

∎

Almost-sure termination could however be seen as too weak a property: there is
no guarantee about the average computation length. For this reason, another
stronger notion is often considered, namely _positive_ almost-sure
termination:

######  Definition 13.

A term $M$ is said to be _positively almost-surely terminating_ (or _PAST_)
iff the average reduction length $[M]$ is finite.

Gödel’s $\mathbb{T}$, when paired with ${\mathtt{R}}$, is combinatorially too
powerful to guarantee positive almost sure termination. More precisely, the
issue is triggered by the ability to describe programs with exponential
reduction time such as the term $\boldsymbol{\mathtt{Expo}}$ from Example 2
which is computing the function $n\mapsto 2^{n+1}$ in time $\sim 2^{n+1}$.

######  Theorem 14.

$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ is not positively almost-
surely terminating.

###### Proof.

The term $(\boldsymbol{\mathtt{Expo}}\ {\mathtt{R}}):\mathtt{NAT}$ is
computing, with probability $\frac{1}{2^{n+1}}$ the number $2^{n+1}$ in time
$2^{n+1}$; the average reduction length is thus

$[\boldsymbol{\mathtt{Expo}}\ {\mathtt{R}}]\ =\
\sum_{n}\frac{2^{n+1}}{2^{n+1}}\ =\ +\infty\ .$

∎

###  3.4 On Fragments of $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$: a
Roadmap

The calculus $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ contains at least
four fragments, namely Gödel’s $\mathbb{T}$ and the three fragments
$\mathbb{T}^{\oplus}$, $\mathbb{T}^{{\mathtt{R}}}$ and
$\mathbb{T}^{{\mathtt{X}}}$ corresponding to the three probabilistic choice
operators we consider. It is then natural to ask oneselves how these fragments
relate to each other as for their respective expressive power. At the end of
this paper, we will have a very clear picture in front of us.

The first such result is the equivalence between the apparently dual fragments
$\mathbb{T}^{{\mathtt{R}}}$ and $\mathbb{T}^{{\mathtt{X}}}$. The embeddings
are in fact quite simple: getting ${\mathtt{X}}$ from ${\mathtt{R}}$ only
requires “guessing” the number of iterations via ${\mathtt{R}}$ and then use
${\mathtt{rec}}$ to execute them; conversely, capturing ${\mathtt{R}}$ from
${\mathtt{X}}$ is even easier: it corresponds to counting the recursive loops
done by some executions of ${\mathtt{X}}$:

######  Proposition 15.

$\mathbb{T}^{{\mathtt{R}}}$ and $\mathbb{T}^{{\mathtt{X}}}$ are both
equiexpressive with $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$.

###### Proof.

The calculus $\mathbb{T}^{{\mathtt{R}}}$ embeds the full system
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ via the encoding:111Notice
that the dummy abstractions on $z$ and the $\boldsymbol{0}$ at the end ensure
the correct reduction order by making $\lambda z.N$ a value.

$M\oplus_{\mathtt{R}}N:=\ {\mathtt{rec}}\ \langle\lambda z.N,\lambda
xyz.M,{\mathtt{R}}\rangle\
\boldsymbol{0};\qquad\qquad{\mathtt{X}}_{\mathtt{R}}\ :=\ \lambda
x.{\mathtt{rec}}\ \langle\pi_{2}x,\lambda z.\pi_{1}x,{\mathtt{R}}\rangle.$

The fragment $\mathbb{T}^{{\mathtt{X}}}$ embeds the full system
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ via the encoding:

$M\oplus_{\mathtt{X}}N:=\ {\mathtt{X}}\ \langle\lambda xy.M,\lambda
y.N\rangle\ \boldsymbol{0};\qquad\qquad{\mathtt{R}}_{\mathtt{X}}\ :=\
{\mathtt{X}}\ \langle{\mathtt{S}},\boldsymbol{0}\rangle.$

In both cases, the embedding is compositional and preserves types.

We have to prove the correctedness of the two embeddings:

  * •

For any $M$ and $N$:

$\left\llbracket M\oplus_{\mathtt{R}}N\right\rrbracket\ =\ \left\llbracket
M\oplus_{\mathtt{X}}N\right\rrbracket\ =\ \left\llbracket M\oplus
N\right\rrbracket\ =\ \frac{1}{2}\left\llbracket
M\right\rrbracket+\frac{1}{2}\left\llbracket N\right\rrbracket\ .$

Indeed, we only have to perform a few reductions:

$\displaystyle\left\llbracket M\oplus_{\mathtt{R}}N\right\rrbracket$
$\displaystyle=\sum_{n\geq 0}\frac{1}{2^{n+1}}\left\llbracket{\mathtt{rec}}\
\langle\lambda z.N,\lambda xyz.M,\boldsymbol{n}\rangle\
\boldsymbol{0}\right\rrbracket$
$\displaystyle=\frac{1}{2}\left\llbracket{\mathtt{rec}}\ \langle\lambda
z.N,\lambda xyz.M,\boldsymbol{0}\rangle\
\boldsymbol{0}\right\rrbracket+\sum_{n\geq
0}\frac{1}{2^{n+2}}\left\llbracket{\mathtt{rec}}\ \langle\lambda z.N,\lambda
xyz.M,{\mathtt{S}}\boldsymbol{n}\rangle\ \boldsymbol{0}\right\rrbracket$
$\displaystyle=\frac{1}{2}\left\llbracket(\lambda z.N)\
\boldsymbol{0}\right\rrbracket+\sum_{n\geq
0}\frac{1}{2^{n+2}}\left\llbracket(\lambda xyz.M)\ \boldsymbol{n}\
({\mathtt{rec}}\ \langle\lambda z.N,\lambda xyz.M,\boldsymbol{n}\rangle)\
\boldsymbol{0}\right\rrbracket$ $\displaystyle=\frac{1}{2}\left\llbracket
N\right\rrbracket+\sum_{n\geq 0}\frac{1}{2^{n+2}}\left\llbracket
M\right\rrbracket$ $\displaystyle=\frac{1}{2}\left\llbracket
N\right\rrbracket+\frac{1}{2}\left\llbracket M\right\rrbracket$
$\displaystyle\left\llbracket M\oplus_{\mathtt{X}}N\right\rrbracket$
$\displaystyle=\frac{1}{2}\left\llbracket(\lambda y.N)\
\boldsymbol{0}\right\rrbracket+\frac{1}{2}\left\llbracket(\lambda xy.M)\
{\mathtt{R}}_{\mathtt{X}}\ \boldsymbol{0}\right\rrbracket$
$\displaystyle=\frac{1}{2}\left\llbracket(\lambda y.N)\
\boldsymbol{0}\right\rrbracket+\frac{1}{2}\left\llbracket(\lambda xy.M)\
{\mathtt{R}}_{\mathtt{X}}\ \boldsymbol{0}\right\rrbracket$
$\displaystyle=\frac{1}{2}\left\llbracket
N\right\rrbracket+\frac{1}{2}\left\llbracket M\right\rrbracket$

  * •

For any $U$ and $V$:

$\left\llbracket{\mathtt{X}}_{\mathtt{R}}\langle U,V\rangle\right\rrbracket\
=\ \left\llbracket{\mathtt{X}}\langle U,V\rangle\right\rrbracket$

Indeed, both of them are the unique fixedpoint of the following contractive
function:

$f(\mathcal{X})\ :=\ \frac{1}{2}\left\llbracket
U\right\rrbracket+\frac{1}{2}\left\llbracket V\ \mathcal{X}\right\rrbracket\
.$

That $\left\llbracket{\mathtt{X}}\langle
U,V\rangle\right\rrbracket=f(\left\llbracket{\mathtt{X}}\langle
U,V\rangle\right\rrbracket)$ is immediate after a reduction, as for the other,
we have:

$\displaystyle\left\llbracket{\mathtt{X}}_{\mathtt{R}}\langle
U,V\rangle\right\rrbracket$ $\displaystyle=\sum_{n\geq
0}\frac{1}{2^{n+1}}\left\llbracket{\mathtt{rec}}\ \langle U,\lambda
z.V,\boldsymbol{n}\rangle\right\rrbracket$
$\displaystyle=\frac{1}{2}\left\llbracket
U\right\rrbracket+\frac{1}{2}\sum_{n\geq 0}\frac{1}{2^{n+1}}\left\llbracket U\
({\mathtt{rec}}\ \langle U,\lambda z.V,\boldsymbol{n}\rangle)\right\rrbracket$
$\displaystyle=\frac{1}{2}\left\llbracket
U\right\rrbracket+\frac{1}{2}\sum_{n\geq 0}\frac{1}{2^{n+1}}\left\llbracket U\
\left\llbracket{\mathtt{rec}}\ \langle U,\lambda
z.V,\boldsymbol{n}\rangle\right\rrbracket\right\rrbracket$ by Lemma 10
$\displaystyle=\frac{1}{2}\left\llbracket
U\right\rrbracket+\frac{1}{2}\left\llbracket U\ \left(\sum_{n\geq
0}\frac{1}{2^{n+1}}\left\llbracket{\mathtt{rec}}\ \langle U,\lambda
z.V,\boldsymbol{n}\rangle\right\rrbracket\right)\right\rrbracket$
$\displaystyle=\frac{1}{2}\left\llbracket
U\right\rrbracket+\frac{1}{2}\left\llbracket U\
\left\llbracket{\mathtt{X}}_{\mathtt{R}}\langle
U,V\rangle\right\rrbracket\right\rrbracket$

  * •

Finally:

$\left\llbracket{\mathtt{R}}_{\mathtt{X}}\right\rrbracket\ =\
\left\llbracket{\mathtt{R}}\right\rrbracket\ =\
\left\\{\boldsymbol{n}\mapsto\frac{1}{2^{n+1}}\middle|n\geq 0\right\\}\ .$

That
$\left\llbracket{\mathtt{R}}\right\rrbracket=\left\\{\boldsymbol{n}\mapsto\frac{1}{2^{n+1}}\middle|n\geq
0\right\\}$ is just one step of reduction, while
$\left\llbracket{\mathtt{R}}_{\mathtt{X}}\right\rrbracket=\left\\{\boldsymbol{n}\mapsto\frac{1}{2^{n+1}}\middle|n\geq
0\right\\}$ was shown in Example 5.

∎

Notice how simulating ${\mathtt{X}}$ by ${\mathtt{R}}$ requires the presence
of recursion, while the converse is not true. The implications of this fact
are intriguing, but lie outside the scope of this work.

In the following, we will no longer consider $\mathbb{T}^{{\mathtt{X}}}$ nor
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$ but only
$\mathbb{T}^{{\mathtt{R}}}$, keeping in mind that all these are equiexpressive
due to Proposition 15. The rest of this paper, thus, will be concerned with
understanding the relative expressive power of the three fragments
$\mathbb{T}$, $\mathbb{T}^{\oplus}$, and $\mathbb{T}^{{\mathtt{R}}}$. Can any
of the (obvious) strict _syntactical_ inclusions between them be turned into a
strict _semantic_ inclusion? Are the three systems equiexpressive?

In order to compare probabilistic calculi to deterministic ones, several
options are available. The most common one is to consider notions of
observations over the probabilistic outputs; this will be the purpose of
Section 6. In this section, we will look at whether applying a Monte Carlos or
a Las Vegas algorithm on the output of a randomized function in
$\mathbb{T}^{\oplus}$ or $\mathbb{T}^{{\mathtt{R}}}$ can enriched the set of
deterministicaly $\mathbb{T}$-definable functions.

Notice that neither Monte Carlos nor Las Vegas algorithms are definable inside
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$. Indeed, for those algorithms
to be applicable, they require restrictions on the resulting distribution that
we are not able to describe in the calculus. For example, Las Vegas is only
applicable to functions $M:\mathtt{NAT}\rightarrow\mathtt{NAT}$ such that
$\left\llbracket M\ \boldsymbol{n}\right\rrbracket(0)\leq\frac{1}{2}$ for any
$n$.

Since those algorithms are not representable, we have to perform an external
study that can be quite heavy. Hopefully, we where able to define an internal
property, namely the (parameterized) _functional representability_ , that is
sufficient to collapse the results of both algorithms into the deterministic
system $\mathbb{T}$.

We say that the distribution $\mathcal{M}\in\mathfrak{D}(\mathbb{N})$ is
_finitely represented_ by222Here we denote $\mathbb{B}$ for binomial numbers
$\frac{m}{2^{n}}$ (where $m,n\in\mathbb{N}$) and $\mathtt{BIN}$ for their
representation in system $\mathbb{T}$ encoded by pairs $\langle m,n\rangle$ of
natural numbers. $f:\mathbb{N}\rightarrow\mathbb{B}$, if there exists a $q$
such that for every $k\geq q$ it holds that $f(k)=0$ and

$\mathcal{M}=\left\\{\boldsymbol{k}\mapsto f(k)\right\\}$

Moreover, the definition can be extended to families of distributions
$(\mathcal{M}_{n})_{n}$ by requiring the existence of
$f:(\mathbb{N}\times\mathbb{N})\rightarrow\mathbb{B}$,
$q:\mathbb{N}\rightarrow\mathbb{N}$ such that $\forall k\geq q(n),f(n,k)=0$
and

$\forall n,\quad\mathcal{M}_{n}=\ \left\\{\boldsymbol{k}\mapsto
f(n,k)\right\\}.$

In this case, we say that the representation is _parameterized_.

We will see in Section 4 that the distributions computed by
$\mathbb{T}^{\oplus}$ are exactly the (parametrically) finitely representable
by $\mathbb{T}$ terms. Concretely, this means that for any
$M\in\mathbb{T}^{\oplus}(\mathtt{NAT})$ or any
$M\in\mathbb{T}^{\oplus}(\mathtt{NAT}\rightarrow\mathtt{NAT})$, the
distributions $\left\llbracket M\right\rrbracket$ and $(\left\llbracket
N\boldsymbol{n}\right\rrbracket)_{n}$ are (parametrically) finitely
representable.

In $\mathbb{T}^{{\mathtt{R}}}$, however, distributions are more complex
(infinite, non-rational). That is why only a characterization in terms of
approximations is possible. More specifically, a distribution
$\mathcal{M}\in\mathfrak{D}(\mathtt{NAT})$ is said to be _functionally
represented_ by two functions
$f:(\mathbb{N}\times\mathbb{N})\rightarrow\mathbb{B}$ and
$g:\mathbb{N}\rightarrow\mathbb{N}$ iff for every $n\in\mathbb{N}$ and for
every $k\geq g(n)$ it holds that $f(n,k)=0$ and

$\sum_{k\in\mathbb{N}}\ \Bigl{|}\ \mathcal{M}(\boldsymbol{k})\ -\ f(n,k)\
\Bigr{|}\ \leq\ \frac{1}{n}.$

In other words, the distribution $\mathcal{M}$ can be approximated arbitrarily
well, and uniformly, by finitely representable ones. Similarly, we can define
a parameterized version of this definition at first order.

In Section 5 , we show that distributions generated by
$\mathbb{T}^{{\mathtt{R}}}$ terms are indeed uniform limits over those of
$\mathbb{T}^{\oplus}$; using our result on $\mathbb{T}^{\oplus}$ this give
their (parametric) functional representability in the deterministic
$\mathbb{T}$.

##  4 Binary Probabilistic Choice

This section is concerned with two theoretical results on the expressive power
of $\mathbb{T}^{\oplus}$. Taken together, they tell us that this fragment is
not far from $\mathbb{T}$.

###  4.1 Positive Almost-Sure Termination

The average number of steps to normal form can be infinite for terms of
$\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$. We will prove that, on the
contrary, $\mathbb{T}^{\oplus}$ is _positive_ almost-surely terminating. This
will be done by adapting (and strengthening!) the reducibility-based result
from Section 3.3.

For this, we will first give a formalization of the notion of execution tree
discussed in Section 2 in the form of a multistep reduction procedure. Then we
will formally show that this tree is finite.

We can give another notion of evaluation via a notion of multistep reduction.
We will see later on that the multistep reduction is none other than
$\rightarrow^{*}$ for the system T with binary choice, but this is not always
the case.

######  Definition 16.

The multistep reduction $\Rightarrow$ is defined by induction in Figure 7. Due
to the (potentially) countably many preconditions of the rule
$(R\text{-}{\in})$, the derivation tree of a multistep reduction $\Rightarrow$
can be infinitely wide and even of unbounded height, but each path have to be
finite.

$(R\text{-}refl)$ $\\!M\Rightarrow\Bigl{\\{}M\Bigr{\\}}\\!$
$\\!M\rightarrow\mathcal{M}$
$\\!\\!\\!\\!\\!\\!\mathcal{M}\Rightarrow\mathcal{N}\\!$ $(R\text{-}tran)$
$M\Rightarrow\mathcal{N}\vphantom{\Bigr{\\}}}$ $\\!\forall M\in|\mathcal{M}|,\
M\Rightarrow\mathcal{N}_{M}\\!$ $(R\text{-}{\in})\\!\\!$
$\mathcal{M}\Rightarrow\int_{\mathcal{M}}\mathcal{N}_{M}.dM$ Figure 7:
Multistep reduction. All terms and distributions are closed.

The infinitness of the width and the fact that the height is unbounded is
essentially in order to annalise $\mathbb{T}^{{\mathtt{R}}}$ in the same way.
In fact, most theorems in this section will be given for both
$\mathbb{T}^{\oplus}$ and $\mathbb{T}^{{\mathtt{R}}}$. But, for now, we will
focus on $\mathbb{T}^{\oplus}$ and finite derivations, while
$\mathbb{T}^{\oplus}$ and transfinite derivations will be analyzed in details
in Section 5.1.

######  Example 17.

Take the example $rec\langle\boldsymbol{0},\lambda
xy.y\oplus({\mathtt{S}}y),\boldsymbol{2}\rangle$; the execution tree is the
following where we denote $U_{n}:=rec\langle\boldsymbol{0},\lambda
xy.y\oplus({\mathtt{S}}y),\boldsymbol{n}\rangle$:

$U_{2}$$\bullet$$\bullet$$U_{1}\oplus{\mathtt{S}}U_{1}$$U_{1}$${\mathtt{S}}U_{1}$$\bullet$$\bullet$$U_{0}\oplus{\mathtt{S}}U_{0}$$U_{0}$$\boldsymbol{0}$${\mathtt{S}}U_{0}$$\boldsymbol{1}$$\bullet$$\bullet$${\mathtt{S}}(U_{0}\oplus{\mathtt{S}}U_{0})$${\mathtt{S}}U_{0}$$\boldsymbol{1}$${\mathtt{S}}{\mathtt{S}}U_{0}$$\boldsymbol{2}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$

This tree is subsumed by the (more complex) derivation of $U_{2}\Rightarrow\
\frac{1}{4}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{4}\\{\boldsymbol{2}\\}$,
with every arrow of the exectution tree replaced by a $(R\text{-}tran)$ rule
followed by a $(R\text{-}{\in})$ rule:

$(R\text{-}refl)$ $\boldsymbol{1}\Rightarrow\\{\boldsymbol{1}\\}$
$(R\text{-}{\in})\\!\\!$
$U_{0}\rightarrow\>$$\\{\boldsymbol{1}\\}\Rightarrow\\{\boldsymbol{1}\\}$
$(R\text{-}tran)$ $U_{0}\Rightarrow\\{\boldsymbol{1}\\}$ $(R\text{-}refl)$
$\boldsymbol{2}\Rightarrow\\{\boldsymbol{2}\\}$ $(R\text{-}{\in})$
${\mathtt{S}}U_{0}\rightarrow\>$$\\{\boldsymbol{2}\\}\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$ ${\mathtt{S}}U_{0}\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$
$U_{0}\oplus({\mathtt{S}}U_{0})\rightarrow\>$$\frac{1}{2}\\{U_{0}\\}+\frac{1}{2}\\{{\mathtt{S}}U_{0}\\}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$
$U_{0}\oplus({\mathtt{S}}U_{0})\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$ $(\lambda
y.y\oplus({\mathtt{S}}y))U_{0}\rightarrow\>$$\\{U_{0}\oplus({\mathtt{S}}U_{0})\\}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$ $(\lambda
y.y\oplus({\mathtt{S}}y))U_{0}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(\lambda
xy.y\oplus({\mathtt{S}}y)\boldsymbol{1}U_{0})\rightarrow\>$$\\{(\lambda
y.y\oplus({\mathtt{S}}y))U_{0}\\}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(\lambda
xy.y\oplus({\mathtt{S}}y))\boldsymbol{1}U_{0}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$ $U_{1}\rightarrow\>$$\\{(\lambda
xy.y\oplus({\mathtt{S}}y))\boldsymbol{1}U_{0}\\}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$
$U_{1}\Rightarrow\frac{1}{2}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}$
$(R\text{-}refl)$ $\boldsymbol{1}\Rightarrow\\{\boldsymbol{1}\\}$
$(R\text{-}{\in})\\!\\!$
${\mathtt{S}}U_{0}\rightarrow\>$$\\{\boldsymbol{1}\\}\Rightarrow\\{\boldsymbol{1}\\}$
$(R\text{-}tran)$ ${\mathtt{S}}U_{0}\Rightarrow\\{\boldsymbol{1}\\}$
$(R\text{-}refl)$ $\boldsymbol{2}\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$
${\mathtt{S}}{\mathtt{S}}U_{0}\rightarrow\>$$\\{\boldsymbol{2}\\}\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$
${\mathtt{S}}{\mathtt{S}}U_{0}\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$
${\mathtt{S}}(U_{0}\oplus({\mathtt{S}}U_{0}))\rightarrow\>$$\frac{1}{2}\\{{\mathtt{S}}U_{0}\\}+\frac{1}{2}\\{{\mathtt{S}}{\mathtt{S}}U_{0}\\}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$
${\mathtt{S}}(U_{0}\oplus({\mathtt{S}}U_{0}))\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$ ${\mathtt{S}}((\lambda
y.y\oplus({\mathtt{S}}y))U_{0})\rightarrow\>$$\\{{\mathtt{S}}(U_{0}\oplus({\mathtt{S}}U_{0}))\\}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$ ${\mathtt{S}}((\lambda
y.y\oplus({\mathtt{S}}y))U_{0})\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$ ${\mathtt{S}}((\lambda
xy.y\oplus({\mathtt{S}}y))\boldsymbol{1}U_{0})\rightarrow\>$$\\{{\mathtt{S}}((\lambda
y.y\oplus({\mathtt{S}}y))U_{0})\\}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$ ${\mathtt{S}}((\lambda
xy.y\oplus({\mathtt{S}}y))\boldsymbol{1}U_{0})\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$ ${\mathtt{S}}U_{1}\rightarrow\>$$\\{{\mathtt{S}}((\lambda
xy.y\oplus({\mathtt{S}}y))\boldsymbol{1}U_{0})\\}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$
${\mathtt{S}}U_{1}\Rightarrow\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{2}\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$
$U_{1}\oplus({\mathtt{S}}U_{1})\rightarrow\>$$\frac{1}{2}\\{U_{1}\\}+\frac{1}{2}\\{{\mathtt{S}}U_{1}\\}\Rightarrow\frac{1}{4}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{4}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$
$U_{1}\oplus({\mathtt{S}}U_{1})\Rightarrow\frac{1}{4}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{4}\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$ $(\lambda
y.y\oplus({\mathtt{S}}y))U_{1}\rightarrow\>$$\\{U_{1}\oplus({\mathtt{S}}U_{1})\\}\Rightarrow\frac{1}{4}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{4}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$ $(\lambda
y.y\oplus({\mathtt{S}}y))U_{1}\Rightarrow\frac{1}{4}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{4}\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$ $(\lambda
xy.y\oplus({\mathtt{S}}y))\boldsymbol{1}U_{1}\rightarrow\>$$\\{(\lambda
y.y\oplus({\mathtt{S}}y))U_{1}\\}\Rightarrow\frac{1}{4}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{4}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$ $(\lambda
xy.y\oplus({\mathtt{S}}y))\boldsymbol{1}U_{1}\Rightarrow\frac{1}{4}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{4}\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$ $U_{2}\rightarrow\>$$\\{(\lambda
xy.y\oplus({\mathtt{S}}y))\boldsymbol{1}U_{1}\\}\Rightarrow\frac{1}{4}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{4}\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$ $U_{2}\Rightarrow\
\frac{1}{4}\\{\boldsymbol{0}\\}+\frac{1}{2}\\{\boldsymbol{1}\\}+\frac{1}{4}\\{\boldsymbol{2}\\}$

Notice that we are contracting the rule $(R\text{-}tran)$ for readability.
More important, notice also that the derivation is correct and finite because
the execution tree is finite.

######  Lemma 18.

The multistep semantics $\Rightarrow$ is confluent.

###### Proof.

By an easy induction, we show that if $\mathcal{N}_{1}\Leftarrow
M\Rightarrow\mathcal{N}_{2}$ (resp.
$\mathcal{N}_{1}\Leftarrow\mathcal{M}\Rightarrow\mathcal{N}_{2}$), then there
is $\mathcal{L}$ such that
$\mathcal{N}_{1}\Rightarrow\mathcal{L}\Leftarrow\mathcal{N}_{2}$. Now:

  * •

If both reductions are using the same rule ( either $(R\text{-}refl)$,
$(R\text{-}tran)$, or $(R\text{-}{\in})$ ), then it is an immediate use of the
induction hypothesis on the premises as those rules are determinist.

  * •

If one of them use the rule $(R\text{-}refl)$, then it is trivial.

  * •

No other case is possible as $(R\text{-}tran)$ and $(R\text{-}{\in})$ cannot
apply together (one require a term as source and the other a distribution).

∎

######  Lemma 19.

If $(M\
V)\Rightarrow\mathcal{U}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V})$
then there is
$\mathcal{W}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V})$
such that $M\Rightarrow\mathcal{W}$.

###### Proof.

By induction on $\Rightarrow$ we can show that if $(M\
V)\Rightarrow\mathcal{N}$ then $\mathcal{N}=\mathcal{L}+(\mathcal{M}\ V)$ with
$M\Rightarrow\mathcal{W}+\mathcal{M}$ and $(\mathcal{W}\
V)\Rightarrow\mathcal{L}$ (and similarly if $M$ is a distribution):

  * •

the $(R\text{-}refl)$ and $(R\text{-}\in)$ are trivial,

  * •

if $(M\ V)\rightarrow\mathcal{N}^{\prime}\Rightarrow\mathcal{N}$ then there is
two cases:

    * •

either $M\rightarrow\mathcal{M}^{\prime}$ and
$\mathcal{N}^{\prime}=(\mathcal{M}^{\prime}\ V)\Rightarrow\mathcal{N}$ and we
can conclude by induction hypothesis,

    * •

or $M=W$ is a value and $M\Rightarrow\\{W\\}$ with $(\\{W\\}\
V)\rightarrow\mathcal{N}^{\prime}\Rightarrow\mathcal{N}=\mathcal{L}$.

Notice that if $\mathcal{N}$ is a value distribution then $\mathcal{M}$ has to
be one. ∎

The following lemma is an alternative version of Lemma 10 where the evaluation
is obtained after a finite number of steps (in both hypothesis and
conclusions).

######  Lemma 20.

If
$N\Rightarrow\mathcal{V}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V})$
and $M\
\mathcal{V}\Rightarrow\mathcal{U}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}_{V})$
then $M\ N\Rightarrow\mathcal{U}$.

###### Proof.

By induction on the derivation of $N\Rightarrow V$ (generalizing the property
for any distribution $\mathcal{N}$ in place of $N$):

  * •

If $V=\\{N\\}$ this is trivial.

  * •

If $M\rightarrow\mathcal{N}\Rightarrow\mathcal{V}$ then by IH, $M\
\mathcal{N}\Rightarrow U$ and thus $M\ N\rightarrow M\ \mathcal{N}\Rightarrow
U$ so that we can conclude by rule $(R\text{-}trans)$.

  * •

If for all $N\in\left|\mathcal{N}\right|$, $N\Rightarrow\mathcal{V}_{N}$ with
$\mathcal{V}=\int_{\mathcal{N}}\mathcal{V}_{N}dN$ then by applying the IH on
each $N\in\left|\mathcal{N}\right|$, we get that $M\
N\Rightarrow\mathcal{U}_{N}$ for some $\mathcal{U}_{N}$ and we conclude by
rule $(R\text{-}\in)$ using $\mathcal{U}=\int_{\mathcal{N}}\mathcal{U}_{N}dN$.

∎

######  Theorem 21.

For any term $M\in\mathbb{T}^{\oplus,{\mathtt{R}}}$, there exists a value
distribution $\left\llbracket
M\right\rrbracket_{a}\in\mathfrak{D}(\mathbb{T}^{\oplus,{\mathtt{R}}}_{V})$
such that $M\Rightarrow\left\llbracket M\right\rrbracket_{a}$. We call it the
accessible evaluation.

###### Proof.

When it exists, $\left\llbracket M\right\rrbracket_{a}$ is unique due to
confluence. Thus we only have to prove its existence.
The proof goes by reducibility over the candidates:

$\displaystyle Red_{\mathtt{NAT}}$ $\displaystyle:=\
\\{M\in\mathbb{T}^{\oplus}(\mathtt{NAT})\mid\exists\left\llbracket
M\right\rrbracket_{a}\in\mathfrak{D}(\mathbb{T}^{\oplus}_{V}),\
M\Rightarrow\left\llbracket M\right\rrbracket_{a}\\}$ $\displaystyle
Red_{A\rightarrow B}$ $\displaystyle:=\ \\{M\mid\forall V\in
Red_{A}\cap\mathbb{T}^{\oplus}_{V},\ (M\ V)\in Red_{B}\\}$ $\displaystyle
Red_{A\times B}$ $\displaystyle:=\ \\{M\mid({\mathtt{\pi}}_{1}\ M)\in
Red_{A},\ ({\mathtt{\pi}}_{2}\ M)\in Red_{B}\\}$

  1. 1.

The reducibility candidates over $Red_{A}$ are $\rightarrow$-saturated:
By induction on $A$ we can show that if $M\rightarrow\mathcal{M}$ then
$\left|\mathcal{M}\right|\subseteq Red_{A}$ iff $M\in Red_{A}$.

     * •

If $A=\mathtt{NAT}$: then whenever $M^{\prime}\Rightarrow\left\llbracket
M^{\prime}\right\rrbracket_{a}$ for all
$M^{\prime}\in\left|\mathcal{M}\right|$ we get
$\mathcal{M}\Rightarrow\int_{\mathcal{M}}\left\llbracket
M^{\prime}\right\rrbracket_{a}dM^{\prime}=\left\llbracket\mathcal{M}\right\rrbracket_{a}$
by $(R\text{-}\in)$ and thus
$M\Rightarrow\left\llbracket\mathcal{M}\right\rrbracket_{a}=\left\llbracket
M\right\rrbracket_{a}$ by $(R\text{-}trans)$. Conversely, whenever
$M\Rightarrow\left\llbracket M\right\rrbracket_{a}$, this reduction cannot
comes from rule $(R\text{-}refl)$ since $\left\llbracket
M\right\rrbracket_{a}$ is a value distribution and $M$ is reducible, thus it
comes from rule $(R\text{-}trans)$ and
$\mathcal{M}\Rightarrow\left\llbracket\mathcal{M}\right\rrbracket_{a}$ which
itself necessarily comes from an application of $(R\text{-}\in)$ so that
$M^{\prime}\Rightarrow\left\llbracket M^{\prime}\right\rrbracket_{a}$ for any
$M^{\prime}\in\left|\mathcal{M}\right|$.

     * •

If $A={B\rightarrow C}$: then for all value $V\in Red_{B}$, $(M\
V)\rightarrow(\mathcal{M}\ V)$, thus by IH $(M\ V)\in Red_{C}$ iff
$\left|\mathcal{M}\ V\right|=\\{M^{\prime}\ V\mid
M^{\prime}\in\left|\mathcal{M}\right|\\}\subseteq Red_{C}$; which exactly
means that $\left|\mathcal{M}\right|\subseteq Red_{B\rightarrow C}$ iff $M\in
Red_{B\rightarrow C}$.

     * •

If $A={A_{1}\times A_{2}}$: then for $i\in\\{1,2\\}$, $({\mathtt{\pi}}_{i}\
M)\rightarrow({\mathtt{\pi}}_{i}\ \mathcal{M})$ so that by IH,
$({\mathtt{\pi}}_{i}\ M)\in Red_{A_{i}}$ iff $({\mathtt{\pi}}_{i}\
\mathcal{M})\subseteq Red_{A_{i}}$; which exactly means that
$\left|\mathcal{M}\right|\subseteq Red_{A_{1}\times A_{2}}$ iff $M\in
Red_{A_{1}\times A_{2}}$.

  2. 2.

The reducibility candidates over $Red_{A}$ are $\Rightarrow$-saturated:
By a trivial induction on $\Rightarrow$ using the $\rightarrow$-saturation for
the $(R\text{-}trans)$ case.

  3. 3.

$Red_{A}$ is inhabited by a value:
By induction on $A$: $\boldsymbol{0}\in Red_{\mathtt{NAT}}$, $\lambda x.V\in
Red_{A\rightarrow B}$ and $\langle U,V\rangle\in Red_{A\times B}$ whenever
$U\in Red_{A}$ and $V\in Red_{B}$.

  4. 4.

The reducibility candidates $M$ over $Red_{A}$ $\Rightarrow$-reduce to
$\left\llbracket M\right\rrbracket_{a}$:
By induction on $A$:

     * •

Trivial for $A=\mathtt{NAT}$.

     * •

Let $M\in Red_{B\rightarrow C}$, there is a value $V\in Red_{B}$, thus $(M\
V)\in Red_{C}$ and $M\ V\Rightarrow\left\llbracket M\ V\right\rrbracket_{a}$
by IH; we can conclude using Lemma 19.

     * •

Similar for products.

  5. 5.

Every term $\vec{x}:\vec{A}\vdash M:B$ is a candidate in the sense that if
$\vec{V}\in\vec{Red_{A}}$ then $M[\vec{V}/\vec{x}]\in Red_{B}$:
By induction on the type derivation: The only difficult cases, the application
and the recursion and the binary probabilistic operator:

     * •

For the application: we have to show that if $M\in Red_{A\rightarrow B}$ and
$N\in Red_{A}$ then $(M\ N)\in Red_{B}$. But since $N\in Red_{A}$ we get that
$N\Rightarrow\left\llbracket N\right\rrbracket_{a}$ with $|\left\llbracket
N\right\rrbracket_{a}|\subseteq Red_{A}$. The means that $\left|M\
\left\llbracket N\right\rrbracket_{a}\right|\subseteq Red_{B}$ and that $M\
\left\llbracket N\right\rrbracket_{a}\Rightarrow\left\llbracket M\
\left\llbracket N\right\rrbracket_{a}\right\rrbracket_{a}$ supported into
$Red_{B}$. We conclude by Lemma 20 that $\mathcal{U}=\left\llbracket M\
N\right\rrbracket_{a}$ and thus that $(M\ N)\in Red_{B}$.

     * •

For the operator ${\mathtt{rec}}$: We have to show that if $U\in Red_{A}$ and
$V\in Red_{\mathtt{NAT}\rightarrow A\rightarrow A}$ then for all
$n\in\mathbb{N}$, $({\mathtt{rec}}\ \langle U,V,\boldsymbol{n}\rangle)\in
Red_{A}$. We proceed by induction on $n$:

       * •

If $n=0$: ${\mathtt{rec}}\ \langle
U,V,\boldsymbol{0}\rangle\rightarrow\\{U\\}\subseteq Red_{A}$ and we conclude
by saturation.

       * •

Otherwise: ${\mathtt{rec}}\ \langle
U,V,\boldsymbol{(n+1)}\rangle\rightarrow\\{V\ \boldsymbol{n}\ ({\mathtt{rec}}\
\langle U,V,\boldsymbol{n}\rangle)\\}\subseteq Red_{A}$ since
$({\mathtt{rec}}\ \langle U,V,\boldsymbol{n}\rangle)\in Red_{A}$ by IH and
since $\boldsymbol{n}\in Red_{\mathtt{NAT}}$ and $V\in
Red_{\mathtt{NAT}\rightarrow A\rightarrow A}$, we conclude by saturation.

     * •

For the operator $\oplus$: If $M,N\in Red_{A}$ then
$\left|\left\\{\begin{matrix}M\mapsto\frac{1}{2}\\\\[1.99997pt]
N\mapsto\frac{1}{2}\end{matrix}\right\\}\right|\subseteq Red_{A}$, and, by
$\rightarrow$-saturation, $(M\oplus N)\in Red_{A}$.

∎

Notice that this theorem dose not applies in $\mathbb{T}^{{\mathtt{X}}}$ (and
a fortiori in $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$) because the
step (5) of the proof would not be verified.

######  Theorem 22.

The accessible evaluation of a term $M\in\mathbb{T}^{\oplus,{\mathtt{R}}}$ is
its evaluation. Moreover, any term $M$ is almost surely terminating.

###### Proof.

By a trivial induction on $\Rightarrow$, we can easily show that if
$M\Rightarrow\mathcal{M}$ then $\left\llbracket
M\right\rrbracket=\left\llbracket\mathcal{M}\right\rrbracket$. In particular,
$\left\llbracket M\right\rrbracket=\left\llbracket\left\llbracket
M\right\rrbracket_{a}\right\rrbracket=\left\llbracket M\right\rrbracket_{a}$.

By a trivial induction on $\Rightarrow$ we can show that if
$M\Rightarrow\mathcal{N}$ then $||\mathcal{N}||=1$ and that if
$\mathcal{M}\Rightarrow\mathcal{N}$ then $||\mathcal{M}||=||\mathcal{N}||$. ∎

######  Corollary 23.

Any term $M\in\mathbb{T}^{\oplus}$ is positively almost-surely terminating.

###### Proof.

By an induction on $\Rightarrow$ we can show that if
$M\Rightarrow\left\llbracket M\right\rrbracket$ (resp.
$\mathcal{M}\Rightarrow\left\llbracket\mathcal{M}\right\rrbracket$ for
$\mathcal{M}$ finitely supported) then $M\rightarrow^{*}\left\llbracket
M\right\rrbracket$ (resp.
$\mathcal{M}\rightarrow^{*}\left\llbracket\mathcal{M}\right\rrbracket$):

  * •

$(R\text{-}refl)$ is trivial.

  * •

$(R\text{-}trans)$ is immediate once we remark that in $\mathbb{T}^{\oplus}$
whenever $M\rightarrow\mathcal{M}$, necessarily $\mathcal{M}$ is finitely
supported and we can use our induction hypothesis.

  * •

If for all $M\in\left|\mathcal{M}\right|$, $M\Rightarrow\left\llbracket
M\right\rrbracket$, then by IH, $M\rightarrow^{n_{M}}\left\llbracket
M\right\rrbracket$ for some $n_{M}\in\mathbb{N}$. Moreover, since
$\left|\mathcal{M}\right|$ is finite, we can set
$n=sup_{M\in\left|\mathcal{M}\right|}$ so that $M\rightarrow^{\leq
n}\left\llbracket M\right\rrbracket$ and $\mathcal{M}\rightarrow^{\leq
n}\int_{\mathcal{M}}\left\llbracket M\right\rrbracket
dM=\left\llbracket\mathcal{M}\right\rrbracket$.

The reduction time of a term is then bounded by $n$ such that
$M\rightarrow^{n}\left\llbracket M\right\rrbracket$. ∎

Notice that this theorem dose not applies in $\mathbb{T}^{{\mathtt{R}}}$ (and
a fortiori in $\mathbb{T}^{\oplus,{\mathtt{R}},{\mathtt{X}}}$) because the
second bullet of the proof would not be verified.

###  4.2 Mapping to $\mathbb{T}$

This positive almost sure convergence is not the only consequence of Theorem
22. In fact, the finitedness of the resulting distribution over values allows
a finite representation of $\mathbb{T}^{\oplus}$-distributions by
$\mathbb{T}$-definable functions.

Indeed, we can consider an extension of the usual system $T$ with a single
memory cell of type $\mathtt{NAT}$ that we use to store binary encoding of the
determination of every probabilistic choices during the execution. If we
denote $c$ the memory-cell, this means that the $\oplus$ can be
encoded:333Notice that conditionals, parity and fractions are easily
implementable in $\mathbb{T}$.

$(M\oplus N)^{*}\quad:=\quad{\mathtt{if}}\ ({\mathtt{mod}}_{2}\>c)\
{\mathtt{then}}\ (c{\mathtt{:=}}\frac{c}{2}\>;\>M^{*})\ {\mathtt{else}}\
(c{\mathtt{:=}}\frac{c}{2}\>;\>N^{*})$

From theorem 21, we know that for any $M\in\mathbb{T}^{\oplus}(\mathtt{NAT})$,
there is $n\in\mathbb{N}$ such that $M\rightarrow^{n}\left\llbracket
M\right\rrbracket$. Since the execution is bounded by $n$, there cannot be
more than $n$ successive probabilistic choice so that:

$\left\llbracket M\right\rrbracket=\left\\{k\mapsto\frac{\\#\\{m<2^{n}\mid
k=\mathtt{N\\!F}(c{\mathtt{:=}}\boldsymbol{m}\>;\>M^{*})\\}}{2^{n}}\right\\}.$

Using a well known state-passing style transformation, we can enforce
$(c{\mathtt{:=}}\boldsymbol{m}\>;\>M^{*})$ into a term of $\mathbb{T}$. Then,
using a simple recursive operation on $m$, we can represent the whole
$\\#\\{m<2^{n}\mid
k=\mathtt{N\\!F}(c{\mathtt{:=}}\boldsymbol{m}\>;\>M^{*})\\}$ into the result
of a term $k:\mathbb{N}\vdash M^{\prime}:\mathbb{N}$ so that $\lambda
k.M^{\prime}$ define a function that represent the distribution
$\left\llbracket M\right\rrbracket$.

######  Example 24.

Take the term $M\ =\ {\mathtt{rec}}\ \langle\boldsymbol{0},\ \lambda
xy.y\oplus{\mathtt{S}}y,\boldsymbol{2}\rangle$ from Example 17. Then the
encoding is

$M^{*}={\mathtt{rec}}\langle\boldsymbol{0},\ \lambda
xy.\>{\mathtt{if}}\>({\mathtt{mod}}\>c\>\boldsymbol{2})\>{\mathtt{then}}\>(c{\mathtt{:=}}\frac{c}{2}\>;\>y)\>{\mathtt{else}}\>(c{\mathtt{:=}}\frac{c}{2}\>;\>{\mathtt{S}}y),\
\boldsymbol{2}\rangle$

with a state passing style (and a few simplifications) we obtain the term:

$M^{\sim}\ =\ {\mathtt{rec}}\ \langle\lambda c.(\boldsymbol{0},c),\ \lambda
xyc.\>{\mathtt{if}}\>({\mathtt{mod}}\>c\>\boldsymbol{2})\>{\mathtt{then}}\>y\
({\mathtt{div}}\>c\>\boldsymbol{2})\>{\mathtt{else}}\>{\mathtt{S}}\ (y\
({\mathtt{div}}\>c\>\boldsymbol{2})),\ \boldsymbol{2}\rangle$

As we know that there is at most two choices, we can count the number of $c$
below $4$ which result to a certain $u$, we get:

$M^{\$}\ :=\ \lambda u.\>{\mathtt{rec}}\ \langle\boldsymbol{0},\ \lambda
xy.\>{\mathtt{if}}\ (\pi_{1}(M^{\sim}x)==u)\ {\mathtt{then}}\ {\mathtt{S}}y\
{\mathtt{else}}\ y,\ \boldsymbol{4}\rangle$

Then we have:

$\left\llbracket
M\right\rrbracket=\left\\{k\mapsto\frac{\mathtt{N\\!F}(M^{\$}\
\boldsymbol{k})}{4}\right\\}.$

Remains to show that this encoding can be parameterized in the sens that for
any $M\in\mathbb{T}^{\oplus}(\mathtt{NAT}\rightarrow\mathtt{NAT})$, we can
generate
$M_{\downarrow}\in\mathbb{T}(\mathtt{NAT}\rightarrow\mathtt{NAT}\rightarrow\mathtt{NAT})$
and $M_{\\#}\in\mathbb{T}(\mathtt{NAT}\rightarrow\mathtt{NAT})$ such that for
all $n\in\mathbb{N}$:

$\left\llbracket M\
\boldsymbol{n}\right\rrbracket\quad=\quad\left\\{\boldsymbol{k}\mapsto\frac{\\#\\{m<2^{\mathtt{N\\!F}(M_{\\#}\
\boldsymbol{n})}\mid k=\mathtt{N\\!F}(M_{\downarrow}\
\boldsymbol{n})\\}}{2^{\mathtt{N\\!F}(M_{\\#}\ \boldsymbol{n})}}\right\\}.$

The supplementary difficulty, here, comes from the bound $M_{\\#}$ that have
to be computed dynamically in a more complex monadic encoding.

First of all, let us define two maps $((\cdot))$ and
$((\cdot))_{\boldsymbol{V}}$ on types as follows:

$\displaystyle((A))$
$\displaystyle:=\bigl{(}\mathtt{NAT}\rightarrow((A))_{\boldsymbol{V}}\bigr{)}\times\mathtt{NAT}\>;$
$\displaystyle((\mathtt{NAT}))_{\boldsymbol{V}}$
$\displaystyle:=\mathtt{NAT}\>;$ $\displaystyle((A\rightarrow
B))_{\boldsymbol{V}}$
$\displaystyle:=((A))_{\boldsymbol{V}}\rightarrow((B))\>;$
$\displaystyle((A\times B))_{\boldsymbol{V}}$
$\displaystyle:=((A))_{\boldsymbol{V}}\times((B))_{\boldsymbol{V}}\>.$

This can be seen as the monadic lifting of the probabilistic monad. The
embedding is centered around two maps, $((\cdot))$ from $\mathbb{T}^{\oplus}$
terms to $\mathbb{T}$ terms and $((\cdot))_{\boldsymbol{V}}$ from
$\mathbb{T}^{\oplus}$ extended values to $\mathbb{T}$ extended values. These
maps are such that, whenever $\Gamma\vdash M\mathop{:}A$ and $\Gamma\vdash
V\mathop{:}A$, it holds that

$\displaystyle((\Gamma))_{\boldsymbol{V}}$
$\displaystyle\vdash((M))\mathop{:}((A))$
$\displaystyle((\Gamma))_{\boldsymbol{V}}$
$\displaystyle\vdash((V))_{\boldsymbol{V}}\mathop{:}((A))_{\boldsymbol{V}}\>.$

With a slight abuse of notation, we see the type $((A))$, which by definition
is a product type, as given through two components
$((A))_{\\!\downarrow}:=\mathtt{NAT}\rightarrow((A))_{\boldsymbol{V}}$ and
$((A))_{\\!\\#}:=\mathtt{NAT}$. Accordingly, we denote
$M_{\downarrow}:={\mathtt{\pi}}_{1}M:((A))_{\\!\downarrow}$ and
$M_{\\#}:={\mathtt{\pi}}_{2}M:((A))_{\\!\\#}$ whenever $M:((A))$. Similarly,
we may directly define $((M))_{\\!\downarrow}$ and $((M))_{\\!\\#}$ whenever
$((M))=\langle((M))_{\\!\downarrow},((M))_{\\!\\#}\rangle$.

We give a relatively precise (although laborious) definition of the maps
above. What is important for the rest of the development is that for every
natural number $n$, $((\boldsymbol{n}))_{\boldsymbol{V}}=\boldsymbol{n}$, and
that $((\lambda y.M))_{\boldsymbol{V}}=\lambda y.((M))$.

The encoding $((\cdot))_{\boldsymbol{V}}$ of extended values is given by:

$\displaystyle(({\mathtt{S}}))_{\boldsymbol{V}}$ $\displaystyle:=\lambda
y.(({\mathtt{S}}\ y))_{\boldsymbol{V}}$ $\displaystyle(({\mathtt{S}}\
V))_{\boldsymbol{V}}$ $\displaystyle:={\mathtt{S}}\ ((V))_{\boldsymbol{V}}$
$\displaystyle((\boldsymbol{0}))_{\boldsymbol{V}}$
$\displaystyle:=\boldsymbol{0}$ $\displaystyle((\langle
M,N\rangle))_{\boldsymbol{V}}$
$\displaystyle:=\langle((M))_{\boldsymbol{V}},((N))_{\boldsymbol{V}}\rangle$
$\displaystyle((\lambda x.M))_{\boldsymbol{V}}$ $\displaystyle:=\lambda
x.((M))$ $\displaystyle((x))_{\boldsymbol{V}}$ $\displaystyle:=x\hskip
50.00008pt$ $\displaystyle((\pi_{i}))_{\boldsymbol{V}}$
$\displaystyle:=\lambda x.{\mathtt{ret}}(\pi_{i}x)$
$\displaystyle(({\mathtt{rec}}))_{\boldsymbol{V}}$ $\displaystyle:=\hbox
to0.0pt{$\lambda\langle
u,v,w\rangle.{\mathtt{rec}}\>\langle{\mathtt{ret}}\>u,\>\lambda
xy.(vx){=}{<<}y,\>w\rangle$\hss}$

Where ${\mathtt{ret}}$ and ${=}{<<}$ are the return and the bind of the
considered monad:444Technically, this bind is not the usual bind, but a lifted
version.

$\displaystyle{\mathtt{ret}}$
$\displaystyle:((A))_{\boldsymbol{V}}\rightarrow((A))$
$\displaystyle{\mathtt{ret}}$ $\displaystyle:=\lambda x.\langle\lambda
y.x,\;\boldsymbol{0}\rangle$ $\displaystyle\\_{=}{<<}\\_$
$\displaystyle:((A\rightarrow B))\times((A))\rightarrow((B))$ $\displaystyle
M{=}{<<}N$ $\displaystyle:=\langle
M{=}{<<}_{\downarrow}N,M{=}{<<}_{\\#}N\rangle$

However, the computation of the bind is extremely complex. Intuitively, the
right part is computing the number of choices in $M$ in $N$ and in all the
possibles outcomes $(U\ V)$ for $U\in\left|\left\llbracket
M\right\rrbracket\right|$ and $V\in\left|\left\llbracket
N\right\rrbracket\right|$; off course we take the sup of those outcomes as
they are independent:

$\displaystyle\\_{=}{<<}_{\\#}\\_$
$\displaystyle:((A{\rightarrow}B))\times((A))\rightarrow\mathtt{NAT}$
$\displaystyle M{=}{<<}_{\\#}N$
$\displaystyle:=M_{\\#}+N_{\\#}+\mathop{{\mathtt{max}}}_{x<2^{M_{\\#}}}\mathop{{\mathtt{max}}}_{y<2^{N_{\\#}}}(M_{\downarrow}\
x\ (N_{\downarrow}\ y))_{\\#}$

where we use the following syntactical sugar:

$\displaystyle\\_+\\_$
$\displaystyle:\mathtt{NAT}\times\mathtt{NAT}\rightarrow\mathtt{NAT}$
$\displaystyle M+N$ $\displaystyle:={\mathtt{rec}}\langle
M,\>\lambda\\_x.{\mathtt{S}}x,\>N\rangle$ $\displaystyle 2^{\>\\_}$
$\displaystyle:\mathtt{NAT}\rightarrow\mathtt{NAT}$ $\displaystyle 2^{M}$
$\displaystyle:={\mathtt{rec}}\langle\boldsymbol{1},\>\lambda\\_y.{\mathtt{rec}}\langle
y,\lambda\\_v.{\mathtt{S}}v,y\rangle,\>M\rangle$
$\displaystyle\mathop{{\mathtt{max}}}_{x<M}(N)$
$\displaystyle:={\mathtt{rec}}\langle\boldsymbol{0},\>\lambda\\_y.\>N{\vee}y,\>M\rangle$
$\displaystyle\\_\vee\\_$
$\displaystyle:\mathtt{NAT}\times\mathtt{NAT}\rightarrow\mathtt{NAT}$
$\displaystyle M\vee N$ $\displaystyle:={\mathtt{rec}}\langle\lambda
u.u,\>\lambda xyu.{\mathtt{S}}({\mathtt{rec}}\langle x,\lambda
a\\_.ya,u\rangle),\ M\rangle\ N$

The first member of the bind is also complex. It is taking a streams of
probabilistic choices $s$, computing $M$ over this choices, then we have to
shift the stream $s$ in order to remove the choices relative to $M$, this way
we can compute the result from $N$, that we can give to the result from $N$.
After this, we obtain an object of type $((B))$; but we have not finished: we
have to select the first member, to which we give what remain of the stream
(computed by shifting $x$ twice).

$\displaystyle\\_{=}{<<}_{\downarrow\>}\\_$
$\displaystyle:((A{\rightarrow}B))\times((A))\rightarrow\mathtt{NAT}\rightarrow((B))_{\boldsymbol{V}}$
$\displaystyle M{=}{<<}_{\downarrow\>}N$ $\displaystyle:=\lambda
s.(M_{\downarrow}\ s\ (N_{\downarrow}\ ({\mathtt{shift}}\ s\
M_{\\#})))_{\downarrow}\ ({\mathtt{shift}}\ s\ (M_{\\#}{+}N_{\\#}))$

where we use the following syntactical sugar:

$\displaystyle{\mathtt{shift}}$
$\displaystyle:\mathtt{NAT}\rightarrow\mathtt{NAT}\rightarrow\mathtt{NAT}$
$\displaystyle{\mathtt{shift}}$ $\displaystyle:=\lambda
sy.{\mathtt{rec}}\langle s,\>\lambda u.div_{2},\>y\rangle$
$\displaystyle{\mathtt{div_{2}}}$
$\displaystyle:\mathtt{NAT}\rightarrow\mathtt{NAT}$
$\displaystyle{\mathtt{div_{2}}}$ $\displaystyle:=\lambda
x.{\mathtt{rec}}\langle\lambda\\_.\boldsymbol{0},\>\lambda\\_vw.{\mathtt{ite}}\langle
w,{\mathtt{S}}(v\boldsymbol{0}),v\boldsymbol{1}\rangle,\>\ x\rangle\
\boldsymbol{0}$

The encoding $((\cdot))$ is given by the return and the bind operations :

$\displaystyle((V))$ $\displaystyle:={\mathtt{ret}}\ ((V))_{\boldsymbol{V}}$
$\displaystyle((M\ N))$ $\displaystyle:=((M)){=}{<<}((N))$

The binary choice is the defined as intuited:

$\displaystyle((M\oplus N))_{\\!\\#}$
$\displaystyle:=((M))_{\\!\\#}{\vee}((N))_{\\!\\#}$ $\displaystyle((M\oplus
N))_{\\!\downarrow}$ $\displaystyle:=\lambda
x.{\mathtt{ite}}\langle{\mathtt{mod_{2}}}x,\>((M))_{\\!\downarrow}({\mathtt{div_{2}}}x),\>((N))_{\\!\downarrow}({\mathtt{div_{2}}}x)\rangle$

where we use the following syntactical sugar:

$\displaystyle{\mathtt{ite}}$ $\displaystyle:\mathtt{NAT}\times A\times
A\rightarrow A$ $\displaystyle{\mathtt{ite}}$ $\displaystyle:=\lambda
x.{\mathtt{rec}}\ \langle\pi_{3}x,\>\lambda\\_\\_.\pi_{2}x,\>\pi_{1}x\rangle\
.$ $\displaystyle{\mathtt{mod_{2}}}$
$\displaystyle:\mathtt{NAT}\rightarrow\mathtt{NAT}$
$\displaystyle{\mathtt{mod_{2}}}$ $\displaystyle:=\lambda
x.{\mathtt{rec}}\langle\boldsymbol{0},\>\lambda\\_v.{\mathtt{ite}}\langle
v,\boldsymbol{0},\boldsymbol{1}\rangle,\>\ x\rangle$

######  Theorem 25.

Distributions in $\mathbb{T}^{\oplus}$ are finitely parameterically
representable by $\mathbb{T}$-definable functions, i.e. for any
$M:\mathtt{NAT}\rightarrow\mathtt{NAT}$ in $\mathbb{T}^{\oplus}$ there is
$F:\mathtt{NAT}\rightarrow\mathtt{NAT}\rightarrow\mathtt{BIN}$ and
$Q:\mathtt{NAT}\rightarrow\mathtt{NAT}$ in $\mathbb{T}$ such that for all $n$:

$\left\llbracket M\ \boldsymbol{n}\right\rrbracket\ =\
\left\\{\boldsymbol{k}\mapsto\mathtt{N\\!F}(F\ \boldsymbol{n}\
\boldsymbol{k})\right\\}\quad\quad\quad\forall k\geq\mathtt{N\\!F}(Q\
\boldsymbol{n}),\ \mathtt{N\\!F}(F\ \boldsymbol{n}\
\boldsymbol{k})=\boldsymbol{0}.$

##  5 Countable Probabilistic Choice

###  5.1 Multistep semantics

We have seen that none of Theorems 21, 22 and 23, about the multistep
semantics, hold anymore for the $\mathbb{T}^{{\mathtt{X}}}$. Indeed Theorem
21, which is a premise to the two others, is broken by the term
${\mathtt{X}}\langle\boldsymbol{0},{\mathtt{S}}\rangle$ that will never
$\Rightarrow$-reduce to a value distribution.

The fragment $\mathbb{T}^{{\mathtt{R}}}$ is more interesting as both Theorem
21 and Theorem 22 hold. However, as we have seen in Theorem 14, the positive
almost sure normalization (and Theorem 23) does not hold. This is because we
are manipulating infinitely supported distributions (due to the reduction rule
of ${\mathtt{R}}$).

######  Example 26.

Recall that ${\mathtt{X}}_{\mathtt{R}}\ :=\ \lambda x.{\mathtt{rec}}\
\langle\pi_{2}x,\lambda z.\pi_{1}x,{\mathtt{R}}\rangle$ is the encoding of
${\mathtt{X}}$ into $\mathbb{T}^{{\mathtt{R}}}$. We have
${\mathtt{X}}_{\mathtt{R}}\
\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\Rightarrow\\{\boldsymbol{2n}\mapsto\frac{1}{2^{n+1}}\mid
n\geq 0\\}$; indeed, if we fix $U_{n}={\mathtt{rec}}\
\langle\pi_{2}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle,\lambda
z.\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle,\boldsymbol{n}\rangle$:

$(R\text{-}refl)$ $\boldsymbol{0}\Rightarrow\\{\boldsymbol{0}\\}$
$(R\text{-}{\in})$
$\pi_{2}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\rightarrow\
$$\\{\boldsymbol{0}\\}\Rightarrow\\{\boldsymbol{0}\\}$ $(R\text{-}tran)$
$\pi_{2}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\Rightarrow\\{\boldsymbol{0}\\}$
$(R\text{-}{\in})$ $U_{0}\rightarrow\
$$\\{\pi_{2}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\\}\Rightarrow\\{\boldsymbol{0}\\}$
$(R\text{-}tran)\hskip 42.00009pt$ $U_{0}\Rightarrow\\{\boldsymbol{0}\\}$
$(R\text{-}refl)$ ${\mathtt{S}}{\mathtt{S}}\
\boldsymbol{0}\Rightarrow\\{\boldsymbol{2}\\}$ $(R\text{-}{\in})$
$\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>\boldsymbol{0}\rightarrow\
$ $\\{{\mathtt{S}}{\mathtt{S}}\
\boldsymbol{0}\\}\Rightarrow\\{\boldsymbol{2}\\}$ $(R\text{-}tran)$
$\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>\boldsymbol{0}\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$
$\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>(\pi_{2}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle)\rightarrow\
$$\\{\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>\boldsymbol{0}\\}\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$
$\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>(\pi_{2}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle)\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$
$\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>U_{0}\rightarrow\
$$\\{\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>(\pi_{2}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle)\\}\Rightarrow\\{\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>\boldsymbol{0}\\}$
$(R\text{-}tran)$
$\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>U_{0}\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}{\in})$ $U_{1}\rightarrow\
$$\\{\pi_{1}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\>U_{0}\\}\Rightarrow\\{\boldsymbol{2}\\}$
$(R\text{-}tran)$ $U_{1}\Rightarrow\\{\boldsymbol{2}\\}$ $\cdots$
$(R\text{-}{\in})$ $U_{\mathtt{R}}\rightarrow\
$$\\{U_{n}\mapsto\frac{1}{2^{n+1}}\mid n\geq
0\\}\Rightarrow\\{\boldsymbol{2n}\mapsto\frac{1}{2^{n+1}}\mid n\geq 0\\}$
$(R\text{-}tran)$ $U_{\mathtt{R}}\Rightarrow\mathcal{N}$ $(R\text{-}{\in})$
${\mathtt{X}}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\rightarrow$$\\{U_{\mathtt{R}}\\}\Rightarrow\\{\boldsymbol{2n}\mapsto\frac{1}{2^{n+1}}\mid
n\geq 0\\}$ $(R\text{-}tran)$
${\mathtt{X}}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\Rightarrow\
\\{\boldsymbol{2n}\mapsto\frac{1}{2^{n+1}}\mid n\geq 0\\}$

we can see that the tree is infinite due to the second application of
$(R\text{-}{\in})$; but, despite being infinite, and with an infinite height,
each subtree above the second application of $(R\text{-}{\in})$ is finite,
making the derivation correct.

However,
${\mathtt{X}}_{\mathtt{R}}\langle\boldsymbol{0},{\mathtt{S}}{\mathtt{S}}\rangle\not\Rightarrow\\{\boldsymbol{2n}\mapsto\frac{1}{2^{n+1}}\mid
n\geq 0\\}$. We can aproach this distribution, but it is impossible to
$\Rightarrow$-reduce to a value distribution.

Remember that $\mathbb{T}^{{\mathtt{R}}}$ and $\mathbb{T}^{{\mathtt{X}}}$ are
equivalent, so why such a difference? This is due to the difference of nature
in their execution trees. Indeed, we have seen that the execution trees of
$\mathbb{T}^{{\mathtt{X}}}$ are finitely branching, but with infinite paths,
while those of $\mathbb{T}^{{\mathtt{R}}}$ are infinitely branching, but with
finite paths. The inference of the multistep reduction following those
execution trees, we can see that we only need derivations with infinite arity
to get a correct multistep semantics for $\mathbb{T}^{{\mathtt{R}}}$.

The whole point is that we can perform transfinite structural inductions over
these trees. Indeed, by considering the reduction trees themselves with the
inclusion (or subtree) order gives you a well-founded poset, recalling that
there is no infinite path. If one want to unfold this well-founded poset into
an ordinal, then it should be the smallest ordinal $o$ such that $o=1+\omega
o$, i.e. $o=\omega^{\omega}$.

Remark that, due to the encoding of $\oplus$ and ${\mathtt{X}}$ into
$\mathbb{T}^{{\mathtt{R}}}$, Theorem 22 is subsuming Theorem 12. Remark,
moreover, that we did not have to go thought the definition of approximants.
Nonetheless, those approximants exists and point out that morally
$\mathbb{T}^{\oplus}$ should be approximating $\mathbb{T}^{{\mathtt{R}}}$ is
some way or another.

###  5.2 The approximants: State-Bounded Random Integers

In this section, we show that $\mathbb{T}^{\oplus}$ approximates
$\mathbb{T}^{{\mathtt{R}}}$: for any term
$M\in\mathbb{T}^{{\mathtt{R}}}(\mathtt{NAT})$, there is a term
$N\in\mathbb{T}^{\oplus}(\mathtt{NAT}\rightarrow\mathtt{NAT})$ that represents
a sequence approximating $M$ uniformly. We will here make strong use of the
fact that $M$ has type $\mathtt{NAT}$. This is a natural drawback when we
understand that the encoding $(\cdot)^{\dagger}$ on which the result above is
based is not direct, but goes through an other state passing style
transformation. Nonetheless, everything can be lifted easily to the first
order, achieving the parameterization of our theorem.

A naive idea would be to use $\mathbb{T}^{{\mathtt{X}}}$ and to stope the
evaluation after a given reduction time as schematised in Figure 10. Despite
the encoding to be a nightmare, this should be encodable in
$\mathbb{T}^{\oplus}$. However, for the convergence time to be independant
from the term and uniform, ther is vitually no hope. That is why we have
swiched to $\mathbb{T}^{{\mathtt{R}}}$ which carries much nicer properties as
seen in the previous chapter.

The basic idea behind the embedding $(\cdot)^{\dagger}$ is to mimic any
instance of the ${\mathtt{R}}$ operator in the source term by some term
$\boldsymbol{0}\oplus(\boldsymbol{1}\oplus(\cdots(\boldsymbol{n}\oplus\bot)\cdots\\!)$,
where $n$ is _sufficiently large_ , and $\bot$ is an arbitrary value of type
$\mathtt{NAT}$. Of course, the semantics of this term is _not_ the same as
that of ${\mathtt{R}}$, due to the presence of $\bot$; however, $n$ will be
chosen sufficiently large for the difference to be negligible. Notice,
moreover, that this term can be generalized into the following parametric form
${\mathtt{R}}^{\ddagger}:=\lambda n.{\mathtt{rec}}\ \bot\ (\lambda
x.{\mathtt{S}}\oplus(\lambda y.\boldsymbol{0}))\ n$.

${\mathtt{R}}^{\ddagger}\
\boldsymbol{n}$$\boldsymbol{0}$$\boldsymbol{1}$$\boldsymbol{2}$$\boldsymbol{3}$$\cdots\vphantom{1}\\!\cdots$$\boldsymbol{n}$$\bot$$\bot$$\bot$$\cdots\vphantom{1}\\!\cdots$$\frac{1}{2}\
\ \ \phantom{.}$$\frac{1}{4_{\vphantom{1}}}$$\frac{1}{8}$

Once ${\mathtt{R}}^{\ddagger}$ is available, a natural candidate for the
encoding $(\cdot)^{\dagger}$ would be to consider something like
$M^{\ddagger}:=\lambda z.M[({\mathtt{R}}^{\ddagger}\ z)/{\mathtt{R}}]$. In the
underlying execution tree, $(M^{\ddagger}\ \boldsymbol{n})$ correctly
simulates the first $n$ branches of each ${\mathtt{R}}$ (which had infinite-
arity), but truncates the rest with garbage terms $\bot$. As schematized in
Figure 10, by increasing $n$, we can hope to obtain the $M$ at the limit.

The question is whether the remaining untruncated tree has a “sufficient
weight”, i.e., that there is a minimal bound to the probability to stay in
this untruncated tree. However, in general $(\cdot)^{\ddagger}$ fails on this
point, not achieving to approximate $M$ uniformly. In fact, this probability
is basically $(1-\frac{1}{2^{n}})^{d}$ where $d$ is its depth. Since in
general the depth of the untruncated tree can grow very rapidly on $n$ in a
powerful system like $\mathbb{T}$ , there is no hope for this transformation
to perform a uniform approximation.

… Figure 8:
Horizontal truncature of $\mathbb{T}^{\oplus}$ Figure 9:
Vertical truncatur of $\mathbb{T}^{{\mathtt{R}}}$ Figure 10:
Biaised Tuncatur of $\mathbb{T}^{{\mathtt{R}}}$

It may well be possible to perform a complex monadic transformation in the
syle of Section 4.2, that computes a function relating the size $n$ of the
truncature to the depth $d$ of the execution tree. But there is a much easyer
solution.

The solution we are using is to have the precision $m$ of
$\boldsymbol{0}\oplus(\boldsymbol{1}\oplus(\cdots(\boldsymbol{m}\oplus\bot)\cdots))$
to dynamically grow along the computation, as schematized in Figure 10. More
specifically, in the approximants $M^{\dagger}\boldsymbol{n}$, the growing
speed of $m$ will increase with $n$: in the $n$-th approximant
$M^{\dagger}\boldsymbol{n}$, ${\mathtt{R}}$ will be simulated as
$\boldsymbol{0}\oplus\boldsymbol{(}1\oplus(\cdots(\boldsymbol{m}\oplus\bot)\cdots))$
_and_ , somehow, $m$ will be updated to $m+n$. Why does it work? Simply
because even for an (hypothetical) infinite and complete execution tree of
$M$, we would stay inside the $n^{th}$ untruncated tree with probability
$\prod_{k\geq 0}(1-\frac{1}{2^{k*n}})$ which is asymptotically above
$(1-\frac{1}{n})$.

Implementing this scheme in $\mathbb{T}^{\oplus}$ requires a feature which is
not available (but which can be encoded), namely ground-type references. We
then prefer to show that the just described scheme can be realized in an
intermediate language called $\mathbb{T}^{\boldsymbol{\bar{\mathtt{R}}}}$,
whose operational semantics is formulated not on _terms_ , but rather on
triples in the form $(M,m,n)$, where $M$ is the term currently being
evaluated, $m$ is the current approximation threshold value, and $n$ is the
value of which $m$ is incremented whenever ${\mathtt{R}}$ is simulated. The
operational semantics is standard, except for the following rule:

$(r\text{-}\boldsymbol{\bar{\mathtt{R}}})$
$(\boldsymbol{\bar{\mathtt{R}}},m,n)\rightarrow\Bigl{\\{}(k,m{+}n,n)\mapsto\frac{1}{2^{k+1}}\mid
k<m\Bigr{\\}}$

Notice how this operator behaves similarly to ${\mathtt{R}}$ with the
exception that it fails when drawing too big of a number (i.e., bigger that
the fist state $m$). Notice that the failure is represented by the fact that
the resulting distribution does not necessarily sum to $1$. The intermediate
language $\mathbb{T}^{\boldsymbol{\bar{\mathtt{R}}}}$ is able to approximate
$\mathbb{T}^{{\mathtt{R}}}$ at every order (Theorem 31 below). Moreover, the
two memory cells can be shown to be expressible in $\mathbb{T}^{\oplus}$,
again by way of a continuation-passing transformation. Crucially, the initial
value of $n$ can be passed as an argument to the encoded term.

######  Definition 27.

For any $M\in\mathbb{T}^{{\mathtt{R}}}$ we denote
$M^{*}:=M[\boldsymbol{\bar{\mathtt{R}}}/{\mathtt{R}}]$. We say that
$(M,m,n)\in\mathbb{T}^{\boldsymbol{\bar{\mathtt{R}}}}$ if $m,n\in\mathbb{N}$
and $M=N^{*}$ for some $N\in\mathbb{T}^{{\mathtt{R}}}$. Similarly,
$\mathfrak{D}(\mathbb{T}^{\boldsymbol{\bar{\mathtt{R}}}})$ is the set of
probabilistic distributions over
$\mathbb{T}^{\boldsymbol{\bar{\mathtt{R}}}}\times\mathbb{N}^{2}$, i.e., over
the terms plus states. The reduction rules of the system T with state-bounded
random integers are given by Figure 11.

M $(s\text{-}\beta)$ $(\lambda x.M,m,n)\
V\rightarrow\Bigl{\\{}(M[V/x],m,n)\Bigr{\\}}$ $(M,m,n)\rightarrow\mathcal{M}$
$(s\text{-}c@L)$ $(M\ V,m,n)\rightarrow\mathcal{M}\ V\vphantom{\Bigl{\\{}}$
$(N,m,n)\rightarrow\mathcal{N}$ $(s\text{-}c@R)$ $(M\ N,m,n)\rightarrow M\
\mathcal{N}\vphantom{\Bigl{\\{}}$ $(s\text{-}{\mathtt{rec}}\boldsymbol{0})$
$({\mathtt{rec}}\ U\ V,m,n)\
\boldsymbol{0}\rightarrow\Bigl{\\{}(U,m,n)\Bigr{\\}}$
$(s\text{-}{\mathtt{rec}}{\mathtt{S}})$ $({\mathtt{rec}}\ U\ V\ ({\mathtt{S}}\
\boldsymbol{k}),\ m,n)\rightarrow\Bigl{\\{}(V\ \boldsymbol{k}\
({\mathtt{rec}}\ U\ V\ \boldsymbol{k}),m,n)\Bigr{\\}}$
$(s\text{-}{\mathtt{\pi}}_{1})$ $\\!({\mathtt{\pi}}_{1}\ \langle
M,N\rangle,m,n)\rightarrow\Bigl{\\{}(M,m,n)\Bigr{\\}}\\!$
$(s\text{-}{\mathtt{\pi}}_{2})$ $\\!({\mathtt{\pi}}_{2}\ \langle
M,N\rangle,m,n)\rightarrow\Bigl{\\{}(N,m,n)\Bigr{\\}}\\!$
$(s\text{-}\boldsymbol{\bar{\mathtt{R}}})$
$(\boldsymbol{\bar{\mathtt{R}}},m,n)\rightarrow\left\\{\begin{matrix}(k,m+n,n)\mapsto\frac{1}{2^{k+1}},\
\text{if }k<m\quad\\\ (N,m^{\prime},n^{\prime})\mapsto
0,\quad\text{otherwise}\end{matrix}\right\\}$
$\forall(M,m,n)\in\left|\mathcal{M}\right|,\
(M,m,n)\rightarrow^{?}\mathcal{N}_{(M,m,n)}$ $(s\text{-}{\in})$
$\mathcal{M}\rightarrow\int_{\mathcal{M}}\mathcal{N}_{M,m,n}.dMdmdn$ Figure
11: Operational semantics. Except for the $M$ in $(b\text{-}\beta)$ that can
have $x$ as a free variable, all terms and distributions are closed. Notice
that $\rightarrow^{?}$ stands for the identity if the premise is a value and
for $\rightarrow$ otherwise.

For any $m$ and $n$, the behavior of $M$ and $(M^{*},m,n)$ are similar, except
that $(M^{*},m,n)$ will “fail” more often. In other words, all
$(M^{*},m,n)_{m,n\in\mathbb{N}}$ are good candidates in order to approach $M$
from bellow:

######  Lemma 28.

For any $M\in\mathbb{T}^{{\mathtt{R}}}$ and any $m,n\in\mathbb{N}$,
$\left\llbracket M\right\rrbracket\succeq\left\llbracket
M^{*},m,n\right\rrbracket$, i.e., for every
$V\in\mathbb{T}^{{\mathtt{R}}}_{V}$, we have

$\left\llbracket
M\right\rrbracket(V)\geq\sum_{m^{\prime},n^{\prime}}\left\llbracket
M^{*},m,n\right\rrbracket(V^{*},m^{\prime},n^{\prime}).$

###### Proof.

By an easy induction, one can show that for any
$\mathcal{M}\in\mathfrak{D}(\mathbb{T}^{{\mathtt{R}}})$ and
$\mathcal{N}\in\mathfrak{D}(\mathbb{T}^{\boldsymbol{\bar{\mathtt{R}}}})$ if
$\mathcal{M}\succeq\mathcal{N}$, $\mathcal{M}\rightarrow\mathcal{M}^{\prime}$
and $\mathcal{N}\rightarrow\mathcal{N}^{\prime}$, then
$\mathcal{M}^{\prime}\succeq\mathcal{N}^{\prime}$. This ordering is then
preserved at the limit so that we get our result. ∎

In fact, the probability of “failure” of any $(M,m,n)_{m,n\in\mathbb{N}}$ can
be upper-bounded explicitly. More precisely, we can find an infinite product
underapproximating the success rate of $(M,m,n)$ by reasoning inductively over
$(M,m,n)\Rightarrow\left\llbracket(M,m,n)\right\rrbracket$, which is possible
because of PAST.

######  Lemma 29.

For any $M\in\mathbb{T}^{\boldsymbol{\bar{\mathtt{R}}}}$ and any $m,n\geq 1$

$Succ(M,m,n)\geq\prod_{k\geq 0}\Bigl{(}1-\frac{1}{2^{m+kn}}\Bigr{)}.$

###### Proof.

We denote

$\\#(m,n):=\prod_{k\geq
0}\Bigl{(}1-\frac{1}{2^{m+kn}}\Bigr{)}\quad\quad\text{and}\quad\quad\\#\mathcal{M}:=\int_{\mathcal{M}}\\#(m,n)\;dMdmdn.$

By induction on $\Rightarrow$, we can show that if
$(M,m,n)\Rightarrow\mathcal{M}$ then $\\#\mathcal{M}=\\#(m,n)$ and that if
$\mathcal{N}\Rightarrow\mathcal{M}$ then $\\#\mathcal{M}=\\#\mathcal{N}$.

  * •

$(R\text{-}refl)$ and $(R\text{-}int)$ are immediate.

  * •

If $(M,m,n)\rightarrow\mathcal{N}\Rightarrow\mathcal{M}$ then $\mathcal{N}$ is
either of the form $\\{(N,m,n)\\}$ or
$\\{(N_{i},m+n,n)\mapsto\frac{1}{2^{i+1}}\mid i<m\\}$ for some $N$ of
$(N_{i})_{i\leq m}$. In the first case it is clear that
$\\#\mathcal{N}=\\#(m,n)$, but the equality hold also in the second:

$\\#\mathcal{N}\quad=\quad\sum_{i\leq
m}\frac{1}{2^{i+1}}\\#(m+n,n)\quad=\quad(1-\frac{1}{2^{m}})\\#(m+n,n)\quad=\quad\\#(m,n).$

By IH, we conclude that $\\#\mathcal{M}=\\#\mathcal{N}=\\#(m,n)$.

In particular we have

$\displaystyle Succ(M,m,n)$ $\displaystyle:=\int_{\left\llbracket
M,m,n\right\rrbracket}1\ dMdmdn$ $\displaystyle\geq\\#\left\llbracket
M\right\rrbracket$ $\displaystyle\text{since }\forall m,n,\ \ 1\geq\\#(m,n)$
$\displaystyle=\\#(m,n)$ $\displaystyle\text{since
}(M,m,n)\Rightarrow\left\llbracket M,m,n\right\rrbracket.$

∎

This gives us an analytic lower bound to the success rate of $(M,m,n)$.
However, it is not obvious that this infinite product is an interesting bound,
it is not even clear that it can be different from $0$. This is why we will
further underapproximate this infinite product to get a simpler expression
whenever $m=n$:

######  Lemma 30.

For any $M\in\mathbb{T}^{\boldsymbol{\bar{\mathtt{R}}}}$ and any $n\geq 4$

$Succ(M,n,n)\quad\geq\quad 1-\frac{1}{n}.$

###### Proof.

By Lemma 29 we have that $Succ(M,n,n)\geq\prod_{k\geq
1}\bigl{(}1-\frac{1}{2^{k*n}}\bigr{)}$ which is above the product
$\prod_{k\geq 1}\bigl{(}1-\frac{1}{n^{2}k^{2}}\bigr{)}$ whenever $n\geq 4$.
This infinite product has been shown by Euler to be equal to
$\frac{sin(\frac{\pi}{n})}{\frac{\pi}{n}}$. By an easy numerical analysis we
then obtain that $\frac{sin(\frac{\pi}{n})}{\frac{\pi}{n}}\geq 1-\frac{1}{n}$.
∎

This lemma can be restated by saying that the probability of “failure” of
$(M^{*},n,n)$, i.e. the difference between $\left\llbracket
M^{*},n,n\right\rrbracket$ and $\left\llbracket M\right\rrbracket$, is bounded
by $\frac{1}{n}$. With this we then get our first theorem, which is the
uniform approximability of elements of $\mathbb{T}^{{\mathtt{R}}}$ by those of
$\mathbb{T}^{\boldsymbol{\bar{\mathtt{R}}}}$:

######  Theorem 31.

For any $M\in\mathbb{T}^{{\mathtt{R}}}$ and any $n\in\mathbb{N}$,

$\sum_{V}\ \Bigl{|}\ \left\llbracket M\right\rrbracket(V)\ -\
\Sigma_{m^{\prime},n^{\prime}}\left\llbracket
M^{*},n,n\right\rrbracket(V^{*},m^{\prime},n^{\prime})\
\Bigr{|}\quad\leq\quad\frac{1}{n}.$

###### Proof.

By Lemma 28, for each $V$ the difference is positive, thus we can remove the
absolute value and distribute the sum. We conclude by using the fact that
$SuccM=1$ and $Succ(M^{*},n,n)\geq 1-\frac{1}{n}$. ∎

The second theorem, i.e., the uniform approximability of ground elements of
$\mathbb{T}^{{\mathtt{R}}}$ by those of $\mathbb{T}^{\oplus}$, follows
immediately:

######  Theorem 32.

Distributions in $\mathbb{T}^{{\mathtt{R}}}(\mathtt{NAT})$ can be approximated
by $\mathbb{T}^{\oplus}$-distributions (which are finitely
$\mathbb{T}$-representable), i.e., for any
$M\in\mathbb{T}^{{\mathtt{R}}}(\mathtt{NAT})$, there is
$M^{\dagger}\in\mathbb{T}^{\oplus}(\mathbb{N})$ such that:

$\forall n,\quad\sum_{k}\ \Bigl{|}\ \left\llbracket
M\right\rrbracket(\boldsymbol{k})\ -\ \left\llbracket M^{\dagger}\
\boldsymbol{n}\right\rrbracket(\boldsymbol{k})\
\Bigr{|}\quad\leq\quad\frac{1}{n}.$

Moreover:

  * •

the encoding is parameterizable in the sens that for all
$M\in\mathbb{T}^{{\mathtt{R}}}(\mathtt{NAT}\rightarrow\mathtt{NAT})$, there is
$M^{\dagger}\in\mathbb{T}^{\oplus}(\mathtt{NAT}\rightarrow\mathtt{NAT})$ such
that $(M\ \boldsymbol{n})^{\dagger}=M^{\dagger}\ \boldsymbol{n}$ for all
$n\in\mathbb{N}$,

  * •

the encoding is such that $\left\llbracket
M\right\rrbracket(\boldsymbol{k})\leq\left\llbracket M^{\dagger}\
\boldsymbol{n}\right\rrbracket(\boldsymbol{k})$ possible only for $k=0$.

###### Proof.

It is clear that in an extension of $\mathbb{T}^{\oplus}$ with two global
memory cells $m,n$ and with exceptions, the $\boldsymbol{\bar{\mathtt{R}}}$
operator can be encoded by

$\boldsymbol{\bar{\mathtt{R}}}\quad:=\quad{\mathtt{rec}}\langle\lambda
u.\bot,\>\lambda xyu.\>\boldsymbol{0}\oplus{\mathtt{S}}(y\ u),\
m:=!m+!n\rangle\ \boldsymbol{0},$

where $\bot$ is raising an error/exception and $m:=!m+!n$ is returning the
value of $m$ before changing the memory cell to $m+n$. Remark that the only
objective of the dummy abstraction over $u$ and of the dummy aplication to
$\boldsymbol{0}$, is to block the evaluation of the $\bot$. We can conclude by
referring to the usual state passing style encoding of exceptions and state-
monads into $\mathbb{T}$ (and thus into $\mathbb{T}^{\oplus}$).

In fact, we do not have any requirement over the $\bot$ since we are just
majoring the divergence toward a required result. This means that we can
replace $\bot$ by any value $\bot_{A}$ of the correct type $A$ (which is
possible since every type is inhabited). Then we do not need to implement the
exception monad, but only the state monad which we can present easily here:

$\displaystyle((A))$
$\displaystyle:=\mathtt{NAT}^{3}\rightarrow(((A))_{\boldsymbol{V}}\times\mathtt{NAT}^{3})$
$\displaystyle((\mathtt{NAT}))_{\boldsymbol{V}}$ $\displaystyle:=\mathtt{NAT}$
$\displaystyle((A\rightarrow B))_{\boldsymbol{V}}$
$\displaystyle:=((A))_{\boldsymbol{V}}\rightarrow((B))$
$\displaystyle((A\times B))_{\boldsymbol{V}}$
$\displaystyle:=((A))\times((B))$

Where the first state is monitoring the presence of an error along the
reduction, the second represents the state $m$ and the third represents the
state $n$.

The encoding $((-))_{\boldsymbol{V}}$ of extended values is the same as for
the encoding of Section 4.2:

$\displaystyle(({\mathtt{S}}))_{\boldsymbol{V}}$ $\displaystyle:=\lambda
y.(({\mathtt{S}}\ y))_{\boldsymbol{V}}$ $\displaystyle(({\mathtt{S}}\
V))_{\boldsymbol{V}}$ $\displaystyle:={\mathtt{S}}\ ((V))_{\boldsymbol{V}}$
$\displaystyle((\boldsymbol{0}))_{\boldsymbol{V}}$
$\displaystyle:=\boldsymbol{0}$ $\displaystyle((\langle
M,N\rangle))_{\boldsymbol{V}}$
$\displaystyle:=\langle((M))_{\boldsymbol{V}},((N))_{\boldsymbol{V}}\rangle$
$\displaystyle((\lambda x.M))_{\boldsymbol{V}}$ $\displaystyle:=\lambda
x.((M))$ $\displaystyle((x))_{\boldsymbol{V}}$ $\displaystyle:=x\hskip
50.00008pt$ $\displaystyle((\pi_{i}))_{\boldsymbol{V}}$
$\displaystyle:=\lambda x.{\mathtt{ret}}(\pi_{i}x)$
$\displaystyle(({\mathtt{rec}}))_{\boldsymbol{V}}$
$\displaystyle:=\lambda\langle
u,v,w\rangle.{\mathtt{rec}}\>\langle{\mathtt{ret}}\>u,\>\hbox to0.0pt{$\lambda
xy.(vx){=}{<<}y,\>w\rangle$\hss}$

Where ${\mathtt{ret}}$ and ${=}{<<}$ are the return and the bind of the
considered monad:555Technically, this bind is not the usual bind, but a lifted
version.

$\displaystyle{\mathtt{ret}}$
$\displaystyle:((A))_{\boldsymbol{V}}\rightarrow((A))$
$\displaystyle{\mathtt{ret}}$ $\displaystyle:=\lambda xs.\langle x,s\rangle$
$\displaystyle\\_{=}{<<}\\_$ $\displaystyle:((A\rightarrow
B))\times((A))\rightarrow((B))$ $\displaystyle M{=}{<<}N$
$\displaystyle:=\lambda s_{1}.(\lambda\langle x,s_{2}\rangle.(\lambda\langle
y,s_{3})\rangle.xys_{3})\ (Ns_{2}))\ (Ms_{1})$

What $M{=}{<<}N$ does is looking at the current state $s_{1}$, evaluating $M$
under the state $s_{1}$ which results to $\langle x,s_{2}\rangle$, then
evaluating $N$ under the state $s_{2}$ which results to $\langle
y,s_{3}\rangle$, and, finally, evaluating $(x\ y):((B))$ under the state
$s_{3}$.

The encoding $((\cdot))$ is given by the return and the bind operations as
well as the encoding of effectfull operations:

$\displaystyle((V))$ $\displaystyle:={\mathtt{ret}}\ ((V))_{\boldsymbol{V}}$
$\displaystyle((M\ N))$ $\displaystyle:=((M)){=}{<<}((N))$
$\displaystyle((M\oplus N))$ $\displaystyle:=\lambda s.\;\left(((M))\
s\right)\;\oplus\;\left(((N))\ s\right)$ $\displaystyle((m:=!m+!n))$
$\displaystyle:=\lambda\langle e,m,n\rangle.\;\langle\;m\;,\;\langle
e,m+n,n\rangle\;\rangle$ $\displaystyle(({\mathtt{\bot}}))$
$\displaystyle:=\lambda\langle
e,m,n\rangle.\langle*,\langle\boldsymbol{1},\langle m,n\rangle\rangle\rangle.$

where $*$ is any term of correct type.

In the end, we set $M^{\dagger}:=\lambda x.(\lambda\langle
y,e,m,n\rangle.{\mathtt{rec}}\ y\ (\lambda uv.\boldsymbol{0})\ e)\ (((M))\
\langle x,x\rangle)$ for $M\in\mathbb{T}^{{\mathtt{R}}}(\mathtt{NAT})$. The
parameterizability is obtained by using the equality
$((\boldsymbol{n}))_{\boldsymbol{V}}=\boldsymbol{n}$.

∎

######  Corollary 33.

Distributions in $\mathbb{T}^{{\mathtt{R}}}$ are functionally parameterically
representable by $\mathbb{T}$-definable functions, i.e. for any
$M:\mathtt{NAT}\rightarrow\mathtt{NAT}$ in $\mathbb{T}^{{\mathtt{R}}}$ there
is
$F:\mathtt{NAT}\rightarrow\mathtt{NAT}\rightarrow\mathtt{NAT}\rightarrow\mathtt{BIN}$
and $Q:\mathtt{NAT}\rightarrow\mathtt{NAT}\rightarrow\mathtt{NAT}$ in
$\mathbb{T}$ such that for all $m$ and $n$:

$\sum_{k\in\mathbb{N}}\Bigl{|}\>\left\llbracket M\
\boldsymbol{m}\right\rrbracket(\boldsymbol{k})-\mathtt{N\\!F}(F\
\boldsymbol{m}\ \boldsymbol{n}\ \boldsymbol{k})\>\Bigr{|}\ \leq\
\frac{1}{n}\quad\quad\quad\forall k\geq\mathtt{N\\!F}(Q\ \boldsymbol{m}\
\boldsymbol{n}),\ \mathtt{N\\!F}(F\ \boldsymbol{m}\ \boldsymbol{n}\
\boldsymbol{k})=\boldsymbol{0}.$

##  6 Subrecursion

We recall that a function $f:\mathbb{N}\rightarrow\mathbb{N}$ is
$\mathbb{T}$-definable if there is a program $\vdash
M:\mathbb{N}\rightarrow\mathbb{N}$ in $\mathbb{T}$ such that $(M\
\boldsymbol{n})\rightarrow^{*}f(n)$ for all $n$. We denote
$\boldsymbol{D\\!T}$ the set of $\mathbb{T}$-definissable functions.

If one wishes to define $\mathbb{T}^{\oplus}$-definable or
$\mathbb{T}^{{\mathtt{R}}}$-definable functions as a set of ordinary set-
theoretic functions (say from $\mathbb{N}$ to $\mathbb{N}$), it is necessary
to collapse the random output into a deterministic one. As already
acknowledged by the complexity community, there are at least two reasonable
ways to do so: by using a either Monte Carlo or Las Vegas observations.

###  6.1 Monte Carlo

We call Monte Carlo observation on $\mathbb{T}^{\oplus}$ (rep.
$\mathbb{T}^{{\mathtt{R}}}$) the class $\boldsymbol{B\\!P\\!T}^{\oplus}$ (rep.
$\boldsymbol{B\\!P\\!T}^{R}$) of functions $f$ definable by a program $\vdash
M:\mathtt{NAT}\rightarrow\mathtt{NAT}$ (in $\mathbb{T}^{\oplus}$ and
$\mathbb{T}^{{\mathtt{R}}}$ resp.) in the sens that $(M\ \boldsymbol{n})$
evaluate into $f(n)$ with probability $p\geq\frac{2}{3}$.

$f\in\boldsymbol{B\\!P\\!T}^{\oplus}\quad\quad\text{if}\quad\quad\exists
M\in\mathbb{T}^{\oplus}(\mathtt{NAT}\rightarrow\mathtt{NAT}),\ \ \forall
n\in\mathbb{N},\ \ \left\llbracket
M\boldsymbol{n}\right\rrbracket(\boldsymbol{f(n)})\geq\frac{2}{3}$

In fact, the bound $\frac{2}{3}$ is arbitrary and we could have equivalently
use any bound strictly above $\frac{1}{2}$. That is why it is natural to also
consider the limit. We call probabilistic observation on $\mathbb{T}^{\oplus}$
(rep. $\mathbb{T}^{{\mathtt{R}}}$) the class $\boldsymbol{P\\!T}^{\oplus}$
(rep. $\boldsymbol{P\\!T}^{R}$) of functions $f$ definable by a program
$M:\mathtt{NAT}\rightarrow\mathtt{NAT}$ of $\mathbb{T}^{\oplus}$ (rep.
$\mathbb{T}^{{\mathtt{R}}}$) in the sens that $(M\ \boldsymbol{n})$ evaluate
into $f(n)$ with probability $p>\frac{1}{2}$:

$f\in\boldsymbol{P\\!T}^{\oplus}\quad\quad\text{if}\quad\quad\exists
M\in\mathbb{T}^{\oplus}(\mathtt{NAT}\rightarrow\mathtt{NAT}),\ \ \forall
n\in\mathbb{N},\ \ \left\llbracket
M\boldsymbol{n}\right\rrbracket(\boldsymbol{f(n)})>\frac{1}{2}$

In its all generality, the pertinence of this class is dubitative. Indeed, we
can see it as the class where $(M\ \boldsymbol{n})$ evaluates into $f(n)$ with
probability $p\geq\frac{1}{2}+h(n)$ for an arbitrary non null $n$, in
particular for $h$ non commutable. In this case, the result may not make much
sense in practice.

Due to the functional aspect of the considered objects,666 in contrast to what
happened for the polynomial classes. we can nonetheless consider subclasses of
$\boldsymbol{P\\!T}^{\oplus}$ (rep. $\boldsymbol{P\\!T}^{R}$) for a reasonable
dynamic bound $h$.

We call dynamic Monte Carlo observation on $\mathbb{T}^{\oplus}$ (rep.
$\mathbb{T}^{{\mathtt{R}}}$) the class
$\boldsymbol{B\\!P\\!T}_{\\!\geq\mathbb{T}\\!}^{\oplus}$ (rep.
$\boldsymbol{B\\!P\\!T}_{\\!\geq\mathbb{T}\\!}^{R}$) of functions $f$
definable by a program $\vdash M:\mathtt{NAT}\rightarrow\mathtt{NAT}$ (in
$\mathbb{T}^{\oplus}$ and $\mathbb{T}^{{\mathtt{R}}}$ resp.) in the sens that
$(M\ \boldsymbol{n})$ evaluate into $f(n)$ with probability
$p\geq\frac{1}{2}+\frac{1}{h(n)}$ for a $\mathbb{T}$-definable function $h$.

$f\in\boldsymbol{P\\!T}^{\oplus}\quad\quad\text{if}\quad\quad\exists
h\in\boldsymbol{D\\!T},\ \ \exists
M\in\mathbb{T}^{\oplus}(\mathtt{NAT}\rightarrow\mathtt{NAT}),\ \ \forall
n\in\mathbb{N},\ \ \left\llbracket
M\boldsymbol{n}\right\rrbracket(\boldsymbol{f(n)})>\frac{1}{2}+\frac{1}{h(n)}$

######  Theorem 34.

$\boldsymbol{P\\!T}^{\oplus}\ =\ \boldsymbol{D\\!T},$

in particular we also have
$\boldsymbol{B\\!P\\!T}^{\oplus}=\boldsymbol{B\\!P\\!T}_{\\!\geq\mathbb{T}\\!}^{\oplus}=\boldsymbol{D\\!T}$.

###### Proof.

Let $f\in\boldsymbol{P\\!T}^{\oplus}$.

There is $M\in\mathbb{T}^{\oplus}(\mathtt{NAT}\rightarrow\mathtt{NAT})$ such
that $\left\llbracket M\ \boldsymbol{m}\right\rrbracket(f(m))>\frac{1}{2}$.

By Theorem 25, there is
$F\in\mathbb{T}(\mathtt{NAT}\rightarrow\mathtt{NAT}\rightarrow\mathtt{BIN})$
and $G\in\mathbb{T}(\mathtt{NAT}\rightarrow\mathtt{NAT})$ such that

$\forall
k\leq\mathtt{N\\!F}(G\>n),\quad\quad\mathtt{N\\!F}(F\>\boldsymbol{n}\>\boldsymbol{k})>\frac{1}{2}\quad\Leftrightarrow\quad
k=f(n)\ .$

In this case can we set
$M^{\prime}\in\mathbb{T}(\mathtt{NAT}\rightarrow\mathtt{NAT})$ such that
$\mathtt{N\\!F}(M^{\prime}\ \boldsymbol{n})=f(n)$, by:

$\displaystyle M^{\prime}$ $\displaystyle:=\lambda n.{\mathtt{rec}}\langle
Fn\boldsymbol{0},\>\lambda
ky.{\mathtt{ite}}\langle{\mathtt{sup}}_{\frac{1}{2}}(F\>n\>k),\>k,\>y\rangle,\>G\>n\rangle$

where ${\mathtt{sup}}_{\frac{1}{2}}$ is testing whether the input is above
$\frac{1}{2}$:

$\displaystyle{\mathtt{sup}}_{\frac{1}{2}}$
$\displaystyle:\mathtt{NAT}\times\mathtt{NAT}\rightarrow\mathtt{NAT}$
$\displaystyle{\mathtt{sup}}_{\frac{1}{2}}$ $\displaystyle:=\lambda\langle
m,n\rangle.(m+m)>2^{n}$ $\displaystyle\\_>\\_$
$\displaystyle:\mathtt{NAT}\times\mathtt{NAT}\rightarrow\mathtt{NAT}$
$\displaystyle M>N$ $\displaystyle:={\mathtt{rec}}\langle\lambda
u.\boldsymbol{0},\>\lambda xyu.{\mathtt{rec}}\langle\boldsymbol{1},\lambda
a\\_.ya,u\rangle,\ M\rangle\ N$

∎

######  Theorem 35.

$\boldsymbol{B\\!P\\!T}_{\\!\geq\mathbb{T}\\!}^{R}\ =\ \boldsymbol{D\\!T},$

in particular we also have $\boldsymbol{B\\!P\\!T}^{R}=\boldsymbol{D\\!T}$.

###### Proof.

Let $f\in\boldsymbol{B\\!P\\!T}_{\\!\geq\mathbb{T}\\!}^{R}$.
There is $M\in\mathbb{T}^{{\mathtt{R}}}(\mathtt{NAT}\rightarrow\mathtt{NAT})$
and $H\in\mathbb{T}(\mathtt{NAT}\rightarrow\mathtt{NAT})$ such that

$\left\llbracket M\
\boldsymbol{m}\right\rrbracket(f(m))\geq\frac{1}{2}+\frac{1}{\mathtt{N\\!F}(H\
\boldsymbol{m})}.$

By Theorem 33, there exists
$F:\mathtt{NAT}{\rightarrow}\mathtt{NAT}{\rightarrow}\mathtt{NAT}{\rightarrow}\mathtt{BIN}$
and $Q:\mathtt{NAT}{\rightarrow}\mathtt{NAT}{\rightarrow}\mathtt{NAT}$ in
$\mathbb{T}$ such that:

$\sum_{k\in\mathbb{N}}\Bigl{|}\>\left\llbracket M\
\boldsymbol{m}\right\rrbracket(\boldsymbol{k})-\mathtt{N\\!F}(F\
\boldsymbol{m}\ \boldsymbol{n}\ \boldsymbol{k})\>\Bigr{|}\ \leq\
\frac{1}{n}\quad\quad\quad\forall k\geq\mathtt{N\\!F}(Q\ \boldsymbol{m}\
\boldsymbol{n}),\ \mathtt{N\\!F}(F\ \boldsymbol{m}\ \boldsymbol{n}\
\boldsymbol{k})=\boldsymbol{0}.$

In particular, $f(m)$ is the only $k\leq\mathtt{N\\!F}(Q\ \boldsymbol{m}\ (H\
\boldsymbol{m}))$ such that:

$\mathtt{N\\!F}(F\ \boldsymbol{m}\ (H\ \boldsymbol{m})\
\boldsymbol{k})>\frac{1}{2}$

In this case can we set $M^{\prime}$ such that $\mathtt{N\\!F}(M^{\prime}\
\boldsymbol{n})=f(n)$ by:

$\displaystyle M^{\prime}$ $\displaystyle:=\lambda m.{\mathtt{rec}}\langle
F\>m\>(H\>m)\>\boldsymbol{0},\>\lambda
ky.{\mathtt{ite}}\langle{\mathtt{sup}}_{\frac{1}{2}}(F\>m\>(H\>m)\>k),k,y\rangle,\>G\>m\>(H\>m)\rangle$

∎

###  6.2 Las Vegas

We call Las Vegas observation on $\mathbb{T}^{\oplus}$ (rep.
$\mathbb{T}^{{\mathtt{R}}}$) the class777The polynomial equivalent to this
class is the class $\boldsymbol{Z\\!P\\!P}$, which name comes from an
equivalent representation of zero-error probabilistic programs in polynomial
mid-time. Notice that the equivalence does not hold her.
$\boldsymbol{L\\!V\\!T}^{\oplus}$ (rep. $\boldsymbol{L\\!V\\!T}^{R}$) of
functions $f$ definable by a program $M:\mathtt{NAT}\rightarrow\mathtt{NAT}$
(in $\mathbb{T}^{\oplus}$ and $\mathbb{T}^{{\mathtt{R}}}$ resp.) in the sens
that $(M\ \boldsymbol{n})$ evaluate either to $\boldsymbol{0}$ representing a
failure or to $({\mathtt{S}}\boldsymbol{f(n)})$, the later happening with
probability at least $\frac{1}{3}$:

$f\in\boldsymbol{L\\!V\\!T}^{\oplus}\quad\quad\text{if}\quad\quad\exists
M\in\mathbb{T}^{\oplus}(\mathtt{NAT}\rightarrow\mathtt{NAT}),\ \
\left\llbracket
M\boldsymbol{n}\right\rrbracket=\left\\{\begin{matrix}{\mathtt{S}}\boldsymbol{f(n)}&\mapsto&p\\\
\boldsymbol{0}&\mapsto&(1-p)\end{matrix}\right\\}\ \text{ with }\
p\geq\frac{1}{3}$

Similarly, the bound $\frac{1}{3}$ is arbitrary and we can consider the limit
class (which corresponds to a non-deterministic interpretation on $\oplus$)
and the bounded restrictions.

We call non-deterministic observation on $\mathbb{T}^{\oplus}$ (rep.
$\mathbb{T}^{{\mathtt{R}}}$) the class $\boldsymbol{N\\!T}^{\oplus}$ (rep.