Hypercoherences: a strongly stable model of linear logic

Thomas Ehrhard Laboratoire de Mathématiques Discrètes UPR 9016 du CNRS, 163 avenue de Luminy, case 930 F 13288 MARSEILLE CEDEX 9 ehrhard@lmd.univ-mrs.fr

Abstract

We present a model of classical linear logic based on the notion of strong stability that was introduced in [BE], a work about sequentiality written jointly with Antonio Bucciarelli.

Introduction

The present article is a new version of an article already published, with the same title, in Mathematical Structures in Computer Science (1993), vol. 3, pp. 365–385. It is identical to this previous version, except for a few minor details.

In the denotational semantics of purely functional languages (such as PCF [P, BCL]), types are interpreted as objects and programs as morphisms in a cartesian closed category (CCC for short). Usually, the objects of this category are at least Scott domains, and the morphisms are at least continuous functions. The goal of denotational semantics is to express, in terms of “abstract” properties of these functions, some interesting computational properties of the language.

One of these abstract properties is “continuity”. It corresponds to the basic fact that any computation that terminates can use only a finite amount of data. The corresponding semantics of PCF is the continuous one, where objects are Scott domains, and morphisms continuous functions.

Thomas Ehrhard

But the continuous semantics does not capture an important property of computations in PCF, namely “determinism”. Vuillemin and Milner are at the origin of the first (equivalent) definitions of sequentiality, a semantic notion corresponding to determinism. Kahn and Plotkin ([KP]) generalized this notion of sequentiality. More precisely, they defined a category of “concrete domains” (represented by “concrete data structures”) and of sequential functions.

We shall begin with an intuitive description of what sequentiality is, in the framework of concrete data structures (CDS’s). A CDS D, very roughly, is a Scott domain equipped with a notion of “places” or “cells”. An element of D is a partial piece of data where some cells are filled, and others are not. A cell can be filled, in general, by different values. (Think of the cartesian product of two ground types: there are two cells corresponding to the two places one can fill in a couple.) In a CDS, an element x is less than an element x′ if any cell that is filled in x is also filled in x′, and by the same value. If D and E are CDS’s, a sequential function f from D to E is a Scott continuous function from D to E such that, if x ∈ D (that is, x is a partial data; some cells of D may not be filled in x), for any cell d not filled in f(x), there exists a cell c not filled in x and filled in any x′ ∈ D such that x′ ≥ x and such that d is filled in f(x′). This definition is a bit complicated, but the idea is simple. Consider, in order to simplify a bit, the case where E has only one cell. If f(x) is undefined, there is a cell c not filled in x that must be filled in any data x′ more defined than x and such that f(x′) is defined. This means the following: if f(x) is undefined, then there is some “place” in x where the computation is stuck by a lack of information. If we want the computation to go on, we must fill the corresponding cell in x. So sequentiality is a way of speaking about the determinism of programs, considering only their input-output behavior; the basic rule of denotational semantics is that it is forbidden to look inside programs.

The idea of sequentiality is beautiful, but the category of CDS’s and sequential functions has the bad taste to not be cartesian closed. The fundamental reason for this phenomenon is that, in general, there is no reasonable notion of cell for a domain of sequential functions.

The notion of “stability”, introduced by Berry [B1, B2] is a weakening of the idea of sequentiality, that allows the definition of a model of PCF (a CCC). A stable function is a continuous function which commutes to the glb’s (greatest lower bounds) of finite, non-empty and bounded subsets of its domain. However, among stable maps, there are functions that are not sequential (typically the so called Berry function), and so, even if it has nice mathematical properties, the stable model is not very satisfactory with respect to the modelization of determinism. It should be noticed that stability has also been used by Girard (see [G1]) to model system F. He used a very simple kind of domains (qualitative domains), and he also observed that a subclass of these domains (coherence spaces) has very good properties with respect to stability.

Hypercoherences: a strongly stable model of linear logic

This work gave rise to the first proof-theoretic model of classical linear logic.

Berry and Curien (see [BC, C]) defined a CCC where morphisms are sequential, but are not functions; they are sequential algorithms.

In [BE], a joint work with Antonio Bucciarelli, we introduced the notion of strong stability in order to build a CCC where, at first order, the morphisms are sequential functions. Our basic observation was the following: sequentiality can be expressed as a preservation property similar to stability. More precisely, let us say that a family x_{1}, …, x_{n} of points of a CDS is coherent if it has the following property: any cell that is filled in all x_{i}’s is filled by the same value in all x_{i}’s. Then it can be proved that a function is sequential if and only if it sends a coherent family to a coherent family, and commutes to the glb’s of coherent families. (In fact, this holds only for “sequential” CDS’s.) In [BE], we proved the corresponding result for coherence spaces, taking as set of cells on a coherence space a suitable set of linear open subsets of this coherence space, but the intuition is the same. The families that are coherent in the sense described above will be called “linearly coherent” in the following. In order to get a CCC (a model of PCF), we had to abandon the notion of cell (since there is no known CCC of Kahn-Plotkin sequential functions), so we kept the notion of coherence. This led us to define a category where objects are qualitative domains^{1} endowed with an additional structure called “coherence of states”. A coherence of states is a set of non-empty and finite subsets of the qualitative domain that has to satisfy some closure properties. A qualitative domain endowed with a coherence of states is called a qualitative domain with coherence (QDC for short), and an element of the coherence of states of a QDC is said to be a coherent subset of the qualitative domain. A morphism between two QDC’s is a Scott-continuous function between the associated qualitative domains, which, furthermore, maps any coherent set to a coherent set and commutes to the intersections of coherent sets. Such a function is said to be strongly stable. It turns out that the category of QDC’s and strongly stable functions is cartesian closed.

Studying more precisely the coherences of states which are generated when a model of PCF is built up starting from ground types interpreted as suitable coherence spaces endowed with a linear coherence of states, it appears that these coherences of states in fact satisfy stronger properties than the ones we required in [BE].

Let us call “coherence of atoms” of a QDC the family of all coherent subsets of the qualitative domain that are made of atoms. (So the coherence of atoms is a subset of the coherence of states.)

1A qualitative domain is a domain whose elements are subsets of a given set called “web”

of the qualitative domain. These elements are ordered under inclusion, and any subset of an element of a qualitative domain has to be an element of the qualitative domain. The singleton elements of a qualitative domain are called “atoms”.

Essentially, for the QDC’s that are obtained in the construction of a model of PCF, we observe two main phenomena:

• When the coherence of atoms of the qualitative domain is known, the whole coherence of states is known.

• When the coherence of atoms of the qualitative domain is known, the set of all states of the qualitative domain is known: the states are simply the hereditarily coherent subsets of the web. (That is, the subsets of the web, any non-empty and finite subset of which is in the coherence of atoms.)

The first of these observations is not so surprising; it simply means that the coherence of states is in some sense “prime algebraic” (that is, here, “generated by atoms”), as the qualitative domain itself. The second one is very strange, because it says that the coherence of states is actually a more primitive notion than the notion of state itself.

These observations lead to a simplification of the theory of strong stability. Instead of considering qualitative domains with coherence as objects of the category, we just have to consider a very simple kind of structure, which we call “hypercoherence”. (Actually, hypercoherences are hypergraphs, this is why we choose this name.) A hypercoherence is a set of finite subsets of a given set which we call the “web” of the hypercoherence. This set of finite parts of the web is intended to represent the coherence of atoms of a QDC. There is no commitment to any primitive notion of state, since, in a qualitative domain, we certainly want any singleton to be a state.

The only difference between hypercoherences and qualitative domains is that we do not require the family of sets which defines a hypercoherence to be hereditary (i.e. down-closed under inclusion).

This difference, which at first sight could seem innocuous, is, in fact, essential, because it allows us to define the orthogonal of a hypercoherence as its complement with respect to the set of all finite parts of its web. This operation does not make any sense in the framework of qualitative domains, because the complement of a down-closed set of subsets has no reason to be down-closed (and usually, it is not).

Indeed, the category HCohL of hypercoherences equipped with a suitable notion of linear morphisms, gives rise to a new model of full commutative classical linear logic (with the exponential “of course” which categorically is a comonad on HCohL).

Formally, hypercoherences are similar to coherence spaces in the sense that the interpretations of the linear connectives in this model are similar to those of Girard in coherence spaces (see [G2]), even if there are some surprises for the “with” and for the “of course” connectives. But this model seems to authorize some considerations which were impossible with pure coherence spaces. Specifically, it seems very natural to distinguish two classes of hypercoherences that play dual roles: the hereditary ones and the antihereditary ones (many hypercoherences are in neither of these classes). These two classes might be connected to the notion of polarity that Girard introduced in his treatment of classical logic (see [G3]).

This model of linear logic is compatible with the notion of strong stability. Any hypercoherence gives rise canonically and injectively to a qualitative domain with coherence. This object is defined accordingly to the two observations stated before. So we have a notion of strongly stable maps between hypercoherences. Call the category of hypercoherences and strongly stable maps HCohFS. (The letters “FS” in HCohFS come from the french “fortement stable” which means “strongly stable”.) It turns out that this category is equivalent to the co-Kleisli category of the comonad “of course” which is cartesian closed. Furthermore, HCohFS can be considered as a full subcategory of the category of qualitative domains with coherence and strongly stable functions, and in fact, it is a full sub-CCC. This means that the product and exponential of the co-Kleisli category of the comonad “of course” are the same as the ones we defined in [BE] for more general objects. This result can be considered as a formal statement of the two observations we started from.

The remainder of the paper consists of seven sections. Section 1 is devoted to some preliminaries. We recall the basic definitions concerning qualitative domains and stable functions, and also the results of [BE] that we use later. Section 2 gives the definition of hypercoherences and of (linear) morphisms of hypercoherences. To simplify the presentation, morphisms are presented as traces (a trace is a kind of graph) and not as functions. Section 3 presents the model of linear logic from a purely formal point of view. In section 4, we connect this model of linear logic with our previous work about strong stability. Some acquaintance with [BE] could be useful for reading this section, though all the results we need are (briefly) recalled in the preliminaries. Section 5 consists of some definitions and very simple results about a notion of polarity that seems natural in this new framework. Section 6 makes explicit a relation between this model of linear logic and Girard’s model of coherence spaces. Section 7 makes explicit the connection between hypercoherences and sequentiality at first order.

We have chosen this particular presentation, although it may not be very intuitive, for two reasons: first, we hope that the above introduction has provided the reader with sufficient intuition; and second, the notion of hypercoherence is simpler than the notion of QDC and it is very easy and natural to present the category of hypercoherences and linear morphisms in a purely self-contained way.

1 Preliminaries

If E is a set, we denote its cardinality by #E.

Let E and F be two sets. If C ⊆ E × F, we denote the first and second projections of C by C_{1} and C_{2} respectively. We say that C is a pairing of E and F if C_{1} = E and C_{2} = F.

The disjoint union of E and F will be denoted by E + F, and represented by G = (E × {1}) ∪ (F × {2}). If C ⊆ G, we use C_{1} = {a ∈ E | (a, 1) ∈ C} for its first component and C_{2} = {b ∈ F | (b, 2) ∈ C} for its second component.

Definition 1 Let E and F be sets. Let R ⊆ E × F be a binary relation. Let A ⊆ E and B ⊆ F. We say that A and B are paired under R and write A ⋈ B mod (R) if (A × B) ∩ R is a pairing of A and B.

If R is the relation “∈”, we say that A is a multisection of B and we write A < B. If the relation R is “⊆”, we say that A is Egli-Milner lower than B and we write A ⊑ B.

So A < B means that A ⊆ ⋃ B and that A ∩ b is non empty for all b ∈ B, and A ⊑ B means that any element of A is a subset of an element of B and any element of B is a superset of an element of A (this corresponds to the Egli-Milner relation in power-domain theory).

Obviously, the relation ⊑ is a preorder on P (E). Furthermore, if A < B ⊑ C then A < C.

If E is a set, we use P_{fin}^{∗} (E) to denote the set of its finite and non-empty subsets. We write x ⊆_{fin}^{∗} E when x is a finite and non-empty subset of E.

The theory of hypercoherences is closely related to that of qualitative domains, so let us recall some basic definitions and results from [G1].

Definition 2 A qualitative domain is a pair (|Q| , Q) where |Q| is a set (the web) and Q is a subset of P (|Q|) satisfying the following conditions:

• ∅ ∈ Q and, if a ∈ |Q|, then {a} ∈ Q.

• if x ∈ Q and if y ⊆ x then y ∈ Q.

• if D ⊆ Q is directed with respect to inclusion, then ⋃ D ∈ Q.

The elements of Q are called states of the qualitative domain, and the qualitative domain itself will also be denoted Q (for the web can be retrieved from Q).

Observe that a qualitative domain Q can alternatively be presented as a pair (|Q| , Q_{fin}) where |Q| is a set and Q_{fin} is a set of finite subsets of |Q| satisfying all the conditions enumerated above except the last.

If Q is a qualitative domain, we call the set of its finite states Q_{fin}.

Definition 3 A qualitative domain Q is called coherence space when, for u ⊆ |X|, if u satisfies

∀a, b ∈ u {a, b} ∈ Q ,

then u ∈ Q.

Definition 4 Let Q and R be qualitative domains. A function f : Q → R is stable if it is continuous and if

∀x, x′ ∈ Q x ∪ x′ ∈ Q ⇒ f(x ∩ x′) = f(x) ∩ f(x′) .

Furthermore, f is linear if f(∅) = ∅ and

∀x, x′ ∈ Q x ∪ x′ ∈ Q ⇒ f(x ∪ x′) = f(x) ∪ f(x′) .

The adequate notion of order for stable functions is not the extensional one, but the stable one, as observed by Berry (see [B1, B2]).

Definition 5 If f, g : R → Q are two stable functions, f is stably less than g (written f ≤ g) iff

∀x, x′ ∈ Q x ⊆ x′ ⇒ f(x) = f(x′) ∩ g(x) .

If f : Q → R is a stable function, we define its trace tr (f) ⊆ Q_{fin} × |R| by

tr (f) = {(x, b) | b ∈ f(x) and x minimal with this property },

giving

• ∀x ∈ Q f(x) = {b | ∃x_{0} ⊆ x (x_{0}, b) ∈ tr (f)}

• if f, g : Q → R are stable, then f ≤ g iff tr (f) ⊆ tr (g).

(See [G1] for more details about traces.)

A stable function f is linear iff all the elements of the first projection of tr (f) are singletons. So the trace of a linear function Q → R will always be considered as a subset of |Q| × |R|.

Definition 6 Let Q and R be qualitative domains. A rigid embedding of Q into R is an injection f : |Q| → |R| such that, for all u ⊆ |Q|, one has u ∈ Q iff f(u) ∈ R.

It is the canonical notion of substructure for qualitative domains. (For more details, see [GLT].)

Now we recall some definitions and results of [BE].

Definition 7 A qualitative domain with coherence (qDC) is a pair (Q, C (Q)) where Q is a qualitative domain and C (Q) is a subset of P_{fin}^{∗} (Q) satisfying the following properties:

• if x ∈ Q then {x} ∈ C (Q),

• if A ∈ C (Q) and if B ∈ P_{fin}^{∗} (Q) is such that B ⊑ A, then B ∈ C (Q),

• if D_{1}, …, D_{n} are directed subsets of Q such that for any x_{1} ∈ D_{1}, …, x_{n} ∈ D_{n} the family {x_{1}, …, x_{n}} is in C (Q), then the family {⋃ D_{1}, …, ⋃ D_{n}} is in C (Q).

An element of C (Q) will be called a coherent set of Q. Such a qDC (Q, C (Q)) will be denoted by Q simply.

The strongly stable functions are similar to stable functions, but they have to preserve coherence as well as intersections of coherent sets of states, and not just of bounded ones:

Definition 8 Let Q and R be qDC’s. A strongly stable map f from Q to R is a continuous function f : Q → R such that, if A ∈ C (Q), then f(A) ∈ C (R) and f(⋂ A) = ⋂ f(A).

The preservation of coherence (A ∈ C (Q) ⇒ f(A) ∈ C (R)) is as important as the preservations of intersections of coherent families of states. It was not present in the theory of stable functions, because a stable function has to be monotone, and thus maps a bounded set of states to a bounded set of states. Here there is no reason why the image of a coherent set of states should be coherent.

Observe that any strongly stable map is stable, because, if Q is a qDC and if A ⊆ Q is finite, non-empty and bounded, then A ∈ C (Q). Actually, A ⊑ {x} for any upper bound x of A.

Definition 9 A strongly stable function is linear if it is linear as a stable function.

In [BE] we have proved that the category QDC of qDC’s and strongly stable maps is cartesian closed. Let us just recall the characterizations of cartesian products and function spaces.

Proposition 1 Let Q and R be qDC’s. Their cartesian product Q × R in the category QDC is (P, C (P)) where P is the usual product of the qD’s Q and R (that is, up to a canonical isomorphism, P is the cartesian product of the sets Q and R, equipped with the product order) and C (P) is the set of non-empty and finite subsets C of P such that C_{1} ∈ C (Q) and C_{2} ∈ C (R).

In the next propositions, if T is the trace of a strongly stable function, then f^{T} denotes this function.

Proposition 2 Let Q and R be qDC’s. The function space FS (Q, R) of Q and R in the category QDC is (P, C (P)) where P is the qualitative domain of traces of strongly stable functions Q → R and C (P) is the set of all non-empty and finite sets T of traces of strongly stable functions Q → R such that, for any A ∈ C (Q) and for any pairing E of T and A, we have

{f^{T} (x) | (T, x) ∈ E} ∈ C (R)

and

⋂{f^{T} (x) | (T, x) ∈ E} = f^{⋂ T} (⋂ A) .

Let us now recall how this notion of strong stability is connected to sequentiality.

Let Q be a coherence space. The orthogonal Q^{⊥} of Q is the coherence space whose web is |Q| and such that, for a, b ∈ |Q|, we have {a, b} ∈ Q^{⊥} iff a = b or {a, b} ∉ Q.

In this framework, we rephrase the definition of sequentiality outlined in the introduction. The idea is to consider Q^{⊥} as a set of cells for Q, and to say that x ∈ Q fills α ∈ Q^{⊥} if x ∩ α ≠ ∅ (observe that, in that case, x ∩ α is a singleton).

Definition 10 Let Q and R be coherence spaces. We say that a function f : Q → R is sequential iff it is continuous, and for any x ∈ Q, for any β ∈ R^{⊥} such that f(x) ∩ β = ∅, there exists α ∈ Q^{⊥} such that x ∩ α = ∅ and such that, for any x′ ∈ Q, if x ⊆ x′ and f(x′) ∩ β ≠ ∅, then x′ ∩ α ≠ ∅.

Let Q be any coherence space. We endow Q with its “linear coherence” C^{L} (Q) which is the set of non-empty and finite subsets {x_{1}, …, x_{n}} of Q such that for any {a_{1}, …, a_{n}} ∈ Q^{⊥}, if a_{1} ∈ x_{1}, …, a_{n} ∈ x_{n}, then a_{1} = … = a_{n}. It is easily checked that (Q, C^{L} (Q)) is then a qDC.

Proposition 3 Let Q and R be coherence spaces. A function f : Q → R is sequential iff it is strongly stable (Q, C^{L} (Q)) → (R, C^{L} (R)).

2 Hypercoherences: basic definitions

Definition 11 A hypercoherence is a pair X = (|X| , Γ (X)) where |X| is an enumerable set and Γ (X) is a subset of P_{fin}^{∗} (|X|) such that for any a ∈ |X|, {a} ∈ Γ (X). The set |X| is called web of X and Γ (X) is called atomic coherence of X.

If X is a hypercoherence, we note Γ^{∗} (X) the set of all u ∈ Γ (X) such that #u > 1. This set is called strict atomic coherence of X. A hypercoherence can be described by its strict atomic coherence as well as by its atomic coherence.

Observe that the only difference between a hypercoherence and a qualitative domain is that, if u ∈ Γ (X) and if v ⊆ u, we do not require that v be in Γ (X).

Definition 12 A hypercoherence X is hereditary if, for all u ∈ Γ (X) and for all v ⊆_{fin}^{∗} u, one has v ∈ Γ (X).

Not all hypercoherences are hereditary.

We explain now how to build a qDC out of a hypercoherence.

Definition 13 Let X be a hypercoherence. We define qD (X) and C (X) as follows:

qD (X) = {x ⊆ |X| | ∀u ⊆_{fin}^{∗} |X| u ⊆ x ⇒ u ∈ Γ (X)}

and

C (X) = {A ⊆_{fin}^{∗} qD (X) | ∀u ⊆_{fin}^{∗} |X| u < A ⇒ u ∈ Γ (X)} .

qD (X) will be called the qualitative domain generated by X, and C (X) will be called the state coherence generated by X. The couple (qD (X) , C (X)) will be noted qDC (X). The set of finite states of qD (X) will be noted qD_{fin} (X).

So, qD_{fin} (X) is the set of elements of Γ (X) which are hereditary, that is of which any subset is either empty or in Γ (X).

The following result justifies the terminology and notations:

Proposition 4 If X is a hypercoherence, then (qD (X) , C (X)) is a qualitative domain with coherence, and |qD (X)| = |X|.

The proof is straightforward. The qualitative domain with coherence qDC (X) will be called qualitative domain with coherence generated by X.

Observe that, for a hypercoherence X, the atomic coherence Γ (X) can be retrieved from C (X) (and thus from qDC (X)). Namely, the elements of Γ (X) are the finite and non-empty subsets u of |X| such that {{a} | a ∈ u} be in C (X). So the hypercoherences can be seen as certain qDC’s.

We give now two important classes of examples of hypercoherences:

• If Q is a qualitative domain, we can define a hereditary hypercoherence X as follows: we take |X| = |Q| and Γ (X) = Q_{fin} \ {∅}. Then it is easy to see that qD (X) = Q and that C (X) is the set of all non-empty and finite bounded subsets of Q.

• If Q is a coherence space, we can also define a hypercoherence Y as follows: |Y | = |Q| and a finite and non-empty subset of |Q| is in Γ (Y) iff it is a singleton, or it contains distinct elements a and a′ of |Q| such that {a, a′} ∈ Q. Then it is easily checked that qD (Y) = Q and that C (Y) = C^{L} (Q).

Now we have enough material to start the presentation of our model of linear logic. To avoid boring and trivial categorical calculations, we shall use the informal notion of “canonical isomorphism” between hypercoherences. An isomorphism between two hypercoherences X and Y is a bijection f : |X| → |Y | such that, for all u ⊆_{fin}^{∗} |X|, we have f(u) ∈ Γ (Y) iff u ∈ Γ (X). For us, a canonical isomorphism is an isomorphism which corresponds to a bijection on the webs which is standard and universal from the set-theoretic point of view. A typical example is the bijection which corresponds to the associativity of cartesian product of sets.

Definition 14 Let X and Y be hypercoherences. We call linear implication of X and Y and note X −∘ Y the hypercoherence defined by |X −∘ Y | = |X|×|Y | and w ∈ Γ (X −∘ Y) iff w is a non-empty and finite subset of |X −∘ Y | such that

w_{1} ∈ Γ (X) ⇒ (w_{2} ∈ Γ (Y) and (#w_{2} = 1 ⇒ #w_{1} = 1)) .

Equivalently, w ∈ Γ (X −∘ Y) iff w ⊆_{fin}^{∗} |X −∘ Y | and

w_{1} ∈ Γ (X) ⇒ w_{2} ∈ Γ (Y) and w_{1} ∈ Γ^{∗} (X) ⇒ w_{2} ∈ Γ^{∗} (Y) .

Of course, X −∘ Y satisfies the only axiom of hypercoherences.

Definition 15 Let X and Y be hypercoherences. A linear morphism X −∘ Y is an element of qD (X −∘ Y).

We shall often write s : X −∘ Y instead of s ∈ qD (X −∘ Y).

Proposition 5 Let X, Y and Z be hypercoherences.

• The set Id_{X} = {(a, a) | a ∈ |X|} is in qD (X −∘ X).

• Let s ∈ qD (X −∘ Y) and t ∈ qD (Y −∘ Z). Then the set

t ∘ s = {(a, c) | ∃b (a, b) ∈ s and (b, c) ∈ t}

is in qD (X −∘ Z).

Proof: The fact that Id_{X} ∈ qD (X −∘ X) is obvious.

Observe first that if (a, c) ∈ t ∘ s then there is exactly one b such that (a, b) ∈ s and (b, c) ∈ t. Actually, if y is a non-empty and finite subset of {b | (a, b) ∈ s and (b, c) ∈ t}, then y ∈ Γ (Y) because {a} ∈ Γ (X), and thus #y = 1 because #{c} = 1.

Let w ⊆ t ∘ s be finite, non-empty and such that w_{1} ∈ Γ (X). Let

u = {(a, b) ∈ s | ∃c ∈ w_{2} (a, c) ∈ w and (b, c) ∈ t}

and

v = {(b, c) ∈ t | ∃a ∈ w_{1}(a, c) ∈ w and (a, b) ∈ s} .

Finiteness of u and v follows from the observation above. We clearly have u_{1} ⊆ w_{1}. Conversely, let a ∈ w_{1}. Let c ∈ w_{2} be such that (a, c) ∈ w. By definition, there is a b such that (a, b) ∈ s and (b, c) ∈ t, so a ∈ u_{1}. Thus u_{1} = w_{1} ∈ Γ (X). So u_{2} ∈ Γ (Y). But clearly u_{2} = v_{1}. So v_{2} ∈ Γ (Z). We conclude that w_{2} ∈ Γ (Z) because v_{2} = w_{2}.

Assume furthermore that #w_{2} = 1. Then #v_{1} = 1 and #u_{1} = 1 and we conclude.

We have obviously defined a category, where objects are hypercoherences, composition is ∘ and the identity morphisms are the Id_{X}’s. We note HCohL this category.

3 A model of classical linear logic

The goal of this section is to interpret in the category HCohL the connectives of classical linear logic. In fact, the linear implication has already been partially treated in the previous section.

We note 1 the hypercoherence whose web is a singleton.

Definition 16 Let X and Y be hypercoherences. Their tensor product X ⊗Y is the hypercoherence whose web is |X| × |Y | and whose atomic coherence is defined by: w ∈ Γ (X ⊗ Y) iff w_{1} ∈ Γ (X) and w_{2} ∈ Γ (Y).

The tensor product is in fact a functor HCohL × HCohL → HCohL. If s : X −∘ X′ and t : Y −∘ Y′, define s ⊗ t by

s ⊗ t = {((a, b), (a′, b′)) | (a, a′) ∈ s and (b, b′) ∈ t} .

Let us check that s ⊗ t : X ⊗ Y −∘ X′ ⊗ Y′. Let w ⊆_{fin}^{∗} s ⊗ t and assume that w_{1} ∈ Γ (X ⊗ Y), that is w_{11} ∈ Γ (X) and w_{12} ∈ Γ (Y). Let us prove that w_{21} ∈ Γ (X′). Let

w^{1} = {(a, a′) ∈ s | ∃(b, b′) ∈ t ((a, b), (a′, b′)) ∈ w} .

We have w^{1} ⊆_{fin}^{∗} s and w_{1}^{1} = w_{11}, w_{2}^{1} = w_{21}. Hence w_{21} ∈ Γ (X′). Similarly w_{22} ∈ Γ (Y′). Assume furthermore that #w_{2} = 1. Let (a′, b′) be the unique element of that set. Then w_{11} × {a′} = w^{1}, so #w_{11} = 1. Similarly #w_{12} = 1 and we conclude.

Proposition 6 The tensor product is, up to canonical isomorphisms, a commutative and associative operation which admits 1 as neutral element. Furthermore, the canonical isomorphisms associated to commutativity and associativity satisfy the axioms of symmetric monoidal categories.

This is a purely formal verification. See [M] for details about monoidal categories.

Definition 17 Let X be a hypercoherence. We call orthogonal of X and note X^{⊥} the hypercoherence whose web is |X| and whose atomic coherence is P_{fin}^{∗} (|X|) \ Γ^{∗} (X).

So that u ∈ Γ^{∗} (X^{⊥}) iff u is finite and non-empty and u ∉ Γ (X).

Proposition 7 Let X be a hypercoherence. Then (X^{⊥})^{⊥} = X.

The proof is straightforward.

Proposition 8 Let X and Y be hypercoherences. Up to a canonical isomorphism,

X^{⊥} −∘ Y^{⊥} = Y −∘ X .

Proof: Just contrapose the definition of X^{⊥} −∘ Y^{⊥}.

If s : X −∘ Y, we note ^{t}s the corresponding morphism Y^{⊥} −∘ X^{⊥}, which is simply {(b, a) | (a, b) ∈ s}. This operation on morphisms is called transposition, and turns ( )^{⊥} into a contravariant and involutive endofunctor on HCohL.

Definition 18 Let X and Y be hypercoherences. The par of X and Y is the hypercoherence X℘Y = (X^{⊥} ⊗ Y^{⊥})^{⊥}.

Proposition 9 Let X and Y be hypercoherences. We have |X℘Y | = |X|×|Y |, and w ∈ Γ^{∗} (X℘Y) iff w is non-empty and finite and satisfies w_{1} ∈ Γ^{∗} (X) or w_{2} ∈ Γ^{∗} (Y).

Easy calculation.

Observe that, because of propositions 8 and 6, the par is commutative, associative and admits 1 as neutral element, because clearly 1^{⊥} = 1. This last phenomenon is a drawback that this semantics of linear logic shares with the coherence spaces semantics.

Proposition 10 Let X and Y be hypercoherences, then X −∘ Y = X^{⊥}℘Y.

Proof: Obviously, these hypercoherences have the same web. If w ⊆_{fin}^{∗} |X| × |Y |, then w ∈ Γ (X −∘ Y) iff

w_{1} ∈ Γ (X) ⇒ w_{2} ∈ Γ (Y) and w_{1} ∈ Γ^{∗} (X) ⇒ w_{2} ∈ Γ^{∗} (Y)

that is

(w_{1} ∈ Γ^{∗} (X^{⊥}) or w_{2} ∈ Γ (Y)) and (w_{1} ∈ Γ (X^{⊥}) or w_{2} ∈ Γ^{∗} (Y))

and we conclude.

As a corollary, we get:

Proposition 11 The category HCohL is monoidal closed with respect to the tensor product ⊗ and the function space −∘. More precisely, if X, Y and Z are hypercoherences, then, up to canonical isomorphisms:

(X ⊗ Y) −∘ Z = X −∘ (Y −∘ Z) .

Proof: This results from the associativity (up to canonical isomorphisms) of par.

Definition 19 Let X and Y be hypercoherences. We call with of X and Y and note X × Y the hypercoherence whose web is |X| + |Y | and whose atomic coherence is the set of all w ⊆_{fin}^{∗} |X| + |Y | such that:

w_{1} = ∅ ⇒ w_{2} ∈ Γ (Y) and w_{2} = ∅ ⇒ w_{1} ∈ Γ (X) .

Of course, this satisfies the axiom of hypercoherence.

In that definition, the contrast with coherence spaces appears clearly: as soon as a (finite) subset of |X| + |Y | is such that both of its components are non-empty, it is coherent, whereas in coherence spaces (or qualitative domains), both of its components had to be coherent. This phenomenon has important consequences. Consider for instance the hypercoherence Bool = ({T, F }, {{T }, {F }}). A subset u of |Bool^{3}| = |Bool|×{1, 2, 3} is in Γ^{∗} (Bool^{3}) iff there exist i, j ∈ {1, 2, 3} such that i ≠ j and u_{i} ≠ ∅ and u_{j} ≠ ∅. As a consequence, the set {{(T, 1), (F, 2)}, {(T, 2), (F, 3)}, {(T, 3), (F, 1)}} is in C (Bool^{3}), whereas it is not bounded, and not even pairwise bounded. This is

why the stable but non sequential Berry’s function qD (Bool^{3}) → qD (Bool) whose trace is:

{({(T, 1), (F, 2)}, T), ({(T, 2), (F, 3)}, T), ({(T, 3), (F, 1)}, T)}

will not be in our model (see below). This definition of cartesian product is strongly related to sequentiality.

Proposition 12 Let X and Y be hypercoherences. Then X × Y is the cartesian product of X and Y in the category HCohL.

The proof is straightforward. The projection π_{1} : X × Y −∘ X is {((a, 1), a) | a ∈ |X|}, and similarly for π_{2}. If s : Z −∘ X and t : Z −∘ Y are linear morphisms, their pairing p : Z −∘ X × Y is

p = {(c, (a, 1)) | (c, a) ∈ s} ∪ {(c, (b, 2)) | (c, b) ∈ t} .

Definition 20 Let X and Y be hypercoherences. We call plus of X and Y and note X ⊕ Y the hypercoherence (X^{⊥} × Y^{⊥})^{⊥}.

Proposition 13 If X and Y are hypercoherences, the web of X⊕Y is |X|+|Y | and its atomic coherence is the set of all w ⊆_{fin}^{∗} |X| + |Y | such that

w_{1} = ∅ and w_{2} ∈ Γ (Y) or w_{2} = ∅ and w_{1} ∈ Γ (X) .

Straightforward verification.

Definition 21 Let X be a hypercoherence. We define a hypercoherence !X by setting |!X| = qD_{fin} (X) and by taking for Γ (!X) the restriction of C (X) to qD_{fin} (X). In other words, if A ⊆_{fin}^{∗} qD_{fin} (X), then A ∈ Γ (!X) iff

∀u ⊆_{fin}^{∗} |X| u < A ⇒ u ∈ Γ (X) .

Proposition 14 An element of qD (!X) is a bounded subset of qD_{fin} (X).

Proof: Let A ∈ qD (!X). We can assume that A is finite. Let u ⊆_{fin}^{∗} ⋃ A. Let B = {x ∈ A | u ∩ x ≠ ∅}. Then B ⊆_{fin}^{∗} A, so B ∈ Γ (!X). So u ∈ Γ (X), since u < B by definition of B, and thus ⋃ A ∈ qD (X).

Proposition 15 Let X and Y be hypercoherences. Up to a canonical isomorphism,

!(X × Y) = !X ⊗!Y .

Proof: It is a corollary of the forthcoming proposition 21.

Definition 22 Let X be a hypercoherence. We define the hypercoherence ?X by

?X = (!X^{⊥})^{⊥} .

An element A of P_{fin}^{∗} (qD_{fin} (X^{⊥})) is in Γ^{∗} (?X) iff there exists u ∈ Γ^{∗} (X) such that u < A.

We extend now the operation “!” into a functor HCohL → HCohL and we exhibit the comonad structure of this functor.

Proposition 16 Let X and Y be hypercoherences. Let t ∈ qD (X −∘ Y). Then the set !t defined by

!t = {(x, y) ∈ qD_{fin} (X) × qD_{fin} (Y) | x ⋈ y mod (t)}

is an element of qD (!X −∘ !Y).

Proof: Let U be any non-empty and finite subset of !t. Assume that U_{1} ∈ Γ (!X). Let v ⊆ |Y | be finite, non-empty and such that v < U_{2}. Let

w = {(a, b) ∈ t | b ∈ v and ∃(x, y) ∈ U a ∈ x, b ∈ y} .

Then we have w_{2} = v and w_{1} < U_{1}. Let us just check the second of those statements. If x ∈ U_{1}, let y ∈ U_{2} be such that (x, y) ∈ U. Let b ∈ v be such that b ∈ y. Since x ⋈ y mod (t), we can find some a ∈ x such that (a, b) ∈ t. Clearly, (a, b) ∈ w, so a ∈ w_{1} and we have proven one direction of the statement w_{1} < U_{2}, the second one being a direct consequence of the definition of w.

Since w is finite, non-empty and satisfies w ⊆ t, we have w ∈ Γ (X −∘ Y). But w_{1} ∈ Γ (X) since w_{1} < U_{1} ∈ C (X), and thus w_{2} ∈ Γ (Y), that is v ∈ Γ (Y). This holds for any v < U_{2}, so U_{2} ∈ Γ (!X).

Assume now that #U_{2} = 1, say U_{2} = {y}. Take x_{0} ∈ U_{1}. We prove that for any x ∈ U_{1}, we have x_{0} ⊆ x. This clearly will entail that #U_{1} = 1. Let a_{0} ∈ x_{0}. Let b ∈ y be such that (a_{0}, b) ∈ t. Let

u = {a | (a, b) ∈ t and ∃x ∈ U_{1} a ∈ x} .

One easily checks that u < U_{1}, so u ∈ Γ (X). But u × {b} ⊆ t, so #u = 1, but a_{0} ∈ u, so u = {a_{0}}. Hence, since u < U_{1}, for all x ∈ U_{1} one has a_{0} ∈ x, and we conclude.

Proposition 17 Let X, Y and Z be hypercoherences. Then !Id_{X} = Id_{!X} and if s : X −∘ Y and t : Y −∘ Z then !(t ∘ s) =!t∘!s.

Proof: Let us check that !(t ∘ s) =!t∘!s. First, let (x, z) ∈!(t ∘ s). This means that x ⋈ z mod (t ∘ s). Let

y = {b | ∃a ∈ x ∃c ∈ z (a, b) ∈ s and (b, c) ∈ t} .

We have (x, y) ∈!s and (y, z) ∈!t. Let us prove the first of these statements, the second being similar. Let a ∈ x. Let c ∈ z be such that (a, c) ∈ t ∘ s. Let b be such that (a, b) ∈ s and (b, c) ∈ t. We have b ∈ y by definition of y. Conversely, if b ∈ y, we can find, by definition of y, a a ∈ x such that (a, b) ∈ s. So x ⋈ y mod (s), that is (x, y) ∈!s.

Next, let (x, z) ∈!t∘!s. Let y be such that (x, y) ∈!s and (y, z) ∈!t. Let a ∈ x. Let b ∈ y be such that (a, b) ∈ s. Since y ⋈ z mod (t) we can find a c ∈ z such that (b, c) ∈ t. So we have found a c such that (a, c) ∈ t ∘ s. Conversely, if c ∈ z, we can similarly find a a ∈ x such that (a, c) ∈ t ∘ s, and this concludes the proof.

So now we can consider the operation ! as an endofunctor on HCohL. We show that it has a natural structure of comonad.

Let X be a hypercoherence. Let ε_{X} = {({a}, a) | a ∈ |X|}. It is clear that ε_{X} ∈ qD (!X −∘ X).

Let μ_{X} = {(x, {x_{1}, …, x_{n}}) | x, x_{1}, …, x_{n} ∈ qD_{fin} (X) and ⋃_{i=1}^{n} x_{i} = x}. Let us check that μ_{X} ∈ qD (!X −∘ !!X). Let T ⊆ μ_{X} be finite, non-empty and such that T_{1} ∈ Γ (!X). Let A ⊆ qD_{fin} (X) be such that A < T_{2}. We clearly have A ⊑ T_{1} and thus A ∈ Γ (!X). So T_{2} ∈ Γ (!!X). If furthermore T_{2} is a singleton, then T_{1} is obviously also a singleton.

Proving that ε and μ are the counit and comultiplication of a comonad whose functor is ! is a straightforward verification.

For the notion of comonad, and of co-Kleisli category of a comonad, we refer to [M].

Proposition 18 The co-Kleisli category coKl(!) of the comonad ! is cartesian closed.

Proof: Remember that in this co-Kleisli category, the objects are the hypercoherences, and that a morphism X → Y is a linear morphism !X −∘ Y. If S : X → Y and T : Y → Z are morphisms in coKl(!), their composition T ∘ S : X → Z is given by:

T ∘ S = T ∘!S ∘ μ_{X}

and the identity X → X is simply ε_{X}. Observe that in this last equation, the symbol “∘” has two different meanings: in the left-hand side, it denotes composition in coKl(!), whereas in the right-hand side, it denotes composition in HCohL.

First, this category has products, the product of X and Y being X × Y. For cartesian closedness, let X, Y and Z be hypercoherences. Up to canon-

ical isomorphisms we have, using proposition 15:

(X × Y) → Z = !(X × Y) −∘ Z
= (!X ⊗!Y) −∘ Z
= !X −∘ (!Y −∘ Z)
= X → (Y → Z) .

To be more precise, these equalities correspond to canonical (and thus natural) isomorphisms in HCohL which are easily transfered to coKl(!) using ε.

4 Hypercoherences and strong stability

The purpose of this section is to connect the model we just have presented to the model of (simply typed) λ-calculus presented in [BE]. The section is important because it contains the main intuitions at the origin of the construction of HCohL, and it provides an “abstract” characterization of the morphisms of this category.

Definition 23 The category HCohFS of hypercoherences and strongly stable functions is the category where the objects are the hypercoherences, and where a morphism X → Y is a strongly stable function qDC (X) → qDC (Y).

Proposition 19 The categories coKl(!) and HCohFS are equivalent.

Proof: On objects, this equivalence is simply the identity.

For morphisms, the proposition is mainly a characterization of the traces of strongly stable functions.

If X and Y are hypercoherences, we recall that X → Y denotes the hypercoherence !X −∘ Y.

First, let T ∈ qD (X → Y). We prove that, by setting

f^{T} (x) = {b ∈ |Y | | ∃x_{0} ⊆ x (x_{0}, b) ∈ T }

we define a function qD (X) → qD (Y) that is strongly stable.

Let us prove that if x ∈ qD (X), y = f^{T} (x) ∈ qD (Y). We can assume that x ∈ qD_{fin} (X). Let v ⊆_{fin}^{∗} |Y | be such that v ⊆ y. Let U = {(x_{0}, b) ∈ T | x_{0} ⊆ x and b ∈ v}. We know that U ∈ Γ (X → Y), since U is non-empty and finite. But U_{1} is bounded by x, and thus U_{1} ∈ Γ (!X). Thus U_{2} ∈ Γ (Y). But U_{2} = v and we are finished. So f^{T} is well defined, and Scott continuous by definition.

Let A ∈ C (X). We prove that f^{T} (A) ∈ C (Y). Since f^{T} is continuous, we can assume that any element of A is finite. Let v ⊆_{fin}^{∗} |Y | be such that v < f^{T} (A). Let

U = {(x_{0}, b) ∈ T | ∃x ∈ A x_{0} ⊆ x and b ∈ v} .

Again, U is non-empty and finite, so U ∈ Γ (X → Y). We have U_{1} ⊑ A. Actually, let x ∈ A and let b ∈ v be such that b ∈ f^{T} (x) (such a b can be found since v < f^{T} (A)). Let x_{0} ⊆ x be such that (x_{0}, b) ∈ T. One has x_{0} ∈ U_{1}. So U_{1} ∈ Γ (!X). So U_{2} ∈ Γ (Y), but U_{2} = v and we are finished.

Now, let b ∈ ⋂ f^{T} (A). We want to prove that b ∈ f^{T} (⋂ A). We can assume again that any element of A is finite. Let

A_{0} = {x_{0} | ∃x ∈ A x_{0} ⊆ x and (x_{0}, b) ∈ T } .

A_{0} is finite and satisfies A_{0} ⊑ A, so A_{0} ∈ Γ (!X), but U = A_{0} × {b} ⊆ T, thus U ∈ Γ (X → Y), and thus #A_{0} = 1. Let x_{1} be the unique element of A_{0}, we have x_{1} ⊆ ⋂ A and (x_{1}, b) ∈ T, and we conclude that f^{T} is strongly stable.

Conversely, let f : qD (X) → qD (Y) be strongly stable. We shall prove now that its trace T is in qD (X → Y). Let U ⊆ T be finite, non-empty and such that U_{1} ∈ Γ (!X). We have f(U_{1}) ∈ C (Y) and U_{2} < f(U_{1}), so U_{2} ∈ Γ (Y). Assume furthermore that #U_{2} = 1 and let b be the unique element of U_{2}. We have b ∈ ⋂ f(U_{1}) = f(⋂ U_{1}), so there exists an x_{1} ⊆ ⋂ U_{1} such that (x_{1}, b) ∈ T. But for x_{0} ∈ U_{1}, we have x_{0} ⊇ ⋂ U_{1} ⊇ x_{1} and thus, since f is stable, x_{0} = x_{1}, so U_{1} = {x_{1}} and we conclude that U ∈ Γ (X → Y).

It is fairly obvious that tr (f^{T} ) = T and that f^{tr(f)} = f, since this already holds for stable functions.

It remains to prove that the correspondence we have just established is functorial.

The identity X → X in coKl(!) is ε_{X}, that is {({a}, a) | a ∈ |X|} which clearly is the trace of the identity X → X in HCohFS.

Let S : X → Y and T : Y → Z be morphisms in coKl(!). Remember that T ∘ S = T ∘!S ∘ μ_{X}, that is T ∘ S is the set

\begin{matrix}\{(x, c) | ∃x_{1}, …, x_{n} ∃b_{1}, …, b_{n}, \\ ⋃_{i=1}^{n} x_{i} = x and ∀i (x_{i}, b_{i}) ∈ S and (\{b_{1}, …, b_{n}\}, c) ∈ T \} , \end{matrix}

so if x ∈ qD (X),

f^{T ∘S}(x) = {c | ∃(x_{1}, b_{1}), …, (x_{n}, b_{n}) ∈ S ∀i x_{i} ⊆ x and ({b_{1}, …, b_{n}}, c) ∈ T } , that is f^{T ∘S}(x) = f^{T} (f^{S}(x)).

For the other direction, let f : X → Y and g : Y → Z be morphisms in HCohFS. We have

tr (g ∘ f) = {(x, c) | c ∈ g(f(x)), x minimal}
= {(x, c) | ∃y y ⊆ f(x), (y, c) ∈ tr (g) , x minimal}
= tr (g) ∘ tr (f) (see above the computation of this trace) .

From this result, we deduce that HCohFS is cartesian closed.

Observe now that the stable function G : qD (Bool^{3}) → qD (Bool) whose trace is

{({(T, 1), (F, 2)}, T), ({(T, 2), (F, 3)}, T), ({(T, 3), (F, 1)}, T)}

is not in qD (Bool^{3} → Bool) since the set

{{(T, 1), (F, 2)}, {(T, 2), (F, 3)}, {(T, 3), (F, 1)}}

is in C (Bool^{3}): as we have said before; the Berry’s function is not a morphism in coKl(!).

As a corollary of the previous proposition, we get:

Proposition 20 The category HCohL is equivalent to the category of hypercoherences and linear strongly stable functions.

Proof: Just observe that if X is a hypercoherence, if a_{1}, …, a_{n} ∈ |X|, then {{a_{1}}, …, {a_{n}}} ∈ C (X) iff {a_{1}, …, a_{n}} ∈ Γ (X).

We conclude the section with the proof that the product objects and internal arrow objects in HCohFS are the same as in QDC.

Proposition 21 If X and Y are hypercoherences, then

qDC (X × Y) = qDC (X) × qDC (Y) .

Proof: First, let z ∈ qD (X × Y), and let us prove that z_{1} ∈ qD (X). Let u ⊆ z_{1} be non-empty and finite. We have u × {1} ⊆ z and (u × {1})_{2} = ∅, so u ∈ Γ (X). Similarly z_{2} ∈ qD (Y). The inclusion qD (X) × qD (Y) ⊆ qD (X × Y) is also trivial.

Now let C ∈ C (X × Y), and let us prove that C_{1} ∈ C (X). Let u be finite and non-empty such that u < C_{1}. We have u × {1} < C, and thus u ∈ Γ (X). Similarly for C_{2}.

Finally, let C be in the state coherence of qDC (X) × qDC (Y). Let w be finite and non-empty such that w < C. Assume that w_{2} = ∅. Then certainly w_{1} < C_{1}, so w_{1} ∈ Γ (X), since C_{1} ∈ C (X). Similarly if w_{1} = ∅. So C ∈ C (X × Y).

Proposition 22 If X and Y are hypercoherences, then

qDC (X → Y) = FS (qDC (X), qDC (Y)) .

Proof: In proving proposition 19, we have shown that qDC (X → Y) and FS (qDC (X), qDC (Y)) have the same underlying qD. We prove now that they have the same state coherence.

First, let T ∈ C (X → Y). We want to prove that T is state coherent in FS (qDC (X), qDC (Y)). Let A ∈ C (X) and let E be any pairing of T and A. Let

B = {f^{T} (x) | (T, x) ∈ E} .

We prove that B ∈ C (Y). We can assume that any T ∈ T and any x ∈ A is finite. Let v < B. Let

U = {(x_{0}, b) | ∃(T, x) ∈ E x_{0} ⊆ x and (x_{0}, b) ∈ T and b ∈ v} .

It is clear that U is non-empty and finite. Let T ∈ T . Let x ∈ A be such that (T, x) ∈ E. Let b ∈ v be such that b ∈ f^{T} (x). Let x_{0} ⊆ x be such that (x_{0}, b) ∈ T. We have (x_{0}, b) ∈ U, and thus U < T . Thus U ∈ Γ (X → Y). By the same kind of reasoning, we can check that U_{1} ⊑ A and that U_{2} = v. So v ∈ Γ (Y).

Next we prove that ⋂ B = f^{⋂ T} (⋂ A). Let b ∈ ⋂ B. Let

A_{0} = {x_{0} | ∃(T, x) ∈ E x_{0} ⊆ x and (x_{0}, b) ∈ T } .

Again we can check easily that A_{0} × {b} < T and that A_{0} ⊑ A. So A_{0} is a singleton {x_{1}} and we get x_{1} ⊆ ⋂ A and (x_{1}, b) ∈ ⋂ T , and we are finished.

Finally, let T ⊆ FS (qDC (X), qDC (Y)) be state coherent in that qDC. Let U be finite, non-empty and such that U < T . We want to prove that U ∈ Γ (X → Y), so assume that U_{1} ∈ C (X) and consider the set

E = {(T, x_{0}) ∈ T × U_{1} | ∃b ∈ U_{2} (x_{0}, b) ∈ T ∩ U} .

Clearly E is a pairing of T and U_{1}. Let B = {f^{T} (x_{0}) | (T, x_{0}) ∈ E}. We know that B ∈ C (Y). But U_{2} < B, so U_{2} ∈ Γ (Y). Suppose furthermore that U_{2} is a singleton {b}. We certainly have b ∈ ⋂ B, and thus b ∈ f^{⋂ T} (⋂ U_{1}). So there exists x_{1} ⊆ ⋂ U_{1} such that (x_{1}, b) ∈ ⋂ T . If x_{0} is an element of U_{1}, then (x_{0}, b) ∈ U (since U_{2} = {b}), and thus there is a T ∈ T such that (x_{0}, b) ∈ T (since U < T ). But we have seen that (x_{1}, b) ∈ T and that x_{1} ⊆ x_{0}, so x_{1} = x_{0}, and thus #U_{1} = 1. This achieves the proof of the proposition.

As a corollary, we get:

Proposition 23 The category coKl(!) is (equivalent to) a full sub-cartesian-closed category of QDC.

5 A notion of polarity in hypercoherences

This section contains some simple observations about two subcategories of HCohL. We feel intuitively that these two classes of objects could be connected to Girard’s polarities (cf. [G3]). There remain, however, some mismatches and this intuition could very well be misleading.

Definition 24 A hypercoherence X is positive if Γ (X) is hereditary. It is negative if X^{⊥} is positive.

So a positive hypercoherence can simply be seen as a qualitative domain. There is a very natural direct characterization of negative hypercoherences:

Proposition 24 A hypercoherence X is negative iff Γ^{∗} (X) is antihereditary, that is, if u ∈ Γ^{∗} (X) and if v ⊆_{fin}^{∗} |X| is such that u ⊆ v, then v ∈ Γ^{∗} (X).

The proof is straightforward.

The states of a negative hypercoherence have a very simple structure:

Proposition 25 If X is a negative hypercoherence, then qD (X) is a coherence space.

Proof: Let u ⊆ |X| be such that for all a, a′ ∈ u, {a, a′} ∈ Γ (X). Let v ⊆_{fin}^{∗} u. If #v = 1, then v ∈ Γ (X). Suppose #v > 1. Let a, a′ ∈ v be such that a ≠ a′. Since a, a′ ∈ u, we know that {a, a′} ∈ Γ^{∗} (X). Since X is antihereditary, and since {a, a′} ⊆ v, we have v ∈ Γ^{∗} (X).

Of course, if X is a negative hypercoherence, it is impossible in general to retrieve X from qD (X) (in contrast with what happens for positive hypercoherences). This corresponds to the fact that, in that case, the elements of C (X) are far from being only the bounded elements of P_{fin}^{∗} (qD (X)).

Proposition 26 Let X and Y be hypercoherences.

• If X and Y are positive, then so are X ⊗ Y and X ⊕ Y, and X^{⊥} is negative.

• If X and Y are negative, then so are X℘Y and X × Y, and X^{⊥} is positive.

The proof is straightforward.

Observe that it is almost true that, when X is positive, !X is positive too. However, it is false, because any A ⊆_{fin}^{∗} qD_{fin} (X) such that ∅ ∈ A belongs to Γ (!X), and for such an A, the set A \ {∅} can perfectly well not be in Γ (!X). When A ∈ Γ (!X) is such that ∅ ∉ A, any non-empty subset B of A is in Γ (!X)

(for X positive). Here we have an important mismatch between this notion of polarity and Girard’s; in his framework, !A is always positive, even when A is not.

This remark also suggests that the “of course” connective could be decomposed in two operations: one operation corresponding to contraction, and the other one to weakening. We actually have, up to a canonical isomorphism:

!X = 1 × C(X)

where C(X) is the hypercoherence having qD_{fin} (X) \ {∅} as web, and the restriction of C (X) to this web as coherence. This decomposition is motivated by the fact that the operation X ↦ C(X) maps positive hypercoherences to positive hypercoherences, whereas the operation X ↦ 1 × X maps negative hypercoherences to negative hypercoherences.

Definition 25 The full subcategory of HCohL whose objects are the positive (respectively negative) hypercoherences is denoted by HCohL^{+} (respectively HCohL^{−}).

Now we define two coercions.

Definition 26 Let X be a hypercoherence. Its associated positive hypercoherence is X^{+} defined by |X^{+}| = |X| and

Γ (X^{+}) = {u ∈ Γ (X) | ∀v ⊆_{fin}^{∗} u v ∈ Γ (X)} .

Its associated negative hypercoherence is X^{−} = ((X^{⊥})^{+})^{⊥}.

Clearly, X^{+} is positive and X^{−} negative. By definition of our polarities, X is positive (respectively negative) iff it is equal to X^{+} (respectively X^{−}).

Proposition 27 If X is a hypercoherence, then

Γ^{∗} (X^{−}) = {u ⊆_{fin}^{∗} |X| | ∃v ⊆ u v ∈ Γ^{∗} (X)} .

The proof is a straightforward verification.

So the operation X ↦ X^{+} appears as a restriction of Γ (X), whereas, dually, the operation X ↦ X^{−} is a completion of Γ (X).

Now we prove that the negative and positive coercions are functors that act trivially on morphisms.

Proposition 28 Let X and Y be hypercoherences. If t : X −∘ Y, then t : X^{+} −∘ Y^{+} and t : X^{−} −∘ Y^{−}.

Proof: Let t : X −∘ Y and let w ⊆_{fin}^{∗} t be such that w_{1} ∈ Γ (X^{+}). If #w_{2} = 1, then #w_{1} = 1 because w ⊆_{fin}^{∗} t ∈ qD (X −∘ Y). Let us prove that w_{2} ∈ Γ (Y^{+}). Let v ⊆_{fin}^{∗} w_{2} and let w′ = {(a, b) ∈ w | b ∈ v}. Then w′_{1} ⊆_{fin}^{∗} w_{1}, and thus w′_{1} ∈ Γ (X), and thus, since w′ ⊆_{fin}^{∗} t, we have w′_{2} ∈ Γ (Y), that is v ∈ Γ (Y). Since this holds for any v ⊆_{fin}^{∗} w_{2}, we have w_{2} ∈ Γ (Y^{+}).

To prove that t : X^{−} −∘ Y^{−}, observe that ^{t}t : Y^{⊥} −∘ X^{⊥}, thus ^{t}t : (Y^{⊥})^{+} −∘ (X^{⊥})^{+}, thus ^{t}(^{t}t) : X^{−} −∘ Y^{−}, that is t : X^{−} −∘ Y^{−}.

We shall denote by P the functor HCohL → HCohL^{+} that maps X to X^{+} and t : X −∘ Y to t : X^{+} −∘ Y^{+}, and by N the functor HCohL → HCohL^{−} that maps X to X^{−} and t : X −∘ Y to t : X^{−} −∘ Y^{−}.

Now we prove that these functors have a universal property. Let I^{+} : HCohL^{+} → HCohL and I^{−} : HCohL^{−} → HCohL denote the inclusion functors.

Proposition 29 The functor P is right adjoint to I^{+} and the functor N is left adjoint to I^{−}.

Proof: Let X be a positive hypercoherence and let Y be a hypercoherence. If t : X −∘ Y, we know that t : X^{+} −∘ Y^{+}, that is, since X is positive, t : X −∘ Y^{+}. Conversely, if t : X −∘ Y^{+}, we have t : X −∘ Y simply because Γ (Y^{+}) ⊆ Γ (Y). So we have qD (X −∘ Y) = qD (X −∘ Y^{+}), and the first adjunction holds (in a very strong sense).

Now let X be a hypercoherence and let Y be a negative hypercoherence. We have

t : X −∘ Y  iff ^{t}t : Y^{⊥} −∘ X^{⊥}
iff ^{t}t : Y^{⊥} −∘ (X^{⊥})^{+} since Y is negative
iff t : X^{−} −∘ Y

and we conclude that qD (X −∘ Y) = qD (X^{−} −∘ Y), and the second adjunction holds.

Observe that HCohL^{+} is equivalent to the category of qualitative domains and linear stable functions, and that HCohL^{−} is equivalent to (HCohL^{+})^{op}, this equivalence being defined by the functor ( )^{⊥}, which acts on morphisms by transposition.

6 A connection with the stable model of linear logic

We use CS to denote the category of coherence spaces and linear stable functions, which is the well known model of linear logic discovered by Girard (see [G2]).

Consider the functor PN = P∘N : HCohL → HCohL^{+}. By our previous observations, we can consider this functor as having CS as codomain. Actually, if X is a hypercoherence, PN(X) is the hereditary hypercoherence whose web is |X| and such that u ∈ Γ (PN(X)) iff u ⊆_{fin}^{∗} |X| and for all a, a′ ∈ u, {a, a′} ∈ Γ (X). (See proposition 25.) So PN(X) can be viewed as the coherence space defined by: {a, a′} ∈ PN(X) iff {a, a′} ∈ Γ (X). Furthermore, if t : X −∘ Y is a linear morphism in HCohL, then PN(t) = t.

Now we consider CS as a model of linear logic, with linear connectives interpreted as specified in [G2].

Proposition 30 The functor PN preserves all linear connectives except the exponentials. More precisely, if X and Y are hypercoherences, then PN(X^{⊥}) is the orthogonal of the coherence space PN(X), PN(X ⊗ Y) is the tensor product of the coherence spaces PN(X) and PN(Y), and so on.

Furthermore, there is a natural rigid embedding from PN(!X) into !PN(X) and from PN(?X) into ?PN(X)

Proof: Let {a, a′} ∈ PN(X^{⊥}). This means that {a, a′} ∈ Γ (X^{⊥}), that is a = a′ or {a, a′} ∉ Γ (X), but this exactly means that {a, a′} ∈ PN(X)^{⊥}.

Let {(a, b), (a′, b′)} ∈ PN(X ⊗ Y). This means that {a, a′} ∈ Γ (X) and {b, b′} ∈ Γ (Y) (because any coherent set with two elements or less is hereditary), that is {a, a′} ∈ PN(X) and {b, b′} ∈ PN(Y), that is {(a, b), (a′, b′)} ∈ PN(X) ⊗ PN(Y).

Let {(c, i), (c′, j)} ∈ PN(X ⊕ Y). This means that i = j and that, if i = 1, then {c, c′} ∈ Γ (X), and similarly for Y if j = 2. So we conclude. The fact that the inclusion |PN(!X)| ⊆ |!PN(X)| defines a rigid embedding is a corollary of propositions 14.

For the remainder of the connectives, simply use the De Morgan laws.

It is easy to check that PN is right adjoint to the inclusion functor I^{+} : CS → HCohL.

References

[B1] G. Berry. Modèles des lambda-calculs typés. Thèse de Doctorat, Université Paris 7, 1979.

[B2] G. Berry. Stable Models of Typed Lambda-calculi. Proc. ICALP 1978, Springer-Verlag LNCS 62, 1978.

[BC] G. Berry and P.-L. Curien. Sequential algorithms on concrete data structures. Theor. Comp. Sci. 20, 1982.

[BCL] G. Berry, P.-L. Curien, J.-J. Levy. Full abstraction for sequential languages: the state of the art. French-US Seminar on the Applications of Algebra to Language Definition and Compilation, Fontainebleau (June 1982), Cambridge University Press, 1985.

[BE] A. Bucciarelli, T. Ehrhard. Sequentiality and strong stability. Proc. LICS 1991.

[C] P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Progress in Theoretical Computer Science, Birkhäuser, 1993.

[G1] J.-Y. Girard. The system F of variable types fifteen years later. Theor. Comp. Sci 45, 1986.

[GLT] J.-Y. Girard, Y. Lafont, P. Taylor. Proofs and Types. vol. 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1991.

[G2] J.-Y. Girard. Linear Logic. Theor. Comp. Sci. 50, 1988.

[G3] J.-Y. Girard. A new constructive logic: classical logic. Math. Str. in Comp. Sci. vol. 1.3, 1991.

[KP] G. Kahn and G. Plotkin. Domaines Concrets. Rapport IRIA-LABORIA 336, 1978.

[M] S. MacLane. Categories for the Working Mathematician. Springer-Verlag Graduate Texts in Mathematics vol. 5, 1971.

[P] G. Plotkin. LCF considered as a programming language. Theor. Comp. Sci. 5, 1977.