BRICS RS-97-34 Cattani et al.: Presheaf Models for the π-Calculus BRICS

Basic Research in Computer Science

Presheaf Models for the π-Calculus

Gian Luca Cattani Ian Stark Glynn Winskel BRICS Report Series RS-97-34 ISSN 0909-0878 December 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, 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 BRICS Report Series publications. 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 the World Wide Web and anonymous FTP through these URLs:

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

This document in subdirectory RS/97/34/

Presheaf Models for the π-Calculus

Gian Luca Cattani, Ian Stark and Glynn Winskel BRICS^{∗}, Department of Computer Science, University of Aarhus, Denmark

December 1997

Abstract

Recent work has shown that presheaf categories provide a general model of concurrency, with an inbuilt notion of bisimulation based on open maps. Here it is shown how this approach can also handle systems where the language of actions may change dynamically as a process evolves. The example is the π-calculus, a calculus for ‘mobile processes’ whose communication topology varies as channels are created and discarded. A denotational semantics is described for the π-calculus within an indexed category of profunctors; the model is fully abstract for bisimilarity, in the sense that bisimulation in the model, obtained from open maps, coincides with the usual bisimulation obtained from the operational semantics of the π-calculus. While attention is concentrated on the ‘late’ semantics of the π-calculus, it is indicated how the ‘early’ and other variants can also be captured.

A version of this paper appears in Category Theory and Computer Science: Proceedings of the 7th International Conference CTCS ’97, Lecture Notes in Computer Science 1290. Springer-Verlag, September 1997.

∗Basic Research in Computer Science, a centre of the Danish National Research Foundation.

1 Introduction

The gap between domain theory and the theory of concurrency is narrowing. In particular, the π-calculus, which for a long time resisted all but operational semantics, has yielded to a fully abstract denotational semantics; a key idea was to move to domains indexed by a category of name sets (Stark 1996; Fiore, Moggi, and Sangiorgi 1996; Hennessy 1996). Why add yet another model, based this time not on familiar, complete partial orders but instead on presheaf categories?

Several reasons can be given, even at this preliminary stage.

Models for concurrency are best presented as categories where one can take advantage of the universality of constructions (see Winskel and Nielsen (1995)). If domain theory is to meet models for concurrency, it seems that the points of information in a complete partial order need to be replaced by more detailed objects in a category. A problem with the categories of traditional models is that they do not support higherorder constructions. Presheaf categories, on the other hand, not only include important traditional models like synchronisation trees and event structures,^{1} but also support function spaces. We see presheaf models as taking us towards a a new domain theory in which presheaf models are analogous to nondeterministic domains (Hennessy and Plotkin 1979).

Another motivation comes in getting a more systematic and algebraic understanding of bisimulation. A traditional way to proceed in giving a theory to a process language has been first to endow it with an operational semantics, provide a definition of bisimulation, follow this by the task of verifying that the bisimulation is a congruence (maybe by modifying it a bit), and then establish proof rules. Often the pattern is standard, but sometimes even getting a passable definition of bisimulation can be tricky, as, for example, when higher-order features are involved. An advantage of presenting models for concurrency as categories has been that they then support a general definition of bisimulation based on open maps (Joyal et al. 1996). We can then exploit the universality of various constructions in showing that they preserve bisimulation (Cattani and Winskel 1997). Presheaf categories come along with a concept of open map and bisimulation. They themselves form a category (strictly a bicategory of profunctors), in which the objects are presheaf categories, yielding ways to combine presheaf categories and their bisimulations.

1In the sense that these traditional models embed fully, faithfully and densely in particular presheaf models (Joyal, Nielsen, and Winskel 1996).

The problem with general definitions is that it’s not always so easy to see what their instances amount to. Indeed, a major task of this paper is showing that the bisimulation on processes of the π-calculus obtained from open maps coincides with a traditional definition (following up on earlier work for value-passing processes (Winskel 1996)). However, the presheaf model for the π-calculus contributes more than this. Along the way, the presheaf model casts light on bisimulation for the π-calculus and why operations preserve it; the normal form for processes in the π-calculus (Fiore et al. 1996), which can be read off from the definition of the model (Theorem 7); and suggests smooth translations between variants of the π-calculus (Section 5). We also claim that, compared to the domain model, the “domain equation” of our model is rather simpler, because we seek a category of paths, not processes; the presheaf construction then fills in the necessary nondeterminism. As a result the system is particularly flexible: here we present the full ‘late’ π-calculus in detail, but we also sketch how the same category holds models of the ‘early’ π-calculus and other popular variants.

The recent domain models for the π-calculus lie within a functor category Cpo^{I} (Fiore et al. 1996; Stark 1996). Here I is the category of finite sets of names and injections between them, representing the fact that over time new names may be created and old names relabelled to avoid clashes. Hennessy (1996) has followed the same approach in his model for testing equivalences. The key to capturing the π-calculus is that the categorical requirements of functoriality and naturality give uniformity over varying name sets. Most notably Cpo^{I} is cartesian closed, and the function space correctly handles the fact that old processes must be prepared to receive new names. This paper makes the same step up in the presheaf approach, to give a model of the π-calculus not in Prof but in Prof^{I}.

In the remainder of this section we provide a brief overview of the material that we shall need: syntax and operational semantics of the π-calculus; presheaf models for concurrency; the category Prof of profunctors; and the functor category Prof^{I}. Section 2 presents our equation for the π-calculus and analyses the path category P it defines. Section 3 builds three important operations on P: parallel composition, restriction and replication. In Section 4 we show how to interpret processes in P and prove full abstraction for the model. Section 5 closes with a description of current and future adaptations of the work to other calculi.

1.1 The π-calculus

The version of the π-calculus we use is entirely standard. We summarise it only very briefly here: for discussion and further detail see the original papers (Milner, Parrow, and Walker 1992a,b; Milner 1991). Processes have the following syntax

P :: = x̄y.P | x(y).P | νx P | [x=y]P | 0 | P + P | P | P | !P

with x and y ranging over some infinite supply of names. Note that we include the match operator [x=y]P, unguarded sum and unguarded replication !P. This selection is fairly arbitrary: our model copes equally well with mismatch [x≠y]P and processes defined by recursion, guarded or unguarded. Similarly, it makes no difference if we restrict to one of the popular subsets, such as the asynchronous π-calculus (Boudol 1992).

To simplify presentation we identify processes up to a structural congruence, the smallest congruence relation satisfying

[x = x]P ≡ P  !P ≡ P |!P \begin{aligned}x(y).P & ≡ x(z).P [z/y] & z ∉ fn(P) \\ νy P & ≡ νz P [z/y] & z ∉ fn(P) \end{aligned}
P + 0 ≡ P P + Q ≡ Q + P (P + Q) + R ≡ P + (Q + R)
P | 0 ≡ P P | Q ≡ Q | P  (P | Q) | R ≡ P |(Q | R).

Here P [z/y] denotes capture-avoiding substitution — which may of course require in turn the α-conversion of subexpressions. This equivalence is not as aggressive as the structural congruence of, say, Definition 3.1 in (Milner 1992), which allows name restriction νx(−) to change its scope. Nevertheless it cuts down the operational rules we shall need, with none at all for matching and replication. All this is to some degree a matter of taste: if we treat process terms as concrete syntax, with no structural identification, the model is still valid. Indeed full abstraction then allows us to read off the fact that α-conversion, commuting ‘+’ and so forth all respect bisimilarity (replacing, for example, the proofs of Theorems 1 to 9 in (Milner et al. 1992b, §3)).

The operational semantics of processes are given by transitions of four kinds: internal or ‘silent’ action τ, input x(y), free output x̄y and bound output x̄(y). We denote a general transition by α, and define its free and bound names thus:

fn(τ) = ∅ fn(x̄y) = {x, y} fn(x(y)) = fn(x̄(y)) = {x}
bn(τ) = ∅ bn(x̄y) = ∅  bn(x(y)) = bn(x̄(y)) = {y}.

OUT  x̄y.P ⟶^{x̄y} P  SUM  \frac{P ⟶^{α} P′}{P + Q ⟶^{α} P′}
IN  x(y).P ⟶^{x(y)} P  PAR  \frac{P ⟶^{α} P′}{P | Q ⟶^{α} P′ | Q} \begin{matrix}bn(α) ∩ fn(Q) \\ = ∅ \end{matrix}

RES \frac{P ⟶^{α} P′}{νx P ⟶^{α} νx P′} x ∉ fn(α) COM  \frac{P ⟶^{x(y)} P′ Q ⟶^{x̄z} Q′}{P | Q ⟶^{τ} P′[z/y] | Q′}

OPEN \frac{P ⟶^{x̄y} P′}{νy P ⟶^{x̄(y)} P′} x ≠ y  CLOSE \frac{P ⟶^{x(y)} P′ Q ⟶^{x̄(y)} Q′}{P | Q ⟶^{τ} νy(P′ | Q′)}

Figure 1: Transition rules for π-calculus processes

The transitions that a process may perform are given inductively by the rules in Figure 1. This is a late semantics, in that input substitution happens in the (COM) rule when communication actually occurs, rather than at (IN). The chief difference between these rules and Table 2 of (Milner et al. 1992b) is that we let structural congruence do some of the work. Thus there are no symmetric forms for the four right-hand rules, and sometimes processes must be α-converted before they can interact. Of course the possible transitions derived are exactly the same as with the original definitions.

A symmetric relation S between processes is a bisimulation if for every (P, Q) ∈ S the following conditions hold.

• For α = τ, x̄y, x̄(y), if P ⟶^{α} P′ then there is Q′ such that Q ⟶^{α} Q′ and (P′, Q′) ∈ S.

• If P ⟶^{x(y)} P′ then there is Q′ such that Q ⟶^{x(y)} Q′ and for any name z, (P′[z/y], Q′[z/y]) ∈ S.

To check this second condition it is only necessary that z ranges over the free names of P and Q, and one fresh name. This relation is strong, in that τ-actions must match, and late, in that input actions must match before the transmitted value is known. Two processes are (strong, late) bisimilar if there is some bisimulation relating them. We write P ˙∼ Q and observe that bisimilarity is itself a bisimulation, and contains all others.

Bisimilarity is preserved by all process constructors except for input prefix x(y).P. This is because bisimilarity assumes all names are distinct, while the substitution that happens on input can cause names to become identified. One thus defines processes to be equivalent P ∼ Q if they are bisimilar under all possible name substitutions. Equivalence is then the smallest congruence containing bisimilarity.

1.2 Presheaf Models and Bisimulation

Let P be a small category. The category of presheaves over P, often denoted by P̂ or by Set^{P^{op}}, is the category whose objects are contravariant functors from P to Set (the category of sets and functions) and whose arrows are the natural transformations between such functors.

A category of presheaves, P̂, is accompanied by the Yoneda embedding, a functor y_{P} : P → P̂, which fully and faithfully embeds P in the category of presheaves.

Via the Yoneda embedding we can regard P essentially as a full subcategory of P̂. In our applications, the category P is to be thought of as consisting of path objects, or computation-path shapes. The Yoneda Lemma, by providing a natural bijection between P̂(y_{P}(p), X) and X(p), justifies the intuition that a presheaf X : P^{op} → Set can be thought of as specifying for a typical path object p the set X(p) of computation paths of shape p. The presheaf X acts on a morphism m : p → q in P to give a function X(m) saying how q-paths restrict to p-paths. A presheaf being a colimit of path objects can be thought of as a collection of computation paths glued together by identifying subpaths.

Bisimulation on presheaves is derived from notion of open map between presheaves (Joyal and Moerdijk 1994). Recall, a morphism h : X → Y, between presheaves X, Y, is P-open iff for all morphisms m : p → q in P, the square

X(p)_{h_{p}}  X(q)^{Xm}  _{h_{q}} Y (p)  Y (q)_{Y m}

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

We say that presheaves X, Y in P̂ are P-bisimilar iff there is a span of surjective open maps between them. This is equivalent to there being a subobject R ↪ X × Y such that the compositions with the projections

R ↪ X × Y →^{π_{1}} X and R ↪ X × Y →^{π_{2}} Y

are surjective open.

The category P̂, over a small category P, is the free colimit completion of P. In more detail, the Yoneda embedding y_{P} : P → P̂ satisfies the universal property that for any functor F : P → E, where E is a cocomplete category, there is a colimit-preserving functor Lan_{y_{P}}(F) : P̂ → E, the left Kan extension of F along y_{P}, unique to within isomorphism, such that F ≅ Lan_{y_{P}}(F) ∘ y_{P}:

P ^{y_{P}}_{F}  P̂_{Lan_{y_{P}}(F)} E

Consequently, if G : P̂ → E is a colimit-preserving functor then, to within isomorphism, G is the left Kan extension Lan_{y_{P}}(G ∘ y_{P}). Recall, in addition, that Lan_{y_{P}}(F) is left adjoint to the functor taking Y in E to the presheaf E(F (-), Y).

Here we shall only be interested in left Kan extensions where E is a presheaf category Q̂. They, and so any colimit-preserving functor between presheaf categories, preserve open maps. Because they preserve colimits they necessarily preserve surjectivity of maps too (and hence bisimulation). Spelt out:

Lemma 1 (Cattani and Winskel 1997). Let G : P̂ → Q̂ be any colimitpreserving functor between presheaf categories. Then G preserves (surjective) open maps: If h is a (surjective) P-open map in P̂, then G(h) is a (surjective) Q-open map in Q̂.

Notation 2. If F : P → Q̂ is a functor, we will often write F_{!} for the left Kan extension Lan_{y_{P}}(F) and F^{⋆} its right adjoint, mentioned above. This notation is reminiscent of a more usual one (that we shall also employ) that given a functor F : P → Q between small categories writes F_{!} ⊣ F^{⋆} for the left Kan extension Lan_{y_{P}}(y_{Q}F) and its right adjoint. In this second case a further right adjoint is also present F^{⋆} ⊣ F_{⋆}, making F^{⋆} into a colimit preserving functor.

Thus we have a variety of general methods to obtain functors P̂ → Q̂, several of them automatically preserving colimits and hence bisimilarity. The following construction gives a relevant example.

1.2.1 A Lifting Construction

Given any category P, define P_{⊥} as the category isomorphic to P but for a new initial object ⊥ freely added. Clearly there exists a full embedding l(ift) : P → P_{⊥}. This gives rise to a triple of adjoint functors, l_{!} ⊣ l^{⋆} ⊣ l_{⋆}

P̂ ^{l_{⋆}}_{l_{!}} P̂_{⊥}^{l^{⋆}}

where for any presheaf X ∈ P̂ and path p ∈ P we have l_{⋆}(X)(p) ≅ X(p) and l_{⋆}(X)(⊥) ≅ {⋆}; from which l^{⋆}(l_{⋆}(X)) ≅ X.

The adjoint pair l^{⋆} ⊣ l_{⋆} plays an important rôle in (Joyal and Moerdijk 1995) where the base category P is actually the linear order ω of natural numbers, and l_{⋆} is considered as a successor operator. It is not difficult to prove the following proposition analogous to Lemma 2.2 loc. cit.

Proposition 3. l_{⋆} preserves surjective open maps.

1.3 Profunctors

There are several equivalent ways of presenting profunctors (also called distributors and bimodules, see Borceux (1994)). For us, a profunctor F : P → Q, between small categories P and Q, is a functor F : P → Q̂. The composition G ∘ F of profunctors F : P → Q and G : Q → R is defined to be the composition of functors

(Lan_{y_{Q}}(G)) ∘ F ,

which is only defined to within isomorphism. Thus, we obtain a bicategory^{2} of profunctors Prof .

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.

2However, henceforth we won’t be pernickety in our category-theoretic terminology, and use terms from traditional category theory, even when constructions, strictly speaking, take place in a bicategory setting.

It is helpful to view Prof as a category of “nondeterministic domains” (Hennessy and Plotkin 1979; Hennessy 1996), analogous to those obtained as the Kleisli category of a powerdomain monad. We exhibit an adjunction to back up this claim. Write ω-Acc for the category of finitely accessible categories, the category analogue of algebraic cpo’s; morphisms are functors preserving filtered colimits. The functor

(−)^{0} : ω-Acc → Prof

takes a finitely accessible category C to its “basis” C^{0}, a choice of skeletal subcategory of its finitely presentable elements; a filtered-colimit preserving functor H : B → C is sent to the profunctor H^{0} : B^{0} → C^{0} such that H^{0}(B) = C(−, H(B)) : (C^{0})^{op} → Set. The functor

ˆ(−) : Prof → ω-Acc

takes a profunctor F : P → Q to a choice of left Kan extension Lan_{y_{P}}(F). There is an equivalence of categories

ω-Acc(C, P̂) ≃ Prof (C^{0}, P) ,

given by restriction to finitely presentable objects, expressing an adjunction between ω-Acc and Prof :

ω-Acc ^{(−)^{0}}^{⊥} Prof ˆ(−)

With bicategorical quibbles, there is good reason to call Prof the Kleisli category of the monad ˆ(−)^{0}, and to think of the monad as analogous to powerdomains in that it introduces nondeterminism.

Turning the monad around we obtain a comonad !P = (P̂)^{0}, amounting to the finite-colimit completion of P, whose co-Kleisli category consists of presheaf categories with filtered-colimit-preserving functors as morphisms. In addition, the bicategory Prof is rich in constructions which enable us to handle higher-order processes as presheaves. Many of these constructions are associated with Prof being a model of classical linear logic. The tensor ⊗ is of particular interest: on objects P ⊗ Q is the product of categories P × Q; while on morphisms if F : P → P′ and G : Q → Q′ are profunctors then F ⊗ G : P ⊗ Q → P′ ⊗ Q′ acts according to:

((F ⊗ G)(p, q))(p′, q′) = ((F (p))(p′)) × ((G(q))(q′)) ,

where × is the product functor in Set. The unit of ⊗ is 1, the category with a single object and morphism. Defining the linear function space P→Q to be the product of categories P^{op}×Q, we see the natural bijection

Prof (P, [Q → R]) ≅ Prof (P ⊗ Q, R) .

It is easy to see that presheaves over P→Q correspond to profunctors, and so, to within isomorphism, to colimit-preserving functors from P̂ to Q̂. Filtered-colimit-preserving functors are represented, with the help of the exponential !, as presheaves over !P → Q. Products (&) and coproducts (+, Σ) in Prof coincide on objects, where both are given by coproduct of categories; similarly ⊤ and 0 are both the empty category. Linear involution P^{⊥} is isomorphic to P → 1 and so to P^{op}. Prof is compactclosed: par (�) coincides with tensor (⊗), and ⊥ with 1.

1.3.1 A Diagonal

Later, in our treatment of replication in the π-calculus, we shall use a diagonal map, which we now construct. Let P and Q be two small categories. Take w_{P} : P × Q → P and w_{Q} : P × Q → Q to be the two projection functors. By composing with the Yoneda embedding they can be promoted to the status of maps in Prof and therefore give rise to a universal profunctor w_{P,Q} = ⟨w_{P}, w_{Q}⟩ : P ⊗ Q → P&Q.^{3} This induces an adjoint pair between the associated presheaf categories:

{ \atop P × Q} ^{w_{!}}^{⊥} P̂ × Q̂_{w^{⋆}} .

Since Prof has products we also have that for any small category P a diagonal arrow Δ_{P} : P → P&P is definable. By composing the extension Δ_{P,!} with w_{P,P}^{⋆}, we obtain a functor

d_{P} : P̂ → { \atop P × P} .

It is not difficult to prove that for any presheaf X over P and for any two objects p_{1}, p_{2} of P:

d_{P}X⟨p_{1}, p_{2}⟩ = X(p_{1}) × X(p_{2}) .

Like the lifting of Section 1.2.1, this is a structural arrow, and it makes sense to establish the following preservation property.

3Given the “linear logic” structure of Prof , the map w does correspond to a form of weakening.

Proposition 4. Let P and Q be two small categories; then w_{P,Q}^{⋆} preserves surjective open maps and, consequently, d_{P} does too.

1.4 The Functor Category Prof^{I}

As a π-calculus process evolves, the ambient set of channel names may change. To take account of this variability, our path category for the πcalculus will be indexed by I, the category of finite name sets and injective maps between them. Rather than Prof itself then, we are specifically interested in the functor category Prof^{I}.

Our first construction is an object of names N, the functor N : I → Prof given by the composition I ⊆ Set → Cat → Prof , an inclusion followed by two embeddings. This takes a set s ∈ I to the corresponding discrete category, which we write also as s.

Several Prof operations can be extended pointwise to Prof^{I}: lifting (−)_{⊥}, the involution (−)^{op}, tensor ‘⊗’, which is the same as par ‘�’, and product ‘&’, which is the same as coproduct ‘+’.

We do not know whether or not Prof^{I} is monoidal closed with respect to ⊗. There is however, a Yoneda lemma expressing an isomorphism

Â(s) ≅ Prof^{I}(I(s, −), A)

for s in I and A in Prof^{I}. Thus given objects A, B ∈ Prof^{I} there is always a candidate for the function space

“{ \atop (A → B)(s)}” ≅ Prof^{I}(I(s, −) ⊗ A, B) ,

but this is only meaningful if we can exhibit it as an actual presheaf. Conveniently, for the purposes of the π-calculus it is enough to take function spaces N → A and it happens that these do exist. On objects they turn out to be given by

(N → A)(s) = s × A(s) + A(s + 1) .  (1)

A presheaf over this comprises a pair ⟨F, Y ⟩, where F : s → A(s) is a profunctor arrow from the discrete category s, and Y ∈ { \atop A(s + 1)}.

Paths of (N → A)(s) can be seen, rather loosely, as elements of the graph of a function. Thus a path in the s × A(s)-component of (1) we write as (x↦p) for name x ∈ s and path p ∈ A(s). A path in the A(s+1)- component we write as (∗↦p′) for p′ ∈ A(s + 1). In a similar spirit we can inject a presheaf X ∈ Â(s) into the left x-component as (x↦X), and a presheaf Y ∈ { \atop A(s + 1)} into the right component as (∗↦Y).

Here we have used a convention that we shall follow throughout, that for any set of names s we write ‘∗’ for the extra element provided in s+1, subscripting ‘∗_{s}’ when necessary.

This said we can now describe the action of the profunctor (N→A)(i) when i : s → s′ is an arrow in I. On the component s × A(s)

(x ↦ p) ↦ (i(x) ↦ A(i)(p)) ,  (2)

while on A(s + 1)

(∗_{s} ↦ p′) ↦ ∑_{y∉Im(i)}(y ↦ A[i, y](p′)) + (∗_{s′} ↦ A(i + 1)(p′)) . (3)

Here [i, y] : s + 1 → s′ is the injection that extends i over s + 1 by taking ∗_{s} to y ∈ (s′ \Im(i)). Note how in this second equation the path (∗_{s}↦p′) serves as a ‘seed’ to set paths for all the fresh names of s′ not in the image of i.

To handle name creation we use a construction δ on Prof^{I}, defined by δA = A( + 1). This is in fact also a form of function space from N to A, arising from the construction of Day (1970) which lifts the disjoint union ‘+’ of I to a symmetric monoidal closed structure on Prof^{I}. Approximately speaking, δA comprises functions that will only accept a fresh name as argument. This allows processes to synchronize on the choice of a local name, as required by the (CLOSE) rule of Figure 1. Stark (1996) expands on this a little.

2 The Equation

We derive a suitable π-calculus path object P in Prof^{I} from the following equations:

P ≅ P_{⊥} + Out + In
Out = (N ⊗ N ⊗ P_{⊥}) + (N ⊗ (δP)_{⊥})  (4)
In = N ⊗ (N → P)_{⊥}  (5)

Unfolding, the four components of P represent silent action, free output, bound output and input respectively. We give the solution to this equation in two stages: first we describe recursively at each set s the corresponding path category P(s); and then we specify the profunctor arrow that connnects P(s) to P(s′) for any injective function i : s → s′.

From the descriptions of the constructors δ and →, we can think of the family P(−) as being recursively described by

P(s) = P(s)_{⊥} + s × s × P(s)_{⊥} + s × P(s + 1)_{⊥} + s × (s × P(s) + P(s + 1))_{⊥} .

Our minimal P(s) is thus a poset, in fact a forest of trees. We have four kinds of root: τ., x!y., x!∗. and x? for any x, y ∈ s. Above these in the order relation we find respectively: τ.p, x!y.p, x!∗.p′, x?(y↦p) and x?(∗↦p′), where the last two lie above x? and where p is an object of P(s) while p′ is an object of P(s + 1). The arrows of P(s) are the prefix order, with for example

x?(y↦p) ≤ x?(y↦p̄) iff p ≤ p̄ in P(s)
x?(∗↦p′) ≤ x?(∗↦p̄′) iff p′ ≤ p̄′ in P(s + 1).

Definition 5. We have already used for the objects of P(s) a notation suggesting the sequence of “atomic” actions that a path represents. In order to describe the arrow part of the functor P, and later on for the semantics of processes, we now give presheaf analogues of the evident prefix operations on paths.

• For α one of τ or x!y we have a prefixing functor α : P(s)_{⊥} → P(s). This gives an operation on presheaves α. = α_{!} ∘ l_{⋆} : P̂(s) → P̂(s) with

α.X(p) = \begin{cases}\{⋆\} & if p = α. \\ X(p′) & if p = α.p′ \\ ∅ & otherwise. \end{cases}

Similarly with Y ∈ { \atop P(s + 1)} we apply (x!∗)_{!} ∘ l_{⋆} in order to obtain x!∗.Y ∈ P̂(s).

• Given X ∈ P̂(s) and x, y ∈ s we define x?(y↦X) ∈ P̂(s) by

x?(y ↦ X) (p) = \begin{cases}\{⋆\} & if p = x? \\ X(p′) & if p = x?(y↦p′) \\ ∅ & otherwise. \end{cases}

Again we could also have obtained this from a path map (x?(y↦ )).

• Suppose that ⟨F, Y ⟩ is a presheaf over (N → P)(s), i.e. a profunctor F : s → P(s) and a presheaf Y ∈ { \atop P(s + 1)}. We define

x?⟨F, X⟩(p) = \begin{cases}\{⋆\} & if p = x? \\ F (y)(p′) & if p = x?(y↦p′) \\ Y (p′) & if p = x?(∗↦p′) \\ ∅ & otherwise. \end{cases}

Once again we could instead have derived this from the operations on paths taking ⟨y, p⟩ ∈ s × P(s) to x?(y↦p) and p′ ∈ P(s + 1) to x?(∗↦p′).

Lemma 1 and Proposition 3 are sufficient to show that all these functors preserve surjective open maps.

Moving on to the morphism part of P, we need a profunctor P(i) : P(s) → P(s′) for every injection i : s → s′. We work by induction on the structure of paths in P(s). In the base cases minimal paths in P(s) go to the same in P(s′), regarded via Yoneda as presheaves:

P(i)(τ.) = τ.  P(i)(x!y.) = i(x)!i(y).
P(i)(x!∗_{s}.) = i(x)!∗_{s′}.  P(i)(x?) = i(x)?

The inductive steps are:

P(i)(τ.p) = τ.P(i)(p)  P(i)(x!∗_{s}.p′) = i(x)!∗_{s′}.P(i + 1)(p′)
P(i)(x!y.p) = i(x)!i(y).P(i)(p) P(i)(x?(y ↦ p)) = i(x)?(i(y) ↦ P(i)(p))
P(i)(x?(∗ ↦ p′)) = i(x)?(N → P)(i)(p′) .

In the last of these we use the non-trivial action of (N → P)(i) from (3) to ‘fill in’ input behaviour on receiving names from (s′ \ Im(i)).

2.1 A Decomposition Result

We will now observe that every presheaf X ∈ P̂(s) decomposes into a sum of disjoint components rooted at one of the minimal path objects τ., x!y., x!∗., x? where x, y ∈ s. The decomposition not only allows us to read off a normal form for presheaves, but also leads to a natural notion of transitions for presheaves.

Let m be a minimal object in P(s) and X ∈ P̂(s). Any x ∈ X(m) determines a sub-presheaf C of X as follows:

C(p) = \begin{cases}\{ y ∈ X(p) | X(m, p)(y) = x \} & if m ≤ p \\ ∅ & otherwise \end{cases}

for p ∈ P(s), and when p ≤ q define the function C(p, q) : C(q) → C(p) by

C(p, q)(z) = X(p, q)(z) for z ∈ C(q)

— because X is a contravariant functor it follows that

X(m, p)(X(p, q)(z)) = X(m, q)(z) = x

so that X(p, q)(z) ∈ C(p). It is easily checked that C 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 6. In this situation, we shall say that C is a rooted component of X at x.

Rooted components of X are pairwise disjoint in the sense that if m, m′ are minimal objects of P(s) and C is a rooted component at x ∈ X(m) and C′ is a rooted component at x′ ∈ C(m′), then if C(p) ∩ C′(p) ≠ ∅ for any p ∈ P(s), then m = m′ and x = x′. Thus, X is isomorphic to a sum of its rooted components:

X ≅ ∑_{m} ∑_{x∈X(m)} C_{x}  (6)

where m ranges over minimal objects of P(s) and C_{x} is the rooted component of X at x.

We analyse further the form of rooted components of X ∈ P̂(s). A rooted component C_{i} at i ∈ X(τ.) is isomorphic to τ.X_{i} where X_{i} ∈ P̂(s) is given by

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

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_{j} at j ∈ X(x!y.), for x, y ∈ s, is isomorphic to x!y.X_{j}, where X_{j} ∈ P̂(s) is given by

X_{j}(p) = C_{j}(x!y.p), on objects p ∈ P(s), and
X_{j}(p, q) = C_{j}(x!y.p, x!y.q), on morphisms p ≤ q of P(s).

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

{X′ | X ⟶^{x!y} X′}.

A rooted component C_{k} at k ∈ X(x!∗.), for x ∈ s, is isomorphic to x!∗.X_{k}, where X_{k} ∈ { \atop P(s + 1)} is given by

X_{k}(p′) = C_{k}(x!∗.p′), on objects p′ ∈ P(s + 1), and
X_{k}(p′, q′) = C_{k}(x!∗.p′, x!∗.q′), on morphisms p′ ≤ q′ of P(s + 1).

We write X ⟶^{x!∗} X′ when there is k ∈ X(x!∗.) such that X′ = X_{k}. The assignment k ↦ X_{k} is a bijection between the sets X(x!∗.) and

{X′ | X ⟶^{x!∗} X′}.

Let C_{l} be a rooted component at L ∈ X(x?). Define for any y ∈ s, X_{l}^{y} ∈ P̂(s) as

\begin{aligned}X_{l}^{y}(p) & = C_{l}(x?(y ↦ p)), and \\ X_{l}^{y}(p, q) & = C_{l}(x?(y ↦ p), x?(y ↦ q)) : X_{l}^{y}(q) → X_{l}^{y}(p). \end{aligned}

Define also X_{l}^{∗} ∈ { \atop P(s + 1)} as

\begin{aligned}X_{l}^{∗}(p′) & = C_{l}(x?(∗ ↦ p′)), and \\ X_{l}^{∗}(p′, q′) & = C_{l}(x?(∗ ↦ p′), x?(∗ ↦ q′)) : X_{l}^{∗}(q′) → X_{l}^{∗}(p′). \end{aligned}

Then X_{l} can be regarded as a pair ⟨λy.X_{l}^{y}, X_{l}^{∗}⟩ with λy.X_{l}^{y} : s → P(s). We write X ⟶^{x?} ⟨F, Y ⟩ when there is l ∈ X(x?) such that F (y) is isomorphic to X_{l}^{y} for every y ∈ s and Y is isomorphic to X_{l}^{∗}. The assignment l ↦ ⟨λy.X_{l}^{y}, X_{l}^{∗}⟩ is a bijection between the sets X(x?) and

{⟨F, Y ⟩ | X ⟶^{x?} ⟨F, Y ⟩}.

This analysis of rooted components transforms (6) into the following result.

Theorem 7 (Decomposition of Presheaves). Let X ∈ P̂(s). Then

X ≅ ∑_{i∈X(τ.)} τ.X_{i} + ∑_{x,y∈s} ∑_{j∈X(x!y.)} x!y.X_{j} + ∑_{x∈s} ∑_{k∈X(x!∗.)} x!∗.X_{k}

+ ∑_{x∈s} ∑_{l∈X(x?)} x?⟨λy.X_{l}^{y}, X_{l}^{∗}⟩ .

This gives a similar decomposition of morphisms, which preserves surjective opens. Proposition 8. Let X, Y be two presheaves over P(s) with f : X → Y a surjective open map beween them. Then the following “restrictions” of f are surjective open:

f_{i} : X_{i} → Y_{i′} where i ∈ X(τ.) and i′ = f_{τ.}(i)
f_{j} : X_{j} → Y_{j′} where j ∈ X(x!y.) and j′ = f_{x!y.}(j)
f_{k} : X_{k} → Y_{k′} where k ∈ X(x!∗.) and k′ = f_{x!∗.}(k)
f_{l}^{y} : X_{l}^{y} → Y_{l′}^{y} where l ∈ X(x?) and l′ = f_{x?}(l)
f_{l}^{∗} : X_{l}^{∗} → Y_{l′}^{∗} where l ∈ X(x?) and l′ = f_{x?}(l).

2.2 Indexed Late Bisimilarity for P

The previous section gave a notion of transitions on presheaves; naturally enough, this leads to a form of bisimilarity. Definition 9. A P-late bisimulation is a family (R_{s})_{s∈I} of symmetric binary relations on presheaves in P̂(s) such that for any finite name set s and any two presheaves X, Y over P(s), if X R_{s} Y then

X ⟶^{τ} X′ ⇒ ∃Y′. Y ⟶^{τ} Y′ & X′ R_{s} Y′
X ⟶^{x!y} X′ ⇒ ∃Y′. Y ⟶^{x!y} Y′ & X′ R_{s} Y′
X ⟶^{x!∗} X′ ⇒ ∃Y′. Y ⟶^{x!∗} Y′ & X′ R_{s+1} Y′
X ⟶^{x?} ⟨F, X′⟩ ⇒ ∃⟨G, Y′⟩. Y ⟶^{x?} ⟨G, Y′⟩ \begin{matrix}& X′ R_{s+1} Y′ \\ & ∀y ∈ s. F (y) R_{s} G(y) . \end{matrix}

We say that X, Y ∈ P̂(s) are P-late bisimilar iff X R_{s} Y for some P-late bisimulation (R_{s})_{s∈I}. Lemma 10. P-late bisimilarity is an equivalence relation. Using Proposition 8 we can show that this P-late bisimilarity corresponds exactly to open map bisimilarity:

Lemma 11. Suppose X and Y are presheaves over P(s). Then:

(i) If f : X → Y is a surjective open map then X and Y are P-late bisimilar.

(ii) If X R_{s} Y for some P-late bisimulation (R_{s})_{s∈I} then X and Y are

related by a span of surjective open maps. Combining these gives: Proposition 12. Two presheaves X and Y over P(s) are P-late bisimilar if and only if they are connected by a span of surjective open maps. Moving to a larger set of free names does not affect P-late bisimilarity.

Proposition 13 (Weakening). If X, Y ∈ P̂(s) are P-late bisimilar then so are P(i)_{!}(X) and P(i)_{!}(Y) for any injection i : s → s′. Moving to smaller name sets is a little more complicated. For any i : s → s′ in I define e_{i} : P(s) → P(s′) by induction as follows (omitting the trivial base cases):

e_{i}(τ.p) = τ.e_{i}(p)  e_{i}(x!y.p) = i(x)!i(y).e_{i}(p)
e_{i}(x!∗_{s}.p) = i(x)!∗_{s′}.e_{i+1}(p) e_{i}(x?(y ↦ p)) = i(x)?(i(y) ↦ e_{i}(p))
e_{i}(x?(∗_{s} ↦ p′)) = i(x)?(∗_{s′} ↦ e_{i+1}(p)) .

This differs from P(i) in having a much simpler action on input of unknowns x?(∗↦p′). Even so e_{i}^{⋆}, which by Proposition 1 preserves open maps, turns out to be a left inverse to P(i)_{!}. This allows us to prove the following result.

Proposition 14 (Strengthening). For X, Y ∈ P̂(s) and i : s → s′ in I, if P(i)_{!}(X) and P(i)_{!}(Y) are P-late bisimilar over P(s′) then so are X and Y over P(s). These results suggest that we could have imposed similar uniformity constraints on the family (R_{s})_{s∈I} in Definition 9: we conjecture that without loss of generality we can require that R ↣ (P&P) be a cartesian subobject in Prof^{I}.

3 Constructions

3.1 A Restriction Operator

We define here the operator that will be used to interpret name restriction in π-calculus processes. It arises as a natural family of profunctor arrows indexed by finite sets s and their elements:

ν_{y∈s} : P(s) ⟶ P(s − {y}) .

Naturality means that for any injective function i : s → s′, the following square commutes:

P(s)  ^{+}^{ν_{y∈s}}_{+}_{P(i)}  P(s − {y})_{+}_{P(i′)} P(s′)  _{+}_{ν_{i(y)∈s′}} P(s′ − {i(y)})

where i′ : (s − {y}) → (s′ − {i(y)}) is the restriction of i. In particular we can observe that the family (ν_{∗∈s+1})_{s} define a natural transformation

ν : δ(P) →^{.} P.

We define the ν_{y∈s} simultaneously for all s by induction on the structure of the paths. So for each path in P(s), according to its structure:

ν_{y∈s}(τ.p) = τ.ν_{y∈s}(p)

ν_{y∈s}(x!z.p) = \begin{cases}x!z.ν_{y∈s}(p) & if x, z ≠ y \\ x!∗_{s−\{y\}}.P(b_{s,y})(p) & if x ≠ y and z = y \\ ∅ & otherwise \end{cases}

ν_{y∈s}(x!∗_{s}.p′) = \begin{cases}x!∗_{s−\{y\}}.ν_{y∈s+1}(p′) & if x ≠ y \\ ∅ & otherwise \end{cases}

ν_{y∈s}(x?(z ↦ p)) = \begin{cases}x?(z ↦ ν_{y∈s}(p)) & if x, z ≠ y \\ ∅ & otherwise \end{cases}

ν_{y∈s}(x?(∗_{s} ↦ p′) = \begin{cases}x?(∗_{s−\{y\}} ↦ ν_{y∈s+1}(p′)) & if x ≠ y \\ ∅ & otherwise \end{cases}

where b_{s,y} : s → (s − {y}) ∪ {∗_{s−{y}}} is the bijection that renames y to ∗_{s−{y}}. The base cases are the evident instances of these for null p: for example ν_{y∈s}(τ.) = τ. .

The only complication in this definition is the clauses that ensure restriction correctly turns free output into bound output, as summarised in this result:

Lemma 15. Let X be a presheaf over P(s) and let x, y ∈ s. If X ⟶^{x!y} X′,

then ν_{y∈s,!}(X) ⟶^{x!∗_{s−{y}}} P(b_{s,y})_{!}(X′).

Observe that if y, z are two different elements of a set s, then

ν_{z∈s−{y}} ∘ ν_{y∈s} = ν_{y∈s−{z}} ∘ ν_{z∈s}.

This suggests a definition of ν as a contravariant functor from I to Prof with ν(s) = P(s) and ν(i) : P(s′) → P(s) the restriction, in any order, of the elements of (s′ \ Im(i)).

3.2 Parallel Composition

We give an inductive definition for parallel composition of presheaves over P(s) based on the decomposition result of Section 2.1. We then outline how the same definition arises from an interleaving operation on paths, and so deduce that surjective open maps are preserved. Definition 16. Let X and Y be two presheaves over P(s) with the respective decompositions indexed by i, j, k, l and i′, j′, k′, l′. Define X∥_{s}Y inductively as follows:

∑_{i∈I} τ.(X_{i}∥_{s}Y) + ∑_{x,y∈s} ∑_{j∈J_{x!y}} x!y.(X_{j}∥_{s}Y) + ∑_{x∈s} ∑_{k∈K_{x}} x!∗_{s}.(X_{k}∥_{s+1}P(i)_{!}(Y))

+ ∑_{x∈s} ∑_{l∈L_{x}} x?⟨λy.(X_{l}^{y}∥_{s}Y), X_{l}^{∗}∥_{s+1}P(i)_{!}(Y)⟩

+ ∑_{i′∈I′} τ.(X∥_{s}Y_{i′}) + ∑_{x,y∈s} ∑_{j′∈J′_{x!y}} x!y.(X∥_{s}Y_{j′}) + ∑_{x∈s} ∑_{k′∈K′_{x}} x!∗_{s}.(P(i)_{!}(X)∥_{s+1}Y_{k′})

+ ∑_{x∈s} ∑_{l′∈L′_{x}} x?⟨λy.(X∥_{s}Y_{l′}^{y}), P(i)_{!}(X)∥_{s+1}Y_{l′}^{∗}⟩

\begin{matrix}+ ∑_{x,y∈s} ∑_{j∈J_{x!y}} ∑_{l′∈L′_{x}} τ.(X_{j}∥_{s}Y_{l′}^{y}) & + ∑_{x∈s} ∑_{k∈K_{x}} ∑_{l′∈L′_{x}} τ.ν_{∗∈s+1,!}(X_{k}∥_{s+1}Y_{l′}^{∗}) \\ + ∑_{x,y∈s} ∑_{j′∈J′_{x!y}} ∑_{l∈L_{x}} τ.(X_{l}^{y}∥_{s}Y_{j′}) & + ∑_{x∈s} ∑_{k′∈K′_{x}} ∑_{l∈L_{x}} τ.ν_{∗∈s+1,!}(X_{l}^{∗}∥_{s+1}Y_{k′}) , \end{matrix}

where i : s → s + 1 is the obvious inclusion function.

Much as with the prefixing operations of Definition 5, a more systematic approach begins with the profunctor arrow

∥_{s,⊥} : P(s)_{⊥} ⊗ P(s)_{⊥} ⟶ P(s)_{⊥}

that interleaves pairs of paths. Judicious use of Kan extension and the lifting maps of Proposition 3 give the parallel composition of presheaves as a bifunctor

∥_{s} : P̂(s) × P̂(s) ⟶ P̂(s)

with the following preservation property:

Proposition 17. Let X, Y, Z, W be presheaves over P(s). If maps f : X → Z and g : Y → W are surjective open, then so is f∥_{s}g : X∥_{s}Y → Z∥_{s}W.

3.3 Replication

In the same way that the operational semantics of π-calculus replication vanishes into structural congruence, its presheaf interpretation is built entirely from arrows already at hand. Given any small category P, define the “replicated” category P^{∞} by solving the following recursive equation^{4}

P^{∞} = 1 & (P ⊗ P^{∞}).

This P^{∞} is easily calculated to be equivalent to ∑_{n∈ω} P^{n}, where P^{0} = 1 and P^{n+1} = P ⊗ P ⋯ ⊗ P, (n + 1) times. Taking now the diagonal and parallel composition maps at P(s) we can inductively define replicated versions

d_{s}^{∞} : P̂(s) → { \atop P^{∞}(s)} and ∥_{s}^{∞} : { \atop P^{∞}(s)} → P̂(s).

Replication itself is simply their composition !_{s} = ∥_{s}^{∞} ∘ d_{s}^{∞}, and the inductive definition ensures that for any presheaf X over P(s):

!_{s}(X) = X ∥_{s}!_{s}(X).

4 The Interpretation

4.1 Semantics

Following (Stark 1996), we give the interpretation to process terms in two steps. First we associate a process P with free names in s to a presheaf ([P])_{s} ∈ |P̂(s)|. Then later, in the full interpretation, we take account of all possible name substitutions by giving a process P with free names s a denotation as a natural transformation:

[[P]] : N^{|s|} ⟶^{.} P .

4Note the relationship beween the way P^{∞} is defined and the way the linear logic !

can be defined in presence of infinite products.

Let s be a set of names. For π-calculus processes whose free names lie in s we inductively define:

([0])_{s} = ∅  ([P + Q])_{s} = ([P])_{s} + ([Q])_{s}
([x̄y.P])_{s} = x!y.([P])_{s}  ([P | Q])_{s} = ([P])_{s}∥_{s}([Q])_{s}
([!P])_{s} = !_{s}(([P])_{s})  ([ νx P])_{s} = ν_{x∈s+{x}}(([P])_{s+{x}}
([[x = x]P])_{s} = ([P])_{s}  ([[x = y]P])_{s} = ∅ if (x ≠ y)

([x(y).P])_{s} = x?⟨F, Y ⟩ where F (z) = ([P [z/y]])_{s} for any z ∈ s, and Y = ([P [∗_{s}/y]])_{s+1}.

Lemma 18. Let i : s → s′ be an injective function between finite sets, with x = ⟨x_{1}, x_{2}, …, x_{|s|}⟩ the names in s. Then for any process P using these names,

P(i)_{!}(([P])_{s}) ≅ ([P [i(x)/x]])_{s′} .

The free names of a process may be bound differently in different contexts. To cope with this, we interpret a process P with |s| free names as a natural transformation [[P]] : N^{|s|} ⟶^{.} P, where

[[P]]_{s′} : \overbrace{s′ × s′ ⋯ × s′}^{|s|−times} ⟶ P(s′) ⟨a_{1}, a_{2}, …, a_{|s|}⟩ ⟼ ([P [a/x]])_{s′}

Thus the denotation of a process with free names s carries an environment N^{|s|} as a parameter. The proof that this is indeed a natural transformation depends on Lemma 18, that the ([−])-interpretation respects name substitution.

4.2 Full Abstraction

We can now show our major result, that bisimulation between processes in the π-calculus coincides with that obtained in the model via open maps.

The first two propositions establish a bisimulation between a process P with free names in s and its denotation ([P])_{s}. Proposition 19. Let P be a process whose free names lie in s. Then

• P ⟶^{x̄y} Q implies ([P])_{s} ⟶^{x!y} X with X ≅ ([Q])_{s}

• P ⟶^{x̄(y)} Q implies ([P])_{s} ⟶^{x!∗_{s}} X with X([Q[∗_{s}/y]])_{s+1}

• P ⟶^{x(y)} Q implies ([P])_{s} ⟶^{x?} ⟨F, Y ⟩ with F (z) ≅ ([Q[z/y]])_{s} and

Y ≅ ([Q[∗_{s}/y]])_{s+1}

• P ⟶^{τ} Q implies ([P])_{s} ⟶^{τ} X with X([Q])_{s}

Proposition 20. Let P be a process whose free names lie in s. Then

• ([P])_{s} ⟶^{x!y} X implies ∃Q with P ⟶^{x̄y} Q and ([Q])_{s} ≅ X

• ([P])_{s} ⟶^{x!∗_{s}} X implies ∃Q, y with P ⟶^{x̄(y)} Q and ([Q[∗_{s}/y]])_{s+1} ≅ X

• ([P])_{s} ⟶^{x?} ⟨F, Y ⟩ implies ∃Q, y with P ⟶^{x(y)} Q and

([Q[∗_{s}/y]])_{s+1} ≅ Y and F (z) ≅ ([Q[z/y]])_{s}

• ([P])_{s} ⟶^{τ} X implies ∃Q with P ⟶^{τ} Q and ([Q])_{s} ≅ X.

Using these results and Proposition 12 we can deduce the following.

Theorem 21. Let P and Q be two π-calculus processes with free names in s. Then P is late bisimilar to Q if and only if ([P])_{s} and ([Q])_{s} are connected by a span of surjective open maps.

Suppose now that P is a π-calculus process with free names s_{P}. Then for any larger set of names s, an injection i : s_{P} → s induces a natural transformation π^{s_{P} ,i} : N^{|s|} →^{.} N^{|s_{P} |} that projects |s|-tuples of names to |s_{P} |-tuples. When i is simply an inclusion and no confusion arises we write this as π^{s_{P}}.

Theorem 22. Let P and Q be two π-calculus processes with free names s_{P} and s_{Q} respectively. Take s_{P,Q} to be the union s_{P} ∪ s_{Q}. Then P is late equivalent (bisimulation congruent) to Q if and only if for any finite set s and any |s_{P,Q}|-tuple a of elements of s, [[P]]_{s}π_{s}^{s_{P}} (a) and [[Q]]_{s}π_{s}^{s_{Q}}(a) are connected by a span of surjective open maps.

Note that it is sufficient here to take s to be exactly the free names s_{P,Q} of the two processes. We can also present this result using the 2-categorical setting of our model:

Corollary 23. Let P and Q be two π-calculus processes with free names s_{P} and s_{Q} respectively. Then P is late equivalent to Q if and only if [[P]] ∘ π^{s_{P}} and [[Q]] ∘ π^{s_{Q}} are connected by a span of modifications whose components are surjective open maps.

These results show a precise correspondence between operational and denotational notions of process equivalence; notice though that we do not interpret equivalent process by equal elements in the model. This could be arranged, by quotienting the categories P̂(s) to make every open map invertible, but there seems little reason to do so. In particular this is not likely to be very well-behaved as open maps do not form a calculus of fractions.

5 Other Results and Future Work

The model we have described is just one drawn from a spectrum of namepassing process calculi that can be described within Prof^{I}. We outline some possibilities below.

5.1 Late vs. Early

We have given the π-calculus here in its late version, where a process x(y).P carries out input in two stages: it first synchronizes with another process that is prepared to send on channel x; then, later, the transmitted value is substituted for y in the body of P. There is an alternative early semantics where these two steps happen together and processes synchronize on (channel,value) pairs. The operational consequences of this choice are discussed in (Milner et al. 1992b, §2.3). There is a corresponding early bisimulation ‘ ˙∼_{E}’ and early equivalence ‘∼_{E}’, which are both strictly coarser than their late forms.

We can follow these late and early alternatives in our denotational semantics. In presheaf models, synchronization points are marked by lifting (−)_{⊥} in the equation for the path category. An early version of (5) would be

In_{E} = N ⊗ (N → P_{⊥})  (7)

where instead of paths x?, x?(y↦p) and x?(∗↦p′) we now have x?y, x?∗, x?y.p and x?∗.p′. Solving this new equation in Prof gives an object P_{E}, and we conjecture that this provides a fully abstract model for the early π-calculus, for suitably adjusted interpretation functions ([−])^{E} and [[−]]^{E}.

More directly, this early model seems to arise as a collapse of the late one. A recursively defined morphism of path categories, k : P_{E} → P, induces an arrow in Prof^{I}

k^{⋆} : P ⟶ P_{E}  (8)

which we conjecture maps the late semantics for processes into the early one:

k^{⋆}(([P])_{s}) = ([P])_{s}^{E} ∈ P_{E}(s)  k^{⋆} ∘ [[P]]_{s} = [[P]]_{s}^{E} : N^{s} → P_{E}

for any process P with free names in s.

We can even move the synchronization point for output: clause (4) has a later variant

Out_{L} = N ⊗ (N ⊗ P)_{⊥} .  (9)

It turns out that this makes no difference to process bisimilarity, but it does correspond closely to the presentation style of (Milner 1991). There processes synchronize on channel names alone, P ⟶^{x̄} C or P ⟶^{x} F, becoming concretions C (name-process pairs, N ⊗ P) and abstractions F (name-to-process functions, N → P) respectively. Actual communication is represented by the application of abstractions to concretions F • C .

The domain models of the π-calculus in (Fiore et al. 1996; Stark 1996) do not cover the early version, chiefly because rearrangements like equation (7) are harder to express. There the domain equation for processes uses the Plotkin powerdomain to mark synchronization; while our equation for paths uses the much simpler lifting operation.

5.2 Other π-calculi

The development of our model has been purely denotational, with no operational manipulation of processes through expansion laws or the like. As a consequence, there are no required operators in the language, and the model remains valid for any subset of the π-calculus. Even so, particular sublanguages may fit simpler equations. For example, the asynchronous π-calculus of Boudol (1992) constrains output to the form x̄y.0, suggesting the clause

Out_{A} = N ⊗ N  (10)

to replace (4). The πI-calculus of Sangiorgi (1995) allows only bound output x̄(y).P, equivalence to νy(x̄y.P) in the original π-calculus. Every communication now passes a fresh name, and we would replace (5) and (4) with

In_{I} = Out_{I} = N ⊗ δP .  (11)

Moreover the morphism P(i) now arises from the category map e_{i} introduced just before Proposition 14, with the restrictions ν(i) from the end of Section 3.1 being e_{i}^{⋆}, the left inverse, and now also right adjoint, to P(i)_{!}. This gives some support to Sangiorgi’s claim that the πI-calculus is a simpler, more symmetric version of the π-calculus.

These examples show the flexibility of our approach by drawing on the rich categorical structure of Prof^{I}. As ever in category theory, this also leads us to look at the maps between models: we hope to find further morphisms like (8), from ‘late’ to ‘early’, that might tie together the wide selection of customized π-calculi proposed in recent years.

More speculatively, while we do not have a general function space in Prof^{I}, where it does exist we are no longer be constrained to passing just names or other ground values. Process-passing systems like CHOCS (Thomsen 1993) or even the full higher-order π-calculus of Sangiorgi (1992) could then fit into our framework. The difficulties here lie not just in writing plausible equations, but also in extracting their operational content to see if the semantics and bisimilarities that arise fit any existing scheme.

References

Francis Borceux. Handbook of Categorical Algebra, vol. 1, volume 50 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994.

Gérard Boudol. Asynchrony and the π-calculus. Rapport de recherche 1702, INRIA, Sophia Antipolis, 1992.

Gian Luca Cattani and Glynn Winskel. Presheaf models for concurrency. In Computer Science Logic 1996, Lecture Notes in Computer Science 1258, pages 58–75. Springer-Verlag, 1997. A preliminary version appeared as BRICS Report RS-96-35.

Brian J. Day. On closed categories of functors. In Reports of the Midwest Category Seminar IV, Lecture Notes in Mathematics 137, pages 1–38. Springer-Verlag, 1970.

Marcelo Fiore, Eugenio Moggi, and Davide Sangiorgi. A fully-abstract model for the π-calculus. In (LICS 1996).

Matthew Hennessy. A fully abstract denotational semantics for the πcalculus. Technical Report 96:04, School of Cognitive and Computing Sciences, University of Sussex, 1996.

Matthew Hennessy and Gordon Plotkin. Full abstraction for a simple parallel programming language. In Mathematical Foundations of Computer Science: Proceedings of the 8th International Symposium, Lecture Notes in Computer Science 74, pages 108–120. Springer-Verlag, 1979.

André Joyal and Ieke Moerdijk. A completeness theorem for open maps. Annals of Pure and Applied Logic, 70:51–86, 1994.

André Joyal and Ieke Moerdijk. Algebraic Set Theory, volume 220 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1995.

André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Information and Computation, 127(2):164–185, 1996.

LICS 1996. Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 27–30, 1996. IEEE Computer Society Press, 1996.

Robin Milner. The polyadic π-calculus — a tutorial. Technical Report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, University of Edinburgh, 1991.

Robin Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2):119–141, 1992.

Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, part I. Information and Computation, 100:1–40, 1992a.

Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, part II. Information and Computation, 100:41–77, 1992b.

Davide Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD Thesis CST-99-93, Department of Computer Science, University of Edinburgh, 1992.

Davide Sangiorgi. π-calculus, internal mobility, and agent-passing calculi. Rapport de recherche 2539, INRIA, Sophia Antipolis, 1995.

Ian Stark. A fully abstract domain model for the π-calculus. In (LICS 1996), pages 36–42.

Bent Thomsen. Plain CHOCS. Acta Informatica, 30:1–59, 1993.

Glynn Winskel. A presheaf semantics of value-passing processes. In CON-CUR ’96: Proceedings of the 7th International Conference on Concurrency Theory, Lecture Notes in Computer Science 1119, pages 98–114. Springer-Verlag, 1996. An extended version appears as BRICS Report RS-96-44.

Glynn Winskel and Mogens Nielsen. Models for concurrency. In Handbook of Logic in Computer Science, volume IV. Oxford University Press, 1995.

Recent BRICS Report Series Publications

RS-97-34 Gian Luca Cattani, Ian Stark, and Glynn Winskel. Presheaf Models for the π-Calculus. December 1997. ii+27 pp. Appears in Moggi and Rosolini, editors, Category Theory and Computer Science: 7th International Conference, CTCS ’97 Proceedings, LNCS 1290, 1997, pages 106–126.

RS-97-33 Anders Kock and Gonzalo E. Reyes. A Note on Frame Distributions. December 1997. 15 pp.

RS-97-32 Thore Husfeldt and Theis Rauhe. Hardness Results for Dynamic Problems by Extensions of Fredman and Saks’ Chronogram Method. November 1997. i+13 pp.

RS-97-31 Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund. Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal. November 1997. 23 pp. To appear in The 18th IEEE Real-Time Systems Symposium, RTSS ’97 Proceedings.

RS-97-30 Ulrich Kohlenbach. Proof Theory and Computational Analysis. November 1997. 38 pp.

RS-97-29 Luca Aceto, Augusto Burgueño, and Kim G. Larsen. Model Checking via Reachability Testing for Timed Automata. November 1997. 29 pp.

RS-97-28 Ronald Cramer, Ivan B. Damgård, and Ueli Maurer. Span Programs and General Secure Multi-Party Computation. November 1997. 27 pp.

RS-97-27 Ronald Cramer and Ivan B. Damgård. Zero-Knowledge Proofs for Finite Field Arithmetic or: Can Zero-Knowledge be for Free? November 1997. 33 pp.

RS-97-26 Luca Aceto and Anna Ingólfsdóttir. A Characterization of Finitary Bisimulation. October 1997. 9 pp. To appear in Information Processing Letters.

RS-97-25 David A. Mix Barrington, Chi-Jen Lu, Peter Bro Miltersen, and Sven Skyum. Searching Constant Width Mazes Captures the AC^{0} Hierarchy. September 1997. 20 pp. To appear in STACS ’98: 15th Annual Symposium on Theoretical Aspects of Computer Science Proceedings, LNCS, 1998.