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

Leave a comment