Coherent spaces

Coherent spaces are a variation on the notion of Scott domains, introduced by Girard. Like Scott domains, they can be used to construct models of pure lambda-calculus, but they also model System F and linear logic; in fact, the development of linear logic was spurred by features of coherent spaces such as the decomposition of X \to Y as !X \multimap Y.

Definition

There are several equivalent definitions of coherent spaces, varying in simplicity and legibility. Here is probably the simplest (although it does not make the correct notion of morphism immediately obvious):

A coherent space X consists of a set |X|, called the web of X, along with a reflexive, symmetric binary relation ⁐ on |X| called coherence.

A clique of a coherent space X is a subset A \subseteq |X| of its web such that every pair of elements a, b \in A are coherent with one another a \mathrel{⁐} b. Cliques, not elements of the web, are the "elements" of a coherent space; x \in X means that x is a clique, not that x \in |X|. Then X (abusing notation to refer to the space of cliques) is ordered by set inclusion, under which it forms a Scott domain, of which the web (or rather, the singleton cliques) is just a basis. In general, you can think of an element of |X| as an "atomic datum", "single observation", or "basic fact" regarding an element of X (a clique), whereas an element of X may more generally be a compound datum or require multiple observations to fully consume. Then a \mathrel{⁐} b means that a and b do not conflict; as facts about a single object, they are compatible. An element of X is thus simply a consistent collection of facts.

The simplest example of a coherent space is the flat domain on a set A, say the natural numbers. We define |X| = A and a \mathrel{⁐} b iff a = b; then the cliques, as a poset, indeed form the flat domain on A. In this case, all elements of X are "atomic".

A more enlightening example is given by the product X \times Y of two coherent spaces. The web is given by |X \times Y| = |X| + |Y| and the coherence by the clauses

• \operatorname{inl}(x) \mathrel{⁐} \operatorname{inr}(y) always
• \operatorname{inl}(x) \mathrel{⁐} \operatorname{inl}(x') \leftrightarrow x \mathrel{⁐} x'
• \operatorname{inr}(y) \mathrel{⁐} \operatorname{inr}(y') \leftrightarrow y \mathrel{⁐} y'.

Then a clique of X \times Y breaks down into a clique of X and a clique of Y. More to the point, one notes that an atomic fact about a pair is an atomic fact about only one of the components. For example, although an atomic fact about a natural number (assuming that the naturals are a flat domain) is something like "it is 3" or "it is 5", an atomic fact about a pair of natural numbers is not something like "it is (7, 9)", but something like "the first element is 7".

Categories of coherent spaces

There are a number of notions of morphism between coherent spaces. The most important ones are stable maps and linear maps. Embeddings are of less intrinsic interest, but have technical utility. Coherent spaces form a category under any of these notions of morphism, and there are faithful (in fact pseudomonic) forgetful functors from the category of embeddings to the category of linear maps and from the category of linear maps to the category of stable maps. That said, there is a case for linear maps being more basic than stable ones, and embeddings are not necessarily best understood as special stable or linear maps.

Stable maps

A stable map f : X \to Y is a function from cliques of X to cliques of Y satisfying the following conditions:

• Monotonicity: if x \subseteq x', then f(x) \subseteq f(x').
• Scott-continuity: f preserves directed joins (which are unions, since cliques are closed under directed unions). Explicitly, if x_i is a directed family of cliques, then f(\bigcup_i x_i) = \bigcup_i f(x_i).
• Stability: if x \cup x' is a clique, then f(x \cap x') = f(x) \cap f(x').

In categorical terms, a stable map is a functor preserving filtered colimits and pullbacks.

Scott domains famously form a cartesian closed category with Scott-continuous maps as the morphisms. In the case of coherent spaces, this fails.^[1] Restricting to stable maps recovers cartesian closure.

TODO

Linear maps

TODO

Embeddings

TODO

History

The notion of a stable function is historically prior to coherent spaces. Girard credits them to Berry, who discusses them, among other places, in

@inproceedings{Berry78,
  location = {Berlin, Heidelberg},
  title = {Stable models of typed λ-calculi},
  isbn = {978-3-540-35807-7},
  doi = {10.1007/3-540-08860-1_7},
  series = {Lecture Notes in Computer Science},
  pages = {72--89},
  booktitle = {Automata, Languages and Programming},
  publisher = {Springer},
  author = {Berry, Gérard},
  editor = {Ausiello, Giorgio and Böhm, Corrado},
  date = {1978},
  langid = {english},
}

Coherent spaces arose as a simplification/special case of qualitative domains. Qualitative domains were first^[2] introduced in an appendix to

@article{Girard88,
  title = {Normal functors, power series and λ-calculus},
  volume = {37},
  issn = {0168-0072},
  url = {https://www.sciencedirect.com/science/article/pii/0168007288900255},
  doi = {10.1016/0168-0072(88)90025-5},
  pages = {129--177},
  number = {2},
  journaltitle = {Annals of Pure and Applied Logic},
  shortjournal = {Annals of Pure and Applied Logic},
  author = {Girard, Jean-Yves},
  date = {1988-02-01},
  langid = {english},
}

They were subsequently elaborated upon in

@article{Girard86,
  title = {The system F of variable types, fifteen years later},
  volume = {45},
  issn = {03043975},
  url = {https://linkinghub.elsevier.com/retrieve/pii/0304397586900447},
  doi = {10.1016/0304-3975(86)90044-7},
  pages = {159--192},
  journaltitle = {Theoretical Computer Science},
  shortjournal = {Theoretical Computer Science},
  author = {Girard, Jean-Yves},
  date = {1986},
  langid = {english},
}

which in turn considered coherent spaces as "binary qualitative domains" in an appendix of its own. Coherent spaces were given center stage and a name of their own at least by

@article{Girard87,
  title = {Linear logic},
  volume = {50},
  issn = {0304-3975},
  url = {http://www.sciencedirect.com/science/article/pii/0304397587900454},
  doi = {10.1016/0304-3975(87)90045-4},
  pages = {1--101},
  number = {1},
  journaltitle = {Theoretical Computer Science},
  shortjournal = {Theoretical Computer Science},
  author = {Girard, Jean-Yves},
  date = {1987-01-01},
  langid = {english},
}