A Fully-Abstract Model for the π-calculus

(Extended Abstract)

M.P. Fiore^{∗} LFCS, Univ. of Edinburgh JCMB, The King’s Buildings

Edinburgh EH9 3JZ, UK mf@dcs.ed.ac.uk

E. Moggi^{†} DISI, Univ. di Genova

v. Dodecaneso 35 16146 Genova, Italy moggi@disi.unige.it

D. Sangiorgi^{‡} INRIA, Sophia Antipolis 2004 r. des Lucioles 06902, Sophia Antipolis, France davide@cma.cma.fr

Abstract

This paper provides both a fully abstract (domaintheoretic) model for the π-calculus and a universal (settheoretic) model for the finite π-calculus with respect to strong late bisimulation and congruence. This is done by: considering categorical models, defining a metalanguage for these models, and translating the π-calculus into the metalanguage. A technical novelty of our approach is an abstract proof of full abstraction: The result on full abstraction for the finite π-calculus in the set-theoretic model is axiomatically extended to the whole π-calculus with respect to the domain-theoretic interpretation. In this proof, a central role is played by the description of non-determinism as a free construction and by the equational theory of the metalanguage.

Introduction

The π-calculus [16] is a process algebra for communicating processes with a dynamically-changing topology. Processes (or agents) interact with each other by exchanging names. A name can be private (i.e. local) to a process, which, however, may decide to export the name thus accepting to share it with other processes. Communication of private names is the main difference between π-calculus and its predecessor CCS, and makes the calculus very expressive. Late bisimulation is the operational equivalence on π-calculus processes analised in [16]. It is preserved by all operators of the calculus except for input. Late congruence is the induced congruence. Roughly, in late bisimulation free names of processes are viewed as constants, whereas in late congruence they are viewed as free variables and hence can be freely instantiated.

This paper substantiates the claim that “the π-calculus is CCS with local channels”. Indeed, we construct a model for the π-calculus combining techniques used for modelling CCS and local variables in the light of an abstract approach to denotational semantics; notably: powerdomains as free algebras, functor categories, and a kind of monadic metalanguage. Powerdomains as free algebras were introduced in [12] for modelling the bounded non-determinism of a parallel imperative language. Functor categories were used in [18] to model local variables in Algol-like languages. Monads were proposed as a tool for structuring denotational semantics [17, 8].

Using monads we can exhibit the semantics for the π-calculus as a special case of a general construction, which can be instantiated to get semantics for calculi ranging from pure CCS to value-passing CCS to the polyadic π-calculus. This uniform treatment highlights the intrinsic differences and similarities among these calculi. Here, for brevity, we will only present a model for the π-calculus. The model captures essential properties of the role of names in the π-calculus: for instance, that the identity of names does not affect the behaviour of a process and that equality and inequality conditions on names may affect process bisimilarity.

We give a denotational semantics for the π-calculus by: considering categorical models, defining a metalanguage for these models, and translating the π-calculus into the metalanguage. The metalanguage is a simply typed λ-calculus with sums, operations for nondeterminism and dynamic allocation, base types for names and agents, and recursion (over exponents of the type of agents). It has an interpretation in a standard domain-theoretic model given by a functor category over Cpo (the category of cpos —posets closed under lubs of ω-chains possibly without bottom element— and continuous functions) equipped with a powerdomain monad. This model is shown to provide a fullyabstract denotational semantics for the π-calculus with respect to strong late bisimulation and congruence. Indeed, the model also provides fully abstract semantics for bisimulations under a distinction [16] and bisimulations under a constraint (Section 3), which are bisimulation relations in between late bisimulation and late congruence.

∗Supported by EPSRC grant RR29300 and HCM ERB-CHRXCT 92-0046.

†Supported by ESPRIT BRA CLICS-II, HCM EXPRESS and SCIENCE ERBSC1*CT920795.

‡Supported by HCM EXPRESS and ESPRIT BRA CONFER.

The metalanguage without recursion has an interpretation in a set-theoretic model given by a functor category over Set (the category of sets and functions) equipped with the free-semilattice monad. This model is in bijective correspondence with certain canonical normal forms of π-calculus processes and provides a universal denotational semantics for the finite π-calculus with respect to late bisimulation and congruence.

An important aspect of the metalanguage is its associated equational theory which permits reasoning about the denotational semantics. For example, to validate laws on π-calculus processes we first validate analogous laws between terms of the metalanguage using its equational theory, and then infer the original laws by compositionality of the denotational interpretation. Also, the denotational semantics implicitly defines a model of synchronisation trees for the π-calculus under late bisimulation (i.e. an abstract notion of late transition system) and process-like operations on these, whose laws can be established using the equational theory of the metalanguage.

A novelty of our approach is an abstract proof of full abstraction. The result on full abstraction for canonical normal forms in the set-theoretic model is axiomatically extended to the whole calculus with respect to the domain-theoretic interpretation. This is done by relating the free-semilattice monad and the powerdomain monad by means of their universal properties, and by exploiting the equational theory of the metalanguage. As a technical benefit, an explicit description of the powerdomain is not needed and we can work with cpos instead of bifinite domains.

Related work. In [13] and [10], Hennessy and Plotkin constructed term models for CCS-like languages (where actions are pure synchronisations). Later, Abramsky [1] gave a denotational semantics for SCCS using a domain of synchronisation trees defined as the initial solution in SFP (the category of bifinite domains and continuous functions) of a domain equation involving Plotkin’s powerdomain. Further, he provided two full abstraction results: one for finite SCCS with respect to strong partial bisimulation and another one for the whole SCCS with respect to the finitely observable part of strong bisimulation. More recently, Aceto and Ingólfsdóttir [4], using the same domain of synchronisation trees, have generalised Abramsky’s results to a class of CCS-like languages (those described in the compact GSOS format). Outside the realm of domain theory, in [21], Rutten provides fully abstract semantics with respect to strong bisimulation in a nonwell-founded set (specified by a recursive equation) for a different class of CCS-like languages (a subclass of those described in the tyft/txft format).

Independently from us, other researchers have been working on a denotational semantics for the π-calculus. Stark has given a denotational semantics in a functor category over SFP. His interpretation coincides with ours but, as he has not extracted a metalanguage from the model, his constructions are concrete and do not identify the uniformities that our axiomatic approach highlights. Abramsky and Meredith are investigating a model for the π-calculus based on non-well-founded sets. Details of this work are not known to us. Organisation of the paper. In Section 1 we review the syntax and the operational semantics of the π-calculus. In Section 2 we present our denotational model and in Section 3 the full abstraction results. Finally, in Section 4 we discuss conclusions and directions for future research.

1 π-calculus

We review the syntax and operational semantics of the π-calculus. N is the countably infinite set of all names, ranged over by a, b, c, d. The class Pr of processes is built from the operators of inaction, sum, matching, mismatching, prefixing, restriction, parallel composition and guarded replication; a prefix can be an input, a free output, a bound output or an silent prefix:

Definition 1.1 (π-calculus, concrete syntax)

P := 0 | P + P | [a = b]P | [a ≠ b]P | α. P |
νa P | P | P | !α. P
α := a(b) | \overline{a}b | \overline{a}(b) | τ

A process is finite when it uses only the operators in the first row.

Remark. It is possible to extend the definition of finite processes to include the parallel composition and restriction operators, but this does not add new process behaviours and complicates some of our technical developments.

We refer to [16] for detailed discussions on the operators of the language. We remind that a matching [a = b]P means “if a = b then P ”, that a mismatching [a ≠ b]P means “if a ≠ b then P ”, and that a replication !α. P represents a countably infinite number of copies of α. P in parallel. Guarded replications enjoy simpler algebraic laws than plain replication !P. The restriction to guarded replications does not affect expressiveness, since every plain replication can be rewritten in terms of guarded replications, up to strong late congruence [23]. A bound output \overline{a}(b) represents the output of a private name b at a; one can think of \overline{a}(b). P as an abbreviation for νb \overline{a}b. P. In a(b). P, νb P, and \overline{a}(b). P all free occurrences of name b in P are bound. Free names (fn) and bound names (bn) of processes and prefixes, name substitution, and alpha conversion are defined as expected. Terminology and notation. We use V to range over finite lists of distinct names and Pr_{V} for the set of processes with free names in V. We write [a ∉ a_{0}, …, a_{n−1}]P as abbreviation for [a ≠ a_{0}] … [a ≠ a_{n−1}]P. For a finite list without repetitions I = i_{0}, …, i_{n−1}, we write ∑_{i∈I} P_{i} as an abbreviation for P_{i_{0}} + … + P_{i_{n−1}}. We use the symbol ≡ for syntactic identity, and ≡_{α} for syntactic identity modulo alpha conversion. We assign parallel composition and sum the lowest precedence among the operators.

Table 1 shows the transitional rules for the calculus. We have omitted the symmetric of rules sum1, par1, com1, and close1. Note that there are four kinds of transitions, corresponding to the four kinds of prefixes in the syntax.

Definition 1.2 (Late bisimulation [16]) Late bisimulation is the largest symmetric relation ∼ on processes such that P ∼ Q implies

1. Whenever P ⟶^{a(b)} P′ and b ∉ fn(Q), then Q′ ex-

ists such that Q ⟶^{a(b)} Q′ and for all names c, P′{c/b} ∼ Q′{c/b}.

2. Whenever P ⟶^{α} P′ for α ≡ \overline{a}b or α ≡ τ, then Q′ exists such that Q ⟶^{α} Q′ and P′ ∼ Q′.

3. Whenever P ⟶^{\overline{a}(b)} P′ and b ∉ fn(Q), then Q′ exists

such that Q ⟶^{\overline{a}(b)} Q′ and P′ ∼ Q′.

Late bisimilarity is preserved by all operators except input prefix. The induced congruence, called late congruence, is denoted by ∼^{c} and can be defined thus:

Definition 1.3 (Late congruence [16]) Two processes P, Q are late congruent, written P ∼^{c} Q, if P σ ∼ Qσ for all name substitutions σ.

In the semantics of Section 2, ∼ will correspond to the closed interpretation —where free names of processes are treated as constants— and ∼^{c} will correspond to the open interpretation —where free names are treated as free variables.

To have a simpler axiomatic proof of full abstraction (Section 3), we will make use of the auxiliary operators of left merge and synchronisation [6], written ⌋ and ∥, respectively. They are related to parallel composition by the law:

Par P | Q = P ⌋Q + Q⌋P + P ∥ Q.

In this law, left merge accounts for the behaviour of P | Q given by rules par1-2, whereas synchronisation accounts for that given by com1-2 and close1-2.

Definition 1.4 (CN F_{V}) Given a finite list of distinct names V, the set of processes N F_{V}, called the V -normal forms, is defined from the grammar below, where it is assumed that a, b ∈ V and that c ∉ V:

P_{V} := P_{V} + P_{V} | 0 | \overline{a}b. P_{V} | \overline{a}(c). P_{V,c} |

τ. P_{V} | a(c). ( ∑_{a∈V}[c = a]P_{V} + [c ∉ V]P_{V,c})

CN F_{V}, called the canonical V -normal forms, is the set of canonical representatives of the equivalence classes obtained by quotienting N F_{V} by ∼. Formally, CN F_{V} is defined from the grammar for N F_{V} by imposing a canonical choice for bound names and requiring that, in any term of the form ∑_{i} P_{i}, processes P_{i} are ordered lexicographically and are not duplicated (i.e. P_{i} ≡ P_{j} implies i = j).

2 Denotational semantics

The denotation of a process is given relative to the names which are free (or visible) in it. Thus, our model is a type A of agents which varies over stages; intuitively, the number of free names available for interaction. That is, the type A consists of the following data: for every natural number n a type A(n) of ‘processes with at most n free names’ and for every injective substitution ι : n ↪ m of n names into m names a mapping A(n) ^{A(ι)} A(m) which allows us to view every process with n free names as a process with m free names. Of course, these mappings cannot be arbitrary: we expect that A(id_{n}) = id_{A(n)} as the substitution id_{n} : n ↪ n produces no renaming; whilst for

alpha   \frac{P ≡_{α} P′ P′ ⟶^{α} P′′}{P ⟶^{α} P′′}  pre  α. P ⟶^{α} P  sum1   \frac{P ⟶^{α} P′}{P + Q ⟶^{α} P′}
rep !α. P ⟶^{α} P | !α. P if bn(α) ∉ fn(!α. P)  par1  \frac{P ⟶^{α} P′}{P | Q ⟶^{α} P′ | Q} if bn(α) ∉ fn(Q)

com1   \frac{P ⟶^{a(b)} P′ Q ⟶^{\overline{a}c} Q′}{P | Q ⟶^{τ} P′\{c/b\} | Q′}  close1   \frac{P ⟶^{a(b)} P′ Q ⟶^{\overline{a}(b)} Q′}{P | Q ⟶^{τ} νb (P′ | Q′)}  open   \frac{P ⟶^{\overline{a}b} P′}{νb P ⟶^{\overline{a}(b)} P′} if a ≢ b

res   \frac{P ⟶^{α} P′}{νa P ⟶^{α} νa P′} a ∉ names(α) mismch   \frac{P ⟶^{α} P′}{[a ≠ b]P ⟶^{α} P′} if a ≢ b mch    \frac{P ⟶^{α} P′}{[a = a]P ⟶^{α} P′}

Table 1. The transition system for the π-calculus

injective substitutions ι : i ↪ j and κ : j ↪ k we expect that the mapping A(i) ^{A(κι)} A(j) induced by κι decomposes as the mappings A(i) ^{A(ι)} A(j) ^{A(κ)} A(k) induced by ι and κ. All this amounts to saying that A is a functor from a category I (of injective maps between finite cardinals) to a category C (of meanings).

Henceforth we will take the viewpoint that A is a type in the functor category C^{I} whose objects are functors from I to C and whose arrows are natural transformations between such functors. (Recall that a natural transformation φ : X → Y between functors X, Y : I → C is given by a family {φ_{n} : X(n) → Y (n)}_{n∈|I|} of morphisms in C such that for all injective maps ι : n ↪ m, Y (ι)∘φ_{n} = φ_{m}∘X(ι).) A process with no free names will have a denotation as a global element of A (i.e. a natural transformation 1 \underrightarrow{.} A) or, equivalently, as an element of A(0) because, by Yoneda, every p : A is uniquely determined by p_{0} : A(0) as p_{n} = A(0 ↪ n)(p_{0}) : A(n). Thus, the naturality condition imposes a uniform interpretation at all stages. To interpret arbitrary processes we will introduce a type N of names and assign to a process with n free names a denotation as a natural transformation N^{n} \underrightarrow{.} A. As before the naturality condition imposes a uniform interpretation which, for example, will account for the irrelevance of the identity of names.

It is possible to axiomatise the structure needed from our category C of meanings in order to support the denotational semantics, in particular C must be a Cpoenriched bicartesian closed category (Cpo-biCCC). We will not give an explicit axiomatisation of C in this extended abstract, indeed we will only be concerned with two categories C of meanings; viz. Cpo and Set. In Cpo^{I} we will obtain a domain-theoretic model for the whole π-calculus; whilst in Set^{I} we will obtain a settheoretic model for the finite processes.

Our denotational semantics is given by translation into a metalanguage. The metalanguage is a type theory (with an associated equational theory) which is an internal language for the part of C^{I} we are interested in. In this way we can perform constructions and definitions in C^{I} and prove properties (e.g. about the equality of certain morphisms) without the need of looking at explicit descriptions. The core of the metalanguage is a simply typed λ-calculus (1, ×, ⇒) with sums (+), type constructors for non-determinism and dynamic allocation of names, and base types for names (N) and agents (A). In addition, we have operators for recursion (over exponents of the type of agents): in the domaintheoretic interpretation arbitrary recursive definitions are possible; whilst in the set-theoretic interpretation we only consider finite agents.

In the remainder of the section we define the constructors for modelling non-determinism and dynamic allocation; then we introduce the objects of names and agents; finally we present the open and closed interpretations, respectively corresponding to late congruence and bisimulation.

Notation. In expressions of the metalanguage we adopt the following conventions: e is an expression, x, y are variables, f, g are variables of functional type, p, q are variables of computational type.

2.1 Non-determinism

We introduce the power type constructor ℙ for modelling non-determinism. It has associated operations val_{X} : X ⇒ ℙ X and let_{X,Y} : (X ⇒ ℙ Y) × ℙ X ⇒ ℙ Y subject to the laws for a commutative monad —e.g. let(λx_{1}. let(λx_{2}. e, p_{2}), p_{1}) = let(λx_{2}. let(λx_{1}. e, p_{1}), p_{2}); and operations 0 : ℙ X and ∪ : ℙ X × ℙ X ⇒ ℙ X making (ℙ X, 0, ∪) into a semilattice. Moreover, the operations for nondeterminism interact with let according to the following laws: let(f, 0) = 0 and let(f, ∪(p_{1}, p_{2})) = ∪(let(f, p_{1}), let(f, p_{2})). To understand these laws think that, roughly, let(f, p) is ‘⋃{f(x) | x ∈ p}’.

In general these power types arise as free constructions by considering left adjoints to forgetful functors from a category of non-deterministic computations to a category of values (see [12, 5]). Two such constructions that will be used later are:

• The free-semilattice monad. Let S be a Cpocartesian category, and let SL(S) be the Cpocategory of semilattices in S and homomorphisms.

The free-semilattice monad on S is the Cpo-monad induced by the Cpo-adjunction SL(S) [figure: ⊥] S whenever it exists. When S = Set the freesemilattice monad is the finite powerset functor equipped with the singleton and the big union.

• Abramsky’s powerdomain monad. Let D be a Cpo-cartesian category. We define the category ND(D) of non-deterministic computations over D as the Cpo-category with objects (D, ⊥, 0, ∪), where ⊥ : D is the least element of D and (D, 0, ∪) is a semilattice in D; arrows are strict semilattice homomorphisms.

Abramsky’s Powerdomain monad on D is the Cpo-monad on D induced by the Cpo-adjunction ND(D) [figure: ⊥] D whenever it exists.

When D = Cpo Abramsky’s powerdomain monad exists; see [12, 3].

Below we will be concerned with commutative monads for non-determinism arising as above over functor categories. The following observation incorporates them in our setting:

Proposition 2.1 If C admits Abramsky’s powerdomain monad (resp. the free-semilattice monad) then so does C^{W} for every small category W and it is given pointwise. That is, writing ℙ and ℙ ^{W} for the monad on C and C^{W} respectively, we have ℙ ^{W}(X)(w) = ℙ (X(w)).

2.2 Dynamic allocation

We introduce the type constructor δ for modelling dynamic allocation of names. It has associated operations δ_{X,Y} : (X ⇒ Y) ⇒ δX ⇒ δY, up_{X} : X ⇒ δX, and swap_{X} : δ^{2}X ⇒ δ^{2}X; which are the internal version of categorical structure on C^{I} (made explicit below) induced by I. Intuitively δX stands for the type X when one new name is available. With this in mind, • up_{X,n} is the canonical coercion mapping an element

of X at stage n to the same element at stage n + 1;

• swap_{X,n} is an involution mapping an element of X at stage n + 2 to the element of the same type where the last two names in n + 2 have been swapped.

To explain how such structure is obtained, we consider an alternative characterisation of the category I of finite cardinals n = {0, …, n − 1} and injective maps:

I is the strict monoidal category (I, 0, +) freely generated from one object 1 and morphisms up : 0 → 1 and swap : 2 → 2 (here 2 = 1+1) such that swap∘swap = id_{2} : 2 → 2, (up + id_{1}) ∘ up = (id_{1} + up) ∘ up : 0 → 2 and swap ∘ (up + id_{1}) = (id_{1} + up) : 1 → 2.

δ : C^{I} → C^{I}, up : δ^{0} \underrightarrow{.} δ, swap : δ^{2} \underrightarrow{.} δ^{2} are defined in terms of the generating data (1, up, swap) for I

• (δX)(n) =^{def} X(n + 1)

• up_{X,n} =^{def} X(n + up) : X(n) → X(n + 1)

• swap_{X,n} =^{def} X(n + swap) : X(n + 2) → X(n + 2)

and inherit the equational properties of up and swap; i.e. swap_{X} ∘swap_{X} = id_{δ^{2}X}, δ(up_{X})∘up_{X} = up_{δX} ∘up_{X}, and swap_{X} ∘δ(up_{X}) = up_{δX}. Moreover, δ, up, and swap preserve anything defined pointwise; such as limits and colimits, and Abramsky’s powerdomain monad with its associated structure (⊥, 0, and ∪).

The functor δ has a tensorial strength up_{X}×id_{δY} : X×δY → δ(X×Y) —here we use that δ(X × Y) = δ(X) × δ(Y)— which, as usual in the presence of exponentials, allow us to internalise the action of δ on morphisms as a map δ_{X,Y} : (X ⇒ Y) ⇒ δX ⇒ δY.

2.3 Names and agents

We introduce the objects N of names and A of agents in C^{I} together with their associated operations.

Names. The type of names N is defined as the inclusion of I into the biCCC C; i.e. N(n) =^{def} n (on the rhs n is the coproduct in C of n copies of the terminal object). N admits a decidable equality eq : N ×N ⇒ 2 (here 2 = 1 + 1) and satisfies the following properties which are used for interpreting the π-calculus and establishing full-abstraction:

• There is a global element new : δN (viz. new_{n} =^{def} n)

making N ^{up_{N}} δN new 1 into a coproduct diagram in C^{I}. Thus we can do case analysis on δN; to improve readability we write [ \begin{matrix}λx : N. e_{1} \\ λt : 1. e_{2} \end{matrix} ] a for

case a of up_{N}(x) =>e_{1} or new =>e_{2}. (We use a similar notation for doing case analysis on coproducts.)

• swap_{N} is an involution that swaps δ(new) and δ (up_{N}) new; that is, swap_{N}(δ new) = δ (up_{N}) new.

• For h : N × N ⇒ X,

swap_{X}(δ (λx : N. δ (λy : N. h(x, y)) new) new)

= δ (λy : N. δ (λx : N. h(x, y)) new) new.  (1)

We will also use the following proposition stating that an element of N ⇒ X at stage n is determined by n elements of X at stage n together with an element of δX at stage n.

Proposition 2.2 For any biCCC K, the exponential N⇒X in K^{I} exists and is given by (N⇒X)(n) = X(n)^{n} × X(n + 1).

Remark. In particular, the natural transformation interpreting f : N ⇒ X ⊢ δ f new : δX is, at stage n, π_{n+1} : X(n)^{n} × X(n + 1) → X(n + 1).

Agents. The type of agents A is defined as μX. ℙ (HX) where

• HX =^{def} N ×(N⇒X)+N ×N ×X +N ×δX +X; each

summand respectively giving meaning to inputs, free outputs, bound outputs, and internal actions of processes; and

• in the set-theoretic interpretation ℙ is the freesemilattice monad on Set^{I}, whilst in the domaintheoretic interpretation it is Abramsky’s powerdomain monad on Cpo^{I}. Here one can apply the standard techniques for solving recursive domain equations —see [25] and [9, Chapter 7].

By Propositions 2.1 and 2.2, and results on the solution of domain equations, we can give a concrete description of A on objects as the initial solution to the following system of equations in C (where ℙ below is the appropriate power monad on C) with n ∈ | I |

X_{n} = ℙ (n×X_{n}^{n}×X_{n+1} + n×n×X_{n} + n×X_{n+1} + X_{n}).

We introduce some auxiliary notation (related to a suitable monad transformer —see [8]) which simplifies the description of the denotational semantics and helps in validating equational properties:

• S : HA ⇒ A is given (up to the isomorphism ℙ HA ≅ A) by S(x) = val(x). We write S_{i} (i = 1, 4) for the i^{th} component of S; so that S = [S_{1}, S_{2}, S_{3}, S_{4}].

• C : (HA⇒A)×A ⇒ A is given (up to the isomorphism ℙ HA ≅ A) by C(f, p) = let(f, p).

We write CC : (HA × HA ⇒ A) × A × A ⇒ A for C iterated twice; i.e. CC(k, p_{1}, p_{2}) = C(λx. C(λy. k(x, y), p_{2}), p_{1}).

S and C inherit the properties of val and let, and since ℙ is commutative we have

CC(K, p_{1}, p_{2}) = CC(K ∘ ⟨π_{2}, π_{1}⟩, p_{2}, p_{1}). (2)

From now on we will consistently treat the isomorphism ℙ HA ≅ A as an equality.

Finally we introduce the operation R : δA ⇒ A, which maps, at stage n, a process with n+1 free names to one with n free names by restricting on the last allocated name. The definition of R, given in Table 2, relies on the type equalities δA = ℙ (δN×δ(N⇒A) + δN×δN×δA+δN×δ^{2}A+δA) and δN = N +1, and inspects whether each action capability involves the last allocated name (i.e. the new one) or not:

• In case of an input at a: if a is new, then we cancel the input capability, otherwise we allow the input and restrict on the continuation.

• In case of a free output at a of b: if a is new, then we cancel the output capability; if a is not new but b is, then we make the free output into a bound output; if neither a nor b are new, then we allow the output and restrict on the continuation.

• In case of a bound output at a: if a is new, then we cancel the output capability, otherwise we allow the output and restrict on the second last allocated name (not on the last allocated one as this is the one being allocated by the bound output).

• In case of an internal action: we allow the action and restrict on the continuation.

2.4 Interpretation

We give the interpretation of the term constructors for an abstract syntax of the π-calculus (c.f. Definition 1.1). The interpretation is defined by translation into the metalanguage of the previous subsections as follows:

nil : A  deadlock
sum : A, A → A non-deterministic choice

are given by the semilattice structure of ℙ HA.

M : N, N, A → A  matching
MM : N, N, A → A mismatching

R(p) =^{def} let([ \begin{matrix}λa : δN, f : δ(N ⇒ A). [ \begin{matrix}λa′ : N. S_{1}(a′, λb : N. R(δ (λf′ : N ⇒ A. f′b) f)) \\ λt : 1. 0 \end{matrix} ] a \\ λa : δN, b : δN, p′ : δA. [ \begin{matrix}λa′ : N. [ \begin{matrix}λb′ : N. S_{2}(a′, b′, R p′), \\ λt : 1. S_{3}(a′, p′) \end{matrix} ] b \\ λt : 1. 0 \end{matrix} ] a \\ λa : δN, p′ : δ^{2}A. [ \begin{matrix}λa′ : N. S_{3}(a′, δ R (swap_{A} p′)) \\ λt : 1. 0 \end{matrix} ] a \\ λp′ : δA. S_{4}(R p′) \end{matrix} ] , p)

Table 2. R : δA ⇒ A

are defined by case analysis using the decidable equality on the type of names.

in : N, (N ⇒ A) → A  input
out : N, N, A → A  output
bout : N, (N ⇒ A) → A bound output
tau : A → A  internal action

correspond, except for bout, to components of the operation S : HA ⇒ A; explicitly, [in, out, S_{3}, tau] = S. Bounded output is given by bout(a, f) = S_{3}(a, δ f new) —see Proposition 2.2 and the remark after it.

res : (N ⇒ A) → A local name

is given by res(f) = R(δ f new). (Note that the definition of res in terms of R mimics that of bout in terms of S_{3}.)

par : A, A → A parallel composition
lm : A, A → A left merge
syn : A, A → A synchronisation

are defined by mutual recursion as follows: par(p, q) = sum(lm(p, q), lm(q, p), syn(p, q), syn(q, p)). lm(p, q) =

C([ \begin{matrix}λa : N, f : N ⇒ A. in(a, λb : N. par(fb, q)) \\ λa : N, b : N, p′ : A. out(a, b, par(p′, q)) \\ λa : N, p′ : δA. S_{3}(a, δ par (p′, up q)) \\ λp′ : A. tau(par(p′, q)) \end{matrix} ] , p).

When two processes try to communicate there are 16 possibilities to consider, since each process may perform 4 possible actions. This explains the case analysis in the definition of syn below. syn(p_{1}, p_{2}) = CC(K, p_{1}, p_{2}); the cases covered by K : (HA × HA) ⇒ A are summarised in the symmetric Table 3 where

• com : N × N × A × A ⇒ A is com(x, y, p, q) = M(x, y, tau(par(p, q))), and • close : N × N × δA × δA ⇒ A is close(x, y, p′, q′) =

M(x, y, tau(R(δ par (p′, q′)))).

!in : N, (N ⇒ A) → A  replicated input
!out : N, N, A → A  replicated output
!bout : N, (N ⇒ A) → A replicated bound output
!tau : A → A  replicated internal action

are defined by recursion (but not mutual recursion) as follows: !in(a, f) = in(a, λb : N. par(fb,!in(a, f))). !out(a, b, p) = out(a, b, par(p,!out(a, b, p))). !bout(a, f) = bout(a, λb : N. par(fb,!bout(a, f))). !tau(p) = tau(par(p,!tau(p))).

Open interpretation. Given the interpretation/translation of the above term constructors it is straightforward to extend it to names and well-formed processes following the paradigm of categorical logic. For a name a ∈ V, O[[V ⊢ a]] is the obvious projection N^{|V |} \underrightarrow{.} N in C^{I}. For a process P ∈ Pr_{V}, O[[V ⊢ P]] is a morphism N^{|V |} \underrightarrow{.} A in C^{I} defined by induction on the structure of P. For example,

O[[V ⊢ P_{1} | P_{2}]] =^{def} par ∘ ⟨O[[V ⊢ P_{1}]], O[[V ⊢ P_{2}]]⟩

and O[[V ⊢ a(b). P]] =^{def} in ∘ ⟨O[[V ⊢ a]], λ O[[V, b ⊢ P]]⟩.

Closed interpretation. Bisimulation cannot correspond to the above interpretation, because the operational semantics considers free names of a process semantically different. In the denotational semantics this requirement can be captured smoothly by exploiting the functor category structure and adopting a closed interpretation such that for V with | V | = n, C[[V ⊢ a]] ∈ N(n) = n and C[[V ⊢ P]] ∈ A(n). Then the closed interpretation is defined in terms of the open interpretation: C[[V ⊢ ]] =^{def} O[[V ⊢ ]]_{n}(0, …, n−1). It

x_{2} : N, f_{2} : N ⇒ A  x_{2} : N, y_{2} : N, q_{2} : A  x_{2} : N, q′_{2} : δA  q_{2} : A
x_{1} : N, f_{1} : N ⇒ A  nil  com(x_{1}, x_{2}, f_{1}(y_{2}), q_{2}) close(x_{1}, x_{2}, (δ f_{1} new), q′_{2}) nil
x_{1} : N, y_{1} : N, q_{1} : A  com(x_{2}, x_{1}, f_{2}(y_{1}), q_{1})  nil  nil  nil
x_{1} : N, q′_{1} : δA close(x_{2}, x_{1}, (δ f_{2} new), q′_{1})  nil  nil  nil
q_{1} : A  nil  nil  nil  nil

Table 3. K : (HA × HA) ⇒ A

is then possible to prove that the close interpretation is compositional on all constructs but input. For instance, for parallel composition: C[[V ⊢ P_{1} | P_{2}]] = par_{|V |}(C[[V ⊢ P_{1}]], C[[V ⊢ P_{2}]]). The clause for input cannot be purely compositional because late bisimulation is not preserved by this operator but, for V ≡ a_{0}, …, a_{n−1}, we have C[[V ⊢ a(b). P]] = in_{n}(C[[V ⊢ a]], ⟨C[[V ⊢ P {a^{i}/b}]]⟩_{i∈n}, C[[V, b ⊢ P]]). A straightforward consequence of naturality is that the induced semantics is preserved by renaming; i.e. for b ∉ V, a,

C[[V, a ⊢ P]] = C[[V, b ⊢ P {b/a}]]  (3)

2.5 Examples of denotational validity

To see the denotational machinery at work, we validate the semantic counterpart of the following three laws for late congruence:

Syn1 P ∥ Q = Q ∥ P
Syn2 x(u). P ∥ \overline{y}(v). Q =

[x = y]τ. νz (P {z/u} | Q{z/v}), if z ∉ fn(P, Q)

R1  νx \overline{z}(y). P = \overline{z}(y). νx P, if x ∉ \{y, z\}

(Syn1) For p, q : A, we have that CC(K, p, q) = CC(K, q, p) by (2) because K is symmetric (i.e. K = K ∘ ⟨π_{2}, π_{1}⟩). Hence syn(p, q) = syn(q, p) and then also par(p, q) = sum(lm(p, q), lm(q, p), syn(p, q)).

Notice below how in translating the laws into the metalanguage π-bindings become λ-bindings; whilst substitutions become applications.

(Syn2) For x, y : N and p, q : N ⇒ A,

syn(in(x, p), bout(y, q))

= syn(S_{1}(x, p), S_{3}(y, δ q new))
= close(x, y, δ p new, δ q new)
= M(x, y, tau(R(δ par (δ p new, δ q new))))
= M(x, y, tau(R(δ (λz : N. par(pz, qz)) new)))
= M(x, y, tau(res(λz : N. par(pz, qz)))).

(R1) For z : N and p : N × N ⇒ A,

res(λx : N. bout(z, λy : N. p(x, y)))

= R(δ (λx. S_{3}(z, δ (λy. p(x, y)) new)) new) = R(S_{3}(δ z, δ (λx. δ (λy. p(x, y)) new) new)) = S_{3}(z, δ R (swap(δ (λx. δ (λy. p(x, y)) new) new))) = S_{3}(z, δ R (δ (λy. δ (λx. p(x, y)) new) new)) , by (1) = S_{3}(z, δ (λy. R(δ (λx. p(x, y)) new)) new) = S_{3}(z, δ (λy. res(λx. p(x, y))) new) = bout(z, λy : N. res(λx : N. p(x, y))).

3 Full abstraction

This section contains the main results of our study.

Theorem 3.1 (Universality of the set-theoretic interpretation) In the set-theoretic interpretation of finite agents, writing A_{0} ∈ Set^{I} for the object of agents

1. C[[V ⊢ ]] establishes a bijective correspondence CN F_{V} ≅ A_{0}( |V | ), and so

2. for every finite P, Q ∈ Pr_{V}, P ∼ Q iff C[[V ⊢ P]] = C[[V ⊢ Q]].

Proof: A_{0} is the least solution in Set of the following system of domain equations (with n ∈ | I | )

X_{n} = 𝕄 (n×X_{n}^{n}×X_{n+1} + n×n×X_{n} + n×X_{n+1} + X_{n})

where 𝕄 is the free-semilattice monad.

So A_{0}( |V |) is a set of finite labelled trees, each tree representing an equivalence class of N F_{V} modulo the equational laws stating that (0, +) is a semilattice.

Theorem 3.2 (Finite full abstraction of the close domain-theoretic interpretation) In the domain-theoretic interpretation, for every finite P, Q ∈ Pr_{V}, P ∼ Q iff C[[V ⊢ P]] = C[[V ⊢ Q]].

Proof: Let 𝕄 be the free-semilattice monad, ℙ Abramsky’s powerdomain monad, and H the endofunctor HX = N × (N⇒X) + N × N × X + N × δX + X.

The domain equations X_{0} = 𝕄 (HX_{0}) and X = ℙ (HX) have initial solutions in Cpo^{I}, say A_{0} and A respectively. Moreover, it can be shown that A_{0} is the set-theoretic interpretation (ordered by equality), A has an 𝕄 H-algebra structure, and the unique 𝕄 H-homomorphism e : A_{0} → A is an embedding (with a partial projection as right adjoint). Therefore, the domain-theoretic interpretation of a finite agent is the image via e of the set-theoretic interpretation and, since e is monic, the two interpretations make the same identifications.

Such an easy transfer of finite full abstraction from a set-theoretic to a domain-theoretic model relies crucially on extending H to partial morphisms; this is possible for the endofunctor V ⇒ , only when V is of a very simple nature.

Theorem 3.3 (Full abstraction of the close domain-theoretic interpretation) In the domaintheoretic interpretation, for every P, Q ∈ Pr_{V}, P ∼ Q iff C[[V ⊢ P]] = C[[V ⊢ Q]].

Proof: We highlight the main steps of the proof. First, we prove that ∼ coincides with ⋂_{n} ∼^{n}, where ∼^{n} is the n-th approximant of ∼ (i.e. only the first n actions of the processes are observed). This, which is similar to the stratification result for strong bisimilarity for CCS finitely branching processes, holds because, modulo α-conversion, the transition system of any π-calculus process is finitely branching.

Second, we introduce a key ingredient: a system A_{π} of axioms and inference rules on π-calculus processes which allows to rewrite a process P ∈ Pr_{V} into an expanded form up to level n, say Exp_{V}^{n} (P); that is, a syntactic form where the operators of parallel composition, restriction and replication can only occur underneath n prefixes.

Third, using the approximants {∼^{n}}_{n} and the operational validity of the laws in the system A_{π} we can convert the bisimilarity between any pair of processes (P, Q) into the bisimilarity between a set {(Nil_{V}^{n} (P), Nil_{V}^{n} (Q)) | n ∈ ω} of pairs of processes in normal form. Nil_{V}^{n} (P) is obtained from Exp_{V}^{n} (P) by replacing the subprocesses underneath n prefixes with 0.

Having normal forms, we can apply the finite full abstraction Theorem 3.2, therefore Nil_{V}^{n} (P) and Nil_{V}^{n} (Q) are bisimilar iff their closed interpretations are equal. To conclude the proof, we have to establish the denotational counterpart of the previous steps, obtained by replacing ∼ with semantic equivalence.

The processes P and Exp_{V}^{n} (P) are semantically equivalent, because the laws in A_{π} are semantically valid. Technically, this is the most delicate point and we discuss it after this proof.

By continuity and the semantic validity of the laws in A_{π} we can convert semantic equivalence between P and Q into the semantic equivalence of their syntactic approximations Bot_{V}^{n} (P) and Bot_{V}^{n} (Q). Bot_{V}^{n} (P) is obtained from Exp_{V}^{n} (P) by replacing the subprocesses underneath n prefixes with ⊥ (a new constant representing the least element in the semantic domain).

With some simple considerations one can show that for any P, Q ∈ Pr_{V}, Bot_{V}^{n} (P) and Bot_{V}^{n} (Q) are semantically equivalent iff Nil_{V}^{n} (P) and Nil_{V}^{n} (Q) are.

We now comment on A_{π} and its semantic validation. In A_{π}, the axioms for sum, restriction and conditionals are those used in [16] or [19] for axiomatising π-calculus late bisimilarity, and include the semilattice axioms for nil and sum, and distributivity axioms for restriction like R1 (Section 2.5) and νa (P + Q) = νa P + νa Q. We need one axiom for each form of replication, like !\overline{a}b. P = \overline{a}b. (P | !\overline{a}b. P). To have a finite set of axioms for parallel composition, we use the auxiliary operators left merge and synchronisation. This yields 12 axioms, among which Syn1 and Syn2 (Section 2.5) and Par (Section 1). The inference rules are those for equivalence and the congruence rules for prefixing, sum, restriction, left merge and synchronisation. However, since late bisimulation is not preserved by input prefix, the inference rule for input is

\frac{∀ i ∈ n. P \{a^{i}/b\} = Q\{a^{i}/b\} P = Q}{a(b). P = a(b). Q}

with the proviso fn(a(b). P, a(b). Q) = {a_{0}, …, a_{n−1}}. The statement of validation of the laws says that for all P, Q ∈ Pr_{V}, if A_{π} ⊧ P = Q then C[[V ⊢ P]] = C[[V ⊢ Q]], and the proof is by induction on the depth of the derivation of A_{π} ⊧ P = Q. Examples of validation of axioms have been given in Section 2.5.

Because of the link between open and closed interpretation in the functor category C^{I}, it is easy to get a full-abstraction result for late congruence from one for late bisimulation (and conversely).

Corollary 3.4 (Full abstraction of the open domain-theoretic interpretation) In the domaintheoretic interpretation, for P, Q ∈ Pr_{V}, P ∼^{c} Q iff O[[V ⊢ P]] = O[[V ⊢ Q]].

Distinctions and constraints. We briefly mention the extension of our theory to distinctions and constraints. In the π-calculus, it is possible to define bisimilarity equivalences in between late bisimilarity and congruence, using distinctions [16]. These are conjunctions of inequalities between names which must be respected in any use of the processes. Guided by the denotational model, we have generalised distinctions to constraints, roughly decidable properties on finite tuples of names. Constraints are more expressive than distinctions, in that they allow us to express more refined forms of process bisimilarities. In particular, for any pair of processes there is an optimal constraint which expresses the necessary conditions on names under which the processes are behaviourally equivalent. Full abstraction for bisimilarity under constraint follows as a corollary of full abstraction for late bisimilarity (Theorem 3.3); the proof is similar to that for the open interpretation (Corollary 3.4).

4 Conclusions and future work

The denotational model is superior to the operational approach in revealing a few basic properties of ∼ and ∼^{c}. For instance, the invariance of ∼ under injective substitutions is a straightforward consequence of (3); and the congruence properties of ∼ and ∼^{c} (e.g. that ∼^{c} is preserved by all operators, and that ∼ is preserved by all operators but input) follow directly from the definitions of O[[ ]] and C[[ ]].

The denotational model is also interesting for proving basic laws of the operators of π-calculus, like associativity of parallel composition and the extrusion law for restriction “νa (P | Q) ∼^{c} P | νa Q if a ∉ fn(P)”. The operational proofs of these laws in [16] require some ingenuity (e.g. the “bisimilarity up to bisimilarity and up to restriction” technique). For an idea of how these proofs may be carried over in the denotational model, see the validation of laws in Subsection 2.5.

Guarded replication. In our π-calculus syntax the plain replication !P has been replaced by a guarded replication !α. P. This simplification is justified by the laws of π-calculus strong bisimilarity [23] and allows us to avoid the issue of divergence. For instance, with plain replication a denotational semantics would validate !0 = ⊥, whilst bisimulation validates !0 = 0.

Matching/mismatching. For describing the canonical forms induced by our model and hence to obtain the universality Theorem 3.1 we need both matching and mismatching —operators whose theoretical and pragmatical relevance for π-calculus is often debated. The importance of these constructs for equational reasoning had already been expressed in [19].

The metalanguage. We have factored the denotational semantics for the π-calculus through a metalanguage suggested by model-theoretic considerations.

The metalanguage can easily cope with operators not in the π-calculus syntax. For instance, interrupt operators like those in LOTOS [7], which are not definable in the π-calculus —even up to weak bisimulation. An interesting direction of research is to turn the metalanguage into a typed higher order process calculus, with an operational semantics and notion of bisimulation conservatively extending those of the π-calculus.

The translation of the π-calculus in the metalanguage uses a type of agents A = ℙ (HA), where ℙ is Abramsky’s powerdomain monad and H is an endofunctor corresponding to the action capabilities. It is conceivable to replace ℙ with some other monad and H with some other endofunctor. This flexibility allows to accommodate smoothly other languages, e.g.

• to deal with global variables one should replace ℙ with the monad 𝕋X =^{def} ℙ (X × S)^{S}, where S is an object of states;

• to deal with the πI-calculus [24] (a symmetric subcalculus of π-calculus where the free-output construct is forbidden and hence only private names can be exchanged), one should use the endofunctor HX =^{def} N × δX + N × δX + X. This gives a fully abstract model for πI-bisimilarity; the proof mimics the one outlined in Section 3.

In particular, by changing H we can define a denotational semantics in Cpo^{I} for languages ranging from pure CCS to Higher-Order π-calculus (HOπ) [22], along the lines outlined for the π-calculus.

Also the proof of full abstraction is fairly reusable. It copes with the polyadic π-calculus (where several names can be sent at once) and value-passing CCS (with binary sums and guarded recursion), provided the set of values is finite; but it cannot cope with HOπ and CCS with infinite-value passing.

We have obtained full abstraction with respect to a simple minded domain-theoretic model (in comparison to other categories proposed for Algol-like languages). The main problem to get full abstraction results for domain-theoretic models is not local names and mobility, but higher order! In fact, simple domain-theoretic models cannot achieve full abstraction for PCF nor for the λν-calculus (a CBV λ-calculus whose base types are bool and unit ref, see [20]). Therefore, to get full abstraction results for higher-order calculi with static binding, like Plain CHOCS [26] and HOπ, one should consider more refined models (probably based on game semantics [2, 14]). Thomsen [26], Hennessy [11], and Jeffrey [15] have given denotational models for higherorder process calculi with dynamic binding. But their constructions cannot account for calculi based on static binding like the π-calculus, Plain CHOCS, and HOπ.

Limits of our approach. Our semantics for π-calculus is a special case of a uniform approach to give semantics to a variety of calculi. However, this approach deals only with strong late bisimulation, which from a denotational point of view appears to be the simplest equivalence to handle (among those proposed for the π-calculus). We do not know how to capture denotationally other equivalences, namely early and open bisimulations (which differ from late bisimulation and congruence in the requirements on name instantiations) and weak bisimulations (where the internal actions of processes are partially ignored). The problem with weak bisimulations is not specific to the π-calculus semantics as there is no established domain-theoretic model for weak bisimulation even in pure CCS.

References

[1] S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.

[2] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF (extended abstract). In M. Hagiya and J.C. Mitchell, editors, Proceedings, Theoretical Aspects of Computer Software. International Symposium TACS’94, volume 789 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

[3] S. Abramsky and A. Jung. Domain theory. In Handbook of Logic in Computer Science. Oxford University Press, 1994.

[4] L. Aceto and A. Ingólfsdóttir. CPO models for a class of GSOS languages. In Proceedings, TAPSOFT’95, volume 915 of Lecture Notes in Computer Science. Springer-Verlag, 1995.

[5] S.O. Anderson and A.J. Power. A representable approach to nondeterminism. Manuscript, 1993.

[6] J. Baeten and W. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.

[7] T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. In P.H.J. van Eijk, C.A. Vissers, and M. Diaz, editors, The Formal Description Technique LOTOS. North Holland, 1989.

[8] P. Cenciarelli and E. Moggi. A syntactic approach to modularity in denotational semantics. In Proceedings, CTCS-5 (Category Theory and Computer Science Fifth Biennial Meeting), pages 9–12. CWI, September 1993.

[9] M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, Department of Computer Science, University of Edinburgh, 1994. (To be published by Cambridge University Press in the Distinguished Dissertations Series).

[10] M. Hennessy. A term model for synchronous processes. Information and Control, 51(1):58–75, October 1981.

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

[12] M. Hennessy and G. Plotkin. Full abstraction for a simple parallel programming language. In J. Becvar, editor, Proceedings, 8^{th} Symposium on Mathematical Foundations of Computer Science, volume 74 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

[13] M. Hennessy and G. Plotkin. A term model for CCS. In P. Dembinski, editor, Proceedings, 9^{th} Symposium on Mathematical Foundations of Computer Science, volume 88 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

[14] J.M.E. Hyland and C.-H.L Ong. Pi-calculus, dialogue games and PCF. In Proceedings, 7^{th} Annual ACM Conference on Functional Programming Languages and Computer Architecture. ACM, 1995.

[15] A. Jeffrey. A fully abstract semantics for a concurrent functional language with monadic types. In Proceedings, 10^{th} Annual IEEE Symposium on Logic in Computer Science, pages 255–264. IEEE Computer Society Press, 1995.

[16] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1–77, September 1992.

[17] E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991.

[18] F.J. Oles. Type algebras, functor categories and block structure. In M. Nivat and J.C. Reynolds, editors, Algebraic Methods in Semantics, 1985.

[19] J. Parrow and D. Sangiorgi. Algebraic theories for name-passing calculi. Information and Computation, 120(2):174–197, 1 August 1995.

[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 A.M. Borzyszkowski and S. Sokolowski, editors, Proceedings, MFCS’93, volume 711 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

[21] J. Rutten. Processes as terms: non-well-founded models for bisimulation. Mathematical Structures in Computer Science, 2:257–275, 1992.

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

[23] D. Sangiorgi. On the bisimulation proof method. Technical Report ECS–LFCS–94–299, LFCS, Department of Computer Science, University of Edinburgh, 1994. (A revised version is available via anonymous ftp from ftp.dcs.ed.ac.uk as

pub/sad/bis-proof.ps.Z).

[24] D. Sangiorgi. πI: A symmetric calculus based on internal mobility. In Proceedings, TAPSOFT’95, volume 915 of Lecture Notes in Computer Science. Springer-Verlag, 1995.

[25] M. Smyth and G. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal of Computing, 11(4):761–783, November 1982.

[26] B. Thomsen. Calculi for Higher Order Communicating Systems. PhD thesis, Department of Computing, Imperial College, 1990.