# The Free Exponential Modality of Probabilistic Coherence Spaces

Thomas Ehrhard, Christine Tasson, Michele Pagani, Raphaëlle Crubillé

► To cite this version:

Thomas Ehrhard, Christine Tasson, Michele Pagani, Raphaëlle Crubillé. The Free Exponential Modality of Probabilistic Coherence Spaces. Foundations of Software Science and Computation Structures (FOSSACS 2017), Apr 2017, Uppsala, Sweden. pp.20-35, 10.1007/978-3-662-54458-7_2. hal-02357979

HAL Id: hal-02357979

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

Submitted on 13 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>
# The Free Exponential Modality of Probabilistic Coherence Spaces

Raphaëlle Crubillé, Thomas Ehrhard, Michele Pagani, and Christine Tasson

IRIF, UMR 8243, Université Paris Diderot, Sorbonne Paris Cité, F-75205, France

**Abstract.** Probabilistic coherence spaces yield a model of linear logic and lambda-calculus with a linear algebra flavor. Formulas/types are associated with convex sets of $\mathbb{R}^+$-valued vectors, linear logic proofs with linear functions and $\lambda$-terms with entire functions, both mapping the convex set of their domain into the one of their codomain.

Previous results show that this model is particularly precise in describing the observational equivalences between probabilistic functional programs. We prove here that the exponential modality is the free commutative comonad, giving a further mark of canonicity to the model.

# 1 Introduction

Linear Logic [6] (LL for short) is a resource aware logic whose relevance in the study of the semantics of computation has been illustrated by several papers. It has three kinds of connectives: additive, mutliplicative and exponential. The connectives of the first two classes are determined by their logical rules: for instance, if one introduces a second tensor product $\otimes'$ in the system, it is easy to prove that $A \otimes B$ and $A \otimes' B$ are canonically equivalent (isomorphic, actually) for all formulas $A$ and $B$. The exponential connectives behave quite differently: one can add a second exponential modality $!'$ with the same rules as for $!$ and it is not possible to prove that $!A$ and $!A'$ are equivalent in general.

This discrepancy is also well visible at the semantical level. Given a category, the multiplicative-additive structures (if exist) are univocally characterized by universal properties as soon as a notion of multilinear map is given, while various different notions of the exponential modality are possible, in general. Well-known examples are the category **Coh** of coherence spaces, where the exponential modality can be expressed by both the finite clique and the finite multi-clique functors [7], as well as the category **Rel** of sets and relations, for which [2] introduces a wide family of exponential modalities in addtion to the more standard one based on the finite multiset functor.

Choosing an exponential interpretation in the model is not at all anodyne, as it defines the way we express the structural rules of weakening and contraction, or, from a programming perspective, the operations of erasure and copy. For instance, the new exponential modalities in **Rel**, introduced by [2], allow to construct non-sensible models of the untyped $\lambda$-calculus, while the models based on the finite multiset functor are all sensible. Let us also mention that this variety of exponentials has been used for modeling different notions of co-effects [1].
Any interpretation of the ! LL modality is an operation transforming an object $A$ into a commutative comonoid $!A$ with respect to $\otimes$, the comultiplication allowing one to interpret contraction, and the con neutral element allowing one to interpret weakening. This simple fact shows that among all possible notions of !, there might be one which is more canonical than any other, being the terminal object in the category of commutative comonoids over $A$. Lafont [9] proved in fact that the free commutative comonoid, whenever it exists, always gives an interpretation of the exponential modality, which is then called the *free exponential modality*, and written as $!_f$.

The study of this free exponential $!_f A$, when it exists, is particularly important because its universal property expresses a direct connection with the tensor product of the categorical model of LL under consideration. This fact is particularly well illustrated by [11] where it is shown that, under some fairly general assumptions, this free exponential can be described as a kind of “symmetric infinite tensor product”; we come back to this characterization later since it is at the core of the present work.

The free exponential modality is well-kwown in both **Coh** and **Rel**, being given respectively by the multi-clique and the multi-set functors. The goal of this paper is to prove the existence of and to study the free exponential modality of the category **Pcoh** of probabilistic coherence spaces.

**Pcoh** is a model of linear logic carrying both linear algebraic and probabilistic intuitions. Sketched by Girard in [8], it was more deeply investigated in [3]. Formulas/types are interpreted as suitable sets $P(\mathcal{A})$, $P(\mathcal{B})$,... of real-valued vectors which are both Scott-closed (allowing the usual definition of fixed-points) and convex (i.e. closed under barycentric sums). This latter feature makes **Pcoh** particularly suitable for modeling (discrete) probabilistic computations: the barycentric sum $\kappa v + \rho w$ (for $\kappa, \rho \in [0, 1]$, $\kappa + \rho \le 1$, $v, w$ vectors) expresses a computation which returns $v$ with probability $\kappa$, $w$ with probability $\rho$, and the remainder $1 - (\kappa + \rho)$ is the probability that the computation diverges.

The morphisms of **Pcoh** are Scott-continuous and linear functions mapping the set $P(\mathcal{A})$ of vectors associated with the domain into the set $P(\mathcal{B})$ associated with the codomain. These linear maps are described as (usually infinite-dimensional) matrices and the set of these matrices is the hom-object $P(\mathcal{A} \to \mathcal{B})$ associated with linear implication. From a programming perspective, the matrices in $P(\mathcal{A} \to \mathcal{B})$ correspond to probabilistic programs that use their inputs exactly once in order to compute a result. In order to interpret non-linear programs one has to choose an exponential modality. The only known ! modality of **Pcoh** is the one introduced in [3], which is based on the notion of entire function and hence we will call it the *entire exponential modality* and denote it with $!_e$. The set $P(\mathcal{A} \to \mathcal{B})$ can be seen as a set of matrices giving the coefficients of a power series expressing an entire function from $P(\mathcal{A})$ to $P(\mathcal{B})$. As usual the interpretation of a (call-by-name) program of type $A \Rightarrow B$ is represented as an LL proof of $!A \to B$ and hence as an entire function in **Pcoh**.

The entire exponential modality of **Pcoh** has been recently shown to be particularly relevant for describing the observational behavior of higher-order
probabilistic programs. Namely, [4] proves that the Kleisli category associated
with !_e is fully-abstract with respect to call-by-name probabilistic PCF, while
[5] proves, using the Eilenberg-Moore category, that Pcoh is fully-abstract for
a call-by-push-value version of probabilistic PCF. Let us stress that these are
indeed the only known fully-abstract models for probabilistic PCF.

It is then natural to ask whether !_f exists in Pcoh and if it is the case, how
it relates with !_e. In this paper we answer the first question positively and prove
that !_f and !_e are the same modality, in spite of their different presentations.

Our main tool is a recipe for constructing !_f out of a model of the multi-
plicative additive fragment of LL, given by Melliès, Tabareau and Tasson [11].
The idea is to adapt the well-known formula defining the symmetric algebra gen-
erated by a vector space, the latter being the free commutative monoid. More
precisely, the recipe gives (under suitable conditions) !_f A as the limit of a se-
quence of approximants A<sup>&le;n</sup> which correspond to the equalizers of the tensor
symmetries of a suitable space (see Section 3). At a first sight, A<sup>&le;n</sup> moves us far
away from the entire exponential !_e A of [3], in fact the coefficients appearing in
A<sup>&le;n</sup> are greater than those of !_e A, so that one is tempted to suppose that !_f A
is a space much bigger than !_e A, exactly as it is the case for standard coherence
spaces where the images under the finite multi-clique functor strictly contain
those under the finite clique functor (Example 5). We prove that this is not the
case, the limit !_f A of the approximants A<sup>&le;n</sup> exists (Proposition 4), and, more
surprisingly, it is equal to the entire exponential modality (Proposition 5). For
any n, the coefficients of A<sup>&le;n</sup> are larger than those of !_e A, but as n &rarr; &infin;, these
coefficients tend to be exactly those of !_e A (see Section 4.3).

*Contents of the paper.* In Section 2, we briefly recall the semantics of LL in Pcoh as defined in [3]. In particular, Equations (8) and (9) sketch the definition of the entire exponential modality. Section 3 gives the categorical definition of the free exponential modality and Melliés, Tabareau and Tasson’s recipe for constructing it (Proposition 2). The major contributions are in Section 4, where we apply this recipe to Pcoh (Propositions 3 and 4) and prove that the free exponential modality is equal to the entire one (Proposition 5).

Notation. We write as $S_n$ the set of permutations of the set $\{1, \dots, n\}$, the factorial $n!$ being its cardinality. The writing $f : A \hookrightarrow B$ denotes an injection $f$ from a set $A$ into a set $B$. A multiset $\mu$ over $A$ is a function from $A$ to $\mathbb{N}$, $\text{Supp}(\mu)$ denoting its support $\{a \in A ; \mu(a) \neq 0\}$, and $\#\mu$ its cardinality $\sum_{a \in A} \mu(a)$. Given $n \in \mathbb{N}$, $\mathcal{M}_n(A)$ is the set of multisets of cardinality $n$, while $\mathcal{M}_f(A)$ is the set of finite multisets, i.e. $\mathcal{M}_f(A) = \bigcup_n \mathcal{M}_n(A)$. A multiset $\mu$ can also be presented by listing the occurrences of its elements within brackets, like $\mu = [a, a, b]$, as well as $\mu = [a^2, b]$, for the multiset $\mu(a) = 2, \mu(b) = 1, \text{Supp}(\mu) = \{a, b\}$. Finally, $\mu \uplus \nu$ is the disjoint union of two multisets, i.e. $(\mu \uplus \nu)(a) = \mu(a) + \nu(a)$, the empty multiset $[]$ being its neutral element. We denote by $\mathbf{a}$ a finite sequence of elements of $A$, $\mathbf{a}_i$ being its $i$-th element. Given such a sequence $\mathbf{a}$, we denote as $\tilde{\mathbf{a}}$ the multiset of its elements, and given a multiset $\mu$, we write as $\text{ Enum}(\mu)$ the set of all its different enumerations. The cardinality of
Enum($\mu$) depends on $\mu$ and can be given by the multinomial coefficient $m(\mu)$:

$$ \tilde{a} = [a_1, \dots, a_n], \qquad \text{for } a = (a_1, \dots, a_n), \qquad (1) $$

$$ \text{Enum}(\mu) = \{(a_{\sigma(1)}, \dots, a_{\sigma(n)}); \sigma \in S_n\}, \qquad \text{for } \mu = [a_1, \dots, a_n], \qquad (2) $$

$$ m(\mu) = \frac{\#\mu!}{\prod_{a \in \text{Supp}(\mu)} \mu(a)!}. \qquad (3) $$

## 2 The model of probabilistic coherence spaces

In order to be self-contained, we shortly recall the linear logic model based on probabilistic coherence spaces, as defined in [3]. For the sake of brevity we will omit the proofs of this section.

Let $I$ be a set, for any vectors $v, w \in (\mathbb{R}^+)^I$, the pairing is defined as usual

$$ \langle v, w \rangle = \sum_{i \in I} v_i w_i \in \mathbb{R}^+ \cup \{\infty\}. \qquad (4) $$

Given a set $P \subseteq (\mathbb{R}^+)^I$ we define $P^{\perp}$, the polar of $P$, as

$$ P^{\perp} = \{w \in (\mathbb{R}^+)^I \mid \forall v \in P \ \langle v, w \rangle \le 1\}. \qquad (5) $$

The polar satisfies the following immediate properties: $P \subseteq P^{\perp}$, if $P \subseteq Q$ then $Q^{\perp} \subseteq P^{\perp}$, and then $P^{\perp} = P^{\perp \perp}$.

**Definition 1 ([8,3]).** A probabilistic coherence space, or PCS for short, is a pair $A = (|A|, P(A))$ where $|A|$ is a countable set called the web of $A$ and $P(A)$ is a subset of $(\mathbb{R}^+)^{|A|}$ such that the following holds:

**closedness:** $P(A)^{\perp \perp} = P(A)$,

**boundedness:** $\forall a \in |A|, \exists \mu > 0, \forall v \in P(A), v_a \le \mu$,

**completeness:** $\forall a \in |A|, \exists \lambda > 0, \lambda e_a \in P(A)$,

where $e_a$ denotes the base vector for $a$: $(e_a)_b = \delta_{a,b}$, with $\delta$ the Kronecker delta.

The dual of a PCS $A$ is defined by $A^{\perp} = (|A|, P(A)^{\perp})$.

Notice that we do not require $P(A) \subseteq [0, 1]^{|A|}$, we shall understand why with the exponential construction (see Example 4).

We consider $(\mathbb{R}^+ \cup \{\infty\})^{|A|}$ endowed with the pointwise order:

$$ v \le w = \forall a \in |A|, v_a \le w_a, \qquad (6) $$

with the lub of $P \subseteq (\mathbb{R}^+ \cup \{\infty\})^{|A|}$ given by: $\forall a \in |A|$, $(\sup P)_a = \sup_{v \in P} v_a$. Notice that, thanks to boundedness, $(\sup P(A))_a \in \mathbb{R}^+$, we denote it by $(\sup A)_a$ and call it the greatest coefficient of $A$ along $a$.

The following is a variant of a theorem in [8], giving an equivalent presentation of a PCS, based on the notions of Scott closure and convex closure. Its proof is a standard application of the Hahn-Banach Theorem.
**Proposition 1 ([8]).** Let I be a countable set and S ⊆ ℝ$^{+I}$. The pair (I, S) is a probabilistic coherence space iff:

1. S is bounded and complete (see Def. 1);

2. S is Scott closed, i.e. ∀u ≤ v ∈ S, u ∈ S, and ∀D ⊆ S directed, sup D ∈ S;

3. S is convex, i.e. ∀u, v ∈ S, λ ≤ 1, λu + (1 − λ)v ∈ S.

**Definition 2.** The category Pcoh has as objects PCSs and the set Pcoh($\mathcal{A}$, $\mathcal{B}$) of morphisms from $\mathcal{A}$ to $\mathcal{B}$ is the set of those matrices $f \in (\mathbb{R}^+)^{|\mathcal{A}| \times |\mathcal{B}|}$ s.t.:

$$ \forall v \in \mathbf{P}(\mathcal{A}), f v \in \mathbf{P}(\mathcal{B}), \qquad (7) $$

where $fv$ is the usual matricial product: $\forall b \in |\mathcal{B}|$, $(fv)_b = \sum_{a \in |\mathcal{A}|} f_{a,b}v_a$.

The identity id$^A$ on $\mathcal{A}$ is defined as the diagonal matrix given by $(\mathrm{id}^A)_{a,a'} = \delta_{a,a'}$. Composition of morphisms is matrix multiplication: $(g \circ f)_{a,c} = \sum_{b \in |\mathcal{B}|} f_{a,b}g_{b,c}$, where $f \in \mathrm{Pcoh}(\mathcal{A}, \mathcal{B})$, $g \in \mathrm{Pcoh}(\mathcal{B}, \mathcal{C})$, and $a \in |\mathcal{A}|$, $c \in |\mathcal{C}|$.

The above sum $\sum_{b \in |\mathcal{B}|} f_{a,b}g_{b,c}$ converges in $\mathbb{R}^+$, because $f, g$ enjoy condition (7).

We will often use Lemma 1, allowing us to infer condition (7) for all $v \in \mathbf{P}(\mathcal{A})$, just by testing it on a set G of generators of P($\mathcal{A}$) (see the proof in Appendix):

**Lemma 1.** Let $\mathcal{A}$, $\mathcal{B}$ be two probabilistic coherence spaces and f be a matrix in $\mathbb{R}^{|\mathcal{A}| \times |\mathcal{B}|}$. Let G ⊆ P($\mathcal{A}$) such that: (i) $G^{\perp} = \mathbf{P}(\mathcal{A})$, and (ii) $\forall v \in G$, $fv \in \mathbb{R}^{|\mathcal{B}|}$, then: $f(G)^{\perp} = f(\mathbf{P}(\mathcal{A}))^{\perp}$.

**Monoidal structure.** The bifunctor $\otimes: \mathrm{Pcoh} \times \mathrm{Pcoh} \to \mathrm{Pcoh}$ is defined as

$$ |\mathcal{A} \otimes \mathcal{B}| = |\mathcal{A}| \times |\mathcal{B}|, \quad \mathrm{P}(\mathcal{A} \otimes \mathcal{B}) = \{v \otimes w; v \in \mathrm{P}(\mathcal{A}), w \in \mathrm{P}(\mathcal{B})\}^{\perp}, $$

where $(x \otimes y)_{a,b} = x_a y_b$, for $a \in |\mathcal{A}|$ and $b \in |\mathcal{B}|$. The action of $\otimes$ on morphisms $u \in \mathrm{Pcoh}(\mathcal{A}, \mathcal{B})$ and $v \in \mathrm{Pcoh}(\mathcal{A}', \mathcal{B}')$ is defined as $(u \otimes v)_{(a,a'),(b,b')} = u_{a,b}v_{a',b'}$, for $(a, a') \in |\mathcal{A} \otimes \mathcal{A}'|$, $(b, b') \in |\mathcal{B} \otimes \mathcal{B}'|$. The symmetry $\mathrm{swap} \in \mathrm{Pcoh}(\mathcal{A} \otimes \mathcal{B}, \mathcal{B} \otimes \mathcal{A})$ is given by $\mathrm{swap}_{(a,b),(b',a')} = \delta_{a,a'}\delta_{b,b'}$. The other natural isomorphisms (associativity, neutrality) are given similarly.

In the next sections, we will often refer to the n-fold ($n \in \mathbb{N}$) tensor product over a PCS $\mathcal{A}$, which can be presented as: $|\mathcal{A}^{\otimes n}| = \{(a_1, \dots, a_n) ; a_i \in |\mathcal{A}|\}$, and $\mathrm{P}(\mathcal{A}^{\otimes n}) = \{v_1 \otimes \dots \otimes v_n ; v_i \in \mathrm{P}(\mathcal{A})\}^{\perp}$. Notice that any permutation $\sigma \in S_n$ defines a symmetry over $\mathcal{A}^{\otimes n}$, which we denote in the same way: $\sigma_{(a_1, \dots, a_n), (a'_1, \dots, a'_n)} = \prod_{i=1}^n \delta_{a_i, a'_i}$. For example, the image of a vector of the form $v_1 \otimes \dots \otimes v_n$ under $\sigma$ is $v_{\sigma(1)} \otimes \dots \otimes v_{\sigma(n)}$. The unit of $\otimes$ is given by the singleton web PCS 1 = ({★}, [0, 1]^{★}), which is also equal to $\mathcal{A}^{\otimes 0}$ for any $\mathcal{A}$.

The object of linear morphisms $\mathcal{A} \to \mathcal{B}$ is defined as

$$ |\mathcal{A} \to \mathcal{B}| = |\mathcal{A}| \times |\mathcal{B}|, \quad \mathrm{P}(\mathcal{A} \to \mathcal{B}) = \mathrm{Pcoh}(\mathcal{A}, \mathcal{B}). $$

Pcoh is ★-autonomous, the dualizing object $\perp$ being defined as the dual of 1 which is indeed equal to 1: $\perp = \mathbf{1}^{\perp} = \mathbf{1}$.
**Cartesian structure.** Pcoh admits cartesian products of any countable family $(\mathcal{A}_i)_{i \in I}$ of PCSs, defined as

$$ |\&_{i \in I} \mathcal{A}_i| = \bigcup_{i \in I} (\{i\} \times |\mathcal{A}_i|), \quad \mathrm{P}(\&_{i \in I} \mathcal{A}_i) = \{v \in \mathbb{R}^+ | \&_{i \in I} \mathcal{A}_i; \forall i \in I, \pi_i v \in \mathrm{P}(\mathcal{A}_i)\} $$

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 = v_{(i,a)}$. The $j$-th projection $\mathrm{pr}^j \in \mathrm{Pcoh}(\&_{i \in I} \mathcal{A}_i, \mathcal{A}_j)$ is $\mathrm{pr}^j_{(i,a),b} = \delta_{i,j} \delta_{a,b}$.

Notice that the empty product yields the terminal object $\top$ defined as $|\top| = \emptyset$ and $\top = \{0\}$. We may write the binary product by $\mathcal{A}_1 \& \mathcal{A}_2$, as well as any $v \in \mathrm{P}(\mathcal{A}_1 \& \mathcal{A}_2)$ by the pair $(\pi_1 v, \pi_2 v) \in \mathrm{P}(\mathcal{A}_1) \times \mathrm{P}(\mathcal{A}_2)$ of its components.

**Example 1.** All examples in this paper will be built on top of the flat interpretation of the boolean type, which is defined as the space $\mathrm{Bool} = (\bot \& \bot)^{\perp}$, which can be equally written as $\mathbf{1} \oplus \mathbf{1}$, with $\oplus$ referring to the co-product. The web $|\mathrm{Bool}|$ has two elements, that we denote as $\mathbf{t}$ and $\mathbf{f}$. The set $\mathrm{P}(\mathrm{Bool})$ is $\{\kappa e_{\mathbf{t}} + \rho e_{\mathbf{f}}; \kappa + \rho \le 1\}$, that is the sub-probabilistic distributions on the base vectors $e_{\mathbf{t}}, e_{\mathbf{f}}$. This is because $\mathrm{P}(\mathrm{Bool})^{\perp} = \mathrm{P}(\bot \& \bot) = \{\kappa e_{\mathbf{t}} + \rho e_{\mathbf{f}}; \kappa, \rho \le 1\}$.

**Example 2.** Let us compute $\mathrm{Bool}^{\otimes 2} = \mathrm{Bool} \otimes \mathrm{Bool}$. By definition we have: $|\mathrm{Bool}^{\otimes 2}| = \{(\mathbf{t}, \mathbf{t}), (\mathbf{t}, \mathbf{f}), (\mathbf{f}, \mathbf{t}), (\mathbf{f}, \mathbf{f})\}, \mathrm{P}(\mathrm{Bool}^{\otimes 2}) = \{v \otimes w; v, w \in \mathrm{P}(\mathrm{Bool})\}^{\perp}$. Using Example 1, one checks that $\{v \otimes w; v, w \in \mathrm{P}(\mathrm{Bool})\}^{\perp}$ is equal to $\{u \in \mathbb{R}^+ | \mathrm{Bool}^{\otimes 2}|; \forall (b, b') \in |\mathrm{Bool}^{\otimes 2}|, u_{b, b'} \le 1\}$. Hence, $\mathrm{P}(\mathrm{Bool}^{\otimes 2})$ is the set $\{u; \sum_{(b, b') \in \{\mathbf{t}, \mathbf{f}\}^2} u_{b, b'} \le 1\}$ of sub-probability distributions of pairs of booleans.

**Example 3.** As for $\mathrm{Bool} \to \mathrm{Bool}$, its web is $|\mathrm{Bool} \to \mathrm{Bool}| = |\mathrm{Bool} \otimes \mathrm{Bool}|$, and $f \in \mathrm{P}(\mathrm{Bool} \to \mathrm{Bool})$ whenever $\forall v \in \mathrm{P}(\mathrm{Bool}), f v \in \mathrm{P}(\mathrm{Bool})$. By Example 1, this is equivalent to $\forall \kappa + \rho \le 1$, $f(\kappa e_{\mathbf{t}} + \rho e_{\mathbf{f}})_{\mathbf{t}} + f(\kappa e_{\mathbf{t}} + \rho e_{\mathbf{f}})_{\mathbf{f}} \le 1$. By linearity, the condition boils down to $f_{\mathbf{t}, \mathbf{t}} + f_{\mathbf{t}, \mathbf{f}} \le 1$ and $f_{\mathbf{f}, \mathbf{t}} + f_{\mathbf{f}, \mathbf{f}} \le 1$. That is: $\mathrm{P}(\mathrm{Bool} \to \mathrm{Bool})$ is the set of stochastic matrices over $\{\mathbf{t}, \mathbf{f}\}$, as expected.

**Exponential structure.** We recall the exponential modality given in [3] and we call it the *entire exponential modality*, denoted by $!_e$, in opposition to the *free exponential modality* $!_f$ whose definition is the goal of Section 4. The main result of the paper is proving that the two modalities, although different in the presentation, actually give the same object (Proposition 5). The adjective *entire* is motivated by the key property that the morphisms from $\mathcal{A}$ to $\mathcal{B}$ in the Kleisli category associated with $!_e$, that is the linear morphisms from $!_e \mathcal{A}$ to $\mathcal{B}$, can be seen as entire functions from $\mathrm{P}(\mathcal{A})$ to $\mathrm{P}(\mathcal{B})$. We refer to [3] for details.

The functorial promotion $!_e : \mathrm{Pcoh} \to \mathrm{Pcoh}$ is defined on objects as

$$ |!_e \mathcal{A}| = \mathcal{M}_f(|\mathcal{A}|), \quad \mathrm{P}(!_e \mathcal{A}) = \{v^{!_e}; v \in \mathrm{P}(\mathcal{A})\}^{\perp}, \quad (8) $$

where $v^{!_e}$ is the vector of $(\mathbb{R}^+)^{\mathcal{M}_f(|\mathcal{A}|)}$ defined as $v^{!_e} = \prod_{a \in \mathrm{Supp}(\mu)} v_a^{\mu(a)}$, for any $\mu \in \mathcal{M}_f(|\mathcal{A}|)$. The action of $!_e$ on a morphism $f \in \mathrm{Pcoh}(\mathcal{A}, \mathcal{B})$ is defined, for
any $\mu \in |!_e A|$ and $\nu = [b_1, \dots, b_n] \in |!_e B|$, as:

$$ (!_e f)_{\mu,\nu} = \sum_{\substack{(a_1, \dots, a_n); \\ [a_1, \dots, a_n]=\mu}} \prod_{i=1}^{n} f_{a_i, b_i} \qquad (9) $$

Notice that the above sum varies on the set of different enumerations of $\mu$. If $\mu$ is a multiset $[a, \dots, a]$ of support a singleton, then the sum has only one term, while in case of multisets with no repetitions, the sum has $n!$ terms. Remark also that the definition is independent from the chosen enumeration of $\nu$.

**Example 4.** Equation (9) introduces arbitrary large scalars, moving us away from the intuitive setting of distributions and stochastic matrixes (see Examples 1, 3). For an example, consider the morphism $f \in \mathbf{Pcoh}(\mathbf{Bool}, \mathbf{1})$ defined by $f_{\mathbf{t},*} = f_{\mathbf{f},*} = 1$. Remark that for any $n, m \in \mathbb{N}$, we have: $!_e f_{[\mathbf{t}^n, \mathbf{f}^m], [\star^{n+m}]} = \frac{(n+m)!}{n!m!}$, which is the number of different enumerations of the multiset $[\mathbf{t}^n, \mathbf{f}^m]$ with $n$ (resp. $m$) occurrences of $\mathbf{t}$ (resp. $\mathbf{f}$). This shows why, in the definition of a PCS, coefficients have to be in the whole of $\mathbb{R}^+$ and cannot be restricted to $[0, 1]$.

The functorial promotion is equipped with a structure of comonad. The counit (or dereliction) $\mathrm{der}_A \in \mathbf{Pcoh}(!_e A, A)$ is defined as $(\mathrm{der}_A)_{\mu,a} = \delta_{\mu, [a]}$. The comultiplication (or digging), denoted as $\mathrm{digg}_A \in \mathbf{Pcoh}(!_e A, !_e A)$, is given by $(\mathrm{digg}_A)_{\mu,M} = \delta_{\mu, \biguplus M}$, where $\biguplus M$ is the multiset in $|!_e A|$ obtained as the multiset union of the multisets in $M \in |!_e A|$.

The PCSs $!_e A \otimes !_e B$ and $!_e (A \& B)$ are naturally isomorphic, hence we get a model of LL, according to the so-called new-Seely axiomatisation (see [10]). In particular, contraction $\mathrm{contr}_A \in \mathbf{Pcoh}(!_f A, !_f A \otimes !_f A)$ and weakening $\mathrm{weak}_A \in \mathbf{Pcoh}(!_f A, \mathbf{1})$ are given by $(\mathrm{contr}_A)_{\mu, (\mu', \mu'')} = \delta_{\mu, \mu' \uplus \mu''}$, and $(\mathrm{weak}_A)_{\mu, \star} = \delta_{\mu, \llcorner}$.

# 3 The free exponential modality

We first recall Lafont’s axiomatisation of linear logic models (Theorem 1), this is a more restricted axiomatisation than the new-Seely one. The key notion is the free exponential modality. We then recall a general recipe by Melliès, Tasson and Tabareau [11] for constructing this free modality whenever specific conditions hold (Proposition 2). Section 4 applies this recipe to $\mathbf{Pcoh}$.

## 3.1 Lafont's model

By definition, the structure of an exponential modality turns an object $A$ into a commutative comonoid $!A$, with the comultiplication given by contraction and the neutral element given by weakening: $1 \leftarrow \mathbf{weak}_{!A} !A \xrightarrow{\mathrm{contr}_{!A}} !A \otimes !A$. The converse does not hold in general, since commutative comonoids may lack a comonad structure (dereliction, digging, and the action on morphisms). However, Lafont proves that in case the commutative comonoid is the free one then its universal property allows one to canonically construct the missing structure:
**Theorem 1 ([9]).** A $\star$-autonomous category $\mathbb{C}$ is a model of linear logic if:

1. it has finite products and,

2. for every object $A$, there exists a triplet ($!_f A$, weak$_{!f} A$, contr$_{!f} A$) which is the free commutative comonoid generated by $A$.

Condition (2) requires the comonoid $!_f A$ to be endowed with a morphism $\mathrm{der}_A \in \mathbb{C}(!_f A, A)$, such that, for all commutative comonoid $C$ and $f \in \mathbb{C}(C, A)$, there exists exactly one commutative comonoid morphism $f^\dagger$ such that $f^\dagger \circ \mathrm{der}!_f A = f$.

This corresponds to saying that the category of commutative comonoids over $A$ has $!_f A$ as the terminal object.

*Example 5 (Coh)*. The first model of LL was introduced by Girard using the notion of coherence space [6]. A coherence space $A = (|A|, \oslash_A)$ is a pair of a set $|A|$, the *web*, and a symmetric reflexive relation $\oslash_A$, the *coherence*. The exponential modality of the original model is given by the finite cliques functor, $|!A| = \{x \subseteq_f |A| \mid \forall a, a' \in x, a \oslash_A a'\}$, while the free exponential modality $|!_f A| = \{\mu \in \mathcal{M}_f(|A|) \mid \forall a, a' \in \mathrm{Supp}(\mu), a \oslash_A a'\}$ is given by the finite multi-cliques functor, as shown in [12]. The morphism $(\mathrm{der}_A)^\dagger$ factoring $!A$ through $!_f A$ is given by the support relation: $(\mathrm{der}_A)^\dagger = \{(\mathrm{Supp}(\mu), \mu) \mid \mu \in |!_f A|\}$.

## 3.2 Melliès, Tasson and Tabareau's formula

Melliès et al. give a recipe for constructing free commutative comonoids in [11], adapting the well-known formula defining the symmetric algebra generated by a vector space in the setting of LL. This adaptation is non-trivial mainly because the vector space construction uses biproducts, while products and coproducts are in general distinct in LL models, and in fact this is the case for **Pcoh**.

The idea of [11] is to define $!_f A$ as the projective limit of the sequence of its "approximants" $A^{\le 0}, A^{\le 1}, A^{\le 2}, \dots$, where an approximant $A^{\le n}$ is the equalizer of the $n!$ tensor symmetries over $(A \& 1)^{\otimes n}$. Intuitively, the object $A^{\le n}$ describes the behavior of data of type $!_f A$ when duplicated *at most* $n$ times. This behavior is given by the equalizers of the tensor symmetries because the model does not distinguish between the evaluation order of the $n$ copies (in categorical terms, we are considering *commutative comonoids*). We start from $A \& 1$ instead of $A$ because, in order to have a sequence, we need that each $A^{\le n}$ in some sense encompasses its predecessors $A^{\le 0}, A^{\le 1}, \dots, A^{\le n-1}$. The exact meaning of "*to encompass*" is given by a family of morphisms $\rho_{n,n-1} \in \mathbb{C}(A^{\le n} \mapsto A^{\le n-1})$ generated by the right projection of the product $A \& 1$ (see Notation 2). In standard coherence spaces, this turns out to be the simple fact that the set of cliques of $A^{\le n+1}$ *contains* the cliques of $A^{\le n}$. In contrast, this intuition is misleading for **Pcoh** (Example 8), making our construction considerably subtler.

**Notation 2** Given an object $A$ of a symmetric monoidal category with finite cartesian products $\mathbb{C}$ and a number $n \in \mathbb{N}$, we denote by $A^{\le n}$ the equalizer of the $n! \otimes$ symmetries of $(A \& 1)^{\otimes n}$ (Figure 1a), whenever it exists. Moreover, we denote by $\rho_{n+1,n}$ the morphism $\mathbb{C}(A^{\le n+1}, A^{\le n})$ obtained by applying the universal
<figure><img src="image_2.png" /></figure>

(a) Universal property of $A^{\le n}$, eq: $\forall C, \forall f \in C(C, (A \otimes 1)^{\otimes n})$ invariant under $\otimes$ symm., $\exists! f^\dagger \in C(C, A^{\le n})$ commuting the diagram.

(b) diagram defining the commutation of $A^{\le n}$ with the $\otimes$ product.

<figure><img src="image_3.png" /><figcaption>Fig. 1: Properties of the approximants $A^{\le n}$ of $!_f A$</figcaption></figure>

Fig. 2: Diagram defining the commutation of the limit $!_f A$ with $\otimes$: for every objects $B, C$ and family of morphisms $(f_i)_{i \in \mathbb{N}}$ making the diagram above commute, there exists a unique $f^\dagger \in C(C, !_f A \otimes B)$ making the diagram commute.

property of $A^{\le n}$ to $(\mathrm{id} \otimes \mathrm{pr}_r) \circ \mathrm{eq}$, i.e. taking in Figure 1a the object $C = A^{\le n+1}$ and $f = (\mathrm{id} \otimes \mathrm{pr}_r) \circ \mathrm{eq}$, with $\mathrm{pr}_r$ denoting the right projection of $A \& 1$.

**Proposition 2** ([11]). Let $A$ be an object of a cartesian symmetric monoidal category $\mathcal{C}$, the free commutative comonoid generated by $A$ is the limit of:

$$A^{\le 0} \leftarrow \rho_{1,0} \quad A^{\le 1} \leftarrow \rho_{2,1} \quad A^{\le 2} \leftarrow \rho_{3,2} \quad A^{\le 3} \leftarrow \rho_{4,3} \dots$$

provided that:

1. $\forall n \in \mathbb{N}$, the equalizer $A^{\le n}$ exists and commutes with tensor products (Fig. 1b);

2. the limit $!_f A$ of the diagram exists and commutes with tensor products (Fig. 2).

# 4 The case of probabilistic coherence spaces

In this section we prove that **Pcoh** is a Lafont model. First, we define the free commutative comonad $!_f \mathcal{A}$ (Definition 3 and Corollary 1) by applying Melliès et al.'s recipe (Subsections 4.1 and 4.2), then we prove that $!_f \mathcal{A}$ is actually equivalent to the entire exponential modality $!_e \mathcal{A}$ defined in Section 2 (Proposition 5).

## 4.1 The approximants $\mathcal{A}^{\le n}$

The first step for applying Proposition 2 is to define the approximants $\mathcal{A}^{\le n}$ and to prove that they commute with the tensor product (Condition 1 of Proposition 2). By definition $\mathcal{A}^{\le n}$ is the equalizer of the symmetries of $(\mathcal{A} \& 1)^{\otimes n}$, so
first we prove that the equalizer $\mathcal{A}^n$ of the symmetries of $\mathcal{A}^{\otimes n}$ exists for any space $\mathcal{A}$ and that it commutes with $\otimes$ (Proposition 3), then we show (Lemma 3) that $\mathcal{A}^{\le n} = (\mathcal{A} \& \mathbf{1})^n$ can be directly defined from $\mathcal{A}$, by means of an operator $\langle u_1, \dots, u_n \rangle$ over the vectors in $\mathbf{P}(\mathcal{A})$, crucial for the next step.

Recall from Section 2 that $\mathcal{A}^{\otimes n}$ can be described as having as web the set of length $n$ sequences $\mathbf{a}$ of elements in $|\mathcal{A}|$. Recall also the notation given in Section 1. Given the permutation group $S_n$, we define an endomorphism $s_n$ over $\mathcal{A}^{\otimes n}$, by taking the barycentric sum of the actions of $S_n$ over $\mathcal{A}$, so: $s_n = \frac{1}{n!} \sum_{\sigma \in S_n} \sigma$, which can be explicitly defined as a matrix by: $(s_n)_{\mathbf{a}, \mathbf{a}'} = \delta_{\tilde{\mathbf{a}}, \tilde{\mathbf{a}}'} \frac{1}{m(\tilde{\mathbf{a}})}$.

In fact, $(s_n)_{\mathbf{a}, \mathbf{a}'} = \frac{\#\{\sigma \in S_n : \forall i \le n, a_{\sigma(i)} = a_i'\}}{n!} = \delta_{\tilde{\mathbf{a}}, \tilde{\mathbf{a}}'} \frac{\prod_{\mathbf{a} \in \text{Supp}(\tilde{\mathbf{a}})} (\tilde{\mathbf{a}})(\mathbf{a})!}{n!}$.

**Remark 1.** The value of the matrix $s_n$ defined above does not depend on the sequences $\mathbf{a}, \mathbf{a}'$ but just on their associated multisets $\tilde{\mathbf{a}}, \tilde{\mathbf{a}}'$. Hence, for any $v \in \mathbb{R}^+ |\mathcal{A}^{\otimes n}|$, the vector $s_n v \in \mathbb{R}^+ |\mathcal{A}^{\otimes n}|$ can be also presented as in $\mathbb{R}^+ \mathcal{M}_n(|\mathcal{A}|)$:

$$ (s_n v)_\mu = \frac{1}{m(\mu)} \sum_{\mathbf{a} \in \text{Enum}(\mu)} v_\mathbf{a}, \quad \text{for } \mu \in \mathcal{M}_n(|\mathcal{A}|) \quad (10) $$

which is a barycentric sum because $m(\mu)$ gives exactly the cardinality of Enum($\mu$).

This “change of base” can be explained also as follows: the image-set $s_n(\mathcal{A}^{\otimes n})$ of $s_n$ is a subspace of $\mathcal{A}^{\otimes n}$ and the “canonical base” of this subspace can be given by $\mathcal{M}_n(|\mathcal{A}|)$. A vector $s_n v \in s_n(\mathcal{A}^{\otimes n}) \subseteq \mathcal{A}^{\otimes n}$ can be presented then either as a family indexed by sequences (using the canonical base of $\mathcal{A}^{\otimes n}$) or as a family indexed by multisets (using the canonical base of $s_n(\mathcal{A}^{\otimes n})$).

**Lemma 2.** The following are equivalent characterizations of a PCS $\mathcal{A}^n$ with web $|\mathcal{A}^n| = \mathcal{M}_n(|\mathcal{A}|)$:

1. $\text{P}(\mathcal{A}^n) = \{s_n (\otimes_{i=1}^n u_i) ; u_i \in \text{P}(\mathcal{A})\}^{\perp\perp}$,

2. $\text{P}(\mathcal{A}^n) = \{s_n u ; u \in \text{P}(\mathcal{A}^{\otimes n})\}$.

*Proof.* First, by Remark 1 notice that both sets in conditions 1. and 2. can be seen as sets of vectors over $\mathcal{M}_n(|\mathcal{A}|)$. The case 1. is a PCS by definition, while 2. can be checked to be a PCS by means of Proposition 1. In particular, notice that 2. is Scott closed over the web $\mathcal{M}_n(|\mathcal{A}|)$, but not over $|\mathcal{A}^{\otimes n}|$.

Then, the equivalence between 1. and 2. is obtained by Lemma 1, taking $\mathcal{A} = \mathcal{A}^{\otimes n}$, $G = \{\otimes_{i=1}^n u_i ; u_i \in \text{P}(\mathcal{A})\}$, $\mathcal{B}$ the set described in 2. and $f = s_n$. The set described in 1. is equal to $f(G)^{\perp\perp} = f(P(\mathcal{A}^{\otimes n}))^{\perp\perp}$ which turns out to be the bipolar of $\mathcal{B}$ by Lemma 1. We conclude since $\mathcal{B} = \mathcal{B}^{\perp\perp}$ as just remarked. $\square$

**Example 6.** Let us illustrate the construction of $\mathcal{A}^n$ in the case where $\mathcal{A}$ is the boolean space $\text{Bool}$ (see Example 1). It is trivial to check that $\text{Bool}^0$ is isomorphic to $\mathbf{1}$ and $\text{Bool}^1$ to $\text{Bool}$. Concerning $\text{Bool}^2$, we have $|\text{Bool}^2| = \{[\mathbf{t}, \mathbf{f}], [\mathbf{t}, \mathbf{t}], [\mathbf{f}, \mathbf{f}]\}$. Recall that Example 2 computes $\text{P}(\text{Bool}^{\otimes 2})$ as the set of
sub-probability distributions over boolean pairs, so that by item 2. of Lemma 2 we have that: $P(\mathbf{Bool}^2) = \{w \in \mathbb{R}^{+\mathcal{M}_2(|\mathbf{Bool}|)}; w_{[\mathbf{t},\mathbf{t}]} + w_{[\mathbf{f},\mathbf{f}]} + 2w_{[\mathbf{t},\mathbf{f}]} \le 1\}$.

This characterization allows us to compute: $(\sup \mathbf{Bool}^2)_{[\mathbf{t},\mathbf{t}]} = (\sup \mathbf{Bool}^2)_{[\mathbf{f},\mathbf{f}]} = 1$, while $(\sup \mathbf{Bool}^2)_{[\mathbf{t},\mathbf{f}]} = \frac{1}{2}$. Actually, using Equation (10), one can check in general: $(\sup \mathbf{Bool}^n)_\mu = \frac{1}{m(\mu)}$ (recall Equation (3)). Notice that these coefficients are the inverses of the coefficients computed in Example 4.

**Proposition 3.** Let $\mathcal{A}$ be a PCS and $n \in \mathbb{N}$. The object $\mathcal{A}^n$ together with the morphism $\mathrm{eq}^{\mathcal{A}^n} \in \mathbf{Pcoh}(\mathcal{A}^n, \mathcal{A}^{\otimes n})$, defined as $\mathrm{eq}_{\mu, \tilde{\mathbf{a}}}^{\mathcal{A}^n} = \delta_{\mu, \tilde{\mathbf{a}}}$, is the equalizer of the $n!$ symmetries of the $n$-fold tensor $\mathcal{A}^{\otimes n}$.

Moreover, these equalizers commute with the tensor product, meaning that for any $\mathcal{B}$, the morphism $\mathrm{eq}^{\mathcal{A}^n} \otimes \mathrm{id}^{\mathcal{B}}$ is the limit of the morphisms $\sigma \otimes \mathrm{id}^{\mathcal{B}}$ for $\sigma \in S_n$ (see diagram in Figure 1b, replacing $\mathcal{A}$ & 1 with $\mathcal{A}$ and $\mathcal{A}^{\le n}$ with $\mathcal{A}^n$).

*Proof.* The fact that $\mathrm{eq}^{\mathcal{A}^n}$ is a morphism in $\mathbf{Pcoh}(\mathcal{A}^n, \mathcal{A}^{\otimes n})$ is immediate, because $\mathrm{eq}^{\mathcal{A}^n}$ simply maps a vector $s_n u$ seen as a vector over the web $M_n(|\mathcal{A}|)$ to the same vector seen over the web $|\mathcal{A}^{\otimes n}|$. This latter is a vector of $P(\mathcal{A}^{\otimes n})$ (supposing $u \in P(\mathcal{A}^{\otimes n})$) because it is a barycentric sum of vectors in $P(\mathcal{A}^{\otimes n})$.

We only prove the commutation with $\otimes$, as the universal property of the equalizer is a direct consequence of the commutation, taking $\mathcal{B} = 1$.

Let $\mathcal{C}$ be a PCS and $f \in \mathbf{Pcoh}(\mathcal{C}, \mathcal{A}^{\otimes n} \otimes \mathcal{B})$ be a morphism such that $(\sigma \otimes \mathrm{id}^{\mathcal{B}}) \circ f = f$ for any $\sigma \in S_n$. Then, define $f^\dagger \in \mathbf{Pcoh}(\mathcal{C}, \mathcal{A}^n \otimes \mathcal{B})$ as follows: for every $c \in |\mathcal{C}|$, $b \in |\mathcal{B}|$, $\mu \in |\mathcal{A}^n|$, $f^\dagger_{c,(b,\mu)} = f_{c,(b,\mathbf{a})}$, where $\mathbf{a}$ is any enumeration of $\mu$ (no matter which one because $f$ is invariant under the tensor symmetries). The fact that $f^\dagger$ is the unique morphism commuting the diagram of Figure 1a is a trivial calculation. We have then to prove that it is indeed a morphism in $\mathbf{Pcoh}(\mathcal{C}, \mathcal{A}^n \otimes \mathcal{B})$, that means that, for any $v \in P(\mathcal{C})$, $f^\dagger v \in P(\mathcal{A}^n \otimes \mathcal{B})$.

Consider $w \in P(\mathcal{A}^n \otimes \mathcal{B})^\perp$ and let us prove that $\langle f^\dagger v, w \rangle \le 1$. This will allow us to conclude $f^\dagger v \in P(\mathcal{A}^n \otimes \mathcal{B})$. Define $\bar{w} \in \mathbb{R}^+|\mathcal{A}^{\otimes n} \otimes \mathcal{B}|$ as $\bar{w}_{(\mathbf{a},b)} = \frac{1}{m(\tilde{\mathbf{a}})}w_{\tilde{\mathbf{a}},b}$.

First, notice that $\bar{w} \in P(\mathcal{A}^{\otimes n} \otimes \mathcal{B})^\perp$. In fact, for any $u \in P(\mathcal{A}^{\otimes n})$, $z \in P(\mathcal{B})$:

$$ \begin{aligned} \langle u \otimes z, \bar{w} \rangle &= \sum_{\mathbf{a},b} u_{\mathbf{a}} z_b \bar{w}_{(\mathbf{a},b)} = \sum_{\mathbf{a},b} u_{\mathbf{a}} z_b \frac{1}{m(\tilde{\mathbf{a}})} w_{\tilde{\mathbf{a}},b} = \sum_{\mu,b} z_b w_{\mu,b} \sum_{\mathbf{a} \in \mathrm{Enum}(\mu)} \frac{1}{m(\mu)} u_{\mathbf{a}} \\ &= \sum_{\mu,b} z_b w_{\mu,b} (s_n u)_\mu = \langle (s_n u) \otimes z, w \rangle \le 1. \end{aligned} $$

The last inequality is due to $w \in P(\mathcal{A}^n \otimes \mathcal{B})^\perp$, $s_n u \in P(\mathcal{A}^n)$ and Lemma 2.

Second, $\langle f^\dagger v, w \rangle = \langle f v, \bar{w} \rangle$. In fact,

$$ \langle f^\dagger v, w \rangle = \sum_{\mu,b} (f^\dagger v)_{\mu,b} w_{\mu,b} = \sum_{\mathbf{a},b} \frac{(f v)_{\mathbf{a},b} w_{\tilde{\mathbf{a}},b}}{m(\tilde{\mathbf{a}})} = \sum_{\mathbf{a},b} (f v)_{\mathbf{a},b} \bar{w}_{\mathbf{a},b} = \langle f v, \bar{w} \rangle. $$

We then conclude because by hypothesis $f v \in P(\mathcal{A}^{\otimes n} \otimes \mathcal{B})$. $\square$
Given a PCS $\mathcal{A}$ and $n \in \mathbb{N}$, let us introduce the notation $\mathcal{A}^{\le n} = (\mathcal{A} \& \mathbf{1})^n$, for the equalizer of the $n$-fold tensor symmetries of $\mathcal{A} \& \mathbf{1}$.

**Lemma 3.** The PCS $\mathcal{A}^{\le n}$ can be presented as follows:

$$|\mathcal{A}^{\le n}| = \bigcup_{k \le n} \mathcal{M}_k(|\mathcal{A}|), \quad \mathrm{P}(\mathcal{A}^{\le n}) = \{\langle u_1, \dots, u_n \rangle ; \forall i \le n, u_i \in \mathrm{P}(\mathcal{A})\}^{\perp\perp}$$

where, for any $[a_1, \dots, a_k] \in |\mathcal{A}^{\le n}|$,

$$\langle u_1, \dots, u_n \rangle_{[a_1, \dots, a_k]} = \frac{1}{n!} \sum_{\sigma \in S_n} \prod_{i=1}^{k} (u_{\sigma(i)})_{a_i} \quad (11)$$

$$= \frac{(n-k)!}{n!} \sum_{f: \{1, \dots, k\} \to \{1, \dots, n\}} \prod_{i=1}^{k} (u_{f(i)})_{a_i}. \quad (12)$$

*Proof.* First, notice that there is a bijection between $|\mathcal{A}^{\le n}|$ and $\mathcal{M}_n(|\mathcal{A}|\uplus\{\star\}) = |(\mathcal{A} \& \mathbf{1})^n|$ obtained just by adding the necessary number of $\star$'s to a multiset in $|\mathcal{A}^{\le n}|$. Second, the definitions of $\mathrm{P}(\mathcal{A}^{\le n})$ and of $\langle u_1, \dots, u_n \rangle$ immediately follow by remarking that the latter is a notation for $s_n((u_1, e_\star) \otimes \dots \otimes (u_n, e_\star))$, with $s_n$ the endomorphism over $(\mathcal{A} \& \mathbf{1})^{\otimes n}$ defined by Equation (10). $\square$

*Example 7.* We have no simple characterization of $\mathrm{Bool}^{\le 2}$, but Lemma 3 helps us in computing the coefficients of its generators. For example, we have $\langle e_t, e_f \rangle_\mu = 1$ if $\mu = []$, otherwise $\langle e_t, e_f \rangle_\mu = \frac{1}{2}$. While $\langle e_t, e_t \rangle_\mu = 1$ for any multiset of support $\{e_t\}$, otherwise it is 0. One can observe in general that $(\sup \mathrm{Bool}^{\le n})_\mu = 1$ for any multiset $\mu \in |\mathrm{Bool}^{\le n}|$ which is uniform (i.e. of which support is at most a singleton), while $(\sup \mathrm{Bool}^{\le n})_\mu < 1$ for $\mu$ non-uniform.

Henceforth, we will consider $\mathcal{A}^{\le n}$ as presented in Lemma 3.

## 4.2 The limit $!_f \mathcal{A}$

The quest for a limit $!_f \mathcal{A}$ of the family $(\mathcal{A}^{\le n})_n$ requires the study of the relations between approximants of different degree. This is done starting from the following notions of injection and projection. Given $\mathcal{A}, \mathcal{B}$ s.t. $|\mathcal{A}| \subseteq |\mathcal{B}|$, we define the matrices injection $\iota_{\mathcal{A},\mathcal{B}} \in \mathbb{R}^{+|\mathcal{A}|\times|\mathcal{B}|}$ and projection $\rho_{\mathcal{B},\mathcal{A}} \in \mathbb{R}^{+|\mathcal{B}|\times|\mathcal{A}|}$ as follows:

$$(\iota_{\mathcal{A},\mathcal{B}})_{a,b} = (\rho_{\mathcal{B},\mathcal{A}})_{b,a} = \delta_{a,b}. \quad (13)$$

The injection $\iota_{\mathcal{A},\mathcal{B}}$ maps a vector $u \in \mathbb{R}^{+|\mathcal{A}|}$ to the vector $(u, \mathbf{0}) \in \mathbb{R}^{+|\mathcal{B}|}$ associating the directions in $|\mathcal{B}| \setminus |\mathcal{A}|$ with zero. The projection $\rho_{\mathcal{B},\mathcal{A}}$ maps a vector $(u, v) \in \mathbb{R}^{+|\mathcal{B}|}$ to its restriction $u$ to the directions within $|\mathcal{A}|$. In order to have these matrices as morphisms in $\mathrm{Pcoh}$, we have to prove that $(u, \mathbf{0}) \in \mathrm{P}(\mathcal{B})$ whenever $u \in \mathrm{P}(\mathcal{A})$ (resp. $u \in \mathrm{P}(\mathcal{A})$ whenever $(u, v) \in \mathrm{P}(\mathcal{B})$).

As already remarked in Definition 2, the projection of $\mathcal{A}^{\le n+1}$ into $\mathcal{A}^{\le n}$ is actually obtained by applying the universal property to the morphism $(\mathrm{id} \otimes \mathrm{pr}_r) \circ \mathrm{eq}$. So we get the following immediate lemma.
**Lemma 4.** For any $m \ge n$ and $\mathcal{A}$, we have: $\rho_{\mathcal{A}^{\le m}, \mathcal{A}^{\le n}} \in \mathrm{Pcoh}(\mathcal{A}^{\le m}, \mathcal{A}^{\le n})$ and $\iota_{\mathcal{A}^{\le n}, \mathcal{A}^{\le m}} \in \mathrm{Pcoh}(\mathcal{A}^{\le n}, \mathcal{A}^{\le m})$.

The interesting point is that the dual version of Lemma 4 does not hold: in general, the injection of $\mathcal{A}^{\le n}$ into $\mathcal{A}^{\le n+1}$ (resp. projection of $(\mathcal{A}^{\le n+1})^{\perp}$ into $(\mathcal{A}^{\le n})^{\perp}$) is not a morphism of $\mathrm{Pcoh}$.

**Example 8.** In Example 7, we discussed $\langle e_t, e_f \rangle \in P(\mathrm{Bool}^{\le 2})$. Let us prove now that $\iota_{\mathrm{Bool}^{\le 2}, \mathrm{Bool}^{\le 3}} \langle e_t, e_f \rangle \notin P(\mathrm{Bool}^{\le 3})$. In fact, $(\iota_{\mathrm{Bool}^{\le 2}, \mathrm{Bool}^{\le 3}} \langle e_t, e_f \rangle)_{[t,f]} = \langle e_t, e_f \rangle_{[t,f]} = \frac{1}{2}$, while we can prove $(\sup P(\mathrm{Bool}^{\le 3}))_{[t,f]} = \frac{1}{3}$. The latter claim is because $P(\mathrm{Bool}^{\le 3}) = \{\langle e_t, e_t, e_t \rangle, \langle e_t, e_t, e_f \rangle, \langle e_t, e_f, e_f \rangle, \langle e_f, e_f, e_f \rangle\}^{\perp\perp}$ and the maximal value of these generators on $[t,f]$ is $\frac{1}{3}$.

One can however add a correction factor in order to embed $\mathcal{A}^{\le n}$ into $\mathcal{A}^{\le N}$ for any $N \ge n$, as follows. Let:

$$ (\iota_{\mathcal{A},n,N}^{\mathrm{cor}})_{\mu,\nu} = \begin{cases} \frac{(N-k)!q^k n!}{N!(n-k)!} & \text{if } \mu = \nu \text{ and } \#\mu = k \le n \\ 0 & \text{and } q = \lfloor \frac{N}{n} \rfloor \text{ and } r = N \mod n; \\ 0 & \text{otherwise.} \end{cases} \quad (14) $$

**Lemma 5.** The matrix $\iota_{\mathcal{A},n,N}^{\mathrm{cor}}$ is a morphism in $\mathrm{Pcoh}(\mathcal{A}^{\le n}, \mathcal{A}^{\le N})$ mapping, in particular, $\langle u_1, \dots, u_n \rangle \in P(\mathcal{A}^{\le n})$ to $\langle u_1^q, \dots, u_n^q, \mathbf{0}^r \rangle \in P(\mathcal{A}^{\le N})$, where $q$ is the quotient $\lfloor \frac{N}{n} \rfloor$ and $r$ the remainder $N \mod n$ of the euclidean division $\frac{N}{n}$. Moreover, $u_i^q$ is a notation for $\underbrace{u_i, \dots, u_i}_{q \text{ times}}$ (and similarly for $\mathbf{0}^r$).

*Proof.* One has just to prove the last part of the statement, the rest follows by Lemma 1 because the vectors of the form $\langle u_1, \dots, u_n \rangle$ yield a base for $P(\mathcal{A}^{\le n})$ (Lemma 3). We have, for any multiset $\mu = [a_1, \dots, a_k]$,

$$ \begin{align*} (\iota_{\mathcal{A},n,N}^{\mathrm{cor}} \langle u_1, \dots, u_n \rangle)_{\mu} &= \left( \frac{(N-k)!q^k n!}{N!(n-k)!} \right) \frac{(n-k)!}{n!} \sum_{f:\{1,\dots,k\} \hookrightarrow \{1,\dots,n\}} \prod_{i=1}^{k} (u_{f(i)})_{a_i} \\ &= \frac{(N-k)!}{N!} q^k \sum_{f:\{1,\dots,k\} \hookrightarrow \{1,\dots,n\}} \prod_{i=1}^{k} (u_{f(i)})_{a_i} \\ &= \frac{(N-k)!}{N!} \sum_{f:\{1,\dots,k\} \hookrightarrow \{1,\dots,nq\}} \prod_{i=1}^{k} (u_{\lfloor f(i)/q \rfloor+1})_{a_i} \\ &= \langle u_1^q, \dots, u_n^q, \mathbf{0}^r \rangle_{\mu}. \end{align*} $$

where we use $\hookrightarrow$ to denote injective functions and where from line 2 to 3, we use the count $q^k$ to enlarge the codomain of the injections $f$ indexing the sum. $\square$
Notice that, with $N = nq + r$:

$$ \lim_{N \to \infty} \frac{(N-k)!q^k n!}{N!(n-k)!} = \frac{n!}{n^k(n-k)!}, \qquad (15) $$

$$ ( \lim_{N \to \infty} \iota_{A,n,N}^{\text{cor}} \langle u_1, \dots, u_n \rangle )_{\mu} = \frac{1}{n^k} \sum_{f: \{1, \dots, k\} \hookrightarrow \{1, \dots, n\}} \prod_{i=1}^{k} (u_{f(i)})_{a_i}. \quad (16) $$

This allows us to introduce the following definition and key proposition:

**Definition 3.** Given $\mathcal{A}$, we define $!_f \mathcal{A}$ as:

$$ \begin{gathered} !_f \mathcal{A} = \mathcal{M}_f(|\mathcal{A}|), \quad \mathrm{P}(!_f \mathcal{A}) = \{\langle\langle u_1, \dots, u_n \rangle\rangle; n \in \mathbb{N}, \forall i \le n, u_i \in \mathrm{P}(\mathcal{A})\}^{\perp\perp}, \\ \text{where: } \langle\langle u_1, \dots, u_n \rangle\rangle_{[a_1, \dots, a_k]} = \frac{1}{n^k} \sum_{f: \{1, \dots, k\} \hookrightarrow \{1, \dots, n\}} \prod_{i=1}^k (u_{f(i)})_{a_i}. \end{gathered} $$

Notice that whenever $k > n$, $\langle\langle u_1, \dots, u_n \rangle\rangle_{[a_1, \dots, a_k]} = 0$.

**Proposition 4.** Let $\mathcal{A}$ be a PCS. The object $!_f \mathcal{A}$ together with the family of morphisms $\rho_{!_f \mathcal{A}, \mathcal{A} \le n} \in \mathrm{Pcoh}(!_f \mathcal{A}, \mathcal{A} \le n)$ for $n \in \mathbb{N}$, constitute the limit of the chain $1 \stackrel{\ell}{\leftarrow} \mathcal{A}^{\le 1} \stackrel{\ell}{\leftarrow} \mathcal{A}^{\le 2} \stackrel{\ell}{\leftarrow} \dots$.

Moreover, this limit commutes with the tensor product (Figure 2).

*Proof.* First, we prove that $\rho_{!_f \mathcal{A}, \mathcal{A} \le m}$ is a correct morphism mapping $\mathrm{P}(!_f \mathcal{A})$ into $\mathrm{P}(\mathcal{A}^{\le m})$, for any $m$. By Lemma 1 it is enough to check that any $\langle\langle u_1, \dots, u_n \rangle\rangle$ is mapped to the pcs $\mathrm{P}(\mathcal{A}^{\le m})$ by $\rho_{!_f \mathcal{A}, \mathcal{A} \le m}$. As $\mathrm{P}(\mathcal{A}^{\le m}) = \mathrm{P}(\mathcal{A}^{\le m})^{\perp\perp}$, it is equivalent to show that for any $n \in \mathbb{N}$, $u_i \in \mathrm{P}(\mathcal{A})$, and $w \in \mathrm{P}(\mathcal{A}^{\le m})^{\perp}$ we have:

$$ \langle \rho_{!_f \mathcal{A}, \mathcal{A} \le m} \langle\langle u_1, \dots, u_n \rangle\rangle, w \rangle \le 1 \qquad (17) $$

Lemma 4 and 5 give us, $\forall N \ge m, n$, resp.: $\iota_{\mathcal{A}^{\le m}, \mathcal{A} \le N} w \in \mathrm{P}(\mathcal{A}^{\le N})^{\perp}$ and $\iota_{\mathcal{A}^{\le m}, \mathcal{A} \le N}^{\mathrm{cor}} \langle u_1, \dots, u_n \rangle \in \mathrm{P}(\mathcal{A}^{\le N})$. Thus the inner product between the two vectors is bounded by 1. Consider then the limit of this product for $N \to \infty$:

$$ \begin{align*} 1 &\ge \lim_{N \to \infty} \langle \iota_{\mathcal{A},n,N}^{\mathrm{cor}} \langle u_1, \dots, u_n \rangle, \iota_{\mathcal{A}^{\le m}, \mathcal{A}^{\le N}} w \rangle \\ &= \langle\langle u_1, \dots, u_n \rangle\rangle, \iota_{\mathcal{A}^{\le m},!_f \mathcal{A}} w \rangle \tag{Eq. (16) and Def. 3} \\ &= \langle \rho_{!_f \mathcal{A}, \mathcal{A}^{\le m}} \langle\langle u_1, \dots, u_n \rangle\rangle, (\rho_{!_f \mathcal{A}, \mathcal{A}^{\le m}} \circ \iota_{\mathcal{A}^{\le m},!_f \mathcal{A}}) w \rangle \\ &= \langle \rho_{!_f \mathcal{A}, \mathcal{A}^{\le m}} \langle\langle u_1, \dots, u_n \rangle\rangle, w \rangle \end{align*} $$

Line 2 gives line 3 using the definition of $\iota$ and $\rho$ in (13).

Now we prove that $!_f \mathcal{A}$ together with its projections $\rho_{!_f \mathcal{A}, \mathcal{A} \le m}$ is indeed a limit cone. As for Proposition 3, we prove straight the commutation with the $\otimes$, as the first part of the statement is a consequence of this latter, taking $\mathcal{B} = 1$.

Take a PCS $\mathcal{C}$ and an $\mathbb{N}$-indexed family of morphisms $f_n \in \mathrm{Pcoh}(\mathcal{C}, \mathcal{A}^{\le n} \otimes \mathcal{B})$ commuting with the chain $\mathcal{B} \stackrel{\ell}{\leftarrow} \mathcal{A}^{\le 1} \stackrel{\ell}{\leftarrow} \mathcal{B} \stackrel{\ell}{\leftarrow} \mathcal{A}^{\le 2} \stackrel{\ell}{\leftarrow} \dots$. We should define
a unique $f^\dagger$ s.t. Figure 2 commutes. The matrix $f^\dagger$ is defined as: $f_{c,(\mu,b)}^\dagger =$ ($f_{\#\mu})_{c,(\mu,b)}$. The fact that $f^\dagger$ is the unique one such that Figure 2 commutes is an easy calculation. We should then prove that it is a morphism in $\mathbf{Pcoh}(\mathcal{C}, !_f \mathcal{A} \otimes \mathcal{B})$, i.e. for every $v \in \mathcal{P}(\mathcal{C})$, $f^\dagger v \in \mathcal{P}(!_f \mathcal{A} \otimes \mathcal{B})$. Since $\mathcal{P}(!_f \mathcal{A} \otimes \mathcal{B}) = \mathcal{P}(!_f \mathcal{A} \otimes \mathcal{B})^{\perp\perp}$, it is equivalent to prove that: $\forall w \in \mathcal{P}(!_f \mathcal{A} \otimes \mathcal{B})^{\perp}$, $\langle f^\dagger v, w \rangle \le 1$.

For any $n$, define $w \downarrow_n \in \mathbb{R}^{|\mathcal{A}^{\le n} \otimes \mathcal{B}|}$ as:

$$ (w \downarrow_n)_{(\mu,b)} = \begin{cases} \frac{n!}{n^k(n-k)!} w_{(\mu,b)} & \text{if } \#\mu = k \le n, \\ 0 & \text{otherwise.} \end{cases} $$

Notice that, for any $\langle u_1, \dots, u_n \rangle \in \mathcal{P}(\mathcal{A}^{\le n})$ and $z \in \mathcal{P}(\mathcal{B})$, we have the inequality: $\langle\langle u_1, \dots, u_n \rangle \otimes z, w \downarrow_n \rangle = \langle\langle u_1, \dots, u_n \rangle \otimes z, w \rangle \le 1$. We conclude that $w \downarrow_n \in \mathcal{P}(\mathcal{A}^{\le n} \otimes \mathcal{B})^{\perp}$, for any $n$. Then we have:

$$ 1 \ge \lim_{n \to \infty} \langle f_n v, w \downarrow_n \rangle = \lim_{n \to \infty} \langle (\rho_{!_f \mathcal{A}, \mathcal{A}^{\le n}} \circ f^\dagger) v, w \downarrow_n \rangle \quad (\text{def } f^\dagger) $$

$$ = \langle f^\dagger v, w \rangle. \qquad (\text{Eq. (16)}) $$

□

Propositions 2, 3 and 4 give the last corollary.

**Corollary 1.** For any $\mathcal{P}\mathcal{C}\mathcal{S} \mathcal{A}$, the $\mathcal{P}\mathcal{C}\mathcal{S} !_f \mathcal{A}$ yields the free commutative comonoid generated by $\mathcal{A}$.

## 4.3 The free and entire exponential modalities are the same.

How do the approximants $\mathcal{A}^{\le n}$ of $!_f \mathcal{A}$ relate with $!_e \mathcal{A}$? Let us consider $\mathcal{A} = \mathbf{Bool}$, and compare the maximal coefficients of these spaces on $[\mathbf{t}, \mathbf{f}]$. It is easy to check that $(\sup!_e \mathbf{Bool})_{[\mathbf{t}, \mathbf{f}]} = (\frac{e_e+e_f}{2})^!_{[\mathbf{t}, \mathbf{f}]} = \frac{1}{4}$. While $(\sup \mathbf{Bool}^{\le n})_{[\mathbf{t}, \mathbf{f}]} = ((e_t^{\lfloor \frac{n}{2} \rfloor}, e_f^{\lfloor \frac{n}{2} \rfloor})_{[\mathbf{t}, \mathbf{f}]}) = ((e_t^{\lfloor \frac{n}{2} \rfloor}, e_f^{\lfloor \frac{n}{2} \rfloor})_{[\mathbf{t}, \mathbf{f}]})$, whose values are, for $n = 2, 3, 4, \dots$ (using Equation (12)): $\frac{1}{2}, \frac{1}{3}, \frac{1}{3}, \frac{3}{10}, \frac{3}{10}, \frac{2}{7}, \dots, \frac{1}{n(n-1)} \lfloor \frac{n}{2} \rfloor \lfloor \frac{n}{2} \rfloor \dots$ converging to $\frac{1}{4}$. This remark can be generalized, showing that the approximants $\mathcal{A}^{\le n}$ are actually approaching to $!_e \mathcal{A}$ from above, giving that their limit is equal to $!_e \mathcal{A}$.

**Proposition 5.** For any $\mathcal{P}\mathcal{C}\mathcal{S} \mathcal{A}$, we have $!_f \mathcal{A} = !_e \mathcal{A}$.

*Proof.* The two spaces have the same web, we prove that $\mathcal{P}(!_f \mathcal{A}) = \mathcal{P}(!_e \mathcal{A})$.

Concerning $\mathcal{P}(!_f \mathcal{A}) \subseteq \mathcal{P}(!_e \mathcal{A})$. Take any $\langle\langle u_1, \dots, u_n \rangle\rangle \in \mathcal{P}(!_f \mathcal{A})$, we have $\langle\langle u_1, \dots, u_n \rangle\rangle \in \mathcal{P}(!_e \mathcal{A})$, because $\langle\langle u_1, \dots, u_n \rangle\rangle \le (\frac{1}{n} \sum_i u_i)^! \in \mathcal{P}(!_e \mathcal{A})$.

Conversely, let $u^n$ denotes $u, \dots, u$ repeated $n$ times in

$$ \langle\langle u^n \rangle\rangle_{[a_1, \dots, a_k]} = \frac{n!}{n^k(n-k)!} \prod_{i=1}^{k} u_{a_i} = \frac{n!}{n^k(n-k)!} u_{[a_1, \dots, a_k]} $$

As for $k < n$, $\frac{n!}{n^k(n-k)!}$ is an increasing sequence converging to 1, we get that $\forall u \in \mathcal{P}(\mathcal{A})$, $\sup_n \langle\langle u^n \rangle\rangle = u^!$. Now, $u^! \in \mathcal{P}(!_f \mathcal{A})$ since it is Scott-closed. Since $u^!$ for $u \in \mathcal{P}(\mathcal{A})$ are generating $\mathcal{P}(!_e \mathcal{A})$, we conclude that $\mathcal{P}(!_e \mathcal{A}) \subseteq \mathcal{P}(!_f \mathcal{A})$. □
Acknowledgments

We thank Sam Staton, Hugh Steele, Lionel Vaux and the anonymous review-
ers for useful comments and discussions. This work has been partly funded by
the French project ANR-14-CE25-0005 Elica and by the French-Chinese project
ANR-11-IS02-0002 and NSFC 61161130530 Locali.

References

1. F. Breuvart and M. Pagani. Modelling Coefficients in the Relational Semantics of Linear Logic. In S. Kreutzer, editor, *Proceedings of the 24th EACSL Annual Conference on Computer Science Logic*, CSL15, Berlin, Germany, LIPICS, 2015.

2. A. Carraro, T. Ehrhard, and A. Salibra. Exponentials with infinite multiplicities. In A. Dawar and H. Veith, editors, *Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings*, volume 6247 of *Lecture Notes in Computer Science*, pages 170–184, 2010.

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

4. T. Ehrhard, M. Pagani, and C. Tasson. Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF. In P. Sewell, editor, *The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL14, San Diego, USA*. ACM, 2014.

5. T. Ehrhard and C. Tasson. Probabilistic call by push value. preprint available at http://arxiv.org/abs/1607.04690, 2016.

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

7. J.-Y. Girard. Linear logic: its syntax and semantics. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, *Advances in Linear Logic*, volume 222 of *London Math. Soc. Lect. Notes Ser.*, pages 1–42, 1995.

8. 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.

9. Y. Lafont. *Logiques, catégories et machines*. PhD thesis, Université Paris 7, 1988.

10. P.-A. Melliès. Categorical semantics of linear logic. *Panoramas et Synthèses*, 27, 2009.

11. P.-A. Melliès, N. Tabareau, and C. Tasson. An explicit formula for the free exponential modality of linear logic. In *Automata, Languages and Programming*, volume 5556 of LNCS, pages 247–260. Springer, 2009.

12. J. van de Wiele. Manuscript. 1987.