BRICS RS-02-49 Nygaard & Winskel: HOPLA—A Higher-Order Process Language BRICS

Basic Research in Computer Science

HOPLA—A Higher-Order Process Language

Mikkel Nygaard Glynn Winskel BRICS Report Series RS-02-49 ISSN 0909-0878 December 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Mikkel Nygaard & Glynn Winskel.

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/02/49/

HOPLA—A Higher-Order Process Language

Mikkel Nygaard  Glynn Winskel
BRICS^{∗}  Computer Laboratory
University of Aarhus University of Cambridge

Abstract

A small but powerful language for higher-order nondeterministic processes is introduced. Its roots in a linear domain theory for concurrency are sketched though for the most part it lends itself to a more operational account. The language can be viewed as an extension of the lambda calculus with a “prefixed sum”, in which types express the form of computation path of which a process is capable. Its operational semantics, bisimulation, congruence properties and expressive power are explored; in particular, it is shown how it can directly encode process languages such as CCS, CCS with process passing, and mobile ambients with public names.

1 Introduction

We present an economic yet expressive language for higher-order nondeterministic processes that we discovered recently in developing a domain theory for concurrent processes. The language can be given a straightforward operational semantics, and it is this more operational account we concentrate on in the paper.

The language is typed. The type of a process describes the possible (shapes of) computation paths (or runs) the process can perform. Computation paths may consist simply of sequences of actions but they may also represent the input-output behaviour of a process. A typing judgement

x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℚ

∗ Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

means that a process t yields computation paths in ℚ once processes with computation paths in ℙ_{1}, …, ℙ_{k} are assigned to the variables x_{1}, …, x_{k} respectively. The types ℙ are built using a “prefixed sum,” products, function spaces and recursive definition. It is notable that although we can express many kinds of concurrent processes in the language, the language itself does not have many features typical of process calculi built-in, beyond that of a nondeterministic sum and prefix operations.

In general, the language allows processes to be copied and discarded arbitrarily. In particular, the language will allow us to write terms which take a process as argument, copy it and then set those copies in parallel composition with each other. However some operations are by nature linear in certain arguments. Linearity, detected in the denotational semantics, translates into the property of preserving nondeterministic sums.

The operations associated with the prefix-sum type constructor are central to the expressiveness of the language. A prefix-sum type has the form Σ_{α∈A}α.ℙ_{α}; it describes computation paths in which first an action β ∈ A is performed before resuming as a computation path in ℙ_{β}. The association between an initial action β and ensuing type ℙ_{β} is deliberate; performing an action should lead to a unique type. The prefix sum is associated with prefix operations taking a process t of type ℙ_{β} to β.t of type Σ_{α∈A}α.ℙ_{α}, as well as a prefix match [u > β.x ⇒ t], where u has prefix-sum type, x has type ℙ_{β} and t generally involves the variable x. The term [u > β.x ⇒ t] matches u against the pattern β.x and passes the results of successful matches for x on to t. More precisely, prefix match is linear in the argument u so that the possibly multiple results of successful matches are nondeterministically summed together.

The language supports an operational semantics and bisimulation. It is expressive and, as examples, it is easy to translate CCS, a form of CCS with process passing, and mobile ambients with public names into the language. The translated languages inherit bisimulation. Linearity plays a role in deriving traditional expansion laws for the translations.

The reader may like to look ahead to the operational treatment of the language in Sects. 3–6 for a fuller description. These sections are essentially self-contained, with references to the account in Sect. 2 of the denotational semantics of the language, and how it arose from a process model of Girard’s linear logic, only to highlight the correspondence to the operational semantics.

2 Denotational semantics

2.1 Presheaf Models

Let ℙ be a small category. The category of presheaves over ℙ, written ℙ̂, is the category [ℙ^{op}, Set] with objects the functors from ℙ^{op} (the opposite category) to the category of sets and functions, and maps the natural transformations between them. In our applications, the category ℙ is thought of as consisting of computation-path shapes where a map e : p → q expresses how the path p is extended to the path q. A presheaf X ∈ ℙ̂ specifies for a typical path p the set X(p) of computation paths of shape p, and acts on e : p → q to give a function X(e) saying how paths of shape q restrict to paths of shape p. In this way a presheaf can model the nondeterministic branching of a process. For more information of presheaf models, see [14, 4].

A presheaf category has all colimits and so in particular all sums (coproducts); for any set I, the sum Σ_{i∈I}X_{i} of presheaves X_{i} over ℙ has a contribution Σ_{i∈I}X_{i}(p), the disjoint union of sets, at p ∈ ℙ. The empty sum is the presheaf ∅ with empty contribution at each p. In process terms, a sum of presheaves represents a nondeterministic sum of processes.

2.2 A Linear Category of Presheaf Models

Because the presheaf category ℙ̂ is characterised abstractly as the free colimit completion of ℙ we expect colimit-preserving functors to be useful. Define the category Lin to consist of small categories ℙ, ℚ, … with maps F : ℙ → ℚ the colimit-preserving functors F : ℙ̂ → ℚ̂. Lin can be understood as a categorical model of classical linear logic, with the involution of linear logic, ℙ^{⊥}, given by ℙ^{op}. The tensor product of ℙ and ℚ is given by the product of small categories, ℙ × ℚ, and the function space from ℙ to ℚ by ℙ^{op} × ℚ. On objects ℙ and ℚ, products (written ℙ & ℚ) and coproducts are both given by ℙ + ℚ, the sum of categories ℙ and ℚ; the empty category 𝕆 is a zero object. While rich in structure, Lin does not support all operations associated with process languages; since all maps are linear (i.e.. colimit-preserving), when applied to the inactive process ∅, the result will be ∅. So, in particular, a prefix operation cannot be interpreted as a map of Lin.

There are (at least) two reasonable responses to this: One is to move to a model of affine-linear logic where maps are allowed to ignore their arguments in giving non-trivial output. One such model is the category Aff, where maps are connected-colimit preserving functors. In [18] we used the category Aff to interpret an expressive affine-linear process language. Unfortunately, its operational semantics is proving difficult, and has not yet been extended to higher order.

This leads us to consider a second answer. Following the discipline of linear logic, suitable nonlinear maps are obtained as linear maps whose domain is under an exponential. As for the exponential ! of linear logic, there are many possible choices—see [18]. One is to interpret !ℙ as the finitecolimit completion of ℙ. With this understanding of !ℙ, it can be shown that ℙ̂ with the inclusion functor !ℙ → ℙ̂ is the free filtered colimit completion of !ℙ—see [15]. It follows that maps !ℙ → ℚ in Lin correspond, to within isomorphism, to continuous (i.e., filtered colimit preserving) functors ℙ̂ → ℚ̂.

2.3 A Cartesian Closed Category of Presheaf Models

Define Cts to be the category consisting of small categories ℙ, ℚ, … as objects and morphisms F : ℙ → ℚ the continuous functors F : ℙ̂ → ℚ̂; they compose as functors. Clearly Lin is a subcategory of Cts, one which shares the same objects. We have

Cts(ℙ, ℚ) ≃ Lin(!ℙ, ℚ)

for all small categories ℙ, ℚ. The category Cts is the coKleisli category of the comonad based on finite-colimit completions.^{1} The unit of the corresponding adjunction is given by maps copy : ℙ → !ℙ of Cts, used to interpret prefixing below. We can easily characterize those maps in Cts which are in Lin:

Proposition 2.1 Suppose F : ℙ̂ → ℚ̂ is a functor which preserves filtered colimits. Then, F preserves all colimits iff F preserves finite coproducts.

In other words a continuous map is linear iff it preserves sums.

There is an isomorphism

!(ℙ & ℚ) ≅ !ℙ ×!ℚ

making Cts cartesian closed; this immediately allows us to interpret the simply-typed lambda calculus with pairing in Cts. Products ℙ & ℚ in Cts are given as in Lin but now viewing the projections as continuous functors. The function space ℙ → ℚ is given by (!ℙ)^{op} × ℚ.

The category Cts does not have coproducts. However, we can build a useful sum in Cts with the help of the coproduct of Lin and !. Let (ℙ_{α})_{α∈A} be a family of small categories. Their prefixed sum,

Σ_{α∈A}α.ℙ_{α} ,

1We are glossing over 2-category subtleties as ! is really a pseudo functor.

is based on the coproduct in Lin given by Σ_{α∈A}!ℙ_{α} with corresponding injections in_{β} : !ℙ_{β} → Σ_{α∈A}α.ℙ_{α}, for β ∈ A. The injections

β.(−) : ℙ_{β} → Σ_{α∈A}α.ℙ_{α}

in Cts, for β ∈ A, are defined to be the compositions β.(−) = in_{β} ∘ copy. As the notation suggests, β.(−) is used to interpret prefixing with β.

The construction above satisfies a property analogous to the universal property of a coproduct. Suppose F_{α} : ℙ_{α} → ℚ are maps in Cts for all α ∈ A. Then, within Lin, we find a mediating map

F : Σ_{α∈A}α.ℙ_{α} → ℚ

determined to within isomorphism such that

F ∘ α.(−) ≅ F_{α}

for all α ∈ A. Since Lin is a subcategory of Cts, the mediating map F also belongs to Cts, but here it is not uniquely determined, not even up to isomorphism. Therefore, the prefixed sum is not a coproduct in Cts, but the linearity of the mediating map is just what we need for interpreting prefix match. Consider a prefix match term [u > β.x ⇒ t] where t denotes a map F_{β} : ℙ_{β} → ℚ. We interpret it as the mediating map obtained for F_{β} together with constantly ∅ maps F_{α} : ℙ_{α} → ℚ for α ∈ A different from β, applied to the denotation of u.

2.4 Rooted Presheaves and Operational Semantics

The category !ℙ has an initial element ⊥, given by the empty colimit, and a presheaf over !ℙ is called rooted if it has a singleton contribution at ⊥—see [14]. As an example, the denotation of β.t with t closed is rooted. We can decompose any presheaf X over !ℙ as a sum of rooted presheaves Σ_{i∈X(⊥)}X_{i}, each X_{i} a presheaf over !ℙ. This is the key to the correspondence between the denotational semantics and the operational semantics of Sect. 4. Judgements t ⟶^{β} t′, with t of prefix-sum type Σ_{α∈A}α.ℙ_{α} and β ∈ A, in the operational semantics will express that copy[[t′]] is a rooted component of [[t]] restricted to !ℙ_{β}. In fact, derivations of transitions t ⟶^{β} t′ will be in 1-1 correspondence with such components.

3 A Higher-Order Process Language

The types of the language are given by the grammar

ℙ, ℚ ::= Σ_{α∈A}α.ℙ_{α} | ℙ → ℚ | ℙ & ℚ | P | μ_{j}P⃗ .ℙ⃗ .

P is drawn from a set of type variables used in defining recursive types; μ_{j}P⃗ .ℙ⃗ abbreviates μ_{j}P_{1}, …, P_{k}.(ℙ_{1}, …, ℙ_{k}) and is interpreted as the j-component, for 1 ≤ j ≤ k, of the “least” solution (given by a suitable ω-colimit in the category of small categories and functors) to the defining equations P_{1} = ℙ_{1}, …, P_{k} = ℙ_{k}, in which the expressions ℙ_{1}, …, ℙ_{k} may contain the P_{j}’s. We shall write μP⃗ .ℙ⃗ as an abbreviation for the k-tuple with j-component μ_{j}P⃗ .ℙ⃗.

The constructions of Cts form the basis of a syntax of terms:

t, u ::= x | rec x.t | Σ_{i∈I}t_{i} | α.t | [u > α.x ⇒ t] | λx.t | t u | (t, u) | fst t | snd t

In a nondeterministic sum term, Σ_{i∈I}t_{i}, the indexing set I may be an arbitrary set; we write t_{1}+⋯ +t_{k} for a typical finite sum and ∅ when I is empty. The variable x in the match term [u > α.x ⇒ t] is a binding occurrence and so binds later occurrences of the variable in the body t. We shall take for granted an understanding of free and bound variables, and substitution on raw terms.

Let ℙ_{1}, …, ℙ_{k}, ℚ be closed type expressions and assume that the variables x_{1}, …, x_{k} are distinct. A syntactic judgement x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℚ can be interpreted as a map ℙ_{1} & ⋯ & ℙ_{k} → ℚ in Cts. We let Γ range over environment lists x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k}, which we may treat as finite maps from variables to closed type expressions. The term formation rules are:

\frac{Γ(x) = ℙ}{Γ ⊢ x : ℙ} \frac{Γ, x : ℙ ⊢ t : ℙ}{Γ ⊢ rec x.t : ℙ} \frac{Γ ⊢ t_{j} : ℙ all j ∈ I}{Γ ⊢ Σ_{i∈I}t_{i} : ℙ}

\frac{Γ ⊢ t : ℙ_{β} β ∈ A}{Γ ⊢ β.t : Σ_{α∈A}α.ℙ_{α}} \frac{Γ ⊢ u : Σ_{α∈A}α.ℙ_{α} Γ, x : ℙ_{β} ⊢ t : ℚ β ∈ A}{Γ ⊢ [u > β.x ⇒ t] : ℚ}

\frac{Γ, x : ℙ ⊢ t : ℚ}{Γ ⊢ λx.t : ℙ → ℚ} \frac{Γ ⊢ t : ℙ → ℚ Γ ⊢ u : ℙ}{Γ ⊢ t u : ℚ}

\frac{Γ ⊢ t : ℙ Γ ⊢ u : ℚ}{Γ ⊢ (t, u) : ℙ & ℚ} \frac{Γ ⊢ t : ℙ & ℚ}{Γ ⊢ fst t : ℙ} \frac{Γ ⊢ t : ℙ & ℚ}{Γ ⊢ snd t : ℚ}

\frac{Γ ⊢ t : ℙ_{j}[μP⃗ .ℙ⃗/P⃗]}{Γ ⊢ t : μ_{j}P⃗ .ℙ⃗} \frac{Γ ⊢ t : μ_{j}P⃗ .ℙ⃗}{Γ ⊢ t : ℙ_{j}[μP⃗ .ℙ⃗/P⃗]}

We have a syntactic substitution lemma:

Lemma 3.1 Suppose Γ, x : ℙ ⊢ t : ℚ and Γ ⊢ u : ℙ. Then Γ ⊢ t[u/x] : ℚ.

The semantic counterpart essentially says that the denotation of t[u/x] is the functorial composition of the denotations of t and u.

4 Operational Semantics

With actions given by the grammar

a ::= α | u ↦ a | (a, −) | (−, a) ,

the operational rules below define a transition semantics for closed, wellformed terms:

\frac{t[rec x.t/x] ⟶^{a} t′}{rec x.t ⟶^{a} t′} \frac{t_{j} ⟶^{a} t′}{Σ_{i∈I}t_{i} ⟶^{a} t′} j ∈ I

\overline{α.t ⟶^{α} t}  \frac{u ⟶^{α} u′ t[u′/x] ⟶^{a} t′}{[u > α.x ⇒ t] ⟶^{a} t′}

\frac{t[u/x] ⟶^{a} t′}{λx.t ⟶^{u↦a} t′}  \frac{t ⟶^{u↦a} t′}{t u ⟶^{a} t′}

\frac{t ⟶^{a} t′}{(t, u) ⟶^{(a,−)} t′}  \frac{u ⟶^{a} u′}{(t, u) ⟶^{(−,a)} u′}  \frac{t ⟶^{(a,−)} t′}{fst t ⟶^{a} t′}  \frac{t ⟶^{(−,a)} t′}{snd t ⟶^{a} t′}

In the rule for lambda-abstraction, we must have x : ℙ ⊢ t : ℚ and ⊢ u : ℙ for some ℙ, ℚ.

To show that the rules are type-correct, we assign types to actions a using a judgement of the form ℙ : a : ℙ′. Intuitively, after performing the action a, what remains of a computation path in ℙ is a computation path in ℙ′. For β ∈ A we take Σ_{α∈A}α.ℙ_{α} : β : ℙ_{β} and inductively

\frac{⊢ u : ℙ ℚ : a : ℙ′}{ℙ → ℚ : u ↦ a : ℙ′} \frac{ℙ : a : ℙ′}{ℙ & ℚ : (a, −) : ℙ′} \frac{ℙ_{j}[μP⃗ .ℙ⃗/P⃗] : a : ℙ′}{μ_{j}P⃗ .ℙ⃗ : a : ℙ′}

—with a symmetric rule for (−, a). Notice that in ℙ : a : ℙ′, the type ℙ′ is unique given ℙ and a.

Proposition 4.1 Suppose ⊢ t : ℙ. If t ⟶^{a} t′ then ℙ : a : ℙ′ and ⊢ t′ : ℙ′.

We interpret ℙ : a : ℙ′ as a map ℙ → !ℙ′ of Lin by letting the judgement for β above denote restriction to !ℙ_{β}, and inductively interpreting u ↦ a, (a, −), (−, a) as the denotation of a precomposed with the map given by application to [[u]], and first and second projections, respectively. The rules are then sound in the sense that if t ⟶^{a} t′ then (identifying a term with its denotation) copy t′ is a rooted component of a(t). In fact, there is a 1-1 correspondence between derivations with conclusion t ⟶^{a} t′, for some t′, and the rooted components of a(t), so the rules are also complete.

As a side-remark, the operational rules incorporate evaluation in the following sense: Let values v be given by v ::= α.t | λx.t | (t, u). Then we can define a nondeterministic evaluation-relation ⇓ such that

Proposition 4.2 If d is a derivation of t ⟶^{a} t′, then there is a value v such that t ⇓ v and v ⟶^{a} t′ by a subderivation of d.

5 Equivalences

After introducing some notation regarding relations, we explore four standard notions of equivalence for our language. A relation R between typing judgements is said to respect types if, whenever R relates

Γ_{1} ⊢ t_{1} : ℙ_{1} and Γ_{2} ⊢ t_{2} : ℙ_{2} ,

we have syntactic identities Γ_{1} ≡ Γ_{2} and ℙ_{1} ≡ ℙ_{2}. Below, all our relations will respect types, so we’ll often suppress the typing information, writing just t_{1} R t_{2}.

Suppose Γ is an environment list

x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} .

A Γ-closure is a substitution [u⃗/x⃗] such that for 1 ≤ j ≤ k, ⊢ u_{j} : ℙ_{j}. If R relates only closed terms, we write R^{o} for its open extension, relating Γ ⊢ t_{1} : ℙ and Γ ⊢ t_{2} : ℙ if for all Γ-closures [u⃗/x⃗] we have t_{1}[u⃗/x⃗] R t_{2}[u⃗/x⃗].

We’ll write R_{c} for the restriction of a type-respecting relation R to closed terms.

For a type-respecting relation R we write R also for the induced relation on actions, given as the least congruence on actions so that u_{1} ↦ a R u_{2} ↦ a if u_{1} R u_{2}.

5.1 Bisimulation

A type-respecting relation R on closed terms is a bisimulation [19, 21] if the following holds. If t_{1} R t_{2}, then

1. if t_{1} ⟶^{a} t′_{1}, then t_{2} ⟶^{a} t′_{2} for some t′_{2} such that t′_{1} R t′_{2};

2. if t_{2} ⟶^{a} t′_{2}, then t_{1} ⟶^{a} t′_{1} for some t′_{1} such that t′_{1} R t′_{2}.

Bisimilarity, ∼, is the largest bisimulation.

Theorem 5.1 Bisimilarity is a congruence.

Proof. We use Howe’s method [11] as adapted to a typed setting by Gordon [9]. In detail, we define the precongruence candidate ˆ∼ as follows:

\frac{x ∼^{o} w}{x ˆ∼ w} \frac{t ˆ∼ t′ rec x.t′ ∼^{o} w}{rec x.t ˆ∼ w} \frac{t_{j} ˆ∼ t′_{j} all j ∈ I Σ_{i∈I}t′_{i} ∼^{o} w}{Σ_{i∈I}t_{i} ˆ∼ w}

\frac{t ˆ∼ t′ α.t′ ∼^{o} w}{α.t ˆ∼ w} \frac{t ˆ∼ t′ u ˆ∼ u′ [u′ > α.x ⇒ t′] ∼^{o} w}{[u > α.x ⇒ t] ˆ∼ w}

\frac{t ˆ∼ t′ λx.t′ ∼^{o} w}{λx.t ˆ∼ w} \frac{t ˆ∼ t′ u ˆ∼ u′ t′ u′ ∼^{o} w}{t u ˆ∼ w}

\frac{t ˆ∼ t′ u ˆ∼ u′ (t′, u′) ∼^{o} w}{(t, u) ˆ∼ w} \frac{t ˆ∼ t′ fst t′ ∼^{o} w}{fst t ˆ∼ w} \frac{t ˆ∼ t′ snd t′ ∼^{o} w}{snd t ˆ∼ w}

Following Howe we now have: (i) ˆ∼ is reflexive; (ii) ˆ∼ is operator respecting; (iii) ∼^{o}⊆ ˆ∼; (iv) if t ˆ∼ t′ and t′ ∼^{o} w then t ˆ∼ w; (v) if t ˆ∼ t′ and u ˆ∼ u′ then t[u/x] ˆ∼ t′[u′/x] whenever the substitutions are well-formed; (vi) since ∼ is an equivalence relation, the transitive closure ˆ∼^{+} of ˆ∼ is symmetric, and therefore, so is ˆ∼_{c}^{+}.

Now we just need to show that ˆ∼_{c} is a simulation, because then ˆ∼_{c}^{+} is a bisimulation by (vi), and so ˆ∼_{c}^{+}⊆∼. In particular, ˆ∼_{c}⊆∼. By (i) and (v), it follows that ˆ∼⊆∼^{o}, and so by (iii), ˆ∼=∼^{o}. Hence, ∼ is a congruence because it is an equivalence relation and by (ii) it is operator respecting.

We prove that ˆ∼_{c} is a simulation by induction on the derivations of the operational semantics and using (iv-v). In fact, we need an induction hypothesis slightly stronger than one might expect:

if t_{1} ˆ∼_{c} t_{2} and t_{1} ⟶^{a_{1}} t′_{1}, then for all a_{2} with a_{1} ˆ∼_{c} a_{2} we have

t_{2} ⟶^{a_{2}} t′_{2} for some t′_{2} such that t′_{1} ˆ∼_{c} t′_{2}.

By (i), a ˆ∼_{c} a for all actions a, from which it follows that ˆ∼_{c} is a simulation.

□

Proposition 5.2 The following pairs of closed, well-formed terms are bisimilar:

1.  rec x.t ∼ t[rec x.t/x]
2.  [α.u > α.x ⇒ t] ∼ t[u/x]
3.  [β.u > α.x ⇒ t] ∼ ∅ if α ≠ β
4. [Σ_{i∈I}u_{i} > α.x ⇒ t] ∼ Σ_{i∈I}[u_{i} > α.x ⇒ t]
5. [u > α.x ⇒ Σ_{i∈I}t_{i}] ∼ Σ_{i∈I}[u > α.x ⇒ t_{i}]
6.  (λx.t) u ∼ t[u/x]
7.  λx.(t x) ∼ t
8.  λx.(Σ_{i∈I}t_{i}) ∼ Σ_{i∈I}(λx.t_{i})
9.  (Σ_{i∈I}t_{i}) u ∼ Σ_{i∈I}(t_{i} u)
10.  fst(t, u) ∼ t
11.  snd(t, u) ∼ u
12.  t ∼ (fst t, snd t)
13.  (Σ_{i∈I}t_{i}, Σ_{i∈I}u_{i}) ∼ Σ_{i∈I}(t_{i}, u_{i})
14.  fst(Σ_{i∈I}t_{i}) ∼ Σ_{i∈I}(fst t_{i})
15.  snd(Σ_{i∈I}t_{i}) ∼ Σ_{i∈I}(snd t_{i})

In each case t_{1} ∼ t_{2}, we can prove that the identity relation extended by the pair (t_{1}, t_{2}) is a bisimulation, so the correspondence is very tight, as is to be expected since in the denotational semantics, we have [[t_{1}]] ≅ [[t_{2}]].

Proposition 5.3 Let t_{1}, t_{2} be closed terms of type ℙ → ℚ. The following are equivalent:

1. t_{1} ∼ t_{2};

2. t_{1} u ∼ t_{2} u for all closed terms u of type ℙ;

3. t_{1} u_{1} ∼ t_{2} u_{2} for all closed terms u_{1} ∼ u_{2} of type ℙ.

5.2 Applicative Bisimulation

A type-respecting relation R on closed terms is an applicative bisimulation [1] if the following holds:

1. If ⊢ t_{1} R t_{2} : Σ_{α∈A}α.ℙ_{α}, we have

(a) if t_{1} ⟶^{β} t′_{1}, then t_{2} ⟶^{β} t′_{2} for some t′_{2} such that ⊢ t′_{1} R t′_{2} : ℙ_{β};

(b) if t_{2} ⟶^{β} t′_{2}, then t_{1} ⟶^{β} t′_{1} for some t′_{1} such that ⊢ t′_{1} R t′_{2} : ℙ_{β}.

2. If ⊢ t_{1} R t_{2} : ℙ → ℚ then for all ⊢ u : ℙ we have ⊢ t_{1} u R t_{2} u : ℚ.

3. If ⊢ t_{1} R t_{2} : ℙ & ℚ then ⊢ fst t_{1} R fst t_{2} : ℙ and ⊢ snd t_{1} R snd t_{2} : ℚ.

4. If ⊢ t_{1} R t_{2} : μ_{j}P⃗ .ℙ⃗ then ⊢ t_{1} R t_{2} : ℙ_{j}[μP⃗ .ℙ⃗/P⃗].

Applicative bisimilarity, ∼_{A}, is the largest applicative bisimulation. We have

Proposition 5.4 Bisimilarity and applicative bisimilarity coincide.

Proof. Since ∼ is a congruence, it follows that ∼ is an applicative bisimulation, and so ∼⊆∼_{A}. Conversely, we can show that ∼_{A} is a bisimulation by structural induction on (typing derivations of) actions a, and so ∼_{A}⊆∼. □

5.3 Higher Order Bisimulation

A type-respecting relation R on closed terms is a higher order bisimulation [23] if the following holds: If t_{1} R t_{2}, then

1. if t_{1} ⟶^{a_{1}} t′_{1}, then t_{2} ⟶^{a_{2}} t′_{2} for some a_{2}, t′_{2} such that a_{1} R a_{2} and

t′_{1} R t′_{2};

2. if t_{2} ⟶^{a_{2}} t′_{2}, then t_{1} ⟶^{a_{1}} t′_{1} for some a_{1}, t′_{1} such that a_{1} R a_{2} and

t′_{1} R t′_{2}.

Higher order bisimilarity, ∼_{H}, is the largest higher order bisimulation.

Proposition 5.5 Bisimilarity and higher order bisimilarity coincide.

Proof. Clearly, bisimilarity is a higher order bisimulation so that ∼⊆∼_{H}. For the converse, we observe that the proof of Theorem 5.1 goes through if we replace ∼ by ∼_{H}, and so ∼_{H} is a congruence. It then follows by structural induction on actions a that ∼_{H} is a bisimulation, so that ∼_{H}⊆∼. □

5.4 Contextual Equivalence

Let the type 𝟙 be given as •.𝕆 where 𝕆 is the empty prefixed sum. If ⊢ t : 𝟙 we’ll write t ⟶^{•} if there exists a t′ such that t ⟶^{•} t′. Two terms Γ ⊢ t_{1} : ℙ and Γ ⊢ t_{2} : ℙ are said to be contextually equivalent [16, 8] if C(t_{1}) ⟶^{•} iff C(t_{2}) ⟶^{•} for all contexts C such that C(t_{1}), C(t_{2}) are closed and have type 𝟙.

The following two terms can be shown contextually equivalent:

t_{1} ≡ α.∅ + α.β.∅ and t_{2} ≡ α.β.∅.

However, they are clearly not bisimilar, so contextual equivalence fails to take account of the nondeterministic branching of processes.

6 Examples

The higher-order language is quite expressive as the following examples show.

6.1 CCS

As in CCS [21], let N be a set of names and N̄ the set of complemented names {n̄ | n ∈ N}. Let l range over labels L = N ∪ N̄, with complementation extended to L by taking ¯ n̄ = n, and let τ be a distinct label. We can then specify a type ℙ as

ℙ = τ.ℙ + Σ_{n∈N}n.ℙ + Σ_{n∈N} n̄.ℙ .

Below, we let α range over L ∪ {τ}. The terms of CCS can be expressed in the higher-order language as the following terms of type ℙ:

[[x]] ≡ x  [[rec x.P]] ≡ rec x.[[P]]
[[α.P]] ≡ α.[[P]]  [[Σ_{i∈I}P_{i}]] ≡ Σ_{i∈I}[[P_{i}]]
[[P |Q]] ≡ Par [[P]] [[Q]] [[P \ S]] ≡ Res_{S} [[P]]
[[P [f]]] ≡ Rel_{f} [[P]]

Here, Par : ℙ → (ℙ → ℙ), Res_{S} : ℙ → ℙ, and Rel_{f} : ℙ → ℙ are abbreviations for the following recursively defined processes:

Par ≡ rec p.λx.λy.Σ_{α}[x > α.x′ ⇒ α.(p x′ y)] +
Σ_{α}[y > α.y′ ⇒ α.(p x y′)] +
Σ_{l}[x > l.x′ ⇒ [y > l̄.y′ ⇒ τ.(p x′ y′)]]
Res_{S} ≡ rec r.λx.Σ_{α∉(S∪S̄)}[x > α.x′ ⇒ α.(r x′)]
Rel_{f} ≡ rec r.λx.Σ_{α}[x > α.x′ ⇒ f(α).(r x′)]

Proposition 6.1 If P ⟶^{α} P′ is derivable in CCS then [[P]] ⟶^{α} [[P′]] in the higher-order language.

Conversely, if [[P]] ⟶^{a} t′ in the higher-order language, then a ≡ α and t′ ≡ [[P′]] for some α, P′ such that P ⟶^{α} P′ according to CCS.

It follows that the translations of two CCS terms are bisimilar in the general language iff they are strongly bisimilar in CCS.

We can recover the expansion law for general reasons. Write P |Q for the application Par P Q, where P and Q are terms of type ℙ. Suppose

P ∼ Σ_{α}Σ_{i∈I(α)}α.P_{i} and Q ∼ Σ_{α}Σ_{j∈J(α)}α.Q_{j}.

Using Proposition 5.2 items 1 and 6, then items 2-4, we get

P |Q ∼ Σ_{α}[P > α.x′ ⇒ α.(x′|Q)] +
Σ_{α}[Q > α.y′ ⇒ α.(P |y′)] +
Σ_{l}[P > l.x′ ⇒ [Q > l̄.y′ ⇒ τ.(x′|y′)]]
∼ Σ_{α}Σ_{i∈I(α)}α.(P_{i}|Q) +
Σ_{α}Σ_{j∈J(α)}α.(P |Q_{j}) +
Σ_{l}Σ_{i∈I(l),j∈J(l̄)}τ.(P_{i}|Q_{j}) .

6.2 Higher-Order CCS

In [10], Hennessy considers a language like CCS but where processes are passed at channels C; the language can be seen as an extension of Thomsen’s CHOCS [23]. For a translation into our language, we follow Hennessy in defining types that satisfy the equations

ℙ = τ.ℙ + Σ_{c∈C}c!.ℂ + Σ_{c∈C}c?.𝔽 ℂ = ℙ & ℙ 𝔽 = ℙ → ℙ .

We are chiefly interested in the parallel composition of processes, Par_{ℙ,ℙ} of type ℙ & ℙ → ℙ. But parallel composition is really a family of mutually dependent operations also including components such as Par_{𝔽,ℂ} of type 𝔽 & ℂ → ℙ to say how abstractions compose in parallel with concretions etc. All these components can be tupled together in a product and parallel composition defined as a simultaneous recursive definition whose component at ℙ & ℙ → ℙ satisfies

P |Q = Σ_{α}[P > α.x ⇒ α.(x|Q)] +
Σ_{α}[Q > α.y ⇒ α.(P |y)] +
Σ_{c}[P > c?.f ⇒ [Q > c!.p ⇒ τ.((f fst p)| snd p)]] +
Σ_{c}[P > c!.p ⇒ [Q > c?.f ⇒ τ.(snd p|(f fst p))]] ,

where, e.g., P |Q abbreviates Par_{ℙ,ℙ} (P, Q). In the summations c ∈ C and α ranges over c!, c?, τ.

The bisimulation induced on higher-order CCS terms is perhaps the one to be expected; a corresponding bisimulation relation is defined like an applicative bisimulation but restricted to the types of processes ℙ, concretions ℂ, and abstractions 𝔽.

6.3 Mobile Ambients with Public Names

We can translate the Ambient Calculus with public names [2] into the higherorder language, following similar lines to the process-passing language above. Assume a fixed set of ambient names n, m, … ∈ N. Following [3], the syntax of ambients is extended beyond processes (P) to include concretions (C) and abstractions (F):

P ::= ∅ | P |P | rep P | n[P] | in n.P | out n.P | open n!.P |
τ.P | mvin n!.C | mvout n!.C | open n?.P | mvin n?.F | x
C ::= (P, P) F ::= λx.P .

The notation for actions departs a little from that of [3]. Here some actions are marked with ! and others with ?—active (or inceptive) actions are marked by ! and passive (or receptive) actions by ?. We say actions α and β are complementary iff one has the form open n! or mvin n! while the other is open n? or mvin n? respectively. Complementary actions can synchronise together to form a τ-action. We adopt a slightly different notation for concretions ((P, R) instead of ⟨P ⟩R) and abstractions (λx.P instead of (x)P) to make their translation into the higher-order language clear.

Types for ambients are given recursively by (n ranges over N):

ℙ = τ.ℙ + Σ_{n}in n.ℙ + Σ_{n}out n.ℙ + Σ_{n}open n!.ℙ + Σ_{n}mvin n!.ℂ +
Σ_{n}mvout n!.ℂ + Σ_{n}open n?.ℙ + Σ_{n}mvin n?.𝔽
ℂ = ℙ & ℙ 𝔽 = ℙ → ℙ .

The eight components of the prefixed sum in the equation for ℙ correspond to the eight forms of ambient actions τ, in n, out n, open n!, mvin n!, mvout n!, open n? and mvin n?. We obtain the prefixing operations as injections into the appropriate component of the prefixed sum ℙ.

Parallel composition is really a family of operations, one of which is a binary operation between processes but where in addition there are parallel compositions of abstractions with concretions, and even abstractions with processes and concretions with processes. The family of operations

\begin{matrix}(−|−) : 𝔽 & ℂ → ℙ, & (−|−) : 𝔽 & ℙ → 𝔽, & (−|−) : ℂ & ℙ → ℂ, \\ (−|−) : ℂ & 𝔽 → ℙ, & (−|−) : ℙ & 𝔽 → 𝔽, & (−|−) : ℙ & ℂ → ℂ \end{matrix}

are defined in a simultaneous recursive definition:

Processes in parallel with processes:

P |Q = Σ_{α}[P > α.x ⇒ α.(x|Q)] + Σ_{α}[Q > α.y ⇒ α.(P |y)] +
Σ_{n}[P > open n!.x ⇒ [Q > open n?.y ⇒ τ.(x|y)]] +
Σ_{n}[P > open n?.x ⇒ [Q > open n!.y ⇒ τ.(x|y)]] +

Σ_{n}[P > mvin n?.f ⇒ [Q > mvin n!.p ⇒ τ.((f fst p)| snd p)]] + Σ_{n}[P > mvin n!.p ⇒ [Q > mvin n?.f ⇒ τ.(snd p|(f fst p))]] .

Abstractions in parallel with concretions: F |C = (F fst C)| snd C.

Abstractions in parallel with processes: F |P = λx.((F x)|P).

Concretions in parallel with processes: C|P = (fst C, (snd C|P)).

The remaining cases are given symmetrically. Processes P, Q of type ℙ will— up to bisimilarity—be sums of prefixed terms, and by Proposition 5.2, their parallel composition satisfies the obvious expansion law.

Ambient creation can be defined recursively in the higher-order language:

m[P] = [P > τ.x ⇒ τ.m[x]] +
Σ_{n}[P > in n.x ⇒ mvin n!.(m[x], ∅)] +
Σ_{n}[P > out n.x ⇒ mvout n!.(m[x], ∅)] +
[P > mvout m!.p ⇒ τ.(fst p|m[snd p])] +
open m?.P + mvin m?.λy.m[P |y] .

The denotations of ambients are determined by their capabilities: an ambient m[P] can perform the internal (τ) actions of P, enter a parallel ambient (mvin n!) if called upon to do so by an in n-action of P, exit an ambient n (mvout n!) if P so requests through an out n-action, be exited if P so requests through an mvout m!-action, be opened (open m?), or be entered by an ambient (mvin m?); initial actions of other forms are restricted away. Ambient creation is at least as complicated as parallel composition. This should not be surprising given that ambient creation corresponds intuitively to putting a process behind (so in parallel with) a wall or membrane which if unopened mediates in the communications the process can do, converting some actions to others and restricting some others away. The tree-containment structure of ambients is captured in the chain of open m?’s that they can perform.

By the properties of prefix match (Proposition 5.2, items 2-4), there is an expansion theorem for ambient creation. For a process P with P ∼ Σ_{α}Σ_{i∈I(α)}α.P_{i}, where α ranges over atomic actions of ambients,

m[P] ∼ Σ_{i∈I(τ)}τ.m[P_{i}] +
Σ_{n}Σ_{i∈I(in n)}mvin n!.(m[P_{i}], ∅) +
Σ_{n}Σ_{i∈I(out n)}mvout n!.(m[P_{i}], ∅) +
Σ_{i∈I(mvout m!)}τ.(fst P_{i}|m[snd P_{i}]) +
open m?.P + mvin m?.(λy.m[P |y]) .

7 Discussion

Matthew Hennessy’s work on domain models of concurrency [10] is analogous to the domain theory we describe; our use of presheaf categories, functor categories of the form [ℙ^{op}, Set] for a category ℙ, is mirrored in Hennessy’s work by domains of the form [ℙ^{op}, 2] for a partial order ℙ (here 2 is the partial order 0 < 1). In this sense Hennessy’s work anticipates the pathbased domain theory used here.

Flemming Nielson’s Typed Parallel Language (TPL) [17] is essentially a juxtaposition of value-passing CCS and simply-typed lambda calculus. Our language gains considerably in simplicity by integrating evaluation and transition semantics. The focus of TPL is a static type system in which processes are assigned a representation of their possible future communication possibilities, with no notion of causality. In contrast, our type system (which is also static) reflects that the capabilities of a process may change over time.

Andrew Gordon uses transition semantics and bisimulation to reason about the lambda calculus [9]. Our transitions correspond roughly to those of Gordon’s “active” types, integrating evaluation and observation. “Passive” types include function space, for which Gordon uses transitions of the form t ⟶^{@u} t u (where, in our notation, t has type ℙ → ℚ and u has type ℙ). Such transitions have no counterpart in our semantics, because they would destroy the correspondence between derivations in the operational semantics and rooted components in the presheaf model.

Every presheaf category possesses a notion of bisimulation, derived from open maps [13, 14]. Open maps are a generalization of functional bisimulations, or zig-zag morphisms, known from transition systems. Presheaves over ℙ are open-map bisimilar iff there is a span of surjective open maps between them. The maps of Lin and Aff preserve open maps and so openmap bisimulation [7, 4], giving congruence results for free when a process language is interpreted in these categories. Interestingly, although the operational bisimulation of Park/Milner is a congruence for the higher-order language, maps of Cts need not preserve open maps. This suggests that one should look at other notions of open map; in fact, as shown in [7], to every comonad T on Lin there is a corresponding notion of “T -open map”, and thus a notion of “T -bisimulation”. In the case of the exponential !, the corresponding !-bisimulation degenerates into isomorphism, but there are models where !-bisimulation and open-map bisimulation coincide, and one may hope to recover operational bisimulation as !-bisimulation for some choice of exponential (or expose it as a union of such bisimulations). In fact, it appears that the correspondence between the denotational and operational semantics can be proved abstractly, depending only on properties of the prefixed sum, so that it holds also for other choices of exponential.

The language has no distinguished invisible action τ, so there is the issue of how to support more abstract operational equivalences such as weak bisimulation, perhaps starting from [5].

Work is in progress on extending the idea of prefixed sum to include namegeneration as in Milner’s π-calculus. The π-calculus already has a presheaf semantics [6] but it has not been extended to higher order (see [22] for an operational extension). We hope to be able to link up with the work on the ν-calculus by Pitts and Stark [20] and Jeffrey and Rathke [12].

Acknowledgments. We thank the encyclopaedic Andy Pitts for helpful advice. Part of this paper was prepared during a pleasant visit of MN to DISI—the people there are thanked for their hospitality.

References

[1] S. Abramsky. The lazy lambda calculus. In D. Turner (ed): Research Topics in Functional Programming. Addison-Wesley, 1990.

[2] L. Cardelli and A. D. Gordon. Anytime, anywhere. Modal logics for mobile ambients. In Proc. POPL’00.

[3] L. Cardelli and A. D. Gordon. A commitment relation for the ambient calculus. Note. October 6th, 2000.

[4] G. L. Cattani. Presheaf Models for Concurrency. BRICS Dissertation Series DS-99-1, 1999.

[5] G. L. Cattani, M. Fiore, and G. Winskel. Weak bisimulation and open maps. In Proc. LICS’99.

[6] G. L. Cattani, I. Stark, and G. Winskel. Presheaf models for the π-calculus. In Proc. CTCS’97, LNCS 1290.

[7] G. L. Cattani and G. Winskel. Profunctors, open maps and bisimulation. Manuscript, 2000.

[8] A. D. Gordon and L. Cardelli. Equational properties of mobile ambients. In Proc. FoSSaCS’99.

[9] A. D. Gordon. Bisimilarity as a theory of functional programming. In Proc. MFPS’95, ENTCS 1.

[10] M. Hennessy. A fully abstract denotational model for higher-order processes. Information and Computation, 112(1):55–95, 1994.

[11] D. J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103–112, 1996.

[12] A. Jeffrey and J. Rathke. Towards a theory of bisimulation for local names. In Proc. LICS’99.

[13] A. Joyal and I. Moerdijk. A completeness theorem for open maps. Annals of Pure and Applied Logic, 70:51–86, 1994.

[14] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Information and Computation, 127:164–185, 1996.

[15] G. M. Kelly. Basic concepts of enriched category theory. London Math. Soc. Lecture Note Series 64, CUP, 1982.

[16] J. H. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, MIT, December 1968.

[17] F. Nielson. The typed λ-calculus with first-class processes. In Proc. PARLE’89, LNCS 366.

[18] M. Nygaard and G. Winskel. Linearity in process languages. In Proc. LICS’02.

[19] D. Park. Concurrency and automata on infinite sequences. In Proc. 5th GI Conference, LNCS 104, 1981.

[20] A. M. Pitts and I. D. B. Stark. Observable properties of higher order functions that dynamically create local names, or: What’s new? In Proc. MFCS’93, LNCS 711.

[21] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[22] D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh, 1992.

[23] B. Thomsen. A calculus of higher order communicating systems. In Proc. POPL’89.

Recent BRICS Report Series Publications

RS-02-49 Mikkel Nygaard and Glynn Winskel. HOPLA—A Higher-Order Process Language. December 2002. 18 pp. Appears in Brim, Jančar, Křetínský and Antonín, editors, Concurrency Theory: 13th International Conference, CONCUR ’02 Proceedings, LNCS 2421, 2002, pages 434–448.

RS-02-48 Mikkel Nygaard and Glynn Winskel. Linearity in Process Languages. December 2002. 27 pp. Appears in Plotkin, editor, Seventeenth Annual IEEE Symposium on Logic in Computer Science, LICS ’02 Proceedings, 2002, pages 433–446.

RS-02-47 Zoltán Ésik. Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators. December 2002. 16 pp. To appear in 6th International Conference, Developments in Language Theory, DLT ’02 Revised Papers, LNCS, 2002.

RS-02-46 Zoltán Ésik and Hans Leiß. Greibach Normal Form in Algebraically Complete Semirings. December 2002. 43 pp. An extended abstract appears in Bradfield, editor, European Association for Computer Science Logic: 16th International Workshop, CSL ’02 Proceedings, LNCS 2471, 2002, pages 135–150.

RS-02-45 Jesper Makholm Byskov. Chromatic Number in Time O(2.4023^{n}) Using Maximal Independent Sets. December 2002. 6 pp.

RS-02-44 Zoltán Ésik and Zoltán L. Németh. Higher Dimensional Automata. November 2002. 32 pp. A preliminary version appears under the title Automata on Series-Parallel Biposets in Kuich, Rozenberg and Salomaa, editors, 5th International Conference, Developments in Language Theory, DLT ’01 Revised Papers, LNCS 2295, 2001, pages 217–227. This report supersedes the earlier BRICS report RS-01-24.

RS-02-43 Mikkel Christiansen and Emmanuel Fleury. Using IDDs for Packet Filtering. October 2002. 25 pp.

RS-02-42 Luca Aceto, Jens A. Hansen, Anna Ingólfsdóttir, Jacob Johnsen, and John Knudsen. Checking Consistency of Pedigree Information is NP-complete (Preliminary Report). October 2002. 16 pp.