[Prev][Next][Index][Thread]
Hypercoherences
Hypercoherences: an extensional model of linear logic based on sequentiality.
-----------------------------------------------------------------------------
In a previous work with Bucciarelli (see the LICS91 proceedings), we
have proposed the notion of strongly stable functions on qualitative
domains (or dI domains) equipped with a "coherence". We were able to
build a cartesian closed category with these structures and morphisms.
The basic observation was the following:
1) it is reasonable to define a notion of Kahn-Plotkin sequential
functions between coherence spaces (for instance) taking the orthogonal
of a coherence space E as set of "cells" on E.
If x is in E and q is in orth(E), then x "fills" q if x intersects q.
2) let us call "linearly coherent" a subset A of E which is non-empty, finite,
and such that: for any q in orth(E), if all the elements of A intersect q,
then the intersection of A intersects q.
In other words: A={x1,...,xn} is linearly coherent if, for all
a1 in x1,...,an in xn, if {a1,...,an} in orth(E), then a1=...=an.
In other words: any section of A which is in orth(E) is constant.
Let us note CL(E) the set of all linearly coherent subsets of E.
3) then a continuous function f:E->F is sequential iff, for all
A in CL(E), the set f(A) is in CL(F) and f(inter A)=inter f(A).
Then we built a CCC considering couples (Q,C(Q)) where Q is a qualitative
domain and C(Q) is a set of non-empty and finite subsets of Q satisfying
some requirements. In this category, a morphism (Q,C(Q))->(R,C(R))
is a continuous function f:Q->R such that, for all A in C(Q),
f(A) in C(R) and f(inter A)=inter f(A). (Where inter A is the intersection
of A.)
Such a function is called "strongly stable".
This short note presents a framework were all the constructions presented
in our LICS paper make sense, but where the objects admit a simpler
description and where the morphisms admit a simple trace characterization.
Furthermore, this framework allows to construct a model of
linear logic. This model is presented in a paper which will appear soon
in "Mathematical Structures in Computer Science".
The objects are called "hypercoherences" (following an observation
of Danos: they are hypergraphs).
A hypercoherence is a pair X=(|X|,G(X)) (read G(X) as "Gamma of X") where
* |X| is an enumerable set (the web)
* G(X) is a set of finite and non-empty subsets of |X|
The only requirement is that, for any a in |X|, {a} is in G(X).
Let us note G*(X) the set of all elements of G(X) which are not singletons.
G(X) is called the "coherence of X" or the "atomic coherence of X".
G*(X) is called the "strict (atomic) coherence of X".
Beware: G(X) is not required to be down-closed under inclusion. That is,
we may have u in G(X), v non-empty subset of u but v not in G(X).
Out of a hypercoherence X, one defines:
* a qualitative domain qD(X). The elements of qD(X) are the subsets x of
|X| such that any finite and non empty subset of x be in G(X)
* a "state coherence" on qD(X), that we note C(X). An element of C(X)
is a finite and non-empty subset A of qD(X) such that any finite
"multisection" of A be in G(X). A multisection of A is a subset u of
|X| such that any element of u be an element of an element of A, and
any element of A contain an element of u. That is: u is contained
in the union of A and intersects each element of A.
It is easy to check that qD(X) is a qD whose web is |X|.
It is also clear that any finite, non-empty and bounded subset of qD(X)
is in C(X). However, there are in general elements of C(X) which are not bounded
(observe for instance that any finite subset of qD(X) which contains
the empty set is in C(X))
If X and Y are hypercoherences, a strongly stable map from X to Y
is a continuous function qD(X)->qD(Y) such that, for all A in C(X),
f(A) be in C(Y) and f(inter A)=inter f(A).
Clearly, a strongly stable map is a stable map qD(X)->qD(Y), but the converse
is false in general.
A strongly stable map f is "linear" if it is linear as a stable map,
that is f(emptyset)=emptyset and f(x union y)=f(x) union f(y).
Since strongly stable functions from X to Y are stable,
they admit a trace representation "a la Girard".
These traces turn out to form a qD which is of the shape qD(Z) where
Z is a hypercoherence definable in terms of X and Y.
We describe this construction for linear strongly stable functions:
Let X and Y be hypercoherences. Define a hypercoherence X-oY by:
* |X-oY|=|X|x|Y|
* a subset w of this web is in G(X-oY) iff it is finite, non-empty
and satisfies:
w1 in G(X) => w2 in G(Y)
w1 in G*(X) => w2 in G*(Y)
in other words:
w1 in G(X) => (w2 in G(Y) and (#w2=1 => #w1=1))
(w1 and w2 are the projections of w on |X| and |Y| respectively).
Then qD(X-oY) is exactly the set of all traces of linear strongly stable
functions X->Y. G(X-oY) contains additionnal informations which are
not used in qD(X-oY) but which are essential for defining the state
coherence C(X-oY).
Observe that this definition of X-oY is very similar to Girard's definition
of E-oF in the framework of coherence spaces. The only diference is that
here the size of the "coherence" is unbound.
Tensor product of X and Y:
|X tens Y|=|X|x|Y|
w in G(X tens Y) iff w1 in G(X) and w2 in G(Y).
This product admits a neutral element 1 (the hypercoherence whose web has only
one element). It is commutative and associative. Furthermore, up to a
canonical isomorphism: (X tens Y)-oZ=X-o(Y-oZ)
so that we have built a monoidal closed category.
Orthogonal of X:
we note it Orth X. It is defined by
|Orth X|=|X|
u in G(Orth X) iff u is a finite and non-empty subset of |X|
which is not in G*(X).
Then all the usual isomorphisms are satisfied
(Orth Orth X=X, contraposition, Orth X=X-oBot where Bot=Orth 1 which
turns out to be isomorphic to 1, like in coherence spaces,...)
The "par" is defined by duality.
Cartesian product ("with"):
|XxY|=|X|+|Y| (disjoint union)
w is in G(XxY) iff w is a finite and non-empty subset of |X|+|Y| and
w1 empty => w2 in G(Y)
w2 empty => w1 in G(X)
(where w1 is the first component of w, that is w inter |X| if |X|
and |Y| are assumed to be disjoint, and similarly for w2).
One checks that qD(XxY)=qD(X)xqD(Y) (usual order theoretic product)
up to a canonical isomorphism. And C(XxY) is the largest state coherence
(wrt inclusion) making the two projections strongly stable.
The "plus" is defined by duality.
The exponential "!":
|!X| is the set of all finite elements of qD(X), and G(X) is the
restriction of C(X) to |!X|.
And the exponential "?" is defined by duality.
Then one proves that ! is a comonade, and that
!(XxY)=(!X)tens(!Y), so that the co-Kleisli category of ! is
cartesian closed.
This co-Kleisli category is equivalent to the category of hypercoherences
and strongly stable functions ( qD((!X)-oY) is the domain of all traces
of strongly stable functions from X to Y).
It is actually a full sub-CCC of the category
of qualitative domains with coherence we defined in our LICS91 paper.
Specifically, this means that C((!X)-oY) is the greatest possible state
coherence on qD((!X)-oY) such that the evaluation function
qD((!X)-oY)xqD(X)->qD(Y) be strongly stable.
If E is a coherence space, let us define a hypercoherence H(E) as follows:
|H(E)|=|E| and u in G(H(E)) iff u is a finite and non-empty subset of |E|
which is either a singleton or contains at least two strictly
compatible elements of |E| (that is, iff u is a singleton or is not
in the orthogonal of the coherence space E).
Then one checks that qD(H(E))=E and that C(H(E))=CL(E).
So, according to the observation stated at the beginning of this note,
a function from E to F is sequential iff it is strongly stable from
H(E) to H(F). One can also observes that H(ExF)=H(E)xH(F) (the sign "x"
does not have the same significance on both sides of this equation),
so that the category of coherence spaces and sequential functions is
a sub-cartesian category of the category of hypercoherences and strongly
stable functions. (The category of coherence spaces and sequential
functions is cartesian but not cartesian closed.)
So, in some sense, strong stability is a "conservative extension"
of sequentiality to higher order.
In the MSCS paper, we develop also some simple considerations about a notion
of "polarity" which seems to make sense in this new framework.
Some additional work has also be done for comparing strongly stable
functions between hypercoherences with sequential algorithms between
"sequential structures" (a slight extension of CDS's), and it appears
that, in some sense, the notions are equivalent.
Thomas Ehrhard
e-mail: ehrhard@dmi.ens.fr