Not to be confused with the notion of coherent space in topology.
The notion of coherence space (Girard 1989, §8, also sometimes “coherent space” but beware of the alternative meaning discussed there) is used for the semantics of linear logic in proof theory. They form a star-autonomous category.
A coherence space is analogous to a locale defined by a basis for its frame of opens. A coherence space has a set of “tokens” we think of as “primitive observations” along with a coherence relation that says when primitive observations are “coherent” in that they can both be satisfied by the same point of the space. A point of the space can then be defined as a clique of observations: a set of observations such that every pair in the set is coherent.
A coherence space $X$ is a collection of subsets of a set $|X|$ which verify some conditions. We call:
The conditions to be verified are:
Equivalently, a coherence space $X$ consists of
A clique is then a subset of $|X|$ such that each pair of elements is coherent. A co-clique is a subset of $|X|$ where any two distinct elements $x \neq y$ are incoherent $\neg (x ~ y)$.
Coherence spaces can be defined as arity spaces for the “subunary” class of arities $\{0,1\}$.
A linear function of coherence spaces $f : X \multimap Y$ is a relation $f \subseteq |X|\times|Y|$ that
The notion in terms of a set of cliques and a coherence relation are equivalent by the following:
The map which send an undirected simple graph $G$ to the pair $(C(G), V(G))$ where $V(G)$ is the set of all the vertices of $G$ and $C(G)$ is the set of all the cliques of $G$ is a bijection between undirected simple graphs and coherence spaces where the coherence space associated to $G$ is $C(G)$ with $|C(G)|=V(G)$. The reciprocal map associates to a coherence space $X$ the undirected simple graph $G$ obtained by taking $V(G)=|X|$ and the set $E(G)$ of edges equal to the set of all cliques of cardinal $2$.
The terminology “coherence space” seems to be due to:
Other references say instead “coherent space”:
Wikipedia, Coherent space
LLwiki, Coherent semantics
Jean-Yves Girard, Linear logic, Theoretical Computer Science 50:1, 1987. (pdf)
Last revised on September 17, 2022 at 14:14:06. See the history of this page for a list of all contributions to it.