Coherent semantics

Revision as of 23:20, 8 February 2009

Coherent semantics was invented by Girard in the paper The system F, 15 years later^[1]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.

The cartesian closed structure of coherent semantics

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 $a\in\web X$ .
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.

A coherent space is completely determined by its web and its coherence relation, or equivalently by its web and its strict coherence.

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 space.

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 b,\\ \text{if } x_0\cup y_0\in X\text{ and } a = b\text{ then } x_0 = y_0\end{cases}$ .

One could equivalently define the strict coherence relation on $X\rightarrow Y$ by: $(x_0,a)\scoh_{X\rightarrow Y}(y_0, b)$ iff $x_0\cup y_0\in X$ and $x_0\neq y_0$ entails that $a\scoh_Y b$ .

Definition (Trace of a stable function)

Let $F:X\mapsto Y$ be a function. The trace of $F$ is the set:

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

Theorem

$F$ is stable iff $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.

Definition (The evaluation function)

Let $f$ be a clique in $X\rightarrow Y$ . We define a function $\mathrm{Fun}\,f:X\mapsto Y$ by: $\mathrm{Fun}\,f(x) = \{b\in Y,$ there is $x_0\subset x$ such that $(x_0, b)\in f\}$ .

Theorem (Closure)

If $f$ is a clique of the function space $X\rightarrow Y$ then we have $\mathrm{Tr}(\mathrm{Fun}\,f) = f$ . Conversely if $F:X\mapsto Y$ is a stable function then we have $F = \mathrm{Fun}\,\mathrm{Tr}(F)$ .

Cartesian product

Definition (Cartesian product)

Let $X 1$ and $X 2$ be two coherent spaces. Their cartesian products $X_1\with X_2$ is the coherent space defined by:

the web is the disjoint union of the webs: $\web{X_1\with X_2} = \{1\}\times\web{X_1}\cup \{2\}\times\web{X_2}$ ;
the coherence relation is the serie composition of the relations on $X 1$ and $X 2$ : $(i, a)\coh_{X_1\with X_2}(j, b)$ iff $i\neq j$ or $i = j$ and $a\coh_{X_i} b$ .

This definition is just the way to put a coherent space structure on the cartesian product. Indeed one easily shows the

Theorem

Given cliques $x 1$ and $x 2$ in $X 1$ and $X 2$ , we define the subset $\langle x_1, x_2\rangle$ of $\web{X_1\with X_2}$ by: $\langle x_1, x_2\rangle = \{1\}\times x_1\cup \{2\}\times x_2$ . Then $\langle x_1, x_2\rangle$ is a clique in $X_1\with X_2$ .

Conversely, given a clique $x\in X_1\with X_2$ , for $i = 1,2$ we define $\pi_i(x) = \{a\in X_i, (i, a)\in x\}$ . Then $π i (x)$ is a clique in $X i$ and the function $\pi_i:X_1\with X_2\mapsto X_i$ is stable.

Furthemore these two operations are inverse of each other: $\pi_i(\langle x_1, x_2\rangle) = x_i$ and $\langle\pi_1(x), \pi_2(x)\rangle = x$ . In particular any clique in $X_1\with X_2$ is of the form $\langle x_1, x_2\rangle$ .

Altogether the results above (and a few other more that we shall leave to the reader) allow to get:

Theorem

The category of coherent spaces and stable functions is cartesian closed.

In particular this means that if we define $\mathrm{Eval}:(X\rightarrow Y)\with X\mapsto Y$ by: $\mathrm{Eval}(\langle f, x\rangle) = \mathrm{Fun}\,f(x)$ then $Eval$ is stable.

Linear functions

Definition (Linear function)

A function $F:X\mapsto Y$ is linear if it is stable and furthemore satisfies: for any family $A$ of pairwise compatible cliques of $X$ , that is such that for any $x, y\in A$ , $x\cup y\in X$ , we have $\bigcup_{x\in A}F(x) = F(\bigcup A)$ .

In particular if we take $A$ to be the empty family, then we have $F(\emptyset) = \emptyset$ .

The condition for linearity is quite similar to the condition for Scott continuity, except that we dropped the constraint that $A$ is directed. Linearity is therefore much stronger than stability: most stable functions are not linear.

As with stable function we have an equivalent and much more tractable caracterisation of linear function:

Theorem

Let $F:X\mapsto Y$ be a continuous function. Then $F$ is linear iff it satisfies: for any clique $x\in X$ and any $b\in F(x)$ there is a unique $a\in x$ such that $b\in F(\{a\})$ .

Just as the caracterisation theorem for stable functions allowed us to build the coherent space of stable functions, this theorem will help us to endow the set of linear maps with a structure of coherent space.

Definition (The linear functions space)

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

$\web{X\limp Y} = \web X\times \web Y$ ,
$(a,b)\coh_{X\limp Y}(a', b')$ iff $\begin{cases}\text{if }a\coh_X a'\text{ then } b\coh_Y b'\\ \text{if }a\coh_X a' \text{ and }b=b'\text{ then }a=a'\end{cases}$

Equivalently one could define the strict coherence to be: $(a,b)\scoh_{X\limp Y}(a',b')$ iff $a\scoh_X a'$ entails $b\scoh_Y b'$ .

Definition (Linear trace)

Let $F:X\mapsto Y$ be a function. The linear trace of $F$ denoted as $LinTr(F)$ is the set: $\mathrm{LinTr}(F) = \{(a, b)\in\web X\times\web Y$ such that $b\in F(\{a\})\}$ .

Theorem

If $F$ is linear then $LinTr(F)$ is a clique of $X\limp Y$ .

Definition (Evaluation of linear function)

Let $f$ be a clique of $X\limp Y$ . We define the function $\mathrm{LinFun}\,f:X\mapsto Y$ by: $\mathrm{LinFun}\,f(x) = \{b\in\web Y$ such that there is an $a\in x$ satisfying $(a,b)\in f\}$ .

Theorem (Linear closure)

Let $f$ be a clique in $X\limp Y$ . Then we have $\mathrm{LinTr}(\mathrm{LinFun}\, f) = f$ . Conversely if $F:X\mapsto Y$ is linear then we have $F = \mathrm{LinFun}\,\mathrm{LinTr}(F)$ .

It remains to define a tensor product and we will get that the category of coherent spaces with linear functions is monoidal symetric (it is actually *-autonomous).

References

↑ Girard, Jean-Yves. The System F of Variable Types, Fifteen Years Later. Theoretical Computer Science. Volume 45, Issue 2, pp. 159-192, doi:10.1016/0304-3975(86)90044-7, 1986.

[0] Girard, Jean-Yves. The System F of Variable Types, Fifteen Years Later. Theoretical Computer Science. Volume 45, Issue 2, pp. 159-192, doi:10.1016/0304-3975(86)90044-7, 1986.

[1]

@@ Line 87: / Line 87: @@
 {{Definition|title=Cartesian product|
 Let <math>X_1</math> and <math>X_2</math> be two coherent spaces. Their cartesian products <math>X_1\with X_2</math> is the coherent space defined by:
-* the web is the disjoint union of the webs: <math>\web{X_1\with X_2} = \{1\}\times\web X_1\cup \{2\}\times\web X_2</math>;
+* the web is the disjoint union of the webs: <math>\web{X_1\with X_2} = \{1\}\times\web{X_1}\cup \{2\}\times\web{X_2}</math>;
 * the coherence relation is the serie composition of the relations on <math>X_1</math> and <math>X_2</math>: <math>(i, a)\coh_{X_1\with X_2}(j, b)</math> iff <math>i\neq j</math> or <math>i=j</math> and <math>a\coh_{X_i} b</math>.
 }}
@@ Line 110: / Line 110: @@
 == Linear functions ==
+{{Definition|title=Linear function|
+A function <math>F:X\mapsto Y</math> is ''linear'' if it is stable and furthemore satisfies: for any family <math>A</math> of pairwise compatible cliques of <math>X</math>, that is such that for any <math>x, y\in A</math>, <math>x\cup y\in X</math>, we have <math>\bigcup_{x\in A}F(x) = F(\bigcup A)</math>.
+}}
+In particular if we take <math>A</math> to be the empty family, then we have <math>F(\emptyset) = \emptyset</math>.
+The condition for linearity is quite similar to the condition for Scott continuity, except that we dropped the constraint that <math>A</math> is ''directed''. Linearity is therefore much stronger than stability: most stable functions are not linear.
+As with stable function we have an equivalent and much more tractable caracterisation of linear function:
+{{Theorem|
+Let <math>F:X\mapsto Y</math> be a continuous function. Then <math>F</math> is linear iff it satisfies: for any clique <math>x\in X</math> and any <math>b\in F(x)</math> there is a unique <math>a\in x</math> such that <math>b\in F(\{a\})</math>.
+}}
+Just as the caracterisation theorem for stable functions allowed us to build the coherent space of stable functions, this theorem will help us to endow the set of linear maps with a structure of coherent space.
+{{Definition|title=The linear functions space|
+Let <math>X</math> and <math>Y</math> be coherent spaces. The ''linear function space'' <math>X\limp Y</math> is defined by:
+* <math>\web{X\limp Y} = \web X\times \web Y</math>,
+* <math>(a,b)\coh_{X\limp Y}(a', b')</math> iff <math>\begin{cases}\text{if }a\coh_X a'\text{ then } b\coh_Y b'\\
+                                                                   \text{if }a\coh_X a' \text{ and }b=b'\text{ then }a=a'\end{cases}</math>
+}}
+Equivalently one could define the strict coherence to be: <math>(a,b)\scoh_{X\limp Y}(a',b')</math> iff <math>a\scoh_X a'</math> entails <math>b\scoh_Y b'</math>.
+{{Definition|title=Linear trace|
+Let <math>F:X\mapsto Y</math> be a function. The ''linear trace'' of <math>F</math> denoted as <math>\mathrm{LinTr}(F)</math> is the set: <math>\mathrm{LinTr}(F) = \{(a, b)\in\web X\times\web Y</math> such that <math>b\in F(\{a\})\}</math>.
+}}
+{{Theorem|
+If <math>F</math> is linear then <math>\mathrm{LinTr}(F)</math> is a clique of <math>X\limp Y</math>.
+}}
+{{Definition|title=Evaluation of linear function|
+Let <math>f</math> be a clique of <math>X\limp Y</math>. We define the function <math>\mathrm{LinFun}\,f:X\mapsto Y</math> by: <math>\mathrm{LinFun}\,f(x) = \{b\in\web Y</math> such that there is an <math>a\in x</math> satisfying <math>(a,b)\in f\}</math>.
+}}
+{{Theorem|title=Linear closure|
+Let <math>f</math> be a clique in <math>X\limp Y</math>. Then we have <math>\mathrm{LinTr}(\mathrm{LinFun}\, f) = f</math>. Conversely if <math>F:X\mapsto Y</math> is linear then we have <math>F = \mathrm{LinFun}\,\mathrm{LinTr}(F)</math>.
+}}
+It remains to define a tensor product and we will get that the category of coherent spaces with linear functions is monoidal symetric (it is actually *-autonomous).
 == References ==

Coherent semantics

Revision as of 23:20, 8 February 2009

Contents

The cartesian closed structure of coherent semantics

Coherent spaces

As domains

As graphs

Stable functions

Cartesian product

Linear functions

References

Views

Personal tools

Navigation

Search

Tools