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 <math>

\mathcal A

</math>, satisfying the following closure conditions:

  • Down-closure: if <math>a \in \mathcal A</math> and <math>a' \subseteq a</math>, then <math>a' \in \mathcal A</math>.
  • Binary completeness: for every <math>M \subseteq \mathcal A</math>, if <math>a_1 \cup a_2 \in \mathcal A</math> for all <math>a_1, a_2 \in M</math>, then <math>\bigcup M \in \mathcal A</math>.

The elements of the sets in <math>\mathcal A</math> are tokens. The set of tokens is<math display="block">

|\mathcal A| = \bigcup \mathcal A = \{\alpha \mid \{\alpha\} \in \mathcal A\}.

</math>We say that each <math>

a \in A

</math> is a coherent set of tokens. If a set <math>X</math> is given in advance, and the elements of <math>\mathcal A</math> are presented as subsets of <math>X</math>, then one also requires <math>\{\alpha\} \in \mathcal A</math> for every <math>\alpha \in X</math>. This intuitively states that any token is coherent at least to itself.

Given such a family, one obtains a reflexive, symmetric relation <math>\sim</math> on <math>|\mathcal A|</math>, called coherence modulo <math>\mathcal A</math>, by setting<math display="block">

\alpha \sim \beta \quad \text{if and only if} \quad \{\alpha,\beta\} \in \mathcal A.

</math>The elements of <math>\mathcal A</math> are then precisely the subsets of <math>|\mathcal A|</math> whose elements are pairwise related by <math>\sim</math>.

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, <math>\mathcal A_{\max}</math>, then perform a down-closure:<math display="block">\mathcal A = \{a : \exists a' \in \mathcal A_{\max}, a' \supset a\}</math>The only condition on <math>\mathcal A_{\max}</math> is that any two <math>a, a'\in \mathcal A_{\max}</math>, 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 <math>\mathcal A</math>, its associated graph, called the web of <math>\mathcal A</math>, has vertex set <math>|\mathcal A|</math>. Its edges are the unordered pairs <math>\{\alpha,\beta\}</math> such that <math>\alpha \sim \beta</math>. Note that we require each vertex to have a self-edge purely as a convenient convention.

Conversely, given an undirected graph <math>(|\mathcal A|,E)</math> where each vertex has a self-edge, one obtains a coherence space by taking <math>\mathcal A</math> to be the family of all cliques of the graph:<math display="block">

\mathcal A = \{a \subseteq |\mathcal A| \mid \forall \alpha,\beta \in a, \{\alpha,\beta\} \in E\}.

</math>That is, the elements of <math>\mathcal A</math> are the sets of vertices whose elements are pairwise adjacent.

As a biorthogonally closed family

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

For a family <math>\mathcal A \subseteq \mathcal P(|\mathcal A|)</math>, its dual is the family<math display="block">

\mathcal A^\perp = \{a \subseteq |\mathcal A| \mid \forall b \in \mathcal A,\ a \perp b\}.

</math>A coherence space is a family <math>\mathcal A \subseteq \mathcal P(|\mathcal A|)</math> satisfying<math display="block">

\mathcal A = (\mathcal A^\perp)^\perp.

</math>That is, it is a family that is biorthogonally closed under polarity.

Stable functions

The coherent spaces make up a category <math>\mathbf{Coh}</math>. Each object is a coherent space, and each morphism <math>f: \mathcal A \to \mathcal B</math> is a stable function.

Definition

A stable function is defined as a function mapping cliques to cliques:<math display="block">f : \mathcal A \to \mathcal B</math>such that it is

  • continuous: If <math>\{a_i\}_i \subset \mathcal A</math> is a directed family, then <math>f(\cup_i a_i) = \cup_i f(a_i)</math>.
  • stable: If <math>a, a' \in \mathcal A</math> such that <math>a \cup a' \in \mathcal A</math>, then <math>f(a \cap a') = f(a) \cap f(a')</math>.

By stability, if <math>a \subset a' \in \mathcal A </math> then <math>f(a) \subset f(a')</math>, so <math>f </math> is monotonic.

By stability, <math>f(a) = \cup_{a' \subset a, a'\text{ is finite f(a')</math>. So it shows that <math>f</math> is determined by its value on finite coherent sets.

For continuity, considering the special case where <math>\{a_i\}_i \subset \mathcal A</math> is the empty set, we have <math>f(\emptyset) = \emptyset </math>.

Trace

Given a stable function, its trace <math>Tr(f) \subset \mathcal A \times |\mathcal B|</math> is defined as<math display="block">Tr(f) := \{(a, \beta) | a \in \mathcal A, \beta \in f(a) , (\forall a' \subsetneq a, \beta\not\in f(a'))\}</math>That is, each <math>(a, \beta) \in Tr(f)</math> is such that <math>a</math> is a minimal coherent set needed to produce token <math>\beta</math>. By stability, any <math>(a, \beta) \in Tr(f)</math> must have a finite <math>a</math>.

Conversely, each stable function is determined by its trace:<math display="block">f(a) = \{\beta : (a', \beta) \in Tr(f), a' \subset a\}</math>

Linearity

A stable function <math>f</math> is linear iff any <math>(a, \beta) \in Tr(f)</math>, <math>a</math> 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 <math>f: |\mathcal A| \to \mathcal B</math> such that given a clique <math>a \in \mathcal A</math>, <math>\cup_{\alpha\in a} f(\alpha) </math> is still a clique in <math>\mathcal B</math>.

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 <math>\mathcal A</math>, its polar <math>\mathcal A^\perp</math> is still a coherent space. This is a dual object construction in category theory.

Given any set <math>X</math>, we have the discrete/minimal coherent space <math>\{\{\alpha\}: \alpha \in X\}</math>, and the indiscrete/maximal coherent space <math>\mathcal P(X)</math>.

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

Given two coherent spaces <math>\mathcal A, \mathcal B</math>, there is a coherent space <math>\mathcal A \sqcup \mathcal B</math>. The set of tokens is still<math display="block">|\mathcal A\sqcup \mathcal B| = |\mathcal A| + |\mathcal B|</math> and the edges of <math>\mathcal A\sqcup \mathcal B</math> is the union of the edges in <math>\mathcal A</math>, the edges in <math>\mathcal B</math>. This is the coproduct. This can be defined in general for a family of coherent spaces, <math>\{\mathcal A_i\}_{i\in I}</math>.

Coherent space of stable functions

Given two sets <math>X, Y</math>, the set of partial functions of type <math>X \to Y</math> can be modelled by a coherent space. The token set is <math>X \times Y</math>, and the edges are <math>\{(x, y), (x', y')\}</math> for all <math>x \neq x'</math>. Equivalently, for each <math>x \in X</math>, define <math>\mathcal Y_x</math> to be the discrete/minimal coherent space of <math>Y</math>. Then <math>\&_{x\in X}\mathcal Y_x</math> is the coherent space that we constructed.

This can be intuitively understood as follows: a partial function <math>f: X \to Y</math> has the set of traits <math>\{(x, f(x)) : x \in X \and f(x) \text{ is defined}\}</math>. 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 <math>f</math> is computed by a Turing machine that might fail to halt on some entries. If <math>f(x)</math> 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 <math>\mathcal X, \mathcal Y </math> to be the discrete/minimal coherent spaces. Then <math>f : \mathcal X \to \mathcal Y </math> is a stable function iff there is a partial function <math>f': X \to Y </math>, such that<math display="block">f(\{x\}) = \begin{cases}

\{f'(x)\} &\text{ if }f'(x) \text{ is defined,}\\

\emptyset &\text{ else}

\end{cases} </math>and <math>f' </math> can be identified with its set of traits, which is a coherent set in <math>\&_{x\in X}\mathcal Y_x </math>. Thus, <math>\mathrm{Hom}_{\mathbf{Coh(\mathcal X, \mathcal Y) \simeq \&_{x\in X}\mathcal Y_x

</math> is a coherent space.

In general, we have a functor <math>\Rightarrow: \mathbf{Coh}^2 \to \mathbf{Coh}</math>, contravariant in the first argument and covariant in the second argument, such that<math display="block">\mathrm{Hom}_{\mathbf{Coh(\mathcal A , \mathcal B) \simeq \mathcal A \Rightarrow \mathcal B</math>That is, given any two coherent spaces <math>\mathcal A , \mathcal B</math>, the hom-set between them is structured as a coherent space as well. This makes the category enriched over itself.

The token set <math>|\mathcal A \Rightarrow \mathcal B|</math> is <math>\mathcal A_{\text{fin \times |\mathcal B|</math>, where <math>\mathcal A_{\text{fin</math> is the set of nonempty finite coherent sets in <math>\mathcal A</math>. Two tokens <math>(a, \beta), (a', \beta')</math> are coherent iff

  • If <math>a \cup a' \in \mathcal A</math>, then <math>\{\beta, \beta'\}\in \mathcal B</math>.
  • If <math>a \cup a' \in \mathcal A</math> and <math>a \neq a'</math>, then <math>\beta \neq \beta'</math>.

Note that, if <math>a \cup a'\not\in \mathcal A</math>, then <math>(a, \beta), (a', \beta')</math> for any <math>\beta, \beta' \in |\mathcal B|</math>. That is, we only demand coherence in <math>\mathcal B</math> given coherence in <math>\mathcal A</math>. If there is no coherence in <math>\mathcal A</math>, then we make no demands on coherence in <math>\mathcal B</math>.

Coherence spaces as types

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

Stable functions

Functions between types <math>\mathcal A \to \mathcal B</math> 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, <math>F : \mathcal A \to \mathcal B</math> is a stable function when

  1. It is monotone with respect to the subset order (respects approximation, categorically, is a functor over the poset <math>\mathcal A</math>): <math>a' \subset a \in \mathcal A \implies F(a') \subset F(a).</math>
  2. It is continuous (categorically, preserves filtered colimits): <math display="inline">F(\bigcup_{i\in I}^{\uparrow}a_i)= \bigcup_{i\in I}^\uparrow F(a_i)</math> where <math display="inline">\bigcup_{i\in I}^\uparrow</math> is the directed union over <math>I</math>, the set of finite approximants of <math>a</math>.
  3. It is stable: <math>a_1 \cup a_2 \in \mathcal A \implies F(a_1 \cap a_2) = F(a_1) \cap F(a_2).</math> Categorically, this means that it preserves the pullback:alt=Commutative diagram of the pullback preserved by stable functions|center|frameless

Product space

In order to be considered stable, functions of two arguments must satisfy the criterion 3 above in this form: <math display="block">a_1 \cup a_2 \in \mathcal A \land b_1 \cup b_2 \in \mathcal B \implies F(a_1 \cap a_2, b_1 \cap b_2) = F(a_1, b_1) \cap F(a_2, b_2)</math>which would mean that in addition to stability in each argument alone, the pullback

center|frameless

is preserved with stable functions of two arguments. This leads to the definition of a product space <math>\mathcal A\ \&\ \mathcal B</math> 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:

  • <math>| \mathcal A \ \&\ \mathcal B| = |\mathcal A| + |\mathcal B| = (\{1\} \times |\mathcal A|) \cup (\{2\} \times |\mathcal B|)</math> (i.e. the set of tokens of <math>\mathcal A \ \&\ \mathcal B</math> is the coproduct (or disjoint union) of the token sets of <math>\mathcal A</math> and <math>\mathcal B</math>.
  • Tokens from differents sets are always coherent and tokens from the same set are coherent exactly when they are coherent in that set.
  • <math>(1, \alpha) \sim_{\mathcal A\ \&\ \mathcal B} (1, \alpha') \iff \alpha \sim_{\mathcal A} \alpha'</math>
  • <math>(2, \beta) \sim_{\mathcal A\ \&\ \mathcal B} (2, \beta') \iff \beta \sim_{\mathcal B} \beta'</math>
  • <math>(1, \alpha) \sim_{\mathcal A\ \&\ \mathcal B} (2, \beta), \forall \alpha \in |\mathcal A|, \beta \in |\mathcal B|</math>

References

  • .
  • .