# Probabilistic coherence spaces are fully abstract for probabilistic PCF

Thomas Ehrhard, Christine Tasson, Michele Pagani

► To cite this version:

Thomas Ehrhard, Christine Tasson, Michele Pagani. Probabilistic coherence spaces are fully abstract for probabilistic PCF. The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14), Jan 2014, San Diego, CA, United States. pp.309-320, 10.1145/2535838.2535865 . hal-04670288

HAL Id: hal-04670288

https://hal.science/hal-04670288v1

Submitted on 12 Aug 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Probabilistic Coherence Spaces are
Fully Abstract for Probabilistic PCF *

Thomas Ehrhard

Christine Tasson

Laboratoire PPS - CNRS - Université Paris Diderot

thomas.ehrhard@pps.univ-paris-diderot.fr

christine.tasson@pps.univ-paris-diderot.fr

Michele Pagani

Laboratoire LIPN - Université Paris 13

michele.pagani@lipn.univ-paris13.fr

## Abstract

Probabilistic coherence spaces (PCoh) yield a semantics of higher-order probabilistic computation, interpreting types as convex sets and programs as power series. We prove that the equality of interpretations in PCoh characterizes the operational indistinguishability of programs in PCF with a random primitive.

This is the first result of full abstraction for a semantics of probabilistic PCF. The key ingredient relies on the regularity of power series and introduces, in denotational semantics, techniques coming from Calculus.

Along the way to the theorem, we design a weighted intersection type assignment system giving a logical presentation of PCoh.

*Categories and Subject Descriptors* CR-number [subcategory]: third-level

## 1. Introduction

Probabilistic behaviors appear in many places in the study of programming languages, for instance if the environment of a program behaves randomly or if the program uses probabilistic constructs.

To understand how the introduction of probabilities changes the computational landscape, we use *Semantics*. Indeed, in the last decades [24, 27, 30], semantics has succeeded in giving insights on the way programs compute. More precisely, *operational semantics* allows one to formalize a program by the sequence of its execution steps, while *denotational semantics* represents programs by functions in some mathematical space relating the interpretations of inputs and outputs in a compositional way. If this last mathematical representation is correct and accurate enough, then denotational properties lead to computational features. A key example is *full abstraction* [23], stating that operational indistinguishability (i.e. behaving in the same way in any context) is characterized by denotational equivalence (i.e. having the same interpretation). So semantics is useful both to give a precise meaning to syntactical constructs and to separate non-equivalent programs.

Of course, probabilistic semantics have already been investigated. First, the domain-theoretic approach has led to a *probabilistic powerdomain* [19, 29] which is a sibling of the non-deterministic power domain [27]. This approach follows the computational monad method [25]: programs are interpreted as functions from the input domain to the powerdomain of the output domain. Intuitively, a program takes an input and returns a probability distribution on outputs. This line of work has been continued by the continuous random variable construction [15], introducing standard tools of probability theory into semantics. Secondly, the game-theoretic approach [1, 18] has been extended with probabilistic features [5]. Intuitively, probabilistic programs are interpreted as probabilistic strategies, that are stochastic processes on the plays of the games associated with the types of the programs.

*Quantitative semantics* follows another tradition stemming from Linear Logic models [10, 11]. From the very beginning, Linear Logic has been associated with intuitions coming from calculus and linear algebra [7, 8, 12]. Indeed, programs are interpreted as entire series between mathematical spaces or as analytic functors between sets [17], and programs that use their resources only once are interpreted as linear functions. This connection with resource consumption has been fruitful in the last decade with the introduction of differential nets and resource calculus [2, 9]. Recently, quantitative semantics has been explicitly related to the study of quantitative properties such as time or space consumed by a computation [22]. This illustrates a new paradigm where a semiring of scalars allows one to encode non-deterministic or probabilistic computations as opposed to the domain paradigm where monads are used. Another important tenet of Linear Logic is the perfect duality between programs and environments since a program can be seen as the environment of other programs. Therefore, representing probabilistic environments or programs will boil down to the same study. *Probabilistic coherence spaces* provide a quantitative semantics [4, 14] which model probabilistic computations.

The main contribution of the present work is to show that probabilistic coherence spaces provide a fully abstract model of PPCF, a probabilistic extension of the functional programming language PCF [28]. Although the proof follows the general pattern that consists in finding a *definable* context that separates two terms, the key ingredient is based on Calculus (see Lemma 25) since programs are interpreted as power series.

To our knowledge, no known model of probabilistic PCF has yet been proved to be fully abstract. Games semantics provide fully abstract models of standard PCF via an extensional collapse [1, 18]. This technique has been adapted to probabilistic game semantics, providing a fully abstract model of probabilistic idealized ALGOL [5] (an extension of probabilistic PCF with references). Our result characterizes the operational indistinguishability without the

<footnote>* Partially founded by French ANR project COQUAS (number 12 JS02 006 01) and CNRS chair "Logique linéaire et calcul".</footnote>

<footnote>Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.</footnote>

<footnote>POPL '14, January 22-24, 2014, San Diego, CA, USA.</footnote>

<footnote>Copyright is held by the owner/author(s). Publication rights licensed to ACM.</footnote>

<footnote>ACM 978-1-4503-2544-8/14/01...$15.00.</footnote>

<footnote>http://dx.doi.org/10.1145/2535838.2535865</footnote>
instructions and that they call once or twice their input. Their interpretation is given by a matrix indexed by finite multisets (the input) and integers (the output). Coefficients are non zero only if the multiset is of size one or two:

$$ \llbracket \text{Once} \rrbracket : \qquad \llbracket \text{Twice} \rrbracket : \begin{cases} \llbracket [0], 0 \rrbracket \mapsto \frac{1}{2} \\ \llbracket [0], 1 \rrbracket \mapsto \frac{1}{2} \\ \llbracket [a], 42 \rrbracket \mapsto 1 & \text{if } a \neq 0 \\ (m, a) \mapsto 0 & \text{otherwise.} \end{cases} \qquad \begin{cases} \llbracket [0, 0], 0 \rrbracket \mapsto \frac{1}{2} \\ \llbracket [0, 0], 1 \rrbracket \mapsto \frac{1}{2} \\ \llbracket [0, a], 42 \rrbracket \mapsto 2 & \text{if } a \neq 0 \\ \llbracket (a, b], 0 \rrbracket \mapsto 1 & \text{if } a \neq 0, b \neq 0 \\ (m, a) \mapsto 0 & \text{otherwise.} \end{cases} $$

On the second example, two quantitative phenomena are mixed up. The first one is probabilistic: coefficient $\frac{1}{2}$ comes from the use of coin. The second one stems from branching construction: two different execution traces are leading to 42, either the two outcomes of the random variable $x$ are first 0, and then $a \neq 0$, or its outcomes are first $a$, and then 0. In our model, these traces are gathered in the same multiset $[0, a]$ and the coefficient 2 is the combinatorial counterpart. This gives a hint of why programs are not represented as random variables.

Now, the interaction of a probabilistic program with a probabilistic data boils down to a matrix product adapted to take into account multiplicities.

Let us consider a probabilistic datum $x : \text{Int}$ and a program $M : \text{Int} \Rightarrow \text{Int}$. As a reminder, the $a$-th coefficient $\llbracket x \rrbracket_a$ is the probability that $a$ is the outcome of $x$. The probability $\llbracket (M) x \rrbracket_b$, that $(M) x$ returns $b$, is given by decomposing the computation in pairwise disjoint events. Each event corresponds to an intermediate multiset $m$ gathering the input values that are effectively used during computation:

$$ \llbracket (M) x \rrbracket_b = \sum_{m \in \mathcal{M}_f(\mathbb{N})} \llbracket M \rrbracket_{(m,b)} \llbracket x \rrbracket^m, \quad (2) $$

(see Notation 1 for $\llbracket x \rrbracket^m$) is the probability that independent calls to $x$ returns the values gathered in $m$. In this way, every coefficient $\llbracket (M) x \rrbracket_b$ is a power series with infinitely many variables, that are the $\llbracket x \rrbracket_a$ for $a \in \mathbb{N}$.

Applying Formula (2), we compute the non zero coefficients:

$$ \llbracket (\text{Once}) x \rrbracket_0 = \llbracket (\text{Once}) x \rrbracket_1 = \frac{1}{2} \llbracket x \rrbracket_0 \qquad \llbracket (\text{Once}) x \rrbracket_{42} = \sum_{a \ge 1} \llbracket x \rrbracket_a $$

$$ \llbracket (\text{Twice}) x \rrbracket_0 = \frac{1}{2} \llbracket x \rrbracket_0^2 + \sum_{a,b \ge 1} \llbracket x \rrbracket_a \llbracket x \rrbracket_b \\ \llbracket (\text{Twice}) x \rrbracket_1 = \frac{1}{2} \llbracket x \rrbracket_0^2 \qquad \llbracket (\text{Twice}) x \rrbracket_{42} = 2 \sum_{a \ge 1} \llbracket x \rrbracket_a \llbracket x \rrbracket_a $$

Notice that every coefficient of $\llbracket (\text{Once}) x \rrbracket$ is a linear function and every coefficient of $\llbracket (\text{Twice}) x \rrbracket$ is a polynomial of degree 2. Besides, Once and Twice preserve subprobability distributions:

$$ \sum_b \llbracket (\text{Once}) x \rrbracket_b = \frac{1}{2} \llbracket x \rrbracket_0 + \frac{1}{2} \llbracket x \rrbracket_0 + \sum_{a \ge 1} \llbracket x \rrbracket_a \le 1 \\ \sum_b \llbracket (\text{Twice}) x \rrbracket_b = \llbracket x \rrbracket_0^2 + 2 \llbracket x \rrbracket_0 \sum_{a \ge 1} \llbracket x \rrbracket_a + (\sum_{a \ge 1} \llbracket x \rrbracket_a)^2, \\ = (\sum_{a \ge 0} \llbracket x \rrbracket_a)^2 \le 1. $$

### 3. Probabilistic PCF

We define the language PPCF in Figure 1. This system is a minor variant with respect to the probabilistic extension of PCF presented in [4] (see Remark 6). The grammar of terms is obtained by adding to standard PCF a random number generator rand. The

typing rules (Figure 1(b)) are the usual ones, with rand of type Int $\Rightarrow$ Int. From now on, we call program a closed term of type Int. Figure 1(c) gives the one step reduction relation $\stackrel{\kappa}{\Rightarrow}$, implementing a weak head-reduction (i.e. a lazy call-by-name strategy). The relation is weighted with a probability $\kappa \in [0, 1]$ equal to 1 except for steps firing a (rand) n re dex, reducing to any numeral in $\{0, ..., n-1\}$ with equal probability $\frac{1}{n}$. The probability of a reduction sequence is the product of the weights of all its steps. Some notational conventions are introduced in Figure 1(d) and will be used henceforth.

**Example 2.** Notice (by induction on $n \ge 1$) that the term choose($M_i$)$_{i=1}^n$, for $1 \le i \le n$ reduces (in several steps) to any $M_i$ with equal probability $\frac{1}{n}$. In general, any reduction sequence has a probability given by a rational number in $[0, 1]$, since rand $n$ introduces just fractions.

**Example 3.** The fix-point constructor yields infinite reduction sequences, like the typical loop $\Omega_A \stackrel{1}{\Rightarrow} (\lambda x^A \cdot x) \Omega_A \stackrel{1}{\Rightarrow} \Omega_A$. However, we can have terms with infinite reduction sequences but converging to a normal form with probability 1. Indeed, take $M \stackrel{\Delta}{=} \text{fix}(\lambda x^{\text{Int}} \cdot x \oplus \emptyset)$ (see notations in Figure 1(d)) we have:

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

The probability that $M$ reduces to $\emptyset$ is equal to the sum of the probabilities of all finite reductions sequences from $M$ to $\emptyset$, which is $\sum_{n=0}^{\infty} \frac{1}{2^{n+1}} = 1$, $n$ being the number of loops taken by a sequence.

A way for precisely defining the probability of convergence of a term to a normal form is by giving the operational semantics as a Markov process over the set of PPCF terms, following [4]. The transition matrix $\text{PROBA} \in [0, 1]^{\text{PPCF} \times \text{PPCF}}$ is defined by:

$$ \text{PROBA}_{M,N} \stackrel{\Delta}{=} \begin{cases} \kappa & \text{if } M \stackrel{\kappa}{\Rightarrow} N, \\ 1 & \text{if } M = N \text{ is a normal form,} \\ 0 & \text{otherwise.} \end{cases} \quad (3) $$

Notice that $\text{PROBA}_{M,N}$ is well-defined since there exists at most one reduction step $M \stackrel{\kappa}{\Rightarrow} N$, once fixed $M$ and $N$. PROBA is a stochastic matrix (i.e. for all $M$, $\sum_{N \in \text{PPCF}} \text{PROBA}_{M,N} = 1$). The value of $\text{PROBA}_{M,N}$ intuitively describes the probability of evolving from the state $M$ to the state $N$ in one step.

A term $M$ is absorbing whenever $\text{PROBA}_{M,M} = 1$: the absorbing states are those which are invariant under the transition matrix. Notice that the normal forms are all absorbing, but the converse is false, e.g. $\Omega$ is an absorbing term.

The $n$-th power $\text{PROBA}^n$ of the matrix PROBA is a stochastic matrix on PPCF (in case $n = 0$, we have the identity matrix on PPCF). Intuitively, the value of $\text{PROBA}^n_{M,N}$ is the probability of evolving from the state $M$ to the state $N$ in exactly $n$ steps.

**Proposition 4** ([4, Lemma 32]). Let $M \in \text{PPCF}$ and $N$ absorbing, the sequence $\{\text{PROBA}^n_{M,N}\}_{n \in \mathbb{N}}$ is monotonic.

We can thus define, for every program $M$ and $n \in \mathbb{N}$:

$$ \text{PROBA}^\infty_{M,n} \stackrel{\Delta}{=} \sup_{k=0}^\infty (\text{PROBA}^k_{M,n}) \quad (4) $$

Intuitively, $\text{PROBA}^\infty_{M,n}$ defines the probability that $M$ reaches a numeral $n$ in an arbitrary number of steps.

In standard PCF the observational pre-order is defined with respect to the termination of a term in a context of type Int. In a probabilistic framework like PPCF, one can refine such a pre-order
Types $A, B, C ::= \mathbf{Int} \mid A \Rightarrow B$ Terms $M, N, P ::= x \mid \lambda x^A.M \mid (M) N \mid \mathbf{fix}(M) \mid \mathbf{0} \mid \mathbf{s}(M) \mid \mathbf{p}(M) \mid \mathbf{if}(M, N, P) \mid \mathbf{rand}$

(a) Grammar of types and terms. The constant Int is the base type of integers. Given $n \in \mathbb{N}$, $\underline{n}$ will denote its associated numeral, defined as $s^n(\underline{0})$.

$\frac{\Gamma, x : A \vdash x : A}{\Gamma, x : A \vdash M : B}$ $\frac{\Gamma \vdash M : A \Rightarrow B}{\Gamma \vdash (M) N : B}$ $\frac{\Gamma \vdash M : A \Rightarrow A}{\Gamma \vdash \mathbf{fix}(M) : A}$

$\frac{\Gamma \vdash \mathbf{P} : \mathbf{Int}}{\Gamma \vdash \mathbf{s}(P) : \mathbf{Int}}$ $\frac{\Gamma \vdash \mathbf{P} : \mathbf{Int}}{\Gamma \vdash \mathbf{p}(P) : \mathbf{Int}}$ $\frac{\Gamma \vdash M : \mathbf{Int}}{\Gamma \vdash \mathbf{if}(M, N, P) : A}$ $\frac{\Gamma \vdash M : \mathbf{Int}}{\Gamma \vdash \mathbf{rand} : \mathbf{Int}} \Rightarrow \mathbf{Int}$

(b) Simple type assignment system.

$\frac{(\lambda x^A.M) N \stackrel{1}{\rightarrow} M [N/x]}{\mathbf{fix}(M) \stackrel{1}{\rightarrow} (M) \mathbf{fix}(M)}$ $\frac{\mathbf{if}(\underline{0}, N, P) \stackrel{1}{\rightarrow} N}{\mathbf{if}(\underline{n+1}, N, P) \stackrel{1}{\rightarrow} P}$ $\frac{\mathbf{p}(n+1) \stackrel{1}{\rightarrow} \underline{n}}{(\mathbf{rand}) \underline{n} \stackrel{1}{\rightarrow} \underline{k}}$

$\frac{M \stackrel{\kappa}{\rightarrow} M', M \text{ not abstract.}}{(M) N \stackrel{\kappa}{\rightarrow} (M') N}$ $\frac{M \stackrel{\kappa}{\rightarrow} M'}{\mathbf{s}(M) \stackrel{\kappa}{\rightarrow} \mathbf{s}(M')}$ $\frac{M \stackrel{\kappa}{\rightarrow} M'}{\mathbf{p}(M) \stackrel{\kappa}{\rightarrow} \mathbf{p}(M')}$ $\frac{M \stackrel{\kappa}{\rightarrow} M'}{\mathbf{if}(M, N, P) \stackrel{\kappa}{\rightarrow} \mathbf{if}(M', N, P)}$ $\frac{M \stackrel{\kappa}{\rightarrow} M'}{(\mathbf{rand}) M \stackrel{\kappa}{\rightarrow} (\mathbf{rand}) M'}$

(c) Reduction rules. In case $n = 0$, $(\mathbf{rand}) \underline{n}$ is a normal form.

$\Omega_A \stackrel{\Delta}{=} \mathbf{fix}(\lambda x^A.x)$ $M \oplus N \stackrel{\Delta}{=} \mathbf{if}((\mathbf{rand}) \underline{2}, M, N)$

$\mathbf{choose}() \stackrel{\Delta}{=} \Omega_A$ $\mathbf{choose}(M_1, \dots, M_{n+1}) \stackrel{\Delta}{=} \mathbf{if}((\mathbf{rand}) \underline{n+1}, M_{n+1}, \mathbf{choose}(M_1, \dots, M_n))$

$\mathbf{if}(\wedge_{i=1}^0 M_i, N, P) \stackrel{\Delta}{=} N$ $\mathbf{if}(\wedge_{i=1}^{n+1} M_i, N, P) \stackrel{\Delta}{=} \mathbf{if}(M_{n+1}, \mathbf{if}(\wedge_{i=1}^n M_i, N, P), P)$

$\mathbf{if}(M = \underline{0}, N, P) \stackrel{\Delta}{=} \mathbf{if}(M, N, P)$ $\mathbf{if}(M = \underline{n+1}, N, P) \stackrel{\Delta}{=} \mathbf{if}(\mathbf{p}(M) = \underline{n}, N, P)$

(d) Notational conventions. Also, we can use $\mathbf{choose}(M_i)_{i=1}^n$ as a shortcut for $\mathbf{choose}(M_1, \dots, M_n)$.

<caption>**Figure 1:** Probabilistic extension of PCF.</caption>

by comparing the probability of convergence. Let $C^{\Gamma,A}$ be the set of contexts $Q$ mapping terms $M$ of type $A$ in the environment $\Gamma$, into programs $Q[M]$, i.e. closed terms of type Int.

**Definition 5** (Observational pre-order). Given $\Gamma \vdash M : A$, and $\Gamma \vdash N : A$, we define$^4$:

$$M \sqsubseteq_{\Gamma} N \quad \text{iff} \quad \forall Q \in C^{\Gamma,A}, \mathrm{PROBA}_{Q[M],0}^{\infty} \leq \mathrm{PROBA}_{Q[N],0}^{\infty}.$$

Let $\equiv_{\Gamma}$ be the equivalence induced by $\sqsubseteq_{\Gamma}$.

**Remark 6.** There are slightly different probabilistic primitives that can be added to PCF. We have chosen a quite standard one, **rand**, implementing CAML function Random.int. In [5, 21] it is also considered the more basic Coin $\stackrel{\Delta}{=} (\mathbf{rand}) \underline{2}$. Another possibility is to allow an arbitrary superposition of two terms $M \oplus_{\kappa} N$, for $\kappa \in [0, 1]$, evaluating to $M$ with probability $\kappa$ and to $N$ with probability $1 - \kappa$, see e.g. [15, 19]. Concerning $n$-ary distributions, there is $\oplus_{i=1}^n \kappa_i M_i$, evaluating to any $M_i$ with probability $\kappa_i$ [26]. Finally, [4] allows any probabilistic distribution over the whole set of numerals $(\kappa_n)_{n \in \mathbb{N}}$, evaluating to $\underline{n}$ with probability $\kappa_n$.

Obviously, **Coin** can be defined as $\oplus_{\frac{1}{2}}$ as well as $(\mathbf{rand}) \underline{2}$. Also, both $\oplus_{\kappa}$ and **rand** are definable as $\oplus_{i=1}^{\underline{n}} \kappa_i M_i$, and the latter

as $(\kappa_n)_{n \in \mathbb{N}}$. However, the converses are less trivial. In [5, Figure 6] the authors show how to define **rand** as a recursive program using just **Coin**. On the contrary, $\oplus_{\kappa}$ is strictly more expressive than **rand** and **Coin**, since it is not true that all real numbers can be approximated by series of rational numbers generated from PPCF terms (hence recursively enumerable series). One can then wonder whether the observational equivalence on PCF terms depends on the chosen probabilistic primitive. The full abstraction gives a negative answer to the question: all such primitives induce the same observational equivalence on PCF terms, which is in fact the equivalence induced by **Pcoh** (Corollary 28).

# 4. Probabilistic Coherence Spaces

We present probabilistic coherence spaces [4, 14] and recall the main results needed to state and prove the full abstraction theorem.

The category **PCoh** of probabilistic coherence spaces is a model of PPCF. As usual, types are interpreted as objects of the category and programs as maps between the interpretation of the input and output types.

Actually, **PCoh** is underlied by a model of linear logic that we do not make explicit for the sake of brevity, but we refer to [4].

## 4.1 Probabilistic Coherence Spaces

A probabilistic coherence space is a pair $(|A|, P(A))$ of a set $|A|$ and a set $P(A)$ of vectors in the module $\mathbb{R}_+^{|A|}$. Intuitively, the elements in $|A|$ represent atomic data, while the vectors in $P(A)$

<footnote>$^4$ The numeral $\underline{0}$ chosen for testing the equality is not significant. Indeed, from a context $Q$ semi-separating two terms $M, N$ on a numeral $\underline{n}$, i.e. such that $\mathrm{PROBA}_{Q[M],\underline{n}}^{\infty} \not\leq \mathrm{PROBA}_{Q[N],\underline{n}}^{\infty}$, one can get a context semi-separating $M$ and $N$ on another numeral $\underline{m}$ by applying a suitable number of $\mathbf{p}()$ or $\mathbf{s}()$ constructors.</footnote>
express probabilistic data. At the ground type, P (Int) is in fact the convex set of the subprobability distributions of the elements in |Int|. However, at higher-order types, this intuition is lost<fnref n="5" /> and the definition of P (A) depends on a duality condition describing the probability of having an interaction between a datum of type A (which is a program) and an environment.

Consider a program and an environment interacting on atomic data a included in a set $|A|$ such that their respective interpretation are positive real vectors: $v, w \in \mathbb{R}_+^{|A|}$. Their pairing gives a quantitative estimation of the interaction success

$$ \langle v, w \rangle \triangleq \sum_{a \in |A|} v_a w_a \in \bar{\mathbb{R}}_+. \quad (5) $$

We say that their interaction is probabilistic whenever $\langle v, w \rangle \le 1$. We then define a polar operation on sets of vectors $P \subseteq \mathbb{R}_+^{|A|}$ as

$$ P^{\perp} \triangleq \{w \in \mathbb{R}_+^{|A|} \text{ s.t. } \forall v \in P \ \langle v, w \rangle \le 1\}. \quad (6) $$

The probabilistic duality environment/program is then enforced in our model by the closedness condition $P^{\perp \perp} = P$.

**Definition 7** ([4, 14]). A probabilistic coherence space, or PCS for short, is a pair $\mathcal{A} = (|\mathcal{A}|, P(\mathcal{A}))$ where $|\mathcal{A}|$ is a countable set called the web of $\mathcal{A}$ and $P(\mathcal{A})$ is a subset of $\mathbb{R}_+^{|\mathcal{A}|}$ satisfying:

1. $P(\mathcal{A})^{\perp \perp} = P(\mathcal{A})$,

2. $\forall a \in |\mathcal{A}|, \exists \kappa > 0, \forall v \in P(\mathcal{A}), v_a \le \kappa$,

3. $\forall a \in |\mathcal{A}|, \exists \kappa > 0, \kappa \in \mathcal{A} \in P(\mathcal{A})$.

As a side effect, Condition (1) forces $P(\mathcal{A})$ to be a convex set. Condition (2) requires the projection of $P(\mathcal{A})$ in any direction to be bounded, while (3) forces $P(\mathcal{A})$ to cover every direction.<fnref n="6" />

**Example 8.** The set $P(\text{Int})$ of subprobability distributions over $\mathbb{N}$ yields a PCS. In particular, $P(\text{Int})^{\perp \perp} = P(\text{Int})$, its polar being $P(\text{Int})^{\perp} = [0, 1]^N$.

## 4.2 The category PCoh

The objects of PCoh are the PCSs and the set $\text{PCoh}(\mathcal{A}, \mathcal{B})$ of morphisms from $\mathcal{A}$ to $\mathcal{B}$ is the set of matrices $\phi \in \mathbb{R}_+^{M_f(|\mathcal{A}|) \times |\mathcal{B}|}$ such that $\forall v \in P(\mathcal{A}), \phi(v) \in P(\mathcal{B})$, where

$$ \forall b \in |\mathcal{B}|, (\phi(v))_b \triangleq \sum_{m \in \mathcal{M}_f(|\mathcal{A}|)} \phi_{m,b} \cdot v^m, \quad (7) $$

(see Notation 1 for the definition of $v^m$). Following Section 2, a morphism is presented as a matrix that gathered the coefficients of the power series described by the Equation (7).

The identity on $\mathcal{A}$ is given by the matrix

$$ \mathrm{Id}_{m,a}^{\mathcal{A}} \triangleq \begin{cases} 1 & \text{if } m = [a], \\ 0 & \text{otherwise.} \end{cases} $$

In fact, we have $\mathrm{Id}^{\mathcal{A}}(v) = v$, for every $v \in P(\mathcal{A})$.

Let $\phi \in \text{PCoh}(\mathcal{A}, \mathcal{B})$ and $\psi \in \text{PCoh}(\mathcal{B}, \mathcal{C})$, their composition must satisfy: $\forall v \in P(\mathcal{A}), (\psi \circ \phi)(v) = \psi(\phi(v))$. In matricial terms, this comes out as: $\forall c \in |\mathcal{C}|$,

$$ \sum_{m \in \mathcal{M}_f(|\mathcal{A}|)} (\psi \circ \phi)_{m,c} \cdot v^m = \sum_{p \in \mathcal{M}_f(|\mathcal{B}|)} \psi_{p,c} \cdot (\phi(v))^p \\ = \sum_{p \in \mathcal{M}_f(|\mathcal{B}|)} \psi_{p,c} \cdot \prod_{b \in \text{Supp}(p)} \left( \sum_{q \in \mathcal{M}_f(|\mathcal{A}|)} \phi_{q,b} \cdot v^q \right)^{p(b)}. $$

Now, to extract the coefficient of the monomial $v^m$, we distribute product over sum. This amounts to choosing a partition of $m = \bigcup (q_{(b,i)})(b,i) \in p$ matching the enumeration $\{(b, i) \text{ s.t. } b \in \text{Supp}(p), i \le p(b)\}$ of p.

Therefore, the composition $\psi \circ \phi$ is defined<fnref n="7" /> as the matrix coefficients, for $m \in \mathcal{M}_f(|\mathcal{A}|)$ and $c \in |\mathcal{C}|$:

$$ (\psi \circ \phi)_{m,c} \triangleq \sum_{p \in \mathcal{M}_f(|\mathcal{B}|)} \psi_{p,c} \sum_{\substack{(m_{(b,i)})(b,i) \in p \\ \text{s.t.} \\ m=\bigcup(m_{(b,i)})}} \prod_{(b,i) \in p} \phi_{m_{(b,i)},b}. \quad (8) $$

## 4.3 PCoh is Cartesian Closed

The cartesian product of any countable family $(\mathcal{A}_i)_{i \in I}$ of PCSs is:

$$ |\prod_{i \in I} \mathcal{A}_i| \triangleq \bigcup_{i \in I} (\{i\} \times |\mathcal{A}_i|), \\ P(\prod_{i \in I} \mathcal{A}_i) \triangleq \left\{ v \in (\mathbb{R}_+)^{|\prod_{i \in I} \mathcal{A}_i|} \text{ s.t. } \forall i \in I, \pi_i(v) \in P(\mathcal{A}_i) \right\}, $$

where $\pi_i(v)$ is the vector in $\mathbb{R}_+^{|\mathcal{A}_i|}$ denoting the i-th component of $v$, i.e. $(\pi_i(v))_a \triangleq v_{(i,a)}$.

The j-th projection $\text{Pr}^j \in \text{PCoh}(\prod_{i \in I} \mathcal{A}_i, \mathcal{A}_j)$ and the product $\langle \phi_i \rangle_{i \in I} \in \text{PCoh}(\mathcal{B}, \prod_{i \in I} \mathcal{A}_i)$ are given by:

$$ \text{Pr}_{m,a}^j \triangleq \begin{cases} 1 & \text{if } m = [(j, a)], \\ 0 & \text{otherwise.} \end{cases} \quad (\langle \phi_i \rangle_{i \in I})_{p,(j,a)} = (\phi_j)_{p,a} $$

The terminal object 1 is given by the empty product $(\emptyset, \{0\})$. Notice that the set of points of a PCS $\mathcal{A}$, i.e. the set $\text{PCoh}(1, \mathcal{A})$, is isomorphic to the convex set $P(\mathcal{A})$.

**Notation 9.** We write $\mathcal{A}_1 \times \mathcal{A}_2$ for the binary product: in the sequel, we present any $v \in P(\mathcal{A}_1 \times \mathcal{A}_2)$ as the pair $(\pi_1(v), \pi_2(v)) \in P(\mathcal{A}_1) \times P(\mathcal{A}_2)$ of its components.

Notice that the set $\mathcal{M}_f(|\prod_{i \in I} \mathcal{A}_i|)$ is isomorphic to the set-theoretic cartesian product $\prod_{i \in I} (\mathcal{M}_f(|\mathcal{A}_i|))$, via the map associating any $m \in \mathcal{M}_f(|\prod_{i \in I} \mathcal{A}_i|)$ with the I-indexed family $(m_i)_{i \in I}$ defined as $m_i(a) \triangleq m(i, a)$. This means that any morphism $\phi \in \text{PCoh}(\prod_{i \in I} \mathcal{A}_i, \mathcal{B})$ can be presented as a matrix indexed by sequences in $(\prod_{i \in I} \mathcal{M}_f(|\mathcal{A}_i|)) \times |\mathcal{B}|$.

The object of morphisms is defined as

$$ |\mathcal{A} \Rightarrow \mathcal{B}| \triangleq \mathcal{M}_f(|\mathcal{A}|) \times |\mathcal{B}|, \quad P(\mathcal{A} \Rightarrow \mathcal{B}) \triangleq \text{PCoh}(\mathcal{A}, \mathcal{B}). $$

$\text{PCoh}$ is then turned into a cartesian closed category by the evaluation $\text{Ev} \in \text{PCoh}((\mathcal{A} \Rightarrow \mathcal{B}) \times \mathcal{A}, \mathcal{B})$ and the currying function $\text{Cur}(\phi) \in \text{PCoh}(\mathcal{C}, \mathcal{A} \Rightarrow \mathcal{B})$, for every $\phi \in \text{PCoh}(\mathcal{C} \times \mathcal{A}, \mathcal{B})$, defined as:

$$ \text{Ev}_{(m,p),a} \triangleq \begin{cases} 1 & \text{if } m = [(p,v)], \\ 0 & \text{otherwise,} \end{cases} \quad \text{Cur}(\phi)_{m,(p,b)} \triangleq \phi_{(m,p),b} $$

Notice that the above equations use Notation 9, e.g. representing a multiset in $\mathcal{M}_f(|(\mathcal{A} \Rightarrow \mathcal{B}) \times \mathcal{A}|)$ as a pair $(m, p)$ of multisets in $\mathcal{M}_f(|\mathcal{A} \Rightarrow \mathcal{B}|) \times \mathcal{M}_f(|\mathcal{A}|)$.

Actually, the category PCoh is well-pointed in the sense that the equality of morphisms is extensional, i.e. given two matrices $\phi, \psi \in \text{PCoh}(\mathcal{A}, \mathcal{B})$, if for every $v \in P(\mathcal{A})$, $\phi(v) = \psi(v)$, then $\phi = \psi$. To sum up, we have:

<footnote n="5">⁵P ($\mathcal{A}$) is not anymore a subset of $[0, 1]^{|\mathcal{A}|}$, see discussion in Section 2.</footnote>

<footnote n="6">⁶These conditions are introduced in [4] for keeping finite all the scalars involved, yet they are not explicitly stated in the definition of PCS in [14].</footnote>

<footnote n="7">⁷The definition of Equation (8) is due to [17]. On a side note, remark that in [4], the authors use another formulation in which identical summands produced by different partitions are gathered. This gives rise to multinomial coefficients that are hidden in the sums of the present formulation. However, the two definitions give rise to the same matrix.</footnote>
**Proposition 10** ([4, §1.6]). **PCoh** is a well pointed cartesian closed category.

## 4.4 Object of numerals and Cpo-Enrichement

The object of numerals of **PCoh** is the PCS $\mathcal{I}nt \triangleq (\mathbb{N}, \mathbb{P}(\mathcal{I}nt))$ equipped with the morphisms $z \in \mathbf{PCoh}(\mathbf{1}, \mathcal{I}nt) \simeq \mathbb{P}(\mathcal{I}nt)$, pred, succ $\in \mathbf{PCoh}(\mathcal{I}nt, \mathcal{I}nt)$, and ifz $\in \mathbf{PCoh}(\mathcal{I}nt \times \mathcal{I}nt \times \mathcal{I}nt, \mathcal{I}nt)$ defined as

$$z_n = \delta_{0,n}, \quad \text{pred}_{m,n} = \delta_{m,[n+1]}, \quad \text{succ}_{m,n+1} = \delta_{m,[n]},$$

$$\text{ifz}_{(m,p,q),n} = \begin{cases} 1 & \text{if } (m,p,q) = ([0], [n], []), \\ & \text{or } (m,p,q) = ([k+1], [], [n]), \\ 0 & \text{otherwise.} \end{cases}$$

The natural order on $\mathbb{R}_+$ enriches **PCoh** with a cpo-structure, defined componentwise on morphisms: i.e., given $\phi, \psi \in \mathbf{PCoh}(\mathcal{A}, \mathcal{B})$

$$\phi \le \psi \quad \text{iff} \quad \forall m \in \mathcal{M}_f(|\mathcal{A}|), \forall b \in \mathcal{M}_f(|\mathcal{B}|), \phi_{m,b} \le \psi_{m,b}.$$

The matrix **0** is the minimum element and the lub of a directed net $(\phi_d)_{d \in D}$ is then given by

$$(\sup_{d \in D}(\phi_d))_{m,b} \triangleq \sup_{d \in D}((\phi_d)_{m,b}),$$

**Remark 11.** The componentwise order on matrices is not extensional, i.e. there are $\phi, \psi \in \mathbf{PCoh}(\mathcal{A}, \mathcal{B})$ such that $\forall v \in \mathbb{P}(\mathcal{A}), \phi(v) \le \psi(v)$, but $\phi \not\le \psi$. For example, take $\phi, \psi \in \mathbf{PCoh}(\mathcal{I}nt, \mathcal{I}nt)$:

$$\phi_{m,n} \triangleq \begin{cases} 1 & \text{if } m = [k], n = 0, \\ 0 & \text{otherwise.} \end{cases}, \quad \psi_{m,n} \triangleq \begin{cases} 1 & \text{if } m = [], n = 0, \\ 0 & \text{otherwise.} \end{cases}$$

Although $\phi \not\le \psi$, for every subprobability distribution of natural numbers $v \in \mathbb{P}(\mathcal{I}nt)$, we get $\phi(v) = (\sum_k v_k, 0, 0, \dots) \le (1, 0, 0, \dots) = \psi(v)$. In fact, we will use this mismatch for disproving the inequality full abstraction in Section 6.

## 4.5 PCoh is an Adequate Model of PPCF

The model of PPCF is obtained by extending the usual categorical interpretation of PCF to **rand**.

With a type $\mathcal{A}$, we associate a PCS $\mathcal{A}$, by induction on the type: $\mathcal{I}nt \mapsto \mathcal{I}nt$ and $\mathcal{A} \Rightarrow \mathcal{B} \mapsto \mathcal{A} \Rightarrow \mathcal{B}$.

Let $\Gamma = x_1 : A_1, \dots, x_n : A_n$. The interpretation of a judgment $\Gamma \vdash M : \mathcal{A}$ is a morphism $[[M]]^\Gamma$ of **PCoh**($\coprod_{i=1}^n \mathcal{A}_i, \mathcal{B}$), defined in Figure 2 by structural induction on the unique derivation of $\Gamma \vdash M : \mathcal{B}$.

The fix-point operator $\text{fix}(M)$ is the lub of its approximants, given by induction by

$$\text{fix}^0 \phi \triangleq \mathbf{0}, \quad \text{fix}^{n+1} \phi \triangleq \text{Ev} \circ \langle \phi, \text{fix}^n \phi \rangle.$$

The operator **rand** is defined by using (a multiset variant of) the matrix **Rand** of Equation (1):

$$[[\text{rand}]]_{m,k} \triangleq \begin{cases} \frac{1}{n} & \text{if } m = [n], k < n, \\ 0 & \text{otherwise.} \end{cases}$$

Together with the categorical interpretation of a term, we describe its action on the vectors in the convex set associated with its input type. Notice that, since the category is well pointed of the category, this action univocally determines the interpretation of the term. Notice also that the matrices interpreting the basic constructs in Figure 2 have 0, 1 coefficients, except for $[[\text{rand}]]$ which is interpreted as the random function that introduces rational numbers in $[0, 1]$. Coefficients greater than 1 may be produced by composition of morphisms (Equation 8).

Thanks to Notation 9, $[[M]]^\Gamma$ can be described as a vector indexed by a tuple $(\vec{m}, b)$ of $\vec{m} \in \mathcal{M}_f(|\Gamma|)$ and a web element $b \in |\mathcal{B}|$. This convention will be used hereafter.

**Example 12.** If **Coin** is identified with $(\text{rand})^2$, then the interpretation of **Once** and **Twice** are the matrices given in Section 2.

Consider the term $\Omega_A \triangleq \text{fix}(\lambda x^A . x)$. Notice that $[[\lambda x^A . x]]$ is different from zero only on the web elements of the form $([a], a)$, so that $\text{fix}^n [[\lambda x^A . x]](0) = \mathbf{0}$ for any natural number $n$. We conclude $[[\Omega_A]] = \mathbf{0}$, as expected.

Consider now the term $P \triangleq \text{fix}(\lambda x^{\text{Int}} . x \oplus \mathbf{0})$. We have that $[[\lambda x^{\text{Int}} . x \oplus \mathbf{0}]]_{(m,a)} = \frac{1}{2} [[x]]_a^m + \frac{1}{2} [[0]]_a^m$, i.e. it is equal to $\frac{1}{2}$ when $m = [a]$, or when $m = []$ and $a = 0$, otherwise it is equal to 0. This means that $\text{fix}^n [[\lambda x^{\text{Int}} . x \oplus \mathbf{0}]](0) = \frac{1}{2} + \frac{1}{4} + \dots + \frac{1}{2n}$, for any $n > 0$. We conclude that $[[P]] \triangleq \sup_n \text{fix}^n [[\lambda x^{\text{Int}} . x \oplus \mathbf{0}]](0) = 1$.

**Proposition 13** (Soundness [4]). The semantics is invariant under reduction, i.e. for every $\Gamma \vdash M : \mathcal{B}$:

$$[[M]]^\Gamma = \sum_N \text{PROBA}_{M,N} [[N]]^\Gamma.$$

*Proof (Sketch).* The invariance under reduction rules of the standard PCF redexes follows by cartesian closedness and the cpo-enrichement of **PCoh**. The soundness of the reduction of $(\text{rand})_n$ is straight from the definition of $[[\text{Rand}]]$. The soundness of the context rules depends on the fact that the interpretation of a context is linear in the argument associated with the fired redex. For example, the soundness of the context rule associated with application depends on the equality: $\text{Ev} \circ \langle \kappa\phi + \mu\psi, \xi \rangle = \kappa(\text{Ev} \circ \langle \phi, \xi \rangle) + \mu(\text{Ev} \circ \langle \psi, \xi \rangle)$ □

**Theorem 14** (Adequacy [4]). Let $M$ be a closed term of type $\mathcal{I}nt$. Then, $[[M]]$ is the sub-probability distribution on $\mathbb{N}$ such that

$$\forall n \in \mathbb{N}, [[M]]_n = \text{PROBA}_{\mathbb{M}, \mathbb{N}}^{\infty}.$$

**Remark 15.** Adequacy allows one to prove that specific primitives are not definable in the language. A noteworthy example is the parallel or function [27]. In our setting, this should be a closed term $\text{por} : \mathcal{I}nt \Rightarrow \mathcal{I}nt \Rightarrow \mathcal{I}nt$ such that $\text{PROBA}_{((\text{por})_0)\Omega, 0, 0, 0}^{\infty}$, $\text{PROBA}_{((\text{por})_1)\Omega, 1, 1}$ and $\text{PROBA}_{((\text{por})_\Omega)\Omega, 1, 1}$ are equal to 1. By adequacy, $[[\text{por}]](e_0)(e_0)_1 = [[\text{por}]](e_1)(\mathbf{0})_0 = [[\text{por}]](\mathbf{0})(e_1)_0 = 1$. By definition of a morphism in **PCoh**, $[[\text{por}]](e_0)(e_0)_0$ must be a subprobability distribution, hence $[[\text{por}]](e_0)(e_0)_0 = 0$. That implies $[[\text{por}]]([1], [1])_0 = 0$. On the other hand, $[[\text{por}]](e_1)(e_1)_0 \ge [[\text{por}]](e_1)(\mathbf{0})_0 + [[\text{por}]](\mathbf{0})(e_1)_0 - [[\text{por}]]([1], [1])_0 = 2$, which contradicts that $[[\text{por}]](e_1)(e_1)$ is a subprobability distribution. We conclude that $\text{por}$ is not a term of PPCF.

However, let us mention that the *Gustave function* is a valid morphism of **PCoh** (see [13]).

Full abstraction extends to higher-order types the perfect matching syntax / semantics stated by adequacy on $\mathcal{I}nt$. One direction of full abstraction is indeed a consequence of Theorem 14.

**Corollary 16** (Abstraction). Given $\Gamma \vdash M : A$, and $\Gamma \vdash N : A$, we have that $[[M]] \le [[N]]$ implies $M \sqsubseteq_\Gamma N$. In particular, $[[M]] = [[N]]$ implies $M \equiv_\Gamma N$.

*Proof.* By induction on $C[]$, one proves that $[[M]] \le [[N]]$ implies $[C[M]] \le [C[N]]$. Then the result follows from Theorem 14. □

## 5. Full Abstraction

We prove *equational full abstraction* (Theorem 27), that is the converse of the part of Corollary 16 dealing with equality. This is a straightforward consequence of Lemma 26 stating that for any
$$
\Gamma \xrightarrow{\text{Pr}^i} A_i
\xrightarrow{\vec{v} \searrow} \vec{v}_i
\llbracket x_i \rrbracket^\Gamma
$$

$$
\Gamma \xrightarrow{\text{Cur}(\llbracket M \rrbracket^{\Gamma, x:B})} A \Rightarrow B
\xrightarrow{\vec{v} \searrow} \text{Cur}(u \mapsto \phi(\vec{v}, u))
\llbracket \lambda x^B . M \rrbracket^\Gamma, \text{ with } \phi = \llbracket M \rrbracket^{\Gamma, x:B}
$$

$$
\Gamma \xrightarrow{\langle [M]^\Gamma, [N]^\Gamma \rangle} (A \Rightarrow B) \& A \xrightarrow{\text{Ev}} B
\xrightarrow{\vec{v} \searrow} \phi(\vec{v})(\psi(\vec{v}))
\llbracket (M) N \rrbracket^\Gamma, \text{ with } \phi = \llbracket M \rrbracket^\Gamma, \psi = \llbracket N \rrbracket^\Gamma
$$

$$
\Gamma \xrightarrow{\mathbb{T}} \mathbb{1} \xrightarrow{z} \text{Int}
\xrightarrow{\vec{v}} (1, 0, 0, \dots)
\llbracket \mathbb{0} \rrbracket^\Gamma
$$

$$
\Gamma \xrightarrow{[M]^\Gamma} \text{Int} \xrightarrow{\text{succ}} \text{Int}
\xrightarrow{\vec{v}} (0, w_0, w_1, \dots)
\llbracket \mathfrak{s}(M) \rrbracket^\Gamma, \text{ with } w = \llbracket M \rrbracket^\Gamma(\vec{v})
$$

$$
\Gamma \xrightarrow{[M]^\Gamma} \text{Int} \xrightarrow{\text{pred}} \text{Int}
\xrightarrow{\vec{v}} (w_1, w_2, \dots)
\llbracket \mathfrak{P}(M) \rrbracket^\Gamma, \text{ with } w = \llbracket M \rrbracket^\Gamma(\vec{v})
$$

$$
\Gamma \xrightarrow{\mathbb{T}} \mathbb{1} \xrightarrow{\text{rand}} \text{Int} \Rightarrow \text{Int}
\xrightarrow{\vec{v}} \llbracket \text{rand} \rrbracket
\llbracket \text{rand} \rrbracket^\Gamma
$$

$$
\Gamma \xrightarrow{\langle [M]^\Gamma, [N]^\Gamma, [N']^\Gamma \rangle} \text{Int} \times A \times A \xrightarrow{\text{ifz}} \text{Int}
\xrightarrow{\vec{v}} w_0 u + \sum_{n=1}^\infty w_n u'
\llbracket \text{if}(M, N, P) \rrbracket^\Gamma, \text{ with } w = \llbracket M \rrbracket^\Gamma(\vec{v}), u = \llbracket N \rrbracket^\Gamma(\vec{v}), u' = \llbracket N' \rrbracket^\Gamma(\vec{v})
$$

$$
\Gamma \xrightarrow{\text{sup}_n \text{ fix}^n ([M]^\Gamma)} A
\xrightarrow{\vec{v}} \text{sup}_n \text{ fix}^n(w)
\llbracket \text{fix}(M) \rrbracket^\Gamma, \text{ with } w = \llbracket M \rrbracket^\Gamma(\vec{v})
$$

<caption>Figure 2: The standard semantics of PPCF terms together with its action on $\vec{v} \in \mathbb{P}(\Gamma)$.</caption>

closed terms *M* and *N* having different interpretations in **Pcoh**.
there is a testing term *P* such that (*P*) *M* and (*P*) *N* reduce to 0
with different probabilities. Let us outline the path to this result.

With any web element *a*, we associate a testing term *P*(*a*) that
is described in Figure 5 and that reminds the contexts used in [3].
*P*(*a*) is not an ordinary term of PPCF since its construction uses a
random operator, weighted by a list **X** of formal parameters. How-
ever, a parameterized term becomes an ordinary PPCF term when
we substitute **X** by a list **κ** of rationals in [0, 1]. Following [6],
we introduce in Figure 3 an intersection type system that defines
semantics of parameterized terms. This interpretation is a formal
power series over **X** (Definition 21). Moreover, parameterized se-
mantics is compatible with Pcoh through substitution of parameters
(Lemma 20).

Now, assume that *M* and *N* are interpreted by different matrices
and pick a web element *a* such that [[*M*]]<sub>*a*</sub> ≠ [[*N*]]<sub>*a*</sub>. Then, the
semantics of the parameterized terms (*P*(*a*)) *M* and (*P*(*a*)) *N* are
distinct formal power series. Indeed, Lemma 24 implies that they
differ at least on one coefficient.

Finally, Lemma 25 ensures the existence of a list $\vec{\kappa}$ of rationals
in $[0, 1]$ on which these power series disagree. So, the substitution
of $\vec{X}$ by $\vec{\kappa}$ in $\mathcal{P}(a)$ produces a testing context separating $M$ and $N$.

We first describe *parameterized PPCF* in Subsection 5.1. Then,
testing terms are presented in Subsection 5.2. We conclude in
Subsection 5.3 with the full abstraction theorem.

**5.1 Parameterized PPCF**

Let $\mathfrak{P}$ be a denumerable set of formal parameters. $X, Y, Z$ range
over parameters in $\mathfrak{P}$.

The *grammar* of parameterized PPCF is an extension of PPCF
(Figure 1(a)) by multiplication of terms by parameters:

$$
\mathrm{PPCF}^{\mathfrak{P}} ::= \dots | X \cdot M, \text{ where } X \in \mathfrak{P}.
$$

The simple type of $X \cdot M$ under a context $\Gamma$ is $A$ whenever
$\Gamma \vdash M : A$ in PPCF (Figure 1(b)).

The substitution of parameters by scalars let us recover ordinary
terms from parameterized ones. More precisely, let $M \in \text{PPCF}^{\mathfrak{P}}$
and $\frac{n}{m} \in [0, 1]$ be a rational number. We define $M[\frac{n}{m}/X]$ as the

term obtained by replacing in *M* any subterm of shape *X* · *N* with

$$
\text{choose}(N^n, \Omega^{m-n}) \triangleq \text{choose}\left(\underbrace{N, \dots, N}_{n \text{ times}}, \underbrace{\Omega, \dots, \Omega}_{m-n \text{ times}}\right) \quad (9)
$$

(see Figure 1(d) for choose definition). Substitution is then gener-
alized to lists $\vec{X}$ of parameters and $\vec{\kappa}$ of rationals as $M[\vec{\kappa}/\vec{X}]$.

**Fact 17.** If $\vec{X}$ is the list of all parameters in $M$ and $\vec{\kappa}$ a list of rational numbers in $[0, 1]$, then $M[\vec{\kappa}/\vec{X}]$ is a term of PPCF.

The semantics of PPCF<sup>¶</sup> is a refinement of PPCF semantics taking into account parameters. Yet, for the sake of the full abstraction proof, we give a different presentation and use a weighted intersection type system. Roughly speaking, types are web elements and with each type derivation π, we associate a weight ω(π) which is a positive monomial, i.e. a product of rationals in [0, 1] and of finitely many parameters. Then, the interpretation [[M]] of a PPCF<sup>¶</sup> term M is a matrix indexed by web elements. For each web element, there can be several type derivations and the corresponding coefficient is the sum of their weights.

More precisely, Figure 3 describes the rules for constructing a
derivation $\pi :: \Gamma^\bullet \vdash_\alpha M : a$ of what we call a web judgment
$\Gamma^\bullet \vdash_\alpha M : a$. Notice that $\Gamma \vdash M : A$ is a valid simple type
judgment, $a \in |A|$ and $\alpha$ is a monomial. Besides, a web context $\Gamma^\bullet$
is defined as a function mapping any typed variable $x^C$ occurring in
$\Gamma$ to a finite multiset $m \in \mathcal{M}_f(|C|)$ of web elements and mapping
variables non-appearing in $\Gamma$ to the empty multiset. For instance,
for any $\Gamma = x_1 : C_1 \dots x_n : C_n$ and $\vec{m} \in \mathcal{M}_f(|\Gamma|)$, $\Gamma^\bullet$
denotes the web context $x_i^{C_i} \mapsto \vec{m}_i$ for $1 \le i \le n$. Disjoint unions
$\Gamma^\bullet \uplus \Delta^\bullet$
of web contexts are defined pointwise.

**Fact 18.** If $\Gamma^\bullet \vdash_\alpha M : a$ is derivable and $\Gamma^\bullet(x)$ is a non-empty multiset, then $x$ is free in $M$.

Rules `app` and `fix` deserve some comments. Application of
PPCF<sup>¶</sup> terms is interpreted following Equation (8) that defines
composition. Remark that indices of `app` mainly coincide with the
indices of the sums in (8), with one more difficulty since we have
to split contexts. Now, `fix` is derived from the rule `app` and from
<figure><img src="image_3.png" /><figcaption>**Figure 3:** Semantics of parameterized PPCF.</figcaption></figure>

$\text{fix}(M) \stackrel{1}{\to} (M) \text{fix}(M)$. To illustrate this point and the followings, we detail Examples 22 and 23 at the end of this subsection.

**Fact 19.** If $\Gamma \vdash M : A$ then $\sum_{\pi::\Gamma\vec{m}\vdash M:a} \omega(\pi)$ is a power series with finitely many variables in $\mathfrak{F}$ and non negative coefficients. Thus, for any list $\vec{\kappa}$ of non negative reals, $(\sum_{\pi::\Gamma\vec{m}\vdash M:a} \omega(\pi))(\vec{\kappa})$ is well defined.

The following fundamental lemma ensures the soundness of the weighted type system that computes the semantics of PPCF$^{\mathfrak{F}}$.

**Lemma 20 (Soundness).** Let $M$ be a term of PPCF$^{\mathfrak{F}}$ such that $\Gamma \vdash M : B$ and $\vec{X}$ lists its parameters. For any $\vec{p} \in \mathcal{M}_f(|\Gamma|)$, $b \in |\mathcal{B}|$, and any list $\vec{\kappa}$ of rational numbers in $[0, 1]$,

$$ \left[ M \left[ \vec{\kappa} / \vec{X} \right] \right]_{\vec{p}, b}^{\Gamma} = \left( \sum_{\pi::\Gamma\vec{p} \vdash M:b} \omega(\pi) \right) (\vec{\kappa}) \quad (10) $$

*Proof.* We prove Equation (10) by structural induction on $M$, using rules of Figure 3 and the definition of the categorical interpretation of a term in PPCF. We consider the term $\text{fix}(M)$ greater than $(M^n)$ $y$ for any natural number $n > 0$ and variable $y$. In fact, we are using the induction on the ordinal $\omega^2$.

Most cases follow directly from induction hypothesis. We only detail three cases: (i) multiplication with a parameter, (ii) application, (iii) fix-point.

(i) Assume $M = X_i \cdot N$ and $\kappa_i = \frac{n}{m}$. Then (using Equation (9)) we get: $M[\vec{\kappa}/\vec{X}] = \text{choose}(N[\vec{\kappa}/\vec{X}]^n, \Omega^{m-n})$. Besides, $[[\Omega]] = 0$ (Example 12), so $\left[ M[\vec{\kappa}/\vec{X}] \right]_{\vec{p},b}^{\Gamma} = \frac{n}{m} \left[ N[\vec{\kappa}/\vec{X}] \right]_{\vec{p},b}^{\Gamma}$.

Now, any derivation $\tau :: \Gamma^{\vec{p}} \vdash M[\vec{\kappa}/\vec{X}] : b$ consists of a sequence of $h \le n$ rules $\text{if}_s$ with on top, the rule $\text{if}_0$ with a derivation $\pi :: \Gamma^{\vec{p}} \vdash N[\vec{\kappa}/\vec{X}] : b$ as right premise. Indeed, the subterm $\Omega$ has no web type (see Example 23). When $\pi$ is fixed, $\omega(\tau) = \frac{\omega(\pi)}{m}$ and there are as many derivations $\tau$ as many choices

of $h \in \{1, \dots, n\}$. So, we compute

$$ \sum_{\pi::\Gamma^{\vec{p}} \vdash M:b} \omega(\tau) [\vec{\kappa}/\vec{X}] = \frac{n}{m} \left( \sum_{\pi::\Gamma^{\vec{p}} \vdash N:b} \omega(\pi) [\vec{\kappa}/\vec{X}] \right), $$
which is equal to $\frac{n}{m} \left( \left[ N[\vec{\kappa}/\vec{X}] \right]_{\vec{p},b}^{\Gamma} \right)$ by induction hypothesis. We conclude by gathering the equalities of the two paragraphs.

(ii) Assume $M = (N)P$. Thanks to the categorical semantics, $[(N)P]_{\vec{p},b}^{\Gamma} = (\text{Ev} \circ \langle [[N]^{\Gamma}, [[P]^{\Gamma}] \rangle)_{\vec{p},b}$. Then by definition of composition (Equation (8)) and left linearity of Ev, $[(N)P]_{\vec{p},b}^{\Gamma}$ is

$$ \sum_{\substack{m \in \mathcal{M}_f(|\mathcal{A}|), \\ (\vec{p}_{(a,i)})(a,i) \in m \text{ s.t.} \\ \cup_{(a,i) \in m} \vec{p}_{(a,i)} \subseteq \vec{p}}} \left[ N \right]_{\vec{p} \cup \cup_{(a,i) \in m} \vec{p}_{(a,i)}, (m,b)}^{\Gamma} \prod_{(a,i) \in m} \left[ P \right]_{\vec{p}_{(a,i)}, a}^{\Gamma} $$

By induction hypothesis and distributing product over sum, we get

$$ \sum_{m \in \mathcal{M}_f(|\mathcal{A}|)} \sum_{\substack{\tau::\vec{q}^- N:(m,b) \\ (\vec{p}_{(a,i)})(a,i) \in m \\ \cup_{(a,i) \in m} \vec{p}_{(a,i)} \subseteq \vec{p}}} \omega(\tau) \sum_{(\pi_{(a,i)})(a,i) \in m} \prod_{(a,i) \in m} \omega(\pi_{(a,i)}) \\ \text{s.t.} \quad \forall (a,i) \in m, \pi_{(a,i)} :: \vec{p}_{(a,i)} \vdash P:a $$

Although the indices of the sums might be frightening, they precisely describe all possible derivations of $\Gamma^{\vec{p}} \vdash (N)P : b$. Namely, the first sum defines the label of the terminal application rule, while the other sums give the choices of the derivations of their premises. The total weight is then the product of premise weights.

(iii) Assume $M = \text{fix}(N)$. Any derivation $\pi :: \Gamma^{\vec{p}} \vdash \text{fix}(N) : b$ ends with a cluster of fix rules (see Example 23). For $n \in \mathbb{N}^*$, let $\Pi^n$ be the set of derivations whose cluster height is at most $n$.

Now, remark that a derivation in $\Pi^n$ can be transformed into a derivation $\tau :: \Gamma^{\vec{p}}, y^B :: [] \vdash (N^n)y : b$ (where $y$ is fresh) by replacing fix rules with app rules (keeping labels) and each occurrence of $\text{fix}(N)$ with $(N^h)y$ for the suitable $h \le n$. Besides, this transformation preserves weights. Therefore:

$$ \sum_{\pi \in \Pi^n} \omega(\pi) = \sum_{\tau::\Gamma^{\vec{p}}, y^B:: [] \vdash (N^n)y:b} \omega(\tau) $$
Since $\llbracket \text{fix}(N) \rrbracket_{\vec{p},b}^{\Gamma} = \bigvee_{n \in \mathbb{N}} \llbracket (N^n) y \rrbracket_{(\vec{p},[1]),b}^{\Gamma;y}$ and by induction hypothesis: $\llbracket (N^n) y \rrbracket_{(\vec{p},[1]),b}^{\Gamma;y} = \bigvee_{n \in \mathbb{N}} \sum_{\tau::\Gamma\vec{p},y^{B}:[n]-(N^n)y:b} \omega(\tau)$

$$ \llbracket \text{fix}(N) \rrbracket_{\vec{p},b}^{\Gamma} = \bigvee_{n \in \mathbb{N}} \sum_{\pi \in \Pi^n} \omega(\pi) = \sum_{\pi \in \bigcup_n \Pi^n} \omega(\pi) = \sum_{\pi::\Gamma\vec{p} \vdash \text{fix}(N):b} \omega(\pi) \quad \square $$

According to this result, we generalize the semantics notation to parameterized PPCF:

**Definition 21.** For any term $M$ in PPCF$^{\mathfrak{F}}$ with $n$ parameters,

$$ \llbracket M \rrbracket_a^{\Gamma \triangleq \sum_{\pi::\Gamma^{\bullet} \vdash M:a} \omega(\pi)} \quad (11) $$

It is a power series whose domain of convergence contains $[0, 1]^n$.

The weighted type assignment system of Figure 3 has an interest by its own. It turns computation of semantics of terms (and hence its observational behavior) into a proof search problem.

The reader can convince himself that this approach is useful by computing the semantics of the following examples by applying directly rules of Figure 2.

**Example 22.** Let $k$ and $k'$ be non negative integers. Let us consider the possible derivations of the application $(M) N$ with

$$ M \triangleq \lambda x^{\text{Int}}. \text{if}(x, \Omega_{\text{Int}}; \text{if}(x, \Omega_{\text{Int}}, \underline{42})), \quad N \triangleq \text{if}(y, k, k'). $$

The derivable judgments on the term $N$ are of the form $y^{\text{Int}}: [\bar{n}] \vdash_1 N: \bar{k}$, with $\bar{k} \in \{k, k'\}$. In fact, once fixed $\bar{n}$, the derivation is unique and is given at the left-hand side of Figure 4. As for the term $M$, the derivable judgments are of the form $y^{\text{Int}}: [] \vdash_1 M: ([h, h'], 42)$, with $h, h' > 0$. However, in this case we have two different derivations whenever $h \neq h'$: one derivation is given at the right-hand side of Figure 4, while the other one is obtained by swapping the order between the var rules on $h$ and $h'$.

The weight of a derivation of $(M) N$ is 1. However, the number of derivation of a fix judgment $y^{\text{Int}}: [n, n'] \vdash_1 (M) N: 42$ depends on $n, n', k, k'$ following cases:

* if $k = k'$ and $n = n'$, then there is exactly one derivation;

* if $k = k'$ and $n \neq n'$, then there are two derivations, one ending with the rule $\text{app}_{([k,k], \{(k,1) \to [n], (k,2) \to [n']\})}$ and the other one with the rule $\text{app}_{([k,k], \{(k,1) \to [n'], (k,2) \to [n]\})}$;

* if $k \neq k'$ and $n = n'$, then there are two possible derivations, depending on which is the derivation used for inferring the judgment on $M$; notice that the final rule typing $(M) N$ must be $\text{app}_{([k,k'], \{(k,1) \to [n], (k',1) \to [n']\})}$;

* if $k \neq k'$ and $n \neq n'$, then there are four possible derivations, depending on the last rule (i.e. $\text{app}_{([k,k'], \{(k,1) \to [n], (k',1) \to [n']\})}$ or $\text{app}_{([k,k'], \{(k,1) \to [n'], (k',1) \to [n]\})}$) and on the derivation for inferring $M$.

Actually, by Lemma 20, weights of possible derivations sums into $\llbracket (M) N \rrbracket^y$, i.e.

$$ \llbracket (M) N \rrbracket_{m,h}^y = \begin{cases} 1 & \text{if } h = 42, k = k', m = [n, n], \\ 2 & \text{if } h = 42, k = k', m = [n \neq n'], \\ & \text{or } h = 42, k \neq k', m = [n, n], \\ 4 & \text{if } h = 42, k \neq k', m = [n \neq n'], \\ 0 & \text{otherwise.} \end{cases} $$

**Example 23.** Any derivation of a fix-point term $\text{fix}(M)$ ends with a cluster of fix rules, each rule has one premise typing $M$ and a number of premises typing $\text{fix}(M)$ and along which the cluster grows. Since the derivation must be finite, the cluster eventually ends with fix rules of label $([], (\cdot))$. They have exactly one premise

$$ \mathcal{P}(n) = \lambda x^{\text{Int}}. \text{if}(x = \underline{n}, \underline{0}, \Omega_{\text{Int}}) $$

$$ \mathcal{N}(n) = \underline{n} $$

$$ \mathcal{P}(a) = \lambda z^{B \Rightarrow C}. (\mathcal{P}(c)) ((z) \text{ choose } (X_i \cdot \mathcal{N}(b_i)))_{i=1}^n $$

$$ \mathcal{N}(a) = \lambda x^B. \text{if}(\wedge_{i=1}^n (\mathcal{P}(b_i)) x, \mathcal{N}(c), \Omega_C) $$

**Figure 5:** testing terms. In the higher-order case, i.e. $A = B \Rightarrow C$, we suppose $a = ([b_1, \dots, b_n], c)$, with $b_i \in |\mathcal{B}|$ and $c \in |\mathcal{C}|$. Sub-testing terms are supposed to have disjoint parameters and the $X_i$'s occurring in the definition of $\mathcal{P}(a)$ are assumed to be fresh.

typing $M$ with a web element of shape $([], a)$. As a consequence, the term $\Omega_A = \text{fix}(\lambda x^A \cdot x)$ has no web type, as $\lambda x^A \cdot x$ cannot have a web type of shape $([], a)$. We find again $\llbracket \Omega_A \rrbracket = 0$.

On the other hand, any derivation of $\text{fix}(\lambda x^{\text{Int}} \cdot x \oplus 0)$ will end with a branch of $n > 0$ fix rules: $n-1$ rules labelled by $([0], (\cdot))$, and the rule at the top of the branch labelled by $([], (\cdot))$ and having as premise the unique derivation of $\vdash_1 \frac{1}{2} \lambda x^{\text{Int}} \cdot x \oplus 0 : ([], 0)$. The whole derivation has conclusion $\vdash_1 \frac{1}{2n} \text{ fix}(\lambda x^{\text{Int}} \cdot x \oplus 0) : 0$ and the sum of these weights for $n > 0$ yields $\llbracket \text{fix}(\lambda x^{\text{Int}} \cdot x \oplus 0) \rrbracket_0 = 1$. We find again the results of Examples 3 and 12.

## 5.2 Testing terms

Figure 5 associates with every web element $a \in |\mathcal{A}|$ two closed terms of PPCF$^{\mathfrak{F}}$: one term $\mathcal{P}(a)$ of type $A \Rightarrow \text{Int}$ and one term $\mathcal{N}(a)$ of type $A$, defined by mutual induction on $A$.

$\mathcal{P}(a)$ and $\mathcal{N}(a)$ are named testing terms. The parameters occurring in this terms are in a bijective correspondence with the elements of the multisets appearing in $a$ (at all depths).

In the following, we focus on $\llbracket \mathcal{P}(a) \rrbracket_{(m,0)}$ and $\llbracket \mathcal{N}(a) \rrbracket_{a'}$, for any $m \in \mathcal{M}_f(|\mathcal{A}|)$ and $a' \in \mathcal{A}$, which are formal series in the parameters occurring in the terms (Fact 19). More precisely, we are interested in the coefficient of the monomial having each parameter of the term occurring with degree 1. This monomial is called the skeleton of $a$ and is denoted by $\mathbf{sk}(a)$.

**Lemma 24.** Let $A$ be a type, $a, a' \in |\mathcal{A}|$ and $m \in \mathcal{M}_f(|\mathcal{A}|)$. In the series $\llbracket \mathcal{P}(a) \rrbracket_{(m,0)}$ (resp. $\llbracket \mathcal{N}(a) \rrbracket_{a'}$), the monomial $\mathbf{sk}(a)$ has a non zero coefficient if and only if $m = [a]$ (resp. $a' = a$).

*Proof.* By definition, the coefficient of the monomial $\mathbf{sk}(a)$ in $\llbracket \mathcal{P}(a) \rrbracket_{(m,0)}$ can be recovered from the sum of the weights of the derivations of shape $P :: \vdash_{\kappa \mathbf{sk}(a)} \mathcal{P}(a) : (m, 0)$, and similarly for $\llbracket \mathcal{N}(a) \rrbracket_{a'}$. Hence, the statement is equivalent to the following property $\text{IH}(A)$, which will be proved by induction on type $A$:

* For any $a \in |\mathcal{A}|$, there is a derivation of $\vdash_{\kappa \mathbf{sk}(a)} \mathcal{P}(a) : (m, 0)$, with $\kappa \neq 0$, if and only if $m = [a]$

* For any $a \in |\mathcal{A}|$, there is a derivation of $\vdash_{\kappa \mathbf{sk}(a)} \mathcal{N}(a) : a'$, with $\kappa \neq 0$, if and only if $a' = a$.

For the ground type $\text{Int}$, testing terms have no parameters, so that the monomial $\mathbf{sk}(n)$ is the constant term of the series. The derivations of $\mathcal{P}(n)$ and $\mathcal{N}(n)$ are unique and of shape:

$$ \frac{m = [n]}{x : m \vdash_1 x : n} \quad \frac{\vdash_1 \underline{0} : 0}{x : m \vdash_1 \text{if}(x = \underline{n}, 0, \Omega_\iota) : 0} \quad \frac{a' = n}{\vdash_1 \underline{n} : a'} $$
<figure><img src="image_4.png" /><figcaption>Figure 4: Weighted derivations discussed in the Example 22</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Figure 6: Proof derivation contributing in the sk(a) monomial in P(a).</figcaption></figure>

We conclude that the coefficient is non zero iff $m = [n]$ and $a' = n$.

For the inductive case, let us assume that the result holds for type B and C and that $a = ([b_1, \dots, b_k], c) \in \mathcal{B} \Rightarrow \mathcal{C}$. Notice that $\mathbf{sk}(a) = \mathbf{sk}(c) \prod_{i=1}^k X_i \mathbf{sk}(b_i)$. A derivation of $\vdash_{\kappa \mathbf{sk}(a)} \mathcal{P}(a) : (m, 0)$, with $\kappa \neq 0$, must be as described in Figure 6, as justified below:

① The only possible rule is the abstraction one.

②,③ For using the application rule, we have to choose an intermediate multiset $q \in \mathcal{M}_f(|\mathcal{B} \Rightarrow \mathcal{C}|)$ and a context $\Gamma^{\bullet'}$ such that $\Gamma^{\bullet'} \vdash_{\gamma} \mathcal{P}(c) : (q, 0)$ is derivable. Since $\mathcal{P}(c)$ is a closed term, by Fact 18, $\Gamma^{\bullet'}$ must be empty (i.e. mapping all variables to the empty multiset). Moreover, by definition, the parameters occurring in $\mathcal{P}(c)$ must be different from those occurring in each $X_i \cdot \mathcal{N}(b_i)$. Therefore, $\gamma = \nu \mathbf{sk}(c)$, with $\nu \neq 0$. By induction hypothesis in ③, we infer that $q = [c]$. We then deduce that ② is a binary applicative rule of label $\mathbf{app}_{([c], (z:m))}$. Hence, the right premise is the sequent $z : m \vdash_{\beta} (z) \mathbf{choose}(X_i \cdot \mathcal{N}(b_i))_{i=1}^k : c$, for a $\beta$ of the shape $\mu \prod_{i=1}^k X_i \cdot \mathbf{sk}(b_i)$.

④,⑤ The shape of the term forces us to use the application rule again: let $p' = [b'_1, \dots, b'_{k'}]$ denote the intermediate multiset. Since the left premise is the only one in which $z$ appears, there is only one possible way of separating the context: $\Gamma^{\bullet'} = z : m$ and $\Gamma^{\bullet'}_{b'_j} = \emptyset$. Since the only possible rule for ⑤ is the var rule, we get $m = [(p', c)]$. We conclude that ④ is an applicative rule with $k' + 1$ premises, the $k'$ right premises being of shape $\vdash_{\beta_j} \mathbf{choose}(X_i \cdot \mathcal{N}(b_i))_{i=1}^k : b'_j$.

⑥,⑦,⑧ For any $j \in \{1 \dots k'\}$, there is a cluster of $h < k$ rules if $s$ and at the top of it a rule $\mathbf{if}_0$ with, as right premise, a weighted typing of a summand $X_{ij} \cdot \mathcal{N}(b_{ij})$. From that we must apply a par rule (numbered ⑦) and get as premise a sequent of shape $\vdash_{\beta_{ij}} \mathcal{N}(b_{ij}) : b'_{j}$, for $i_j \in 1 \dots k$ and weight $\beta_{ij}$. Then, notice that the weight of the conclusion of ⑦ is $X_{ij} \beta_{ij}$ and that of the conclusion of ⑥ is $\frac{1}{k} X_{ij} \beta_{ij}$. On the one hand, the reasoning on ② gives us $\beta = \mu \prod_{i=1}^k X_i \cdot \mathbf{sk}(b_i)$, while the definition of the weight of the conclusion of ④ gives us $\beta = \prod_{j=1}^{k'} \frac{1}{k} X_{ij} \cdot \beta_{ij}$.

Since by definition no parameter $X_i$ occurs in $\mathcal{N}(b_{ij})$, hence no $X_i$ appears in $\beta_{ij}$, we have that the mapping $j \to i_j$ is a bijective correspondence between $\{1, \dots, k'\}$ and $\{1, \dots, k\}$, so $k = k'$. Finally, since the sets of parameters occurring in the $\mathcal{N}(b_{ij})$ are pairwise disjoint, we deduce that $\beta_{ij}$ is proportional to $\mathbf{sk}(b_{ij})$. We can then apply the induction hypothesis on ⑧ and deduce that $b_{ij} = b_i$, and so $p' = [b_1, \dots, b_k]$.

Combining all these results, we eventually get that $m = [(p', c)] = [[b_1, \dots, b_k], c] = [a]$. We conclude that there is a derivation of $\vdash_{\kappa \mathbf{sk}(a)} \mathcal{P}(a) : (m, 0)$ if and only if $m = [a]$.

Now, let us consider a derivation of $\vdash_{\kappa \mathbf{sk}(a)} \mathcal{N}(a) : a'$, which must have the following form:

$$ \frac{x : p' \vdash_{\alpha} \mathbf{if}(\wedge_{i=1}^k (\mathcal{P}(b_i)) x, \mathcal{N}(c), \Omega_C) : c' \quad \vdash_{\alpha} \lambda x^B. \mathbf{if}(\wedge_{i=1}^k (\mathcal{P}(b_i)) x, \mathcal{N}(c), \Omega_C) : (p', c')}{\mathbf{choose}(X_i \cdot \mathcal{N}(b_i))_{i=1}^k : b'_j} $$

We prove by recursion on $k-j$ the property RH(j):

★ if $x : p' \vdash_{\alpha} \mathbf{if}(\wedge_{i=1}^k (\mathcal{P}(b_i)) x, \mathcal{N}(c), \Omega_C) : c'$ is derivable, then $\alpha$ is proportional to $\mathbf{sk}(c) \prod_{i=j}^k \mathbf{sk}(b_i)$ if and only if $c = c'$ and $p' = [b_j, \dots, b_k]$.

The base case ($j=k$) is the induction hypothesis IH(C). Indeed, if $x : p' \vdash_{\alpha} \mathcal{N}(c) : c'$ is derivable, then, by Fact 18, $p'$ is empty, so that the weight $\alpha$ is proportional to $\mathbf{sk}(c)$ if and only if $c = c'$. The inductive case is proved accordingly to Figure 7:

① Since $\Omega_C$ has no web type (Example 23), the only possible rule is $\mathbf{if}_0$. The choice of how to partition the context $m_1 \uplus m_2$ will be deduced from the type derivation. Since by definition the set of parameters in $\mathcal{P}(b_j)$ and the set of parameters in $\mathbf{if}(\wedge_{i=j+1}^k (\mathcal{P}(b_i)) x, \mathcal{N}(c), \Omega_C)$ are disjoint, we have that $\beta$ is proportional to $\mathbf{sk}(b_j)$ and $\gamma$ is proportional to $\prod_{i=j+1}^k \mathbf{sk}(b_i)$.

② For the right premise we can then apply the hypothesis RH(j+1) and deduce that $c = c'$ and $m_2 = [b_{j+1}, \dots, b_k]$.

③,④ For the left premise, the only possible rule is app. We have then to choose the intermediate multiset $m'$. As in the previous cases, one can argue that the left premise has empty context
$$
\frac{\mathrm{IH}(A): m_1 = [b_j] \qquad \mathrm{RH}(j+1): c = c', m_2 = [b_{j+1}, \dots, b_k] \qquad \mathrm{RH}(j+1): x : m_1 \vdash_\beta (P(b_j)) x : 0 \qquad \mathrm{RH}(j+1): x : m_1 \vdash_\beta (P(b_j)) x : 0 \qquad \mathrm{RH}(j+1): x : m_1 \vdash_\beta (P(b_j)) x : 0}{x : m_1 \vdash_\beta (P(b_j)) x : 0} \quad \begin{array}{c} \textcircled{4} \\ \textcircled{3} \\ \textcircled{2} \\ \textcircled{1} \end{array}
$$

<caption>Figure 7: Proof derivation contributing in the sk(a) monomial in N(a).</caption>

since $\mathcal{P}(b_j)$ is closed and then the induction hypothesis IH($C$)
gives $m' = [b_j]$. This means that $\textcircled{3}$ has only one premise at
the right-hand side, which is a conclusion of a var rule, so that
$m' = m_1$.

We conclude by combining all these results: we get that the context
$m_1 \uplus m_2 = [b_1, \dots, b_k]$ and $c = c'$.

We have proved that RH(1) holds: $c = c'$ and $p' = [b_1, \dots, b_k]$,
hence $a' = a$. $\square$

5.3 Main Result

The theory of multi-variables analytic functions can be subtler than
single variable ones (for instance zeros of functions are not isolated
in general). In the following Lemma 25, we underline that the
coefficients of a power series vanishing on a neighborhood of zero
have to be null. Indeed, coefficients are computed by successive
derivations as limits of difference quotients. We then apply this
result to power series with possibly negative coefficients.

**Lemma 25.** [16] Let $f$ be a power series from $\mathbb{R}^n$ to $\mathbb{R}$ absolutely converging on $[0, 1]^n$. If $f$ vanishes on a dense subset of $[0, 1]^n$, then the coefficients of the power series $f$ are zero.

**Lemma 26.** Let $M$ and $N$ be two closed terms of PPCF with the same type A. If $[[M]] \neq [[N]]$, then there is a PPCF term $P$ of type $A \Rightarrow \text{Int}$ such that $\text{PROBA}_{(P)M,0}^{\infty} \neq \text{PROBA}_{(P)N,0}^{\infty}$.

*Proof.* Let $a \in |A|$ such that $[[M]]_a \neq [[N]]_a$. Consider the testing term $\mathcal{P}(a)$ as defined in Figure 5.

Let $f$ denote the series $[[(\mathcal{P}(a))M]]_0$, which, by Definition 21 is a power series from $[0, 1]^n$ to $[0, 1]$, where $n$ is the number of parameters in $\mathcal{P}(a)$. Let $\text{cf}(\mathbf{sk}(a), f)$ denote the coefficient of the monomial $\mathbf{sk}(a)$ in $f$. By definition (Equation (11)) this coefficient is given by the sum of the weights of the possible derivations of $\vdash_\alpha (\mathcal{P}(a))M : 0$, for $\alpha$ proportional to $\mathbf{sk}(a)$. The last rule of this derivation must be an app rule of shape:

$$
\frac{\vdash_{\gamma} \mathcal{P}(a) : (m, 0) \quad \forall (a', i) \in m, \quad \vdash_{\beta_{(a', i)}} M : a' \qquad \vdash_{\gamma} \prod_{(a', i) \in m} \beta_{(a', i)} (\mathcal{P}(a)) M : 0}{\vdash_{\gamma} \prod_{(a', i) \in m} \beta_{(a', i)} (\mathcal{P}(a)) M : 0}
$$

Since $M$ has no free parameter (it is a term of PPCF), each
$\beta_{(a',i)}$ is a positive real number. Hence, $\alpha = \gamma \prod_{(a',i) \in m} \beta_{(a',i)}$
is proportional to $\mathbf{sk}(a)$ iff $\gamma$ is proportional to $\mathbf{sk}(a)$. We can then
apply Lemma 24 and get $m = [a]$. Moreover, by Lemma 20, the
sum of the weights of the derivations of $\vdash M : a$ is equal to the
scalar $[[M]]_a$. To sum up, we conclude:

$$
\mathrm{cf}(\mathbf{sk}(a), f) = \mathrm{cf}(\mathbf{sk}(a), [[\mathcal{P}(a)]_{([a],0)}][M]]_a
$$

with $\mathrm{cf}(\mathbf{sk}(a), [[\mathcal{P}(a)]_{([a],0)}]) \neq 0$. By an analogous reasoning:

$$
\mathrm{cf}(\mathbf{sk}(a), g) = \mathrm{cf}(\mathbf{sk}(a), [[\mathcal{P}(a)]_{([a],0)}][N]]_a
$$

where $g$ denotes the power series $[[(\mathcal{P}(a))N]]_0$. We can conclude
that $f$ and $g$ have a different coefficient for the monomial $\mathbf{sk}(a)$ as
soon as $[[M]]_a \neq [[N]]_a$.

Now, we apply Lemma 25 to the series $f-g$, which is not the
zero power series because of the coefficient of sk(a). Therefore,
as rational numbers are dense in $[0, 1]$, there is a list $\vec{\kappa}$ of rational
numbers in $[0, 1]$ such that $f(\vec{\kappa}) \neq g(\vec{\kappa})$. By Lemma 20, this
is equivalent to $[[ (\mathcal{P}(a)[\vec{\kappa}/\vec{X}])M]]_0 \neq [[ (\mathcal{P}(a)[\vec{\kappa}/\vec{X}])N]]_0$.
We conclude by setting $P = \mathcal{P}(a)[\vec{\kappa}/\vec{X}]$. Actually, $P$ is a well-
defined PPCF term by Fact 17. So, by adequacy (Theorem 14),
$\text{PROBA}_{(P)M,0}^{\infty} = [[(P)M]]_0 \neq [[(P)N]]_0 = \text{PROBA}_{(P)N,0}^{\infty}$. $\square$

**Theorem 27 (Full Abstraction).** Given $\Gamma \vdash M : A$, and $\Gamma \vdash N : A$, we have:

$$
M \equiv_{\Gamma} N \text{ iff } [[M]]^{\Gamma} = [[N]]^{\Gamma}.
$$

*Proof.* By Corollary 16 and Lemma 26. $\square$

As a consequence, the observational equivalence does not de-
pend on the chosen probabilistic primitive (recall Remark 6):

**Corollary 28.** For any $p \in \{\text{Coin}, \text{rand}, \oplus_{\kappa}, \oplus_{i\kappa_i}, (\kappa_n)_{n \in \mathbb{N}}\}$, let $\equiv_p$ denote the observational equivalence induced by the extension of PCF with the probabilistic primitive $p$. The equivalence $\equiv_p$ coincides with the equality of the interpretations in PCoh. In particular, $\equiv_p$ gives the same equivalence on PCF terms, for any choice of $p$.

*Proof (Sketch).* We have that $\equiv_{\text{coin}} = \equiv_{\text{rand}}$ since the two primi-
tives Coin and rand are interdefinable by [5]. Similarly, by the
discussion of Remark 6, we have: $\equiv_{\text{rand}} \supset \equiv_{\oplus_{\kappa}} \supset \equiv_{\oplus_{i\kappa_i}}$
$\supset \equiv_{(\kappa_n)_{n \in \mathbb{N}}}$. In [4], the adequacy property of PCoh is es-
tablished for the language containing the the $(\kappa_n)_{n \in \mathbb{N}}$ primitive,
hence $\equiv_{(\kappa_n)_{n \in \mathbb{N}}}$ contains the equality $\equiv_{\text{Pcoh}}$ of the interpretations
in PCoh. Finally, by Theorem 27, we have $\equiv_{\text{Pcoh}} \supset \equiv_{\text{rand}}$ and we
can conclude. $\square$

6. A counter-example to inequational FA

We prove that inequational full abstraction fails for **PCoh**. The
proof consists in: (i) showing that the morphisms of Remark 11,
that proves the non-extensionality of the **PCoh** order, are definable
in PPCF (Equation 12); (ii) achieving a context lemma (Proposi-
tion 31) allowing us to infer the observational inequality by just
observing the behavior of closed terms in applicative contexts.

If one would like to enrich the language in order to make
observable also the componentwise order of PCoh, one should
add a kind of differential operator to PPCF, in the spirit of [9].
However, such an extension is not trivial, since PCoh is known not
to be sound for the whole differential λ-calculus.

Let us define $M_1$ and $M_2$ as follows:

$$
M_1 \triangleq \lambda x^{\text{Int}}.\text{if}(x, 0, 0), \quad M_2 \triangleq \lambda x^{\text{Int}}.0. \quad (12)
$$

By using rules of Figure 3 and Lemma 20, one can check that the
semantics of the two terms is given by the morphisms of Exam-
ple 11, i.e. $[[M_1]] = \phi$ and $[[M_2]] = \psi$. Hence, the two matrices
$[[M_1]]$ and $[[M_2]]$ are incomparable in Pcoh.
In order to prove $M_1 \subseteq M_2$, we use a standard reasoning and introduce a logical relation (Definition 29) allowing us to shrink the set of contexts (Proposition 31). We conclude with Corollary 32.

**Definition 29.** By structural induction on a type $A$, we define the binary relation $\langle\subset_A\rangle$ over closed PPCF terms of type $A$, as follows: $N \langle\subset_{\text{Int}}\rangle N'$ iff $\forall n \in \mathbb{N}$, $\llbracket N \rrbracket_n \le \llbracket N' \rrbracket_n$, and $M \langle\subset_{A\Rightarrow B}\rangle M'$ iff $\forall N \subset_A N'$, $(M) N \subset_B (M') N'$.

**Lemma 30.** Let $M$ be a term of type $x_1 : A_1, \dots, x_n : A_n \vdash M : A$. If for all $i$, $N_i \subset_{A_i} N'_i$, then $M[\vec{N}/\vec{x}] \subset_A M[\vec{N'}/\vec{x}]$.

**Proposition 31.** Let $M$ and $N$ be closed terms of type $A$. Then, $M \subset_A N$ iff $M \subseteq_A N$.

**Corollary 32.** The terms $M_1$ and $M_2$ of Equation (12) are logically related: $M_1 \langle\subset_{\text{Int}}\rangle \subset_{\text{Int}} M_2$. Hence, $M_1 \subseteq M_2$.

# 7. Conclusion

We show that the observational equality over probabilistic programs is faithfully described by **PCoh**, a relatively abstract model based on convex sets and extensional functions. The proof uses innovative tools which might be useful to study probabilistic programming from a semantical viewpoint. In a language with random functions, two programs should be considered different not only when they give different results, but also when they give the same result but with different probabilities. Showing this difference can be much harder than in a deterministic language. Indeed, it requires a sharp control over coefficients expressing probabilities. **PCoh** denotes programs with power series, this allows us to use standard tools of Calculus for handling probabilities.

Although we chose one probabilistic primitive (see Remark 6), Corollary 28 shows that our result does not depend on this choice. Moreover, we focused on PPCF, a call-by-name functional language, but our result might be extended to other frameworks. In fact, **PCoh** comes from a model of linear logic: it is the cokleisli category associated with the exponential comonad, that corresponds to the translation of the functional arrow $A \Rightarrow B$ into the linear logic formula $!A \to B$. Call-by-value can be obtained by using the Eilenberg-Moore construction, i.e. translating $A \Rightarrow B$ into $(A \to B)$. Control operators can be introduced considering a polarized fragment of linear logic. Yet, extending this model to concurrent systems or references is certainly more challenging.

A crucial tool in the proof of full abstraction is the use of the type system of Figure 3, which is a kind of intersection type system. In fact, a web element $([a_1, \dots, a_n], b)$ can be seen as a type $(a_1 \wedge \dots \wedge a_n) \to b$, where the intersection is non-idempotent. This system is a quantitative refinement of De Carvalho's [6] and yields the first logical presentation of a vectorial based semantics. Clearly, both type inference and type checking are undecidable. However, one can look for interesting restrictions of PPCF where the system becomes decidable, in the spirit of [20].

Last, it should be noticed that, unlike most full abstraction models for PCF, our model has no simple PPCF-definability properties. Our full abstraction proof builds applicative contexts using terms which belong to a very small subset of the domains associated with types. Their discriminating power relies on a strong regularity property of power series (unlike smooth functions, a power series which vanishes on an open set must be equal to 0, see for example to the function defined by $e^{-1/x^2}$ for $x > 0$ and $0$ for $x \le 0$). In contrast, most full abstraction proofs build applicative contexts using terms which belong to a dense subset of the corresponding domains.

# References

[1] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. *Information and Computation*, 163(2):409–470, Dec. 2000.

[2] G. Boudol, P.-L. Curien, and C. Lavatelli. A semantics for lambda calculi with resources. *Math. Struct. Comp. Sci.*, 9(4):437–482, 1999.

[3] A. Bucciarelli, A. Carraro, T. Ehrhard, G. Manzonetto, et al. Full abstraction for resource calculus with tests. In *CSL11 – Annual Conference of the EACSL*, volume 12, pages 97–111, 2011.

[4] V. Danos and T. Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. *Inf. Comput.*, 209(6):966–991, 2011.

[5] V. Danos and R. Harmer. Probabilistic game semantics. *ACM Transactions on Computational Logic*, 3(3):359–382, July 2002.

[6] D. de Carvalho. Execution Time of $\lambda$-Terms via Denotational Semantics and Intersection Types. Preprint, 2009.

[7] T. Ehrhard. On Kôthe sequence spaces and linear logic. *Math. Struct. Comput. Sci.*, 12:579–623, 2002.

[8] T. Ehrhard. Finiteness spaces. *Math. Struct. Comput. Sci.*, 15(4):615–646, 2005.

[9] T. Ehrhard and L. Regnier. The Differential Lambda-Calculus. *Theor. Comput. Sci.*, 309(1):1–41, 2003.

[10] J.-Y. Girard. The system F of variable types, fifteen years later. *Theor. Comput. Sci.*, 45:159–192, 1986.

[11] J.-Y. Girard. Linear logic. *Theor. Comput. Sci.*, 50:1–102, 1987.

[12] J.-Y. Girard. Normal functors, power series and lambda-calculus. *Ann. Pure Appl. Logic*, 37(2):129–177, 1988.

[13] J.-Y. Girard. Coherent banach spaces: a continuous denotational semantics. *Theor. Comput. Sci.*, 227:297, 1999.

[14] J.-Y. Girard. Between logic and quantic: a tract. In T. Ehrhard, J.-Y. Girard, P. Ruet, and P. Scott, editors, *Linear Logic in Computer Science*, volume 316 of *London Math. Soc. Lect. Notes Ser.* CUP, 2004.

[15] J. Goubault-Larrecq and D. Varacca. Continuous random variables. In *LICS*, pages 97–106. IEEE Computer Society, 2011.

[16] É. Goursat. *Cours d'analyse mathématique. Tome I.* Gauthier-Villars, 1918.

[17] R. Hasegawa. Two applications of analytic functors. *Theor. Comput. Sci.*, 272(1-2):113–175, 2002.

[18] M. Hyland and L. Ong. On full abstraction for PCF. *Information and Computation*, 163(2):285–408, Dec. 2000.

[19] C. Jones and G. Plotkin. A probabilistic powerdomains of evaluation. In *LICS*. IEEE Computer Society, 1989.

[20] A. J. Kfoury and J. B. Wells. Principality and decidable type inference for finite-rank intersection types. In *POPL*, pages 161–174, 1999.

[21] U. D. Lago and M. Zorzi. Probabilistic operational semantics for the lambda calculus. *RAIRO - Theor. Inf. and Applic.*, 46(3):413–450, 2012.

[22] J. Laird, G. Manzonetto, G. McCusker, and M. Pagani. Weighted relational models of typed lambda-calculi. In *LICS 2013*. IEEE Press, June 2013.

[23] R. Milner. Fully abstract models of typed lambda-calculi. *Theor. Comput. Sci.*, 4:1–22, 1977.

[24] R. Milner and C. Strachey. *A Theory of Programming Language Semantics*. Chapman and Hall, London, 1976.

[25] E. Moggi. Computational lambda-calculus and monads. In *LICS*, pages 14–23. IEEE Computer Society, 1989.

[26] A. D. Pierro, C. Hankin, and H. Wiklicky. Probabilistic lambda-calculus and quantitative program analysis. *J. Log. Comput.*, 15(2): 159–179, 2005.

[27] G. D. Plotkin. A powerdomain construction. *SIAM J. Comput.*, 5(3): 452–487, 1976.

[28] G. D. Plotkin. LCF considered as a programming language. *Theor. Comput. Sci.*, 5(3):225–255, 1977.

[29] N. Saheb-Djahromi. Cpo's of measures for nondeterminism. *Theor. Comput. Sci.*, 12:19–37, 1980.

[30] D. Scott. Continuous lattices. In Lawvere, editor, *Toposes, Algebraic Geometry and Logic*, volume 274 of *Lecture Notes in Math.*, pages 97–136. Springer, 1972.