Since $\llbracket N\rrbracket_{\star}$ is a _discrete_ sub-probability
distribution, there exists a finite set
$\mathcal{E}^{\prime}_{k}\subseteq\mathcal{E}_{k}$ such that $\llbracket
N\rrbracket_{\star}(\mathcal{E}_{k}\setminus\mathcal{E}^{\prime}_{k})\leq\epsilon/(2M)$.
From there, since $g$ is bounded by $M$, and both
$V[f(\vec{r_{n}})],V[f(\vec{r})]$ are probability measure, we see that:

$\displaystyle A$
$\displaystyle\leq\lvert\sum_{(V,f)\in\mathcal{E}^{\prime}_{k}}(\llbracket
N\rrbracket_{\star}(V,f)\cdot(\int_{\mathscr{V}}g.dV[f(\vec{r_{n}})]-\int_{\mathscr{V}}g.dV[f(\vec{r})])\rvert+\frac{\epsilon}{2}$

At that point, in order to conclude, it is enough to show that for every
$(V,f)$ in the finite set $\mathcal{E}^{\prime}_{k}$, it holds that
$\lvert\int_{\mathscr{V}}g.dV[f(\vec{r_{n}})]-\int_{\mathscr{V}}g.dV[f(\vec{r})])\rvert\rightarrow_{n\rightarrow\infty}0$.
Since by hypothesis $g$ is bounded continuous, it means that it is enough to
show that the probability kernel $K_{V,f}:=\vec{y}\in\mathbb{R}^{k}\mapsto
V[f(\vec{y})]\in\Delta^{=}{(\mathscr{V})}$ is Feller continuous. First,
observe that $K_{(V,f)}$ can be written as the composition of two probability
kernels: $K_{(V,f)}=I_{V}\circ f$, with
$I_{V}:\vec{z}\in\mathbb{R}^{p}\mapsto\\{V[\vec{z}]^{1}\\}$ (with $p$ the
number of holes in $V$). By hypothesis, the kernel $f$ is Feller continuous.
Moreover, $I_{V}$ also is Feller continuous, since the function
$z\in\mathbb{R}^{p}\mapsto V[\vec{z}]\in\mathscr{V}$ is continuous. From
there, we can conclude using Lemma 4.12 that $K_{(V,f)}$, as the composition
of two Feller continuous kernel, is also Feller continuous. ∎

Our goal now is to use Proposition 5.4 to show that
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ is a Feller LMP, in the sense of
Definition 4.4. That amounts to prove Feller continuity of two families of
kernels:
$h_{a}:\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$,
for $a\in\mathcal{A}_{\Lambda_{\mathbf{P}}^{c}}$; and
$\widehat{h}^{s}=(a\in\mathcal{A}_{\Lambda_{\mathbf{P}}^{c}})\times(A\in\Sigma_{\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}})\mapsto
h_{a}(s,A)$, for $s\in\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$.

We are now ready to show that all relevant kernels for the LMP
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ are Feller continuous. We do this
below in Lemma 5.5 and Lemma 5.6.

###### Lemma 5.5.

For every $a\in\mathcal{A}$, the kernel
$h_{a}:\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$
is Feller continuous.

###### Proof.

We present only the most interesting cases, the others can be found in the
long version of this paper, and are obtained by small variations on the proofs
below.

  * •

If $a=\text{eval}$, then the thesis directly follows from Proposition 5.4.

  * •

for $a=\sigma$ with $\sigma\in T$: Observe that
$h_{\sigma}=\text{id}^{\mathscr{V}_{\sigma}}\sqcup\text{id}^{\mathscr{T}_{\sigma}}\sqcup
0$, using the notation of Lemma 4.10. From Lemma 4.10, we see that it is
enough to show that both
$\text{id}^{\mathscr{V}_{\sigma}}:\mathscr{V}_{\sigma}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$
and
$\text{id}^{\mathscr{T}_{\sigma}}\mathscr{T}_{\sigma}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$
are Feller continuous. Since for every $\mu\in\Delta{(\mathscr{V}_{\sigma})}$,
$\text{id}^{\mathscr{T}_{\sigma}}(\mu)=\mu$, this is obviously the case.

  * •

If $a=V\in\mathscr{V}_{\sigma}$, then we observe that
$h_{V}=\bigsqcup_{\tau}h^{\sigma}_{V}\sqcup 0$, where
$h_{V}^{\sigma}:\mathscr{V}_{\sigma\to\tau}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$.
From Lemma 4.10, we see that it is enough to show that for every $\tau$, and
every $V\in\mathscr{V}_{\sigma}$, the kernel
$h_{V}^{\sigma}:\mathscr{V}_{\sigma\to\tau}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$
is Feller. Moreover, we see that $h_{V}^{\sigma}$ is deterministically
generated by the function
$\widehat{h}_{V}^{\sigma\to\tau}=W\in\mathscr{V}_{\sigma\to\tau}\mapsto
WV\in\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$. Looking at the topologies on
$\mathscr{V}_{\sigma}$ and $\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$, we see
immediately that $\widehat{h}_{V}^{\sigma}$ is a continuous function.

  * •

If $a=case(\hat{\imath})$, with $i\in I$. As above we can write $h_{a}$ as a
coproduct kernel, i.e. we split $\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$ as
$\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}=\bigsqcup_{{(\sigma_{j})}_{j\in
I}}\\{\hat{\imath}\\}\times\mathscr{V}_{\sigma_{i}}\sqcup Z$. Observe that
this splitting is indeed consistent with Definition 3.20, in the following
sense: if we start from the component $\mathscr{V}_{\sum\nolimits_{j\in
I}{\sigma_{j}}}$ from $\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$, then it is
itself defined–see Definition 2.3 as the disjoint union of components of the
form $\\{\hat{\jmath}\\}\times\mathscr{V}_{\sigma_{j}}$. From there, we can
write: $h_{a}=\bigsqcup_{{\mathcal{F}=(\sigma_{j})}_{j\in
I}}h_{\hat{\imath}}^{\mathcal{F}}\sqcup 0$, where
$h_{\hat{\imath}}^{\mathcal{F}}:\\{\hat{\imath}\\}\times\mathscr{V}_{\sigma_{i}}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$
is defined as $h_{\hat{\imath}}^{\mathcal{F}}(\hat{\imath},V)=\\{V^{1}\\}$.
From Lemma 4.10, we see that it is enough to show that
$h_{\hat{\imath}}^{\mathcal{F}}$ is Feller continuous. Then, we show easily
that $h_{\hat{\imath}}^{\mathcal{F}}$ is deterministically generated by a
continuous function, and we can conclude.

  * •

if $a=\text{unbox}$

  * •

If $a=\overset{\text{?}}{\leq}q$, then we first recall that we have 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$. Since all primitive functions are continuous, $op_{\leq}$
is continuous too. Let us split $\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$ as
$\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}=\mathscr{V}_{\mathbf{real}}\sqcup Z$,
and observe that $h_{a}=h_{a}^{\mathscr{V}_{\mathbf{real}}}\sqcup 0$. As
before, we apply Lemma 4.10, and we see that it is enough to show that
$h_{a}^{\mathscr{V}_{\mathbf{real}}}$ is Feller continuous. Recall that
$h_{a}^{\mathscr{V}_{\mathbf{real}}}(\bm{r})=p_{\leq}(r,q)\cdot\\{r^{1}\\}$
Let $(\mu_{n})_{n\in\mathbb{N}}$ be a sequence of measures over $\mathbb{R}$
that converges weakly towards $\mu$ and let
$f:\mathbb{R}\rightarrow\mathbb{R}$ be a bounded continuous function. Notice
that for every distribution $\nu$ over reals, we have:

(12)
$\int_{\mathbb{R}}fd(h_{a}^{\mathscr{V}_{\mathbf{real}}}(\nu))=\int_{\mathbb{R}}f\times
op_{\leq}(\cdot,q)d\nu.$

Since $op_{\leq}$ is bounded and continuous, we deduce from weak convergence
of $(\mu_{n})_{n\in\mathbb{N}}$ that $\int_{\mathbb{R}}f\times
op_{\leq}(\cdot,q)d\mu_{n}\rightarrow_{n\rightarrow\infty}\int_{\mathbb{R}}f\times
op_{\leq}(\cdot,q)d\mu$. By combining this with (12), we conclude that
$\int_{\mathbb{R}}fd(h_{a}^{\mathscr{V}_{\mathbf{real}}}(\mu_{n}))\rightarrow_{n\rightarrow\infty}\int_{\mathbb{R}}fd(h_{a}^{\mathscr{V}_{\mathbf{real}}}(\mu))$.
Since it is true for every bounded continuous function $f$, it means that
$h_{a}^{\mathscr{V}_{\mathbf{real}}}(\mu_{n})$ converges weakly towards
$h_{a}^{\mathscr{V}_{\mathbf{real}}}(\mu)$, and we can conclude from there.

∎

###### Lemma 5.6.

For every $s\in\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$, the kernel
$\widehat{h}_{s}:\mathcal{A}_{\Lambda_{\mathbf{P}}^{c}}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$
is Feller continuous.

###### Proof.

We do the proof by case analysis on $s$. We present the most interesting cases
only.

  * •

If $s=M$, with $M\in\mathscr{V}_{\sigma}$, then we split
$\mathcal{A}_{\Lambda_{\mathbf{P}}^{c}}$ as
$\mathcal{A}_{\Lambda_{\mathbf{P}}^{c}}=\\{\text{eval}\\}\sqcup\\{\sigma\\}\sqcup
Z$ (observe that this splitting is indeed consistent with Definition 3.20),
and we write:
$\widehat{h}_{s}=\widehat{h}_{s}^{\\{\text{eval}\\}}\sqcup\widehat{h}_{s}^{\\{\sigma\\}}\sqcup
Z$, with
$\widehat{h}_{s}^{\\{\text{eval}\\}}:\\{\text{eval}\\}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$
and
$\widehat{h}_{s}^{\\{\sigma\\}}:\\{\sigma\\}\rightarrowtriangle\mathcal{S}_{\Lambda_{\mathbf{P}}^{c}}$.
It is immediate that those two kernels are Feller, since they are defined on
one-point spaces, so we can conclude the thesis by Lemma 4.10.

  * •

if $s=\bm{r^{\prime}}$, we split $\mathcal{A}_{\Lambda_{\mathbf{P}}^{c}}$ as
$\mathcal{A}_{\Lambda_{\mathbf{P}}^{c}}=\sqcup_{q\in\mathbb{Q}}\\{(\bm{f}_{\leq
q})\\}\sqcup\\{\mathbf{real}\\}\sqcup Z$. Using Lemma 4.10, we can conclude.

  * •

If $s=W$, with $W$ of type $\sigma\to\tau$, then we see that using Lemma 4.10
as above, it is enough to show that the kernel
$\widehat{h}_{s}^{app}:V\in\mathscr{V}_{\sigma}\mapsto\\{WV^{1}\\}$ is Feller.
Observe that this kernel can be written as the deterministic kernel
$\overline{f}$, with $f(V)=WV$. Since $f$ is continuous, we can conclude the
thesis because kernels deterministically generated by a continuous function
are Feller continuous.

∎

From Lemma 5.5 and Lemma 5.6, we immediately obtain Feller continuity of the
applicative LMP for our continuous $\lambda$-calculus
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$:

###### Proposition 5.7.

$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ is Feller continuous.

Finally, combining Proposition 5.7 and Theorem 4.17, we obtain the main result
of this section: the _full abstraction theorem_. The latter states that all
notions of bisimilarity we consider coincide on
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$. Consequently, we obtain a
characterization of bisimilarity by means of tests, and we can then use such a
characterization to prove full abstraction of bisimilarity with respect to
context equivalence, this way showing that all the notions of equivalence on
$\Lambda_{\mathbf{P}}^{c}$ considered so far coincide.

###### Theorem 5.8 (Full Abstraction Theorem).

${\stackrel{{\scriptstyle\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}}}{{\sim_{\mathit{state}}}}}={\stackrel{{\scriptstyle\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}}}{{\sim_{\mathit{logic}}}}}={\stackrel{{\scriptstyle\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}}}{{\sim_{\mathit{event}}}}}={\stackrel{{\scriptstyle\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}}}{{\sim_{\mathit{test}}}}}={\stackrel{{\scriptstyle\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}}}{{\equiv_{\mathit{ctx}}}}}.$

###### Proof.

By Proposition 5.7 and Theorem 4.17, on
$\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ we have:
${\sim_{\mathit{state}}}=\sim_{\mathit{logic}}=\sim_{\mathit{event}}=\sim_{\mathit{test}}$.
The inclusion
${\stackrel{{\scriptstyle\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}}}{{\sim_{\mathit{state}}}}}\subseteq{\stackrel{{\scriptstyle\Lambda_{\mathbf{P}}^{c}}}{{\equiv_{\mathit{ctx}}}}}$
is obtained exactly as in the proof of soundness of applicative bisimilarity
for $\Lambda_{\mathbf{P}}$ (Dal Lago and Gavazzo, 2019) (recall that state
bisimilarity on $\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}$ corresponds to
applicative bisimilarity for $\Lambda_{\mathbf{P}}^{c}$ as defined by Dal Lago
and Gavazzo (2019)). To conclude the proof, we need to show that
${\stackrel{{\scriptstyle\Lambda_{\mathbf{P}}^{c}}}{{\equiv_{\mathit{ctx}}}}}\subseteq{\stackrel{{\scriptstyle\mathcal{M}_{\Lambda_{\mathbf{P}}^{c}}}}{{\sim_{test}}}}$.
The proof is based on the following construction: for every test
$\alpha\in\mathcal{T}$, we build by induction on $\alpha$ a pair of contexts
$(\mathfrak{C}^{\mathscr{V},\sigma}_{\alpha})$ and
$(\mathfrak{C}^{\mathscr{T},\sigma}_{\alpha})$ such that the following
invariant holds, for all values $V\in\mathscr{V}_{\sigma}$ and terms
$M\in\mathscr{T}_{\sigma}$.

$\displaystyle\text{Prob}(\alpha,(V,\sigma))=\llbracket{\mathfrak{C}^{\mathscr{V},\sigma}_{\alpha}}[V]\rrbracket(1)$
$\displaystyle,\quad\mathsf{supp}(\llbracket{\mathfrak{C}^{\mathscr{V},\sigma}_{\alpha}}[V]\rrbracket)\subseteq[0,1]$
$\displaystyle\text{Prob}(\alpha,(M,\sigma))=\llbracket{\mathfrak{C}^{\mathscr{T},\sigma}_{\alpha}}[M]\rrbracket(1)$
$\displaystyle,\quad\mathsf{supp}(\llbracket{\mathfrak{C}^{\mathscr{T},\sigma}_{\alpha}}[V]\rrbracket)\subseteq[0,1].$

The construction is similar to the one used in the proof of full abstraction
of bisimilarity for discrete probabilistic $\lambda$-calculi (Crubillé and Dal
Lago, 2014; Crubillé et al., 2015), the most interesting case now being the
one of $\alpha=\overset{\text{?}}{\leq}q\cdot\alpha^{\prime}$, with
$q\in\mathbb{Q}$. We take $\mathfrak{C}^{\mathcal{U},\sigma}_{\alpha}=\bm{0}$,
if $\sigma\neq\mathbf{real}$ or $\mathcal{U}\neq\mathscr{V}$; and
$\mathfrak{C}^{\mathcal{\mathscr{V}},\mathbf{real}}_{\alpha}=\bm{\mathit{op}_{\leq}}(\mathbf{sample},\bm{\mathit{op}_{\leq}}(q,[]))\bm{*}\mathfrak{C}^{\mathscr{V},\mathbf{real}}_{\alpha^{\prime}}[]$,
otherwise. We then see that when two programs $M,N$ of type $\sigma$ are
context equivalent, then they have the same probability of success for any
$\alpha\in\mathcal{T}$, and from there we can deduce that they are test
bisimilar. ∎

##  6\. Perspectives on the General Case

After having proved that continuity of the first-order functions implies
coincidence between the four notions of equivalence we have introduced in
Section 3, we go back to the general case, namely the one of
$\Lambda_{\mathbf{P}}$. The only difference with respect to
$\Lambda_{\mathbf{P}}^{c}$ is that first-order functions are not necessarily
continuous. This, as we are going to see, turns out to have very strong
consequences on the nature of coinductive relational reasoning. Before
proceeding further, let us consider an example, which very clearly shows where
the crux is.

###### Example 6.1.

Consider the following two programs:

$\displaystyle M:\quad\mathbf{let}\ x=\mathbf{sample}\ \mathbf{in}\ (\lambda
y.\mathbf{if}\,x=y\,\mathbf{then}\,1\,\mathbf{else}\,0)$ $\displaystyle
N:\quad\mathbf{let}\ x=\mathbf{sample}\ \mathbf{in}\ \lambda y.0.$

The programs $M$ and $N$ are contextually equivalent. The easiest way to prove
that is by going through a denotational semantics of $\Lambda_{\mathbf{P}}$.
Vákár et al. (2019) have recently introduced quasi-Borel domains and have
proved their adequacy as a denotational semantics for a Bayesian
$\lambda$-calculus with recursive types subsuming $\Lambda_{\mathbf{P}}$.
Quasi-Borel domains thus provides an adequate semantics for
$\Lambda_{\mathbf{P}}$ too, and one can show the denotational interpretations
of $M$ and $N$ to coincide.444 The proof of denotational equality of $M$ and
$N$ (and thus of their contextual equivalence) has been communicated to the
authors by Dario Stein based on previous work by Sabok et al. (2021). .  The
proof is done in the denotational model based on Quasi-Borel spaces, for a
monadic call-by-value probabilistic language. We can show that their proof
also holds for $\Lambda_{\mathbf{P}}$ by formalizing an embedding of
$\Lambda_{\mathbf{P}}$ into that language. As highlighted by Sabok et al.
(2021) relying on a connection with the privacy rule in $\nu$-calculus, the
equivalence between $M$ and $N$ can be understood from a security-oriented
viewpoint: we see the sampling of $x$ as the generation of a _private name_ —
or in cryptographic terms, a private key. Indeed, no adversary — i.e. external
context—can _a priori_ guess the private key $x$ with non-negligible
probability. On the other hand, are these programs also state bisimilar?
Actually, state bisimilarity of $M$ and $N$ seems very hard to prove. How,
then, about event bisimilarity?

###  6.1. Event Bisimulation is _Unsound_

We look now at programs $M$ and $N$ from Example 6.1 from the point of view of
event bisimulation. We are going to show that they are event bisimilar; to do
this we first need to present additional tools from (Danos et al., 2005).

###### Definition 6.2.

A $\pi$-system on $\mathcal{S}$ is a subset of $\mathcal{S}$ closed under
(finite) intersections and containing $\mathcal{S}$.

###### Lemma 6.3 (From (Danos et al., 2005)).

Let $\pi$ be a $\pi$-system. Then $\sigma(\pi)$ is an event bisimulation if
$\pi$ is _stabl.e_

###### Definition 6.4.

We note $L_{r}=\lambda
x.\mathbf{if}\,(x==r)\,\mathbf{then}\,1\,\mathbf{else}\,0$. We consider the
following $\pi$-system:

$\displaystyle\pi$
$\displaystyle:=\left\\{\mathcal{S},\emptyset,\\{M,N\\},\\{1\\},\\{0\\}\right\\}\cup\\{A_{r}\mid
r\in\mathbb{R}\\}\cup\\{B_{I}\mid I\subseteq\mathbb{R}\text{ finite set}\\}$
$\displaystyle A_{r}$ $\displaystyle:=\\{L_{r}\\}$ $\displaystyle B_{I}$
$\displaystyle:=\\{\lambda x.0\\}\cup\\{L_{r}\mid r\not\in I\\}$

We take $\Lambda$ as the $\sigma$-algebra generated by $\pi$.

###### Lemma 6.5.

$\pi$ is stable.

###### Proof.

We need to check that for every $A\in\Lambda$, $a\in\mathcal{A}$, and
$q\in[0,1[$, it holds that $\langle a\rangle_{q}{A}\in\pi$. Here, we give some
examples of $\langle a\rangle_{q}{A}$, And we can check that they are indeed
in $\pi$:

$\displaystyle\langle eval\rangle_{q}{A_{r}}=\emptyset;$ $\displaystyle\langle
eval\rangle_{q}{B_{I}}=\\{M,N\\};$ $\displaystyle\langle
r\rangle_{q}{\\{0\\}}=B_{\\{r\\}};$ $\displaystyle\langle
r\rangle_{q}{\\{1\\}}=A_{r}\ldots$

∎

###### Proposition 6.6.

The states $M$ and $N$ are _event bisimilar_.

###### Proof.

It can be directly obtained by combining Lemma 6.5 and Lemma 6.3. ∎

Using the testing characterization from Theorem 3.17, we can in fact show that
context equivalence is contained in event applicative bisimilarity.

###### Proposition 6.7.

${\equiv^{\mathit{ctx}}}\subseteq{\sim_{\mathit{event}}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}}}$.

###### Proof.

Recall that event bisimilarity is caracterised by tests, i.e.
${\sim_{\mathit{event}}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}}}={\sim_{\mathit{test}}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}}}$.
From there, the proof is done exactly as in the proof of Theorem (5.8), by
building for every test a context that emulates it. ∎

The problem with event bisimilarity, at least when spelled out for
$\Lambda_{\mathbf{P}}$, is that you simply become too coarse, thus unsound for
context equivalence. The problem here lies in the fact that programs can do
strictly more than what an “adversary” for event bisimilarity does: indeed
they can somehow perform _man-in-the-middle attacks_ ; by contrast once the
adversary from event bisimilarity has created two copies of a process, it
cannot make them _interact_ with each other. This is exploited in the
following example.

###### Example 6.8.

Let us consider the following two programs:

$\displaystyle M$ $\displaystyle:\quad\mathbf{let}\ x=\mathbf{sample}\
\mathbf{in}\ \lambda
y.((\mathbf{if}\,x=y\,\mathbf{then}\,1\,\mathbf{else}\,0)\oplus x)$
$\displaystyle N$ $\displaystyle:\quad\mathbf{let}\ x=\mathbf{sample}\
\mathbf{in}\ \lambda y.({0}\oplus x),$

where $\oplus$ is as in Example 2.1. The two programs first sample a real
number $x$, to be thought of as a private key. Then, with probability
$\frac{1}{2}$, they behave as the corresponding process of Example 6.1, but
with probability $\frac{1}{2}$ they just _reveal_ their secret key. It means
that a context, seen as an adversary, can perform the following attack: first,
it _initiates_ a session, which means that the process needs to choose its
secret key. Then the adversary creates two copies of the underlying process:
from there, it obtains with probability $\frac{1}{4}$ the original process of
Example 6.1, and the secret key, and it can conclude its attack by passing the
key to the process. Indeed, it turns out that $M$ and $N$ are not context
equivalent, and we can prove it by building a context that distinguishes them.
We take $C=(\lambda z.z(z1))[\,].$ To compute $\llbracket C[M]\rrbracket$ and
$\llbracket C[N]\rrbracket$, we the intermediate functions
$f_{M},f_{N}:\mathbb{R}\rightarrow\mathscr{V}$ defined thus:

$\displaystyle f_{M}(r)$ $\displaystyle:=\lambda
y.((\mathbf{if}\,r==y\,\mathbf{then}\,1\,\mathbf{else}\,0)\oplus r)$
$\displaystyle f_{N}(r)$ $\displaystyle:=\lambda y.(0\oplus r).$

This way, we have $\llbracket M\rrbracket(A)=\lambda\\{r\mid f_{M}(r)\in A\\}$
and $\llbracket N\rrbracket(A)=\lambda\\{r\mid f_{N}(r)\in A\\}$, where we
recall that $\lambda$ stands for the Lebesgue measure on $[0,1]$. For
$L\in\\{M,N\\}$, we thus have $\llbracket C[L]\rrbracket(A)=\int\llbracket
f_{L}(r)(f_{L}(r)1)\rrbracket(A)\lambda(dr)$. We need now to compute
$\llbracket f_{L}(r)(f_{L}(r)1)\rrbracket$ for $L\in\\{M,N\\}$: observe that
the probabilistic behavior here is purely _discrete_ :

$\displaystyle\llbracket f_{M}(r)1\rrbracket$
$\displaystyle=\frac{1}{2}\\{\delta_{1}(r)^{1}\\}+\frac{1}{2}\\{r^{1}\\},$
$\displaystyle\text{ }\llbracket f_{N}(r)1\rrbracket$
$\displaystyle=\frac{1}{2}\\{0^{1}\\}+\frac{1}{2}\\{r^{1}\\},$

with $\delta_{1}(r)=1$ if $r=1$, and $\delta_{1}(r)=0$ otherwise. From there,
we can show that

$\displaystyle\llbracket f_{M}(r)(f_{M}(r)1)\rrbracket$
$\displaystyle=\frac{1}{2}\\{r^{1}\\}+\frac{1}{4}\\{1^{1}\\}+\frac{1}{4}\\{\delta_{0,1}(r)^{1}\\}$
$\displaystyle\llbracket f_{N}(r)(f_{N}(r)1)\rrbracket$
$\displaystyle=\frac{1}{2}\\{0^{1}\\}+\frac{1}{2}\\{r^{1}\\},$

so that we can compute

$\displaystyle\llbracket C[M]\rrbracket$
$\displaystyle=\frac{1}{2}\lambda+\frac{1}{4}\\{1^{1}\\}+\frac{1}{4}\\{0^{1}\\}$
$\displaystyle\quad\llbracket C[N]\rrbracket$
$\displaystyle=\frac{1}{2}\lambda+\frac{1}{2}\\{0^{1}\\}.$

From there, it is enough to compose $C$ with a context $D$ that tests the
equality to $1$.

The programs $M,N$ of Example 6.8 are designed as a counter-example to the
soundness of event bisimilarity. We have shown in Example 6.8 that they are
not context _equivalent_ : now, we are going to show that they are event
_bisimilar_ , using our approximation Lemma 3.19.

###### Example 6.9.

Let $\mathscr{W}$ be any countable set of values. First, we define a
restriction of the LMP $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ from Definition
3.20: we keep the same state space, but we restrict the transitions to the
ones labelled by a countable restriction of
$\mathcal{A}_{\Lambda_{\mathbf{P}}}$, that depends on $\mathscr{W}$. More
formally, we take:

$\mathcal{M}^{\text{app}}_{\mathscr{W}}:=(\mathcal{S}_{\Lambda_{\mathbf{P}}},\mathcal{A}^{\text{app}}_{\mathscr{W}},\\{h_{a}\mid
a\in\mathcal{A}^{\text{app}}_{\mathscr{W}}\\}),$

where $\mathcal{A}^{\text{app}}_{\mathscr{W}}$ is the standard Borel space
defined by taking the restriction of $\mathcal{A}_{\Lambda_{\mathbf{P}}}$ to
the set
$T\cup\mathscr{W}\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}\\}$. We are going to show that the programs $M$ and
$N$ are bisimilar in each of the $\mathcal{M}^{\text{app}}_{\mathscr{W}}$ —
that have countable labels and analytical state spaces, thus state
bisimilarity and event bisimilarity coincide there (by Theorem 3.16). From
this point, we will be able to conclude by Lemma 3.19 that $M$ and $N$ are
also event bisimilar in $\mathcal{M}_{\Lambda_{\mathbf{P}}}$.

We write $\mathcal{R}_{\mathscr{W}}$ for the bisimilarity on
$\mathcal{M}^{\text{app}}_{\mathscr{W}}$. We define:
$S=\\{(M,N)\\}\cup\\{(\hat{f_{M}(r)},\hat{f_{N}(r)})\mid
r\in\mathbb{R},r\not\in\mathscr{W}\\}\cup\\{(r,r)\mid
r\in\mathbb{\mathbb{R}}\\},$ where
$f_{M},f_{N}:\mathbb{R}\rightarrow\mathscr{V}$ are defined thus:

$\displaystyle f_{M}(r)$ $\displaystyle:=\lambda
y.((\mathbf{if}\,r=y\,\mathbf{then}\,1\,\mathbf{else}\,0)\oplus r);$
$\displaystyle f_{N}(r)$ $\displaystyle:=\lambda y.(0\oplus r);$

and we show that the reflexive closure of $S$ — that we note $\mathcal{R}$ —
is a bisimulation. That is: for each $(a,b)\in S$ and action $\alpha$,
$a\rightarrow_{\alpha}\mu_{a}$, $b\rightarrow_{\alpha}\mu_{b}$ implies that
$\mu_{a}\Gamma\mathcal{R}\mu_{b}$.

  * •

Let $r\in\mathbb{R}$ such that $r\not\in\mathscr{W}$, and $\alpha$ be a
_relevant_ action for $(f_{M}(r),f_{N}(r))$. It means that $\alpha$ is an
applicative action with a value of real type, so is of the form
$r^{\prime}\in\mathbb{R}$ with $r^{\prime}\in\mathscr{W}$. Observe that in
particular, it means that $r^{\prime}\neq r$. So we need to show that
$\llbracket f_{M}(r)r^{\prime}\rrbracket\Gamma\mathcal{R}\llbracket
f_{N}(r)r^{\prime}\rrbracket$. Since we know that $r\neq r^{\prime}$, we can
see $\llbracket f_{M}(r)r^{\prime}\rrbracket=\llbracket
f_{N}(r)r^{\prime}\rrbracket=\frac{1}{2}\\{0^{1}\\}+\frac{1}{2}\\{r^{1}\\},$
which allows us—since $\mathcal{R}$ is reflexive—to immediately conclude that
$\llbracket f_{M}(r)r^{\prime}\rrbracket\Gamma\mathcal{R}\llbracket
f_{N}(r)r^{\prime}\rrbracket$.

  * •

We look now at the pair $(M,N)\in S$. The only relevant action there is the
eval action, so we can reformulate our goal as: $\llbracket
M\rrbracket\Gamma\mathcal{R}\llbracket N\rrbracket$. To do that, we consider
any $A\in\Sigma^{\text{app}}$ which is $\mathcal{R}$-closed. We need to show
that $\llbracket M\rrbracket(A)=\llbracket N\rrbracket(A)$. First, looking at
the operational semantics for $M$ and $N$ that we have computed in Example
6.8, we see that (notice that $\lambda(\mathscr{W})=0$):

$\displaystyle\llbracket M\rrbracket(A)$
$\displaystyle=\lambda\\{r\in\mathbb{R}\mid f_{M}(r)\in A\\}$
$\displaystyle=\lambda\\{r\in\mathbb{R}\setminus{\mathscr{W}}\mid f_{M}(r)\in
A\\}+\lambda\\{r\in\mathbb{R}\cap{\mathscr{W}}\mid f_{M}(r)\in A\\}$
$\displaystyle=\lambda\\{r\in\mathbb{R}\setminus{\mathscr{W}}\mid f_{M}(r)\in
A\\}\quad\text{ since }\lambda(\mathscr{W})=0$ and similarly:
$\displaystyle\llbracket N\rrbracket(A)$
$\displaystyle=\lambda\\{r\in\mathbb{R}\mid f_{N}(r)\in
A\\}=\lambda\\{r\in\mathbb{R}\setminus{\mathscr{W}}\mid f_{N}(r)\in A\\}$

Recall that $A$ is $R$-closed: it means that for any $r\in\mathscr{W}$,
$f_{M}(r)\in A$ if and only if $f_{N}(r)\in A$, thus
$\\{r\in\mathbb{R}\setminus{\mathscr{W}}\mid f_{M}(r)\in
A\\}=\\{r\in\mathbb{R}\setminus{\mathscr{W}}\mid f_{N}(r)\in A\\}$, which ends
the proof.

###### Theorem 6.10.

${\sim_{\mathit{event}}^{\mathcal{M}_{\Lambda_{\mathbf{P}}}}}\not\subseteq{\equiv^{\mathit{ctx}}}$.

###### Proof.

Directly from Example 6.8, Example 6.9, and our approximation Lemma 3.19. ∎

###  6.2. On Full Abstraction for State Bisimilarity

Unfortunately, $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ is _not_ one among the
LMPs to which the correspondence results from Section 3 can be applied.
Indeed, as we have just proved, logical equivalence, testing equivalence, and
event bisimilarity are in fact _not sound_. Completeness of applicative
bisimilarity was left as an open question in the work by Dal Lago and Gavazzo
(2019). We still cannot give a definite answer to that question, but some
further light on the subject can indeed be given.

###### Example 6.11.

Consider, once again, the programs $M$ and $N$ from Example 6.1. The relevant
fragment of the underlying LMPs is in Figure 5, call it $\mathcal{M}_{\mid}$.

$M$$N$$\lambda x.0$ $\lambda y.{\textbf{if }{(y=r)}}$ $\textbf{then }1\textbf{
else }0$ … $\lambda y.{\textbf{if }{(y=r^{\prime})}}$ $\textbf{then }1\textbf{
else }0$
…evaleval$0$$1$$r$$r^{\prime}$$r^{\prime\prime}$$r$$r^{\prime}$$r^{\prime\prime}$$r^{\prime}$$r$$r^{\prime\prime}$$=0$$=1$

Figure 5. The programs $M,N$: it holds that $M\not\sim_{\mathit{state}}N$,
$M\equiv^{\mathit{ctx}}N$, $M\sim_{\mathit{event}}N$.

Observe that $\mathcal{M}_{\mid}$ is a _stable fragment_ of
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$, in the sense that from every state $s$
in this fragment, the probability to end up again in this fragment after doing
any action $a$ is $1$. Clearly, this is only a fragment of the whole
applicative LMP, but _in this fragment_ , it is easy to show that $M$ and $N$
are not bisimilar. Let $\mathcal{R}$ be a bisimulation. We can first observe
easily that $(1,0)\not\in\mathcal{R}$. From there, we can see that for each
state of the form:

$L_{r}:\quad\lambda y.{\mathbf{if}\ {(y=r)}}\ \mathbf{then}\ 1\ \mathbf{else}\
0,$

it holds that $(L_{r},\lambda x.0)\not\in\mathcal{R}$: that is because the
action $a=r$ goes to $1$ with probability $1$ when starting from the state
$L_{r}$, and to $0$ with probability $0$ when starting from $\lambda x.0$.
Looking at Figure 5, we see that there are actually no other states in
$\mathcal{M}_{\mid}$ such that $(v,\lambda x.0)\in\mathcal{R}$. As a
corollary, the set $\\{\lambda x.0\\}$ is $\mathcal{R}$-closed. Since moreover
it is measureable, it means that $\\{\lambda x.0\\}\in\Sigma(\mathcal{R})$.
From there, we end the proof by contradiction. Suppose that $M\mathcal{R}N$.
We should have $h_{\text{eval}}(M,\\{\lambda
x.0\\})=h_{\mathit{eval}}(N,\\{\lambda x.0\\})$, but it is not the case since
$h_{\text{eval}}(M,\\{\lambda x.0\\})=0$, while $h_{\text{eval}}(N,\\{\lambda
x.0\\})=1$.

It should be noted that to show that $\\{\lambda x.0\\}$ is
$\mathcal{R}$-closed, we implicitely use the fact that there are no other
states in the LMP, which is not the case if we consider the whole applicative
LMP instead of just a fragment. In order to adapt the proof for the whole LMP,
we would need to show the existence of a $\mathcal{R}$-closed measurable set
$X$ that contains $\lambda x.0$, and not more that a negligible number of the
$L_{r}$. We were however not able to show or disprove the existence of such a
set $X$. A natural choice for $X$ could seem to be the
$\mathcal{R}$-equivalence class of $\lambda x.0$ instead of simply $\\{\lambda
x.0\\}$. However, while this set is indeed $\mathcal{R}$-closed, it is however
potentially not measurable. We can indeed show the existence of primitive
functions which makes the equivalence class of $\\{\lambda x.0\\}$ non
measurable .

It would be intuitively appealing to be able to say that whenever two states
are not bisimilar in a stable fragment, as in Example 6.11, then they are also
not bisimilar in the whole LMP. We call this property a _locality property_ :
it formalizes the philosophical requirement that whenever two processes in a
transition system are not equivalent, this should stay true when we add to the
global system some other processes that do not interact at all with the
original processes. From a more practical point of view, locality is appealing
too: a non-local relation on a LMP is indeed much less usable than a local
one, since no matter how simple are the processes we are really interested in,
we are forced to consider the whole LMP with an uncountable state space.

We can see, using its logical characterization, that this locality property
holds for $\sim_{\mathit{event}}$. Indeed, whether a formula $\phi$ holds for
some state $s$ does not depend on the behaviour of states independent from
$s$. By contrast, we are not able to show locality in general for
$\sim_{\mathit{state}}$ when both the states and the action space are standard
Borel; crucially we are not able to show it in the special case of the LMP
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$. We have not been able either to find a
concrete proof that locality does not hold for
$\mathcal{M}_{\Lambda_{\mathbf{P}}}$. The crux of the matter, as illustrated
in Example 6.11, is the definition of the relator $\Gamma$ from Definition
3.1. As mentioned in Definition 3.6, there exists an alternative notion of
relator $\Theta$ based on _couplings_ , that coincide with $\Gamma$ in the
restricted case of Borel relations (cf. Theorem 3.8). While the relation we
would obtain when replacing $\Gamma$ by $\Theta$ would be local, it is not
know whether it is transitive, and thus an equivalence. Moreover this new
state bisimilarity would not be complete, since it can be shown that it
distinguishes the two programs of Example 6.11.

###  6.3. Bounding Non-Measurability in Descriptive Set-Theory

For context equivalence, we can go beyond our negative non-measurability
result in Proposition 2.10, by using tools from descriptive set theory
(Kechris, 2012) to bound _how much_ non-measurable $\equiv^{\mathit{ctx}}$ is.
We can make the notion of non-measurability more precise relying on the so-
called projective hierarchy (Kechris, 2012) — the latter starting from Borel
sets, and defining bigger and bigger classes using projections and
complementation. More precisely, we can show that $\equiv^{\mathit{ctx}}$ is
in the class of _co-analytic_ sets, i.e. those that are defined as the
complementary of an _analytic_ set. All of that means that (the graph of)
context equivalence is in the first layer of the projective hierarchy.

###### Lemma 6.12.

The graph of ${\equiv^{\mathit{ctx}}}\subseteq\mathscr{P}\times\mathscr{P}$ is
a co-analytic set, and thus for every program $M$, the equivalence class of
$M$ by $\equiv^{\mathit{ctx}}$ is a co-analytic set.

###### Proof.

First, since the class of co-analytic sets is stable by countable union (see
(Kechris, 2012), Chapter 4), we see that it is sufficient to show that for
every type $\sigma$, $\equiv^{ctx}$ restricted to programs of type $\sigma$ is
co-analytic. Moreover, it holds that:

$\displaystyle\equiv^{ctx}_{\sigma}$
$\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)\\}$

We show the equation above in exactly the same way as for
$\Lambda_{\mathbf{P}}^{c}$ in the proof of Proposition 2.12. The class of co-
analytic sets is 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 co-analytic. As a first step,
observe that we can rewrite $S_{C,q}$ as the complementary of:

(13) $\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}$.
We can reformulate Equation 13 as saying that $\overline{S_{C,q}}$ is the
image of $A_{C,q}$ by the projection function from
$\mathbb{R}^{k}\times\mathscr{T}_{\sigma}\times\mathscr{T}_{\sigma}$ to
$\mathscr{T}_{\sigma}\times\mathscr{T}_{\sigma}$. In order to end the proof,
it is enough from there to show that $A_{C,q}$ is a Borel set: indeed it is
known that the projections of Borel sets are analytical (see (Kechris, 2012),
Exercise 14.3), and as soon as we know that $\overline{S_{C,q}}$ is
analytical, we can deduce that its complementary $S_{C,q}$ is co-analytical.
We now show that $A_{C,q}$ is a Borel set: to do that we write it 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\times g)$, where we define
the functions $f_{C}$, $g_{q}$ as follows:

$\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}.$

We defined the $\sigma$-algebra on $\mathscr{T}$ in such a way that the
syntaxical operations used in the definition of the terms grammar are all
measurable; as a consequence the function $f_{C}$, that can be decomposed
using such elementary operations, is measurable. Moreover, since we have shown
that the operational semantics $\llbracket\,\rrbracket$ is a Markov kernel, we
obtain as an immediate consequence that $g_{q}$ is measureable. As a
consequence, $h_{C,q}$ is also measurable, as composition and cartesian
products of measurable functions. From there, and since
$\\{(a,b)\in\mathbb{R}^{2}\mid a\neq b\\}$ is a Borel set, we obtain that
$A_{C,q}$ is a Borel set, so we can conclude. ∎

We can now ask what is the position of the other notions of equivalence
considered in this paper in the projective hierarchy: are their graphs
measurable? Co-analytical? Are they in some levels of the projective
hierarchy, at least? For event bisimilarity, we can show using its logical
characterization that the situation is the same as for context equivalence:
there exists a choice of primitive functions making (the graph of)
$\sim_{\mathit{event}}$ not measurable. Nonetheless, $\sim_{\mathit{event}}$
is co-analytic. For state bisimilarity, instead, things are more complicated:
as for event bisimilarity and contextual equivalence, we can show that there
exists a choice of primitive functions making $\sim_{\mathit{state}}$ not
measurable; but in contrast to co-analiticity of $\sim_{\mathit{event}}$, we
are unable to show that $\sim_{\mathit{state}}$ stays in some level of the
projective hierarchy.

###### Remark 6.13.

We could ask ourselves what is the mesurability status of the equivalence
class for $\sim_{\mathit{logic}}$, when we consider the logical equivalence on
the LMPs we use for $\Lambda_{P}$ programs. On the one hand, we can see that
it is _at least as complex_ as contextual equivalence, meaning that in the
same way that we were able to build a mesurable primitive function that make
the graph of $\equiv^{ctx}$ non-mesurable, the same primitive function makes
the graph of $\sim_{\mathit{logic}}$ non mesurable. It is because, whenever
two values $V,W$ are of type $\mathbf{real}\rightarrow\mathbf{real}$, we can
show that $V\equiv^{ctx}W$ if and only if $V\sim_{\mathit{logic}}W$. Indeed,
we obtain immediately the $\Leftarrow$ implication from our completeness
result Proposition 3.17. In the other direction, we see that for the type
$\mathbf{real}\rightarrow\mathbf{real}$, the formulas $\\{\langle
r\rangle_{q}{\langle=r^{\prime}\rangle_{1}{\top}}\mid
r,r^{\prime}\in\mathbb{R},q\in\mathbb{Q}\\}$ are enough to completely
caracterise context equivalence on values. As a consequence, and since we have
shown that the graph of context equivalence at this type
$\mathbf{real}\rightarrow\mathbf{real}$ is not Borel, the graph of
$\sim_{\mathit{logic}}$ is not a Borel set.

###### Lemma 6.14.

Let $(\mathcal{S},\mathcal{A},\\{h_{a}\mid a\in\mathcal{A}\\})$ be a
measurably labelled LMP, with moreover $\mathcal{S}$ and $\mathcal{A}$ polish
spaces equiped with their Borel $\sigma$-algebras. Then the graph of
$\sim_{\mathit{logic}}$ is a co-analytical subset of
$\mathscr{P}\times\mathscr{P}$.

###### Proof.

First, observe that since $\mathcal{A}$ is a polish space, we can write the
set of all formulas as a countable coproduct of polish space. Since polish
spaces are stable by countable coproduct, we can equipp the set of all
formulas $\mathcal{L}$ with the structure of a polish space. More precisely,
we can define pre-logical formula, that are to logical formula the same as
terms are to pre-terms, i.e. logical formulas with holes for actions. More
precisely, pre-logical formulas are generated by the grammar
$\psi\;::=\;\top\mid\psi_{1}\wedge\psi_{2}\mid\langle[]^{n}\rangle_{q}{\psi}$
with $n\in\mathbb{N}$, and we ask for aditional constraints that the holes
$[]^{1},\ldots[]^{n}$ appear in this order.

In order to do the proof, we first look at the set $\\{(\phi,s)\mid
s\in\llbracket\phi\rrbracket\\}\subseteq\mathcal{L}\times\mathcal{S}$. First,
we can show that for any pre-formula $\psi$, the set
$A_{\psi}:=\\{(\vec{a},s)\mid s\in\llbracket\psi[\vec{a}]\rrbracket\\}$ is a
Borel set: the proof is by induction of the size of $\psi$.

  * •

if $\psi=\top$, $A_{\psi}=\\{\star\\}\times\mathcal{S}$, where $\star$
represents the unique element of $\mathcal{A}^{0}$, and the result is
immediate;

  * •

if $\psi=\psi_{1}\wedge\psi_{2}$:
$A_{\psi}=\\{((\vec{a}_{1},\vec{a}_{2}),s)\mid(\vec{a}_{1},s)\in
A_{\psi_{1}}\wedge(\vec{a}_{2},s)\in A_{\psi_{2}}\\}$, and from there we can
conclude using the fact that Borel sets are stable by finite intersections;

  * •

if $\psi={\langle[]^{1}\rangle_{q}{\psi^{\prime}}}$: recall that
$\llbracket\psi[a_{1},\vec{a_{2}}]\rrbracket=\\{s\mid
h_{a_{1}}(s,\llbracket\psi^{\prime}[\vec{a}_{2}]\rrbracket)>q\\}$. Thus:

$A_{\psi}=\\{(a_{1},\vec{a}_{2},s)\mid
h_{a_{1}}(s,\llbracket\psi^{\prime}[\vec{a}_{2}]\rrbracket)>q\\}.$

By induction hypothesis, we know that $\\{\vec{a}_{2},t\mid
t\in\llbracket\psi^{\prime}[\vec{a}_{2}]\rrbracket\\}$ is a Borel set, i.e. a
measurable set. From there, and using (Kechris, 2012) 17.25, we can deduce
that the map
$u:(\vec{a}_{2},\mu)\in\mathcal{A}^{n}\times\Delta{(\mathcal{S})}\mapsto\mu(\psi^{\prime}[\vec{a_{2}}])\in\mathbb{R}$
is mesurable. We can now use the map $u$ by pre-composing it with the map
$v:(s,a)\in\mathcal{S}\times\mathcal{A}\mapsto
h_{a}(s)\in\Delta{(\mathcal{S})}$: since the LMP we consider is measurable
labelled, this map is measurable. Summing up, we obtain:

$A_{\psi}=((v\times id_{\mathcal{A}^{n}});u)^{-1}(]-\infty,q[),$

and since we have established measurability of $v$ and $u$, we obtain that
$A_{\psi}$ is Borel.

We now want to use this result to show that the graph of
$\sim_{\mathit{logic}}$ is co-analytical. To do that, we observe that
$\\{(s,t)\mid s\sim_{\mathit{logic}}t\\}=\cap_{\psi\text{ a pre-
formula}}\\{(s,t)\mid\forall\vec{a},(\vec{a},(s,t))\in B_{\psi}\\}$, where
$B_{\psi}=\\{\phi,s,t\mid(s,\phi)\in A_{\psi},(t,\phi)\in
A_{\psi})\\}\cup\\{\phi,s,t\mid(s,\phi)\not\in A_{\psi},(t,\phi)\not\in
A_{\psi})\\}$. By stability of measurable substes by finite unions and
complementation, we obtain that $B_{\psi}$ is a measurable subset of
$\mathcal{A}^{n}\times\mathcal{S}^{2}$. From there, we can use (as in our
proof of the same statement for context equivalence), that a universal
quantification over a Borel subset leads to a co-analytical space, and we can
conclude.

∎

##  7\. Related Work

Programming languages with continuous probabilistic choices and higher-order
functions have been the subject of numerous studies in the last ten years
(e.g. (Borgström et al., 2016; Staton et al., 2016; Ehrhard et al., 2018;
Vákár et al., 2019)). This, in particular, thanks to the potential
applications to Bayesian programming, which however require the presence of
conditioning operators, which we have not considered in this work. Program
equivalence for higher-order languages with continuous probabilities has been
studied mostly by means of denotational models, the latter being based on
nontrivial mathematical structures — such as quasi-Borel spaces and domains
(Staton et al., 2016; Staton, 2017; Vákár et al., 2019), and measurable cones
(Ehrhard et al., 2018) (in fact, measurable spaces do not form a closed
category (Aumann, 1961), and therefore they cannot provide an adequate
semantics for higher-order languages). In this line of research, the recent
work by Sabok et al. (2021) connecting probabilistic behaviours and name
generation greatly inspired us in finding the examples from Section 6.
Although all the aforementioned (denotational) semantics have been proved to
be adequate for languages similar to (and sometimes even more expressive than
(Vákár et al., 2019)) $\lambda_{\mathbf{P}}$, to the best of the authors’
knowledge full abstraction for such semantics is currently an open problem.

In contrast to the many results on denotationally-based program equivalence,
only few works have focused on operationally-based notions of program
equivalence. Among those, we mention the work by Wand et al. (2018) (see also
the work by Culpepper and Cobb (2017)), where full abstraction of suitable bi-
orthogonal logical relations on a stochastic $\lambda$-calculus with scoring
is proved, and the work by Dal Lago and Gavazzo (2019), where soundness of a
notion of applicative bisimilarity essentially coinciding with our notion of
state bisimilarity on $\mathcal{M}_{\Lambda_{\mathbf{P}}}$ is proved. Even if
fully abstract, bi-orthogonal logical relations have a high logical
complexity: to logically relate two programs one needs to execute such
programs inside arbitrary evaluation contexts. This makes bi-orthogonal
logical relations oftentimes not readily usable to prove equivalence between
programs. In contrast, the applicative bisimilarity by Dal Lago and Gavazzo
(2019) is a lightweight technique, although it is currently unknown whether it
is fully abstract.

Applicative bisimilarity (Abramsky, 1990) is, together with open bisimilarity
(Sangiorgi, 1994; Lassen, 1999, 2005), among the most effective and best
studied notions of coinductive equivalence for programming languages with
higher-order functions. Applicative bisimilarity has been studied for
different languages, including nondeterministic (Lassen, 1998; Ong, 1993) and
probabilistic (Dal Lago et al., 2014; Crubillé and Dal Lago, 2014; Dal Lago
and Gavazzo, 2019) languages, and, more generally, languages with algebraic
effects (Dal Lago et al., 2017a, 2020, b; Gavazzo, 2019). For all those
languages, applicative bisimilarity has been proved to be a sound technique
for contextual equivalence. Full-abstraction results, instead, are more
delicate. Even if applicative bisimilarity is known to be fully abstract in
presence of certain kinds of effects, there are effects for which full
abstraction fails, the prime example being nondeterminism (Lassen, 1998).
Applicative bisimilarity is also known to be unsound for specific (non-
algebraic) effects, such as local names (Koutavas et al., 2011). The case of
discrete probabilistic effects is among those for which full-abstraction
results are possible, at least when programs are evaluated following the call-
by-value discipline (Crubillé and Dal Lago, 2014). This is somehow surprising,
since in the case of $\lambda$-calculi with nondeterministic choice, this
correspondence no longer holds (Lassen, 1998). Probabilistic effects, in other
words, appear to somehow _lie in between_ determinism and nondeterminism. This
phenomenon can be read through the lenses provided by characterizations of
notions of bisimulation through _testing_ (Van Breugel et al., 2005; Larsen
and Skou, 1991). When one moves from discrete to continuous distributions the
situation changes. As already mentioned, applicative bisimilarity is sound in
presence of continuous probabilities (Dal Lago and Gavazzo, 2019), but full
abstraction is currently an open problem.

There is a large body of work on generalization of the classic notion of
probabilistic bisimilarity — and its logical and testing characterizations —
as defined by Larsen and Skou (1991) to the setting of continuous
distributions and LMPs (Panangaden, 2009). In particular, starting with the
seminal work by Blute et al. (1997); Desharnais et al. (2002, 1998), the
notions of state and event bisimilarity (Danos et al., 2005, 2006) (as well as
their metric counterparts (Desharnais et al., 1999, 2004)) have been proposed
as notions of equivalence for LMPs. In that respect, there is a vast
literature that investigates the characterization of the aforementioned
notions of bisimilarity through logic-based and testing-based notions (Van
Breugel et al., 2005; Danos et al., 2005, 2006; Fijalkow et al., 2017; Clerc
et al., 2019). Even if dealing with LMPs (and thus with uncountable state
spaces), all the aforementioned works consider LMPs with _countable_ actions,
and thus cannot be applied to the study of expressive higher-order languages,
such as the ones studied in this paper. As an exception to that, we mention
the work on bisimulation-based equivalences (and their characterizations) on
LMPs with _continuous time_ (Desharnais and Panangaden, 2003; Fijalkow et al.,
2017). There, the set of actions of the LMP is replaced with a suitable notion
of time, which usually have the cardinality of the continuum, and thus gives
something closer to the LMPs we use in this paper. It should remarked,
however, that even if one can in principle see time as a continuous set of
actions, the role played by these two notions is different, as different are
the goals and challenges one has when working with LMPs with continuous time
and with continuous actions.

##  8\. Conclusion

This paper studies the nature of coinductive relational reasoning in the
context of $\lambda$-calculi with continuous probabilistic choices.
Surprisingly, the well-known correspondence between logical, testing, and
bisimilarity equivalences is lost, with many equivalences turning out to be
unsound for contextual equivalence. This, despite the fact that the theory of
bisimilarity for probabilistic systems allows for a very smooth transition
from the discrete to the continuous case. The deep reason for this hiatus
comes from the fact that _uncountably_ many actions are around, and this
falsifies the characterization of bisimilarity by testing, namely the key step
towards full-abstraction.

More on the positive side, this paper introduces a new class of probabilistic
systems with uncountable actions in which the transition function is itself
continuous, in the sense of Feller. For such systems, surprisingly, it is once
again true that testing precisely characterizes bisimilarity, and this holds
for both state and event bisimilarity. The aforementioned result is put at
work in the context of a calculus in which real numbers can only be
manipulated through continuous functions. This way the result of full
abstraction is restored.

In this paper, we are _not_ concerned with evaluating the expressive power of
the thus obtained calculus, namely of ${\Lambda_{\mathbf{P}}^{c}}$. It is
clear that not allowing a flow of information from reals to other types of
data to happen — therefore preventing the value of any real number argument
from altering the control flow — is a very strong restriction. However, it is
not certain that this restriction is unacceptable, think for example at
Bayesian programming. Along the same lines, we may wonder whether the
${\Lambda_{\mathbf{P}}^{c}}$ _contexts_ are as powerful as the ones from
$\Lambda_{\mathbf{P}}$, i.e., whether two
${\Lambda_{\mathbf{P}}^{c}}$-programs that are context equivalent in
${\Lambda_{\mathbf{P}}^{c}}$ are still equivalent when we consider _all_ the
contexts in $\Lambda_{\mathbf{P}}$. Such a full abstraction property does not
seem to hold, since the higher-order nature of the considered languages could
make it possible for a $\Lambda_{\mathbf{P}}$ context $C$ to inject non-
continuity inside a program $M$ of ${\Lambda_{\mathbf{P}}^{c}}$. In any case,
a thorough investigation along these lines is outside the scope of this paper,
and left for future work.

## References

  * Abramsky (1990) Samson Abramsky.  The lazy lambda calculus.  In D. Turner, editor, _Research Topics in Functional Programming_ , pages 65–117. Addison Wesley, 1990.
  * Aumann (1961) Robert J. Aumann.  Borel structures for function spaces.  _Illinois Journal of Mathematics_ , 5(4):614 – 630, 1961.
  * Backhouse and Hoogendijk (1993) Roland Carl Backhouse and Paul F. Hoogendijk.  Elements of a relational theory of datatypes.  In _Formal Program Development - IFIP TC2/WG 2.1 State-of-the-Art Report_ , pages 7–42, 1993.
  * Barendregt (1984) H.P. Barendregt.  _The lambda calculus: its syntax and semantics_.  Studies in logic and the foundations of mathematics. North-Holland, 1984\.
  * Barr (1970) M. Barr.  Relational algebras.  _Lect. Notes Math._ , 137:39–55, 1970.
  * Beiglböck et al. (2009) Mathias Beiglböck, Christian Léonard, and Walter Schachermayer.  A general duality theorem for the monge–kantorovich transport problem.  _arXiv preprint arXiv:0911.4347_ , 2009.
  * Billingsley (1986) Patrick Billingsley.  _Probability and Measure_.  John Wiley and Sons, second edition, 1986.
  * Blount and Kouritzin (2010) Douglas Blount and Michael A Kouritzin.  On convergence determining and separating classes of functions.  _Stochastic processes and their applications_ , 120(10):1898–1907, 2010.
  * Blute et al. (1997) Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden.  Bisimulation for labelled markov processes.  In _Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997_ , pages 149–158. IEEE Computer Society, 1997.  doi: 10.1109/LICS.1997.614943.
  * Bogachev and Ruas (2007) Vladimir Igorevich Bogachev and Maria Aparecida Soares Ruas.  _Measure theory_ , volume 1.  Springer, 2007.
  * Borgström et al. (2016) Johannes Borgström, Ugo Dal Lago, Andrew D Gordon, and Marcin Szymczak.  A lambda-calculus foundation for universal probabilistic programming.  _ACM SIGPLAN Notices_ , 51(9):33–46, 2016.
  * Clerc et al. (2019) Florence Clerc, Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden.  Expressiveness of probabilistic modal logics: A gradual approach.  _Information and Computation_ , 267:145–163, 2019.
  * Crubillé and Dal Lago (2014) Raphaëlle Crubillé and Ugo Dal Lago.  On probabilistic applicative bisimulation and call-by-value $\lambda$-calculi.  In _Proc. of ESOP 2014_ , volume 8410 of _LNCS_ , pages 209–228. Springer, 2014.
  * Crubillé et al. (2015) Raphaëlle Crubillé, Ugo Dal Lago, Davide Sangiorgi, and Valeria Vignudelli.  On applicative similarity, sequentiality, and full abstraction.  In _Proc. of Symposium in Honor of Ernst-Rüdiger Olderog._ , volume 9360 of _LNCS_ , pages 65–82. Springer, 2015.
  * Culpepper and Cobb (2017) Ryan Culpepper and Andrew Cobb.  Contextual equivalence for probabilistic programs with continuous random variables and scoring.  In Hongseok Yang, editor, _Proc. of ESOP 2017_ , volume 10201 of _Lecture Notes in Computer Science_ , pages 368–392. Springer, 2017.  doi: 10.1007/978-3-662-54434-1“˙14.
  * Dal Lago et al. (2014) U. Dal Lago, D. Sangiorgi, and M. Alberti.  On coinductive equivalences for higher-order probabilistic functional programs.  In _Proc. of POPL 2014_ , pages 297–308, 2014.
  * Dal Lago and Gavazzo (2019) Ugo Dal Lago and Francesco Gavazzo.  On bisimilarity in lambda calculi with continuous probabilistic choice.  In _Proc. of MFPS 2019_ , pages 121–141, 2019.
  * Dal Lago et al. (2017a) Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy.  Effectful applicative bisimilarity: Monads, relators, and howe’s method.  In _Proc. of LICS 2017_ , pages 1–12. IEEE Computer Society, 2017a.
  * Dal Lago et al. (2017b) Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka.  Effectful applicative similarity for call-by-name lambda calculi.  In _Proc. of ICTCS 2017_ , pages 87–98, 2017b.
  * Dal Lago et al. (2020) Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka.  Effectful applicative similarity for call-by-name lambda calculi.  _Theor. Comput. Sci._ , 813:234–247, 2020.  doi: 10.1016/j.tcs.2019.12.025.
  * Danos et al. (2005) Vincent Danos, François Laviolette, Josée Desharnais, and Prakash Panangaden.  Almost sure bisimulation in labelled markov processes.  2005\.
  * Danos et al. (2006) Vincent Danos, Josée Desharnais, François Laviolette, and Prakash Panangaden.  Bisimulation and cocongruence for probabilistic systems.  _Information and Computation_ , 204(4):503–523, 2006.
  * Desharnais and Panangaden (2003) Josée Desharnais and Prakash Panangaden.  Continuous stochastic logic characterizes bisimulation of continuous-time markov processes.  _J. Log. Algebraic Methods Program._ , 56(1-2):99–115, 2003.  doi: 10.1016/S1567-8326(02)00068-1.
  * Desharnais et al. (1998) Josée Desharnais, Abbas Edalat, and Prakash Panangaden.  A logical characterization of bisimulation for labeled markov processes.  In _Proc. of LICS 1998_ , pages 478–487. IEEE Computer Society, 1998.  doi: 10.1109/LICS.1998.705681.
  * Desharnais et al. (1999) Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labeled markov systems.  In Jos C. M. Baeten and Sjouke Mauw, editors, _Proc. of CONCUR ’99_ , volume 1664 of _Lecture Notes in Computer Science_ , pages 258–273. Springer, 1999.  doi: 10.1007/3-540-48320-9“˙19.
  * Desharnais et al. (2002) Josée Desharnais, Abbas Edalat, and Prakash Panangaden.  Bisimulation for labelled markov processes.  _Inf. Comput._ , 179(2):163–193, 2002.  doi: 10.1006/inco.2001.2962.
  * Desharnais et al. (2004) Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labelled markov processes.  _Theor. Comput. Sci._ , 318(3):323–354, 2004\.  doi: 10.1016/j.tcs.2003.09.013.
  * Ehrhard et al. (2018) Thomas Ehrhard, Michele Pagani, and Christine Tasson.  Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming.  _Proc. ACM Program. Lang._ , 2(POPL):59:1–59:28, 2018.
  * Ethier and Kurtz (2009) Stewart N Ethier and Thomas G Kurtz.  _Markov processes: characterization and convergence_ , volume 282\.  John Wiley & Sons, 2009.
  * Fijalkow et al. (2017) Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden.  Expressiveness of probabilistic modal logics, revisited.  In _44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)_. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017\.
  * Gavazzo (2019) Francesco Gavazzo.  _Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. (Equivalences coinductives et métriques pour les langages d’ordre supérieur avec des effets algébriques)_.  PhD thesis, University of Bologna, Italy, 2019.
  * Giry (1982) Michèle Giry.  A categorical approach to probability theory.  In _Categorical Aspects of Topology and Analysis_ , pages 68–85. Springer Berlin Heidelberg, 1982.
  * Hernández-Lerma and Lasserre (2012) Onésimo Hernández-Lerma and Jean B Lasserre.  _Markov chains and invariant probabilities_ , volume 211.  Birkhäuser, 2012.
  * Katsumata and Sato (2015) Shin-ya Katsumata and Tetsuya Sato.  Codensity liftings of monads.  In _6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)_. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015.
  * Katsumata et al. (2018) Shin-ya Katsumata, Tetsuya Sato, and Tarmo Uustalu.  Codensity lifting of monads and its dual.  _Logical Methods in Computer Science_ , 14(4), 2018.
  * Kechris (2012) A. Kechris.  _Classical Descriptive Set Theory_.  Graduate Texts in Mathematics. Springer New York, 2012.
  * Kellerer (1984) Hans G Kellerer.  Duality theorems for marginal problems.  _Zeitschrift für Wahrscheinlichkeitstheorie und verwandte Gebiete_ , 67(4):399–432, 1984.
  * Kelly (2005) Gregory M. Kelly.  Basic concepts of enriched category theory.  _Reprints in Theory and Applications of Categories_ , (10):1–136, 2005.
  * Koutavas et al. (2011) Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii.  From applicative to environmental bisimulation.  In _Proc. of MFPS 2011_ , volume 276 of _Electronic Notes in Theoretical Computer Science_ , pages 215–235, 2011.
  * Larsen and Skou (1991) Kim Guldstrand Larsen and Arne Skou.  Bisimulation through probabilistic testing.  _Inf. Comput._ , 94(1):1–28, 1991.
  * Lassen (1999) Søren B. Lassen.  Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context.  _Electr. Notes Theor. Comput. Sci._ , 20:346–374, 1999\.
  * Lassen (2005) Søren B. Lassen.  Eager normal form bisimulation.  In _Proceedings of LICS 2005_ , pages 345–354, 2005.
  * Lassen (1998) Søren Lassen.  _Relational Reasoning about Functions and Nondeterminism_.  PhD dissertation, Aarhus University, 1998.  BRICS Dissertation Series BRICS DS-98-2.
  * Levy et al. (2003) Paul Blain Levy, John Power, and Hayo Thielecke.  Modelling environments in call-by-value programming languages.  _Inf. Comput._ , 185(2):182–210, 2003.  doi: 10.1016/S0890-5401(03)00088-9.
  * Manes and Arbib (1986) Ernest G. Manes and Michael A. Arbib.  _Algebraic Approaches to Program Ssemantics_.  Texts and Monographs in Computer Science. Springer, 1986.
  * Mislove et al. (2007) Michael W. Mislove, Dusko Pavlovic, and James Worrell.  Labelled markov processes as generalised stochastic relations.  _Electron. Notes Theor. Comput. Sci._ , 172:459–478, 2007\.  doi: 10.1016/j.entcs.2007.02.015.  URL https://doi.org/10.1016/j.entcs.2007.02.015.
  * Morris (1969) J. Morris.  _Lambda Calculus Models of Programming Languages_.  PhD thesis, MIT, 1969.
  * Ong (1993) C.-H. Luke Ong.  Non-determinism in a functional setting.  In _Proc. of LICS 1993_ , pages 275–286. IEEE Computer Society, 1993.
  * Ong (1988) C.H.L. Ong.  _The Lazy Lambda Calculus: An Investigation Into the Foundations of Functional Programming_.  University of London. Imperial College of Science and Technology, 1988\.
  * Panangaden (1999) Prakash Panangaden.  The category of markov kernels.  _Electron. Notes Theor. Comput. Sci._ , 22:171–187, 1999\.  doi: 10.1016/S1571-0661(05)80602-4.
  * Panangaden (2009) Prakash Panangaden.  _Labelled Markov Processes_.  Imperial College Press, 2009.
  * Parthasarathy (2005) Kalyanapuram Rangachari Parthasarathy.  _Probability measures on metric spaces_ , volume 352.  American Mathematical Soc., 2005.
  * Piotrowski (1985) Zbigniew Piotrowski.  Separate and joint continuity.  _Real Analysis Exchange_ , 11(2):293–322, 1985\.
  * Sabok et al. (2021) Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman.  Probabilistic programming semantics for name generation.  _Proc. ACM Program. Lang._ , 5(POPL):1–29, 2021.
  * Sangiorgi (1994) Davide Sangiorgi.  The lazy lambda calculus in a concurrency scenario.  _Inf. Comput._ , 111(1):120–153, 1994.
  * Staton (2017) Sam Staton.  Commutative semantics for probabilistic programming.  In Hongseok Yang, editor, _Proc. of ESOP 2017_ , volume 10201 of _Lecture Notes in Computer Science_ , pages 855–879. Springer, 2017.  doi: 10.1007/978-3-662-54434-1“˙32.
  * Staton et al. (2016) Sam Staton, Hongseok Yang, Frank D. Wood, Chris Heunen, and Ohad Kammar.  Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints.  In _Proc. of LICS ’16_ , pages 525–534, 2016.
  * Swart and Winter (2013) Jan Swart and Anita Winter.  Markov processes: Theory and examples.  2013\.  Course Notes.
  * Terraf (2011) Pedro Sánchez Terraf.  Unprovability of the logical characterization of bisimulation.  _Information and Computation_ , 209(7):1048–1056, 2011.
  * Vákár et al. (2019) Matthijs Vákár, Ohad Kammar, and Sam Staton.  A domain theory for statistical probabilistic programming.  _Proc. ACM Program. Lang._ , 3(POPL):36:1–36:29, 2019.
  * Van Breugel et al. (2005) Franck Van Breugel, Michael Mislove, Joël Ouaknin, and James Worrell.  Domain theory, testing and simulation for labelled markov processes.  _Theoretical Computer Science_ , 333(1-2):171–197, 2005.
  * van Breugel et al. (2005) Franck van Breugel, Michael W. Mislove, Joël Ouaknine, and James Worrell.  Domain theory, testing and simulation for labelled markov processes.  _Theor. Comput. Sci._ , 333(1-2):171–197, 2005\.  doi: 10.1016/j.tcs.2004.10.021.  URL https://doi.org/10.1016/j.tcs.2004.10.021.
  * Viglizzo (2005) Ignacio D. Viglizzo.  Final sequences and final coalgebras for measurable spaces.  In José Luiz Fiadeiro, Neil Harman, Markus Roggenbach, and Jan J. M. M. Rutten, editors, _Algebra and Coalgebra in Computer Science: First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005, Proceedings_ , volume 3629 of _Lecture Notes in Computer Science_ , pages 395–407. Springer, 2005.  doi: 10.1007/11548133“˙25.
  * Villani (2008) Cédric Villani.  _Optimal transport: old and new_ , volume 338.  Springer Science & Business Media, 2008.
  * Wand et al. (2018) Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, and Andrew Cobb.  Contextual equivalence for a probabilistic language with continuous random variables and recursion.  _Proc. ACM Program. Lang._ , 2(ICFP):87:1–87:30, 2018.  doi: 10.1145/3236782.