BRICS RS-99-42 Nestmann & Pierce: Decoding Choice Encodings BRICS

Basic Research in Computer Science

Decoding Choice Encodings

Uwe Nestmann Benjamin C. Pierce BRICS Report Series RS-99-42 ISSN 0909-0878 December 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Uwe Nestmann & Benjamin C. Pierce.

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/99/42/

Decoding Choice Encodings^{∗}

Uwe Nestmann, BRICS^{†}, Aalborg University, Denmark Benjamin C. Pierce, University of Pennsylvania, USA

Abstract

We study two encodings of the asynchronous π-calculus with input-guarded choice into its choice-free fragment. One encoding is divergence-free, but refines the atomic commitment of choice into gradual commitment. The other preserves atomicity, but introduces divergence. The divergent encoding is fully abstract with respect to weak bisimulation, but the more natural divergence-free encoding is not. Instead, we show that it is fully abstract with respect to coupled simulation, a slightly coarser—but still coinductively defined—equivalence that does not enforce bisimilarity of internal branching decisions. The correctness proofs for the two choice encodings introduce a novel proof technique exploiting the properties of explicit decodings from translations to source terms.

∗This paper is a revised full version of a technical report that appeared first as IMMD-VII-01/96 at University of Erlangen and TR 342 at University of Cambridge. An extended summary then appeared in the Proceedings of the 7th International Conference on Concurrency Theory (CONCUR’96) LNCS 1119, pages 179–194, Springer-Verlag, 1996. The work was mainly carried out while the first author was at the University of Erlangen-Nürnberg, Germany (supported by Deutsche Forschungsgemeinschaft, Sonderforschungsbereich 182, project C2, and by Deutscher Akademischer Austauschdienst within the ARC-program), and while the second author was at the University of Cambridge, UK (supported by the British Science and Engineering Research Council). The first revision took place while the first author was supported by a post-doc fellowship from ERCIM (European Research Consortium for Informatics and Mathematics); it is available as ERCIM Research Report 10/97-R051.

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

Contents

1 Introduction 1

2 Technical preliminaries: The asynchronous π-calculus 2 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Operational semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.4 When weak bisimulation is too strong . . . . . . . . . . . . . . . . . . . . . . 8 2.5 Up-to techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3 Discussion: Correctness of encodings 12

4 Encoding input-guarded choice, asynchronously 15 4.1 The setting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2 Two choice encodings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 4.3 An example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.4 Expanding the encodings . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

5 Correctness proof by decoding 24 5.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.2 Annotated choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 5.3 Factorization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 5.4 Decoding derivatives of A-translations . . . . . . . . . . . . . . . . . . . . . 33 5.5 Expanding derivatives of C-translations . . . . . . . . . . . . . . . . . . . . 41 5.6 Main result . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 5.7 Correctness of the divergent protocol . . . . . . . . . . . . . . . . . . . . . . 44 5.8 Divergence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

6 Conclusions 48

A Some Proofs 53 A.1 F is a strong bisimulation (Proposition 5.3.4) . . . . . . . . . . . . . . . . . 53 A.2 Operational correspondence for the B-encoding (Proposition 5.5.1) . . . . . 55

1 Introduction

The problem of implementing the concurrent choice operator in terms of lower-level constructs is interesting from a number of points of view. Theoretically, it contributes new insight on the expressiveness of process calculi and the computational content of choice. More practically, it provides correctness arguments supporting the design of high-level concurrent languages on top of process calculi. Furthermore, it is tightly related to the distributed implementation of synchronization and selective communication [Mit86, PS92, Kna93, BG95].

Our interest in the study of choice encodings originates from the design and implementation of the high-level concurrent language Pict [PT95, PT99], an asynchronous choice-free π-calculus [HT91, Bou92] enriched with several layers of encoded syntactic sugar. The abstract machine of Pict does not provide instructions for selective communication; instead, choice is provided as a library module by a straightforward encoding. Surprisingly, however, this encoding turns out not to be valid with respect to standard weak bisimulation.

We study choice encodings in the π-calculus with asynchronous messages (or equivalently, with non-blocking output prefix). This setting has received increasing attention in recent years. In the ν-calculus, asynchrony was treated using a non-standard labeled semantics [HT91, HT92, Hon92]; the mini π-calculus used a chemical semantics [Bou92]; it has also been investigated using reduction semantics [HY95], concurrent combinators [HY94a, HY94b], and output-only barbed congruences [Ode95a, FG96]. Only recently, it has been extended with an input-guarded choice operator, equipped with a standard labeled semantics, and studied with bisimulation from an asynchronous observer’s viewpoint [ACS98].

We use standard notations for restriction (x)P of name x to process P, parallel composition P_{1}|P_{2}, input y(x).P of a name from channel y for use as x in P, and output \overline{y}z of name z on channel y. Furthermore, ∏ and ∑ denote indexed parallel composition and input-guarded choice, respectively. For convenience, we introduce the conditional form if l then P else Q, which performs a case analysis driven by the special names t and f by reading from l either t or f and behaving afterwards like P or Q, respectively.

We study two variants of the choice encoding. The non-divergent version, which is more interesting from a pragmatic perspective, will occupy most of our attention. For each choice expression ∑_{j∈J} y_{j}(x).P_{j}, the translation

C[[ ∑_{j∈J} y_{j}(x).P_{j} ]] =^{def} (l)( \overline{l}t | ∏_{j∈J} Branch_{l}⟨ y_{j}(x).P_{j} ⟩ )

runs a mutual exclusion protocol, installing a local lock—a message that carries a special name—on the parallel composition of its branches. The branches

Branch_{l}⟨ y_{j}(x).P_{j} ⟩ =^{def} y_{j}(x) . l(b) . if b then ( C[[ P_{j} ]] | \overline{l}f ) else ( \overline{y_{j}}x | \overline{l}f )

concurrently try to (destructively) test the lock after reading messages from the environment. Only the first branch managing to interrogate the lock (via l(b)) will proceed with its continuation (then) and thereby commit the choice — every other branch will then be forced to resend its message and abort its continuation (else). The resending of messages by non-chosen branches essentially reflects the asynchronous character of the encoding. For an asynchronous observer, who can not detect when a message is consumed by a receptor, the resending of messages is immaterial, and so this encoding seems intuitively to be correct.

However, even for the asynchronous observer, it turns out that source terms and their Ctranslations are not weakly bisimilar. The reason is that the latter carry out commitments only gradually, resulting in intermediate states that do not correspond to any source term. In order to deal with partially committed states, we instead characterize the correctness of the encoding as a pair of simulations which are coupled by requiring that less committed (i.e., simulating) processes can always internally evolve into more committed (i.e., simulated) processes [PS92].

For comparison, we also study another encoding that introduces an alternate path in each branch of a choice allowing it to “back out” and return to its initial state after it has been given the lock. This encoding avoids gradual commitments and can, in fact, be proven fully abstract with respect to weak bisimilarity. However, it is pragmatically unsatisfactory since it introduces divergence.

The remainder of the paper is organized as follows. We first introduce the setting of an asynchronous π-calculus (§2) and review some standard notions of correctness (§3). We then present the divergence-free encoding C and the divergent encoding D, followed by an example that shows the failure of full abstraction of the C-encoding with respect to weak bisimulation ≈ (§4). Using an intermediate language which lets us factor the C-encoding into two steps, we define two decoding functions that constitute an asynchronous coupled simulation. This leads to our main result: for all source terms S,

S ⇄ C[[ S]]

where ⇄ is (asynchronous) coupled simulation equivalence; we also prove that the Cencoding is divergence-free, and we sketch a proof that S ≈ D[[ S]] (§5). Finally, we offer some concluding remarks and hint at related and future work (§6).

2 Technical preliminaries: The asynchronous π-calculus

Many variants of the π-calculus [MPW92] have appeared in the recent process algebra literature. We use here a version which is close to the core language of Pict [PT95, PT99]: an asynchronous, first-order, monadic π-calculus [HT91, Bou92], where replication is restricted to input processes and evaluated lazily [HY95, MP95], i.e., copies of a replicated input are spawned during communication.

2.1 Syntax

Let N be a countable set of names. Then, the set ℙ of processes P is defined by

\begin{aligned}P & ::= & (x)P | P |P | \overline{y}z | 0 | R | !R \\ R & ::= & y(x).P \end{aligned}

where x, y, z ∈ N. The semantics of restriction, parallel composition, input, and output, is standard. The form !y(x).P is the replication operator restricted to input-prefixes. In \overline{y}z and y(x), the name y is called the subject, whereas x, z are called objects. We refer to outputs as messages and to (ordinary or replicated) inputs as receptors. A term is guarded when it occurs as a subterm of an input prefix R. As a notational abbreviation, if the object in some input or output is of no importance in some term, then it may be completely omitted, i.e., y(x).P with x ∉ P and \overline{y}z are written y.P and \overline{y}. The usual constant 0 denoting the inactive process can be derived as (x)\overline{x}, but we prefer to include it explicitly for a clean specification of structural and operational semantics rules.

The definitions of name substitution and α-conversion are standard. A name x is bound in P, if P contains an x-binding operator, i.e., either a restriction (x)P or an input prefix y(x).P as a subterm. A name x is free in P if it occurs outside the scope of an x-binding operator. We write bn(P) and fn(P) for the sets of P ’s bound and free names; n(P) is their union. Renaming of bound names by α-conversion =_{α} is as usual. Substitution P {^{z}/_{x}} is given by replacing all free occurrences of x in P with z, first α-converting P to avoid capture.

Operator precedence is, in decreasing order of binding strength: (1) prefixing, restriction, (2) substitution, (3) parallel composition.

2.2 Operational semantics

Let y, z ∈ N be arbitrary names. Then, the set L of labels μ is generated by

μ ::= \overline{y}(z) | \overline{y}z | yz | τ

representing bound and free output, early input, and internal action. The functions bn and fn yield the bound names, i.e., the objects in bound (bracketed) outputs, and free names (all others) of a label. We write n(μ) for their union bn(μ) ∪ fn(μ).

The operational semantics for processes is given as a transition system with ℙ as its set of states. The transition relation ⟶ ⊆ ℙ × L × ℙ is defined as the smallest relation generated by the set of rules in Table 1. We use an early instantiation scheme as expressed in the INP and COM /CLOSE-rules, since it allows us to define bisimulation without clauses for name instantiation and since it allows for a more intuitive modeling in §4, but this decision does not affect the validity of our results. Rule OPEN prepares for scope extrusion, whereas in CLOSE the previously opened scope of a bound name is closed upon its reception.

[figure]

OUT: \overline{y}z \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{y}z} → 0

INP: y(x).P \begin{matrix}− \\ − \\ − \end{matrix}^{yz} → P \{^{z}/_{x}\}

R-INP: !y(x).P \begin{matrix}− \\ − \\ − \end{matrix}^{yz} → P \{^{z}/_{x}\} | !y(x).P

COM_{1}^{∗}: \frac{P_{1} \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{y}z} → P′_{1}  P_{2} \begin{matrix}− \\ − \\ − \end{matrix}^{yz} → P′_{2}}{P_{1} | P_{2}  \begin{matrix}− \\ − \end{matrix}^{τ} → P′_{1} | P′_{2}}

OPEN: \frac{P \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{y}z} → P′}{(z)P \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{y}(z)} → P′} if y ≠ z

CLOSE_{1}^{∗}: \frac{P_{1} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{y}(z)} → P′_{1}  P_{2} \begin{matrix}− \\ − \\ − \end{matrix}^{yz} → P′_{2}}{P_{1} | P_{2}  \begin{matrix}− \\ − \end{matrix}^{τ} → (z)( P′_{1} | P′_{2} )}  if z ∉ fn(P_{2})

PAR_{1}^{∗}: \frac{P_{1} \begin{matrix}− \\ − \end{matrix}^{μ} → P′_{1}}{P_{1} | P_{2} \begin{matrix}− \\ − \end{matrix}^{μ} → P′_{1} | P_{2}} if bn(μ) ∩ fn(P_{2}) = ∅

RES: \frac{P \begin{matrix}− \\ − \end{matrix}^{μ} → P′}{(x)P \begin{matrix}− \\ − \end{matrix}^{μ} → (x)P′} if x ∉ n(μ)

ALPHA: \frac{P̂ \begin{matrix}− \\ − \end{matrix}^{μ} → P̂′}{P \begin{matrix}− \\ − \end{matrix}^{μ} → P̂′} if P =_{α} P̂

∗: and the evident symmetric rules COM_{2}, CLOSE_{2}, and PAR_{2} Table 1: Transition semantics

Weak arrows ( ⟹) denote the reflexive and transitive closure of internal transitions; arrows with hats denote that two processes are either related by a particular transition or else equal in the case of an internal transition.

⟹ =^{def} \begin{matrix}− \\ − \end{matrix}^{τ} →^{∗}  μ̂ ; \begin{matrix}− \\ − \end{matrix} → =^{def} \{ \begin{matrix}\begin{matrix}− \\ − \end{matrix}^{μ} → & if μ ≠ τ \\ \begin{matrix}− \\ − \end{matrix}^{τ} → ∪ = & if μ = τ \end{matrix}  \begin{aligned}μ̂ ; {= \atop =} ⇒ & =^{def} & ⟹ μ̂ ; \begin{matrix}− \\ − \end{matrix} → ⟹ \\ {= \atop =}^{μ} ⇒ & =^{def} & ⟹ \begin{matrix}− \\ − \end{matrix}^{μ} → ⟹ \end{aligned}

2.3 Bisimulation

Two process systems are equivalent when they allow us to observe the same operational behavior. Bisimulation equivalence is defined as the mutual simulation of single computation steps resulting in equivalent system states. In the standard literature on bisimulations, e.g. [Mil89, MPW92], a simulation is a binary relation S on processes such that (P, Q) ∈ S implies, for arbitrary label μ:

• if P \begin{matrix}− \\ − \end{matrix}^{μ} → P′, then there is Q′ such that Q \begin{matrix}− \\ − \end{matrix}^{μ} → Q′ and (P′, Q′) ∈ S.

A bisimulation is a simulation whose opposite is again a simulation. In this subsection, we review various refinements of standard bisimulation: we define its asynchronous variant, identify a few structural laws, refine it to a preorder that takes efficiency into account, and finally refine it to deal with divergence.

Asynchrony

In calculi with synchronous message-passing, output- and input-transitions are dealt with symmetrically in the definition of bisimulation. In contrast, the concept of asynchronous messages suggests a non-standard way of observing processes. Since the sending of a message to an observed system is not blocking for the observer, the latter can not immediately detect whether the message was actually received, or not. The only possible observations are messages eventually coming back from the system. Different formulations of asynchronous bisimulation (all inducing the same equivalence) have been proposed in the literature, based on a modified labeled input rule [HT92], on output-only barbed congruences [HY95], and on a standard labeled semantics with asynchronous observers [ACS98]. Here, we follow the latter approach. Unless otherwise stated, we implicitly assume an asynchronous interpretation of observation throughout the paper.

Definition 2.3.1 (Simulation, bisimulation) A binary relation S on processes is a strong simulation if (P, Q) ∈ S implies:

• if P \begin{matrix}− \\ − \end{matrix}^{μ} → P′, where μ is either τ or output with bn(μ) ∩ fn(P |Q) = ∅, then there is Q′ such that Q \begin{matrix}− \\ − \end{matrix}^{μ} → Q′ and (P′, Q′) ∈ S

[figure]

α-conversion  P ≡ Q  if P =_{α} Q
associativity  P | (Q|R) ≡ (P |Q) | R
commutativity  P | Q ≡ Q | P
neutrality  P | 0 ≡ P
scope extrusion  (y)P | Q ≡ (y)(P |Q) if y ∉ fn(Q)
scope elimination  (y)Q ≡ Q  if y ∉ fn(Q)

Table 2: Structural laws

• ( \overline{a}z|P , \overline{a}z|Q ) ∈ S for arbitrary messages \overline{a}z.

B is called a strong bisimulation if both B and B^{−1} are strong simulations. Two processes P and Q are strongly bisimilar, written P ∼ Q, if they are related by some strong bisimulation.

Replacing Q \begin{matrix}− \\ − \end{matrix}^{μ} → Q′ with Q μ̂ ; {= \atop =} ⇒ Q′ in this definition yields the weak versions of the corresponding simulations. Write ≈ for weak bisimulation. Process Q weakly simulates P, written P ≼ Q, if there is a weak simulation S with (P, Q) ∈ S.

Fact 2.3.2 ≈ is a congruence on ℙ. [Hon92, ACS98]

Structural laws

Certain laws on processes have been recognized as having merely “structural” content; they are valid with respect to all different kinds of behavioral congruences, equivalences and preorders, including strong bisimulation (the finest “reasonable” equivalence). In this paper, we use a few structural laws (indicated by the symbol ≡) listed in Table 2 in order to simplify the presentation of some derivation sequences of transitions in the proofs of Section 5.

Fact 2.3.3 ≡ ⊂ ∼ .

In particular, we work up to α-conversion, where appropriate, i.e., we omit to mention the implicit application of rule ALPHA since it may be captured by a simple structural transformation. Thus, we silently identify processes or actions which only differ in the choice of bound names. Furthermore, due to the associativity law for composition, we omit brackets in multiple parallel composition and use finite parallel composition ∏ with the usual meaning.

Efficiency

Often, weakly bisimilar processes differ only in the number of internal steps. The expansion preorder [AH92] takes this into account by stating that one process engages in at least as many internal actions as another. We use expansions to define an up-to technique in Section 2.5, and to precisely formulate the correctness of an encoding in Section 5.5.

Deviating from the standard presentation of expansion, we introduce some auxiliary terminology that will be useful in the next subsection for capturing aspects of divergence. It is partly inspired by the notion of progressing bisimulation in CCS [MS92b].

Definition 2.3.4 A weak simulation S is called

• progressing, if P \begin{matrix}− \\ − \end{matrix}^{μ} → P′ implies that there is Q′ with Q {= \atop =}^{μ} ⇒ Q′ such that (P′, Q′) ∈ S

• strict, if P \begin{matrix}− \\ − \end{matrix}^{μ} → P′ implies that there is Q′ with Q μ̂ ; \begin{matrix}− \\ − \end{matrix} → Q′ such that (P′, Q′) ∈ S

for all (P, Q) ∈ S and for all μ being τ or output with bn(μ) ∩ fn(P |Q) = ∅.

Note that a weak simulation is strong if it is both progressing and strict.

Definition 2.3.5 (Expansion) A binary relation E on processes is an expansion if E is a progressing simulation and E^{−1} is a strict simulation. Process Q expands P, written P ≲ Q, if there is an expansion E with (P, Q) ∈ E.

Fact 2.3.6 ∼ ⊂ ≲ ⊂ ≈ .

Divergence

Since we are going to formally reason about divergence properties of encodings in Section 5.8, we need some basic definitions. According with standard intuitions, a process P is said to be divergent, written P ⇑, if there is an infinite sequence of τ-steps starting at P; otherwise it is called convergent, written P ⇓.

Weak (bi-)simulation is insensitive to the divergence of processes. This lack of expressiveness arises from the definition of weak simulation, which may always choose to mimic τ-steps trivially. Weak bisimulation, or observation equivalence, may therefore equate two processes exactly one of which is diverging: it simply ignores the existence of infinite τsequences. Enhancements of bisimulation have been investigated that take divergence behavior explicitly into account, resulting in preorders among bisimilar processes [Wal90].

For our purposes in Section 5.8, the simpler property of preserving divergence will suffice. A weak simulation S has this property if P ⇑ implies Q⇑ for all (P, Q) ∈ S. Intuitively, when required to weakly simulate an infinite τ-sequence, S must progress infinitely often. Let us introduce some further notation (inspired by Priese [Pri78]) to make precise what this means.

Let \begin{matrix}− \\ − \end{matrix}^{τ} →^{n} denote a τ-sequence of length n and \begin{matrix}− \\ − \end{matrix}^{τ} →^{+} =^{def} \begin{matrix}− \\ − \end{matrix}^{τ} →^{n} for some n > 0 denote a non-empty, but arbitrarily long, finite sequence of τ-steps.

Definition 2.3.7 (Eventually progressing simulation) A weak simulation S is called eventually progressing if, for all (P, Q) ∈ S, there is a natural number k_{P} ∈ ℕ such that P \begin{matrix}− \\ − \end{matrix}^{τ} →^{n} P′ with n > k_{P} implies that there is Q′ with Q \begin{matrix}− \\ − \end{matrix}^{τ} →^{+} Q′ such that (P′, Q′) ∈ S.

According to the definition, a simulation S is eventually progressing if, for sufficiently long finite τ-sequences, S must eventually reproduce a τ-step. In this respect, k_{P} is to be understood as an upper bound for the number of τ-steps starting from P that may be trivially simulated. Note that every progressing simulation is, by definition, eventually progressing with upper bound 0.

With a progressing simulation, every infinite sequence may be simulated by subsequently simulating sufficiently long finite subsequences non-trivially, i.e., such that they represent progress. This resembles the chunk-by-chunk idea of simulation due to Gammelgaard [Gam91].

Lemma 2.3.8 Eventually progressing simulations preserve divergence.

Proof: Let S be a progressing simulation and (P, Q) ∈ S. If P ⇑ then there is P \begin{matrix}− \\ − \end{matrix}^{τ} →^{ω}. Since S is progressing, there is k_{P} ∈ ℕ such that P \begin{matrix}− \\ − \end{matrix}^{τ} →^{k_{P} +1} P′ \begin{matrix}− \\ − \end{matrix}^{τ} →^{ω} and Q \begin{matrix}− \\ − \end{matrix}^{τ} →^{+} Q′ with (P′, Q′) ∈ S. Since now P′⇑, we can repeat the procedure infinitely often. □

2.4 When weak bisimulation is too strong …

Every bisimulation B can be regarded as a pair (S_{1}, S_{2}) of contrary simulations S_{1} and S_{2}^{−1}, where S_{1} and S_{2} contain exactly the same pairs of processes, i.e., S_{1} = B = S_{2}. For some applications, this requirement is too strong. For example, consider the following ℙ-processes:

\begin{matrix}P & =^{def} & (i) & ( & \overline{i} & | i.A & | i.B & | i.C & ) \\ Q & =^{def} & (i_{1})(i_{2}) & ( & \overline{i_{1}} | \overline{i_{2}} & | i_{1}.A & | i_{1}.( i_{2}.B | i_{2}.C) & ) \end{matrix}

where i, i_{1}, i_{2} ∉ fn(A, B, C). The example was originally introduced in CCS, using choice operators [PS92]. In fact, both P and Q implement two different versions of some behavior that performs an internal choice among the processes A, B, and C by the concurrent race of inputs for an output on some shared internal channel. The difference is that P only uses one internal channel (i), whereas Q uses two of them (i_{1} and i_{2}) and, as a result, needs two internal steps in order to decide which of B or C is chosen in the case that A was preempted. Hence, the choice implemented by P is atomic, whereas the choice of Q is gradual.

Although intuitively P and Q might be regarded as observably equivalent by disregarding the internal choices, which are present in Q but not in P, they are not weakly bisimilar. According to the derivation trees up to ∼ (using the law (i)( i.P | Q) ∼ Q, if i ∉ fn(Q)) and with BC := (i_{2})( \overline{i_{2}} | i_{2}.B | i_{2}.C ),

\xymatrix{ & P \ar[dl]_{τ} \ar[d]_{τ} \ar[dr]^{τ} &  &  & Q \ar[dl]_{τ} \ar[dr]^{τ} \\ A & B & C & A &  & BC \ar[dl]_{τ} \ar[dr]^{τ} \\  &  &  &  & B &  & C}

the state BC cannot be related to any of the states beneath P, which would both simulate BC and be simulated by BC. At best, we can find two contrary simulations S_{1} and S_{2}^{−1} with

S =^{def} { (P, Q), (A, A), (B, B), (C, C), … }
S_{1} =^{def} S ∪ { (B, BC ), (C, BC ) }
S_{2} =^{def} S ∪ { (P, BC ) }

which, unfortunately, do not coincide. The distinguishing pairs express the problem with the partially committed τ-derivative BC of Q: on the one hand, it cannot be simulated by any τ-derivative of P due to their lack of ability to reach both B and C; on the other hand, it can itself no longer simulate P, because it has lost the ability to reach A.

As an appropriate mathematical tool to handle situations as the above example, Parrow and Sjödin developed the notion of coupled simulation [PS92]: two contrary simulations are no longer required to coincide, but only to be coupled in a certain way. Several candidates have been presented for what it means to be coupled. No coupling at all would just lead to the notion of mutual simulation. A non-trivial notion of coupling was based on the property of stability by requiring the coincidence of two contrary simulations in at least the stable states. This style induces a relation which is an equivalence only for convergent processes, and it has been proven to be strictly weaker than bisimulation and strictly stronger than testing equivalence [PS92]; indeed, the two processes P and Q of the introductory example are equivalent in that sense, as formalized in Definition 2.4.1 below.

In this paper, we use a generalization for divergent processes, as suggested by van Glabbeek [Gla93, PS94], where coupling requires the ability of a simulating process to evolve into a simulated process by internal action. We recapitulate the formal definition:

Definition 2.4.1 (Coupled simulation) A mutual simulation is a pair (S_{1}, S_{2}), where S_{1} and S_{2}^{−1} are weak simulations. A coupled simulation is a mutual simulation (S_{1}, S_{2}) satisfying • if (P, Q) ∈ S_{1}, then there is some Q′ such that Q ⟹ Q′ and (P, Q′) ∈ S_{2};

• if (P, Q′) ∈ S_{2}, then there is some P′ such that P ⟹ P′ and (P′, Q′) ∈ S_{1}.

Processes P and Q are coupled simulation equivalent (or coupled similar), written P ⇄ Q, if they are related by both components of some coupled simulation.

Using dotted lines to represent the simulations, the coupling property of (S_{1}, S_{2}) may be depicted as an ‘internally out-of-step bisimulation’ by:

[figure: P; S_{1}; P′; S_{1}; ⋯; P; ≽; P′; ≽; ⋯; Q; Q′; S_{2}; ⋯; or:; Q; Q′; ≽; ⋯]

Of two processes contained in one component relation of some coupled simulation, the simulated (more committed) process is always a bit ahead of its simulating (less committed) counterpart. Intuitively, ‘Q coupled simulates P ’ means that ‘Q is at most as committed as P ’ with respect to internal choices and that Q may internally evolve to a state Q′ where it is at least as committed as P, i.e., where P coupled simulates Q′.

Fact 2.4.2 Let (S_{1}, S_{2}) be a coupled simulation. Then (S_{2}^{−1}, S_{1}^{−1}) is a coupled simulation.

Observe that the pair (≈, ≈) is a coupled simulation by trivial coupling sequences, as motivated at the beginning of the section. Furthermore, the motivating example witnesses that coupled simulation equivalence is strictly coarser than weak bisimilarity.

Fact 2.4.3 ≈ ⊂ ⇄ .

On processes without infinite τ-sequences, coupled simulation is strictly finer than testing equivalence, so it represents a reasonable (and coinductively defined) candidate in the lattice of process equivalences [Gla93]. In general, it is compatible with all operators of ℙ.

Proposition 2.4.4 ⇄ is a congruence on ℙ.

Proof: Reflexivity is immediate by definition.

For symmetry, let P_{1} ⇄ P_{2} by (S_{1}, S_{2}) with (P_{1}, P_{2}) ∈ S_{1} ∩ S_{2}. This is equivalent to (P_{2}, P_{1}) ∈ S_{2}^{−1} ∩ S_{1}^{−1}, and, by Fact 2.4.2, we have P_{2} ⇄ P_{1}.

For transitivity, let P ⇄ Q ⇄ R due to their containment in coupled simulations (P, Q) ∈ (S_{PQ}, S_{QP}) and (Q, R) ∈ (S_{QR}, S_{RQ}). Now, let S_{PQR} := S_{PQ}S_{QR} and S_{RQP} := S_{QP}S_{RQ}. Then, both S_{PQR} and S_{RQP}^{−1} are simulations by transitivity of simulation. For the coupling between S_{PQR} and S_{RQP}, we show only one direction. Since (S_{PQ}, S_{QP}) is a coupled simulation, we know that Q ⟹ Q′ with (P, Q′) ∈ S_{QP}. Since (Q, R) ∈ S_{QR}, this sequence can be simulated by R ⟹ R′ with (Q′, R′) ∈ S_{QR}. Now, since (S_{QR}, S_{RQ}) is a coupled simulation, we have R′ ⟹ R′′ such that (Q′, R′′) ∈ S_{RQ}. Therefore, we conclude that R ⟹ R′′ with (P, R′′) ∈ S_{QP}S_{RQ} = S_{RQP}.

For congruence, we show that ⇄ is preserved by all operators in ℙ. For each pair (P_{1}, P_{2}) in ⇄, there is a witnessing coupled simulation (S_{1}, S_{2}). Congruence of ⇄ requires the preservation of ⇄ under all operators in ℙ. It is known that weak simulation is preserved by all operators of ℙ. In addition, we only have to check that the required coupling is preserved correspondingly. This, however, is straightforward since the coupling is just the existence of some possibly trivial internal sequence. For parallel composition and restriction, the coupling is inherited directly from the components; for (replicated) guards, the coupling is trivial. □

2.5 Up-to techniques

By the coinductive definition of bisimulation, a proof that two processes P and Q are bisimilar, i.e., P ≈ Q, rests on the construction of some bisimulation B which contains the pair (P, Q). Up-to techniques have been introduced in order to improve the bisimulation proof technique by relaxing the proof obligations and thereby reducing the size of the witness relation B [Mil89, San95b]. We explain the idea by the notion of weak simulation up to expansion. (The composition of relations is denoted by juxtaposition.)

Definition 2.5.1 (Simulation up to expansion) A binary relation S on processes is a (weak) simulation up to ≲ if (P, Q) ∈ S implies:

• if P \begin{matrix}− \\ − \end{matrix}^{μ} → P′, where μ is τ or an output with bn(μ) ∩ fn(P |Q) = ∅, then there is Q′ such that Q μ̂ ; {= \atop =} ⇒ Q′ and (P′, Q′) ∈ S ≲

• ( \overline{a}z|P , \overline{a}z|Q ) ∈ S for arbitrary messages \overline{a}z.

Note that the first obligation on S does not require of Q′ that (P′, Q′) ∈ S, but only that Q′ expands some process Q′′ with (P′, Q′′) ∈ S. The following lemma provides a proof technique for weak simulation based on the above definition.

Lemma 2.5.2 If Q simulates P up to expansion, then P ≼ Q.

Proof: Let U be a weak simulation up to expansion that contains (P, Q). Then the relation

U ∪ \{ (P′, Q′) | ∃(P_{0}, Q_{0}) ∈ U. ∃(P′, Q′′) ∈ U. ∃μ ∈ L. (P \begin{matrix}− \\ − \end{matrix}^{μ} → P′ ∧ Q μ̂ ; {= \atop =} ⇒ Q′′ ≲ Q′) \} is a

weak simulation and contains (P, Q). □

The following lemma allows us to compose coupled simulations with bisimulations.

Lemma 2.5.3 Let (S_{1}, S_{2}) be a coupled simulation and B a weak bisimulation. Then the composite pair (S_{1}B, S_{2}B) is again a coupled simulation.

Proof: We have to prove that both S_{1}B and (S_{2}B)^{−1} are weak simulations and that there is the desired coupling via internal transition sequences. All of these facts are straightforward. We only show the case for the reachability of coupled states.

Let (P, R) ∈ S_{1}B via Q, i.e., (P, Q) ∈ S_{1} and (Q, R) ∈ B. Then, since (S_{1}, S_{2}) is a coupled simulation, we know that there is Q′ with Q ⟹ Q′ and (P, Q′) ∈ S_{2}. Furthermore, from (Q, R) ∈ B we know that there is some R′ with R ⟹ R′ and (Q′, R′) ∈ B. Thus, (P, R′) ∈ S_{2}B.

The proof of the second clause for coupling is even simpler. Let (P, R) ∈ S_{2}B via Q, i.e., (P, Q) ∈ S_{2} and (Q, R) ∈ B. From (S_{1}, S_{2}) being a coupled simulation we know that there is P′ with P ⟹ P′ and (P′, Q) ∈ S_{2}. Then, immediately (P′, R) ∈ S_{1}B via Q. □

Thus, in order to prove that two processes S and T are coupled similar, it suffices to show that S is coupled similar to some other process A (this might be considerably easier), which, in turn, is bisimilar to the process T. We may call the composite (S_{1}B, S_{2}B) a coupled simulation up to bisimulation, although this is not exactly in the spirit of up-to techniques. There, the aim is to reduce the size of relations that are necessary to prove that two processes are related. Here, we do not decrease the size, but simply carry out the proof on another, but bisimilar, set of terms that may provide richer structure for actually doing the proof.

3 Discussion: Correctness of encodings

In this section, we briefly digress to review a few known notions of correctness and discuss their advantages and disadvantages. Thereby, we aim at precisely characterizing the class of non-prompt encodings that is represented by the choice encodings of the Introduction and Section 4. As shown later on in Section 5, it is the non-prompt character of choice encodings that complicates the definition of and reasoning about their correctness.

Intuitively, if we can compare terms and their translations directly, then we may require that every source term S and its translation [[ S]] should be semantically equivalent

S ≍ [[ S]]

where ≍ denotes some notion of equivalence; we provide examples with Theorems 5.6.1 and 5.7.4. The stronger the employed equivalence, the more we are tempted to accept [[ ]] as being correct. For process calculi, some prominent candidates among the vast number of equivalences are (with decreasing ability to distinguish process terms): strong and weak bisimulation, testing, and trace equivalence. Since most encodings introduce additional computation steps compared to the behavior of source terms, we may hardly expect correctness up to strong bisimulation. Weak bisimulation may be applicable whenever the additional steps are internal. Furthermore, bisimulation comes with coinductive proof techniques. Testing equivalences that are strictly weaker than bisimulation may often be sufficient as correctness criteria, but they lack a convenient proof technique. Therefore, bisimulation is also appealing in those cases where, for example, some testing equivalence would suffice.

In general, however, we cannot assume that we have a formal setting at hand that allows us to compare terms and their translations directly. The notion of full abstraction has been developed to get around this problem. Here, correctness is expressed as the preservation and reflection of equivalence of source terms. Let ≍_{s} and ≍_{t} denote equivalences of the source and the target language, respectively. Then, the full abstraction property is formulated as:

S_{1} ≍_{s} S_{2} if and only if [[ S_{1} ]] ≍_{t} [[ S_{2} ]].

Up to the chosen notions of equivalence, fully abstract encodings allow us—for reasoning about terms—to freely switch between the source and target languages in both directions. Note that, usually, the reflection (if ) of equivalence, often called adequacy, is relatively easy to establish. In contrast, to prove the preservation (only if ) of equivalence is not an easy task: the chosen notions of equivalence should be insensitive to the additional computation steps that are introduced by the encoding; moreover, when one is interested in congruences, the equivalence has to be preserved in not only translated high-level contexts, but arbitrary low-level contexts. Yet, only when both reflection and preservation hold the theory and proof techniques of a low-level language can always be used for reasoning about high-level terms; preservation then provides behavioral completeness, reflection provides behavioral soundness.

Often, e.g. for encodings of object-oriented languages, the source language is not a priori equipped with a notion of equivalence. Thus, we may not be able to check the encoding’s correctness via a full abstraction result. The notion of operational correspondence was therefore designed to capture correctness as the preservation and reflection of execution steps as defined by an operational semantics of the source and the target languages, and expressed in the model of transition systems which specify the execution of terms. Let →_{s} and →_{t} denote transition relations on the source and target language, respectively, and let ⇒_{s} and ⇒_{t} denote their reflexive transitive closure. Then, operational correspondence is characterized by two complementary propositions, which we briefly call completeness (ℭ) and soundness (𝔖).

Completeness (Preservation of execution steps.) The property

if S →_{s} S′, then [[ S]] ⇒_{t} [[ S′]]  (ℭ)

states that all possible executions of S may be simulated by its translation, which is naturally desirable for most encodings.

Soundness (Reflection of execution steps.) The converse of completeness, i.e., the property

if [[ S]] ⇒_{t} [[ S′]] then S ⇒_{s} S′,

is, in general, not strong enough since it deals neither with all possible executions of translations nor with the behavior of intermediate states between [[ S]] and [[ S′]]. For example, nondeterministic or divergent executions, sometimes regarded as undesirable, could although starting from a translation [[ S]] never again reach a state that is a translation [[ S′]]. A refined property may consider the behavior of intermediate states to some extent:

if [[ S]] →_{t} T then there is S →_{s} S′ such that T ≍_{t} [[ S′]]  (ℑ)

says that initial steps of a translation can be simulated by the source term such that the target-level derivative is equivalent to the translation of the source-level derivative.

Let us call a target-level step committing if it directly corresponds to some source-level step. It should be clear that only prompt encodings, i.e., those where initial steps of literal translations are committing, will satisfy ℑ. As a matter of fact, most encodings studied up to now in the literature are prompt. Promptness also leads to ‘nice’ proof obligations since it requires case analysis over single computation steps.

However, non-prompt encodings do not satisfy ℑ; like choice encodings, they allow administrative (or book-keeping) steps to precede a committing step. Sometimes (cf. [Ama94]), these administrative steps are well behaved in that they can be captured by a confluent and strongly normalizing reduction relation. Then, the encoding is optimized to perform itself the initial administrative overhead by mapping source terms onto administrative normal forms to satisfy ℑ. A satisfyingly general approach to take administrative steps into account is:

if [[ S]] ⇒_{t} T then there is S ⇒_{s} S′ such that T ⇒_{t} [[ S′]]  (𝔖)

says that arbitrary sequences of target steps are simulated (up to completion) by the source term. It takes all derivatives T —including intermediate states—into account and does not depend on the encoding being prompt or normalizable. Thus, 𝔖 is rather appealing. However, it only states correspondence between sequences of transitions and is therefore, in general, rather hard to prove, since it involves analyzing arbitrarily long transition sequences between [[ S]] and T (see [Wal95] for a successful proof).

Finally, note that a proof that source terms and their translations are the same up to some operationally defined notion of equivalence gives full abstraction up to that equivalence and operational correspondence for free (see Corollaries 5.6.4 and 5.7.6, and the discussion at the end of Section 5.4).

4 Encoding input-guarded choice, asynchronously

This section defines encodings of the asynchronous π-calculus with input-guarded choice ℙ^{Σ} into its choice-free fragment ℙ (§4.1): a divergence-free choice encoding, and a divergent variant of it (§4.2). The essential idea of the encodings is that a branch may consume a message before it checks whether it was allowed to do so; if yes, then it may proceed, otherwise it simply resends the consumed message. Such protocols are only correct with respect to asynchronous observation, which is insensitive to the temporary buffering of messages. An example process term (§4.3) exhibits the essential difference between the two choice encodings and prepares the ground for a discussion of possible correctness statements.

In the above-mentioned protocols, mutual exclusion among the branches of a choice is implemented by a concurrent race for a shared lock. Since the lock may be most succinctly expressed by means of some form of boolean values, we introduce (in §4.1) an intermediate language that provides a convenient primitive operator for testing boolean-valued messages; §4.4 gives a careful treatment of the expansion of those intermediate terms.

4.1 The setting

An encoding is a function from some source syntax into some target syntax. This subsection introduces the language ℙ^{Σ} that represents the source syntax. In addition, we refine the setting by an intermediate language ℙ^{test} to be used instead of the intended target language ℙ.

\xymatrix{𝕊 := & ℙ^{Σ} \ar@{|->}[dr] \ar@{=>}[d] \\  & ℙ & ℙ^{test} \ar@{|->}[l] & =: 𝕋}

In diagrams like the above, dotted arrows are just placeholders for encoding functions.

Source language We introduce choice as a finitely indexed operator on input terms. Its behavior is specified by the operational semantics rule in Table 3, which formally describes that each branch in a choice may be selected and consume an external message, preempting all of its competing branches. The set ℙ^{Σ} of processes with input-guarded choice is generated by adding a clause for ∑-expressions to the grammar of ℙ:

P ::= … | ∑_{j∈J} R_{j}

where J is some finite indexing set. We also use the abbreviation R_{1} + R_{2} to denote binary input-guarded choice. The labeled transition semantics of ℙ^{Σ} is the relation generated by the rules in Table 1 and rule C-INP in Table 3.

Target language(s) Instead of directly defining the encodings from ℙ^{Σ} into ℙ, we use an intermediate language ℙ^{test} that provides special boolean names, and also a conditional form test l then P else Q for testing the (boolean) value of messages along some channel l.

Let B := {f, t} be the set of special names that we interpret as boolean values. Let V := N ⊎ B be referred to as the set of values. Then the set ℙ^{test} of processes with conditionals is defined by adding a clause for test-expressions to the grammar of ℙ:

P ::= … | test y then P else P

In addition, in order to forbid restriction on, communication on, and substitution for booleans, we adopt some naming conventions concerning their admissible occurrences in the clauses of the grammar of ℙ (cf. §2) by requiring that x, y ∈ N and z ∈ V. Thus, the only use of booleans in ℙ^{test} is as objects in messages. Note that test-expressions can be regarded as abbreviations of if-expressions that are prefixed with some input of a boolean message.

test y then P_{1} else P_{2} ˆ= y(b) . if b then P_{1} else P_{2}

The reason for using test instead of if is, on the one hand, better readability and, on the other hand, that if, like matching operators, destroys some congruence properties of the language. In order to model the behavior of test-expressions that can interact with messages, we supply an operational semantics by the rules in Table 4 that properly fits with the labeled transition system semantics of ℙ and the explanation in terms of if.^{1} The

[figure: C-INP: ∑_{j∈J} y_{j}(x).P_{j} \begin{matrix}− \\ − \\ − \end{matrix}^{y_{k}z} → P_{k} if k ∈ J]

Table 3: Operational semantics for ∑-expressions labeled transition semantics of ℙ^{test} is then determined as the smallest relation generated by the rules in Table 4 and Table 1, where we add the side-condition z ∈ N to the rules INP and R-INP; this additional side-condition prevents the standard input forms from receiving special names, and thus also from unintendedly using special names as channels.

1By using an early instantiation scheme, the interaction between boolean messages and test-expressions is handled by the standard COM -rule; otherwise, we would have to supply some refined interaction rule for controlling the admissible transmission of booleans.

After having presented the encodings into 𝕋 in §4.2, we formalize in §4.4 the interpretation of those encodings as encodings into ℙ. The reader might object that these encodings can not be regarded as identical since 𝕋 contains test-expressions. However, we can safely make this identification up to some notion of equivalence. As one might expect, this depends on the way that we actually use the additional primitives in our choice encodings: we only use the booleans on restricted channels, so they never become visible. The formal justification later on uses this fact explicitly (cf. §5.5).

4.2 Two choice encodings

This subsection contains two simple encodings of 𝕊 into its choice-free fragment 𝕋. Both encodings C[[ ]], D[[ ]] : 𝕊 → 𝕋 map terms of the source language 𝕊 inductively into the target language 𝕋. Since the encodings coincide on all constructors but choice, we use a common homomorphic scheme of definition, where [[ ]] may denote either C[[ ]] or D[[ ]]:

[[ (x)P ]] =^{def} (x)[[ P ]]  [[ P_{1}|P_{2} ]] =^{def} [[ P_{1} ]] | [[ P_{2} ]]
[[ \overline{y}z]] =^{def} \overline{y}z  [[ 0 ]] =^{def} 0
[[ y(x).P ]] =^{def} y(x).[[ P ]]  [[ ! R]] =^{def} ! [[ R]]

This scheme will also be reused later on for other encoding functions: if an encoding X [[ ]] acts homomorphically on each constructor of ℙ, then it is defined according to the scheme with [[ ]] replaced by X [[ ]].

A source-level choice term is implemented by a particular target-level structure: for each choice expression, the translation

[[ ∑_{j∈J} R_{j} ]] =^{def} (l)( \overline{l}t | ∏_{j∈J} Branch_{l}⟨ [[ R_{j} ]] ⟩ )

installs a local lock—a message on l that carries a boolean name—that is only accessible for the parallel composition of its branches, which use the lock for running a mutual exclusion

[figure]

TRUE: test l then P_{1} else P_{2} \begin{matrix}− \\ − \end{matrix}^{lt} → P_{1}
FALSE: test l then P_{1} else P_{2} \begin{matrix}− \\ − \end{matrix}^{lf} → P_{2}

Table 4: Operational semantics for test-expressions protocol, as specified by the semantic rule C-INP. The protocol crucially depends on the invariant that at any time there is at most one boolean message available on l. If we manage to maintain this invariant, i.e., if it holds for all derivatives, then we are guaranteed that at any time the value of the lock is uniquely determined, which allows us to regard possible subsequent messages on l as representing the behavior of a ‘determinate’ lock that is accessible via l. The determinacy of the lock limits the nondeterminacy of the encoding solely to the concurrent race of the translations of the branches. Initially the lock carries t, so it represents the fact that the choice is not yet resolved; consequently, a committed choice will be recognizable by the lock carrying f.

Two slightly different ways of implementing the mutual exclusion protocol are given in the following subsections, differing only with respect to the possibility of undoing activities of branches, thus yielding two different definitions for the implementation Branch_{l}.

Divergence-free protocol

In the Introduction, we presented the following algorithm (note the use of test):

Branch_{l}⟨ y_{j}(x).P_{j} ⟩ =^{def} y_{j}(x) . test l then ( C[[ P_{j} ]] | \overline{l}f ) else ( \overline{y_{j}}x | \overline{l}f )

Every branch tests the lock after having received a value on its channel. If the lock carries t, then the testing branch proceeds with its continuation, otherwise it resends the message that it has consumed and terminates. Each time the lock is read, it is immediately reinstalled— independent of its former value—with the value f. Thus, at most one branch will ever be chosen, since only the first branch that reads the lock will read t.

In order to conveniently denote intermediate states in the branches of an encoding, we use the following abbreviations, where R on the left hand side matches the term y(x).P such that y, x, P may be used on the right-hand side of the definitions.

Read_{l}⟨ R ⟩ =^{def} y(x).Test_{l}⟨ R ⟩
Test_{l}⟨ R ⟩ =^{def} test l then Commit_{l}⟨ R ⟩ else Abort_{l}⟨ R ⟩
Commit_{l}⟨ R ⟩ =^{def} \overline{l}f | P
Abort_{l}⟨ R ⟩ =^{def} \overline{l}f | \overline{y}x

Observe that Branch_{l}⟨ R ⟩ = Read_{l}⟨ R ⟩ by definition, so a choice expression is translated by

C[[ ∑_{j∈J} R_{j} ]] =^{def} (l)( \overline{l}t | ∏_{j∈J} Read_{l}⟨ C[[ R_{j} ]] ⟩ )  where l is fresh

into the composition of its branches in Read-state and the lock carrying t.

Note that the C-encoding does not add divergence to the behavior of source terms, as can be observed by inspection of the abbreviations: only finite τ-sequences are used in order to implement a choice, whereas τ-loops are not possible (we prove it formally in §5.8).

Protocol with undo-loops

We now define the other choice encoding. Its main difference from the encoding C[[ ]] is that a supposedly committed branch may change its mind and deny the commitment, releasing the lock and giving back the value it consumed from the environment. Let internal choice be:

P ⊕ Q =^{def} (i) ( \overline{i} | i.P | i.Q ) where i fresh

The encoding D[[ ]] is then defined by modifying just the clause Test_{l}⟨ R ⟩ of the C-encoding by inserting an internal choice as follows:

Test_{l}⟨ R ⟩ =^{def} test l then Commit_{l}⟨ R ⟩ ⊕ Undo_{l}⟨ R ⟩ else Abort_{l}⟨ R ⟩
Undo_{l}⟨ R ⟩ =^{def} \overline{l}t | \overline{y}x

Note that in contrast to the cases of Commit/Abort, where the lock’s value is set to f, in the case of Undo it is crucial to set it to t, because in this case the choice is still not resolved. In order to have a fresh copy of the branch in initial state available after having undone an activity, we use replication of the Read-agents as the translation of branches: with Branch_{l}⟨ R ⟩ = ! Read_{l}⟨ R ⟩ a choice expression is translated by:

D[[ ∑_{j∈J} R_{j} ]] =^{def} (l)( \overline{l}t | ∏_{j∈J}! Read_{l}⟨ D[[ R_{j} ]] ⟩ ) where l is fresh

In their D-translation, convergent branches of a choice term possibly engage in internal loops that may be used to restart a possibly committing branch from an initial state. This behavior might be considered problematic from an implementation point of view, but in the next subsection, we shall see that the D-encoding is interesting despite its divergence.

4.3 An example

We highlight the difference between the two choice encodings by comparing a particular source term with both of its translations. Let

S = \overline{y_{2}}z | N  where  N = R_{1} + R_{2}  with  R_{i} = y_{i}(x).P_{i}

describe a binary choice in the presence of a single message matching the second of the branches, where P_{1}, P_{2} are arbitrary terms in ℙ (i.e., not containing choices or test-expressions). It turns out that both S ≉ C[[ S]] and S ≈ D[[ S]] hold, which imply that the C-encoding neither preserves nor reflects weak bisimulation (Lemmas 4.3.3 and 4.3.4).

Divergence-free encoding

The transition systems of the above S and C[[ S]] can be depicted as follows. Since, for establishing bisimulations in the asynchronous π-calculus, input transitions are only considered in the context of arbitrary messages, we do not mention them explicitly in the pictures, but just the internal and output transitions. The dotted lines representing simulation relations are to be read from left to right; when the lines are vertical, simulation holds in both directions. We get

[figure: 𝕊 :; N; ≽; S; ≽; \overline{y_{2}}z; τ; P_{2}\{^{z}/_{x}\}; ≽; ≽; 𝕋 :; C[[ N ]]; ≼; C[[ S]]; \overline{y_{2}}z; ≼; τ; C; τ; ≽; C_{2}; ≼]

where (letting B_{i} = Read_{l}⟨ C[[ R_{i}]] ⟩):

C[[ S]] = \overline{y_{2}}z | C[[ N ]]
C[[ N ]] = (l)( \overline{l}t | B_{1} |  B_{2} )
C = (l)( \overline{l}t | B_{1} |  Test_{l}⟨ C[[ R_{2} ]] ⟩ \{^{z}/_{x}\} )
C_{2} = (l)( 0 | B_{1} |  Commit_{l}⟨ C[[ R_{2} ]] ⟩ {^{z}/_{x}} )

≡ \underbrace{(l)( \overline{l}f | B_{1} )}

≈0 (see Lemma 5.2.2)

| C[[ P_{2} ]]{^{z}/_{x}}

We may phrase the intermediate state C as having partially committed: at that stage of commitment, it is already clear that one of the branches will eventually be chosen, but it is not yet clear if it will be the activated branch (as we chose in the computation path with C_{2}) or if it will be the competing branch (still waiting at y_{1} for some value), since there might still be a suitable message provided by the context which could activate the latter and afterwards pre-empt the former. As a consequence, the state C does not directly correspond to any of the source terms with respect to weak bisimulation, which implies:

Fact 4.3.1 S ≉ C[[ S]].

On the other hand, the observation that S ≽ C ≽ P_{2}{^{z}/_{x}} with S ⟹ P_{2}{^{z}/_{x}} in the above example suggests coupled simulation as an appropriate notion of correctness for the C-encoding.

Divergent encoding

The corresponding transition systems of S and D[[ S]], again omitting input transitions, are

[figure: 𝕊 :; N; ≈; S; ≈; \overline{y_{2}}z; τ; P_{2}\{^{z}/_{x}\}; ≈; 𝕋 :; D[[ N ]]; D[[ S]]; \overline{y_{2}}z; τ; D; τ; ≈; D′; τ; ≈; τ; D_{2}]

where (letting B_{i} = ! Read_{l}⟨ D[[ R_{i}]] ⟩):

D[[ S]] = \overline{y_{2}}z | D[[ N ]]
D[[ N ]] = (l)( \overline{l}t | B_{1} | B_{2} )
D = (l)( \overline{l}t | B_{1} | B_{2} | Test_{l}⟨ D[[ R_{2} ]] ⟩ \{^{z}/_{x}\} )
D′ = (l)( 0 | B_{1} | B_{2} | (Commit_{l}⟨ D[[ R_{2} ]] ⟩ ⊕ Undo_{l}⟨ D[[ R_{2} ]] ⟩){^{z}/_{x}} )
= (l)( 0 | B_{1} | B_{2} | (D[[ P_{2} ]]\{^{z}/_{x}\} | \overline{l}f) ⊕ (\overline{y_{2}}z | \overline{l}t) )

D_{2} ≡ \underbrace{(l)( \overline{l}f | B_{1} | B_{2} )}

≈0 (see Lemma 5.7.1)

| D[[ P_{2} ]]{^{z}/_{x}}

The internal undo-transition from D′ back to D[[ S]] is essential in proving that the intermediate states D and D′ are actually weakly bisimilar to S, since only by internally looping back to the initial state can they simulate all of S’s behavior; that possibility is lacking in the C-encoding.

Proposition 4.3.2 S ≈ D[[ S]].

Note another aspect of the above computation paths of C[[ S]] and D[[ S]]: Whereas the step from C[[ S]] to C uses up the component B_{2}, its correspondent survives in the step from D[[ S]] to D since, there, it is a replication.

Full abstraction?

We can now use S to prove that the C-encoding is not fully abstract with respect to weak bisimulation. Note that both C[[ ]] and D[[ ]], extended in the obvious way for test-clauses, act as an identity on terms in 𝕋, which implies that C[[ C[[ S]] ]] = C[[ S]] and C[[ D[[ S]] ]] = D[[ S]].

Weak bisimulation is not reflected by the C-encoding.

Lemma 4.3.3 C[[ S_{1} ]] ≈ C[[ S_{2} ]] does not imply S_{1} ≈ S_{2}.

Proof: Let S_{1} = S be the example above and S_{2} = C[[ S]] its translation. By definition, we have C[[ S_{2} ]] = C[[ C[[ S]] ]] = C[[ S]] = C[[ S_{1} ]], but S_{2} ≉ S. □

Weak bisimulation is also not preserved by the C-encoding.

Lemma 4.3.4 S_{1} ≈ S_{2} does not imply C[[ S_{1} ]] ≈ C[[ S_{2} ]].

Proof: Let S_{1} = S and S_{2} = D[[ S]], so that S_{1} ≈ S_{2}. Suppose, for a contradiction, that C[[ ]] preserved ≈; then, by definition, we would have C[[ S]] = C[[ S_{1} ]] ≈ C[[ S_{2} ]] = C[[ D[[ S]] ]] = D[[ S]] ≈ S, which contradicts Fact 4.3.1. □

4.4 Expanding the encodings

In §4.1, we introduced the intermediate language ℙ^{test} as a for the convenient presentation of choice encodings. We justify the use of ℙ^{test} by translating it itself into the language ℙ.

We first sketch the idea of expanding boolean messages and test-expressions into ℙ by using 2-adic messages. It is directly inspired from a standard protocol for encoding the behavior of persistent boolean values [Mil93] adapted to the needs of the example, where the boolean messages correspond to ephemeral boolean variables. The encoding function B̃[[ ]] acts homomorphically on every constructor of ℙ that does not involve booleans; for those constructors that apply to or just mention booleans, B̃[[ ]] is defined by

B̃[[ \overline{l}t ]] =^{def} l(t, f).\overline{t}
B̃[[ \overline{l}f ]] =^{def} l(t, f).\overline{f}
B̃[[ test l then P else Q]] =^{def} (t)(f)( \overline{l}⟨t, f⟩ | t.B̃[[ P ]] | f.B̃[[ Q]] )

where \overline{l}⟨t, f⟩ and l(t, f).P denote 2-adic communication (cf. [Mil93]). In contrast to the higher-level test-notation, the B̃-encoding causes one additional τ-step for each test.

We still have not yet arrived at the language ℙ due to the use of 2-adic messages in the B̃-encoding; note that we do not need the expressive power of the full polyadic π-calcu-lus, here. To get rid of them, we may use a technique for asynchronously encoding 2-adic messages [HT91] that was called ‘zip-lock’ technique by Odersky [Ode95a]. The encoding function Z[[ ]] acts homomorphically on every constructor of ℙ; for 2-adic messages and inputs,

\begin{matrix}Z[[ \overline{l}⟨t, f⟩]] & =^{def} & (u)(\overline{l}u & | & u(v) & .( & \overline{v}t & | & u(w) & . & \overline{w}f)) \\ Z[[ l(t, f).P ]] & =^{def} & l(u) & . & (v)(\overline{u}v & | & v(t) & . & (w)(\overline{u}w & | & w(f).Z[[ P ]])) \end{matrix}

yields monadic processes, where the names u, v, w are assumed not to occur free in P. We could have used fewer freshly created names by reusing u for different purposes, but the number of necessary internal actions cannot be reduced, since one (on l) is needed to establish the connection, two (on v, w) for transferring the data, and another two (on u) for transmitting the local channels and also serving as internal acknowledgments in order to maintain the order of the data by transmitting them in a ‘zip-lock’ way.

By using the zip-lock encoding, we give an expanded B-encoding into the monadic target language ℙ, where we also use ‘void’ names that are merely used as signal objects and could be instantiated with any name since they are never used as channels.

B[[ \overline{l}t ]] =^{def} Z[[ l(t, f).\overline{t}]]
B[[ \overline{l}f ]] =^{def} Z[[ l(t, f).\overline{f} ]]
B[[ test l then P else Q]] =^{def} (t)(f)( Z[[ \overline{l}⟨t, f⟩]] | t.B[[ P ]] | f.B[[ Q]] )

Obviously, a language with boolean messages and test-expressions as primitives will be much clearer than the B-translations, when used in order to write down an encoding function.

Finally, we are ready to give the full encodings C_{≲}[[ ]] and D_{≲}[[ ]] by composing the earlier encodings into the intermediate target language 𝕋 with the expanding encoding B[[ ]]:

\begin{matrix}C_{≲}[[ ]] & =^{def} & (B^{∘} C)[[ ]] \\ D_{≲}[[ ]] & =^{def} & (B^{∘} D)[[ ]] \end{matrix}

which are indeed encodings of ℙ^{Σ} into its choice-free fragment ℙ.

\xymatrix{𝕊 = & ℙ^{Σ} \ar@{|->}[dr]^{C[[ ]],D[[ ]]} \ar@{|->}[d]_{C_{≲}[[ ]],D_{≲}[[ ]]} \\  & ℙ & ℙ^{test} \ar@{|->}[l]^{B[[ ]]} & = 𝕋}

We can ‘safely’ use primitive test-forms within the encoding functions since, as we will show in §5.5, the following property holds:

for all S ∈ 𝕊 : for all C[[ S]] ⟶^{∗} T : T ≲ B[[ T ]]

i.e., the encoding B[[ ]] ‘expands’ certain 𝕋-terms in the sense of Definition 2.3.5: T and B[[ T ]] are weakly bisimilar, but the latter uses more τ-steps. The proof of this property relies on the fact that any use of booleans within the encoding C[[ ]] is restricted for an outside observer of a choice expression. The same property holds of the encoding D[[ ]].

4.5 Discussion

As the distinguishing example in §4.3 indicates, for reasoning about the choice encoding’s behavioral correctness, we are able to compare source terms S and their translations [[ S]] directly; the visible labels of source and target transitions are the same. Furthermore, by the arguments of the previous section, both encodings can be regarded as endomorphic mappings where the target 𝕋 is a fragment of the source 𝕊, at least up to expansion of translations.

With respect to operational correspondence, the choice encodings represent the class of non-prompt translations where, as in the motivation of the soundness property 𝔖, committing steps of translations are preceded by administrative steps. Those pre-administrative steps can not be simply defined away (by using administrative normal forms) since, in general, they are not confluent: imagine a process containing two choices that compete for a single message; both choices could evolve by consuming the message, but each would pre-empt the other.

In the first author’s PhD thesis [Nes96], the discussion of appropriate notions of correctness as well as a discussion of possible (correct) and impossible (incorrect) variants of the proposed choice encodings are carried out in considerably more detail.

5 Correctness proof by decoding

In this section, we prove the correctness of the C-encoding with respect to coupled simulation equivalence (§5.2–§5.6) and sketch the corresponding proof for the D-encoding with respect to weak bisimulation equivalence (§5.7). The main contribution of this section is a proof notation and technique, with decoding functions, which we use to exhibit that source terms and their translations are in fact equivalent. We also include a proof that the C_{≲}-encoding is divergence-free (§5.8).

5.1 Overview

Since the choice encodings are not prompt, we have to explicitly deal with the behavior of intermediate states and relate them to source terms with equivalent behavior. Moreover, in the case of the C_{≲}-encoding, an intermediate state may be partially committed, so we may have to relate it to two different source terms. By definition, partial commitments are absent in source terms; thus, a partially committed derivative of a translation can only be related to source terms which represent either its reset or its completion.

Technically, we are going to build the coupled simulation constructively as a pair of decoding functions from target terms to source terms. However, intermediate states are target terms that have lost the structure of being literal translations of source terms; thus, it is impossible to denote the source term from which an intermediate target term derives without some knowledge of its derivation history.

We therefore introduce annotated source terms (§5.2) as abbreviations for derivatives of their translations. An annotated term shows its source-level choice structure while providing information about which target state its choices inhabit, using a representation of its derivation history that is constructed from an operational semantics of annotated choice. We formally introduce the language 𝔸 of annotated source terms and use it as follows for the investigation of the correctness of the C_{≲}-encoding:

Factorization (§5.3) Annotated source terms represent abbreviations of target terms. We define an annotation encoding A mapping source terms to abbreviations and a flattening encoding F expanding abbreviations to target terms.

Decoding (§5.4) Annotated source terms deal with partial commitments explicitly. We define two decoding functions U of annotated terms back into source terms, where U_{♭} resets and U_{♯} completes partial commitments.

Expansion (§5.5) Since the target language 𝕋 is a language extended with booleans, we show that their use in our setting is rather well-behaved according to the expanding encoding B.

[figure: 𝕊; A[[ ]]; C[[ ]]; 𝔸; F[[ ]]; ℙ; 𝕋; 𝕊; 𝔸; U_{♯}[[ ]]; U_{♭}[[ ]]; ℙ; 𝕋; B[[ ]]]

The factorization, the decodings, and the expansion enjoy several nice properties:

1. F is a strong bisimulation between abbreviations and boolean target terms.

2. (U_{♭}, U_{♯}) is a coupled simulation between abbreviations and source terms.

3. B, i.e., a variant of it, is an expansion for booleans in target terms.

Those can be combined to provide a coupled simulation on 𝕊 × ℙ. The observation that every source term S and its translation C_{≲}[[ S]] are related by this relation concludes the proof of coupled-simulation-correctness of the C_{≲}-encoding (§5.6).

Simplifications due to homomorphic encodings and decodings Many of the proofs in this section have in common that they exhibit particular transitions of terms by constructing appropriate inference trees either

• from the inductive structure of (annotated) terms, or

• by simply replacing some leafs in the inference trees of their encodings or decodings.

Since the A, F, U_{♭}, U_{♯}, B-functions are each defined homomorphically on every constructor of ℙ according to the scheme in §4, there is a strong syntactic correspondence between terms and their respective translations, and, as a consequence, there is also a strong correspondence between transition inference trees. More precisely, since in transitions involving choice

• there is at most one application of a choice rule, and

• an application of the choice rule always represents a leaf in the inference tree,

it suffices for all proofs to regard choice terms in isolation.

When looking for simulations between terms and their translations (as in the proofs of Proposition 5.3.4, Lemmas 5.3.1, 5.4.2 and 5.4.3), a transition which does not involve choice rules is trivially simulated via the identical inference tree by the translated term. A transition which emanates from a choice term inside a term context, and which may be simulated by the translated choice term in isolation, will also be derivable by the same inference tree, except for the leaf being adapted to the simulating transition. Note that possible side-conditions are not critical, if the simulation has been successful for the choice term itself.

When (as in the proofs 5.4.7 and 5.4.6) looking for internal transitions of a particular term, generated by occurrences of choice, it suffices to use choices in isolation since τ-steps are passed through arbitrary contexts without condition.

5.2 Annotated choice

This subsection introduces an annotated variant of choice, which provides abbreviations for all derivatives of C-translations. Its shape reveals the high-level structure, but it exhibits low-level operational behavior. The attached annotations record essential information about the low-level derivation history.

According to the definition in §4, the computations of individual branches of a choice will pass through basically three different states: Read, Test, and one of Commit or Abort as the final state. The state of each branch is completely determined by the result of two inputs:

• the value (if any) which is currently carried by the channel, and

• the boolean (if any) which has been assigned by acquiring the lock.

For the representation of that information for a J-indexed choice, we use

• a partial function v : J ⇀ V, mapping choice indices to values, and

• a possibly empty set B ⊆ J of choice indices such that B ∩ dom(v) = ∅.

In the context of a particular J-indexed choice with branches R_{j} = y_{j}(x).P_{j} for each j ∈ J, the definedness of v_{j} (the value v(j) held by branch j) means that a value has been read from the environment, but has not yet either led to a commitment of branch j or been reinjected into the environment. The set B records those branches which have already accessed the

[figure]

READ: ( ∑_{j∈J} R_{j})_{B}^{v} \begin{matrix}− \\ − \\ − \end{matrix}^{y_{k}z} → ( ∑_{j∈J} R_{j})_{B}^{v +(k↦z)}  if k ∈ J\(V ∪B)

COMMIT: ( ∑_{j∈J} R_{j})_{∅}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{\{k\}}^{v −k} | P_{k}\{^{v^{k}}/_{x}\} if k ∈ V

ABORT: ( ∑_{j∈J} R_{j})_{B≠∅}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{B+k}^{v −k} | \overline{y_{k}} v_{k}  if k ∈ V

Table 5: Early transition semantics for annotated choice

boolean lock. An empty set B means that none of the branches has yet been chosen, i.e., that the choice has not (yet) committed. Then, with the abbreviation V := dom(v), the state of each individual branch can be retrieved from the annotations v and B. Branch k ∈ J is in

• Read-state if k ∈ J\(V ∪B)

• Test-state if k ∈ V

• Commit/Abort-state if k ∈ B.

The state of the whole choice is completely determined by the states of its branches.

Definition 5.2.1 (Annotated choice) Let J be a set of indices. Let R_{j} = y_{j}(x).P_{j} be input prefixes for j ∈ J. Let v : J ⇀ V and B ⊆ J with B ∩ V = ∅, where V := dom(v). Then,

∑_{j∈J} R_{j}  and  ( ∑_{j∈J} R_{j})_{B}^{v}

are referred to as bare and annotated choice, respectively.

Annotated choice is given the operational semantics in Table 5. The dynamics of annotated choice mimic precisely the behavior of the intended low-level process. READ allows a branch k in Read-state (k ∈ J\(V ∪B)) to optimistically consume a message.^{2} If the choice is not yet resolved (B = ∅), COMMIT specifies that an arbitrary branch k in Test-state (k ∈ V) can immediately evolve into its Commit-state. i.e., trigger its continuation process P_{k}. After the choice is resolved (B ≠ ∅), ABORT allows any branch k in Commit-state (k ∈ V) to evolve into its Abort-state release their consumed messages. Intuitively, by reading the lock, a branch immediately leaves the choice system and exits. Therefore, annotated choice only contains branches in either Read- or Test-state.

2Compared to its late counterpart, the early instantiation scheme may be more intuitive for showing that a particular value has entered the choice system. Furthermore, we do not have to deal with α-conversion of homonym bound names in different branches. Nevertheless, the further development in this paper does not depend on this decision. Note also that early and late bisimulation coincide in our setting (cf. §2.3).

We distinguish three cases for choice constructors that are important enough to give them names: initial for V = ∅ = B, partial for V ≠ ∅ and B = ∅, and committed for B ≠ ∅. Note that both initial and partial choice contain all branches, whereas committed choice never does; it will even become empty, once all branches have reached their final state (B = J).

Committed choice exhibits a particularly interesting property: its branches in Test-state already have consumed a message which they will return after recognizing, by internally testing the lock, that the choice is already committed; its branches in Read-state are still waiting for values to be consumed and—since the choice is resolved and the lock carries f— immediately resent after an internal step. Processes with such receive-and-resend behavior are weakly bisimilar to 0 and were called identity receptors by Honda and Tokoro [HT92]. In fact, a stronger property holds:

Lemma 5.2.2 ( ∑_{j∈J} R_{j})_{B≠∅}^{v} ≳ ∏_{j∈V} \overline{y_{j}} v_{j}.

Proof: Let M be an arbitrary m-ary composition of messages. We show that

R =^{def} \{ ( \underbrace{M | ( ∑_{j∈J} R_{j})_{B≠∅}^{v}}_{LHS} , \underbrace{M | ∏_{j∈V} \overline{y_{j}} v_{j}}_{RHS} ) | ( ∑_{j∈J} R_{j})_{B}^{v} ∈ 𝔸 \}

is an expansion.

case internal steps According to the operational semantics, τ-transitions are only possible for LHS. Since RHS does not exhibit τ-transitions, we show that for all LHS \begin{matrix}− \\ − \end{matrix}^{τ} → LHS′, we have (LHS′, RHS) ∈ R. There are two subcases: either (1) via an ABORTstep of choice, or (2) via choice consuming an M-message due to READ.

case ABORT Since B ≠ ∅, for k ∈ V, via ABORT, followed by m times PAR_{1}, we have

LHS = M | ( ∑_{j∈J} R_{j})_{B}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} →≡ M | \overline{y_{k}} v_{k} | ( ∑_{j∈J} R_{j})_{B+k}^{v −k} =: LHS′

Since k’s values are erased from v, we observe that the R-correspondent of LHS′—note that it is an admissible left hand side for R—as defined by

M | \overline{y_{k}} v_{k} | ∏_{k≠j∈V} \overline{y_{j}} v_{j} = M | ∏_{j∈V} \overline{y_{j}} v_{j}

coincides with RHS. case READ For M ≡ N | \overline{y}z and k ∈ J\(V ∪B) such that y = y_{k}, let v′ = v +(k↦z). Then, via rule READ for the choice part, OUT for the indicated y-message, and rule COM to derive the τ-transition from the former visible transitions, we have

LHS = N | \overline{y}z | ( ∑_{j∈J} R_{j})_{B}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → N | ( ∑_{j∈J} R_{j})_{B}^{v′} =: LHS′

By definition, the R-correspondent of LHS′, is of the form

N | ∏_{j∈V′} \overline{y_{j}} v_{j} = N | \overline{y_{k}} v_{k} | ∏_{j∈V} \overline{y_{j}} v_{j} = M | ∏_{j∈V} \overline{y_{j}} v_{j}

which coincides with RHS.

case output steps According to the operational semantics, output-transitions are possible for each message in M, i.e., for both LHS and RHS. The (strong) bisimulation behavior for that case is trivial. LHS does not exhibit further immediate outputs. In contrast, RHS allows outputs for each message in ∏_{j∈V} \overline{y_{j}} v_{j}, i.e., for k ∈ V, via OUT

and PAR, we have

RHS = M | ∏_{j∈V} \overline{y_{j}} v_{j} \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{\overline{y_{k}} v_{k}} → M | ∏_{k≠j∈V} \overline{y_{j}} v_{j} =: RHS′

Due to ABORT, we derive an internal step and afterwards release the message \overline{y_{k}} v_{k}

LHS = M | ( ∑_{j∈J} R_{j})_{B}^{v}  \begin{matrix}− \\ − \end{matrix}^{τ} → M | ( ∑_{j∈J} R_{j})_{B+k}^{v −k} | \overline{y_{k}} v_{k}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{\overline{y_{k}} v_{k}} → M | ( ∑_{j∈J} R_{j})_{B+k}^{v −k} =: LHS′

which weakly simulates the transition of RHS. We observe that (LHS′, RHS′) ∈ R.

□

Corollary 5.2.3 (Inertness) ( ∑_{j∈J} R_{j})_{B≠∅}^{∅} ≳ 0.

From an asynchronous observer’s point of view, committed choice behaves exactly like the composition of the messages that are held by branches in Test-state, except that it involves additional internal computation. Note that a standard (synchronous) observer, which may detect inputs, would be able to tell the difference.

Since the purpose of annotated choice is to keep track of which low-level actions belong to the same high-level choice, we introduce a language of annotated processes. The set ℙ^{(Σ)} such processes is generated by adding a clause for (∑)-expressions to the grammar of ℙ:

P ::= … | ( ∑_{j∈J} R_{j})_{B}^{v}

The operational semantics of ℙ^{(Σ)} is given by the rules in Table 1 and Table 5.

5.3 Factorization

We now introduce the components of a factorization for the encoding C[[ ]]: an annotation encoding A[[ ]], and a flattening encoding F[[ ]].

\xymatrix{𝕊 \ar@{|->}[r]^{A[[ ]]} \ar@{|->}[dr]_{C[[ ]]} & 𝔸 \ar@{|->}[d]^{F[[ ]]} & : ⊂ ℙ^{(Σ)} \\  & 𝕋}

An intermediate sublanguage 𝔸 will be characterized as the sublanguage of ℙ^{(Σ)} that precisely contains the derivatives of A-translations. We write C, A, and F for the encoding functions considered as relations.

Annotation.

The encoding A[[ ]] : 𝕊 → ℙ^{(Σ)} acts homomorphically on every constructor except for choice according to the scheme in §4. The latter case is given by

A[[ ∑_{j∈J} R_{j} ]] =^{def} ( ∑_{j∈J} A[[ R_{j} ]])_{∅}^{∅}

which translates choices into their annotated counterparts with all branches in initial state. The following lemma represents a first simple operational completeness statement for A[[ ]].

Lemma 5.3.1 (Completeness) A is a weak simulation up to expansion.

Proof: We show the proof for weak synchronous simulation, which implies the asynchronous case. The proof is by structural induction on S ∈ 𝕊 and transition induction on S ⟶ S′. By the simplification discussed in Section 5.1, it suffices to regard the case

S = ∑_{j∈J} R_{j}

where, according to the rules in Table 3, there is only one subcase.

case C-INP For k ∈ J, with ∑_{j∈J} R_{j} \begin{matrix}− \\ − \\ − \end{matrix}^{y_{k}z} → P_{k}\{^{z}/_{x}\} ,

there is always a weakly simulating sequence by READ and COMMIT

A[[ ∑_{j∈J} R_{j} ]] = ( ∑_{j∈J} A[[ R_{j} ]])_{∅}^{∅} \begin{matrix}− \\ − \\ − \end{matrix}^{y_{k}z} → ( ∑_{j∈J} A[[ R_{j} ]])_{∅}^{(k↦z)}
\begin{matrix}− \\ − \end{matrix}^{τ} → A[[ P_{k}]]\{^{z}/_{x}\} | ( ∑_{j∈J} A[[ R_{j} ]])_{\{k\}}^{∅}
≳ A[[ P_{k}]]{^{z}/_{x}} | 0
≡ A[[ P_{k}{^{z}/_{x}}]]

where the expansion relation holds due to Lemma 5.2.2. □

Intermediate language.

Terms in the target of A[[ ]] and also their derivatives are of a particular restricted form, which can be made precise by characterizing the possible shape of occurrences of choice terms. Let a subterm be called guarded when it occurs as a subterm of a guard. The basic syntactic properties of the intermediate language then are:

• All occurrences of choice are annotated.

• All guarded occurrences of choice are initial.

• Unguarded occurrences of choice may be initial, partial, or committed.

Later on in this paper (for the proofs of the Lemmas 5.4.6 and 5.4.8), we need these properties in order to conclude that no guarded annotated choice is in an intermediate state.

Therefore, let 𝔸 denote the sublanguage of terms in ℙ^{(Σ)} that satisfy the above syntactic requirements; we give an inductive grammar for generating appropriate terms by two levels. One level generates terms I with only initially annotated occurrences of choice terms

\begin{aligned}G & ::= & y(x).I \\ I & ::= & 0 | \overline{y}z | G | (y)I | I|I | ! G | ( ∑_{j∈J} G_{j})_{∅}^{∅} \end{aligned}

Another level on top generates terms A which allow active (top-level) choices to be in intermediate state, but guarded occurrences of choice only to be initial, as specified by I:

\begin{aligned}R & ::= & y(x).I \\ A & ::= & 0 | \overline{y}z | R | (y)A | A|A | ! R | ( ∑_{j∈J} R_{j})_{B}^{v} \end{aligned}

where v : J ⇀ V and B ⊆ J for arbitrary index set J, as usual. A term A ∈ 𝔸 is called partially committed (or partial), if it contains at least one occurrence of partial choice, and fully committed (or full), otherwise.

An important property of 𝔸 is that it is transition-closed.

Lemma 5.3.2 For all A ∈ 𝔸, if A \begin{matrix}− \\ − \end{matrix}^{μ} → A′, then A′ ∈ 𝔸.

Proof: By inspection of the rules in Table 5. □

Flattening.

The encoding F[[ ]] : ℙ^{(Σ)} → 𝕋 acts homomorphically on every constructor but annotated choice according to the scheme in §4. For annotated choice, the translation

F[[ ( ∑_{j∈J} R_{j})_{B}^{v} ]] =^{def} (l)( \overline{l}b | ∏_{j∈J\(V ∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{j∈V}  Test_{l}⟨ F[[ R_{j} ]] ⟩{^{v(j)}/_{x}} )

where b is t, if B = ∅, and f, otherwise, expands the abbreviations into the intended target term by following the semantic rules in Table 5. Branches in Test-state are those that carry values (therefore j ∈ V); the substitution {^{v(j)}/_{x}} replaces the input variable in the continuation process P_{j} with the corresponding value. Branches in Read-state must neither currently carry values (j ∉ V) nor have accessed the lock after reading values (j ∉ B).

Lemma 5.3.3 (Factorization) 1. F[[ ]]^{∘} A[[ ]] = C[[ ]].

2. F[[ ]] is surjective. for all A ∈ 𝔸, F[[ Aσ]] = F[[ A]]σ.

Proof:

1. Straightforward induction on the structure of source terms.

2. Straightforward. Neither A[[ ]] nor F[[ ]] erase names. Free (bound) occurrences of names of terms correspond to free (bound) occurrences in their translations. □

The important property of the factorization is that the semantics of annotated choice (cf. Table 5) precisely mirrors the behavior of the original translations and their derivatives.

Proposition 5.3.4 (Semantic correctness) F is a strong bisimulation.

Proof: By simple induction on the structure of A ∈ 𝔸 and transition induction on A ⟶ A′ and F[[ A]] ⟶ T′, where it suffices to check the induction case for annotated choice constructors (see Appendix A.1). □

Corollary 5.3.5 (Mirroring) For all S ∈ 𝕊 and C[[ S]] ⟶^{∗} T ∈ 𝕋, there is A ∈ 𝔸 such that (A[[ S]] ⟶^{∗} A and) F[[ A]] = T.

With Proposition 5.3.4 we prove the correctness of C[[ ]] by proving the correctness of A[[ ]]. This is a considerably simpler task, since the 𝔸-annotations in the target of A[[ ]] provide more structure, in particular concerning partially committed derivatives, which is heavily exploited in §5.4.

5.4 Decoding derivatives of A-translations

We want to construct a coupled simulation (cf. Definition 2.4.1) between source terms and abbreviated target terms by mapping the latter back to the former. Since derivatives of target terms may correspond to source-level choices in a partially committed intermediate state, there are two natural strategies for decoding. The decoding functions U_{♭}[[ ]] and U_{♯}[[ ]]

\xymatrix{𝕊 & 𝔸 \ar@{|->}[l]_{U_{♯}[[ ]]} \ar@{|->}[l]^{U_{♭}[[ ]]}}

map partially committed annotated terms in 𝔸 back to source terms in 𝕊 which are either

• the least possible committed (resetting decoding U_{♭}), or

• the most possible committed (committing decoding U_{♯}).

The functions U_{♭}[[ ]], U_{♯}[[ ]] : 𝔸 → 𝕊 act homomorphically on every constructor but annotated choice according to the scheme in §4. For the latter, we distinguish between choices that are initial, committed, or partial.

For non-partial choices, the two decoding functions have the same definition (read U[[ ]] as either U_{♭}[[ ]] or U_{♯}[[ ]]): initial choice (V = ∅ = B) is mapped to its bare counterpart,

initial :  U[[ ( ∑_{j∈J} R_{j})_{∅}^{∅} ]] =^{def} ∑_{j∈J} U[[ R_{j} ]]
committed :  U[[ ( ∑_{j∈J} R_{j})_{B≠∅}^{v} ]] =^{def} ∏_{j∈V} \overline{y_{j}} v_{j}

while committed choice (B ≠ ∅) is mapped to the parallel composition of those messages which are currently held by its branches.

For partial choice (B = ∅ and V ≠ ∅), the two decoding functions act in a different way according to the intuition described above.

Resetting. The aim is to decode an annotated term to its least possible committed source correspondent. Intuitively, this means that we have to reset all of its partial commitments by mapping it to the original choice in parallel with the already consumed messages.

partial :  U_{♭}[[ ( ∑_{j∈J} R_{j})_{∅}^{v≠∅} ]] =^{def} ∏_{j∈V} \overline{y_{j}} v_{j} | ∑_{j∈J} U_{♭}[[ R_{j} ]]

Committing. The aim is to decode an annotated term to a committed source correspondent. Intuitively, this means that we have to complete one of the (possibly several) activated branches that the annotated choice has engaged in. Let k := take(V) select an arbitrary element of V. Then,

partial :  U_{♯}[[ ( ∑_{j∈J} R_{j})_{∅}^{v≠∅} ]] =^{def} ∏_{j∈V −k} \overline{y_{j}} v_{j} | U_{♯}[[ P_{k}]]\{^{v^{k}}/_{x}\}

maps to the source-level commitment to the selected branch.

Lemma 5.4.1 (Decoding)

1. Let U ∈ {U_{♭}, U_{♯}}. Then U[[ ]]^{∘} A[[ ]] = id.

2. Both U_{♭}[[ ]] and U_{♯}[[ ]] are surjective.

3. For A ∈ 𝔸 and U ∈ {U_{♭}, U_{♯}}, U[[ Aσ]] = U[[ A]]σ.

Proof: Immediate by definition (1,2); straightforward by induction (3). □

In the remainder of this subsection, we prove that (U_{♭}, U_{♯}) is a coupled simulation on 𝔸×𝕊 (Proposition 5.4.9). This requires, in particular, that U_{♭} and U_{♯}^{−1} are weak simulations. We will see that these simulations are eventually progressing. First, we show that U_{♭}[[ A]] simulates A (i.e., A ≼ U_{♭}[[ A]]) for all A ∈ 𝔸.

Lemma 5.4.2 U_{♭} is a weak simulation.

Proof: The proof is by structural induction on A ∈ 𝔸 and transition induction on U_{♯}[[ A]] ⟶ S′. By the simplification discussed in Section 5.1, it suffices to regard the case

A = ( ∑_{j∈J} R_{j})_{B}^{v}

where, by the operational rules in Table 5, there are three subcases.

case (committed) B ≠ ∅ : Then, U_{♭}[[ A]] = ∏_{j∈V} \overline{y_{j}} v_{j} .

Since we know by Lemma 5.2.2 that ( ∑_{j∈J} R_{j})_{B}^{v} ≳ ∏_{j∈V} \overline{y_{j}} v_{j},

we have that, in this case, U_{♭}[[ A]] is even bisimilar to A.

case (initial) V = ∅ = B : Then, U_{♭}[[ A]] = ∑_{j∈J} U_{♭}[[ R_{j} ]]

and there is only one type of transitions possible. Note that we do not have to directly simulate input transitions for simulation in the asynchronous π-calculus, but we have to care about the simulation in all contexts, including matching messages. Therefore: case READ /OUT /COM : For k ∈ J\(V ∪B), we have

\overline{y_{k}}z | ( ∑_{j∈J} R_{j})_{B}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{B}^{v +(k↦z)} and

U_{♭}[[ \overline{y_{k}}z | ( ∑_{j∈J} R_{j})_{B}^{v} ]] = \overline{y_{k}}z | ∑_{j∈J} R_{j} | ∏_{j∈V} \overline{y_{j}} v_{j} ≡ U_{♭}[[ ( ∑_{j∈J} R_{j})_{B}^{v +(k↦z)} ]]

immediately concludes the proof by an empty weakly simulating sequence.

case (partial) B = ∅ ≠ V : Let k = take(v). There are two subcases:

case READ /OUT /COM : (completely analogous to previous case). case COMMIT : For k ∈ V, we have

( ∑_{j∈J} R_{j})_{∅}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → P_{k}σ_{k} | ( ∑_{j∈J} R_{j})_{\{k\}}^{v −k}

and via C-INP/OUT/PAR/COM , there is the simulating step

U_{♭}[[ ( ∑_{j∈J} R_{j})_{∅}^{v} ]] = ∑_{j∈J} R_{j} | ∏_{j∈V} \overline{y_{j}} v_{j}
\begin{matrix}− \\ − \end{matrix}^{τ} → P_{k}\{^{v^{k}}/_{z}\} | ∏_{k≠j∈V} \overline{y_{j}} v_{j}
= U_{♭}[[ P_{k}σ_{k} | ( ∑_{j∈J} R_{j})_{{k}}^{v −k} ]]

which concludes the proof. □

Next, we show that U_{♯}[[ A]] is simulated by A (i.e., A ≽ U_{♯}[[ A]]) for all A ∈ 𝔸.

Lemma 5.4.3 U_{♯}^{−1} is a weak simulation.

Proof: The proof is by structural induction on A ∈ 𝔸 and transition induction on U_{♯}[[ A]] ⟶ S′. By the simplification discussed in Section 5.1, it suffices to regard the case

A = ( ∑_{j∈J} R_{j})_{B}^{v}

where, by definition of U_{♯}, there are three subcases.

case (initial) V = ∅ = B : Then U_{♯}[[ A]] = ∑_{j∈J} y_{j}(x).U_{♯}[[ P_{j} ]]

where, according to the rule in Table 3, there is only one subcase for generating transitions: C-INP. For k ∈ J, we have

∑_{j∈J} y_{j}(x).U_{♯}[[ P_{j} ]] \begin{matrix}− \\ − \\ − \end{matrix}^{y_{k}z} → U_{♯}[[ P_{k}]]\{^{z}/_{x}\}

and there is always a weakly simulating sequence by READ and COMMIT

A = ( ∑_{j∈J} R_{j})_{∅}^{∅} \begin{matrix}− \\ − \\ − \end{matrix}^{y_{k}z} → ( ∑_{j∈J} R_{j})_{∅}^{(k↦z)} \begin{matrix}− \\ − \end{matrix}^{τ} → P_{k}σ_{k} | ( ∑_{j∈J} R_{j})_{\{k\}}^{∅} =: A′

where U_{♯}[[ A′]] = U_{♯}[[ P_{k}]]{^{z}/_{x}} holds. case (committed) B ≠ ∅ : Then, U_{♯}[[ A]] = ∏_{j∈V} \overline{y_{j}} v_{j} .

case OUT : For k ∈ V, the transitions

U_{♯}[[ A]] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{y}v_{k}} → ∏_{j∈V −k} \overline{y_{j}} v_{j} =: S_{k}

can be simulated by

A \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{B+k}^{v −k} | \overline{y_{k}} v_{k} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{y}v_{k}} → ( ∑_{j∈J} R_{j})_{B+k}^{v −k} =: A_{k}

such that S_{k} = U_{♯}[[ A_{k}]].

case (partial) B = ∅ ≠ V : Let k = take(v). Then

U_{♯}[[ A]] = ∏_{j∈V −k} \overline{y_{j}} v_{j} | U_{♯}[[ P_{k}]]σ_{k} =: S′.

By A \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{\{k\}}^{v −k} | P_{k}σ_{k} =: A′ such that S′ = U_{♯}[[ A′]]

we can always take an internal step in order to fully commit A. Note that A′ is fully committed since, as a guarded subterm, P_{k} is fully committed by definition of 𝔸. The observation that S′ = U_{♯}[[ A′]] already concludes the proof since we may reduce it to the case of full terms. □

In addition, the weak simulations U_{♭} and U_{♯}^{−1} satisfy further useful properties (cf. §5.8).

Lemma 5.4.4

1. U_{♭} is strict, U_{♯}^{−1} is progressing.

2. Both U_{♭} and U_{♯}^{−1} are eventually progressing.

Proof: Both the strictness of U_{♭} and the progressiveness of U_{♯}^{−1} follow from previous proofs: For U_{♭}, proof 5.4.2 shows that some τ-steps of A may be simulated trivially by U_{♭}[[ A]]:

A \begin{matrix}− \\ − \end{matrix}^{τ} → A′  implies  U_{♭}[[ A]] τ̂ ; \begin{matrix}− \\ − \end{matrix} → U_{♭}[[ A′]]

For U_{♯}^{−1}, proof 5.4.3 shows that no τ-step of U_{♯}[[ A]] may be suppressed by A:

U_{♯}[[ A]] \begin{matrix}− \\ − \end{matrix}^{τ} → U_{♯}[[ A′]]  implies  A {= \atop =}^{τ} ⇒ A′

Immediately, we get that U_{♯}^{−1} is eventually progressing.

However, we have not yet proven that also U_{♭} is eventually progressing. We proceed by analyzing τ-sequences starting from an arbitrary A ∈ 𝔸.

A = A_{0} \begin{matrix}− \\ − \end{matrix}^{τ} → A_{1} \begin{matrix}− \\ − \end{matrix}^{τ} → A_{2} \begin{matrix}− \\ − \end{matrix}^{τ} → ⋯

Since we know that U_{♭} is strict, we have that

A_{i} \begin{matrix}− \\ − \end{matrix}^{τ} → A_{i+1}  implies  U_{♭}[[ A_{i}]] τ̂ ; \begin{matrix}− \\ − \end{matrix} → U_{♭}[[ A_{i+1} ]],

so we only have to argue that there is an upper bound k_{A} for the number of steps where the τ-step may be simulated trivially such that for n > k_{A}:

A = A_{0} \begin{matrix}− \\ − \end{matrix}^{τ} → A_{1} \begin{matrix}− \\ − \end{matrix}^{τ} → ⋯ \begin{matrix}− \\ − \end{matrix}^{τ} → A_{n}  implies  U_{♭}[[ A]] \begin{matrix}− \\ − \end{matrix}^{τ} →^{+} U_{♭}[[ A_{n}]].

For arbitrary steps

A_{i} \begin{matrix}− \\ − \end{matrix}^{τ} → A_{i+1}

we may distinguish four different cases, according to which combination of rules have been applied in the inference. We omit merely structural rules and mention only the essential rules. The following analysis resembles the proof of Lemma 5.4.2. The difference is that, here, we are not interested in visible steps; instead, we take a closer look at the simulations of τ-steps.

case COM/CLOSE/∗-INP Here, no choice operator is involved. The transition is caused by a subterm which may be regarded as a target term. The decoding U_{♭}[[ ]] reproduces this part homomorphically at the source level, wherefore we have

U_{♭}[[ A_{i}]] \begin{matrix}− \\ − \end{matrix}^{τ} → U_{♭}[[ A_{i+1} ]]

case COM/CLOSE/READ An occurrence of a choice operator is involved. By inspection of rule READ and the definition of U_{♭}[[ ]], we have

U_{♭}[[ A_{i}]] ≡ U_{♭}[[ A_{i+1} ]]

case COMMIT The transition is coming from a partially committed occurrence of annotated choice. Here, we have,

U_{♭}[[ A_{i}]] \begin{matrix}− \\ − \end{matrix}^{τ} → U_{♭}[[ A_{i+1} ]]

case ABORT Similar to the case before, except that there is no need to perform a τ-step at the source-level.

U_{♭}[[ A_{i}]] ≡ U_{♭}[[ A_{i+1} ]]

Now, if we look at the above τ-sequence between A_{0} and A_{n}, we have to argue that the second and fourth case cannot happen unboundedly often and, by that, prevent the first and third case. In fact, if A contains no choices, only the first case applies, concluding the proof.

If A contains choices, we may count the number of all branches in Read- or Test-state of all (unguarded) occurrences of choice, since exactly those may give rise to the sequence of τ-steps. In a partial/initial choice, the number of its branches in Read-state, determined by |J\(V ∪ B)|, tells how many subsequent applications of the second case (READ) might be possible, before a COMMIT-step has to be derived. In a committed choice, the number of its branches in Test-state (provided by |V |) yields the number of possible subsequent applications of the forth case (ABORT); afterwards, no more τ-steps are generated from this choice, since it is strongly bisimilar to 0.

Since each term A may only contain a finite number of unguarded occurrences of choice, k_{A} is determined as the sum of all of their branches in either Read- or Test-state. □

Apart from the simulation proofs for the components, a coupled simulation also requires two coupling properties—the existence of internal transition sequences connecting the simulation relations on both sides (Definition 2.4.1). For the proofs of these two properties, which we carry out by induction on the structure of terms, we only exploit the annotations of choices in A to derive the required internal transitions. We start by stating a useful fact.

Fact 5.4.5 Let A ∈ 𝔸 be fully committed. Then U_{♯}[[ A]] = U_{♭}[[ A]].

Full 𝔸-terms trivially satisfy coupling properties, since the two decodings coincide. For partially committed terms, this does not hold. There, we have to derive nontrivial internal transitions. Since choice may also occur guarded in a term, we might have to deal with transitions under prefixes, which are forbidden in the operational semantics. Therefore, we must restrict guarded occurrences of choice to being non-partial (e.g. initial)—which is exactly what is guaranteed by the definition of 𝔸 in Section 5.3.

Since U_{♭}[[ A]] ≽ A for all A ∈ 𝔸, the first coupling property requires the existence of transition U_{♭}[[ A]] ⟹ U_{♯}[[ A]] (in 𝕊, thus called 𝕊-coupling).

[figure: 𝕊 :; U_{♭}[[ A]]; U_{♯}[[ A]]; ≽; 𝔸 :; A; ≽]

Lemma 5.4.6 (𝕊-coupling) For all A ∈ 𝔸, U_{♭}[[ A]] ⟹ U_{♯}[[ A]].

Proof: The proof is by structural induction on A ∈ 𝔸. By the simplification discussed in Section 5.1, it suffices to regard the case

A = ( ∑_{j∈J} R_{j})_{B}^{v}

where, by definition of U_{♯}[[ ]], there are three subcases.

case (initial) V = ∅ = B or (committed) B ≠ ∅ :

Immediate by Fact 5.4.5. case (partial) B = ∅ ≠ V : Let k = take(V). Then,

\begin{aligned}U_{♭}[[ A]] & = & ∏_{j∈V} \overline{y_{j}} v_{j} | ∑_{j∈J} U_{♭}[[ R_{j} ]] \\ & \begin{matrix}− \\ − \end{matrix}^{τ} → & ∏_{j∈V −k} \overline{y_{j}} v_{j} | U_{♭}[[ P_{k}]]σ_{k} = ∏_{j∈V −k} \overline{y_{j}} v_{j} | U_{♯}[[ P_{k}]]σ_{k} = U_{♯}[[ A]]. \end{aligned}

where U_{♭}[[ P_{k}]]σ_{k} = U_{♯}[[ P_{k}]]σ_{k} since P_{k}σ_{k} is fully committed.

There may be several occurrences of partially committed choices in a term A, but, by definition, they only occur unguarded. We may simply collect the corresponding internal steps in either order which leads to A ⟹ A′. □

Since A ≽ U_{♯}[[ A]] for all A ∈ 𝔸, the second coupling property addresses U_{♯}-related terms. In this case, it is not as simple as for the 𝕊-coupling to denote what coupling means, so we explain it a bit more carefully: For all A ∈ 𝔸, whenever (A, S) ∈ U_{♯}, i.e., S = U_{♯}[[ A]], there is an internal sequence A ⟹ A′ (in 𝔸, thus called 𝔸-coupling), such that (A′, S) ∈ U_{♭}, i.e., S = U_{♭}[[ A′]]. If we link the two equations for S, we get the coupling requirement U_{♯}[[ A]] = U_{♭}[[ A′]] for A ⟹ A′. In the diagram

[figure: 𝕊 :; U_{♯}[[ A]]; ≽; = U_{♯}[[ A′]] =; ≼; U_{♭}[[ A′]]; 𝔸 :; A; A′; ≽]

we also indicate the way we proceed in order to do the proof. The relation on the left is the assumption because U_{♯}^{−1} is a simulation. The two relations on the right hold if A′ is fully committed. The following lemma states that such an A′ always exists as a derivative of A and, furthermore, connects the left- and right-hand sides of the diagram.

Lemma 5.4.7 For all A ∈ 𝔸, there is a fully committing A ⟹ A′ such that U_{♯}[[ A]] = U_{♯}[[ A′]].

A = ( ∑_{j∈J} R_{j})_{B}^{v}

where, by definition of U_{♯}[[ ]], there are three subcases.

case (initial) V = ∅ = B or (committed) B ≠ ∅ :

Immediate with A′ =^{def} A. case (partial) B = ∅ ≠ V : Let k = take(V).

Then, with A \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{\{k\}}^{v −k} | P_{k}σ_{k} =^{def} A′

we have U_{♯}[[ A]] = ∏_{j∈V −k} \overline{y_{j}} v_{j} | U_{♯}[[ P_{k}]]σ_{k} = U_{♯}[[ A′]].

Note that P_{k} is fully committed since it was guarded in A and not changed by the transition; thus, A′ is fully committed, since branch k has been successfully chosen.

□

Lemma 5.4.8 (𝔸-coupling) For all A ∈ 𝔸, there is A ⟹ A′ such that U_{♯}[[ A]] = U_{♭}[[ A′]].

Proof: Let A′ be constructed as in the proof of Lemma 5.4.7. Thus, we know that U_{♯}[[ A]] = U_{♯}[[ A′]] and, since A′ is fully committed, we also know (Fact 5.4.5) that U_{♯}[[ A′]] = U_{♭}[[ A′]].

□

Finally, the main property of the decoding functions U_{♭}[[ ]] and U_{♯}[[ ]] is:

Proposition 5.4.9 (U_{♭}, U_{♯}) is a coupled simulation.

Proof: By Lemmas 5.4.2 and 5.4.3, we know that (U_{♭}, U_{♯}) is a mutual simulation. By Lemmas 5.4.6 and 5.4.8, we have the necessary coupling between U_{♭} and U_{♯}. □

Corollary 5.4.10 (U_{♯}^{−1}, U_{♭}^{−1}) is a coupled simulation.

Proof: By Fact 2.4.2. □

Before ending this section, we show how the decoding functions may be used to provide a notably sharp operational correctness argument for the A-encoding. Let = = = = = =^{a_{1}···a_{n}} ⇒ denote the sequence = = =^{a_{1}} ⇒ ⋯ = = =^{a_{n}} ⇒ where the a_{i} are output-labels. Then, for arbitrary S ∈ 𝕊 and A[[ S]] = = = = = =^{a_{1}···a_{n}} ⇒ A, we have the following relations:

[figure: 𝕊 :; S; a_{1}···a_{n}; ≽; ≼; U_{♭}[[ A]]; U_{♯}[[ A]] =: S′; ≽; ≽; ≼; 𝔸 :; A[[ S]]; a_{1}···a_{n}; A; ≽; A[[ S′]]]

each derivative A of a translation A[[ S]] represents an intermediate state in some sourcelevel computation evolving from an S-derivative U_{♭}[[ A]] into an S-derivative S′ := U_{♯}[[ A]], as proved by Proposition 5.4.6 (𝕊-coupling). Furthermore, by Proposition 5.4.8 (𝔸-coupling), A can internally evolve into the A-translation of S′. In arbitrary contexts within 𝕊, the derivation trace of S corresponds to the derivation trace of A[[ S]], since U_{♭} is a weak simulation containing (A[[ S]], S). Finally, U_{♭}[[ A]] and U_{♯}[[ A]] coincide in the case that A is not partial.

The results of this subsection provide a very tight correspondence between source terms S and their annotated translations A[[ S]]. It may be written as S ⇄ A[[ S]] for every S ∈ 𝕊, since every pair (S, A[[ S]]) is contained in both components of the coupled simulation (U_{♯}^{−1}, U_{♭}^{−1}). However, we are not primarily interested in properties of A[[ ]], but in properties of C[[ ]] and C_{≲}[[ ]]. Those results are assembled in §5.6 after we have shown rigorously in the next subsection that the use of booleans in the target language 𝕋 is of mere notational convenience.

5.5 Expanding derivatives of C-translations

Another advantage of abbreviated target terms is that we can use their structure to prove that boolean messages and test-expressions are correctly expanded into terms of the language ℙ. More precisely, the above Corollary 5.3.5 allows us to quantify over all derivatives T of C-translations by simply quantifying over all terms A in 𝔸, and assuming that T = F[[ A]].

We start with an operational correspondence result for the B-encoding of derivatives of C-translations. It makes explicit the number of additional τ-steps that are needed in order to perform the exchange of 2-adic messages via the zip-lock encoding, and the subsequent triggering action, where the void name is exchanged.

Lemma 5.5.1 (Operational correspondence for B[[ ]]) Let T := F[[ A]] for some A ∈ 𝔸.

1. Let μ ≠ τ. Then T \begin{matrix}− \\ − \end{matrix}^{μ} → T′ iff B[[ T ]] \begin{matrix}− \\ − \end{matrix}^{μ} → B[[ T′]].

2. If T \begin{matrix}− \\ − \end{matrix}^{τ} → T′, then there is either B[[ T ]] \begin{matrix}− \\ − \end{matrix}^{τ} → B[[ T′]] or B[[ T ]] \begin{matrix}− \\ − \end{matrix}^{τ} →^{6} ≡ B[[ T′]].

3. If B[[ T ]] \begin{matrix}− \\ − \end{matrix}^{τ} → P, then there is T \begin{matrix}− \\ − \end{matrix}^{τ} → T′ such that either P = B[[ T′]] or P \begin{matrix}− \\ − \end{matrix}^{τ} →^{5} ≡ B[[ T′]].

Proof: By transition induction on F[[ A]] \begin{matrix}− \\ − \end{matrix}^{μ} → T′ and (B^{∘} F)[[ A]] \begin{matrix}− \\ − \end{matrix}^{μ} → P (see §A.2). □

Note that part 3 of the operational correspondence lemma witnesses the promptness of the B-encoding: the first low-level interaction in

B[[ T ]] \begin{matrix}− \\ − \end{matrix}^{τ} → P \begin{matrix}− \\ − \end{matrix}^{τ} →^{5} ≡ B[[ T′]]

always corresponds to some 𝕋-level interaction.

According to the proof, the rather constrained behavior of interactions along the channels u, v, w, t, f (as introduced by the B-encoding) is due to its temporarily determinate character. As soon as the first private interaction has taken place (via l according to the encoding functions), the following five interactions are determined since any of the above private channels is used uniquely and is restricted to the outside world—no other actions may prevent those five from taking place. This leads us to a strengthening of cases 2 and 3 of the operational correspondence lemma, so for the intermediate states P′ after the first interaction and before reaching the expansion of the successor state:

B[[ T ]] \begin{matrix}− \\ − \end{matrix}^{τ} → P ⟹ P′ ⟹≡ B[[ T′]] implies P′ ≳ B[[ T′]].

Lemma 5.5.2 Let T := F[[ A]] for some A ∈ 𝔸.

2. If T \begin{matrix}− \\ − \end{matrix}^{τ} → T′, then there is B[[ T ]] \begin{matrix}− \\ − \end{matrix}^{τ} → P with P ≳ B[[ T′]].

3. If B[[ T ]] \begin{matrix}− \\ − \end{matrix}^{τ} → P, then there is T \begin{matrix}− \\ − \end{matrix}^{τ} → T′ and P ≳ B[[ T′]].

Proof: By looking closer at the proof for operational correspondence in Appendix A.2; all the details are already there. □

In order to carry over this result to the relation between test-expressions and their Btranslations, we define an extension of the relation B by including the required pairs for intermediate derivatives P′ of B[[ T ]].

B^{→} =^{def} B ∪ { (T′, P′) ∈ ℙ^{test} × ℙ | there is T = F[[ A]] for A ∈ 𝔸

such that T \begin{matrix}− \\ − \end{matrix}^{τ} → T′ and B[[ T ]] \begin{matrix}− \\ − \end{matrix}^{τ} →^{+} P′ ⟹≡ B[[ T′]] \}

Lemma 5.5.3 B^{→} is an expansion.

Proof: Immediate by the operational correspondence (Lemma 5.5.1) and the expansion property for all intermediate states P′. □

Fact 5.5.4 For all T = F[[ A]] for A ∈ 𝔸 : (T, B[[ T ]]) ∈ B^{→}.

Corollary 5.5.5 Let A ∈ 𝔸 and S ∈ 𝕊.

1. For all T := F[[ A]] : T ≲ B[[ T ]].

2. For all C[[ S]] \begin{matrix}− \\ − \end{matrix}^{τ} →^{∗} T : T ≲ B[[ T ]].

Proof: (1) is a consequence from Fact 5.5.4 and Lemma 5.5.3. (2) is then a direct consequence of (1) and Corollary 5.3.5. □

Lemma 5.5.6 B^{→} is progressing; (B^{→})^{−1} is eventually progressing.

Proof: Directly from the operational correspondence Lemma 5.5.1. The eventually progressing property for (B^{→})^{−1} comes with an upper bound for trivially simulating τ-steps as determined by the (finite) number of ‘active’ test-expressions, multiplied with 5 as the worst case that all of the active test-expressions have just done the first step. □

5.6 Main result

In this section, we establish a coupled simulation (cf. Definition 2.4.1) between source terms and their C_{≲}-translations by exploiting the results for the A-encoding via the decodings U_{♭}[[ ]] and U_{♯}[[ ]]. Reasoning about the annotated versions of choice allowed us to use their highlevel structure for the decoding functions.

We argued that we could safely concentrate on the annotated language 𝔸, since F[[ ]] flattens abbreviation terms correctly (up to ∼) into terms of ℙ^{test}, whereas B[[ ]] expands test-expressions correctly (up to ≲) into terms of ℙ. In order to combine those ideas, let the simulations ℭ (completeness) and 𝔖^{−1} (soundness) be defined by

ℭ =^{def} U_{♯}^{−1}F B^{→}  and  𝔖 =^{def} U_{♭}^{−1}F B^{→}

according to the diagram

\xymatrix{ℙ^{Σ} \ar@{|->}[d]_{ℭ} \ar@{|->}[d]^{𝔖} & ℙ^{(Σ)} \ar@{|->}[l]_{U_{♯}} \ar@{|->}[l]^{U_{♭}} \ar@{|->}[d]^{F} \\ ℙ & ℙ^{test} \ar@{|->}[l]^{B^{→}}}

where the relations U_{♭} and U_{♯} are only defined on the subset 𝔸 of ℙ^{(Σ)}. The results for annotated terms carry over smoothly to the expanded versions.

Theorem 5.6.1 ( ℭ, 𝔖 ) is a coupled simulation.

Proof: By Corollary 5.4.10, Proposition 5.3.4, and Lemma 2.5.3 twice. □

Observe that ℭ is constructed from the committing decoding U_{♯}[[ ]], so derivatives of target terms are at most as committed as their ℭ-related source terms. Analogously, 𝔖 is constructed from the resetting decoding U_{♭}[[ ]], so derivatives of target terms are at least as committed as their 𝔖-related source terms.

By construction, the relations ℭ and 𝔖 are big enough to contain all source and target terms and, in particular, to relate all source terms and their C_{≲}-translations.

Lemma 5.6.2 For all S ∈ 𝕊 : (S, C_{≲}[[ S]]) ∈ ℭ ∩ 𝔖.

Proof: By the syntactic adequacy lemmas (5.4.1 and 5.3.3), we know that, for all S ∈ 𝕊, the translations A[[ S]] and C[[ S]] = (F ^{∘} A)[[ S]] yield the witnesses for (S, C_{≲}[[ S]]) being contained in both ℭ and 𝔖. □

Thus, the C_{≲}-encoding is operationally correct, in the sense that every source term is simulated by its translation (completeness via ℭ) and also itself simulates its translation (soundness via 𝔖). Moreover, the result is much stronger since the simulations are coupled.

Theorem 5.6.3 (Correctness of C_{≲}) For all S ∈ 𝕊 : S ⇄ C_{≲}[[ S]].

Proof: By Theorem 5.6.1 and Lemma 5.6.2. □

Corollary 5.6.4 (Full abstraction) For all S_{1}, S_{2} ∈ 𝕊 : S_{1} ⇄ S_{2} iff C_{≲}[[ S_{1} ]] ⇄ C_{≲}[[ S_{2} ]].

Proof: By transitivity. □

Note that the C_{≲}-encoding is not fully abstract up to weak bisimulation, as proven in §4.3.

5.7 Correctness of the divergent protocol

The proof for the divergent choice encoding follows the outline of Sections 5.2 to 5.6. In contrast to the divergence-free encoding, the D_{≲}-encoding is correct up to weak bisimulation. The overall proof is simpler since the proof obligations for weak bisimulation require less work than those of coupled simulation. We sketch the full proof here by carefully defining just the main ingredient of the factorization and decoding diagram:

[figure: 𝕊; A[[ ]]; D_{≲}[[ ]]; 𝔸; F[[ ]]; U[[ ]]; ℙ; 𝕋; B[[ ]]]

The annotated intermediate language 𝔸 that we use here is similar to the one for the Cencoding. Of course, the annotations and the operational semantics have to be different in the case of the D-encoding, since they are now expected to model different behavior. Also, since we expect source terms and translations to be bisimilar, we only need a single decoding function.

Annotated divergent choice. Since many (replicated) copies of the same branch may be activated at the same time, we enhance the annotation v to map indices to multisets of values ℕ^{V}. The information whether a choice is resolved can only be inferred from the value of the lock. In case it is held by an activated branch, the choice is not (yet) resolved, since this branch may still decide to undo its activity.

Let J be some indexing set. Let v : J ⇀ ℕ^{V} be a partial function mapping indices to multisets of values and let v +(k, z) and v −(k, z) denote appropriate extensions and removals of single index-value pairs. Let b ∈ {t, f }∪{ (k, z) ∈ J ×V | z ∈ v_{k} } denote either the state of the lock or a single index-value pair. The annotated divergent choice

( ∑_{j∈J} R_{j})_{b}^{v}

is given the operational semantics in Table 6.

Lemma 5.7.1 (Inertness) ( ∑_{j∈J} R_{j})_{f}^{v} ≈ ∏_{j∈V} \overline{y_{j}} v_{j}.

Factorization. The annotation translation is almost the same as in Section 5.3. Here, we have to initialize the lock-information with t.

A[[ ∑_{j∈J} R_{j} ]] =^{def} ( ∑_{j∈J} A[[ R_{j} ]])_{t}^{∅}

[figure]

READ: ( ∑_{j∈J} R_{j})_{b}^{v} \begin{matrix}− \\ − \\ − \end{matrix}^{y_{k}z} → ( ∑_{j∈J} R_{j})_{b}^{v +(k,z)}  if k ∈ J
TRY: ( ∑_{j∈J} R_{j})_{t}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{(k,z)}^{v}  if z ∈ v_{k}

COMMIT: ( ∑_{j∈J} R_{j})_{(k,z)}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{f}^{v −(k,z)} | P_{k}\{^{z}/_{x}\}

UNDO: ( ∑_{j∈J} R_{j})_{(k,z)}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{t}^{v −(k,z)} | \overline{y_{k}}z

ABORT:  ( ∑_{j∈J} R_{j})_{f}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{f}^{v −(k,z)} | \overline{y_{k}}z  if z ∈ v_{k}

Table 6: Transition semantics for annotated divergent choice

The flattening of annotated divergent choice into 𝕋 is

F[[ ( ∑_{j∈J} R_{j})_{B}^{v} ]] =^{def} (l)( T | ∏_{j∈J} ! Read_{l}⟨ F[[ R_{j} ]] ⟩
| ∏_{(j,z)∈V −b} Test_{l}⟨ F[[ R_{j} ]] ⟩{^{z}/_{x}} )
where T =^{def} \begin{cases}( Commit_{l}⟨ R_{k} ⟩ ⊕ Undo_{l}⟨ R_{k} ⟩ )\{^{z}/_{x}\} & if b = (k, z) \\ \overline{l}b & otherwise \end{cases}

Proposition 5.7.2 F is a strong bisimulation. Decoding. The decoding function also takes care of ‘hesitating’ branches.

U[[ ( ∑_{j∈J} R_{j})_{b}^{v} ]] =^{def} ∏_{j∈V} \overline{y_{j}} v_{j} | S
where S =^{def} \begin{cases}∑_{j∈J} U[[ R_{j} ]] & if b = t or b = (k, z) \\ 0 & if b = f \end{cases}

Proposition 5.7.3 U is a weak bisimulation. Theorem 5.7.4 U^{−1}F is a weak bisimulation. Theorem 5.7.5 (Correctness of D) For all S ∈ 𝕊 : S ≈ D[[ S]].

Corollary 5.7.6 (Full abstraction) For all S_{1}, S_{2} ∈ 𝕊 : S_{1} ≈ S_{2} iff D[[ S_{1} ]] ≈ D[[ S_{2} ]].

Every annotated choice term with at least one branch holding some value, has τ-loops, i.e., divergent computations. For example,

( ∑_{j∈J} R_{j})_{t}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{(k,z)}^{v} \begin{matrix}− \\ − \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{t}^{v −(k,z)} | \overline{y_{k}}z \begin{matrix}− \\ − \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{t}^{v}

where z ∈ v_{k}, is infinitely often trying, undoing, reading, …

Finally, if we define D_{≲}[[ ]] as B[[ ]]^{∘} D[[ ]], then by proving that U^{−1}FB^{→} is a weak bisimulation, we also get that D_{≲}[[ ]] is correct and fully abstract with respect to weak bisimulation.

5.8 Divergence

In §4, we have claimed that our two choice encodings differ in their divergence-behavior. Our results in the previous subsections do not yet provide any rigorous justification of this, since the definition of weak simulation ignores divergence, as we discussed in Section 2.3.

As explained in §2.3, an encoding [[ ]] is called divergence-free if it does not add divergence to the behavior of source terms. More technically, every infinite τ-sequence of a derivative T′ of a translation [[ S]] corresponds to some infinite τ-sequence of a derivative S′ of S, i.e., T′⇑ implies S′⇑. Whereas it is simple to show that the D_{≲}-encoding is not divergence-free by giving an example of a τ-loop (which is possible in almost every D-translation for terms containing choices, and carries over to their B-expansions), as we did in the previous section, our claim that the C-encoding is divergence-free requires a proof (cf. Theorem 5.8.2).

We are going to prove the divergence-freedom by establishing an eventually progressing simulation between derivatives of translations and source terms; by this simulation, we capture any reachable state of some translation and are guaranteed that its divergence was not introduced by the encoding, but already present at the source-level.

A good candidate for such a simulation is 𝔖^{−1} since it relates all derivatives of C_{≲}- translations and is itself composed of three eventually progressing simulations.

Proposition 5.8.1 𝔖^{−1} is eventually progressing.

Proof: By 𝔖 =^{def} U_{♭}^{−1}F B^{→}, we have 𝔖^{−1} = (B^{→})^{−1}F^{−1}U_{♭}. Since all of (B^{→})^{−1}, F^{−1}, and U_{♭} are eventually progressing, there composition is also eventually progressing, as proved by simply multiplying the upper bounds for the number of trivial simulation steps of the components. □

Theorem 5.8.2 C_{≲}[[ ]] is divergence-free.

Proof: Since (S, C_{≲}[[ S]]) ∈ 𝔖^{−1} for all S ∈ 𝕊, and 𝔖^{−1} is an eventually progressing simulation by Proposition 5.8.1. □

6 Conclusions

We have investigated two different encodings of the asynchronous π-calculus with inputguarded choice into its choice-free fragment. Several points deserve to be discussed.

Correctness: For both choice encodings, we provided a framework that allowed us to compare source terms and their translations directly. This enabled us to use a correctness notion that is stronger than the usual full abstraction, which here comes up as a simple corollary. The strength of our results may be compared with the notion of representability in [HY94a, HY94b], where it was left as an open problem whether some form of summation could be behaviorally represented by concurrent combinators. Our divergent encoding (for theoretical questions like representability, divergence is acceptable) provides a first positive answer for the representability of input-guarded choice up to weak asynchronous bisimulation. Our results also hold in the setting of value-passing CCS with boolean values and test-expressions. However, in the π-calculus, these additional notions can be encoded by a simple name-passing protocol (as shown in this paper). Furthermore, the results (except for the congruence properties) can be generalized to calculi with polyadic communication, full replication, and matching.

Asynchrony: For both encodings, the correctness proofs cannot be built upon standard (i.e., synchronous) notions of simulation. The reason lies in the inherent asynchrony of the implementation algorithm, which arises from the resending of messages (which must not be kept by a branch when the choice has already committed to a competing branch).

Non-promptness: Most examples of encodings into process calculi known in the literature enjoy the simplifying property of being prompt, i.e., initial transitions of translations are committing, by corresponding to some particular computation step of their source. Both of our choice encodings fall in the class of non-prompt encodings that, moreover, can not be dealt with by optimization with administrative normal forms.

Partial commitments: With respect to the different results for the two choice encodings, it is crucial to notice that only C[[ ]] breaks up the atomicity of committing a choice. The resulting partially committed states are exactly the reason why correctness up to weak bisimulation has to fail, whereas coupled simulation applies successfully.

Divergence: We have not been able to formulate a choice encoding which is divergence-free

and correct with respect to weak bisimulation. We conjecture that it is impossible. Decodings: Any operational correctness proof which states that an encoding is sound in

the sense that each step of a translation is compatible with some source step implicitly uses the idea of mapping back the translation to its source term in order to detect the correspondence. We made this intuition explicit in decoding functions which provide a notation for the proofs that is both compact and intuitive. With prompt encodings, the reconstruction of source terms from target terms is rather simple, since it suffices to deal with literal translations. In contrast, non-prompt encodings require the decoding of derivatives of translations.

Annotations: The only way to detect the origin of derivatives of translations is to retrace their derivation histories. As the underlying semantics, one could, for example, use causality-based techniques, but this would introduce extra technical overhead. Instead, we exploit annotated source terms that precisely capture the information that is necessary to perform the backtracking. An intermediate language built from annotated source terms provides the basis for a sound factorization and a proper setting for the definition of decodings.

According to the soundness interpretation of the correctness results for the A-encoding in §5.4, the operational character of coupled simulation (ℭ, 𝔖) also induces a sharp characterization the operational soundness of the C-encoding: for all source terms S ∈ 𝕊,

[figure: ℙ^{Σ} :; S; a_{1}···a_{n}; 𝔖; ℭ; S′; S′′; ℭ; 𝔖; ℭ; ℙ :; C_{≲}[[ S]]; a_{1}···a_{n}; T; 𝔖; C_{≲}[[ S′′]]]

an arbitrary derivative T of a translation represents an intermediate state in some sourcelevel computation evolving from S′ into S′′. The correspondence between the derivation traces of target C[[ S]] and source S is guaranteed by 𝔖. The relations S′ ≽ T ≽ S′′ hold due to 𝔖 and ℭ, respectively. If T is not partial, then S′ and S′′ coincide.

Related work

The C-encoding represents a striking example where weak bisimulation is too strong a criterion to compare process systems. It is similar to the multiway synchronization example of [PS92]. The latter led to the definition of coupled simulation in order to deal with gradual commitments, which do also appear in the C-encoding. Our encodings differ in that they address the implementation of channel-based choice in the context of an underlying medium supplying asynchronous message-passing; they are thus more closely related to the work of Mitchell [Mit86], Knabe [Kna93], and Busi and Gorrieri [BG95].

In [Mit86], a divergent choice encoding in the rather restricted setting of Static CCS was proved correct with respect to an adapted (‘weak-must’) testing equivalence that accepts divergent implementations (τ^{ω}|P) of P as valid, but that lacks a powerful (e.g. coinductive) proof technique. Here, we have given two asynchronous choice encodings, one of which is divergence-free, and presented a way to prove them correct using asynchronous simulation techniques. Since the original definition of stably coupled simulation equivalence has been shown to imply testing equivalence, we argue that our correctness result for the C-encoding is powerful, even though it is strictly more permissive than weak bisimulation.

The distributed implementation of mixed guarded channel-based choice by Knabe [Kna93] has not been investigated concerning its functional correctness. The emphasis was more on the question of deadlock-freedom; a proof was sketched in [Kna93]. However, the semantics and implementation of this and other choice operators have been studied within the chemical abstract machine framework for the semantics of Facile by Leth and Thomsen [LT95].

In the CCS-setting of Busi and Gorrieri [BG95], choice is replaced by a lower-level notion of conflict that is based on a set of conflict names (and contrasting conames) together with corresponding prefix and restriction operators. An operational semantics keeps track of the set of conflicts that a process must respect as permission for performing actions; an auxiliary kill-operator deals with the proper handling of permissions. The idea is that, in a process P |Q, “if P performs an action, it propagates its effect to Q by killing its conflicting subagents”. Then, the hidden activities that go on in a process like P + Q are modeled explicitly by means of a fully abstract (w.r.t. strong bisimulation) encoding of choice into this calculus. Instead of interpreting P + Q as first resolving the choice, their approach is guided by the idea of a posteriori choice which means that both P and Q may start their activities, and the first that manages to complete its action wins, preventing the other from completion. Some similarities and differences between their approach and ours are clear: whereas we use the primitives of a fragment of the source language by only exploiting the concept of asynchronous communication of private names, their approach needs the additional concept of conflict names. In fact, the choice encodings of the current paper follow the same idea of a posteriori choice as in [BG95]; yet, we go a step further. In our case, concurrent branches in a choice may start their activity by consuming matching messages from the environment that afterwards might have to be given back. Technically, their encoding introduces conflict names for each occurrence of P + Q and restricts that name on the parallel composition of the branches P and Q, ours introduce lock-messages that are accessible within restricted scope and perform the propagation of conflicts via internal communication.

The idea of committing steps, i.e., those target steps which directly correspond to a source-level computation step, is comparable to the notion of principal transition that has been developed for proving the correctness of a compiler from an Occam-like programming language into an assembler language [Gam91]. However, in this setting principal steps could always be chosen as the initial steps. Committing steps have also been recognized by distinguishing real and administrative steps in the non-prompt encoding of Facile [Ama94] and the concurrent λ-calculus [ALT95] into the π-calculus. In both settings, however, preadministrative steps were normalizable, allowing for an optimized prompt encoding, which is not the case in the choice encodings.

Encodings of languages into fragments of themselves have been proposed or investigated by several authors, e.g. by the study of encodings of higher-order-communication into first-order communication within process calculi [San93, Tho93, Ama93], the translation of polyadic into monadic π-calculus [Mil93], the implementation of synchronous via asynchronous message-passing within the choice-free (mini) π-calculus [Bou92], several encodings within a hierarchy of π-calculi with internal mobility [San96], the encoding of the choice-free asynchronous π-calculus into the join-calculus [FG96] (which may be interpreted as a fragment of the π-calculus), and the translation of the choice-free synchronous π-cal-culus into trios [Par99].

Much more work has been done on the compilation of whole languages into process calculi, exploring both semantics and expressiveness. Examples include translations between the process calculi CSP and CCS [Li83, Mil87], between the join-calculus and the π-calculus [FG96], of λ-calculi into process calculi [Mil92, San94b, Lav93, San94a, Tho95, San94b, San95a, ALT95, Ode95b, Nie96], data types and other sequential programming constructs [Mil89, Mil93, Wal91b, Ode95a], from object-oriented languages into process calculi [Vaa90, Wal91a, Wal95, Wal93, Jon93, Wal94, PT95], from logic programming languages into the π-calculus [Ros93, Li94], and from concurrent constraint languages into the π-calculus [Smo94, VP96].

The formalization of compilers for concurrent languages has also motivated the study of encodings, e.g. for Occam [Gam91], Facile [Ama94], Urlang [Gla94], and Pict [PT99]. Further interesting examples report on translations between various notions of rewrite systems [OR94, But94], addressing both semantics and implementation issues.

Future work

The observation that the completeness simulation ℭ and the soundness simulation 𝔖 are progressing and strict, respectively, and both eventually progressing, suggests the study of enhancements of coupled simulation equivalence. The coupled simulation (ℭ, 𝔖) does not constitute an expansion, though, since ℭ and 𝔖 do not coincide. However, it would be straightforward to define the notion of coupled expansion as a mutual simulation exhibiting the coupling as required in Definition 2.4.1 such that one of the component simulations is progressing while the other is strict. Another idea that arises immediately is to enhance coupled simulation with the requirement that the two simulations should be eventually progressing. In fact, (ℭ, 𝔖) is such an eventually progressing coupled simulation as the results in §5 show. Putting all observations together, (ℭ, 𝔖) would satisfy the requirements of an eventually progressing coupled expansion being a coupled expansion where the strict component is also progressing. This preorder would in our case express that (1) source terms and target terms are behaviorally the same, (2) source terms are more efficient than target terms since they use fewer τ-steps, and (3) target terms may only diverge if the corresponding source terms do, and vice versa. We think that equivalence notions along this line deserve further investigation.

Axiomatizations of both weak asynchronous bisimulation and asynchronous coupled simulation are not yet known. Alternative formulations of the definitions of asynchronous bisimulation (see [ACS98], also for an axiomatization in the strong case) might prove convenient for finding modal characterizations and also, in general, for establishing bisimulations.

Endomorphic encodings into a language fragment, like the ones which we investigated in this paper, are easier to deal with than encodings between different languages. This fact relies on the use of a common (labeled) transition semantics for the source and target language which allowed us to directly compare terms and translations in a common formal setting. Furthermore, our choice encodings guaranteed that high-level channels are used in exactly the same way in translations. This not always the case, as even for the tuple encoding into monadic π-calculus channels are used differently in source and target. Barbed bisimulation, which was invented to provide a uniform definitional scheme of term equivalence based on reduction semantics [MS92a, HY95], could be especially useful with respect to encodings between different calculi, since it rests on laxer notions of observation. Also, a barbed definition of coupled simulation, based on reduction semantics, might allow to prove results for encodings which are not fully abstract up to weak bisimulation.

Since the writing of the conference version of this paper, new results have been presented concerning more sophisticated choice operators and their encodings. Palamidessi showed in [Pal97] that it is not possible to give a divergence-free encoding of mixed-guarded choice in a fully distributed way, i.e., where parallel composition and restriction do not add centralizing components that could be used to globally manage the interactions on channels. Nestmann showed in [Nes97] that it is, however, possible to encode separate choice (either purely input-guarded or purely output-guarded) up to Palamidessi’s criteria. Furthermore, the latter contains a discussion on how to relax the criteria for full distribution to get also ‘good’ encodings for mixed choice along the lines of [Kna93]. Full abstraction results are not yet known for these more recent encodings.

Acknowledgments

We are indebted to David N. Turner for the original asynchronous choice encodings in Pict, on which our encoding C[[ ]] is based. Ole Jensen helped us with clarifying intuitions on the nature of coupled simulation. Kohei Honda helped in improving the paper by providing detailed comments on a draft version. Cédric Fournet suggested the proof technique for Lemma 4.3.4. Robin Milner, Davide Sangiorgi, Peter Sewell, and the rest of the Edinburgh/Cambridge Pi Club and the Dienstagsclub at Erlangen joined us in many productive discussions.

A Some Proofs

A.1 F is a strong bisimulation (Proposition 5.3.4)

We show the proof for strong synchronous bisimulation, which implies the asynchronous case; we simply omit the second clause of Definition 2.3.1 and use the first clause also for input transitions. The proof is by structural induction on A ∈ 𝔸 and transition induction on A ⟶ A′. By the simplification discussed in Section 5.1, it suffices to regard the case

A = ( ∑_{j∈J} R_{j})_{B}^{v}

where, according to the rules in Table 5, there are three subcases.

The following proofs are in each case to be read if-and-only-if since the enabling sideconditions for the respective transitions of A and its translation F[[ A]] coincide in each case. Let σ_{j} := {^{v(j)}/_{x}} for all j ∈ V.

case READ In the following J-indexed annotated choice, let k ∈ J\(V ∪B) and let z be transmittable on y_{k} and v′ = v +(k ↦ z). Let b be defined as t if B = ∅, and as f otherwise. Then, we have

( ∑_{j∈J} R_{j})_{B}^{v} \begin{matrix}− \\ − \\ − \end{matrix}^{y_{k}z} → ( ∑_{j∈J} R_{j})_{B}^{v′} and

F[[ ( ∑_{j∈J} R_{j})_{B}^{v} ]]

= (νl)( \overline{l}b |  ∏_{j∈J\(V ∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{j∈V}  Test_{l}⟨ F[[ R_{j} ]] ⟩σ_{j} )
\begin{matrix}− \\ − \\ − \end{matrix}^{y_{k}z} → (νl)( \overline{l}b | ∏_{k ≠ j∈J\(V ∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  Test_{l}⟨ F[[ R_{k}]] ⟩{^{z}/_{x}}
|  ∏_{j∈V}  Test_{l}⟨ F[[ R_{j} ]] ⟩σ_{j} )
≡ (νl)( \overline{l}b |  ∏_{j∈J\(V′∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{j∈V′}  Test_{l}⟨ F[[ R_{j} ]] ⟩σ′_{j} )
= F[[ ( ∑_{j∈J} R_{j})_{B}^{v′} ]]

where σ is extended to σ′ according to v′, yields the proof. case ABORT In every context, for k ∈ V, via rule ABORT, we have

( ∑_{j∈J} R_{j})_{B≠∅}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{B+k}^{v −k} | \overline{y_{k}} v_{k} and

F[[ ( ∑_{j∈J} R_{j})_{B}^{v} ]]

= (νl)( \overline{l}f | ∏_{j∈J\(V ∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{j∈V}  Test_{l}⟨ F[[ R_{j} ]] ⟩σ_{j} )
\begin{matrix}− \\ − \end{matrix}^{τ} → (νl)(  ∏_{j∈J\(V ∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{k ≠ j∈V} Test_{l}⟨ F[[ R_{j} ]] ⟩σ_{j}
|  Abort_{l}⟨ F[[ R_{k}]] ⟩σ_{k} )
≡ (νl)( \overline{l}f | ∏_{j∈J\(V ∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{k≠j∈V} Test_{l}⟨ F[[ R_{j} ]] ⟩σ_{j}
|  \overline{y_{k}} v_{k} )
≡ F[[ ( ∑_{j∈J} R_{j})_{B}^{v} | \overline{y_{k}} v_{k} ]]

which holds since J\(V −k)\(B+k) = J\(V ∪B) and \overline{y_{k}} v_{k} = \overline{y_{k}}xσ_{k}. case COMMIT In every context, for k ∈ V, via rule COMMIT, we have

( ∑_{j∈J} R_{j})_{∅}^{v} \begin{matrix}− \\ − \end{matrix}^{τ} → ( ∑_{j∈J} R_{j})_{\{k\}}^{v −k} | P_{k}σ_{k} and

F[[ ( ∑_{j∈J} R_{j})_{∅}^{v} ]]

= (νl)( \overline{l}t | ∏_{j∈J\(V)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{j∈V}  Test_{l}⟨ F[[ R_{j} ]] ⟩σ_{j} )
\begin{matrix}− \\ − \end{matrix}^{τ} → (νl)(  ∏_{j∈J\(V ∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{k ≠ j∈V} Test_{l}⟨ F[[ R_{j} ]] ⟩σ_{j}
|  Commit_{l}⟨ F[[ R_{k}]] ⟩σ_{k} )
≡ (νl)( \overline{l}t | ∏_{j∈J\(V ∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{k≠j∈V} Test_{l}⟨ F[[ R_{j} ]] ⟩σ_{j}
|  F[[ P_{k}]]σ_{k} )
≡ F[[ ( ∑_{j∈J} R_{j})_{B}^{v} | P_{k}σ_{k} ]]

which holds because of J\(V −k)\(B+k) = J\(V ∪B) and since substitutions satisfy F[[ R_{k}σ_{k}]] = F[[ R_{k}]]σ_{k}. □

A.2 Operational correspondence for the B-encoding (Proposition 5.5.1)

Proof: We know by T = F[[ A]] for some A ∈ 𝔸 that all test-subterms of F[[ A]] are generated as part of some branch in the flattening of an annotated choice. Because of the simplification discussed in Section 5.1, we regard annotated choice terms in isolation.

A = ( ∑_{j∈J} R_{j})_{B}^{v}

Then, the possible occurrences of test-subterms are those given by

T := F[[ A]] = (l)( \overline{l}b | ∏_{j∈J\(V ∪B)} Read_{l}⟨ F[[ R_{j} ]] ⟩
|  ∏_{j∈V}  Test_{l}⟨ F[[ R_{j} ]] ⟩{^{v(j)}/_{x}} )

so the B-encoding will only act nontrivially on them.

The proof is by transition induction, where it suffices to regard the cases where transitions involve test-expressions and their translations since other constructs are mapped homomorphically identical by the B-encoding.

1. Immediate since the above test-expressions are always restricted on their channel l such that they can never show any visible behavior.

2. Straightforward, since we only have to follow the encoding’s idea. Let us emphasize the structure of T by

T = (l)( \overline{l}b | Q | test l then Q_{1} else Q_{2} )

(where the test-expression is the derivative of the particular branch that causes the 𝕋level transition, and Q represents the remaining branches). If the rules TRUE/FALSE are not involved in the derivations, then the simulation by some transition of B[[ T ]] is trivial by the identical inference tree. Otherwise, the transition is of the form

T \begin{matrix}− \\ − \end{matrix}^{τ} → (l)( 0 | Q | Q′_{i} ) =: T′

where Q′_{i} is either the continuation process (i = 1) of the test-ing branch, or the resent message (i = 2), in both cases also providing the message \overline{l}f; we omit the explicit syntax.

In the B-translation, the first action of B[[ T ]] that is necessary in order to simulate the above transition of T has to be on the lock-channel l as becomes clear from the translated term by expanding the 2-adic subterms via the zip-lock encoding:

B[[ T ]] = (l) ( Z[[ l(t, f).\overline{b}]]

| B[[ Q]]

| (t)(f)( Z[[ \overline{l}⟨t, f⟩]] | t.B[[ Q_{1} ]] | f.B[[ Q_{2} ]] ) )

= (l) ( l(u).(v)(\overline{u}v|v(t).(w)(\overline{u}w|w(f).\overline{b}))

| B[[ Q]]

| (t)(f) \begin{matrix}( (u)(\overline{l}u|u(v).(\overline{v}t|u(w).\overline{w}f)) \\ | t.B[[ Q_{1} ]] \\ | f.B[[ Q_{2} ]] ) ) \end{matrix}

\begin{matrix}− \\ − \end{matrix}^{τ} → (l) \begin{aligned}(u) & ( (v)(\overline{u}v|v(t).(w)(\overline{u}w|w(f).\overline{b})) \\ & | B[[ Q]] \\ & | (t)(f) \begin{matrix}( u(v).(\overline{v}t|u(w).\overline{w}f) \\ | t.B[[ Q_{1} ]] \\ | f.B[[ Q_{2} ]] ) ) \end{matrix} \end{aligned}

=: P

where b = t, if b = t, and b = f, otherwise. Note the extrusion of the scope of u, which may now be used as a private communication line between the 2-adic sender and receiver. In the resulting derivative P, the behavior of the ℙ-level subsystem that belongs to the test-expression—i.e., disregarding B[[ Q]]—is completely determined by four subsequent reductions (interactions along u, v, u, and w, where there is always exactly one sender and receiver) for the exchange of the 2-adic message, such that it arrives at

P \begin{matrix}− \\ − \end{matrix}^{τ} →^{4} (l)(t)(f) ( (v)(w)\overline{b}
| B[[ Q]]
| (u)0
| t.B[[ Q_{1} ]]
| f.B[[ Q_{2} ]] ) )
=: P′
≡_{ν} (l)(t)(f) ( \overline{b}
| B[[ Q]]
| t.B[[ Q_{1} ]]
| f.B[[ Q_{2} ]]

where we have done a bit of garbage collection that is possible since the names u, v, and w are no longer used. Finally, after another determinate reduction, depending on the actual value of the 𝕋-level lock-message, we get

P′ ≡ \begin{matrix}− \\ − \end{matrix}^{τ} → \begin{cases}(l)(t)(f)( 0 | B[[ Q]] | B[[ Q_{1} ]] | f.B[[ Q_{2} ]] ) \\ ≡ (l)( B[[ Q]] | B[[ Q_{1} ]] ) & if b = t \\ (l)(t)(f)( 0 | B[[ Q]] | t.B[[ Q_{1} ]] | B[[ Q_{2} ]] ) \\ ≡ (l)( B[[ Q]] | B[[ Q_{2} ]] ) & if b = f \end{cases}

again by garbage-collecting obsolete name restrictions and inaccessible processes.

3. Straightforward, again by distinguishing the possible cases for τ-steps of B[[ T ]]: if the rules TRUE/FALSE are involved in the derivations, then the begun ℙ-level interaction can be simulated at the 𝕋-level since the only test-expressions have come from Teststates of branches in annotated choices. □

References

[ACS98] R. M. Amadio, I. Castellani and D. Sangiorgi. On Bisimulations for the Asynchronous π-Calculus. Theoretical Computer Science, 195(2):291–324, 1998. An extended abstract appeared in Proceedings of CONCUR ’96, LNCS 1119: 147–162.

[AH92] S. Arun-Kumar and M. Hennessy. An Efficiency Preorder for Processes. Acta Informatica, 29:737–760, 1992.

[ALT95] R. M. Amadio, L. Leth and B. Thomsen. From a Concurrent λ-Calculus to the π-Calculus. In H. Reichel, ed, Proceedings of FCT ’95, volume 965 of LNCS, pages 106–115. Springer, 1995. Full version as Technical Report ECRC-95-18.

[Ama93] R. M. Amadio. On the reduction of CHOCS bisimulation to π-calculus bisimulation. In E. Best, ed, Proceedings of CONCUR ’93, volume 715 of LNCS, pages 112–126. Springer, 1993. Extended version as Rapport de Recherche, INRIA-Lorraine, 1993.

[Ama94] R. M. Amadio. Translating Core Facile. Technical Report ECRC-94-3, European Computer-Industry Research Centre, München, Feb. 1994.

[BG95] N. Busi and R. Gorrieri. Distributed Conflicts in Communicating Systems. In P. Ciancarini, O. Nierstrasz and A. Yonezawa, eds, Object-Based Models and Languages for Concurrent Systems, volume 924 of LNCS, pages 49–65. Springer, 1995.

[Bou92] G. Boudol. Asynchrony and the π-calculus (Note). Rapport de Recherche 1702, INRIA Sophia-Antipolis, May 1992.

[But94] K.-H. Buth. Simulation of SOS Definitions with Term Rewriting Systems. In D. Sannella, ed, Proceedings of ESOP ’94, volume 788 of LNCS, pages 150–164. Springer, 1994.

[FG96] C. Fournet and G. Gonthier. The Reflexive Chemical Abstract Machine and the Join-Calculus. In J. G. Steele, ed, Proceedings of POPL ’96, pages 372–385. ACM, Jan. 1996.

[Gam91] A. Gammelgaard. Constructing Simulations Chunk by Chunk. Internal Report DAIMI IR-106, Computer Science Department, Aarhus University, Dec. 1991. Part of the authors’ PhD Thesis Simulation Techniques, available as Report DAIMI PB-379.

[Gla93] R. Glabbeek. The Linear Time – Branching Time Spectrum II: The semantics of sequential systems with silent moves (Extended Abstract). In E. Best, ed, Proceedings of CONCUR ’93, volume 715 of LNCS, pages 66–81. Springer, 1993.

[Gla94] D. Gladstein. Compiler Correctness for Concurrent Languages. PhD thesis, Northeastern University, Dec. 1994.

[Hon92] K. Honda. Two Bisimilarities in ν-Calculus. CS report 92-002, Keio University, 1992. Revised on March 31, 1993.

[HT91] K. Honda and M. Tokoro. An Object Calculus for Asynchronous Communication. In P. America, ed, Proceedings of ECOOP ’91, volume 512 of LNCS, pages 133–147. Springer, July 1991.

[HT92] K. Honda and M. Tokoro. On Asynchronous Communication Semantics. In M. Tokoro, O. Nierstrasz and P. Wegner, eds, Object-Based Concurrent Computing 1991, volume 612 of LNCS, pages 21–51. Springer, 1992.

[HY94a] K. Honda and N. Yoshida. Combinatory Representation of Mobile Processes. In Proceedings of POPL ’94, pages 348–360. ACM, January 1994.

[HY94b] K. Honda and N. Yoshida. Replication in Concurrent Combinators. In M. Hagiya and J. C. Mitchell, eds, Proceedings of TACS ’94, volume 789 of LNCS, pages 786–805. Springer, 1994.

[HY95] K. Honda and N. Yoshida. On Reduction-Based Process Semantics. Theoretical Computer Science, 152(2):437–486, 1995. An extract appeared in Proceedings of FSTTCS ’93, LNCS 761.

[Jon93] C. Jones. A Pi-Calculus Semantics for an Object-Based Design Notation. In E. Best, ed, Proceedings of CONCUR ’93, volume 715 of LNCS, pages 158–172. Springer, 1993.

[Kna93] F. Knabe. A Distributed Protocol for Channel-Based Communication with Choice. Computers and Artificial Intelligence, 12(5):475–490, 1993.

[Lav93] C. Lavatelli. Non-deterministic Lazy λ-calculus vs. π-calculus. Technical Report LIENS-93-15, Ecole Normale Supérieure, Paris, Sept. 1993.

[Li83] W. Li. An Operational Approach to Semantics and Translation for Concurrent Programming Languages. PhD thesis, LFCS, University of Edinburgh, Jan. 1983. Report CST-20-83.

[Li94] B. Z. Li. A π-Calculus Specification of Prolog. In D. Sannella, ed, Proceedings of ESOP ’94, volume 788 of LNCS, pages 379–393. Springer, 1994.

[LT95] L. Leth and B. Thomsen. Some Facile Chemistry. Formal Aspects of Computing, 7(3):314– 328, 1995. A Previous Version appeared as ECRC-Report ECRC-92-14.

[Mil87] M. Millington. Theories of Translation Correctness for Concurrent Programming Languages. PhD thesis, LFCS, University of Edinburgh, Aug. 1987. Report CST-46-87.

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

[Mil92] R. Milner. Functions as Processes. Journal of Mathematical Structures in Computer Science, 2(2):119–141, 1992. Previous version as Rapport de Recherche 1154, INRIA Sophia-Antipolis, 1990, and in Proceedings of ICALP ’91, LNCS 443.

[Mil93] R. Milner. The Polyadic π-Calculus: A Tutorial. In F. L. Bauer, W. Brauer and H. Schwichtenberg, eds, Logic and Algebra of Specification, volume 94 of Series F: Computer and System Sciences. NATO Advanced Study Institute, Springer, 1993. Available as Technical Report ECS-LFCS-91-180, University of Edinburgh, October 1991.

[Mit86] K. Mitchell. Implementations of Process Synchronisation and their Analysis. PhD thesis, LFCS, University of Edinburgh, July 1986.

[MP95] U. Montanari and M. Pistore. Concurrent Semantics for the π-calculus. In S. Brookes, M. Main, A. Melton and M. Mislove, eds, Proceedings of MFPS ’95, volume 1 of ENTCS. Elsevier Science Publishers, 1995.

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

[MS92a] R. Milner and D. Sangiorgi. Barbed Bisimulation. In W. Kuich, ed, Proceedings of ICALP ’92, volume 623 of LNCS, pages 685–695. Springer, 1992.

[MS92b] U. Montanari and V. Sassone. Dynamic Congruence vs. Progressing Bisimulation for CCS. Fundamenta Informaticae, XVI(2):171–199, 1992.

[Nes96] U. Nestmann. On Determinacy and Nondeterminacy in Concurrent Programming. PhD thesis, Technische Fakultät, Universität Erlangen, November 1996. Arbeitsbericht IMMD-29(14).

[Nes97] U. Nestmann. What Is a ‘Good’ Encoding of Guarded Choice? In C. Palamidessi and J. Parrow, eds, Proceedings of EXPRESS ’97, volume 7 of ENTCS. Elsevier Science Publishers, 1997. Latest full version as report BRICS-RS-99-43, Universities of Aalborg and Århus, Denmark, 1999. To appear in Journal of Information and Computation.

[Nie96] J. Niehren. Functional Computation as Concurrent Computation. In J. G. Steele, ed, Proceedings of POPL ’96, pages 333–343. ACM, Jan. 1996. Full version as Research Report RR-95-14, DFKI Saarbrücken.

[Ode95a] M. Odersky. Applying π: Towards a Basis for Concurrent Imperative Programming. In U. S. Reddy, ed, Proceedings of SIPL ’95, pages 95–108. ACM/SIGPLAN, University of Illinois at Urbana-Champaign, January 22 1995. Available as Technical Report UIUCDCS-R-95-1900.

[Ode95b] M. Odersky. Polarized Name Passing. In P. S. Thiagarajan, ed, Proceedings of FSTTCS ’95, volume 1026 of LNCS, pages 324–337. Springer, 1995.

[OR94] V. Oostrom and F. Raamsdonk. Comparing Combinatory Reduction Systems and Higher-Order Rewrite Systems. In J. Heering, K. Meinke, B. Möller and T. Nipkow, eds, Proceedings of HOA ’93, volume 816 of LNCS, pages 276–304. Springer, 1994.

[Pal97] C. Palamidessi. Comparing the Expressive Power of the Synchronous and the Asynchronous π-calculus. In Proceedings of POPL ’97, pages 256–265. ACM, Jan. 1997.

[Par99] J. Parrow. Trios in Concert. In G. Plotkin, C. Stirling and M. Tofte, eds, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1999. To appear.

[Pri78] L. Priese. On the Concept of Simulation in Asynchronous, Concurrent Systems. In Progress in Cybernetics and Systems Research, volume VII, pages 85–92. Hemisphere Dubl. Corp., 1978. Proceedings of EMCSR (1978, Linz, Österreich).

[PS92] J. Parrow and P. Sjödin. Multiway Synchronization Verified with Coupled Simulation. In R. Cleaveland, ed, Proceedings of CONCUR ’92, volume 630 of LNCS, pages 518–533. Springer, 1992.

[PS94] J. Parrow and P. Sjödin. The Complete Axiomatization of cs-Congruence. In P. Enjalbert, E. W. Mayr and K. W. Wagner, eds, Proceedings of STACS ’94, volume 775 of LNCS, pages 557–568. Springer, 1994.

[PT95] B. C. Pierce and D. N. Turner. Concurrent Objects in a Process Calculus. In T. Ito and A. Yonezawa, eds, Proceedings of TPPP ’94, volume 907 of LNCS, pages 187–215. Springer, 1995.

[PT99] B. C. Pierce and D. N. Turner. Pict: A Programming Language Based on the Pi-Calculus. In G. Plotkin, C. Stirling and M. Tofte, eds, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1999. To appear.

[Ros93] B. Ross. A π-calculus semantics of logical variables and unification. In S. Purushothaman and A. Zwarico, eds, Proceedings of First North American Process Algebra Workshop, Stony Brook, 1992, Workshops in Computing, pages 216–230. Springer, 1993.

[San93] D. Sangiorgi. From π-calculus to Higher-Order π-calculus — and back. In M.-C. Gaudel and J.-P. Jouannaud, eds, Proceedings of TAPSOFT ’93, volume 668 of LNCS, pages 151–166. Springer, 1993.

[San94a] D. Sangiorgi. An investigation into functions as processes. In S. Brookes, M. Main, A. Melton and D. Schmidt, eds, Proceedings of MFPS ’93, volume 802 of LNCS, pages 143–159. Springer, 1994.

[San94b] D. Sangiorgi. The Lazy Lambda Calculus in a Concurrency Scenario. Information and Computation, 111(1):120–131, 1994. An extended abstract appeared in Proceedings of LICS ’92.

[San95a] D. Sangiorgi. Lazy functions and mobile processes. Rapport de Recherche RR-2515, INRIA Sophia-Antipolis, 1995.

[San95b] D. Sangiorgi. On the Bisimulation Proof Method. In J. Wiedemann and P. Hájek, eds, Proceedings of MFCS ’95, volume 969 of LNCS, pages 479–488. Springer, 1995.

[San96] D. Sangiorgi. π-Calculus, Internal Mobility and Agent-Passing Calculi. Theoretical Computer Science, 167(1,2):235–274, 1996. Also as Rapport de Recherche RR-2539, INRIA Sophia-Antipolis, 1995. Extracts of parts of the material contained in this paper can be found in Proceedings of TAPSOFT ’95 and ICALP ’95.

[Smo94] G. Smolka. A Foundation for Higher-Order Concurrent Constraint Programming. In J.-P. Jouannaud, ed, Proceedings 1st International Conference of Constraints in Computational Logics, volume 845 of LNCS, pages 50–72. Springer, 1994. Available as Research Report RR-94-16 from DFKI Kaiserslautern.

[Tho93] B. Thomsen. Plain CHOCS. A Second Generation Calculus for Higher Order Processes. Acta Informatica, 30(1):1–59, 1993.

[Tho95] B. Thomsen. A Theory of Higher Order Communicating Systems. Information and Computation, 116(1):38–57, 1995.

[Vaa90] F. Vaandrager. Process Algebra Semantics of POOL. In J. Baeten, ed, Application of Process Algebra, pages 173–236. Cambridge University Press, 1990. Earlier version: CWI-Report CS-R8629.

[VP96] B. Victor and J. Parrow. Constraints as Processes. In U. Montanari and V. Sassone, eds, Proceedings of CONCUR ’96, volume 1119 of LNCS, pages 389–405. Springer, 1996.

[Wal90] D. Walker. Bisimulation and Divergence. Information and Computation, 85(2):202–241, 1990. An extended abstract appeared in the Proceedings of LICS’ 88.

[Wal91a] D. Walker. π-calculus Semantics of Object-Oriented Programming Languages. In T. Ito and A. Meyer, eds, Proceedings of TACS ’91, volume 526 of LNCS, pages 532–547. Springer, 1991. Available as Report ECS-LFCS-90-122, University of Edinburgh.

[Wal91b] D. Walker. Some Results on the π-Calculus. In A. Yonezawa and T. Ito, eds, Concurrency: Theory, Languages, and Architecture, volume 491 of LNCS, pages 21–35. Springer, 1991.

[Wal93] D. Walker. Process Calculus and Parallel Object-Oriented Programming Languages. In P. Tvrdik, T. Casavant and F. Plasil, eds, Parallel Computers: Theory and Practice, pages 369–390. Computer Society Press, 1993. Available as Research Report CS-RR-242, Department of Computer Science, University of Warwick.

[Wal94] D. Walker. Algebraic Proofs of Properties of Objects. In D. Sannella, ed, Proceedings of ESOP ’94, volume 788 of LNCS, pages 501–516. Springer, 1994.

[Wal95] D. Walker. Objects in the π-calculus. Information and Computation, 116(2):253–271, 1995.

Recent BRICS Report Series Publications

RS-99-42 Uwe Nestmann and Benjamin C. Pierce. Decoding Choice Encodings. December 1999. ii+62 pp. To appear in Journal of Information and Computation. An extended abstract appeared in Montanari and Sassone, editors, Concurrency Theory: 7th International Conference, CONCUR ’96 Proceedings, LNCS 1119, 1996, pages 179–194.

RS-99-41 Nicky O. Bodentien, Jacob Vestergaard, Jakob Friis, Kåre J. Kristoffersen, and Kim G. Larsen. Verification of State/Event Systems by Quotienting. December 1999. 17 pp. Presented at Nordic Workshop in Programming Theory, Uppsala, Sweden, October 6–8, 1999.

RS-99-40 Bernd Grobauer and Zhe Yang. The Second Futamura Projection for Type-Directed Partial Evaluation. November 1999. Extended version of an article to appear in Lawall, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’00 Proceedings, 2000.

RS-99-39 Romeo Rizzi. On the Steiner Tree \frac{3}{2}-Approximation for Quasi-Bipartite Graphs. November 1999. 6 pp.

RS-99-38 Romeo Rizzi. Linear Time Recognition of P_{4}-Indifferent Graphs. November 1999. 11 pp.

RS-99-37 Tibor Jordán. Constrained Edge-Splitting Problems. November 1999. 23 pp. A preliminary version with the title Edge-Splitting Problems with Demands appeared in Cornujols, Burkard and Wöginger, editors, Integer Programming and Combinatorial Optimization: 7th International Conference, IPCO ’99 Proceedings, LNCS 1610, 1999, pages 273–288.

RS-99-36 Gian Luca Cattani and Glynn Winskel. Presheaf Models for CCS-like Languages. November 1999. ii+46 pp.

RS-99-35 Tibor Jordán and Zoltán Szigeti. Detachments Preserving Local Edge-Connectivity of Graphs. November 1999. 16 pp.

RS-99-34 Flemming Friche Rodler. Wavelet Based 3D Compression for Very Large Volume Data Supporting Fast Random Access. October 1999. 36 pp.