Coherent semantics

Coherent semantics was invented by Girard in the paper The system F, 15 years later. It is a refinement of the former qualitative domains that allows for building an interpretation of system F terms, that is for second order quantifiers.

Coherent semantics is based on the notion of stable functions that was initially proposed by Gérard Berry. Stability is a condition on Scott continuous functions that expresses the determinism of the relation between the output and the input: the typical Scott continuous but non stable function is the parallel or because when the two inputs are both set to true, only one of them is the reason why the result is true but there is no way to determine which one.

Although coherent semantics allowed to solve for the first time the old standing problem of building a denotationnal semantics for polymorphism, one of its main interest is that it also lead Girard to discover the notion of linear function, which rapidly gave rise to linear logic. It is one of the originality of linear logic that its syntax was derived from its semantics.

Preliminary definitions and notations

There are two equivalent definitions of coherence spaces: the first one, coherent spaces as graphs, is the most commonly used and will be our "official" definition in the sequel. The second one, coherent spaces as domains, is however interesting from a historical point of view.

Coherent spaces

As graphs

Definition (Coherent space)

A coherent space X is a set of points denoted $\web X$ and called the web of X together with a reflexive and symetric relation $\coh_X$ on $\web X$ called the coherence relation. Coherent spaces are identified with the simple unoriented graphes of their coherence relations.

The strict coherence relation $\scoh_X$ on X is defined by: $a\scoh_X b$ iff $a\neq b$ and $a\coh_X b$.

Definition (Clique)

A clique of the coherent space X is a set of points in $\web X$ that are pairwise coherent. In other terms a clique is a subgraph of X that is complete. The set of cliques of X is denoted as $\mathcal{C}(X)$.

As domains

Definition (Coherent space)

A coherent space X is a family of subsets of a set $\web X$ which is closed by subset (if $x\subset y\in X$ then $x\in X$) and satisfies the binary compatibility: if A is a family of pairwise compatible elements of X, that is if $x\cup y\in X$ for any $x,y\in A$, then $\bigcup A\in X$.

The reader will easily check that one recovers the previous definition by setting $a\coh_X b$ iff $\{a,b\}\in X$ and conversely that the set of cliques of a coherent space in the graph sense is a coherent space in the domain sense.