Coherent space

In proof theory, a coherent space (also coherence space) is a concept introduced in the semantic study of linear logic.

In Proofs and Types, coherent spaces are called coherence spaces. A footnote explains that although in the French original they were "espaces cohérents", the translation used "coherence space", because spectral spaces are sometimes called "coherent spaces".

Definitions

There are several equivalent definitions of a coherent space.

As a family of subsets

The original definition by Jean-Yves Girard is a family of sets $𝒜$, satisfying the following closure conditions:

• Down-closure: if $a\in 𝒜$ and $a^{\prime }\subseteq a$, then $a^{\prime }\in 𝒜$.
• Binary completeness: for every $M\subseteq 𝒜$, if $a_1\cup a_2\in 𝒜$ for all $a_1,a_2\in M$, then $\bigcup M\in 𝒜$.

The elements of the sets in $𝒜$ are tokens. The set of tokens is$$|𝒜|=\bigcup 𝒜=\{\alpha \mid \{\alpha \}\in 𝒜\}.$$We say that each $a\in A$ is a coherent set of tokens. If a set $X$ is given in advance, and the elements of $𝒜$ are presented as subsets of $X$, then one also requires $\{\alpha \}\in 𝒜$ for every $\alpha \in X$. This intuitively states that any token is coherent at least to itself.

Given such a family, one obtains a reflexive, symmetric relation $\sim$ on $|𝒜|$, called coherence modulo $𝒜$, by setting$$\alpha \sim \beta \text{if and only if}\{\alpha ,\beta \}\in 𝒜.$$The elements of $𝒜$ are then precisely the subsets of $|𝒜|$ whose elements are pairwise related by $\sim$.

As a family of maximally coherent subsets

The coherent sets are partially ordered under inclusion. By binary completeness and Zorn's lemma, any coherent set is contained in a maximally coherent set. Consequently, it is only necessary to specify the maximally coherent sets, ${𝒜}_{max}$, then perform a down-closure:$$𝒜=\{a:\mathrm{\exists }{a}^{\prime }\in {𝒜}_{max},a^{\prime }\supset a\}$$The only condition on ${𝒜}_{max}$ is that any two $a,a^{\prime }\in {𝒜}_{max}$, if they are distinct, then neither contains the other.

As an undirected graph

Coherence spaces are in bijection with undirected graphs whose vertices are tokens.

Given a coherence space $𝒜$, its associated graph, called the web of $𝒜$, has vertex set $|𝒜|$. Its edges are the unordered pairs $\{\alpha ,\beta \}$ such that $\alpha \sim \beta$. Note that we require each vertex to have a self-edge purely as a convenient convention.

Conversely, given an undirected graph $(|𝒜|,E)$ where each vertex has a self-edge, one obtains a coherence space by taking $𝒜$ to be the family of all cliques of the graph:$$𝒜=\{a\subseteq |𝒜|\mid \mathrm{\forall }\alpha ,\beta \in a,\{\alpha ,\beta \}\in E\}.$$That is, the elements of $𝒜$ are the sets of vertices whose elements are pairwise adjacent.

As a biorthogonally closed family

Let $|𝒜|$ be a set of tokens. Two subsets $a,b\subseteq |𝒜|$ are said to be orthogonal, (or polar), if $a\cap b$ is either empty or a singleton. We write this as $a\perp b$.

For a family $𝒜\subseteq 𝒫(|𝒜|)$, its dual is the family$${𝒜}^{\perp }=\{a\subseteq |𝒜|\mid \mathrm{\forall }b\in 𝒜,a\perp b\}.$$A coherence space is a family $𝒜\subseteq 𝒫(|𝒜|)$ satisfying$$𝒜=({𝒜}^{\perp }{)}^{\perp }.$$That is, it is a family that is biorthogonally closed under polarity.

Stable functions

The coherent spaces make up a category $𝐂𝐨𝐡$. Each object is a coherent space, and each morphism $f:𝒜\to ℬ$ is a stable function.

Definition

A stable function is defined as a function mapping cliques to cliques:$$f:𝒜\to ℬ$$such that it is

• continuous: If $\{a_i{\}}_i\subset 𝒜$ is a directed family, then $f({\cup }_i{a}_i)={\cup }_{i}f(a_i)$.
• stable: If $a,a^{\prime }\in 𝒜$ such that $a\cup a^{\prime }\in 𝒜$, then $f(a\cap a^{\prime })=f(a)\cap f(a^{\prime })$.

By stability, if $a\subset a^{\prime }\in 𝒜$ then $f(a)\subset f(a^{\prime })$, so $f$ is monotonic.

By stability, $f(a)={\cup }_{a^{\prime }\subset a,a^{\prime }\text{ is finite}}f(a^{\prime })$. So it shows that $f$ is determined by its value on finite coherent sets.

For continuity, considering the special case where $\{a_i{\}}_i\subset 𝒜$ is the empty set, we have $f(\mathrm{\varnothing })=\mathrm{\varnothing }$.

Trace

Given a stable function, its trace $Tr(f)\subset 𝒜\times |ℬ|$ is defined as$$Tr(f):=\{(a,\beta )|a\in 𝒜,\beta \in f(a),(\mathrm{\forall }{a}^{\prime }⊊a,\beta \in ̸f(a^{\prime }))\}$$That is, each $(a,\beta )\in Tr(f)$ is such that $a$ is a minimal coherent set needed to produce token $\beta$. By stability, any $(a,\beta )\in Tr(f)$ must have a finite $a$.

Conversely, each stable function is determined by its trace:$$f(a)=\{\beta :(a^{\prime },\beta )\in Tr(f),a^{\prime }\subset a\}$$

Linearity

A stable function $f$ is linear iff any $(a,\beta )\in Tr(f)$, $a$ has just one element. This was the original motivation for linear logic.

Linear stable functions are particularly simple and can be thought of as a clique-valued function $f:|𝒜|\to ℬ$ such that given a clique $a\in 𝒜$, ${\cup }_{\alpha \in a}f(\alpha )$ is still a clique in $ℬ$.

Examples

The intuition of a coherent space is that each token is a trait that an object might possess, and a coherent set of tokens is a set of traits that is possessed by some object simultaneously. There is no object that can possess an incoherent set of tokens as its traits. One explores an object by observing more and more of its traits. The set of observed traits grows, but will always remain coherent.

Categorical constructions

Any coherent space can be specified by its maximally coherent sets. Any union of two distinct maximally coherent sets is incoherent.

Given a coherent space $𝒜$, its polar ${𝒜}^{\perp }$ is still a coherent space. This is a dual object construction in category theory.

Given any set $X$, we have the discrete/minimal coherent space $\{\{\alpha \}:\alpha \in X\}$, and the indiscrete/maximal coherent space $𝒫(X)$.

Given two coherent spaces $𝒜,ℬ$, there is a coherent space $𝒜\mathrm{\&}ℬ$ (pronounced "A and B"). It is defined as a graph. The set of tokens is the disjoint union of the two sets of tokens:$$|𝒜\mathrm{\&}ℬ|=|𝒜|+|ℬ|$$and the edges of $𝒜\mathrm{\&}ℬ$ is the union of the edges in $𝒜$, the edges in $ℬ$, and $\{\{\alpha ,\beta \}:\alpha \in 𝒜,\beta \in ℬ\}$. More generally, given a family of coherent spaces, $\{{𝒜}_i{\}}_{i\in I}$, we can define ${\mathrm{\&}}_{i\in I}{𝒜}_i$ similarly.

Given two coherent spaces $𝒜,ℬ$, there is a coherent space $𝒜\bigsqcup ℬ$. The set of tokens is still$$|𝒜\bigsqcup ℬ|=|𝒜|+|ℬ|$$ and the edges of $𝒜\bigsqcup ℬ$ is the union of the edges in $𝒜$, the edges in $ℬ$. This is the coproduct. This can be defined in general for a family of coherent spaces, $\{{𝒜}_i{\}}_{i\in I}$.

Coherent space of stable functions

Given two sets $X,Y$, the set of partial functions of type $X\to Y$ can be modelled by a coherent space. The token set is $X\times Y$, and the edges are $\{(x,y),(x^{\prime },y^{\prime })\}$ for all $x\ne x^{\prime }$. Equivalently, for each $x\in X$, define ${𝒴}_x$ to be the discrete/minimal coherent space of $Y$. Then ${\mathrm{\&}}_{x\in X}{𝒴}_x$ is the coherent space that we constructed.

This can be intuitively understood as follows: a partial function $f:X\to Y$ has the set of traits $\{(x,f(x)):x\in X\wedge f(x)\text{ is defined}\}$. A maximally coherent set is the set of traits of a total function. As we enumerate the values of a partial function, we enumerate the set of traits, which is coherent at every step. This is useful when $f$ is computed by a Turing machine that might fail to halt on some entries. If $f(x)$ does not halt, then we simply never observe the trait during trait-enumeration. The set of observed traits will remain coherent at all steps of our enumeration.

Now, define $𝒳,𝒴$ to be the discrete/minimal coherent spaces. Then $f:𝒳\to 𝒴$ is a stable function iff there is a partial function $f^{\prime }:X\to Y$, such that$$f(\{x\})=\{\begin{array}{cc}\{f^{\prime }(x)\}& \text{ if }{f}^{\prime }(x)\text{ is defined,}\\ \mathrm{\varnothing }& \text{ else}\end{array}$$and $f^{\prime }$ can be identified with its set of traits, which is a coherent set in ${\mathrm{\&}}_{x\in X}{𝒴}_x$. Thus, ${\mathrm{H}\mathrm{o}\mathrm{m}}_{𝐂𝐨𝐡}(𝒳,𝒴)\simeq {\mathrm{\&}}_{x\in X}{𝒴}_x$ is a coherent space.

In general, we have a functor $\Rightarrow :{𝐂𝐨𝐡}^2\to 𝐂𝐨𝐡$, contravariant in the first argument and covariant in the second argument, such that$${\mathrm{H}\mathrm{o}\mathrm{m}}_{𝐂𝐨𝐡}(𝒜,ℬ)\simeq 𝒜\Rightarrow ℬ$$That is, given any two coherent spaces $𝒜,ℬ$, the hom-set between them is structured as a coherent space as well. This makes the category enriched over itself.

The token set $|𝒜\Rightarrow ℬ|$ is ${𝒜}_{\text{fin}}\times |ℬ|$, where ${𝒜}_{\text{fin}}$ is the set of nonempty finite coherent sets in $𝒜$. Two tokens $(a,\beta ),(a^{\prime },{\beta }^{\prime })$ are coherent iff

• If $a\cup a^{\prime }\in 𝒜$, then $\{\beta ,{\beta }^{\prime }\}\in ℬ$.
• If $a\cup a^{\prime }\in 𝒜$ and $a\ne a^{\prime }$, then $\beta \ne {\beta }^{\prime }$.

Note that, if $a\cup a^{\prime }\in ̸𝒜$, then $(a,\beta ),(a^{\prime },{\beta }^{\prime })$ for any $\beta ,{\beta }^{\prime }\in |ℬ|$. That is, we only demand coherence in $ℬ$ given coherence in $𝒜$. If there is no coherence in $𝒜$, then we make no demands on coherence in $ℬ$.

Coherence spaces as types

Coherence spaces can act as an interpretation for types in type theory where points of a type $𝒜$ are points of the coherence space $𝒜$. This allows for some structure to be discussed on types. For instance, each term $a$ of a type $𝒜$ can be given a set of finite approximations $I$ which is in fact, a directed set with the subset relation. With $a$ being a coherent subset of the token space $|𝒜|$ (i.e. an element of $𝒜$), any element of $I$ is a finite subset of $a$ and therefore also coherent, and we have $a=\bigcup a_i,a_i\in I.$

Stable functions

Functions between types $𝒜\to ℬ$ are seen as stable functions between coherence spaces. A stable function is defined to be one which respects approximants and satisfies a certain stability axiom. Formally, $F:𝒜\to ℬ$ is a stable function when

1. It is monotone with respect to the subset order (respects approximation, categorically, is a functor over the poset $𝒜$): $a^{\prime }\subset a\in 𝒜⟹F(a^{\prime })\subset F(a).$
2. It is continuous (categorically, preserves filtered colimits): $F({\bigcup }_{i\in I}^{\uparrow }{a}_i)={\bigcup }_{i\in I}^{\uparrow }F(a_i)$ where ${\bigcup }_{i\in I}^{\uparrow }$ is the directed union over $I$, the set of finite approximants of $a$.
3. It is stable: $a_1\cup a_2\in 𝒜⟹F(a_1\cap a_2)=F(a_1)\cap F(a_2).$ Categorically, this means that it preserves the pullback:

   

Product space

In order to be considered stable, functions of two arguments must satisfy the criterion 3 above in this form: $$a_1\cup a_2\in 𝒜\wedge b_1\cup b_2\in ℬ⟹F(a_1\cap a_2,b_1\cap b_2)=F(a_1,b_1)\cap F(a_2,b_2)$$which would mean that in addition to stability in each argument alone, the pullback

is preserved with stable functions of two arguments. This leads to the definition of a product space $𝒜\mathrm{\&}ℬ$ which makes a bijection between stable binary functions (functions of two arguments) and stable unary functions (one argument) over the product space. The product coherence space is a product in the categorical sense i.e. it satisfies the universal property for products. It is defined by the equations:

• $|𝒜\mathrm{\&}ℬ|=|𝒜|+|ℬ|=(\{1\}\times |𝒜|)\cup (\{2\}\times |ℬ|)$ (i.e. the set of tokens of $𝒜\mathrm{\&}ℬ$ is the coproduct (or disjoint union) of the token sets of $𝒜$ and $ℬ$.
• Tokens from differents sets are always coherent and tokens from the same set are coherent exactly when they are coherent in that set.
  • $(1,\alpha ){\sim }_{𝒜\mathrm{\&}ℬ}(1,{\alpha }^{\prime })⟺\alpha {\sim }_{𝒜}{\alpha }^{\prime }$
  • $(2,\beta ){\sim }_{𝒜\mathrm{\&}ℬ}(2,{\beta }^{\prime })⟺\beta {\sim }_{ℬ}{\beta }^{\prime }$
  • $(1,\alpha ){\sim }_{𝒜\mathrm{\&}ℬ}(2,\beta ),\mathrm{\forall }\alpha \in |𝒜|,\beta \in |ℬ|$

References

• Girard, J.-Y.; Lafont, Y.; Taylor, P. (1989), Proofs and types (PDF), Cambridge University Press.
• Girard, J.-Y. (2004), "Between logic and quantic: a tract", in Ehrhard; Girard; Ruet; et al. (eds.), Linear logic in computer science (PDF), Cambridge University Press.
• Girard, Jean-Yves (1986-01-01). "The system F of variable types, fifteen years later". Theoretical Computer Science. 45: 159–192. doi:10.1016/0304-3975(86)90044-7. ISSN 0304-3975.