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