BRICS RS-94-13 G. Winskel: Stable Bistructure Models of PCF

BRICS

Basic Research in Computer Science

Stable Bistructure Models of PCF

Glynn Winskel

BRICS Report Series RS-94-13 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

Stable bistructure models of PCF

Preliminary draft

Glynn Winskel

BRICS^{1}, Comp. Sc. Dept. Aarhus University Aarhus, Denmark

Abstract

Stable 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. They represent Berry’s bidomains. The representation can proceed in two stages. Bistructures form a categorical model of Girard’s linear logic consisting of a linear category together with a comonad. The comonad has a co-Kleisli category which is equivalent to a cartesian-closed full subcategory of Berry’s bidomains. A main motivation for bidomains came from the full abstraction problem for Plotkin’s functional language PCF. However, although the bidomain model incorporates both the Berry stable order and the Scott pointwise order, its PCF theory (those inequalities on terms which hold in the bidomain model) does not include that of the Scott model. With a simple modification we can obtain a new model of PCF, combining the Berry and Scott orders, which does not have this inadequacy.

1 Introduction

Plotkin’s PCF is a programming language based on typed lambda calculus with recursion. It has proved difficult to obtain a domain theory which yields a fully abstract model for PCF, one where the inequations on terms given by the domain orderings coincide with those inequations obtained from the operational semantics, where it is said that one term approximates another if in any closed context at ground type its convergence implies the other’s convergence to the same value. In particular, the obvious Scott model, based on domains and continuous functions ordered pointwise, is not fully abstract.

Event structures and related models can be used to represent domains in the semantics of programming languages. For example, event structures give a representation of Berry’s cartesian closed category of dIdomains and stable functions [2, 18], while Berry and Curien’s category of sequential algorithms on Kahn and Plotkin’s concrete datastructures provides a domain theory in which the method of computation is represented explicitly [3]. These two domain theories can be used to give models of PCF. But they do not give order-extensional models; a model is orderextensional if elements of the function spaces are ordered according to the pointwise order. If we limit attention to extensional models, that is models where denotations correspond to functions between input and output values, then from Milner’s results [12] it is known that any extensional model of PCF which is fully abstract is necessarily order-extensional.

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

Here we focus on stable-bistructure models of PCF, as a means to obtain order-extensional models which at the same time take some account of the way a function is computed. Stable bistructures were introduced in [17] 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, pointwise ordering, inherited from Scott’s domain theory; their morphisms are functions which respect both, a property shared by functions definable in PCF. The represention of bidomains goes via a view of bistructures as a categorical model of Girard’s linear logic [8]. The model consists of a linear category of bistructures together with a comonad; a category of bistructures equivalent to a cartesian-closed full subcategory of bidomains is obtained as the coKleisli category of the model. The work here overlaps with that of [15] which shows bistructures form a model of classical linear logic.

In particular, it is shown how to correct an inadequacy of Berry’s bidomains; 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 (cf. [10]), essentially because the model fails to eliminate the first of Curien’s examples in [7], Proposition 4.4.2. Adjoining an additional conflict relation to bistructures leads to a model of PCF bearing a satisfactory relationship to the Scott model. The proof of this fact is inspired by the work of Bucciarelli and Ehrhard in the context of making their coherence models extensional—see e.g. [5] Chapter 8.

Of course, it is hoped that bistructures have a more important role to play in understanding the extensional fully abstract model of PCF. Two rather independent lines of work on sequentiality appear central here: one is the work on coherences and hypercoherences [5, 6]; the other the successes in obtaining intensionally fully abstract models of PCF [1, 9]— models which although not extensional do have the property that every finite element of the domains is definable by a PCF term. The work on hypercoherences combines smoothly with bistructures (as observed jointly with Gordon Plotkin), providing one route to extensional sequential models of PCF, though not directly to the fully abstract model of PCF.

2 PCF

PCF is a programming language based on LCF, Scott’s logic of computable functions. It is a form of typed lambda calculus in which certain terms are singled out as programs.

The set of types is the least set containing o (for booleans), ι (for integers) and (σ → τ) whenever it contains σ and τ. We write (σ_{1}, ⋯, σ_{n}; τ) for

(σ_{1} → ⋯ (σ_{n} → τ) ⋯).

The types o and ι are called ground types.

Terms are produced from the following collection of constant functions with the indicated types:

\underline{0}, \underline{1}, ⋯ \underline{n}, ⋯: type ι  (numerals)
tt, ff : type o  (truth values)
(+1), (−1) : type ι → ι (increment and decrement by 1)
Z : type ι → o  (test for zero)
⊃_{ι} : type (o, ι, ι; ι)  (conditional with integer result)
⊃_{o} : type (o, o, o; o)  (conditional with boolean result)

Starting with the above collection of constants and countably many variables v_{i}, i ∈ ω, for each type the terms are given by the formation rules:

1. Every variable x_{i}^{σ} is a term of type σ.

2. Every constant of type σ is a term of type σ.

3. if M is a term of type σ → σ then Y_{σ}M (its least fixed point) is a term of type σ.

4. If M and N are terms of type σ → τ and σ respectively then MN is a terms of type τ.

5. If M is a term of type τ then λv^{σ}M is one of type σ → τ.

The programs are closed terms of ground type. Intuitively they yield observable output, concrete values consisting of integers or truth values; other terms are significant only as subterms of programs.

An operational semantics is given to the language by defining eval, a partial function from programs to constants. It is defined using an immediate reduction relation → between terms: eval(M) = c iff M →^{∗} c, for any program M and constant c.

The immediate reduction relation is given by:

1. (+1)\underline{n} → \underline{n + 1}

2. (−1)\underline{n + 1} → \underline{n}

3. Z\underline{0} → tt Z\underline{n + 1} → ff

4. ⊃_{σ}ttMN → M ⊃_{σ}ffMN → N, where σ = o, ι

5. If M → M′ then ⊃_{σ}M → ⊃_{σ}M′ for M, M′ of type o, and σ a type o or ι

6. If M → M′ then (MN) → (M′N)

7. If M is (+1) or (−1) or Z and N → N′ then (MN) → (MN′)

8. Y_{σ}M → M(Y_{σ}M)

9. ((λv M)N) → [N/v]M

The relation → is a partial function so eval is well-defined above.

We base the notion of a standard model for PCF on (standard) type structure consisting of:

1. A cpo D_{σ} for each type σ with D_{ι} being isomorphic to the flat cpo of integers and D_{o} to the flat cpo of booleans.

2. For all types σ and τ a two place application operations · : D_{σ→τ} × D_{σ} → D_{τ} which is continuous and order-extensional i.e.

x ⊑ x′ iff ∀y. x · y ⊑ x′ · y.

Condition 2 ensures that the element of D_{σ→τ} are in 1-1 correspondence with a subset of the continuous functions [D_{σ} → D_{τ}] so that the ordering on D_{σ→τ} is the restriction of the pointwise ordering on functions.

With respect to a type structure the environment Env consists of all type-respecting functions ρ from variables into ⋃_{σ} D_{σ}

A standard model for PCF consists of a type structure D and a semantics 𝔐 a type-respecting map giving values in D to terms with respect to an environment ρ. They are required to satisfy the following conditions:

1. The terms \underline{n}, (+1), (−1), Z, ⊃_{o}, ⊃_{ι} and least fixed points get their usual interpretation.

2. 𝔐[[v]]ρ = ρ(v)

𝔐[[MN]] = 𝔐[[M]]ρ · 𝔐[[N]]ρ (𝔐[[λv.M]]ρ) · d = 𝔐[[M]]ρ[d/v]

—ρ[d/v] is the environment obtained from ρ updated so the variable v is assigned the value d.

Not all type structures determine models; there may be simply not enough functions in the domains to support the semantics. An obvious standard model is obtained by taking the type structure so that D_{σ→τ} = [D_{σ} → D_{τ}], all continuous functions from D_{σ} to D_{τ}, with the application operator just the ordinary application of functions. Many other models are possible and according to criteria derived from the operational semantics the obvious model is not the best.

The denotational semantics should “match” the operational semantics. Plotkin defined two natural operational relations. Terms are of interest only insofar as they are part of programs. For this reason it is natural to regard two terms as operationally equivalent if they can be freely substituted for each other in a program without affecting its behaviour. Formally define the equivalence relation between terms of the same type by : M ≈ N iff whenever C[M] and C[N] are programs eval(C[M]) and eval(C[N]) are both undefined or otherwise defined and equal. More generally an operational preorder can be defined by: M≪N iff whenever C[M] and C[N] are programs then whenever eval(C[M]) is c then so is eval(C[N]). Clearly M ≈ N iff M≪N and N≪M. For a semantics 𝔐 the expected semantic counterparts of these two relations are the relations on terms given by M ⊑_{M} N iff 𝔐[[M]]ρ ⊑ 𝔐[[N]]ρ for all ρ, and M =_{M} N iff M ⊑_{M} N and N ⊑_{M} M. In the circumstance when the relations ≪ and ⊑_{M} coincide the semantics 𝔐 is said to be fully abstract.

For a standard semantics 𝔐, Plotkin showed the denotational relations will be included in the corresponding operational ones. However the converse will not generally hold. In particular Plotkin showed the Scott model with the obvious semantics, based on taking D_{σ→τ} as all continuous functions [D_{σ} → D_{τ}] is not fully abstract. The counterexample depended on producing two terms which were operationally equivalent but denotationally distinct through acting differently on “parallel-or”— parallel-or is the continuous function on booleans with ⊥ which extends the usual boolean disjunction and returns true if either argument is true, regardless of whether the other argument is ⊥.

3 Event structures

As a rehearsal for the work on bistructures we will present the Scott model for PCF in terms of event structures. We will show that a full subcategory of Scott domains with continuous functions, viz. the coherent prime algebraic domains [13], is equivalent to a cartesian-closed category of event structures; the continuous function space of two prime algebraic domains can itself be represented by an event structure. The types of PCF can be then be interpreted as event structures. We will present the category of event structures as the coKleisli category of a model of Girard’s linear logic.

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

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 [13]; such domains are precisely the infinitely distributive, coherent Scott domains [19].

An instance of the causal dependency ordering e′ ≤ e when e and e′ are distinct, is usually understood as meaning that the event e causally depends on the event e′, that the event e can only occur after e′ has ocurred. Usually we impose a finiteness axiom:

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

expressing that an event has finite causes. Though we won’t do this here, in order to represent a portion of Scott domain theory via a model of intuitionistic linear logic (an example of a nonstable model of linear logic, cf. [11]).

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},
(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^{2} which correspond to events. While the inclusion ordering on configuration reflects the pointwise ordering on functions; in particular, the function events (e_{0}, e_{1}) correspond to special step functions and the order ≤ to the pointwise order between them.

A morphism from E_{0} to 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. Its tensor, for instance, is given in a coordinatewise fashion: For event structures E_{i} = (E_{i} ≤_{i}, #_{i}), for i = 0, 1, define

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

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} or e_{1}#_{1}e′_{1}.

The comonad operation is

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

for an event structure E, with finite configurations Γ(E)^{0}, on which conflict is defined by

x#_{!}y ⇔ ∃e_{1} ∈ x, e_{2} ∈ y. e_{1}#e_{2},

which is equivalent to incompatibility with respect to inclusion in Γ(E)^{0}. The continuous functions from Γ(E_{0}) to Γ(E_{1}), between configurations of event structures E_{0}, E_{1}, are in 1-1 correspondence with configurations of !E_{0} ⊸ E_{1}. A configuration y of !E_{0} ⊸ E_{1} can be applied to a configuration x of E_{0},

y.x = {e | ∃x_{0} ⊂ x. (x_{0}, e) ∈ y},

yielding a configuration of E_{1}. The association of y to the function (x ↦ y · x) gives the 1-1 correspondence with continuous functions from Γ(E_{0}) to Γ(E_{1}).

Linear types σ, given by

σ ::= o | ι | σ ⊸ σ′| !σ

can be interpreted as event structures C_{σ}. The event structure C_{o} representing the booleans has two events t, f, corresponding to tt, ff, related by the conflict relation and with the identity relation as causal dependency. Similarly, C_{ι} is the event structure representing the flat domain of integers; it has events ω, the natural numbers, pairwise in conflict, with the identity relation as its causal dependency. A type σ ⊸ σ′ denotes the event structure C_{σ} ⊸ C_{σ′}, while !σ denotes the event structure !C_{σ}. Throughout, we will identify a PCF type σ → σ′ with the linear type !σ ⊸ σ′.

We can reformulate the Scott model of PCF via the representation using event structures. In the model a PCF type σ is interpreted as the cpo of configurations Γ(C_{σ}). For M a term of type σ, and for ρ an environment, we define C[[M]]ρ ∈ Γ(C_{σ}). For example,

\begin{matrix}C[[MN]]ρ = & \{e | ∃d ⊆ C[[N]]ρ & (d, e) ∈ C[[M]]ρ\} \\ C[[λvM]]ρ = & \{(d, e) | e ∈ C[[M]]ρ[d/v]\}, \end{matrix}

reflecting the way application and currying are represented in event structures.

It is also possible to give an event structure representation of the stable model of PCF (see e.g. [18]), though this won’t be a standard model in our sense because it isn’t order-extensional. However we can obtain a stable model, which is at the same time order-extensional, by working with bistructures.

4 Bistructures

In the last section we obtained a model of PCF from event structures, but at a price. In this model the order ≤ can no longer be thought of as causal dependency, ≤ does not correspond to precedence in time, and we have lost one of the key intuitions behind event structures. The loss 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}.

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}. Their finitary nature reflects their expressing temporal precedence: increasing with respect to ≤^{R} corresponds to producing further output over time; decreasing with respect to ≤^{L} is associated with inspecting further input. This factorisation is the first step towards the definition of bistructures. We obtain further encouragement when we notice a suggestive characterisation of the stable additive functions. We have already observed that additive functions from Γ(E_{0}) to Γ(E_{1}) correspond to configurations of E_{0} ⊸ E_{1}, i.e. to subsets of events x ⊆ E_{0} × E_{1} which are ≤-downwards closed and consistent. Consider the ≤^{L} maximal events M(x) of such a configuration. The set M(x) will correspond to what Girard calls the trace of the function. The associated function will be stable if whenever events (e_{0}, e_{1}), (e′_{0}, e_{1}) are in M(x) then either e_{0} and e′_{0} are equal or in conflict. Just as inclusion between traces determines the stable order, so an inclusion M(x) ⊆ M(y), for configurations x, y for stable additive functions, means that the functions are in the stable order.

We can jointly enforce the consistency required of all configurations of (E_{0} ⊸ E_{1}) and the extra property of stability by introducing a new conflict relation. For two events (e_{0}, e_{1}), (e′_{0}, e′_{1}) of the linear function space, write (e_{0}, e_{1}) ⌣ (e′_{0}, e′_{1}) iff they are distinct and

¬e_{0}(# ∪ 1_{E_{0}})e′_{0} & e_{1}(# ∪ 1_{E_{1}})e′_{1}.

Stable, additive functions from Γ(E_{0}) to Γ(E_{1}) correspond to configurations x of E_{0} ⊸ E_{1} such that

• x is consistent with respect to the relation ⌣, in the sense that

∀e, e′ ∈ M(x). ¬e ⌣ e′,

• x is downwards closed with respect to ≤.

The new conflict relation ⌣ imposes stability, and we call it stable conflict. Unlike # it is not preserved upwards with respect to ≤. However we observe that it satisfies the weaker axioms: ↓^{L} ⊆ ⌣ ⌢ and ↑^{R} ⊆ ⌢ ⌣.^{3}

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. The definition of stable bistructures (based on that in [17]) arose in extending these results beyond the first order.

3We shall 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.

Definition: A (stable) bistructure consists of

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

where E is a countable set, ≤^{L}, ≤^{R} are partial orders on E, ⌣ is a binary irreflexive symmetric relation on E, called stable conflict, 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.

Let E = (E, ≤^{L}, ≤^{R}, ⌣) be a bistructure. As in the motivating discussion, for x ⊆ E, we take M(x) to consist of the ≤^{L}-maximal events in x, and define an extensional configuration of E, to be a subset x ⊆ E which is

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

• ≤-downwards closed: ∀e, e′. e′ ≤ e ∈ x ⇒ e′ ∈ x .

Alternatively, we can choose to regard the “trace” M(x) itself as a configuration: A stable configuration of the bistructure E is a subset y ⊆ E which is • consistent: ∀e_{1}, e_{2} ∈ y. e_{1} ⌢ ⌣ e_{2},

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

Notice that e′′ is unique in any consistent set because ↓^{L}⊆⌣ ⌢. The securedness condition is quite intuitive. It says that for any output, lesser output must have arisen previously through the same or lesser input. The finiteness axiom 2(a) on bistructures, says that the succession of inspecting input, delivering output, inspecting more input, and so on, leading up to a particular output for some input, is a finite procedure. The intuition that event structures capture temporal precedence, lost in the representation of coherent prime algebraic domains and continuous functions, is regained in this modified form for bistructures.

The two forms of configuration are intimately related. For x ⊆ E, define its ≤-downwards closure to be

⌈x⌉ = {e ∈ E | ∃e′ ∈ x. e ≤ e′}.

Proposition 1 For y a stable configuration, ⌈y⌉ is an extensional configuration. For x an extensional configuration, M(x) is a stable configuration. Moreover, ⌈−⌉ and M(−) are mutual inverses, giving a 1-1 correspondence between stable configurations and extensional configurations.

By Proposition 1, extensional and stable configurations carry the same information. However, here it’s more convenient to work with extensional configurations. We write Γ(E) for the set of extensional configurations of a bistructure E; write Γ(E)^{0} for its finite configurations. (For a development paralleling that here, but based on stable configurations see [15].)

The inclusion orders on the two kinds of configurations, extensional and stable, correspond to the extensional and stable orders of a Berry bidomain:

The order ⊑ is given by inclusion on extensional configurations, and on stable configurations by

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

The order ⊑^{R} is given by inclusion on stable configurations, and on extensional configurations by

x ⊑^{R} y iff M(x) ⊆ M(y).

Proposition 2 (Γ(E), ⊑^{R}, ⊑) is a Berry bidomain in which ⊑^{R} is the stable and ⊑ the extensional order.

Another order on configurations, ⊑^{L}, will come to play an important role. For x, y ∈ Γ(E) define

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

Thus, x ⊑^{L} y means y is a ⊑^{R}-minimum configuration such that x ⊑ y. In characterising ⊑^{L} we use:

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

Let x ∈ Γ(E). Let e ∈ x. Then, by Proposition 1, e ≤ e′, for some e′ ∈ M(x). Factorising ≤, we obtain e ≤^{L} e′′ ≤^{R} e′, and as M(x) is a stable configuration there is a unique e_{max} ∈ M(x) such that e′′ ≤^{L} e_{max}. This shows that any event e in an extensional configuration x is ≤^{L}- dominated by a unique event e_{max} in M(x). We write m(e, x) for this event e_{max}.

For x ∈ Γ(E), 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′′ ∈ M(x). e′′ ≤^{L} e & e′′ ≤^{R} e′.

We characterise compatibility with respect to ⊑^{R} and the order ⊑^{L}:

Lemma 3 For a bistructure E, let x, y ∈ Γ(E),

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

In particular, we obtain a unique factorisation for configurations:

x ⊑ y ⇒ ∃!z. x ⊑^{L} z ⊑^{R} y

—the intermediate value z is such that M(z) is the stable configuration generated by the ≤^{L}-image of x in M(y). The factorisation restricts to finite configurations.

5 A category of bistructures

Morphisms between bistructures will correspond to configurations of a linear function space.

Assuming

E_{i} = (E_{i}, ≤_{i}^{L}, ≤_{i}^{R}, ⌣_{i}), i = 0, 1,

are bistructures, define

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 stable bistructures by taking morphisms E_{0} to E_{1} to be extensional configurations of E_{0} ⊸ E_{1}, composed as relations. Of course, we should show that this composition is well-defined and has identities.

Lemma 4 Let α be an extensional configuration of E_{0} ⊸ E_{1} and β an extensional configuration of E_{1} ⊸ E_{2}. Then their relational composition β ∘ α is an extensional configuration of E_{0} ⊸ E_{2}. Furthermore

M(β ∘ α) = M(β) ∘ M(α).

A bistructure of the form E ⊸ E has the relation

Id_{E} = {(e, e′) | e′ ≤ e}

as an extensional configuration. It is an identity for composition. Furthermore M(Id_{E}) is the identity relation on events of E.

Proof: This proof is trickier than might be thought. One proof relies on Lemma 5 of [15] which shows that relational composition of stable configurations yields a stable configuration. An argument very similar to the proof of Lemma 5, yields

⌈β ∘ α⌉ = ⌈β⌉ ∘ ⌈α⌉

for stable configurations—here it is helpful to observe that for stable configurations x,

⌈x⌉ = {e′ | ∃e ∈ x. e′ ≤^{L} e}.

It follows that the composition of extensional configurations α, β is welldefined, being

β ∘ α = ⌈M(β)⌉ ∘ ⌈M(α)⌉ = ⌈M(β) ∘ M(α)⌉

where M(β) ∘ M(α) is a stable configuration by Lemma 5. Applying M, we obtain M(β ∘ α) = M(β) ∘ M(α). □

Morphisms on bistructures determine (special) extensional, linear (= stable and additive) functions on bidomains:

Proposition 5 Let F ∈ Γ(E_{0} ⊸ E_{1}) and x ∈ Γ(E_{0}). Defining

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

yields a configuration of E_{1}. The function ΓF : Γ(E_{0}) → Γ(E_{1}) is linear with respect to ⊑^{R} and continuous with respect to ⊑. The operation Γ is a faithful functor from the category of bistructures to bidomains.

5.1 Categorical constructions

Throughout this section assume E_{i} = (E_{i}, ≤_{i}^{L}, ≤_{i}^{R}, #_{i}) are bistructures, for i = 0, 1.

Define their tensor E_{0} ⊗ E_{1} to be (E_{0} × E_{1}, ≤^{L}, ≤^{R}, ⌣) where

(e_{0}, e_{1}) ≤^{L} (e′_{0}, e′_{1}) ⇔ e_{0} ≤_{0}^{L} e′_{0} & e_{1} ≤_{1}^{L} e′_{1}
(e_{0}, e_{1}) ≤^{R} (e′_{0}, e′_{1}) ⇔ e_{0} ≤_{0}^{R} e′_{0} & e_{1} ≤_{1}^{R} e′_{1}
(e_{0}, e_{1}) ⌣ (e′_{0}, e′_{1}) ⇔ e_{0} ⌣_{0} e′_{0} or e_{1} ⌣_{1} e′_{1}.

This construction extends to a functor; for α_{0} : E_{0} → E′_{0} and α_{1} : E_{1} → E′_{1}, define define α_{0} ⊗ α_{1} : E_{0} ⊗ E_{1} → E′_{0} ⊗ E′_{1} by

((e_{0}, e_{1}), (e′_{0}, e′_{1})) ∈ α_{0} ⊗ α_{1} ⇔ (e_{0}, e′_{0}) ∈ α_{0} & (e_{1}, e′_{1}) ∈ α_{1}.

This operation is easily checked to be well-defined and because morphisms compose as relations the functor laws follow directly.

The unit of tensor, 1, has a single event on which ≤^{L} and ≤^{R} are the identity, and the conflict relation is empty:

1 = ({•}, 1, 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_{2}.

The product in the category bistructures 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} iff they are injections of conflicting events in one or the other component.

The coproduct is given by

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

again obtained as the juxtaposition of the two bistructures, made disjoint, but this time extending conflict across the two components, so

⌣=⌣_{0} ∪ ⌣_{1} ∪(E_{0} × E_{1}) ∪ (E_{1} × E_{0}).

In fact, bistructures form a model of classical linear logic [15]. Define linear negation, the involution of linear logic, by

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

where E = (E, ≤^{L}, ≤^{R}, ⌣). Clearly (E^{⊥})^{⊥} = E.

To get the exponential !E, of a bistructure E, we use the orderings ≤^{L}, ≤^{R} on configurations introduced in Section 4. Define

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

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

Lemma 6 !E is a bistructure. The operation ! extends to a functor: for α : E → E′ , define !α :!E →!E′ by taking

!α = {(x, y) ∈ Γ(E)^{0} × Γ(E′)^{0} | y ⊆ αx}.

A configuration y of a bistructure !E_{0} ⊸ E_{1} may be applied to a configuration x of E_{0}:

y · x = {e | ∃x_{0} ⊆ x. (x_{0}, e) ∈ y}

This operation of application yields a configuration of E_{1}. It shows how the configuration y determines a function x ↦ y · x. In fact, !E_{0} ⊸ E_{1} has configurations in 1-1 correspondence with elements in the function space

[(Γ(E_{0}), ⊑^{R}, ⊑) → (Γ(E_{1}), ⊑^{R}, ⊑)]

in the cartesian-closed category of Berry’s bidomains:

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

ŷ(x) = {e | ∃x_{0} ⊆ x. (x_{0}, e) ∈ y}.

Then ŷ is a function Γ(E_{0}) → Γ(E_{1}) which is continuous with respect to ⊑ and stable with respect to ⊑^{R}. In fact, y ↦ ŷ is a 1-1 correspondence between configurations of !E_{0} ⊸ E_{1} and such functions.

More completely:

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

In particular, ! is a comonad. Its counit ϵ_{E} :!E → E is given by

(x, e) ∈ ϵ_{E} ⇔ e ∈ x,

where x is an event of !E and e an event of E. Its comultiplication: μ_{E} :!E →!!E is given by

(x, X) ∈ μ_{E} ⇔ ⋃X ⊆ x,

where x is an event of !E and X an event of !!E. There is also a natural isomorphism

α_{E_{0},E_{1}} :!E_{0}⊗!E_{1} ≅!(E_{0} × E_{1})

where

((x_{0}, x_{1}), y) ∈ α_{E_{0},E_{1}} ⇔ y ⊆ x_{0} ∪ x_{1}

for events (x_{0}, x_{1}) of !E_{0}⊗!E_{1} and y of !(E_{0} × E_{1})—we assume that the events of E_{0} and E_{1} are disjoint.

6 PCF in bidomains

Linear types can be interpreted as bistructures straightforwardly: The event structures of Section 3, interpreting the types o and ι of booleans and integers, correspond to special bistructures, with degenerate ≤^{L} relations; linear types σ ⊸ σ′ and !σ are interpreted by the associated constructions on bistructures. For M a term of type σ, and any environment ρ , we can define, by structural induction, the denotation of M in an environment ρ lies in the cpo of extensional configurations of the bistructure for the type of M. Application between an extensional configuration y of type σ → σ′ and an extensional configuration of type σ is as defined in Section 5.1. The semantic definition holds no surprises; in particular, the clauses for applications and λ-abstractions follow that earlier for event-structure semantics in Section 3.

But, as Jim and Meyer point out in [10] there is a problem with the bidomain, and so bistructure model of PCF. The theory it induces on PCF is not even comparable with that of the Scott model. Despite cuting down to stable functions we are no closer to the fully abstract model for PCF, and, as argued in [10], it is hard to extend PCF to make the bidomain (and bistructure) model fully abstract. The two PCF terms

lor ≡ λxλy(⊃_{o}x tt(⊃_{o}y tt ff)) and
ror ≡ λxλy(⊃_{o}y tt(⊃_{o}x tt ff))

for disjunction, one first evaluating its left argument and the other first its right argument are denoted by the configurations lor and ror respectively in the bistructure model. The restriction to stable functions excludes the parallel-or function so in bistructures lor and ror have no upper bound with respect to either the stable or extensional order. For this reason the bistructure model has a configuration representing an ortester, a function returning tt on lor and ff on ror. The following term will denote an ortester-tester

F ≡ λh ⊃_{o}(h lor)(⊃_{o}(h ror)Ω_{o}tt)Ω_{o}

—it yields tt precisely when h is an ortester, and otherwise gives ⊥, the denotation of Ω_{o} ≡ Y_{o}(λv^{o}v). According to the bistructure model where an ortester is represented, F, with type σ, will not receive the same denotation as Ω_{σ} ≡ Y_{σ}(λv^{σ}v). However, according to the Scott model F and Ω_{σ} will be identified, i.e. C[[F]] = C[[Ω_{σ}]]. This is because there cannot be an ortester in the Scott model; by monotonicity, it would have to send parallel-or to a truth value bigger than both tt and ff, which is absurd.

It follows that the PCF theory in bistructures does not include the PCF theory in the Scott model; according to the Scott semantics the ortester-tester F is equivalent to Ω_{σ}, which not so in the bistructure semantics. In fact, the theories in the Scott and bistructure semantics are incomparable. In the paper [14], Plotkin exhibits two terms which are operationally equivalent but whose denotations act differently on parallelor. According to the bistructure semantics the two terms are equivalent (bistructures rule out parallel-or, the only continuous function on which the two terms differ), but they are not equivalent according to the Scott semantics.

7 Extending bistructures

The incomparability in two PCF theories arises because, in limiting attention to stable conflict ⌣, we have lost track of the conflict # in event-structures. In the event-structure model, the events lor and ror corresponding to the functions lor and ror are not in conflict which ensures that the two events (lor, t) and (ror, f) are in conflict in the function space. So in the event-structure model undesirable functions like ortesters are not represented. One way to correct this problem with bistructures, and bidomains, is to reinstate # as extra structure on bistructures, marrying together the constructions of Sections 3 and 5.

An extended bistructure is a structure E = (E, ≤^{L}, ≤^{R}, ⌣, #) where

• (E, ≤^{L}, ≤^{R}, ⌣) is a stable bistructure, and

• extensional conflict # is a binary, irreflexive, symmetric relation on

E satisfying

e#e′ ≤ e′′ ⇒ e#e′′.

A configuration is an extensional configuration x of the bistructure which also satisfies

∀e_{1}, e_{2} ∈ x. ¬e_{1}#e_{2}.

We write Γ(E) for the set of configurations.

We can now imitate Section 5, to obtain a new model of PCF. As the linear function space of extended bistructures E_{i} = (E_{i}, ≤_{i}^{L}, ≤_{i}^{R}, ⌣_{i}, #_{i}) for i = 0, 1,, we take

E_{0} ⊸ E_{1} = (E, ≤^{L}, ≤^{R}, ⌣, #)

where (E, ≤^{L}, ≤^{R}, ⌣) is the linear function space of bistructures, and

(e_{0}, e_{1})#(e′_{0}, e′_{1}) ⇔ ¬e_{0}#_{0}e′_{0} & e_{1}#_{1}e′_{1}.

As before, morphisms are configurations of the function space which compose as relations.

The category is monoidal-closed with respect to a tensor of two extended bistructures, given as in Sections 3 and 5. Precisely, two extended bistructures E_{i} = (E_{i}, ≤_{i}^{L}, ≤_{i}^{R}, ⌣_{i}, #_{i}) for i = 0, 1, have tensor

E_{0} ⊗ E_{1} = (E, ≤^{L}, ≤^{R}, ⌣, #)

where (E, ≤^{L}, ≤^{R}, ⌣) is the tensor of the bistructures and

(e_{0}, e_{1})#(e′_{0}, e′_{1}) ⇔ e_{0}#_{0}e′_{0} or e_{1}#_{1}e′_{1}.

Tensor extends to a functor just as in Section 5.

Products are obtained by disjoint juxtaposition, and coproducts similarly, but extending the two conflict relations across the event structures.

As the exponential of an extended bistructure E = (E, ≤^{L}, ≤^{R}, ⌣, #), we take

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

where

x#_{!}y ⇔ ∃e_{1} ∈ x, e_{2} ∈ y. e_{1}#e_{2}.

It extends to a functor as in Section 5. The same definitions of counit and comultiplication suffice to form a comonad and still have natural isomorphism α as defined there. The natural isomorphism α, where

α_{E_{0},E_{1}} :!E_{0}⊗!E_{1} ≅!(E_{0} × E_{1}),

together with monoidal-closure ensures that the coKleisli category of ! is cartesian-closed. We obtain a model of intuitionistic linear logic.

Linear types σ can be interpreted as extended bistructures B_{σ}. The extended bistructure B_{o}, representing the booleans, has the two events t, f, corresponding to tt, ff, related by both conflict relations and with the identity relation as ≤^{L}, ≤^{R}. Similarly, B_{ι} is the event structure representing the flat domain of integers; it has events ω, the natural numbers, pairwise in conflict according to both conflict relations, with the identity relation for ≤^{L} and ≤^{R}. A type σ ⊸ σ′ denotes the extended bistructure B_{σ} ⊸ B_{σ′}, while !σ denotes the extended bistructure !B_{σ}.

We obtain a standard model for PCF by interpreting a PCF type σ as the cpo of configurations Γ(B_{σ}), ordered by inclusion. Application between a configuration y of type σ → σ′ and a configuration of type σ is again given by

y · x = {e | ∃x_{0} ⊆ x. (x_{0}, e) ∈ y}.

For M a term of type σ, and any environment ρ, we define, by structural induction, B[[M]]ρ to be an element of Γ(B_{σ}). For example,

\begin{matrix}B[[MN]]ρ = & \{e | ∃d ⊆ B[[N]]ρ & (d, e) ∈ B[[M]]ρ\} \\ B[[λvM]]ρ = & \{(d, e) | e ∈ B[[M]]ρ[d/v]\}. \end{matrix}

Now it can be checked that the configurations lor and ror denoting the PCF terms lor and ror are not in extensional conflict in B_{!(o,o;o)}, so that an ortester taking lor to tt and ror to ff can not be represented by any configuration of the extended bistructure model.

It’s reassuring that we have avoided ortesters in the extended-bistructure model. But of course we want that the PCF theory of the Scott model is included in that of the extended-bistructure model. The argument that this is so goes via an embedding between the interpretations the two models give to types. Here it is useful to refer to the representation of the Scott model by event structures given in Section 3.

Definition: By structural induction on linear types σ, define functions θ_{σ} from the events of B_{σ} to the events of C_{σ} as follows:

• θ_{o}, θ_{ι} are the identity functions on events.

• θ_{!σ}(x) = ⌈θ_{σ}x⌉, for events x of B_{!σ}.

• θ_{σ_{0}⊸σ_{1}}((e_{0}, e_{1})) = (θ_{σ_{0}}(e_{0}), θ_{σ_{0}}(e_{1})), for events (e_{0}, e_{1}) of B_{σ_{0}⊸σ_{1}}.

Proposition 9 For any linear type σ, the function θ_{σ} is injective from the events of B_{σ} to the events of C_{σ} and such that

e ≤ e′ in B_{σ} ⇔ θ_{σ}(e) ≤ θ_{σ}(e′) in C_{σ}
e # e′ in B_{σ} ⇔ θ_{σ}(e) # θ_{σ}(e′) in C_{σ}

where e, e′ are events of B_{σ}.

Proof: By structural induction on σ. □

Notation: We call environments in the event-structure semantics of Section 3 C-environments, while those in the extended-bistructure semantics will be B-environments. For ρ a B-environment, we write θ ∘ ρ for the environment sending variable x^{σ} to ⌈θ_{σ}ρ(x)⌉—we’ll drop the types on θ whenever we can get away with it.

Lemma 10 For M a PCF term of type σ, ρ a B-environment,

e ∈ B[[M]]ρ ⇔ θ(e) ∈ C[[M]]θ ∘ ρ.

Proof: We use a result of Berry: In any least fixed point semantics of PCF, which B[[−]] and C[[−]] are, the denotation of any term is the least upper bound of the denotations of its Böhm tree approximations (see [4], Theorem 4.3.1). A Böhm tree is a well-typed term of PCF of the form

• Ω_{σ} ≡ Y_{σ}(λv^{σ}v^{σ}), or

• λv_{1} ⋯ v_{n} uBT_{1} ⋯ BT_{m}, where u is a variable or PCF constant and BT_{1}, ⋯, BT_{m} are themselves Böhm trees.

By Berry’s result it is sufficient to verify the statement of the lemma for terms M which are Böhm trees. This we do by structural induction on Böhm trees. Consider the cases according to the form of the Böhm tree. Case Ω: If the Böhm tree is Ω, then both B[[Ω]] and C[[Ω]]θ ∘ ρ are the empty set. Case v, a variable: This case follows directly from the semantics of variables. Case f\overrightarrow{BT}, where f is a PCF constant: At ground and first-order types σ the events is both models coincide and θ_{σ} is the identity on events. PCF constants f (remember these do not include the fixed-point operators Y_{σ}) receive the same set of events as denotations in the two models, and hence B[[f]]ρ = C[[f]]θ ∘ ρ, for an arbitrary B-environment ρ. Now, consider a term f\overrightarrow{BT}, for f a PCF constant, where, by induction, for any argument BT, we have for a B-environment ρ, that

d ⊆ B[[BT]]ρ ⇔ θd ⊆ C[[BT]]θ ∘ ρ.

Here BT must have type ι or o where θ is the identity. Thus

d ⊆ B[[BT]]ρ ⇔ d ⊆ C[[BT]]θ ∘ ρ

Now, using self-evident vector notation, we see that for any B-environment ρ,

e ∈ B[[f\overrightarrow{BT}]]ρ ⇔ ∃\overrightarrow{d ⊆ B[[BT]]ρ}. (\overrightarrow{d}, e) ∈ B[[f]]ρ
⇔ ∃\overrightarrow{d ⊆ C[[BT]]θ ∘ ρ}. (\overrightarrow{d}, e) ∈ C[[f]]θ ∘ ρ
⇔ e ∈ C[[f\overrightarrow{BT}]]θ ∘ ρ i.e. θ(e) ∈ C[[f\overrightarrow{BT}]]θ ∘ ρ.

Case v\overrightarrow{BT}, where v is a variable: We consider just vBT —the argument is essentially the same for v\overrightarrow{BT}. We require

e ∈ B[[v BT]]ρ ⇔ θ(e) ∈ C[[v BT]]θ ∘ ρ.

“⇒” Suppose e ∈ B[[v BT]]ρ. Then for some d ∈ Γ(B_{σ})^{0}, with σ the type of BT,

d ⊆ B[[BT]]ρ & (d, e) ∈ ρ(v).

Thus (θ(d), θ(e)) ∈ θ ∘ ρ(v). By induction, θd ⊆ C[[BT]]θ ∘ ρ so θ(d) ⊆ C[[BT]]θ∘ρ. But now, from the definition of the semantics of C[[v BT]]θ∘ρ, we obtain θ(e) ∈ C[[v BT]]θ ∘ ρ.

“⇐” Suppose θ(e) ∈ C[[v BT]]θ ∘ ρ. Then for some d ∈ Γ(C_{σ})^{0}, with σ the type of BT,

d ⊆ C[[BT]]θ ∘ ρ & (d, θ(e)) ∈ θ(ρ(v)).

Now, (d, θ(e)) ∈ θ(ρ(v)) = ⌈θρ(v)⌉ implies there is (d_{0}, e_{0}) ∈ ρ(v) with

θ(d_{0}) ⊆ d & θ(e) ≤ θ(e_{0}).

Hence θd_{0} ⊆ C[[BT]]θ ∘ ρ. By induction, d_{0} ⊆ B[[BT]]ρ. Thus e_{0} ∈ B[[v BT]]ρ, and because e ≤ e_{0} (by Proposition 9), e ∈ B[[v BT]]ρ, as required. Case λ\overrightarrow{v} u\overrightarrow{BT}, where u is a PCF constant or variable. The cases where \overrightarrow{v} is an empty list have already been covered above. From the semantics, for a B-environment ρ,

(\overrightarrow{d}, e) ∈ B[[λ\overrightarrow{v}u\overrightarrow{BT}]]ρ ⇔ e ∈ B[[u\overrightarrow{BT}]]ρ[\overrightarrow{d/z}]
⇔ θ(e) ∈ C[[u\overrightarrow{BT}]]θ ∘ (ρ[\overrightarrow{s/z}])
— this case of the induction hypothesis

has already been covered,

⇔ θ(e) ∈ C[[u\overrightarrow{BT}]](θ ∘ ρ)[\overrightarrow{θ(d)/z}]
⇔ (\overrightarrow{θ(d)}, θ(e)) ∈ C[[λ\overrightarrow{v}u\overrightarrow{BT}]]θ ∘ ρ
⇔ θ((\overrightarrow{d}, e)) ∈ C[[λ\overrightarrow{v}u\overrightarrow{BT}]]θ ∘ ρ.
□

As a corollary we can relate the theories of the two models, the eventstucture model (representing the Scott model) and the bistructure model. For PCF terms M, N of the same type, we have the following preorders induced by the semantics:

M ⊑_{B} N ⇔ B[[M]]ρ ⊑ B[[N]]ρ for all B-environments ρ, and
M ⊑_{C} N ⇔ C[[M]]ρ ⊑ C[[N]]ρ for all C-environments ρ.

Theorem 11 For PCF terms M, N of the same type:

M ⊑_{C} N ⇒ M ⊑_{B} N

Proof: Assume M ⊑_{C} N. For ρ a B-environment, argue:

e ∈ B[[M]]ρ ⇒ θ(e) ∈ C[[M]]θ ∘ ρ by Lemma 10
⇒ θ(e) ∈ C[[N]]θ ∘ ρ as M ⊑_{C} N,
⇒ e ∈ B[[N]]ρ by Lemma 10.

Thus B[[M]]ρ ⊆ B[[N]]ρ for an arbitrary B-environment ρ, i.e. M ⊑_{B} N.□

8 Concluding remarks

Can the syntax of PCF be extended to make the extended-bistructures model fully abstract? More significantly, can bistructures help construct extensional fully abstract models for pure PCF? Gordon Plotkin and I have had some preliminary success adapting ideas like those here to a sequential, rather than just a stable model, by replacing the conflict relations of extended bistructures by Ehrhard’s hypercoherences (in a stable and extensional form)—presently, it seems we can eliminate all but the third of Curien’s examples in Proposition 4.4.2 [7].

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] Berry, G.,and Curien, P-L., Sequential algorithms on concrete data structures. Theoretical Computer Science 20, pp.265-321, 1982.

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

[5] Bucciarelli, A., Sequential models of PCF: some contributions to the domain-theoretic approach to full abstraction. PhD thesis in Computer Science, University of Pisa, March 1993.

[6] Ehrhard, T., Hypercoherences: a strongly stable model of linear logic. Mathematical Structures in Computer Science, 1993.

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

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

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

[10] Jim, T., and Meyer, A., Full abstraction and the context lemma. Invited lecture, proceedings of Theoretical Aspects of Computer Software, Sendai, Springer Lecture Notes in Computer Science 526, 1991.

[11] Hoofman, R., Nonstable models of linear logic. PhD thesis, University of Utrecht, 1992.

[12] Milner, A.R.G., Fully abstract models of typed lambda-calculi. Theoretical Computer Science 4(1), pp. 1-23, 1977.

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

[14] Plotkin, G.D., LCF considered as a programming language. Theoretical Computer Science 5(3), pp.223-256, 1977.

[15] Plotkin, G.D., and Winskel, G., Bistructures, bidomains and linear logic. To appear in the proceedings of ICALP 94, Springer Lecture Notes in Computer Science, 1994.

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

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

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

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

Recent Publications in the BRICS Report Series

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.

RS-94-12 Glynn Winskel and Mogens Nielsen. Models for Concurrency. May 1994, 144 pp. To appear as a chapter for the Handbook of Logic and the Foundations of Computer Science, Oxford University Press.

RS-94-13 Glynn Winskel. Stable Bistructure Models of PCF. May 1994, 26 pp. Preliminary draft. Invited lecture for MFCS 94. To appear in the LNCS proceedings of MFCS 94.