Coherent semantics

Revision as of 13:14, 8 February 2009

Coherent semantics was invented by Girard in the paper The system F, 15 years later with the objective of building a denotationnal interpretation of second order intuitionnistic logic (aka polymorphic lambda-calculus).

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.

A further achievement of coherent semantics was that it allowed to endow the set of stable functions from $X$ to $Y$ with a structure of domain, thus closing the category of coherent spaces and stable functions. However the most interesting point was the discovery of a special class of stable functions, linear functions, which was the first step leading to Linear Logic.

Preliminary definitions and notations

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

Coherent spaces

As domains

Definition (Coherent space)

A coherent space $X$ is a family of subsets of a given set $\web X$ (the web of $X$ ), which satisfies:

subset closure: if $x\subset y\in X$ then $x\in X$ ,
singletons: $\{a\}\in X$ for
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$ .

A coherent space is thus ordered by inclusion; one easily checks that it is a domain. In particular finite elements of $X$ correspond to compact elements.

As graphs

Definition (Coherent space)

A coherent space $X$ is a family of subsets of a given set $\web X$ (the web of $X$ ) which satisfies that there is a reflexive and symetric relation $\coh_X$ on $\web X$ (the coherence relation) such that $x\in X$ iff $\forall a,b\in x,\, a\coh_X b$ , for any $x\subset\web X$ . In other terms $X$ is the set of complete subgraphs of the simple unoriented graph of the $\coh_X$ relation. For this reason, the elements of $X$ are called cliques.

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

A coherent space in the domain sense is seen to be a coherent space in the graph sense by setting $a\coh_X b$ iff $\{a,b\}\in X$ ; conversely one easily checks that cliques in the graph sense are subset closed and satisfy the binary compatibility condition.

Stable functions

Definition (Stable function)

Let $X$ and $Y$ be two coherent spaces. A function $F:X\mapsto Y$ is stable if it satisfies:

it is non decreasing: for any $x,y\in X$ if $x\subset y$ then $F(x)\subset F(y)$ ;
it is continuous (in the Scott sense): if $A$ is a directed family of cliques of $X$ , that is if for any $x,y\in A$ there is a $z\in A$ such that $x\cup y\subset z$ , then $\bigcup_{x\in A}F(x) = F(\bigcup A)$ ;
it satisfies the stability condition: if $x,y\in X$ are compatible, that is if $x\cup y\in X$ , then $F(x\cap y) = F(x)\cap F(y)$ .

This definition is admitedly not very tractable. An equivalent and most useful caracterisation of stable functions is given by the following theorem.

Theorem

Let $F:X\mapsto Y$ be a non-decreasing function from the coherent space $X$ to the coherent space $Y$ . The function $F$ is stable iff it satisfies: for any $x\in X$ , $b\in\web Y$ , if $b\in F(x)$ then there is a finite clique $x_0\subset x$ such that:

$b\in F(x_0)$ ,
for any $y\subset x$ if $b\in F(y)$ then $x_0\subset y$ ( $x 0$ is the minimum sub-clique of $x$ such that $b\in F(x_0)$ ).

Note that the stability condition doesn't depend on the coherent space structure and can be expressed more generally for continuous functions on domains. However, as mentionned in the introduction, the restriction to coherent spaces allows to endow the set of stable functions from $X$ to $Y$ with a structure of coherent spaces.

Definition (The space of stable functions)

Let $X$ and $Y$ be coherent spaces. The function space $X\rightarrow Y$ is defined by:

$\web{X\rightarrow Y} = \mathcal{C}_{\mathrm{fin}}(X)\times \web Y$ ,
$(x_0, a)\coh_{X\rightarrow Y}(y_0, b)$ iff $\begin{cases}\text{if } x_0\cup y_0\in X\text{ then } a\coh_Y y,\\ \text{if } x_0\cup y_0\in X\text{ and } x_0\neq y_0 \text{ then } a\scoh_Y b\end{cases}$ .

Definition (Trace of a stable function)

Let $F:X\mapsto Y$ be a function (from the cliques of $X$ to the cliques of $Y$ ). The trace of $F$ is the set:

$Tr(F) = {(x 0, b), x 0$ minimal such that $b\in F(x_0)\}$ .

Theorem

If $F$ is stable then $Tr(F)$ is a clique of the function space $X\rightarrow Y$

In particular the continuity of $F$ entails that if $x 0$ is minimal such that $b\in F(x_0)$ , then $x 0$ is finite.

@@ Line 1: / Line 1: @@
-''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'' was invented by Girard in the paper ''The system F, 15 years later'' with the objective of building a denotationnal interpretation of second order intuitionnistic logic (aka polymorphic lambda-calculus).
 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.
+A further achievement of coherent semantics was that it allowed to endow the set of stable functions from <math>X</math> to <math>Y</math> with a structure of domain, thus closing the category of coherent spaces and stable functions. However the most interesting point was the discovery of a special class of stable functions, ''linear functions'', which was the first step leading to Linear Logic.
 == 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.
+There are two equivalent definitions of coherence spaces: the first one, coherent spaces as domains, is interesting from a historical point of view as it emphazises the fact that coherent spaces are particular cases of Scott domains. The second one, coherent spaces as graphs, is the most commonly used and will be our "official" definition in the sequel.
 === Coherent spaces ===
-====  As graphs ====
+==== As domains ====
 {{Definition|title=Coherent space|
-A ''coherent space'' <math>X</math> is a set of ''points'' denoted <math>\web X</math> and called the ''web'' of <math>X</math> together with a reflexive and symetric relation <math>\coh_X</math> on <math>\web X</math> called the ''coherence relation''. Coherent spaces are identified with the simple unoriented graphes of their coherence relations.
+A ''coherent space'' <math>X</math> is a family of subsets of a given set <math>\web X</math> (the ''web'' of <math>X</math>), which satisfies:
+* subset closure: if <math>x\subset y\in X</math> then <math>x\in X</math>,
-The ''strict coherence relation'' <math>\scoh_X</math> on <math>X</math> is defined by: <math>a\scoh_X b</math> iff <math>a\neq b</math> and <math>a\coh_X b</math>.
+* singletons: <math>\{a\}\in X</math> for
+* binary compatibility: if <math>A</math> is a family of pairwise compatible elements of <math>X</math>, that is if <math>x\cup y\in X</math> for any <math>x,y\in A</math>, then <math>\bigcup A\in X</math>.
 }}
-{{Definition|title=Clique|
+A coherent space is thus ordered by inclusion; one easily checks that it is a domain.  In particular finite elements of <math>X</math> correspond to compact elements.
-A ''clique'' of the coherent space <math>X</math> is a set of points in <math>\web X</math> that are pairwise coherent. In other terms a clique is a subgraph of <math>X</math> that is complete. The set of cliques of <math>X</math> is denoted as <math>\mathcal{C}(X)</math>. We will often use the set of ''finite'' cliques of <math>X</math> that will be denoted <math>\mathcal{C}_\mathrm{fin}(X)</math>.
-}}
-==== As domains ====
+====  As graphs ====
 {{Definition|title=Coherent space|
-A coherent space <math>X</math> is a family of subsets of a set <math>\web X</math> which is closed by subset (if <math>x\subset y\in X</math> then <math>x\in X</math>) and satisfies the ''binary compatibility'': if <math>A</math> is a family of pairwise compatible elements of <math>X</math>, that is if <math>x\cup y\in X</math> for any <math>x,y\in A</math>, then <math>\bigcup A\in X</math>.
+A ''coherent space'' <math>X</math> is a family of subsets of a given set <math>\web X</math> (the ''web'' of <math>X</math>) which satisfies that there is a reflexive and symetric relation <math>\coh_X</math> on <math>\web X</math> (the ''coherence relation'') such that <math>x\in X</math> iff <math>\forall a,b\in x,\, a\coh_X b</math>, for any <math>x\subset\web X</math>. In other terms <math>X</math> is the set of complete subgraphs of the simple unoriented graph of the <math>\coh_X</math> relation. For this reason, the elements of <math>X</math> are called ''cliques''.
+The ''strict coherence relation'' <math>\scoh_X</math> on <math>X</math> is defined by: <math>a\scoh_X b</math> iff <math>a\neq b</math> and <math>a\coh_X b</math>.
 }}
-When viewed as a set ordered by inclusion a coherent space is particular case of domain. The reader will easily check that one recovers the previous definition by setting <math>a\coh_X b</math> iff <math>\{a,b\}\in X</math> and conversely that the set of cliques of a coherent space in the graph sense is a coherent space in the domain sense. In particular finite cliques of <math>X</math> correspond to compact elements.
+A coherent space in the domain sense is seen to be a coherent space in the graph sense by setting <math>a\coh_X b</math> iff <math>\{a,b\}\in X</math>; conversely one easily checks that cliques in the graph sense are subset closed and satisfy the binary compatibility condition.
 === Stable functions ===
-From now on we will identify the coherent space (in the graph sense) <math>X</math> with its set of cliques <math>\mathcal{C}(X)</math>. Accordingly a function <math>F</math> from <math>X</math> to <math>Y</math> is a function defined on the cliques of <math>X</math> taking values in the cliques of <math>Y</math>.
 {{Definition|title=Stable function|
@@ Line 48: / Line 46: @@
 }}
-Note that the stability condition doesn't depend on the coherent space structure and can be expressed more generally for continuous functions on domains. However the restriction to coherent spaces allows to get an interesting property: the set of stable functions from <math>X</math> to <math>Y</math> may be in turn endowed with a structure of coherent spaces. In categorical terms, the category of coherent spaces with stable functions is closed.
+Note that the stability condition doesn't depend on the coherent space structure and can be expressed more generally for continuous functions on domains. However, as mentionned in the introduction, the restriction to coherent spaces allows to endow the set of stable functions from <math>X</math> to <math>Y</math> with a structure of coherent spaces.
 {{Definition|title=The space of stable functions|

Coherent semantics

Revision as of 13:14, 8 February 2009

Contents

Preliminary definitions and notations

Coherent spaces

As domains

As graphs

Stable functions

Linear functions

Views

Personal tools

Navigation

Search

Tools