# 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

Tags:

Updated: