# 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.

Since $I$ is finite and $D$ directed, we have:

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

and we have an $x β D$ s.t.

Therefore:

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} β β_+

$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)^β₯$:

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

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

Tags:

Updated: