Metric Reasoning About $\lambda$-Terms: The General Case (Long Version)

TL;DR

This paper explores the properties of context distance in probabilistic lambda calculi, extending analysis beyond affine cases, and introduces pseudometrics that are fully abstract for call-by-name and call-by-value settings.

Contribution

It provides a comprehensive analysis of context distance in probabilistic lambda calculi, including trivialization conditions, coinductive characterizations, and fully abstract pseudometrics.

Findings

Characterizes when context distance trivializes.

Defines coinductive, tuple-based distance in $ ext{Lambda}^ ext{oplus}_!$.

Derives and proves full abstraction of pseudometrics for probabilistic lambda calculi.

Abstract

In any setting in which observable properties have a quantitative flavour, it is natural to compare computational objects by way of \emph{metrics} rather than equivalences or partial orders. This holds, in particular, for probabilistic higher-order programs. A natural notion of comparison, then, becomes context distance, the metric analogue of Morris' context equivalence. In this paper, we analyze the main properties of the context distance in fully-fledged probabilistic $\lambda$-calculi, this way going beyond the state of the art, in which only affine calculi were considered. We first of all study to which extent the context distance trivializes, giving a sufficient condition for trivialization. We then characterize context distance by way of a coinductively defined, tuple-based notion of distance in one of those calculi, called $\Lambda^\oplus_!$. We finally derive pseudometrics for call-by-name and call-by-value probabilistic $\lambda$-calculi, and prove them fully-abstract.

Figures

Equations

$$M\equiv N\iff \forall C.{\sum }_{[[C[M]]]}={\sum }_{[[C[N]]]}.$$

$$\delta (M,N)=\underset{C}{\sup }\left|{\sum }_{[[C[M]]]}-{\sum }_{[[C[N]]]}\right|.$$

$$M\in\mathscr{T}::=\;x\;\;\mbox{\Large{$\mid$}}\;\;MM\;\;\mbox{\Large{$\mid$}}\;\;\lambda x.M\;\;\mbox{\Large{$\mid$}}\;\;\lambda{!{x}}.M\;\;\mbox{\Large{$\mid$}}\;\;!{M}\;\;\mbox{\Large{$\mid$}}\;\;M\,\oplus\,M\;\;\mbox{\Large{$\mid$}}\;\;\,\left([M\parallel M]\rightarrowtail M\right)\,,$$

$$V\in\mathscr{V}::=\lambda x.M\;\;\mbox{\Large{$\mid$}}\;\;\lambda{!{x}}.M\;\;\mbox{\Large{$\mid$}}\;\;!{M}.$$

$$E::=\;[\cdot]\;\;\mbox{\Large{$\mid$}}\;\;EV\;\;\mbox{\Large{$\mid$}}\;\;ME\;\;\mbox{\Large{$\mid$}}\;\;\,\left([M\parallel E]\rightarrowtail N\right)\,\;\;\mbox{\Large{$\mid$}}\;\;\,\left([E\parallel M]\rightarrowtail N\right)\,.$$

$$M\oplus N\hookrightarrow M,N$$

$$\left([V\parallel M]\rightarrowtail N\right)\hookrightarrow N$$

$$V\Rightarrow \{V^1\}$$

$$\sigma\in\mathscr{A}::=\alpha\;\;\mbox{\Large{$\mid$}}\;\;\mu{\alpha}.\sigma\multimap\sigma\;\;\mbox{\Large{$\mid$}}\;\;\mu{\alpha}.!{\sigma}\;\;\mbox{\Large{$\mid$}}\;\;\sigma\multimap\sigma\;\;\mbox{\Large{$\mid$}}\;\;!{\sigma}$$

$$\mu \alpha .\sigma ⊸\tau {=}^{\mathcal{A}}\sigma [\alpha \to (\mu \alpha .\sigma ⊸\tau )]⊸\tau [\alpha \to (\mu \alpha .\sigma ⊸\tau )]$$

$$\mu \alpha .!\sigma {=}^{\mathcal{A}}!(\sigma [\alpha \to \mu \alpha .!\sigma ])$$

$$!\Gamma ,!x:!\sigma ⊢x:\sigma$$

$$!x:\sigma ,!\Gamma ,\Delta ⊢M:\tau$$

$$!\Gamma ⊢M:\sigma$$

$$!\Gamma ,\Delta ⊢M:\sigma$$

$$M{\oplus }^{0}N$$

$$M{\oplus }^{1}N$$

$$M{\oplus }^{\frac{n}{2^m}}N$$

$${\delta }_{\sigma ,!,\parallel }^c(M,N)=\underset{C\in {\mathcal{C}}_{\sigma }^{\tau }}{\sup }|\text{Obs}(C[M])-\text{Obs}(C[N])|.$$

$$\left.\begin{array}[]{r}\vdash M,N:\sigma\\ \text{Obs}(M)=\alpha\\ \text{Obs}(N)=\beta\end{array}\right\}\Rightarrow\left\lvert\text{Obs}(C_{\sigma}^{\alpha,\beta,\gamma}[!{M}])-\text{Obs}(C_{\sigma}^{\alpha,\beta,\gamma}[!{N}])\right\rvert\geq 1-\gamma.$$

$$P_n^f(x)={\sum }_{0\le k\le n}f\left(\frac{k}{n}\right)\cdot B_k^n(x),\text{ where }{B}_k^n(x)=\left(\genfrac{}{}{0ex}{}{n}{k}\right)\cdot x^k\cdot (1-x{)}^{n-k}.$$

$$C_n=\left(\lambda !x.\left([x\parallel \left([x\parallel \dots ]\rightarrowtail I\right)]\rightarrowtail I\right)\right)[\cdot ].$$

$$C_n^m=\lambda !y.\left({\bigwedge }^n({\bigvee }^m(y,\dots ,y),\dots ,{\bigvee }^m(y,\dots ,y))\right)[\cdot ]$$

$${\bigvee }^n(M_1,\dots M_n)$$

$${\bigwedge }^n(M_1\dots M_n)$$

$$\underset{n\to \infty }{\lim }\text{Obs}(C_n^{m(n,\iota )}[!M])=\{\begin{array}{l}1\text{ if }\text{Obs}(M)>\iota ;\\ 0\text{ if }\text{Obs}(M)<\iota .\end{array}.$$

$$r(n,\iota )={\left(\frac{1}{1-\iota }\right)}^n.$$

$$f_{n,\iota }(x)=(1-(1-x{)}^n{)}^{\lceil r(n,\iota )\rceil }$$

$$\underset{n\to \infty }{\lim }{f}_{n,\iota }(x)=\{\begin{array}{l}0\text{ if }x<\iota \\ 1\text{ if }x>\iota \end{array}$$

$$g_{n,\alpha }(x)=\{\begin{array}{l}{\int }_0^x{g}_{n,\alpha }^{\prime }(t)dt+1\text{ if }x<\alpha \\ -{\int }_x^1{g}_{n,\alpha }^{\prime }(t)dt\text{ if }x>\alpha \end{array}$$

$$\underset{n\to \infty }{\lim }{\int }_0^x{g}_{n,\alpha }^{\prime }(t)dt=0\text{and}\underset{n\to \infty }{\lim }{\int }_x^1{g}_{n,\alpha }^{\prime }(t)dt=0.$$

$$g_{n,\alpha }^{\prime }(x)=-\lceil r(n,1-\alpha )\rceil \cdot n\cdot {\left(1-x^n\right)}^{\lceil r(n,1-\alpha )\rceil -1}\cdot x^{n-1}$$

Full text

1 Introduction

Probability theory offers computer science models which enable system abstraction (at the price of introducing uncertainty), but which can also be seen as a a way to compute, like in randomized computation. Domains in which probabilistic models play a key role include machine learning [28], robotics [35], and linguistics [25]. In cryptography, on the other hand, having access to a source of uniform randomness is essential to achieve security, e.g., in the public key setting [20]. This has stimulated the development of concrete and abstract programming languages, which most often are extensions of their deterministic siblings. Among the many ways probabilistic choice can be captured in programming, the simplest one consists in endowing the language of programs with an operator modelling the flipping of a fair coin. This renders program evaluation a probabilistic process, and under mild assumptions the language becomes universal for probabilistic computation. Particularly fruitful in this sense has been the line of work on the functional paradigm, both at a theoretical [22, 30, 27] and at a more practical level [21].

We are still far, however, from a satisfactory understanding of higher-order probabilistic computation. As an example, little is known about how much of the classic, beautiful, theory underlying the $\lambda$-calculus [1] can be lifted to probabilistic $\lambda$-calculi, although the latter have been known from forty years now [31]. Until the beginning of this decade, indeed, most investigations were directed towards domain theory, which has been proved to be much more involved in presence of probabilistic choice than in a deterministic scenario [23]. In the last ten years, however, some promising results have appeared. As an example, both quantitative semantics and applicative bisimilarity have been shown to coincide with context equivalence for certain kinds of probabilistic $\lambda$-calculi [14, 5]. This not only provides us with new proof methodologies for program equivalence, but also sheds new light on the very nature of probabilistic higher-order computation. As an example, recent results tell us that program equivalence in presence of probabilistic choice lies somehow in between determinism and non-determinism [5].

But are equivalences the most proper way to compare terms? Actually, this really depends on what the underlying observable is. If observables are boolean, then equivalences (and preorders) are indeed natural choices: two programs are dubbed equivalent if they give rise to the same observable (of which there are just two!) in any context. If, on the other hand, the observable is an element of a metric space, which happens for example when we observe (the probability of) convergence in a probabilistic setting, one may wonder whether replacing equivalences with metrics makes sense. This is a question that has recently been given a positive answer in the affine setting [7], i.e., in a $\lambda$-calculus in which copying is simply not available. More specifically, a notion of context distance has been shown to model differences between terms satisfactorily, and has also been shown to be characterized by notions of trace metrics, and to be approximated from below by behavioural metrics.

Affine $\lambda$-calculi are very poor in terms of the computations they are able to model. Measuring the distance between terms in presence of copying, however, is bound to be problematic. On the one hand, allowing contexts to copy their argument has the potential risk of trivialising the underlying metric. On the other hand, finding handier characterizations of the obtained notion of metric in the style of behavioural or trace metrics is inherently hard. A more thorough discussion on these issues can be found in Section 2 below.

In this paper, we attack the problem of analyzing the distance between $\lambda$-terms in its full generality. More specifically, the contributions of this paper are fourfold:

• •

First of all, we define a linear probabilistic $\lambda$-calculus, called $\Lambda_{\oplus}^{!,\parallel}$, in which copying and a nonstandard construct, namely Plotkin’s parallel disjunction, are both available. A very liberal type system prevents deadlocks, but nevertheless leaves the expressive power of the calculus very high. This choice has been motivated by our will to put ourselves in the most general setting, so as to be able to talk about different fragments. The calculus is endowed with a notion of context distance, in Morris’ style. This is covered in Section 3 below.

• •

We study trivialization of the obtained notion(s) of metric for different fragments of $\Lambda_{\oplus}^{!,\parallel}$, showing that both parallel disjunction and strong normalization give us precisely the kind of discriminating power we need to arbitrarily amplify distances, while in the most natural fragment, namely $\Lambda_{\oplus}^{!}$, trivialization does not hold. This is the subject of Section 4.

• •

In Section 5, we prove that context distance can be characterized as a coinductively defined distance on a labelled Markov chain of tuples. The way (tuples of) terms interact with their environment makes proofs of soundness laborious and different from their affine counterparts from [7]. An up-to-context notion of bisimulation is proved to be sound, and to be quite useful when evaluating the distance between concrete programs.

• •

Finally, we show that the results from Section 5 can be lifted back to ordinary probabilistic $\lambda$-calculi from the literature [10, 5]. Both when call-by-name evaluation and call-by-value are considered, our framework can be naturally adapted, and helps in facilitating concrete proofs. This is in Section 6.

2 Metrics and Trivialisation, Informally

The easiest way to render the pure $\lambda$-calculus a universal probabilistic computation model [10] consists in endowing it with a binary construct $\oplus$ for probabilistic choice. The term $M\oplus N$ evolves as either $M$ or $N$, each with probability $\frac{1}{2}$. The obtained calculus can be given meaning by an operational semantics which puts terms in correspondence with distributions of values. The natural notion of observation, at least in an untyped setting like the one we will consider in this paper, is thus the probability of convergence of the observed term $M$, which will be denoted as ${\sum\nolimits_{\llbracket M\rrbracket}}$. One could then define a notion of context equivalence following Morris’ pattern, and stipulate that two terms $M$ and $N$ should be equivalent whenever they terminate with exactly the same probability when put in any context:

[TABLE]

The anatomy of the obtained notion of equivalence has been recently studied extensively, the by-products of this study being powerful techniques for it in the style of bisimilarity and logical relations [24, 5, 3].

As observed by various authors (see, e.g., [26] for a nice account), probabilistic programs and processes are naturally compared by metrics rather than equivalences: the latter do not give any quantitative information about how different two non-equivalent programs are. Given that the underlying notion of observation is inherently quantitative, on the other hand, generalizing context equivalence to a pseudometric turns out to be relatively simple:

[TABLE]

Observe that the obtained notion of context distance between two terms is a real number between [math] and $1$, which is minimal precisely when the considered terms are context equivalent. It is the least discriminating pseudometric which is non-expansive and adequate, and as such it provides some quite precise information about how far the two argument programs are, observationally. A similar notion has recently been studied by the authors [7], but only in a purely affine setting.

Let us now consider two prototypical examples of non-equivalent terms, namely $I=\lambda x.x$ (the identity) and $\Omega$ (the always-divergent term). The context distance $\delta^{c}(I,\Omega)$ between them is maximal: when applied, e.g., to the trivial context $[\cdot]$, they converge with probability $1$ and [math], respectively. A term which is conceptually “in the middle” of them is $M=I\oplus\Omega$. Indeed, in a purely affine $\lambda$-calculus, $\delta^{c}(I,M)=\delta^{c}(M,\Omega)=\frac{1}{2}$.

If we render the three terms duplicable (by putting them in the scope of a $!$-operator), however, the situation becomes much more complicated. Consider the terms $!I$ and $!(I\oplus\Omega)$. One can easily define a family of contexts $\{C_{n}\}_{n\in\mathbb{N}}$ such that the probability of convergence of $C_{n}[!I]$ and $C_{n}[!(I\oplus\Omega)]$ tend to $1$ and [math] (respectively) when $n$ tends to infinity. It suffices to take $C_{n}$ as (\lambda!x.\underbrace{x\ldots x}_{\mbox{n times}})[\cdot]. Allowing contexts to have the capability to duplicate their argument seems to mean that they can arbitrarily amplify distances. Indeed, the argument above also works when $(I\oplus\Omega)$ is replaced by any term which behaves as $\Omega$ with probability $\varepsilon$ and as $I$ with probability $1-\varepsilon$, provided of course $\varepsilon>0$. But how about $!\Omega$ and $!(I\oplus\Omega)$? Are they at maximal distance, i.e. is it that $\delta^{c}(!\Omega,!(I\oplus\Omega))=1$? Apparently, this is not the case. The previously defined contexts $C_{n}$ cannot amplify the “linear” distance between the two terms above, namely $\frac{1}{2}$, up to $1$. But what is the distance between $!\Omega$ and $!(I\oplus\Omega)$, then? Evaluating it is hard, since you need to consider all contexts, which do not have a nice structure. In Section 5, we will introduce a different, better behaved, notion of distance, this way being able to prove that, indeed, $\delta^{c}(!\Omega,!(I\oplus\Omega))=\frac{1}{2}$.

All this hints at even more difficult examples, like the one in which $M_{\varepsilon}=!{(\Omega\oplus^{\varepsilon}I)}$, where $\oplus^{\varepsilon}$ is the natural generalization of $\oplus$ to a possibly unfair coin flip, and one is interested in evaluating $\delta^{c}(M_{\varepsilon},M_{\mu})$. In that case, we can easily see that the ”linear” distance between them is $\lvert\varepsilon-\mu\rvert$. In some cases, it is possible to amplify it: the most natural way is again to consider the contexts $C_{n}$ defined above. Indeed, we see that the probabilities of convergence of $C_{n}[M]$ and $C_{n}[N]$ are $\varepsilon^{n}$ and $\mu^{n}$, respectively. It follows that $\delta^{c}(M_{\varepsilon},M_{\mu})\geq\sup_{n\in\mathbb{N}}{\lvert\varepsilon^{n}-\mu^{n}\rvert}$. For some $\varepsilon$ and $\mu$ (for example if $\varepsilon+\mu>1$), the context distance can be greater than $|\varepsilon-\mu|$. But there is no easy way to know how far amplification can lead us. The terms $M_{\varepsilon}$ and $M_{\mu}$ will be running examples in the course of this paper. Despite their simplicity, evaluating the distance between them is quite challenging.

We are also going to consider the case where contexts can evaluate terms in parallel, converging if and only if at least one of the copies converges. This behaviour is not expressible in the usual $\lambda$-calculus, but is captured by well-known constructs and in particular by Plotkin’s parallel disjunction [29]. In Section 4 below, we prove that all this is not accidental: the presence of parallel disjunction turns a non-trivialising metric into a trivialising one. The proof of it, by the way, relies on building certain amplifying contexts which are then shown to be universal using tools from functional analysis.

3 A Linear Probabilistic $\lambda$-Calculus

In this section, we present the syntax and operational semantics of our language $\Lambda_{\oplus}^{!,\parallel}$, on which we will later define metrics. $\Lambda_{\oplus}^{!,\parallel}$ is a probabilistic and linear $\lambda$-calculus, designed not only to allow copying, but to have a better control on it. It is based on a probabilistic variation of the calculus defined in [34], whose main feature is to never reduce inside exponential boxes. As we will see in Section 6, the calculus is capable of encoding both call-by-value and call-by-name fully-fledged probabilistic $\lambda$-calculi. We add a parallel disjunction construct to the calculus, being inspired by Plotkin’s parallel disjunction [29]. Noticeably, it has been recently shown [8] that adding parallel disjunction to a (non-linear) $\lambda$-calculus increases the expressive power of contexts to the point of enabling coincidence between the contextual preorder and applicative similarity. The choice of studying a very general calculus is motivated by our desire to be as general as possible. This being said, many of our results hold only in absence of parallel disjunction.

Definition 1

We assume a countable set of variables $\mathscr{X}$. The set of terms of $\Lambda_{\oplus}^{!,\parallel}$ (denoted $\mathscr{T}$) is defined by the following grammar:

[TABLE]

where $x\in\mathscr{X}$. The fragment of $\Lambda_{\oplus}^{!,\parallel}$ without the $\,\left([\cdot\parallel\cdot]\rightarrowtail\cdot\right)\,$ construct will be indicated as $\Lambda_{\oplus}^{!}$. Values are those terms derived from the following grammar:

[TABLE]

As already mentioned, $M\,\oplus\,N$ can evolve to either $M$ or $N$, each with probability $\frac{1}{2}$. The term $!{M}$ is a duplicable version of $M$, often called an (exponential) box. We have two distinct abstraction operators: $\lambda x.M$ is a linear abstraction, while the non-linear abstraction $\lambda{!{x}}.M$ requires exponential boxes as arguments. The term $\,\left([M\parallel N]\rightarrowtail L\right)\,$ behaves as $L$ if either $M$ or $N$ converges. Please observe that both abstractions and boxes are values—our notion of reduction is weak and surface [34].

We are now going to define an operational semantics for the closed terms of $\Lambda_{\oplus}^{!,\parallel}$ in a way similar to the one developed for a (non-linear) $\lambda$-calculus in [10]. We need to first define a family of approximation semantics, and then to take the semantics of a term as the least upper bound of all its approximations. The approximation semantics relation is denoted $M\Rightarrow\mathcal{D}$, where $M$ is a closed term of $\Lambda_{\oplus}^{!,\parallel}$, and $\mathcal{D}$ is a (sub)distribution on values with finite support, i.e., a function from $\mathscr{V}$ to $\mathbb{R}_{[0,1]}$ which sums to a real number $\sum_{\mathcal{D}}\leq 1$. For any distribution $\mathcal{D}$ on a set $X$, we call support of $\mathcal{D}$, and we note $\textsf{S}(\mathcal{D})$, the set $\{x\in X\mid\mathcal{D}(x)>0\}$. We say that $\mathcal{D}$ is finite if $\textsf{S}(\mathcal{D})$ is a finite set.

The rules deriving the approximation semantics relation are given in Figure 1, and are based on the notion of an evaluation context, which is an expression generated from the following grammar:

[TABLE]

As usual, $E[M]$ stands for the term obtained by filling the sole occurrence of $[\cdot]$ in $E$ with $M$. In Figure 1 and elsewhere in this paper, we indicate the distribution assigning probability $p_{i}$ to $V_{i}$ for every $i\in\{1,\ldots,n\}$ as $\{V_{1}^{p_{1}},\ldots,V_{n}^{p_{n}}\}$. Similarly for the expression $\{V_{i}^{p_{i}}\}_{i\in I}$, where $I$ is any countable index set. Observe how we first define a one-step reduction relation $\cdot\rightarrow\cdot$ between closed terms and sequences of terms, only later extending it to a small-step reduction relation $\cdot\Rightarrow\cdot$ between closed terms and distributions on values.

A reduction step can be a linear or non-linear $\beta$-reduction, or a probabilistic choice. Moreover, there can be more than one active redex in any closed term $M$, due to the presence of parallel disjunction. For any term $M$, the set of sub-distributions $\mathcal{D}$ such that $M\Rightarrow\mathcal{D}$ is a countable directed set. Since the set of sub-distributions (with potentially infinite support) is an $\omega$-complete partial order, we can define the semantics of a term $M$ as $\llbracket M\rrbracket=\sup\{\mathcal{D}\mid M\Rightarrow\mathcal{D}\}$. We could also define alternatively a big-step semantics, again in the same way as that of the probabilistic $\lambda$-calculus considered in [10].

Not all irreducible terms are values in $\Lambda_{\oplus}^{!,\parallel}$, e.g. $(\lambda{!{x}}.x)(\lambda x.x)$. We thus need a type-system which guarantees the absence of deadlocks. Since we want to be as general as possible, we consider recursive types as formulated in [2], which are expressive enough to type the image of the embeddings we will study in Section 6. The grammar of types is the following:

[TABLE]

Types are defined up to the equality $=^{\mathscr{A}}$, defined in Figure 2. $\sigma[\alpha\rightarrow\tau]$ stands for the type obtained by substituting all free occurrences of $\alpha$ by $\tau$ in $\sigma$.

An environment is a set of expressions in the form $x:\sigma$ or $!{x}:!{\sigma}$ in which any variable occurs at most once. Environments are often indicated with metavariables like $!\Gamma$, which stands for an environment in which all variables occur as $!{x}$, or $\Delta$ in which, on the contrary, only variables can occur, i.e. $\Delta$ is of the form $x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}$. Typing judgments are thus of the form $!\Gamma,\Delta\vdash M:\sigma$. The typing system is given in Figure 3. The role of this type system is not to guarantee termination, but rather to guarantee a form of type soundness:

Lemma 1

If $\vdash M:\sigma$ and $M\Rightarrow\mathcal{D}$, then $\vdash V:\sigma$ for every $V$ in the support of $\mathcal{D}$. Moreover, if $\vdash M:\sigma$ and $M$ is irreducible (i.e. $M\not\hookrightarrow N$ for every $N$), then $M$ is value.

Example 1

The term $I=\lambda x.x$ can be typed as $\vdash I:\sigma\multimap\sigma$ for every $\sigma\in\mathscr{A}$. We define ${\Omega_{!}}$ to be the term $(\lambda{!{x}}.x{!{x}})(!{(\lambda{!{x}}.x{!{x}})})$, which is the counterpart in our linear calculus of the prototypical diverging term of the $\lambda$-calculus, namely $\Omega=(\lambda x.xx)(\lambda x.xx)$. We can type this divergent term with any possible type: indeed, if we take $\tau::=\mu{\alpha}.!{\alpha}\multimap\sigma$, then $\tau=^{\mathscr{A}}!{\tau}\multimap\sigma$ and $\vdash\lambda{!{x}}.x{!{x}}:\sigma$. Using that, we can see that $\vdash{\Omega_{!}}:\sigma$ for every type $\sigma$. We will see in Section 6 that, more generally, there are several ways to turn any pure $\lambda$-term $M$ into a $\Lambda_{\oplus}^{!}$ term in such a way as to obtain meaningful typing and semantics: $\Lambda_{\oplus}^{!}$ is actually at least as powerful as the usual untyped probabilistic $\lambda$-calculus [10].

Termination could in principle be guaranteed if one considers strictly positive types, as we will do in Section 4.1 below. Let $\mathbb{D}$ be the set of dyadic numbers (i.e. those rational numbers in the form $\frac{n}{2^{m}}$ (with $n,m\in\mathbb{N}$ and $n\leq 2^{m}$). It is easy to derive, for every $\varepsilon\in\mathbb{D}$, a new binary operator on terms $\cdot\oplus^{\varepsilon}\cdot$ such that $\llbracket M\oplus^{\varepsilon}N\rrbracket=(1-\varepsilon)\llbracket M\rrbracket+\varepsilon\llbracket N\rrbracket$ for every closed $M,N$. It can be defined, e.g., as follows by induction on $m$:

[TABLE]

Example 2

We define here a family of terms that we use as a running example. We consider terms of the form $M_{\varepsilon}=!{(\Omega_{!}\oplus^{\varepsilon}I)}$, for $\varepsilon\in\mathbb{D}$. It holds that $\vdash M_{\varepsilon}:!{(\sigma\multimap\sigma)}$ for every $\sigma$. $M_{\varepsilon}$ corresponds to a duplicable term each copy of which behaves as $I$ with probability $\varepsilon$, and does not terminate with probability $1-\varepsilon$.

3.1 Some Useful Terminology and Notation

In this paper, we will make heavy use of sequences of terms and types. It is thus convenient to introduce some terminology and notation about them.

A finite (ordered) sequence whose elements are $e_{1},\ldots,e_{n}$ will be indicated as $\boldsymbol{e}=[e_{1},\ldots,e_{n}]$, and called an $n$-sequence. Metavariables for sequences are boldface variations of the metavariables for their elements. Whenever $E=\{i_{1},\ldots,i_{m}\}\subseteq\{1,\ldots,n\}$ and $i_{1}<\ldots<i_{m}$, the sub-sequence $[e_{i_{1}},\ldots,e_{i_{m}}]$ of an $n$-sequence $\boldsymbol{e}$ will be indicated as $\boldsymbol{e}_{E}$. If the above holds, $E$ will be called an $n$-set. If $\boldsymbol{e}$ is an $n$-sequence, and $\varphi$ is a permutation on $\{1,\ldots,n\}$, we note $e_{\varphi}$ the $n$-sequence $[e_{\varphi(1)},\ldots,e_{\varphi{(n)}}]$. We can turn an $n$-sequence into a $(n+1)$-sequence by adding an element at the end: this is the role of the semicolor operator. We denote by $[e^{n}]$ the $n$-sequence where all components are equal to $e$.

Whenever this does not cause ambiguity, notations like the ones above will be used in conjunction with syntactic constructions. For example, if $\boldsymbol{\sigma}$ is an $n$-sequence of types, then $!{\boldsymbol{\sigma}}$ stands for the sequence $[!{\sigma_{1}},\ldots,!{\sigma_{n}}]$. As another example, if $\boldsymbol{\sigma}$ is an $n$-sequence of types and $E$ is an $n$-set, then $\boldsymbol{x}_{E}:\boldsymbol{\sigma}_{E}$ stands for the environment assigning type $\sigma_{i}$ to $x_{i}$ for every $i\in E$. As a final example, if $\boldsymbol{M}$ is an $n$-sequence of terms and $\boldsymbol{\sigma}$ is an $n$-sequence of types, $\vdash\boldsymbol{M}:\boldsymbol{\sigma}$ holds iff $\vdash M_{i}:\sigma_{i}$ is provable for every $i\in\{1,\ldots,n\}$.

3.2 Context Distance

A context of type $\sigma$ for terms of type $\tau$ is a term $C$ which can be typed as $\mathit{hole}\,:\,\tau\vdash C:\sigma$, where $\mathit{hole}$ is a distinguished variable. $\mathcal{C}^{\tau}_{\sigma}$ collects all such terms. If $C\in\mathcal{C}^{\tau}_{\sigma}$ and $M$ is a closed term of type $\tau$, then the closed term $C\{\mathit{hole}/M\}$ has type $\sigma$ and is often indicated as $C[M]$.

The context distance [7] is the natural quantitative refinement of context equivalence. Intuitively, it corresponds to the maximum separation that contexts can induce between two terms. Following [7], we take as observable the probability of convergence: for any term $M$, we define its observable $\text{Obs}(M)$ as ${\sum\nolimits_{\llbracket M\rrbracket}}$. Then, for any terms $M$, $N$ such that $\vdash M:\sigma$ and $\vdash N:\sigma$, we define:

[TABLE]

Please observe that this distance is a pseudometric, and that moreover we can recover context equivalence by considering its kernel, that is the set of pairs of terms which are at distance [math]. The binary operator $\delta^{c}_{\sigma,!}$ is defined similarly, but referring to terms (and contexts) from $\Lambda_{\oplus}^{!}$.

Example 3

What can we say about ${\delta_{\sigma,!{},\parallel}^{c}}(M_{\varepsilon},M_{\mu})$? Not much apparently, since all contexts should be considered. Even if we put ourselves in the fragment $\Lambda_{\oplus}^{!}$, the best we can do is to conclude that ${\delta^{c}_{\sigma,!}}(M,N)\geq\sup_{n\in\mathbb{N}}\lvert\varepsilon^{n}-\mu^{n}\rvert$, as explained in Section 2.

4 On Trivialisation

As we have already mentioned, there can well be classes of terms such that the context distance collapses to context equivalence, due to the copying abilities of the language. The question of trivialisation can in fact be seen as a question about the expressive power of contexts: given two duplicable terms, how much can a context amplify the observable differences between their behaviours?

More precisely, we would like to identify trivialising fragments of $\Lambda_{\oplus}^{!,\parallel}$, that is to say fragments such that for any pair of duplicable terms, their context distance (with respect to the fragment) is either 0 or 1. This is not the case in $\Lambda_{\oplus}^{!}$ (see Example 9 below).

In fact, a sufficient condition to trivialization is to require the existence of amplification contexts: for every observable type $\sigma$, for every $\alpha,\beta\in[0,1]$ distinct, for every $\gamma>0$, we want to have a context $C_{\sigma}^{\alpha,\beta,\gamma}$ such that:

[TABLE]

Fact 1

Any fragment of $\Lambda_{\oplus}^{!,\parallel}$ admitting all amplifications contexts trivializes.

4.1 Strictly Positive Types

First, let us consider the case of the fragment $\Lambda_{\oplus}^{!,\downarrow}$ of $\Lambda_{\oplus}^{!}$ obtained by considering strictly positive types, only (in a similar way to [2]), and by dropping parallel disjunction. Every term $M$ of $\Lambda_{\oplus}^{!,\downarrow}$ is terminating (i.e. $\sum\llbracket M\rrbracket=1$), so we need to adapt our notion of observation: we define the type $\mathbb{B}=!{\alpha}\multimap!{\alpha}\multimap\alpha$, which can be seen as boolean type using a variant of the usual boolean encoding in $\lambda$-calculi. Our new notion of observation, defined only at type $\mathbb{B}$, is $\text{Obs}(M)={\sum\nolimits_{\llbracket M!{I}!{{\Omega_{!}}}\rrbracket}}$, which corresponds to the probability that $M$ evaluates to true. While this notion of observation uses the full power of $\Lambda_{\oplus}^{!}$, the context distance $\delta_{!{},\downarrow}^{c}$ based on it only consider contexts in $\Lambda_{\oplus}^{!,\downarrow}$.

Theorem 1

$\delta_{!{},\downarrow}^{c}$* trivialises.*

The proof of Theorem 1 is based on the construction of amplification contexts. We are going to use Bernstein constructive proof of the Stone-Weierstrass theorem. Indeed, Bernstein showed that for every continuous function $f:[0,1]\rightarrow\mathbb{R}$, the following sequence of polynomials converges uniformly towards $f$:

[TABLE]

Let us consider the following continuous function: we fix $f(\alpha)=0$, $f(\beta)=1$, and $f$ defined elsewhere in such a way that it is continuous, that it has values in $[0,1]$, and that moreover $f(\mathbb{Q})\subseteq\mathbb{Q}$. We can easily implement $P_{n}^{f}$ by a context, i.e. define $C$ such that for every $M$, $\text{Obs}(C[M])=P_{n}^{f}(\text{Obs}(M))$. In $\Lambda_{\oplus}^{!,\downarrow}$, we can indeed copy an argument $n$ times, then evaluate it, and then for every $k$ between [math] and $n$, if the number of trues obtained is exactly $k$, return the term $\textbf{false}\oplus^{f(\frac{k}{n})}\textbf{true}$ (that corresponds to a term returning true with probability ${f\left(\frac{k}{n}\right)}$). Please observe that this construction works only because in $\Lambda_{\oplus}^{!,\downarrow}$ all terms converge with probability $1$.

4.2 Parallel Disjunction

As we have seen, trivialization can be enforced by restricting the class of terms, but we can also take the opposite road, namely increasing the discriminating power of contexts. Indeed, consider the full language $\Lambda_{\oplus}^{!,\parallel}$, with the usual notion of observation.

We can first see how parallel disjunction increases the expressive power of the calculus on a simple example. Consider the following two terms: $M=!{\Omega_{!}}$ and $N=!{(\Omega_{!}\,\oplus\,I)}$. We will see later that these two terms are the simplest example of non-trivialization in $\Lambda_{\oplus}^{!}$: indeed ${\delta^{c}_{!{(\tau\multimap\tau)},!}}(M,N)=\frac{1}{2}$, while ${\delta_{!{(\tau\multimap\tau)},!{},\parallel}^{c}}(M,N)=1$. In $\Lambda_{\oplus}^{!,\parallel}$, we are able to define a family of contexts $(C_{n})_{n\in\mathbb{N}}$ as follows:

[TABLE]

Essentially, $C_{n}$ makes $n$ copies of its argument, and then converges towards $I$ if at least one of these copies itself converges. When we apply the context $C_{n}$ to $M$ and $N$, we can see that the convergence probability of $C_{n}[M]$ is always [math] independently of $n$, whereas the convergence probability of $C_{n}[N]$ tends towards $1$ when $n$ tends to infinity.

Theorem 2

$\delta_{!{},\parallel}^{c}$* trivializes.*

The proof is based on the construction of amplification contexts $C_{\sigma}^{\alpha,\beta,\gamma}$. If $\max(\alpha,\beta)=1$, we can extend the informal argument from Section 2, by taking contexts that copy an arbitrary number of times their argument. If $\min(\alpha,\beta)=0$, we can use the same idea as in the example above, by taking contexts that do an arbitrary number of disjunctions. What remains to be done to obtain the trivialization result is treating the case in which $0<\alpha,\beta<1$. The overall idea is to somehow mix the contexts we use in the previous cases. More precisely, we define a family of contexts $(C_{n}^{m})_{n,m\in\mathbb{N}}$ as follows:

[TABLE]

where

[TABLE]

The term ${\bigvee}^{n}(M_{1},\ldots,M_{n})$ behaves as a $n$-ary disjunction: it terminates if at least one of the $M_{i}$ terminates. On the other hand, ${\bigwedge}^{n}(M_{1},\ldots,M_{n})$ can be seen as a $n$-ary conjunction: it terminates if all the $M_{i}$ terminates. The contexts $C_{n}^{\alpha}$ compute $m$-ary conjunctions of $n$-ary disjunction. Now, let $\iota$ be such that $\alpha<\iota<\beta$. We need to show that for every $n$, we can choose $m(n,\iota)\in\mathbb{N}$ such that:

[TABLE]

We can express this problem purely in terms of functional analysis, by observing that $\text{Obs}(C_{n}^{m}[!{M}])=(1-(1-\text{Obs}(M))^{m})^{n}$. We are now going to show the result by applying the dominated convergence theorem to a well-chosen sequence of functions.

We choose $m(n,\gamma)=\lceil r(n,\iota)\rceil$, with

[TABLE]

Now, we see that $\text{Obs}(C_{n}^{m(n,\iota)}[!{M}])$, is equal to $f_{n,\iota}(\text{Obs}(M))$, where $f_{n,\iota}$ is the real function defined by:

[TABLE]

The result we are trying to show can now be expressed by way of the following lemma:

Lemma 2

[TABLE]

• Proof.

In order to simplify the proof, we show an equivalent result on $g_{n,\alpha}(x)=f_{n,1-\alpha}(1-x)$. Lemma 2 is equivalent to say that: $\lim_{n\rightarrow\infty}g_{n,\alpha}(x)=\begin{cases}1\text{ if }x<\alpha,\\ 0\text{ if }x>\alpha.\end{cases}$ We express $g$ as an integral, since we want to use known results about inversion of integral and limits:

[TABLE]

We can now express our goal using $g^{\prime}$: we have to show that

[TABLE]

We first establish a bound on the $g^{\prime}_{n,\alpha}$:

[TABLE]

And consequently:

[TABLE]

We have to use the following well-known inequality, that we recall here:

[TABLE]

For every $x<\alpha$, we’re going to use the bounded convergence theorem, which is a well-known theorem in real analysis, on $[0,x]$ and on $[x,1]$ for every $x>\alpha$ . We recall this theorem here:

Theorem 3** (Bounded Convergence Theorem)**

If ${k_{n}}$ is a sequence of uniformly bounded real-valued measurable functions which converges pointwise on a bounded measure space $(S,\Sigma,\mu)$ to a function $k$, then the limit $k$ is an integrable function and: $\int_{S}{\lim_{n\rightarrow\infty}k_{n}}=\lim_{n\rightarrow\infty}\int_{S}k_{n}$.

• •

Let’s first take $0\leq x<\alpha$. Here, we take $(S,\Sigma,\mu)$ as the segment $[0,x]$ with the Lebesgue measure (corresponding to the usual notion of integration on real functions). We obtain using (1), that for every $t\in[0,x]$, it holds:

[TABLE]

where $K$ is a constant. We can already see that $g^{\prime}_{n,\alpha}$ converge pointwise to the [math]-function on $[0,x]$ (using (2)). We’re now going to show it’s bounded. Using the fact that $t\leq x$, we obtain:

[TABLE]

Please observe that the $\max$ is well-defined and $<\infty$ because the sequence $n\cdot\left(\frac{x}{\alpha}\right)^{n-1}$ has a finite limit (by (2)). So we have achieved to bound $g^{\prime}_{n,\alpha}(t)$ by a constant depending neither on $t$ nor on $n$. Consequently, we can apply the bounded convergence theorem, and we obtain :

[TABLE]

• •

Now we consider the case where $\alpha<x\leq 1$. Here, we take $(S,\Sigma,\mu)$ as the segment $[0,x]$ with the Lebesgue measure. By using 1, we can see that for every $t\in[x,1]$:

[TABLE]

Using 2 (and doing several computation), we can see that for every $a,b>1$, it holds that:

[TABLE]

By applying this, we obtain:

[TABLE]

Now, please observe that 4 gives us both the pointwise limit and the uniform bound (since $g_{n,\alpha}(t)$ is bounded by a sequence that doesn’t depends on t, and has a finite limit when n goes towards infinity). So we can apply the bounded convergence theorem, and we obtain that:

[TABLE]

This concludes the proof $\Box$

5 Tuples and Full Abstraction

This section is structured as follows: first, we define a labelled Markov chain (LMC) which expresses the semantics of our calculus in an interactive way, and then we use it to give a coinductively defined notion of distance on an LTS of distributions, which coincides with the context distance as defined in Section 3.2. We are not considering parallel disjunction here: the motivations for that should be clear from Theorem 2.

5.1 A Labelled Markov Chain over Tuples

Labelled Markov chains are the probabilistic analogues to labelled transition systems. Formally, a LMC is a triple $\mathscr{M}=(\mathcal{S},\mathcal{A},\mathcal{P})$, where $\mathcal{S}$ is a countable set of states, $\mathcal{A}$ is a countable set of labels, and $\mathcal{P}:\mathcal{S}\times\mathcal{A}\rightarrow{\text{Distr}(\mathcal{S})}$ is a transition probability matrix (where $\text{Distr}(X)$ is the set of all distributions over $X$).

Following [9], the interactive behaviour of probabilistic $\lambda$-terms can be represented by an LMC whose states are the terms of the language, whose actions are values, and where doing the action $V$ starting from a state $M$ corresponds to applying the value $V$ to $M$. This approach is bound not to work in presence of pairs when metrics take the place of equivalences, due to the unsoundness of projective actions. In [7], this observation lead us to introduce a new LMC whose states are tuples of terms, and whose actions include one splitting a pair: $\mathcal{P}(\left[\langle M,N\rangle\right])({\text{destruct}})={\{{\left[M,N\right]}^{1}\}}$. This turns out to work well in an affine setting [7]. We are going to define a LMC $\mathscr{M}_{\oplus}^{!{}}=(\mathcal{S}_{\mathscr{M}_{\oplus}^{!{}}},\mathcal{A}_{\mathscr{M}_{\oplus}^{!{}}},\mathcal{P}_{\mathscr{M}_{\oplus}^{!{}}})$ which is an extension of the one from [7], and which is adapted to a language with copying capabilities. The idea is to treat exponentials in the spirit of Milner’s Law: $!{A}\multimap A\otimes!{A}$.

5.1.1 States

Tuples are pairs of the form $K=(\boldsymbol{M},{\boldsymbol{V}})$ where ${\boldsymbol{M}}$ and $\boldsymbol{V}$ are a sequence of terms and values, respectively. The set of all such tuples is indicated as $\mathscr{U}$. The first component of a tuple is called its exponential part, while the second one is called its linear part. We write $\vdash(\boldsymbol{M},\boldsymbol{V}):(\boldsymbol{\sigma},\boldsymbol{\tau})$ if $\vdash\boldsymbol{M}:\boldsymbol{\sigma}$ and $\vdash\boldsymbol{V}:\boldsymbol{\tau}$. We note $\mathbf{T}$ the set of pairs $A=(\boldsymbol{\sigma},\boldsymbol{\tau})$, and we call tuple types the elements of $\mathbf{T}$. Moreover, we say that $(\boldsymbol{\sigma},\boldsymbol{\tau})$ is a $(n,m)$ tuple type if $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ are, respectively, an $n$-sequence and an $m$-sequence. To any term $M$, we associate a tuple in a natural way: we note $\dot{M}$ the tuple $(\left[\right],\left[M\right])$, and similarly if $\sigma$ is a type, we indicate the tuple type $(\left[\right],\left[\sigma\right])$ as $\dot{\sigma}$. Please observe that if $\vdash M:\sigma$, then it holds that $\vdash\dot{M}:\dot{\sigma}$.

A sequence of the form $(E,F,\boldsymbol{\sigma},\boldsymbol{\tau},M,\gamma)$ is said to be an applicative typing judgment when $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ are, respectively, an $n$-sequence and an $m$-sequence of types, $E$ and $F$ are respectively an $n$-set and an $m$-set, and moreover it holds that $!{\boldsymbol{x}_{E}}:!{\boldsymbol{\sigma}_{E}},\boldsymbol{y}_{F}:\boldsymbol{\tau}_{F}\vdash M:\gamma$. Intuitively, this means that if we have a tuple $K=(\boldsymbol{N},\boldsymbol{V})$ of type $(\boldsymbol{\sigma},\boldsymbol{\tau})$, we can replace free variables of $M$ by some of the terms from $K$. More precisely, we can replace variables in linear position by the $V_{i}$ with $i\in F$, and variables in non linear position by $N_{j}$, with $j\in E$. We note as $M[K]$ the closed term of type $\gamma$ that we obtain this way. We note $\mathscr{J}$ the set of all applicative typing judgments. We are specially interested in those judgments $(E,F,\boldsymbol{\sigma},\boldsymbol{\tau},M,\gamma)$ in $\mathscr{J}$ such that for every tuple $K$, the resulting term $M[K]$ is a value: that is when either $M=y_{i}$ for a $i\in\mathbb{N}$, or $M$ is of the form $\lambda z.N$, $\lambda{!{z}}.N$, or $!{N}$. We note $\mathscr{J}^{\mathscr{V}}$ the set of those judgments.

We are now in a position to define $\mathscr{M}_{\oplus}^{!{}}$ formally. The set of its states is indeed defined as $\mathcal{S}_{\mathscr{M}_{\oplus}^{!{}}}=\{(K,A)\mid K\in\mathscr{U},\,A\in\mathbf{T},\,\,\vdash K:A\}.$

5.1.2 Labels and Transitions

How do states in $\mathcal{S}_{\mathscr{M}_{\oplus}^{!{}}}$ interact with the environment? This is captured by the labels in $\mathcal{A}_{\mathscr{M}_{\oplus}^{!{}}}$, and the associated probability matrix. We define $\mathcal{A}_{\mathscr{M}_{\oplus}^{!{}}}$ as the disjoint union of ${\mathcal{A}_{?}}$, $\mathcal{A}_{{!}}$ and $\mathcal{A}_{@}$, where:

[TABLE]

In order to distinguish actions in $\mathcal{A}_{{!}}$ and ${\mathcal{A}_{?}}$, we write the action $i\in\mathbb{N}$ as $({?}^{i})$ if it comes from ${\mathcal{A}_{?}}$, and as $(!^{i})$ if it comes from $\mathcal{A}_{{!}}$. The action $(\kappa,i)\in\mathcal{A}_{@}$ is often indicated as $@^{i}_{\kappa}$. The probability matrix $\mathcal{P}_{\mathscr{M}_{\oplus}^{!{}}}$ is defined formally in Figure 4. We give below some intuitions about it. The general idea is that $\mathscr{M}_{\oplus}^{!{}}$ is designed to express every possible effect that a context can have on tuples. ${\mathcal{A}_{?}}$ and $\mathcal{A}_{{!}}$ are designed to model copying capabilities, while $\mathcal{A}_{@}$ corresponds to applicative interactions.

Actions in ${\mathcal{A}_{?}}$ take any term of the form $!{M}$ from the linear part of the underlying tuple, unbox it and transfer $M$ to the exponential part of the tuple. Please observe that this action is in fact deterministic: the resulting tuple is uniquely determined. Labels in $\mathcal{A}_{{!}}$, on the other hand, model the act of copying terms in the exponential part. We call its elements Milner’s actions. More specifically, the action $(!^{i})$ takes the $i$-th term in the exponential part of the tuple, makes a copy of it, evaluates it and adds the result to the linear part. Please observe that, contrary to $({?}^{i})$, this action can have a probabilistic outcome: the transferred term is evaluated.

Labels in $\mathcal{A}_{@}$ are analogues of the applicative actions from applicative bisimulation over terms (see, e.g. [9]). As such, they model environments passing arguments to programs. Here, we have to adapt this idea to our tuple framework: indeed, we can see the tuple as a collection of programs available to the environment, who is free to choose with which of the programs to interact with by passing it an argument. This argument, however, could depend on other components of the tuple, which need to be removed from it if lying in its linear part. Finally, please observe that all this should respect types. Labels in $\mathcal{A}_{@}$ are indeed defined as a pair of an index $i$ corresponding to the position in the tuple of the term the environment chooses, and an applicative typing judgment, used to specify the argument. Please observe that in the definition of probability matrix for applicative actions, in Figure 4, the condition on $i$ implies that the $i$-th linear component of the tuple is not used to construct the argument term.

Example 4

We give in Figure 5 a fragment of $\mathscr{M}_{\oplus}^{!{}}$ illustrating our definitions on an example. Let $\tau$ be an element of $\mathscr{A}$. We consider terms of the form $M_{\varepsilon}=!{(\Omega_{!}\oplus^{\varepsilon}I)}$, for $\varepsilon\in\mathbb{D}$ and we look at some of the possible evolutions in $\mathscr{M}_{\oplus}^{!{}}$ from the associated state $(\dot{M_{\varepsilon}},\dot{!{({\tau\multimap\tau})}})=(\left[\right],\left[M_{\varepsilon}\right]),(\left[\right],\left[!{({\tau\multimap\tau})}\right])$. In Figure 5, we denote by $\sigma$ the type $\tau\multimap\tau$.

5.2 Distributions as States

Now that we have a LMC $\mathcal{P}_{\mathscr{M}_{\oplus}^{!{}}}$ modelling interaction between (tuple of) terms and their environment, we could define notions of metrics following one of the abstract definitions from the literature, e.g. by defining the trace distance or the behavioural distance between terms. This is, by the way, the approach followed in [7]. We prefer, however, to first turn $\mathcal{P}_{\mathscr{M}_{\oplus}^{!{}}}$ into a transition system $\mathscr{L}_{\oplus}^{!{}}$ whose states are distributions of tuples. This supports both a simple, coinductive presentation of the trace distance, but also up-to techniques, as we will see in Section 5.6 below. Both will be very convenient when evaluating the distance between concrete terms, e.g. our running example.

It turns out that the usual notion of an LTS is not sufficient for our purposes, since it lacks a way to expose the observables of each state, i.e., its sum. We thus adopt the following definition:

Definition 2

A weighted labelled transition system (WLTS for short) is a quadruple in the form $\mathscr{L}=(\mathcal{S},\mathcal{A},{}{\stackrel{{\scriptstyle\cdot}}{{\rightarrow}}}{},w)$ where:

• •

$\mathcal{S}$* is a set of states and $\mathcal{A}$ is a countable set of actions,*

• •

${}{\stackrel{{\scriptstyle\cdot}}{{\rightarrow}}}{}$* is a transition function, such that, for every $t\in\mathcal{S}$ and $a\in\mathcal{A}$, there exists at most one $s\in\mathcal{S}$, such that ${t}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{s}$,*

• •

$w:\mathcal{S}\rightarrow[0,1]$.

Please observe how WLTSs are deterministic transition systems. We define the WLTS $\mathscr{L}_{\oplus}^{!{}}$ by way of the equations in Figure 6.

If $t=(\mathcal{D},A)$ is in $\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$, we say that $t$ is a $A$-state. It is easy to check that $\mathscr{L}_{\oplus}^{!{}}$ is nothing more than the natural way to turn $\mathcal{P}_{\mathscr{M}_{\oplus}^{!{}}}$ into a deterministic transition system. We illustrate this idea in Figure 7, by giving a fragment of $\mathscr{L}_{\oplus}^{!{}}$ corresponding to (part of) the fragment of $\mathscr{M}_{\oplus}^{!{}}$ given in Example 4.

5.3 A Coinductively Defined Metric

Following Desharnais et al. [13], we use a quantitative notion of bisimulation on $\mathscr{L}_{\oplus}^{!{}}$ to define a distance between terms. The idea is to stipulate that, for any $\varepsilon\in[0,1]$, a relation $\mathrel{R}$ is an $\varepsilon$-bisimulation if it is, somehow, $\varepsilon$-close to a bisimulation. The distance between two states $t$ and $s$ is just the smallest $\varepsilon$ such that $t$ and $s$ are $\varepsilon$-bisimilar. However, while in [13] the notion of $\varepsilon$-bisimulation is local, we want it to be more restricted by the global deviation we may accept considering arbitrary sequences of actions.

Definition 3

Let $\mathscr{L}=(\mathcal{S},\mathcal{A},{}{\stackrel{{\scriptstyle\cdot}}{{\rightarrow}}}{},w)$ be a WLTS. Let $\mathrel{R}$ be a symmetric and reflexive relation on $\mathcal{S}$, and $\varepsilon\in[0,1]$. $\mathrel{R}$ is a $\varepsilon$-bisimulation whenever the following two conditions hold:

• •

if $t\,{\mathrel{R}}\,s$, and ${t}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{u}$, then there exists $v$ such that ${s}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{v}$, and it holds that $u\,{\mathrel{R}}\,v$.

• •

if $t\,{\mathrel{R}}\,s$, then $\lvert w(t)-w(s)\rvert\leq\varepsilon$.

For every $\varepsilon\in[0,1]$, there exists a largest $\varepsilon$-bisimulation, that we indicate as $\mathrel{R}^{\varepsilon}$. Please observe that it is not an equivalence relation (since it is not transitive). We can now define a metric on $\mathcal{S}$ : ${\delta^{b}_{\mathscr{L}}}(t,s)=\inf{\left\{\varepsilon\mid t\,{\mathrel{R}^{\varepsilon}}\,s\right\}}$.

The greatest lower bound is in fact reached as a ${\delta^{b}_{\mathscr{L}}}(t,s)$-bisimulation: that’s the sens of the following lemma.

Lemma 3

Let $t,s\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$. Then ${\delta^{b}_{\mathscr{L}}}(t,s)\leq\varepsilon$ if and only if $t\,{\mathrel{R}^{\varepsilon}}\,s$.

• Proof.

The right-to-left implication is given by the definition of $\delta^{b}_{\mathscr{L}}$. The other one comes from the fact that the relation $\mathrel{R}$ given by $t\,{\mathrel{R}}\,s$ if ${\delta^{b}_{\mathscr{L}}}(t,s)\leq\varepsilon$ is a $\varepsilon$-bisimulation. $\Box$

As a corollary, it is easy to see that the infinum in Definition 3 is in fact reached.

How can we turn $\delta^{b}_{\mathscr{L}}$ into a metric on terms? The idea is to consider the distributions on tuples one naturally gets when evaluating the term. To every term $M$ of type $\sigma$, we define $\hat{s}_{\sigma}(M)\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$ as $(\{{\dot{V}}^{\llbracket M\rrbracket(V)}\}_{V\in\mathscr{V}},\dot{\sigma}).$

Definition 4

For every terms $M$ and $N$ such that $\vdash M:\sigma$ and $\vdash N:\sigma$, we set ${\delta_{\sigma,!{}}^{b}}(M,N)={\delta^{b}_{\mathscr{L}_{\oplus}^{!{}}}}(\hat{s}_{\sigma}(M),\hat{s}_{\sigma}(N))$.

Example 5

Consider again the terms $M_{\varepsilon}$ from Example 2. We fix a type $\tau$, and define $\sigma=\tau\multimap\tau$. As mentioned in Example 2, it holds that $\vdash M_{\varepsilon}:!{\sigma}$. Let now $\varepsilon,\mu,\alpha$ be in $[0,1]$, and let $\mathrel{R}$ be any $\alpha$-bisimulation, such that $\hat{s}_{!{\sigma}}(M_{\varepsilon})\,{\mathrel{R}}\,\hat{s}_{!{\sigma}}(M_{\mu})$. Let $\{t_{i}\}_{i\in\mathbb{N}}$, and $\{s_{i}\}_{i\in\mathbb{N}}$ be families from $\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$ such that ${\hat{s}_{!{\sigma}}(M_{\varepsilon})}{\stackrel{{\scriptstyle({?}^{1})}}{{\rightarrow}}}{{t_{0}}{\stackrel{{\scriptstyle(!^{1})}}{{\rightarrow}}}{{\ldots}{\stackrel{{\scriptstyle(!^{1})}}{{\rightarrow}}}{t_{i}\ldots}}}$ and ${\hat{s}_{!{\sigma}}(M_{\mu})}{\stackrel{{\scriptstyle({?}^{1})}}{{\rightarrow}}}{{s_{0}}{\stackrel{{\scriptstyle(!^{1})}}{{\rightarrow}}}{{\ldots}{\stackrel{{\scriptstyle(!^{1})}}{{\rightarrow}}}{s_{i}\ldots}}}$. Since $\mathrel{R}$ is an $\alpha$-bisimulation, for every $i$, it holds that $t_{i}\,{\mathrel{R}}\,s_{i}$. Looking at the definition of $\mathscr{L}_{\oplus}^{!{}}$, it is easy to realise that:

[TABLE]

By the definition of a $\alpha$-bisimulation, we see that this implies that $\alpha\geq\lvert\varepsilon^{i}-\mu^{i}\rvert$. Since this reasoning can be done for every $\alpha$ such that $M_{\varepsilon}$ and $M_{\mu}$ are $\alpha$-bisimilar, it means that: ${\delta_{!{\sigma},!{}}^{b}}(M_{\varepsilon},M_{\mu})\geq\sup_{i\in\mathbb{N}}\lvert\varepsilon^{i}-\mu^{i}\rvert$. Moreover, if we consider the special case where $\varepsilon=0$, we can actually construct a $\mu$-bisimulation by taking

[TABLE]

*We can easily check that $\mathrel{R}$ is indeed a $\mu$-bisimulation, which tells us that ${\delta_{!{\sigma},!{}}^{b}}(M_{0},M_{\mu})=\mu$. *

In Section 5.5 below, we will prove that $\delta_{\sigma,!{}}^{b}$ coincides with $\delta^{c}_{\sigma,!}$. While, as we will see soon, this helps a lot when precisely evaluating the distance between terms, sometime a characterization of $\delta_{\sigma,!{}}^{b}$ by traces is very effective when deriving lower bounds on the distance between terms (see, e.g., Section 5.4).

5.4 A Trace Characterization

In this section, we will characterize the metric defined in the previous section in an inductive way, by way of traces. This will be useful when proving full abstraction. A trace is a (possibly empty) sequence of actions in $\mathcal{A}_{\mathscr{L}_{\oplus}^{!{}}}$. Formally, the set of traces is generated by the following grammar:

[TABLE]

If $\mathsf{T}\in\mathscr{T}$, and $t\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$, we write ${t}{\stackrel{{\scriptstyle\mathsf{T}}}{{\rightarrow}}}{s}$ if $\mathsf{T}=a_{1},\ldots,a_{n}$ and there exists a sequence of states $t_{0},\ldots,t_{n}$ where $t_{0}=t$, $t_{n}=s$, and moreover for every $1\leq i<n$, it holds that ${t_{i-1}}{\stackrel{{\scriptstyle a_{i}}}{{\rightarrow}}}{t_{i}}$. A trace $\mathsf{T}$ is said to be * admissible * for $t$ if there exists $s$ such that ${t}{\stackrel{{\scriptstyle\mathsf{T}}}{{\rightarrow}}}{s}$. The set of admissible traces for $t$ is indicated as $\mathcal{A}(t)$. The following is a well-posed definition, because the underlying WLTS $\mathscr{L}_{\oplus}^{!{}}$ is by definition deterministic.

Definition 5

Let be $t\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$, and $\mathsf{T}\in\mathcal{A}(t)$. Then there is a unique $u$ such that ${t}{\stackrel{{\scriptstyle\mathsf{T}}}{{\rightarrow}}}{u}$, and we define the success probability of $\mathsf{T}$ starting from $t$, that we note $\mathsf{PR}_{\mathsf{T}}(t)$, as $w(u)$.

We can express the metric $\delta^{b}_{\mathscr{L}_{\oplus}^{!{}}}$ as the maximum separation that a trace can induce:

Proposition 1

Let $t,s\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$. Then:

[TABLE]

• Proof.

We show separately the two inequalities:

• •

First, if two states $t$ and $s$ are related by an $\varepsilon$-bisimulation, we can see that $\lvert\mathsf{PR}_{\mathsf{T}}(t)-\mathsf{PR}_{\mathsf{T}}(s)\rvert\leq\varepsilon$ (since the states obtained after having done every action in $\mathsf{T}$ are still $\varepsilon$-bisimilar).

• •

To show the other implication, it is sufficient to define, for every $\varepsilon$, a relation imposing a bound $\varepsilon$ on the success probabilities of traces, and to show that it is a $\varepsilon$-bisimulation.

$\Box$

Please observe that Proposition 1 gives an inductive definition of $\delta_{!{}}^{t}$, while the notion of $\varepsilon$-bisimulation is defined coinductively.

We conclude this section by stating a corollary of Proposition 1 which will be useful in the following.

Corollary 1

Let be $M$ and $N$ of type $\sigma$, such that $\hat{s}_{\sigma}(M)$ and $\hat{s}_{\sigma}(N)$ are not $\varepsilon$-bisimilar. Then there exists a trace $\mathsf{T}$ such that $\lvert\mathsf{PR}_{\mathsf{T}}(\hat{s}_{\sigma}(M))-\mathsf{PR}_{\mathsf{T}}(\hat{s}_{\sigma}(N))\rvert\geq\varepsilon$.

5.5 Full Abstraction

In this section, we prove that $\delta_{\sigma,!{}}^{b}$ coincides with $\delta^{c}_{\sigma,!}$.

5.5.1 Soundness

We first of all show that the metric $\delta_{\sigma,!{}}^{b}$ is sound with respect to $\delta^{c}_{\sigma,!}$, i.e. that $\delta_{\sigma,!{}}^{b}$ discriminates at least as much as $\delta^{c}_{\sigma,!}$:

Theorem 4** (Soundness)**

For any terms $M$ and $N$ of $\Lambda_{\oplus}^{!}$, such that $\vdash M:\sigma$ and $\vdash N:\sigma$, it holds that ${\delta^{c}_{\sigma,!}}(M,N)\leq{\delta_{\sigma,!{}}^{b}}(M,N)$.

The rest of this section is devoted to the proof of Theorem 4. Please remember that our definition of the tuple distance is based on the notion of $\varepsilon$-bisimulation. Proving the soundness theorem, thus, requires us to show that for any terms $M$ and $N$ of type $\sigma$ such that $\hat{s}_{\sigma}(M)$ and $\hat{s}_{\sigma}(N)$ are $\varepsilon$-bisimilar, and for any $\tau\in\mathscr{A},C\in\mathcal{C}^{\sigma}_{\tau}$, it holds that $\mid{\sum\nolimits_{\llbracket C[M]\rrbracket}}-{\sum\nolimits_{\llbracket C[N]\rrbracket}}\mid\leq\varepsilon$.

Our proof strategy is based on the fact that we can decompose every evaluation path of a term in the form $C[L]$ into external reduction steps (that is, steps that do not affect $L$), and internal reduction steps (that is, reduction steps affecting $L$, but which can be shown to correspond only to actions from $\mathscr{L}_{\oplus}^{!{}}$). Intuitively, if we reduce in parallel $C[M]$ and $C[N]$, we are going to have steps where only the context is modified (and the modification does not depend on whether we are considering the first program or the second), and steps where the internal part is modified, but these steps cannot induce too much of a difference between the two programs, since the two internal terms are $\varepsilon$-bisimilar.

We first of all need to generalize the notion of a context to one dealing with tuples rather than terms. We in particular need contexts with multiple holes having types which match those of the tuple (or, more precisely, the $typtuplone$-state) they are meant to be paired with. More formally:

Definition 6** (Tuple Contexts)**

Tuple contexts* are triples of the form $(C,A,\gamma)$, where $C$ is an open term, $A=(\boldsymbol{\sigma},\boldsymbol{\tau})$ is a $(n,m)$ tuple type, and $\gamma$ is a type such that $!{\boldsymbol{x}_{\{1,\ldots,n\}}}:!{\boldsymbol{\sigma}},\boldsymbol{y}_{\{1,\ldots,m\}}:{\boldsymbol{\tau}}\vdash C:\gamma$. We note $\mathscr{C}^{\mathbf{T}}$ the set of tuple contexts. A tuple context $(C,A,\gamma)$ is said to be an open value if $C$ is of one of the following four forms: $\lambda x.M$, $\lambda{!{x}}.M$, $!{M}$, $y_{i}$ (where $i\in\mathbb{N}$).*

We now want to define when a tuple context and an $A$-state) can be paired together, and the operational semantics of such an object, which will be derived from that of $\Lambda_{\oplus}^{!}$ terms. This is the purpose of the following definition:

Definition 7** (Tuple Context Pairs)**

We say that a pair $u=(C,t)$ is a tuple context pair iff $t=(A,\mathcal{D})$ is an $A$-state, and $\exists\gamma\in\mathscr{A},\,(C,A,\gamma)\in\mathscr{C}^{\mathbf{T}}$. We indicate as $\mathbf{C\times\Delta(\mathscr{U})}$ the set of tuple context pairs. Moreover, given such a $u=(C,(A,\mathcal{D}))$, we define $\textbf{F}(u)$ as the (potentially infinite) distribution over $\mathscr{T}$ given by:

[TABLE]

Giving a notion of context distance for $A$-states is now quite easy and natural, since we know how contexts for such objects look like. For the sake of being as general as possible, this notion of a distance is parametric on a set of tuple contexts $\mathscr{C}\subseteq\mathscr{C}^{\mathbf{T}}$.

Definition 8

Let be $\mathscr{C}\subseteq\mathscr{C}^{\mathbf{T}}$ , $A\in\mathbf{T}$, and $t,s$ two $A$-states. We define:

[TABLE]

Unsurprisingly, the context distance between terms equals $\delta^{\text{c}}_{\mathscr{C}^{\mathbf{T}}}$ when applied to $A$-states obtained through $\hat{s}_{\sigma}(\cdot)$:

Proposition 2

If $\vdash M,N:\sigma$, then ${\delta^{c}_{\sigma,!}}(M,N)={\delta^{\text{c}}_{\mathscr{C}^{\mathbf{T}}}}(\hat{s}_{\sigma}(M),\hat{s}_{\sigma}(N))$.

But why did we introduce $\mathbf{C\times\Delta(\mathscr{U})}$? Actually, these pairs allow for a fine analysis of how tuples behave when put in a context, which in turn is precisely what we need to prove Theorem 4. This analysis, however, is not possible without endowing $\mathbf{C\times\Delta(\mathscr{U})}$ itself with an operational semantics, which is precisely what we are going to do in the next paragraphs.

Semantics for $\mathbf{C\times\Delta(\mathscr{U})}$:

In this paragraph, we define, for every $h\in\mathbf{C\times\Delta(\mathscr{U})}$, its semantics ${\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}$, which is a (potentially infinite) distribution over $\{k\in\mathbf{C\times\Delta(\mathscr{U})}\mid\textbf{F}(k)\in\text{Distr}(\mathscr{V})\}$.

Two relations need to be defined. On on the one hand, we need a one-step labelled transition relation $\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}$ which turn an element of $\mathbf{C\times\Delta(\mathscr{U})}$ into a distribution over $\mathbf{C\times\Delta(\mathscr{U})}$ by perfoming an action. Intuitively, one step of reduction in $\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}$ corresponds to at most one step of reduction in $\mathscr{L}_{\oplus}^{!{}}$. If that step exists, (i.e. if the term is reduced) then the label is the same, and otherwise (i.e., if only the context is reduced), the label is just $\tau$. We also need a multi-step approximation semantics ${\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}$ between elements of $\mathbf{C\times\Delta(\mathscr{U})}$ and subdistributions over the same set. The latter is based on the former, and both are formally defined in Figure 8, where

• •

$E$ is an evaluation context;

• •

$t$ is an $(n,m)$-state from $\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$;

• •

$h$ is a tuple-context pair from $\mathbf{C\times\Delta(\mathscr{U})}$;

• •

For every context $C$, $C_{\text{remove}(E)}$ stands for the context

[TABLE]

Definition 9

*We define a one-step labelled transition relation for $\mathbf{C\times\Delta(\mathscr{U})}$, that we note ${h}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{D}}$ with $h\in\mathbf{C\times\Delta(\mathscr{U})}$, $a\in\mathcal{A}_{\mathscr{M}_{\oplus}^{!{}}}\cup\{\tau\}$, and $\mathcal{D}$ a finite distribution over $\mathbf{C\times\Delta(\mathscr{U})}$, as specified in Figure 8.

We call normal form those elements in $\mathbf{C\times\Delta(\mathscr{U})}$ that cannot be reduced by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, and we note $NF(\mathbf{C\times\Delta(\mathscr{U})})$ the set of normal forms.*

Observe that we can actually give a characterization of normal forms:

[TABLE]

If $\mathcal{D}\in\text{Distr}(\mathbf{C\times\Delta(\mathscr{U})})$, we note $\mathscr{V}(\mathcal{D})=\sum_{h\in NF(\mathbf{C\times\Delta(\mathscr{U})})}\mathcal{D}(h)\cdot{\{{h}^{1}\}}$.

Definition 10

*We define an approximation semantics relation for $\mathbf{C\times\Delta(\mathscr{U})}$, that we note ${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}$, where $h$ is an element of $\mathbf{C\times\Delta(\mathscr{U})}$, and $\mathcal{D}$ is a finite distribution over $NF(\mathbf{C\times\Delta(\mathscr{U})})$, as specified in Figure 8.

We define a semantics for $\mathbf{C\times\Delta(\mathscr{U})}$, that we denote ${\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}$ for $h\in\mathbf{C\times\Delta(\mathscr{U})}$, as:*

[TABLE]

Relating ${\llbracket\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}$ and $\llbracket\rrbracket$:

We first show that this definition can indeed be related to the usual semantics for terms. This takes the form of the following lemma:

Lemma 4

Let be $u\in\mathbf{C\times\Delta(\mathscr{U})}$. Then:

• •

$\{\mathcal{D}\mid{u}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}\}$* is a directed set. We define ${\llbracket u\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}$ as its least upper bound;*

• •

$\textbf{F}(\cdot):\text{Distr}(\mathbf{C\times\Delta(\mathscr{U})})\rightarrow\text{Distr}(\mathscr{T})$* is continuous;*

• •

$\llbracket\textbf{F}(u)\rrbracket=\textbf{F}({\llbracket u\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})$.

• Proof.

The proof of the first point is exactly the same as the one given in [10] for the operational semantics of a probabilistic $\lambda$-calculus. The second and third ones are more involved.

Continuity of $\textbf{F}()$:

We have to show that, for any countable directed subset $I$ of $\text{Distr}(\mathbf{C\times\Delta(\mathscr{U})})$:

[TABLE]

where we have extended in a natural way the definition of $\textbf{F}(h)$ to $\textbf{F}(\mathcal{D})$, with $\mathcal{D}\in\text{Distr}(\mathbf{C\times\Delta(\mathscr{U})})$.

We can first observe that, since $\textbf{F}()$ is monotonous, it holds that: $\textbf{F}(\sup\{\mathcal{D}\mid\mathcal{D}\in I\})\geq\sup\{\textbf{F}(\mathcal{D})\mid\mathcal{D}\in I\}$. The other inequality is more involved. Let be $\mathcal{E}=\sup\{\mathcal{D}\mid\mathcal{D}\in I\}$. Since $I$ is a countable directed set, there exists an increasing sequence $(\mathcal{F}_{n})_{n\in\mathbb{N}}$ in $I$ such that $\mathcal{E}=\sup\{\mathcal{F}_{n}\mid n\in\mathbb{N}\}$. For $M\in\mathscr{T}$, we note $\alpha_{M,(C,t)}=\sum_{\{K\mid C[K]=M\}}t(K)$. We use it to express $\textbf{F}(\mathcal{E})$:

[TABLE]

Moreover, please observe that we can restrict ourselves to consider distributions over a countable subset of $\mathbf{C\times\Delta(\mathscr{U})}$ (which consists in the element of $\mathbf{C\times\Delta(\mathscr{U})}$ that can be generated by our language). Since $\mathcal{E}$ is a distribution on a countable set, we know that for every $\varepsilon$ there exists a finite subset $J_{\varepsilon}$ of $I$, such that $\sum_{(C,t)\not\in J_{\varepsilon}}\mathcal{E}(C,t)\leq\varepsilon$. So for every $\varepsilon$, it holds that:

[TABLE]

Since we now have to consider only a finite sum, we can exchange sum and limit:

[TABLE]

And since that’s true for every $\varepsilon$, we have the result.

$\llbracket\textbf{F}(\cdot)\rrbracket=\textbf{F}({\llbracket\cdot\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})$:

We show separately the two inequalities. First, we show that, for every $h\in\mathbf{C\times\Delta(\mathscr{U})}$, $\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})\leq\llbracket\textbf{F}(h)\rrbracket$. The proof is based on the fact that Diagram (6) commutes:

[TABLE]

The result stated by (6) is formally given by the following lemma.

Lemma 5

For every $h\in\mathbf{C\times\Delta(\mathscr{U})}$, it holds that if ${h}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{D}}$, then $\llbracket\textbf{F}(h)\rrbracket=\sum_{k\in\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}(k)\cdot\llbracket\textbf{F}(k)\rrbracket$

• Proof.

The proof consists in considering every case in the definition of ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, and use continuity result for $\llbracket\cdot\rrbracket$. $\Box$

We are now able to show that $\textbf{F}({\llbracket\cdot\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})\leq\llbracket\textbf{F}(\cdot)\rrbracket$:

Proposition 3

For every $h\in\mathbf{C\times\Delta(\mathscr{U})}$, it holds that $\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})\leq\llbracket\textbf{F}(h)\rrbracket$.

• Proof.

Observe that it is sufficient to show that ${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}$ implies $\textbf{F}(\mathcal{D})\leq\llbracket\textbf{F}(h)\rrbracket$. We prove it by induction on the derivation of ${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}$.

• •

If this derivation is :

${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\emptyset$

, then $\mathcal{D}=\emptyset$, and the result holds.

• •

If this derivation is

$h\text{ in normal form }$

${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}{\{{h}^{1}\}}$

, then $\textbf{F}(h)$ is a distribution over values (it can be checked easily by considering the carcaterisation of normal forms given in Equation (5)), and so $\llbracket\textbf{F}(h)\rrbracket=\textbf{F}(h)$, and the result holds.

• •

If this derivation is:

${h}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{F}}$         $({k}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{E}_{k})_{k\in\textsf{S}(\mathcal{F})}$

${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\sum_{k\in\textsf{S}(\mathcal{F})}\mathcal{F}(k)\cdot\mathcal{E}_{k}$

, we apply Lemma 5 : $\llbracket\textbf{F}(h)\rrbracket=\sum_{k\in\textsf{S}(\mathcal{F})}\mathcal{F}(s)\cdot\llbracket\textbf{F}(k)\rrbracket$. Moreover, we can apply the induction hypothesis to ${s}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{E}_{s}$ for every $k\in\textsf{S}\mathcal{F}$, which leads to: $\textbf{F}(\mathcal{E}_{k})\leq\llbracket\textbf{F}(k)\rrbracket$. Using it, we obtain:

[TABLE]

, which is the result.

$\Box$

We are now going to show the other inequality, namely that, for any $h\in\mathbf{C\times\Delta(\mathscr{U})}$, $\llbracket\textbf{F}(h)\rrbracket\leq\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})$. We first define a particular subset of $\mathbf{C\times\Delta(\mathscr{U})}$, namely those $h$, such that $\textbf{F}(h)$ can be seen as a term (remember that in the general case, it is a distribution over terms).

Definition 11

We define a subset $\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$ of $\mathbf{C\times\Delta(\mathscr{U})}$, as: $\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}=\{(C,(\mathcal{D},A))\in\mathbf{C\times\Delta(\mathscr{U})}\mid\mathcal{D}\text{ is a Dirac distribution}\}$. We define an operator $\overline{(\cdot)}^{\text{U}}$:

[TABLE]

Observe that if $h\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$, $\textbf{F}(h)$ is a Dirac distribution on terms. By abuse of notation, we’ll use $\textbf{F}(h)$ to denote the term $M$ such that $\textbf{F}(h)={\{{M}^{1}\}}$. The operator $\overline{(\cdot)}^{\text{U}}$ preserves ${\llbracket\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}$, as formally stated in Lemma 6 below:

Lemma 6

For every $\mathcal{D}\in\text{Distr}(\mathbf{C\times\Delta(\mathscr{U})})$, it holds that: $\textbf{F}({\llbracket\mathcal{D}\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})=\textbf{F}({\llbracket\overline{\mathcal{D}}^{\text{U}}\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})$.

• Proof.

It is a consequence of the fact that $\mathscr{L}_{\oplus}^{!{}}$ has the corresponding property: if $t=(\mathcal{D},A)\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$, ${t}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{(\mathcal{E},B)}$, then for every $K\in\textsf{S}(\mathcal{D})$ there exists $\mathcal{F}_{K}$ such that ${({\{{K}^{1}\}},A)}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{(\mathcal{F}_{K},B)}$, and moreover $\mathcal{E}=\sum_{K\in\textsf{S}(\mathcal{D})}\mathcal{D}(K)\cdot\mathcal{F}_{K}$. $\Box$

We introduce some notations on $\Rightarrow$: we write $M\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{D}$ with $n\in\mathbb{N}$, if there exists a derivation ${\Updelta}:M\Rightarrow\mathcal{D}$ of size at most $n$. Moreover, we write $\mathcal{D}\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{E}$ if there exists a finite set $I$ such that $\mathcal{D}=\sum_{i\in I}\alpha_{i}\cdot{\{{M_{i}}^{1}\}}$, and such that moreover $M_{i}\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{E}_{i}$, and $\mathcal{E}=\sum_{i\in I}\alpha_{i}\cdot\mathcal{E}_{i}$. Please observe that this definition imply that $\mathcal{D}$ is always a finite distribution over terms. We also introduce auxiliary notations for ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, as given in Figure 9.

Moreover, if $\mathcal{D}$, $\mathcal{E}$ are distributions over a set, we say that $\mathcal{D}$ is a finite approximation of $\mathcal{E}$ if $\mathcal{D}$ is finite, and moreover $\mathcal{D}\leq\mathcal{E}$. We denote it by $\mathcal{D}\stackrel{{\scriptstyle f}}{{\leq}}\mathcal{E}$.

We first consider the case where $h\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$ is such that $\textbf{F}(h)$ is a value. We can see that the following diagram commutes

[TABLE]

, as formally stated in Lemma 7 below.

Lemma 7

Let be $h\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$, such that $\textbf{F}(h)$ is a value. There exists $k\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$ such that ${h}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}^{\star}{{\{{k}^{1}\}}}$ and $k\in NF(\mathbf{C\times\Delta(\mathscr{U})})$ verifies $\textbf{F}(k)=\textbf{F}(h)$.

• Proof.

The proof consists in showing that, if $\textbf{F}(h)$ is a value, then there is a finite sequence $h=k_{0}\ldots,k_{n}$ with ${k_{i}}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{{\{{k_{i+1}}^{1}\}}}$, every $k_{i}\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$, $k_{n}\in NF(\mathbf{C\times\Delta(\mathscr{U})})$, and moreover $\textbf{F}(k_{i})=\textbf{F}(h)$. $\Box$

We now consider the case where $\textbf{F}(h)$ is not a value: it means that we have to consider $\mathcal{D}\in\text{Distr}(\mathscr{T})$, such that $\textbf{F}(h)\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{D}$, with $n>1$. Our aim is to show that $\mathcal{D}\leq{\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}$. In that aim, we show first that Diagram 8 below commutes,

[TABLE]

as formally stated by the following Lemma:

Lemma 8

For any $h\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$, such that $\textbf{F}(h)$ is not a value, there exists $\mathcal{E}\in\text{Distr}(\mathbf{C\times\Delta(\mathscr{U})})$ such that ${h}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}^{+}{\mathcal{E}}$, and for every $\mathcal{D}\in\text{Distr}(\mathscr{T})$, and $n\geq 1$ such that $\textbf{F}(h)\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{D}$ , there exists $\mathcal{F}$ such that $\mathcal{F}\stackrel{{\scriptstyle f}}{{\leq}}\overline{\mathcal{E}}^{\text{U}}$, and moreover $\textbf{F}(\mathcal{F})\stackrel{{\scriptstyle m}}{{\Rightarrow}}\mathcal{D}$ with $m<n$.

Before doing the proof, we give some intuitions about this diagram: we first consider these steps of ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{}$ that reduce more that one redex. It forces us to use not the one step transition $\rightarrow$ to talk about the semantics for terms, but directly the approximation semantics $\Rightarrow$. Let us consider now the steps of ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{}$ where no redex is reduced: more precisely, we can characterize them as the ones corresponding to actions passing a term that is already a value from the exponential part to the linear part of the inside tuple. The proof is made possible by the fact that we can show that there can only be a finite number of reduction step ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{}$ that don’t reduce the underlying term, before there is a step reducing at least a redex in it.

• Proof.

We are first going to state a lemma about the approximation semantics $\Rightarrow$, which we’ll need later in the proof of Lemma 8. Indeed, in order to manage the problem of a step of ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{}$ corresponding to strictly more than one step of $\rightarrow$, we need to transform a derivation ${\Updelta}:M\Rightarrow\mathcal{D}$ in derivations corresponding to reduction processes done after having completely reduced part of $M$. More precisely, the Lemma 9 below gives us a way to extract of a derivation tree the subtrees corresponding to the evaluation after having reduced all the redex in a subterm in evaluation position. Please observe that it talks only about semantics of term, and express a form of compositionnality in the derivation. It will be used to treat the case of applicative actions, where we reduce many redex in one step of reduction for ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{}$.

Lemma 9

Let be $M$ a closed term which isn’t a value, with $E[M]\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{D}$ a valid derivation of the approximation semantics. Then there exists a finite set $I\subseteq\mathbb{N}$, and for every $i\in I$ a value $V_{i}$, a coefficient $\alpha_{i}$, and a valid derivation $\Upxi_{i}:E[V_{i}]\stackrel{{\scriptstyle m}}{{\Rightarrow}}\mathcal{E}_{i}$ such that $n<m$, $\mathcal{D}=\sum_{i\in I}\alpha_{i}\cdot\mathcal{E}_{i}$, and moreover for every $V$, $\sum_{i\mid V_{i}=V}\alpha_{i}\leq\llbracket M\rrbracket(V)$

• Proof.

The proof is by induction on ${\Updelta}$. $\Box$

Let us now show the first part of Lemma 8. Let $h\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$ such that $\textbf{F}(h)$ is not a value. By definition of $\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$, $h$ is of the form: $h=(C,({\{{K}^{1}\}},A))$. We are going to construct the distribution $\mathcal{E}$ by case analysis on $C$ . Please observe that there is at most one possible action $a$ such that ${(C,({\{{K}^{1}\}},A))}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, and moreover it depends only on in $C$ and $A$. Consequently, we do a case analysis on the action $a$.

• •

If $a=\tau$: it means that the reduced redex doesn’t affect the inside tuple. We take $\mathcal{E}$ such that ${h}{\stackrel{{\scriptstyle\tau}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{E}=\sum_{1\leq i\leq n}\frac{1}{n}{\{{(C_{i},{(K,A)})}^{1}\}}}$. Observe that $\mathcal{E}$ is actually a finite distribution. Let be $\mathcal{D}\in\text{Distr}(\mathscr{V})$, and $n\geq 1$, such that $\textbf{F}(h)\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{D}$. Since $\textbf{F}(h)\not\in\mathscr{V}$, and $n\geq 1$, $\textbf{F}(h)\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{D}$ is of the form:

[TABLE]

, where for every $i$, $m_{i}<n$. We take $\mathcal{F}=\mathcal{E}$, $m=\max\{n_{i}\mid 1\leq i\leq p\}<n$ and the result is obtained by seeing that $\textbf{F}(\mathcal{F})=\sum_{1\leq i\leq p}\frac{1}{n}\cdot{\{{N_{i}}^{1}\}}\stackrel{{\scriptstyle m}}{{\Rightarrow}}\mathcal{D}$.

• •

If $a=({?}^{j})$: then $C=E[(\lambda{!{z}}.M){y_{j}}]$.

It means that the only rule than can be used to show ${h}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{\cdot}$ is:

[TABLE]

where $k=({E[(\lambda{!{z}}.M)!{x_{n+1}}]}_{\text{remove}(\{j\})},s)$.

Observe that $k\in\{l\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}\mid{l}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\cdot}\,\text{ implies }a=\tau\}$.

Using the previous case, we know that there exist $\mathcal{E}_{k}$ verifying the condition of Lemma 8 with respect to $k$. Now, we are going to show that we can reuse it with respect to $h$. First, notice that ${h}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}^{+}{\mathcal{E}}$ (since ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}^{+}{}$ is transitive). So we can take $\mathcal{E}=\mathcal{E}_{k}$. Let be $n\geq 1$, and $\mathcal{D}$ such that $\textbf{F}(h)\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{D}$. Since $\textbf{F}(h)=\textbf{F}(k)$, it holds that $\textbf{F}(k)\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{D}$. We can conclude by using the properties of $\mathcal{E}_{k}$ with respect to $k$.

• •

If $a=@^{j}_{\kappa}$: it means that $C=E[y_{j}V]$, and the rule used to reduce $h$ by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$ is the applicative one. So we can take $\mathcal{E}$ defined as:

[TABLE]

We see that ${h}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}^{+}{\mathcal{E}}$. Let be $\mathcal{D}$, and $n\geq 1$, such that $\textbf{F}(h)\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{D}$. We need to define $\mathcal{F}$ as specified in Lemma 8. Notice that $\mathcal{E}\not\in\text{Distr}(\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}})$, but we are able to express $\overline{\mathcal{E}}^{\text{U}}$ as:

[TABLE]

where $\textbf{F}(k_{W})=(\textbf{F}(E,t))[W]$, and moreover $k_{W}\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$. We are going to apply Lemma 9 to $(\textbf{F}(E,t))[\textbf{F}(y_{j}V,t)]$ : there exist a finite set $I$, and a family $(W_{i})_{i\in I}$ of $\mathscr{V}$, such that $\sum_{i\in I}\alpha_{i}\cdot{\{{(\textbf{F}(E,t))[W_{i}]}^{1}\}}\stackrel{{\scriptstyle m}}{{\Rightarrow}}\mathcal{D}$, with $m<n$, and for every $W\in\mathscr{V}$, it holds that $\sum_{i\mid W_{i}=W}\alpha_{i}\leq\llbracket\textbf{F}(y_{j}V,t)\rrbracket(W)$. Now we define $\mathcal{F}=\sum\alpha_{i}\cdot{\{{k_{W_{i}}}^{1}\}}$, and we can see that $\mathcal{F}\stackrel{{\scriptstyle f}}{{\leq}}{\overline{\mathcal{E}}^{\text{U}}}$ and $\textbf{F}(\mathcal{F})\stackrel{{\scriptstyle m}}{{\Rightarrow}}\mathcal{D}$, and so we have the result.

• •

If $a=(!^{j})$: it means that $C=E[x_{j}]$, and that the rule used is:

[TABLE]

We define $\boldsymbol{M}$ and $\boldsymbol{N}$ such that $K=(\boldsymbol{M},\boldsymbol{N})$. We can distinguish two cases, depending on $\boldsymbol{M}_{j}$:

• •

If $\boldsymbol{M}_{j}$ is not a value. Then we are going to apply Lemma 9. Indeed, $\textbf{F}(C,t)=\textbf{F}(E,t)[\boldsymbol{M}_{j}]$. The proof is essentially the same that for the applicative case.

• •

If $\boldsymbol{M}_{j}$ is a value. Then we can define $k\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$ by $k=(E[y_{m+1}],s)$. It is possible that the only action able to reduce $k$ is of the form $(!^{k})$, However, we can iterate the previous reasonning (which intuitively corresponds to do reduction on $\mathbf{C\times\Delta(\mathscr{U})}$, but not in the actual term) only a finite number of times (because we can have only a finite number of occurrences of values that are in an evaluation position in $M=\textbf{F}(C,t)$). So after a finite number of steps like that, we arrive to reduce this case to one we have already considered.

$\Box$

Lemma 10

For every $h\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$, if $\textbf{F}(h)\Rightarrow\mathcal{D}$, then $\mathcal{D}\leq{\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})}$.

• Proof.

The proof is by induction on the size $n$ of the derivation $\textbf{F}(h)\Rightarrow\mathcal{D}$:

If $n=0$, then $\mathcal{D}=\emptyset$, and the result is true.

• *

If $n=1$, or $\mathcal{D}=\emptyset$, or $\mathcal{D}={\{{\textbf{F}(h)}^{1}\}}$, and then $\textbf{F}(h)$ is a value, and we can apply the second point of Lemma 8.

• *

If $n>1$, then it implies that $\textbf{F}(h)$ is not a value, and so we can apply the second point of Lemma 8, and apply the induction hypothesis on the strictly smaller derivations it gives us.

$\Box$

As a corollary, we can see that that $\llbracket\textbf{F}(h)\rrbracket\leq\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})$ holds in fact for every $h\in\mathbf{C\times\Delta(\mathscr{U})}$, and not only for those in $\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$:

Proposition 4

For any $h\in\mathbf{C\times\Delta(\mathscr{U})}$, it holds that $\llbracket\textbf{F}(h)\rrbracket\leq\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})$

• Proof.

First, we can see that Lemma 10 imply that $\llbracket\textbf{F}(h)\rrbracket\leq\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})$ for every $h\in\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}}$. Lemma 6 allows to generalize it to the whole if $\mathbf{C\times\Delta(\mathscr{U})}$. $\Box$

We have now only to sum up Proposition 3 and 4 to obtain the correspondence between ${\llbracket\cdot\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}$ and $\llbracket\cdot\rrbracket$. $\Box$

Equivalence relations on $\mathbf{C\times\Delta(\mathscr{U})}$:

Before proceeding, we need to understand how any reflexive and symmetric relation on $\mathbf{C\times\Delta(\mathscr{U})}$ can be turned into a relation on distributions on $\mathbf{C\times\Delta(\mathscr{U})}$. If $\mathrel{R}$ is a reflexive and symmetric relation on $\mathbf{C\times\Delta(\mathscr{U})}$, we lift it to distributions over $\mathbf{C\times\Delta(\mathscr{U})}$ by stipulating that $\mathcal{D}\mathrel{R}\mathcal{E}$ whenever there exists a countable set $I$, a family $(p_{i})_{i\in I}$ of positive reals of sum smaller than 1, and families $(h_{i})_{i\in I},(k_{i})_{i\in I}$ in $\mathbf{C\times\Delta(\mathscr{U})}$, such that $\mathcal{D}=\{{h_{i}}^{p_{i}}\}_{i\in I}$, $\mathcal{E}=\{{k_{i}}^{p_{i}}\}_{i\in I}$, and moreover $h_{i}\mathrel{R}k_{i}$ for every $i\in I$.

We now want to precisely capture when a relation on $\mathbf{C\times\Delta(\mathscr{U})}$ can used to evaluate the distance between tuple-context pairs.

Definition 12

Let $\mathrel{R}$ be a reflexive and symmetric relation on $\mathbf{C\times\Delta(\mathscr{U})}$.

• •

We say that $\mathrel{R}$ is ** preserved by $\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}$* if, for any $h,k\in\mathbf{C\times\Delta(\mathscr{U})}$ such that $h\mathrel{R}k$, if ${h}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{D}}$, then there exists $\mathcal{E}$ such that ${k}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{E}}$, and $\mathcal{D}\mathrel{R}\mathcal{E}$.*

• •

We say that $\mathrel{R}$ is $\varepsilon$-bounding if $h\mathrel{R}k$, implies $\lvert{\sum\nolimits_{\textbf{F}(h)}}-{\sum\nolimits_{\textbf{F}(k)}}\rvert\leq\varepsilon$.

• •

Let $\mathscr{C}$ be a set of tuple contexts, and $t,s\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$ be two $A$-states. We say that $\mathrel{R}$ is $\mathscr{C}$-closed with respect to $t$ and $s$, if for every $C$ and $\gamma$ such that $(C,A,\gamma)\in\mathscr{C}$, it holds that $(C,t)\mathrel{R}(C,s)$.

Please observe how any relation preserving $\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}$ and being $\varepsilon$-bounding can be seen somehow as an $\varepsilon$-bisimulation, but on tuple-context pairs. The way we defined the lifting, however, makes it even a stronger notion, i.e., the ideal candidate for an intermediate step towards Soundness.

Preservation by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$ leads us to preservation (in a weaker sense) by ${}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}$. That’s the sense of the following lemma.

Lemma 11

Let $\mathrel{R}$ be a reflexive and symmetric relation on $\mathbf{C\times\Delta(\mathscr{U})}$ preserved by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$. Let $h,k\in\mathbf{C\times\Delta(\mathscr{U})}$ be such that $h{\mathrel{R}}k$. Let $\mathcal{D}$ be such that ${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}$. Then there exists $\mathcal{E}$ such that ${k}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{E}$, and $\mathcal{D}{\mathrel{R}}\mathcal{E}$.

• Proof.

The proof is by induction on the derivation of ${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}$.

• •

if the derivation is

${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\emptyset$

, the result holds.

$\Box$

Lemma 12

If $h,k\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$ are such that there exists a reflexive and symmetric relation $\mathrel{R}$ preserved by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, $\varepsilon$-bounding, and containing $(h,k)$, then it holds that ${\lvert{\sum\nolimits_{\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})}}-{\sum\nolimits_{\textbf{F}({\llbracket k\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}})}}\rvert\leq\varepsilon}$.

We use Lemma 12 to show the following proposition.

Proposition 5

Let $\mathscr{C}$ be a set of tuple contexts, $t,s$ two $A$-states and $\mathrel{R}$ a reflexive and transitive relation preserved by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, $\varepsilon$-bounding, and $\mathscr{C}$-closed with respect to $t$ and $s$. Then it holds that ${\delta^{c}_{\mathscr{C},!}}(t,s)\leq\varepsilon$.

• Proof.

It’s a direct consequence of Lemma 12. $\Box$

Moreover, we see that the conditions from Definition 12 are enough to guarantee that two terms are at context distance at most $\varepsilon$.

Proposition 6

Let $M,N$ be two terms of type $\sigma$. Suppose there exists a reflexive and symmetric relation $\mathrel{R}$ on $\mathbf{C\times\Delta(\mathscr{U})}$, which is preserved by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, $\varepsilon$-bounding, and $\mathscr{C}^{\mathbf{T}}$-closed with respect to $\hat{s}_{\sigma}(M)$ and $\hat{s}_{\sigma}(N)$. Then ${\delta^{c}_{\sigma,!}}(M,N)\leq\varepsilon$.

$\varepsilon$-bisimulation and ${}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}$

: What remains to be done, then, is to show that if two terms are related by $\mathrel{R}^{\varepsilon}$, then they themselves satisfy Definition 12. Compulsory to that is showing that any $\varepsilon$-bisimulation can at least be turned into a relation on $\mathbf{C\times\Delta(\mathscr{U})}$.

We need to do that, in particular, in a way guaranteeing the $\mathscr{C}$-closure of the resulting relation, and thus considering all possible tuple contexts from $\mathscr{C}$:

Definition 13

Let $\mathrel{R}$ be a reflexive and symmetric relation on $\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$. Let be $\mathscr{C}$ a set of tuple contexts. We define its contextual lifting to $\mathbf{C\times\Delta(\mathscr{U})}$ with respect to $\mathscr{C}$ as the following binary relation on $\mathbf{C\times\Delta(\mathscr{U})}$:

[TABLE]

The following result tells us that, indeed, any $\varepsilon$-bisimulation can be turned into a relation satisfying Definition 12:

Proposition 7

Let $\mathrel{R}$ be a $\varepsilon$-bisimulation. Then $\widehat{\mathrel{R}}^{\mathscr{C}^{\mathbf{T}}}$ is preserved by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$ and $\varepsilon$-bounding, and $\mathscr{C}^{\mathbf{T}}$-closed with respect to every $t,s$ such that $t\mathrel{R}s$.

• Proof.

Let $\mathrel{R}$ be an $\varepsilon$-bisimulation. We obtain that $\widehat{\mathrel{R}}^{\mathscr{C}^{\mathbf{T}}}$ is $\mathscr{C}^{\mathbf{T}}$-closed as a direct consequence of the lifting definition. Similarly, we see that $\widehat{\mathrel{R}}^{\mathscr{C}^{\mathbf{T}}}$ is $\varepsilon$-bounding as a direct consequence of the definition of a $\varepsilon$-bisimulation. Now, let us show that $\widehat{\mathrel{R}}^{\mathscr{C}^{\mathbf{T}}}$ is preserved by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$. Let be $A$ such that $(h,k)\in{\widehat{\mathrel{R}}^{\mathscr{C}^{\mathbf{T}}}}_{A}$. The proof is by induction on the derivation of ${h}{\Rightarrow}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}$. It is based on the following idea: for every $C$ such that there exist $\sigma$ for which $(C,A,\sigma)$ is a tuple context:

• •

or for every $A$-state $t$, $(C,t)$ is in normal form.

• •

or there exists a family $(C_{i})_{1\leq i\leq n}$ such that $(C_{i},A,\sigma)\in\mathscr{C}^{\mathbf{T}}$, and moreover for every $A$-state $t$, ${(C,t)}{\stackrel{{\scriptstyle\tau}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\sum_{1\leq i\leq n}{\{{(C_{i},t)}^{1}\}}}$

• •

or there exists an action $a$ of $\mathscr{L}_{\oplus}^{!{}}$, and $D,B$ such that $(D,B,\sigma)$, such that for every $A$-state $t$, ${(C,t)}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{{\{{(D,s)}^{1}\}}}$, and ${t}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{s}$.

$\Box$

We are finally ready to give a proof of soundness:

• Proof.

[of Theorem 4] Consider two terms $M$ and $N$ of type $\sigma$. Let $\varepsilon$ be ${\delta_{\sigma,!{}}^{b}}(M,N)$. We take $\mathrel{R}^{\varepsilon}$ (defined in Definition 3 as the largest $\varepsilon$-bisimulation), and we see that $\hat{s}_{\sigma}(M)\,{\mathrel{R}^{\varepsilon}}\,\hat{s}_{\sigma}(N)$. Proposition 7 tells us that we can apply Proposition 6 to $M$, $N$, and $\widehat{(\mathrel{R}^{\varepsilon})}^{\mathscr{C}^{\mathbf{T}}}$. Doing so we obtain that ${\delta^{c}_{\sigma,!}}(M,N)\leq\varepsilon$, which is the thesis. $\Box$

5.5.2 Completeness

We can actually show that $\delta_{\sigma,!{}}^{b}$ is also complete with respect to the contextual distance: that is the aim of this section.

Theorem 5** (Full Abstraction)**

For every $\sigma$, ${\delta^{c}_{\sigma,!}}=\delta_{\sigma,!{}}^{b}$.

• Proof.

One inequality is given by Theorem 4.

Please observe that Theorem 4 gives us already half of Theorem 5: indeed, it says that for every $M$ and $N$ of type $\sigma$, it holds that: ${\delta^{c}_{\sigma,!}}(M,N)\leq{\delta_{\sigma,!{}}^{b}}(M,N)$. Our goal is now to show the other inequality, that is ${\delta^{c}_{\sigma,!}}(M,N)\geq{\delta_{\sigma,!{}}^{b}}(M,N)$ . The proof of the other one is based on the trace characterization $\delta^{b}_{\mathscr{L}_{\oplus}^{!{}}}$ given in Section 5.4. More precisely, we use the fact that every trace can be simulated by a context: for every $A\in\mathbf{T}$, we construct a tuple context $(C,A,\tau)$, such that for every $A$-state $t$, it holds that $\mathsf{PR}_{\mathsf{T}}(t)=\text{Obs}(\textbf{F}(C,t)).$

Lemma 13

For every $\mathsf{T}\in\mathscr{T}$, for every $A\in\mathbf{T}$ such that $\mathsf{T}$ is an admissible trace for $A$, there exists a term $C$, and a type $\gamma$ such that:

• •

$(C,A,\gamma)$* is a tuple context.*

• •

for every $t\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$ of the form $t=(\mathcal{D},A)$, it holds that ${\sum\nolimits_{\llbracket\textbf{F}(C,t)\rrbracket}}=\mathsf{PR}_{\mathsf{T}}(t).$

• Proof.

Let be $A=(\boldsymbol{\sigma},\boldsymbol{\tau})$ a type for tuple. Let be $(n,m)$ the arity of $A$. We define a context $C$, and a type $\gamma$, by induction on the length of the admissible trace :

• •

if $\mathsf{T}=\top$: We want a context that terminates with probability $1$, whatever term we fill it with. We take:

[TABLE]

• •

if $\mathsf{T}={({?}^{i})\cdot\mathsf{S}}$. Let be $B$ such that, whenever we do the action $({?}^{i})$ from a $A$-state, we obtain a $B$-state. Let $D$ and $\eta$ the open term and type obtained by induction hypothesis applied to $\mathsf{S}$ and $B$. We take $\gamma=\eta$, and:

[TABLE]

• •

if $\mathsf{T}={(!^{i})\cdot\mathsf{S}}$. Let be $B$ such that, whenever we do the action $(!^{i})$ from a $A$-state, we obtain a $B$-state. Let $D$ and $\eta$ be the open term and type obtained by induction hypothesis applied to $\mathsf{S}$ and $B$. We take $\gamma=\eta$, and $C=D\{x_{i}/y_{m+1}\}$.

• •

if $\mathsf{T}={@^{i}_{\kappa}\cdot\mathsf{S}}$. Since $\mathsf{T}$ is an admissible trace for $A=(\boldsymbol{\sigma},\boldsymbol{\tau})$, $\kappa$ should be of the form: $\kappa=(E,F,\boldsymbol{\sigma},\boldsymbol{\tau},M,\iota)$. Let $B$ be the corresponding tuple type obtained after the action $(!^{i})$, and let be $D$ and $\eta$ the term and the type given by the induction hypothesis and $B$. Then we take $\gamma=\eta$:

[TABLE]

$\Box$

When we combine Proposition 13 and Proposition 1, we obtain the following corollary:

Corollary 2

Let be $t$ and $s$ two $A$-states.

[TABLE]

• Proof.

Let be $t$ and $s$ two $A$-states that are not $\varepsilon$-bisimilar. Then there exists a trace $\mathsf{T}$ that shows it, that is verifying $\lvert{\mathsf{PR}_{t}(\mathsf{T})}-{\mathsf{PR}_{s}(\mathsf{T})}\rvert>\varepsilon$. Now, we just have to take the open term $C$ such that $(C,A,\cdot)\in\mathscr{C}^{\mathbf{T}}$ , corresponding to this trace $\mathsf{T}$. And we have $\lvert{\text{Obs}(\textbf{F}(C,t))-\text{Obs}(\textbf{F}(C,s))}\rvert>\varepsilon$, and the result folds. $\Box$

We can now transform Corollary 2 in a result on terms, which is exactly what we need to end the proof of theorem 5.

Lemma 14

Let be $M$, $N$ of type $\sigma$. Then:

[TABLE]

• Proof.

Let us unfold the definition of ${\delta_{\sigma,!{}}^{b}}(M,N)$: please recall that we defined it as ${\delta^{b}_{\mathscr{L}_{\oplus}^{!{}}}}(\hat{s}_{\sigma}(M),\hat{s}_{\sigma}(N))$. Let be $A$ such that $\hat{s}_{\sigma}(\cdot)$ is an $A$-term. Please recall that $A=([],[\sigma])$. We can see that for every $C,\tau$ such that $(C,A,\tau)\in\mathscr{C}^{\mathbf{T}}$, it holds that $C$ can in fact be see as a context for terms: more precisely, it holds that $y_{1}:\sigma\vdash C:\tau$ and moreover, it holds that

[TABLE]

Since we can transform every tuple of context for $A$ into a context on terms in that way, we obtain the result. $\Box$

Theorem 5 is a direct consequence of Lemma 14: indeed, please recall that we had to show that ${\delta^{c}_{\sigma,!}}(M,N)\geq{\delta_{\sigma,!{}}^{b}}(M,N)$. Since that’s exactly what Lemma 14 says, it ends the proof.

$\Box$

5.6 On an Up-to-Context Technique

5.6.1 Up-to $\varepsilon$-bisimulation

As we have just shown, context distance can be characterized as a coinductively defined metric, which turns out to be useful when evaluating the distance between terms. In this section, we will go even further, and show how an up-to-context [32] notion of $\varepsilon$-bisimulation is precisely what we need to handle our running example.

We first of all need to generalize our definition of a tuple: an open tuple is a pair $(\boldsymbol{M},\boldsymbol{N})$, where $\boldsymbol{M}$ and $\boldsymbol{N}$ are sequences of (not necessarily closed) typable terms.

Definition 14

If $K=(\boldsymbol{M},\boldsymbol{N})$ is an open tuple, and $A=(\boldsymbol{\gamma},\boldsymbol{\eta})$ is a tuple type, we say that $(\boldsymbol{\sigma},\boldsymbol{\tau},K,A)$ is a substitution judgment iff:

• •

$!{\boldsymbol{x}}:!{\boldsymbol{\sigma}}\vdash{\boldsymbol{M}_{i}}:{\boldsymbol{\gamma}}_{i}$;

• •

if $n$ and $m$ are such that $\boldsymbol{\tau}$ is a $n$-sequence, and $\boldsymbol{N}$ a $m$-sequence, then there exists a partition $\{E_{1},\ldots E_{m}\}$ of $\{1,\ldots,n\}$ such that $\boldsymbol{y}_{E_{j}}:\boldsymbol{\tau}_{E_{j}}\vdash N_{j}:\eta_{j}$ for every $j\in\{1,\ldots,m\}$.

$\mathscr{J}^{\text{subst}}$* is the set of all substitution judgments.*

If $\kappa=(\boldsymbol{\sigma},\boldsymbol{\tau},K,A)\in\mathscr{J}^{\text{subst}}$, and $H\in\mathscr{U}$ is of type $(\boldsymbol{\sigma},\boldsymbol{\tau})$, then there is a natural way to form a tuple $\kappa[H]$, namely by substituting the free variables of $K$ by the components of $H$. In the following, we restrict $\mathscr{J}^{\text{subst}}$ to those judgments $\kappa$ such that for every $H$, terms in the linear part of $\kappa[H]$ are values. Observe that we always have $\vdash\kappa[H]:A$. We extend the notation $\kappa[H]$ to distributions over $\mathscr{U}$: if $\mathcal{D}$ is a distribution over tuples of type $(\boldsymbol{\sigma},\boldsymbol{\tau})$, we note $\kappa[\mathcal{D}]=\{{\kappa[H]}^{\mathcal{D}(H)}\}_{H\in\mathscr{U}}$, which is a distribution over tuples of type $A$. Moreover, we want to be able to apply our substitution judgments to the states of $\mathscr{L}_{\oplus}^{!{}}$. If $t=(\mathcal{D},(\boldsymbol{\sigma},\boldsymbol{\tau}))\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$, and $\kappa=(\boldsymbol{\sigma},\boldsymbol{\tau},K,A)$, the state of $\mathscr{L}_{\oplus}^{!{}}$ defined by $(\kappa[\mathcal{D}],A)$ will be often indicated as $\kappa[t]$.

Example 6

We illustrate on a simple example the use of substitution judgments. Let be $\tau$ any type. Consider $\boldsymbol{\sigma}=\left[\tau\multimap\tau\right]$, and $\boldsymbol{\tau}=\left[\right]$. Moreover, let $K=(\left[x_{1}\right],\left[I\right])$ and $A=(\left[\tau\multimap\tau\right],\left[\tau\multimap\tau\right])$. Then $\kappa=(\boldsymbol{\sigma},\boldsymbol{\tau},K,A)$ is a substitution judgment. We consider now a tuple of type $(\boldsymbol{\sigma},\boldsymbol{\tau})$. In fact, we take here a tuple that will be useful in order to analyze our running example: $H=(\left[\Omega_{!}\oplus^{\varepsilon}I\right],\left[\right])$. By substituting $H$ in $\kappa$, we obtain $\kappa[H]=(\left[\Omega_{!}\oplus^{\varepsilon}I\right],\left[I\right])$, and we can see easily that we obtain indeed a tuple of type $A$.

The main idea behind up-to context bisimulation is to allow for the freedom of discarding any context when proving a relation to be a bisimulation. This is captured by the following definition:

Definition 15

Let $\mathrel{R}$ be a relation on $\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$. $\mathrel{R}$ is an $\varepsilon$-bisimulation up to context if for every $t$ and $s$ such that $t\mathrel{R}s$, the following holds:

• •

there exists $C\in\mathbf{T}$ such that $t=(\mathcal{D},C)$, $s=(\mathcal{E},C)$, and $\lvert{\sum\nolimits_{\mathcal{D}}}-{\sum\nolimits_{\mathcal{E}}}\rvert\leq\varepsilon$.

• •

for any $a\in\mathcal{A}_{\mathscr{M}_{\oplus}^{!{}}}$, if ${t}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{u}=(\mathcal{D},A)$ and ${s}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{v}=(\mathcal{E},A)$, then there exists a finite set $I\subseteq\mathbb{N}$ such that:

• •

there is a family of rationals $(p_{i})_{i\in I}$ such that $\sum_{i\in I}p_{i}\leq 1$;

• •

there are families $\boldsymbol{\sigma}^{i}$, $\boldsymbol{\tau}^{i}$, and $K^{i}$, such that $\kappa_{i}=(\boldsymbol{\sigma}^{i},\boldsymbol{\tau}^{i},K^{i},A)$ is a substitution judgment for every $i\in I$;

• •

there are distributions over tuples $\mathcal{D}_{i}$, $\mathcal{E}_{i}$ such that $(\mathcal{D}_{i},B_{i})\mathrel{R}(\mathcal{E}_{i},B_{i})$;

and moreover $\mathcal{D}=\sum\nolimits_{i\in I}p_{i}\cdot\kappa_{i}[\mathcal{D}_{i}]$, and $\mathcal{E}=\sum\nolimits_{i\in I}p_{i}\cdot\kappa_{i}[\mathcal{E}_{i}].$

The just introduced proof method is indeed quite useful when handling our running example.

Example 7

We show that up-to bisimulations can handle our running example. Please recall the definition of $M_{\varepsilon}$ given in Example 2. First, we can see that, for every $a$, for every type $\tau$, $\hat{s}_{!{(\tau\multimap\tau)}}(M_{a})=({\{{(\left[\right],\left[!{\Omega_{!}\oplus^{a}I}\right])}^{1}\}},(\left[\right],\left[!{\tau\multimap\tau}\right]))$. We define a relation $\mathrel{R}$ on $\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$ containing $(\hat{s}_{!{(\tau\multimap\tau)}}(M_{\varepsilon}),\hat{s}_{!{(\tau\multimap\tau)}}(M_{\mu}))$, and we show that it is an $\gamma$-bisimulation up-to context for an appropriate $\gamma$. In order to simplify the notations, we define $B=({\left[\tau\multimap\tau\right]},\left[\right])$, and $t_{n},s_{n}\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$ as:

[TABLE]

Then, we define the relation $\mathrel{R}$ as $\mathrel{R}=\left\{\left(\hat{s}_{\sigma}(M),\hat{s}_{\sigma}(N)\right)\right\}\cup\left\{(t_{n},s_{n})\mid n\in\mathbb{N}\right\}.$ One can check that $\mathrel{R}$ is indeed a $\gamma$-bisimulation up-to-context (where $\gamma=\sup_{n\in\mathbb{N}}\lvert\varepsilon^{n}-\mu^{n}\rvert$) by carefully analysing every possible action. The proof is based on the following observations:

• •

The only action starting from $\hat{s}_{\sigma}(M)$ or $\hat{s}_{\sigma}(N)$ is $a=({?}^{1})$, passing a term to the exponential part of the tuple, then we end up in $t_{0}$ and $s_{0}$ respectively.

• •

If we start from $t_{n}$ or $s_{n}$, the only relevant action is Milner’s action $a=(!^{1})$, consisting in taking a copy of the term in the exponential part, evaluating it, and putting the result in the linear part. We can see (using the substitution judgment $\kappa$ defined in Example 6), that ${t_{n}}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{\kappa[t_{n+1}]}$, and similarly ${s_{n}}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}{\kappa[s_{n+1}]}$, and the result follows.

Example 8

We give now an example illustrating a not-so-obvious constraint in the definition of a substitution judgment. Suppose we take $K=(\left[x_{1}\right],\left[x_{1}\right])$, and $A=(\left[\sigma\right],\left[\sigma\right])$. Then $\kappa=(\left[\sigma\right],\left[\right],K,A)$ is a not a substitution judgment, since $x_{1}$ appear in the linear part of $K$, and we need non-linear variables to type it. The constraint is there to avoid the situation in which, $({\{{(\left[V\right],\left[\right])}^{1}\}},(\left[\sigma\right],\left[\right]))$ and $({\{{(\left[W\right],\left[\right])}^{1}\}},(\left[\sigma\right],\left[\right]))$ would be up-to bisimilar for every $V$ and $W$ of type $\sigma$.

5.6.2 Soundness of up-to technique

Bisimulations up-to contexts would be useless without a correctness result like the following one:

Theorem 6

If $\mathrel{R}$ is an $\varepsilon$-bisimulation up-to context, then $\mathrel{R}\subseteq\mathrel{R}^{\varepsilon}$.

The remaining of this section consists in the proof of Theorem 6. The proof is an extension of that of Theorem 4 (although technically more involved).

We first define a relation $\mathcal{D}\triangleright\mathcal{E}$ between distribution over $\mathbf{C\times\Delta(\mathscr{U})}$, which expresses the fact that $\mathcal{E}$ is obtained from $\mathcal{D}$ by changing the way we split our term into external environment and inside tuple:

Definition 16

Let be $\mathcal{D}$ and $\mathcal{E}$ two distributions over $\mathbf{C\times\Delta(\mathscr{U})}$. We write $\mathcal{D}\triangleright\mathcal{E}$ if:

• •

$\mathcal{D}=\sum_{i\in I}\alpha_{i}{\{{(C_{i},t_{i})}^{1}\}}$, $I$ countable set.

• •

$t_{i}$* is a $A_{i}$-state.*

• •

For every $i$, there exist an open tuple $K_{i}$, a tuple type $B_{i}=(\boldsymbol{\sigma}^{i},\boldsymbol{\tau}^{i})$, and $s_{i}$ a $B_{i}$-state, such that:

• •

$(\boldsymbol{\sigma}^{i},\boldsymbol{\tau}^{i},K^{i},A_{i})$* is a substitution judgment,*

• •

$t_{i}=\kappa_{i}[s_{i}]$**

• •

$\mathcal{E}=\sum_{i\in I}\alpha_{i}\cdot{\{{\textbf{F}(C_{i},(K_{i},A_{i})),s_{i}}^{1}\}}$**

Please observe that there are many possible distributions $\mathcal{E}$ that verify $\mathcal{D}\triangleright\mathcal{E}$. We can express the fact that $\triangleright$ is a congruence relation that doesn’t modify the underlying program, and that moreover, the relation $\triangleright$ is designed to preserve normal forms with respect to ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, by the following lemma:

Lemma 15

Let be $\mathcal{D}$, $\mathcal{E}$ such that $\mathcal{D}\triangleright\mathcal{E}$. Then:

• •

$\textbf{F}(\mathcal{D})=\textbf{F}(\mathcal{E})$.

• •

If $\textsf{S}(\mathcal{D})\subseteq NF(\mathbf{C\times\Delta(\mathscr{U})})$, it holds that $\textsf{S}(\mathcal{E})\subseteq NF(\mathbf{C\times\Delta(\mathscr{U})})$.

• Proof.

It is a direct consequence of the unfolding of the definition of $\triangleright$. $\Box$

Now, we are ready to define a relation $h\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}$, that intuitively corresponds to do a step ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, and then potentially change the way we split programs between internal part and external part.

Definition 17

We define a relation $h\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}$, where $h\in\mathbf{C\times\Delta(\mathscr{U})}$, and $\mathcal{D}$ a finite distribution over $\mathbf{C\times\Delta(\mathscr{U})}$, by the following rule:

[TABLE]

We define below the lifting of $\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}$ to distribution over $\mathbf{C\times\Delta(\mathscr{U})}$:

Definition 18

We define a one-step relation reduction $\mathcal{D}\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{E}$ on (finite) distributions over $\mathbf{C\times\Delta(\mathscr{U})}$ as follows:

[TABLE]

Since $\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}$ is non-confluent, we cannot use it to define a semantics for $\mathbf{C\times\Delta(\mathscr{U})}$ as we did for ${}\rightarrow_{\mathbf{C\times\Delta(\mathscr{U})}}{}$. We are going to define a notion of semantics for $\mathbf{C\times\Delta(\mathscr{U})}$ depending on what infinite sequance of reduction we are considering: for $h\in\mathbf{C\times\Delta(\mathscr{U})}$, we call infinite reduction sequence starting from $h$ a sequence $\mathit{s}=(\mathcal{D}_{n})_{n\in\mathbb{N}}$ of distributions over $\mathbf{C\times\Delta(\mathscr{U})}$, where $\mathcal{D}_{0}={\{{h}^{1}\}}$, and $\mathcal{D}_{n}\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}_{n+1}$ for every $n\in\mathbb{N}$. The idea is that every reduction sequence gave a different semantics for $h$, but that we obtain the same distribution over terms for all of them if we use $\textbf{F}(\cdot)$ on them. Let us formalize this idea.

Definition 19

If $h\in\mathbf{C\times\Delta(\mathscr{U})}$, and $\mathit{s}=(\mathcal{D}_{n})_{n\in\mathbb{N}}$ a reduction sequence starting from $h$. We call semantics of $h$ with respect to $\mathit{s}$, and we note ${\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}_{\mathit{s}}$ the distribution over $\mathbf{C\times\Delta(\mathscr{U})}$ given by ${\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}_{\mathit{s}}=\sup\{\mathscr{V}(\mathcal{D}_{n})\mid n\in\mathbb{N}\}$.

Please observe that Definition 19 is well-posed since the $\mathscr{V}(\mathcal{D}_{n})$ are an increasing sequence of distributions over normal forms.

We state below the analogue of the third point of Lemma 4 for up-to bisimulation:

Proposition 8

Let be $h\in\mathbf{C\times\Delta(\mathscr{U})}$, and an infinite reduction sequence $\mathit{s}=\mathcal{D}_{0}={\{{h}^{1}\}}\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}_{1}\ldots\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}_{n}\ldots\,$. Then $\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}_{\mathit{s}})=\llbracket\textbf{F}(h)\rrbracket$.

• Proof.

The proof is similar to the one of Lemma 4, and is based on the following two lemmas, that are a variant of Lemma 5 and 8: the following first lemma is used to show that $\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}_{\mathit{s}})\leq\llbracket\textbf{F}(h)\rrbracket$.

Lemma 16

Let be $\mathcal{D}$, $\mathcal{E}$ such that $\mathcal{D}\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{E}$. Then $\llbracket\textbf{F}(\mathcal{D})\rrbracket=\llbracket\textbf{F}(\mathcal{E})\rrbracket$.

[TABLE]

That other lemma is used to show the other direction, namely that $\textbf{F}({\llbracket h\rrbracket}^{\mathbf{C\times\Delta(\mathscr{U})}}_{\mathit{s}})\geq\llbracket\textbf{F}(h)\rrbracket$.

Lemma 17

Let be $h\in\mathbf{C\times\Delta(\mathscr{U})}$ such that $\textbf{F}(h)\not\in\mathscr{V}$, and an infinite reduction sequence $\mathcal{D}_{0}={\{{h}^{1}\}}\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}_{1}\ldots\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}_{m}\ldots\,$. Then there exists $i\in\mathbb{N}$, such that for every $\mathcal{E}$ and $n\in\mathbb{N}$ with $\textbf{F}(h)\stackrel{{\scriptstyle n}}{{\Rightarrow}}\mathcal{E}$, there exists a finite $\mathcal{F}\in\text{Distr}(\text{Unary}^{\mathbf{C\times\Delta(\mathscr{U})}})$, and an infinite reduction sequence $\mathcal{F}_{i}=\mathcal{F}\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{F}_{i+1}\ldots\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{F}_{m}\ldots$, verifying $\forall i,\,\overline{\mathcal{F}_{i}}^{\text{U}}\leq\overline{\mathcal{D}_{i}}^{\text{U}}$, and such that moreover $\textbf{F}(\mathcal{F})\stackrel{{\scriptstyle m}}{{\Rightarrow}}\mathcal{E}$, with $m<n$.

It can be expressed by the following diagram:

[TABLE]

$\Box$

Observe that, even if $\mathrel{R}$ is an up-to bisimulation, it does not necessarily means that $\widehat{\mathrel{R}}^{\mathscr{C}^{\mathbf{T}}}$ preserves ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$. We want to express the fact that it preserves $\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}$, but we have to be more careful, since this reduction relation is non-deterministic. To deal with it, we introduce a more general preservation notion:

Definition 20

We say that a relation $\mathrel{R}$ over $\mathbf{C\times\Delta(\mathscr{U})}$ is weakly preserved by $\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}$ if, for any $h,k\in\mathbf{C\times\Delta(\mathscr{U})}$ such that $h\mathrel{R}k$, and $h\not\in NF(\mathbf{C\times\Delta(\mathscr{U})})$, then there exists $\mathcal{D}$ and $\mathcal{E}$ such that $h\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{D}$, $k\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}\mathcal{E}$, and $\mathcal{D}\mathrel{R}\mathcal{E}$.

Our notion of weak preservation is enough to state the following variant of Proposition 5.

Proposition 9

Let $\mathscr{C}$ be a set of tuple contexts, $t,s$ two $A$-states and $\mathrel{R}$ a reflexive and symmetric relation weakly preserved by $\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, $\varepsilon$-bounding, and $\mathscr{C}$-closed with respect to $t$ and $s$. Then it holds that ${\delta^{c}_{\mathscr{C},!}}(t,s)\leq\varepsilon$.

An $\varepsilon$ up-to bisimulation verifies the condistions of Proposition9, as stated by the analogue of Proposition 7 below.

Proposition 10

Let be $\mathrel{R}$ an up-to bisimulation. Then $\widehat{\mathrel{R}}^{\mathscr{C}^{\mathbf{T}}}$ is weakly preserved by $\rightarrow^{\triangleright}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$ and $\varepsilon$-bounding, and $\mathscr{C}^{\mathbf{T}}$-closed with respect to every $t,s$ such that $t\mathrel{R}s$.

We are now ready to do the proof of Theorem 6. Let be $\mathrel{R}$ an $\varepsilon$ up-to bisimulation, ans $t,s\in\mathcal{S}_{\mathscr{L}_{\oplus}^{!{}}}$ such that $t\,{\mathrel{R}}\,s$. Using our completness result stated in Theorem 5, we see that it is enough to show that ${\delta^{c}_{\mathscr{C}^{\mathbf{T}},!}}(t,s)\leq\varepsilon$. Propositions 9 and 10 give us immediately the result.

Example 9

We can exploit the soundness of up-to bisimulation to obtain the contextual distance for our running example, and conclude that ${\delta^{c}_{!{(\tau\multimap\tau)},!}}(M_{\varepsilon},M_{\mu})=\sup_{n\in\mathbb{N}}\lvert\varepsilon^{n}-\mu^{n}\rvert$. The context distance between $M_{\varepsilon}$ and $M_{\mu}$ is thus strictly between [math] and $1$ whenever $\lvert\varepsilon-\mu\rvert$

6 Probabilistic $\lambda$-Calculi, in Perspective

The calculus $\Lambda_{\oplus}^{!,\parallel}$ we analyzed in this paper is, at least apparently, nonstandard, given the presence of parallel disjunction, but also because of the linear refinement it is based on. In this section, we will reconcile what we have done so far with calculi in the literature, and in particular with untyped probabilistic $\lambda$-calculi akin to those studied, e.g., in [9, 5].

We consider a language $\Lambda_{\oplus}$ defined by the following grammar:

[TABLE]

6.1 On Stable Fragments of $\mathscr{M}_{\oplus}^{!{}}$.

Our objective in this section is to characterize various notions of context distance for $\Lambda_{\oplus}$ by way of appropriate embeddings into $\Lambda_{\oplus}^{!}$, and thus by the LMC $\mathscr{M}_{\oplus}^{!{}}$. It is quite convenient, then, to understand when any fragment of $\mathscr{M}_{\oplus}^{!{}}$ is sufficiently robust so as to be somehow self-contained:

Definition 21

We say that the pair $(\hat{\mathcal{S}},\hat{\mathcal{A}})$, where $\hat{\mathcal{S}}\subseteq\mathcal{S}_{\mathscr{M}_{\oplus}^{!{}}}$, and $\hat{\mathcal{A}}\subseteq\mathbf{T}\times\mathcal{A}_{\mathscr{M}_{\oplus}^{!{}}}$ is a stable fragment of $\mathscr{M}_{\oplus}^{!{}}$ iff for every pair $(A,a)\in\hat{\mathcal{A}}$, for every $A$-state $t$, and for every $s\in\mathcal{S}$ such that $\mathcal{P}_{\mathscr{M}_{\oplus}^{!{}}}(t,a,s)>0$, it holds that $s\in\hat{\mathcal{S}}$.

Using a stable fragment of $\mathscr{M}_{\oplus}^{!{}}$, we can restrict the WLTS $\mathscr{L}_{\oplus}^{!{}}$ in a meaningful way. The idea is that we only consider some of the states of $\mathscr{L}_{\oplus}^{!{}}$, and we are able to choose the possible actions depending on the type of the state of $\mathscr{L}_{\oplus}^{!{}}$ we consider.

Definition 22

If $\mathscr{F}=(\hat{\mathcal{S}},\hat{\mathcal{A}})$ is a stable fragment of $\mathscr{M}_{\oplus}^{!{}}$, we define a WLTS by $\mathscr{L}_{\mathscr{F}}=(\mathcal{S}_{\mathscr{L}_{\mathscr{F}}},\mathcal{A}_{\mathscr{L}_{\mathscr{F}}},{}{\stackrel{{\scriptstyle\cdot}}{{\rightarrow}}}{{}_{\mathscr{F}}},w_{{\mathscr{F}}})$, as

[TABLE]

[TABLE]

and $w_{{\mathscr{F}}}$ is defined as expected.

We want to be able to define a notion of distance on a fragment of the original language $\Lambda_{\oplus}^{!}$, so that it verifies the soundness property for a restricted set of contexts. To do that, we need the restricted set of contexts $\mathscr{C}$ to be preserved by the stable fragment:

Definition 23

Let $\mathscr{F}=(\hat{\mathcal{S}},\hat{\mathcal{A}})$ be a stable fragment of $\mathscr{M}_{\oplus}^{!{}}$. Let $\mathscr{C}$ be a set of tuple contexts. We say that $\mathscr{C}$ is preserved by $\mathscr{F}$, if the following holds: for any $(C,A,\gamma)\in\mathscr{C}$ that is not an open value and any $A$-state $t$ in $\mathcal{S}_{\mathscr{L}_{\mathscr{F}}}$, there exists $a$ such that $(A,a)\in\hat{\mathcal{A}}\bigcup(\mathbf{T}\times\{\tau\})$, ${(C,t)}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{E}}$, and moreover:

[TABLE]

We are now able to provide guarantees that the contextual distance $\delta^{\text{c}}_{\mathscr{C}}$ with respect to our restricted set of contexts $\mathscr{C}$ is smaller that the distance defined on the LTS $\mathscr{L}_{\mathscr{F}}$ induced by our stable fragment $\mathscr{F}$. In the following, we assume to have fixed a stable fragment $\mathscr{F}=(\hat{\mathcal{S}},\hat{\mathcal{A}})$ of $\mathscr{M}_{\oplus}^{!{}}$, and $\mathscr{C}$ a set of tuple contexts preserved by $\mathscr{F}$.

Proposition 11

Let be $\mathrel{R}$ an $\varepsilon$-bisimulation on $\mathscr{L}_{\mathscr{F}}$. Then $\widehat{\mathrel{R}}^{\mathscr{C}}$ is preserved by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, $\varepsilon$-bounding, and $\mathscr{C}$-closed with respect to every $t,s$ such that $t\,{\mathrel{R}}\,s$.

• Proof.

• •

The fact that $\widehat{\mathrel{R}}^{\mathscr{C}}$ is $\mathscr{C}$-closed is a direct consequence of the definition of lifting.

• •

The fact that it is $\varepsilon$-bounding is a direct consequence of the definition of a $\varepsilon$-bisimulation.

• •

It is preserved by ${}{\stackrel{{\scriptstyle}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$: it is indeed guarantee by our definition of preservation of $\mathscr{C}$ by $\mathscr{F}$.

$\Box$

Proposition 12

Let $\mathscr{F}=(\hat{\mathcal{S}},\hat{\mathcal{A}})$ be a stable fragment of $\mathscr{M}_{\oplus}^{!{}}$, $\mathscr{C}$ a set of tuple contexts preserved by $\mathscr{F}$, and $t,s\in\mathcal{S}_{\mathscr{L}_{\mathscr{F}}}$. Then ${\delta^{\text{c}}_{\mathscr{C}}}(t,s)\leq{\delta^{b}_{\mathscr{L}_{\mathscr{F}}}}(t,s).$

• Proof.

Let be $\varepsilon={\delta^{b}_{\mathscr{L}_{\mathscr{F}}}}(t,s)$. Let be $\mathrel{R}$ the biggest $\varepsilon$-bisimulation on $\mathscr{L}_{\mathscr{F}}$. By lemma 3, it holds that $t\,{\mathrel{R}}\,s$. Using Proposition 11 and 5, we obtain that ${\delta^{c}_{\mathscr{C},!}}(t,s)\leq\varepsilon$, which is exactly the result. $\Box$

In the following, we make use of Proposition 12 on stable fragments corresponding to embeddings of $\Lambda_{\oplus}$ into $\Lambda_{\oplus}^{!}$. We will consider two different encodings depending on the underlying notion of evaluation.

6.2 Call-by-Name

$\Lambda_{\oplus}$ can first of all be endowed with call-by-name semantics, as in Figure 10. We use it to define an approximation semantics exactly in the same way as in Figure 1, and we take as usual the semantics of a term to be the least upper bound of its approximated semantics. Moreover, we denote by $\delta_{\text{cbn}}^{c}$ the context distance on $\Lambda_{\oplus}$, defined the natural way. We are going, in the remainder of this section, to use our results about $\Lambda_{\oplus}^{!}$ to obtain a characterization of $\delta_{\text{cbn}}^{c}$.

6.2.1 The Call-By-Name Embedding

Girard’s translation [19] gives us an embedding $\langle\cdot\rangle^{\text{cbn}}:\Lambda_{\oplus}\rightarrow\Lambda_{\oplus}^{!}$, defined as follows:

[TABLE]

Please observe that $\langle\cdot\rangle^{\text{cbn}}$ respects typing, in the sense that, when we define $\sigma^{\text{cbn}}=\mu{\alpha}.!{\alpha}\multimap\alpha$ , it holds that for every term $M$ of $\Lambda_{\oplus}$ whose free variables are in $\{x_{1},\ldots,x_{n}\}$, we can show that $!{x}_{1}:!{\sigma^{\text{cbn}}},\ldots,!{x}_{n}:!{\sigma^{\text{cbn}}}\vdash\langle M\rangle^{\text{cbn}}:\sigma^{\text{cbn}}.$

This definition allows us to have some useful properties:

Lemma 18

• •

Let be $M,N\in\Lambda_{\oplus}$, and $z\in\mathscr{X}$. Then $\langle M\{z/N\}\rangle^{\text{cbn}}=\langle M\rangle^{\text{cbn}}\{z/\langle N\rangle^{\text{cbn}}\}$;

• •

Let be $M$ a closed term in $\Lambda_{\oplus}$. Then $\langle\llbracket M\rrbracket\rangle^{\text{cbn}}=\llbracket\langle M\rangle^{\text{cbn}}\rrbracket$.

• •

Let be $M\in{\langle\Lambda_{\oplus}\rangle^{\text{cbn}}}$, such that there exists an evaluation context $E$, and $N\in\Lambda_{\oplus}$, verifying $\langle M\rangle^{\text{cbn}}=E[\langle N\rangle^{\text{cbn}}]$. There for any term $L\in\Lambda_{\oplus}$, it holds that $E[\langle L\rangle^{\text{cbn}}]\in\langle\Lambda_{\oplus}\rangle^{\text{cbn}}$.

6.2.2 Metrics for $\Lambda_{\oplus}$

It is very tempting to define a metric on $\Lambda_{\oplus}$ just as follows: ${\delta_{\text{cbn}}^{b}}(M,N)={\delta_{!{\sigma^{\text{cbn}}},!{}}^{b}}(!{\langle M\rangle^{\text{cbn}}},!{\langle N\rangle^{\text{cbn}}})$. We can easily see that it is sound with respect to the context distance for $\Lambda_{\oplus}$, since any context of this language can be seen, through $\langle\cdot\rangle^{\text{cbn}}$, as a context in $\Lambda_{\oplus}^{!}$. However, it is not complete, as shown by the following example:

Example 10

We consider $M=\Omega\,\oplus\,(\lambda x.\Omega)$ and $N={(\lambda x.\Omega)}$. We can see that ${\delta_{!{\sigma^{\text{cbn}}},!{}}^{b}}(!{\langle M\rangle^{\text{cbn}}},!{\langle N\rangle^{\text{cbn}}})=1$: indeed, when we define a sequence of $\Lambda_{\oplus}^{!}$-contexts by $C_{n}=\lambda{!{x}}.\left((\lambda y_{1}.\ldots\lambda y_{n}.(\lambda z.zy_{1},\ldots y_{n}))x\ldots x\right)[]$, we see that $\text{Obs}(!{\langle M\rangle^{\text{cbn}}})=1/{2^{n}}$ while $\text{Obs}(!{\langle N\rangle^{\text{cbn}}})=1$. But those contexts $C_{n}$ have more expressive power that any context in $\langle\Lambda_{\oplus}\rangle^{\text{cbn}}$, since they do something that none of the context from $\Lambda_{\oplus}$ can do: they evaluate a copy of the term, and then shift their focus to another copy of the term. It can be seen in the embedding: a term in $\langle\Lambda_{\oplus}\rangle^{\text{cbn}}$ has never several redexes in linear position. We are now going to explicit this idea, and show that ${\delta_{\text{cbn}}^{c}}(M,N)=\frac{1}{2}<{\delta_{\text{cbn}}^{b}}(M,N)$.

The way out consists in using the notion of stable fragment to refine the Markov Chain $\mathscr{M}_{\oplus}^{!{}}$ by keeping only the states and actions we are interested in.

Definition 24

We define a stable fragment $\mathscr{F}^{\text{cbn}}$ as specified in Figure 12, and a distance $\delta_{\text{cbn}}$ on $\Lambda_{\oplus}$ as:

[TABLE]

where $\hat{s}^{\text{cbn}}(M)=({\{{([\langle M\rangle^{\text{cbn}}],[])}^{1}\}},A^{0})$.

We need now to define a set of tuple contexts preserved by $\mathscr{F}^{\text{cbn}}$, the aim of applying Proposition 12.

Definition 25

$\mathscr{C}_{\text{cbn}}$* is the smallest set of tuple contexts such that:*

• •

If $M\in\Lambda_{\oplus}$ with $FV(M)\subseteq\{x_{1}\}$, then $(\langle M\rangle^{\text{cbn}},A^{0},\sigma^{\text{cbn}})\in\mathscr{C}_{\text{cbn}}$;

• •

If $(C,A^{0},\sigma^{\text{cbn}})\in\mathscr{C}_{\text{cbn}}$, and $C=E[x_{1}]$, it holds that $(E[y_{1}],A^{1},\sigma^{\text{cbn}})\in\mathscr{C}_{\text{cbn}}$.

$\mathscr{C}_{\text{cbn}}$ is designed to allow us to link $\delta_{\text{cbn}}^{c}$ and $\delta^{\text{c}}_{\mathscr{C}_{\text{cbn}}}$.

Lemma 19

For $M,N\in\Lambda_{\oplus}$ closed terms, ${\delta_{\text{cbn}}^{c}}(M,N)={\delta^{\text{c}}_{\mathscr{C}_{\text{cbn}}}}(\hat{s}^{\text{cbn}}(M),\hat{s}^{\text{cbn}}(N)).$

• Proof.

The proof is based on Lemma 18. $\Box$

Lemma 20

$\mathscr{C}_{\text{cbn}}$* is preserved by the stable fragment $\mathscr{F}^{\text{cbn}}$.*

• Proof.

Let be $(C,A,\gamma)\in\mathscr{C}_{\text{cbn}}$, and $t$ a $A$-state in $\mathscr{L}_{\mathscr{F}^{\text{cbn}}}$. Using the definition of $\mathscr{C}$, we may see that $\gamma=\sigma^{\text{cbn}}$, and moreover we are in one of the following cases:

• •

Or $A=A^{0}$, $C=\langle M\rangle^{\text{cbn}}$ with $FV(M)\subseteq\{x_{1}\}$ and $t$ is of the form $(\mathcal{D},A^{0})$, where $\mathcal{D}=\sum_{i\in\mathbb{N}}p_{i}\cdot{\{{([\langle N\rangle^{\text{cbn}}_{i}],[])}^{1}\}}$. Then we still have to consider separately two cases:

• •

or $\langle M\rangle^{\text{cbn}}=E[x_{1}]$. We take $a=({?}^{1})$. We can easily check that $(A^{0},({?}^{1}))\in\mathcal{A}_{\mathscr{M}_{\oplus}^{\text{cbn}}}\bigcup(\mathbf{T}\times\{\tau\})$. Moreover, we see that there exists $\mathcal{E}$ such that ${(C,t)}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{E}}$, and more precisely $\mathcal{E}={\{{(E[y_{1}],s)}^{1}\}}$ where $s$ is a $A^{1}$-state. Since $(E[y_{1}],A^{1},\sigma^{\text{cbn}})\in\mathscr{C}_{\text{cbn}}$ by construction, it holds that $\textsf{S}(\mathcal{E})\subseteq\bigcup_{B\in\mathbf{T}}\{(D,s)\mid s\text{ a }B\text{-state}\wedge\exists\eta\text{ s.t. }(D,B,\eta)\in\mathscr{C}_{\text{cbn}}\}$, which shows the result.

• •

or $\langle M\rangle^{\text{cbn}}=E[R]$, where $R$ is a redex. We take $a=\tau$, and we obtain the result by a similar reasoning as the previous case.

• •

Or $A=A^{1}$. Then $t$ is of the form $(\mathcal{D},A^{1})$, where $\mathcal{D}=\sum_{i\in\mathbb{N}}p_{i}\cdot([\langle N\rangle^{\text{cbn}}],[\langle V\rangle^{\text{cbn}}])$. Moreover, it implies that $C=E[y_{1}]$, and there exists $L$ such that $E[x_{1}]=\langle L\rangle^{\text{cbn}}$. Looking at the cbn encoding, we see that the only way to have $E[x_{1}]\in\langle\Lambda_{\oplus}\rangle^{\text{cbn}}$ is $E=F[[\cdot]!{\langle P\rangle^{\text{cbn}}}]$. It means that $C=F[y_{1}!{\langle P\rangle^{\text{cbn}}}]$. We take $a=@^{1}_{\kappa}$ with $\kappa=(\{1\},\{\},[\sigma^{\text{cbn}}],[\sigma^{\text{cbn}}],!{\langle P\rangle^{\text{cbn}}},\sigma^{\text{cbn}})$. We can easily check that $(A^{1},a)\in\mathcal{A}_{\mathscr{M}_{\oplus}^{\text{cbn}}}\bigcup(\mathbf{T}\times\{\tau\})$. Moreover, we see that there exists $\mathcal{E}$ and $s$ a $A^{1}$-state such that ${(C,t)}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{E}}$, and $\mathcal{E}={\{{(F[y_{1}],s)}^{1}\}}$. Using the third point of Lemma 18, and that $F[x_{1}!{\langle P\rangle^{\text{cbn}}}]\in\langle\Lambda_{\oplus}\rangle^{\text{cbn}}$, we see that $F[x_{1}]\in\langle\Lambda_{\oplus}\rangle^{\text{cbn}}$. Looking at the definition of $\mathscr{C}_{\text{cbn}}$, we see that it means that $(F[y_{1}],A^{1},\sigma^{\text{cbn}})\in\mathscr{C}_{\text{cbn}}$, and so we have the result.

$\Box$

Theorem 7** (Full Abstraction for CBN)**

${\delta_{\text{cbn}}^{c}}$* and ${\delta_{\text{cbn}}}$ coincide.*

• Proof.

We first show that $\delta_{\text{cbn}}$ is at least as discriminating $\delta_{\text{cbn}}^{c}$. Let be $M,N\in\Lambda_{\oplus}$. By definition of $\mathscr{L}_{\mathscr{F}^{\text{cbn}}}$, we know that $\hat{s}^{\text{cbn}}(M),\hat{s}^{\text{cbn}}(N)\in\mathcal{S}_{\mathscr{L}_{\mathscr{F}^{\text{cbn}}}}$. Moreover, we know by Lemma 20 that $\mathscr{C}_{\text{cbn}}$ is preserved by $\mathscr{F}^{\text{cbn}}$. So we can apply Proposition 12, and we see that ${\delta^{\text{c}}_{\mathscr{C}_{\text{cbn}}}}(\hat{s}^{\text{cbn}}(M),\hat{s}^{\text{cbn}}(N))\leq{\delta_{\text{cbn}}}(M,N)$. Then, soundness follows using Lemma 19. When proving completeness part, we rely on an “intrinsic” characterization of $\delta_{\text{cbn}}$. The details can be found in the next section. $\Box$

6.2.3 An intrinsic trace characterization of $\delta_{\text{cbn}}$

Looking at the structure of $\mathscr{F}^{\text{cbn}}$, we see that we can in fact give an intrinsic definition of $\delta_{\text{cbn}}$, without considering tuples and exponential constructs. In fact, every sequence of actions in $\mathscr{L}_{\mathscr{F}^{\text{cbn}}}$ can be see as an element of the set $\mathscr{T}_{r}^{\text{cbn}}$ defined by:

[TABLE]

We can now talk about the probability for a term $M$ to effectuate a trace $\mathsf{T}$ defined by:

[TABLE]

and we obtain a simple characterization of $\delta_{\text{cbn}}$:

Proposition 13

Let be $M,N\in\Lambda_{\oplus}$. Then:

[TABLE]

Please observe that we can alternatively see traces as contexts. As a consequence, if we define CIU-contexts in $\Lambda_{\oplus}$ as $E=\left(\lambda x.xM_{1}\ldots M_{n}\right)[]$. We may express $\delta_{\text{cbn}}$ in a purely contextual way:

Proposition 14

Let be $M,N\in\Lambda_{\oplus}$. Then ${\delta_{\text{cbn}}}(M,N)=\sup_{E\text{ CIU context}}\lvert{\sum\nolimits_{\llbracket E[M]\rrbracket}}-{\sum\nolimits_{\llbracket E[N]\rrbracket}}\rvert$.

Please observe that Proposition 14 allows us to see easily that ${\delta_{\text{cbn}}}(M,N)\leq{\delta_{\text{cbn}}^{c}}(M,N)$. As such, it allows us to do the completeness part of the proof Theorem 7.

6.3 Call-by-Value

In a similar way, we can endow $\Lambda_{\oplus}$ with a call-by-value semantics, and embedd it into $\Lambda_{\oplus}^{!}$. We are then able to define a suitable fragment of $\mathscr{M}_{\oplus}^{!{}}$, a suitable set of tuple contexts preserving it, and a caracterisation of a call-by-value context distance for $\Lambda_{\oplus}$ follows. While the construction of the stable fragment (and the set of tuple contexts to consider) are more involved than in the call-by-name case, we noticed that the caracterisation we obtain seem to have some similarities with the way environmental bisimulation for a CBV probabilistic $\lambda$-calculus was defined in [33]. In this section, we endow $\Lambda_{\oplus}$ with a call-by-value semantics, as specified in Figure 13.

We denote $\delta_{\text{cbv}}^{c}$ the contextual metric on $\Lambda_{\oplus}$ induced by this semantics. We define a new embedding: $\Lambda_{\oplus}\rightarrow\Lambda_{\oplus}^{!}$, which respects the CBV semantics, as:

[TABLE]

We define $\sigma^{\text{cbv}}$ as the following type : $\sigma^{\text{cbv}}=\mu{\alpha}.!{(\alpha\multimap\alpha)}$. We define $\tau^{\text{cbv}}=\sigma^{\text{cbv}}\multimap\sigma^{\text{cbv}}$: it verifies $\sigma^{\text{cbv}}=^{\mathscr{A}}!{\tau^{\text{cbv}}}$. For any term $M\in\Lambda_{\oplus}$, if $FV(M)=\{z_{1},\ldots,z_{n}\}$ it holds that $(!{z}_{i}:\sigma^{\text{cbv}})_{1\leq i\leq n}\vdash\langle M\rangle^{\text{cbv}}:\sigma^{\text{cbv}}$.

We will use later the following nice property of the encoding:

Lemma 21

Let be $M$ and $N$ in $\Lambda_{\oplus}$, and $z$ a free variable of $M$. Then $\langle M\rangle^{\text{cbv}}\{z/\lambda{!{z}}.\langle N\rangle^{\text{cbv}}\}\in\langle\Lambda_{\oplus}\rangle^{\text{cbv}}$.

• Proof.

The proof is by induction on the form of $M$. $\Box$

Lemma 22

Let be $M\in\Lambda_{\oplus}$. Then for any $V\in\textsf{S}({{\llbracket\langle M\rangle^{\text{cbv}}\rrbracket}})$, it holds that $V\in\langle\Lambda_{\oplus}\rangle^{\text{cbv}}$.

• Proof.

The proof uses Lemma 21. $\Box$

Again, we are now going to define a stable fragment of $\mathscr{M}_{\oplus}^{!{}}$. However, contrary to the call-by-name case, it does not contain the full call-by-value encoding $\Lambda_{\oplus}$. It actually contains only the encoding of values in $\Lambda_{\oplus}$, which allows us to have a more tractable characterization. We are able to treat the general case simply by noting that for any term $M$ and $N$, it holds that ${\delta_{\text{cbv}}^{c}}(M,N)={\delta_{\text{cbv}}^{c}}(\lambda z.M,\lambda z.N)$.

Definition 26

We define a fragment $\mathscr{F}^{\text{cbv}}=(\mathcal{S}_{\mathscr{M}_{\oplus}^{\text{cbv}}},\mathcal{A}_{\mathscr{M}_{\oplus}^{\text{cbv}}})$ as specified in Figure 14, and a metric $\delta_{\text{cbv}}$ on $\Lambda_{\oplus}$ specified by:

[TABLE]

Please observe that contrary to the cbn-case, we do not need to restrict action by considering the type of states.

Proposition 15

$\mathscr{F}^{\text{cbv}}$* is a stable fragment of $\mathscr{M}_{\oplus}^{!{}}$.*

• Proof.

Let be $(K,A)\in\mathcal{S}_{\mathscr{M}_{\oplus}^{\text{cbv}}}$. Since $(K,A)$ is in $\mathcal{S}_{\mathscr{M}_{\oplus}^{\text{cbv}}}$, there exist $\varphi$, and $\boldsymbol{M},\boldsymbol{N},\boldsymbol{L}$ respectively $n,m,p$ term sequences, such that $K=({{\lambda{!{x}}.\boldsymbol{M}}},{\lambda{!{x}}.\boldsymbol{N};!{(\lambda{!{x}}.\boldsymbol{L})}}_{\varphi})$ and $A=A_{n,(m,p)}^{\varphi}$. Let be $a$ such that $(A,a)\in\mathcal{A}_{\mathscr{M}_{\oplus}^{\text{cbv}}}$. Let be $s=(H,B)$ such that $\mathcal{P}_{\mathscr{M}_{\oplus}^{!{}}}(t,a,s)>0$. We want to show that $s\in\mathcal{S}_{\mathscr{M}_{\oplus}^{\text{cbv}}}$. We distinguish cases depending on $a$.

• –

Or $a=(!^{i})$. It implies that $H=(\lambda{!{x}}.\boldsymbol{M},{\lambda{!{x}}.\boldsymbol{N};!{(\lambda{!{x}}.\boldsymbol{L})}}_{\varphi};V)$ with $\vdash V:\sigma^{\text{cbv}}$ and $B=([{(\tau^{\text{cbv}})}^{n}],{[{(\tau^{\text{cbv}})}^{m},{(!{\tau^{\text{cbv}}})}^{p}]}_{\varphi},\sigma^{\text{cbv}})$. Since $V$ is obtained by the evaluation of a term in $\langle\Lambda_{\oplus}\rangle^{\text{cbv}}$, it is also in $\langle\Lambda_{\oplus}\rangle^{\text{cbv}}$. It allows us to see that $V$ is of the form $!{\lambda{!{x}}.P}$. So we see that we can construct a permutation $\psi$ from $\{1,\ldots,m+p+1\}$ such that $s=((\lambda{!{x}}.\boldsymbol{M},{\lambda{!{x}}.\boldsymbol{N};!{(\lambda{!{x}}.(\boldsymbol{L};P))}}_{\psi}))$, and $B=([{(\tau^{\text{cbv}})}^{n}],{[{(\tau^{\text{cbv}})}^{m},{(!{\tau^{\text{cbv}}})}^{p+1}]}_{\psi})$. As a consequence, $s\in\mathcal{S}_{\mathscr{M}_{\oplus}^{\text{cbv}}}$.

• –

Or $a=({?}^{i})$. It implies that $H=(\lambda{!{x}}.(\boldsymbol{M};L_{j}),{\lambda{!{x}}.\boldsymbol{N};!{(\lambda{!{x}}.\boldsymbol{L}_{\{1,\ldots,p\}\setminus\{j\}})}}_{\varphi_{\text{remove}}(\{j\})})$, when $\varphi(m+j)=i$, and $B=([{(\tau^{\text{cbv}})}^{n+1}],{[{(\tau^{\text{cbv}})}^{m},{(!{\tau^{\text{cbv}}})}^{p-1}]}_{\varphi_{\text{remove}}(\{j\})})$. So we can see that $s\in\mathcal{S}_{\mathscr{M}_{\oplus}^{\text{cbv}}}$.

• –

Or $a=@^{i}_{\kappa}$ with $\kappa\in\mathscr{J}^{\mathscr{V}}_{\text{cbv}}$. Then $\kappa=(E,F,\boldsymbol{\sigma},\boldsymbol{\tau},M,\sigma^{\text{cbv}})$ and $M$ is an open value in $\langle\Lambda_{\oplus}\rangle^{\text{cbv}}$. Since there exist $s$ such that $\mathcal{P}_{\mathscr{M}_{\oplus}^{!{}}}(t,a,s)>0$, it means that $E\subseteq\{1,\ldots,n\}$, and $F\subseteq\{1,\ldots m+p\}$, and moreover $(\boldsymbol{\sigma},\boldsymbol{\tau})$ is one of the $A^{m,n,p}_{\varphi}$. verifying $1\leq\varphi(i)\leq m$ (that is, $\boldsymbol{\tau}_{i}=\tau^{\text{cbv}}\multimap\tau^{\text{cbv}}$). By a similar reasoning as previous cases, we can see that $s\in\mathcal{S}_{\mathscr{M}_{\oplus}^{\text{cbv}}}$.

$\Box$

Please observe that for any term $M\in\Lambda_{\oplus}$, the associated state $\hat{s}_{\sigma^{\text{cbv}}}(\langle\lambda z.M\rangle^{\text{cbv}})$ is in $\mathcal{S}_{\mathscr{M}_{\oplus}^{\text{cbv}}}$.

As in the previous section, we define a suitable set $\mathscr{C}_{\text{cbv}}$ of tuple contexts preserving $\mathscr{F}^{\text{cbv}}$, in order to apply Proposition 12.

Definition 27

We define a set of tuple contexts $\mathscr{C}_{\text{cbv}}$ as those of the form $(C_{1}\ldots C_{k}D,(\boldsymbol{\sigma},\boldsymbol{\tau}),\sigma^{\text{cbv}})$ such that:

• •

$C_{i}\in\{y_{j}\mid\tau_{j}=\sigma^{\text{cbv}}\multimap\sigma^{\text{cbv}}\}\cup\{\lambda{!{z}}.z\langle M\rangle^{\text{cbv}}\mid z\not\in FV(M)\}\cup\lambda{!{z}}.\langle\Lambda_{\oplus}\rangle^{\text{cbv}}\cup\{x_{j}\}$**

• •

$D\in\langle\Lambda_{\oplus}\rangle^{\text{cbv}}\cup\{y_{j}\mid\tau_{j}=!{(\sigma^{\text{cbv}}\multimap\sigma^{\text{cbv}})}\}\cup\{x_{j}\}$**

Proposition 16

$\mathscr{C}_{\text{cbv}}$* is preserved by $\mathscr{F}^{\text{cbv}}$.*

• Proof.

Let be $(C,A,\gamma)\in\mathscr{C}_{\text{cbv}}$. Let be $a$ such that $(A,a)\in\mathcal{A}_{\mathscr{M}_{\oplus}^{\text{cbv}}}$. Let be $t$ a $A$-state $t$ in $\mathcal{S}_{\mathscr{L}_{\mathscr{F}^{\text{cbv}}}}$.Let be $\mathcal{E}$ such that ${(C,t)}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{\mathcal{E}}$. Let be $h\in\textsf{S}(\mathcal{E})$. We note $h=(F,s)$, and $B$ the tuple type such that $s$ is a $B$-state. We have to show that $(F,B,\sigma^{\text{cbv}})\in\mathscr{C}_{\text{cbv}}$.

Please observe that there exists actually only one $a$ such that ${(C,t)}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{}$, and it depends only on $C$. Consequently, we do the proof by considering separately the different form of $C$. We know, by definition of $\mathscr{C}_{\text{cbv}}$, that $C$ is of the form $C_{1}\ldots C_{k}D$.

• –

If one of the $C_{i}$ is of the form $x_{j}$, we consider the smallest index $i$ for which it happens. Then $a=(!^{i})$, and $F=C_{1},\ldots,!{y_{n+1}},\ldots C_{n}D$.

• –

Otherwise, $C_{1}\ldots C_{k}[\cdot]$ is an evaluation context. Then:

If $D=x_{i}$. We have that $a=(!^{i})$. It follows that ${t}{\stackrel{{\scriptstyle a}}{{\rightarrow}}}_{\mathbf{C\times\Delta(\mathscr{U})}}{s}$, and $F=C_{1},\ldots,C_{k}y_{m+p+1}$. So we can see that the result holds.

• *

If $D=y_{j}$, with $\tau_{j}=!{\tau^{\text{cbv}}}$. Then it holds that $a=({?}^{i})$., and $F=C_{1},\ldots,C_{k}!{x_{n+1}}$.

• *

If $D$ is in $\langle\Lambda_{\oplus}\rangle^{\text{cbv}}$. We show the result by induction on the term $L$ such that $D=\langle L\rangle^{\text{cbv}}$.

• ·

Or $D=\langle M\,\oplus\,N\rangle^{\text{cbv}}$. Then $a=\tau$, and $F=C_{1},\ldots,C_{k}G$, with $G\in\{\langle M\rangle^{\text{cbv}},\langle N\rangle^{\text{cbv}}\}\subseteq\langle\Lambda_{\oplus}\rangle^{\text{cbv}}$ and so the result holds.

• ·

Or $D=\langle MN\rangle^{\text{cbv}}$. Then $D=(\lambda{!{z}}.z{\langle N\rangle^{\text{cbv}}}){\langle M\rangle^{\text{cbv}}}$. We can take $G=\langle M\rangle^{\text{cbv}}$, $C_{n+1}=(\lambda{!{z}}.z{\langle N\rangle^{\text{cbv}}})$, and we can see that $C=C_{1},\ldots,C_{n+1}G$, and so we can apply the induction hypothesis to $G=\langle M\rangle^{\text{cbv}}$.

• ·

If $D$ is an open value. It means that $D=!{\lambda{!{z}}.\langle M\rangle^{\text{cbv}}}$, or $D=!{x_{i}}$. Please observe that $C_{n}$ is always an open value (by construction). It means that the redex $C_{n}D$ is going to be reduced.

• item

If $C_{n}=y_{j}$, with $\tau_{j}=\sigma^{\text{cbv}}\multimap\sigma^{\text{cbv}}$, then $a=@^{j}_{\kappa}$, where $\kappa=(E,F,\boldsymbol{\sigma},\boldsymbol{\tau},D,\sigma^{\text{cbv}})$, where $E\subseteq\{1,\ldots,n\}$, and $!{{\boldsymbol{x}}_{E}}:!{\boldsymbol{\sigma}_{E}},{\boldsymbol{y}}_{F}:\boldsymbol{\tau}_{F}\vdash D:\sigma^{\text{cbv}}$ and we see that indeed $\kappa\in\mathscr{J}^{\mathscr{V}}_{\text{cbv}}$. Moreover, if we note $q$ the cardinality of $E$, we can see that $F=C_{1},\ldots,C_{n-1}y_{n+1-{q+1}}$. As a consequence, we have the result.

• item

If $C_{n}=\lambda{!{z}}.(z\langle N\rangle^{\text{cbv}})$. Then $a=\tau$. Please observe that we can define $C_{n+1}$ such that $!{C}_{n+1}=D$. Now, please observe that we should have $F=C_{1},\ldots,C_{n-1}C_{n+1}\langle N\rangle^{\text{cbv}}$, and so the result holds.

• item

If $C_{n}=\lambda{!{z}}.(\langle N\rangle^{\text{cbv}})$. Then if $D=!{x_{i}}$, we have that $F=C_{1},\ldots,C_{n-1}\langle M\{z/x_{i}\}\rangle^{\text{cbv}}$, and we have the result. Similarly, if $D=!{\lambda{!{z}}.\langle M\rangle^{\text{cbv}}}$, it holds that $F=C_{1},\ldots,C_{n-1}\langle M\{z/\lambda{!{z}}.\langle M\rangle^{\text{cbv}}\}\rangle^{\text{cbv}}$. We use Lemma 21 to obtain the result.

$\Box$

Definition 28

We define a metric $\delta_{\text{cbv}}$ on $\Lambda_{\oplus}$ by: ${\delta_{\text{cbv}}}(M,N)={\delta^{b}_{\mathscr{L}_{\mathscr{F}^{\text{cbv}}}}}(\hat{s}_{\sigma^{\text{cbv}}}(!{\langle\lambda x.M\rangle^{\text{cbv}}}),\hat{s}_{\sigma^{\text{cbv}}}(!{\langle\lambda x.N\rangle^{\text{cbv}}})).$

Theorem 8** (Full Abstraction for CBV)**

$\delta_{\text{cbv}}^{c}$* and $\delta_{\text{cbv}}^{b}$ coincide.*

The proof can be found in [6]. Again, soundness is based on Proposition 12, while completeness relies on yet another characterization of the context distance.

6.3.1 Intrinsic characterization

We don’t have an intrinsic characterization as simpler as in the cbn case. However, we can express the distance $\delta_{\text{cbv}}^{c}$ using a LMC $\mathscr{M}_{\oplus}^{\text{cbv}}$, designed to be a simplified and untyped version of $\mathscr{M}_{\oplus}^{!{}}$, and that doesn’t use the embedding.

Definition 29

We define a labelled Markov chain $\mathscr{M}_{\oplus}^{\text{cbv}}=(\mathscr{S}_{\oplus}^{\text{cbv}},\mathscr{A}_{\oplus}^{\text{cbv}},\mathscr{P}_{\oplus}^{\text{cbv}})$, where:

• •

$\mathscr{S}_{\oplus}^{\text{cbv}}=\{(\boldsymbol{V},n)\mid\boldsymbol{V}\text{ a }n\text{-sequence of values}\}$**

• •

$\mathscr{A}_{\oplus}^{\text{cbv}}=\{@^{M}_{i}\mid\exists k\in\mathbb{N},\,M=x_{k}\text{ or }L=\lambda z.M\}$**

• •

$\mathscr{P}_{\oplus}^{\text{cbv}}$* is defined in Figure 15.*

As for $\Lambda_{\oplus}^{!}$, we transform the LMC $\mathscr{M}_{\oplus}^{\text{cbv}}$ into a purely non-deterministic WLTS. We define $\mathscr{L}_{\oplus}^{\text{cbv}}=(\mathcal{S}_{\mathscr{L}_{\oplus}^{\text{cbv}}},\mathcal{A}_{\mathscr{L}_{\oplus}^{\text{cbv}}},{}{\stackrel{{\scriptstyle\cdot}}{{\rightarrow}}}{},w)$, where:

• •

The set of states is $\mathcal{S}_{\mathscr{L}_{\oplus}^{\text{cbv}}}=\bigcup_{n\in\mathbb{N}}\left(\text{Distr}(\{\boldsymbol{V}\mid\boldsymbol{V}\text{ a }n\text{-sequence }\})\times\{n\}\right)$

• •

The set of actions is $\mathcal{A}_{\mathscr{L}_{\oplus}^{\text{cbv}}}=\mathscr{A}_{\oplus}^{\text{cbv}}\cup\mathbb{N}$,

• •

The transition function ${}{\stackrel{{\scriptstyle\cdot}}{{\rightarrow}}}{}$ is defined as follows:

[TABLE]

• •

The weight $w$ is such that $w(\mathcal{D},n)={\sum\nolimits_{\mathcal{D}}}$.

Please remember that we give in Section 5.3 a definition of the trace metric $\delta^{b}_{\mathscr{L}}$ for any WLTS. We can apply it to $\mathscr{L}_{\oplus}^{\text{cbv}}$, and it gives us a characterization of $\delta_{\text{cbv}}$.

Proposition 17

Let be $M,N\in\Lambda_{\oplus}$. Then:

[TABLE]

7 Related Work

This is definitely not the first work on metrics in the context of programming languages semantics. A very nice introduction to the topic, together with a comprehensive (although outdated) list of references can be found in [36]. One of the many uses of metrics is as an alternative to order-theoretic semantics. This has also been applied to higher-order languages, and to deterministic $\mathsf{PCF}$ [15].

If one focuses on probabilistic programming languages, the first attempts at using metrics as a way to measure “how far” two programs are, algebraically or behaviourally, are due to Giacalone et al. [18], and Desharnais et al. [11, 12], who both consider process algebras in the style of Milner’s CCS. Most of further work in this direction has focused on concurrent specifications. Among the recent advances in this direction (and without any hope of being comprehensive), we can cite Gebler et al.’s work on uniform continuity as a way to enforce compositionality in metric reasoning [17, 16].

Finally, great inspiration for this work came from the many contributions on metrics for labelled Markov chains and processes appeared in the last twenty years (e.g. [37, 13]).

8 Conclusions

We have shown how the context distance can be characterized so as to simplify concrete proofs, and to which extent this metric trivializes. All this has been done in a universal linear $\lambda$-calculus for probabilistic computation. This clarifies to which extent refining equivalences into metrics is worth in such a scenario. The tuple-based techniques in Section 5.6 are potentially very interesting in view of possible applications to cryptography, as hinted in [4]. This is indeed what we are working on currently.