BRICS RS-94-9 Plotkin & Winskel: Bistructures, Bidomains and Linear Logic

BRICS

Basic Research in Computer Science

Bistructures, Bidomains and Linear Logic

Gordon Plotkin Glynn Winskel

BRICS Report Series RS-94-9 ISSN 0909-0878 May 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

Bistructures, Bidomains and Linear Logic

Gordon Plotkin

LFCS, Comp. Sc. Dept. Edinburgh University Edinburgh, Scotland Glynn Winskel BRICS^{1}, Comp. Sc. Dept. Aarhus University Aarhus, Denmark

Abstract Bistructures are a generalisation of event structures to represent spaces of functions at higher types; the partial order of causal dependency is replaced by two orders, one associated with input and the other 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 associated co-Kleisli category which is equivalent to a cartesian-closed full subcategory of Berry’s bidomains.

1 Introduction

Girard has shown how to implement and analyse intuitionistic logic in his more primitive linear logic. When we look to models this is reflected in the fact that cartesian-closed categories (categorical models for intuitionistic logic) arise as co-Kleisli categories associated with the categorical models of linear logic. In particular, linear logic is leading to refined analyses of the categories of domains used in denotational semantics. For instance, recent work on sequentiality, obtaining intensional fully-abstract models of the programming language PCF [1, 6], has been informed by the insight that Berry and Curien’s category of concrete data structures and sequential algorithms [3] is got as a co-Kleisli category from a games model of linear logic [3, 7].

Bistructures were introduced in [10] as a generalisation of event structures to represent a full subcategory of Berry’s bidomains [2]. Bidomains possess an intensional, stable ordering, based on the method of computation, and an extensional ordering, inherited from Scott’s domain theory; their morphisms are functions which respect both, a property shared by functions definable in PCF. Here we show that, with a small modification to their original definition, bistructures can be equipped with morphisms to form a model of classical linear logic. Through this observation we provide an explanation of a cartesian-closed full subcategory of bidomains as the co-Kleisli category got from a linear category of bistructures with a suitable comonad for the exponential !. This result fits into a more general programme. We are interested in weaker axioms for bistructures, variations in the exponential, and extensions of bistructures to models other than event structures, one motivation being to understand extensional fully abstract models of languages like PCF.

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

The work presented here can be viewed as generalising Girard’s model of classical linear logic of webs (E, ⌣) [5]; as morphisms one considers relations α ⊆ E × E′ where it is required that for a α a′ and b α b′:^{2}

a ⌢ ⌣ b ⇒ a′ ⌢ ⌣ b′ and a′ ⌣ ⌢ b′ ⇒ a ⌣ ⌢ b.

This category is equivalent to the category of coherence spaces and linear functions. The stable functions are obtained via the co-Kleisli construction associated with the model. Adding a partial order, we obtain event structures (E, ≤, ⌣) which represent coherent prime algebraic domains [8], and, with a finiteness axiom added, coherent dI-domains [2, 11, 12]. We can consider the corresponding categories of relations, again representing the linear stable functions; we must now add the condition:

a α b ≥ b′ ⇒ ∃a′ ≤ a. a′ α b′

However, this only yields a model of intuitionistic linear logic [11, 13]. By passing to bistructures we add enough objects to obtain again a model of classical linear logic.

2 Motivation

Recall that an event structure is a structure (E, ≤, ⌣) where

• E is a set of events,

• ≤ is a partial order of causal dependency

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

2Throughout 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.

e ⌣ e′ ≤ e′′ ⇒ e ⌣ e′′.

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

• consistent: ∀e_{1}, e_{2} ∈ x. e_{1} ⌢ ⌣ e_{2},

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

Ordered by inclusion, the configurations (Γ(E), ⊆), form a coherent prime algebraic domain [8]; such domains are precisely the infinitely distributive, coherent Scott domains [12]. 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′, that the event e can only after e′ has ocurred. 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 domains which are precisely the coherent dI-domains of Berry [2].

If we ignore for the moment the intended interpretation of event structures, temporarily forgetting the axiom of finite causes, we can move quickly to a model of intuitionistic linear logic. The categorical model we have in mind is equivalent to the category of coherent prime algebraic domains, with additive functions (i.e. functions preserving arbitrary lubs). The category has as objects event structures (without the axiom of finite causes) and morphisms configurations of a “function space” of event structures, constructed as follows: 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} & e_{1} ≤_{1} e′_{1}
and (e_{0}, e_{1}) ⌣ (e′_{0}, e′_{1}) ⇔ e_{0} ⌢ ⌣_{0} e′_{0} & e_{1} ⌣_{1} e′_{1}.

The configurations of E_{0} ⊸ E_{1} correspond to additive functions from Γ(E_{0}) to Γ(E_{1})—additive functions are determined by their action on complete primes^{3} which correspond to events. The inclusion ordering on configuration reflects the Scott pointwise ordering on functions; in particular, the function events (e_{0}, e_{1}) correspond to special step functions and the order ≤ to the Scott order between them.

3A complete prime of a Scott domain (D, ⊑) is an element p for which whenever p ⊑ ⨆ X then p ⊑ x for some x ∈ X.

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 [9]; 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} & e_{1} ≤_{1} e′_{1}
and (e_{0}, e_{1}) ⌢ ⌣ (e′_{0}, e′_{1}) ⇔ e_{0} ⌢ ⌣_{0} e′_{0} & e_{1} ⌢ ⌣_{1} e′_{1}.

Monoidal-closure follows from the isomorphism

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

natural in event structures E_{0}, E_{1}, 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 finite configurations Γ(E)^{0}, on which incompatibility with respect to inclusion is denoted by ∤↑. The continuous functions Γ(E_{0}) → Γ(E_{1}), between configurations of event structures E_{0}, E_{1}, are in 1-1 correspondence with configurations of !E_{0} ⊸ E_{1}

But a price has been paid. In this model of 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}) of event structures E_{i} = (E_{i}, ≤_{i}, ⌣_{i}), i = 0, 1. Its events are ordered by:

(e_{0}, e_{1}) ≤ (e′_{0}, e′_{1}) ⇔ e′_{0} ≤_{0} e_{0} & 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, the extensional/Scott ordering on functions never made any pretence of being a relation of causal dependency, so it is 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 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} & e_{1} = e′_{1} \\ (e_{0}, e_{1}) ≤^{R} (e′_{0}, e′_{1}) & ⇔ e′_{0} = e_{0} & 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}) & (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 the converse ordering ≥^{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 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/Scott 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. Following Girard, 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 nonconflicting but distinct events b and c. A stable function should not have ≤^{L}-downwards compatible distinct events in its trace. For stable functions, the stable/Berry ordering is obtained as inclusion of traces.

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

To summarise:

• additive functions correspond to ≤-downwards-closed, consistent subsets of events of E_{0} ⊸ E_{1},

• the extensional/Scott order corresponds to inclusion of ≤-downwards-closed subsets of events,

• the trace of a function corresponds to its ≤^{L}-maximal events,

• if a function is stable then no two distinct events in its trace are ≤^{L}- downwards compatible, i.e. for e_{1}, e_{2} in its trace, e_{1} ↓^{L} e_{2} implies e_{1} = e_{2}, where e_{1} ↓^{L} e_{2} ⇔_{def} ∃e. e ≤^{L} e_{1} & e ≤_{L} e_{2}.

• the stable/Berry order corresponds to inclusion of traces.

But, of course, several of these observations are based on a special case, that where we construct the function space of ordinary event structures. We have not yet specified how to repeat the function-space construction at higher orders, when the event structures come already equipped with ≤^{L} and ≤^{R} orders. And what axioms should such structures satisfy?

3 Bistructures

The following definition of bistructures provides an answer to the question just raised as well as yielding a model of classical linear logic.

Definition: A bistructure consists of

(E, ≤^{L}, ≤^{R}, ⌣)

where E is a countable set, ≤^{L}, ≤^{R} are partial orders on E and ⌣ is a binary irreflexive symmetric relation on E for which:

1. Defining ≤= (≤^{L} ∪ ≤^{R})^{∗}, we have the unique factorisation prop-

erty:

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

[It follows that ≤ is a partial order.]

2. Defining ⪯= (≥^{L} ∪ ≤^{R})^{∗},

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

(b) ⪯ is a partial order.

3. (a) ↓^{L} ⊆ ≍ (b) ↑^{R} ⊆ ⌢ ⌣ The two compatibility relations mean

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

Ordinary, countable event structures, (E, ≤, ⌣), satisfying the axiom of finite causes, yield special bistructures (E, 1_{E}, ≤, ⌣), in which the ≤^{L} order is degenerate.

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

• consistent: ∀e_{1}, e_{2} ∈ x. e_{1} ⌢ ⌣ e_{2},

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

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

A helpful case to consider is that where the bistructure represents a space of functions, as in the introduction. Configurations then correspond to traces. Because ↓^{L} is included in ⌣ ⌢, consistency has the force of ensuring the functions represented are stable. The securedness condition says that for any output, lesser output must have arisen previously through the same or lesser input.

Γ(E) possesses two orderings making it into a Berry bidomain; the inclusion order corresponds to the stable order while the Scott extensional order is obtained by:

x ⊑ y iff ∀e ∈ x∃e′ ∈ y. e ≤^{L} e′

This is equivalent to every event of x being ≤-below some event of y.

Proposition 1 (Γ(E), ⊆, ⊑) is a Berry bidomain.

Proof: The proof is essentially as in [10] (Theorem 9.9.8—relying on 9.4.8). □

4 A category of bistructures

Morphisms between bistructures will correspond to configurations of a function-space construction. They will determine (special) extensional, linear (= stable and additive) functions on bidomains. Assuming E_{i} = (E_{i}, ≤_{i}^{L}, ≤_{i}^{R}, ⌣_{i}), for i = 0, 1, are bistructures, define their linear function space 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} & e_{1} ≤^{L} e′_{1}
(e_{0}, e_{1}) ≤^{R} (e′_{0}, e′_{1}) ⇔ e′_{0} ≤^{L} e_{0} & e_{1} ≤_{1}^{R} e′_{1}
and (e_{0}, e_{1}) ⌣ ⌢ (e′_{0}, e′_{1}) ⇔ e_{0} ⌢ ⌣_{0} e′_{0} & e_{1} ⌣ ⌢_{1} e′_{1}.

We define the category of bistructures BS by taking morphisms E_{0} to E_{1} to be configurations of E_{0} ⊸ E_{1}, composed as relations. Of course, we should show that this composition is well-defined and has identities. First we observe that with this definition, morphisms of bistructures generalise those of Girard on webs (E, ⌣)—see the introduction:

Proposition 2 A configuration of E_{0} ⊸ E_{1}, for bistructures E_{0}, E_{1}, consists of a morphism α from the web of E_{0} to the web of E_{1} which satisfies:

e′_{0} ≥^{L} e_{0}αe_{1} ≥^{R} e′_{1} ⇒ ∃e′′_{0}, e′′_{1}. e′_{0} ≥^{R} e′′_{0}αe′′_{1} ≥^{L} e′_{1}

Proof: Consistency of a configuration of a function space amounts to the relation being a morphism between the underlying webs. Securedness is equivalent to the condition of the proposition. □

Lemma 3 Let α be a configuration of E_{0} ⊸ E_{1} and β a configuration of E_{1} ⊸ E_{2}. Then their relational composition β ∘ α is a configuration of E_{0} ⊸ E_{2}. A bistructure E ⊸ E has the identity relation as a configuration.

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 consistent and secured. Consistent: From the definition of ⌣ ⌢ on function space we require that for (a, c), (a′, c′) ∈ β ∘ α that

(i) a ⌢ ⌣ a′ ⇒ c ⌢ ⌣ c′ and (ii) c = c′ ⇒ a ⌣ ⌢ a′,

facts which hold of the composition β ∘ α because they hold of α and β. Secured: Suppose (a, c) ∈ β ∘ α and that

(a_{0}, c_{0}) ≤^{R} (a, c),

i.e., a ≤^{L} a_{0} & c_{0} ≤^{R} c. It is required that there is

(a′, c′) ∈ β ∘ α

such that

(a_{0}, c_{0}) ≤^{L} (a′, c′),

i.e., a′ ≤^{R} a_{0} & c_{0} ≤^{L} c′. [In the following argument, it is helpful to refer to the diagram below.]

As (a, c) ∈ β ∘ α there is b′_{0} such that (a, b′_{0}) ∈ α and (b′_{0}, c) ∈ β. Because c_{0} ≤^{R} c, we obtain that

(b′_{0}, c_{0}) ≤^{R} (b′_{0}, c).

As β is secured there is (b_{1}, c_{1}) ∈ β for which (b′_{0}, c_{0}) ≤^{L} (b_{1}, c_{1}), i.e.,

(b_{1}, c_{1}) ∈ β & b_{1} ≤^{R} b′_{0} & c_{0} ≤^{L} c_{1}.  (1β)

As a ≤^{L} a_{0} and b_{1} ≤^{R} b′_{0}, we have (a_{0}, b_{1}) ≤^{R} (a, b′_{0}). But α is secured, so there is (a_{1}, b′_{1}) ∈ α for which (a′_{0}, b_{1}) ≤^{L} (a_{1}, b′_{1}), i.e.

(a_{1}, b′_{1}) ∈ α & a_{1} ≤^{R} a_{0} & b_{1} ≤^{L} b′_{1}.  (1α)

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

a_{0} ≥^{R} a_{1} α b′_{1} ≥_{L} b_{1} β c_{1} ≥^{L} c_{0}  (1)

This pattern in a_{1}, b′_{1}, b_{1}, c_{1} must repeat by the next argument.

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

(b_{2}, c_{2}) ∈ β & b_{2} ≤^{R} b′_{1} & c_{1} ≤^{L} c_{2}  (2β)

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

(a_{2}, b′_{2}) ∈ α & a_{2} ≤^{R} a_{1} & b_{2} ≤^{L} b′_{2}  (2α)

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

a_{0} ≥^{R} a_{2} α b′_{2} ≥_{L} b_{2} β c_{2} ≥^{L} c_{0}  (2)

where b_{2} ≤^{R} b′_{1}. This can be repeated infinitely. In a diagram:

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; b′_{0}; b_{1}; b′_{1}; b_{2}; b′_{2}; c_{0}; c; c_{2}; c_{1}; β; β; a; a_{0}; a_{1}; a_{2}; α; L; L; R; R; R; L; β; R; R; L; α; α; L]

The chain

b′_{0} ≥^{R} b_{1} ≤^{L} b′_{1} ≥^{R} b_{2} ≤^{L} b′_{2} ≥^{R} ⋯

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

(a_{n}, b′_{n}) ∈ α & b_{n} = b′_{n} & (b_{n}, c_{n}) ∈ β

making (a_{n}, c_{n}) ∈ β ∘ α with a_{n} ≤^{R} a_{0} and c_{0} ≤^{L} c_{n}, i.e. (a_{0}, b_{0}) ≤^{L} (a_{n}, c_{n})—and (a_{n}, c_{n}) fulfils the requirements we seek for (a′, c′). □

Using the same kind of well-foundedness argument as in the proof of Lemma 3 above, we can show:

Proposition 4 Let F be a configuration of E_{0} ⊸ E_{1} and x a configuration of E_{0}. Defining

F.x = {b | ∃a ∈ x. (a, b) ∈ F }

yields a configuration of E_{1}. The function x ↦ F.x : Γ(E_{0}) → Γ(E_{1}) is linear with respect to ⊆ and continuous with respect to ⊑. [Not all such functions are represented, unless events of E_{0} correspond to complete primes of Γ(E_{0}).]

5 A model of classical linear logic

Here we give the constructions showing that BS is a model of classical linear logic. 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}^{⊥})^{⊥}

and have a form generalising those of Girard’s constructions on coherence spaces. The construction E^{⊥} is isomorphic to (E ⊸ 1) where 1 = ({•}, 1, 1, ∅) is the unit of ⊗. The product in the category BS is given by

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

obtained as the juxtaposition of the two bistructures, assumed disjoint, so for example ⌣=⌣_{0} ∪ ⌣_{1}. The coproduct E_{0} + E_{1}, isomorphic to (E_{0}^{⊥} × E_{1}^{⊥})^{⊥}, is again obtained as the disjoint juxtaposition of the two bistructures, but this time extending conflict across the two components.

To get the exponential !E, of a bistructure E, we first define orderings on the finite configurations Γ(E)^{0}. For x, y ∈ Γ(E)^{0} define

\begin{matrix}x ⊑^{R} y ⇔ & x ⊆ y \\ x ⊑^{L} y ⇔ & x ⊑ y & (∀y′ ∈ Γ(E). x ⊑ y′ & y′ ⊆ y ⇒ y = y′). \end{matrix}

Thus, x ⊑^{L} y means y is a ⊆-minimum configuration s.t. x ⊑ y. Now define

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

where x ↑^{R} y ⇔_{def} ∃z ∈ Γ(E). x, y ⊆ z.

Notation: Let E = (E, ≤^{L}, ≤^{R}, ⌣) be a bistructure.

Let x ∈ Γ(E). Let e ∈ E be in the ≤-downwards closure of x, i.e., e ≤ e′, for some e′ ∈ x. Factorising ≤, we obtain e ≤^{L} e′′ ≤^{R} e′, and as x is a configuration there is a unique e_{max} ∈ x such that e′′ ≤^{L} e_{max}. This shows that any event e in the ≤-downwards closure of a configuration x is ≤^{L}-dominated by a unique event e_{max} in x. We write m(e, x) for this event e_{max}.

For x ∈ Γ(E)^{0}, we define the relativised relation ⪯_{x} as the reflexive, transitive closure of ⪯_{x}^{1} where, for e, e′ ∈ x,

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

Lemma 5 For a bistructure E, let x, y ∈ Γ(E)^{0},

\begin{matrix}(i) & x ↑^{R} y & e ∈ x ∩ y ⇒ (∀e′ ∈ E. e′ ⪯_{x} e ⇔ e′ ⪯_{y} e) \\ (ii) & x ⊑^{L} y ⇔ x ⊑ y & ∀e′ ∈ y∃e ∈ x. e′ ⪯_{y} m(e, y). \end{matrix}

Lemma 6 !E is a bistructure.

Proof: The main difficulty in the proof is in showing 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} & x_{n} = x_{0} & x′_{n} = x′_{0} (1)

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. We show that it is secured. Suppose e ∈ fix and ε ≤^{R} e. Consider the chain (1). As x_{0} ⊑^{R} x′_{0} we have m(ε, x_{0}) = m(ε, x′_{0}) by the consistency of x′_{0}. At the next link in the chain x′_{0} ⊒^{L} x_{1} with ε in the ≤-downwards closure of x′_{0} and x_{1} so m(ε, x′_{0}) ≥^{L} m(ε, x_{1}) by the consistency of x′_{0}. Continuing in this way along the chain (1) we get:

m(ε, x_{0}) = m(ε, x′_{0}) ≥^{L} m(ε, x_{1}) = m(ε, x′_{1}) ≥^{L} m(ε, x_{2}) = m(ε, x′_{2}) ⋯ ≥^{L} m(ε, x_{n})

But x_{0} = x_{n} so m(ε, x_{0}) = m(ε, x_{n}). As ≤^{L} is a partial order, m(ε, x_{i}) = m(ε, x_{0}) for all i. Thus m(ε, x_{0}) ∈ fix, so 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. By symmetry, it suffices to show x_{0} = x′_{0} = fix.

Take e ∈ x′_{0}. Then by repeated use of Lemma 5(ii), characterising ⊑^{L}, 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} ė_{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 p.o., 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}, it follows that all elements of the chain are in fix—at ≥^{L}-links this follows from the consistency of each x′_{i} and at ⪯_{x′_{i}}-links by Lemma 5(i). In particular, e_{0}(= e) must be the earliest element of (2) in fix. But e was chosen to be an arbitrary event in x′_{0}. Thus x′_{0} = fix. Therefore x_{0} = x′_{0} = fix as required. □

The bistructure, !E_{0} ⊸ E_{1}, has configurations in 1-1 correspondence with elements in the function space [(Γ(E_{0}), ⊆, ⊑) → (Γ(E_{1}), ⊆, ⊑)] in the cartesian-closed category of Berry’s bidomains:

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

R̄(x) = {e | ∃x_{0} ⊆ 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 ⊆ on configurations. In fact, R ↦ R̄ is a 1-1 correspondence between configurations of !E_{0} ⊸ E_{1} and such functions.

Proof: First observe that the configurations of !E_{0} are precisely those sets

x^{+} = {y ∈ Γ(E_{0})^{0} | y ⊆ x}

for some x ∈ Γ(E_{0})—again Γ(E_{0})^{0} denotes the finite configurations of E_{0}. Noting

R̄(x) = R.(x^{+}), for x ∈ Γ(E_{0})

it follows by Proposition 4 that R̄(x) ∈ Γ(E_{1}), so that R̄ is well-defined as a function Γ(E_{0}) → Γ(E_{1}). Moreover, the ⊑-continuity and ⊆-stability of R̄ follow directly from the corresponding properties of the linear function x ↦ R.x : Γ(!E_{0}) → Γ(E_{1}).

We now construct an inverse to R ↦ R̄. Suppose f : Γ(E_{0}) → Γ(E_{1}) is ⊑-continuous and ⊆-stable. Define φ(f) to be the trace of f, i.e.

φ(f) = {(x, e) ∈ Γ(E_{0})^{0} × E_{1} | x is minimal s.t. e ∈ f(x)}

We need first that φ(f) ∈ Γ(!E_{0} ⊸ E_{1}), i.e. that φ(f) is consistent and secured:

Consistent: Suppose (x, e), (x′, e′) ∈ φ(f) and that (x, e) ≍ (x′, e′)i.e.x ↑^{R} x′ & 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 φ(f) the trace of f. Because x ↑^{R} x′ and f is ⊆-stable we conclude that x = x′.

Secured: Suppose (x′, e′) ≤^{R} (x, e) ∈ φ(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

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

where e′′ = m(e′, f(x′)) ∈ f(x). As f is ⊆-stable, there is

x_{0} ⊆ x′  (2)

with (x_{0}, e′′) in its trace, i.e.

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

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

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

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

More completely, this section provides the key constructions in showing:

Theorem 8 The category BS forms a linear category in the sense of [9]. 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 [9]). The associated co-Kleisli category is equivalent to a cartesian-closed full subcategory of Berry’s bidomains, where morphisms are continuous with respect to the Scott order and stable with respect to the Berry order.

References

[1] Abramsky, S., Jagadeesan, R., and Malacaria, P., Games and full abstraction for PCF (first and second preliminary announcement). Linear Logic and Types electronic newsgroups, 1993.

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

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

[4] Girard, J-Y., Linear logic. Theoretical Computer Science 50, 1987.

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

[6] Hyland, J.M.E., and Ong, C-H.L., Games and full abstraction for PCF. Linear Logic and Types electronic newsgroups, 1993.

[7] Lamarche, F., Sequentiality, games and linear logic. Proceedings of the CLICS Workshop, Aarhus University, March 1992, Aarhus University DAIMI PB-397 (II), 1992.

[8] Nielsen, M., Plotkin, G., and Winskel, G., Petri nets, Event structures and Domains, part 1. Theoretical Computer Science, vol. 13, 1981.

[9] Seely, R.A.G., Linear logic, ∗-autonomous categories and cofree coalgebras. Contempory Mathematics, vol.92, 1989.

[10] Winskel, G., Events in Computation. PhD thesis, University of Edinburgh, available as a Comp. Sc. report, 1980.

[11] Winskel, G., Event structures. Lectures for the Advanced Course on Petri nets, September 1986, Springer Lecture Notes in C.S., vol.255, 1987.

[12] Winskel, G., An introduction to event structures. In the lecture notes for the REX summerschool in temporal logic, May 88, in Springer Lecture Notes in C.S., vol.354, 1989.

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

Recent Publications in the BRICS Report Series

RS-94-1 Glynn Winskel. Semantics, Algorithmics and Logic: Basic Research in Computer Science. BRICS Inaugural Talk. February 1994, 8 pp.

RS-94-2 Alexander E. Andreev. Complexity of Nondeterministic Functions. February 1994, 47 pp.

RS-94-3 Uffe H. Engberg and Glynn Winskel. Linear Logic on Petri Nets. February 1994, 54 pp. To appear in Proceedings of REX, LNCS, 1993.

RS-94-4 Nils Klarlund and Michael I. Schwartzbach. Graphs and Decidable Transductions based on Edge Constraints. February 1994, 19 pp. Appears in: Trees in Algebra and Programming CAAP ’94 (ed. S. Tison), LNCS 787, 1994.

RS-94-5 Peter D. Mosses. Uni�ed Algebras and Abstract Syntax. March 1994, 21 pp. To appear in: Recent Trends in Data Type Speci�cation (ed. F. Orejas), LNCS 785, 1994.

RS-94-6 Mogens Nielsen and Christian Clausen. Bisimulations, Games and Logic. April 1994, 37 pp. Full version of paper to appear in: New Results and Trends in Computer Science, LNCS, 1994.

RS-94-7 Andr� e Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from Open Maps. May 1994, 42 pp. Journal version of LICS ’93 paper.

RS-94-8 Javier Esparza and Mogens Nielsen. Decidability Issues for Petri Nets. 1994, 23 pp.

RS-94-9 Gordon Plotkin and Glynn Winskel. Bistructures, Bidomains and Linear Logic. May 1994, 16 pp. To appear in the proceedings of ICALP ’94, LNCS, 1994.

RS-94-10 Jakob Jensen, Michael J�rgensen, and Nils Klarlund. Monadic second-order Logic for Parameterized Veri�cation. May 1994.

RS-94-11 Nils Klarlund. A Homomorphism Concept for ω-Regu-larity. May 1994.