BRICS RS-96-44 G. Winskel: A Presheaf Semantics of Value-Passing Processes

BRICS

Basic Research in Computer Science

A Presheaf Semantics of Value-Passing Processes

Glynn Winskel

BRICS Report Series RS-96-44 ISSN 0909-0878 November 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, 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@brics.dk

BRICS publications are in general accessible through World Wide Web and anonymous FTP:

http://www.brics.dk/
ftp://ftp.brics.dk/pub/BRICS

This document in subdirectory RS/96/44/ A presheaf semantics of value-passing processes

Glynn Winskel

BRICS* – Computer Science Dept., University of Aarhus

Abstract

This paper investigates presheaf models for process calculi with value passing. Denotational semantics in presheaf models are shown to correspond to operational semantics in that bisimulation obtained from open maps is proved to coincide with bisimulation as defined traditionally from the operational semantics. Both “early” and “late” semantics are considered, though the more interesting “late” semantics is emphasised. A presheaf model and denotational semantics is proposed for a language allowing process passing, though there remains the problem of relating the notion of bisimulation obtained from open maps to a more traditional definition from the operational semantics. A tentative beginning is made of a “domain theory” supporting presheaf models.

Introduction

The papers [12, 4] explore presheaf models for concurrency. Here begins an investigation of the use of presheaves to model higher-order features, most dramatic in the situation of process calculi where processes can be communicated as values.

Something of higher-order appears even in value-passing process calculi where values lie in some discrete datatype like integers or booleans. As is customary, for value-passing calculi, we draw a distinction between “early” and “late” semantics. Early semantics coincides with that presented in [14] where a value-passing calculus is reduced to a value-free one by immediately instantiating the variable in an input action to its possible values, the resulting processes being set together in a nondeterministic sum. According to late semantics input actions contain bound variables which only become instantiated when a communication is made. Generally (see e.g. [15, 6, 16]), a late semantics for value passing represents the result of input communication as an abstraction, denoting a function from values to processes. Whereas the usual models for concurrency, transition systems, labelled Petri nets and event structures and the like, accommodate early semantics for value-passing directly, following [14, 7, 8], the late semantics seems accomplished most smoothly in domain-theoretic settings, which readily support abstractions.

* Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

Two ways seem open to extending models for concurrency to higher-order features. One is to take existing models, most of these transitions systems in one disguise or another, and essentially decorate them with extra structure. Another is to develop a new class of models, some of which can be seen to correspond to existing models, and which at the same time are rich enough to support constructions of the kind we are used to seeing in domain theory. This paper follows the latter course in investigating presheaf models.

Presheaf models for concurrency have the advantage of including interleaving models like synchronisation trees and independence models like labelled event structures, as well as contributing a general definition of bisimulation based on open maps. As we will see, they also extend to higher-order, though presently many questions remain, chief among them being the problem of simultaneously combining higher-order features with independence of the kind seen in event structures and Petri nets. A more specific problem is that of obtaining a characterisation in terms of the operational semantics of the bisimulation obtained from open maps for a process-passing calculus. On the positive side, the usual definition of “late bisimulation” and “early bisimulation” for ordinary value-passing is reconciled with the definition of bisimulation obtained on presheaves via open maps.

1 The language VProc

VProc is a process language for passing values along channels, inspired by CCS. Its syntax:

t ::= nil | τ.t | a!e.t | a?x.t | t_{1} | t_{2} | t_{1} + t_{2} | [e_{1} = e_{2}]t | X | recX.t

where x ranges over value-variables V ar, X over process-variables P var, a over channel names C, and e, e_{1}, e_{2} over value-expressions. We will not go into the details of the form of value-expressions beyond remarking that they may contain free value-variables and when evaluated yield values in a set V.

For simplicity we assume that recursive definitions of processes recX.t are guarded in the sense that all free occurrences of X in t lie under, though not necessarily immediately under, a prefix τ.-, a!e.- or a?x.-.

1.1 Late transition semantics for VProc

We specify the transitions a closed term can perform. A transition t →^{α} t′, where t is a closed term, is understood to mean that the process t can perform action α to become t′; actions α range over τ-actions τ, output actions a!v, where a ∈ C and v ∈ V, and input actions a?x, where a ∈ C and x ∈ V ar. τ rule: τ.t ^{\underline{τ}}→ t Output rule: a!e.t ^{\underline{a!v}}→ t where e, necessarily closed, evaluates to value v. Input rule: a?x.t ^{\underline{a?y}}→ t[y/x] where y ∈ V ar is assumed not captured by its substitution for x in t. Parallel rules:

\frac{t_{1} ^{\underline{α}}→ t′_{1}}{t_{1}|t_{2} ^{\underline{α}}→ t′_{1}|t_{2}}  \frac{t_{2} ^{\underline{α}}→ t′_{2}}{t_{1}|t_{2} ^{\underline{α}}→ t_{1}|t′_{2}}

In the first parallel rule t_{2} must have no free variables in common with action α; a symmetric condition is enforced for the second parallel rule.

\frac{t_{1} ^{\underline{a!v}}→ t′_{1} t_{2} ^{\underline{a?y}}→ t′_{2}}{t_{1}|t_{2} ^{\underline{τ}}→ t′_{1}|t′_{2}[v/y]}  \frac{t_{1} ^{\underline{a?y}}→ t′_{1} t_{2} ^{\underline{a!v}}→ t′_{2}}{t_{1}|t_{2} ^{\underline{τ}}→ t′_{1}[v/y]|t′_{2}}

Sum rules:

\frac{t_{1} ^{\underline{α}}→ t′_{1}}{t_{1} + t_{2} ^{\underline{α}}→ t′_{1}}  \frac{t_{2} ^{\underline{α}}→ t′_{2}}{t_{1} + t_{2} ^{\underline{α}}→ t′_{2}}

Condition rule:

\frac{t ^{\underline{α}}→ t′}{[e_{1} = e_{2}]t ^{\underline{α}}→ t′}

provided e_{1} and e_{2} evaluate to the same value. Recursion rule:

\frac{t[recX.t/X] ^{\underline{α}}→ t′}{recX.t ^{\underline{α}}→ t′}

1.2 Late bisimulation

Definition: A late bisimulation is a binary relation R between closed process terms such that whenever t_{1}Rt_{2}

(i) t_{1} →^{τ} t′_{1} ⇒ ∃t′_{2}. t_{2} →^{τ} t′_{2} & t′_{1} R t′_{2} and t_{2} →^{τ} t′_{2} ⇒ ∃t′_{1}. t_{1} →^{τ} t′_{1} & t′_{1} R t′_{2}

(ii) t_{1} →^{a!v} t′_{1} ⇒ ∃t′_{2}. t_{2} →^{a!v} t′_{2} & t′_{1} R t′_{2} and t_{2} →^{a!v} t′_{2} ⇒ ∃t′_{1}. t_{1} →^{a!v} t′_{1} & t′_{1} R t′_{2}

(iii) t_{1} →^{a?y} t′_{1} ⇒ ∃t′_{2}, z. t_{2} →^{a?z} t′_{2} & ∀v ∈ V. t′_{1}[v/y] R t′_{2}[v/z] and

t_{2} →^{a?y} t′_{2} ⇒ ∃t′_{1}, z. t_{1} →^{a?z} t′_{1} & ∀v ∈ V. t′_{1}[v/y] R t′_{2}[v/z].

Say closed process terms t_{1}, t_{2} are late bisimilar iff there is a late bisimulation R such that t_{1}Rt_{2}.

2 Open maps and bisimulation on presheaves

Let P be a small category. It is to be thought of as a category of path objects (or path shapes) in which morphisms stand for an extension of one path by another. Let P̂ = [P^{op}, Set], the category of presheaves over P. Recall, a morphism h : X → Y, between presheaves X, Y, is open iff for all morphisms m : P → Q in P, the square

[figure: \begin{matrix}X(P) & X(Q) \\ Y (P) & Y (Q) \end{matrix}; h_{P}; Xm; h_{Q}; Y m]

is a quasi-pullback, i.e. whenever p ∈ X(P) and q ∈ Y (Q) satisfy h_{P} (p) = (Y m)(q), then there exists p′ ∈ X(Q) such that (Xm)(p′) = p and h_{Q}(p′) = q. (This definition of open map, translates via the Yoneda Lemma to an equivalent path-lifting property of h—see [12].)

Say presheaves X, Y are bisimilar iff there is a span of surjective open maps between them, equivalently, iff there is R ↪ X × Y such that the compositions with the projections R ↪ X × Y →^{π_{1}} X and R ↪ X × Y →^{π_{2}} Y are surjective open.

In [12, 4] we defined bisimulation between rooted presheaves, presheaves X, over a category assumed to have an initial object I, for which X(I) is a singleton. For rooted presheaves bisimulation is defined merely through the presence of a open maps (not requiring surjectivity). This is because open maps between rooted presheaves are necessarily surjective.

We can cast further light on rooted presheaves with the help of a “lifting” construction which will be important later, as is to be expected from traditional domain theory. For P, a small category, define its lifting P_{⊥} to consist of P with a new initial object (called ⊥) adjoined freely. Given X ∈ P̂, define lift(X) ∈ P̂_{⊥} to be the rooted presheaf which acts as X on copies of P ∈ P and yields a singleton, {∗} say, on ⊥. The lift operation extends in the obvious way to a functor which gives an equivalence between P̂ and the subcategory of rooted presheaves over P_{⊥}; on maps h in P̂, lift(h) is open iff h is surjective open. These remarks are useful in another context, that of algebraic set theory—see [10], p. 72.

3 A domain-theoretic setting

In proposing categories of presheaves as our “domains” of processes we are leaving domain theory as traditionally understood; processes are denoted by presheaves, objects in a category rather than elements of a partial order. This is not new; several proposals have been made for generalisation of powerdomains that leave the category of partial orders, for instance [13, 1, 18], and presheaves, being a way to introduce nondeterministic branching to computation paths, have much in common with powerdomains.

We sketch a setting, generalising traditional domain theory, in which we can place the work on presheaf models. The category analogue of algebraic cpo’s is finitely accessible categories [2] in which the role of the basis of finite/isolated/compact elements is replaced by that of a small subcategory of finitely presentable objects; every object of a finitely accessible category is a directed colimit of finitely presentable objects. This is analogous to the fact that an algebraic cpo is the ideal completion of its finite elements. Morphisms between finitely accessible categories are functors preserving directed colimits, the analogue of continuous functions.

A way to introduce nondeterminism to a finitely accessible category C is via a construction on the “basis” of finitely presentable objects C^{0}: Freely close C^{0} under all finite colimits to get a new basis (in which nondeterministic branching has been introduced). The finitely accessible category with this new category as basis, got by closing under directed colimits, can be thought of as the nondeterministic computations of C. This “ideal completion” is equivalent to the category of presheaves over C^{0} (by results of [9], ch.VI). So taking presheaves combines two operations, adding branching to a basis (the part that takes us outside partial orders), and then completing to a finitely accessible category. Viewed in this way, taking presheaves over the basis of a finitely accessible category yields a “monad” on finitely accessible categories, reminiscent of powerdomain monads.^{1}

The Kleisli category of the monad associated with taking presheaves is Prof, the bicategory of profunctors (see e.g. [3] where they are called distributors). Profunctors and their categorical constructions provide a convenient setting in which to provide semantics to process calculi with value and process passing. The bicategory Prof has small categories as objects and as morphisms F : P ∣ →Q, where P and Q are small categories, we take functors F : P → Q̂. Composition in Prof, say of F : P ∣ →Q and G : Q ∣ →R, is given to within isomorphism by G^{†} ∘ F : P ∣ →R—here G^{†} is the left Kan extension Lan_{y_{Q}}G of G with respect to the Yoneda embedding y_{Q} : Q → Q̂. Left Kan extensions and so composition are only determined up to isomorphism; thus the fact that Prof is really a bicategory, and not a category. Note that profunctors, or more properly their left Kan extensions, preserve (surjective) open maps and so bisimulation by [4] Lemma 3—the extra preservation of surjectivity is easy to show. Cat the category of small categories embeds in Prof: A functor F : P → Q is sent to the composition y_{Q} ∘ F with the Yoneda embedding y_{Q} : Q → Q̂. The embedding Cat → Prof preserves small colimits.

Prof forms a model of classical linear logic. To see its monoidal closed structure, for small categories P, Q, define

P ⊸ Q = P^{op} × Q and P ⊗ Q = P × Q ,

where product × on the right is the usual product of categories, and observe the natural bijection:

Prof(P, [Q ⊸ R]) ≅ Prof(P ⊗ Q, R)

The unit of ⊗ is 1, the category with a single object and morphism. Prof has products and coproducts which coincide on objects, where both are given by coproduct in Cat. As a model of classical linear logic there is the same kind of degenerary familiar from the category of relations; par (℘) coincides with tensor (⊗), and ⊥ with 1 (so Prof is compact-closed). Linear involution P^{⊥} is isomorphic to P ⊸ 1 and so to P^{op}.

1In this motivational section, we won’t be distracted by the constructions more properly taking place in a 2-category/bicategory—thus the quotes around “monad”.

Morphisms 1 ∣ →(P ⊸ Q) correspond to presheaves over P^{op} × Q and so to profunctors P ∣ →Q. They correspond to colimit-preserving functors from P̂ to Q̂.

When we attend to presheaf semantics we are involved with various sorts of functors. Certainly we quickly encounter functors from P to Q̂ corresponding, to within isomorphism, to colimit-preserving functors from P̂ to Q̂, between presheaves. We also meet more general “continuous” functors P̂ → Q̂, for example to cope with processes which can receive processes as values. As usual in linear logic we can recover these with the help of an exponential (!). Define !P, to be a completion of P under finite colimits; more precisely we can take !P to be a skeletal subcategory of the subcategory of P̂ consisting of finitely presentable objects. Then profunctors !P ∣ →Q correspond, to within isomorphism, to functors P̂ → Q̂ which are continuous in the sense that they preserve directed colimits.

Prof provides us with a rich repertoire of constructions on categories of presheaves. We pause to ask how the constructions are reflected in notions of open maps and bisimulation.

It is clear when a map is (surjective) open in a coproduct P + Q in Prof: h : X → Y is (surjective) open in { \atop P + Q} iff the two components h_{1} : X_{1} → Y_{1} and h_{2} : X_{2} → Y_{2} are (surjective) open in P̂ and Q̂ respectively. Because products in Prof are given by the same construction on objects, the same holds for products.

Let h : X → Y be a map in { \atop P ⊗ Q}. For P ∈ P, define h^{P} to be the natural transformation h^{P} : X(P, −) → Y (P, −) with component (h^{P})_{Q} = h_{P,Q} at Q ∈ Q. In a similar way, define h^{Q} : X(−, Q) → Y (−, Q) for any Q ∈ Q. Now, we can observe: h : X → Y is (surjective) open in { \atop P ⊗ Q} iff ∀P ∈ P. h^{P} is (surjective) open in Q̂ and ∀Q ∈ Q. h^{Q} is (surjective) open in P̂.

There is a similar characterisation of open maps in { \atop P ⊸ Q} because P ⊸ Q = P^{op} × Q. A map h : X → Y in { \atop P ⊸ Q} is (surjective) open iff ∀P ∈ P. h^{P} is (surjective) open in Q̂ and ∀Q ∈ Q. h^{Q} is (surjective) open in P̂^{op}.

Note openness and bisimilarity in { \atop P ⊸ Q} involves openness and bisimilarity in P̂^{op}! However, in the situation where P is a discrete category, h is open iff h^{P} is open for all P ∈ P.

This proposal of a domain theoretic framework in which to understand presheaf models cannot be definitive at present. We would, for instance, expect to work within some cartesian-closed subcategory of finitely accessible categories. But, more importantly, until the aim of bringing independence models within a domain-theoretic framework is carried out fully we should remain open-minded.

4 A late path category

We seek a path category P with respect to which closed process terms of VProc denote presheaves. Its objects should reflect that a compution path of a process may begin with a τ-action, an output action a!v or an input action a?, when it may either resume with a computation path, or, in the case where it has first performed an input action, input a value before resuming the computation path. This guides us to wishing to denote closed terms of VProc by presheaves over path category P, which is an initial solution to

P ≅ P_{⊥} + ∑_{(a,v)∈C×V} P_{⊥} + ∑_{a∈C}(V ⊸ P)_{⊥}

in Prof—here we treat the set V as a discrete category. The solution is easy to construct, firstly because it is sufficient to find an initial solution to

P ≅ P_{⊥} + ∑_{(a,v)∈C×V} P_{⊥} + ∑_{a∈C}(V^{op} × P)_{⊥}

in Cat (where V^{op} = V as V is discrete), and secondly because all the operations used preserve the property that the category is a partial order. This means an initial solution has the form of a partial order

P = P_{⊥} + ∑_{(a,v)∈C×V} P_{⊥} + ∑_{a∈c}(V^{op} × P)_{⊥}

whose path objects are given inductively by:

• τ. ∈ P, and τ.P ∈ P if P ∈ P, • a!v. ∈ P, and a!v.P ∈ P if P ∈ P,

• a? ∈ P, and a?(v ↦ P) ∈ P if P ∈ P,

where a ∈ C and v ∈ V, and whose morphisms (the partial order) are given inductively by the following clauses, where P, P′ ∈ P, a ∈ C and v ∈ V:

• P ≤ P,

• τ. ≤ τ.P, and τ.P ≤ τ.P′ if P ≤ P′,

• a!v. ≤ a!v.P, and a!v.P ≤ a!v.P′ if P ≤ P′,

• a? ≤ a?(v ↦ P), and a?(v ↦ P) ≤ a?(v ↦ P′) if P ≤ P′.

Notation: We use (P, Q) to name the unique morphism from P to Q in P when P ≤ Q.

We are using suggestive names for the objects of P to pick out to which component of a sum they belong:

• τ. is the least element of the leftmost summand of P, other elements of this component being of the form τ.P.

• a!v. is the least element of the output summand associated with outputting value v on channel a; other elements of this component have the form a!v.P.

• a? is the least element of the summand associated with a commitment to input on channel a; its other elements take the form a?(v ↦ P) and correspond to resuming a computation path after inputting value v.

We could have derived the above constructions on path objects systematically from operations associated with sums, lifting and product of categories.

5 Late presheaf semantics

We introduce operations on presheaves which capture the meaning of operations in VProc.

5.1 Prefixing

Let X ∈ P̂. We define τ.X ∈ P̂ by taking τ.X = In_{τ} ∘ lift(X). where In_{τ} : P̂_{⊥} → P̂ takes a presheaf over P_{⊥} to the corresponding presheaf over the left summand P_{⊥} in

P = P_{⊥} + ∑_{(a,v)∈C×V} P_{⊥} + ∑_{a∈C} (V^{op} × P)_{⊥} .  (†)

Recalling our notation for path objects it follows that for X ∈ P̂ and a path object Q ∈ P

τ.X(Q) = \{ \begin{matrix}X(P) & if Q = τ.P, \\ \{∗\} & if Q = τ., \\ ∅ & otherwise. \end{matrix}

Similarly, for X ∈ P̂, a ∈ C and v ∈ V, we define a!v.X ∈ P̂ so that on a path object Q ∈ P

a!v.X(Q) = \{ \begin{matrix}X(P) & if Q = a!v.P, \\ \{∗\} & if Q = a!v., \\ ∅ & otherwise. \end{matrix}

Let F : V → P̂ and a ∈ C. We define a?F ∈ P̂ as follows. First notice that F corresponds to a presheaf X over V^{op} × P, and now define a?F = In_{a?} ∘ lift(X) where In_{a?} : P̂_{⊥} → P̂ takes a presheaf over (V^{op} × P)_{⊥} to the corresponding presheaf over the a-summand in P (see (†) above). Now, for F : V → P̂, a ∈ C and a path object Q ∈ P we obtain

a?F (Q) = \{ \begin{matrix}(F v)(P) & if Q = a?(v ↦ P), \\ \{∗\} & if Q = a?, \\ ∅ & otherwise. \end{matrix}

Notation: If G(v) ∈ P̂, for any v ∈ V, we can as usual write λv.G(v) for the associated function V → P̂. We write a?v.G(v) for a?(λv.G(v)).

5.2 Sums

Coproducts of presheaves provide nondeterministic sums of processes. If X_{1}, X_{2}, ⋯, X_{n} ∈ P̂, we use X_{1} + ⋯ + X_{n} to denote the presheaf which at a path object P ∈ P takes the set-value

(X_{1} + ⋯ + X_{n})(P) = X_{1}(P) + ⋯ + X_{n}(P),

the disjoint union of sets X_{1}(P), ⋯, X_{n}(P). For a morphism (P, Q) of P, where P ≤ Q,

(X_{1}, + ⋯ + X_{n})(P, Q) = X_{1}(P, Q) + ⋯ + X_{n}(P, Q),

making use of the functorial nature of disjoint union (= coproduct) of sets.

Similarly, if X_{i}, i ∈ I, is an indexed family of presheaves X_{i} ∈ P̂, we use ∑_{i∈I} X_{i} to denote their coproduct. If I = ∅ this is the empty presheaf ∅, with

empty set as value at each path object.

5.3 A decomposition result

We will now observe that every presheaf X ∈ P̂ decomposes into a sum of disjoint components rooted at one of the minimal path objects τ., a!v., a? where a ∈ C, v ∈ V. The notion of rooted component will play a key role. Let M be a minimal object in P, Let X ∈ P̂. Any m ∈ X(M) determines a sub-presheaf C_{m} of X as follows. Letting m ∈ X(M), define

C_{m}(P) = \{ \begin{matrix}\{p ∈ X(P) | X(M, P)(p) = m\} & if M ≤ P, \\ ∅ & otherwise \end{matrix}

for P ∈ P, and when P ≤ Q define the function C_{m}(P, Q) : C_{m}(Q) → C_{m}(P) by

C_{m}(P, Q)(q) = X(P, Q)(q) for q ∈ C_{m}(Q)

— because X is a contravariant functor it follows that

X(M, P)(X(P, Q)(q) = X(M, Q)(q) = m

so that X(P, Q)(q) ∈ C_{m}(P). It is easily checked that C_{m} is a presheaf and indeed a sub-presheaf of X because its action on morphisms (P, Q), when P ≤ Q, restricts that of X.

Notation: In this situation, we shall say C_{m} is a rooted component of X at m.

Rooted components of X are pairwise disjoint in the sense that if M, M′ are minimal objects of P and C_{m} is a rooted component at m ∈ X(M) and C_{m′} is a rooted component at m′ ∈ X(M′), then if at P ∈ P, C_{m}(P) ∩ C_{m′}(P) ≠ ∅ then M = M′ and m = m′. Thus, for any path object P ∈ P,

X(P) = ⋃_{M} ⋃_{m∈X(M)} C_{m}(P) ,  (1)

a disjoint union, where M ranges over minimal objects of P. Consequently, X is isomorphic to a sum of its rooted components:

X ≅ ∑_{M} ∑_{m∈X(M)} C_{m}  (2)

where M ranges over minimal objects of P and C_{m} is the rooted component of X at m.

We analyse further the form of rooted components of X ∈ P̂.

A rooted component C_{i} at i ∈ X(τ.) is isomorphic to τ.X_{i} where X_{i} ∈ P̂ is given by

X_{i}(P) = C_{i}(τ.P), on objects P ∈ P, and
X_{i}(P, Q) = C_{i}(τ.P, τ.Q) : X_{i}(Q) → X_{i}(P), on morphisms P ≤ Q of P.

We write X →^{τ} X′ when there is i ∈ X(τ.) such that X′ = X_{i}. The assignment i ↦ X_{i} is a bijection between the sets X(τ.) and {X′ | X →^{τ} X′}.

A rooted component C_{i} at i ∈ X(a!v), for a ∈ C and v ∈ V, is isomorphic to a!v.X_{j}, where X_{j} ∈ P̂ is given by

X_{j}(P) = C_{j}(a!v.P), on objects P ∈ P, and
X_{j}(P, Q) = C_{j}(a!v.P, a!v.Q), on morphisms P ≤ Q of P.

We write X →^{a!v} X′ when there is j ∈ X(a!v) such that X′ = X_{j}. The assignment j ↦ X_{j} is a bijection between the sets X(a!v.) and {X′ | X →^{a!v} X′}.

Let C_{k} be a rooted component at K ∈ X(a?). Define

\begin{aligned}X_{k}(v)(P) & = C_{k}(a?(v ↦ P)), and \\ X_{k}(v)(P, Q) & = C_{k}(a?(v ↦ P), a?(v ↦ Q)) : X_{k}(v)(Q) → X_{k}(v)(P). \end{aligned}

Then X_{k} is a function from values v ∈ V to presheaves X_{k}(v) ∈ P̂ such that C_{k} is isomorphic to a?X_{k}. We write X →^{a?} F when there is k ∈ X(a?) such that F is isomorphic to X_{k}. The assignment k ↦ X_{k} is a bijection between the sets X(a?) and {F | X →^{a?} F }.

Recalling (1) above and the definition of X_{j} for j ∈ X(a!v) and X_{k} for k ∈ X(a?) we deduce:

\begin{aligned}X(τ.P) & = ⋃_{i∈X(τ.)} X_{i}(P) \\ X(a!v.P) & = ⋃_{j∈X(a!v.)} X_{j}(P) \\ X(a?(v ↦ P)) & = ⋃_{k∈X(a?)} X_{k}(v)(P) \end{aligned}

with unions which are disjoint, where a ∈ C and v ∈ V.

Recalling the decomposition (2) above, we obtain the following decomposition result:

Proposition 1 Let X ∈ P̂. Then

X ≅ ∑_{i∈X(τ.)} τ.X_{i} + ∑_{(a,v)∈C×V} ∑_{j∈X(a!v.)} a!v.X_{j} + ∑_{a∈C} ∑_{k∈X(a?.)} a?X_{k} .

5.4 Guarded recursive definitions

Presheaf categories possess all colimits and so in particular ω-colimits for building denotations of recursive definitions. In fact, because all our definitions have been given concretely as operations on sets, we are able to show that they are all continuous with respect to the sub-presheaf relation, and the solution of recursive definitions reduces to finding fixed points of a continuous function on cpo’s; we obtain solutions up to equality and not just isomorphism.

There is clearly a well-founded relation ≺ on path objects P given by their inductive definition. If a presheaf X say is a solution to a guarded recursive definition then X will be equal to an expression in which each occurrence of X lies under a prefix operation. Hence by the results of Section 5.3, X(P) is given in terms of X(Q) where Q ≺ P. Thus, by well-founded induction any solution is uniquely determined. A similar argument applies to an operation on presheaves, like parallel composition defined below, whose values on presheaves is defined recursively in terms of the operation under prefixes—it too is uniquely determined.

5.5 Parallel composition

Let X, Y ∈ P̂ have the decompositions :

X ≅ ∑_{i∈I} τ.X_{i} + ∑_{(a,v)∈C×V} ∑_{j∈J_{a,v}} a!v.X_{j} + ∑_{a∈C} ∑_{k∈K_{a}} a?X_{k}

Y ≅ ∑_{l∈L} τ.Y_{l} + ∑_{(a,v)∈C×V} ∑_{m∈M_{a,v}} a!v.Y_{m} + ∑_{a∈C} ∑_{n∈N_{a}} a?Y_{n}

Their parallel composition X | Y is defined recursively to be

∑_{i∈I} τ.(X_{i} | Y) + ∑_{(a,v)∈C×V} ∑_{j∈J_{a,v}} a!v.(X_{j} | Y) + ∑_{a∈C} ∑_{k∈K_{a}} a?v.(X_{k}(v) | Y)

+ ∑_{l∈L} τ.(X | Y_{l}) + ∑_{(a,v)∈C×V} ∑_{m∈M_{a,v}} a!v.(X | Y_{m}) + ∑_{a∈C} ∑_{n∈N_{a}} a?v.(X | Y_{n}(v))

+ ∑_{(a,v)∈C×V} ∑_{j∈J_{a,v}} ∑_{n∈N_{a}} τ.(X_{j} | Y_{n}(v)) + ∑_{(a,v)∈C×V} ∑_{m∈M_{a,v}} ∑_{k∈K_{a}} τ.(X_{k}(v) | Y_{m}) .

5.6 Late denotational semantics

Suppose t is a process term with free process-variables within U_{1}, ⋯, U_{m} and free value-variables within x_{1}, ⋯, x_{n} (possibly empty lists). The denotation of t in this context, written [[t[U_{1}, ⋯, U_{m}; x_{1}, ⋯, x_{n}]]], is a function (extendable to a functor) P̂^{m} × V^{n} → P̂, given by structural induction on t in the usual fashion, matching syntactic constructs with the appropriate semantic operations:

[[nil[U^{→}; x^{→}]]] X^{→} v^{→}= ∅, the empty presheaf.

[[τ.t[U^{→}; x^{→}]]] X^{→} v^{→}= τ.([[t[U^{→}; x^{→}]]] X^{→} v^{→})

[[a!e.t[U^{→}; x^{→}]]] X^{→} v^{→}= a!w.([[t[U^{→}; x^{→}]]] X^{→} v^{→})

where e evaluates to w in environment v^{→} / x^{→}.

[[a?y.t[U^{→}; x^{→}]]] X^{→} v^{→}= a?w.([[t[U^{→}; x^{→}, y]]] X^{→} v^{→} w)

[[t_{1} | t_{2}[U^{→}; x^{→}]]] X^{→} v^{→}= [[t_{1}[U^{→}; x^{→}]]] X^{→} v^{→} | [[t_{2}[U^{→}; x^{→}]]] X^{→} v^{→}

[[t_{1} + t_{2}[U^{→}; x^{→}]]] X^{→} v^{→}= [[t_{1}[U^{→}; x^{→}]]] X^{→} v^{→} + [[t_{2}[U^{→}; x^{→}]]] X^{→} v^{→}

[[[e_{1} = e_{2}]t[U^{→}; x^{→}]]] X^{→} v^{→}

= \{ \begin{matrix}[[t[U^{→}; x^{→}]]] X^{→} v^{→} & if e_{1}, e_{2} evaluate to a common value in v^{→} / x^{→}. \\ ∅, & the empty presheaf, otherwise. \end{matrix}

[[U_{i}[U^{→}; x^{→}]]] X^{→} v^{→}= X_{i}

[[recY.t[U^{→}; x^{→}]]] X^{→} v^{→}= R, the unique solution of R = [[t[U^{→}, Y; x^{→}]]] X^{→} R v^{→} .

Lemma 2 Let t be a process term with free process-variables among U_{1}, ⋯, U_{m} and free value-variables among x_{1}, ⋯, x_{n}. Suppose s_{1}, ⋯, s_{m} are closed process-terms and that v_{1}, ⋯, v_{n} are values in V. Then,

[[t[U^{→}; x^{→}]]][[s^{→}]] = [[t[s^{→} / U^{→}][v^{→} / x^{→}]]].

6 The late semantics related

The decomposition result and the preparatory discussion suggest that we view a presheaf over P as a transition system. In particular, it is sensible to view a relation X →^{τ} X′ holding between presheaves X, X′ as meaning that the process represented by the presheaf X can make a τ-transition to a process represented by the presheaf X′. There is a similar reading of X →^{a!v} X′, while X →^{a?} F means X can receive a value on channel a when, depending on the value v received, it will resume as process F (v).

Thus, a closed process term is associated with two transition systems, one from the transition semantics and one from its denotation as a presheaf.

The next lemma asserts, essentially, that the relation

{([[t]], t) | t a closed process term}

is a late-bisimulation between the two transition systems.

Lemma 3 Let t be a closed process term. Then,

\begin{matrix}[[t]] →^{τ} X & iff ∃t′. t →^{τ} t′ & [[t′]] = X , \\ [[t]] →^{a!v} X & iff ∃t′. t →^{a!v} t′ & [[t′]] = X , \\ [[t]] →^{a?} F & iff ∃t′, y. t →^{ay} t′ & [[t′[y]]] = F . \end{matrix}

Proof: For W ∈ P̂ and t a closed process term define W ≈ t iff

\begin{aligned}∀Z. W →^{τ} Z & ⇔ ∃t′. t →^{τ} t′ & [[t′]] = Z, \\ ∀Z, a, v. W →^{a!v} Z & ⇔ ∃t′. t →^{a!v} t′ & [[t′]] = Z, and \\ ∀F, a. W →^{a?} F & ⇔ ∃t′, y. t →^{a?y} t′ & [[t′[y]]] = F. \end{aligned}

The proof proceeds by structural induction an process terms t with induction hypothesis:

If t has free process-variables within X_{1}, ⋯, X_{n}, free value-variables within x_{1}, ⋯, x_{n}, and S_{1}, ⋯, S_{n} are closed process-terms such that

X_{i} is guarded in t or [[S_{i}]] ≈ S_{i}, whenever 1 ≤ i ≤ m,

then for all v_{1}, ⋯, v_{n} ∈ V,

[[t[X^{→}; x^{→}]]] [[s]]^{→}v^{→}≈ t[s^{→} / X^{→}; v^{→} / x^{→}]

—using an obvious vector notation.

Clearly, when t is closed the induction hypothesis amounts to [[t]] ≈ t, as required. □

As will be seen, the bisimilarity induced by spans of open maps in P̂ coincides with the natural translation of late bisimulation to presheaves.

Definition: A late bisimulation on presheaves consists of a binary relation R on presheaves P̂ such that whenever X R Y,

X →^{τ} X′ ⇒ ∃Y′. Y →^{τ} Y′ & X′ R Y′,

Y →^{τ} Y′ ⇒ ∃X′. X →^{τ} X′ & X′ R Y′,

X →^{a!v} X′ ⇒ ∃Y′. Y →^{a!v} Y′ & X′ R Y′,

Y →^{a!v} Y′ ⇒ ∃X′. X →^{a!v} Y & X′ R Y′,

X →^{a?} F ⇒ ∃G. Y →^{a?} G & ∀v ∈ V. F (v) R G(v),

Y →^{a?} G ⇒ ∃F. X →^{a?} F & ∀v ∈ V. F (v) R G(v).

Say X, Y ∈ P̂ are late bisimilar iff X R Y for some late bisimulation on presheaves R.

That surjective open maps induce late bisimulations on presheaves follows directly from the next lemma.

Lemma 4 Assume f : X → Y is an open map P̂.

Let M be a minimal object of P̂. If C_{m} is a rooted component of X at m ∈ X(M) then the image fC_{m} is a rooted component of Y at f_{M}(m); the restriction f_{C_{m}} of f to C_{m} is an open map f_{C_{m}} : C_{m} → fC_{m}.

Moreover, if f is surjective then any rooted component of Y is the image of a rooted component of X under f, and each restriction f_{C_{m}}, where C_{m} is a rooted component of X, is a surjective open map.

Proof: Direct consequence of the definition of open map. □

Corollary 5 If h : X → Y is a surjective open map in P̂, then X, Y are late bisimilar.

Proof: Define R a relation on presheaves by:

W R Z iff ∃f : W → Z surjective and open in P̂.

Then R is a late bisimulation on presheaves by Lemma 4. □

Corollary 6 If X, Y are bisimilar in P̂, i.e. they are related by an span of surjective open maps, then X, Y are late bisimilar as presheaves.

Proof: ¿From Corollary 5, as late bisimilarity on presheaves is easily seen to be an equivalence relation. □

Thus a span of surjective open maps yields a late bisimulation between presheaves. We now show the converse. For the presheaves X, Y and a latebisimulation R which relates them we construct a sub-presheaf of R_{XY} ⊆ X × Y whose projections to X and Y are surjective open maps.

For X ∈ P̂, recall from Section 5.3, the bijections between

• i ∈ X(τ.) and transitions X →^{τ} X_{i} ,

• j ∈ X(a!v) and transitions X →^{a!v} X_{j} ,

• k ∈ X(a?) and transitions X →^{a?} X_{k} .

They are used in the next definition.

Definition: Let R be a late bisimulation. Define, by induction on the structure of path objects P ∈ P, sets R_{XY} (P) whenever X R Y:

\begin{aligned}R_{XY} (τ.) & = & \{(i, l) ∈ X(τ.) × Y (τ.) | X_{i} R Y_{l}\} \\ R_{XY} (τ.P) & = & ⋃\{R_{X_{i}Y_{l}}(P) | (i, l) ∈ R_{XY} (τ.)\} \\ R_{XY} (a!v.) & = & \{(j, m) ∈ X(a!v.) × Y (a!v.) | X_{j} R Y_{m}\} \\ R_{XY} (a!v.P) & = & ⋃\{R_{X_{j}Y_{m}}(P) | (j, m) ∈ R_{XY} (a!v.)\} \\ R_{XY} (a?) & = & \{(k, n) ∈ X(a?) × Y (a?) | ∀v ∈ V. X_{k}(v) R Y_{n}(v)\} \\ R_{XY} (a?(v ↦ P)) & = & ⋃\{R_{X_{k}(v)Y_{n}(v)}(P) | (k, n) ∈ R_{XY} (a?)\} \end{aligned}

Lemma 7 Let R be a late bisimulation on presheaves. If X R Y, then

(i) R_{XY} extends to a sub-presheaf of X × Y.

(ii) The compositions R_{XY} ↪ X × Y →^{π_{1}} X and R_{XY} ↪ X × Y →^{π_{2}} Y

are surjective open, where π_{1}, π_{2} are the projections associated with the product X × Y.

Proof: (i) It is first necessary to show that R_{XY} (P) ⊆ X(P) × Y (P). This follows by induction on the structure of P ∈ P̂. For instance consider a path object of the form a?(v ↦ P). Suppose X →^{a?} X_{k}, k ∈ X(a?), and Y →^{a?} Y_{n}, n ∈ Y (a?), with ∀v ∈ V. X_{k}(v) R Y_{n}(v). Now,

R_{X_{k}(v)Y_{n}(v)}(P) ⊆ X_{k}(v)(P) × Y_{n}(v)(P) by induction,
⊆ X(a?(v ↦ P)) × Y (a?(v ↦ P)) by Section 5.3.

Thus

R_{XY} (a?(v ↦ P)) ⊆ X(a?(v ↦ P)) × Y (a?(v ↦ P)).

An induction on the clauses for deriving morphisms P ≤ Q in P̂ (see Section 4) shows X(P, Q) × Y (P, Q) restricts to a function R_{XY} (Q) → R_{XY} (P), making R_{XY} a sub-presheaf of X × Y.

(ii) Write ρ_{1}, ρ_{2} for the restriction of the projections R_{XY} ↪ X × Y →^{π_{1}} X and R_{XY} ↪ X × Y →^{π_{2}} Y. That each component ρ_{1}_{P} , ρ_{2}_{P} is surjective is proved by induction on the structure of path objects P. The quasi-pullback conditions providing the openness of ρ_{1} and ρ_{2} are shown to hold by induction on the clauses for deriving morphisms P ≤ Q in P̂. □

Hence:

Theorem 8 Presheaves X, Y ∈ P̂ are late-bisimilar iff they are related by a span of surjective open maps.

The next lemma links late-bisimilation on presheaves and late-bisimulation on closed terms of VProc, and yields the main result of this section—the equivalence of the operational and denotational formulations of bisimilarity.

Lemma 9 Let t_{1}, t_{2} be closed process terms. The denotations [[t_{1}]], [[t_{2}]] are late bisimilar as presheaves iff t_{1}, t_{2} are late bisimilar.

Proof: Assuming R is a late-bisimulation on presheaves, it is claimed we obtain a late-bisimulation S on (closed) process terms by defining

S = {(t_{1}, t_{2}) | [[t_{1}]] R [[t_{2}]]}.

Conversely, assuming S is a late-bisimulation on (closed) process terms, it is claimed we obtain a late bisimulation on presheaves by defining

R = {([[t_{1}]], [[t_{2}]]) | t_{1} S t_{2}}.

The proof of these two claims rests on Lemma 3, with recourse to the Substitution Lemma 2.

For example, suppose S is obtained from a late-bisimulation on presheaves as above. Suppose s_{1}Ss_{2} and s_{1} →^{a?y} s′_{1}. For S to be a late bisimulation we are required to find a matching transition of s_{2}. However, by Lemmas 3, [[s_{1}]] →^{a?} [[s′_{1}[y]]], so because [[s_{1}]]R[[S_{2}]] there is G : V → P̂ for which

[[s_{2}]] →^{a?} G and ∀v ∈ V. [[s′_{1}[y]]](v)RG(v).

By Lemma 3 again, there are s′_{2}, z for which

s_{2} →^{a?z} s′_{2} & [[s′_{2}[z]]] = G.

By the Substitution Lemma 2,

∀v ∈ V. [[s′_{1}[v/y]]]R[[s′_{2}[v/z]]],

i.e. ∀v ∈ V. s′[v/y]Ss′_{2}[v/z], as required. □

Theorem 10 Closed process terms t_{1}, t_{2} of VProc are late-bisimilar iff their denotations [[t_{2}]], [[t_{2}]] are related by a span of surjective open maps.

Proof: Directly from Theorem 8 and Lemma 9. □

7 Variations

A transition semantics and bisimulation for VProc with early value passing can be obtained easily on the lines of [14]. An appropriate presheaf semantics is obtained with a path category a partial order which is an initial solution to:

P = P_{⊥} + ∑_{(a,v)∈C×V} P_{⊥} + ∑_{(a,v)∈C×V} P_{⊥}

In fact P̂ is isomorphic to rooted presheaves over P_{⊥} which is readily seen to be isomorphic to a category of synchronisation trees in which labels have the form τ, a!v or a?v where a ∈ C and v ∈ V, a category ST_{C×V} in the notation of [12, 4]. For such categories bisimulation obtained from open maps has been shown to coincide with Park and Milner’s strong bisimulation [12].

Furthermore, denotational semantics is given in [19] in which denotations of terms as synchronisation trees are strong bisimilar to the transition systems from an operational semantics. Thus there is no difficulty in producing a denotational semantics so that the denotation of closed terms in P̂ are connected by a span of open surjections iff the terms are strong bisimilar.

A much greater challenge is provided by a process-passing language with a syntax similar to that of VProc

t ::= nil | τ.t | a!t_{1}.t_{2} | a?X.t | (t_{1} | t_{2}) | t_{1} + t_{2} | X | recX.t

but where in contrast to VProc a process t_{1} can be sent along a channel a by a process a!t_{1}.t_{2} and an arbitrary process can be received on a and bound to process-variable X in a process a?X.t. A transition semantics can be found, for instance, in [16]. A path category for process-passing with late semantics is reasonably taken to be an initial solution to the following isomorphism in Prof

P ≅ P_{⊥} + ∑_{a∈C}(P × P)_{⊥} + ∑_{a∈C}(!P ⊸ P)_{⊥}

or sufficiently an initial solution to

P ≅ P_{⊥} + ∑_{a∈C}(P + P)_{⊥} + ∑_{a∈C}((!P)^{op} × P)_{⊥}

in Cat—the constructions one is led to by Section 3. There is little trouble in giving a denotational semantics to a term with n free variables as a functor P̂^{n} → P̂. So closed terms, denoting presheaves in P̂, inherit a notion of bisimulation from open maps in presheaf categories. But there is a problem in understanding the bisimulation that arises, for example as a coinductive definition based on a transition semantics, along the usual lines. The difficulties are due to the function space component (!P ⊸ P).

On the other hand, there seem to be no fundamental difficulties in presenting a presheaf model of the Pi-calculus, where following the lead of [17, 5] we (Cattani,Stark,Winskel) move to Prof^{I}, indexed by a category of namesets I.

Acknowledgements

I especially thank Martin Hyland for very helpful discussions during my stay at the Isaac Newton Institute, Cambridge University. Thanks also to Jaap van Oosten for useful pointers to the literature.

References

[1] Abramsky, S., On semantic foundations of applicative multiprogramming. Proc. ICALP’83, Barcelona, LNCS 154, 1983.

[2] Adamek, J., and Rosicky J., Locally presentable and accessible categories. LMS Lecture Notes Series 189, 1994.

[3] Borceux, F., Handbook of categorical logic, 1. Cambridge University Press, 1994.

[4] Cattani, G.L., and Winskel, G., Presheaf models for concurrency. Manuscript, 1996.

[5] Fiore, M., Moggi, E., and Sangiori, D., A fully abstract model for the Pi-calculus. Proc. of LICS’96.

[6] Hennessy, M., and Ingolfsdottir, A., A theory of communicating processes with value passing. Information and Computation, 107(2), 1993.

[7] Hennessy, M., and Plotkin, G., A term model for CCS. Proc. 9th MFCS, Poland, LNCS 88, 1980.

[8] Ingolfsdottir, A., A semantic theory for value-passing processes, late appraoch—Parts I and II. BRICS reports RS–95–3/22, 1995.

[9] Johnstone, P.T., Stone Spaces. Cambridge University Press, 1982.

[10] Joyal, A., and Moerdijk, I., Algebraic set theory. LMS Lecture Notes Series 220, Cambridge University Press, 1995.

[11] Joyal, A., and Moerdijk, I., A completeness theorem for open maps. In Annals of Pure and Applied Logic 70, 51-86, 1994.

[12] Joyal, A., Nielsen, M., and Winskel, G., Bisimulation from open maps. Report Series RS-94-7, BRICS, University of Aarhus, Denmark, May 1994. Accepted for a LICS 93 special issue of Information and Computation.

[13] Lehman, D., Categories for fixed point semantics. FOCS 17, 1976.

[14] Milner, A.R.G., Communication and concurrency, Prentice Hall, 1989.

[15] Milner, R., Parrow, J., and Walker, D., A calculus of mobile processes, Parts I and II. Information and Computation, 100:1-77, 1992.

[16] Sangiori, D., Bisimulation for higher-order process calculi. INRIA Report, Sophia-Antipolis, RR-2508, 1995.

[17] Stark, I.,A fully abstract domain model for the Pi-calculus. Proc. of LICS’96, 1996.

[18] Vickers, S., Geometric theories and databases. In LMS Lecture Notes Series 177, 1992.

[19] Winskel, G., and Nielsen, M., Models for concurrency. In the Handbook of Logic in Computer Science, vol.IV, ed. Abramsky, Gabbay and Maibaum, Oxford University Press, 1995.

Recent Publications in the BRICS Report Series

RS-96-44 Glynn Winskel. A Presheaf Semantics of Value-Passing Processes. November 1996. 23 pp. Extended and revised version of paper appearing in Montanari and Sassone, editors, Concurrency Theory: 7th International Conference, CONCUR ’96 Proceedings, LNCS 1119, 1996, pages 98�114.

RS-96-43 Anna Ing� olfsd� ottir. Weak Semantics Based on Lighted Button Pressing Experiments, An Alternative Characterization of the Readiness Semantics. November 1996. An extended abstract to appear in the proceedings of the 10th Annual International Conference of the European Association for Computer Science Logic, CSL ’96.

RS-96-42 Gerth St�lting Brodal and Sven Skyum. The Complexity of Computing the k-ary Composition of a Binary Associative Operator. November 1996. 15 pp.

RS-96-41 Stefan Dziembowski. The Fixpoint Bounded-Variable Queries are PSPACE-Complete. November 1996. 16 pp. Presented at the 10th Annual International Conference of the European Association for Computer Science Logic, CSL ’96.

RS-96-40 Gerth St�lting Brodal, Shiva Chaudhuri, and Jaikumar Radhakrishnan. The Randomized Complexity of Maintaining the Minimum. November 1996. 20 pp. To appear in a special issue of Nordic Journal of Computing devoted to the proceedings of SWAT ’96. Appears in Karlson and Lingas, editors, Algorithm Theory: 5th Scandinavian Workshop, SWAT ’96 Proceedings, LNCS 1097, 1996, pages 4�15.

RS-96-39 Hans H� uttel and Sandeep Shukla. On the Complexity of Deciding Behavioural Equivalences and Preorders � A Survey. October 1996. 36 pp.

RS-96-38 Hans H� uttel and Josva Kleist. Objects as Mobile Processes. October 1996. 23 pp.