BRICS RS-97-52 P. Quaglia: On the Finitary Characterization of π-Congruences BRICS

Basic Research in Computer Science

On the Finitary Characterization of π-Congruences

Paola Quaglia BRICS Report Series RS-97-52 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/52/

On the finitary characterization of π-congruences

Paola Quaglia^{∗}

BRICS^{∗∗}, Aarhus University

Abstract

Some alternative characterizations of late full congruences, either strong or weak, are presented. Those congruences are classically defined by requiring the corresponding ground bisimilarity under all name substitutions.

We first improve on those infinitary definitions by showing that congruences can be alternatively characterized in the π-calculus by sticking to a finite number of carefully identified substitutions, and hence, by resorting to only a finite number of ground bisimilarity checks.

Then we investigate the same issue in both the ground and the non-ground πξ-calculus, a CCS-like process algebra whose ground version has already been proved to coincide with ground π-calculus. The πξ-calculus perspective allows processes to be explicitly interpreted as functions of their free names. As a result, a couple of alternative characterizations of π-congruences are given, each of them in terms of the bisimilarity of one single pair of πξ-processes. In one case, we exploit λ-closures of processes, so inducing the effective generation of the substitutions necessary to infer non-ground equivalence. In the other case, a more promising call-by-need discipline for the generation of the wanted substitutions is used. This last strategy is also adopted to show a coincidence result with open semantics.

By minor changes, all of the above characterizations for late semantics can be suited for congruences of the early family.

0 Introduction

The π-calculus [MPW92] is a by now well-known process algebra that allows the description of mobile systems. The calculus, that has been shown to have great flexibility and expressive power, exploits a name-passing interaction paradigm. Names, synonyms of channels, can be sent around and received, possibly changing the local/global acquaintances of the inputting process. For instance, conveying that \overline{x}z and x(y) stay, respectively, for an output and an input action at channel x, the following behaviour hold of process \overline{x}z.P | x(y).Q.

\overline{x}z.P | x(y).Q ⟶^{τ} P | Q\{z/y\}

∗Funded by the EU, under the Marie Curie TMR Programme. Address: BRICS, Dep. of Computer Science, Aarhus University, Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark.

email: quaglia@brics.dk.

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

Namely, the given process can perform a τ-action and then behave like P in parallel with the actual instance of Q where all the free occurrences of y have been replaced by z.

As the above transition highlights, name substitution has a fundamental role in the operational semantics of the calculus. This same influence is mirrored at the extensional level of bisimulation semantics, essentially due to the fact that substitutions can increase process move capabilities. For instance, unless the notion of name instantiation is moved inside the bisimulation definition itself (like, e.g., in the open semantics [San96]), bisimulation fails to be a congruence w.r.t. input action. The canonical example to see this is in terms of the interleaving interpretation of parallel composition, which equates the two processes (\overline{x} | y) and (\overline{x}.y +y.\overline{x}) (we are omitting unnecessary syntactic details). Each of the – either strong or τ-forgetting – late or early bisimulation semantics, hereby generically denoted by ˙≍, is such that

\begin{matrix}\overline{x} | y & ˙≍ & \overline{x}.y + y.\overline{x} \\ x(y).(\overline{x} | y) & ˙≭ & x(y).(\overline{x}.y + y.\overline{x}) \end{matrix}

The reason for the above inequivalence is that, whenever the leading input action x(y) causes y to be instantiated by x, the left-hand process x(y).(\overline{x} | y) can perform a τ-move that the right-hand agent is not able to match.

The usual way to extract a full congruence ≍ from the ground relation ˙≍ passes through a closure over name substitutions, so that classical definitions read as follows:

P ≍ Q iff P σ ˙≍ Qσ for all substitutions σ

Full congruences, also called non-ground relations, are pragmatically much more appealing than their ground duals. Though, the universal quantification over substitutions induces a prohibitive requirement to check in practice.

The main concern of this paper is to present alternative finitary characterizations of late, either strong or weak, π-calculus full congruences. A coincidence result with open semantics is also proved. Our investigation is carried on in both the π-calculus and the πξ-calculus, a generalization of the calculus appeared in [FMQ96].

As for π-calculus, by adequately classifying name substitutions, we show that P ≍ Q can be expressed in terms of a finite number of bisimilarity checks P σ ˙≍ Qσ, for carefully chosen substitutions σ.

Then we turn to the πξ-calculus, either retaining its ground form or defining a non-ground version of it. This allows us to provide a couple of alternative characterizations of late π-congruences as CCS-like bisimilarities [Mil89, HM85] of one suitable single pair of πξ-processes, either ground or non-ground.

The ground πξ-calculus was introduced with the intent of explicitly mirroring into a CCS-like setting the π-calculus meta-syntactic operation of substitution. The motivation for this being the possibility to easily export to the π-calculus some wellknow results about the automated verification and the mathematical theory (logical, axiomatic, and denotational) of CCS equivalences (see, e.g., [CPS93, HM85, ABV94, Abr91]). The main operational idea underpinning the πξ-calculus is to avoid to directly apply name substitutions to π-processes. An explicit component ξ is deemed to serve the same purpose. It acts as some kind of environment and represents associations among names. So, the generic πξ-process looks like ξ :: P, where P is an agent obtained by the usual π-calculus syntax added with abstraction prefixes ‘λy.’. These last prefixes, in turn, are used to associate a concrete operational counterpart to the name substitution occurring in the definition of the input clause of π-calculus bisimulations, whose strong late version reads like the following:

if P ⟶^{x(y)} P′ with y fresh, then there is Q′ such that

Q ⟶^{x(y)} Q′ and for all w, P′{w/y} is late bisimilar to Q′{w/y}

Remarkably, the operational interpretation of λ-abstraction prefixes ensures that input parameters can always be actualized by a finite number of names. So, except for the unguarded behaviour of the replication operator, πξ-processes can be modelled by finitely branching structures, which is generally not the case for data-dependent agents.

As we recalled, the main concern of the research leading to the πξ-calculus has been to figure out an operational setting which could support a standard CCS bisimulation semantics, both strong and observational. Precisely, the πξ-calculus operational semantics is defined as a two level transition system. The low level system leaves environments unaffected. It defines the relation P ⟶^{α,C} P′ where C makes explicit the requirements on names which are to be met in order for the symbolic step to be converted into a concrete move. The top level transition system is then defined by rules of the following shape

{P ⟶^{α,C} P′ \atop ξ :: P \begin{matrix}− \\ − \end{matrix}▷^{δ(ξ′,α,C)} ξ′ :: P′} ξ′ ∈ η(ξ, α, C) (△)

where the function η takes care of extending the environment ξ with the name associations activated by the symbolic transition P ⟶^{α,C} P′, while the function δ yields a concrete observable action. So, the extensional semantics of the calculus is given as standard strong and weak bisimulations and observational congruence.

In [FMQ95] and [FMQ96] it was shown that suitable distinct definitions of (△) and of the pair (η, δ) lead to the operational and axiomatic characterization of both late and early, either strong or weak, ground π-calculus semantics. The challenging issue of characterizing the corresponding full congruences was left open.

Here we fill that gap. We stress the correspondence between π-calculus name substitutions and πξ-calculus environments, and prove the claim that reasoning about non-ground semantics imposes to regard any π-calculus process as an actual function of its free names.

First, relying on the ground πξ-calculus, we show that suitable λ-closures of P and Q induce, in an effective way, the generation of those environments corresponding to the finite set of substitutions sufficient to infer P ≍ Q from the ground bisimilarities of P σ and Qσ. By this, we prove a coincide result with late strong and weak congruences, and corresponding axiomatic characterizations for finite processes.

Next, we argue that for strong semantics a similar result can be more efficiently achieved by adequately sophisticating the notion of environment and slightly modifying the top level transition system (△). This leads to the definition of the nonground version of the πξ-calculus. Such a calculus allows us to encode in a natural way a call-by-need strategy for the generation of the substitutions required to decide late full congruence. Finally, an analogous call-by-need instantiation discipline is used to provide an alternative characterization of open semantics.

By minor changes, all of the characterizations stated for late equivalence relations do hold for non-ground semantics of the early family [Qua96]. Also, by virtue of the peculiar πξ-calculus interpretation of input actions, those characterizations allow finite π-processes to be modelled by finite transition systems. So, our results could be particularly useful in the perspective of verifying mobile systems.

The rest of the paper is organized as follows. Section 1 and Section 2 contain the necessary background about π-calculus and ground πξ-calculus, respectively. In Section 3 we prove that each non-ground late semantics can be expressed as the conjunction of a finite number of corresponding ground bisimilarities. Building on this property, in Section 4 we characterize late π-congruences in terms of standard strong and weak bisimilarities of one single suitable pair of ground πξ-processes. In Section 5 non-ground πξ-calculus is introduced. Then, from a more promising perspective, yet another characterization of late strong non-groundness is stated, together with a coincidence result for open semantics. Eventually, Section 6 contains some concluding remarks. Also, Appendix A reports (minor modifications and extensions of) the encodings and constructions which appeared in [FMQ96] and are recalled to prove, in Appendix B, the characterization of open congruence.

1 The π-calculus

An overview of the π-calculus follows. Let N be a denumerably infinite set of names, ranged over by x, y, z, . . .. The syntax of π-calculus processes (ranged over by P, Q, …) is defined by the following grammar:

P ::= nil | x(y).P | \overline{x}y.P | τ.P | P + P | P | P | [x = y]P | (y)P | !P

Most of the operators resemble the corresponding CCS constructors [Mil80, Mil89]. The main exceptions are as follows. The matching operator [x = y]P is meant to test names for equality. The restriction operator (y)P declares y to be a new name for local use in P. The replication (or bang) operator ‘!’ is used to express infinite behaviours.

Prefixes x(y), \overline{x}y, and τ are called, respectively, bound input, free output, and silent (or internal, or unobservable) action. The adjective bound recalls that brackets act as formal binder, namely all of the free occurrences of y in P are bound by x(y) in x(y).P. Indeed, the restriction operator (y) in (y)P is another kind of formal binder. Prefix \overline{x}y is given the appellative of free as opposed to the bound output action \overline{x}(y). This last action is not available at the syntactic level, and denotes the ability to communicate at x the private name y. Either in x(y) or in \overline{x}y or in \overline{x}(y), the name x is said to be the subject, while y is called the object. Also, for the bound input x(y), the name y is sometimes referred to either as parameter or as placeholder.

If a name is not bound, it is called free. The set of names occurring free in the action α is written fn(α). Dually, the set of bound names is written bn(α). The set of names of the action α, written n(α), is defined to be the union of free and bound names. The unobservable action τ is such that n(τ) = ∅. Free and bound names of process P, denoted fn(P) and bn(P) respectively, are defined in the obvious way. Also, n(P) = fn(P) ∪ bn(P), and fn(P, Q) is sometimes used as a shorthand for fn(P) ∪ fn(Q).

The π-calculus operational semantics is defined inductively, in the style of [Plo81], by the rules shown in Tab. 1 together with additional symmetric rules for binary operators. Some of the rules, and in general most of the π-calculus theory, make use of the meta-syntactic operation of name substitution. Name substitutions (ranged

τ.P ⟶^{τ} P  x(y).P ⟶^{x(w)} P {w/y} w ∉ fn((y)P)

\overline{x}y.P ⟶^{\overline{x}y} P  {P ⟶^{α} P′ \atop [x = x]P ⟶^{α} P′}

{P ⟶^{α} P′ \atop P + Q ⟶^{α} P′}  {P ⟶^{α} P′ \atop P | Q ⟶^{α} P′ | Q} bn(α) ∩ fn(Q) = ∅

{P ⟶^{\overline{x}y} P′ Q ⟶^{x(z)} Q′ \atop P | Q ⟶^{τ} P′ | Q′\{y/z\}}  {P ⟶^{\overline{x}(w)} P′ Q ⟶^{x(w)} Q′ \atop P | Q ⟶^{τ} (w)(P′ | Q′)}

{P ⟶^{α} P′ \atop (y)P ⟶^{α} (y)P′} y ∉ n(α)  {P ⟶^{\overline{x}y} P′ \atop (y)P ⟶^{\overline{x}(w)} P′\{w/y\}} y ≠ x, w ∉ fn((y)P′)

{P |!P ⟶^{α} P′ \atop !P ⟶^{α} P′}

Table 1: the π-calculus operational semantics

over by σ, σ′, …) are functions from N to N defined almost everywhere as the identity. Sometimes, when the substitution σ differs from the identity for the names in {x_{1}, …, x_{n}}, σ is simply written {x_{1}σ/x_{1}, …, x_{n}σ/x_{n}}. The sets {x_{1}, …, x_{n}} and {x_{1}σ, …, x_{n}σ} are then referred to as domain and codomain of σ, written Dm(σ) and Im(σ), respectively. The term P σ denotes the process obtained from P by simultaneously substituting, for each x, any free occurrence of x in P by xσ, with change of bound names to avoid name clashes. We will use the symbol ≡_{α} to denote the relation of α-convertibility. Syntactic identity of P and Q will be written P ≡ Q.

Process operational behaviours are quotiented by strong or weak equivalence relations defined as bisimulation games. Distinct semantics have been defined, reflecting different strategies for the actual instantiation of names. For instance, depending on the assumed relative atomicity of the act of committing on the input channel and the act of instantiating the input placeholder, π-calculus bisimulation semantics naturally split into early and late families [MPW92].

Late semantics give input actions a functional operational intuition. When inputting, a process becomes a function of the actual transmitted name. So, the input clauses of late bisimulation games claim that the derivatives of the inputting processes continue to simulate each other for all the possible instantiations of the formal parameter. In the following, as usual, we let ⟹ be the reflexive and transitive closure of ⟶^{τ}, the labelled relation ⟹^{α} be ⟹⟶^{α}⟹, and \underrightarrow{α̂} be ⟹ if α = τ, ⟹^{α} otherwise.

Definition 1 Let S be a binary symmetric relation over π-calculus processes. Then - S is a strong late ground bisimulation if P S Q implies that

- if P ⟶^{α} P′ with α ≠ x(y) and bn(α) ∉ fn(P, Q), then for some Q′,

Q ⟶^{α} Q′ and P′ S Q′

- if P ⟶^{x(y)} P′ with y ∉ fn(P, Q), then for some Q′, Q ⟶^{x(y)} Q′ and, for all w, P′{w/y} S Q′{w/y}

- S is a weak late ground bisimulation if P S Q implies that

- if P ⟶^{α} P′ with α ≠ x(y) and bn(α) ∉ fn(P, Q), then for some Q′, Q \underrightarrow{α̂} Q′ and P′ S Q′

- if P ⟶^{x(y)} P′ with y ∉ fn(P, Q), then for some Q′, Q ⟹⟶^{x(y)} Q′ and, for all w, P′{w/y} S Q′{w/y}

P is strong late ground bisimilar to Q, written P ˙∼_{L} Q, if P S Q for some strong late ground bisimulation S.

P is weak late ground bisimilar to Q, written P ˙≈_{L} Q, if P S Q for some weak late ground bisimulation S.

P is weak late ground equal to Q, written P ˙≃_{L} Q, iff P ˙≈_{L} Q and whenever P ⟶^{τ} P′ then for some Q′, Q ⟹^{τ} Q′ with P′ ˙≈_{L} Q′, and symmetrically. □

A couple of observations about the previous definition are worth noticing. First, the input clause of weak late ground bisimilarity breaks down the double arrow of the usual CCS definition of weak bisimilarity. Nevertheless, the claim of instantiating y just after the input move is not surprising if we think again of the late functional intuition about input steps. Interpreting the derivative processes P′ and Q′ as functions of y, requires the bisimilarity of P′{w/y} and Q′{w/y} for all w, without giving Q′ the opportunity of silently slip to a distinct function. Second, weak late ground bisimilarity is not preserved by non-deterministic context. Analogously to the CCS case, to guarantee substitutivity in those contexts, weak late ground equality requires each initial silent action to be matched by at least one unobservable move.

All the above late behavioural relations are equivalences, but neither of them is preserved by substitution of names, and then by input prefix. For instance, process P ≡ [x = y]\overline{x}x. nil, having no outgoing transition, is either bisimilar or equal, in each of the above senses, to the inactive process nil. This is no longer true after substituting x for y in P, and hence when checking, e.g., the corresponding equivalence of x(y).P and x(y). nil.

Indeed, as it is common in the π-calculus literature, the adjective ground, together with the use of a dotted relational symbol, stays just to recall that the actual equivalences are not preserved by substitution of names. Such a propriety is achieved by requiring bisimilarity over all name substitutions, so getting the following relations, sometimes called non-ground bisimilarities.

Definition 2 Let P and Q be π-calculus processes. Then P and Q are

- strong late bisimilar, written P ∼_{L} Q, if P σ ˙∼_{L} Qσ for all substitutions σ

- weak late bisimilar, written P ≃_{L} Q, if P σ ˙≃_{L} Qσ for all substitutions σ Also, we write P ≈_{L} Q, if P σ ˙≈_{L} Qσ for all substitutions σ. □

As far as the definition of ≈_{L} is concerned, notice that, although preserved by name substitutions, this equivalence, just as its ground version, is not preserved by non-deterministic context.

In the following, unless otherwise stated, we will always refer to bisimilarities of the late family, so the adjective ‘late’ will be freely omitted. Further omissions will be those of unnecessary syntactic details, like, e.g., trailing . nil’s.

2 The ground πξ-calculus

This section provides an overview of the ground πξ-calculus, a generalization of the calculus appeared in [FMQ96]. Also, some coincidence results with ground πcalculus semantics are collected. In Appendix A, we report the main constructions and encodings needed to prove those results, and we comment on which extent the actual proofs differ from those presented in [FMQ96]. For complete details the reader is referred to [Qua96].

In the πξ-calculus, processes (ranged over by S, S_{1}, …) are written ξ :: P. The right component of the state operator ‘ :: ’ is (essentially) a π-calculus process, while ξ keeps track of the associations among names carried out in the past of the ongoing computation. Name substitutions are never applied to the right component of ξ :: P. Hence ξ can be viewed as an environment giving the actual associations of names. The syntax of the right component of the process ξ :: P is formally defined as follows.

P ::= nil | x(y).P | λy.P | \overline{x}y.P | τ.P | P + P | P | P | [x = y]P | (y)P | !P

Also, we assume that there is no homonymy either among bound names or among free and bound names of P. This assumption, that amounts to reason up to αconversion, could be easily fulfilled by using an indexing mechanism a là De Bruijn. But for this requirement on names, prefixes λy, which act as formal binders, are the only novelty w.r.t. either the π-calculus syntax or the process algebra presented in [FMQ96]. For the sake of convenience, in spite of new prefixes, we will often refer to the right component of any πξ-calculus process as to π-calculus process. The operational role of λ-prefixes is to call for an actual instantiation of the formal parameter y. In the calculus appeared in [FMQ96], an analogous observable result was obtained by means of more complex environments ξ. The introduction of λ-prefixes allows to simplify the semantic model in [FMQ96] and most of the constructions and intermediate results needed to prove characterization theorems.

The operational semantics of the πξ-calculus follows the SOS style and is based on a two-stage approach. The first stage consists of the definition of a symbolic semantics where transition labels record requirements on names. The evaluation of those requirements is then the main concern of the top level transition system.

The symbolic operational semantics is given by the axioms and rules reported in Tab. 2 together with symmetric rules for choice and asynchronous parallel composition. At this first operational level, requirements on names are not checked and name instantiation is not applied to processes, but rather recorded by transition labels (ranged over by ω, ω′, …). Labels are pairs of the form ⟨α, C⟩: the first component is essentially an action in the same sense of the π-calculus; the second component, called obligation, is a logical formula that codes requirements on names.

τ.P ⟶^{⟨τ,true⟩} P  \overline{x}y.P ⟶^{⟨\overline{x}y,x↓⟩} P
x(y).P ⟶^{⟨x(y),x↓⟩} P  λy.P ⟶^{⟨[y],true⟩} P

{P ⟶^{ω} P′ \atop [x = y]P ⟶^{μ_{y}^{x}(ω)} P′}  {P ⟶^{ω} P′ \atop P + Q ⟶^{ω} P′}

{P ⟶^{ω} P′ \atop P | Q ⟶^{ω} P′ | Q}  {P ⟶^{ω} P′  Q ⟶^{ω′} Q′ \atop P | Q ⟶^{ω∥ω′} P′ | Q′}

{P ⟶^{ω} P′ \atop (y)P ⟶^{o_{y}ω} P′}  {P ⟶^{ω} P′ \atop (y)P ⟶^{ν_{y}ω} (y)P′}

{(P)^{dec 0} |!(P)^{dec 1} ⟶^{ω} P′ \atop !P ⟶^{ω} P′}

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

μ_{y}^{x}⟨α, C⟩ = ⟨α, C ∧ x = y⟩

⟨α_{1}, C′_{1}⟩ ∥ ⟨α_{2}, C′_{2}⟩ = \{ \begin{matrix}⟨τ[y/w], C_{1} ∧ C_{2} ∧ x = z⟩ & if α_{1} ∈ \{\overline{x}y, \overline{x}(y)\}, C′_{1} = C_{1} ∧ x↓ \\ & and α_{2} = z(w), C′_{2} = C_{2} ∧ z ↓ \\ & or symmetrically \\ ⟨τ, false⟩ & otherwise \end{matrix}

ν_{y}⟨α, C⟩ = \{ \begin{matrix}⟨α, C ∧ y ≠ z⟩ & if α = \overline{x}z \\ ⟨α, C⟩ & otherwise \end{matrix}

o_{y}⟨α, C⟩ = \{ \begin{matrix}⟨\overline{x}(z), C ∧ y = z⟩ & if α = \overline{x}z \\ ⟨α, false⟩ & otherwise \end{matrix}

Table 2: symbolic operational semantics

The execution of the new prefixes λy results in the actions [y] which, although resembling the concretions of [Mil92], have no counterpart in the monadic π-calculus. Also, differently from the π-calculus, communication is characterized by a single inference rule. More precisely, we avoided to use the so-called Close rule which describes the communication of a private name and causes a restriction to appear

(P)^{dec a} = case P in

                               nil : nil

τ.P_{1} : τ.(P_{1})^{dec a}
\overline{x}y.P_{1} : \overline{x}y.(P_{1})^{dec a}
x(y^{(s)}).P_{1} : x(y^{(s·a)}).(P_{1}{y^{(s·a)}/y^{(s)}})^{dec a}
λy^{(s)}.P_{1} : λy^{(s·a)}.(P_{1}{y^{(s·a)}/y^{(s)}})^{dec a}
[x = y]P_{1} : [x = y](P_{1})^{dec a}
P_{1} + P_{2} : (P_{1})^{dec a} + (P_{2})^{dec a}
P_{1} | P_{2} : (P_{1})^{dec a} | (P_{2})^{dec a}
(y^{(s)})P_{1} : (y^{(s·a)})(P_{1}{y^{(s·a)}/y^{(s)}})^{dec a}
!P_{1} : !(P_{1})^{dec a}

                        end case

Table 3: definition of ( )^{dec a}

on top of synchronizing processes. In the πξ-calculus the information about privacy of names is completely captured by environments. Before plunging processes into environments, we only impose a consistency requirement: no process must be allowed to commit on a link which is not known outside. To this end, the input and the output transition labels include the obligation x ↓. It actually demands for a delayed check against the privacy of channel x.

The non homonymy condition we assume on names has to dynamically hold for every expansion of the replicated process !P. So, decorated versions of P are used in the premise of the rule for the bang operator. This is meant to assure that any parallel copy of the agent P borns uniquely its bound names. The idea is to label bound names by superscripts and to expand, e.g., process !x(y).y into x(y^{(0)}).y^{(0)} |!x(y^{(1)}).y^{(1)}. To this purpose, we use y^{(s)} to indicate that the name y is superscripted by the finite string s of zeros and ones. Then y^{(s_{1})} ≠ y^{(s_{2})} whenever s_{1} ≠ s_{2}, while y is a short-hand for y superscripted by the empty string^{1}. We feel free to omit the indication of superscripts when it is clear from the context the identity of names. Function ( )^{dec a} is defined in Tab. 3, where s·a denotes the concatenation of the string s with a ∈ {0, 1}.

We now comment on environments, left components of πξ-processes. An environment is a set of equations on two distinct entities: names and constants. Constants are taken from a denumerably infinite set D that is ranged over by c, c_{1}, c_{2}, …, and disjoint from the set N of names. As we are dealing with π-calculus processes where there is no homonymy either among bound names or among free and bound names, we suppose that free and bound names of π-processes are taken from two disjoint, infinite, subsets of N, called N_{I} and N_{RT}, respectively. Similarly, we assume that the set of constants D is partitioned into two disjoint sets D_{I} and D_{RT}.

1We would like to thank Franck van Breugel for pointing out the misbehaviour of a previous decoration operator.

Definition 3 A ground environment ξ is an equivalence relation over N ∪ D which is:

- consistent: c_{i} ξ c_{j} implies c_{i} = c_{j}

- finitely active: the set {(a, b) | a ξ b and a ≠ b} is finite

Given an environment ξ, we denote by [a]_{ξ} the equivalence class of ξ containing a. Such a class is said to be undefined if D ∩ [a]_{ξ} = ∅, defined-by-constant – or shortly defined – otherwise. A constant c is active in ξ iff there exists y such that y ∈ [c]_{ξ}, it is inactive otherwise. The family of all ground environments is denoted by E, and the identity ground environment is denoted by Id_{E}. Let R_{1}, R_{2} be relations over N ∪ D. Then R_{1} + R_{2} is defined as the smallest equivalence relation including (R_{1} ∪ R_{2}). □

We will often refer to ground environments simply as to environments. Also, in view of the above mentioned consistency requirement, we will let ξ sometimes assume the reading of a partial function. Whenever (y ξ c), we will denote the constant c as ξ(y) and will say that the partial function ξ( ) is defined on y, denoted by ξ(y)↓. If ξ( ) is not defined on y, then we will write ξ(y)↑.

The coming definition identifies the environments where π-calculus processes are let start running.

Definition 4 Letting N ⊆ N_{I}, the initial ground environment ξ^{N} is defined as

ξ^{N} = Id_{E} +{(x, ı(x)) | x ∈ N}

where ı : N_{I} → D_{I} is a bijective mapping, and D_{I} ∩ D_{RT} = ∅ and D_{I} ∪ D_{RT} = D and N_{I} ∩ N_{RT} = ∅ and N_{I} ∪ N_{RT} = N. □

During the execution of a πξ-calculus process, the generation of fresh constants is needed. To this end, we assume the existence of the following suitable functions. Function allD : E ⟶ 2_{f}^{D} returns the finite set of all the constants which are active in its argument. Function newD : E ⟶ D_{RT} yields a constant which is inactive in its argument. Here we assume that newD only depends on the active run-time constants in the argument, so that whenever allD(ξ_{1}) ∩ D_{RT} = allD(ξ_{2}) ∩ D_{RT} the equality newD(ξ_{1}) = newD(ξ_{2}) does hold.

The late operational semantics of πξ-calculus processes is described by the inference rules of Tab. 4. Both rules allow to infer the behaviour of ξ :: P from a symbolic transition of P and the definition of the result and of the update function, δ and η respectively. The function δ yields the observable result out of the transition. The possibly many-valued function η takes care of extending the environment ξ with the name associations activated by the transition. In defining η, the satisfiability of the obligation C is checked by means of a specialized evaluation function. Whenever the requirements expressed by C are not met in the environment ξ, the application η returns the empty set, so that the πξ-calculus process at hand is unable to move.

The rule associated with symbolic inputs shows the first-class role of instantiation in the πξ-calculus. Correspondingly to the execution of the symbolic action x(y), the process ξ :: P evolves to the process ξ′ :: λy.P′ whose right component is an explicit function of the placeholder y. The next – compulsory – move of the

\begin{matrix}{P ⟶^{ω} P′  ω ≠ ⟨x(y), C⟩ \atop ξ :: P \begin{matrix}− \\ − \end{matrix}▷^{δ(ξ′,ω)} ξ′ :: P′} ξ′ ∈ η(ξ, ω) \\ {P ⟶^{⟨x(y),C⟩} P′ \atop ξ :: P \begin{matrix}− \\ − \end{matrix}▷^{δ(ξ′,⟨x(y),C⟩)} ξ′ :: λy.P′} ξ′ ∈ η(ξ, ⟨x(y), C⟩) \end{matrix}

Table 4: definition of \begin{matrix}− \\ − \end{matrix}▷

process ξ′ :: λy.P′ is the instantiation of the input parameter. Notice, in fact, that the operational description guarantees instantiations to have priority over any other action even when the inputting agent is, e.g., underneath a parallel composition.

The definition of the update and of the result function (η,δ) is reported in Tab. 5. In the definition of η, elements are coerced to be singleton sets. The first step in computing the update function η consists in checking the satisfiability of the obligation. If the obligation evaluates to false in the environment, then η results in the empty set. Otherwise, depending on the structure of the action α, the update function yields a set of environments obtained by possibly adding a pair to ξ. Any information about the privacy of names is consistently captured by environments at the top level. So, outputting the – syntactically – free name y may be the same as outputting a private name. Precisely, if ξ(y)↑ then η(ξ, \overline{x}y, C) is exactly the same as η(ξ, \overline{x}(y), C). It results into an environment where the name y is associated with a new constant.

One comment is in place for placeholder instantiations. Correspondingly to those actions, the function η yields as many environments as the possible choices of c in allD(ξ), plus a new constant. This corresponds to instantiate y with (possibly a superset of) all the free names of the process at hand, plus a new fresh one. The intuitive reason for this relies on the following. Given any π-calculus process P′, the agents P′{z/y} and P′{u/y} have analogous move potentials whenever z, u ∉ fn(P′). Precisely, either P′{z/y} or P′{u/y} have the same action capabilities as P′ has. As a consequence of the above observation, if P performs the input x(y) transforming into P′, then the relevant instantiations of y in P′{w/y} are given by those names w such that w ∈ fn(P′) ⊆ fn(P) ∪ {y}. Our definition of η(ξ, [y], C) is just meant to mimic those instantiations. The function allD(ξ) plays the role of fn(P) while newD(ξ) stays for the set {y}. Notice, however, that at any time during execution only finitely many constants are active. This implies that finite πξprocesses can be always represented by labelled trees which are finitely branching.

Consider now the result function δ. It yields either τ or the constant(s) associated with the relevant name(s). The parameter of the action x(y) is not relevant. When inputting, the process becomes a function of y and then depends on the actual instantiation of the placeholder. The parameter will become observable at the next step.

What is crucial here is that the result function δ computes concrete – vs. sym-

[[C]]ξ = case C in

                    true : tt
                   false : ff

x↓ : ξ(x)↓ ⟶ tt , ff
x = y : x ξ y ⟶ tt , ff
x ≠ y : x ξ y ⟶ ff , tt
C_{1} ∧ C_{2} : [[C_{1}]]ξ and [[C_{2}]]ξ

                end case

ηξαC = ¬[[C]]ξ ⟶ ∅, case α in
τ : ξ
τ[x/y] : ξ + (y, x)
\overline{x}(y), \overline{x}y : ξ(y)↓ ⟶ ξ, ξ + (y, newD(ξ))
x(y) : ξ
[y] : ⋃_{c∈(allD(ξ) ∪ newD(ξ))} ξ + (y, c)

                              end case

      δξαC = case α in

\begin{aligned}τ, τ[x/y] & : & τ \\ \overline{x}(y), \overline{x}y & : & \overline{ξ(x)}ξ(y) \\ x(y) & : & ξ(x) \\ [y] & : & [ξ(y)] \end{aligned}

                 end case

Table 5: definition of (η, δ)

bolic – labels (ranged over by ρ, ρ_{1}, …) which do not include obligations anymore. As a consequence, the operational behaviour of πξ-calculus processes can be quotiented by the usual CCS bisimulation equivalences [Par81, Mil83, HM85]. We recall those semantics, assuming, as usual, =▷ to be the reflexive and transitive closure

of \begin{matrix}− \\ − \end{matrix}▷^{τ}, and =▷^{ρ} to be =▷\begin{matrix}− \\ − \end{matrix}▷^{ρ}=▷, and ρ̂ ; =▷ to be =▷ if ρ = τ, =▷^{ρ} otherwise.

Definition 5 Let S be a binary symmetric relation over πξ-calculus processes. Then

- S is a strong bisimulation if S_{1} S S_{2} implies that

if S_{1} \begin{matrix}− \\ − \end{matrix}▷^{ρ} S′_{1} then for some S′_{2}, S_{2} \begin{matrix}− \\ − \end{matrix}▷^{ρ} S′_{2} and S′_{1} S S′_{2}

- S is a weak bisimulation if S_{1} S S_{2} implies that

if S_{1} \begin{matrix}− \\ − \end{matrix}▷^{ρ} S′_{1} then for some S′_{2}, S_{2} ρ̂ ; =▷ S′_{2} and S′_{1} S S′_{2}

S_{1} is strong bisimilar to S_{2}, written S_{1} ∼ S_{2}, if S_{1} S S_{2} for some strong bisimulation S.

S_{1} is weak bisimilar to S_{2}, written S_{1} ≈ S_{2}, if S_{1} S S_{2} for some weak bisimulation S.

S_{1} is weak congruent (or observational congruent) to S_{2}, written S_{1} ≈^{c} S_{2}, iff

S_{1} ≈ S_{2} and whenever S_{1} \begin{matrix}− \\ − \end{matrix}▷^{τ} S′_{1} then for some S′_{2}, S_{2} =▷^{τ} S′_{2} and S′_{1} ≈ S′_{2}, and

symmetrically. □

The finite fragment of the symbolic operational semantics of Tab. 2 (that is, all the rules but the one for the bang operator) fits in a simple generalization of the De Simone format [DS85] where labels of transitions are elements of an algebra with several operations rather than elements of a monoid of actions.

As a result of this, we can state a head-normalizing axiom system for the finite terms of the transition system in Tab. 2 by simply exploiting the procedure presented in [ABV94]. The first step of that procedure consists in breaking down, by means of auxiliary operators, each (so-called smooth and not distinctive) process constructor f whose operational behaviour is described by more than one inference rule. This equation expresses the behaviour of the constructor f as a sum of auxiliary operators, one for each inference rule characterizing f (e.g., (y)P = (ν_{y})P + (o_{y})P). The procedure goes on imposing distributive, action and inaction equations on smooth and distinctive operators. Distributive laws describe the interplay between the non-deterministic choice operator and the other operators (e.g., (ν_{y})(P + Q) = (ν_{y})P + (ν_{y})Q). Action laws describe the interactions of all the operators with prefixing. Here, we need to extend action laws to the case of the generalized prefixing ω.P. Action laws cause auxiliary operators to be pushed as deep as possible inside terms (e.g., (ν_{y})(ω.P) = ν_{y}(ω).(y)P). Finally, the so called inaction equations identify as the inactive process any expression having no outgoing transition (e.g., (ν_{y}) nil = nil). The axiom system A_{a} in Tab. 6 is the actual result of the application of the above procedure. The system has the main propriety of being head-normalizing, namely A_{a} allows any term P to be rewritten as a sum of prefixes.

Once its π-component has been reduced in head normal form, any finite πξ-agent can be transformed into a finite labelled tree by means of the laws of the system A_{L} of Tab. 6. Those axioms allow πξ-calculus processes to be rewritten into terms given by the following grammar

\begin{aligned}S & ::= & ξ :: P | ρ; S | S ⊕ S \\ ρ & ::= & τ | c | [c] | c_{1}c_{2} | \overline{c_{1}}c_{2} \end{aligned}

where P makes use of generalized action prefixes ω as explained above, and ‘;’ is a prefixing operator, and ‘⊕’ is a non-deterministic choice constructor. We assume that the empty summation ⨁_{∅} stays for the πξ-process ξ :: nil where ξ is intended to be some fixed environment, say the identity relation. Axioms C1′ −C4′ of system A_{L} are the usual monoidal laws for summation where, for arbitrary instantiations of the environment ξ, process ξ :: nil is a neutral element of the top level summation operator. Axioms U and V are the corresponding of the two operational rules which define the transition relation \begin{matrix}− \\ − \end{matrix}▷. Eventually, the D law describes the distributivity

A_{a} : (C1) P_{1} + P_{2} = P_{2} + P_{1}
(C2) (P_{1} + P_{2}) + P_{3} = P_{1} + (P_{2} + P_{3})
(C3) P + P = P
(C4) P + nil = P
(EX) P_{1} | P_{2} = P_{1} P_{2} + P_{2} P_{1} + P_{1} ∥ P_{2}
(R)  (x)P = (ν_{x})P + (o_{x})P
(A1) [x = y] ω.P = μ_{y}^{x}(ω).P
(A2) ω.P_{1} P_{2} = ω.(P_{1} | P_{2})
(A3) ω_{1}.P_{1} ∥ ω_{2}.P_{2} = (ω_{1} ∥ ω_{2}).(P_{1} | P_{2})
(A4) (ν_{x})(ω.P) = ν_{x}(ω).(x)P
(A5) (o_{x})(ω.P) = o_{x}(ω).P
(D1) [x = y](P_{1} + P_{2}) = [x = y]P_{1} + [x = y]P_{2}
(D2) (P_{1} + P_{2}) P = P_{1} P + P_{2} P
(D3) (P_{1} + P_{2}) ∥ P = P_{1} ∥ P + P_{2} ∥ P
(D4) P ∥ (P_{1} + P_{2}) = P ∥ P_{1} + P ∥ P_{2}
(D5) (ν_{x})(P_{1} + P_{2}) = (ν_{x})P_{1} + (ν_{x})P_{2}
(D6) (o_{x})(P_{1} + P_{2}) = (o_{x})P_{1} + (o_{x})P_{2}
(IN) [x = y] nil = (ν_{x}) nil = (o_{x}) nil = nil P = P ∥ nil = nil ∥ P = nil

A_{L} : (C1′) S_{1} ⊕ S_{2} = S_{2} ⊕ S_{1}
(C2′) (S_{1} ⊕ S_{2}) ⊕ S_{3} = S_{1} ⊕ (S_{2} ⊕ S_{3})
(C3′) S ⊕ S = S
(C4′) S ⊕ ξ :: nil = S
(U)  ξ :: ω.P = ⨁_{ξ′∈η_{L}(ξ,ω)} δ(ξ′, ω); (ξ′ :: P) if ω ≠ ⟨x(y), C⟩
(V)  ξ :: ⟨x(y), C⟩.P = ⨁_{ξ′∈η_{L}(ξ,⟨x(y),C⟩)} δ(ξ′, ⟨x(y), C⟩); (ξ′ :: ⟨[y], true⟩.P)
(D) ξ :: (P_{1} + P_{2}) = ξ :: P_{1} ⊕ ξ :: P_{2}

A_{w} : (T 1) ρ; τ; S = ρ; S
(T 2) S ⊕ τ; S = τ; S
(T 3) ρ; (S_{1} ⊕ τ; S_{2}) ⊕ ρ; S_{2} = ρ; (S_{1} ⊕ τ; S_{2})

Table 6: axiom systems A_{a}, A_{L}, A_{w} of the low level choice operator over the state construct ‘ :: ’. Notice that, while U and V are axiom schemata with an infinite number of possible instantiations, in every instantiation the summation ⊕_{ξ′} is extended only to a finite number of summands.

One comment relative to weak semantics is due. Referring to [Hen88], Luca Aceto discussed in [Ace94] the problems given raise by the interplay between the auxiliary constructs for expanding parallel compositions and the second Milner’s τ-law. Here the issue is completely avoided, as the ACP [BK84] merge operators are only used for the axiomatization A_{a} of the low level symbolic transition system, while Milner’s τ-laws, reported in Tab. 6 as A_{w}, are only adopted for the top level transition system.

The coming theorems deal with the characterization of ground π-calculus bisimilarities in terms of the CCS-like πξ-calculus semantics.

Theorem 6 Let ξ^{N} :: P and ξ^{N} :: Q be πξ-calculus processes with P and Q finite and such that N = fn(P, Q). Then

1. ξ^{N} :: P ∼ ξ^{N} :: Q iff A_{a}, A_{L} ⊢ ξ^{N} :: P = ξ^{N} :: Q

2. ξ^{N} :: P ≈^{c} ξ^{N} :: Q iff A_{a}, A_{L}, A_{w} ⊢ ξ^{N} :: P = ξ^{N} :: Q □

Theorem 7 (coincidence with late ground semantics) Let P, Q be π-calculus processes, and let N = fn(P, Q). Then

1. P ˙∼_{L} Q iff (ξ^{N} :: P) ∼ (ξ^{N} :: Q).

Also, if P and Q are finite, then P ˙∼_{L} Q iff A_{a}, A_{L} ⊢ ξ^{N} :: P = ξ^{N} :: Q

2. P ˙≈_{L} Q iff (ξ^{N} :: P) ≈ (ξ^{N} :: Q)

3. P ˙≃_{L} Q iff (ξ^{N} :: P) ≈^{c} (ξ^{N} :: Q).

Also, if P and Q are finite, then P ˙≃_{L} Q iff A_{a}, A_{L}, A_{w} ⊢ ξ^{N} :: P = ξ^{N} :: Q

□

The above results can be proven by minor changes to similar characterizations already appeared in [FMQ96]. The πξ-calculus, as presented here, differs from the semantic model introduced in [FMQ96] just for the explicit use of abstraction prefixes λy. Also, [FMQ96] only dealt with strong semantics. However the proofs of the weak clauses of both Th. 6 and Th. 7 do not present relevant difficulties w.r.t. the corresponding strong items. For instance, once the completeness of the axiom system (A_{a}, A_{L}) has been shown for strong semantics, the proof of Th. 6 requires to pass through a saturation lemma, just as it is the case in CCS [Mil89]. An analogous reasoning holds of Th. 7. There is a one-to-one correspondence between the τ-moves of π-processes and πξ-processes, therefore the characterization of weak semantics is not much more complex than that of strong.

The main concern of the coincidence proof is to define suitable encodings of π-calculus processes into πξ-calculus processes and vice-versa. We can comment on this point illustrating the idea that underlies the proof of

(ξ^{N} :: P) ∼ (ξ^{N} :: Q) implies P ˙∼_{L} Q.

Given a strong bisimulation S containing the pair (ξ^{N} :: P, ξ^{N} :: Q), it is a matter of encoding it into a late ground bisimulation, say T r(S), containing (P, Q). The construction is based on a translation of pairs of πξ-calculus processes into pairs of πagents. Starting from environments, the translation essentially generates the name substitutions to be applied to the π-component of πξ-processes. Given any pair in S, the key point is that the same constant in the environments of the paired processes has to be substituted by the same name. The observability of input parameter actualizations guarantees that S contains pairs of πξ-calculus processes where, once executed an input action, the respective placeholders have been instantiated in the same way. This exactly captures the flavour of the late bisimulation input clause.

For (P′, Q′) ∈ T r(S) and P′ ⟶^{x(y)} P′′, a π-calculus process Q′′ is shown to exist such

that Q′ ⟶^{x(y)} Q′′. Moreover, the relation T r(S) is proved to contain not only all the pairs (P′′{w/y}, Q′′{w/y}) but also (if any) all the pairs of the derivatives of theirs.

The encoding from πξ-calculus to π-calculus is somehow made complex by the structural differences between the two algebras. Translating constants into names and reconstructing the name substitutions coded by environments is not enough. One has as well to remove possible occurrences of leading λ-prefixes, and to recover the possible nesting of those restrictions whose occurrence has been syntactically ‘lost’ because of the use of one single CCS-like communication rule vs. the π-calculus dichotomy between the Close and the usual synchronization rule. Obviously, all these issue are reversed when encoding the π-calculus into the πξ-calculus.

Eventually, another subtle point is the characterization of the operational correspondence between the behaviours of processes which are the one encoding of the other. As it is natural, any proof of this kind can only be based on the syntactic structure of processes, and then, as far as the πξ-calculus is concerned, on the symbolic transition system at the first level. Nevertheless, the behaviour of πξ-calculus processes is ruled by a two level transition system where the top-level evaluation of the obligation C plays a significative role: a symbolic derivation for P may result in no move at all for the global process ξ : P. Hence, an actual operational correspondence between the two calculi can be faithfully captured only at the second level of the πξ-calculus. Also, contrary to πξ-calculus processes, in the π-calculus all of the bound names are always syntactically bound. So the π-inference of Q ⟶^{α} Q′ could pass through the application of a so-called Open rule which has no dual in any symbolic derivation of the πξ-calculus process corresponding to Q. Given any symbolic free output action of the πξ-calculus, there is no way to argue whether or not it is actually free till the environment is investigated in the top level transition system.

The above issues result in quite non standard theorems about the operational correspondence of processes of the two calculi, where, from the πξ-perspective, we are obliged to reason at the level of the symbolic πξ-calculus transition system and to simultaneously carry around inductive information about obligations and names to be used as look-aheads for the top level.

We end up this section with a last comment on Theorem 7. Essentially, an initial ground environment ξ^{N} codes the information that the names in N are all distinct the one from the other. So, comparing the behaviours of ξ^{N} :: P and ξ^{N} :: Q, with N = fn(P, Q), is the same as assuming that the names occurring free in both P and Q are, without exception, all distinct. This exactly captures the ground view which does not take into account that putting processes into arbitrary contexts might result in causing arbitrary equalities of names. Hence, not surprisingly, the bisimilarity of ξ^{N} :: P and ξ^{N} :: Q can only correspond to ground – vs. non-ground – π-calculus bisimilarity of P and Q. We will see in the following that, to capture the flavour of π-calculus non-groundness, either more generous πξ-processes, or a more abstract notion of environment is needed.

3 Limiting π-groundness checks

Let any of the relations in {∼_{L}, ≈_{L}, ≃_{L}} be denoted by the symbol ≍ and assume that ˙≍ stays for the corresponding ground relation. The equivalence ≍ is classically defined by closing ˙≍ over any name substitution, and hence by requiring an infinite number of ground bisimilarity checks. In the following we will show that P ≍ Q can be alternatively expressed in terms of a finite number of checks P σ ˙≍ Qσ for carefully chosen substitutions σ. In the next section, relying on particular features of the πξ-calculus, we will be able to effectively generate the set of name substitutions to be taken into account. The finitary characterization presented below is referred to semantics of the late family, though exactly the same result does hold for early relations [Qua96].

The universal quantification over substitutions in the definition of non-ground bisimilarities gives raise to a heavy requirement to check in practice. Nevertheless, not all of the infinite name substitutions are either always or equally relevant to infer process equivalence. Resorting to infinite checks would be undoubtly useless to infer, e.g., z(y) ≍ z(u). More generally, given an arbitrary process P and any name x ∉ fn(P), for all w it holds that P {w/x} ≡ P. Hence, a first simple improvement in checking P ≍ Q is to consider, rather than all the possible name substitutions, only those whose domains are given by the union of the free names of P and Q.

With some ingenuity, the number of necessary substitutions may be further on diminished. The relevant issue to be investigated here is how the application of name substitutions relates to possible changes in process move potentials. First, at least in the absence of a mismatching operator, substitutions do not decrease those potentials. Indeed, if a process R may execute an action α transforming into R′, then, up to α-equivalence, Rσ can perform ασ and become R′σ [MPW92]. However, as the coming example shows, substitutions may increase performance capabilities.

Example 8 Assuming x ≠ y, let R_{1} ≡ (\overline{x} | y) and σ_{x} = \{x/x, x/y\}. The parallel components of R_{1}σ_{x} may be involved in a communication which is forbidden to the subprocesses of R_{1}. A τ-move is equally possible for R_{1}σ_{y} for σ_{y} = {y/x, y/y}. More generally, given any substitution σ_{z} = {z/x, z/y}, a communication occurs between the subagents \overline{x}σ_{z} and yσ_{z} of R_{1}σ_{z}. □

Suppose to want to check the congruence of the two processes R_{1} and R_{2}, with R_{1} the same as in Ex. 8 and R_{2} such that fn(R_{1}, R_{2}) = {x, y}. We already know that comparable action capabilities are expected for the two processes R_{1}σ_{x} and R_{1}σ_{y}. This suggests that the bisimilarity of R_{1}σ_{x} and R_{2}σ_{x} might be related to that of R_{1}σ_{y} and R_{2}σ_{y} in a very precise sense. If so, then checking both of R_{1}σ_{x} ˙∼_{L} R_{2}σ_{x} and R_{1}σ_{y} ˙∼_{L} R_{2}σ_{y} would be superfluous. In the following we will show the claim that R_{1} ∼_{L} R_{2} can be inferred by choosing any pair of distinct names (w, u) and resorting to only two checks:

R_{1}{u/x, u/y} ˙∼_{L} R_{2}{u/x, u/y}  R_{1}{u/x, w/y} ˙∼_{L} R_{2}{u/x, w/y}

The comparability of the move potentials of the two processes R_{1}σ_{x} and R_{1}σ_{y} of Ex. 8 depends on the fact that either σ_{x} or σ_{y} map both x and y into the same target name. From this we gain the intuition that substitutions can be quotiented according to the way their domains are partitioned into subsets of names sharing the same image, no matter what such an image is.

Definition 9 The name substitution σ : N → N is said to represent the partition of N into the k disjoint and non-empty sets N_{1}, …, N_{k} iff ∀j, h ∈ {1, …, k} : j ≠ h, ∀x, y ∈ N_{j}, ∀z ∈ N_{h} it holds that xσ = yσ and xσ ≠ zσ. □

Given any ground behavioural equivalence ˙≍, our next goal is to prove that checking P σ ˙≍ Qσ is just the same as checking P σ′ ˙≍ Qσ′ whenever σ and σ′ represent the same partition of fn(P, Q). As auxiliary intermediate results, we prove statements on the relationship between the strong and the weak behaviour of P σ and P σ′ with σ and σ′ representing the same partition of fn(P). Since the substitutions σ_{x} = {x/x, x/y} and σ_{y} = {y/x, y/y} considered in Ex. 8 represent the same partition of {x, y} = fn(R_{1}), the coming lemmata actually formalize the intuitive comparability of the action potentials of R_{1}σ_{x} and R_{1}σ_{y}.

Lemma 10 Let σ, σ′ : N → N represent the same partition of fn(P). If P σ ⟶^{α} P_{1} with bn(α) ∉ fn(P σ, P σ′) and such that (bn(α))σ = (bn(α))σ′ = bn(α), then by an inference of equal depth P σ′ ⟶^{β} P_{2} where, for some action γ and some process P′ with fn(P′) ⊆ fn(P) ∪ bn(α), it holds that α ≡ γσ, β ≡ γσ′ and P_{1} ≡_{α} P′σ, P_{2} ≡_{α} P′σ′.

Proof: By induction on depth of inference. Each rule of the π-calculus transition system is considered in turn as the last rule applied. We show in the following only the more interesting cases, the others are either simpler or analogous. In particular, we suppose that the last rule applied in the inference of P σ ⟶^{α} P_{1} is either the input axiom or the communication rule.

(Inp) P ≡ x(y).R. Then, for z ∉ fn((y)R, Rσ) and such that zσ = z, it holds that P σ ≡_{α} xσ(z).R{z/y}σ. Analogously, for u ∉ fn((y)R, Rσ′) and such that uσ′ = u, it holds that P σ′ ≡_{α} xσ′(u).R{u/y}σ′. Suppose that α = xσ(w) with w = wσ = wσ′. Then

P_{1} ≡_{α} R{z/y}σ{w/z} ≡ R{z/y}{w/z}σ ≡ R{w/y}σ

by z = zσ and w = wσ. Also, by the hypothesis that w ∉ fn(P σ′) and by u = uσ′ and w = wσ′, it follows that

P σ′ ⟶^{xσ′(w)} P_{2} ≡_{α} R{u/y}σ′{w/u} ≡ R{w/y}σ′

Then the thesis, taking γ = x(w) and P′ ≡ R{w/y}.

(Com)

P ≡ R_{1} | R_{2} and α = τ. Then R_{1}σ ⟶^{\overline{xσ}zσ} R′_{1} and R_{2}σ ⟶^{yσ(w)} R′_{2} (or symmetrically)

where we can assume w fresh w.r.t. fn(R_{2}σ, R_{2}σ′) and such that w = wσ = wσ′ and where xσ = yσ and P_{1} ≡ R′_{1} | R′_{2}{zσ/w}

⟹ By ind. hyp. R_{1}σ′ ⟶^{\overline{xσ′}zσ′} R′′_{1} and R_{2}σ′ ⟶^{yσ′(w)} R′′_{2} with

\begin{aligned}R′_{1} & ≡_{α} & T_{1}σ & R′_{2} & ≡_{α} & T_{2}σ \\ R′′_{1} & ≡_{α} & T_{1}σ′ & R′′_{2} & ≡_{α} & T_{2}σ′ \end{aligned}

for some T_{1} and T_{2} such that fn(T_{1}) ⊆ fn(R_{1}) and fn(T_{2}) ⊆ fn(R_{2}) ∪ {w} ⟹ As σ and σ′ represent the same partition of fn(P), they also represent the same partition of fn(R_{1}, R_{2}) ⊆ fn(P). So, by xσ = yσ, it follows xσ′ = yσ′. Then

P σ′ ⟶^{τ} P_{2} with

P_{2} ≡ R′′_{1} | R′′_{2}{zσ′/w} ≡_{α} T_{1}σ′ | T_{2}σ′{zσ′/w} ≡ T_{1}σ′ | T_{2}{z/w}σ′

by w = wσ′ ⟹ The thesis, taking P′ ≡ T_{1} | T_{2}{z/w}. In fact

P_{1} ≡ R′_{1} | R′_{2}{zσ/w} ≡_{α} T_{1}σ | T_{2}σ{zσ/w} ≡ T_{1}σ | T_{2}{z/w}σ

by w = wσ. Also, fn(P′) = fn(T_{1}, T_{2}) \ {w} ⊆ fn(R_{1}, R_{2}). □

Lemma 11 Let σ, σ′ : N → N represent the same partition of fn(P). If P σ ⟹ P_{1} then by a derivation of equal length P σ′ ⟹ P_{2} where, for some process P′ with fn(P′) ⊆ fn(P), it holds that P_{1} ≡_{α} P′σ and P_{2} ≡_{α} P′σ′.

Proof: By induction on the length n (n ≥ 0) of the derivation of P_{1} from P σ. (base) For the base case P_{1} ≡ P σ, then simply take P′ ≡ P.

(step) Assume now that P σ ⟹ P_{1} ⟶^{τ} P′_{1} with the derivation P σ ⟹ P_{1} of length n > 0. ⟹ By ind. hyp. P σ′ ⟹ P_{2} with a derivation of n steps, and for some P′ it holds that P_{1} ≡_{α} P′σ and P_{2} ≡_{α} P′σ′ ⟹ By P_{1} ⟶^{τ} P′_{1} and by P_{1} ≡_{α} P′σ and by ≡_{α} ⊂ ˙∼_{L} it follows that P′σ ⟶^{τ} P′′_{1} ≡_{α} P′_{1} ⟹ As fn(P′σ) = fn(P_{1}) ⊆ fn(P σ) and fn(P′σ′) = fn(P_{2}) ⊆ fn(P σ′), the hypotheses of Lemma 10 are satisfied. By such a lemma P′σ′ ⟶^{τ} P′′_{2} where, for some P′′, it holds that P′′_{1} ≡_{α} P′′σ and P′′_{2} ≡_{α} P′′σ′

⟹ By P_{2} ≡_{α} P′σ′ it follows that P_{2} ⟶^{τ} P′_{2} ≡_{α} P′′_{2}. Hence the thesis, since P′_{1} ≡_{α} P′′_{1} ≡_{α} P′′σ and P′_{2} ≡_{α} P′′_{2} ≡_{α} P′′σ′. □

Given two substitutions σ, σ′ representing the same partition of fn(P, Q), the next theorem relates the ground (in)equivalence of P σ and Qσ to the (in)equivalence of P σ′ and Qσ′.

Theorem 12 Let σ, σ′ : N → N represent the same partition of fn(P, Q) and let ˙≍ ∈ { ˙∼_{L}, ˙≈_{L}, ˙≃_{L}}. Then P σ ˙≍ Qσ iff P σ′ ˙≍ Qσ′.

Proof: We first prove the result relative to strong semantics. To this end, let S = ⋃_{n} S_{n} where

S_{0} = ˙∼_{L}
S_{n+1} = { (P σ, Qσ) | P σ′ S_{n} Qσ′ and

σ, σ′ represent the same partition of fn(P, Q) }

We show that S is a strong late ground bisimulation by proving, by induction on n, that P S_{n} Q implies that - if P ⟶^{α} P′ with α ≠ x(y) and bn(α) ∉ fn(P, Q), then for some Q′, Q ⟶^{α} Q′

and P′ S Q′

- if P ⟶^{x(y)} P′ with y ∉ fn(P, Q), then for some Q′, Q ⟶^{x(y)} Q′ and, for all w,

P′{w/y} S Q′{w/y}

(base) By definition of S_{0}. (step) Assume n > 0 and suppose (P σ, Qσ) ∈ S_{n} by (P σ′, Qσ′) ∈ S_{n−1} and σ, σ′ representing the same partition of fn(P, Q). We only consider bound actions, the other cases are easier.

(bound output)

Suppose that P σ ⟶^{\overline{xσ}(y)} P_{1} with y ∉ fn(P σ, Qσ) ⟹ For some y′ ∉ fn(P σ, P σ′, Qσ, Qσ′) and such that y′ = y′σ = y′σ′, it holds that

P σ ⟶^{\overline{xσ}(y′)} P_{1}\{y′/y\}

⟹ By Lemma 10, P σ′ ⟶^{\overline{xσ′}(y′)} P_{2} with P_{1}\{y′/y\} ≡_{α} P′σ and P_{2} ≡_{α} P′σ′ for some

process P′ such that fn(P′) ⊆ fn(P) ∪ {y′}

⟹ By ind. hyp. it follows from (P σ′, Qσ′) ∈ S_{n−1} that Qσ′ ⟶^{\overline{xσ′}(y′)} Q_{2} with (P_{2}, Q_{2}) ∈ S

⟹ By Lemma 10, Qσ ⟶^{\overline{xσ}(y′)} Q_{1} with Q_{2} ≡_{α} Q′σ′ and Q_{1} ≡_{α} Q′σ for some Q′ such that fn(Q′) ⊆ fn(Q) ∪ {y′}.

⟹ By y ∉ fn(Qσ) it holds that Qσ ⟶^{\overline{xσ}(y)} Q_{1}\{y/y′\}. Hence the thesis (P_{1}, Q_{1}\{y/y′\}) ∈ S by

P_{1} ≡ P_{1}{y′/y}{y/y′}
≡_{α} P′σ{y/y′}
S Q′σ{y/y′}
≡_{α} Q_{1}{y/y′}

where (P′σ{y/y′}, Q′σ{y/y′}) ∈ S is justified by (P_{2}, Q_{2}) ∈ S, i.e. (P′σ′, Q′σ′) ∈ S. In fact, from y ∉ fn(P σ, Qσ) and y′ ∉ fn(P σ′, Qσ′) it follows the freshness of y and y′ w.r.t. the relevant codomains of σ{y/y′} and σ′ = σ′{y′/y′}. Then σ{y/y′} and σ′ represent the same partition of fn(P′, Q′) ⊆ fn(P, Q) ∪ {y′}.

(input)

Suppose that P σ ⟶^{xσ(y)} P_{1} with y ∉ fn(P σ, Qσ) ⟹ For some y′ ∉ fn(P σ, P σ′, Qσ, Qσ′) and such that y′ = y′σ = y′σ′, it holds that

P σ ⟶^{xσ(y′)} P_{1}{y′/y}

⟹ By Lemma 10, P σ′ ⟶^{xσ′(y′)} P_{2} with P_{1}{y′/y} ≡_{α} P′σ and P_{2} ≡_{α} P′σ′ for some

process P′ with fn(P′) ⊆ fn(P) ∪ {y′}

⟹ By ind. hyp., it follows from (P σ′, Qσ′) ∈ S_{n−1} that Qσ′ ⟶^{xσ′(y′)} Q_{2} with (P_{2}{u/y′}, Q_{2}{u/y′}) ∈ S for all u

⟹ By Lemma 10, Qσ ⟶^{xσ(y′)} Q_{1} with Q_{2} ≡_{α} Q′σ′ and Q_{1} ≡_{α} Q′σ for some Q′ such that fn(Q′) ⊆ fn(Q) ∪ {y′}. Then (P′σ′{u/y′}, Q′σ′{u/y′}) ∈ S for all u ⟹ By y ∉ fn(Qσ) it holds that Qσ ⟶^{xσ(y)} Q_{1}{y/y′}. Then the thesis, since (P_{1}{w/y}, Q_{1}{y/y′}{w/y}) ∈ S for all w. In fact

P_{1}{w/y} ≡ P_{1}{y′/y}{y/y′}{w/y}
≡_{α} P′σ{w/y′}
S Q′σ{w/y′}
≡_{α} Q_{1}{w/y′}
≡ Q_{1}{y/y′}{w/y}

where (P′σ{w/y′}, Q′σ{w/y′}) ∈ S is justified by (P′σ′{u/y′}, Q′σ′{u/y′}) ∈ S with σ{w/y′} and σ′{u/y′} representing the same partition of fn(P′, Q′) ⊆ fn(P, Q)∪ {y′}. An analogous proof schema is used to handle τ-forgetting relations. Indeed, suppose that either P σ′ ˙≈_{L} Qσ′ or P σ′ ˙≃_{L} Qσ′. By hypothesis, a weak late ground bisimulation U there exists such that (P σ′, Qσ′) ∈ U and, when ground equality is assumed, if P σ′ ⟶^{τ} P′ then for some Q′, Qσ′ ⟹^{τ} Q′ with (P′, Q′) ∈ U, and symmetrically. Then T = ⋃_{n} T_{n} where

T_{0} = U
T_{n+1} = { (P σ, Qσ) | P σ′ T_{n} Qσ′ and

σ, σ′ represent the same partition of fn(P, Q) }

is shown to be a weak late ground bisimulation by proving, by induction on n, that P T_{n} Q implies

- if P ⟶^{α} P′ with α ≠ x(y) and bn(α) ∉ fn(P, Q), then for some Q′, Q \underrightarrow{α̂} Q′

and P′ T Q′

- if P ⟶^{x(y)} P′ with y ∉ fn(P, Q), then for some Q′, Q ⟹⟶^{x(y)} Q′ and, for all w,

P′{w/y} T Q′{w/y}

Also, under the assumption P σ′ ˙≃_{L} Qσ′, the relation T is proved to be such that whenever P σ ⟶^{τ} P′′ then for some Q′′, Qσ ⟹^{τ} Q′′ with (P′′, Q′′) ∈ T , and symmetrically. W.r.t. the proof for strong bisimulation, the only remarkable issue in the proofs for τ-forgetting semantics is the possibly interleaved application of Lemma 10 and Lemma 11 for dealing with weak behaviours. □

The above theorem guarantees that lots of checks may be saved when trying to infer the non-ground bisimilarity of two processes P and Q. In fact, once a certain P σ ˙≍ Qσ has been proved, any other test on the ground equivalence of P σ′ and Qσ′ is useless whenever σ and σ′ happen to represent the same partition of fn(P, Q).

Considering again the introductory Ex. 8, assume to want to test whether or not R_{1} ≡ (\overline{x} | y) ∼_{L} R_{2} with fn(R_{2}) = \{x, y\}. In such a case checking just the ground late bisimilarity of R_{1}{x/x, x/y} and R_{2}{x/x, x/y} gives full information about the late ground equivalence of any pair of processes R_{1}σ and R_{2}σ with σ = {z/x, z/y, w_{1}/u_{1}, …, w_{n}/u_{n}}.

We will show in the following that late congruences of the two processes P and Q may be expressed in terms of a finite number of checks on the corresponding ground bisimilarity of P σ and Qσ. To do that, we first introduce a definition which allows substitutions to be grouped into families representing a given set of names.

Definition 13 Let N ⊆ N be a set of names and {σ_{i}}_{i∈I} be a family of name substitutions σ_{i} : N → N. Then {σ_{i}}_{i∈I} is a partition family of N iff the following holds:

- if N = ∅ then {σ_{i}}_{i∈I} contains only the identity substitution

- for each partition of N ≠ ∅ into k disjoint and non-empty sets N_{1}, …, N_{k}, there is exactly one substitution in {σ_{i}}_{i∈I} that represents N_{1}, …, N_{k} □

Notice that an infinite number of distinct partition families of N ≠ ∅ there exists. However, any partition family of N is somehow unredundant: it contains one and only one representative of each of the possible partition of N.

Relying on the notion of partition family, we can eventually prove the general result which justifies our initial claim that, whenever fn(R_{1}, R_{2}) = {x, y} and u ≠ w, the strong late congruence of R_{1} and R_{2} can be characterized as conjunction of the following ground bisimilarities:

R_{1}{u/x, u/y} ˙∼_{L} R_{2}{u/x, u/y}  R_{1}{u/x, w/y} ˙∼_{L} R_{2}{u/x, w/y}

Theorem 14 Let P, Q be π-calculus processes and let ˙≍ ∈ { ˙∼_{L}, ˙≈_{L}, ˙≃_{L}}. Also, assume ≍ to be the non-ground relation corresponding to the chosen ˙≍. Then P ≍ Q iff P σ ˙≍ Qσ for all σ ∈ {σ_{i}}_{i∈I} with {σ_{i}}_{i∈I} partition family of fn(P, Q).

Proof: ⟹) By definition of ≍. ⟸) Assume that a partition family {σ_{i}}_{i∈I} of fn(P, Q) there exists such that P σ ˙≍ Qσ for all σ ∈ {σ_{i}}_{i∈I}. Any name substitution σ′ represents one out of the possible partitions of fn(P, Q). (For instance, if Dm(σ′) ∩ fn(P, Q) = ∅, then σ′ behaves over fn(P, Q) just like the identity substitution and hence σ′ represents the partition of fn(P, Q) into singleton sets.) By definition of partition family, the substitution σ′ represents the same partition of fn(P, Q) as some σ ∈ {σ_{i}}_{i∈I}. Hence the thesis, by Th. 12. □

As finite set, fn(P, Q) only has a finite number of distinct partitions. Then any partition family of fn(P, Q) is finite. So, an immediate corollary of Theorem 14 is that two π-calculus processes can be shown to be congruent by relying on a (big but) finite number of ground bisimilarity checks.

4 Processes as functions

In the following we will focus on the opportunity of relating the results of Section 3 to the peculiar features of the ground πξ-calculus. Letting ≍ ∈ {∼_{L}, ≈_{L}, ≃_{L}}, this will show up in the characterization of P ≍ Q as corresponding CCS-bisimilarity of two single πξ-processes.

Theorem 7 in Section 2 shows that name substitutions are naturally encoded by environments. Precisely, it proves that a suitable management of environments can take the place of the π-calculus meta-syntactic operation of substitution. So, letting N = fn(P, Q), we expect for instance the double implication

(ξ^{Nσ} :: P σ) ∼ (ξ^{Nσ} :: Qσ) iff (ξ^{Nσ} :: P) ∼ (ξ^{Nσ} :: Q)

to hold. Actually, a more abstract property can be proved. Applying the substitution σ to P and to Q is definitely unnecessary in the πξ-calculus. Besides that, the mere application of σ to N can be rendered by making explicit the way how σ quotients its domain into subsets sharing the same image.

Lemma 15 Let P_{1}, P_{2} be π-calculus processes with N = fn(P_{1}, P_{2}), and, given a name substitution σ : N_{I} → N_{I}, assume ξ^{N/σ} = Id_{E} +{(x, ı(xσ)) | x ∈ N}. Also, let ≏ ∈ {∼, ≈, ≈^{c}}. Then (ξ^{Nσ} :: P_{1}σ) ≏ (ξ^{Nσ} :: P_{2}σ) iff (ξ^{N/σ} :: P_{1}) ≏ (ξ^{N/σ} :: P_{2}).

Proof: We start by commenting on the shape of the environments ξ (ξ′, respectively) which are reachable along the derivations from a given ξ^{Nσ} :: P σ (ξ^{N/σ} :: P, respectively). By the definitions of ξ^{Nσ} and ξ^{N/σ} and η, the only differences between ξ and ξ′ are relative to the equivalence classes containing elements of B = {ı(x) | x ∈ Nσ}. Precisely, for all c ∈ B it holds that [c]_{ξ} ∩ N_{I} = {ı^{−1}(c)} while [c]_{ξ′} may be either such that [c]_{ξ′} ∩ N_{I} ≠ {ı^{−1}(c)} or such that card([c]_{ξ′} ∩ N_{I}) > 1 (for example think of the name substitutions {y/z} and {y/z, y/w} which give raise to [ı(y)]_{ξ′} ∩N_{I} = {z} and to [ı(y)]_{ξ′} ∩ N_{I} = {z, w}, resp.). The above observation is all we need to construct a relation containing (ξ^{Nσ} :: P_{1}σ, ξ^{Nσ} :: P_{2}σ) starting from a relation containing (ξ^{N/σ} :: P_{1}, ξ^{N/σ} :: P_{2}), and vice-versa. Assume that (ξ^{N/σ} :: P_{1}) ≏ (ξ^{N/σ} :: P_{2}). Then there exists a relation S, subset of either ∼ or ≈, which contains the pair (ξ^{N/σ} :: P_{1}, ξ^{N/σ} :: P_{2}) and possibly some other relevant pairs when the two processes are supposed to be observational congruent. We define in the following a relation S′ that proves (ξ^{Nσ} :: P_{1}σ) ≏ (ξ^{Nσ} :: P_{2}σ).

S′ = ⋃_{(ξ_{P}::P,ξ_{Q}::Q)∈S}(ξ′_{P} :: P σ, ξ′_{Q} :: Qσ)

where ξ′_{P} is defined as follows, and ξ′_{Q} is constructed in an analogous way.

ξ′_{P} = ξ̃_{P} + ⋃_{c∈B} {(c, ı^{−1}(c))} ∪ {(c, x) | x ∈ [c]ξ_{P} \ N}

with ξ̃_{P} such that the following holds

- if a ξ_{P} b and, for all c ∈ B, a ∉ [c]ξ_{P}, then a ξ̃_{P} b

- if a ξ_{P} b and there exists c ∈ B such that a ∈ [c]_{ξ_{P}}, then a ξ̃_{P} a and b ξ̃_{P} b

Intuitively, ξ̃_{P} is the same as ξ_{P} but for ‘removing’ the equivalence classes [c] such that c ∈ B, namely, except for replacing any of such [c] by the union of the equivalence classes [a] = {a} with a ∈ [c]. Now assume (ξ^{Nσ} :: P_{1}σ) ≏ (ξ^{Nσ} :: P_{2}σ) and let T , contained in either ∼ or ≈, be the relation which witnesses the hypothesis. In this case the thesis can be shown by transforming T into T′ as follows.

T′ = ⋃_{(ξ_{P}::P,ξ_{Q}::Q)∈T} ⋃_{P′,Q′}(ξ′′_{P} :: P′, ξ′′_{Q} :: Q′)

where

ξ′′_{P} = ξ̃_{P} + ⋃_{c∈B} {(c, x) | ı(xσ) = c} ∪ {(c, x) | x ∈ [c]_{ξ_{P}} \ Nσ}

with ξ̃_{P} defined as above, and ξ′′_{Q} defined analogously to ξ′′_{P}. As far as P′ and Q′ are concerned, if σ is injective, then P′ and Q′ are simply P σ^{−1} and Qσ^{−1}, but this is not the most general case. So, P′ (resp. Q′) is taken from the family of processes which are obtained by non-deterministically substituting in P (resp. in Q) any occurrence of the name y by any name x such that xσ = y. E.g., letting P = \overline{y}y and σ = \{y/x, y/z\}, such a family should be \{\overline{x}x, \overline{x}y, \overline{x}z, \overline{y}x, \overline{y}y, \overline{y}z, \overline{z}x, \overline{z}y, \overline{z}z\}. □

The above result strongly depends on the fact that environments naturally represent, via equivalence classes, partitions of sets of names.

Definition 16 The environment ξ represents the partition of N ⊆ N_{I} into the disjoint and non-empty sets N_{1}, …, N_{k} iff the following holds:

- N = ⋃_{c∈allD(ξ)}([c]_{ξ} ∩ N )

- for all j ∈ {1, …, k} there exists c ∈ allD(ξ) such that N_{j} = ([c]_{ξ} ∩ N ) □

Notice that the partition of N represented by a given environment ξ is identified resorting to the constants in allD(ξ). Nevertheless, the actual distinguishing feature of any environment is just the represented partition, rather than the identity of its active constants. This is claimed by the next proposition.

Proposition 17 Let P_{1} and P_{2} be π-calculus processes, and let the environments ξ and ξ′ represent the same partition of N ⊆ N_{I}. Also, let ≏ ∈ {∼, ≈, ≈^{c}}. Then ξ :: P_{1} ≏ ξ :: P_{2} iff ξ′ :: P_{1} ≏ ξ′ :: P_{2}.

Proof: Let S be a relation over πξ-calculus processes which proves that ξ :: P_{1} ≏ ξ :: P_{2} (resp. ξ′ :: P_{1} ≏ ξ′ :: P_{2}). Then a relation S′ which shows that ξ′ :: P_{1} ≏ ξ′ :: P_{2} (resp. ξ :: P_{1} ≏ ξ :: P_{2}) may be defined by adequately translating the active constants of the environments of any pair (ξ_{P} :: P, ξ_{Q} :: Q) ∈ S. □

It was shown above that πξ-calculus environments represent partitions of sets of names in a genuine way. A more effective feature can now be focussed on. In the πξcalculus, partitions of sets can be effectively generated by sequential compositions of λ-prefixes.

Example 18 Consider for instance the tree depicted in Fig. 1. It represents the transition system associated with the πξ-process

S_{0} ≡ (Id_{E} :: λx.λy.λz. nil)

But for the root node, the environment of any other agent in Fig. 1 is given a compact visualization that only reports on the relevant equivalence classes. We now comment on the computations starting with S_{0}. No constant is active in Id_{E}. Then, when the leading prefix λx fires, the name x is deterministically associated with c_{1} = newD(Id_{E}). Correspondingly, S_{0} becomes

S_{1} ≡ (Id_{E} + (x, c_{1}) :: λy.λz. nil)

with (Id_{E} +(x, c_{1})) representing the single partition of {x} into {x}. Differently from S_{0}, the environment of process S_{1} contains one active constant. So, the symbolic step labelled by ⟨[y], true⟩ induces two distinct transitions of S_{1}. The one is labelled by [c_{1}], the other is labelled by the concretion of a new constant c_{2}. The two

[figure: Id_{E}::λx.λy.λz. nil; [c_{1}]; [x,c_{1}]::λy.λz. nil; [c_{1}]; [c_{2}]; [x,y,c_{1}]::λz. nil; [c_{1}]; [c_{2}]; [x,c_{1}],[y,c_{2}]::λz. nil; [c_{1}]; [c_{2}]; [c_{3}]; [x,y,z,c_{1}]::nil; [x,z,c_{1}],[y,c_{2}]::nil; [x,y,c_{1}],[z,c_{2}]::nil; [x,c_{1}],[y,c_{2}],[z,c_{3}]::nil; [x,c_{1}],[y,z,c_{2}]::nil]

Figure 1: transition system of Id_{E} :: λx.λy.λz. nil

derivatives of S_{1} have a common right component (λz. nil), but their environments are distinct because of the association of the name y with the constant c_{1} and with the constant c_{2}, respectively. Such environments represent the partitioning of the set {x, y} into {x, y} and into {x} ∪ {y}, respectively. Computations go on by the firing of the λz prefix and actually the environments of the leaf-processes represent all the possible partitions of {x, y, z} into disjoint and non-empty sets. □

The above comment on Fig. 1 can be formalized as follows.

Proposition 19 Suppose that ξ :: λy.P \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξ′ :: P, then the following holds.

1. If ξ = Id_{E} then ρ = [newD(Id_{E})] and ξ′ represents the only possible partition of {y}

2. If ξ represents the partition of N into the disjoint and non-empty sets N_{1}, …, N_{k}, with y ∉ N, then

- if ρ = [c] with ([c]_{ξ} ∩N) = N_{j}, then ξ′ represents the partition of N ∪{y} into the k disjoint sets N_{1}, …, N_{j} ∪ {y}, …, N_{k} - if ρ = [newD(ξ)] then ξ′ represents the partition of N ∪{y} into the k +1

disjoint sets N_{1}, …, N_{k}, {y}

Proof: By definition of η, it holds that ξ′ = ξ + (y, c_{j}) with ρ = [c_{j}]. Then the thesis, by Def. 16. □

In the following, the partition generation property of λ-prefixes will be used to describe partition families. This passes through the definition of λ-closures.

Definition 20 Let P be a π-calculus process and L be a list of names. Then the λ-closure of P w.r.t. L is defined as λ clos(P, L) where

λ clos(P, [ ]) = P
λ clos(P, [y, L]) = λ clos(λy.P, L)

with [ ] denoting the empty list, and [ , [ ]] denoting the ‘cons’ list operator. □

The bisimilarity of two agents obtained by a suitable λ-closure may now be used to express the bisimilarity of a whole substitution-indexed family of pairs of πξprocesses.

Lemma 21 Let P_{1}, P_{2} be π-calculus processes with N = fn(P_{1}, P_{2}) and let L be a list containing all and only the elements of N. Also, assume ≏ ∈ {∼, ≈, ≈^{c}} and, given a name substitution σ, let ξ^{N/σ} = Id_{E} +{(x, ı(xσ)) | x ∈ N}. Then Id_{E} :: λ clos(P_{1}, L) ≏ Id_{E} :: λ clos(P_{2}, L) iff (ξ^{N/σ} :: P_{1}) ≏ (ξ^{N/σ} :: P_{2}) for all σ ∈ {σ_{i}}_{i∈I} with {σ_{i}}_{i∈I} partition family of N.

Proof: If N = ∅ then the thesis is immediate by λ clos(P_{i}, L) ≡ P_{i} for i ∈ {1, 2} and by ξ^{N/σ} = Id_{E}. Hence suppose N ≠ ∅. Using Prop. 19, it can be proved by induction that

⋃\{ξ_{p} | Id_{E} :: λ clos(P_{i}, L) \begin{matrix}− \\ − \end{matrix}▷^{∗} ξ_{p} :: P_{i}\}

represents a partition family of N, namely each environment ξ_{p} represents a distinct partition of N into the disjoint and non-empty sets N_{1}, …, N_{k}. Also notice that no internal non-determinism raises at any step during the computation

Id_{E} :: λ clos(P_{i}, L) \begin{matrix}− \\ − \end{matrix}▷^{∗} ξ_{p} :: P_{i}.

Hence Id_{E} :: λ clos(P_{1}, L) ≏ Id_{E} :: λ clos(P_{2}, L) iff ξ_{p} :: P_{1} ≏ ξ_{p} :: P_{2} for all ξ_{p} representing the partition p of N. Actually, any of the above environments ξ_{p} has the following shape

ξ_{p} = Id_{E} +{(x, ξ_{p}(x)) | x ∈ N}

where allD(ξ_{p}) is given by the first k run-time generated constants rather than by constants in D_{I}. Then each ξ_{p} differs from ξ^{N/σ} only for the identities of the active constants. Hence the thesis by Prop. 17. □

Any non-ground bisimilarity of the π-calculus processes P and Q , say P ≍ Q, was already proved (cf. Th. 14) to be expressible in terms of a finite number of suitable checks on P σ ˙≍ Qσ. We now show that P ≍ Q can equally be characterized as the corresponding CCS-like bisimilarity of two single πξ-processes whose right components are the λ-closures of P and Q.

Theorem 22 (coincidence with late non-ground semantics) Let P, Q be π-calculus processes and let L be a list containing all and only the elements of fn(P, Q). Then

1. P ∼_{L} Q iff Id_{E} :: λ clos(P, L) ∼ Id_{E} :: λ clos(Q, L)

2. P ≈_{L} Q iff Id_{E} :: λ clos(P, L) ≈ Id_{E} :: λ clos(Q, L)

3. P ≃_{L} Q iff Id_{E} :: λ clos(P, L) ≈^{c} Id_{E} :: λ clos(Q, L)

Proof: Assume ˙≍ to be the ground dual of ≍ ∈ {∼_{L}, ≈_{L}, ≃_{L}} and the π-calculus dual of ≏ ∈ {∼, ≈, ≈^{c}}. Then, letting N = fn(P, Q), the following holds: P ≍ Q iff (Th. 14) P σ ˙≍ Qσ for all σ ∈ {σ_{i}}_{i} with {σ_{i}}_{i} partition family of N iff (Th. 7) (ξ^{Nσ} :: P σ) ≏ (ξ^{Nσ} :: Qσ) for all σ ∈ {σ_{i}}_{i} with {σ_{i}}_{i} partition family of N iff (Lemma 15) (ξ^{N/σ} :: P) ≏ (ξ^{N/σ} :: Q) for all σ ∈ {σ_{i}}_{i} with {σ_{i}}_{i} partition family of N and ξ^{N/σ} = Id_{E} + {(x, ı(xσ)) | x ∈ N} iff (Lemma 21) Id_{E} :: λ clos(P, L) ≏ Id_{E} :: λ clos(Q, L). □

Theorem 23 (equational characterizations of late non-ground semantics) Let P, Q be finite π-calculus processes and let L be a list containing all and only the elements of fn(P, Q). Then

1. P ∼_{L} Q iff A_{a}, A_{L} ⊢ Id_{E} :: λ clos(P, L) = Id_{E} :: λ clos(Q, L)

2. P ≃_{L} Q iff A_{a}, A_{L}, A_{w} ⊢ Id_{E} :: λ clos(P, L) = Id_{E} :: λ clos(Q, L)

Proof: By Th. 22 and Th. 6. Only recall that equational characterizations of late πξ-calculus semantics does hold for processes of the πξ-calculus, hence for processes whose right component may contain arbitrary occurrences of λ-prefixes. □

Suppose that card(fn(P, Q)) = n. Then there are n! distinct permutations of the elements in fn(P, Q) and consequently n! distinct lists built up by fn(P, Q). Theorem 22 asserts that the bisimilarity of P and Q can be checked relying just on one of those lists, no matter which one. The role of L in λ clos(P, L) is only that of generating environments that represent a partition family of the due names. So, the actual sequencing of the list can only influence the generation order, but the desired final effect is independent on it. Roughly, the choice of the list L stays to λ clos(P, L) the same way as the choice of a correct sequential algorithm for computing the partitions of a finite set stays to the computed function.

When processes P and Q are to be compared, what does really matter is to use the same list L in defining either the λ-closure of P or the λ-closure of Q. This guarantees that the bisimilarity of the pair of processes

(Id_{E} :: λ clos(P, L), Id_{E} :: λ clos(Q, L))

is factorized into the bisimilarity of all the pairs in the set given by

⋃_{p}(ξ_{p} :: P, ξ_{p} :: Q)

where p ranges over the possible partitions of fn(P, Q) and ξ_{p} represents just the partition p.

The results stated in Theorem 22 are far from unexpected. Putting a given process in any context may result in binding some or all of its free names. Therefore, reasoning about congruence compells to think of any process as of a function of its free names. Not randomly, any non-ground relation ≍ coincides with its ground counterpart ˙≍ over terms without any free name. Also, the following might be proved. If fn(P, Q) = {y_{1}, …, y_{n}} then checking P ≍ Q is the same as picking up a fresh name, say x, and checking

x(y_{1}).x(y_{2}). . . . .x(y_{n}).P ˙≍ x(y_{1}).x(y_{2}). . . . .x(y_{n}).Q

Given the process x(y_{1}).x(y_{2}). . . . .x(y_{n}).P which represents a ‘prefix-closure’ of P, the late paradigm directly suggests that x(y_{2}). . . . .x(y_{n}).P is a function of y_{1}, and that the agent x(y_{3}). . . . .x(y_{n}).P is a function of both y_{1} and y_{2}, …, and P is a function of all of {y_{1}, …, y_{n}}. The λ-closures used in the πξ-calculus and the above prefix-closures express exactly the same intrinsic functional dependence of processes on their free names.

A final comment can be related to the observation above. The result in Theorem 22 could have been proved by using an alternative strategy whose pattern can be sketched out as follows.

P ≍ Q
iff x(y_{1}).x(y_{2}). . . . .x(y_{n}).P ˙≍ x(y_{1}).x(y_{2}). . . . .x(y_{n}).Q
iff ξ^{{x}} :: x(y_{1}).x(y_{2}). . . . .x(y_{n}).P ≏ ξ^{{x}} :: x(y_{1}).x(y_{2}). . . . .x(y_{n}).Q
iff Id_{E} :: λy_{1}.λy_{2}. . . . .λy_{n}.P ≏ Id_{E} :: λy_{1}.λy_{2}. . . . .λy_{n}.Q

The approach we used exploits more transparently the correspondence between πcalculus substitutions and πξ-environments.

5 Call-by-need generation strategies

In this section the non-ground version of the πξ-calculus is defined. Relying on that, a more promising characterization of strong late π-calculus congruence is presented. Also, a coincidence result for open semantics is stated.

We commented that reasoning about non-groundness imposes to regard any π-calculus process as a function depending on its free names. So, as πξ-calculus is concerned, more sophisticated environments are adopted where free names are associated with constants not by default, but rather following a call-by-need discipline. This corresponds to adopting a call-by-need strategy for the generation of the substitutions needed to reason about non-groundness.

It was shown that late non-ground bisimilarities of P and Q can be expressed, for σ ranging over a partition family of fn(P, Q), as conjunctions of the corresponding ground equivalences of P σ and Qσ. We also pointed out that any partition family of fn(P, Q) has finite cardinality. So, the alternative characterizations stated in Section 3 are effective improvements on the usual definitions of non-ground bisimilarities. Nevertheless, the finite number of checks they require is quite big: as many checks are needed as the cardinality of a partition family of fn(P, Q), which grows more than 2^{n} with n = card(fn(P, Q)). Depending on n, the pre-processing phase consisting either in generating a partition family of fn(P, Q), or in taking the ground πξ-calculus view and hence firing the λ-abstractions prefixing P and Q, may be really prohibitive. Worst than that, such a pre-processing phase could also be useless. Think, for instance, to have to check the congruence of the two processes

\begin{aligned}P & ≡ & x(y). nil \\ Q & ≡ & x(y).(z)\overline{z}x.Q_{1} \end{aligned}

Since (z)\overline{z}x.Q_{1} is deadlocked, there is no sensible reason for generating lots of substitutions whose number essentially depends on the cardinality of fn(Q_{1}). Free names could more properly and more efficiently be dealt with as variables and could be instantiated following a by-need discipline. Consider for instance the following example.

Example 24 Think of the π-calculus process (\overline{x} | y) as of the agent

P_{v} ≡ \overline{v}_{x} : \{x\} | v_{y} : \{x, y\}

The syntax used for describing P_{v} is meant to suggest that x and y are dealt with as variables whose types are non-disjoint sets of names. Roughly, P_{v} gives the intuition that, whenever (\overline{x} | y) is put in an arbitrary context, x and y may be substituted either by distinct names or by the same name, which we conveyed to be x (x results as intersection of the types of v_{x} and v_{y}). We can now discuss the action potentials of P_{v}. Process P_{v} can surely interleave the execution of the actions \overline{v}_{x} and v_{y}. The more, with the proviso that v_{x} and v_{y} assume the same value, P_{v} can also perform a τ-step. □

The intuition which underlies Ex. 24 will be rendered formal in the πξ-calculus by adequately sophisticating the definitions of environment and of evaluation function. In particular, we will retain either the symbolic transition system of Section 2, or the idea of expressing extensional semantics in terms of ordinary strong bisimilarity. Though, the top-level transition relation and the update and result functions will be refined following a call-by-need name instantiation strategy.

In the present perspective, environments become sets of equations over three distinct entities: names, constants, and variables. Names and constants are as described in Section 2. Variables (ranged over by v, v_{1}, …) are typed, each type being a finite subset of D. More specifically, variables are taken from a domain V which is supposed to contain one variable per type and to be disjoint by both N and D. Notationally v : D indicates that the variable v takes values in the finite set D ⊂ D, and an association of the form (x ξ (v : D)) means that x may take as value any of the constants in D.

Definition 25 A non-ground environment ξ is an equivalence relation over N ∪ D ∪ V which is:

- consistent: c_{i} ξ c_{j} implies c_{i} = c_{j} and c ξ (v : D) implies c ∈ D and (v_{1} : D_{1}) ξ (v_{2} : D_{2}) implies D_{1} ∩ D_{2} ≠ ∅

- finitely active: the set {(a, b) | a ξ b and a ≠ b} is finite

A variable v is active in ξ iff there exists a ≠ v with (v ξ a). A constant c is active in ξ iff there exists either a ≠ c with (c ξ a) or a variable v : D which is active in ξ and c ∈ D. Variables and constants which are not active, are called inactive.

Still, the equivalence class of ξ containing a is indicated as [a]_{ξ}, and the family of all non-ground environments is denoted E, and we write Id_{E} for the identity environment. □

Because of the grown complexity of the environments we now deal with, we refine the notions of definedness and undefinedness of the partial function ξ( ). We say that ξ is defined on y (still denoted by ξ(y)↓) iff for some a ∈ D ∪ V it holds that (y ξ a). If ξ( ) is not defined on y, then we write ξ(y)↑. Also, the class [y]_{ξ} is said to be undefined if ξ(y)↑, defined otherwise. When [y]_{ξ} is defined, we call it defined-by-variable if D ∩ [y]_{ξ} = ∅, defined-by-constant otherwise.

Describing initial non-ground environments needs to generate fresh variables. So, we assume the existence of the following new functions:

newV : E ⟶ 2_{f}^{D} ⟶ V  allV : E ⟶ 2_{f}^{V}  typV : E ⟶ 2_{f}^{D}

Functions newD and allD are defined the same as they were for ground environments, however recall that in the meanwhile the notion of active constant has been slightly modified. The application newV(ξ) : D returns a variable of type D which is inactive in ξ. The function allV returns the finite set of all the variables which are active in the argument, and eventually typV(ξ) yields the union of the types of the variables in allV(ξ).

We define below the non-ground dual of the initial environment ξ^{N}. It actually represents in an abstract way all the possible partitions of N.

Definition 26 Letting L be a list of distinct elements of N_{I}, the initial non-ground environment ξ^{L} is defined as

ξ^{L} = add var(Id_{E}, L)
where add var(ξ, [ ]) = ξ

add var(ξ, [x, L]) = add var(ξ + (x, newV(ξ) : (allD(ξ) ∪ newD(ξ)), L)

□

In the non-ground πξ-calculus the evaluation of symbolic obligations becomes a crucial issue: some equalities of names must be checked, some others must be imposed. The equalities to be tested are those relative to names whose instantiation has been caused by a communication or a placeholder concretion. The equalities to be forced, instead, are relative to those names the process at hand is supposed to be a permanent function of. This exactly captures the essence of non-groundness. Since we are reasoning here modulo name substitutions, imposing the equality x = y when both x and y have initially been free names (cf. Ex. 24) is equivalent to assuming that, no matter what xσ and yσ actually are, if they are the same then the process can move and from now onwards x and y must be taken to be the same.

As a consequence of the above discussion, the obligations of the symbolic semantics must sometimes be considered as actual constraints. This, in turn, implies that the evaluation of obligations cannot be any longer a boolean predicate. It rather yields a relation to be added with the environment. To explain this we can focus our attention on the evaluation of the obligation x = y in ξ. First suppose that the equality of x and y must only be checked. Then, depending on whether x ∈ [y]_{ξ} or not, the evaluation function returns the empty relation (denoted ϕ) or the inconsistent relation (written ε). Assume now that x and y are recognized as names which could be arbitrarily substituted by putting the process into a given context. In this case the equality x = y is forced into the environment by letting the evaluation function return the constraint-relation (x, y).

Having to cope with inconsistent relations, a more general notion of sum operation on environments is needed, too.

Definition 27 Let R_{1}, R_{2} be relations over N ∪D ∪V or the distinguished element ε ∉ N ∪ D ∪ V denoting the inconsistent relation. The sum R_{1} ⊎ R_{2} is defined as:

R_{1} ⊎ R_{2} = \{ \begin{matrix}ε & if R_{1} = ε or R_{2} = ε \\ ε & if R_{1} + R_{2} is not consistent \\ R_{1} + R_{2} & otherwise \end{matrix}

□

A couple of comments are due. First, observe that the active variables of the initial non-ground environment ξ^{L} have incremental types. So, given any pair of variables (v_{1} : D_{1}), (v_{2} : D_{2}) ∈ allV(ξ^{L}) it holds that D_{1} ∩ D_{2} ≠ ∅. This guarantees that the names occurring in L can be arbitrarily joined in the same equivalence class without giving raise to any inconsistency. Second, recall that observable results will be actual functions. Then, correspondingly to the possible inconsistency induced by adding environments with constraints, the result function may yield on some arguments a distinguished error element denoted by ⊥.

It will be made clear soon that requiring the external observer to interact with functions is too strong a requirement when aiming at characterizing extensional semantics via ordinary bisimilarity. We use functions to give a compact representation of behaviours modulo substitutions. Suppose P to be the process at hand, with fn(P) = {x_{1}, …, x_{n}}. Intuitively, observing the n-ary function f gives information that for all the tuples (y_{1}, …, y_{n}) such that f(y_{1}, …, y_{n}) ≠ ⊥, process P {y_{1}/x_{1}, …, y_{n}/x_{n}} can move performing f(y_{1} … y_{n}). By this, a process P_{1} able to execute g_{1} = λx_{1}x_{2}.x_{2} has the same action capabilities of P_{2} which can perform both g_{1} and g_{2} = λx_{1}x_{2}. x_{1} = x_{2} → x_{2}, ⊥. Nevertheless, if the bisimulation game required to match just the above behaviours, then the two processes would not be equated. In fact P_{1} could not properly react to the g_{2}-move played by P_{2}. This leads us to reason about functional observations via the standard partial ordering relation over functions.

Definition 28 Let f and h be n-ary functions. Then f ⊑ h iff fã ≠ ⊥ implies fã = hã. The constant function always yielding ⊥ is denoted by \underline{⊥}. □

5.1 Strong late non-groundness, again

In the following we will introduce the late non-ground πξ-calculus, namely we will define a new top-level transition relation that allows us to characterize late πcalculus non-groundness without resorting to λ-closures.

Introducing the issue of non-groundness we commented on the opportunity of considering any process P as a function of its free names x̃. We also noticed that correspondingly to the firing of input actions any process behaves like a function of the input parameter. These two kinds of functionality are conceptually distinct and must be guaranteed do not interfere. The dependence on the tuple x̃ continues to hold throughout the computation. By contrast, the dependence on an input placeholder is not permanent, it gets immediately lost when the parameter is actualized.

{P ⟶^{ω} P′  ω ≠ ⟨x(y), C⟩  ξ′ ∈ η_{N}(ξ, ω)  ρ ⊑ δ_{N}(ξ′, ω)  ρ ≠ \underline{⊥} \atop ξ :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{ρ} ξ′ :: P′} ; {P ⟶^{⟨x(y),C⟩} P′  ξ′ ∈ η_{N}(ξ, x(y), C)  ρ ⊑ δ_{N}(ξ′, x(y), C)  ρ ≠ \underline{⊥} \atop ξ :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{ρ} ξ′ :: λy.P′}

Table 7: definition of \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}

So, although any derivative of P may have some free names more than P, it must still be dealt with as a function of x̃ only. The information on the identity of the names in the tuple x̃ cannot be recovered syntactically, then it becomes a parameter of the update function, and hence of the top-level transition relation.

The non-ground late behaviour of πξ-processes is described by the relation \begin{matrix}− \\ − \end{matrix}▷_{η_{N}} defined in Table 7. The parameter N represents the set of names that the given running process is supposed to be a permanent function of. The extensional πξ-semantics is then given by the strong bisimulation induced by \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}, hereby denoted ∼_{η_{N}}.

New pairs of update and result functions are involved in the definition of the non-ground transition relation. Besides this, the main difference between \begin{matrix}− \\ − \end{matrix}▷_{η_{N}} and its ground dual \begin{matrix}− \\ − \end{matrix}▷ is that labels are not directly given by the result function δ_{N}(ξ′, ω), but rather by functions less than or equal to δ_{N}(ξ′, ω) and still distinct from \underline{⊥}.

The actual definition of the non-ground update function η_{N} requires a specialized evaluation function whose definition is reported in Tab. 8 together with the definition of (η_{N}, δ_{N}). The revised evaluation function takes as additional argument the set of names whose instantiation is to be forced by-need. As expected, {|C|}Nξ yields either a finite relation over N ∪ D ∪ V or the inconsistent relation ε.

The first step in computing η_{N}(ξ, α, C) is adding ξ with the relation yielded by the evaluation function {|C|}Nξ. If the sum operation causes inconsistency, then the update function returns the empty set and, by definition of \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}, the πξcalculus process taken into account remains blocked. When ξ ⊎ {|C|}Nξ results into an environment ξ_{1} ≠ ε, the definition of η_{N}(ξ, α, C) is essentially the same as that of η(ξ_{1}, α, C) and indeed in this event we still use the ground sum operation ‘+’.

One single difference between η_{N} and η is worth noticing. It is relative to the instantiation of input placeholders, and then to the definition of η_{N}(ξ, [y], C). The ground update function would associate y with all the constants active in ξ_{1} plus a new one. Here y is non-deterministically associated with all the active variables (i.e., with each of the names initially free) and with all the constants activated during the ongoing computation plus a new one.

The observable result δ_{N}(ξ′, ω) yields a function of all the variables which are active in ξ′. Maybe associating variables with some tuple of constants in the variables types gives raise to inconsistency. For instance, this is the case for the association of

{|C|}Nξ = case C in

                true : ϕ
               false : ε

x↓ : ξ(x)↓ ⟶ ϕ, ε
x = y : x ∈ N and y ∈ N ⟶ (x, y), x ξ y ⟶ ϕ, ε
x ≠ y : x ξ y ⟶ ε, ϕ
C_{1} ∧ C_{2} : {|C_{1}|}Nξ ⊎ {|C_{2}|}Nξ

            end case

η_{N}ξαC = case ξ ⊎ {|C|}ξ in
ε : ∅

             ξ_{1} : case α in

τ : ξ_{1}
τ[x/y] : ξ_{1} + (y, x)
\overline{x}(y), \overline{x}y : ξ_{1}(y)↓ ⟶ ξ_{1}, ξ_{1} + (y, newD(ξ_{1}))
x(y) : ξ_{1}
[y] : ⋃_{(v:D)∈allV(ξ_{1})} ξ_{1} + (y, v : D) ∪
⋃_{c∈(allD(ξ_{1}) \ typV(ξ_{1})) ∪ newD(ξ_{1}))} ξ_{1} + (y, c)

                   end case
            end case

δ_{N}ξαC = λd_{1} : D_{1} … λd_{m} : D_{m} . case ξ ⊎ ∑_{i=1}^{m}(v_{i}, d_{i}) in
ε : ⊥

                                    ξ_{1} : case α in

\begin{aligned}τ, τ[x/y] & : & τ \\ \overline{x}(y), \overline{x}y & : & \overline{ξ_{1}(x)}ξ_{1}(y) \\ x(y) & : & ξ_{1}(x) \\ [y] & : & [ξ_{1}(y)] \end{aligned}

                                           end case
                                   end case

where {v_{1} : D_{1}, …, v_{m} : D_{m}} = allV(ξ), D_{1} ⊂ D_{2} ⊂ … ⊂ D_{m}
Table 8: definition of (η_{N}, δ_{N})

(v_{1} : {c_{1}}, v_{2} : {c_{1}, c_{2}}) with the tuple (c_{1}, c_{2}) when v_{2} ∈ [v_{1}]_{ξ′}. Then the function δ_{N} may return on some tuple of arguments the distinguished element ⊥ denoting undefinedness. However for ξ′ ∈ η_{N}(ξ, ω) it holds that δ_{N}(ξ′, ω) ≠ \underline{⊥}. Also, the result yielded by the actualization δ_{N}(ξ′, ω)(c̃) ≠ ⊥ is analogous to the observation returned by the ground function δ.

In order to give a deeper intuition about the definition of η_{N} and δ_{N} we discuss in the following a case study.

Example 29 Let N = {x, z} and let ξ^{L} be as defined below.

ξ^{L} = Id_{E} +(x, v_{1} : {c_{1}}) + (z, v_{2} : {c_{1}, c_{2}})

We compute η_{N} and δ_{N} correspondingly to few symbolic actions and environments.

1. First let ω = ⟨[y], true⟩.

Function η_{N}(ξ^{L}, ω) returns a set composed by three updated environments, say {ξ_{1}, ξ_{2}, ξ_{3}}. Assuming newD(ξ^{L}) = c_{3}, the following equalities hold.

\begin{matrix}ξ_{1} = ξ^{L} + (y, v_{1}) = ξ^{L} + (y, x) & δ_{N}(ξ_{1}, ω) = λd_{1} : \{c_{1}\}.λd_{2} : \{c_{1}, c_{2}\}. [d_{1}] \\ ξ_{2} = ξ^{L} + (y, v_{2}) = ξ^{L} + (y, z) & δ_{N}(ξ_{2}, ω) = λd_{1} : \{c_{1}\}.λd_{2} : \{c_{1}, c_{2}\}. [d_{2}] \\ ξ_{3} = ξ^{L} + (y, c_{3}) & δ_{N}(ξ_{3}, ω) = λd_{1} : \{c_{1}\}.λd_{2} : \{c_{1}, c_{2}\}. [c_{3}] \end{matrix}

2. Assume now ω′ = ⟨τ, y = z⟩. Here η_{N}(ξ_{1}, ω′) = η_{N}(ξ_{3}, ω′) = ∅ in fact the input placeholder y was instantiated by z neither in ξ_{1} nor in ξ_{3}. Hence {|y = z|}Nξ_{1} = {|y = z|}Nξ_{3} = ε. By contrast, as {|y = z|}Nξ_{2} = ϕ, the following holds

\begin{matrix}η_{N}(ξ_{2}, ω′) = \{ξ_{2}\} \\ δ_{N}(ξ_{2}, ω′) = λd_{1} : \{c_{1}\}.λd_{2} : \{c_{1}, c_{2}\}. τ \end{matrix}

The idea is that, no matter what any zσ could be, the action τ may take place only if y was instantiated by zσ. In such a case the action surely fires, with ‘surely’ being represented by the fact that δ_{N}(ξ_{2}, ω′) is a constant function.

3. Now consider ω′′ = ⟨τ, x = z⟩. Here, letting j = 1, 2, 3, the following holds.

{|x = z|}Nξ_{j} = (x, z)
η_{N}(ξ_{j}, ω′′) = {ξ_{j} + (x, z)}
δ_{N}(ξ_{j} + (x, z), ω′′) = λd_{1} : {c_{1}}.λd_{2} : {c_{1}, c_{2}}. d_{1} = d_{2} → τ, ⊥

The above indicates that, independently on the actual instantiation of y, the action τ may be performed only with the proviso that xσ and zσ are the same.

□

Example 29 makes clear that the information furnished by the set indexing η_{N} cannot be recovered by simply checking the association of names with variables. As it is the case for (y ξ_{1} v_{1}) and for (y ξ_{2} v_{2}), those associations might have been inherited, for instance, because of the instantiation of some placeholder.

We can now provide a better understanding of the reason why we defined the relation \begin{matrix}− \\ − \end{matrix}▷_{η_{N}} resorting to the partial ordering on functions, namely using labels ρ ⊑ δ_{N}(ξ′, ω). First observe that

- the πξ-calculus non-ground process ξ :: P stays for a substitution-indexed family of π-calculus processes, say {P_{π}σ}_{σ}

- any substitution σ is actually witnessed by a tuple c̃ such that δ_{N}(ξ′, ω)(c̃) ≠ ⊥

In this view, function δ_{N}(ξ′, ω) is a monolithic – functional vs. point-wise – representation of the family of labels {α_{σ}}_{σ} such that P_{π}σ ⟶^{α_{σ}} P′_{π}. Taking ρ ⊑ δ_{N}(ξ′, ω) is meant to factorize the observable effect δ_{N}(ξ′, ω) while retaining a functional view about processes. Indeed, if the relation \begin{matrix}− \\ − \end{matrix}▷_{η_{N}} were defined assuming ρ = δ_{N}(ξ′, ω) then the induced strong bisimulation semantics over πξ-calculus processes would be finer than late congruence. We comment further on this issue by means of the example below.

Example 30 Consider the following late congruent processes.

\begin{aligned}P & ≡ & x(y).(τ + [x = z]τ) \\ Q & ≡ & x(y).τ \end{aligned}

Let ξ^{L} = Id_{E} +(x, v_{1} : {c_{1}}) + (z, v_{2} : {c_{1}, c_{2}}) with N = {x, z} and also assume ξ_{1} = ξ^{L} + (y, v_{1}). Then the following holds.

\begin{matrix}ξ^{L} :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{ρ} ξ^{L} :: λy.(τ + [x = z]τ) \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{ρ′} ξ_{1} :: τ + [x = z]τ \\ ξ^{L} :: Q \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{ρ} ξ^{L} :: λy.τ \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{ρ′} ξ_{1} :: τ \end{matrix}

A close look at Ex. 29 shows that

δ_{N}(η_{N}(ξ_{1}, τ, [x = z]), τ, [x = z]) = λd_{1} : {c_{1}}.λd_{2} : {c_{1}, c_{2}}. d_{1} = d_{2} → τ, ⊥

while

δ_{N}(η_{N}(ξ_{1}, τ, true), τ, true) = λd_{1} : {c_{1}}.λd_{2} : {c_{1}, c_{2}}. τ

If \begin{matrix}− \\ − \end{matrix}▷_{η_{N}} were directly labelled by δ_{N}(ξ′, ω) in Tab. 7, then ξ^{L} :: P and ξ^{L} :: Q would be deemed to be not strong bisimilar. In fact, the derivative ξ_{1} :: τ of ξ^{L} :: Q could not match the move played by ξ_{1} :: (τ + [x = z]τ) and labelled λd_{1}d_{2}. d_{1} = d_{2} → τ, ⊥. □

In the following we address the issue of translating non-ground environments into ground environments. Once this has been done, we can proceed and prove the characterization theorem.

The following definition is about the consistent transformation of variables into constants in their types.

Definition 31 Let ξ be a non-ground environment. Then a variable substitution for ξ is a substitution from variables to constants defined as it follows.

- if allV(ξ) = ∅ then the only variable substitution for ξ is the empty substitution

- if allV(ξ) = {v_{1} : D_{1}, …, v_{m} : D_{m}} with D_{1} ⊂ … ⊂ D_{m}, then a variable substitution σ for ξ is defined as σ = σ^{v_{1}}(ξ) … σ^{v_{m}}(ξ) where

- σ^{v_{j}}(ξ) is the substitution {a_{j}/v_{j}} with

a_{j} = \{ \begin{matrix}ξ(v_{j}) & if [v_{j}]_{ξ} is defined-by-constant \\ c_{j} ∈ D_{j} & otherwise \end{matrix}

- ∀i, j = 1, …, m if v_{i} ∈ [v_{j}]_{ξ} then Im(σ^{v_{i}}(ξ)) = Im(σ^{v_{j}}(ξ)) □

Variable substitutions are applied to non-ground environments in order to encode them into sets of ground environments. We convey to use the notation below.

\underline{Notation} Let ξ be a non-ground environment, and let σ be a substitution from variables to constants. Then ξσ is defined to be

ξσ = \{ \begin{matrix}ξ & if σ is empty \\ (eraseV(ξ + (v, c))v)σ′ & if σ = \{c/v\}σ′ \end{matrix}

where the application of eraseV : E → V → E to the arguments ξ and v is assumed to return an environment like ξ but where v is made inactive, namely all and only the associations (a, v) with a ≠ v have been erased. □

The following proposition asserts that there exists a precise relationship between the two evaluation functions considered so far.

Proposition 32 Let σ be a variable substitution for ξ, and C be an obligation. Then ξ ⊎ {|C|}Nξ ≠ ε iff ξ ⊎ {|C|}Nξ ⊎ ∑_{Dm(σ)}(v_{j}, v_{j}σ) ≠ ε iff [[C]]ξσ iff ξσ = (ξ ⊎ {|C|}Nξ)σ.

Proof: Notice, in the definition of the two evaluation functions, the correspondence between tt and the empty relation ϕ and the one between ff and the inconsistent relation ε. Then the thesis is an immediate consequence of the definition of variable substitution. □

Making use of variable substitutions, the functional behaviours of non-ground late πξ-calculus processes can be related to the behaviours of ground agents. It can be shown that a precise relationship there exists. We informally explain it in the following.

- Suppose that a ground environment is defined to be equal to ξσ with ξ nonground and σ variable substitution for ξ. Then the fact that ξσ :: P can move implies that ξ :: P can move as well, since its functional behaviour is distinct from ⊥ in at least one point.

- For the other way round, if the non-ground environment ξ′ is reached by executing the observable function f then there exists a corresponding ground step for each point of definedness of f.

Proposition 33 Let ξ :: P be a non-ground πξ-calculus process. Then the following holds.

1. Assume ξσ :: P \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξ′′ :: P′ with σ variable substitution for ξ.

Then ξ :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{f} ξ′ :: P′ with f(Im(σ)) = ρ. Also, σ is a variable substitution for ξ′ and ξ′′ = ξ′σ.

2. Assume ξ :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{f} ξ′ :: P′.

Then f(c̃) ≠ ⊥ iff c̃ = Im(σ′) with σ′ variable substitution for ξ′. Moreover any σ′ such that f(Im(σ′)) ≠ ⊥ is also a variable substitution for ξ and

ξσ′ :: P \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξ′σ′ :: P′ with ρ = f(Im(σ′)).

Proof:

1. Let ξσ :: P \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξ′′ :: P′

⟹ P ⟶^{⟨α,C⟩} P′′ with [[C]]ξσ and P′′ such that either P′ ≡ P′′ or P′ ≡ λy.P′′

depending on α ⟹ By Prop. 32 and the hypothesis that σ is a variable substitution for ξ it follows that ξ ⊎ {|C|}Nξ ≠ ε and that (ξ ⊎ {|C|}Nξ)σ = ξσ ⟹ The thesis comes by the definitions of η, η_{N}, δ, δ_{N} and by the definition of variable substitution.

2. Assume ξ :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{f} ξ′ :: P′

⟹ P ⟶^{⟨α,C⟩} P′′ with ξ ⊎ {|C|}Nξ ≠ ε and P′′ such that either P′ ≡ P′′ or

P′ ≡ λy.P′′. Moreover, the thesis that f(c̃) ≠ ⊥ iff c̃ = Im(σ′) with σ′ variable substitution for ξ′ directly comes by the definition of variable substitution. In fact variable substitutions are the only possible associations of variables with constants which do not give raise to inconsistency. Hence any c̃ distinct from the codomain of a variable substitution for ξ′ is such that ξ′ ⊎ ∑_{i=1}^{m}(v_{i}, c_{i}) = ε which implies f(c̃) = ⊥. Also, as in general ξ′ encodes more constraints than ξ does, any variable substitution for ξ′ is a variable substitution for ξ as well ⟹ By Prop. 32 and the hypothesis that σ′ is a variable substitution for ξ it follows that [[C]]ξσ′ holds. Hence the thesis that ξσ′ :: P \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξ′σ′ :: P′ is a consequence of the definitions of of η, η_{N}, δ, δ_{N}. □

We can now state a more efficient characterization of strong late non-ground πcalculus semantics. The coincidence result exploits the relationship between nonground πξ-processes and the πξ-agents obtained by λ-closure. On the one hand, non-ground environments are let to burst out into sets of ground environments. On the other way round, sets of ground environments are given a compact representation via one single non-ground environment.

Theorem 34 (coincidence with strong late non-ground semantics) Let P_{1}, P_{2} be π-calculus processes and let L be a list containing all and only the elements of the set N = fn(P_{1}, P_{2}). Then P_{1} ∼_{L} P_{2} iff ξ^{L} :: P_{1} ∼_{η_{N}} ξ^{L} :: P_{2}.

Proof: We prove in the following that

ξ^{L} :: P_{1} ∼_{η_{N}} ξ^{L} :: P_{2} iff Id_{E} :: λ clos(P_{1}, L) ∼ Id_{E} :: λ clos(P_{2}, L)

then the thesis comes by Th. 22.

(if) Assume that a relation S ⊆ ∼_{η_{N}} there exists with (ξ^{L} :: P_{1}, ξ^{L} :: P_{2}) ∈ S. Then transform the relation S into the relation S_{λ} ∪ S_{1} with the two components defined as follows.

S_{λ} = ⋃_{L_{2},ξ_{L_{1}}} {(ξ_{L_{1}} :: λ clos(P_{1}, L_{2}), ξ_{L_{1}} :: λ clos(P_{2}, L_{2}))}

where L_{1}, L_{2} are lists such that L = [L_{1}, L_{2}] and, for j = 1, 2, the environment ξ_{L_{1}} ranges over the environments which are reachable from Id_{E} :: λ clos(P_{j}, [L_{1}, L_{2}]) by firing the λ-abstractions over the names contained in L_{1}.

S_{1} = ⋃_{(ξ_{P}::P,ξ_{Q}::Q)∈S}{(adj con(ξ_{P} σ) :: P, adj con(ξ_{Q}σ) :: Q)}

where σ is a variable substitution for both ξ_{P} and ξ_{Q} and adj con( ) is a function which possibly renames the constants of the defined equivalence classes of its argument. The use of the function adj con( ) is due to the fact that, when applying a variable substitution to a non-ground environment, some care is needed in order to be respectful of the constant generation mechanism. For instance, assume that such a mechanism returns in the order the constants (c_{1}, c_{2}, c_{3}, …) and that ξ = Id_{E} + (x, v_{1} : {c_{1}}) + (z, v_{2} : {c_{1}, c_{2}}) + (y, c_{3}) and eventually that σ = {c_{1}/v_{1}, c_{1}/v_{2}}. In such a case ξσ = Id_{E} + (x, c_{1}) + (z, c_{1}) + (y, c_{3}). Instead of this we want to get the environment Id_{E} + (x, c_{1}) + (z, c_{1}) + (y, c_{2}). That is why we use the function adj con(ξσ). It is supposed to suitably act on [c]_{ξσ} in order to let allD(ξσ) be given by the first k generated constants whenever card(allD(ξσ)) = k. By construction the relation S_{λ} ∪ S_{1} contains the pair (Id_{E} :: λ clos(P_{1}, L), Id_{E} :: λ clos(P_{2}, L)). We now want to prove that (S_{λ} ∪ S_{1}) ⊆ ∼. Given any pair (ξ_{L_{1}} :: P, ξ_{L_{1}} :: Q) ∈ S_{λ} it can be easily proved that whenever ξ_{L_{1}} :: P moves then the process ξ_{L_{1}} :: Q can match the move and the derivative agents are either in S_{λ} or in S_{1}. Letting y_{n} be the last name in the list L, the only care is relative to processes of the shape P ≡ λy_{n}.P_{i} and Q ≡ λy_{n}.P_{j} with i, j = 1, 2 and i ≠ j. In such cases the thesis that the derivative agents belong to the relation S_{1} just depends on the definitions of λ clos( , L) and of ξ^{L}. In fact, suppose that y_{k} is the k-th element of the list L. Then there is a neat relationship between the set of constants associated with y_{k} in the environments which are derivable from Id_{E} :: λ clos( , L) and the type of the variable associated with y_{k} in the environment ξ^{L}. Both the two sets are given by the first k generated constants. Then the thesis directly comes from the definition of variable substitution. Now consider the relation S_{2} defined as it follows.

S_{2} = ⋃_{(ξ_{P}::P,ξ_{Q}::Q)∈S}{(ξ_{P} σ :: P, ξ_{Q}σ :: Q)}

where σ is a variable substitution for both ξ_{P} and ξ_{Q}. As far as the proof that S_{1} ⊆ ∼ is concerned, we get rid of the function adj con( ) and show instead that the relation S_{2} is a late ground strong bisimulation. Then the thesis is a consequence of Prop. 17. Assume that (ξ_{P} σ :: P, ξ_{Q}σ :: Q) ∈ S_{2} because of (ξ_{P} :: P, ξ_{Q} :: Q) ∈ S with σ variable substitution for both ξ_{P} and ξ_{Q}. Also assume that ξ_{P} σ :: P \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξ′′ :: P′.

⟹ By Prop. 33 it follows that ξ_{P} :: P \begin{matrix}− \\ − \end{matrix}▷^{f} ξ_{P′} :: P′ with ρ = f(Im(σ)) and σ variable substitution also for ξ_{P′} and ξ′′ = ξ_{P′}σ ⟹ By (ξ_{P} :: P, ξ_{Q} :: Q) ∈ S it follows that some ξ_{Q′} :: Q′ there exists such that

ξ_{Q} :: Q \begin{matrix}− \\ − \end{matrix}▷^{f} ξ_{Q′} :: Q′ with (ξ_{P′} :: P′, ξ_{Q′} :: Q′) ∈ S

⟹ By Prop. 33 and by f(Im(σ)) = ρ it comes that ξ_{Q}σ :: Q \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξ_{Q′}σ :: Q′ with σ variable substitution for ξ_{Q′} ⟹ By (ξ_{P′} :: P′, ξ_{Q′} :: Q′) ∈ S and by definition of S_{2} it follows that (ξ_{P′}σ :: P′, ξ_{Q′}σ :: Q′) ∈ S_{2} (only if) Assume that the relation T ⊆ ∼ contains the pair (Id_{E} :: λ clos(P_{1}, L), Id_{E} :: λ clos(P_{2}, L)). Then define the relation T′ acting as follows. For each subset of T of the shape

⋃_{σ}{(adj con((ξ^{L} + ξ_{P})σ)) :: P, adj con((ξ^{L} + ξ_{Q})σ) :: Q)}

where P, Q ≢ λz.R for z ∈ N and σ is a variable substitution for both (ξ^{L} + ξ_{P}) and (ξ^{L} + ξ_{Q}), the relation T′ is let to contain the pair (ξ^{L} + ξ_{P} :: P, ξ^{L} + ξ_{Q} :: Q). By the definitions of λ clos( , ) and of variable substitution, the pair (ξ^{L} :: P_{1}, ξ^{L} :: P_{2}) is contained in T′. We now prove that T′ ⊆ ∼_{η_{N}}. Assume that the pair (ξv_{P} :: P, ξv_{Q} :: Q) is put in T′ because of

⋃_{σ}{(adj con(ξv_{P}σ) :: P, adj con(ξv_{Q}σ) :: Q)} ⊆ T

Also, suppose that ξv_{P} :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{f} ξv_{P′} :: P′ ⟹ By Prop. 33 for all c̃ such that f(c̃) ≠ ⊥ it holds that c̃ = Im(σ′) with σ′ variable substitution for both ξv_{P} and ξv_{P′}. Moreover it also holds that ξv_{P}σ′ :: P \begin{matrix}− \\ − \end{matrix}▷^{ρ}

ξv_{P′}σ′ :: P′ with ρ = f(c̃)

⟹ By definition of the function adj con( ) and by

⋃_{σ}{(adj con(ξv_{P}σ) :: P, adj con(ξv_{Q}σ) :: Q)} ⊆ T ⊆ ∼

it follows that ξv_{Q}σ′ :: Q \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξv_{Q′}σ′ :: Q′ with

{(adj con(ξv_{P′}σ′) :: P′, adj con(ξv_{Q′}σ′) :: Q′)} ⊆ T

⟹ ξv_{Q} :: Q \begin{matrix}− \\ − \end{matrix}▷_{η_{N}}^{h} ξv_{Q′} :: Q′ with (ξv_{P′} :: P′, ξv_{Q′} :: Q′) ∈ T′ by

{(adj con(ξv_{P′}σ′) :: P′, adj con(ξv_{Q′}σ′) :: Q′)} ⊆ T

for all σ′ which is a variable substitution for both ξv_{P′} and ξv_{Q′} and where h = f. In fact, by the assumed generality of σ′, the two functions are point-wise equal on each c̃ = Im(σ′) and by Prop. 33 these are the only points where the two functions are distinct from ⊥. □

5.2 Digression on open semantics

In order to show the flexibility of the non-ground πξ-calculus, we now go further in adopting a functional interpretation of processes and show an alternative characterization of π-calculus open semantics, whose definition follows [San96].

Definition 35 A binary symmetric relation S is an open bisimulation if P S Q implies that for all name substitutions σ

if P σ ⟶^{α} P′ with bn(α) ∉ fn(P σ, Qσ), then for some Q′, Qσ ⟶^{α} Q′ and

P′ S Q′

P is open bisimilar to Q, written P ∼_{O} Q, if P S Q for some open bisimulation S.

□

{P ⟶^{ω} P′  ξ′ ∈ η_{O}(ξ, ω)  ρ ⊑ δ_{O}(ξ′, ω)  ρ ≠ \underline{⊥} \atop ξ :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{O}}^{ρ} ξ′ :: P′}

Table 9: definition of \begin{matrix}− \\ − \end{matrix}▷_{η_{O}}

Open semantics moves name instantiation inside the definition of bisimulation, immediately qualifying itself as a congruence. Indeed, as well as late non-ground bisimilarity, it involves a universal quantification over substitutions, so requiring at each step an infinite number of checks. Nevertheless, a more efficient characterization of open bisimilarity was proposed. It is based on a specialized transition system that allows name substitutions to be delayed as much as possible.

The πξ-calculus open semantics is in that same spirit. Indeed, free names and instantiation are interpreted much as variables and unification are dealt with in logic programming. When an input action fires, a variable is associated with the formal parameter of the performed action. This shows up in the definitions of the open πξ-calculus transition system, denoted by \begin{matrix}− \\ − \end{matrix}▷_{η_{O}}, where the actualization of input placeholders is delayed as much as possible. The transition relation \begin{matrix}− \\ − \end{matrix}▷_{η_{O}} is reported on Tab. 9, and again the actual πξ-semantics is given by the induced strong bisimulation, written ∼_{η_{O}}. There is no need here to let the transition relation be parametric over a set of names. In fact, the present instantiation strategy genuinely consists in delaying actualization as much as possible. At any point during computation, all the variables can still be considered as formal parameters. This implies that the evaluation function can always add constraints on variables. More specifically, suppose that one name out of x and y, or also both, are associated with a variable. If so, evaluating whether or not x = y in ξ results in the constraint (x, y). Then the addition of ξ with the relation (x, y)

- either respects the required equality (e.g. [x]_{ξ} = [y]_{ξ} = {x, y, c})

- or induces the required equality (e.g. [x]_{ξ} = {x, c} and [y]_{ξ} = {y, v : {c} ∪ D} or, also, [x]_{ξ} = {x, v_{1} : D} and [y]_{ξ} = {y, v_{2} : D ∪ D′})

- or causes inconsistency (e.g. [x]_{ξ} = {x, c_{1}} and [y]_{ξ} = {y, c_{2}})

The refined evaluation function ⟨[C]⟩ξ is reported in Tab. 10 together with specialized update and result functions for open semantics. As far as ⟨[x = y]⟩ξ is concerned, notice that a constraint is added to the environment only when (ξ(x)↓ and ξ(y)↓). If this is not the case, then we have just to test whether or not (x ξ y). In fact, if (ξ(x)↑ or ξ(y)↑) then at least one name out of x and y is private. Think, for instance, of the obligation in the symbolic action o_{x}⟨\overline{z}y, z ↓⟩ = ⟨\overline{z}(y), x = y ∧ z ↓⟩. The issue of variable instantiation plays no role when x and y are as above: no association can make them to be the same.

⟨[C]⟩ξ = case C in

              true : ϕ
             false : ε

x↓ : ξ(x)↓ ⟶ ϕ, ε
x = y : (ξ(x)↓ and ξ(y)↓) ⟶ (x, y), x ξ y ⟶ ϕ, ε
x ≠ y : x ξ y ⟶ ε, ϕ
C_{1} ∧ C_{2} : ⟨[C_{1}]⟩ξ ⊎ ⟨[C_{2}]⟩ξ

          end case

η_{O}ξαC = case ξ ⊎ ⟨[C]⟩ξ in
ε : ∅

             ξ_{1} : case α in

τ : ξ_{1}
τ[x/y] : ξ_{1} + (y, x)
\overline{x}(y), \overline{x}y : ξ_{1}(y)↓ ⟶ ξ_{1}, ξ_{1} + (y, newD(ξ_{1}))
x(y) : ξ_{1} + (y, newV(ξ_{1}) : (allD(ξ_{1}) ∪ newD(ξ_{1})))
[y] : ξ_{1}

                   end case
            end case

δ_{O}ξαC = λd_{1} : D_{1} … λd_{m} : D_{m} . case ξ ⊎ ∑_{i=1}^{m}(v_{i}, d_{i}) in
ε : ⊥

                                    ξ_{1} : case α in

\begin{aligned}τ, τ[x/y] & : & τ \\ \overline{x}(y), \overline{x}y & : & \overline{ξ_{1}(x)}ξ_{1}(y) \\ x(y) & : & ξ_{1}(x) \\ [y] & : & [ξ_{1}(y)] \end{aligned}

                                          end case
                                   end case

where {v_{1} : D_{1}, …, v_{m} : D_{m}} = allV(ξ), D_{1} ⊂ D_{2} ⊂ … ⊂ D_{m}
Table 10: definition of (η_{O}, δ_{O})

Apart from the use of distinct criteria for evaluating obligations, the function η_{O} differs from η_{N} only as far as input actions are concerned. The improvement in efficiency over the transition systems described so far is made evident by the fact that η_{O}(ξ, x(y), C) causes – at most – the association of the name y with one single fresh variable. The information that such a variable may assume any of the constants already active in ξ or a new one is coded in the variable type. This treatment of input actions delays as much as possible the actual instantiation of the parameter. More properly, the instantiation is fully delegated to the constraint system implemented by the evaluation function ⟨[ ]⟩ and hence it takes place only if, and when, it is strictly necessary for the computation to go on.

The definition of the result function δ_{O} is analogous to the one of δ_{N}. Anyway, contrary to δ_{N}, the number of arguments of the function returned by δ_{O} is not a priori fixed by the definition of the non-ground environment ξ^{L} chosen to start running. Here, the result yielded by δ_{O} is a function of all the names in the list L and of all the placeholders of the input actions already fired. The act of inputting potentially makes free one more name. Hence, assuming the list L in ξ^{L} to contain all the free names of the initial π-calculus process, the present transition system interprets any agent as a function of all its free names.

The open instantiation strategy can be illustrated by means of the following example.

Example 36 Let ξ^{L} be defined as it follows.

ξ^{L} = Id_{E} +(x, v_{1} : {c_{1}}) + (z, v_{2} : {c_{1}, c_{2}})

We investigate on the values returned by η_{O} and by δ_{O} when they are applied to distinct environments and symbolic actions.

1. Assume ω = ⟨x(y), x↓⟩ and suppose newD(ξ^{L}) = c_{3}. Then

\begin{matrix}η_{O}(ξ^{L}, ω) = \{ξ^{L} + (y, v_{3} : \{c_{1}, c_{2}, c_{3}\})\} \\ δ_{O}(ξ^{L} + (y, v_{3}), ω) = λd_{1} : \{c_{1}\}.λd_{2} : \{c_{1}, c_{2}\}.λd_{3} : \{c_{1}, c_{2}, c_{3}\}. d_{1} \end{matrix}

2. For ω′ = ⟨τ, true⟩ the following holds.

\begin{matrix}η_{O}(ξ^{L} + (y, v_{3}), ω′) = \{ξ^{L} + (y, v_{3})\} \\ δ_{O}(ξ^{L} + (y, v_{3}), ω′) = λd_{1} : \{c_{1}\}.λd_{2} : \{c_{1}, c_{2}\}.λd_{3} : \{c_{1}, c_{2}, c_{3}\}. τ \end{matrix}

3. Suppose now ω′′ = ⟨τ, y = z⟩. In such a case

η_{O}(ξ^{L} + (y, v_{3}), ω′′) = {ξ^{L} + (y, v_{3}) + (y, z)}
δ_{O}(ξ^{L} + (y, v_{3}) + (y, z), ω′′) =
λd_{1} : {c_{1}}.λd_{2} : {c_{1}, c_{2}}.λd_{3} : {c_{1}, c_{2}, c_{3}}. d_{3} = d_{2} → τ, ⊥

Given any name substitution σ, the result yielded by δ_{O}(ξ^{L}+(y, v_{3})+(y, z), ω′′) means that the action τ may be performed only with the proviso that y is instantiated by zσ. In the meanwhile, the name zσ could be either the same as xσ (d_{1} = d_{2} = d_{3} = c_{1}) or distinct from it (d_{1} = c_{1} and d_{2} = d_{3} = c_{2}). Obviously, when y is instantiated by a name which is assumed to be fresh w.r.t. all the other names around (d_{3} = c_{3}) the requirement y = zσ cannot be met. □

Open π-calculus semantics distinguishes the process x(y).(τ.τ + τ) from x(y).(τ.τ + τ + τ.[y = z]τ). Correspondingly in the πξ-calculus, we can see that

ξ^{L} :: x(y).(τ.τ + τ) ≁_{O} ξ^{L} :: x(y).(τ.τ + τ + τ.[y = z]τ)

for ξ^{L} = Id_{E} +(x, v_{1} : {c_{1}}) + (z, v_{2} : {c_{1}, c_{2}}). The reason for this is that process ξ^{L} :: x(y).(τ.τ + τ) cannot win any bisimulation game started by the partner and terminating in the state ξ^{L} + (y, v_{3}) :: [y = z]τ. More precisely, a bisimulation relation should contain

- either the pair (ξ^{L} + (y, v_{3}) :: [y = z]τ, ξ^{L} + (y, v_{3}) :: τ)
- or the pair (ξ^{L} + (y, v_{3}) :: [y = z]τ, ξ^{L} + (y, v_{3}) :: nil)

This is impossible. In the first case the process ξ^{L} + (y, v_{3}) :: [y = z]τ could not match the move (λd_{1}d_{2}d_{3}.τ) performed by ξ^{L} + (y, v_{3}) :: τ. In the second case, the deadlocked ξ^{L} + (y, v_{3}) :: nil could not react to any ρ ⊑ λd_{1}d_{2}d_{3}. d_{3} = d_{2} → τ, ⊥.

The following proposition, analogous to Prop. 32, provides the basis for the encoding of open non-groundness into the ground πξ-calculus.

Proposition 37 Let σ be a variable substitution for ξ, and C be an obligation. Then ξ ⊎ ⟨[C]⟩ξ ≠ ε iff ξ ⊎ ⟨[C]⟩ξ ⊎ ∑_{Dm(σ)}(v_{j}, v_{j}σ) ≠ ε iff [[C]]ξσ.

Proof: The statement is a direct consequence of the definitions of the involved evaluation functions and of variable substitution. The only interesting difference between [[ ]] and ⟨[ ]⟩ raises from the evaluation of obligations of the shape x = y when (ξ(x)↓ and ξ(y)↓). So, assume ξ ⊎ ⟨[x = y]⟩ξ ≠ ε. This does hold iff [x]_{ξ} and [y]_{ξ} are

- either both defined-by-constant and such that [x]_{ξ} ∩ D = [y]_{ξ} ∩ D

- or both defined-by-variable

- or one is defined-by-variable via v : D and the other is defined-by-constant via c ∈ D

Then the theses by definition of variable substitution and of ξσ. □

The next statement is the actual corresponding of Prop. 33. It addresses the relationship between variable substitutions and functional observations.

Proposition 38 Assume ξ :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{O}}^{f} ξ′ :: P′. Then the following holds.

1. f(c̃) ≠ ⊥ iff c̃ = Im(σ) with σ variable substitution for ξ′

2. if σ is a variable substitution for ξ′ then frag(σ, ξ) is a variable substitution for ξ, where frag(σ, ξ) = {v_{1}σ/v_{1}, …, v_{m}σ/v_{m}} for allV(ξ) = {v_{1}, …, v_{m}}

Proof:

1. By definition, the set of the variable substitutions for a given environment represents all the possible ways to transform variables into constants without giving raise to inconsistency. Hence, in the definition of δ_{O} the sum ξ′ ⊎ ∑_{i=1}^{m}(v_{i}, c_{i}) is distinct from the distinguished element ε iff the tuple (c_{1}, …, c_{m}) is the codomain of some variable substitution.

2. The updated environment ξ′ potentially encodes some constraints more than ξ. Then, although the other way round is not true, whenever allV(ξ′) = allV(ξ) any variable substitution for ξ′ is a variable substitution for ξ as well. By definition of η_{O}, correspondingly to the symbolic execution of the input action x(y) it holds that allV(ξ′) = allV(ξ) ∪ {v_{m} : D_{m}}. In such a case a variable substitution for ξ may be obtained by the variable substitution σ for ξ′ by simply getting rid of the component relative to the variable v_{m}. In fact, correspondingly to the execution of x(y) it holds that [y]_{ξ} = {y} and [y]_{ξ′} = {y, v_{m}}. Hence any variable substitution for ξ′ has the shape σ^{v}{c_{m}/v_{m}} with c_{m} ∈ D_{m} and Dm(σ^{v}) = allV(ξ). □

The following characterization theorem concludes our investigation into call-by-need instantiation strategies in the πξ-calculus. The proof of the result involves either the previous encoding of non-groundness into groundness or the encoding of πξ-calculus into π-calculus (and back) reported in Appendix A.

Theorem 39 (coincidence with open semantics) Let P_{1}, P_{2} be π-calculus processes and let L be a list containing all and only the elements of fn(P_{1}, P_{2}). Then P_{1} ∼_{O} P_{2} iff ξ^{L} :: P_{1} ∼_{η_{O}} ξ^{L} :: P_{2}

Proof: See Appendix B. □

6 Concluding remarks

We provided operational and axiomatic characterizations of late, either strong or weak, π-calculus congruences. A coincidence result with open semantics was also shown. Target languages of our characterizations were either the π-calculus or the πξ-calculus, a process algebra whose ground version was already proved to coincide with ground π-calculus.

The main contributions of the paper are the finitary nature of the proposed characterizations and the fact that they allow π-calculus semantics to be rephrased in terms of CCS equivalences which come equipped with well-known mathematical properties and verification tools. By this, our results could be particularly promising in the perspective of veryfing mobile systems.

Relating to π-calculus, it was shown that each non-ground equivalence relation can be expressed by closing the corresponding ground bisimilarity under the substitutions of a suitable finite family {σ_{i}}_{i}. This result can be directly instantiated to early semantics, either strong or τ-forgetting [Qua96]. So, the cardinality of {σ_{i}}_{i} gives full insights about the actual complexity of π-congruence checking, both late and early.

Then, the πξ-calculus view allowed processes to be explicitely interpreted as functions of their free names. So we resorted, in turn, to ground environments paired with λ-closures of π-processes, and to functional environments paired with standard π-processes.

The main advantage of the first of these approaches is that the mere evolution of a λ-closed term induces the generation of (the environments corresponding to) the substitutions {σ_{i}}_{i} needed to check non-groundness. This, on its side, adds effectiveness to the very first alternative characterization we presented. Also, interpreting late congruence as bisimilarity of ground πξ-processes permits equational characterizations for non-groundness to be directly stated on the πξ-calculus axiom system for groundness [FMQ95].

Eventually, by introducing the non-ground dual of ground πξ-calculus, we exploited, for the characterization of both late and open semantics, a more promising call-by-need discipline for the instantiation of the arguments which the running process is considered to depend on. Analogous instantition strategies are a common feature of symbolic semantics for data-dependent calculi [HL95]. Indeed, a call-by-need discipline underlies the alternative characterizations of late and open π-calculus semantics presented in [Lin95, Lin94] and [San96], respectively. The relationship between their approach and the one proposed here deserves further investigation. What is immediately evident is the difference at the extensional level. Symbolic semantics is defined as closure over a family of bisimulation relations indexed by equalities and inequalities on names. By contrast, in the non-ground πξ-calculus, the call-by-need strategy is adopted just to recognize the minimal symbolic requirements for the computation to go on. Then those requirements are actually interpreted and made concrete by updating environments. So, πξ-processes are equated by standard bisimulation semantics.

Another topic for future work, suggested by the proposed functional interpretation of processes, is the study of possible relationships between our results and the π-calculus presentation in [HLMP97].

A final comment is about non-ground π-calculus semantics of the early family. They can be characterized using an approach analogous to that we adopted for the late case. Precisely, the early view can be retrieved as a special case of late πξ-semantics by minor changes to the ground and non-ground transition systems [Qua96]. In the same spirit as the free input actions of [MPW93], those changes essentially amount to make atomic any input step and the subsequent instantiation move.

Acknowledgments

We would like to thank Gian-Luigi Ferrari and Ugo Montanari for the joint work that provided the basis of the πξ-calculus, and for helpful comments relating to this.

References

[Abr91] S. Abramsky. A Domain Equation for Bisimulation. Information and Computation, 92(2):161–218, 1991.

[ABV94] L. Aceto, B. Bloom, and F. Vaandrager. Turning SOS Rules into Equations. Information and Computation, 111(1):1–52, 1994.

[Ace94] L. Aceto. On “axiomatising finite concurrent processes”. SIAM Journal of Computing, 23(4):852–863, 1994.

[BK84] J.A. Bergstra and J.W. Klop. Process Algebra for Synchronous Communication. Information and Control, 60:109–137, 1984.

[CPS93] R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems. ACM Trans. on Programming Languages and Systems, 15(1):36– 72, 1993.

[DS85] R. De Simone. Higher level synchronizing devices in MEIJE-SCCS. Theoretical Computer Science, 37(3):245–267, 1985.

[FMQ95] G.-L. Ferrari, U. Montanari, and P. Quaglia. The Weak Late π-calculus Semantics as Observation Equivalence. In I. Lee and S.A. Smolka, editors, Proc. 6th International Conference on Concurrency Theory, CON-CUR ’95, volume 962 of LNCS, pages 57–71. Springer-Verlag, 1995.

[FMQ96] G.-L. Ferrari, U. Montanari, and P. Quaglia. A π-calculus with Explicit Substitutions. Theoretical Computer Science, 168(1):53–103, 1996.

[Hen88] M. Hennessy. Axiomatising finite concurrent processes. SIAM Journal of Computing, 17(5):997–1017, 1988.

[HL95] M. Hennessy and H. Lin. Symbolic Bisimulations. Theoretical Computer Science, 138:353–389, 1995.

[HLMP97] F. Honsell, M. Lenisa, U. Montanari, and M. Pistore. Final Semantics for the π-calculus. Submitted for publication, 1997.

[HM85] M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM, 32(1):137–161, 1985.

[Lin94] H. Lin. Symbolic Bisimulation and Proof Systems for the π-Calculus. Technical Report 7/94, School of Cognitive and Computing Sciences, University of Sussex, 1994.

[Lin95] H. Lin. Complete Inference Systems for Weak Bisimulation Equivalences in the π-Calculus. In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, Proc. 6th International Joint Conference CAAP/FASE, TAP-SOFT ’95, volume 915 of LNCS. Springer-Verlag, 1995.

[Mil80] R. Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer-Verlag, 1980.

[Mil83] R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983.

[Mil89] R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

[Mil92] R. Milner. The Polyadic π-Calculus: a Tutorial. In F.L. Bauer, W. Brauer, and H. Schwichtenberg, editors, Logic and Algebra of Specification, pages 203–246. Springer-Verlag, 1992.

[MPW92] R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes, Part I and II. Information and Computation, 100(1):1–77, 1992.

[MPW93] R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. Theoretical Computer Science, 114(1):149–171, 1993.

[Par81] D. Park. Concurrency and automata on infinite sequences. In Proc. 5th GI-Conference, volume 104 of LNCS. Springer-Verlag, 1981.

[Plo81] G. D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI-FN-19, Computer Science Department, Aarhus University, 1981.

[Qua96] P. Quaglia. The π-calculus with explicit substitutions. PhD thesis, Università degli Studi di Pisa, Dipartimento di Informatica, 1996. Report TD-09/96.

[San96] D. Sangiorgi. A Theory of Bisimulation for the π-calculus. Acta Informatica, 33(1):69–97, 1996.

Appendix A

We recall in the following the main constructions and encodings needed to show Th. 7. They result from mild simplifications of analogous statements appeared in [FMQ96]. These simplifications, on their hand, are essentially due to the introduction of explicit λ-prefixes which allows us to avoid the use of more sophisticated environments, similar to those presented in Sec. 5 of this paper.

As commented in Sec. 2, the proof of the characterization result is quite complex. The definitions and the few auxiliary statements that follow are not meant to cover each single detail. They have rather been selected to bear out a sketch of the proof of Th. 7, and to provide the formal constructions used in Appendix B to show Th. 39. Complete proofs and detailed comments on encodings can be found in [Qua96], Chapter 3.

The first definition presents the core issue of the transformation of environments into actual name substitutions. Roughly, each relevant name x in ξ is classified according to the following criterion:

- it was involved in the communication of a bound name and there is still a name z ∈ [x]_{ξ} which occurs bound in P;

- it was involved in a communication which should be indeed a closing communication;

- it is really (i.e. semantically) a free name of ξ :: P, namely ξ(x)↓.

Definition 40 (restriction, constant, admissible substitutions) Let ξ :: P be a πξ-calculus process. Also, given the set A ⊆ N, assume to be able to choose a canonical representative of A, say crep(A) ∈ A. (E.g. assume the existence of a standard ordering on the names in N, then crep(A) might be the least element of A w.r.t. that order). Then we define the following substitutions.

- letting rep(x, ξ :: P) = z whenever ([x]_{ξ} ∩ bn(P)) = {z}

s(ξ :: P) = {rep(x_{0}, ξ :: P)/x_{0}, …, rep(x_{m}, ξ :: P)/x_{m}}

where Dm(s(ξ :: P)) = {x | card([x]_{ξ}) ≥ 2 and ξ(x)↑ and ([x]_{ξ} ∩bn(P)) ≠ ∅}

- the restriction substitution σ^{r} of ξ :: P is

σ^{r}(ξ :: P) = {crep([x_{0}]_{ξ})/x_{0}, …, crep([x_{m}]_{ξ})/x_{m}}

where Dm(σ^{r}(ξ :: P)) = {x | card([x]_{ξ}) ≥ 2 and ξ(x)↑ and ([x]_{ξ} ∩ bn(P)) = ∅}

- the constant substitution σ^{c} of ξ is

σ^{c}(ξ) = {ξ(x_{0})/x_{0}, …, ξ(x_{m})/x_{m}}

where Dm(σ^{c}(ξ)) = {x | [x]_{ξ} is defined-by-constant}

- an admissible name substitution for {c_{0}, …, c_{j}, c_{j+1}, …, c_{j+k}} is an injective substitution

rsp(R, P) = case R in

\begin{aligned}∅ & : & \{P \} \\ \{x\} ∪ R′ & : & ⋃_{y∈ R} ⋃_{P′∈ rnp(y,P)} rsp(R \ \{y\}, P′) \end{aligned}

                end case

where

rnp(y, P) = case P in

                      nil : {nil}

α.P_{1} : {α.P_{1}}
[x = z]P_{1} : {[x = z]P_{1}}
P_{1} + P_{2} : {P_{1} + P_{2}}
P_{1} | P_{2} : y ∈ (fn(P_{1}) ∩ fn(P_{2})) ⟶ {(y)(P_{1} | P_{2})},
{(y)(P_{1} | P_{2})}∪
{(P_{1} | P′_{2}) s.t. P′_{2} ∈ rnp(y, P_{2}) and y ∈ bn(P_{1} | P′_{2})}
{(P′_{1} | P_{2}) s.t. P′_{1} ∈ rnp(y, P_{1}) and y ∈ bn(P′_{1} | P_{2})}
(z)P_{1} : {(z)P′ s.t. P′ ∈ rnp(y, P_{1})}
!P_{1} : {!P_{1}}

                end case

Table 11: definition of rsp( , )

σ^{n} = {ı^{−1}(c_{0})/c_{0}, …, ı^{−1}(c_{j})/c_{j}, x_{1}/c_{j+1}, …, x_{k}/c_{j+k}}

where {c_{0}, …, c_{j}} ⊆ D_{I} and {c_{j+1}, …, c_{j+k}} ⊆ D_{RT} and ı : N_{I} → D_{I} is the bijective mapping of Def. 4 and {x_{1}, …, x_{k}} ⊆ N □

The coming definition supplies us with the formal machinery needed to recover the lack in πξ-calculus of a proper analogous of the Close rule. Given a set of names R and a process P, the function rsp(R, P) returns a set of processes where the names in R are non-deterministically put on top of the parallel compositions in P.

We then proceed with the formalization of the actual encoding of πξ-calculus into π-calculus.

Definition 41 (rsp(R, P)) Let R be a finite set of names, and let P be a π-calculus process. The set rsp(R, P) is defined in Table 11. □

\underline{Notation} Given a π-calculus process P and a substitution s, we denote by [P]^{s} the process obtained from P by substituting any free occurrence of x by xs, without caring of name clashes. Then, given [P]^{s} and a substitution σ with Dm(σ) = bn([P]^{s}), we denote by [P]_{σ}^{s} the α-conversion of [P]^{s} which respects σ, namely the π-calculus process obtained by substituting any occurrence of y ∈ bn([P]^{s}) by yσ.

□

Translation 1 (from ground πξ-calculus to π-calculus) Let S be a bisimulation for η-reachable πξ-calculus processes. Then

T r_{ξ}(S) = ⋃_{(ξ_{P}::P′,ξ_{Q}::Q′)∈S} T r_{ξ}((ξ_{P} :: P, ξ_{Q} :: Q))

where

- P ≡ P′′ if P′ ≡ λy.P′′ and P ≡ P′ otherwise
- Q ≡ Q′′ if Q′ ≡ λz.Q′′ and Q ≡ Q′ otherwise
- T r_{ξ}((ξ_{P} :: P, ξ_{Q} :: Q)) is the set of pairs (P_{π}, Q_{π}) such that
- P_{π} ≡_{α} P̂(σ^{c}(ξ_{P})σ^{n})
- Q_{π} ≡_{α} Q̂(σ^{c}(ξ_{Q})σ^{n})
- P̂ ∈ rsp(Im(σ^{r}(ξ_{P} :: P)), [P]^{s(ξ_{P}::P)}σ^{r}(ξ_{P} :: P))
- Q̂ ∈ rsp(Im(σ^{r}(ξ_{Q} :: Q)), [Q]^{s(ξ_{Q}::Q)}σ^{r}(ξ_{Q} :: Q))

- σ^{n} admissible name substitution for Im(σ^{c}(ξ_{P})) ∪ Im(σ^{c}(ξ_{Q})). □

Remark 42 Let P_{π} and Q_{π} be as in Trans. 1. By definition, for some P_{r} without homonymy either among bound names or among free and bound names P_{π} ≡_{α} P_{r} where

- P_{r} ∈ rsp(Dm(σ^{r}(ξ_{P} :: P))σ_{P} , [P]_{σ′_{P}}^{s(ξ_{P}::P)}σ_{P})

- σ_{P} = σ^{r}(ξ_{P} :: P)σ′′_{P}(σ^{c}(ξ_{P})σ^{n})

- σ′_{P} , σ′′_{P} are, respectively, the refreshment of the bound names of P and the refreshment of the names in Im(σ^{r}(ξ_{P} :: P))

Similarly, for a suitable Q_{r} without homonymy and for suitable substitutions σ′_{Q}, σ′′_{Q}, it holds that

Q_{π} ≡_{α} Q_{r} ∈ rsp(Dm(σ^{r}(ξ_{Q} :: Q))σ_{Q}, [Q]_{σ′_{Q}}^{s(ξ_{Q}::Q)}σ_{Q})

where σ_{Q} = σ^{r}(ξ_{Q} :: Q)σ′′_{Q}(σ^{c}(ξ_{Q})σ^{n}). □

We now consider the opposite encoding: from π-calculus to πξ-calculus. Given a π-process, supposingly obtained by some derivation, we need

- either to know which would be its syntactic structure if no name instantiation (but decoration of bound names of replicated subprocesses) had ever been applied during the derivation;

- or to build a suitable corresponding environment, and possibly prefix the process by a λ-abstraction.

The following definitions, leading to the wanted encoding, are meant to meet the demands above.

Definition 43 (sub(P)) Let P be a π-calculus process. The set sub(P) is defined in Table 12, where n stays for a positive integer. □

sub(P) = case P in

                       nil : {nil}

α.P_{1} : {α.P_{1}} ∪ sub(P_{1})
[x = z]P_{1} : {[x = z]P_{1}} ∪ sub(P_{1})
P_{1} + P_{2} : {P_{1} + P_{2}} ∪ sub(P_{1}) ∪ sub(P_{2})
P_{1} | P_{2} : {P_{1} | P_{2}} ∪ {(P′_{1} | P′_{2}) s.t.
(P′_{1} ∈ sub(P_{1}) and P′_{2} ≡ P_{2}) or
(P′_{1} ≡ P_{1} and P′_{2} ∈ sub(P_{2})) or
(P′_{1} ∈ sub(P_{1}) and P′_{2} ∈ sub(P_{2}))}
(y)P_{1} : {(y)P_{1}} ∪ {(y)P′_{1} s.t. P′_{1} ∈ sub(P_{1})} ∪ sub(P_{1})
!P_{1} : {!P_{1}} ∪ {(P′_{1} | P′′_{1}) s.t.
P′_{1} ∈ sub((P_{1})^{dec 0}) and
P′′_{1} ∈ sub(repl((P_{1})^{dec 1}, n − 1))}

                 end case

where

repl(P, j) = case j in
j = 0 : !P
j > 0 : (P)^{dec 0} | repl((P)^{dec 1}, j − 1)

                  end case

Table 12: definition of sub( )

\underline{Notation} We use the operator (R)^{dec^{n}} meaning that the names in the set R have been arbitrarily decorated, up to n times, by either ( )^{dec 0} or ( )^{dec 1}. Namely

(R)^{dec^{n}} = ⋃_{x∈R,|s|≤n} {x^{(s)}}

where s is a string of zeros and ones. □

Definition 44 ((P_{j}, P_{r}, R, s, σ)-dual of P_{π}) Let P_{j}, P_{π} be π-calculus processes. Process P ∈ sub(P_{j}) is a (P_{j}, P_{r}, R, s, σ)-dual of P_{π} if a set of names R and name substitutions s, σ exist such that P_{π} ≡_{α} P_{r} ∈ rsp(R, [P]^{s}σ) where, letting Res be the set of the restricted names of P_{j}, the following holds:

- R ⊆ ⋃_{k≥0}(Res \ bn(P))^{dec^{k}}
- Dm(s), Dm(σ) ⊆ ⋃_{k≥0}(bn(P_{j}))^{dec^{k}}
- Im(s) ⊆ bn(P)

- Im(σ) ⊆ R ∪ (N \ ⋃_{k≥0}(n(P_{j}))^{dec^{k}}) □

Definition 45 ((N, R_{P} , s_{P} , σ_{P})-environment for P_{r}) Let N ⊆ N_{I}, and R_{P} ⊆ N_{RT}, and s_{P} , σ_{P} be name substitutions, and P_{r} be a π-calculus process. Also, take F = {x | x ∈ Dm(σ_{P}) and xσ_{P} ∉ R_{P} }. Then, a (N, R_{P} , s_{P} , σ_{P})-environment for P_{r} is defined as follows.

- If F = ∅, then the only (N, R_{P} , s_{P} , σ_{P})-environment for P_{r} is given by ξ = ξ^{N} + {(x, y) | y = xs_{P} or (y = xσ_{P} and xσ_{P} ∈ R_{P}) or (yσ_{P} = xσ_{P} and xσ_{P} ∉ R_{P})}.

- If F ≠ ∅ then choose any ordering (x_{1}, …, x_{m}) of its elements.

An (N, R_{P} , s_{P} , σ_{P})-environment for P_{r} is given by the following recurrence:

\begin{aligned}ξ_{0} & = & ξ \\ ξ_{i+1} & = & ξ_{i} + (x_{i+1}, newD(ξ_{i})) \end{aligned}

Let ξ_{P} be an (N, R_{P} , s_{P} , σ_{P})-environment for P_{r} and let ξ_{Q} be an (N, R_{Q}, s_{Q}, σ_{Q})- environment for Q_{r} where R_{Q} ⊆ N_{RT} and s_{Q}, σ_{Q} are name substitutions and Q_{r} is a π-calculus process. Then, ξ_{P} and ξ_{Q} are compatible iff allD(ξ_{P}) = allD(ξ_{Q}) and ∀x ∈ Dm(σ_{P}), ∀y ∈ Dm(σ_{Q}), (xσ_{P} ∉ bn(P_{r}) and yσ_{Q} ∉ bn(Q_{r}) and xσ_{P} = yσ_{Q}) implies ξ_{P} (x) = ξ_{Q}(y). □

Translation 2 (from π-calculus to ground πξ-calculus) Let P_{1}, P_{2} be π-calculus processes with N = fn(P_{1}, P_{2}) and let S be a late ground bisimulation containing (P_{1}, P_{2}). Then define the relation T r_{E}((P_{1}, P_{2}), S) as it follows.

T r_{E}((P_{1}, P_{2}), S) = ⋃_{(P_{π},Q_{π})∈S} T r_{E}((P_{1}, P_{2}), (P_{π}, Q_{π}))

where T r_{E}((P_{1}, P_{2}), (P_{π}, Q_{π})) is the set of pairs (ξ_{P} :: P, ξ_{Q} :: Q) such that, letting i, j = 1, 2 and i ≠ j, the following holds:

- P is a (P_{i}, P_{r}, R_{P} , s_{P} , σ_{P})-dual of P_{π} and Q is a (P_{j}, Q_{r}, R_{Q}, s_{Q}, σ_{Q})-dual of

Q_{π}
- ξ_{P} is an (N, R_{P} , s_{P} , σ_{P})-environment for P_{r} and
ξ_{Q} is an (N, R_{Q}, s_{Q}, σ_{Q})-environment for Q_{r}
- ξ_{P} and ξ_{Q} are compatible

The translation T r_{L}((P_{1}, P_{2}), S) is given by T r_{E}((P_{1}, P_{2}), S) plus the pairs defined as follows. For each subset of T r_{E}((P_{1}, P_{2}), S) of the shape

⋃_{c∈allD(ξ_{P})∪newD(ξ_{P})}(ξ_{P} + (y, c) :: P, ξ_{Q} + (z, c) :: Q)

add T r_{E}((P_{1}, P_{2}), S) with the pair (ξ_{P} :: λy.P, ξ_{Q} :: λz.Q). □

Remark 46 By construction, if (ξ_{P} :: P, ξ_{Q} :: Q) ∈ T r_{E}((P_{1}, P_{2}), (P_{π}, Q_{π})) then

- P_{π} ≡_{α} P_{r} ∈ rsp((Dm(σ^{r}(ξ_{P} :: P)))σ^{r}(ξ_{P} :: P), [P]^{s(ξ_{P}::P)}σ^{r}(ξ_{P} :: P)(σ^{c}(ξ_{P})σ^{n}))

- Q_{π} ≡_{α} Q_{r} ∈ rsp((Dm(σ^{r}(ξ_{Q} :: Q)))σ^{r}(ξ_{Q} :: Q), [Q]^{s(ξ_{Q}::Q)}σ^{r}(ξ_{Q} :: Q)(σ^{c}(ξ_{Q})σ^{n}))

where P_{r} and Q_{r} are without homonymy of names and σ^{n} is an admissible name substitution for Im(σ^{c}(ξ_{P})) ∪ Im(σ^{c}(ξ_{Q})) and the restriction substitutions σ^{r}(ξ_{P} :: P) and σ^{r}(ξ_{Q} :: Q) were computed fixing a particular choice for the canonical representative crep of Def. 40. □

The next step is to establish an operational correspondence in between π-calculus and πξ-calculus. What we state is actually the relationship between behaviours of processes which are the one encoding of the other. Since this is proved in an inductive way, we cannot work directly on translated processes, but rather have to consider the generic process which could occur in the derivation of a transition of the encoded agent. Such a generic process is much similar to the process P_{π} of Remark 42 and Remark 46, but can have restrictions on a subset of Im(σ^{r}(ξ_{P} :: P)) instead of on the whole of it.

Definition 47 We call P_{π}^{−} any α-converse of P_{r}^{−} ∈ rsp(Rσ, [P]_{σ′}^{s(ξ_{P}::P)}σ) where

- Rσ ⊆ Dm(σ^{r}(ξ_{P} :: P))σ
- Dm(σ′) ⊆ bn([P]^{s(ξ_{P}::P)})
- σ = σ^{r}(ξ_{P} :: P)σ′′(σ^{c}(ξ_{P})σ^{n})

with Dm(σ′′) = Im(σ^{r}(ξ_{P} :: P)) and σ^{n} admissible name substitution for D ⊇ Dm(σ^{c}(ξ_{P})) and the refreshments σ′, σ′′ such that P_{r}^{−} is without homonymy either among its bound names or among its free and bound names. □

Theorem 48 (relating P_{π}^{−} with P) Let P_{π}^{−}, P_{r}^{−} be as in Def. 47 and let s = s(ξ_{P} :: P)σ′σ. Then the following holds.

1. If P_{π}^{−} ⟶^{\overline{u_{1}}u_{2}} P′_{π} then

P ⟶^{⟨\overline{x}y,C∧x↓⟩} P′ and [[C]]ξ_{P} and xs = u_{1} and ys = u_{2} and

P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P)}σ)

2. If P_{π}^{−} ⟶^{\overline{u_{1}}(w)} P′_{π} with w fresh then

- either P ⟶^{⟨\overline{x}(y),C∧x↓⟩} P′ and [[C]]ξ_{P} and xs = u_{1} and

P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P)}σ{w/ys}) and ys ∉ Rσ

- or P ⟶^{⟨\overline{x}y,C∧x↓⟩} P′ and [[C]]ξ_{P} and xs = u_{1} and

P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ \ {ys}, [P′]_{σ′}^{s(ξ_{P}::P)}σ{w/ys}) and ys ∈ Rσ

3. If P_{π}^{−} ⟶^{u_{1}(w)} P′_{π} with w fresh then

P ⟶^{⟨x(y),C∧x↓⟩} P′ and [[C]]ξ_{P} and xs = u_{1} and

P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P)}σ{w/ys})

4. If P_{π}^{−} ⟶^{τ} P′_{π} then

- either P ⟶^{⟨τ,C⟩} P′ and [[C]]ξ_{P} and P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P)}σ)

- or P ⟶^{⟨τ[x/y],C⟩} P′ and [[C]]ξ_{P} and

- if [x]_{ξ_{P}} ∩ bn(P) ≠ ∅ and [x]_{ξ_{P}} ∩ bn(P′) = ∅ then P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ ∪ {w}, [P′]_{σ′}^{s(ξ_{P}::P)}σ{w/xs, w/ys}) with w fresh

- else either P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P){xs/y}}σ) or P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ{w/xs}, [P′]_{σ′}^{s(ξ_{P}::P)}σ{w/xs, w/ys}) with w fresh □ Theorem 49 (relating P with P_{π}^{−}) Let P_{π}^{−}, P_{r}^{−} be as in Def. 47 and let s = s(ξ_{P} :: P)σ′σ. Then the following holds.

1. If P ⟶^{⟨\overline{x}y,C∧x↓⟩} P′ and [[C]]ξ_{P} and [x]_{ξ_{P}} ∩ bn(P) = ∅ and xs ∉ Rσ then

- if ys ∉ Rσ then P_{π}^{−} ⟶^{\overline{xs}ys} P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P)}σ)

- else P_{π}^{−} ⟶^{\overline{xs}(w)} P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ \ \{ys\}, [P′]_{σ′}^{s(ξ_{P}::P)}σ\{w/ys\}) with w

fresh

2. If P ⟶^{⟨\overline{x}(y),C∧x↓⟩} P′ and [[C]]ξ_{P} and [x]_{ξ_{P}} ∩ bn(P) = ∅ and xs ∉ Rσ then

P_{π}^{−} ⟶^{\overline{xs}(w)} P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P)}σ\{w/ys\}) with w fresh

3. If P ⟶^{⟨x(y),C∧x↓⟩} P′ and [[C]]ξ_{P} and [x]_{ξ_{P}} ∩ bn(P) = ∅ and xs ∉ Rσ then

P_{π}^{−} ⟶^{xs(w)} P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P)}σ{w/ys}) with w fresh

4. If P ⟶^{⟨τ,C⟩} P′ and [[C]]ξ_{P} then P_{π}^{−} ⟶^{τ} P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P)}σ)

5. If P ⟶^{⟨τ[x/y],C⟩} P′ and [[C]]ξ_{P} then P_{π}^{−} ⟶^{τ} P′_{π} and

- if [x]_{ξ_{P}} ∩ bn(P) ≠ ∅ and [x]_{ξ_{P}} ∩ bn(P′) = ∅ then P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ ∪ {w}, [P′]_{σ′}^{s(ξ_{P}::P)}σ{w/xs, w/ys}) with w fresh

- else either P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ, [P′]_{σ′}^{s(ξ_{P}::P){xs/y}}σ)

or P′_{π} ≡_{α} P′_{r} ∈ rsp(Rσ{w/xs}, [P′]_{σ′}^{s(ξ_{P}::P)}σ{w/xs, w/ys}) with w fresh

□

Eventually, the following proposition provides, in terms of statements on relevant name substitutions and obligations, what is needed to definitely relate (both ways) the symbolic transitions of the processes in Th. 48 and Th. 49 with the concrete moves of the (encoding/encoded) top-level πξ-processes.

Proposition 50 Let P_{π}, P_{r} and Q_{π}, Q_{r} be as in Remark 42. Then the following holds.

1. xs(ξ_{P} :: P)σ′_{P} σ_{P} ∈ fn(P_{π}) implies [[x↓]]ξ_{P}

2. ξ_{P} (x) = ξ_{Q}(y) ∈ D implies xs(ξ_{P} :: P)σ′_{P} σ_{P} = ys(ξ_{Q} :: Q)σ′_{Q}σ_{Q}

3. [[x↓]]ξ_{Q} implies [x]_{ξ_{Q}} ∩ bn(Q) = ∅ and xs(ξ_{Q} :: Q)σ′_{Q}σ_{Q} ∉ Dm(σ^{r}(ξ_{Q} :: Q))σ_{Q}

□

Proof of Theorem 7, sketch Once proved the results on semantic correspondences, those about equational characterizations are easy corollaries of Th. 6. We then concentrate on the first kind of statements, dealing with all of the three items simultaneously.

(only if) Assume that either (ξ^{N} :: P_{1}) ≏ (ξ^{N} :: P_{2}) with ≏ ∈ {∼, ≈} or (ξ^{N} :: P_{1}) ≈^{c} (ξ^{N} :: P_{2}). In both cases, by hypothesis there exists a bisimulation S ⊆ ≏ containing the pair (ξ^{N} :: P_{1}, ξ^{N} :: P_{2}), and also some extra hypotheses do hold when (ξ^{N} :: P_{1}) ≈^{c} (ξ^{N} :: P_{2}). The relation T r_{ξ}(S) contains by construction the pair (P_{1}, P_{2}) and it is proven to be the wanted π-calculus equivalence relation. Letting (P_{π}, Q_{π}) ∈ T r_{ξ}((ξ_{P} :: P, ξ_{Q} :: Q)) ⊆ T r_{ξ}(S), the proof is by case analysis on P_{π} ⟶^{α} P′_{π}. Each case goes as it follows. By Th. 48 the corresponding symbolic transition from P is recovered. Then Prop. 50 is invoked to guarantee that the symbolic step from P is actually converted into a concrete move from ξ_{P} :: P. By the hypothesis (ξ_{P} :: P, ξ_{Q} :: Q) ∈ S, we then have complete information about the corresponding move of ξ_{Q} :: Q and proceed to find out the wanted transition Q_{π} ⟶^{α} Q′_{π} with (P′_{π}, Q′_{π}) ∈ T r_{ξ}(S). This requires a kind of inversion of the above reasoning that appeals, this time, to Prop. 50 and Th. 49. Also, in the case when S is a weak relation (i.e. it proves that (ξ^{N} :: P_{1}) and (ξ^{N} :: P_{2}) are either weak bisimilar or weak congruent) we resort to an intermediate result about the relationship of the weak behaviours of ξ_{Q} :: Q and Q_{π}. Eventually, when the action α is an input action, the fact that (P′_{π}{z/w}, Q′_{π}{z/w}) ∈ T r_{ξ}(S) for all z follows quite easily by the definition of the encoding.

(if) Assume that either P_{1} ˙≍_{L} P_{2} with ˙≍_{L} ∈ { ˙∼_{L}, ˙≈_{L}} or P_{1} ˙≃_{L} P_{2}. Also suppose that the relation S ⊆ ˙≍_{L} contains the pair (P_{1}, P_{2}) and witnesses their bisimilarity. By definition of T r_{L}, the relation T r_{L}((P_{1}, P_{2}), S) contains the pair (ξ^{N} :: P_{1}, ξ^{N} :: P_{2}). It remains to show that T r_{L}((P_{1}, P_{2}), S) is the required πξ-calculus bisimulation, and, in case P_{1} ˙≃_{L} P_{2}, also that T r_{L}((P_{1}, P_{2}), S) guarantees (ξ^{N} :: P_{1}) ≈^{c} (ξ^{N} :: P_{2}). By construction, given any pair (ξ_{P} :: P, ξ_{Q} :: Q) ∈ T r_{L}((P_{1}, P_{2}), (P_{π}, Q_{π})) either both or none of P and Q are led by a λ-abstraction. In both cases the proof of T r_{L}((P_{1}, P_{2}), S) ⊆ ∼ is based on a case analysis of the actions performed by ξ_{P} :: P. Then assume that ξ_{P} :: P \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξ_{P′} :: P′′. If P has the shape λy.P′, namely if ρ = [c] for some constant c, then the thesis is an easy consequence of the fact that, by definition of the encoding, some ξ_{Q} :: λz.Q′ there exists such that (ξ_{P} :: λy.P′, ξ_{Q} :: λz.Q′) ∈ T r_{L}((P_{1}, P_{2}), S). Suppose now that P is not led by a λ-abstraction. In this case we first appeal to the symbolic transition of P which induced the concrete move labelled by ρ. Prop. 50 ensures that the hypotheses of Th. 49 are met, hence we retrieve a corresponding transition from P_{π}. By that, and by (P_{π}, Q_{π}) ∈ S, we switch to investigate the symbolic behaviour of Q, by invoking Th. 48, and possibly its weak version (in case we are dealing with a τ-forgetting relation). At this point of the proof, Prop. 50 can be applied to guarantee that the symbolic step actually induces the concrete

move ξ_{Q} :: Q \begin{matrix}− \\ − \end{matrix}▷^{ρ} ξ_{Q′} :: Q′′ with (ξ_{P′} :: P′′, ξ_{Q′} :: Q′′) ∈ T r_{L}((P_{1}, P_{2}), S), whether

or not P′′ is led by a λ-abstraction. □

Appendix B

In the following we will refer to some of the main constructions and statements presented in Appendix A.

Translation 3 (from open πξ-calculus to π-calculus) Let S be a strong bisimulation relation contained in ∼_{η_{O}}. Then

T r_{ξ}^{v}(S) = ⋃_{(ξ_{P}^{v}::P,ξ_{Q}^{v}::Q)∈S} T r_{ξ}((ξv_{P}σ^{v} :: P, ξv_{Q}σ^{v} :: Q))

with

- σ^{v} variable substitution for both ξv_{P} and ξv_{Q}

- T r_{ξ}((ξv_{P}σ^{v} :: P, ξv_{Q}σ^{v} :: Q)) defined analogously as in Trans. 1, that is as the set of pairs (P_{π}, Q_{π}) such that

- P_{π} ≡_{α} P̂(σ^{c}(ξv_{P}σ^{v})σ^{n})

- Q_{π} ≡_{α} Q̂(σ^{c}(ξv_{Q}σ^{v})σ^{n})

- P̂ ∈ rsp(Im(σ^{r}(ξv_{P}σ^{v} :: P)), [P]^{s(ξ_{P}^{v} σ^{v}::P)}σ^{r}(ξv_{P}σ^{v} :: P))

- Q̂ ∈ rsp(Im(σ^{r}(ξv_{Q}σ^{v} :: Q)), [Q]^{s(ξ_{Q}^{v}σ^{v}::Q)}σ^{r}(ξv_{Q}σ^{v} :: Q))

- σ^{n} admissible name substitution for Im(σ^{c}(ξv_{P}σ^{v})) ∪ Im(σ^{c}(ξv_{Q}σ^{v})). □

Translation 4 (from π-calculus to open πξ-calculus) Let P_{1}, P_{2} be π-calculus processes and let S be an open bisimulation containing (P_{1}, P_{2}). Then define the relation T r_{O}((P_{1}, P_{2}), S) as it follows.

T r_{O}((P_{1}, P_{2}), S) = ⋃_{S_{(Pπ ,Qπ)}} T r_{O}((P_{1}, P_{2}), S_{(P_{π},Q_{π})})

where

- S_{(P_{π},Q_{π})} is the subset of S of the shape ⋃_{σ_{π}} {(P_{π}σ_{π}, Q_{π}σ_{π})}

- T r_{O}((P_{1}, P_{2}), S_{(P_{π},Q_{π})}) is given by the set of pairs (ξv_{P} :: P, ξv_{Q} :: Q) such that,

letting i, j = 1, 2 and i ≠ j

- P is a (P_{i}, P_{r}, R_{P} , s_{P} , σ_{P} σ_{π})-dual of P_{π}σ_{π}

- Q is a (P_{j}, Q_{r}, R_{Q}, s_{Q}, σ_{Q}σ_{π})-dual of Q_{π}σ_{π}

- ξv_{P} and ξv_{Q} such that for all variable substitutions σ^{v} for both ξv_{P} and ξv_{Q} it holds that ξv_{P}σ^{v} = ξ_{P} and ξv_{Q}σ^{v} = ξ_{Q} where ξ_{P} and ξ_{Q} are defined as it follows

- ξ_{P} is an (∅, R_{P} , s_{P} , σ_{P} σ_{π})-environment for P_{r}

- ξ_{Q} is an (∅, R_{Q}, s_{Q}, σ_{Q}σ_{π})-environment for Q_{r}

- ξ_{P} and ξ_{Q} are compatible □

The observations collected below partially correspond to both Remark 42 and Remark 46. Those comments will allow us to take advantage of the main theorems of Appendix A while reasoning modulo arbitrary substitutions.

Remark 51 The following observations about Translations 3 and 4 do hold.

1. (on Trans. 3) Let P_{π} and Q_{π} be as in Trans. 3 and let σ_{π} be any substitution from names to names. By construction, for some P_{r} without homonymy either among bound names or among free and bound names P_{π}σ_{π} ≡_{α} P_{r} where

- P_{r} ∈ rsp(Dm(σ^{r}(ξv_{P}σ^{v} :: P))σ_{P} , [P]_{σ′_{P}}^{s(ξ_{P}^{v} σ^{v}::P)}σ_{P})

- σ_{P} = σ^{r}(ξv_{P}σ^{v} :: P)σ′′_{P}(σ^{c}(ξv_{P}σ^{v})σ^{n})σ_{π}

- σ′_{P} , σ′′_{P} are, respectively, the refreshment of the bound names of P and the refreshment of the names in Im(σ^{r}(ξv_{P}σ^{v} :: P))

Similarly, for a suitable Q_{r} without homonymy of names and suitable substitutions σ′_{Q}, σ′′_{Q}, it holds that Q_{π}σ_{π} ≡_{α} Q_{r} where

- Q_{r} ∈ rsp(Dm(σ^{r}(ξv_{Q}σ^{v} :: Q))σ_{Q}, [Q]_{σ′_{Q}}^{s(ξ_{Q}^{v}σ^{v}::Q)}σ_{Q})

- σ_{Q} = σ^{r}(ξv_{Q}σ^{v} :: Q)σ′′_{Q}(σ^{c}(ξv_{Q}σ^{v})σ^{n})σ_{π}

2. (on Trans. 4)

Let (ξv_{P} :: P, ξv_{Q} :: Q) ∈ T r_{O}((P_{1}, P_{2}), S_{(P_{π},Q_{π})}) then

- P_{π}σ_{π} ≡_{α} P_{r} ∈ rsp((Dm(s_{P}))s_{P} , [P]^{s(ξ_{P}^{v} σ^{v}::P)}s_{P} (σ^{c}(ξv_{P}σ^{v})σ^{n})σ_{π})

- Q_{π}σ_{π} ≡_{α} Q_{r} ∈ rsp((Dm(s_{Q}))s_{Q}, [Q]^{s(ξ_{Q}^{v}σ^{v}::Q)}s_{Q}(σ^{c}(ξv_{Q}σ^{v})σ^{n})σ_{π})

where

- P_{r} and Q_{r} are without homonymy of names

- s_{P} stays for the restriction substitution σ^{r}(ξv_{P}σ^{v} :: P)

- s_{Q} stays for the restriction substitution σ^{r}(ξv_{Q}σ^{v} :: Q)

- σ^{v} is a variable substitution for both ξv_{P} and ξv_{Q}

- σ^{n} is an admissible name substitution for Im(σ^{c}(ξv_{P}σ^{v})) ∪ Im(σ^{c}(ξv_{Q}σ^{v}))

3. The above observations guarantees that the main statements about operational correspondence recalled in Appendix A (Th. 48, Th. 49, and Prop. 50) can be revisited by letting

- P_{π} be substituted by P_{π}σ_{π}

- Q_{π} be substituted by Q_{π}σ_{π}

- ξ_{P} be substituted by ξv_{P}σ^{v}

- ξ_{Q} be substituted by ξv_{Q}σ^{v}

- P_{π}^{−} be substituted by (P_{π}σ_{π})^{−}

- etcetera. □

We can now prove the coincidence result for open semantics.

Proof of Theorem 39 For the proof of both the ‘if’ and the ‘only if’ directions, we suppose that a given relation S witnesses the hypothesis. Then the actual statement is shown to hold by transforming the relation S along the guide-lines described in Trans. 3 and Trans. 4.

(only if) Assume that a relation S ⊆ ∼_{η_{O}} there exists with (ξ^{L} :: P_{1}, ξ^{L} :: P_{2}) ∈ S. By construction (P_{1}, P_{2}) ∈ T r_{ξ}^{v}(S). We now show that T r_{ξ}^{v}(S) ⊆ ∼_{O}. Letting (P_{π}, Q_{π}) ∈ T r_{ξ}((ξv_{P}σ^{v} :: P, ξv_{Q}σ^{v} :: Q)), it is a matter of proving that for all substitutions σ_{π}

whenever P_{π}σ_{π} ⟶^{α_{π}} P′_{π} with bn(α_{π}) fresh

then Q_{π}σ_{π} ⟶^{α_{π}} Q′_{π} and (P′_{π}, Q′_{π}) ∈ T r_{ξ}^{v}(S)

The proof is by case analysis, and each case has the following structure.

Assume P_{π}σ_{π} ⟶^{α_{π}} P′_{π}

⟹ By Th. 48 and Remark 51 it follows that P ⟶^{⟨α_{P} ,C_{P} ⟩} P′ with [[C_{P}]]ξv_{P}σ^{v} and a given relationship between α_{P} and α_{π} and between P′_{π} and the pair (ξv_{P}σ^{v}, P′). Also, if the action α_{P} uses a name as subject – i.e. if α_{P} ≠ τ, τ[x/y] – then by Prop. 50 and Remark 51 it follows that the equivalence class of such a channel name is defined in the environment ξv_{P}σ^{v}. This fact partially satisfies the hypothesis which are necessary for the forthcoming application of the revisited version of Th. 49 ⟹ By [[C_{P}]]ξv_{P}σ^{v} and by Prop. 37 it follows that ξv_{P} ⊎ ⟨[C_{P}]⟩ξv_{P} ≠ ε

⟹ ξv_{P} :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{O}}^{f} ξv_{P′} :: P′ with some precise relationship between α_{P} and f(Im(σ^{v})) and hence between α_{π} and f(Im(σ^{v}))

⟹ By (ξv_{P} :: P, ξv_{Q} :: Q) ∈ S some ξv_{Q′} :: Q′ there exists such that ξv_{Q} :: Q \begin{matrix}− \\ − \end{matrix}▷_{η_{O}}^{f}

ξv_{Q′} :: Q′ and (ξv_{P′} :: P′, ξv_{Q′} :: Q′) ∈ S

⟹ Q ⟶^{⟨α_{Q},C_{Q}⟩} Q′ with ξv_{Q} ⊎ ⟨[C_{Q}]⟩ξv_{Q} ≠ ε and a sharp relationship between α_{Q} and f(Im(σ^{v})) and then, by transitivity, between α_{Q} and α_{π} ⟹ By the hypothesis that σ^{v} is a variable substitution for ξv_{Q} and by Prop. 37 it follows that [[C_{Q}]]ξv_{Q}σ^{v}

⟹ By Remark 51 and Th. 49 it comes that Q_{π}σ_{π} ⟶^{α_{π}} Q′_{π} with a relationship between P′_{π} and Q′_{π} which guarantees that (P′_{π}, Q′_{π}) ∈ T r_{ξ}^{v}(S). In fact it holds that (ξv_{P′} :: P′, ξv_{Q′} :: Q′) ∈ S. Moreover, if α_{π} is not an input action then just (P′_{π}, Q′_{π}) ∈

T r_{ξ}((ξv_{P′}σ^{v} :: P′, ξv_{Q′}σ^{v} :: Q′)). Otherwise (P′_{π}, Q′_{π}) ∈ T r_{ξ}((ξv_{P′}σ :: P′, ξv_{Q′}σ :: Q′))

for σ which coincides with σ^{v} on the common domain and extends it with a new component {c/v_{m+1}}. Such a component makes ground the last generated variable.

(if) Assume now that the relation S ⊆ ∼_{O} is given, and that (P_{1}, P_{2}) ∈ S. By construction (ξ^{L} :: P_{1}, ξ^{L} :: P_{2}) ∈ T r_{O}((P_{1}, P_{2}), S). We now show that T r_{O}((P_{1}, P_{2}), S) is a strong bisimulation contained in ∼_{η_{O}}.

Let (ξv_{P} :: P, ξv_{Q} :: Q) ∈ T r_{O}((P_{1}, P_{2}), S_{(P_{π},Q_{π})}). Also suppose that ξv_{P} :: P \begin{matrix}− \\ − \end{matrix}▷_{η_{O}}^{f}

ξv_{P′} :: P′ and let σ be any variable substitution for ξv_{P′}

⟹ P ⟶^{⟨α_{P} ,C_{P} ⟩} P′ with ξv_{P} ⊎ ⟨[C_{P}]⟩ξv_{P} ≠ ε and a fixed relationship between α_{P} and f(Im(σ)) ⟹ By Prop. 38 and Prop. 37 it holds that [[C_{P}]]ξv_{P}σ^{v} where σ^{v} = frag(σ, ξv_{P})

⟹ By Remark 51 and Th. 49 it follows that P_{π}σ_{π} ⟶^{α_{π}} P′_{π} with a precise relationship between P′_{π} and ξv_{P′} :: P′ and between α_{π} and α_{P}, that is between α_{π} and f(Im(σ)). The ground observation f(Im(σ)) is in turn related to f(Im(σ^{v})) in the obvious way

⟹ By (P_{π}, Q_{π}) ∈ S it follows that Q_{π}σ_{π} ⟶^{α_{π}} Q′_{π} with (P′_{π}, Q′_{π}) ∈ S

⟹ By Remark 51 and Th. 48 it comes that Q ⟶^{⟨α_{Q},C_{Q}⟩} Q′ with [[C_{Q}]]ξv_{Q}σ^{v} and a fixed relationship between Q′_{π} and ξv_{Q}σ^{v} :: Q′ and between α_{Q} and α_{π}, that is between α_{Q} and f(Im(σ^{v}))

⟹ By Prop. 37 it comes that ξv_{Q} ⊎ ⟨[C_{Q}]⟩ξv_{Q} ≠ ε. Hence the thesis follows. In fact

ξv_{Q} :: Q \begin{matrix}− \\ − \end{matrix}▷_{η_{O}}^{h} ξv_{Q′} :: Q′ and by the assumed generality of σ and by Prop. 38 it derives that the two functions f and h are point-wise equal. Moreover, by (P′_{π}, Q′_{π}) ∈ S and the assumption on σ it also holds that (ξv_{P′} :: P′, ξv_{Q′} :: Q′) ∈ T r_{O}((P_{1}, P_{2}), S_{(P′_{π},Q′_{π})}).

□

Recent BRICS Report Series Publications

RS-97-52 Paola Quaglia. On the Finitary Characterization of π-Congruences. December 1997. 59 pp.

RS-97-51 James McKinna and Robert Pollack. Some Lambda Calculus and Type Theory Formalized. December 1997. 43 pp.

RS-97-50 Ivan B. Damgård and Birgit Pfitzmann. Sequential Iteration of Interactive Arguments and an Efficient Zero-Knowledge Argument for NP. December 1997. 19 pp.

RS-97-49 Peter D. Mosses. CASL for ASF+SDF Users. December 1997. 22 pp. Appears in ASF+SDF’97, Proceedings of the 2nd International Workshop on the Theory and Practice of Algebraic Specifications, Electronic Workshops in Computing, http://www.springer.co.uk/ewic/workshops/ASFSDF97. Springer-Verlag, 1997.

RS-97-48 Peter D. Mosses. CoFI: The Common Framework Initiative for Algebraic Specification and Development. December 1997. 24 pp. Appears in Bidoit and Dauchet, editors, Theory and Practice of Software Development. 7th International Joint Conference CAAP/FASE, TAPSOFT ’97 Proceedings, LNCS 1214, 1997, pages 115–137.

RS-97-47 Anders B. Sandholm and Michael I. Schwartzbach. Distributed Safety Controllers for Web Services. December 1997. 20 pp. To appear in European Theory and Practice of Software. 1st Joint Conference FoSSaCS/FASE/ESOP/CC/TACAS, ETAPS ’97 Proceedings, LNCS, 1998.

RS-97-46 Olivier Danvy and Kristoffer H. Rose. Higher-Order Rewriting and Partial Evaluation. December 1997. 20 pp. Extended version of paper to appear in Rewriting Techniques and Applications: 9th International Conference, RTA ’98 Proceedings, LNCS, 1998.

RS-97-45 Uwe Nestmann. What Is a ‘Good’ Encoding of Guarded Choice? December 1997. 28 pp. Revised and slightly extended version of a paper published in 5th International Workshop on Expressiveness in Concurrency, EXPRESS ’97 Proceedings, volume 7 of Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers.