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 as .
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 consists of a set , called the web of , along with a reflexive, symmetric binary relation on called coherence.
A clique of a coherent space is a subset of its web such that every pair of elements are coherent with one another . Cliques, not elements of the web, are the "elements" of a coherent space; means that is a clique, not that . Then (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 as an "atomic datum", "single observation", or "basic fact" regarding an element of (a clique), whereas an element of may more generally be a compound datum or require multiple observations to fully consume. Then means that and do not conflict; as facts about a single object, they are compatible. An element of is thus simply a consistent collection of facts.
The simplest example of a coherent space is the flat domain on a set , say the natural numbers. We define and iff ; then the cliques, as a poset, indeed form the flat domain on . In this case, all elements of are "atomic".
A more enlightening example is given by the product of two coherent spaces. The web is given by and the coherence by the clauses
Then a clique of breaks down into a clique of and a clique of . 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 " or "it is ", an atomic fact about a pair of natural numbers is not something like "it is ", but something like "the first element is ".
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.
A stable map is a function from cliques of to cliques of satisfying the following conditions:
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
TODO
TODO
The notion of a stable function is historically prior to coherent spaces. Girard credits them to Berry, who discusses them, among other places, in
Berry, Gérard. “Stable Models of Typed λ-Calculi.” In Automata, Languages and Programming, edited by Giorgio Ausiello and Corrado Böhm, 72–89. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1978. https://doi.org/10.1007/3-540-08860-1_7.
@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
Girard, Jean-Yves. “Normal Functors, Power Series and λ-Calculus.” Annals of Pure and Applied Logic 37, no. 2 (February 1, 1988): 129–77. https://doi.org/10.1016/0168-0072(88)90025-5.
@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
Girard, Jean-Yves. “The System F of Variable Types, Fifteen Years Later.” Theoretical Computer Science 45 (1986): 159–92. https://doi.org/10.1016/0304-3975(86)90044-7.
@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
Girard, Jean-Yves. “Linear Logic.” Theoretical Computer Science 50, no. 1 (January 1, 1987): 1–101. https://doi.org/10.1016/0304-3975(87)90045-4.
@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},
}
If we form a category of coherent spaces with the merely Scott-continuous maps as the morphisms, it embeds as a full subcategory into Scott domains. But this full subcategory is not closed under exponentials. That is, the set of Scott-continuous maps from one coherent space to another is naturally equipped as a Scott domain, but not necessarily one which arises as the cliques of a web. (Technically, in such a situation, it is still possible for the subcategory to be cartesian closed; exponentials computed in the subcategory simply would not agree with ones computed in the larger category. This is not the case here, however.) ↩︎
By order of writing. Several of the papers cited in this section were published in a different order from the one in which they were written, so that some of the "first" and "subsequently" language is incorrect by publication order. ↩︎