# On Feller Continuity and Full Abstraction

Gilles Barthe  0000-0002-3853-1777 MPI Security and PrivacyGermany
<EMAIL_ADDRESS>,  Raphaëlle Crubillé  0000-0002-4197-0439 CNRSFrance
<EMAIL_ADDRESS>,  Ugo Dal Lago  0000-0001-9200-070X University
of BolognaItaly INRIAFrance<EMAIL_ADDRESS>and  Francesco Gavazzo
0000-0002-2159-0615 University of BolognaItaly INRIAFrance
<EMAIL_ADDRESS>
###### Abstract.

We study the nature of applicative bisimilarity in $\lambda$-calculi endowed
with operators for sampling from _continuous_ distributions. On the one hand,
we show that bisimilarity, logical equivalence, and testing equivalence all
coincide with contextual equivalence when real numbers can be manipulated only
through continuous functions. The key ingredient towards this result is a
novel notion of Feller-continuity for labelled Markov processes, which we
believe of independent interest, being a broad class of LMPs for which
coinductive and logically inspired equivalences coincide. On the other hand,
we show that if no constraint is put on the way real numbers are manipulated,
characterizing contextual equivalence turns out to be hard, and most of the
aforementioned notions of equivalence are even _unsound_.

Applicative Bisimilarity, Labelled Markov Processes, Lambda Calculus, Event
Bisimilarity

††copyright: none††ccs: Theory of computation Semantics and reasoning††ccs:
Theory of computation Probabilistic computation

##  1\. Introduction

There exist many different definitions of program equivalence for higher-order
programs. These definitions come in different flavours, including contextual
equivalence (Morris, 1969), coalgebraic and bisimulation-based definitions
(Abramsky, 1990; Sangiorgi, 1994; Lassen, 1999), logical definitions based on
modal logics (Abramsky, 1990; Ong, 1988), and operational definitions based on
tests (Ong, 1993). In the baseline setting, where program evaluation does not
produce computational effects, all these definitions coincide, and provide a
rich set of methods for proving program equivalence.

In contrast, these different notions are not known to coincide in effectful
programming languages; and even for some specific effect, such as sampling
from distributions, it can be difficult to relate, or even define, the
underlying relations. On the positive side, it is known that the
aforementioned notions of equivalence coincide for _discrete_ probabilistic
effects, i.e. when values are sampled from discrete distributions (Crubillé
and Dal Lago, 2014; Crubillé et al., 2015). However, little is known about the
correspondence between different notions of equivalence for higher-order
languages with sampling from _continuous_ distributions, which are crucial in
many application domains such as Bayesian programming. One main challenge with
these languages is that their underlying operational semantics goes beyond
well-understood classes of probabilistic processes. When sampling from
continuous distributions is available, programs no longer form a labelled
Markov chain, but form instead a _labelled Markov process_ (Panangaden, 2009)
(LMP in the following). Unfortunately, even if these LMPs have an _analytic_
state space, they come with an _uncountable_ set of labels. As a consequence,
they fall outside of the class of LMPs with analytic state spaces _and_
countable sets of labels, for which correspondence between the different
definitions of equivalence still holds (Panangaden, 2009).

The question addressed in this paper is therefore: what is (_if any_) a
natural condition on LMPs (with _analytic_ state space and an _uncountable_
set of labels), such that the different notions of equivalence coincide? The
idea explored in this paper is to ask that programs are only built from
_continuous_ functions. And indeed, asking basic functions to be continuous
has the consequence of making contextual equivalence, both forms of
bisimilarity from the literature (i.e. state bisimilarity (Desharnais et al.,
2002) and event bisimilarity (Danos et al., 2006, 2005)), logical equivalence
and testing equivalence to coincide. The path to this result is not trivial,
and goes through the definition of a new class of LMPs, called _Feller-
continuous_ LMPs, whose transition functions satisfy a continuity constraint.

Now equipped with Feller continuity as a sufficient condition for proving
correspondence between the different notions, we ask for the _necessity_ of
Feller continuity. We do not provide a definitive answer to this question.
However, our partial exploration provides several results of independent
interest. On the positive side, we prove that several key technical results
used to establish equivalence between the different notions extend to the
general setting. On the negative side, we show that _event_ bisimilarity, as
well as _testing_ and _logical_ equivalence, are not _sound_ in the general
case. We also point to some undesirable behavior of _state_ bisimilarity.
These negative results do not rule out the existence of alternative better
behaved definitions. However, we also show that contextual equivalence is not
measurable. This, in itself, points to the broader challenge of proving
program equivalence in absence of Feller continuity.

At a higher level, our results show a conceptual gap between discrete and
continuous distributions. When working with calculi with _discrete_
probabilistic choice, operational reasoning is mostly set-theoretic: programs
form an ordinary set, and program execution is modeled as a set-theoretic
function; accordingly, operational reasoning is mostly performed relying on
the classic notion of a (program) relation. When we enter the realm of
continuous probability, operational reasoning drastically changes, moving from
a set-theoretic to a _measure-theoretic_ base: programs now form not just a
set, but a _measurable_ space, and their evaluation becomes a _measurable
function_. What about relations? One would expect that relations should
become, morally, measurable too: and indeed, mathematically speaking, things
work smoothly if one restricts to measurable relations, with beautiful,
classic theorems — such as the well-known Monge-Kantorovich duality (Villani,
2008) — extending to measurable spaces, functions, and relations. That
suggests that to have well-behaved program equivalences, one should require
such equivalences to be measurable. However, such a requirement is simply too
strong: in absence of continuity constraints, contextual equivalence is _not_
measurable. Consequently, even if in principle we could define _measurable_
notions of program equivalence, the latter are doomed not to capture the full
power of contextual equivalence: the very expressive power of the calculus
simply goes beyond the world of measurable relations. Looking back at the
notion of Feller-continuity from this perspective, we can see the latter as a
somehow minimal condition ensuring contextual equivalence (and, _a fortiori_ ,
all the aforementioned notions of equivalence) to be measurable, this way
establishing a new, deep connection between the syntax of a calculus and the
semantics of its associated operational reasoning.

###  1.1. Organization of the Paper and Summary of Contributions

The paper is organized as follows:

  * •

In Section 2, we introduce $\Lambda_{\mathbf{P}}$, a simply-typed
probabilistic $\lambda$-calculus with recursive types and real numbers, which
we use as a vehicle language for our study. We show that for some choice of
primitive functions, contextual equivalence for $\Lambda_{\mathbf{P}}$ is not
measurable. We also introduce technical notions, such as that of a preterm,
which are central to our development. Finally, we introduce a fragment of
$\Lambda_{\mathbf{P}}$, called $\Lambda_{\mathbf{P}}^{c}$, in which all
function symbols are continuous.

  * •

We then present, in Section 3, a unified overview of different notions of
equivalence and of their correspondence, in the case of LMPs with analytic
state spaces and countable set of labels. We also single out correspondences
that extend to the case of arbitrary LMPs. We also define the LMP describing
the interactive behaviour of $\Lambda_{\mathbf{P}}$ programs, and observe that
its set of labels is uncountable; as a consequence, it falls out of the class
of LMPs for which different notions of correspondence are related;

  * •

We introduce the notion of a Feller continuous LMP and prove that state and
event bisimilarity coincide for Feller continuous LMPs (Theorem 4.17). It
follows that the correspondence between different notions of equivalence for
Feller continuous LMPs holds, similar to LMPs with analytical state space and
discrete set of labels. All this is in Section 4.

  * •

We prove that the LMP resulting from $\Lambda_{\mathbf{P}}^{c}$ is indeed
Feller continuous. As a corollary, we get that full abstraction holds for
$\Lambda_{\mathbf{P}}^{c}$, and that all the aforementioned notions of
equivalence coincide (Theorem 5.8). This is in Section 5.

  * •

We present in Section 6 a preliminary analysis of the general case. Our main
result is that event bisimilarity, as defined in Section 3, is unsound.
Additionally, we illustrate by way of examples how measurability issues pose a
challenge to the role of state bisimilarity in the context of
$\Lambda_{\mathbf{P}}$.

##  2\. The Stochastic $\lambda$-Calculus

The target language of this work is a (call-by-value) $\lambda$-calculus with
finite sums and recursive types endowed with specific operators for sampling
from continuous distributions, and for first-order functions on the real
numbers. As such, the calculus is very expressive, both at the level of terms
and at the level of types. We separate values from terms (Levy et al., 2003),
this way requiring terms to be explicitly sequenced via the let-in construct.

###  2.1. Syntax and Static Semantics

The syntax and static semantics of $\Lambda_{\mathbf{P}}$ are defined in
Figure 1.

$\displaystyle\sigma$
$\displaystyle\;::=\;\alpha\mid\mathbf{real}\mid\sum\nolimits_{i\in
I}{\sigma_{i}}\mid\sigma\to\sigma\mid\mu\alpha.\sigma$ $\displaystyle V$
$\displaystyle\;::=\;x\mid\bm{r}\mid\langle\imath,V\rangle\mid\lambda
x.M\mid\mathbf{fold}\ V$ $\displaystyle M$
$\displaystyle\;::=\;V\mid\mathbf{sample}\mid\bm{f}(V,\ldots,V)\mid\bm{b}(V,\ldots,V)\mid\mathbf{pm}\
V\ \mathbf{as}\ \langle i,x\rangle.M\mid VV\mid\mathbf{let}\ x=M\ \mathbf{in}\
M\mid\mathbf{unfold}\ V$

$\Gamma,x:\sigma\vdash^{\scriptscriptstyle{\mathscr{V}}}x:\sigma\phantom{x}\quad\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}\bm{r}:\mathbf{real}r\in\mathbb{R}\quad\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}\mathbf{sample}:\mathbf{real}\phantom{x}$

$\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}\bm{\bm{f}}(V_{1},\ldots,V_{n}):\mathbf{real}\lx@proof@logical@and\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V_{1}:\mathbf{real},\ldots,\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V_{n}:\mathbf{real}\bm{f}\in\mathcal{C}_{n}\quad\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}\bm{b}(V_{1},\ldots,V_{n}):\mathbf{bool}\lx@proof@logical@and\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V_{1}:\mathbf{real},\ldots,\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V_{n}:\mathbf{real}b\in\mathcal{B}_{n}$

$\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}V:\sigma\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V:\sigma\quad\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}\mathbf{let}\
x=M\ \mathbf{in}\
N:\tau\lx@proof@logical@and\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}M:\sigma\Gamma,x:\sigma\vdash^{\scriptscriptstyle{\mathscr{T}}}N:\tau\quad\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}\lambda
x.M:\sigma\to\tau\Gamma,x:\sigma\vdash^{\scriptscriptstyle{\mathscr{T}}}M:\tau\quad\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}VW:\tau\lx@proof@logical@and\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V:\sigma\to\tau\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}W:\sigma$

$\quad\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}\langle\hat{\imath},V\rangle:\sum\nolimits_{i\in
I}{\sigma_{i}}\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V:\sigma_{\hat{\imath}}\quad\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}\mathbf{pm}\
V\ \mathbf{as}\ \langle
i,x\rangle.M_{i}:\sigma\lx@proof@logical@and\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V:\sum\nolimits_{i\in
I}{\sigma_{i}}\Gamma,x:\sigma_{i}\vdash^{\scriptscriptstyle{\mathscr{T}}}M_{i}:\sigma\
(\forall i\in I)$

$\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}\mathbf{fold}\
V:\mu\alpha.\sigma\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V:\sigma[\mu\alpha.\sigma/\alpha]\quad\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}\mathbf{unfold}\
V:\sigma[\mu\alpha.\sigma/\alpha]\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V:\mu\alpha.\sigma$

Figure 1. Syntax and Static semantics of $\Lambda_{\mathbf{P}}$.

Types of $\Lambda_{\mathbf{P}}$ are built starting from a countable set of
type variables (denoted by the letter $\alpha$ in Figure 1) and the basic type
$\mathbf{real}$ for real numbers, using finite sums, arrows, and recursion. In
particular, in a type of the form $\sum\nolimits_{i\in I}{\sigma_{i}}$ we
assume the letter $I$ to stand for a finite set whose elements are denoted by
$\hat{\imath},\hat{\jmath},\ldots$. We write $\mathbf{void}$ for the empty sum
type, $\mathbf{unit}$ for $\mathbf{void}\to\mathbf{void}$, and $\mathbf{bool}$
for $\mathbf{unit}+\mathbf{unit}$. Concerning the latter, we also use standard
syntactic sugar, viz. $\mathbf{true}$, $\mathbf{false}$, and $\textbf{if}\ V\
\textbf{then}\ M\ \textbf{else}\ N$. As usual, we write $VM$ for
$\mathbf{let}\ x=M\ \mathbf{in}\ Vx$ and $MN$ for $\mathbf{let}\ x=M\
\mathbf{in}\ xN$.

We use _term_ judgments (resp. _value_ judgments) of the form
$\Gamma\vdash^{\scriptscriptstyle{\mathscr{T}}}M:\sigma$ (resp.
$\Gamma\vdash^{\scriptscriptstyle{\mathscr{V}}}V:\sigma$) to state that $M$
(resp. $V$) is a term (resp. value) of _closed_ type $\sigma$ in the
environment $\Gamma$, whereas an environment is a finite sequence
$x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}$ of distinct variables with
associated _closed_ types (we denote by $\cdot$ the empty environment). Notice
that we work with closed types only. We use letters $M,N,\ldots$ and
$V,W,\ldots$ to denote terms and values, respectively. We write
$\mathscr{T}_{\sigma}$, $\mathscr{V}_{\sigma}$ for the set of closed terms and
values, respectively, of type $\sigma$.

The syntax of $\Lambda_{\mathbf{P}}$ consists of three distinct parts: the
first one is a standard $\lambda$-calculus with recursive types and
coproducts; the second one allows one to perform real-valued computations;
finally, the third one is the actual probabilistic core of
$\Lambda_{\mathbf{P}}$. Concerning real-valued computations, we indicate real
number in boldface with metavariables like $\bm{r}$, while we take
$\Lambda_{\mathbf{P}}$ parametric with respect to a $\mathbb{N}$-indexed
family $\mathcal{C}$ of _countable_ sets $\mathcal{C}_{n}$, each of which
contains measurable functions from $\mathbb{R}^{n}$ to $\mathbb{R}$. In
particular, we assume standard real-valued arithmetic operations to be in
$\mathcal{C}$. We also assume the existence of a comparison operator
$op_{\leq}\in\mathcal{C}_{2}$ such that
$op_{\leq}:\mathbb{R}\times\mathbb{R}\to[0,1]$, and $op_{\leq}(x,y)=1$ if and
only if $x\leq y$. We use letters $f,g,\ldots$ to denote elements in
$\mathcal{C}_{n}$, writing their $\Lambda_{\mathbf{P}}$ syntactic
representation in boldface. To relate numerical and general computations, we
assume to have collections $\mathcal{B}_{n}$ of functions
$b:\mathbb{R}^{n}\to\\{0,1\\}$ to perform Boolean tests on real numbers. For
simplicity, we just take $\mathcal{B}=\\{=,<\\}$. Further functions can be
encoded relying on programs on $\mathbf{bool}$ representing Boolean operators.

Probabilistic behaviours are triggered by the term $\mathbf{sample}$. The
latter samples from the uniform distribution over the unit interval, which is
nothing but the Lebesgue measure $\lambda$ on $[0,1]$. It is well-known
(Ehrhard et al., 2018) that starting from $\mathbf{sample}$ several
probabilistic measures (e.g. binomial, geometric, and exponential
distribution) can be defined through functions in $\mathcal{C}$.

###### Example 2.1.

Given closed terms $M_{\mu}$, $M_{\sigma}$ of type $\mathbf{real}$ (encoding
mean $\mu$ and standard deviation $\sigma$), we represent the normal
distribution with mean $\mu$ and standard deviation $\sigma$ as the expression
$\mathbf{normal}\ M_{\mu}\ M_{\sigma}$, where the term
$\mathbf{normal}_{\mathbf{std}}$ encodes the normal distribution with mean $0$
and standard deviation $1$.

$\displaystyle\mathbf{normal}_{\mathbf{std}}$
$\displaystyle\triangleq\mathbf{let}\ x=\mathbf{sample}\ \mathbf{in}\
(\mathbf{let}\ y=\mathbf{sample}\ \mathbf{in}\ (\sqrt{-2\log(x)}\cos(2\pi
y)))$ $\displaystyle\mathbf{normal}\ M_{\mu}\ M_{\sigma}$
$\displaystyle\triangleq\mathbf{let}\ x_{\mu}=M_{\mu},\
x_{\sigma}=M_{\sigma},y=\mathbf{normal}_{\mathbf{std}}\ \mathbf{in}\
((x_{\sigma}*y)+x_{\mu}).$

For any type $\sigma$, we have the Bernoulli choice term
$\textbf{bernoulli}:\sigma\to\sigma\to\mathbf{real}\to\sigma$ acting as a
probabilistic choice construct. Such a term is defined as $\lambda
m,n,p.\mathbf{let}\ x=\mathbf{sample}\ \mathbf{in}\ (\textbf{if}\ x>p\
\textbf{then}\ n\ \textbf{else}\ m)$ In particular, the term
$\textbf{bernoulli}\ M\ N\ \bm{0.5}$ is the fair probabilistic choice between
$M$ and $N$. We employ the notation $M\oplus N$ in place of
$\textbf{bernoulli}\ M\ N\ \bm{0.5}$.

Finally, we adopt standard notational conventions (Barendregt, 1984). In
particular, we denote by $FV(M)$ the collection of free variables of $M$
(resp. $V$) and we refer to closed expressions as _programs_. We denote by
$M[V/x]$ the capture-avoiding substitution of the value $V$ for all free
occurrences of $x$ in $M$. We extend the aforementioned conventions to types.
For instance, we denote by $\sigma[\tau/\alpha]$ the result of capture-
avoiding substitution of the type $\tau$ for the type variable $\alpha$ in
$\sigma$.

###  2.2. Dynamic Semantics

The dynamic semantics of $\Lambda_{\mathbf{P}}$ is given by a type-indexed
family of evaluation functions $\llbracket-\rrbracket_{\sigma}$ mapping
programs of type $\sigma$ to _sub-probability measures_ over values of type
$\sigma$. As such, the semantics is measure-theoretic and defining it requires
some preliminary definitions that we are going to give. Due to lack of space,
we assume that the reader is familiar with basic definitions from measure
theory and refer to classic textbooks for additional background (Billingsley,
1986).

##### Measurable Spaces

We denote by Meas the category of measurable spaces and measurable functions.
When $X$ is a measurable space, we write $\Sigma_{X}$ for the underlying
$\sigma$-algebra. Moreover, given a measurable space $(X,\Sigma_{X})$ with a
measure $\mu$ on it and a function $f:X\to[0,\infty]$, we denote by
$\int_{X}f\mathit{d}\mu$ or $\int_{X}f(x)\mu(\mathit{d}x)$ the number in
$[0,\infty]$ obtained by Lebesgue integrating $f$ over $X$ with respect to
$\mu$. Oftentimes, we will work with measurable spaces associated to a Polish
space. More precisely, we shall work with standard Borel spaces, i.e. those
measurable spaces generated by complete, separable metric spaces equipped with
their Borel $\sigma$-algebra. We denote by Pol the full subcategory of Meas
whose objects are standard Borel spaces (notice that arrows in Pol remain
measurable functions). Finally, we remark that both Meas and Pol have
countable products and coproducts.

##### Probability Measures

We denote by $\Delta(X)$ the collection of sub-probability measures on a
measurable space $(X,\Sigma_{X})$, using the notation $\emptyset$ and
$\\{x^{1}\\}$ for the empty-subdistribution (on $X$) and the Dirac
distribution on $x$, respectively. We endow $\Delta(X)$ with the
$\sigma$-algebra generated by the set of evaluation maps
$\\{\mathit{ev}_{A}:\Delta(X)\to[0,1]\mid A\in\Sigma_{X}\\}$, where
$\mathit{ev}_{A}(\mu)=\mu(A)$. Recall that, given a measurable function
$f:X\to Y$, the push forward of $f$ is the (measurable) function
$f_{\sharp}:\Delta(X)\to\Delta(Y)$ defined by
$f_{\sharp}(\mu)(B)=\mu(f^{-1}(B))$. These data induce a functor $\mathcal{G}$
on Meas, which is the functor part of the _Giry monad_ (Giry, 1982). In fact,
$\mathcal{G}$ has a unit map $\eta$ associating to each element $x$ the Dirac
distribution $\\{x^{1}\\}$, and for a measurable function
$f:X\to\mathcal{G}(Y)$, the map $f^{\dagger}$ defined by
$f^{\dagger}(\mu)(B)=\int f(x)(B)\mu(dx)$ gives the Kleisli extension of $f$.
When $(X,\Sigma_{X})$ is a standard Borel space, then $\Delta(X)$ is is
standard Borel space too — so that $\mathcal{G}$ is also a monad on Pol — and
the $\sigma$-algebra of $\Delta(X)$ coincides with the Borel algebra of the
weakest topology making the integration map $\mu\mapsto\int fd\mu$,
continuous, for any bounded continuous real-valued function $f$ (see (Kechris,
2012), Theorem 17.23 and 17.24).

##### Probability Kernels

Given measurable spaces $X,Y$, we recall that a _(sub)probability kernel_
(Panangaden, 1999) is a map $f:X\times\Sigma_{Y}$ such that:

  * •

For every $A\in\Sigma_{Y}$, the map $x\in X\mapsto f(x,A)$ is measurable;

  * •

For every $x\in X$, the map $A\in\Sigma_{Y}\mapsto f(x,A)$ is a
(sub)probability measure.

We write $f:X\rightarrowtriangle Y$ when $f$ is a sub-probability kernel, and
$f:X\rightarrowtriangle^{=}Y$ when $f$ is a probability kernel (also called
Markov kernel). For any space $X$, the Dirac measure on $X$ induces a kernel
$X\rightarrowtriangle X$. Moreover, given $f:X\rightarrowtriangle Y$ and
$g:Y\rightarrowtriangle Z$, we define their composition $g\circ
f:X\rightarrowtriangle Z$ by $(g\circ f)(x,C)=\int_{Y}g(y,C)\cdot f(x,dy)$. By
the monotone convergence theorem, the composition operation $\circ$ is
associative and has Dirac measures as unit, meaning that kernels form a
category. Such a category is nothing but the Kleisli category of
$\mathcal{G}$. Panangaden (Panangaden, 1999) showed that the category of sub-
probability kernels is partially additive (Manes and Arbib, 1986). As a
consequence, for all spaces $X$, $Y$, the set of sub-probability kernels from
$X$ to $Y$ forms an $\omega$-cppo when ordered pointwise. In particular, the
bottom element associates to any element $x$ the empty distribution
$\emptyset$, whereas the least upper bound of an $\omega$-chain
$\\{f_{n}\\}_{n\geq 0}$ of kernels is defined as $\sup_{n}f_{n}$.
Additionally, kernel composition is monotone and continuous with respect to
such $\omega$-cppo structure, meaning that the category of sub-probability
kernels is $\omega\text{-}\mathbf{cppo}$-enriched (Kelly, 2005), where
$\omega\text{-}\mathbf{cppo}$ is the category of $\omega$-cppos and continuous
functions. All of this works both on Meas and Pol (with the notion of a
probability kernel restricted to standard Borel spaces).

Observe that the space of probability kernels (sub-probability kernels
respectively) is equipped with a convex structure. Moreover, the composition
commutes with the convex operations, as stated in Lemma 2.2 below. We prove
this here since we will need to use it in later sections.

###### Lemma 2.2.

Let $k:X\rightarrowtriangle Y$ and $g,h:Y\rightarrowtriangle Z$ be sub-
probability kernels. Then $k\circ(\alpha.g+\beta.h)=\alpha.k\circ
g+\beta.k\circ h$, and similarly $(\alpha.g+\beta.h)\circ k=\alpha.g\circ
k+\beta.h\circ k$.

###### Proof.

Let $x\in X$, $A\in\Sigma_{Y}$. Then
$k\circ(\alpha.f+\beta.g)(x,A)=\int_{Y}k(\cdot,A)d(\alpha.f+\beta.g)(x)=\int_{Y}k(\cdot,A)d(\alpha.f(x)+\alpha.g(x))=\alpha.\int_{Y}k(\cdot,A)df(x)+\beta.\int_{Y}k(\cdot,A)dg(x)$.
∎

##### Dynamic Semantics

We now turn to the dynamic semantics of $\Lambda_{\mathbf{P}}$. Such a
semantics is given as a monadic evaluation semantics (Dal Lago et al., 2017a)
for the Giry monad in the category Pol. More concretely, the semantics is
given by type-indexed (sub-probability, due to the presence of full recursion)
kernels $\mathscr{T}_{\sigma}\rightarrowtriangle\mathscr{V}_{\sigma}$. Recall
that for any type $\sigma$, the sets $\mathscr{T}_{\sigma}$ and
$\mathscr{V}_{\sigma}$ carry a a standard Borel space structure (Ehrhard et
al., 2018; Vákár et al., 2019; Staton et al., 2016; Borgström et al., 2016).
We recall this structure here, since we will use it explicitly in the
technical developments.

###### Definition 2.3.

We call _pre-terms_ and _pre-values_ the syntactic objects obtained from terms
and values respectively, by removing all occurrences of real numbers and
replacing them by numbered holes $[\cdot]^{n}$. Moreover, we add the
constraint that whenever $P$ is a pre-term (or a pre-value) with $n$ holes, it
means that each hole $[\cdot]^{i}$ for $1\leq i\leq n$ must occur exactly once
in $P$. Whenever $P$ is a pre-term (or a pre-value) with $n$ holes, and
$\vec{r}\in\mathbb{R}^{n}$, we write $P[\vec{\bm{r}}]$ for the term obtained
by replacing each hole $[\cdot]^{i}$ by the corresponding real value
$\bm{r}_{i}$. We write $\mathscr{T}_{P}$ (resp. $\mathscr{V}_{V}$) for the set
of all terms (resp. values) of the form $P[\vec{\bm{r}}]$ (resp.
$V[\vec{\bm{r}}]$), where $\vec{r}$ ranges over $\mathbb{R}^{n}$.

Observe that, for any pre-term $P$ with $n$ holes, the set $\mathscr{T}_{P}$
is in bijection with $\mathbb{R}^{n}$, so that we can naturally endow
$\mathscr{T}_{P}$ with a standard Borel space structure. Since $\mathscr{T}$
consists of the disjoint union of the sets $\mathscr{T}_{P}$, it is in fact
the countable coproduct of standard Borel spaces, thus a standard Borel space
itself. A standard Borel space structure can be similarly given to
$\mathscr{V}$.

###### Definition 2.4.

Define the type-indexed family of ($\mathbb{N}$-indexed) kernels
$\llbracket-\rrbracket^{(n)}_{\sigma}:\mathscr{T}_{\sigma}\rightarrowtriangle\mathscr{V}_{\sigma}$
as follows (for readability, we omit type annotations):

$\displaystyle\llbracket M\rrbracket^{(0)}(A)$ $\displaystyle=0$
$\displaystyle\llbracket V\rrbracket^{(n+1)}(A)$
$\displaystyle=\\{V^{1}\\}(A)$
$\displaystyle\llbracket\bm{f}(\bm{r_{1}},\ldots,\bm{r_{n}})\rrbracket^{(n+1)}(A)$
$\displaystyle=\llbracket\bm{\bm{f}(r_{1},\ldots,r_{n})}\rrbracket^{(n)}(A)$
$\displaystyle\llbracket\bm{b}(\bm{r_{1}},\ldots,\bm{r_{n}})\rrbracket^{(n+1)}(A)$
$\displaystyle=\llbracket\bm{b(r_{1},\ldots,r_{n})}\rrbracket^{(n)}(A)$
$\displaystyle\llbracket\mathbf{sample}\rrbracket^{(n+1)}(A)$
$\displaystyle=\lambda\\{r\mid\bm{r}\in A\\}$ $\displaystyle\llbracket(\lambda
x.M)V\rrbracket^{(n+1)}(A)$ $\displaystyle=\llbracket
M[V/x]\rrbracket^{(n)}(A)$ $\displaystyle\llbracket\mathbf{let}\ x=M\
\mathbf{in}\ N\rrbracket^{(n+1)}(A)$ $\displaystyle=\int\llbracket
N[V/x]\rrbracket^{(n)}(A)\llbracket M\rrbracket^{(n)}(\mathit{d}V)$
$\displaystyle\llbracket\mathbf{pm}\ \langle\hat{\imath},V\rangle\
\mathbf{as}\ \langle i,x\rangle.M_{i}\rrbracket^{(n+1)}(A)$
$\displaystyle=\llbracket M_{\hat{\imath}}[V/x]\rrbracket^{(n)}(A)$
$\displaystyle\llbracket\mathbf{unfold}\ (\mathbf{fold}\
V)\rrbracket^{(n+1)}(A)$ $\displaystyle=\llbracket V\rrbracket^{(n)}(A).$

By observing that for any term
$\Gamma,x:\sigma\vdash^{\scriptscriptstyle{\mathscr{T}}}M:\tau$, the map
$M[-/x]:\mathscr{V}_{\Gamma\vdash\sigma}\to\mathscr{T}_{\Gamma\vdash\tau}$ is
measurable (Ehrhard et al., 2018; Staton et al., 2016; Borgström et al.,
2016), we immediately notice that each $\llbracket-\rrbracket^{(n)}$ is indeed
a kernel and that $\\{\llbracket-\rrbracket^{(n)}_{\sigma}\\}_{n\geq 0}$ forms
an $\omega$-chain, so that we can define $\llbracket M\rrbracket_{\sigma}$ as
$\sup_{n}\llbracket M\rrbracket^{(n)}_{\sigma}$. By
$\omega\text{-}\mathbf{cppo}$-enrichment, $\llbracket M\rrbracket$ is the
least solution to the system of equations induced by Definition 2.4.

###  2.3. Contextual Equivalence

Before moving to the study of coinductively-based notions of equivalence, we
recall the notion of _probabilistic contextual equivalence_.

###### Definition 2.5 (Context Equivalence).

For every type $\sigma$, an _observable context for $\sigma$_ is a program
$\mathfrak{C}$ with a hole $[\cdot]$ such that
$[\cdot]:\sigma\vdash\mathfrak{C}:\mathbf{real}$. The set of all observable
contexts for $\sigma$ is indicated as $\mathfrak{C}_{\sigma}$. Contextual
equivalence of terms and values is defined as usual, by quantifying over all
possible observable contexts:

$\displaystyle\forall
M,N\in\mathscr{T}_{\sigma},\,M\equiv^{\mathit{ctx}}N\text{ when
}\forall\mathfrak{C}\in\mathfrak{C}_{\sigma},\llbracket\mathfrak{C}[M]\rrbracket=\llbracket\mathfrak{C}[N]\rrbracket$
$\displaystyle\forall
V,W\in\mathscr{V}_{\sigma},\,V\equiv^{\mathit{ctx}}W\text{ when
}\forall\mathfrak{C}\in\mathfrak{C}_{\sigma},\llbracket\mathfrak{C}[V]\rrbracket=\llbracket\mathfrak{C}[W]\rrbracket$

By Definition 2.5, the underlying notion of observation is the whole
distribution produced in output by any observable context. This notion can, as
usual, be proved robust to small changes in the language and in the notion of
observation .

####  2.3.1. Alternative Caracterisations of Context Equivalence.

###### Remark 2.6.

Recall that, in generic terms, two programs are context equivalent if and only
if their _observables_ are the same in any context. If we reframe Definition
2.5 in this general framework, we see that it uses a very strong notion of
_observation_ at real type: indeed Definition 2.5 means that when $M$ is a
real-type program, its precise operational semantics $\llbracket
M\rrbracket:\mathbb{R}\rightarrow[0,1]\in\Delta{(\mathbb{R})}$ can be
observed. A weaker notion of observation would be to suppose that only the
_expected value_ of $\llbracket M\rrbracket$ can be observed. This could seem
to be a more reasonnable computational choice, since–from the law of large
numbers–we know that the expected value of a distribution can be approximated
from a large number of trials. Whether these two notions of observation lead
to the same context equivalences depends on the primitive functions on reals
that we put into our language. We are going to show in Proposition 2.9 below,
that it is the case for $\Lambda_{\mathbf{P}}$, due to the fact that
$\mathcal{C}_{2}$ contains multiplication and the comparaison operator
$op_{\leq}$, and more generically that it is the case for any language that
is:  (1) able to express multiplication between reals, and  (2) contains a
countable collection $\mathcal{D}$ of functions $\mathbb{R}\to\mathbb{R}$ that
_separates points_ , in the sense that for every reals $x\neq y$, there exists
a function $f\in\mathcal{D}$ such that $f(x)\neq f(y)$.  Our main tool for
showing this result is Lemma 2.7 below, that comes from the literature on weak
convergence for probability measure.

###### Lemma 2.7.

Let $\mathcal{F}$ be a countable set of bounded mesureable functions
$\mathbb{R}\to\mathbb{R}$ such that:

  1. (1)

$\forall x,y\in\mathbb{R},\exists f\in\mathcal{F},\text{s.t. }f(x)\neq f(y)$;

  2. (2)

$\forall x\in\mathbb{R},\exists f\in\mathcal{F},\text{s.t.}f(x)>0$.

Then for every $\mu,\nu$ sub-probability measures on $\mathbb{R}$:

(1) $(\forall f\in\mathcal{M}(\mathcal{F}),\,\int f\cdot d\mu=\int f\cdot
d\nu)\qquad\Leftrightarrow\qquad\mu=\nu,$

where for any set of functions $A$, $\mathcal{M}(A):=\\{f_{1}\cdot
f_{2}\ldots\cdot f_{n}\mid n\in\mathbb{N}\wedge\forall
k\in\\{1,\ldots,n\\},f_{k}\in A\\}$.

###### Proof.

In the literature, e.g (Ethier and Kurtz, 2009), a set of bounded measureable
functions that verify (1) is called _separating_ –a concept which is actually
defined for general topological space $E$, and not only for $\mathbb{R}$. We
have to be careful here, because the literature consider _proper_ probability
distributions instead of sub-distributions: it means that we need to rewrite
our goal as: for every $\mu,\nu$ probability measures on
$\mathbb{R}\cup\\{\bot\\}$:

(2) $(\forall f\in\mathcal{M}(\mathcal{F}),\,\int f_{\bot}\cdot
d\mu_{\bot}=\int f_{\bot}\cdot
d\nu_{\bot})\qquad\Leftrightarrow\qquad\mu_{\bot}=\nu_{\bot},$

where $f_{\bot}:x\in\mathbb{R}\cup\\{\bot\\}\mapsto f(x)\text{ for
}x\in\mathbb{R},\,0\text{ otherwise}$, and
$\mu_{\bot}(A)=\mu(A\cap\mathbb{R})+(1-\mu(\mathbb{R}))\cdot\delta_{\bot}(A)$.
Theorem 11.b. in (Blount and Kouritzin, 2010) show that a sufficient condition
for a set of bounded measureable functions to be separating is to be
countable, to be stable under multiplication, and to _separate points_ , i.e.
that: $\forall x,y\in\mathbb{R}\cup\\{\bot\\}$, whenever $x\neq y$ there exist
$f\text{ s.t. }f(x)\neq f(y)$. It is immediate that the two first conditions
hold for $\\{f_{\bot}\mid f\in\mathcal{M}(\mathcal{F})\\}$. Moreover the
hypothesis on $\mathcal{F}$ gives us exactly the third condition. ∎

###### Example 2.8.

We give here an example of a countable set $\mathcal{F}$ of bounded functions
$\mathbb{R}\to[0,1]$ such that the hypothesis (1) and (2) from Lemma 2.7 hold
(it can be shown by using the density of $\mathbb{Q}$ in $\mathbb{R}$ ):

$\mathcal{F}:=\\{op_{\leq}(\cdot,q)\mid
q\in\mathbb{Q},n\in\mathbb{N}\\}\cup\\{x\in\mathbb{R}\mapsto 1\\}.$

###### Proposition 2.9.

Suppose that the sets $\mathcal{C}_{n},\mathcal{B}_{n}$ of primitive functions
allow to implement in $\Lambda_{\mathbf{P}}$ a family $\mathcal{F}$ such that
first the hypothesis (1) from Lemma 2.7 holds, and second $\mathcal{F}$
contains the multiplication function:
$(\cdot):\mathbb{R}\times\mathbb{R}\to\mathbb{R}$. Then it holds that $\forall
M,N\in\mathscr{T}_{\sigma},V,W\in\mathscr{V}_{\sigma}$:

$\displaystyle\,M\equiv^{ctx}N\text{ iff
}(\forall\mathfrak{C}\in\mathfrak{C}_{\sigma},\int_{x\in\mathbb{R}}x\cdot
d\llbracket\mathfrak{C}[M]\rrbracket=\int_{x\in\mathbb{R}}x\cdot
d\llbracket\mathfrak{C}[N]\rrbracket)$ $\displaystyle V\equiv^{ctx}W\text{ iff
}(\forall\mathfrak{C}\in\mathfrak{C}_{\sigma},\int_{x\in\mathbb{R}}x\cdot
d\llbracket\mathfrak{C}[V]\rrbracket=\int_{x\in\mathbb{R}}x\cdot
d\llbracket\mathfrak{C}[W]\rrbracket)$

###### Proof.

We do the proof for terms (it is exactly the same for values). First, observe
that the left-to-right implication is immediate; in the following we show the
right-to-left one. Suppose that
$\forall\mathfrak{C}\in\mathfrak{C}_{\sigma},\int_{x\in\mathbb{R}}x\cdot
d\llbracket\mathfrak{C}[M]\rrbracket=\int_{x\in\mathbb{R}}x\cdot
d\llbracket\mathfrak{C}[N]\rrbracket$. Let
$\mathfrak{C}\in\mathfrak{C}_{\sigma}$: we want to show that
$\llbracket\mathfrak{C}[M]\rrbracket=\llbracket\mathfrak{C}[N]\rrbracket$. Let
$f\in\mathcal{M}(\mathcal{F}\cup\\{x\in\mathbb{R}\mapsto 1\\})$: we write
$f=f_{1}\cdot\ldots\cdot f_{n}$, with
$f_{i}\in\mathcal{F}\cup\\{x\in\mathbb{R}\mapsto 1\\})$. We look at the
context: $C_{f}:\mathbf{let}\ x=[\cdot]\ \mathbf{in}\ f_{1}(x)\cdot\ldots\cdot
f_{n}(x)\in\mathfrak{C}_{\mathbf{real}}$–observe that this context is indeed
in $\Lambda_{\mathbf{P}}$, by hypothesis on
$(\mathcal{C}_{n})_{n\in\mathbb{N}}$ and $(\mathcal{B}_{n})_{n\in\mathbb{N}}$,
and since $\bm{1}\in\Lambda_{\mathbf{P}}$. Recall from Definition 2.4 that for
any real-typed term $L$,
$\llbracket{\mathfrak{C}_{f}}[L]\rrbracket=f_{\star}(\llbracket L\rrbracket)$,
where $f_{\star}$ stands for the push-forward operation for $f$. From there,
we can see:

(3) $\displaystyle\int_{x\in\mathbb{R}}x\cdot
d\llbracket\mathfrak{C}_{f}[L]\rrbracket=$
$\displaystyle\int_{x\in\mathbb{R}}x\cdot d(f_{\star}(\llbracket
L\rrbracket))$ (4) $\displaystyle=$
$\displaystyle\int_{x\in\mathbb{R}}f(x)\cdot d(\llbracket L\rrbracket),$

where (4) above holds by the change of variable formula–a standard result on
push-forward measures. By hypothesis, we know that
$\int_{x\in\mathbb{R}}x\cdot
d\llbracket\mathfrak{C}_{f}[\mathfrak{C}[M]]\rrbracket=\int_{x\in\mathbb{R}}x\cdot
d\llbracket\mathfrak{C}_{f}[\mathfrak{C}[N]]\rrbracket$, thus (4) implies that
$\int_{x\in\mathbb{R}}f(x)\cdot
d\llbracket\mathfrak{C}[M]\rrbracket=\int_{x\in\mathbb{R}}f(x)\cdot
d\llbracket\mathfrak{C}[N]\rrbracket$. Since it is true for every
$f\in\mathcal{M}(\mathcal{F})$, we can conclude by Lemma 2.7 ∎

####  2.3.2. (Non)-Measurability of Context Equivalence.

It is now instructive to observe that contextual equivalence is _not_ a
_measurable relation_ , meaning that the graph of $\equiv^{\mathit{ctx}}$ is
not a measurable (i.e. Borel, in our setting) set, as we show in Lemma 6.12
below. 111Even more, we can rely on descriptive set theory (Kechris, 2012) to
bound the non-measurability of contextual equivalence (and its equivalence
classes), showing, e.g., that the graph of $\equiv^{\mathit{ctx}}$ is a co-
analytic set.

###### Proposition 2.10.

There exists a choice of measurable functions in $\mathcal{C}$ such that the
graph of $\equiv^{\mathit{ctx}}$ is not a Borel set.

###### Proof.

We are going to use the existence of a non-Borel co-analytical set
$X\subseteq\mathbb{R}$ to build measurable primitive functions that lead to a
non-Borel equivalence class for $\equiv^{ctx}$ (and thus to a non-Borel graph
for $\equiv^{ctx}$). We know that such a set exists from descriptive set
theory (see (Kechris, 2012), 14.2). Moreover, we also know (see (Kechris,
2012), 32.B) that there exists some open set $O$ of
$\mathbb{R}\times\mathcal{N}$, such that $X=\\{y\mid\forall x,(x,y)\in O\\}$:
here $\mathcal{N}$ is the Baire space, that is known ((Kechris, 2012), 3.4) to
be homomorphic to the set of all irrational numbers. It means that we can
embedd $O$ in $\mathbb{R}\times\mathbb{R}$, and we again obtain a Borel set
(observe that $O$ is not an open set anymore, but we can show it is an open
set minus a set of rational numbers, and since $\mathbb{Q}$ is countable this
removal operation preserves Borel sets). From $O$, we define a function
$f_{O}:\mathbb{R}^{2}\rightarrow\mathbb{R}$ defined as $f_{O}(x,y)=1$ whenever
$(x,y)\in O$, and $0$ otherwise. Observe that since
$O\subseteq\mathbb{R}\times\mathbb{R}$ is a Borel set, it holds that $f_{O}$
is measurable. We are now going to consider the (very simple) program
$M:=\lambda x.0:\mathbf{real}\rightarrow\mathbf{real}$, and show that its
equivalence class for $\equiv^{ctx}$ is not a Borel set. We are able to
caracterise exactly the equivalence class of $M$: it consists of all the
$N:\mathbf{real}\rightarrow\mathbf{real}$ such that for every
$r\in\mathbf{real}$, $\llbracket Nr\rrbracket=\\{0^{1}\\}$. (In order to show
that formally, we can use our results of soundness and completeness of event
bisimulation and state bisimulation respectively, or we can for instance use
denotational arguments in the quasi-Borel space model). Now, looking at the
way we define the standard Borel space of terms as a countable co-product, we
see that it is enough to show that there exists one pre-term $P$, such that
$\\{\vec{r}\mid P[\vec{r}]\equiv^{ctx}M\\}$ is not measurable. We consider the
pre-term $P$ with one hole defined by $P[r]:=\lambda x.\text{ if
}f_{O}(x,r)=1\text{ then }0\text{ else }1$. Using the caracterisation of $M$’s
equivalence class we have previously established, we see that $\\{r\mid
P[r]\equiv^{ctx}M\\}=\\{r\mid\forall
r^{\prime}\in\mathbb{R},f(r,r^{\prime})\in O\\}=X$, and we can conclude from
there. ∎

In other words, even if we insist, like we did, in constraining the basic
building blocks of our calculus in such a way that everything stays
measurable, the central concept of contextual equivalence somehow breaks the
mold. There is however a way to recover measurability of contextual
equivalence, which we will now describe.

####  2.3.3. Recovering Measurability

We consider a natural restriction of $\Lambda_{\mathbf{P}}$, called
$\Lambda_{\mathbf{P}}^{c}$, in which we require primitive functions to be
continuous.

###### Definition 2.11.

The language $\Lambda_{\mathbf{P}}^{c}$ is the fragment of
$\Lambda_{\mathbf{P}}$ obtained by requiring $\mathcal{C}$ to only contain
symbols denoting _continuous_ functions, and $\mathcal{B}$ to be empty.

Noticeably, what we obtained is not a _different_ calculus, but rather an
instance of $\Lambda_{\mathbf{P}}$ in which $\mathcal{C}$ and $\mathcal{B}$
satisfy certain conditions. Even if functions in $\mathcal{C}$ are required to
be continuous, the presence in $\mathcal{C}_{2}$ of a (now, continuous)
comparison operator $\mathit{op}_{\leq}$ is still required. Observe that
sampling from discrete distributions is not available anymore from within
$\Lambda_{\mathbf{P}}^{c}$, because standard tests on real numbers are not
continuous. Discrete distributions could however be added natively to
$\Lambda_{\mathbf{P}}^{c}$, e.g. by endowing the language with a standard
binary choice operator $\oplus_{p}$ complementing $\mathbf{sample}$. For the
sake of simplicity, we do not pursue this further, and work with a rather
minimal language. Our proof techniques, however, are robust enough to ensure
that our results would not be affected by the presence of $\oplus_{p}$.

We will extensively study the nature of program equivalence for
$\Lambda_{\mathbf{P}}^{c}$ in Section 4 and Section 5. For the moment, we
simply observe that moving from $\Lambda_{\mathbf{P}}$ to
$\Lambda_{\mathbf{P}}^{c}$ indeed ensures contextual equivalence to be
measurable.

###### Proposition 2.12.

The graph of contextual equivalence on $\Lambda_{\mathbf{P}}^{c}$ is a Borel
set.

###### Proof.

First, since Borel sets are stable by countable union, we see that it is
sufficient to show that for every type $\sigma$, $\equiv^{ctx}$ restricted to
programs of type $\sigma$ is Borel. By definition of context equivalence, we
can write:

$\displaystyle\equiv^{ctx}_{\sigma}$
$\displaystyle=\bigcap_{\begin{subarray}{c}C\text{ a pre-context }\\\
\text{with }k\text{ holes
}\end{subarray}}\\{(M,N)\mid\forall\vec{r}\in\mathbb{R}^{k},\,\llbracket
C[\vec{r}][M]\rrbracket=\llbracket C[\vec{r}][N]\rrbracket\\}$
$\displaystyle=\bigcap_{\begin{subarray}{c}C\text{ a pre-context}\\\ \text{
with }k\text{ holes
}\end{subarray}}\bigcap_{q\in\mathbb{Q}\cup{+\infty}}\quad\\{(M,N)\mid\forall\vec{r}\in\mathbb{R}^{k},\,\llbracket
C[\vec{r}][M]\rrbracket(]-\infty,q])=\llbracket
C[\vec{r}][N]\rrbracket(]-\infty,q)\\}$

where the last holds by Example 2.8 and Lemma 2.7. Borel sets are also closed
by countable intersections, thus it is enough to show that for every pre-
context $C$, and every $q\in\mathbb{Q}\cup\\{+\infty\\}$, the set
$S_{C,q}:=\\{(M,N)\mid\forall\vec{r}\in\mathbb{R}^{k},\,\llbracket
C[\vec{r}][M]\rrbracket(]-\infty,q])=\llbracket
C[\vec{r}][N]\rrbracket(]-\infty,q)\\}$ is Borel. As a first step, observe
that we can rewrite $S_{C,q}$ as the complementary of:

(5) $\overline{S_{C,q}}:=\\{(M,N)\mid\exists
r\in\mathbb{R}^{k},(\vec{r},M,N)\in A_{C,q}\\},$

where $A_{C,q}=\\{(r,M,N)\mid\llbracket
C[\vec{r}][M]\rrbracket(]-\infty,q])\neq\llbracket
C[\vec{r}][N]\rrbracket(]-\infty,q)\\}\subseteq\mathbb{R}^{k}\times\mathscr{T}_{\sigma}\times\mathscr{T}_{\sigma}$.
It means that it is enough to show that the projection of $A_{C,q}$ is a Borel
set. Observe that it is not true that the projection of a Borel set is a Borel
set; however it is true that the projection of an open set is an open set, and
thus a Borel set. Using the fact that now all our primitive functions are
continuous, we are now able to show that $A_{C,q}$ is an open set. We write
$A_{C,q}$ as:

$A_{C,q}=(h_{C},q)^{-1}{(\\{(a,b)\in\mathbb{R}^{2}\mid a\neq b\\})},$

where
$h_{C},q:\mathbb{R}^{k}\times\mathscr{T}_{\sigma}\times\mathscr{T}_{\sigma}\rightarrow\mathbb{R}^{2}$
is the sequential composition $h_{C,q}:=f_{C};(g_{q}\times g_{q})$, where
$f_{C}$ and $g_{q}$ are defined thus:

$\displaystyle
f_{C}:(\vec{r},M,N)\in\mathbb{R}^{k}\times\mathscr{T}_{\sigma}\times\mathscr{T}_{\sigma}\mapsto(C[\vec{r}][M],C[\vec{r}][N])\in\mathscr{T}_{\mathbf{real}}\times\mathscr{T}_{\mathbf{real}}$
$\displaystyle g_{q}:P\in\mathscr{T}_{\mathbf{real}}\mapsto\llbracket
P\rrbracket(]-\infty,q])\in\mathbb{R}.$

Looking at the definition of the standard Borel space $\mathscr{T}$, we can
see that elementary syntactic operations are not only measurable, but also
continuous: from there, we obtain that $f_{C}$ is continuous. Moreover,
enforcing continuity of primitive functions allows us to show that the
function $g_{q}$ is also continuous: we will show formally this result in
Section 5 (it is a direct corollary of Proposition 5.4). Since continuous
functions are stable by composition and cartesian product, it means that also
the function $h_{C,q}$ is continuous. It means that $A_{C,q}$ is the inverse
image of an open $\mathbb{R}^{2}$-set by a continuous function, thus it is
also open, and that concludes the proof. ∎

Having defined the target calculi of this work and their associated notion of
contextual equivalence, we can now proceed to the introduction of
bisimulation-based equivalences and their logical and testing-based
characterizations.

##  3\. On Labelled Markov Processes and Equivalences on Them

In this section, we briefly recap the definition of _state_ -bisimilarity, and
we give the alternative notion of _event_ bisimilarity, introduced by Danos et
al. (2005, 2006). A summary of all results presented in this section can be
found in Figure 2.

$\sim_{\mathit{state}}\,\subseteq\,\sim_{\mathit{event}}\,=\,\sim_{\mathit{logic}}\,=\,\sim_{\mathit{test}}$
Analytical State Space Countable Labels Discrete States and Countable Labels
$\displaystyle\sim_{\mathit{state}}$ $\displaystyle=\sim_{\mathit{event}}$
$\bullet$ LMP for the stochastic $\lambda$-calculus $\bullet$ From (Clerc et
al., 2019) $\sim_{\mathit{state}}\,\neq\,\sim_{\mathit{event}}$ $\circ$ From
(Terraf, 2011) $\sim_{\mathit{state}}\,\neq\,\sim_{\mathit{event}}$

Figure 2. Comparison of LMP-equivalences

###  3.1. Relational Reasoning

Before introducing bisimulation-based equivalences, it is convenient to
introduce some basic definitions on measurable spaces, relational reasoning on
them, and the crucial notion of a relational extension on probability
measures. We denote by $\mathcal{R},\mathcal{S},\ldots$ binary relations,
writing $\mathcal{I}$ for the identity relation (with subscripts, when
necessary), $\mathcal{R};\mathcal{S}$ for relation composition (in
diagrammatic order), and $\mathcal{R}^{-}$ for the converse (or transpose) of
$\mathcal{R}$. Even if most of the results presented in this section hold for
arbitrary (endo)relations, it is convenient to work right from the beginning
with equivalence relations: given a set $X$, we denote by $\mathscr{R}(X)$ the
complete lattice of equivalence relations on $X$. Finally, when reasoning
relationally, we implicitly view any function $f$ as a relation (via its
graph).

The crucial ingredient to define bisimulation-like equivalences on Markov
processes (as introduced later in the paper) is the notion of an extension of
relations over a space $X$ to relations over $\Delta(X)$. Relational
extensions of that form are known in the literature as _relators_ or _lax
extensions_ (Backhouse and Hoogendijk, 1993; Barr, 1970). In this paper, we
are mostly concerned with the notion of relational extension used by Dal Lago
and Gavazzo (2019) to define applicative bisimilarity on stochastic
$\lambda$-calculi. At a high level, this extension is obtained as the
codensity lifting of the Giry monad (Katsumata et al., 2018). To define such
an extension formally, let us first recall that given a space $(X,\Sigma_{X})$
and a relation $\mathcal{R}\in\mathscr{R}(X)$, a set $A\subseteq X$ is
$\mathcal{R}$-closed if $\mathcal{R}[A]=A$. Moreover, we define
$\Sigma(\mathcal{R})$ as the sub-$\sigma$-algebra of $\Sigma$ defined as:
$\Sigma(\mathcal{R})=\\{A\in\Sigma\mid A\text{ is
}\mathcal{R}\text{-closed}\\}$.

###### Definition 3.1 (Probabilistic Relation Lifting).

Let $(X,\Sigma)$ be a measurable space. Define
$\Gamma:\mathscr{R}(X)\rightarrow\mathscr{R}{(\Delta{(X)})}$ by:222 Notice
that if $\mathcal{R}$ is an equivalence, then so is $\Gamma{\mathcal{R}}$.

$\mu\mathrel{\Gamma\mathcal{R}}\nu\iff\forall A\in\Sigma(\mathcal{R}).\
\mu(A)=\nu(A).$

The map $\Gamma$ essentially defines a relator for the Giry monad, as stated
by the following result.

###### Proposition 3.2.

The map $\Gamma$ is monotone. Moreover, we have:

$\displaystyle\mathcal{I}_{\Delta{(X)}}\subseteq\Gamma{(\mathcal{I}_{X})},\text{
}{\Gamma{\mathcal{R}}};{\Gamma{\mathcal{S}}}\subseteq\Gamma{(\mathcal{R};\mathcal{S})},\text{
}f_{\sharp}\subseteq\Gamma{f},\text{ }f_{\sharp}^{-}\subseteq\Gamma(f^{-})$
$\displaystyle\mathcal{R};\eta_{Y}\subseteq\eta_{X};\Gamma{\mathcal{R}},\quad\mathcal{R};g\subseteq
f;\Gamma{\mathcal{S}}\implies\Gamma{\mathcal{R}};g^{\dagger}\subseteq
f^{\dagger};\Gamma{\mathcal{S}}.$

###### Proof.

By noticing–see (Katsumata and Sato, 2015)–that for any $\mu,\nu\in\Delta(X)$
and $\mathcal{R}\in\mathscr{R}(X)$, one has
$\mu\mathrel{\Gamma\mathcal{R}}\nu$ if and only if
$\int_{X}f\mathit{d}\mu\leq\int_{X}f\mathit{d}\nu$, for any measurable
function $f:X\to[0,1]$ such that $x\mathrel{\mathcal{R}}y\implies f(x)\leq
f(y)$. ∎

In the literature, $\Gamma\mathcal{R}$ is often considered as a relation on
_proper_ distributions over $X$, instead of all sub-distributions as here. In
order to bridge this gap, we can encode sub-distributions as proper
distributions over the set $X\cup\\{\bot\\}$, where $\bot$ is a new point
designed to represent divergence. We formalize this idea in Lemma 3.4 below.

###### Notation 3.3.

We can see a sub-distributions on $Z$ as a (proper) distribution on
$Z_{\bot}:=Z\sqcup\\{\bot\\}$, where $\sqcup$ is the disjoint union operation
on polish spaces. If $\eta$ is a sub-distribution on $Z$, we note
$\eta_{\bot}$ the corresponding distribution on $Z_{\bot}$. Similarly, if $R$
is a binary relation on $X\times Y$, we write $R_{\bot}$ for the binary
relation on $X_{\bot}\times Y_{\bot}$ defined as
$R\cup\\{\bot_{X},\bot_{Y}\\}$.

###### Lemma 3.4.

Let $R$ be a binary relation on $X\times Y$, and $\mu$, $\nu$ two sub-
disributions on respectively $X$ and $Y$. Then $\mu\,\Gamma R\,\nu$ if and
only if $\mu_{\bot}\,\Gamma R_{\bot}\,\nu_{\bot}$.

When working with standard Borel spaces, there is another well-known
relational extensions corresponding to the so-called Wasserstein-Kantorovich
distance (Villani, 2008). Such an extension crucially relies on the notion of
a probabilistic coupling.

###### Definition 3.5.

Let $(X,\Sigma_{X})$, $(Y,\Sigma_{Y})$ be standard Borel spaces and
$\mu\in\Delta(X)$, $\nu\in\Delta(Y)$ be probability measures. A _coupling_ of
$\mu,\nu$ is a probability measure $\omega\in\Delta(X\times Y)$ such that for
all $A\in\Sigma_{X}$, $B\in\Sigma_{Y}$, we have: $\omega(A\times Y)=\mu(A)$
and $\omega(X\times B)=\nu(B)$. We denote by $\Omega(\mu,\nu)$ the set of
couplings of $\mu$ and $\nu$. Oserve that such a set is non-empty (e.g.,
product distributions form a coupling).

We now extend a relation $\mathcal{R}$ to probability measures by asking the
existence of a coupling compatible with $\mathcal{R}$ (cf. the existential
character of the following extension with the universal one of Definition
3.1).

###### Definition 3.6.

Let $(X,\Sigma_{X})$ be a standard Borel space. We define
$\Theta:\mathscr{R}(X)\to\mathscr{R}(\Delta(X))$ by:

$\mu\mathrel{\Theta\mathcal{R}}\nu\iff\exists\omega\in\Omega(\mu,\nu).\exists\mathcal{S}\in\Sigma_{X\times
X}.\
\mathcal{S}\subseteq\mathcal{R}\mathrel{\&}\omega(\mathcal{S})=\omega(X\times
X).$

It is easy to see that ${\Theta{\mathcal{R}}}\subseteq{\Gamma\mathcal{R}}$,
although $\Gamma$ and $\Theta$ define different relational extensions, in
general.333 In fact, whereas $\Gamma$ gives a lax relational extension of
$\mathcal{G}$, the map $\Theta$ does not. In particular, the map $\Theta$
corresponds to the so-called Barr lifting (Barr, 1970) of $\mathcal{G}$. Good
properties (viz. being a lax extension) of such a lifting are deeply connected
with weak-pullback preservation of $\mathcal{G}$ which, in general, does not
hold (Viglizzo, 2005).  This is due to the fact that we are working with
arbitrary equivalence relations, which do not reflect the (standard) Borel
structure of the spaces considered. Moving to relations reflecting such a
structure — known as _Borel_ relations — we indeed obtain the desired
equality.

###### Definition 3.7.

Given a standard Borel space $(X,\Sigma_{X})$ and
$\mathcal{R}\in\mathscr{R}(X)$, we say that $\mathcal{R}$ is a _Borel_
relation when the set $\\{(x,y)\mid x\mathcal{R}y\\}$ is a Borel set in
$X\times X$.

The advantage of working with Borel relations is that they are extremely well-
behaved. In particular, Borel relations allow us to generalise Monge-
Kantorovich duality to the measurable case, a result that we will need in
Section 5 .

###### Theorem 3.8.

Let $(X,\Sigma_{X})$ be a standard Borel space and
$\mathcal{R}\in\mathscr{R}(X)$ be a Borel relation. Then
$\Gamma{\mathcal{R}}=\Theta{\mathcal{R}}$.

###### Proof.

It is a result from (Katsumata and Sato, 2015) that for any
$\mu,\nu\in\Delta(X)$ and $\mathcal{R}\in\mathscr{R}(X)$, one has
$\mu\mathrel{\Gamma\mathcal{R}}\nu$ if and only if
$\int_{X}f\mathit{d}\mu\leq\int_{X}f\mathit{d}\nu$, for any measurable
function $f:X\to[0,1]$ such that $x\mathrel{\mathcal{R}}y\implies f(x)\leq
f(y)$. From there, we can conclude by applying the Monge-Kantorowitch duality
result for Borel cost functions from e.g. (Kellerer, 1984) (Beiglböck et al.,
2009). ∎

###  3.2. State Bisimilarity

The first notion of equivalence we consider is the natural generalization of
bisimilarity to transition systems on continuous state spaces. The natural
generalization of a (probabilistic) transition system to continuous states is
the notion of a Labelled Markov Process (LMP, for short).

###### Definition 3.9 (Labelled Markov Processes).

A _Labelled Markov Process_ (LMP) $\mathcal{M}$ is a triple
$(\mathcal{S},\mathcal{A},\\{h_{a}\mid a\in\mathcal{A}\\})$, where
$\mathcal{S}$ (the set of states) is measurable, $\mathcal{A}$ (the set of
labels) is an arbitrary set, and for every $a\in\mathcal{A}$ the map
$h_{a}:\mathcal{S}\times\Sigma_{\mathcal{S}}\rightarrow[0,1]$ is a sub-
probability kernel. If moreover $\mathcal{A}$ is a measureable set, and for
every $s\in\mathcal{S}$ the map $a\in\mathcal{A}\times
A\in\Sigma_{\mathcal{S}}\mapsto h_{a}(s,A)$ is a sub-probability kernel, then
we say that $\mathcal{M}$ is a _Measurably Labelled Markov Process_.

In the literature, the set $\mathcal{A}$ is very often taken to be countable.
However, this is not the case for the LMPs which model parameter passing in
calculi whose set of terms is itself not countable, since labels _include_
terms. Notice that a LMP $(\mathcal{S},\mathcal{A},\\{h_{a}\mid
a\in\mathcal{A}\\})$ gives a $\mathcal{A}$-indexed family of measurable maps
$h_{a}:\mathcal{S}\to\mathcal{G}(\mathcal{S})$. Exploiting this observation, a
state bisimulation is defined in terms of relational extensions for the Giry
monad.

###### Definition 3.10 (State Bisimulations).

Given a LMP $\mathcal{M}$, a _state bisimulation relation_ is a relation
$\mathcal{R}\in\mathscr{R}(\mathcal{S})$ such that, for all states $s,t$, if
$s\mathrel{\mathcal{R}}t$ holds, then so does
$h_{a}(s)\mathrel{\Gamma{\mathcal{R}}}h_{a}(t)$, for any label $a$.

We say that $s$ and $t$ are _state bisimilar_ — and write
$s\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}t$ — if there
exists a state bisimulation $\mathcal{R}$ such that $s\mathrel{\mathcal{R}}t$.
When the LMP $\mathcal{M}$ is clear from the context, we write
$\sim_{\mathit{state}}$ in place of
$\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}$ (and adopt the
same convention for all the equivalences defined in this paper).

Notice the crucial presence of the map $\Gamma$ in Definition 3.10. In fact,
one can obtain another definition of state bisimilarity simply by replacing
$\Gamma$ with $\Theta$ in Definition 3.10. Since
$\Theta{\mathcal{R}}\subseteq\Gamma{\mathcal{R}}$ holds for any relation
$\mathcal{R}$, bisimilarity based on $\Theta$ is included in bisimilarity
based on $\Gamma$, and the two coincide when they are Borel relations (Theorem
3.8). Unless otherwise specified, state bisimilarity will always refer to
Definition 3.10, and thus to the map $\Gamma$. The reason behind such a choice
is twofold: on the one hand, $\Gamma$-based bisimilarity is the one usually
finds in the literature; on the other hand, $\Gamma$ has in general nicer
properties than $\Theta$ ensuring, e.g., $\Gamma$-based bisimilarity to be an
equivalence relation.

###  3.3. Logical Equivalence

Another classic approach to define program equivalence is via logic (Larsen
and Skou, 1991; Desharnais et al., 1998). Informally, formulas of the logic
are used as discriminators between programs, and two programs are equivalent
if they yield the same interpretation for all formulas. In our setting, such a
logic takes the form of a probabilistic modal logic.

###### Definition 3.11 (Probabilistic Modal Logic).

Given a set $\mathcal{A}$ of actions, we define a class of logical formulas by
way of the following grammar, where $a\in\mathcal{A}$ and
$q\in\mathbb{Q}\cap[0,1]$:

$\displaystyle\phi\in\mathcal{L}$
$\displaystyle\;::=\;\top\;\;\mbox{\Large{$\mid$}}\;\;\phi_{1}\wedge\phi_{2}\;\;\mbox{\Large{$\mid$}}\;\;\langle
a\rangle_{q}{\phi}.$

The semantics of formulas is given parametrically on a LMP
$(\mathcal{S},\mathcal{A},\\{h_{a}\mid a\in\mathcal{A}\\})$ by associating to
each formula in $\mathcal{L}$ an element of $\Sigma$ as follows, where
$\langle a\rangle_{r}{A}=\\{s\mid h_{a}(s,A)>r\\}$.

$\displaystyle\llbracket\top\rrbracket$ $\displaystyle=\mathcal{S};$
$\displaystyle\llbracket\phi_{1}\wedge\phi_{2}\rrbracket$
$\displaystyle=\llbracket\phi_{1}\rrbracket\cap\llbracket\phi_{2}\rrbracket;$
$\displaystyle\llbracket\langle a\rangle_{q}{\phi}\rrbracket$
$\displaystyle=\langle a\rangle_{q}{\llbracket\phi\rrbracket}.$

We say that two states $s,t\in\mathcal{S}$ are _equivalent_ with respect to
$\mathcal{L}$ — and write $s\sim_{\mathit{logic}}t$ — when for every
$\phi\in\mathcal{L}$, it holds that
$(s\in\llbracket\phi\rrbracket\Leftrightarrow t\in\llbracket\phi\rrbracket)$.

###  3.4. Testing Equivalence

The idea behind testing equivalence (Larsen and Skou, 1991; Van Breugel et
al., 2005) is close to the one behind logical equivalence: in both cases,
syntactic entities play the role of state discriminators. However, in a
testing scenario one is allowed to use tests whose outcome is not necessarily
a _truth value_ , but rather the probability of passing the underlying test.
The shift from a boolean to a quantitative setting allows one to define
equivalence between states of a LMP using a restricted grammar of tests.

###### Definition 3.12.

Let $\mathcal{A}$ be a set of labels. We consider the following test language:

$\mathcal{T}:=\omega\;\;\mbox{\Large{$\mid$}}\;\;\alpha\wedge\alpha\;\;\mbox{\Large{$\mid$}}\;\;a\cdot\alpha\qquad\text{
with }a\in\mathcal{A}.$

For a given $\mathcal{M}=(\mathcal{S},\Sigma,\\{h_{a}\mid
a\in\mathcal{A}\\})$, we define by induction on tests the _success probability
of the test $\alpha$ starting from a state $s$_ as the measurable $1$-bounded
function $\text{Prob}(\alpha,\cdot):\mathcal{S}\rightarrow[0,1]$:

$\displaystyle\text{Prob}(\omega,s)$ $\displaystyle=1;$
$\displaystyle\text{Prob}(a\cdot\alpha,s)$
$\displaystyle=\int\text{Prob}(\cdot,\alpha)dh_{a}(s,\cdot);$
$\displaystyle\text{Prob}(\alpha\wedge\beta,s)$
$\displaystyle=\text{Prob}(\alpha,s)\cdot\text{Prob}(\beta,s).$

Notice that since tests have numerical outcomes, we do not need modalities in
the test language.

###### Definition 3.13.

Let $\mathcal{M}$ be a LMP. We write $s\sim_{\mathit{test}}t$ if
$\text{Prob}(s,\alpha)=\text{Prob}(t,\alpha)$ for every
$\alpha\in\mathcal{T}$.

###  3.5. Event Bisimilarity

The last notion of equivalence on LMPs we consider is _event bisimilarity_ ;
it has been introduced in (Danos et al., 2005, 2006) as a coinductively
defined notion of equivalence larger than state bisimilarity and coinciding
with testing and logical equivalence for a wide class of LMPs. From a
categorical viewpoint, it can be seen as going from a span-based notion of
bisimulation to a co-span-based one. From an operational point of view, it is
obtained by shifting the focus from equivalent states to visible _events_ —
represented as sub $\sigma$-algebras. In order to introduce event
bisimilarity, it useful to recall how state bisimilarity can be characterized
measure-theoretically:

###### Lemma 3.14.

Given an LMP $(\mathcal{S},\Sigma,\\{h_{a}:\mid a\in\mathcal{A}\\})$, a binary
relation $\mathcal{R}$ is a bisimulation if and only if
$(\mathcal{S},\Sigma(\mathcal{R}),\\{h_{a}\mid a\in\mathcal{A}\\})$ is a LMP.

Event bisimilarity arises as a variation on the characterization in Lemma 3.14
obtained by removing the constraint about the underlying $\sigma$-algebra:

###### Definition 3.15.

An event bisimulation on a LMP $(\mathcal{S},\Sigma,\\{h_{a}:\mid
a\in\mathcal{A}\\})$ is a sub-$\sigma$-algebra $\Lambda$ of $\Sigma$, such
that $(\mathcal{S},\Lambda,\\{h_{a}\mid a\in\mathcal{A}\\})$ is a LMP. Let
$\Lambda$ be a $\sigma$-algebra on $\mathcal{S}$. We note
$\mathcal{R}_{\Lambda}$ for the binary relation on states defined by
$\mathcal{R}_{\Lambda}=\\{(s,t)\mid\forall A\in\Lambda,s\in A\Leftrightarrow
t\in A\\}$. We say that two states $s,t\in\mathcal{S}$ are event bisimilar —
and write $s\sim_{\mathit{event}}t$ — when there exists an an event
bisimulation $\Lambda$ such that $(s,t)\in\mathcal{R}_{\Lambda}$.

###  3.6. Comparing the Equivalences

Now that we have introduced four notions of equivalence on the state of LMPs —
viz. _state_ and _event_ bisimilarity, and _logical_ and _testing_ equivalence
— it is natural to consider the correspondence between them. As long as one
focus on systems with discrete states (and countable actions) all the
equivalences mentioned so far coincide (van Breugel et al., 2005; Danos et
al., 2006; Fijalkow et al., 2017; Danos et al., 2005). The correspondence
still holds if LMPs have a _countable_ number of labels and their underlying
states space is _analytic_ :

###### Theorem 3.16.

Let $\mathcal{M}$ be a LMP with analytic state space and countably many
labels. Then:

${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{logic}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{test}}}}}.$

###### Proof.

Fijalkow et al. (2017) have proved
${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{logic}}}}}$,
whereas Danos et al. (2005) have shown
${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}$.
The remaining identities actually hold on arbitrary LMPs, as we are going to
see. ∎

Moving from LMPs with an analytic state space and countable actions to
arbitrary LMPs, the logical and testing characterizations of event
bisimilarity remains valid (van Breugel et al., 2005; Danos et al., 2006),
whereas state bisimilarity has been proved to be finer then event bisimilarity
(Danos et al., 2006).

###### Theorem 3.17 ((van Breugel et al., 2005; Danos et al., 2006)).

Let $\mathcal{M}$ be any LMP. Then

${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}}\subseteq{\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{logic}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{test}}}}}.$

###### Proof.

Danos et al. (2006) have proved
${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}}\subseteq{\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}$,
whereas van Breugel et al. (2005) and Danos et al. (2006) have shown
${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{logic}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{test}}}}}$.
To be precise on bibliographical references for this last equality, we should
note that–as clarified in a follow-up paper (Mislove et al., 2007)–the proof
of the testing characterization for LMP given in (van Breugel et al., 2005)
works for event bisimulation with no restriction on states spaces. However,
both in (Mislove et al., 2007) and (van Breugel et al., 2005), the labels are
restricted to a countable set. It doesn’t appear that this restriction is used
in the proof, but nonetheless we can extend the testing characterization to
the general case using the logical characterization from Theorem 3.17 and our
approximation Lemma 3.19. ∎

###### Remark 3.18.

Looking at Theorem 3.17, we could ask ourselves wether there exist LMP such
that all the equivalence notions we consider do not coincide. Of course, we
know from Theorem 3.16 that such a LMP should have non-analytic state space,
or uncountable labels. Such counter-examples have been built in the
literature, for both cases: on the one hand, a LMP with uncountable labels,
analytical states spaces have been presented (Clerc et al., 2019); on the
other hand, it has been shown (Terraf, 2011) that, under the assumption that
there exist non-measurable sets (which can be derived from the axiom of
choice), there exists a LMP with countable labels, non analytic state space,
where the two bisimulation do not coincide.

As corollaries of Theorem 3.17, we obtain an approximation scheme for event
bisimulation on LMPs with _uncountably many_ labels and that event
bisimilarity on LMPs with countably many actions is a Borel relation, a result
we will use in Section 5 below.

###### Lemma 3.19.

  1. (1)

Let $\mathcal{A}$ be a (possibly uncountable) set and let
$(\mathcal{S},\Sigma,\\{h_{a}\mid a\in\mathcal{A}\\})$ be a LMP. Then two
states $s,t$ are event bisimilar in this LMP if and only if they are event-
bisimilar in every LMP of the form $(\mathcal{S},\Sigma,\\{h_{a}\mid
a\in\mathcal{B}\\})$ where $\mathcal{B}$ a _countable_ subset of
$\mathcal{A}$.

  2. (2)

Let $\mathcal{M}$ be a LMP with a countable set of actions, then
${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}$ is Borel.

###### Proof.

  1. (1)

The proof relies on the equality
${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{logic}}}}}$
and the fact that to check whether a given formula $\phi$ holds for some state
$s$, it is sufficient to consider a finite numbers of labels. Let
$\mathcal{M}=(\mathcal{S},\Sigma,\\{h_{a}\mid a\in\mathcal{A}\\})$ be a LMP.

     * •

First, observe that the set $\mathcal{L}$ of logical formulas that caracterise
event bisimilarity on $\mathcal{M}$ contains the set of formulas that
caracterise event bisimilarity on any of the
$\mathcal{M}^{\prime}=(\mathcal{S},\Sigma,\\{h_{a}\mid
a\in\mathcal{A}^{\prime}\\})$ with $\mathcal{A}^{\prime}$ a countable subset
of $\mathcal{A}$. It means that two states $s,t$ event bisimilar in
$\mathcal{M}$ are also state bisimilar in $\mathcal{M}^{\prime}$.

     * •

Let us consider now two states $s,t$ that are not event bisimilar in
$\mathcal{M}$: we need to show that there exists a countable subset
$\mathcal{A}^{\prime}$ of $\mathcal{A}$, such that $s,t$ are not event
bisimilar in $\mathcal{M}^{\prime}=(\mathcal{S},\Sigma,\\{h_{a}\mid
a\in\mathcal{A}^{\prime}\\})$. To show that, we use again the logical
caracterisation of event bisimilarity, and it gives us a formula
$\phi\in\mathit{logic}$ such that $s\in\llbracket\phi\rrbracket$, and
$t\not\in\llbracket\phi\rrbracket$–or $t\in\llbracket\phi\rrbracket$, and
$s\not\in\llbracket\phi\rrbracket$, but the reasonning would be identical in
this case. Recall that $\phi$ is generated by the BNF grammar of Definition
3.11, so in particular there is a _finite_ number of $a\in\mathcal{A}$ that
occur in $\phi$. Looking at the Definition of $\llbracket\phi\rrbracket$, we
see that it is identical in $\mathcal{M}$ and
$\mathcal{M}^{\prime}=(\mathcal{S},\Sigma,\\{h_{a}\mid
a\in\mathcal{A}^{\prime}\\})$, as long as all the action that occur in $\phi$
are in $\mathcal{A}^{\prime}$. From there, we are able to conclude using
Proposition 3.17.

  2. (2)

We notice that if $\mathcal{M}$ has countably many actions, then the set
$\mathcal{L}$ of logical formulas for $\mathcal{M}$ is countable. Since for
any such formula $\phi$ the set $\llbracket\phi\rrbracket$ is Borel, we have
that ${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{logic}}}}}$, and
thus ${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}$, is
Borel.

∎

###  3.7. A LMP for $\Lambda_{\mathbf{P}}$.

The dynamic semantics of the language $\Lambda_{\mathbf{P}}$ we introduced in
Section 2 can be presented as a LMP, this way enabling the various forms of
equational reasoning principles presented above. In this section, we define
the aforementioned LMP, then discuss why this LMP is problematic, deferring a
more thorough discussion about it to Section 6 below.

####  3.7.1. Definition of the LMP $\mathcal{M}_{\Lambda_{\mathbf{P}}}$

Actually, there is a standard way of turning (possibly effectful) typed
$\lambda$-calculi into labelled transition systems: states are partitioned
into two classes, namely computations and values, and the environment
interacts with the former through an evaluation action and with the latter by
inspecting the value (e.g. if it has a coproduct type) or by passing it an
argument (if it is of an arrow type). We are going to follow this pattern, but
an additional difficulty is present here, namely the one of dealing with real
numbers as values. How should the environment inspect such a value? Ground
types are generally managed through actions which fully reveal the underlying
value. Remarkably, this works quite well in presence of discrete ground types
and discrete probabilities. However, when we go from discrete to continuous
probabilities — and thus from natural numbers to real numbers as base type —
things become more complicated. In particular, a real number value can be
inspected through the comparison operator $\mathit{op}_{\leq}$, which we ask
to always be part of $\mathcal{C}$.

###### Definition 3.20.

We define $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ as the LMP
$(\mathcal{S}_{\Lambda_{\mathbf{P}}},\mathcal{A}_{\Lambda_{\mathbf{P}}},\\{h_{a}\mid
a\in\mathcal{A}_{\Lambda_{\mathbf{P}}}\\})$ where:

  * •

The set of states is $\mathcal{S}_{\Lambda_{\mathbf{P}}}=\bigcup_{\sigma\in
T}\\{(M,\sigma)\mid M\in\mathscr{T}_{\sigma}\\}\cup\\{(V,\sigma)\mid
V\in\mathscr{V}_{\sigma}\\}$; we take as topology on
$\mathcal{S}_{\Lambda_{\mathbf{P}}}$ the countable disjoint union topology,
see (Ehrhard et al., 2018; Borgström et al., 2016) (recall that Pol has
countable coproducts).

  * •

The set of actions is
$\mathcal{A}_{\Lambda_{\mathbf{P}}}=T\cup(\bigcup_{\sigma\in
T}\mathscr{V}_{\sigma})\cup\\{\text{eval}\\}\cup\\{\overset{\text{?}}{\leq}q\mid
q\in\mathbb{Q}\\}\cup\\{\text{case}(\hat{\imath})\mid i\in
I\\}\cup\\{\text{unbox}\\}$. Again, we take the disjoint union topology on
$\mathcal{A}_{\Lambda_{\mathbf{P}}}$.

  * •

The transition functions are defined as follows, where $h_{a}(s)=\emptyset$ in
all cases not listed below.

$\displaystyle h_{\sigma}(s)$ $\displaystyle=\\{s^{1}\\}$
$\displaystyle\mbox{if }s=(M,\sigma)\text{ or }s=(V,\sigma);$ $\displaystyle
h_{V}(s)$ $\displaystyle=\\{(WV,\tau)^{1}\\}$ $\displaystyle\mbox{if
}s=(W,\sigma\to\tau);$ $\displaystyle h_{\text{eval}}(s)$
$\displaystyle=(\llbracket M\rrbracket,\sigma)$ $\displaystyle\mbox{if
}s=(M,\sigma);$ $\displaystyle h_{\overset{\text{?}}{\leq}q}(s)$
$\displaystyle=op_{\leq}(r,q)\cdot\\{s^{1}\\}$ $\displaystyle\mbox{if }\exists
r\in\mathbb{R},s=(\bm{r},\mathbf{real})$ $\displaystyle
h_{\text{case}(\hat{\imath})}(s)$ $\displaystyle=\\{(V,\sigma_{i})^{1}\\}$
$\displaystyle\mbox{if }s=((\hat{\imath},V),\sum\nolimits_{j\in
I}{\sigma_{j}})$ $\displaystyle h_{\text{unbox}}(s)$
$\displaystyle=\\{(V,\sigma[\mu\alpha.\sigma/\alpha])^{1}\\}$
$\displaystyle\mbox{if }s=(\mathbf{fold}\ V,\mu\alpha.\sigma)$

The LMP $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ we have just introduced naturally
captures the interaction between a term and the environment, in the spirit of
Abramsky’s applicative bisimilarity. In particular, _state_ bisimilarity on
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$ captures applicative bisimilarity on
$\Lambda_{\mathbf{P}}$ (Dal Lago and Gavazzo, 2019), meaning that
$M,N\in\mathscr{T}_{\sigma}$ are applicative bisimilar precisely when
$(M,\sigma)\sim_{\mathit{state}}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}}(N,\sigma)$
(oftentimes, we use the notation
$M\sim_{\mathit{state}}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}}N$) and similarly
for values. Unfortunately, $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ is not among
those LMPs for which nice correspondence results exist between the various
notions of equivalences. Although the _state_ space is analytic, indeed, the
_action_ space is inherently uncountable, due to the presence of values among
the labels. This is unavoidable, given the nature of applicative bisimilarity,
and has some deep consequences, as we are going to see in Section 6 below. But
how about $\Lambda_{\mathbf{P}}^{c}$? Actually, one can naturally define
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ exactly as
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$, with the additional proviso that terms
occurring in states and actions are taken from $\Lambda_{\mathbf{P}}^{c}$
rather than from $\Lambda_{\mathbf{P}}$. In the next two sections we are going
to show that going from $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ to
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ indeed makes a difference as far as
the nature of relational reasoning is concerned.

####  3.7.2. How To Act on Real Numbers

While the structure of $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ with respect to
evaluation, application of function to values are quite standard for
applicative bisimulations on typed $\lambda$-calculi–see for instance the way
the applicative bisimulation was defined in (Crubillé and Dal Lago, 2014) for
a discrete probabilistic $\lambda$-calculus–deciding which actions we put on
$\mathbf{real}$ values is more subtle. The leading principle behind our choice
was that for programs at base type, context equivalence, event bisimilarity
and state bisimilarity should all coincide. Moreover, in order to avoid un-
necessary complexity, we were looking for a _countable_ family of ground-type
actions. It can be checked that these guidelines hold for the ground-type
action we gave in Definition 3.20. It can also be observed that they would not
hold for the–perhaps more intuitive–family of ground type actions indexed by
$r\in\mathbb{R}$
$(h_{r^{\prime}}(\bm{r}):=(?(r=r^{\prime}))\cdot\\{\bm{r}^{1}\\})_{r^{\prime}\in\mathbb{R}}$:
not only this family is not countable, but more importantly event bisimulation
do not coincide with context equivalence for real typed programs. For
instance, we can see using the testing caracterisation that the program
$\mathbf{sample}$ and $(\mathbf{sample}+1)$ would not be event bisimilar for
this variation of $\mathcal{M}_{\Lambda_{\mathbf{P}}}$.

In this section, we explore in which sense we can say that our notions of
state and event bisimilarities for $\Lambda_{\mathbf{P}}$ are stable under
changes to the way we define the actions on real type in
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$. To do that, we first define formally an
applicative LMP parametric in which actions we choose on real type. We are
actually interested on variation of the following form: an action on $a$ on a
ground type value $\bm{r}$ must do a loop on $\bm{r}$, but this loop only
succeeds with a probability that depends on $r$ and $a$. We formalize this
idea in Definition 3.21 below.

###### Definition 3.21.

Let $\mathcal{P}$ be any family of measureable functions $\mathbb{R}\to[0,1]$.
We will write $\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})$ for the LMP
obtained from $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ by removing the actions
${\overset{\text{?}}{\leq}q}_{q\in\mathbb{Q}}$, and adding the action
$(h_{p})_{p\in\mathcal{P}}$ where:

$h_{p}(s)=\begin{cases}p(r)\cdot\\{\bm{r}^{1}\\}\text{ if }\exists r\text{
with }s=\bm{r};\\\ \emptyset\text{ otherwise.}\end{cases}$

We first show a quite generic criteria for changes on ground-type action that
preserves state bisimilarity for $\mathcal{M}_{\Lambda_{\mathbf{P}}}$: it says
that whenever we keep a family of ground-type action that is generated by a
family of function that separates points–in the sense of Remark 2.6–then the
state bisimilarity stays the same.

###### Lemma 3.22.

For every $\mathcal{P}$ that separates points, the state bisimulation on
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})$ coincide with the state
bisimulation on $\mathcal{M}_{\Lambda_{\mathbf{P}}}$.

###### Proof.

First, observe that the ground-type action on
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$ are generated by a family of function
that separates points (the family
$\mathcal{F}_{\leq}:={(\overset{\text{?}}{\leq}q)}_{q\in\mathbb{Q}}$). Now, we
show that for every families $\mathcal{P}$, $\mathcal{F}$ that separates
points any state bisimulation $\mathcal{R}$ for
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})$ is also a state bisimulation
for $\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})$. Let be
$s,t\in\mathcal{S}_{\Lambda_{\mathbf{P}}}$ such that $s\mathcal{R}t$, and
$a\in\mathcal{A}_{\Lambda_{\mathbf{P}}}$. Let $a$ an action in
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})$. We want to show that
$h_{a}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})}(s)\Gamma\mathcal{R}h_{a}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})}(t)$.
Observe that if $a$ is not in $\mathcal{P}$, the action
$h_{a}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})}$ coincide with
$h_{a}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})}$, so we can conclude
using our hypothesis on $\mathcal{R}$. Now, suppose that $a=p$, with
$p\in\mathcal{P}$. Observe that since $s,t$ are bisimilar in
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})$, then either $s,t$ are both
$\mathbf{real}$ values, or none of them is. In the second case, we can
immediately conclude. In the first case, since the original family of actions
$\mathcal{F}$ separates all reals, we know that $s=t$, thus we can conclude. ∎

We look now for a criterion for event bisimilarity. As a first step, we
formalize in Definition 3.23 below the idea that a family of actions can
generates all Borel sets on $\mathbb{R}$.

###### Definition 3.23.

We say that a family $\mathcal{F}$ be a family of measureable functions
$\mathbb{R}\to[0,1]$ is _Borel-generating_ whenever the smallest
$\sigma$-algebra containing all the sets $f^{-1}(I)$ for
$I\in\text{Borel}([0,1])$, $f\in\mathcal{F}$ is the Borel algebra over
$\mathbb{R}$.

We can check easily that the family
$\mathcal{F}_{\leq}:={(\overset{\text{?}}{\leq}q)}_{q\in\mathbb{Q}}$ is Borel
generating. Now, Lemma 3.24 tells us that as long as the family of functions
$\mathcal{F}$ we consider is Borel genrating, the event bisimilarity on
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})$ stays the same as the event
bisimilarity on $\mathcal{M}_{\Lambda_{\mathbf{P}}}$.

###### Lemma 3.24.

Let $\mathcal{F}$ be Borel-generating family of functions. Then
$\sim^{\mathcal{M}_{\Lambda_{\mathbf{P}}}}_{event}\,=\,\sim^{\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})}_{event}.$

The proof of Lemma 3.24 is more involved that the one of Lemma 3.22, and as a
consequence we first prove the auxilliary Lemma 3.25 below: it tells us that
to show that we obtain the same event bisimilarity on the two LMPs
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})$ and
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})$, it is enough to look at the
states of the form $\bm{r}$.

###### Lemma 3.25.

Let $\mathcal{P}$, $\mathcal{F}$ be two families of measureable functions
$\mathbb{R}\to\mathbb{R}$, and $\Lambda_{\mathcal{P}}$,
$\Lambda_{\mathcal{F}}$ the event bisimilarities in
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})$ and
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})$ respectively. We suppose
that $\\{A\mid
A\in\Lambda_{\mathcal{P}}\cap\mathscr{V}_{\mathbf{real}}\\}=:(\Lambda_{\mathcal{P}})_{\mid\mathscr{V}_{\mathbf{real}}}\supseteq(\Lambda_{\mathcal{F}})_{\mid\mathscr{V}_{\mathbf{real}}}:=\\{A\mid
A\in\Lambda_{\mathcal{F}}\cap\mathscr{V}_{\mathbf{real}}\\}$. Then it holds
that $\Lambda_{\mathcal{P}}\subseteq\Lambda_{\mathcal{F}}$ .

###### Proof.

We note $\mathcal{M}_{\Lambda_{\mathbf{P}}}^{\star}$ for the applicative LMP
without action on reals, that is
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\emptyset)$. We are going to show that
$\Lambda_{\mathcal{P}}$ is an event bisimulation on
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})$. To do that, we need to show
that $(\mathcal{S}_{\Lambda_{\mathbf{P}}},\Lambda_{\mathcal{P}},\\{h_{a}\mid
a\in\mathcal{A}_{\mathcal{F}}\cup\mathcal{A}_{\Lambda_{\mathbf{P}}^{\star}}\\})$
is a LMP, i.e. that for every
$a\in\mathcal{A}_{\mathcal{F}}\cup\mathcal{A}_{\Lambda_{\mathbf{P}}^{\star}}$,
the restriction of $h_{a}$ to the map
$h_{a}:\mathcal{S}_{\Lambda_{\mathbf{P}}}\times\Lambda_{\mathcal{P}}\rightarrow[0,1]$
is a sub-probability kernel. First, observe that when
$a\in\mathcal{A}_{\Lambda_{\mathbf{P}}^{\star}}$, we obtain immediately the
result using the fact that $\Lambda_{\mathcal{P}}$ is an event bisimulation on
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})$, and moreover
$h_{a}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})}$ and
$h_{a}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})}$ coincide. Suppose
now that $a=f\in\mathcal{F}$: We are going to check that $h_{f}$ is indeed a
kernel:

  * •

For every $A\in\Lambda_{\mathcal{P}}$, the map
$m_{A}:s\in(\mathcal{S}_{\Lambda_{\mathbf{P}}},\Lambda_{\mathcal{P}})\mapsto
h_{f}(s,A)\in(\mathbb{R},\text{Borel}(\mathbb{R}))$ is measureable. Let
$I\in\text{Borel}(\mathbb{R})$: we see that
$m_{A}^{-1}(I)=(m_{A}^{-1}(I)\cap\mathscr{V}_{\mathbf{real}})\cup(m_{A}^{-1}(I)\cap(\mathcal{S}_{\Lambda_{\mathbf{P}}}\setminus\mathscr{V}_{\mathbf{real}}))$.
Observe first that
$(m_{A}^{-1}(I)\cap(\mathcal{S}_{\Lambda_{\mathbf{P}}}\setminus\mathscr{V}_{\mathbf{real}}))\in\\{\emptyset,\mathcal{S}_{\Lambda_{\mathbf{P}}}\setminus\mathscr{V}_{\mathbf{real}}\\}\subseteq\Lambda_{\mathcal{P}}$
(the last inclusion is given by the actions $a$ with $a\in T$). Then, we
observe that $m_{A}^{-1}(I)\cap\mathscr{V}_{\mathbf{real}}=\\{\bm{r}\mid
f(r)\in I\wedge\bm{r}\in A\\}=m_{\mathbb{R}}^{-1}(I)\cap A$. From there, since
$(\Lambda_{\mathcal{P}})_{\mid\mathscr{V}_{\mathbf{real}}}\supseteq(\Lambda_{\mathcal{F}})_{\mid\mathscr{V}_{\mathbf{real}}}$,
and
$m_{\mathbb{R}}^{-1}(I)\in(\Lambda_{\mathcal{F}})_{\mid\mathscr{V}_{\mathbf{real}}}$,
it holds that
$m_{A}^{-1}(I)\cap\mathscr{V}_{\mathbf{real}}\in\Lambda_{\mathcal{P}}$, and we
can conclude.

  * •

For every $s\in\mathcal{S}_{\Lambda_{\mathbf{P}}}$, the map
$A\in\Lambda\mapsto h_{a}(s,A)$ is a sub-probability measure. We see that
immediately from the fact that
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{P})$ is a LMP, and $\Lambda$ is a
sub sigma-algebra of $\Sigma_{\mathcal{S}_{\Lambda_{\mathbf{P}}}}$.

∎

###### Proof of Lemma 3.24.

Let $\Lambda_{\mathcal{F}},\Lambda$ be the event bisimilarities in
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})$ and
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$ respectively. Observe that
$\mathscr{V}_{\mathbf{real}}$ is a self-contained fragment of both
$\mathcal{M}_{\Lambda_{\mathbf{P}}}(\mathcal{F})$ and
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$: as a consequence
$\Lambda_{\mathcal{F}}\cap\mathscr{V}_{\mathbf{real}}$, and
$\Lambda\cap\mathscr{V}_{\mathbf{real}}$ can be caracterised as the event
bisimulations on the LMPs
$(\mathscr{V}_{\mathbf{real}},\Sigma_{\mid\mathbf{real}},\\{h_{f}\mid
f\in\mathcal{F}_{\leq}\cup\\{\mathbf{real}\\}\\})$ and
$(\mathscr{V}_{\mathbf{real}},\Sigma_{\mid\mathbf{real}},\\{h_{f}\mid
f\in{\mathcal{F}}\cup\\{\mathbf{real}\\}\\})$ respectively. Using the
definition of event bisimulation, we obtain that for every $f\in\mathcal{F}$,
the map
$\bm{r}\in(\mathscr{V}_{\mathbf{real}},\Lambda_{\mathcal{F}}\cap\mathscr{V}_{\mathbf{real}})\to
h_{f}(r,\mathbb{R})=f(r)\in(\mathbb{R},\text{Borel}(\mathbb{R}))$ is
measureable. It is a known result from the literature–see for instance ,
caracterisation of a $\sigma$-algebra generated by a collection of
mappings–that this condition implies that
$\Lambda_{\mathcal{F}}\cap\mathscr{V}_{\mathbf{real}}$ contains the
$\sigma$-algebra generated by $\mathcal{F}$. By hypothesis, the
$\sigma$-algebra generated by $\mathcal{F}$ coincides with
$\text{Borel}(\mathbb{R})$, meaning that
$\text{Borel}(\mathbb{R})=\Sigma\cap\mathscr{V}_{\mathbf{real}}\supseteq(\Lambda_{\mathcal{F}}\cap\mathscr{V}_{\mathbf{real}}\supseteq\text{Borel}(\mathbb{R})\supseteq(\Lambda\cap\mathscr{V}_{\mathbf{real}})$,
and from there we can conclude by applying Lemma 3.25. For the reverse
inclusion, we can do the same reasonning in exchanging $\mathcal{F}$ and
$\mathcal{F}_{\leq}$, using the fact that also $\mathcal{F}_{\leq}$ is Borel-
generating.

∎

##  4\. Continuity to the Rescue

As already mentioned, most of the literature on relational reasoning on LMPs
focuses on cases where labels are countable. A notable exception is (Fijalkow
et al., 2017), in which it is shown that adding a _continuity_ condition on
the LMP transition function allows, in the case of _uncountably_ many labels,
to recover the coincidence between some notions of equivalence. We now briefly
present the setting from (Fijalkow et al., 2017), showing that, unfortunately,
it cannot be applied to LMPs like $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ or
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$.

###### Definition 4.1.

Let $\mathcal{M}=(\mathcal{S},\mathcal{A},\\{h_{a}\mid a\in\mathcal{A}\\})$ be
a LMP, such that $\mathcal{S}$ is a standard Borel space. We say it has a
_continuous transition function_ if, whenever $a\in\mathcal{A}$,
$X\in\Sigma_{\mathcal{S}}$, the function $s\in\mathcal{S}\mapsto
h_{a}(s,X)\in[0,1]$ is continuous.

Unfortunately, the continuity requirement on the underlying transition
function is not suitable for probabilistic transition systems built out of the
operational semantics of higher-order programming languages like
$\Lambda_{\mathbf{P}}$. Intuitively—and as illustrated in Remark 4.2 below —
this comes from the fact that Definition 4.1 forces any transition to either
have a fuzzy probabilistic behaviour, or to go into a constant state _not_
depending on the reals in the state of departure. As a consequence, it
excludes deterministic (labelled) transitions in which a value is passed as an
argument to a function. Since such steps exist independently on any continuity
requirements, the continuous transition function constraint does not hold in
(the LMPs underlying) any meaningful fragment of $\Lambda_{\mathbf{P}}$.

###### Remark 4.2.

We illustrate on an example why neither
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ nor
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$ have continuous transition functions. We
start from the action eval, and the measureable set $X=\\{\bm{0}\\}$. We
consider the family of terms $M_{n}=\bm{f}(\bm{r_{n}})$, where
$(r_{n})_{n\in\mathbb{N}}$ is a sequence of non-zero numbers converging to
$0$, and $f$ is the identity, thus a continuous function on $\mathbb{R}$. In
the standard Borel space $\mathcal{S}_{{\Lambda_{\mathbf{P}}^{c}}}$ (or
$\mathcal{S}_{\Lambda_{\mathbf{P}}}$), we define a sequence
$(u_{n})_{n\in\mathbb{N}}$ by $u_{n}:=(M_{n},\mathbf{real})$. Observe that
$u_{n}\xrightarrow[n\rightarrow\infty]{}(\bm{f}{(\bm{0})},\mathbf{real})$ in
the $\mathcal{S}_{{\Lambda_{\mathbf{P}}^{c}}}$ (or
$\mathcal{S}_{\Lambda_{\mathbf{P}}}$) topology. By contrast, we see that
$h_{\text{eval}}(M_{n},\mathbf{real})(X)=0$ for every $n$, while
$h_{\text{eval}}(\bm{f}(\bm{0}),\mathbf{real})(X)=1$; thus $h_{\text{eval}}$
is not a continuous transition function.

We thus need to go towards a different notion of continuity, which is what we
are going to do in the next subsection.

###  4.1. Feller-Continuous LMPs

analytical states spaces, uncountable labels labelwise continuous transition
function Feller-continuous kernels $\displaystyle\sim_{\mathit{state}}$
$\displaystyle=\sim_{\mathit{event}}$
$\bullet$$\mathcal{M}_{\Lambda_{\mathbf{P}}}$
$\bullet$$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$

Figure 3. LMP-equivalences for Analytical States Spaces and Uncountable Labels

Our goal now is to introduce a different continuity requirement on LMPs, that
both holds for $\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ and enforces
coincidence of event and state bisimilarities.

####  4.1.1. Definition of Feller-Continuous Kernels

We first introduce a notion of convergence for measures on a standard Borel
space, which is in fact standard (Swart and Winter, 2013; Parthasarathy,
2005). Recall that for any program $M$, $\llbracket M\rrbracket$ is a measure
on the standard Borel space $\mathscr{V}$.

###### Definition 4.3.

Let $X$ be a standard Borel space, equipped with its Borel $\sigma$-algebra.
Let $(\mu_{n})_{n\in\mathbb{N}}$ be a sequence of measures over $X$. We say
that $(\mu_{n})_{n\in\mathbb{N}}$ _converges weakly_ towards $\mu$ when for
every bounded and continuous $f:X\rightarrow\mathbb{R}$ it holds that

$\lim_{n\rightarrow\infty}\int_{X}f.d\mu_{n}=\int_{X}f.d\mu.$

The notion of weak convergence corresponds to a _topology_ (actually, the
space of sub-probability measures of a standard Borel space equipped with the
weak convergence forms a Polish space, and thus a standard Borel space). Since
we have equipped the space of measures with a topology, all this gives us a
notion of continuity for kernels, called _Feller continuity_ in the literature
(see, e.g., (Swart and Winter, 2013)).

###### Definition 4.4 (Feller-Continuous Kernels).

Let $X,Y$ be two standard Borel spaces. We say that a sub-probability kernel
$k:X\rightarrowtriangle Y$ is _Feller continuous_ when the function
$f_{k}:X\rightarrow\Delta{(Y)}$ is continous when equipping $\Delta{(Y)}$ with
the weak topology.

. Being a Feller kernel is a well-behaved notion: in particular, we can
observe that whenever a LMP $\mathcal{M}$ is actually a (non-probabilistic)
LTS, its transition kernel is Feller continuous. It is a consequence of the
following Lemma 4.5.

###### Lemma 4.5.

For every measurable function $f:\mathbb{R}^{k}\rightarrow\mathbb{R}^{p}$, we
denote by $\overline{f}$ the associated deterministic kernel
$f:\mathbb{R}^{k}\rightarrowtriangle^{=}\mathbb{R}^{p}$ defined as
$\vec{r}\mapsto\\{f(\vec{r})^{1}\\}$. Similarly, for any distribution
$\mu\in\Delta{(\mathbb{R}^{n})}$, we denote by $\overline{\mu}$ the associated
kernel $\mathbb{R}^{0}\rightarrowtriangle^{=}\mathbb{R}^{n}$. Whenever $f$ is
continuous, $\overline{f}$ is Feller continous. Moreover $\overline{\mu}$ is
always Feller continuous.

We now use this notion of Feller kernel to enforce additional continuity
requirements on LMPs.

###### Definition 4.6.

Let $\mathcal{M}=(\mathcal{S},\mathcal{A},\\{h_{a}\mid a\in\mathcal{A}\\})$ be
a measureably labelled Markov process. We say that $\mathcal{M}$ is _Feller
continuous_ whenever $\mathcal{S}$ and $\mathcal{A}$ are two standard Borel
spaces, and:

  * •

for every $a\in\mathcal{A}$, the kernel
$h_{a}:\mathcal{S}\times\Sigma_{\mathcal{S}}\rightarrow[0,1]$ is Feller
continuous;

  * •

for every $s\in\mathcal{S}$ the kernel
$(a\in\mathcal{A})\times(A\in\Sigma_{\mathcal{S}})\mapsto h_{a}(s,A)$ is
Feller continuous.

Please notice that it is enough for a Feller LMP to be continuous on
$\mathcal{A}$ and $\mathcal{S}$ _separately_ , and that we do not ask it to be
jointly continuous on $\mathcal{A}\times\mathcal{S}$, which is in general a
stronger condition (Piotrowski, 1985). Being a Feller continuous LMP is a
well-behaved notion: in particular, we can observe that whenever a LMP
$\mathcal{M}$ is actually a (non-probabilistic) LTS, its transition kernel is
Feller. The same holds when actions and states are both countable. Our aim is
to show that this notion of Feller continuity can indeed be applied to the
applicative LMP for $\Lambda_{\mathbf{P}}^{c}$, but not the one for
$\Lambda_{\mathbf{P}}$.

###### Remark 4.7.

Let us now discuss why $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ is _not_ Feller
continuous: we consider the action eval, and we show that the kernel
$h_{\text{eval}}:\mathcal{S}_{\Lambda_{\mathbf{P}}}\times\Sigma_{\mathcal{S}_{\Lambda_{\mathbf{P}}}}\rightarrow[0,1]$
is not Feller continuous. We consider the sequence of terms defined as:
$M_{n}=\bm{f}{(\bm{r_{n}})}$, where $f:\mathbb{R}\to\mathbb{R}$ is the
measureable function defined as $f(r)=1$ if $r<0$, and $0$ otherwise, and
$(r_{n})_{n\in\mathbb{N}}$ is a sequence of strictly negative real numbers
tending towards $0$. We see that
$h_{\text{eval}}(M_{n},\mathbf{real})=\\{\bm{1}^{1}\\}$ for every
$n\in\mathbb{N}$, but
$h_{\text{eval}}(\bm{f}{(\bm{0})},\mathbf{real})=\\{\bm{0}^{1}\\}$. Since it
is not the case that the stationary sequence
$(\\{\bm{1}^{1}\\})_{n\in\mathbb{N}}$ converges weakly towards
$\\{\bm{0}^{1}\\}$–with respect to the Borel topology on
$\mathcal{S}_{\Lambda_{\mathbf{P}}}$–we can conclude that
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$ is not Feller continuous.

Remark 4.7 indeed shows that $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ is not
Feller continuous. Note that our counterexample is based on the existence of
_non-continuous_ primitive real functions in $\Lambda_{\mathbf{P}}$. We will
deal with the Feller continuity of $\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ in
Section 5 below.

####  4.1.2. Technical Lemmas on Feller Continuous Kernels

In this section, we show structural properties of Feller kernels, that we will
need later in the proofs: stability of Feller constraints under countable
coproducts, compositionnality of Feller kernels, and caracterisation of weak
convergence of sub-probability measures as weak convergence for the associated
proper probability measures. Before stating formally those lemmas, let us
first give some elments about their relevance: we are interested in stability
under the infinite coproduct construction because all polish space that we use
for programs–$\mathscr{V},\mathscr{T}...$– are built as infinite coproduct; we
are interested in composing Feller kernels because it allow us to see Feller
kernels as a sub-category of Markov kernels; and we are interested in reducing
the weak convergence decision problem from sub-probability measure to
probability measure because, while we really need sub-probability kernels
model in our semantics the probability of non-termination, it allows us to use
result on proper probability kernels from the literature.

We show stability by countable coproduct first for weak convergence of
measures– in Lemma 4.9, and for the class of Feller kernels– in Lemma 4.10.

###### Notation 4.8.

Let $(X_{n})_{n\in\mathbb{N}}$ be a countable family of (disjoint) Polish
spaces, and $X:=\cup_{n\in\mathbb{N}}X_{n}$ endowed with the disjoint union
topology. For $\mu\in\Delta{(X)}$, we define $\mu^{X_{n}}\in\Delta{(X)}_{n}$
as the restriction of $\mu$ to $X_{n}$.

###### Lemma 4.9.

Let $(X_{n})_{n\in\mathbb{N}}$ be a countable family of (disjoint) polish
spaces, and $X:=\cup_{n\in\mathbb{N}}X_{n}$ endowed with the disjoint union
topology. Suppose $(\mu_{m})_{m\in\mathbb{N}}$ a sequence of
(sub)-distributions over $X$, and $\nu\in\Delta{(X)}$. Suppose that the
sequence $(\mu_{m})_{m\in\mathbb{N}}$ converges weakly towards $\nu$. Then
each of the sequence $(\mu^{X_{n}}_{m})_{m\in\mathbb{N}}$ converges weakly
towards $\nu^{X_{n}}$.

###### Proof.

Observe that for every $n$, for every bounded continuous function
$f:X_{n}\rightarrow\mathbb{R}$, for every measure $\mu$ on $X$,
$\int_{X_{n}}f\cdot d\mu^{X_{n}}=\int_{X}i_{n}(f)\cdot d\mu$, where
$i_{n}(f):x\in X\mapsto f(x)\text{ if }x\in X_{n},\,0\text{ otherwise}$.
Moreover, whenever $f$ is bounded continuous, also $i_{n}(f)$ is bounded
continuous for every $n\in\mathbb{N}$. From there, we can conclude. ∎

###### Lemma 4.10.

Let $(X_{n})_{n\in\mathbb{N}}$ be a countable family of (disjoint) Polish
spaces, and $Z$ a Polish space. Suppose a family
$f_{n}:X_{n}\rightarrowtriangle Z$. We define
$\bigsqcup_{n\in\mathbb{N}}f_{n}:\bigcup_{n\in\mathbb{N}}X\rightarrowtriangle
Z$, where $\bigcup_{n\in\mathbb{N}}X$ is the Polish space obtained as the
disjoint union of the $X_{n}$–with the disjoint union topology:

$\bigsqcup_{n\in\mathbb{N}}f_{n}(s)=f_{n_{0}}(s)\text{ with }X_{n_{0}}\text{
such that }s\in X_{n_{0}}.$

Then, if all the $f_{n}$ are Feller, also $\bigsqcup_{n\in\mathbb{N}}f_{n}$ is
Feller.

###### Proof.

Let $(\mu_{m})_{m\in\mathbb{N}}$ a sequence of (sub)-distributions over
$\bigsqcup_{n\in\mathbb{N}}X_{n}$ that converges weakly towards some
distribution $\nu$. Observe that for every $\mu$,
$(\bigsqcup_{n\in\mathbb{N}}f_{n})(\mu)=\sum_{n\in\mathbb{N}}f_{n}(\mu^{X_{n}})$,
with $\mu^{X_{n}}$ represents the restriction of $\mu$ to $X_{n}$. By Lemma
4.9, we can see that for every $n\in\mathbb{N}$, the sequence
$(\mu_{m}^{X_{n}})_{m\in\mathbb{N}}$ converge weakly towards $\nu^{X_{n}}$.
Since all the $f_{m}$ are Feller, we know that for every $n$, the sequence
$(f_{n}(\mu_{m}^{X_{n}}))_{m\in\mathbb{N}}$ converge weakly towards
$f_{n}(\nu^{X_{n}})$. As a consequence
$(\sum_{n\in\mathbb{N}}f_{n}(\mu_{m}^{X_{n}}))_{m\in\mathbb{N}})$ converge
weakly towards $(\sum_{n\in\mathbb{N}}f_{n}(\nu^{X_{n}}))_{m\in\mathbb{N}})$,
which concludes the proof. ∎

We now show how we can reduce the question of weak convergence for sub-
probability measures to weak convergence for (proper) probability measures.
Recall the notation $\mu_{\bot}$ introduced in Notation 3.3 to talk about the
proper probability measure associated to a sub-probability measure.

###### Lemma 4.11.

Let $(\mu_{n})_{n\in\mathbb{N}}$ be a sequence of sub-distributions that
converges weakly towards $\mu$. Then the sequence
$((\mu_{n})_{\bot})_{n\in\mathbb{N}}$ converges weakly towards $\mu_{\bot}$.

###### Proof.

Recall that by definition, for every $\nu\in\Delta{(X)}$,
$\nu_{\bot}=\nu+(1-\int_{X}d\nu)\cdot\\{\bot^{1}\\}$. By hypothesis we know
that $(\mu_{n})$ converge weakly towards $\mu$, thus its is enough to show
that for every $f:Z_{\bot}\rightarrow\mathbb{R}$ bounded continuous,
$\int_{Z_{\bot}}f\cdot
d((1-\int_{X}d\mu_{n})\cdot\\{\bot^{1}\\})\rightarrow\int_{Z_{\bot}}f\cdot
d((1-\int_{X}d\mu)\cdot\\{\bot^{1}\\})$. Observe that:

$\displaystyle\int_{Z_{\bot}}f\cdot
d((1-\int_{X}d\mu_{n})\cdot\\{\bot^{1}\\})$
$\displaystyle=f(\bot)\cdot(1-\int_{X}d\mu_{n})$ $\displaystyle\rightarrow
f(\bot)\cdot(1-\int_{X}d\mu)\text{ again by hypothesis on
}(\mu)_{n\in\mathbb{N}}$ $\displaystyle=\int_{Z_{\bot}}f\cdot
d((1-\int_{X}d\mu)\cdot\\{\bot^{1}\\}).$

∎

###### Lemma 4.12.

Feller continuous probability kernels are compositional.

###### Proof.

A composition result for Feller kernel is shown in (Swart and Winter, 2013),
as a corollary of Proposition 3.5 there, but with the additional constraints
that $X,Y,Z$ should be _compact_ –which is not adapted for our purposes. We
show it here for general metric spaces.We divide the proof in two steps: in a
first step, we show the result for proper probability kernels, and in a second
step we extend it to sub-probability kernels using Lemma 4.11.

Let $f:X\rightarrowtriangle Y$ and $g:Y\rightarrowtriangle Z$ two (proper)
probability kernels. Let $(x_{n})_{n\in\mathbb{N}}$ be a sequence in $X$ that
converge towards $x$. The well-known _portmanteau theorem_ for weak
convergence–see for instance Theorem 3.1 in (Ethier and Kurtz, 2009)–tells us
that a sequence of probability measures $(\mu_{n})_{n\in\mathbb{N}}$ over an
arbitrary metric space $S$ converges weakly towards $\mu$ when for every open
set $O\subseteq S$, $\liminf_{n\rightarrow\infty}\mu_{n}(O)\geq\mu(O)$. It
means that we can rewrite our goal as proving:

(6) $\forall O\text{ open in }Z,\quad\liminf_{n\rightarrow\infty}(g\circ
f)(x_{n},O)\geq(g\circ f)(x,O)$

Let $O$ be an open set in $Z$. Recall that by definition of kernel
composition, for every $a\in X$, $(g\circ f)(a,O)=\int_{y}g(y,O)\cdot
f(a,dy)$. By hypothesis $f$ is Feller continuous, thus the sequence of measure
$f(x_{n},\cdot)$ converge weakly towards $f(x,\cdot)$. Now, we use Proposition
1.4.18 in (Hernández-Lerma and Lasserre, 2012) that tells us that whenever a
sequence of probability measure $(\mu_{n})_{n\in\mathbb{N}}$ over an arbitrary
metric space $S$ converges weakly towards $\mu$, then for every function
$\alpha:S\rightarrow\mathbb{R}_{\geq 0}$ _lower semi-continuous (l.s.c.)_ ,
then $\liminf_{n\rightarrow\infty}\int\alpha\cdot d\mu_{n}\geq\int\alpha\cdot
d\mu$. Recall that l.s.c. means that for every $a\in S$,
$\liminf_{a_{n}\rightarrow a}\alpha(a_{n})\geq\alpha(a)$. We now consider the
function $\alpha_{O}:y\in Y\mapsto g(y,O)\in\mathbb{R}_{+}$: we can see using
the hypothesis on Feller continuity for $g$ that $\alpha_{O}$ is l.s.c.
Indeed, let $(y_{n})_{n\in\mathbb{N}}$ a sequence in $Y$ that converges
towards $y$:
$\liminf_{n\rightarrow\infty}\alpha_{O}(y_{n},O)=\liminf_{n\rightarrow\infty}g(y_{n},O)\geq
g(y,O)=\alpha_{O}(y,O)$, by the portmanteau theorem and since by hypothesis on
$g$ the sequence of measures $g(y_{n},\cdot)$ converge weakly towards
$g(y,\cdot)$. As a consequence, we can apply Proposition 1.4.18 in (Hernández-
Lerma and Lasserre, 2012) to $\alpha_{O}$, and we obtain:

$\liminf_{n\rightarrow\infty}\int_{y}\alpha_{O}(y)\cdot
f(x_{n},dy)\geq\int_{y}\alpha_{O}(y)\cdot f(x,dy),$

which is exactly (6), thus we can conclude.

Our goal is now to generalize the result to the case of sub-probability
kernels, using Lemma 4.11. Let $k:X\rightarrowtriangle Y$ and
$h:Y\rightarrowtriangle Z$ two sub-probability kernels. We can transform them
into proper probability kernel, by considering
$k_{\bot}:X_{\bot}\rightarrowtriangle Y_{\bot}$, defined as
$k_{\bot}(\bot)=\\{\bot^{1}\\}$, and for $x\in X$,
$k_{\bot}(x)=(k(x))_{\bot}$, and similarly for $h$. The first step is to check
that $h_{\bot}\circ k_{\bot}=(h\circ k)_{\bot}$: it is immediate. The second
step consists in proving that for every kernel $g:X\rightarrowtriangle Z$, $g$
is Feller if and only of $g_{\bot}$ is Feller:

  * •

Suppose that $g$ is Feller. Let $(x_{n}\rightarrow_{n\rightarrow\infty}x)$ a
convergence sequence in $X_{\bot}$. Observe that there are two possible cases:

    * –

either $x=\bot$, and there exists some $N$, such that for every $n\geq N$,
$x_{n}=\bot$: in that case, since the sequence is stationnary we obtain
immediately the result;

    * –

or $x\in X$, and then there exists some $N$, such that for every $n\geq N$,
$x_{n}\in X$: in that case for every $n\geq N$,
$g_{\bot}(x_{n})=g(x_{n})+(1-\int_{X}g(x_{n}))\cdot\\{\bot^{1}\\}=(g(x_{n}))_{\bot}$.
By hypothesis on $g$, we know that $g(x_{n})\rightarrow g(x)$ for the weak
topology. From there, we can apply Lemma 4.11, and we get that
$(g(x_{n}))_{\bot}\rightarrow(g(x))_{\bot}$, thus we can conclude.

  * •

Suppose now that $g_{\bot}$ is Feller continuous; our goal is to show that
also $g$ is Feller continuous. Let $(x_{n}\rightarrow_{n\rightarrow\infty}x)$
a convergence sequence in $X$, and $f:X\rightarrow\mathbb{R}$ a continuous
bounded function. We can see that for every $y\in X$, $\int_{Z}f\cdot
d(g(y))=\int_{Z_{\bot}}f^{\prime}\cdot d(g_{\bot}(y))$, where
$f^{\prime}:X_{\bot}\rightarrow\mathbb{R}$ is defined by $f^{\prime}(\bot)=0$,
and $f^{\prime}(z)=f(z)$ for $z\in X$. We see immediately that $f^{\prime}$ is
bounded, and by definition of the coproduct of Polish space, it is also
continuous. So we can apply the Feller hypothesis on $g_{\bot}$, and we obtain
the result.

By combining these two steps with composition of Feller-continuous probability
kernels, we obtain that also Feller continuous sub-probability kernels are
compositionnal. ∎

###  4.2. State and Event Bisimilarity Coincide for Feller-Continuous LMPs

###### Notation 4.13.

In this section, we fix a Feller continuous LMP $\mathcal{M}$ with
$\mathcal{A}$ as set of labels, and we fix $\mathcal{A}^{\mathbb{Q}}$ a
countably dense subset of $\mathcal{A}$ (such a dense subset always exists,
since Polish spaces are separable). We write $\mathcal{M}^{\mathbb{Q}}$ for
the LMP extracted from $\mathcal{M}$ by retaining only the actions in
$\mathcal{A}^{\mathbb{Q}}$. Observe that in the particular case of the LMP
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ — i.e. the applicative LMP for the
language $\Lambda_{\mathbf{P}}^{c}$ where all primitives are continuous — we
can for instance define $\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}^{\mathbb{Q}}$
as in Definition 3.20, but restricting to values built from rationals.

####  4.2.1. A Key Result from Optimal Transport

The proofs in this section will use in a crucial way a result coming from the
literature on _optimal transport_ (see (Villani, 2008) for an introduction). A
coupling $\omega\in\Omega(\mu,\nu)$ is said to be _optimal_ with respect to
some measurable cost function $c:X\times Y\rightarrow\mathbb{R}$ whenever it
maximizes the quantity $\int c\cdot d\omega$. The field of optimal transport
consists broadly in the study of such optimal couplings. For a Borel relation
$\mathcal{R}$, we can express the relator $\Theta$ from Definition 3.6, by
associating an appropriate cost function $c_{\mathcal{R}}$ to the relation
$\mathcal{R}$: then it holds that $\mu\Theta\mathcal{R}\nu$ if and only if the
cost of the optimal transport from $\mu$ to $\nu$ with respect to this cost
function is $0$. We will make the construction of $c_{\mathcal{R}}$ more
precise in the proof of Corollary 4.15. This caracterisation of $\Theta$ in
terms of optimal transport gives us a way to import results from this field.
In this section, the key result we use comes from (Villani, 2008), and is
stated in Theorem 4.14 below. It can be read as the stability of the operator
$\Theta$ from Definition 3.6 under weak convergence of measures.

###### Theorem 4.14 (from (Villani, 2008) ).

Let $X$ and $Y$ be standard Borel spaces, and let $c:X\times
Y\rightarrow\mathbb{R}$ be a real-valued bounded continuous cost function. Let
$(\mu_{k})_{k\in\mathbb{N}}$, and $(\nu_{k})_{k\in\mathbb{N}}$ be sequences of
probability measures on $X$ and $Y$ respectively. Assume that $\mu_{k}$
converges to $\mu$ (resp. $\nu_{k}$ converges to $\nu$) weakly. For each $k$,
let $\pi_{k}\in\Omega(\mu_{k},\nu_{k})$ be an optimal coupling with respect to
$c$. Then, there exists a coupling $\pi\in\Omega(\mu,\nu)$ such that, up to
extraction of a subsequence, the $\pi_{k}$ converges weakly to $\pi$, and
moreover $\pi$ is an optimal coupling.

###### Corollary 4.15.

Let $R$ be a relation on standard Borel spaces $X,Y$ such that $R$ is a closed
set. Let $(\mu_{n})_{n\in\mathbb{N}}$, and $(\nu_{n})_{n\in\mathbb{N}}$ be two
sequences of sub-distributions such that $(\mu_{n})_{n\in\mathbb{N}}$ and
$(\nu_{n})_{n\in\mathbb{N}}$ converge weakly towards $\mu$ and $\nu$
respectively, and moreover for every $n$, it holds that $\mu_{n}(\Theta
R)\nu_{n}$. Then $\mu(\Theta R)\nu$.

###### Proof.

Using Lemma 3.4 and Lemma 4.11, we see that we can suppose without loss of
generality that the $\mu_{n},\nu_{n}\ldots$ are proper distributions. We
define a bounded continuous function $c_{R}:X\times
Y\rightarrow\mathbb{R}_{\geq 0}$ such that $c_{R}$ is zero on $R$, and
strictly positive everywhere else. We take $c_{R}(z)=\inf\\{1\\}\cup\\{\lVert
z-w\rVert\mid w\in R\\}_{X\times Y}.$ Observe that this function is continuous
_because of_ the closeness of $R$. Since $\mu_{n}\Theta R\nu_{n}$, we know
that there exists a coupling $\pi_{n}$ of zero weight, i.e. such that
$\pi_{n}(X\times Y\setminus R)=0$ (observe that $R$, $(X\times Y\setminus
R)$,…are measureable, since $R$ is closed). From there, and since $c$ is
positive everywhere, zero on $R$ and bounded by $1$, we can see that:

(7) $0\leq\int_{X\times Y}c.d\pi_{n}\leq\pi_{n}(X\setminus R)=0$

From there, we can apply Theorem 4.14, and we see that there exists a coupling
$\pi\in\Pi(\mu,\nu)$ such that, up to extraction of a subsequence, the
$\pi_{k}$ converges weakly to $\pi$, and moreover $\pi$ is an optimal
coupling.

In order to conclude, it is enough to show that $\pi(X\setminus R)=0$. To do
that, we combine Equation (7) with the fact that the
$(\pi_{n})_{n\in\mathbb{N}}$ converge weakly towards $\pi$, and we obtain:

$0=\int_{X\times Y}c.d\pi_{n}=\int_{X\times Y}c.d\pi=\int_{X\times Y\setminus
R}c.d\pi.$

Since $c$ is non-negative, by Corollary 2.5.4 from (Bogachev and Ruas, 2007),
it holds that $c_{\mid{(X\times Y\setminus R)}}$ is $0$ $\pi$-almost
everywhere. Since $c$ is strictly positive on $(X\times Y)\setminus R$, we can
conclude that $\pi((X\times Y)\setminus R)=0$. ∎

####  4.2.2. Application to Feller-Continuous LMPs

We start with studying the bisimilarity landscape for the LMP
$\mathcal{M}^{\mathbb{Q}}$. First, since $\mathcal{A}^{\mathbb{Q}}$ is
countable, we see that event and state bisimilarity coincide on
$\mathcal{M}^{\mathbb{Q}}$ (by Theorem 3.16). From now on, we will denote this
relation $\sim^{\mathcal{M}^{\mathbb{Q}}}$, in order to emphasize that there
is no difference here between state and event bisimilarities. We now look at
how we can relate $\sim^{\mathcal{M}^{\mathbb{Q}}}$ to the state and event
bisimilarities on $\mathcal{M}$: our end goal is to use Feller continuity
constraints to show that all these relations coincide. The first step is to
show, using Corollary (4.15) and Feller continuity of $\mathcal{M}$, that the
topological closure of $\sim^{\mathcal{M}^{\mathbb{Q}}}$ is a state
bisimulation for $\mathcal{M}$, thus is contained into
$\sim^{\mathcal{M}}_{state}$.

###### Proposition 4.16.

The topological closure of $\sim^{\mathcal{M}^{\mathbb{Q}}}$ is a state
bisimulation for $\mathcal{M}$.

###### Proof.

We write $\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}}$ for the topological
closure of $\sim^{\mathcal{M}^{\mathbb{Q}}}$, i.e.,
$\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}}$ is the set of all pairs
$(x,y)\in\mathcal{S}\times\mathcal{S}$ such that there exists a
$(\sim^{\mathcal{M}^{\mathbb{Q}}})$-sequences $(x_{n},y_{n})_{n\in\mathbb{N}}$
with $x=\lim_{n\rightarrow\infty}x_{n}$, and
$y=\lim_{n\rightarrow\infty}y_{n}$. Let $s,t\in\mathcal{S}$ be such that
$s\sim^{\mathcal{M}^{\mathbb{Q}}}t$, and $a\in\mathcal{A}$. Our goal from here
is to show that for every $a\in\mathcal{A}$,
$h_{a}(s)\Gamma\mathcal{R}h_{a}(t)$. Let us first unfold our hypothesis:

  * 1.

Since $\mathcal{A}^{\mathbb{Q}}$ is dense in $\mathcal{A}$, there exists a
sequence $(a_{m})_{m\in\mathbb{N}}$ of $\mathcal{A}^{\mathbb{Q}}$ elements
such that $a_{m}\xrightarrow[n\rightarrow\infty]{}a$;

  * 2.

Since $\mathcal{M}$ is a Feller continuous LMP,
$x_{n}\xrightarrow[n\rightarrow\infty]{}{x}$,
$y_{n}\xrightarrow[n\rightarrow\infty]{}{y}$,
$a_{m}\xrightarrow[m\rightarrow\infty]{}{a}$ implies that: $\forall
m,h_{a_{m}}(x_{n})\xrightarrow[n\rightarrow\infty]{}{h_{a_{m}}(x)}$,
$h_{a_{m}}(y_{n})\xrightarrow[n\rightarrow\infty]{}{h_{a_{m}}(y)}$, and
$\forall
z\in\\{x,y\\},h_{a_{m}}(z)\xrightarrow[m\rightarrow\infty]{}{h_{a}(z)}$,
thanks to weak convergence;

  * 3.

For every $n\in\mathbb{N}$, since
$x_{n}\,\sim^{\mathcal{M}^{\mathbb{Q}}}\,y_{n}$, it holds that for every
$m\in\mathbb{N}$,
$h_{a_{m}}(x_{n})\,\Gamma{(\sim^{\mathcal{M}^{\mathbb{Q}}})}\,h_{a_{m}}(y_{n})$,
thus since $(\sim^{\mathcal{M}^{\mathbb{Q}}})$ is contained into its
topological closure–and by monotonicity of the $\Gamma$ operator, we have that
$h_{a_{m}}(x_{n})\,\Gamma{(\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}})}\,h_{a_{m}}(y_{n})$.

Recall that since $(\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}})$ is closed, it
is in particular Borel, thus we obtain by applying Theorem 3.8 that
${\Gamma{(\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}})}}={\Theta{(\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}})}}$.
From there (and again since $(\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}})$ is
closed), we can apply Corrollary 4.15: first we fix a $m$, and we make $n$
tends towards infinity, obtaining that
$h_{a_{m}}(x)\,\Gamma{(\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}})}\,h_{a_{m}}(y)$.
Now, since this is true for every $m$, we can apply once again Corrollary 4.15
by making $m$ tends toward infinity, and we obtain that
$h_{a}(x)\,\Gamma{(\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}})}\,h_{a}(y)$,
which ends the proof. ∎

We are now able to combine Proposition(4.16) with the logical caracterisation
of state bisimilarity for LMPs with countable labels (Proposition (3.16)) to
show a logical caracterisation of state bisimilarity for Feller LMPs.
Moreover, we obtain the aditional result that bisimilarity on Feller LMPs is a
Borel relation, which is not necessarily the case for bisimilarities on
arbitrary LMPs, as we will discuss in more details later in Section 6.

###### Theorem 4.17.

Let $\mathcal{M}$ is a Feller continuous LMP. Then it holds that
${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{logic}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{test}}}}}$,
and moreover the graph of these relations is a topological closed set, thus a
Borel set.

###### Proof.

Recall that we know already from the literature (see Theorem 3.17) that
${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}}\subseteq{\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{logic}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{test}}}}}$,
thus it is enough to show that
${\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{state}}}}}={\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}$.
The main tool here is Proposition 4.16: it tells us that the topological
closure of $\sim^{\mathcal{M}^{\mathbb{Q}}}$ is a state bisimulation on
$\mathcal{M}$. Recall that by definition,
$\sim_{\mathit{state}}^{\mathcal{M}}$ is the largest state bisimulation on
$\mathcal{M}$; it means that:

(8)
$\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}}\subseteq\sim_{\mathit{state}}^{\mathcal{M}}\subseteq{\stackrel{{\scriptstyle\mathcal{M}}}{{\sim_{\mathit{event}}}}}.$

We are now going to build an inclusion chain in the reverse direction. Since
$\mathcal{M}^{\mathbb{Q}}$ is an approximation of $\mathcal{M}$, we know that
$\sim_{\mathit{event}}^{\mathcal{M}}\,\subseteq\sim^{\mathcal{M}^{\mathbb{Q}}}$
(it can be deduced for instance from Lemma 3.19), and since
$\sim^{\mathcal{M}^{\mathbb{Q}}}$ is contained in its topological closure, it
holds that
$\sim^{\mathcal{M}^{\mathbb{Q}}}\subseteq\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}}$.
Summing up, we have:

(9)
$\sim_{event}^{\mathcal{M}}\,\subseteq\,\sim^{\mathcal{M}^{\mathbb{Q}}}\,\subseteq\,\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}}.$

Combining (8) and (9), we obtain that
$\sim_{\mathit{state}}^{\mathcal{M}}\,=\,\sim_{event}^{\mathcal{M}}\,=\,\sim^{\mathcal{M}^{\mathbb{Q}}}\,=\,\overline{\sim^{\mathcal{M}^{\mathbb{Q}}}},$
which ends the proof. ∎

##  5\. Full Abstraction for $\Lambda_{\mathbf{P}}^{c}$

In this section, we show that the operational semantics of
$\Lambda_{\mathbf{P}}^{c}$ is Feller continuous and prove, as a main
consequence of that, a powerful full abstraction theorem stating that all the
equivalences on $\Lambda_{\mathbf{P}}^{c}$ considered so far coincide. To
achieve such a goal, we rely on the characterization of terms as pre-terms
(Section 2) and show that the evaluation of any pair of programs
$M[\vec{\bm{r}}]$ and $M[\vec{\bm{s}}]$, (where $\vec{r}$ and $\vec{s}$ are
vectors of real numbers) is essentially the same, and only the reals _inside_
the output value change. Moreover, the reals produced in output by
$M[\vec{\bm{r}}]$ depend continuously from $\vec{r}$. To formally express this
idea, we define a _refinement_ of the evaluation semantics of Section 2 that
keeps track separately of the evolution of the program structure — which is
discrete — and of the evolution of the continuous data. As a consequence, such
a refinement needs to be a semantics on _pre-programs_ ; we call this
semantics the _modular semantics_ for pre-programs.

###### Notation 5.1.

To define the modular semantics, we use the following notation:

  * •

We define $\mathcal{E}_{k}=\\{(P,f)\mid P\text{ a pre-value with }p\text{
holes, }f:\mathbb{R}^{k}\rightarrowtriangle^{=}{\mathbb{R}^{p}}\text{ a Feller
continuous kernel}\\}$, for $k\in\mathbb{N}$.

  * •

If $P$ is a pre-term with $l_{P}$ holes and a free variable $x$ that occurs
$l_{x}$ times in $P$, and $V$ is a pre-value with $l_{V}$ holes, we write
$P[V/x]$ for the pre-term with $l_{P[V/x]}=l_{P}+l_{x}\cdot l_{V}$ holes,
obtained by doing the substitution and re-indexing the holes canonically to
obtain an increasing enumeration while reading the terms. We write
$\mathit{subst}_{[\cdot]}$ for the associated function
$\mathit{subst}^{[\cdot]}_{P,V}:\mathbb{R}^{l_{P}+l_{V}}\rightarrow\mathbb{R}^{l_{P[V/x]}}$;

  * •

Finally, recall that we write $\lambda$ for the uniform distribution on
$[0,1]$, and that given kernels $f$ and $g$ and a function
$\phi:\mathbb{R}^{n}\to\mathbb{R}^{m}$, we write $g\circ f$ for the
composition of $f$ and $g$ (in the category of kernels) and
$\overline{\phi}:\mathbb{R}^{n}\rightarrowtriangle^{=}\mathbb{R}^{m}$ for the
deterministic kernel associated to $\phi$.

###### Definition 5.2.

We define _modular approximation semantics_ as a function mapping a pre-term
$M$ with $k$ holes to a non-decreasing family $(\llbracket
M\rrbracket_{\star}^{(n)})_{n\in\mathbb{N}}$ of discrete sub-distributions
over $\mathcal{E}_{k}$. The definition, by induction on $n$, is in Figure 4.
Since $(\llbracket M\rrbracket_{\star}^{(n)})_{n\in\mathbb{N}}$ is a non-
decreasing family on $\Delta{(\mathcal{E}_{k})}$, it has a supremum, which is
also a discrete distribution over $\mathcal{E}_{k}$, that we note $\llbracket
M\rrbracket_{\star}$.

$\llbracket M\rrbracket_{\star}^{(0)}=\emptyset;\qquad\llbracket
V\rrbracket_{\star}^{(n+1)}=\\{(V,\overline{id})^{1}\\}\text{ for }V\text{
pre-
value};\qquad\llbracket\bm{\bm{f}}([]^{1},\ldots,[]^{n})\rrbracket_{\star}^{(n+1)}=\\{([],\overline{\bm{f}})^{1}\\};$

$\llbracket\mathbf{sample}\rrbracket_{\star}^{(n+1)}=\\{([],\overline{\lambda})^{1}\\};\qquad\llbracket\mathbf{unfold}\
\mathbf{fold}\ V\rrbracket_{\star}^{n+1}=\llbracket V\rrbracket_{\star}^{n};$

$\llbracket(\lambda x.P)V\rrbracket_{\star}^{(n+1)}=\sum_{(W,f)}\llbracket
P[x/V]\rrbracket^{(n)}_{\star}(W,f)\cdot\\{(W,f\circ\overline{\mathit{subst}^{[\cdot]{\cdot}}_{P,V}})^{1}\\};$

$\llbracket\mathbf{pm}\ \langle\hat{\imath},V\rangle\ \mathbf{as}\ \langle
i,x\rangle.M_{i}\rrbracket_{\star}^{n+1}=\sum_{(W,f)}\llbracket
M_{\hat{\imath}}[V/x]\rrbracket_{\star}^{n}(W,f)\cdot\\{(W,f\circ\overline{\mathit{subst}^{[\cdot]{\cdot}}_{M_{\hat{\imath}},V}})^{1}\\};$

$\displaystyle\llbracket\mathbf{let}\ x=N_{1}\ \mathbf{in}\
N_{2}\rrbracket_{\star}^{(n+1)}=$ $\displaystyle\sum_{(W_{1},f_{1})}\llbracket
N_{1}\rrbracket_{\star}^{(n)}(W_{1},f_{1})$
$\displaystyle\cdot\sum_{(W_{2},f_{2})}\llbracket
N_{2}[W_{1}/x]\rrbracket_{\star}^{(n)}(W_{2},f_{2})\cdot\\{(W_{2},f_{2}\circ\overline{\mathit{subst}^{[\cdot]{}}_{N_{2},W_{1}}}\circ(f_{1}\times
id))^{1}\\}.$

Figure 4. Modular Semantics for $\Lambda_{\mathbf{P}}^{c}$

Before proceeding any further, let us observe that we can characterize the
semantics of programs using our modular semantics on pre-terms.

###### Lemma 5.3.

For any pre-term $M$ with $p$ holes and $\vec{r}\in\mathbb{R}^{p}$, we have:

(10) $\displaystyle\forall n\in\mathbb{N},\llbracket
M[\vec{\bm{r}}]\rrbracket^{(n)}=\sum\llbracket
M\rrbracket^{(n)}_{\star}(V,f)\cdot V[\bm{f(\vec{r})}]$ (11)
$\displaystyle\llbracket M[\bm{\vec{r}}]\rrbracket=\sum\llbracket
M\rrbracket_{\star}(V,f)\cdot V[\bm{f(\vec{r})}]$

###### Proof.

We first show (10) by induction on $n$.

  * •

if $n=0$, the result holds;

  * •

we suppose that (10) is true for $n\in\mathbb{N}$. We then proceed by case
analysis on the syntax of $M$. We suppose that $M$ has $p$ holes.

    * –

if $M=V$ with $V$ a pre-value, then $\llbracket
M\rrbracket_{\star}^{(n+1)}=\\{(V,\overline{id})^{1}\\}$ and for every
$\vec{r}\in\mathbb{R}^{p}$, $\llbracket
M[\vec{r}]\rrbracket^{n+1}=\\{V[\vec{r}]^{1}\\}$. Since
$V[\overline{id}(\vec{r})]=V[\\{\vec{r}^{1}\\}]=\\{V[\vec{r}]^{1}\\}$, the
result holds;

    * –

if $M=\underline{F}([]^{1},\ldots,[]^{n})$ then $\llbracket
M\rrbracket_{\star}^{(n+1)})=\\{(W,\overline{F})^{1}\\}$ with $W=[]$. Let
$\vec{r}\in\mathbb{R}^{p}$: it holds that $\llbracket
M[\vec{r}]\rrbracket^{n+1}=F(\vec{r})$. Since
$W[\overline{F}(\vec{r})]=\\{F(\vec{r})^{1}\\}$, the result holds;

    * –

if $M=\text{sample}$, then $p=0$, and $\llbracket
M\rrbracket_{\star}^{(n+1)})=\\{(W,f)^{1}\\}$ with $W=[]$ and
$f=(\star\mapsto{\lambda})$. We see that $\llbracket M\rrbracket=\lambda$.
Moreover, $W[f]=\lambda$, thus the result holds;

    * –

if $M=(\lambda x.P)W$, then $p=p_{1}+p_{2}$, with $P$ a pre-term with $p_{1}$
holes, and $V$ a pre-value with $p_{2}$ holes. Let $l$ be the number of holes
for $P[W/x]$: the substitution implies uniquely a function
$\phi:\mathbb{R}^{p}\rightarrow\mathbb{R}^{l}$. Let
$\vec{r}=(\vec{r}_{1},\vec{r}_{2})\in\mathbb{R}^{p_{1}}\times\mathbb{R}^{p_{2}}$.
Observe that:

$\displaystyle\llbracket M[\vec{r}]\rrbracket^{n+1}$ $\displaystyle=\llbracket
P[\vec{r_{1}}][W[\vec{r_{2}}]/x]\rrbracket^{n}$
$\displaystyle=\llbracket(P[W/x])[\phi(\vec{r})]\rrbracket\text{ by definition
of }\phi$ $\displaystyle=\sum_{(V,f)}\llbracket
P[W/x]\rrbracket^{(n)}_{\star}(V,f)\cdot V[f(\phi(\vec{r}))]\text{ by
induction hypothesis}$ $\displaystyle=\sum_{(V,f)}\llbracket
P[W/x]\rrbracket^{(n)}_{\star}(V,f)\cdot V[(f\circ\phi)(\vec{r}))]$
$\displaystyle=\sum_{(V,f)}\llbracket
M\rrbracket^{(n+1)}_{\star}(V,f\circ\phi)\cdot V[(f\circ\phi)(\vec{r}))]\text{
by Definition~{}\ref{def:modular_approx_semantics}}$
$\displaystyle=\sum_{(V,g)}\llbracket M\rrbracket^{(n+1)}_{\star}(V,g)\cdot
V[g(\vec{r}))]\text{ since all }g\in\mathsf{supp}(\llbracket
M\rrbracket^{n+1})\text{ are of the form }f\circ\phi;$

so the result holds.

    * –

if $M=(\texttt{let }x=N_{1}\texttt{ in }N_{2})$, then let $p=p_{1}+p_{2}$ with
$N_{1}$ a pre-term with $p_{1}$ holes, and $N_{2}$ a pre-term with $p_{2}$
holes. Let
$\vec{r}=(\vec{r}_{1},\vec{r}_{2})\in\mathbb{R}^{p_{1}}\times\mathbb{R}^{p_{2}}$.
Observe that:

$\displaystyle\llbracket
M[\vec{r}]\rrbracket^{n+1}=(L\in\mathscr{V}\mapsto\llbracket
N_{2}[\vec{r}_{2}][L/x]\rrbracket)^{n}\circ\llbracket
N_{1}[\vec{r}_{1}]\rrbracket^{n}$
$\displaystyle=(L\in\mathscr{V}\mapsto\llbracket
N_{2}[\vec{r}_{2}][L/x]\rrbracket)^{n}\circ(\sum_{(V,f)}\llbracket
N_{1}\rrbracket_{\star}^{n}(V,f)\cdot V[f(\vec{r}_{1})])\text{ by induction
hypothesis};$ $\displaystyle=\sum_{(V,f)}\llbracket
N_{1}\rrbracket_{\star}^{n}(V,f)\cdot(L\in\mathscr{V}\mapsto\llbracket
N_{2}[\vec{r}_{2}][L/x]\rrbracket)^{n}\circ(V[f(\vec{r}_{1})])\text{ by
Lemma~{}\ref{lemma:addition_kernels}};$ $\displaystyle=\sum_{(V,f)}\llbracket
N_{1}\rrbracket_{\star}^{n}(V,f)\cdot(\vec{z}\mapsto\llbracket(N_{2}[\vec{r}_{2}])[V[\vec{z}]/x]\rrbracket)^{n}\circ(f(\vec{r}_{1}))\text{
by change of variable }$ $\displaystyle=\sum_{(V,f)}\llbracket
N_{1}\rrbracket_{\star}^{n}(V,f)\cdot(\vec{z}\mapsto\llbracket(N_{2}[V/x])[\phi_{V}(z,\vec{r}_{2})]\rrbracket^{n}\circ(f(\vec{r}_{1}))\text{
by definition of }\phi_{V}\text{in Def~{}\ref{def:modular_approx_semantics}}$
$\displaystyle=\sum_{(V,f)}\llbracket
N_{1}\rrbracket_{\star}^{n}(V,f)\cdot(\vec{z}\mapsto\left(\sum_{W,g}\llbracket
N_{2}[V/x]\rrbracket^{(n)}_{\star}(W,g)\cdot
W[g(\phi_{V}(z,\vec{r}_{2}))]\right))\circ(f(\vec{r}_{1}))\text{ by IH}$
$\displaystyle=\sum_{(V,f)}\llbracket
N_{1}\rrbracket_{\star}^{n}(V,f)\cdot\sum_{(W,g)}\llbracket
N_{2}[V/x]\rrbracket^{(n)}_{\star}(W,g)\cdot(\vec{z}\mapsto
W[g(\phi_{V}(z,\vec{r}_{2}))])\circ(f(\vec{r}_{1}))\text{ by
Lemma~{}\ref{lemma:addition_kernels}}$ $\displaystyle=\sum_{(V,f)}\llbracket
N_{1}\rrbracket_{\star}^{n}(V,f)\cdot\sum_{(W,g)}\llbracket
N_{2}[V/x]\rrbracket^{(n)}_{\star}(W,g)\cdot\left(((\vec{z}\mapsto W[z])\circ
h_{V,f,g})\right(\vec{r})$ $\displaystyle\qquad\qquad\qquad\text{ with
}h_{V,f,g}:\mathbb{R}^{p_{1}+p_{2}}\rightarrowtriangle\mathbb{R}^{l_{W}},h_{V,f,g}=g\circ\phi_{V}\circ(f,\overline{id}_{\mathbb{R}^{p_{2}}})$
$\displaystyle=\sum_{(V,f),(W,g)}\llbracket
M\rrbracket_{\star}^{(n+1)}(W,h_{V,f,g})\cdot W[h_{V,f,g}(\vec{r})]\text{ by
Definition~{}\ref{def:modular_approx_semantics}}$
$\displaystyle=\sum_{(V^{\prime},f^{\prime})}\llbracket
M\rrbracket_{\star}^{(n+1)}(V^{\prime},f^{\prime})\cdot
V^{\prime}[f(\vec{r})]\text{ since all
}(V^{\prime},f^{\prime})\in\mathsf{supp}(\llbracket
M\rrbracket_{\star}^{(n+1)})\text{ are of the form }(W,h_{V,f,g}),$

and that concludes the proof.

We now show (11) using (10):

$\displaystyle\llbracket M[\vec{r}]\rrbracket$
$\displaystyle=\sup_{n\in\mathbb{N}}\llbracket
M[\vec{r}]\rrbracket^{(n)}\quad\text{ by definition of the operational
semantics}$ $\displaystyle=\sup_{n\in\mathbb{N}}\sum_{(V,f)}\llbracket
M\rrbracket^{(n)}_{\star}(V,f)\cdot V[f(\vec{r})]\text{ by
}~{}\eqref{eq:approx_modular}$
$\displaystyle=\sum_{(V,f)}(\sup_{n\in\mathbb{N}}\llbracket
M\rrbracket^{(n)}_{\star}(V,f))\cdot V[f(\vec{r})]\text{ because
}\forall(V,f)\text{ the sequence }(\llbracket
M\rrbracket^{(n)}_{\star}(V,f))_{n\in\mathbb{N}}\text{ is non-decreasing}$
$\displaystyle=\sum_{(V,f)}(\llbracket M\rrbracket_{\star}(V,f))\cdot
V[f(\vec{r})]\text{ by definition of }\llbracket M\rrbracket_{\star}.$

∎

The notion of modular approximation semantics from Definition 5.2 has been
designed as a mean to express that the semantics of a program
$M[\vec{\bm{r}}]\in\Lambda_{\mathbf{P}}^{c}$ depends continuously on
$\vec{r}$. We are now able to show this formally.

###### Proposition 5.4.

Let $(M_{n})_{n\in\mathbb{N}}$ be a sequence of terms that converges towards
$M$. Then the sequence of distributions $(\llbracket
M_{n}\rrbracket)_{n\in\mathbb{N}}$ converges weakly towards $\llbracket
M\rrbracket$.

###### Proof.

Observe that the fact that $(M_{n})_{n\in\mathbb{N}}$ is a sequence of terms
that converges towards $M$ actually means that there exists a pre-term $N$
(with $k$ holes), a real-valued vector $\vec{r}\in\mathbb{R}^{k}$, and a
sequence $\vec{r_{n}}\in\mathbb{R}^{k}$ such that
$\vec{r_{n}}\rightarrow\vec{r}$ and $M=N[\vec{\bm{r}}]$,
$M_{n}=N[\vec{\bm{r}}_{n}].$ Consequently, to prove that $(\llbracket
M_{n}\rrbracket)_{n\in\mathbb{N}}$ converges weakly towards $\llbracket
M\rrbracket$, it is enough to prove the following: let
$g:\mathscr{V}\rightarrow\mathbb{R}$ be a bounded and continuous function and
$\epsilon>0$. Then, we need to show: $\exists N\in\mathbb{N},\forall n\geq
N,\lvert\int_{\mathscr{V}}g.d{\llbracket
N[\vec{\bm{r}}_{n}]\rrbracket}-\int_{\mathscr{V}}g.d{\llbracket
N[\vec{\bm{r}}]\rrbracket}\rvert\leq\epsilon.$ Using the equivalence between
semantics on programs and modular semantics on pre-programs given by Lemma
5.3, we see that:

$\displaystyle\left\lvert\int_{\mathscr{V}}g.d{\llbracket
N[\vec{\bm{r}}_{n}]\rrbracket}-\int_{\mathscr{V}}g.d{\llbracket
N\rrbracket[\vec{\bm{r}}]}\right\rvert$
$\displaystyle\qquad=\left\lvert\int_{\mathscr{V}}g.d{(\sum\llbracket
N\rrbracket_{\star}(V,f)\cdot
V[\bm{f(\vec{r_{n}})}])}-\int_{\mathscr{V}}g.d{(\sum\llbracket
N\rrbracket_{\star}(V,f)\cdot V[\bm{f(\vec{r})}])}\right\rvert$
$\displaystyle\qquad=\left\lvert\sum_{(V,f)\in\mathsf{supp}(\llbracket
N\rrbracket_{\star})}(\llbracket
N\rrbracket_{\star}(V,f)\cdot(\int_{\mathscr{V}}g.dV[\bm{f(\vec{r_{n}})}]-\int_{\mathscr{V}}g.dV[\bm{f(\vec{r})}])\right\rvert.$