# Cours 20: Probabilistic Coherence Spaces and Linear Logic

## In Probabilistic Coherence Spaces, $𝒫(𝒜)$ is closed under $\sup$

Let $𝒜 ≝ (\vert 𝒜 \vert, 𝒫(𝒜) ⊆ ℝ_+^{\vert 𝒜 \vert})$ be a probabilistic coherence space

Recall that

• $𝒫(𝒜) = (𝒫(𝒜)^⊥)^⊥$
• $𝒫(𝒜)$ is ordered pointwise

If $D ⊆ 𝒫(𝒜)$ is directed, then

$\sup D ∈ 𝒫(𝒜)$

NB: $(\sup D)_a ≝ \sup_{x ∈ D} x_a$

Let $z ≝ \sup D$. Let’s show that $\sup D ∈ (𝒫(𝒜)^⊥)^⊥$.

$∀y ∈ 𝒫(𝒜)^⊥, \; ⟨z, y⟩ \overset{?}{≤} 1$

Note that $\sup_{x ∈ D} ⟨x, y⟩ ≤ 1$

We want $⟨z, y⟩ \overset{?}{≤} \sup_{x ∈ D} ⟨x, y⟩$

It suffices to show that

$∀ ε > 0, ∃ x ∈ D; ⟨z, y⟩ - ε ≤ ⟨x, y⟩$

Let $ε > 0$. There exists $I ⊆_{fin} \vert 𝒜 \vert$ s.t.

$⟨z_{\mid I}, y⟩ ≥ ⟨z, y⟩ - ε/2$

Since $I$ is finite and $D$ directed, we have:

$⟨z_{\mid I}, y⟩ = \sup_{x ∈ D} ⟨x_{\mid I}, y⟩$

Indeed:

• $≥$ is clear by, since the inequality stands for all $x$

• $≤$:

$⟨z_{\mid I}, y⟩ = (\sup_{x_0∈D} x_0 y_0) + ⋯ + (\sup_{x_n∈D} x_n y_n) = \sup_{(x_0, ⋯, x_n) ∈ D^{n+1}} (x_0 y_0 + ⋯ + x_n y_n)$

But as $D$ is directed, there exists $D \ni \bar{x} ≥ x_0, ⋯, x_n$

So for all $x_0, ⋯, x_n$:

$x_0 y_0 + ⋯ + x_n y_n ≤ ⟨\bar{x}_{\mid I}, y⟩ ≤ \sup_{x ∈ D} ⟨x_{\mid I}, y⟩$

So

$⟨z_{\mid I}, y⟩ = \sup_{x ∈ D} ⟨x_{\mid I}, y⟩$

and we have an $x ∈ D$ s.t.

$⟨x_{\mid I}, y⟩ ≥ ⟨z_{\mid I}, y⟩ - ε/2$

Therefore:

$⟨x, y⟩ ≥ ⟨x_{\mid I}, y⟩ ≥ ⟨z_{\mid I}, y⟩ - ε/2 ≥ ⟨z, y⟩ - ε/2$

NB: Giving $𝒫(𝒜)$ corresponds to giving a norm Scott-continuous, and $𝒫(𝒜)$ is the unit ball for this norm.

Probabilistic Coherence Spaces (PCS) are really similar to Banach spaces: there are cones (semi-modules) equipped with a norm and the ball of this norm. In this setting, $f$ is continues wrt to the Scott topology (induced by the order), and not the topology induced by the norm (too strong).

# Category of Probabilistic Coherence Spaces

• Objects are Probabilistic Coherence Spaces

• Morphisms: $f: A ⟶ B$ is a Scott-continuous linear function which preserves the cliques:

$f ⊆ (ℝ^+)^{\vert A \vert × \vert B \vert}$

s.t.

$∀x ∈ P(A), \; f(x) ∈ P(B)$

where

$f(x)_b ≝ \sum\limits_{ a ∈ \vert 𝒜 \vert } f_{a, b} x_a$

If $A \overset{f}{⟶} B \overset{g}{⟶} C$:

Let’s show that

$(f; g)_{a, c} ≝ \sum\limits_{ b ∈ \vert B \vert } f_{a, b} \cdot g_{b, c}$ is well-defined, i.e.

$(f; g)_{a, c} ∈ ℝ_+$

Proof:

Lemma: $∀a ∈ \vert A \vert, ∃ λ_a > 0; λ_a e_a ∈ 𝒫(A)$

NB: $e_a$ is the vector whose coordinates are all $0$ except the coordinate corresponding to $a$, which is equal to $1$

Indeed: $∀a ∈ \vert A \vert, ∃x ∈ 𝒫(A); x_a > 0$ and $𝒫(A)$ is bottom-closed, so for a small enough $λ_a$, $λ_a e_a ≤ x_a$.

So there exist

• $λ_a e_a ∈ 𝒫(A)$
• $λ_c’ e_c ∈ 𝒫(C^⊥)$
$(f;g)(λ_a e_a) = \underbrace{g(\underbrace{f(λ_a e_a)}_{∈ 𝒫(B)})}_{∈ 𝒫(C)}$

So

$⟨(f;g)(λ_a e_a), λ_c' e_c⟩ ≤ 1$

But

$1 ≥ ⟨(f;g)(λ_a e_a), λ_c' e_c⟩ = \sum\limits_{ c' ∈ \vert C \vert } (f;g)(λ_a e_a)_{c'} (λ_c' e_c)_{c'} = λ_c' (f;g)(λ_a e_a)_c\\ = λ_c' \left(\sum\limits_{ a' ∈ \vert A \vert } (f; g)_{a', c} (λ_a e_a)_{a'} \right) \\ = λ_c' λ_a (f; g)_{a, c}$

So

$(f; g)_{a, c} ∈ ℝ_+$

$A^⊥$:

• $\vert A^⊥ \vert = \vert A \vert$
• $𝒫(A^⊥) ≝ 𝒫(A)^⊥$
1. Covering: $∀a ∈ \vert A \vert, ∃x ∈ 𝒫(A^⊥); x_a > 0$

• we know that we have the bounded property $∃λ_a > 0; ∀x ∈ 𝒫(A), x_a ≤ λ_a$

Let $c(a) ≝ \sup_{x ∈ 𝒫(A)} x_a > 0$.

Let’s show that

$\frac{1}{c(a)} e_a \overset{?}{∈} 𝒫(A^⊥) = 𝒫(A)^⊥$

For $x ∈ 𝒫(A)$,

$⟨\frac{1}{c(a)} e_a, x⟩ = \frac{1}{c_a} x_a ≤ 1$
2. Dual condition: $∀a ∈ \vert A \vert, ∃ λ' > 0, ∀x' ∈ 𝒫(A^⊥), x_a' ≤ λ'$

By 1. on $𝒫(A)$, there exists $x ∈ 𝒫(A)$ s.t. $x_a > 0$

Let $λ’ ≝ \frac{1}{x_a}$.

We have that $∀ x’ ∈ 𝒫(A^⊥)= 𝒫(A)^⊥$:

$⟨x', x⟩ ≤ 1$

But $x_a’ x_a$ is one of the term of $⟨x’, x⟩$ ⟹ we must have $x_a’ x_a ≤ 1$

### Dual of a morphism

If $f: A ⟶ B$,

$f^⊥= B^⊥ ⟶ A^⊥$

is defined as:

$(f^⊥)_{b, a} = f_{a, b}$

### Properties of the dual

If $X ⊆ ℝ_+^{\vert A \vert}$

Recall that

$X^⊥ ≝ \lbrace y ∈ ℝ_+^{\vert A \vert} \mid ∀x ∈ X, ⟨x, y⟩≤ 1 \rbrace$

On can easily show that

1. $X ⊆ (X^⊥)^⊥$
2. $X ⊆ Y ⟹ Y^⊥ ⊆ X^⊥$
3. $((X^⊥)^⊥)^⊥ = X^⊥$
• $((X^⊥)^⊥)^⊥ \overset{?}{⊆} X^⊥$ by applying 1. and 2.

NB: it’s also called “orthogonal”, but this is not a good terminology, as it’s not really an orthogonal as in linear algebra.

## Tensor product Bifunctor of the Monoidal Category

### Action on the objects

$A \otimes B$:

• $\vert A \otimes B \vert = \vert A \vert × \vert B \vert$
• $𝒫(A \otimes B) = \lbrace \underbrace{x \otimes y}_{(x \otimes y)_{a, b} \; ≝ \; x_a \cdot y_b} ∈ ℝ_+^{\vert A \vert × \vert B \vert} \mid x ∈ 𝒫(A), y ∈ 𝒫(B) \rbrace$

### Action on morphisms

If $f: A ⟶ B, \; g: C ⟶ D$.

Let’s construct $f \otimes g: A \otimes C ⟶ B \otimes D$:

$(f \otimes g)_{(a,c), (b, d)} = f_{a,b} \cdot g_{c, d}$

Furthermore:

$∀z ∈ 𝒫(A \otimes C), \; (f \otimes g)(z) ∈ 𝒫(B \otimes D)$

i.e.

$∀x ∈ 𝒫(A), y ∈ 𝒫(C), \;\underbrace{ (f \otimes g)(x \otimes y)}_{= f(x) \otimes g(y)} ∈ 𝒫(B \otimes D)$

## Closure of the Monoidal Category

$A \multimap B$:

• $\vert A \multimap B \vert = \vert A \vert × \vert B \vert$
• $𝒫(A \multimap B) = \lbrace f ∈ ℝ_+^{\vert A \vert × \vert B \vert} \mid ∀x ∈ 𝒫(A), f(x) ∈ 𝒫(B)\rbrace$

NB: $A ⇒ B ≝ !A \multimap B$

these are not linear functions anymore, but analytical functions (series).

$𝒫(A \multimap B) = 𝒫(A \otimes B^⊥)^⊥$
$A \multimap B = A^⊥ ⅋ B$

and we use

$⟨f, \underbrace{x}_{∈ 𝒫(A)} \otimes \underbrace{y'}_{∈ 𝒫(B)^⊥}⟩ = ⟨f(x), y'⟩$

Proof:

$⟨f, x \otimes y'⟩ = \sum\limits_{ (a, b) ∈ \vert A \vert × \vert B \vert } f_{a, b} (x \otimes y')_{(a, b)} \\ = \sum\limits_{ a ∈ \vert A \vert, b ∈ \vert B \vert } f_{a, b} x_a y'_b = \sum\limits_{b ∈ \vert B \vert} \underbrace{\left(\sum\limits_{ a ∈ \vert A \vert } f_{a, b} x_a \right)}_{= f(x)_b} y'_b = ⟨f(x), y'⟩$
$eval: A \otimes (A \multimap B) \leadsto B$ $eval_{(a, (a', b)), b'} = δ_{a, a'} δ_{b, b'}$

NB:

• $eval$ is a trace in the sense of coherence spaces
• all the “base” morphisms (like $eval$, contraction, etc…) have coefficients in $0$ and $1$.

Correctness of the definition:

$∀ x ∈ 𝒫(A), ∀ f ∈ 𝒫(A \multimap B), \; \underbrace{eval(x \otimes f)}_{= \, f(x)} ∈ 𝒫(B)$ $\begin{xy} \xymatrix{ A \otimes (A \multimap B) \ar[r]^{eval} & B \\ A \otimes C \ar@{.>}[u]^{id × λ(f)} \ar[ur]_f & } \end{xy}$

The only possible $λ$ morphism is

$λ(f)_{c, (a,b)} ≝ f_{(c,a), b}$

## Cartesian product

• $\vert A \, \& \, B \vert = \vert A \vert \sqcup \vert B \vert$
• $𝒫(A \, \& \, B) = \lbrace x \& y \mid x ∈ 𝒫(A), y ∈ 𝒫(B) \rbrace$

where the pairing $x \& y$ is defined as:

$∀c ∈ \vert A \vert \sqcup \vert B \vert, \; (x \& y)_{c} ≝ \begin{cases} x_c &&\text{ if } c ∈ \vert A \vert \\ y_c &&\text{ else if } c∈ \vert B \vert \end{cases}$

So that:

$𝒫(A \, \& \, B) = \left(\lbrace x \& 0 \mid x ∈ 𝒫(A)^⊥ \rbrace ∪ \lbrace 0 \& y \mid y ∈ 𝒫(B)^⊥ \rbrace \right)^⊥\\ = \left(𝒫(A)^⊥ \oplus 0 ∪ 0 \oplus 𝒫(B)^⊥\right)^⊥ = P(A^⊥ \oplus B^⊥)^⊥$

NB:

• $𝒫(A \& B)$ is the unit ball of for the norm

$\Vert x \& y \Vert ≝ \max (\Vert x \Vert, \Vert y \Vert)$
• $𝒫(A^⊥ \oplus B^⊥)$ is the unit ball of for the norm

$\Vert x \& y \Vert ≝ \Vert x \Vert + \Vert y \Vert$
• $(A \& B)^⊥ = A^⊥ \oplus B^⊥$

“On probabilistic coherence spaces” Danos/Ehrhard

Roberto DiCosmo MPRI

Tags:

Updated: