# 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} ∈ ℝ_+

# Link with Linear Logic

$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: