Cours 19: Probabilistic Coherence Spaces and the $PCoh$ category

Caractérisation des espaces cohérents

𝒜 = (\vert A \vert, \sim_A)

where $\sim_A$ is reflexive and symmetric.

$Cl(𝒜)$: coherent space

Prop: Giving a coherent space is equivalent to giving

(\vert 𝒜 \vert, C(𝒜))

s.t.

C(𝒜) ⊆ 𝒫(\vert A \vert) and

  1. ∀a ∈ \vert A \vert, ∃x ∈ C(𝒜); a ∈ x
  2. C(𝒜) = (C(𝒜)^{⊥})^{⊥}

where the orthogonal $X^⊥$ of a set $X ⊆ 𝒫(\vert A \vert)$ is given by:

X^⊥ ≝ \lbrace y ∈ 𝒫(\vert A \vert) \mid ∀x ∈ X, card(x ∩ y) ≤ 1\rbrace

NB:

  • Les espaces cohérents ont été introduits par comme une sémantique stable.

  • Fonction stables (VS Scott-continues) ⟶ pour tout morceau d’information dans l’output, il y a une unique information minimale qui génère ce morceau.

  • we always have: X ⊆ (X^⊥)^⊥

Proof:

  • if $(\vert A \vert, \sim_A)$ is a coherent space, then $Cl(A)$ enjoys both of the properties

    • 1: reflexivity of $\sim_A$
    • 2: we claim that Cl(A)^⊥ = Cl(A^⊥)

      where $A^⊥$ is the complementary graph (coherent elements are exactly those which weren’t initially)

      Then (Cl(A)^⊥)^⊥ = Cl((A^⊥)^⊥) = Cl(A)

Lemma: Cl(A)^⊥ = Cl(A^⊥)

Indeed:

\begin{align*} y ∈ Cl(A)^⊥ & ⟺ ∀x ∈ Cl(A), card(y ∩ x) ≤ 1 \\ & ⟺ ∀x ∈ Cl(A), ∀ \lbrace a, a' \rbrace ⊆ y, \lbrace a, a' \rbrace ⟹ a = a'\\ & ⟺ ∀ \lbrace a, a' \rbrace ∈ Cl(A), \lbrace a, a' \rbrace ⊆ y ⟹ a = a' &&\text{ ⟸ comes from the fact that cliques are bottom-closed}\\ &⟺ ∀ \lbrace a, a' \rbrace ⊆ y, a \sim_{A^⊥} a'\\ &⟺ y ∈ Cl(A^⊥) \end{align*}

Secondly:

  • if $(\vert A \vert, X)$ s.t. 1 and 2 hold, then there exists a reflexive and symmetric $\sim_A$ s.t. $X = Cl(𝒜)$

    • We set $a \sim_A a’$ iff $\lbrace a, a’ \rbrace ∈ x$

      • $a \sim_A a$ since:

        ∀y ∈ X^⊥, card(\lbrace a \rbrace ∩ y) ≤ 1

        so

        \lbrace a \rbrace ∈ (X^⊥)^⊥
      • $a \sim_A a’ ⟹ a’ \sim_A a$: trivial

    • Now, we prove that: X = Cl_{\sim_A}(A)

      \begin{align*} x ∈ X & ⟺ x ∈ (X^⊥)^⊥ \\ & ⟺ ∀y ∈ X^⊥, \; card(x ∩ y) ≤ 1 \\ & ⟺ ∀y ∈ X^⊥, \; ∀ \lbrace a, a' \rbrace ⊆ x, \; card(y ∩ \lbrace a, a' \rbrace) ≤ 1\\ & ⟺ ∀ \lbrace a, a' \rbrace ⊆ x, ∀y ∈ X^⊥, \; \; card(y ∩ \lbrace a, a' \rbrace) ≤ 1\\ & ⟺ ∀ \lbrace a, a' \rbrace ⊆ x, \lbrace a, a' \rbrace ∈ (X^⊥)^⊥ = X\\ & ⟺ ∀ \lbrace a, a' \rbrace ⊆ x, \, a \sim_A a'\\ & ⟺ x ∈ Cl_{\sim_A}(A) \end{align*}

NB: Donc on a une définition purement algébrique qui ne parle plus de relation de cohérence !

De plus :

𝒫(\vert A \vert) ≃ \lbrace 0, 1 \rbrace^{\vert A \vert}
card(x ∩ y) ≤ 1 ⟺ \Big(\sum\limits_{ a ∈ \vert A \vert } (a ∈ x) ∧ (a ∈ y)\Big) ≤ 1

Probabilistic Coherence Spaces

On va généraliser l’observation précédente :

  • les booléens sont remplacés par des scalaires
  • \sum\limits_{ a ∈ \vert A \vert } (a ∈ x) ∧ (a ∈ y) = ⟨x, y⟩
A Probabilistic Coherence Space:

is a 𝒜 ≝ (\underbrace{\vert 𝒜 \vert)}_{\text{countable set: } web}, \underbrace{P(𝒜)}_{⊆ (ℝ^+)^{\vert 𝒜 \vert}}) s.t.

  1. ∀a ∈ \vert A \vert, ∃x ∈ P(𝒜); x_a > 0
  2. ∀a ∈ \vert A \vert, ∃λ ∈ ℝ^+, \, ∀x ∈ P(𝒜), \, x_a < λ
  3. P(A) = (P(A)^⊥)^⊥

where the orthogonal $X^⊥$ of a set $X ⊆ (ℝ^+)^{\vert 𝒜 \vert}$ is given by:

X^⊥ ≝ \lbrace y ∈ (ℝ^+)^{\vert 𝒜 \vert} \mid ∀x ∈ X, \underbrace{⟨x, y⟩}_{≝ \; \sum\limits_{ a ∈ \vert 𝒜 \vert } x_a y_a } ≤ 1\rbrace

NB:

  • 1 and 2 are dual conditions: a space satisfies 1 iff its dual satisfies 2.

  • $(ℝ^+)^{\vert 𝒜 \vert}$ est un semi-module car $ℝ^+$ est un semi-anneau

  • $(ℝ^+)^{\vert 𝒜 \vert}$ est ordonné point par point (pointwise)

Scott-closure and Convexity

$X ⊆ (ℝ^+)^{\vert 𝒜 \vert}$ is Scott-closed whenever:
  • ∀ x \underbrace{≤}_{\text{pointwise}} y ∈ X, \; x ∈ X
  • if $D ⊆ X$ is directed, then $\sup D ∈ X$

NB: Scott-closed condition: for recursion

$X$ is convex:

iff for all $x, y ∈ X$, for all $λ ∈ [0, 1]$, λx + (1-λ) y ∈ X

Th: Given $(\vert 𝒜 \vert, 𝒳 ⊆ (ℝ^+)^{\vert 𝒜 \vert})$ s.t. 1. and 2. hold for $𝒳$, we have that:

(𝒳^⊥)^⊥ = 𝒳 ⟺ 𝒳 \text{ is Scott-closed and convex}

Proof:

⟹:

Let’s show that $𝒫(𝒜)$ is Scott-closed and convex.

Bottom-closed: if $x ≤ y ∈ P(𝒜)$, let’s show that $x ∈ P(𝒜) = (P(𝒜)^⊥)^⊥$, i.e.:

∀z ∈ P(𝒜)^⊥, \; ⟨x, z⟩ ≤ 1

And as $x ≤ y$ (and all coefficients are positive):

⟨x, z⟩ ≤ ⟨y, z⟩

And since $y ∈ P(𝒜), z ∈ P(𝒜)^⊥$:

⟨y, z⟩ ≤ 1

Closed by $\sup$: Let $D$ a directed set $⊆ P(𝒜)$.

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

Let’s show that

\sup D ∈ P(𝒜) = (P(𝒜)^⊥)^⊥

i.e.

∀z ∈ P(𝒜)^⊥, \, ⟨\sup D, z⟩ ≤ 1

Let $z ∈ P(𝒜)^⊥$.

\begin{align*} \sum\limits_{ a } (\sup_{x ∈ D} x_a) z_a ≤ 1 & ⟺ \sup_{x ∈ D} \left(\sum\limits_{ a } x_a z_a\right) ≤ 1 \\ & ⟺ \sup_{x ∈ D} ⟨x, z⟩ ≤ 1\\ & ⟸ ∀x ∈ D ⊆ P(𝒜), ⟨x, z⟩ ≤ 1\\ \end{align*}

Because

\sum\limits_{ a } \sup_{x ∈ D} (x_a z_a) = \sup_{x ∈ D} \left(\sum\limits_{ a } (x_a z_a) \right)
  • $≥$ comes from the fact that \sum\limits_{ a } \sup_{x ∈ D} (x_a z_a) ≥ \sum\limits_{ a } x_a z_a

  • $≤$: to do

Convexity: $x, y ∈ P(𝒜), \; λ ∈ [0, 1]$.

λx + (1-λ)y \overset{?}{∈} P(𝒜) = (P(𝒜)^⊥)^⊥

i.e.

∀z ∈ P(𝒜)^⊥, ⟨λx + (1-λ)y, z⟩ ≤ 1

It’s clear, since

  • $∀z ∈ P(𝒜)^⊥, λ ⟨x, z⟩ ≤ 1$
  • $∀z ∈ P(𝒜)^⊥, (1-λ) ⟨y, z⟩ ≤ 1$

⟸ is far more nettlesome: to show $(X^⊥)^⊥ ⊆ X$, we show by contrapositive

x ∉ X ⟹ x ∉ (X^⊥)^⊥

by showing

x ∉ X ⟹ ∃y ∈ X^⊥, ⟨x, y⟩ > 1

with Hahn-Banach

cf.

  • Girard: “Between logic and quantic: a tract”
  • Danos, Ehrhard: “On probabilistic coherence spaces” (for models of linear logic)

NB:

  • previously: a clique was seen as a program (here: probabilistic program)

  • here: $x ∈ (ℝ^+)^{\vert 𝒜 \vert}$ is seen as a probabilistic program

  • $(ℝ^+)^{\vert 𝒜 \vert}$ ensures that the series $⟨x, y⟩$ either converges absolutely or diverge to $+∞$

  • why aren’t the vectors in $[0, 1]^{\vert 𝒜 \vert}$? If you consider $Bool ⇒ Unit$, you’ll have very high coefficients.

  • probability theory comes in when we study the interactions of a program and its dual

The Probabilistic Coherence Space Category: $PCoh$

  • 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 } f_{a, b} x_a

NB:

  • if $\vert A \vert$ and $\vert B \vert$, are finite, the Scott-continuity comes with the linearity.
  • it gives a model of Linear Logic

Leave a comment