Bistructures, Bidomains and Linear Logic

Pierre-Louis Curien, LIENS, CNRS–Ecole Normale Supérieure, Paris, France Gordon Plotkin, LFCS, Comp. Sc. Dept., Edinburgh University, Scotland Glynn Winskel, BRICS^{1}, Comp. Sc. Dept., Aarhus University, Denmark

Abstract

Bistructures are a generalisation of event structures which allow a representation of spaces of functions at higher types in an orderextensional setting. The partial order of causal dependency is replaced by two orders, one associated with input and the other with output in the behaviour of functions. Bistructures form a categorical model of Girard’s classical linear logic in which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. The comonad of the model has an associated co-Kleisli category which is closely related to that of Berry’s bidomains (both have equivalent non-trivial full sub-cartesian closed categories).

1 Introduction

In this paper we link Winskel’s bistructures [25], Girard’s linear logic [10] and Berry’s bidomains [25]. We show how bistructures provide a model of classical linear logic extending Girard’s web model [10, 11]; we show too that a certain class of bistructures represent bidomains. We hope that the structures isolated here will help in the search for a direct, extensional and “mathematically natural” account of sequentiality and thereby of Milner’s fully abstract model of PCF [20].

Girard has given an analysis of intuitionistic logic in terms of his more primitive linear logic. When we consider models, this is reflected in the fact that cartesian closed categories (categorical models of intuitionistic logic) arise as the co-Kleisli categories associated with categorical models of linear logic. In particular, linear logic yields refined analyses of the categories of domains used in denotational semantics. For instance, Berry and Curien’s category of concrete data structures and sequential algorithms [5] may be obtained as the co-Kleisli category of a games model [6, 16]. The connection between games and sequentiality has in turn informed recent work on intensional models of PCF and their fully-abstract extensional collapse [1, 12].

1Basic Research in Computer Science, Centre of the Danish National Research Foundation.

After Berry isolated the mathematically natural notion of stability [3], it was soon realized that sequential functions are stable. While there is a cartesian closed category of stable functions, at higher orders the extensional ordering is not respected. It was therefore natural for Berry to introduce bidomains. These are biorders—that is, sets equipped with two partial orders. One is an intensional stable ordering, based on the method of computation; the other is an extensional ordering, inherited from Scott’s domain theory. Models of this kind can be viewed as mathematically tractable “approximations” to the desired sequential structures.

Event structures are partial orders of events equipped with a conflict relation and obeying an axiom of finite causes. They were introduced in [21] as a model of concurrency, and turned out to have close connections with concrete domains [14] and hence sequentiality [5]; they are also a natural generalisation of Girard’s webs. Winskel introduced bistructures (of events) in [25], representing a full sub-cartesian closed category of bidomains. They are biorders equipped with a binary consistency relation; the two orders are obtained by decomposing the event structure order into left and right (input and output) components.

The main idea of this paper is that the inherent symmetry of bistructures enables one to obtain a model of classical linear logic, generalising the web model. The model is obtained by modifying the original definition—retaining its axiom of finite causes, but with all axioms symmetric. The configurations of a bistructure can be equipped with both a stable and an extensional ordering, that is they are biorders; further, the morphisms of the category of bistructures yield linear functions of the biorders (in a certain sense). Unfortunately not all biorders obtained in this way are bidomains; further not all linear functions come from morphisms of bistructures.

However by considering the co-Kleisli category and then restricting the allowed bistructures, one obtains a category equivalent to a full sub-cartesian closed category of Berry’s category of bidomains and which provides a model of PCF. It has to be admitted that the situation here is not entirely as one would like: perhaps the notions of bistructures and bidomains should be adjusted. Ideal would be to have a bidomain model of classical linear logic, with a co-Kleisli category equivalent to that of stable continuous functions, and containing a (full) submodel equivalent to one of bistructures; further, there should be a representation theorem, that the bidomains corresponding to bistructures are precisely those satisfying suitable axioms.

It may be that a natural extensional account of sequentiality can be given within a “bistructural” framework. One can imagine replacing the stable ordering by a structure for sequentiality. If one does not know the right axioms, one could instead look for suitable variants of bistructures of events.

However, Loader’s undecidability result [19] for the finitary fragment of PCF shows that there is a major obstacle to finding a category of structured sets providing a fully abstract model of PCF. Such a category cannot be “finitary,” in a certain sense.^{2} It may nonetheless be possible to find suitable infinitary structure. The work in this paper suggests that one might do well to seek linear models whose co-Kleisli categories correspond to the sequential functions. There may even be enough symmetry that one has a model of classical linear logic.

In Sections 2 and 3 we give two approaches to bistructures; these represent two independent developments of the ideas of this paper [23, 7]. Section 2 starts from the world of webs and stable domain theory; Section 3 proceeds from that of event structures and continuous domain theory. We introduce bistructures in Section 4, and bistructure morphisms in Section 5. In Section 6 we show (Theorem 1) that bistructures provide a model of classical linear logic. In Section 7 we consider bidomains, establishing the connection with bistructures (Theorem 2). In Section 8 we discuss possible variations and connections with other work; in particular we consider strengthenings of bistructures incorporating Ehrhard’s hypercoherences (see [8]) thereby accounting for strong stability within our approach.

In this paper, cpos are partial orders with a least element and lubs of all directed sets; continuous functions between cpos are those monotonic functions preserving all the directed lubs. For other domain-theoretic terminology see, for example, [28].

2The categories of partial orders and topological spaces are finitary, but structures involving reference to the natural numbers, e.g., measure spaces, are not. The notion can be formalised; one requires that the structures, morphisms and product and function-space functors are given by formulas of higher-order logic referring only to the carrier sets, in such a way that the structured set corresponding to the Booleans has finite carrier, and the function space construction preserves finiteness of the carriers.

2 Motivation from stability

We recall the basics of Girard’s stable model of classical linear logic [10, 11]. A web is a structure (E, ⌣), where:

• E is a set of events (or tokens), and

• ⌣ is a binary irreflexive symmetric relation of conflict (called strict incoherence in [10]).

Throughout this paper we use Girard’s notation: ⌣ ⌢ is the reflexive closure of the irreflexive relation ⌣, and ⌢ ⌣, the complement of ⌣, is the reflexive closure of the irreflexive relation ⌢. It is clear that specifying one relation determines all the others.

The configurations (called cliques in [10]) of (E, ⌣) are the subsets x ⊆ E which are

• consistent: ∀ e, e′ ∈ x e ⌢ ⌣ e′.

Ordered by inclusion, the configurations of E form a cpo (Γ(E), ⊆); as a collection of sets, Γ(E) is a coherence space in the sense of [10, 11]. The webs form a category, taking the morphisms from E_{0} to E_{1} to be the stable functions from Γ(E_{0}) to Γ(E_{1}), i.e., those continuous functions f such that whenever e_{1} ∈ f(x) there is a minimum finite x_{0} ⊆ x such that e_{1} ∈ f(x_{0}). In this setting, the stable functions coincide with the conditionally multiplicative functions, i.e., the continuous functions that preserve binary compatible glbs (which are, categorically speaking, pullbacks).

The category is cartesian closed: the function space E_{0} → E_{1} has as events the pairs (x, e_{1}) of a finite configuration of E_{0} and an event of E_{1}, with incoherence defined by:

(x, e_{1}) ⌣ ⌢ (y, e′_{1}) ⇔ (x ↑ y) and (e_{1} ⌣ ⌢ e′_{1})

where x ↑ y means ∃ z x, y ⊆ z. The configurations of E_{0} → E_{1} are in 1-1 correspondence with the morphisms from E_{0} to E_{1}, associating to each stable function f its trace tr(f), consisting of those pairs (x, e_{1}) such that e_{1} ∈ f(x) and e_{1} ∉ f(y) if y ⊂ x. The inclusion of configurations determines an ordering on stable functions, refining the pointwise ordering and called the stable ordering [2].

The definition of E_{0} → E_{1} is asymmetric in that configurations are paired with events, rather than events with events. This led Girard to two successive decompositions, each of which turned out to have deep logical significance.

• First, E_{0} → E_{1} can be obtained as (!E_{0}) E_{1}, where, for any E, the web !E (the exponential of E, pronounced “bang E”) has as events the finite configurations of E (with ⌢ ⌣ = ↑), and where, for any E_{0}, E_{1}, the web E_{0} E_{1}, the linear function space, has as events pairs (e_{0}, e_{1}) of events of E_{0} and events of E_{1}, with incoherence defined by:

(e_{0}, e_{1}) ⌣ ⌢ (e′_{0}, e′_{1}) ⇔ (e_{0} ⌢ ⌣ e′_{0}) and (e_{1} ⌣ ⌢ e′_{1})

• Second, the remarkable symmetry between ⌢ ⌣ and ⌣ ⌢ in the definition of E_{0} E_{1} leads to the decomposition E_{0} E_{1} = (E_{0}^{⊥}) ℘ E_{1}, where, for any E, the web E^{⊥}, the linear negation of E, has the same events as E, but has as coherence the incoherence of E, and where, for any E_{0}, E_{1}, the web E_{0} ℘ E_{1} (the “par” of E_{0} and E_{1}) has as events the pairs (e_{0}, e_{1}) of an event of E_{0} and an event of E_{1}, with incoherence defined by:

(e_{0}, e_{1}) ⌣ ⌢ (e′_{0}, e′_{1}) ⇔ (e_{0} ⌣ ⌢ e′_{0}) and (e_{1} ⌣ ⌢ e′_{1})

Returning to the consideration of stable functions, let us see how to describe the pointwise order between stable functions at the level of traces. In E_{0} → E_{1} there arises a natural ordering between events (x, e_{1}) if we vary only the input x (whence the superscript ^{L}, for “left”):

(x, e_{1}) ≤^{L} (y, e′_{1}) ⇔ (y ⊆ x and e_{1} = e′_{1})

Now define a partial order ⊑ on Γ(E_{0} → E_{1}) by:

ϕ ⊑ ψ ⇔ ∀ (x, e_{1}) ∈ ϕ ∃ y ⊆ x (y, e_{1}) ∈ ψ

or, equivalently:

ϕ ⊑ ψ ⇔ ∀ e ∈ ϕ ∃ e′ ∈ ψ e ≤^{L} e′

Then it is easy to see that for any two stable functions f, g:

(∀ x f(x) ⊆ g(x)) ⇔ tr(f) ⊑ tr(g)

Since the stable ordering is a refinement of the pointwise ordering, it makes sense to ask whether there exists a sensible “complement” of the stable ordering. Indeed we shall see in Proposition 1 that we can always factor ϕ ⊑ ψ uniquely as ϕ ⊑^{L} χ ⊆ ψ. Here ϕ ⊑^{L} χ means that ϕ ⊑ χ and χ is minimal with respect to inclusion (i.e., the stable ordering) among all χ′ such that ϕ ⊑ χ′; in other words, χ is “the part of ψ showing that ϕ ⊑ ψ” (notice that, given (x, e_{1}), the y in the definition of ϕ ⊑ ψ is unique).

So far, our discussion has been implicitly carried at first-order types, where we have stable functions that can be ordered in two ways (⊆ and ⊑). If we next consider second-order types, or functionals, the explicit consideration of both the pointwise and the stable orderings at first-order types leads us to focus on functionals that are not only stable with respect to the stable ordering, but also monotonic with respect to the pointwise ordering. That is, we want to retain only those stable functionals H from Γ(E_{0} → E_{1}) to Γ(E_{2}) such that:

∀ ϕ, ψ (ϕ ⊑ ψ ⇒ H(ϕ) ⊆ H(ψ))

(where we now freely confuse functions with their traces), which, by the ⊆-monotonicity of H and the definition of ⊑^{L}, can be rephrased as:

∀ ϕ, ψ (ϕ ⊑^{L} ψ ⇒ H(ϕ) ⊆ H(ψ))

Now, specialising to finite ϕ and ψ, suppose that (ϕ, e_{2}) ∈ H. Then we must have that e_{2} ∈ H(ψ), i.e., there must exist (ψ_{0}, e_{2}) in H such that ψ_{0} ⊆ ψ. Therefore we ask for the following condition, called the securedness condition:

∀ e ∈ H ∀ e′ (e′ ≤^{R} e ⇒ ∃ e′′ ∈ H e′ ≤^{L} e′′)

where the order ≤^{R} is defined by

(ψ, e′_{2}) ≤^{R} (ϕ, e_{2}) ⇔ (ϕ ⊑^{L} ψ and e′_{2} = e_{2})

To summarise, by going from base types successively to first-order and then

to second-order types, we have identified two orderings on events.

• The ≤^{L} ordering allows us to describe the extensional ordering between traces.

• The securedness condition, which involves both orderings ≤^{L} and ≤^{R}, allows us to capture the preservation of this extensional ordering by functionals.

This suggests that we consider structures (E, ≤^{L}, ≤^{R}, ⌢ ⌣), where (E, ⌢ ⌣) is a web, with the aim of building a cartesian closed category of biordered domains (cf. the introduction), and, as it turns out, a model of classical linear logic.

3 Motivation from continuity

In event structures (which predate Girard’s webs), a causal dependency relation inspired from Petri net theory is considered in addition to the conflict relation [21]. In full, an event structure is a structure (E, ≤, ⌣) where ^{3} :

• E is a set of events,

• ≤ is a partial order of causal dependency, and

• ⌣ is a binary, irreflexive, symmetric relation of conflict.

The configurations (or states) of such an event structure are those subsets x ⊆ E which are:

• consistent: ∀ e, e′ ∈ x e ⌢ ⌣ e′, and

• left closed: ∀ e, e′ ∈ E e′ ≤ e ∈ x ⇒ e′ ∈ x.

Ordered by inclusion, the configurations form a coherent prime algebraic domain (Γ(E), ⊆) [21]; such domains are precisely the infinitely distributive, coherent Scott domains [27]. An instance of the causal dependency ordering e′ ≤ e when e and e′ are distinct, is understood as meaning that the event e causally depends on the event e′, in that the event e can only occur after e′ has occurred. Given this understanding it is reasonable to impose a finiteness axiom, expressing that an event has finite causes:

{e′ | e′ ≤ e} is finite, for all events e.

The event structures satisfying this axiom yield the dI-domains [2] which are coherent, and therefore lead to a cartesian closed category of stably ordered stable functions. (See [26] where an alternative description of event structures using an enabling relation instead of an ordering on events is used to give a simple description of the function space construction.)

3In [21], an axiom relating causal dependency and conflict is imposed; however it is inessential in that it does not affect the class of domains represented.

But event structures can also be used to describe a continuous model of intuitionistic linear logic, equivalent to the category of coherent prime algebraic domains, with completely additive functions (i.e., functions preserving arbitrary lubs—just called “additive” below). We take as objects event structures (but without the axiom of finite causes: this is the price to pay), and as morphisms configurations of a “function space” of event structures. Let E_{i} = (E_{i}, ≤_{i}, ⌣_{i}), i = 0, 1, be event structures. Define:

E_{0} E_{1} = (E_{0} × E_{1}, ≤, ⌣)
where (e_{0}, e_{1}) ≤ (e′_{0}, e′_{1}) ⇔ e′_{0} ≤_{0} e_{0} and e_{1} ≤_{1} e′_{1},
and (e_{0}, e_{1}) ⌣ (e′_{0}, e′_{1}) ⇔ e_{0} ⌢ ⌣_{0} e′_{0} and e_{1} ⌣_{1} e′_{1}.

The configurations of E_{0} E_{1} are in 1-1 correspondence with the additive functions from Γ(E_{0}) to Γ(E_{1})—additive functions are determined by their action on complete primes^{4} which correspond to events. The configuration associated with an additive function f is its graph, consisting of those pairs (e_{0}, e_{1}) such that e_{1} ∈ f({e′_{0} | e′_{0} ≤ e_{0}}).

The inclusion ordering on configurations reflects the pointwise ordering on functions; in particular, the function events (e_{0}, e_{1}) correspond to the prime additive one-step functions (see [31]); and the order ≤ to the pointwise order between them.

A morphism E_{0} → E_{1} is defined to be a configuration of E_{0} E_{1}. As such it is a relation between the events of E_{0} and E_{1}. Composition in the category is that of relations. The category is a model of intuitionistic linear logic, as defined in [24, 4]. For instance, its tensor is given in a coordinatewise fashion. For event structures E_{i} = (E_{i}, ≤_{i}, ⌣_{i}), for i = 0, 1, define:

E_{0} ⊗ E_{1} = (E_{0} × E_{1}, ≤, ⌣)
where (e_{0}, e_{1}) ≤ (e′_{0}, e′_{1}) ⇔ e_{0} ≤_{0} e′_{0} and e_{1} ≤_{1} e′_{1},
and (e_{0}, e_{1}) ⌢ ⌣ (e′_{0}, e′_{1}) ⇔ e_{0} ⌢ ⌣_{0} e′_{0} and e_{1} ⌢ ⌣_{1} e′_{1}.

4A complete prime of a Scott domain (D, ⊑) is an element p for which whenever X is bounded above and p ⊑ ⨆ X then p ⊑ x for some x in X. Complete primes are a fortiori compact, where the definition of compact is obtained by replacing “X is bounded above”

by “X is directed”.

Monoidal-closure follows from the isomorphism

(E_{0} ⊗ E_{1} E_{2}) ≅ (E_{0} (E_{1} E_{2}))

natural in E_{0} and E_{2}. Product and coproduct are obtained by disjoint juxtaposition of event structures, extending conflict across the two event sets in the case of coproduct. The comonad operation is:

!E = (Γ(E)^{0}, ⊆, ⌣)

for an event structure E, with events the compact configurations Γ(E)^{0}, and where ⌣ stands for incompatibility with respect to inclusion. The continuous functions Γ(E_{0}) → Γ(E_{1}), between configurations of event structures E_{0}, E_{1}, are in 1-1 correspondence with the configurations of !E_{0} E_{1}.

Notice that this does not yield a model of classical linear logic. The reader should compare the asymmetric definition of conflict in E_{0} E_{1} given above to capture continuity with the symmetric definition of incoherence in the stable framework (cf. Section 2).

Moreover, in this model of intuitionistic linear logic, all hope of considering the order ≤ as causal dependency is lost. The difficulty stems from the definition of the order ≤ for (E_{0} E_{1}). Its events are ordered by:

(e_{0}, e_{1}) ≤ (e′_{0}, e′_{1}) ⇔ e′_{0} ≤_{0} e_{0} and e_{1} ≤_{1} e′_{1}

The reversal in the ≤_{0} order can lead to ≤ violating the axiom of finite causes, even though ≤_{0} and ≤_{1} do not: an infinite, ascending chain of events in E_{0} can give rise to an infinite, descending chain in E_{0} E_{1}. Of course, there is no reason why the extensional ordering on functions should be a relation of causal dependency, so it was not to be expected that its restriction to step functions should be finitary.

However, if we factor ≤ into two orderings, one associated with input (on the left) and one with output (on the right), we can expose two finitary orderings. Define

\begin{aligned}(e_{0}, e_{1}) ≤^{L} (e′_{0}, e′_{1}) & ⇔ e′_{0} ≤_{0} e_{0} and e_{1} = e′_{1}, \\ (e_{0}, e_{1}) ≤^{R} (e′_{0}, e′_{1}) & ⇔ e′_{0} = e_{0} and e_{1} ≤_{1} e′_{1}. \end{aligned}

Then, it is clear that ≤ factors as

(e_{0}, e_{1}) ≤ (e′_{0}, e′_{1}) ⇔ (e_{0}, e_{1}) ≤^{L} (e′_{0}, e_{1}) and (e′_{0}, e_{1}) ≤^{R} (e′_{0}, e′_{1}),

and that this factorisation is unique. Provided the orderings of E_{0} and E_{1} are finitary, then so are ≤^{R} and ≥^{L}. This factorisation is the first step towards the definition of bistructures. To indicate its potential, and to further motivate bistructures, we study a simple example.

Let E_{0} and E_{1} be the event structures shown below. Both have empty conflict relations. Taking advantage of the factorisation we have drawn them alongside the additive function space E_{0} E_{1}.

[figure: L; L; L; L; L; L; L; L; L; L; L; L; R; R; R; R; R; R; R; R; c; d; a; b; E_{0}; e; f; g; E_{1}]

The conflict relation of E_{0} E_{1} is empty. So here an additive function from Γ(E_{0}) to Γ(E_{1}) is represented by a ≤-downwards-closed subset of events of E_{0} E_{1}. For instance, the events in the diagram (below left) are associated with the function that outputs e on getting input event a, outputs f for input b or c, and outputs g for input d. The extensional ordering on functions corresponds to inclusion on ≤-downwards-closed subsets of events. It is clear that such a function is determined by specifying the minimal input events which yield some specific output (shown in the diagram below right). This amounts to the subset of ≤^{L}-maximal events of the function, and we can call this subset the trace of the function. Notice, though, that this particular function is not stable; output f can be obtained for two non-conflicting but distinct events b and c. A stable function should not have ≤^{L}-downwards compatible distinct events in its trace.

[figure: ⊙; ⊙; ⊙; ⊙; ⊙; ⊙; ⊙; ⊙; ⊙; ⊙; ⊙; ⊙]

For stable functions, the stable ordering is obtained as inclusion of traces. For example:

[figure: ⊙; ⊙; is stable below; ⊙; ⊙; ⊙]

Notice that traces ϕ of additive functions from from Γ(E_{0}) to Γ(E_{1}) are secured, in the sense that:

(e ∈ ϕ and e′ ≤^{R} e) ⇒ (∃ e′′ ∈ ϕ e′ ≤^{L} e′′)

or more concretely:

((e_{0}, e_{1}) ∈ ϕ and e′_{1} ≤ e_{1}) ⇒ (∃ e′_{0} (e′_{0}, e′_{1}) ∈ ϕ and e′_{0} ≤ e_{0})

This is the same securedness condition that appeared in Section 2. Here we can understand the condition as saying that for any output, lesser output must arise through the same or lesser input.

Let us summarise this discussion.

• The graphs of additive functions are the ≤-downwards-closed, consistent subsets of events.

• The extensional order corresponds to inclusion of graphs.

• The traces of functions are the sets of ≤^{L}-maximal events of their graphs.

• The stable order corresponds to inclusion of traces.

These observations, based on the continuous model construction, will, as it turns out, also make sense in a biordered framework. They encourage us to consider bistructures (E, ≤^{L}, ≤^{R}, ⌢ ⌣) and provide guidance as to which axioms we should impose on ≤^{L},≤^{R}, and ⌢ ⌣. One expects a function-space construction that maintains both stable and extensional orderings, corresponding to taking as morphisms those functions which are continuous with respect to the extensional ordering and stable with respect to the stable ordering.

We end the section with a remark. One might wonder why we have explicitly considered an ordering ≤ on events to describe a cartesian closed category of continuous functions, while webs suffice for the purpose of building a cartesian closed category of stable functions. The reason is that the treatment of stability is based on traces of functions, while the treatment of continuity is based on their graphs. Graphs of continuous functions ^{5} are upwards closed in their first component, even if the underlying event structure has a trivial partial order, and we need an order relation on events to capture that fact.

4 Bistructures

The following definition of bistructures allows us to fulfill the hopes expressed in the previous sections.

Definition 1 A (countable) bistructure is a structure (E, ≤^{L}, ≤^{R}, ⌢ ⌣) where E is a countable set of events, ≤^{L}, ≤^{R} are partial orders on E and ⌢ ⌣ is a binary reflexive, symmetric relation on E such that:

5The graph of a continuous function f from Γ(E_{0}) to Γ(E_{1}) consists of all pairs (x, e_{1})

with x compact such that e_{1} ∈ f(x).

1. defining ≤= (≤^{L} ∪ ≤^{R})^{⋆}, we have the following factorisation property:

e ≤ e′ ⇒ ∃ e′′ e ≤^{L} e′′ ≤^{R} e′

2. defining ⪯= (≥^{L} ∪ ≤^{R})^{⋆},

(a) ⪯ is finitary, i.e., {e′ | e′ ⪯ e} is finite, for all e,

(b) ⪯ is a partial order;

3. (a) ↓^{L} ⊆ ≍ (b) ↑^{R} ⊆ ⌢ ⌣

The two compatibility relations are defined by:

e ↓^{L} e′ ⇔ ∃ e′′ e′′ ≤^{L} e and e′′ ≤^{L} e′,
e ↑^{R} e′ ⇔ ∃ e′′ e ≤^{R} e′′ and e′ ≤^{R} e′′.

Notice the symmetry of the axioms. They are invariant under the “duality”:

≤^{L} ↦ ≥^{R},
≤^{R} ↦ ≥^{L},
⌢ ⌣ ↦ ⌣ ⌢

which is why we obtain a model of the classical logic. Bistructures of the form (E, id_{E}, ≤, ⌢ ⌣), i.e., such that the ≤^{L} order is degenerate, are essentially the ordinary, countable event structures, (E, ≤, ⌣), satisfying the axiom of finite causes. We say “essentially” because Axiom 3(b) is not part of the above definition of event structure, but does not restrict the class of domains represented.

Remark 1 In the presence of Axiom 2(a), Axiom 2(b) is equivalent to requiring that e ≺ e′ is well-founded, where e ≺ e′ means e ⪯ e′ and e ≠ e′.

The axioms of bistructures are strong enough to imply the uniqueness of the decomposition of ≤= (≤^{L} ∪ ≤^{R})^{⋆}, and also that ≤ is a partial order.

Lemma 1 Let E be a bistructure. The following properties hold, for all e, e′ in E:

\begin{aligned}(e ↓^{L} e′ and e ↑^{R} e′) & ⇒ & e = e′, \\ e ≤ e′ & ⇒ & ∃!e′′ e ≤^{L} e′′ ≤^{R} e′ \end{aligned}

Proof. (1) If e ↓^{L} e′ and e ↑^{R} e′, then e ⌣ ⌢ e′ and e ⌢ ⌣ e′, which implies e = e′ by definition of ⌣ ⌢.

(2) Suppose that e ≤^{L} e′′ ≤^{R} e′ and e ≤^{L} e′′′ ≤^{R} e′. Then e′′ ↓^{L} e′′′ and e′′ ↑^{R} e′′′, therefore e′′ = e′′′ by (1). □

The unique factorisation property enables a diagrammatic style of proof.

Lemma 2 The relation ≤ defined in Axiom 1 of bistructures is a partial order.

Proof. The relation ≤ is certainly reflexive and transitive. With the aim of proving antisymmetry, suppose e ≤ e′ and e′ ≤ e. Then pictorially by factorising ≤, for some events ε and ε′, we have:

[figure: \begin{matrix}ε & e_{′} \\ e & ε_{′} \end{matrix}; R; L; L; R]

From

[figure: \begin{matrix}ε & e_{′} \\ e & ε_{′} \end{matrix}; L; L; R]

we know e ≤ ε. Thus by factorising e ≤ ε we get e ≤^{L} ε′′ ≤^{R} e, for some ε′′:

[figure: \begin{aligned}& ε \\ ε_{′′} & e \end{aligned}; R; R; L]

But e ≤^{L} e ≤^{R} e so the uniqueness of factorisation gives e = ε′′. Then as ≤^{R} is a partial order e = ε. Therefore the first picture collapses to:

[figure: \begin{aligned}& e′ \\ e & ε_{′} \end{aligned}; L; L; R]

The uniqueness of the factorisation of e′ ≤ e′ gives ε′ = e′, so as ≤^{L} is a partial order, e = e′, as required. □

As with Girard’s webs, bistructures provide a concrete level of description of abstract points, or configurations, which we define next.

Definition 2 A configuration of a bistructure (E, ≤^{L}, ≤^{R}, ⌢ ⌣) is a subset x ⊆ E which is:

• consistent: ∀ e, e′ ∈ x e ⌢ ⌣ e′, and

• secured: ∀ e ∈ x ∀ e′ ≤^{R} e ∃ e′′ ∈ x e′ ≤^{L} e′′.

[Notice that e′′ is unique in any consistent set because of Axiom 3(a) on bistructures.] Write Γ(E) for the set of configurations of a bistructure E, and Γ(E)^{0} for the set of finite configurations (see Proposition 2).

When ≤^{L}= id, the securedness condition amounts to ≤^{R}-downwards-closure, hence in that case configurations are just the configurations of the underlying event structure (E, ≤^{R}, ⌣).

Definition 3 Let E be a bistructure. We define the stable ordering ⊑^{R} and the extensional ordering ⊑ on configurations by:

⊑^{R} is set-theoretic inclusion, x ⊑ y ⇔ ∀ e ∈ x ∃ e′ ∈ y e ≤^{L} e′

It follows from these definitions and from the reflexivity of ≤^{L} that ⊑^{R} is included in ⊑. We define a third relation ⊑^{L} as follows:

x ⊑^{L} y ⇔ x ⊑ y and (∀ z ∈ Γ(E) (x ⊑ z and z ⊑^{R} y) ⇒ y = z)

Thus, x ⊑^{L} y means that y is a ⊑^{R}-minimal configuration such that x ⊑ y. Write x ↑^{R} y for (∃ z ∈ Γ(E) x, y ⊑^{R} z).

Thus bistructures E yield biorders (Γ(E), ⊑^{R}, ⊑); some of their properties are examined in the rest of this section. In particular, Proposition 1 concerns factorisation—preparing the ground for the definition of exponentials in Section 6, while Propositions 2 and 3 concern finiteness and completeness properties.

Lemma 3 Let E be a bistructure, and suppose that x, y are in Γ(E). If x ↑^{R} y, e ∈ x, e′ ∈ y, and e ↓^{L} e′, then e = e′.

Proof. Let z be such that x ⊑^{R} z and y ⊑^{R} z. Then we have that e ∈ z and e′ ∈ z, hence e ⌢ ⌣ e′. On the other hand, by Axiom 3(a) we find that e ⌣ ⌢ e′, hence e = e′. □

Lemma 3 has two interesting consequences.

• If x is a configuration and e ∈ x, then e is ≤^{L}-maximal in x.

• If x ↑^{R} y, then the set intersection x ∩ y is the glb of x and y with respect to both ⊑^{R} and ⊑.

Lemma 4 Let E be a bistructure, and suppose that x ∈ Γ(E). If e is in the ≤-downwards-closure of x, then it is in the ≤^{L}-downwards-closure of x.

Proof. Let e′ in x be such that e ≤ e′:

∃ e′′ e ≤^{L} e′′ ≤^{R} e′ by factorisation,
∃ e′′′ ∈ x e′′ ≤^{L} e′′′ by securedness

Then e ≤^{L} e′′′, which completes the proof. □

It follows from Lemma 4 that the relation ⊑ is equivalently defined by stating that the ≤-downwards-closure of x is included in the ≤-downwards-closure of y. This characterisation is in accordance with the discussion in Section 3: compare ⊑^{R} and ⊑ with graph and trace inclusion, respectively.

Definition 4 For x in Γ(E), we define the relativised relation ⪯_{x} as the reflexive, transitive closure of ⪯_{x}^{1} where:

e ⪯_{x}^{1} e′ ⇔_{def} e ∈ x and e′ ∈ x and ∃ e′′ e ≥^{L} e′′ ≤^{R} e′.

Lemma 5 Let E be a bistructure. The following property holds, for all x, y in Γ(E):

(x ↑^{R} y and e ∈ x ∩ y) ⇒ (∀ e′ ∈ E e′ ⪯_{x} e ⇔ e′ ⪯_{y} e)

Proof. It is clearly enough to show this for the one step relations ⪯_{x}^{1} and ⪯_{y}^{1}. Suppose e′ ⪯_{x}^{1} e, and let e′′ be such that e′ ≥^{L} e′′ ≤^{R} e. Since y is secured, and since e ∈ y, there exists e′′′ in y such that e′′ ≤^{L} e′′′. By Lemma 3 applied to x, y, e′, and e′′′, we get e′ = e′′′. Hence e′ = e′′′ ⪯_{y} e. □

Proposition 1 Let ⊑^{R}, ⊑, and ⊑^{L} be the relations on configurations defined above. The following properties hold:

1. ⊑ is (⊑^{L} ∪ ⊑^{R})^{⋆}, and satisfies Axiom 1,

2. for all configurations x, y:

x ⊑^{L} y ⇔ (x ⊑ y and ∀ e ∈ y ∃ e_{0} ∈ x, e_{1} ∈ y e ⪯_{y} e_{1} ≥^{L} e_{0})

3. ⊑^{L} is a partial order, and

4. for all configurations x, y with x ⊑ y there is a unique z such that x ⊑^{L} z ⊑^{R} y.

Proof. (1) Suppose x ⊑ y. The subset {e_{1} ∈ y | ∃ e_{0} ∈ x e_{0} ≤^{L} e_{1}} represents the part of y actually used to check x ⊑ y. But we have to close this subset to make it secured. Thus define:

y_{1} = {e ∈ y | ∃ e_{0} ∈ x, e_{1} ∈ y e ⪯_{y} e_{1} ≥^{L} e_{0}}

By construction, this set satisfies the following property: If e ∈ y_{1} and e′ ⪯_{y} e, then e′ ∈ y_{1}. We show that y_{1} is a configuration. It is clearly consistent, as it is a subset of y. If e ∈ y_{1} and e_{1} ≤^{R} e, since y is secured, there exists e_{2} in y such that e_{1} ≤^{L} e_{2}, and e_{2} ∈ y_{1} by construction. Thus y_{1} is a configuration. We show x ⊑^{L} y_{1}. Suppose that x ⊑ y′_{1} ⊑^{R} y_{1}, and let e be an element of y_{1}. By the construction of y_{1}, there are e_{0} in x and e_{1} in y such that e ⪯_{y} e_{1} ≥^{L} e_{0}. Since x ⊑ y′_{1}, e_{0} ≤^{L} e′_{1} for some e′_{1} in y′_{1}. Applying Lemma 3 to y, y′_{1}, e_{1}, and e′_{1}, we get e_{1} = e′_{1}, hence e_{1} ∈ y′_{1}, which implies e ∈ y′_{1} by Lemma 5. Therefore y_{1} ⊑^{R} y′_{1}, which completes the proof that x ⊑^{L} y_{1}. The decomposition x ⊑^{L} y_{1} ⊑^{R} y shows that ⊑ is contained in (⊑^{L} ∪ ⊑^{R})^{⋆}. The converse inclusion is obvious.

(2) follows immediately from the proof of (1).

(3) Reflexivity and antisymmetry follow from the inclusion of ⊑^{L} in ⊑. Suppose that x ⊑^{L} y′ ⊑^{L} y. Clearly x ⊑ y, so with an eye to using (2) to show x ⊑^{L} y suppose e ∈ y. By (2), there exist e_{0} in y′, e_{1} in y, e′_{0} in x and e′_{1} in y′ such that

\begin{matrix}e_{0} ≤^{L} e_{1} and e ⪯_{y} e_{1}, \\ e′_{0} ≤^{L} e′_{1} and e_{0} ⪯_{y′} e′_{1}. \end{matrix}

Or in full:

e_{0} ≤^{L} e_{1} ≥^{R} e_{2} ⋯ ≤^{L} e_{2i+1} = e with e_{2j+1} ∈ y for all 0 ≤ j ≤ i,
e′_{0} ≤^{L} e′_{1} ≥^{R} e′_{2} ⋯ ≤^{L} e′_{2i′+1} = e_{0} with e′_{2j+1} ∈ y′ for all 0 ≤ j ≤ i′

Since y′ ⊑ y and e′_{1} ∈ y′, there exists e′′_{1} such that e′_{1} ≤^{L} e′′_{1} and e′′_{1} ∈ y. Since e′_{2} ≤^{R} e′_{1} ≤^{L} e′′_{1}, there exists e′′_{2} such that e′_{2} ≤^{L} e′′_{2} ≤^{R} e′′_{1}, by factorisation. Since y is secured, there exists e′′_{3} in y such that e′′_{2} ≤^{L} e′′_{3}. In order to continue this lifting of the e′_{i} relative to y′ to a sequence of the e′′_{i} relative to y, we have to make sure that e′_{3} ≤^{L} e′′_{3}: But

e′_{3} ≤^{L} e′′′_{3} ∈ y for some e′′′_{3} ∈ y since y′ ⊑ y, and
e′′′_{3} = e′′_{3} since e′_{2} ≤^{L} e′′_{3}, e′_{2} ≤^{L} e′′′_{3}, and e′′_{3}, e′′′_{3} ∈ y

Continuing in this way, we get:

e′_{0} ≤^{L} e′′_{1} ≥^{R} e′′_{2} ⋯ ≤^{L} e′′_{2i′+1} = e_{1} ≥^{R} e_{2} ⋯ ≤^{L} e_{2i+1} = e

where e′′_{2i′+1} = e_{1} follows from Lemma 3 applied to y, y, e′′_{2i′+1}, and e_{1}. Since e_{2j+1} ∈ y for all 0 ≤ j ≤ i and e′′_{2j+1} ∈ y for all 0 ≤ j ≤ i′, by (2), we conclude that x ⊑^{L} y.

(4) Only the uniqueness of z is in question, so suppose that x ⊑^{L} z ⊑^{R} y and x ⊑^{L} z′ ⊑^{R} y. By symmetry, it is enough to show that z ⊆ z′. So suppose that e ∈ z. Then by (2) there are e_{0} in x and e_{1} in z such that e ⪯_{z} e_{1} ⊒^{L} e_{0}. We begin by showing that e_{1} ∈ z′. Since e_{0} ∈ x ⊑ z′ there is an e′_{1} in z′ such that e_{0} ⊑^{L} e′_{1}. So e_{1} ↓^{L} e′_{1} and therefore, by Lemma 3 applied to z, z′, e_{1}, e′_{1}, we have e_{1} = e′_{1} ∈ z′.

We now consider the chain:

e = e_{n} ⪯_{z}^{1} … ⪯_{z}^{1} e_{2} ⪯_{z}^{1} e_{1}

and show by induction on j (1 ≤ j ≤ n) that e_{j} ∈ z′. This holds for j = 1. Suppose it holds for j < n. Then e_{j+1} ≥^{L} e′′ ≤^{R} e_{j} for some e′′. Then as z′ is a configuration, and e_{j} ∈ z, we have that e′′ ≤^{L} e′_{j+1} for some e′_{j+1} in z′. But then e_{j+1} = e′_{j+1} ∈ z′ follows as before, concluding the proof.

□

Definition 5 For x in Γ(E) and e in x, define

[e]_{x} = {e_{0} ∈ x | e_{0} ⪯_{x} e}

Lemma 6 Let E be a bistructure, and suppose that e ∈ x ∈ Γ(E). Then [e]_{x} is a finite configuration such that:

e ∈ [e]_{x} ⊑^{R} x and (∀ y ∈ Γ(E) (e ∈ y ↑^{R} x) ⇒ ([e]_{x} ⊑^{R} y))

Proof. The set [e]_{x} is clearly a configuration (cf. the proof of Proposition 1). The finiteness of [e]_{x} follows from Axiom 2(a). The rest of the statement is an immediate consequence of Lemma 5. □

Remark 2 For any e the following “canonical” set

[e] = {e′ | e′ ≤^{R} e}

is a configuration containing e, and if x is any other such, then [e] ⊑ x. In contrast, there need be no ⊆-least configuration containing a given e (cf. Lemma 6).

Proposition 2 Let E be a bistructure. The following properties hold of the associated biorder:

1. all ⊑-directed lubs and ⊑^{R}-bounded lubs exist,

2. all ⊑^{R}-lubs of ⊑^{R}-directed sets exist, coinciding with their ⊑-lubs, and

3. a configuration is ⊑-compact iff it is ⊑^{R}-compact iff it is finite.

It follows that (Γ(E), ⊑^{R}) and (Γ(E), ⊑) are ω-algebraic cpos (with common least element ∅), and that, moreover, (Γ(E), ⊑^{R}) is bounded complete, i.e., is a Scott domain.

Proof. (1) Let Δ be ⊑-directed. We show:

z = {e ∈ ⋃ Δ | e is ≤^{L} -maximal in ⋃ Δ} is the ⊑-lub of Δ

We first check that z is a configuration. If e_{1}, e_{2} ∈ z, then e_{1} ∈ δ_{1} and e_{2} ∈ δ_{2} for some δ_{1}, δ_{2} in Δ. Let δ in Δ be such that δ_{1}, δ_{2} ⊑ δ. Then by definition of z and ⊑, it follows that e_{1}, e_{2} ∈ δ. Therefore e_{1} ⌢ ⌣ e_{2}. If e ∈ z and e_{1} ≤^{R} e, let δ in Δ be such that e ∈ δ. Since δ is secured, there exists e_{2} in δ such that e_{1} ≤^{L} e_{2}. By definition of z and by Axiom 2 (cf. Remark 1), we can find e_{3} in z such that e_{2} ≤^{L} e_{3}. Hence z is indeed a configuration. It is obvious from the definition of z that δ ⊑ z holds for any δ in Δ, and that if z_{1} is an ⊑-upper bound of Δ then z ⊑ z_{1}.

The ⊑^{R}-bounded lubs exist: if X ⊆ Γ(E) and if x is an ⊑^{R}-upper bound of X, then ⋃ X is consistent as a subset of x and secured as a union of secured sets of events.

(2) Let Δ be ⊑^{R}-directed (and hence a fortiori ⊑-directed). Clearly ⨆^{R} Δ exists and is ⋃ Δ; we prove that ⨆ Δ = ⋃ Δ (where ⨆^{R} and ⨆ are relative to ⊑^{R} and ⊑, respectively). We have to show that any e in ⋃ Δ is ≤^{L}-maximal. Suppose there exists e_{1} in ⋃ Δ such that e ≤^{L} e_{1}. Then, applying Lemma 3 to ⋃ Δ, ⋃ Δ, e, and e_{1}, we get e = e_{1}.

(3) We prove three implications.

• x finite ⇒ x ⊑ -compact: Let {e_{1}, …, e_{n}} ⊑ ⨆ Δ. There exist e′_{1}, …, e′_{n} in ⨆ Δ such that e_{i} ≤^{L} e′_{i} for all i. Let δ_{1}, … δ_{n} in Δ be such that e′_{i} ∈ δ_{i} for all i, and let δ in Δ be such that δ_{i} ⊑ δ for all i. Then by the ≤^{L}-maximality of e′_{1}, …, e′_{n} we get that e′_{i} ∈ δ for all i. Hence {e_{1}, …, e_{n}} ⊑ δ.

• x ⊑ -compact ⇒ x ⊑^{R} -compact: If x ⊑^{R} ⨆^{R} Δ, then, a fortiori, x ⊑ ⨆ Δ, therefore x ⊑ δ for some δ in Δ. We show that actually x ⊑^{R} δ holds. Suppose e ∈ x and let e_{1} in δ be such that e ≤^{L} e_{1}. Then we get e = e_{1} by Lemma 3 applied to x, δ, e, and e_{1}.

• x ⊑^{R} -compact ⇒ x finite : We claim that, for any z:

{y | y finite and y ⊑^{R} z}

is ⊑^{R}-directed and has z as lub. The directedness is obvious. We have to check that z ⊑^{R} ⨆^{R}{y | y finite and y ⊑^{R} z}, i.e., for all e in z, there exists a finite y such that y ⊑^{R} z and e ∈ y. The configuration [e]_{z} (cf. Lemma 6) does the job. □

Proposition 3 Let E be a bistructure. Then the following properties hold:

1. (Γ(E), ⊑^{R}) is a dI-domain, and

2. the complete primes of (Γ(E), ⊑^{R}) are the configurations of the form [e]_{x}.

Proof. (1) A dI-domain is a Scott domain which is distributive (see Definition 7) and satisfies Axiom I, which states that a compact element dominates finitely many elements. Axiom I follows from the finiteness of compacts, proved in Proposition 2. Distributivity is then equivalent to prime-algebraicity, i.e., the property that any element is the lub of the complete primes that it dominates. (We refer to [31, 27] for a proof.) Primealgebraicity is an immediate consequence of (2).

(2) Consider a configuration [e]_{x}. We show it is a complete prime. If Y is bounded above and [e]_{x} ⊑^{R} ⨆^{R} Y = ⋃ Y, then e ∈ y for some y in Y. Since [e]_{x} ↑^{R} y, we infer that [e]_{x} ⊆ y, by Lemma 5. Conversely, every complete prime is of this form, since for any configuration x we have x = ⋃{[e]_{x} | e ∈ x}. □

The properties proved in Proposition 2 and Proposition 3 correspond to the most interesting structure of Berry’s bidomains. However, to show its configurations form a bidomain we will require a bistructure to fulfill extra axioms; these assure the existence of enough meets. We pursue these matters in Section 7.

5 A category of bistructures

Morphisms between bistructures correspond to configurations of the functionspace construction given below. They determine (certain—see Remark 3) extensional, linear (= stable and additive) functions on domains of configurations. Given bistructures E_{i} = (E_{i}, ≤_{i}^{L}, ≤_{i}^{R}, ⌢ ⌣_{i}), for i = 0, 1, their linear function space is defined by:

E_{0} E_{1} = (E_{0} × E_{1}, ≤^{L}, ≤^{R}, ⌢ ⌣)

where  (e_{0}, e_{1}) ≤^{L} (e′_{0}, e′_{1}) ⇔ e′_{0} ≤^{R} e_{0} and e_{1} ≤^{L} e′_{1},
(e_{0}, e_{1}) ≤^{R} (e′_{0}, e′_{1}) ⇔ e′_{0} ≤^{L} e_{0} and e_{1} ≤_{1}^{R} e′_{1}
and  (e_{0}, e_{1}) ⌣ ⌢ (e′_{0}, e′_{1}) ⇔ e_{0} ⌢ ⌣_{0} e′_{0} and e_{1} ⌣ ⌢_{1} e′_{1}.

It is straightforward to show that this is a bistructure. We define the category of bistructures BS by taking the morphisms from E_{0} to E_{1} to be configurations of E_{0} E_{1}, with composition being that of relations. We must show that this composition is well-defined and has identities.

Proposition 4 Let α be a configuration of E E′ and β be a configuration of E′ E′′. Then their relational composition β ∘ α is a configuration of E E′′. Also the identity relation on a bistructure E is a configuration of E E.

Proof. That identity relations are configurations relies, for securedness, on the factorisation property (1) of bistructures. For the relational composition β ∘ α to be a configuration we require it to be consistent and secured.

Consistency: From the definition of ⌣ ⌢ on function space we require that for (e_{1}, e′′_{1}), (e_{2}, e′′_{2}) in β ∘ α that

(i) e_{1} ⌢ ⌣ e_{2} ⇒ e′′_{1} ⌢ ⌣ e′′_{2} and (ii) e′′_{1} ⌣ ⌢ e′′_{2} ⇒ e_{1} ⌣ ⌢ e_{2},

facts which hold of the composition β ∘ α because they hold of α and β.

Securedness: Suppose (e, e′′) ∈ β ∘ α and that

(e_{0}, e′′_{0}) ≤^{R} (e, e′′),

i.e., e ≤^{L} e_{0} and e′′_{0} ≤^{R} e′′. It is required that there is

(e^{⋆}, e^{′′⋆}) ∈ β ∘ α

such that

(e_{0}, e′′_{0}) ≤^{L} (e^{⋆}, e^{′′⋆}),

i.e., e^{⋆} ≤^{R} e_{0} and e′′_{0} ≤^{L} e^{′′⋆}. [In the following argument, it is helpful to refer to the diagram below.]

As (e, e′′) ∈ β ∘ α there is e_{0}^{′⋆} such that (e, e_{0}^{′⋆}) ∈ α and (e_{0}^{′⋆}, e′′) ∈ β. Because e′′_{0} ≤^{R} e′′, we obtain that

(e_{0}^{′⋆}, e′′_{0}) ≤^{R} (e_{0}^{′⋆}, e′′)

As β is secured there is (e′_{1}, e′′_{1}) in β for which (e_{0}^{′⋆}, e′′_{0}) ≤^{L} (e′_{1}, e′′_{1}), i.e.,

(e′_{1}, e′′_{1}) ∈ β and e′_{1} ≤^{R} e_{0}^{′⋆} and e′′_{0} ≤^{L} e′′_{1}.  (1β)

As e ≤^{L} e_{0} and e′_{1} ≤^{R} e_{0}^{′⋆}, we have (e_{0}, e′_{1}) ≤^{R} (e, e_{0}^{′⋆}). But α is secured, so there is (e_{1}, e_{1}^{′⋆}) in α for which (e_{0}, e′_{1}) ≤^{L} (e_{1}, e_{1}^{′⋆}), i.e.,

(e_{1}, e_{1}^{′⋆}) ∈ α and e_{1} ≤^{R} e_{0} and e′_{1} ≤^{L} e_{1}^{′⋆}.  (1α)

From (1α) and (1β) we obtain:

e_{0} ≥^{R} e_{1} (e_{1}, e_{1}^{′⋆}) ∈ α e_{1}^{′⋆} ≥_{L} e′_{1} (e′_{1}, e′′_{1}) ∈ β e′′_{1} ≥^{L} e′′_{0}  (1)

We now show that this pattern in e_{1}, e_{1}^{′⋆}, e′_{1}, e′′_{1}, relative to e_{0} and e′′_{0}, must repeat.

It follows from e′_{1} ≤^{L} e_{1}^{′⋆} that (e_{1}^{′⋆}, e′′_{1}) ≤^{R} (e′_{1}, e′′_{1}) ∈ β. As β is secured, there is an (e′_{2}, e′′_{2}) in β for which (e_{1}^{′⋆}, e′′_{1}) ≤^{L} (e′_{2}, e′′_{2}), i.e.,

(e′_{2}, e′′_{2}) ∈ β and e′_{2} ≤^{R} e_{1}^{′⋆} and e′′_{1} ≤^{L} e′′_{2}  (2β)

As e′_{2} ≤^{R} e_{1}^{′⋆}, we have (e_{1}, e′_{2}) ≤^{R} (e_{1}, e_{1}^{′⋆}) ∈ α. But α is secured, so there is an (e_{2}, e_{2}^{′⋆}) in α for which (e_{1}, e′_{2}) ≤^{L} (e_{2}, e_{2}^{′⋆}), i.e.,

(e_{2}, e_{2}^{′⋆}) ∈ α and e_{2} ≤^{R} e_{1} and e′_{2} ≤^{L} e_{2}^{′⋆}  (2α)

and the pattern in (1) repeats in (2) below—obtained directly from (2α) and (2β):

e_{0} ≥^{R} e_{2} (e_{2}, e_{2}^{′⋆}) ∈ α e_{2}^{′⋆} ≥_{L} e′_{2} (e′_{2}, e′′_{2}) ∈ β e′′_{2} ≥^{L} e′′_{0}  (2)

where e′_{2} ≤^{R} e_{1}^{′⋆}. This can be repeated infinitely. Diagrammatically:

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; e_{0}^{′⋆}; e′_{1}; e_{1}^{′⋆}; e′_{2}; e_{2}^{′⋆}; e′′_{0}; e′′; e′′_{2}; e′′_{1}; β; β; e; e_{0}; e_{1}; e_{2}; α; L; L; R; R; R; L; β; R; R; L; α; α; L]

The chain

e_{0}^{′⋆} ≥^{R} e′_{1} ≤^{L} e_{1}^{′⋆} ≥^{R} e′_{2} ≤^{L} e_{2}^{′⋆} ≥^{R} ⋯

must eventually be constant by Axiom 2(a) on bistructures. Hence we obtain

(e_{n}, e_{n}^{′⋆}) ∈ α and e′_{n} = e_{n}^{′⋆} and (e′_{n}, e′′_{n}) ∈ β

yielding (e_{n}, e′′_{n}) in β∘α with e_{n} ≤^{R} e_{0} and e′′_{0} ≤^{L} e′′_{n}, i.e., (e_{0}, e′′_{0}) ≤^{L} (e_{n}, e′′_{n}); so (e_{n}, e′′_{n}) fulfills the requirements we seek for (e^{⋆}, e^{′′⋆}). □

Proposition 5 Let F be a configuration of E E′ and let x be a configuration of E. Defining

F ·x = {e′ | ∃ e ∈ x (e, e′) ∈ F }

yields a configuration of E′. The function x ↦ F·x : Γ(E) → Γ(E′) is linear with respect to ⊑^{R} and continuous with respect to ⊑.

Proof. The first part of the statement is a consequence of Proposition 4, since F · x can be read as F ∘ x if x is viewed as a configuration from I (the tensor unit, defined at the beginning of the next section) to E. The verification that x ↦ F ·x is linear is easy. We check only that it preserves compatible binary lubs. Suppose that e′ ∈ F ·(x ⊔^{R} y), i.e., (e, e′) ∈ F for some e in x ⊔^{R} y. Then e ∈ x or e ∈ y, hence e′ ∈ (F ·x) ⊔^{R} (F ·y).

For continuity, by Lemma 7 below, it is enough to check ⊑-monotonicity, which is proved using a “staircase argument” similar to that of the previous proof: if x ⊑ y and e′ ∈ F ·x, let e in x be such that (e, e′) ∈ F ·x, and let e_{1} in y be such that e ≤^{L} e_{1}. Since (e_{1}, e′) ≤^{R} (e, e′), there exists (e_{2}, e′_{1}) in F such that e′ ≤^{L} e′_{1} and e_{2} ≤^{R} e_{1}. From there we find an e_{3} such that e_{3} ∈ y and e_{2} ≤^{L} e_{3}, which leads to an (e_{4}, e′_{2}) in F such that (e_{3}, e′_{1}) ≤^{L} (e_{4}, e′_{2}). In this way, we construct e′ ≤^{L} e′_{1} ≤^{L} e′_{2} ⋯, where the e′_{i} are in y. The sequence eventually ends, yielding an e′_{i} that fits. □

Lemma 7 Let E and E′ be bistructures. Suppose that f : Γ(E) → Γ(E′) is ⊑^{R}-continuous and ⊑-monotonic. Then it is also ⊑-continuous.

Proof. Suppose {e_{1}, …, e_{n}} ⊑ f(x). Then there exist e′_{1}, …, e′_{n} in f(x) such that e_{i} ≤^{L} e′_{i} for all i. By ⊑^{R}-continuity, there exists a finite x_{1} ⊑^{R} x such that e′_{1}, …, e′_{n} ∈ f(x_{1}), hence {e_{1}, …, e_{n}} ⊑ f(x_{1}). □

Remark 3 Not all ⊑^{R}-linear and ⊑-continuous functions are represented by a morphism. The represented functions also satisfy a uniformity requirement, where a ⊑^{R}-stable and ⊑-continuous function f from Γ(E) to Γ(E′) is uniform iff for all e in E and configurations x containing e and for all e′ in E′ we have that ([e]_{x}, e′) ∈ tr(f) implies ([e], e′) ∈ tr(f) (see Definition 6 below, and cf. Remark 2); unfortunately, even this condition is not sufficient for representability. On a more positive note, one can show that the assignment of functions to configurations is 1-1.

6 A model of classical linear logic

Here we give the constructions showing that BS is a (non-compactly closed) model of classical linear logic. The constructions extend those of Girard (recalled in Section 2). Define linear negation, the involution of linear logic, by

E^{⊥} = (E, ≥^{R}, ≥^{L}, ⌣ ⌢)

where E = (E, ≤^{L}, ≤^{R}, ⌢ ⌣). Clearly (E^{⊥})^{⊥} = E. The remaining multiplicatives, ℘ (par) and ⊗ (tensor), are determined by the usual isomorphisms of classical linear logic:

E_{0} ℘ E_{1} ≅ (E_{0}^{⊥} E_{1}), E_{0} ⊗ E_{1} ≅ (E_{0} E_{1}^{⊥})^{⊥}

In more detail, the tensor product is defined as follows:

E_{0} ⊗ E_{1} = (E_{0} × E_{1}, ≤^{L}, ≤^{R}, ⌢ ⌣)

where  (e_{0}, e_{1}) ≤^{L} (e′_{0}, e′_{1}) ⇔ e_{0} ≤^{L} e′_{0} and e_{1} ≤^{L} e′_{1},
(e_{0}, e_{1}) ≤^{R} (e′_{0}, e′_{1}) ⇔ e_{0} ≤^{R} e′_{0} and e_{1} ≤_{1}^{R} e′_{1}
and  (e_{0}, e_{1}) ⌢ ⌣ (e′_{0}, e′_{1}) ⇔ e_{0} ⌢ ⌣_{0} e′_{0} and e_{1} ⌢ ⌣_{1} e′_{1}.

The construction E^{⊥} is isomorphic to (E I) where I = ({•}, id, id, id) is the unit of ⊗. Product and coproduct in the category BS are (again) obtained by disjoint juxtaposition (now of bistructures), extending conflict across the two event sets in the case of coproduct. The terminal object is 1 = (∅, ∅, ∅, ∅).

We define the exponential !E of a bistructure E by:

!E = (Γ(E)^{0}, ⊑^{L}, ⊑^{R}, ↑^{R})

(recall ⊑^{L} and ⊑^{R}, and ↑^{R} from Definition 3).

Lemma 8 !E is a bistructure.

Proof. Obviously, ⊑^{R} is a partial order. By Proposition 1, ⊑^{L} is a partial order and so Axiom 1 is verified. Given the definition of ⌢ ⌣_{!}, Axiom 3(b) holds a fortiori, and we can rephrase Axiom 3(a) as:

(x_{1} ↓^{L} x_{2} and x_{1} ↑^{R} x_{2}) ⇒ x_{1} = x_{2}

which is an immediate consequence of Proposition 1.4.

The main difficulty in the proof is in showing Axiom 2(b), i.e., that the relation ⪯_{!}= (⊒^{L} ∪ ⊑^{R})^{⋆} of !E is a partial order. We need only show antisymmetry. Thus suppose for x_{i}, x′_{i} in Γ(E)^{0} we have:

x_{0} ⊑^{R} x′_{0} ⊒^{L} x_{1} ⊑^{R} x′_{1} ⊒^{L} ⋯ ⊒^{L} x_{n} ⊑^{R} x′_{n}  (1)

with x_{n} = x_{0} and x′_{n} = x′_{0}. We shall show x_{i} = x′_{i} = x_{j} = x′_{j} for all i, j. Then by the definition of ⪯_{!} on !E it follows that ⪯_{!} is antisymmetric.

Define fix = ⋂_{i} x_{i}. We first show fix ∈ Γ(E). Consistency is obvious. Suppose e ∈ fix and e_{1} ≤^{R} e. Since e ∈ x_{i}, there exist e_{1}^{i} in x_{i} such that e_{1} ≤^{L} e_{1}^{i}, for all i ≥ 1. Since x_{i} ⊑ x′_{i−1}, there exist e_{1}^{′i} in x′_{i−1} such that e_{1}^{i} ≤^{L} e_{1}^{′i}, for all i ≥ 1. We now apply Lemma 3 twice.

• From e_{1} ≤^{L} e_{1}^{′i}, e_{1} ≤^{L} e_{1}^{i−1} and x_{i−1} ⊑^{R} x′_{i−1} we conclude e_{1}^{′i} = e_{1}^{i−1}, therefore e_{1}^{i−1} ≥^{L} e_{1}^{i}.

• From e_{1} ≤^{L} e_{1}^{0}, e_{1} ≤^{L} e_{1}^{n} and x_{0} = x_{n}, we obtain e_{1}^{0} = e_{1}^{n}.

Since ≤^{L} is a partial order, we get: e_{1}^{0} = ⋯ = e_{1}^{i} = ⋯ = e_{1}^{n}, hence e_{1}^{0} ∈ fix, which shows that fix is secured. Consequently fix ∈ Γ(E) and clearly fix ⊑^{R} x_{i}, x′_{i} for all i. It remains to show fix = x_{i} = x′_{i} for all i.

Notice that in chain (1) we can bring any index i to the head position, by a circular permutation. Thus, it suffices to show x_{0} = x′_{0} = fix.

Take e in x′_{0}. Then by repeated use of Proposition 1, we deduce from (1) that

e = e_{0} ⪯_{x′_{0}} e′_{0} ≥^{L} e_{1} ⪯_{x′_{1}} e′_{1} ≥^{L} e_{2} ⋯ ≥^{L} e_{m} ⪯_{x′_{[m]n}} e′_{m} ≥^{L} e_{m+1} ⋯ (2)

for some e_{i} in x_{[i]_{n}} and e′_{i} in x′_{[i]_{n}} where i ∈ ω (here [m]_{n} is m modulo n).

The sequence has been continued infinitely by going around and around the loop (1). As x′_{0} is finite and the sequence (2) visits x′_{0} infinitely often there must be e_{m}, e_{q} in x′_{0} such that m < q and [m]_{n} = [q]_{n} = 0 and e_{m} = e_{q}. Then as ⪯ is a partial order, e_{m} = e′_{m} = e_{m+1} = ⋯ = e_{q}. Thus e_{m} ∈ fix so the sequence (2) eventually contains an element of fix. We know fix ⊑^{R} x_{i}, x′_{i}, for all i. Now, working backwards along the chain (2), starting at e_{m}, we show that all elements of the chain are in fix.

• From e_{i+1} to e′_{i}: this follows from Lemma 3 applied to fix, x′_{i}, e_{i+1}, and e′_{i}.

• From e′_{i} to e_{i}: by Lemma 5.

In particular, e_{0} (= e) ∈ fix. We have proved x′_{0} ⊑^{R} fix, which together with fix ⊑^{R} x_{0} ⊑^{R} x′_{0} implies x_{0} = x′_{0} = fix as required. Thus the relation ⪯_{!} on !E is a partial order.

Finally, we prove Axiom 2(a), i.e., {x′ ∈ Γ(E)^{0} | x′ ⪯_{!} x} is finite, for x ∈ Γ(E)^{0}. By Proposition 1 it is clear that

x′ ⪯_{!} x ⇒ ∀ e′ ∈ x′ ∃ e ∈ x e′ ⪯ e

Thus:

x′ ⪯_{!} x ⇒ x′ ⊆ ⋃{e′ | ∃ e ∈ x e′ ⪯ e}

As x is finite and ⪯ is finitary, we have {x′ ∈ Γ(E)^{0} | x′ ⪯_{!} x} is finite, as required. □

The configurations of the bistructure !E_{0} E_{1} are in 1-1 correspondence with the type of functions from (Γ(E_{0}), ⊑^{R}, ⊑) to (Γ(E_{1}), ⊑^{R}, ⊑) considered by Berry in his cartesian closed category of bidomains. We need notions of trace and extensional and stable orderings for such functions (cf. Section 3):

Definition 6 Let f be a ⊑-continuous and ⊑^{R}-stable function from Γ(E_{0}) to Γ(E_{1}). Then:

tr(f) = {(x, e) ∈ Γ(E_{0})^{0} × E_{1} | x is ⊑^{R}-minimal such that e ∈ f(x)}

The stable ordering on such functions is defined by:

f ≤ g ⇔ ∀ x ⊑^{R} y f(x) = f(y) ∩ g(x)

The extensional ordering on such functions is defined by:

f ⊑ g ⇔ ∀ x f(x) ⊑ g(x)

Proposition 6 Let E_{0}, E_{1} be bistructures. For R in Γ(!E_{0} E_{1}) and x in Γ(E_{0}) define

R̄(x) = {e | ∃ x_{0} ⊑^{R} x (x_{0}, e) ∈ R}.

Then R̄ is a function Γ(E_{0}) → Γ(E_{1}) which is continuous with respect to ⊑ and stable with respect to ⊑^{R} on configurations. In fact, R ↦ R̄ is a 1-1 correspondence between configurations of !E_{0} E_{1} and such functions, with inverse f ↦ tr(f). Further, for the stable ordering of functions we have:

f ≤ g ⇔ tr(f) ⊑^{R} tr(g)

and for the extensional ordering we have:

f ⊑ g ⇔ tr(f) ⊑ tr(g)

Proof. We first check that R̄(x) is a configuration. Consistency follows from the definition of ⌢ ⌣ in !E_{0} E_{1}. Suppose e ∈ R̄(x) and e′ ≤^{R} e. Choose x_{0} ⊑^{R} x such that (x_{0}, e) ∈ R. Then (x_{0}, e′) ≤^{R} (x_{0}, e), hence by securedness there exists (x′′, e′′) in R such that (x_{0}, e′) ≤^{L} (x′′, e′′). Then e′′ fits since x′′ ⊑^{R} x_{0} ⊑^{R} x. Thus the function R̄ is well-defined. It is ⊑^{R}-continuous by construction and ⊑^{R}-stable by the definition of ⌢ ⌣ in !E_{0} E_{1}. We next show that R̄ is ⊑-monotonic, hence ⊑-continuous, by Lemma 7. Suppose x ⊑ y and e ∈ R̄(x). Choose x_{0} ⊑^{R} x such that (x_{0}, e) ∈ R. Let us factorise x_{0} ⊑ y as x_{0} ⊑^{L} x_{1} ⊑^{R} y. Since (x_{1}, e) ≤^{R} (x_{0}, e), there exists (x_{2}, e_{1}) in R such that (x_{1}, e) ≤^{L} (x_{2}, e_{1}), by securedness. Then e_{1} fits, since e ≤^{L} e_{1} and x_{2} ⊑^{R} x_{1} ⊑^{R} y.

We now show that tr is the inverse of R ↦ R̄. Suppose f : Γ(E_{0}) → Γ(E_{1}) is ⊑-continuous and ⊑^{R}-stable. We need first that tr(f) ∈ Γ(!E_{0} E_{1}), i.e., that tr(f) is consistent and secured:

Consistency: Suppose (x, e), (x′, e′) ∈ tr(f) and that (x, e) ≍ (x′, e′), i.e., x ↑^{R} x′ and e ≍ e′. We show (x, e) = (x′, e′). As e, e′ ∈ f(x ∪ x′), we must have e ⌢ ⌣ e′, which combined with e ≍ e′, entails e = e′. Now, (x, e), (x′, e) are both in the trace of f. Because x ↑^{R} x′ and f is ⊑^{R}-stable we conclude that x = x′.

Securedness: Suppose (x′, e′) ≤^{R} (x, e) ∈ tr(f). Then x ⊑^{L} x′ and e′ ≤^{R} e. As f is ⊑-monotonic, f(x) ⊑ f(x′). Because e′ ≤^{R} e and e ∈ f(x), we see that e′ is in the ≤-downwards-closure of f(x′). Thus by Lemma 4, there exists e′′ in f(x′) such that:

e′ ≤^{L} e′′  (1)

By the definition of tr(f), there is

x_{0} ⊑^{R} x′  (2)

such that

(x_{0}, e′′) ∈ tr(f)  (3)

Combining (1), (2), (3) we obtain, as required

(x′, e′) ≤^{L} (x_{0}, e′′) ∈ tr(f).

For f a ⊑-continuous, ⊑^{R}-stable function Γ(E_{0}) → Γ(E_{1}) its continuity with respect to ⊑^{R} entails \overline{tr(f)} = f. For R in Γ(!E_{0} E_{1}) a direct translation of the definitions yields tr(R̄) = R. Thus the map R ↦ R̄ = R is a 1-1 correspondence.

Turning to the two orderings of functions, the claim for the stable ordering is established exactly as in the case of webs [11]. For the extensional ordering, suppose first that f ⊑ g and choose (x, e) in tr(f). Then e ∈ f(x) ⊑ g(x), and so for some e′ ≥^{L} e, e′ ∈ g(x). But then there is an x_{0} ⊑^{R} x such that (x_{0}, e′) ∈ tr(g) and we have that (x, e) ≤^{L} (x_{0}, e′) ∈ tr(g). Conversely, suppose that tr(f) ⊑ tr(g) and choose e, x with e ∈ f(x). Then for some subset x_{0} of x, (x_{0}, e) ∈ tr(f) ⊑ tr(g), and so there is a y ⊑^{R} x_{0} and an e′ ≥^{L} e such that (y, e′) ∈ tr(g). Then we have e ≤^{L} e′ ∈ g(y) ⊑^{R} g(x), concluding the proof. □

This section has provided the key constructions for showing that BS is a model of classical linear logic, and that the associated co-Kleisli category is equivalent to one of biorders:

Theorem 1 The category BS forms a linear category in the sense of [24]. The exponential ! forms a comonad on the category BS. Together they form a model of classical linear logic (a Girard category in the sense of [24]—see too [4]).

The associated co-Kleisli category is (necessarily) cartesian closed and isomorphic to the category whose objects are the structures (Γ(E), ⊑^{R}, ⊑), where E is a bistructure, and whose morphisms are the ⊑-continuous and ⊑^{R}-stable functions.

Proof. The proof that BS forms a linear category is a straightforward extension of the web case, while the facts about the co-Kleisli category largely follow from Proposition 6. For the monoidal structure, at the level of events, the canonical isomorphisms are given by:

((e_{0}, e_{1}), e_{2}) ↔ (e_{0}, (e_{1}, e_{2})),
(e, •) ↔ e,
(•, e) ↔ e

The first of these correspondences also serves to establish the closed structure. For example, we have:

((e_{0}, e_{1}), e_{2}) ≤_{E_{0}⊗E_{1} E_{2}}^{L} ((e′_{0}, e′_{1}), e′_{2})
⇔ e′_{0} ≤_{E_{0}}^{R} e_{0} and e′_{1} ≤_{E_{1}}^{R} e_{1} and e_{2} ≤_{E_{2}}^{L} e′_{2}
⇔ (e_{0}, (e_{1}, e_{2})) ≤_{E_{0} (E_{1} E_{2})}^{L} (e′_{0}, (e′_{1}, e′_{2}))

The trace of the canonical morphism from E to (E I) I is:

{(e, ((e, •), •)) | e ∈ E}

It is clear that it has as inverse the function whose trace is:

{(((e, •), •), e) | e ∈ E}

Turning to the comonadic structure, the counit ε : !E E is given by:

ε = {([e]_{x}, e) | e ∈ x ∈ Γ(E)}

For any α : !E_{0} E_{1}, its lift α^{♯} : !E_{0} !E_{1} is given by:

α^{♯} = {( ⋃_{i=1,n} x_{i}, {e_{1}, …, e_{n}}) ∈ !E_{0}×!E_{1} | (x_{i}, e_{i}) ∈ α (for i = 1, n)}

(Then the comultiplication δ : !E !!E is (id_{!E})^{♯} and the functorial action of ! is f ↦ (f ∘ ε)^{♯}.) The canonical isomorphism !(E_{0} × E_{1}) ≅ (!E_{0}) ⊗ (!E_{1}) is given by:

x ↔ (x ∩ E_{0}, x ∩ E_{1})

The isomorphism !1 ≅ I follows immediately from the observation that Γ(1) is a singleton.

For the last part, the isomorphism is to send a bistructure E to the biorder (Γ(E), ⊑^{R}, ⊑), and a morphism R : !E_{0} E_{1} to the function \overline{R} : Γ(E_{0}) → Γ(E_{1}). Given the results of Proposition 6, it only remains to show functoriality, and that is automatic from the comonadicity of the exponential, once we notice that \overline{R}(x) = R ∘ x^{♯}, identifying elements of Γ(E) with morphisms from !1 to E. □

A fortiori, bistructures provide a model of simply-typed λ-calculi, and of PCF in particular. One interprets base types as event structures, i.e., bistructures of the form (E, id, ≤, ⌢ ⌣). At first order, Γ(!E_{0} E_{1}) is up to bijection the set of stable functions from Γ(E_{0}) to Γ(E_{1}), represented, not as an event structure, but as a bistructure with a non-trivial ≤^{L}-order which captures the extensional order between stable functions. At higher orders, as discussed in Section 2, the model diverges from the stable model by enforcing both ⊑^{R}-stability and ⊑-continuity of the morphisms. In the next section we shall see that this model coincides with that obtained from Berry’s category of bidomains.

7 Bidomains

Bidomains are not very widely known so we present their definition here. They were introduced in Gérard Berry’s Thèse de Doctorat d’Etat [2]. More details and background motivation can be obtained either from Berry’s thesis or the references [3, 25].

The most general biordered domains Berry considered were the bicpos.

Definition 7 A bicpo is a biorder (D, ≤, ⊑) such that:

1. the structure (D, ⊑) is a cpo with a continuous greatest-lower-bound operation ⊓ (the order ⊑ is called the extensional order),

2. the structure (D, ≤) is a cpo, with the same least element as (D, ⊑) and the identity on D is a continuous function from (D, ≤) to (D, ⊑) (the order ≤ is called the stable order),

3. the operation ⊓ is ≤-continuous—in fact, ≤-monotonicity suffices, by 1. and 2. (it follows that the ≤-greatest lower bound, x ∧ y, of points x, y, bounded above in (D, ≤), exists and coincides with x ⊓ y), and

4. for all ⊑-directed subsets S, S′ ⊆ D, if for all s in S, s′ in S′ there are t in S, t′ in S′ such that

s ⊑ t and s′ ⊑ t′ and t ≤ t′

then ⨆ S ≤ ⨆ S′.

A bicpo is distributive iff

• whenever x, y are bounded above in (D, ≤) then their least upper bounds, x ∨ y, in (D, ≤), and x ⊔ y, in (D, ⊑), exist and coincide, and

• the cpo (D, ≤) is distributive, i.e., for all x, y, z in D, if {x, y, z} is bounded above, then x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z).

Bicpos form a category where the morphisms are taken to be those functions which are continuous with respect to the extensional order and conditionally multiplicative with respect to the stable order, i.e., the functions preserve binary compatible glbs. This category is cartesian closed; products are given by cartesian products of the underlying sets, the two orders being obtained in a coordinatewise fashion; the function space [D_{0} → D_{1}] consists of the set of morphisms from D_{0} to D_{1} with the extensional order ⊑ being the pointwise order, based on the extensional order of D_{1}, and with the order ≤ being the stable order of functions, based on the stable orders of D_{0} and D_{1}.

Here are brief hints on how the axioms of Definition 7 are used. Lubs and glbs in the function spaces are defined pointwise. The continuity properties of the meet operation are put to use when proving that the pointwise lubs are conditionally multiplicative. Axiom 4 serves to establish that the pointwise extensional lubs are monotonic with respect to the stable ordering.

The smallest category of biordered domains Berry considered was that of bidomains. They are a form of distributive bicpo, satisfying a restriction which ensures that they are dI-domains with respect to the stable order.

Definition 8 A finite projection on a bicpo D is a morphism ψ : D → D such that h ∘ h = h and h(x) ≤ x, for all x in D, and which is compact with respect to the stable order on [D → D].

A bicpo D is said to be a bidomain iff it is distributive and there is a sequence of finite projections ψ_{i} (i ∈ ω) on it, increasing with respect to the stable order, whose least upper bound is the identity function 1_{D} : D → D.

The category of bidomains and of ⊑-continuous and ≤-stable functions is a full sub-cartesian closed category of that of bicpos. [In the subcategory, we have stable = conditionally multiplicative.]

We now make good our earlier claim that configurations of (suitably restricted) bistructures form a bidomain. Let E be a bistructure. The problem is that the axioms of bistructures adopted here are too weak to ensure the existence of enough ⊑-glbs to yield a bicpo. We can prove the existence of the required glbs provided we add two further axioms on bistructures:

Definition 9 A B-bistructure (“B” stands for “Bidomain”) is a bistructure (E, ≤^{L}, ≤^{R}, ⌢ ⌣) that satisfies the following two additional axioms:

4. if e ≥^{L} e′ and e ⌢ e′′, then e′ ⌢ e′′, and

5. bounded binary ≤^{L}-lubs exist, i.e., if e_{1}, e_{2} ≤^{L} e, for some event e, then the lub, e_{1} ∨^{L} e_{2}, with respect to ≤^{L} exists.

B-bistructures are quite similar to the original version of bistructures in [25] —for example, Axioms 1, 2 and 5 are common, factorisation is unique in both, and all the other axioms relate to the interaction between coherence and the two partial orders. Axiom 3(a) is missing in [25]; instead, configurations are defined in a way equivalent to requiring for any elements e, e′ that not only e ⌢ ⌣ e′ but also ¬(e ↓^{L} e′). Pleasantly, as is straightforward to show, the class of biorders obtained from the original version is included in that obtained from B-bistructures.

Proposition 7 Let E be a B-bistructure. Then (Γ(E), ⊑^{R}, ⊑) is a bidomain.

Proof. We must first show that (Γ(E), ⊑^{R}, ⊑) is a distributive bicpo. We already know from Proposition 2 that (Γ(E), ⊑) and (Γ(E), ⊑^{R}) are cpos, and that ⊑^{R}-directed lubs are ⊑-lubs, which is the same as requiring that the identity function is continuous from (Γ(E), ⊑^{R}) to (Γ(E), ⊑). We also know that (Γ(E), ⊑) is algebraic, which is easily seen to imply the continuity of ⊓, provided binary glbs exist, which we prove now, using Axioms 4 and 5. Let x and y be two configurations. We define x ⊓ y as the set of all events e such that e is in the ≤^{L}-downwards-closure of both x and y, and is ≤^{L}-maximal with that property. This is clearly the glb of x and y if only it is a configuration. The definition ensures securedness by construction: if e ∈ x ⊓ y and e′ ≤^{R} e, then e′ is in the ≤^{L}-downwards-closure of both x and y by Lemma 4, and by definition of x ⊓ y there exists e′′ in x ⊓ y such that e′ ≤^{L} e′′. Suppose now that e_{1}, e_{2} are in x ⊓ y. Let e′_{1}, e′_{2} in x be such that e_{1} ≤^{L} e′_{1} and e_{2} ≤^{L} e′_{2}, and let e′′_{1}, e′′_{2} in y be such that e_{1} ≤^{L} e′′_{1} and e_{2} ≤^{L} e′′_{2}. Since e′_{1}, e′_{2} ∈ x, we have e′_{1} ⌢ ⌣ e′_{2}, and similarly e′′_{1} ⌢ ⌣ e′′_{2}. We distinguish several cases.

• e′_{1} ≠ e′_{2}. Here, by two applications of Axiom 4 we get first e_{1} ⌢ e′_{2} then e_{1} ⌢ e_{2}.

• e′′_{1} ≠ e′′_{2}. We obtain e_{1} ⌢ e_{2} similarly to the previous case.

• e′_{1} = e′_{2} and e′′_{1} = e′′_{2}. By Axiom 5, e_{1} ∨^{L} e_{2} exists. It is in the ≤^{L}- downwards-closure of both x and y, which, by the definition of x ⊓ y, forces e_{1} = e_{2} = e_{1} ∨^{L} e_{2}.

In all cases, we have e_{1} ⌢ ⌣ e_{2}. This completes the proof of Axioms 1 and 2.

We next check Axiom 3. Let y ⊑^{R} z and e ∈ x ⊓ y. Then e is in the ≤^{L}-downwards-closure of both x and z. We show that e is ≤^{L}-maximal with that property. Suppose that e ≤^{L} e′ and e′ ≤^{L} e′_{1} ∈ x and e′ ≤^{L} e′_{2} ∈ z. Now, for some e′_{3} in y, e ≤^{L} e′_{3} and thus, by Lemma 3, we have that e′_{2} = e′_{3} ∈ y. Therefore, e = e′ by the maximality property of e with respect to x and y. Hence e ∈ x ⊓ z, and we have proved x ⊓ y ⊑^{R} x ⊓ z.

To check Axiom 4, let subsets S, S′ be ⊑-directed subsets of Γ(E) such that whenever s ∈ S and s′ ∈ S′ there are t in S and t′ in S′ such that

s ⊑ t and s′ ⊑ t′ and t ⊑^{R} t′.

By the proof of Proposition 2,

⨆ S = {e ∈ ⋃ S | e is ≤^{L} -maximal in ⋃ S}

Equivalently, ⨆ S consists of the events e such that e ∈ s for some s in S with the property that

∀t ∈ S (s ⊑ t ⇒ e ∈ t).  (1)

Indeed, suppose that e and s satisfy property (1), and let e_{1} ≥^{L} e be such that e_{1} ∈ ⋃ S, i.e., e_{1} ∈ t for some t in S. Let s′ in S be such that s ⊑ s′ and t ⊑ s′. Then e ∈ s′ and e_{1} is in the ≤^{L}-downwards-closure of s′. This combined with e ≤^{L} e_{1} yields e = e_{1}. Conversely, if e ∈ s ∈ S and e is ≤^{L}-maximal in ⋃ S, then e, s obviously satisfy (1).

Given e and s satisfying (1), we wish to show e ∈ ⨆ S′. By assumption, taking s′ an arbitrary element of S′, we have for some t in S and t′ in S′ that

t ⊑^{R} t′ and s ⊑ t and s′ ⊑ t′.

By (1), we get that e ∈ t′. Suppose t′ ⊑ t′′ ∈ S′. Replacing s′ by t′′, and reasoning as above, we get that e ∈ t′′′ for some t′′′ such that t′′ ⊑ t′′′. Finally, one easily derives that e ∈ t′′ from t′ ⊑ t′′ ⊑ t′′′, e ∈ t′ and e ∈ t′′′. Thus e and t′ satisfy property (1) relative to S′, i.e., e ∈ ⨆ S′. We conclude that ⨆ S ⊑^{R} ⨆ S′, as required. Thus (Γ(E), ⊑^{R}, ⊑) is a bicpo.

For distributivity, by Proposition 3, we know that (Γ(E), ⊑^{R}) is a distributive cpo. Now remark that if x ↑^{R} y, x ⊑ z and y ⊑ z, then also x ∪ y ⊑ z by the definition of ⊑.

Finally, to show that (Γ(E), ⊑^{R}, ⊑) is a bidomain we need to produce an ω-chain of finite projections on it whose least upper bound is the identity on Γ(E). Here we refer to Proposition 6, showing how continuous stable functions on Γ(E) correspond to configurations of the bistructure !E E; a configuration F of !E E corresponds to a continuous, stable function \overline{F} : Γ(E) → Γ(E) so that inclusion of configurations corresponds to the stable ordering of functions. Let X be the configuration of !E E corresponding to the identity function on Γ(E). Because the events of !E E form a countable set we may enumerate them as e_{0}, e_{1}, ⋯, e_{n}, · · ·. Define X_{n} as the configuration

[e_{0}]_{X} ∪ ⋯ ∪ [e_{n}]_{X}.

Each X_{n} is a finite set and so compact with respect to ⊑^{R}. By Proposition 6, we obtain a chain of functions \overline{X}_{n}, n in ω, compact and increasing with respect to the stable order, with least upper bound the identity function on Γ(E). Being stably less than the identity, each function \overline{X}_{n} must be a projection.

We conclude that Γ(E) is a bidomain. □

Proposition 8 If E_{0} and E_{1} are B-bistructures, then so are E_{0} × E_{1} and !E_{0} E_{1}.

Proof. The verification for the product is immediate. We check Axioms 4 and 5 for !E_{0} E_{1}. Let (x, e_{1}) ≥^{L} (y, e′_{1}) and (x, e_{1}) ⌢ (z, e′′_{1}). Then x ⊆ y, e_{1} ≥^{L} e′_{1} and either x ⌣ z or e_{1} ⌢ e′′_{1}. If x ⌣ z then y ⌣ z (as x ⊆ y); if e_{1} ⌢ e′′_{1} then e′_{1} ⌢ e′′_{1}, by Axiom 4 for E_{1}. In either case it follows that (y, e′_{1}) ⌢ (z, e′′_{1}). The verification of Axiom 5 is straightforward: (x, e_{1}) ∨^{L} (y, e′_{1}) = (x ⊓^{R} y, e_{1} ∨^{L} e′_{1}), where we use Axiom 5 for E_{1} and the fact that Γ(E_{0}) is ⊑^{R}-bounded complete (cf. Proposition 2). [In boundedcomplete cpos, all non-empty glbs exist.] □

Remark 4 On the other hand, Axiom 4 is not preserved by any of ⊗, (·)^{⊥} or !. Therefore we do not see how to get a model of linear logic with Bbistructures.

Theorem 2 The B-bistructures yield a full sub-cartesian closed category of the co-Kleisli category of the exponential comonad on BS. It is equivalent to a full sub-cartesian closed category of bidomains.

Proof. The first assertion is immediate from Proposition 8. By Proposition 7 and the last part of Theorem 1, the subcategory is equivalent to a full subcategory of the category of bidomains. It remains to show that there are isomorphisms of bidomains between Γ(E_{0}) × Γ(E_{1}) and Γ(E_{0} × E_{1}), and also between Γ(E_{0}) → Γ(E_{1}) and Γ(!E_{0} E_{1}). The first is easy to see (it is (x, y) ↦ x ∪ y, assuming E_{0} and E_{1} disjoint). The second is given by f ↦ tr(f), by virtue of the remarks above on function spaces of bidomains and Proposition 6. □

Notice that if ≤^{L}= id, Axioms 4 and 5 hold vacuously, hence the category of B-bistructures is large enough to contain the models of typed λ-calculi where the base types are interpreted by event structures.

8 Discussion

In this section, we discuss possible variations and connections with other work.

Variations. Besides coherence spaces there are a few other “web-based” models of intuitionistic linear logic or full classical linear logic. Most notably, there are Ehrhard’s hypercoherences with a Kleisli category of strongly stable functions, which can be seen as an extensional (although not orderextensional) account of sequentiality. At first order, the strongly stable model contains exactly the sequential functions. At higher orders, it is the extensional collapse of the model of sequential algorithms [8, 9]. Generalisations encompassing both Girard’s webs and hypercoherences have been proposed independently by Lamarche [18] (based on quantale-valued sets) and by Winskel [30] (based on a notion of indexing inspired by logical relations). We believe that our biordering treatment can be applied to all these categories. We checked this for hypercoherences. There, the binary coherence relation ⌢ ⌣ is replaced by a coherence hypergraph Γ. Thus, a hypercoherence is given by a set E of events and a set Γ of finite non-empty subsets of E. We axiomatise “hypercoherence-bistructures” exactly like bistructures, replacing ⌢ ⌣ by Γ, and Axiom 3 by:

3(a) (X ∈ Γ and X is ≤^{L} −lower bounded) ⇒ X is a singleton,
3(b) X is ≤^{R} −upper bounded ⇒ X ∈ Γ

The variation works smoothly because there is very little interaction between the axiomatisation of the coherence structure and that of the orders. The two propagate smoothly in the construction of the connectives, and are related only through Axiom 3 or its variants.

Although the bidomain model incorporates both the stable and pointwise order, its PCF theory (those inequalities on terms which hold in the bidomain model) does not include that of the Scott model. The argument follows Jim and Meyer’s in [13], and is based on the bidomain model failing to eliminate an “or-tester”, the first of Curien’s examples in [5], Proposition 4.4.2. The same argument applies to the variation sketched above, where coherence is replaced by hypercoherence. In [29] it is shown how to adjoin an additional conflict relation to bistructures to obtain a model of PCF whose theory strictly includes that of the Scott model. Several strengthenings of this idea are possible; the conflict relation can be combined with hypercoherences on bistructures, or even replaced by coherence relations of a more complex kind (akin to logical relations, as in [30]).

As remarked in the introduction, by Loader’s result [19] there is no hope of finding a direct presentation of the fully abstract model for PCF in this way, adjoining a suitable coherence structure to the two orders of bistructures, unless, as in [22], this is of an infinitary nature. However, the fact that there are hypercoherence-based bistructure models refining the Scott model shows (adapting the “Definability Lemma”, e.g., Proposition 4.1.10 of [5], to a slightly broader setting) that there are extensions of PCF, having some claims to being sequential and functional, but which nevertheless have an effectivelygiven fully abstract model. Such extensions to PCF escape Loader’s proof. But the precise programming constructs associated with these extensions is a mystery, and would need a deeper understanding of the operational nature of bistructure models.

Connections. Lamarche [17] (followed by Kegelmann [15]) has proposed a large cartesian closed category of “interpolative domains” encompassing, as full sub-cartesian closed categories, categories of continuous functions on one hand, and categories of stable functions on the other. Lamarche’s framework has some technical similarities with ours; two orders are axiomatised, with a factorisation property. But the approach and goals are quite different. In Lamarche’s setting, once the standard interpretation of the basic flat domains of, say, PCF, is fixed appropriately, the larger category induces exactly the continuous or stable model, whereas we obtain a model simultaneously refining both the stable and continuous models.

Acknowledgements

Gordon Plotkin’s research was supported by an EPSRC Senior Fellowship.

References

[1] Abramsky, S., Jagadeesan, R., and Malacaria, P., Games and full abstraction for PCF, manuscript available from http://www.dcs.ed.ac.uk, 1995.

[2] Berry, G., Modèles complètement adéquats et stables des lambda-calculs typés. Thèse de Doctorat d’Etat, Université de Paris VII, 1979.

[3] Berry, G., Curien, P.-L. and Lévy, J.-J., The full abstraction problem: state of the art, in Proc. French-US Seminar on the Applications of Algebra to Language Definition and Compilation, Cambridge University Press, 1985.

[4] Bierman, G.M., What is a categorical model of intuitionistic linear logic?, in Proc. 2nd. Int. Conf. on Typed Lambda Calculi and Applications (eds. Dezani-Ciancaglini, M. and Plotkin, G.), LNCS, Vol. 902, pp. 78–93, Springer-Verlag, 1995.

[5] Curien, P.-L., Categorical combinators, sequential algorithms, and functional programming. Second edition, Birkhäuser, 1993.

[6] Curien, P.-L., On the symmetry of sequentiality, in Proc. 9th Int. Conf. on Mathematical Foundations of Programming Semantics (eds. Brookes, S., Main, M., Melton, A., Mislove, M. and Schmidt, D.), LNCS, Vol. 802, pp. 29–71, Springer-Verlag, 1994.

[7] Curien, P.-L., Coherence bistructures, unpublished manuscript, Beijing, 1994.

[8] Ehrhard, T., Hypercoherences: a strongly stable model of linear logic. MSCS, Vol. 3, No. 4, pp. 365–385, 1993.

[9] Ehrhard, T., A relative PCF-definability result for strongly stable functions, available by ftp at iml.univ-mrs.fr, in directory /pub/ehrhard/rel.[dvi,ps].Z, 1996.

[10] Girard, J-Y., Linear logic. TCS Vol. 50, No. 1, pp. 1–102, 1987.

[11] Girard, J-Y., Lafont, Y., and Taylor, P., Proofs and types. Cambridge University Press, 1989.

[12] Hyland, J.M.E., and Ong, C-H.L., On full abstraction for PCF: I, II and III, available by ftp at ftp.comlab.ox.ac.uk, in directory /pub/Documents/techpapers/Luke.Ong/pcf.ps.gz, 1994.

[13] Jim, T., and Meyer, A., Full abstraction and the context lemma. in Proc. 1st. Int. Conf. on Theoretical Aspects of Computer Software (eds. Ito, T. and Meyer, A.R.), Sendai, LNCS Vol. 526, pp. 131–152, Springer-Verlag, 1991.

[14] Kahn, G. and Plotkin, G., Concrete Domains, in A Collection of Contributions in Honour of Corrado Böhm on the Occasion of his 70th Birthday. TCS Vol. 121, Nos. 1–2, pp. 187–278, 1993.

[15] Kegelmann, M., Factorization systems on domains, Technical Report, School of Computer Science, The University of Birmingham, 1996.

[16] Lamarche, F., Sequentiality, games and linear logic, in Proc. CLICS Workshop, Aarhus University, Aarhus University DAIMI PB-397 (II), 1992.

[17] Lamarche, F., A large cartesian closed category of domains, to appear in Inform. and Comp.

[18] Lamarche, F., Generalizing coherence spaces and hypercoherences, in Proc. 11th. Int. Conf. on Mathematical Foundations of Programming Semantics (eds. Brookes, S., Main, M., Melton, A. and Mislove, M.), Electronic Notes in Theoretical Computer Science, pp. 259–268, North-Holland, 1995.

[19] Loader, R., Finitary PCF is not decidable. Submitted for publication, 1996.

[20] Milner, R., Fully Abstract Models of Typed λ-calculi, in Theoretical Comp. Sci., Vol. 4, pp. 1–22, 1977.

[21] Nielsen, M., Plotkin, G., and Winskel, G., Petri nets, event structures and domains, part I. TCS, Vol. 13, No. 1, pp. 85–108, 1981.

[22] O’Hearn, P.W. and Riecke, J.G., Kripke logical relations and PCF. Inform. and Comp., Vol. 120, No. 1, pp. 107–116, 1995.

[23] Plotkin, G., and Winskel, G., Bistructures, bidomains and linear logic, in Proc. 21st ICALP (eds. Abiteboul, S., and Shamir, E.), LNCS, Vol. 820, pp. 352–363, Springer-Verlag, 1994.

[24] Seely, R.A.G., Linear logic, ⋆-autonomous categories and cofree coalgebras, in Categories in Computer Science and Logic (eds. Gray, J.W. and Scedrov, A.), Contempory Mathematics, Vol. 92, pp. 371–382, American Mathematical Society, 1989.

[25] Winskel, G., Events in computation. Ph.D. thesis, University of Edinburgh, CST-10-80, 1980.

[26] Winskel, G., Event structures, in Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, (eds. Brauer, W., Reisig, W. and Rozenberg, G.), LNCS, Vol. 255, pp. 325–392, Springer-Verlag, 1987.

[27] Winskel, G., An introduction to event structures, in REX School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, (eds. de Bakker, J.W., de Roever, W.P. and Rozenberg, G.), LNCS, Vol. 354, pp. 364–397, Springer-Verlag, 1989.

[28] Winskel, G., The formal semantics of programming languages, MIT Press, 1993

[29] Winskel, G., Stable bistructure models of PCF, in Proc. 19th Int. Conf. on Mathematical Foundations of Programming Semantics, (eds. Prívara, I., Rovan, B., and Ružička, P.,) LNCS, Vol. 841, Springer-Verlag, 1994.

[30] Winskel, G., Hypercoherences, handwritten notes, 1994.

[31] Zhang, G.Q., Logic of domains. Birkhäuser, 1991.