In
proof theory, a coherent space (also coherence space) is a concept introduced in the semantic study of
linear logic.
Let a
set
Set, The Set, SET or SETS may refer to:
Science, technology, and mathematics Mathematics
*Set (mathematics), a collection of elements
*Category of sets, the category whose objects and morphisms are sets and total functions, respectively
Electro ...
''C'' be given. Two subsets ''S'',''T'' ⊆ ''C'' are said to be ''orthogonal'', written ''S'' ⊥ ''T'', if ''S'' ∩ ''T'' is ∅ or a
singleton
Singleton may refer to:
Sciences, technology Mathematics
* Singleton (mathematics), a set with exactly one element
* Singleton field, used in conformal field theory Computing
* Singleton pattern, a design pattern that allows only one instance ...
. The ''dual'' of a family ''F'' ⊆ ℘(''C'') is the family ''F''
⊥ of all subsets ''S'' ⊆ ''C'' orthogonal to every member of ''F'', i.e., such that ''S'' ⊥ ''T'' for all ''T'' ∈ ''F''. A coherent space ''F'' over ''C'' is a family of ''C''-subsets for which ''F'' = (''F''
⊥)
⊥.
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 coherence space translation was used because
spectral space In mathematics, a spectral space is a topological space that is homeomorphic to the spectrum of a commutative ring. It is sometimes also called a coherent space because of the connection to coherent topos.
Definition
Let ''X'' be a topological ...
s are sometimes called coherent spaces.
Definitions
As defined by
Jean-Yves Girard
Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is the research director (emeritus) at the mathematical institute of the University of Aix-Marseille, at Luminy.
Biography
Jean-Yves Girard is an alumnus of the ...
, a ''coherence space''
is a collection of
sets satisfying down-closure and binary completeness in the following sense:
* Down-closure: all subsets of a set in
remain in
:
* Binary completeness: for any subset
of
, if the
pairwise union of any of its elements is in
, then so is the union of all the elements of
:
The elements of the sets in
are known as ''tokens'', and they are the elements of the set
.
Coherence spaces correspond one-to-one with
(undirected) graphs (in the sense of a
bijection from the set of coherence spaces to that of undirected graphs). The graph corresponding to
is called the ''web'' of
and is the graph induced a
reflexive,
symmetric relation over the token space
of
known as ''coherence modulo''
defined as:
In the web of
, nodes are tokens from
and an
edge
Edge or EDGE may refer to:
Technology Computing
* Edge computing, a network load-balancing system
* Edge device, an entry point to a computer network
* Adobe Edge, a graphical development application
* Microsoft Edge, a web browser developed ...
is shared between nodes
and
when
(i.e.
.) This graph is unique for each coherence space, and in particular, elements of
are exactly the
cliques
A clique ( AusE, CanE, or ), in the social sciences, is a group of individuals who interact with one another and share similar interests. Interacting with cliques is part of normative social development regardless of gender, ethnicity, or popular ...
of the web of
i.e. the sets of nodes whose elements are pairwise adjacent (share an
edge
Edge or EDGE may refer to:
Technology Computing
* Edge computing, a network load-balancing system
* Edge device, an entry point to a computer network
* Adobe Edge, a graphical development application
* Microsoft Edge, a web browser developed ...
.)
Coherence spaces as types
Coherence spaces can act as an interpretation for types in
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a fou ...
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
of a type
can be given a set of finite approximations
which is in fact, a
directed set
In mathematics, a directed set (or a directed preorder or a filtered set) is a nonempty set A together with a reflexive and transitive binary relation \,\leq\, (that is, a preorder), with the additional property that every pair of elements ha ...
with the subset relation. With
being a coherent subset of the token space
(i.e. an element of
), any element of
is a finite subset of
and therefore also coherent, and we have
Stable functions
Functions between types
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,
is a stable function when
# It is
monotone
Monotone refers to a sound, for example music or speech, that has a single unvaried tone. See: monophony.
Monotone or monotonicity may also refer to:
In economics
*Monotone preferences, a property of a consumer's preference ordering.
*Monotonic ...
with respect to the subset order (respects approximation,
categorically, is a
functor
In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) are associated to topological spaces, and m ...
over the
poset
In mathematics, especially order theory, a partially ordered set (also poset) formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary r ...
):
# It is
continuous
Continuity or continuous may refer to:
Mathematics
* Continuity (mathematics), the opposing concept to discreteness; common examples include
** Continuous probability distribution or random variable in probability and statistics
** Continuous ...
(categorically, preserves
filtered colimits):
where
is the
directed union
In mathematics, a direct limit is a way to construct a (typically large) object from many (typically smaller) objects that are put together in a specific way. These objects may be groups, rings, vector spaces or in general objects from any categor ...
over
, the set of finite approximants of
.
# It is ''stable'':
Categorically, this means that it preserves the
pullback
In mathematics, a pullback is either of two different, but related processes: precomposition and fiber-product. Its dual is a pushforward.
Precomposition
Precomposition with a function probably provides the most elementary notion of pullback: i ...
:
Product space
In order to be considered stable, functions of two arguments must satisfy the criterion 3 above in this form:
which would mean that in addition to stability in each argument alone, the pullback
![Pullback with order](https://upload.wikimedia.org/wikipedia/commons/4/49/Pullback_with_order.png)
is preserved with stable functions of two arguments. This leads to the definition of a product space
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
In mathematics, more specifically in category theory, a universal property is a property that characterizes up to an isomorphism the result of some constructions. Thus, universal properties can be used for defining some objects independently fr ...
for products. It is defined by the equations:
*
(i.e. the set of tokens of
is the coproduct (or
disjoint union
In mathematics, a disjoint union (or discriminated union) of a family of sets (A_i : i\in I) is a set A, often denoted by \bigsqcup_ A_i, with an injection of each A_i into A, such that the images of these injections form a partition of A ( ...
) 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.
**
**
**
References
*.
*.
Mathematical logic
{{Mathlogic-stub