# The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic λ-Calculus

Simona Kašterović

Faculty of Technical Sciences, University of Novi Sad

Trg Dositeja Obradovića 6, 21000 Novi Sad, Serbia

http://imft.ftn.uns.ac.rs/~simona/

simona.k@uns.ac.rs

Michele Pagani

IRIF, University Paris Diderot - Paris 7, France

https://www.irif.fr/~michele/

pagani@irif.fr

## Abstract

We consider the notion of probabilistic applicative bisimilarity (PAB), recently introduced as a behavioural equivalence over a probabilistic extension of the untyped λ-calculus. Alberti, Dal Lago and Sangiorgi have shown that PAB is not fully abstract with respect to the context equivalence induced by the lazy call-by-name evaluation strategy. We prove that extending this calculus with a let-in operator allows for achieving the full abstraction. In particular, we recall Larsen and Skou's testing language, which is known to correspond with PAB, and we prove that every test is representable by a context of our calculus.

**2012 ACM Subject Classification** Theory of computation → Lambda calculus

**Keywords and phrases** probabilistic lambda calculus, bisimulation, Howe's technique, context equivalence, testing

**Digital Object Identifier** 10.4230/LIPIcs.FSCD.2019.26

**Acknowledgements** We wish to thank the anonymous reviewers for their valuable suggestions, helping us to improve the paper.

# 1 Introduction

We consider the probabilistic extension $\Lambda_{\oplus}$ of the untyped $\lambda$-calculus, obtained by adding a probabilistic choice primitive $M \oplus N$ representing a term evaluating to $M$ or $N$ with equal probability. This calculus provides a useful although quite simple framework for importing tools and results from the standard theory of the $\lambda$-calculus to probabilistic programming.

As well-known, the choice of an evaluation strategy for $\Lambda_{\oplus}$ plays a crucial role, even for strongly normalising terms. Consider a function $\lambda x.F$ applied to a probabilistic term $M \oplus N$: if we adopt a call-by-name policy, cbn by short, the whole term $M \oplus N$ would be passed to the calling parameter $x$ before actually performing the choice between $M$ and $N$, while in a call-by-value strategy, cbv by short, we first chose between $M$ and $N$ and then pass the value associated with this choice to $x$. If the evaluation of $F$ calls $n$ times the parameter $x$, then the cbn strategy performs $n$ independent choices between $M$ and $N$, while the cbv strategy copies $n$ times the result of one single choice. In linear logic semantics [11], this phenomenon can be described by precising that the application is a bilinear function in cbv (so $(\lambda x.F)(M \oplus N)$ is equivalent to $((\lambda x.F)M) \oplus ((\lambda x.F)N)$), while it is not linear in the argument position in cbn (see discussion at Example 3).

In probabilistic programming it is worthwhile to have a cbv operator even in a cbn language, as the most of the randomised algorithms need to sample from a distribution and passing to a sub-procedure the *value* of this sample rather than the *whole distribution*.

<figure><img src="image_1.png" /></figure>
26:2 $\Lambda_{\oplus}$ with Let-In Operator

Consider for example the randomised quicksort: this algorithm takes a pivot randomly from an array and it passes it to the partitioning procedure, which uses this pivot several times. The algorithm would be unsound if we allow to make different choices each time the partitioning procedure calls for the same pivot. In [10] the authors enrich the cbn probabilistic PCF with a *let-in* operator, restricted to the ground values, so that *let* $x = M \oplus N$ in *F* behaves like a cbv application of $\lambda x.F$ to $M \oplus N$. In a continuous framework this kind of operator is usually called *sampling* (e.g. [15]), but this is just a different terminology for the same computation mechanism: sampling a value from a distribution before passing it to a parameter.

Both calling policies (cbn and cbv) can be declined with a further attribute which is Abramsky's laziness [1]: a reduction strategy is *lazy* (sometimes called also *weak*) whenever it does not evaluate the body of a function, i.e. it does not reduce a $\beta$-redex under the scope of a $\lambda$-abstraction. This notion has been presented in order to provide a formal model of the evaluation mechanism of the lazy functional programming languages.

Two probabilistic programs are context equivalent if they have the same probability of converging to a value in all contexts. Of course, this notion depends on which reduction strategy has been chosen. The prototypical example of diverging term $\Omega \stackrel{\text{def}}{=} (\lambda x.xx)(\lambda x.xx)$ is context equivalent with $\lambda x.\Omega$ for a non-lazy strategy, while the two terms can be trivially distinguished by a lazy strategy as $\lambda x.\Omega$ is a value for such a reduction. Similarly, the term $(\lambda xy.y)\Omega$ is equivalent to $\Omega$ for cbv, but it is converging for the cbn policy (lazy or not), because the reduction step $(\lambda xy.y)\Omega \rightarrow \lambda y.y$ is admitted.

One of the major contribution of the already mentioned [1] has been to use the notion of bisimilarity in order to study the context equivalence of the lazy cbn $\lambda$-calculus. The idea is to consider a reduction strategy as a labelled transition system where the states and labels of the system are the $\lambda$-terms and a transition labelled by a term $P$ goes from a term $M$ to a value $M'$ whenever $M'$ is the result of evaluating the application $MP$. The benefit of this setting is to be able to transport into $\lambda$-calculus the whole theory of bisimilarity (called in [1] *applicative bisimilarity*) and its associated coinduction reasoning, which is one of the main tools for comparing processes in concurrency theory. Basically, two terms $M$ and $N$ are applicative bisimilar whenever their applications $MP$ and $NP$ are applicative bisimilar for any argument $P$. Abramsky proved that applicative bisimilarity is sound with respect to lazy cbn context equivalence (i.e. the former implies the latter), but it is not fully abstract (there are context equivalent terms that are not bisimilar).

Abramsky's applicative bisimilarity has been recently lifted to $\Lambda_{\oplus}$ by Dal Lago and his co-authors [3, 7]. The transition system becomes now a Markov Chain (here Definition 14) on the top of it one can define a notion of probabilistic applicative bisimilarity (PAB). The paper [7] considers a lazy cbn reduction strategy, while [3] focuses on the (lazy) cbv strategy. In both settings, PAB is proven sound with respect to the associated context equivalence, but, surprisingly, the cbv bisimilarity is also fully abstract, while the lazy cbn is not. Our paper shows that adding the *let-in* operator mentioned before is enough for recovering the full abstraction even for the lazy cbn.

Let us discuss more in detail the problem with the lazy cbn operation semantics. The two terms $\lambda xy.(x \oplus y)$ and $(\lambda xy.x) \oplus (\lambda xy.y)$ are context equivalent but not bisimilar (Example 7). The difference is between a process giving a value *allowing* two choices and a process giving two values *after* a choice (see Figure 4 to have a pictorial representation of the two processes). The cbn contexts are not able to discriminate such a subtle difference while bisimilarity does (Examples 16 and 23). In [3] the authors show a cbv context discriminating a variant of these two terms and they conjecture that a kind of sequencing operator can recover the full abstraction for the lazy cbn : our paper proves this conjecture.
<figure><img src="image_2.png" /><figcaption>Figure 1 Sketch of the main results in the paper, giving Corollary 28.</figcaption></figure>

The result is not surprising if compared to [3], however let us stress the contrast with the non-lazy cbn reduction strategy (i.e. the full head-reduction). We have already mentioned that [10] considers the cbn probabilistic PCF endowed with the *let-in* operator. The full abstraction result of probabilistic coherence spaces proved in [10] shows that the *let-in* operator does not change the context equivalence of probabilistic PCF, as this latter corresponds with the equality in probabilistic coherence spaces, regardless of the presence of the *let-in* in the language. Also, [2, 14] achieve a similar probabilistic coherence spaces full abstraction result for the untyped non-lazy cbn probabilistic λ-calculus without the *let-in* operator. These considerations show that the need of *let-in* operator for getting the full abstraction is due to the notion of *lazy* normal form rather than the call-by-name policy.

**Structure of the paper.** Section 2 defines $\Lambda_{\oplus,let}$, the lazy call-by-name probabilistic λ-calculus extended with the *let-in* operator. The operational semantics is given by a notion of big-step approximation, following [8]. An equivalent notion based on Markov chains could be given as in e.g. [9]. The context equivalence is defined by Equation (5) where what we observe is the probability of getting a value. Notice that the notion of *laziness* plays a crucial role here, since a value is a variable or just an abstraction and not a head-normal form, as it is the case instead in the non-lazy cbn considered in e.g. [2, 9, 13, 14].

Section 3 defines the probabilistic applicative bisimulation and the corresponding bisimilarity by considering $\Lambda_{\oplus,let}$ as a labelled Markov chain. The definitions and results of this section are an adaptation of the ones in [7]. The main result is the soundness of bisimilarity with respect to the context equivalence (Theorem 20), whose proof is based on Lemma 19 stating that the bisimilarity is a congruence. The proof of this lemma is quite technical but follows the same lines of [3, 4, 7], using Howe's lifting: we postpone the details in the Appendix. The last Section 4 achieves the converse of Theorem 20 by considering Larsen and Skou's testing language (Definition 21) which is well-known to induce an equivalence corresponding with probabilistic bisimilarity (Theorem 24). Lemma 25 states that any test can be represented by a context of $\Lambda_{\oplus,let}$ (here we are using in an essential way the presence of the *let-in* operator), so giving Theorem 27 and closing the circle (Corollary 28). Figure 1 sketches the main reasoning of the paper.
## 2 Preliminaries

In this section we introduce the syntax and operational semantics of $\Lambda_{\oplus, let}$.

### 2.1 Probabilistic Lambda Calculus $\Lambda_{\oplus, let}$

We present the probabilistic lambda calculus $\Lambda_{\oplus, let}$, that is the pure, untyped lambda calculus endowed with two new operators: a probabilistic binary sum operator $\oplus$, representing a fair choice and a let-in operator, simulating the call-by-value evaluation in a call-by-name calculus. The operational semantics of $\Lambda_{\oplus, let}$ is defined by a big-step approximation relation as in [8], we refer to this paper for more details. Given a countable set $X = \{x, y, z, \dots\}$ of variables, term expressions (terms) and values are generated by the following grammar:

$$ \begin{array}{l@{\qquad}l} \text{(values)} & V, W ::= x \mid \lambda x.M, \\ \text{(terms)} & M, N ::= V \mid MN \mid M \oplus N \mid \text{let } x = M \text{ in } N, \end{array} \qquad (1) $$

where $x \in X$. The set of all terms (resp. values) is denoted by $\Lambda_{\oplus, let}$ (resp. $\mathcal{V}_{\oplus, let}$) and is ranged over by capital Latin letters $M, N, \dots$, the letters $V, W$ being reserved for values. The set of free variables of a term $M$ is indicated as $FV(M)$ and is defined in the usual way. Given a finite set of variables $\Gamma = \{x_1, \dots, x_n\} \subseteq X$, $\Lambda_{\oplus, let}^{\Gamma}$ (resp. $\mathcal{V}_{\oplus, let}^{\Gamma}$) denotes the set of terms (resp. values) whose free variables are within $\Gamma$. A term $M$ is closed if $FV(M) = \emptyset$, or equivalently if $M \in \Lambda_{\oplus, let}^{\emptyset}$. The capture-avoiding substitution of $N$ for the free occurrences of $x$ in $M$ is denoted by $M\{N/x\}$.

**► Example 1.** Let us define some terms useful in the sequel. The identity $I \stackrel{\text{def}}{=} \lambda x.x$, the boolean projections $T \stackrel{\text{def}}{=} \lambda xy.x$ and $F \stackrel{\text{def}}{=} \lambda xy.y$ and the duplicator $\Delta \stackrel{\text{def}}{=} \lambda x.xx$, this latter giving the ever looping term $\Omega \stackrel{\text{def}}{=} \Delta\Delta$. The let-in operator allows for a call-by-value duplicator $\Delta^\ell \stackrel{\text{def}}{=} \lambda x.\text{let } x = x \text{ in } xx$ that will distribute over the probabilistic choice (see Example 3).

Because of the probabilistic operator $\oplus$, a closed term does not evaluate to a single value, but to a discrete distribution of possible outcomes, i.e. to a function assigning a probability to any value. More formally, a (value) distribution is a map $\mathcal{D} : \mathcal{V}_{\oplus, let}^{\emptyset} \to \mathbb{R}_{[0,1]}$ such that $\sum_{V \in \mathcal{V}_{\oplus, let}^{\emptyset}} \mathcal{D}(V) \le 1$. The set of all value distributions is denoted by $\mathcal{P}$. Given a value distribution $\mathcal{D}$, the set of all values to which $\mathcal{D}$ attributes a positive probability is denoted by $\mathcal{S}(\mathcal{D})$ and we will call it the support of $\mathcal{D}$. Note that value distributions do not necessarily sum to 1, this allowing to model the possibility of divergence (Example 5). We will use the abbreviation $\sum_{\mathcal{D}}$ to stand for $\sum_{V \in \mathcal{V}_{\oplus, let}^{\emptyset}} \mathcal{D}(V)$. The expression $p_1V_1 + \dots + p_nV_n$ denotes the distribution $\mathcal{D}$ with finite support $\{V_1, \dots, V_n\}$ such that $\mathcal{D}(V_i) = p_i$, for every $i \in \{1, \dots, n\}$. Note that $\sum_{\mathcal{D}} = \sum_{i=1}^n p_i$. In particular, 0 denotes the empty distribution and $V$ can denote both a value and the distribution having all of its mass on $V$.

The operational semantics of $\Lambda_{\oplus, let}$ is given in two steps. First, the derivation rules in Figure 2 inductively define a notion of big-step approximation relation $M \downarrow \mathcal{D}$ between a closed term $M$ and a finite value distribution $\mathcal{D}$. Then, the semantics $[[M]]$ of $M$ is given as:

$$ [[M]] = \sup\{\mathcal{D} : M \downarrow \mathcal{D}\}, \qquad (2) $$

according to the point-wise order over value distributions ($\mathcal{D} \le \mathcal{E}$ if and only if $\forall V, \mathcal{D}(V) \le \mathcal{E}(V)$). The lub in Equation (2) is well-defined since $\le$ is a directed-complete partial order and the set $\{\mathcal{D} : M \downarrow \mathcal{D}\}$ is countable and directed (for every $M \downarrow \mathcal{D}$ and $M \downarrow \mathcal{E}$, there exists a distribution $\mathcal{F} \ge \mathcal{D}, \mathcal{E}$ such that $M \downarrow \mathcal{F}$).
$$ \frac{\overline{M \downarrow 0} \qquad \overline{V \downarrow V} \qquad \frac{M \downarrow \mathcal{D} \qquad N \downarrow \mathcal{E}}{M \oplus N \downarrow \frac{1}{2} \cdot \mathcal{D} + \frac{1}{2} \cdot \mathcal{E}}}{MN \downarrow \sum_{\lambda x.P \in \mathcal{S}(\mathcal{D})} \mathcal{D}(\lambda x.P) \cdot \mathcal{E}_{P,N}} \qquad \frac{N \downarrow \mathcal{G} \qquad \{M\{V/x\} \downarrow \mathcal{H}_V\}_{V \in \mathcal{S}(\mathcal{G})}}{\text{let } x = N \text{ in } M \downarrow \sum_{V \in \mathcal{S}(\mathcal{G})} \mathcal{G}(V) \cdot \mathcal{H}_V} $$

Figure 2 Rules for the approximation relation $M \downarrow \mathcal{D}$, with $M \in \Lambda_{\oplus, \text{let}}^{\emptyset}$ and $\mathcal{D}$ a value distribution.

$$ \frac{\frac{\mathbf{I} \downarrow \mathbf{I} \qquad VV \downarrow 0}{\mathbf{I} \oplus VV \downarrow \frac{1}{2}\mathbf{I}}}{V \downarrow V \qquad \frac{V \downarrow V \qquad VV \downarrow \sum_{i=1}^{n-1} \frac{1}{2^i}\mathbf{I}}{V \downarrow V \qquad \mathbf{I} \oplus VV \downarrow \sum_{i=1}^{n} \frac{1}{2^i}\mathbf{I}}} \qquad \frac{V \downarrow V \qquad \mathbf{I} \oplus VV \downarrow \sum_{i=1}^{n} \frac{1}{2^i}\mathbf{I}}{VV \downarrow \sum_{i=1}^{n} \frac{1}{2^i}\mathbf{I}} $$

Figure 3 A derivation of the big-step approximation $VV \downarrow \sum_{i=1}^{n} \frac{1}{2^i} \mathbf{I}$ for $V = \lambda x.(\mathbf{I} \oplus xx)$.

Notice that the rules in Figure 2 implement a lazy call-by-name evaluation: they do not reduce within the body of an abstraction, and an application $(\lambda x.M)N$ is evaluated as $M\{N/x\}$ for any term $N$. However, the let-in operator follows a call-by-value policy: let $x = N$ in $M$ has the same semantics as $M\{N/x\}$ only when $N$ is a value.

**Example 2.** Consider the term $M \stackrel{\text{def}}{=} \Delta(\mathbf{T} \oplus \mathbf{F})$. One can easily check that the rules of Figure 2 allows to derive $M \downarrow \mathcal{D}$ for any $\mathcal{D} \in \{0, \frac{1}{2}\lambda y.(\mathbf{T} \oplus \mathbf{F}), \frac{1}{2}\mathbf{I}, \frac{1}{2}\lambda y.(\mathbf{T} \oplus \mathbf{F}) + \frac{1}{2}\mathbf{I}\}$. The latter distribution is the lub of this set and so it defines the semantics of $M$.

**Example 3.** Let us replace in Example 2 the duplicator $\Delta$ with its call-by-value variant $\Delta^\ell$ (Example 1). We have $\Delta^\ell(\mathbf{T} \oplus \mathbf{F}) \downarrow \mathcal{D}$ for any $\mathcal{D} \in \{0, \frac{1}{2}\lambda y.\mathbf{T}, \frac{1}{2}\mathbf{I}, \frac{1}{2}\lambda y.\mathbf{T} + \frac{1}{2}\mathbf{I}\}$, so $[\Delta^\ell(\mathbf{T} \oplus \mathbf{F})] = \frac{1}{2}\lambda y.\mathbf{T} + \frac{1}{2}\mathbf{I}$. Notice that $[\Delta^\ell(\mathbf{T} \oplus \mathbf{F})] = [\Delta^\ell\mathbf{T} \oplus \Delta^\ell\mathbf{F}] = [\Delta\mathbf{T} \oplus \Delta\mathbf{F}]$, while $[\Delta(\mathbf{T} \oplus \mathbf{F})] \neq [\Delta\mathbf{T} \oplus \Delta\mathbf{F}]$, as calculated in Example 2. Let us mention that this phenomenon is well enlightened by the linear logic encoding of the call-by-name application and the call-by-value one, the latter resulting in an operator linear both in the function and the argument position, while the former is linear only in the functional position [11].

**Remark 4.** In general, notice that the presence of the let-in operator allows for an encoding $(\cdot)^\bullet$ of the call-by-value $\lambda$-calculus into our language, commuting with abstraction and variables and mapping the call-by-value application to $(MN)^\bullet = \text{let } x = M^\bullet \text{ in let } y = N^\bullet \text{ in } xy$. However, our language contains much more terms than the image of this mapping, so the computational behaviour of the terms might not be preserved by $(\cdot)^\bullet$.

**Example 5.** The previous examples are about normalizing terms, in this framework meaning terms $M$ with semantics of total mass $\sum[M] = 1$ and such that there exists a unique finite derivation giving $M \downarrow [M]$. Standard non-converging $\lambda$-terms give partiality, as for example $[\Omega] = 0$, so $[\Omega \oplus \mathbf{I}] = \frac{1}{2}\mathbf{I}$. However, probabilistic $\lambda$-calculi allow for almost sure terminating terms, that is terms $M$ such that $\sum[M] = 1$ but there exists no finite derivation giving $M \downarrow [M]$. For example, consider the term $M \stackrel{\text{def}}{=} VV$, with $V \stackrel{\text{def}}{=} \lambda x.(\mathbf{I} \oplus xx)$: any finite approximation of $M$ gives a distribution bounded by $\sum_{i=1}^n \frac{1}{2^i}\mathbf{I}$ for some $n \ge 0$, as Figure 3 shows, but only the limit sum $\sup_n \sum_{i=1}^n \frac{1}{2^i}\mathbf{I}$ is equal to $[M] = \mathbf{I}$.
26:6 $\Lambda_{\oplus}$ with Let-In Operator

The following lemma states simple properties of the semantics that can be easily proved by continuity of $[[ ]]$ and induction over finite approximations (see e.g. [8] for details).

**Lemma 6 ([8]).** For any terms $M$ and $N$,

1. $[(\lambda x.M)N] = [M\{N/x\}]$.

2. $[M \oplus N] = \frac{1}{2}[M] + \frac{1}{2}[N]$.

## 2.2 Context Equivalence

One standard way of comparing term expressions is by observing their behaviours within programming contexts. A context of $\Lambda_{\oplus,let}$ is a term containing a unique hole $[\cdot]$, generated by the following grammar:

$$ C, D ::= [\cdot] | \lambda x.C \mid CM \mid MC \mid C \oplus M \mid M \oplus C \mid \text{let } x = C \text{ in } M \mid \text{let } x = M \text{ in } C \quad (3) $$

If $C$ is a context and $M$ is a $\Lambda_{\oplus,let}$-term, then $C[M]$ denotes a $\Lambda_{\oplus,let}$-term obtained by substituting the unique hole in $C$ with $M$ allowing the possible capture of free variables of $M$. We will work with closing contexts, that is contexts $C$ such that $C[M]$ is a closed term (where $M$ can be an open term). Thus, we want to keep track of the possible variables captured by filling a context hole. Given two finite sets of variables $\Gamma$, $\Delta$, we denote by $C\Lambda_{\oplus,let}^{(\Gamma;\Delta)}$ the set of contexts capturing the variables in $\Gamma$ of a term filling the hole but keeping free the variables in $\Delta$. So for example the context $\lambda x.\text{let } y = x \oplus z \text{ in } x[\cdot]$ belongs to $C\Lambda_{\oplus,let}^{(\{x,y\};\Delta)}$ for any $\Delta$ containing $z$.

In a probabilistic setting, the typical observation is the probability to converge to a value, so giving the following standard definition, for every $M, N \in \Lambda_{\oplus,let}^{\Gamma}$:

$$ M \leq N \text{ iff } \forall C \in \Lambda_{\oplus,let}^{(\Gamma;\emptyset)}, \sum [[C[M]]] \leq \sum [[C[N]]], \quad (\text{context preorder}) \quad (4) $$

$$ M \simeq N \text{ iff } \forall C \in \Lambda_{\oplus,let}^{(\Gamma;\emptyset)}, \sum [[C[M]]] = \sum [[C[N]]] \quad (\text{context equivalence}) \quad (5) $$

Notice that $M \simeq N$ is equivalent to $M \leq N$ and $N \leq M$.

**Example 7.** As mentioned in the Introduction, the terms $M \stackrel{\text{def}}{=} \lambda xy.(x \oplus y)$ and $N \stackrel{\text{def}}{=} (\lambda xy.x) \oplus (\lambda xy.y)$ are context equivalent in the call-by-name probabilistic $\lambda$-calculus without the let-in operator [7]. However, they can be discriminated in $\Lambda_{\oplus,let}$ by, e.g. the context $C \stackrel{\text{def}}{=} (\text{let } y = [\cdot] \text{ in } (\text{let } z_1 = y\mathbf{I}\Omega \text{ in } (\text{let } z_2 = y\mathbf{I}\Omega \text{ in } \mathbf{I}))$). In fact, by applying the rules of Figure 2, one gets: $\sum [[C[M]]] = \frac{1}{4}$ and $\sum [[C[N]]] = \frac{1}{2}$.

**Example 8.** The two duplicators $\Delta$ and $\Delta^\ell$ (Example 1) are not context equivalent, for example $C \stackrel{\text{def}}{=} [\cdot](\mathbf{I} \oplus \mathbf{\Omega})$ gives $\sum [[C[\Delta]]] = \frac{1}{4}$ while $\sum [[C[\Delta^\ell]]] = \frac{1}{2}$.

**Proposition 9.** Let $M, N \in \Lambda_{\oplus,let}^{\emptyset}$, if $[[M]] \leq [[N]]$ then $M \leq N$. So, $[[M]] = [[N]]$ implies $M \simeq N$.

**Proof.** First, notice that $[[M]] \leq [[N]]$ is equivalent to $\forall D, M \Downarrow D, \exists \mathcal{E} \supset D, N \Downarrow \mathcal{E}$. Then one proves, by structural induction on a context $C$ that $[[C(M)]] \leq [[C(N)]]$, whenever $[[M]] \leq [[N]]$. The delicate points are in the cases $C$ is an application or a let-in operator. $\quad$

**Example 10.** Thanks to Proposition 9, one can prove that quite different terms are indeed context equivalent, e.g. the term $VV$ in Example 5 is context equivalent to $\mathbf{I}$. However, not all context equivalent terms have the same semantics, as for example $\lambda x.(x \oplus x)$ and $\mathbf{I}$.

Proving in general that two terms are context equivalent is rather difficult because of the universal quantifier in Equation (5). For example, proving that $\lambda x.(x \oplus x)$ and $\mathbf{I}$ are context equivalent is not immediate. Various other tools are then used to prove context equivalence, as the bisimilarity and testing introduced in the next sections.
### 3 Probabilistic Applicative Bisimulation

We briefly recall and adapt to $\Lambda_{\oplus, let}$ the definitions of [7] about probabilistic applicative (bi)simulation. This notion mixes Larsen and Skou's definition of (bi)simulation for labelled Markov chains [12] with Abramsky's applicative (bi)simulation for the lazy call-by-name $\lambda$-calculus [1]. The core idea is to look at a closed term $M$ as a state of a transition system, a Markov chain in our setting, having two kinds of transitions. A “solipsistic” transition consisting in evaluating $M$ to a value $\lambda x.P$ (this transition being weighted by the probability $\llbracket M \rrbracket(\lambda x.P)$ of getting $\lambda x.P$ out of $M$) and an “interactive” transition consisting in feeding a value $\lambda x.P$ by a new term $N$ representing an input from the environment, so getting the term $P\{N/x\}$. We can then consider the notions of similarity and bisimilarity (resp. (6), (7)) over such probabilistic transition system. The benefit of this approach is to check program equivalence via an existential quantifier (see Equation (7)) rather than a universal one as in context equivalence (Equation (5)). The main result of this section is Theorem 20 stating that similarity implies context preorder. As a consequence we have that bisimilarity implies context equivalence. The key ingredient for achieving this result is to show that the similarity is a precongruence relation (Definition 18 and Lemma 19). The proof of Lemma 19 is quite technical but standard, see the Appendix and [7] for more details.

We start with the definition of a generic labelled Markov chain and following Larsen and Skou [12] we introduce the notions of a probabilistic simulation and bisimulation.

**Definition 11.** A labelled Markov chain is a triple $\mathcal{M} = (S, \mathcal{L}, P)$ where $S$ is a countable set of states, $\mathcal{L}$ is a set of labels (actions) and $P$ is a transition probability matrix, i.e. a function $P: S \times \mathcal{L} \times S \to \mathbb{R}_{[0,1]}$ satisfying the following condition: $\forall s \in S, \forall l \in \mathcal{L}, \sum_{t \in S} P(s, l, t) \le 1$.

Given a relation $\mathcal{R}, \mathcal{R}(X)$ denotes the image of the set $X$ under $\mathcal{R}$, namely the set $\{y \mid \exists x \in X \text{ such that } x\mathcal{R}y\}$. If $\mathcal{R}$ is an equivalence relation, then $S/\mathcal{R}$ stands for the set of all equivalence classes of $S$ modulo $\mathcal{R}$. The expression $P(s, l, X)$ stands for $\sum_{t \in X} P(s, l, t)$.

**Definition 12.** Let $(S, \mathcal{L}, P)$ be a labelled Markov chain and $\mathcal{R}$ be a relation over $S$:

- $\mathcal{R}$ is a probabilistic simulation if it is a preorder and $\forall (s,t) \in \mathcal{R}, \forall X \subseteq S, \forall l \in \mathcal{L}, P(s,l,X) \le P(t,l,\mathcal{R}(X))$.

- $\mathcal{R}$ is a probabilistic bisimulation if it is an equivalence and $\forall (s,t) \in \mathcal{R}, \forall E \in S/\mathcal{R}, \forall l \in \mathcal{L}, P(s,l,E) = P(t,l,E)$.

We define the probabilistic (bi)similarity, denoted respectively by $\leq$ and $\approx$, as the union of all probabilistic (bi)simulations which can be proven to be still a (bi)simulation:

$$M \leq N \text{ iff } \exists \mathcal{R} \text{ probabilistic simulation s.t. } MRN, \quad (\text{probabilistic similarity}) \quad (6)$$

$$M \sim N \text{ iff } \exists \mathcal{R} \text{ probabilistic bisimulation s.t. } MRN \quad (\text{probabilistic bisimilarity}) \quad (7)$$

One can prove that $M \sim N$ is equivalent to $M \leq N$ and $N \leq M$, i.e. $\sim = \leq \cap \leq^{op}$.

**Definition 13.** For every closed value $V = \lambda x.N \in \Lambda_{\oplus, let}^{\emptyset}$ a distinguished value is indicated as $\tilde{V} = \nu x.N$ and belongs to the set $\forall \Lambda_{\oplus, let}^{\emptyset}$.

As an example, value $\lambda xy.x$ belongs to the set $\Lambda_{\oplus, let}^{\emptyset}$, while the distinguished value $\nu x.\lambda y.x$ is the element of $\forall \Lambda_{\oplus, let}^{\emptyset}$. As previously stated, we want to see the operational semantics of $\Lambda_{\oplus, let}$ as a labelled Markov chain defined as follows:
26:8 $\Lambda_{\oplus}$ with Let-In Operator

**► Definition 14.** The $\Lambda_{\oplus, let}$-Markov chain is defined as the triple $(\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset}, \Lambda_{\oplus, let}^{\emptyset} \cup \{\tau\}, P)$, where the set of states is the disjoint union of the set of closed terms and the set of closed distinguished values, labels (actions) are either closed terms or $\tau$ action and the transition probability matrix $P$ is defined in the following way:

- for every closed term $M$ and distinguished value $\nu x.N$,

$$P(M, \tau, \nu x.N) = [M](\lambda x.N),$$

- for every closed term $M$ and distinguished value $\nu x.N$,

$$P(\nu x.N, M, N\{M/x\}) = 1,$$

- in all other cases, $P$ returns 0.

For technical reasons the set of states is represented as a disjoint union $\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset}$.

Since $\Lambda_{\oplus, let}$ can be seen as a labelled Markov chain, the simulation and bisimulation can be defined as for any labelled Markov chain. A probabilistic applicative simulation is a probabilistic simulation on $\Lambda_{\oplus, let}$ and a probabilistic applicative bisimulation is a probabilistic bisimulation on $\Lambda_{\oplus, let}$. Then, the probabilistic applicative similarity, PAS for short, and the probabilistic applicative bisimilarity, PAB for short, are defined in the usual way applying Equation (6) and (7). From now on, the symbol $\lesssim$ (resp. $\sim$) will denote the probabilistic applicative similarity (resp. bisimilarity).

The notions of PAS and PAB are defined on closed terms, and we extend these definitions to open terms by requiring the usual closure under substitutions. Let $M, N \in \Lambda_{\oplus, let}^{\Gamma}$ where $\Gamma = \{x_1, \dots, x_n\}$. We say $M$ and $N$ are similar, (denoted $M \lesssim N$), if for all $L_1 \in \Lambda_{\oplus, let}^{\emptyset}, \dots, L_n \in \Lambda_{\oplus, let}^{\emptyset}, M\{L_1/x_1, \dots, L_n/x_n\} \lesssim N\{L_1/x_1, \dots, L_n/x_n\}$. The analogous terminology is introduced for bisimilarity.

**► Example 15.** Let us recall the terms $\lambda x.(x \oplus x)$ and $\lambda x.x$ from Example 10 having different semantics but context equivalent. As mentioned, the proof of their context equivalence is not immediate, because of the universal quantifier in Equation (5). However, we can check easily that they are bisimilar, because we need just to exhibit a bisimulation relation between the two terms. By Theorem 20 we then infer context equivalence from bisimilarity. Let us define the relation $\mathcal{R} = \{(\lambda x.(x \oplus x), \lambda x.x)\} \cup \{(\lambda x.x, \lambda x.(x \oplus x))\} \cup \{(\nu x.(x \oplus x), \nu x.x)\} \cup \{(\nu x.x, \nu x.(x \oplus x))\} \cup \{(N \oplus N, N) \mid N \in \Lambda_{\oplus, let}^{\emptyset}\} \cup \{(N, N \oplus N) \mid N \in \Lambda_{\oplus, let}^{\emptyset}\} \cup \{(M, M) \mid M \in \Lambda_{\oplus, let}^{\emptyset}\} \cup \{(\tilde{V}, \tilde{V}) \mid \tilde{V} \in \Lambda_{\oplus, let}^{\emptyset}\}$. We prove that $\mathcal{R}$ is a bisimulation containing $(\lambda x.(x \oplus x), \lambda x.x)$. The relation is trivially an equivalence, so we have to show that $\forall (M, N) \in \mathcal{R}, \forall E \in (\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset})/\mathcal{R}, \forall \ell \in \Lambda_{\oplus, let}^{\emptyset} \cup \{\tau\}, P(M, \ell, E) = P(N, \ell, E)$ (Definition 12). We prove only for $(\lambda x.(x \oplus x), \lambda x.x) \in \mathcal{R}, (\nu x.(x \oplus x), \nu x.x) \in \mathcal{R}$ and $(N \oplus N, N) \in \mathcal{R}$. First we have that $(\lambda x.(x \oplus x), \lambda x.x) \in \mathcal{R}$ and for all closed terms $F \in \Lambda_{\oplus, let}^{\emptyset}$ and all equivalence classes $E \in (\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset})/\mathcal{R}, P(\lambda x.(x \oplus x), F, E) = 0 = P(\lambda x.x, F, E)$ holds by Definition 14. If the equivalence class $E$ contains $\nu x.(x \oplus x)$ then $P(\lambda x.(x \oplus x), \tau, E) = 1$, otherwise $P(\lambda x.(x \oplus x), \tau, E) = 0$. Since $(\nu x.(x \oplus x), \nu x.x) \in \mathcal{R}$, we have that $\nu x.(x \oplus x) \in E$ if and only if $\nu x.x \in E$. Hence, $P(\lambda x.(x \oplus x), \ell, E) = P(\lambda x.x, \ell, E)$ for all $\ell \in \Lambda_{\oplus, let}^{\emptyset} \cup \{\tau\}$ and all $E \in (\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset})/\mathcal{R}$. For all equivalence classes $E \in (\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset})/\mathcal{R}, P(\nu x.(x \oplus x), \tau, E) = 0 = P(\nu x.x, \tau, E)$ holds by Definition 14. Further, $P(\nu x.(x \oplus x), F, E) = 1$ for some $F \in \Lambda_{\oplus, let}^{\emptyset}$ if $F \uplus F \in E$, otherwise $P(\nu x.(x \oplus x), F, E) = 0$. We have that $F \uplus F \in E$ if and only if $F \in E$, because $(F \uplus F, F) \in \mathcal{R}$ for all $F \in \Lambda_{\oplus, let}^{\emptyset}$. Hence, $P(\nu x.(x \oplus x), \ell, E) = P(\nu x.x, \ell, E)$ for all $\ell \in \Lambda_{\oplus, let}^{\emptyset} \cup \{\tau\}$ and all $E \in (\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset})/\mathcal{R}$. Finally, let us consider $(N \oplus N, N) \in \mathcal{R}$, for an arbitrary $N \in \Lambda_{\oplus, let}^{\emptyset}$. For all closed terms $F \in \Lambda_{\oplus, let}^{\emptyset}$ and all equivalence classes
$E \in (\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset}) / \mathcal{R}$, $P(N \oplus N, F, E) = 0 = P(N, F, E)$ holds by Definition 14. By Lemma 6 and Definition 14 we have that the following holds for all equivalence classes $E \in (\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset}) / \mathcal{R}$.

$$
\begin{align*}
P(N \oplus N, \tau, E) &= \sum_{\nu x.M \in E} P(N \oplus N, \tau, \nu x.M) = \sum_{\{\lambda x.M | \nu x.M \in E\}} [[N \oplus N]](\lambda x.M) \\
&= \sum_{\{\lambda x.M | \nu x.M \in E\}} \left(\frac{1}{2}[[N]] + \frac{1}{2}[[N]]\right)(\lambda x.M) = \sum_{\{\lambda x.M | \nu x.M \in E\}} [[N]](\lambda x.M) \\
&= \sum_{\nu x.M \in E} P(N, \tau, \nu x.M) = P(N, \tau, E)
\end{align*}
$$

The proof for the other elements of $\mathcal{R}$ is analogous to the cases we considered.

**► Example 16.** The terms $M = \lambda xy.(x \oplus y)$ and $N = (\lambda xy.x) \oplus (\lambda xy.y)$ are not bisimilar. Let us suppose the opposite. Then, there exists a bisimulation $\mathcal{R}$ such that $(M, N) \in \mathcal{R}$. By definition $\mathcal{R}$ is an equivalence relation. Let $E$ be an equivalence class of $\Lambda_{\oplus, let}^{\emptyset} \uplus \Lambda_{\oplus, let}^{\emptyset}$ with respect to $\mathcal{R}$ which contains $\nu x.\lambda y.(x \oplus y)$. Then, we should have that $1 = P(M, \tau, E) = P(N, \tau, E)$. We know that $P(N, \tau, \nu x.\lambda y.x) = \frac{1}{2}$ and $P(N, \tau, \nu x.\lambda y.y) = \frac{1}{2}$. Thus, we can conclude $\nu x.\lambda y.x \in E$ and $\nu x.\lambda y.y \in E$. If $\nu x.\lambda y.x \in E$, then $(\nu x.\lambda y.(x \oplus y), \nu x.\lambda y.x) \in \mathcal{R}$. Hence we have that $1 = P(\nu x.\lambda y.(x \oplus y), \Omega, E_1) = P(\nu x.\lambda y.x, \Omega, E_1)$, where $E_1$ is an equivalence class which contains $\lambda y.(\Omega \oplus y)$. Using the fact that $P(\nu x.\lambda y.x, \Omega, \lambda y.\Omega) = 1$ we obtain $\lambda y.\Omega \in E_1$. Since $\lambda y.(\Omega \oplus y)$ and $\lambda y.\Omega$ belong to the same equivalence class we conclude $(\lambda y.(\Omega \oplus y), \lambda y.\Omega) \in \mathcal{R}$. If $E_2$ is an equivalence class such that $\nu y.(\Omega \oplus y) \in E_2$, then we have that $1 = P(\lambda y.(\Omega \oplus y), \tau, E_2) = P(\lambda y.\Omega, \tau, E_2)$. By a similar reasoning as before we obtain that $(\nu y.(\Omega \oplus y), \nu y.\Omega) \in \mathcal{R}$. Let $E_3$ be an equivalence class which contains $\Omega \oplus I$. From $1 = P(\nu y.(\Omega \oplus y), I, E_3) = P(\nu y.\Omega, I, E_3)$ it follows that $\Omega \in E_3$, i.e. $(\Omega \oplus I, \Omega) \in \mathcal{R}$. Finally, if $E_4$ is an equivalence class such that $\nu x.x \in E_4$, then $\frac{1}{2} = P(\Omega \oplus I, \tau, E_4) = P(\Omega, \tau, E_4)$. This is in contradiction with $P(\Omega, \tau, E_4) = 0$ which is a consequence of the definition of a transition probability matrix. Thus, terms $M$ and $N$ are not bisimilar.

The following proposition is the analogous to Proposition 9, stating the soundness of
(bi)simulation with respect to the operational semantics.

**Proposition 17.** Let $M, N \in \Lambda_{\oplus, let}^{\emptyset}$, if $[[M]] \leq [[N]]$ then $M \preceq N$. So, $[[M]] = [[N]]$ implies $M \sim N$.

**Proof.** By checking that the relation $\mathcal{R} = \{(M, N) \in \Lambda_{\oplus, let}^{\emptyset} \times \Lambda_{\oplus, let}^{\emptyset} \mid [[M]] \leq [[N]]\} \cup \{(\tilde{V}, \tilde{V}) \in \forall \Lambda_{\oplus, let}^{\emptyset} \times \forall \Lambda_{\oplus, let}^{\emptyset}\}$ is a probabilistic applicative simulation. The second part of the statement follows from $\sim = \leq \cap (\leq)^{op}$. $\quad \blacksquare$

We introduce a new notion of relations called $\Lambda_{\oplus, let}$-relations, which are sets of triples
in the form $(\Gamma, M, N)$ where $M, N \in \Lambda_{\oplus, let}^{\Gamma}$. Any relation $R'$ on the set of $\Lambda_{\oplus, let}$-terms can
be extended to a $\Lambda_{\oplus, let}$-relation $\mathcal{R}$, such that whenever $(M, N) \in R'$ and $M, N \in \Lambda_{\oplus, let}^{\Gamma}$, we
have that $(\Gamma, M, N) \in \mathcal{R}$. We will write $\Gamma \vdash \mathcal{MRN}$ instead of $(\Gamma, M, N) \in \mathcal{R}$.

**Definition 18.** A $\Lambda_{\oplus, let}$-relation $\mathcal{R}$ is a congruence (respectively, a precongruence) if it is an equivalence (respectively, a preorder) and for every $\Gamma \cup \Delta \vdash \mathcal{MRN}$ and every context $C \in C\Lambda_{\oplus, let}^{(\Gamma:\Delta)}$, we have that $\Delta \vdash C[M]\mathcal{RC}[N]$.

It is immediate to check that the context preorder $\leq$ (resp. equivalence $\simeq$) is a precongruence (resp. congruence)(Appendix A.1). Also similarity is a precongruence, but its proof is more involved (Appendix A.2). As a consequence we have that bisimilarity is a congruence.
26:10 $\Lambda_{\oplus}$ with Let-In Operator

**► Lemma 19.** The similarity $\lesssim$ (resp. bisimilarity $\sim$) is a precongruence (resp. congruence) relation for $\Lambda_{\oplus,\text{let}}$-terms.

**Proof (Sketch).** As standard [3, 4, 7], we use Howe's technique to prove that probabilistic similarity is a precongruence, this implying that the probabilistic bisimilarity is also a congruence. The proof is technical and follows the same reasoning as [7], the only difference being in the cases needed to handle the compatibility associated with the let-in operator.

We start with defining Howe's lifting for $\Lambda_{\oplus,\text{let}}$, which turns an arbitrary relation $\mathcal{R}$ to another one $\mathcal{R}^H$. The relation $\mathcal{R}^H$ enjoys some properties with respect to the relation $\mathcal{R}$. In particular, if $\mathcal{R}$ is reflexive, transitive and closed under term-substitution, then it is included in $\mathcal{R}^H$ and the relation $\mathcal{R}^H$ is context closed and also closed under term-substitution. These properties allow to prove that the transitive closure $(\lesssim^H)^+$ of the Howe's lifting $\lesssim^H$ is a precongruence including $\lesssim$. One can conclude then easily that $\lesssim$ is also a precongruence. Finally, from $\sim=\lesssim \cup (\lesssim)^{op}$ we conclude that $\sim$ is a congruence. ◀

Now we can prove that simulation preorder (similarity) is sound with respect to the context preorder. As a consequence we have that bisimulation equivalence (bisimilarity) is included in the context equivalence.

**► Theorem 20 (Soundness).** For every $M, N \in \Lambda_{\oplus,\text{let}}^{\Gamma}$, $\Gamma \vdash M \lesssim N$ implies $\Gamma \vdash M \leq N$. Therefore, $M \sim N$ implies $\Gamma \vdash M \simeq N$.

**Proof.** Suppose that $\Gamma \vdash M \lesssim N$. We have that for every context $C \in \mathcal{C}\Lambda_{\oplus,\text{let}}^{(\Gamma;\emptyset)}$, $\emptyset \vdash C[M] \lesssim C[N]$ holds as a consequence of Lemma 19. Then by definition there exists a simulation between $C[M]$ and $C[N]$, which implies by Definition 12 that $\sum [[C[M]]] \leq \sum [[C[N]]]$ holds. We conclude $\Gamma \vdash M \leq N$. The second part of the statement follows from the definitions $\sim=\lesssim \cap \lesssim^{op}$ and $\simeq=\leq \cap \leq^{op}$. ◀

4 Full Abstraction

The goal of this section is to prove the converse of Theorem 20, showing that context equivalence and bisimilarity coincide. In order to get this result, it is more convenient to use the notion of testing equivalence, which has been proven to coincide with Markov processes bisimilarity in [16] (here Theorem 24). In this framework we need to consider only Markov chains, which are the discrete-time version of Markov processes, so we simplify the definitions and results of [16] to this discrete setting, following [3]. Notice that Theorem 24 is independent from the particular Markov chain considered, so we recall the general definitions and then we applied them to the $\Lambda_{\oplus,\text{let}}$-Markov chain.

**► Definition 21 ([3]).** Let $(S, \mathcal{L}, \mathcal{P})$ be a labelled Markov chain. The testing language $\mathcal{T}_{(S, \mathcal{L}, \mathcal{P})}$ for $(S, \mathcal{L}, \mathcal{P})$ is given by the grammar

$$t ::= \omega \mid a.t \mid (t, t),$$

where $\omega$ is a symbol for termination and $a \in \mathcal{L}$ is an action (label).

It is easy to see that tests are finite objects. A test is an algorithm for doing an experiment on a program. During the execution of a test on a particular program, one can observe the success or the failure of the experiment with a given probability. The symbol $\omega$ represents a test which does not require an experiment at all (it always succeed). The test $a.t$ describes an experiment consisting of performing the action $a$ and in the case of success performing the test $t$, and the test $(t, s)$ makes two copies of the current state and allows both tests $t$ and $s$ to be performed independently on the same state. The success probability of a test is defined as follows:
<figure><img src="image_3.png" /><figcaption>**Figure 4** The experiment $t = \tau.(\mathbf{I}.\tau.\Omega.\tau.\omega, \mathbf{I}.\tau.\Omega.\tau.\omega)$ over the terms of Example 23.</figcaption></figure>

**Definition 22 ([3]).** Let $(S, \mathcal{L}, \mathcal{P})$ be a labelled Markov chain. We define a family $\{P_t(\cdot)\}_{t \in \mathcal{T}_{(S, \mathcal{L}, \mathcal{P})}}$ of maps from the set of states $S$ to $\mathbb{R}_{[0,1]}$, by induction on the structure of $t$:

- $P_{\omega}(s) = 1$;

- $P_{a.t}(s) = \sum_{s' \in S} \mathcal{P}(s, a, s')P_t(s')$;

- $P_{(t_1, t_2)}(s) = P_{t_1}(s) \cdot P_{t_2}(s)$.

**Example 23.** The terms $\lambda xy.(x \oplus y)$ and $(\lambda xy.x) \oplus (\lambda xy.y)$ of Example 7 can be discriminated by the test $t = \tau.(\mathbf{I}.\tau.\Omega.\tau.\omega, \mathbf{I}.\tau.\Omega.\tau.\omega)$. Figure 4 sketches the computation of $P_t(\lambda xy.(x \oplus y)) = \frac{1}{4}$ and $P_t((\lambda xy.x) \oplus (\lambda xy.y)) = \frac{1}{2}$.

The following theorem states the equivalence between the notion of bisimilarity over $(S, \mathcal{L}, \mathcal{P})$ and testing equivalence. The theorem has been proven in [16] for a labelled Markov processes. For lack of space, we have omitted a detailed proof of the adaptation of the results from labelled Markov processes to labelled Markov chains.

**Theorem 24 ([3],[16]).** Let $(S, \mathcal{L}, \mathcal{P})$ be a labelled Markov chain. Then $s, s' \in S$ are bisimilar if and only if $P_t(s) = P_t(s')$ for every test $t \in \mathcal{T}_{(S, \mathcal{L}, \mathcal{P})}$.

It is known that this theorem does not hold for inequalities [16]. More precisely, it is not true that $s \lesssim s'$ just in case $P_t(s) \le P_t(s')$ for every test $t \in \mathcal{T}_{(S, \mathcal{L}, \mathcal{P})}$.

## 4.1 Every Test has an Equivalent Context

Here is the main contribution of our paper, showing that for every test $t$ associated with the $\Lambda_{\oplus, let}^-$-Markov chain there exists a context $C_t$ expressing $t$ in the syntax of $\Lambda_{\oplus, let}$, i.e. $P_t(M) = \sum [[C_t[M]]]$ for every term $M$ (Lemma 25). So context equivalence implies testing equivalence (Theorem 27) and hence bisimilarity by Theorem 24. Together with Theorem 20 this achieves the diagram in Figure 1, so Corollary 28.

**Lemma 25.** For every test $t \in \mathcal{T}_{\Lambda_{\oplus, let}}$, there are contexts $C_t \in \mathcal{C}\Lambda_{\oplus, let}^{(\emptyset;\emptyset)}$ and $D_t \in \mathcal{C}\Lambda_{\oplus, let}^{(\emptyset;\emptyset)}$ such that for every term $M \in \Lambda_{\oplus, let}^{\emptyset}$ and value $V = \lambda x.M \in \mathcal{V}_{\oplus, let}^{\emptyset}$ it holds that:

$$P_t(M) = \sum [[C_t[M]]] \quad \text{and} \quad P_t(\tilde{V}) = \sum [[D_t[V]]],$$

where we recall that $\tilde{V}$ denotes the distinguished value $\nu x.M \in \mathcal{V}\Lambda_{\oplus, let}^{\emptyset}$.
**Proof.** We prove it by induction on the structure of a test $t$.

First we consider the case where $t = \omega$. Then, by the definition of $P_t(\cdot)$, we have that for every $M \in \Lambda_{\oplus, let}^{\emptyset}$ and $V \in \mathcal{V}_{\oplus, let}^{\emptyset}$, $P_{\omega}(M) = 1$ and $P_{\omega}(\tilde{V}) = 1$. Thus, we can define $C_{\omega} = (\lambda xy.x)[\cdot]$ and $D_{\omega} = (\lambda xy.x)[\cdot]$ and we obtain, for every $M \in \Lambda_{\oplus, let}^{\emptyset}$

$$ \sum \llbracket C_{\omega}[M] \rrbracket = \sum \llbracket (\lambda xy.x)M \rrbracket = \sum \llbracket \lambda y.M \rrbracket = 1 = P_{\omega}(M), $$

and for every value $V \in \mathcal{V}_{\oplus, let}^{\emptyset}$

$$ \sum \llbracket D_{\omega}[V] \rrbracket = \sum \llbracket (\lambda xy.x)V \rrbracket = \sum \llbracket \lambda y.V \rrbracket = 1 = P_{\omega}(\tilde{V}). $$

Next, let us consider the case where $t = a.t'$ for some action (label) $a$. By induction hypothesis there are contexts $C_{t'} \in \Lambda_{\oplus, let}^{(\emptyset;\emptyset)}$ and $D_{t'} \in \Lambda_{\oplus, let}^{(\emptyset;\emptyset)}$ such that for every $M \in \Lambda_{\oplus, let}^{\emptyset}$ and $V \in \mathcal{V}_{\oplus, let}^{\emptyset}$ we have that $P_{t'}(M) = \sum \llbracket C_{t'}[M] \rrbracket$ and $P_{t'}(\tilde{V}) = \sum \llbracket D_{t'}[V] \rrbracket$. An action $a$ can be either a closed term or a $\tau$ action, thus depending on it we differ two cases.

1. If $a = \tau$, then a test $t$ is of the form $\tau.t'$. From Definition 14 and Definition 22 we have $P_{\tau.t'}(\tilde{V}) = 0$ for any value $V \in \mathcal{V}_{\oplus, let}^{\emptyset}$. Hence, we define $D_{\tau.t'} = \Omega[\cdot]$ and the statement holds. Let $M$ be a closed term. From the definition of a transition probability matrix $(P(M, \tau, \tilde{V}) = \llbracket M \rrbracket(V))$ and induction hypothesis $P_{t'}(\tilde{V}) = \sum \llbracket D_{t'}[V] \rrbracket$ it follows that

$$ P_{\tau.t'}(M) = \sum_{\tilde{V} \in \Lambda_{\oplus, let}^{\emptyset}} P(M, \tau, \tilde{V}) P_{t'}(\tilde{V}) = \sum_{V \in \mathcal{V}_{\oplus, let}^{\emptyset}} \llbracket M \rrbracket(V) \cdot \sum \llbracket D_{t'}[V] \rrbracket. $$

We define $C_{\tau.t'} = (\text{let } y = [\cdot] \text{ in } D_{t'}[y])$. Then, by the definition of operational semantics we get

$$ \sum \llbracket C_{\tau.t'}[M] \rrbracket = \sum \llbracket \text{let } y = M \text{ in } D_{t'}[y] \rrbracket = \sum_{V \in \mathcal{V}_{\oplus, let}^{\emptyset}} \llbracket M \rrbracket(V) \cdot \sum \llbracket D_{t'}[V] \rrbracket, $$

for any closed term $M \in \Lambda_{\oplus, let}^{\emptyset}$. Thus, $P_{\tau.t'}(M) = \sum \llbracket C_{\tau.t'}[M] \rrbracket$.

2. If $a = F$ for some closed term $F$, then a test $t$ is of the form $F.t'$. From Definition 14 and Definition 22 we have $P_{F.t'}(M) = 0$ for any term $M \in \Lambda_{\oplus, let}^{\emptyset}$. Hence, we define $C_{F.t'} = \Omega[\cdot]$ and the statement holds. Let $V$ be a value $\lambda x.N$ ($\tilde{V} = \nu x.N$). From the definition of a transition probability matrix $(P(\nu x.N, F, N\{F/x\}) = 1)$ and induction hypothesis, $P_{t'}(M) = \sum \llbracket C_{t'}[M] \rrbracket$ for every $M \in \Lambda_{\oplus, let}^{\emptyset}$, it follows that

$$ \begin{aligned} P_{F.t'}(\tilde{V}) &= \sum_{N' \in \Lambda_{\oplus, let}^{\emptyset}} P(\tilde{V}, F, N') P_{t'}(N') \\ &= P(\nu x.N, F, N\{F/x\}) \cdot P_{t'}(N\{F/x\}) \\ &= 1 \cdot P_{t'}(N\{F/x\}) = \sum \llbracket C_{t'}[N\{F/x\}] \rrbracket \end{aligned} $$

By Lemma 6 terms $N\{F/x\}$ and $(\lambda x.N)F$ have the same semantics. Hence, they are bisimilar (Proposition 17). Due to the fact that bisimilarity is included in context equivalence (Theorem 20) we have that terms $N\{F/x\}$ and $(\lambda x.N)F$ are context equivalent. More precisely, for any context $C$, $\sum \llbracket C[N\{F/x\}] \rrbracket = \sum \llbracket C[(\lambda x.N)F] \rrbracket$. Finally, we obtain that

$$ P_{F.t'}(\tilde{V}) = \sum \llbracket C_{t'}[N\{F/x\}] \rrbracket = \sum \llbracket C_{t'}[(\lambda x.N)F] \rrbracket = \sum \llbracket C_{t'}[VF] \rrbracket. $$

We define $D_{F.t'} = C_{t'}[\cdot]F$. Then, we have that $\sum \llbracket D_{F.t'}[V] \rrbracket = \sum \llbracket C_{t'}[VF] \rrbracket$, holds for any value $V \in \mathcal{V}_{\oplus, let}^{\emptyset}$. Thus, $P_{F.t'}(\tilde{V}) = \sum \llbracket D_{F.t'}[V] \rrbracket$.
Finally, let $t = (t_1, t_2)$. By induction hypothesis there exist contexts $C_{t_1}, D_{t_1}, C_{t_2}, D_{t_2} \in C\Lambda_{\oplus, let}^{(\emptyset;\emptyset)}$ such that for any closed term $M$ and a value $V$ the following holds:

$$P_{t_1}(M) = \sum \llbracket C_{t_1}[M] \rrbracket, \quad P_{t_1}(\tilde{V}) = \sum \llbracket D_{t_1}[V] \rrbracket,$$

$$P_{t_2}(M) = \sum \llbracket C_{t_2}[M] \rrbracket \quad \text{and} \quad P_{t_2}(\tilde{V}) = \sum \llbracket D_{t_2}[V] \rrbracket.$$

From Definition 22 we have

$$P_{(t_1,t_2)}(M) = P_{t_1}(M) \cdot P_{t_2}(M) = \sum \llbracket C_{t_1}[M] \rrbracket \cdot \sum \llbracket C_{t_2}[M] \rrbracket,$$

for any closed term $M \in \Lambda_{\oplus, let}^{\emptyset}$. We define:

$$C_{(t_1,t_2)} = (\lambda y.(\text{let } z_1 = C_{t_1}[y] \text{ in } (\text{let } z_2 = C_{t_2}[y] \text{ in } I)))[\cdot] \quad (8)$$

and by the definition of operational semantics we have

$$\sum \llbracket C_{(t_1,t_2)}[M] \rrbracket = \sum \llbracket C_{t_1}[M] \rrbracket \cdot \sum \llbracket C_{t_2}[M] \rrbracket.$$

Since, for a value $V \in \mathcal{V}_{\oplus, let}^{\emptyset}$ it holds that

$$P_{(t_1,t_2)}(\tilde{V}) = P_{t_1}(\tilde{V}) \cdot P_{t_2}(\tilde{V}) = \sum \llbracket D_{t_1}[V] \rrbracket \cdot \sum \llbracket D_{t_2}[V] \rrbracket,$$

we define $D_{(t_1,t_2)} = (\lambda y.(\text{let } z_1 = D_{t_1}[y] \text{ in } (\text{let } z_2 = D_{t_2}[y] \text{ in } I)))[\cdot]$ and the statement holds.

This concludes the proof.

**Lemma 26.** Let $M, N \in \Lambda_{\oplus, let}^{\emptyset}$, $M \le N$ implies that $P_t(M) \le P_t(N)$, for every test $t$.

**Proof.** It is a straightforward consequence of Lemma 25. Let us assume that terms $M$ and $N$ are in the context preorder, $\emptyset \vdash M \le N$. Then, for every context $C \in C\Lambda_{\oplus, let}^{(\emptyset;\emptyset)}$, we have $\sum \llbracket C[M] \rrbracket \le \sum \llbracket C[N] \rrbracket$. By Lemma 25, we have that for each test $t \in \mathcal{T}_{\Lambda_{\oplus, let}}$ there exists context $C_t$ such that for every term $M$, $P_t(M) = \sum \llbracket C_t[M] \rrbracket$. Then, for every test $t \in \mathcal{T}_{\Lambda_{\oplus, let}}$, it holds that $P_t(M) = \sum \llbracket C_t[M] \rrbracket \le \sum \llbracket C_t[N] \rrbracket = P_t(N)$. Hence, for every test $t \in \mathcal{T}_{\Lambda_{\oplus, let}}$ it holds that $P_t(M) \le P_t(N)$. ▲

**Theorem 27.** Let $M, N \in \Lambda_{\oplus, let}^{\emptyset}$, $M \simeq N$ implies that $P_t(M) = P_t(N)$, for every test $t$.

**Proof.** It is a straightforward consequence of Lemma 26 and the fact that $M \simeq N$ is equivalent to $M \le N$ and $N \le M$. ▲

Notice that the let-in operator is crucial in defining the context $C_{(t_1,t_2)}$ associated with the product $(t_1, t_2)$ of tests (Equation (8)) in the proof of Lemma 25. For example, if we consider the call-by-name version of $C_{(t_1,t_2)}$, i.e. the context $C = (\lambda y.(\lambda z_1 z_2.I)D_{t_1}[y]D_{t_2}[y])[\cdot]$, then the semantics of $C[M]$ is independent from the contexts $D_{t_1}[\cdot], D_{t_2}[\cdot]$ and the term $M$, being $\llbracket C[M] \rrbracket = I$. Hence, we cannot have $P_{(t_1,t_2)}(M) = \sum \llbracket C[M] \rrbracket$ for every $M$. Another possibility is to try to use a context not erasing $D_{t_1}[\cdot]$ and $D_{t_2}[\cdot]$ during the evaluation, as for example in $C = (\lambda y.D_{t_1}[y]D_{t_2}[y])[\cdot]$. However this would imply to be able to control the result of $D_{t_1}[M]$ for every term $M$, for example supposing $\llbracket D_{t_1}[M] \rrbracket = P_{t_1}(M)I$, which increases considerably the difficulty of the proof. Anyway, the fact that there are examples of terms distinguished by tests (Example 23) but not by contexts without the let-in operator (Example 7) shows the necessity of this latter.
26:14 Λ⊕ with Let-In Operator

The following resumes all results in the paper, as sketched in Figure 1:

► **Corollary 28 (Full Abstraction).** For any $M, N \in \Lambda_{\oplus, let}^{\emptyset}$, the following items are equivalent:
(context equivalence) $M \simeq N$,
(bisimilarity) $M \sim N$,
(testing equivalence) $P_t(M) = P_t(N)$ for all tests $t$.

Concerning inequalities, the equivalence of similarity and testing preorder, i.e. a relation which contains $(s, s')$ if and only if $P_t(s) \leq P_t(s')$ for every test $t \in T_{(S, \mathcal{L}, \mathcal{P})}$, does not hold as we stated below Theorem 24. So, we have no clue for proving that similarity is fully abstract with respect to the context preorder. A possible way to achieve this inequality full abstraction is to look for the converse of Lemma 25, by representing all contexts by tests. However, such a representation is far to be obvious, and even it might not exists.

5 Conclusion

In this paper we have considered the $\Lambda_{\oplus, let}$-calculus, a pure untyped $\lambda$-calculus extended with two operators: a probabilistic choice operator $\oplus$ and a let-in operator. The calculus implements a lazy call-by-name evaluation strategy, following [1, 7], however the let-in operator allows for a call-by-value passing policy. We prove that context equivalence, bisimilarity and testing equivalence all coincide in $\Lambda_{\oplus, let}$ (Corollary 28).

Concerning the inequalities associated with these equivalences: it is known that the probabilistic similarity does not imply the testing approximation [16]. We prove that similarity implies context preorder (Theorem 20), but it remains open whether also the converse holds.

This paper confirms a conjecture stated in [3], showing that the calculus introduced in [7] can be endowed with a fully abstract bisimilarity by adding a let-in operator. As discussed in the Introduction, our feeling is that the need of this operator is due to the lazyness rather than to the cbn policy of the calculus. In order to precise this intuition we plan to investigate the definition of bisimilarity for the non-lazy cbn probabilistic $\lambda$-calculus, which has already fully abstract denotational models [2, 14] as well as infinitary normal forms [13] but not a theory of bisimulations.

In a more general perspective, one can study the let-in operator in call-by-name languages with different effects than the probabilistic one, as for example the non-determinism. Let us also mention [5], which considers a kind of applicative bisimulation for lazy call-by-name lambda-calculi endowed with various algebraic effects. However, the setting seems different, as in [5] the notion of (bi)simulation is not defined over terms but over their semantics.

Finally, one should address similar questions in typed languages. We have already mentioned in the Introduction that [10] shows that adding a let-in operator at ground types does not alter the observational equality of the cbn probabilistic PCF, but what about allowing a let-in at higher-order types? and what in presence of recursive types?

References

1 Samson Abramsky. *Research Topics in Functional Programming*, chapter The Lazy Lambda Calculus, pages 65–116. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1990. URL: http://dl.acm.org/citation.cfm?id=119830.119834.

2 Pierre Clairambault and Hugo Paquet. Fully Abstract Models of the Probabilistic lambda-calculus. In Dan R. Ghica and Achim Jung, editors, *27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK*, volume 119 of LIPIcs, pages 16:1–16:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. doi: 10.4230/LIPIcs.CSL.2018.16.
3 Raphaëlle Crubillé and Ugo Dal Lago. On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi. In *Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings*, pages 209–228, 2014. doi:10.1007/978-3-642-54833-8_12.

4 Raphaëlle Crubillé, Ugo Dal Lago, Davide Sangiorgi, and Valeria Vignudelli. On Applicative Similarity, Sequentiality, and Full Abstraction. In *Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings*, pages 65–82, 2015. doi:10.1007/978-3-319-23506-6_7.

5 Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. Effectful Applicative Similarity for Call-by-Name Lambda Calculi. In Dario Della Monica, Aniello Murano, Sasha Rubin, and Luigi Sauro, editors, *Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic co-located with the 2017 IEEE International Workshop on Measurements and Networking (2017 IEEE M&N)*, Naples, Italy, September 26-28, 2017., volume 1949 of *CEUR Workshop Proceedings*, pages 87–98. CEUR-WS.org, 2017.

6 Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version). *CoRR*, abs/1311.1722, 2013. arXiv:1311.1722.

7 Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On coinductive equivalences for higher-order probabilistic functional programs. In *The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014*, pages 297–308, 2014. doi:10.1145/2535838.2535872.

8 Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. *RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications*, 46(3):413–450, 2012. doi:10.1051/ita/2012012.

9 Thomas Ehrhard, Michele Pagani, and Christine Tasson. The Computational Meaning of Probabilistic Coherence Spaces. In *Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada*, pages 87–96, 2011. doi:10.1109/LICS.2011.29.

10 Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full Abstraction for Probabilistic PCF. *Journal of the ACM*, 65(4):23:1–23:44, 2018. doi:10.1145/3164540.

11 Jean-Yves Girard. Linear Logic. *Theoretical Computer Science*, 50:1–102, 1987. doi:10.1016/0304-3975(87)90045-4.

12 Kim Guldstrand Larsen and Arne Skou. Bisimulation through Probabilistic Testing. *Information and Computation*, 94(1):1–28, 1991. doi:10.1016/0890-5401(91)90030-6.

13 Thomas Leventis. Probabilistic Böhm Trees and Probabilistic Separation. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018*, pages 649–658, 2018. doi:10.1145/3209108.3209126.

14 Thomas Leventis and Michele Pagani. Strong Adequacy and Untyped Full Abstraction for Probabilistic Coherence Spaces. accepted to FOSSACS 2019, 2019.

15 Sungwoo Park, Frank Pfenning, and Sebastian Thrun. A Probabilistic Language Based on Sampling Functions. *ACM Transactions on Programming Languages and Systems*, 31(1):4:1–4:46, December 2008. doi:10.1145/1452044.1452048.

16 Franck Van Breugel, Michael W. Mislove, Joël Ouaknine, and James Worrell. Domain theory, testing and simulation for labelled Markov processes. *Theoretical Computer Science*, 333(1-2):171–197, 2005. doi:10.1016/j.tcs.2004.10.021.
A Appendix - Proofs

A.1 Context Equivalence is a Congruence

We consider $\Lambda_{\oplus, let}$-relations defined in Section 3. The set $P_{FIN}(X)$ denotes the set of all finite subsets of $X$.

► **Definition 29.** A $\Lambda_{\oplus, let}$-relation $\mathcal{R}$ is compatible if and only if the five conditions below hold:

(Com1) $\forall \Gamma \in P_{FIN}(X), x \in \Gamma : \Gamma \vdash x \mathcal{R} x;$

(Com2) $\forall \Gamma \in P_{FIN}(X), \forall x \in X - \Gamma, \forall M, N \in \Lambda_{\oplus, let}^{\Gamma \cup \{x\}} : \Gamma \cup \{x\} \vdash M \mathcal{R} N \Rightarrow \Gamma \vdash \lambda x.M \mathcal{R} \lambda x.N;$

(Com3) $\forall \Gamma \in P_{FIN}(X), \forall M, N, L, P \in \Lambda_{\oplus, let}^{\Gamma} : \Gamma \vdash M \mathcal{R} N \wedge \Gamma \vdash L \mathcal{R} P \Rightarrow \Gamma \vdash M L \mathcal{R} NP;$

(Com4) $\forall \Gamma \in P_{FIN}(X), \forall M, N, L, P \in \Lambda_{\oplus, let}^{\Gamma} : \Gamma \vdash M \mathcal{R} N \wedge \Gamma \vdash L \mathcal{R} P \Rightarrow \Gamma \vdash M \oplus L \mathcal{R} N \oplus P;$

(Com5) $\forall \Gamma \in P_{FIN}(X), \forall x \in X, \forall M, N \in \Lambda_{\oplus, let}^{\Gamma}, \forall L, P \in \Lambda_{\oplus, let}^{\Gamma \cup \{x\}} : \Gamma \vdash M \mathcal{R} N \wedge \Gamma \cup \{x\} \vdash L \mathcal{R} P \Rightarrow \Gamma \vdash (\text{let } x = M \text{ in } L) \mathcal{R} (\text{let } x = N \text{ in } P).$

► **Definition 30.** A $\Lambda_{\oplus, let}$-relation is a congruence (respectively, precongruence) if it is an equivalence relation (respectively, preorder) and compatible.

This definition of a (pre)congruence is equivalent to Definition 18.

► **Lemma 31.** The context preorder $\leq$ is a precongruence relation.

*Proof.* The proof follows the same basic outline as the proof of Lemma 3.33 in [6].

<figure><img src="image_4.png" /></figure>

► **Lemma 32.** The context equivalence $\simeq$ is a congruence relation.

*Proof.* This statement follows directly from Lemma 31 and the definition of context equivalence, i.e. $\simeq \leq \cap (\leq)^{op}$.

<figure><img src="image_5.png" /></figure>

A.2 Bisimulation Equivalence is a Congruence

We use Howe's technique to prove that probabilistic similarity is a precongruence and as a consequence probabilistic bisimilarity is a congruence. Howe's technique is a commonly used technique for proving precongruence of similarity. The proof is very technical. It is the adaptation of the technique used in [3, 4, 6] and it has the same structure as the proof in [6]. Contrary to the proof in [6], our proof introduces a new notion of compatibility with the let-in operator.

The property $\sim = \lesssim \cap \lesssim^{op}$ ensures it is enough to show that probabilistic similarity ($\lesssim$) is a precongruence in order to prove that probabilistic bisimilarity ($\sim$) is a congruence. The key part is proving that $\lesssim$ is a compatible relation and it is done by Howe's technique.

We call an $\Lambda_{\oplus, let}$-relation $\mathcal{R}$ (term) substitutive if for all $\Gamma \in P_{FIN}(X), x \in X - \Gamma, M, N \in \Lambda_{\oplus, let}^{\Gamma \cup \{x\}}$, $L, P \in \Lambda_{\oplus, let}^{\Gamma}$ the following holds

$$ \Gamma \cup \{x\} \vdash M \mathcal{R} N \wedge \Gamma \vdash L \mathcal{R} P \Rightarrow \Gamma \vdash M\{L/x\} \mathcal{R} N\{P/x\}. $$

If a relation $\mathcal{R}$ satisfies

$$ \Gamma \cup \{x\} \vdash M \mathcal{R} N \wedge L \in \Lambda_{\oplus, let}^{\Gamma} \Rightarrow \Gamma \vdash M\{L/x\} \mathcal{R} N\{L/x\}, $$

we say it is closed under term-substitution.
$$ \frac{\Gamma \vdash x \mathcal{R} M}{\Gamma \vdash x \mathcal{R}^H M} \quad \text{(How1)} \qquad \frac{\Gamma \cup \{x\} \vdash M \mathcal{R}^H L \quad \Gamma \vdash \lambda x.L \mathcal{R} N \quad x \notin \Gamma}{\Gamma \vdash \lambda x.M \mathcal{R}^H N} \quad \text{(How2)} $$

$$ \frac{\Gamma \vdash M \mathcal{R}^H P \quad \Gamma \vdash N \mathcal{R}^H Q \quad \Gamma \vdash PQ \mathcal{R} L}{\Gamma \vdash MN \mathcal{R}^H L} \quad \text{(How3)} $$

$$ \frac{\Gamma \vdash M \mathcal{R}^H P \quad \Gamma \vdash N \mathcal{R}^H Q \quad \Gamma \vdash P \oplus Q \mathcal{R} L}{\Gamma \vdash M \oplus N \mathcal{R}^H L} \quad \text{(How4)} $$

$$ \frac{\Gamma \vdash M \mathcal{R}^H P \quad \Gamma \cup \{x\} \vdash N \mathcal{R}^H Q \quad \Gamma \vdash (\text{let } x = P \text{ in } Q) \mathcal{R} L}{\Gamma \vdash (\text{let } x = M \text{ in } N) \mathcal{R}^H L} \quad \text{(How5)} $$

Figure 5 Howe's lifting for $\Lambda_{\oplus,let}$.

$$ \frac{\Gamma \vdash M \mathcal{R} N}{\Gamma \vdash M \mathcal{R}^+ N} \quad \text{(TC1)} $$ $$ \frac{\Gamma \vdash M \mathcal{R}^+ N \quad \Gamma \vdash N \mathcal{R}^+ L}{\Gamma \vdash M \mathcal{R}^+ L} \quad \text{(TC2)} $$

Figure 6 Transitive closure for $\Lambda_{\oplus,let}$.

Please notice that if $\mathcal{R}$ is substitutive and reflexive then it is closed under term-substitution. As stated in the paper, open extensions of $\leq$ and $\sim$ are closed under term-substitution by definition.

For an arbitrary $\Lambda_{\oplus,let}$-relation $\mathcal{R}$, Howe's lifting $\mathcal{R}^H$ is defined by the rules in Figure 5. We start with some auxiliary statements.

**Lemma 33.** If $\mathcal{R}$ is reflexive, then $\mathcal{R}^H$ is compatible.

*Proof.* The proof follows the same basic outline as the proof of Lemma 3.10 in [6].

**Lemma 34.** If $\mathcal{R}$ is transitive, then $\Gamma \vdash M \mathcal{R}^H N$ and $\Gamma \vdash N \mathcal{R} L$ imply $\Gamma \vdash M \mathcal{R}^H L$.

*Proof.* By induction on the derivation of $\Gamma \vdash M \mathcal{R}^H N$, looking at the last rule used, thus on the structure of $M$.

**Lemma 35.** If $\mathcal{R}$ is reflexive, then $\Gamma \vdash M \mathcal{R} N$ implies $\Gamma \vdash M \mathcal{R}^H N$.

*Proof.* By induction on the structure of $M$.

**Lemma 36.** If $\mathcal{R}$ is reflexive, transitive and closed under term-substitution, then $\mathcal{R}^H$ is (term) substitutive and hence also closed under term-substitution.

*Proof.* We need to show that: $\forall \Gamma \in P_{\text{FIN}}(X), \forall x \in X - \Gamma, \forall M, N \in \Lambda_{\oplus,let}^{\Gamma \cup \{x\}}, \forall L, P \in \Lambda_{\oplus,let}^{\Gamma}$, $\Gamma \cup \{x\} \vdash M \mathcal{R}^H N \wedge \Gamma \vdash L \mathcal{R}^H P \Rightarrow \Gamma \vdash M\{L/x\} \mathcal{R}^H N\{L/x\}$.

*Proof.* Proceeds by induction on the derivation of $\Gamma \cup \{x\} \vdash M \mathcal{R}^H N$.

The goal is to prove that $\leq^H$ is a precongruence, but in order to do that some properties are missing. Hence, following Howe's approach we build a transitive closure of a $\Lambda_{\oplus,let}$-relation $\mathcal{R}$ as a relation $\mathcal{R}^+$ defined by the rules in Figure 6.
**Lemma 37.** If $\mathcal{R}$ is compatible, then so is $\mathcal{R}^+$.

*Proof.* The proof follows the same basic outline as the proof of Lemma 3.14 in [6]. ▼

**Lemma 38.** If $\mathcal{R}$ is closed under term-substitution, then so is $\mathcal{R}^+$.

*Proof.* Proving that $\mathcal{R}^+$ is closed under term-substitution means to show: $\forall \Gamma \in P_{\text{FIN}}(X), \forall x \in X - \Gamma, \forall M, N \in \Lambda_{\oplus, \text{let}}^{\Gamma \cup \{x\}}, \forall L \in \Lambda_{\oplus, \text{let}}^{\Gamma}, \Gamma \cup \{x\} \vdash M \mathcal{R}^+ N \Rightarrow M\{L/x\} \mathcal{R}^+ N\{L/x\}$. Proof proceeds by induction on the derivation of $\Gamma \cup \{x\} \vdash M \mathcal{R}^+ N$. ▼

**Lemma 39.** If a $\Lambda_{\oplus, \text{let}}$-relation $\mathcal{R}$ is a preorder, then so is $(\mathcal{R}^H)^+$.

*Proof.* A relation is a preorder if it is reflexive and transitive. We assume that $\mathcal{R}$ is reflexive and transitive. Then, by Lemma 33 and Lemma 37 we conclude $(\mathcal{R}^H)^+$ is compatible and hence reflexive. Relation $(\mathcal{R}^H)^+$ is transitive by its construction, since it is a transitive closure of relation $\mathcal{R}^H$. Thus, we conclude relation $(\mathcal{R}^H)^+$ is a preorder. ▼

The crucial part in proving that probabilistic similarity is a precongruence is Key Lemma (Lemma 44). First, we need the definition of a probability assignment and an auxiliary lemma about it.

**Definition 40.** $\mathbb{P} = (\{p_i\}_{1\le i\le n}, \{r_I\}_{I\subseteq\{1,\dots,n\}})$ is a probability assignment if for each $I \subseteq \{1, \dots, n\}$ it holds that $\sum_{i \in I} p_i \le \sum_{J \cap I \ne \emptyset} r_J$.

**Lemma 41.** Let $\mathbb{P} = (\{p_i\}_{1\le i\le n}, \{r_I\}_{I\subseteq\{1,\dots,n\}})$ be a probability assignment. Then for every nonempty $I \subseteq \{1, \dots, n\}$ and for every $k \in I$ there is $s_{k,I} \in [0, 1]$ which satisfies the following conditions:

1. for every $I$, it holds that $\sum_{k \in I} s_{k,I} \le 1$;

2. for every $k \in \{1, \dots, n\}$, it holds that $p_k \le \sum_{k \in I} s_{k,I} \cdot r_I$.

The proof of Lemma 41 is omitted, but it can be found in [6]. Besides Lemma 41, in the proof of Key Lemma we use the following technical Lemmas.

**Lemma 42.** For every $X \subseteq \Lambda_{\oplus, \text{let}}^{\{x\}}$, it holds that $\lesssim (\lambda x.X) = \lambda x.(\lesssim (X))$ and $\lesssim (\nu x.X) = \nu x.(\lesssim (X))$. $\lambda x.(\lesssim (X))$ stands for the set $\{\lambda x.M \mid \exists N \in X, N \lesssim M\}$.

*Proof.* Straightforward consequence of the definition of similarity. ▼

**Lemma 43.** If $M \lesssim N$, then for every $X \subseteq \Lambda_{\oplus, \text{let}}^{\{x\}}$, $[[M]](\lambda x.X) \le [[N]](\lambda x. \lesssim (X))$.

*Proof.* It is a straightforward consequence of Lemma 42. ▼

**Lemma 44 (Key Lemma).** If $M \lesssim^H N$, then for every $X \subseteq \Lambda_{\oplus, \text{let}}^{\{x\}}$ it holds that $[[M]](\lambda x.X) \le [[N]](\lambda x.(\lesssim^H (X)))$.

*Proof.* Since $[[M]] = \sup\{\mathcal{D} ; M \Downarrow \mathcal{D}\}$, it is enough to prove the following statement: if $M \lesssim^H N$ and $M \Downarrow \mathcal{D}$ then for every $X \subseteq \Lambda_{\oplus, \text{let}}^{\{x\}}$ it holds that $\mathcal{D}(\lambda x.X) \le [[N]](\lambda x.(\lesssim^H (X)))$. Proof proceeds by induction on the derivation of $M \Downarrow \mathcal{D}$, looking at the last rule used. We only consider the case where $M$ is of the form $\text{let } x = L$ in $P$, while the proofs of other cases follow the same basic outline as the proof of Lemma 3.17 in [6].
Let $M = (\text{let } x = L \text{ in } P)$. Then, we have $\mathcal{D} = \sum_{\lambda x.Q} \mathcal{F}(\lambda x.Q) \cdot \mathcal{H}_{Q,P}$ where $L \Downarrow \mathcal{F}$ and for any $\lambda x.Q \in \mathcal{S}(\mathcal{F})$, $\{P\{\lambda x.Q/x\} \Downarrow \mathcal{H}_{Q,P}\}$. The last rule used in the derivation of $\emptyset \vdash M \lesssim^H N$ has to be (How5), thus we get $\emptyset \vdash L \lesssim^H R$, $x \vdash P \lesssim^H S$ and $\emptyset \vdash (\text{let } x = R \text{ in } S) \lesssim N$ as additional hypothesis. By applying the induction hypothesis on $L \Downarrow \mathcal{F}$ and $\emptyset \vdash L \lesssim^H R$, we obtain that

$$ \mathcal{F}(\lambda x.Y) \leq \llbracket R \rrbracket (\lambda x. \lesssim^H (Y)), \qquad (9) $$

holds for any $Y \subseteq \Lambda_{\oplus, let}^{\{x\}}$. $\mathcal{F}$ is a finite distribution, hence the distribution $\mathcal{D} = \sum_{\lambda x.Q} \mathcal{F}(\lambda x.Q) \cdot \mathcal{H}_{Q,P}$ is a sum of finitely many summands. Let the support of $\mathcal{F}$ be the set $\mathcal{S}(\mathcal{F}) = \{\lambda x.Q_1, \dots, \lambda x.Q_n\}$. Equation (9) implies that for every $I \subseteq \{1, \dots, n\}$ the following holds

$$ \mathcal{F}(\bigcup_{i \in I} \lambda x.Q_i) \leq \llbracket R \rrbracket (\bigcup_{i \in I} \lambda x. \lesssim^H (Q_i)). $$

This allows us to apply Lemma 41. Thus, for every $U \in \bigcup_{i=1}^n \lesssim^H (Q_i)$ there exist numbers $r_1^{U,R}, \dots, r_n^{U,R}$ such that:

$$ \llbracket R \rrbracket (\lambda x.U) \geq \sum_{i=1}^n r_i^{U,R}, \quad \forall U \in \bigcup_{i=1}^n \lesssim^H (Q_i); $$

$$ \mathcal{F}(\lambda x.Q_i) \leq \sum_{U \in \lesssim^H(Q_i)} r_i^{U,R}, \quad \forall i \in \{1, \dots, n\}. $$

Now, we can conclude the following

$$ \mathcal{D} \leq \sum_{i=1}^{n} \left( \sum_{U \in \lesssim^{H}(Q_i)} r_i^{U,R} \right) \cdot \mathcal{H}_{Q_i, P} = \sum_{i=1}^{n} \sum_{U \in \lesssim^{H}(Q_i)} r_i^{U,R} \cdot \mathcal{H}_{Q_i, P}. $$

Since $Q_i \lesssim^H U$ holds and $\lesssim^H$ is compatible by Lemma 33, $\lambda x.Q_i \lesssim^H \lambda x.U$ holds. By applying Lemma 36 on $P \lesssim^H S$ and the latter we get $P\{\lambda x.Q_i/x\} \lesssim^H S\{\lambda x.U/x\}$. If we apply the induction hypothesis on the derivations $P\{\lambda x.Q_i/x\} \Downarrow \mathcal{H}_{Q_i,P}, i \in \{1, \dots, n\}$, we obtain that for every $X \subseteq \Lambda_{\oplus, let}^{\{x\}}$ it holds that

$$ \mathcal{D}(\lambda x.X) \leq \llbracket N \rrbracket (\lambda x. \lesssim^H (X)). $$

This concludes the proof.

<figure><img src="image_6.png" /></figure>

**Proof of Lemma 19.** The proof that similarity is a precongruence consists of two steps: the first step is to show that the relation $(\lesssim^H)^+$ is a precongruence and the second one is to show that it coincide with relation $\lesssim$. Since $\lesssim$ is a preorder, then by Lemma 39, relation $(\lesssim^H)^+$ is also a preorder. Relation $\lesssim$ is reflexive, hence by Lemma 33 we have $\lesssim^H$ is compatible. Furthermore, Lemma 37 ensures that $(\lesssim^H)^+$ is also compatible. So, we can conclude that $(\lesssim^H)^+$ is a precongruence. Next, we want to show that $\lesssim = (\lesssim^H)^+$. From the construction of Howe's lifting $\lesssim^H$ and its transitive closure $(\lesssim^H)^+$ it follows that $\lesssim \subseteq (\lesssim^H)^+$. It remains to show the inclusion $(\lesssim^H)^+ \subseteq \lesssim$. We show that $(\lesssim^H)^+$ is included in some probabilistic simulation $\mathcal{R}$, thus it is also included in the largest one, $\lesssim$. The relation we consider is $\mathcal{R} = \{(M, N) : M (\lesssim^H)^+ N\} \cup \{(\nu x.M, \nu x.N) : M (\lesssim^H)^+ N\}$. It is obvious that $(\lesssim^H)^+ \subseteq \mathcal{R}$, so it only remains to show that $\mathcal{R}$ is a probabilistic simulation. Relation $(\lesssim^H)^+$ is closed under term-substitution (by Lemma 36 and Lemma 38), hence it is enough to consider only closed terms and distinguished values. Since $(\lesssim^H)^+$ is a preorder relation (reflexive and transitive), it is easy to see $\mathcal{R}$ is also a preorder. We show the following two points:
1. If $M (\lesssim^H)^+ N$, then for every $X \subseteq \Lambda_{\oplus, let}^{\{x\}}$ it holds that
   $P(M, \tau, \nu x.X) \leq P(N, \tau, \mathcal{R}(\nu x.X))$.

2. If $M (\lesssim^H)^+ N$, then for every $L \in \Lambda_{\oplus, let}^{\emptyset}$ and for every $X \subseteq \Lambda_{\oplus, let}^{\{x\}}$, $P(\nu x.M, L, X) \leq P(\nu x.N, L, \mathcal{R}(X))$.

The first point we prove by induction on the derivation of $M (\lesssim^H)^+ N$. We look at the last rule used. Let us start with the base case where (TC1) is the last rule used. Then, we have $M \lesssim^H N$ holds by hypothesis. By Key Lemma we conclude the following:

$$
\begin{align*}
P(M, \tau, \nu x.X) &= [M](\lambda x.X) \\
&\le [N](\lambda x. \lesssim^H (X)) \\
&\le [N](\lambda x.(\lesssim^H)^+(X)) \\
&\le [N](\mathcal{R}(\nu x.X)) \\
&= P(N, \tau, \mathcal{R}(\nu x.X)).
\end{align*}
$$

Next, we consider the case where (TC2) is the last rule used and we have that for some
$P \in \Lambda_{\oplus, let}^{\emptyset}$, $M (\lesssim^H)^+ P$ and $P (\lesssim^H)^+ N$ hold. By induction hypothesis on both of them,
we obtain:

$$
P(M, \tau, X) \leq P(P, \tau, \mathcal{R}(X)),
$$

$$
P(P, \tau, \mathcal{R}(X)) \leq P(N, \tau, \mathcal{R}(\mathcal{R}(X))).
$$

It is easy to show that $\mathcal{R}(\mathcal{R}(X)) \subseteq \mathcal{R}(X)$, thus we can conclude

$$
P(M, \tau, X) \leq P(N, \tau, \mathcal{R}(X)).
$$

This concludes the proof of the first point.

If $M (\lesssim^H)^+ N$ and $L \in \Lambda_{\oplus, let}^{\emptyset}$, then because of the fact that $(\lesssim^H)^+$ closed under term-substitution, we have that $M\{L/x\} (\lesssim^H)^+ N\{L/x\}$ holds. As a consequence, we have that whenever $M\{L/x\} \in X$, then $N\{L/x\} \in (\lesssim^H)^+(X)$ and it holds that

$$
\begin{align*}
P(\nu x.M, L, X) &= 1 \\
&= P(\nu x.N, L, (\lesssim^H)^+(X)) \\
&= P(\nu x.N, L, \mathcal{R}(X)).
\end{align*}
$$

On the other hand, if $M\{L/x\} \notin X$, then $P(\nu x.M, L, X) = 0 \le P(\nu x.N, L, \mathcal{R}(X))$.

To prove that bisimilarity is a congruence we need to prove that $\sim$ is an equivalence relation, which is compatible. Relation $\sim$ is an equivalence relation by its definition. Since we know that $\sim=\lesssim \cap \lesssim^{op}$ holds, from the fact that similarity is a precongruence it follows that $\sim$ is also compatible. This concludes the proof. $\quad$