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