Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Coherent space
Summary
In proof theory, a coherent space (also coherence space) is a concept introduced in the semantic study of linear logic.
Let a set C be given. Two subsets S,T ⊆ C are said to be orthogonal, written S ⊥ T, if S ∩ T is ∅ or a singleton. 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 spaces are sometimes called coherent spaces.
As defined by Jean-Yves Girard, 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 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 of the web of i.e. the sets of nodes whose elements are pairwise adjacent (share an edge.)
Coherence spaces can act as an interpretation for types in type theory 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 with the subset relation.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.