# Reversibility in the higher-order π-calculus

Ivan Lanese, Claudio Antares Mezzina, Jean-Bernard Stefani

► To cite this version:

Ivan Lanese, Claudio Antares Mezzina, Jean-Bernard Stefani. Reversibility in the higher-order π-calculus. Theoretical Computer Science, 2016, 625, pp.25-84. 10.1016/j.tcs.2016.02.019. hal-01303090

HAL Id: hal-01303090

https://inria.hal.science/hal-01303090

Submitted on 15 Apr 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
Reversibility in the higher-order π-calculus

Ivan Lanese$^{a,1}$, Claudio Antares Mezzina$^b$, Jean-Bernard Stefani$^{c,2,1}$

$^a$Focus Team, University of Bologna/INRIA, Italy

$^b$IMT Institute for Advanced Studies Lucca, Italy

$^c$INRIA, France

**Abstract**

The notion of reversible computation is attracting increasing interest because of its applications in diverse fields, in particular the study of programming abstractions for reliable systems. In this paper, we continue the study undertaken by Danos and Krivine on reversible CCS by defining a reversible higher-order π-calculus, called rhoπ. We prove that reversibility in our calculus is causally consistent and that the causal information used to support reversibility in rhoπ is consistent with the one used in the causal semantics of the π-calculus developed by Boreale and Sangiorgi. Finally, we show that one can faithfully encode rhoπ into a variant of higher-order π, substantially improving on the result we obtained in the conference version of this paper.

*Keywords:* reversible computation, process algebra, π-calculus

# 1. Introduction

*Motivation.* The notion of reversible computation has already a long history [1]. It has its origin in physics with the observation by Landauer that only irreversible computations need to consume energy [2]. It has since attracted interest in diverse fields, including e.g. hardware design [3], computational biology [4], program debugging [5], and quantum computing [6]. Of particular interest is its application to the study of programming abstractions for reliable systems. For instance, Bishop advocates using reversible computing as a means to achieve *fail-safety* in a sequential setting [7]. Moreover,

<footnote n="1">¹Partly funded by the ANR-11-INSE-007 project REVER.</footnote>

<footnote n="2">²Partly funded by the ANR-2010-BLAN-0305-01 project PiCoq.</footnote>
most fault-tolerant schemes exploiting system recovery techniques [8], includ-
ing exception handling [9], checkpoint/rollback [10] and transaction manage-
ment [11], rely on some form of *undo* or another. All this suggests it can be
worthwhile to formally investigate reversibility in concurrent systems, with
the hope that reversible computing ideas can lead us to more systematic and
more composable abstractions for the design and construction of recoverable
systems.

The seminal work of Danos and Krivine on reversible CCS (RCCS) con-
stitutes a first step on this research programme. They develop in [12] a
basic reversible concurrent programming model in the form of a reversible
variant of CCS, and introduce the notion of *causal consistency* as the least
constraining correctness criterion for reversing a concurrent system. Requir-
ing a concurrent system to go back in a computation by undoing actions in
the inverse order with respect to the one described by its interleaving se-
mantics for the forward computation is too restrictive, since forward actions
could have executed concurrently. Causality constraints should be respected,
however: first the consequences have to be undone, then the causes. Causal
consistency captures exactly this: when reversing a computation, actions are
undone in reverse order up to causal equivalence, i.e. up to swaps of con-
current actions. In [13] Danos and Krivine show how to leverage RCCS for
the design of transactional systems. They provide an interpretation of dis-
tributed transactions as “ballistic” processes, that freely explore the state
space defined by their reversible part until they commit by performing irre-
versible actions, and they show how reversibility can help in the design and
proof of correctness of complex transactional systems. Later on, Phillips and
Ulidowski [14] showed how to devise causally consistent reversible extensions
for process calculi specified by SOS rules in a subset of the path format.

A reversible CCS, or a process calculus defined by operators in the path
format, remains limited as a reversible programming model, however. The
same reasons that motivated the introduction of the π-calculus [15] apply to
motivate the study of a reversible π-calculus. As a first contribution in that
study, we introduced in [16] a causally-consistent reversible extension of an
asynchronous variant of the higher-order π-calculus [17], where we showed
how to preserve the usual properties of the π-calculus operators (e.g., as-
sociativity and commutativity of parallel composition), and that one could
faithfully encode (up to weak barbed bisimilarity) our reversible higher-order
π, called rhoπ, into a variant of the higher-order π-calculus with abstractions
and join patterns. The operational semantics of rhoπ was given in [16] by
way of a reduction semantics. We then showed how to leverage the reversible
machinery in rhoπ for a calculus with explicit rollback [18] called rollπ, and
further, building on rollπ, how to faithfully encode certain kinds of com-
municating transactions [19]. Very recently, Cristescu, Krivine and Varacca
have proposed in [20] a reversible π-calculus, called Rπ, and defined a la-
belled transition system semantics for it. In addition, they showed their LTS
semantics for Rπ to be as liberal as possible in the sense that the causality
relation between labelled transitions is the smallest relation that is consistent
with the structural causality between reductions.

*Contributions.* In this paper, we revisit our work on rhoπ. Apart from providing proofs that where omitted from [16] for lack of space, we discuss in more detail notions of barbed bisimilarity for rhoπ, and we study the relationship between the notion of causality that emerges from our reversibility machinery and that introduced by Boreale and Sangiorgi in their causal π-calculus [21]. Our discussion of barbed bisimilarity shows that the usual notion of weak barbed bisimilarity, not distinguishing between forward and backward reductions, is very coarse in rhoπ since it identifies processes that have the same weak observables. Weak barbed bisimilarity remains a non-trivial relation since the question of knowing whether two rhoπ processes have the same weak observables is undecidable. However, since it was used to show the faithfulness of our encoding of rhoπ in higher-order π, one can wonder whether the result would still hold with a finer bisimilarity, in particular one that could distinguish between forward and backward reductions. We show in this paper that this is indeed the case, at the cost of minor tweaks in our encoding, and at the expense of a much more complex proof.

*Outline.* The paper is organized as follows. Section 2 defines the rhoπ calculus. We explain the main constructions of the calculus and we contrast our way of handling reversibility with that of Danos and Krivine. We also define and discuss barbed equivalences in rhoπ. Section 3 is devoted to the proof of our first main result, namely that reversibility in rhoπ proceeds in a causally consistent way. We also show that the notion of causality built in the rhoπ operational semantics agrees with that of Boreale and Sangiorgi. Section 4 presents a compositional encoding of the rhoπ calculus into a variant of HOπ and proves its faithfulness. Section 5 discusses related work. Section 6 concludes the paper. Main proofs and auxiliary results are collected in Appendix.
This paper constitutes a revised and extended version of our conference paper [16]. While the rhoπ calculus and its reversible machinery are unchanged, the analysis in Section 3 of the relationship between our notion of causality and that provided by Boreale and Sangiorgi for the π-calculus is new. The material in Section 4, which makes up the bulk of the paper, is also entirely new.

## 2. The rhoπ calculus

### 2.1. Informal presentation

Building a reversible variant of a process calculus involves devising appropriate syntactic representations for computation histories. As already hinted at in the Introduction, since a process models a concurrent system, asking for a deterministic reverse execution, which traverses the exact same states of the forward execution, is too restrictive. In fact, those states depend on the chosen interleaving of concurrent actions. An approach more suitable for a concurrent system is *causally consistent reversibility*, where states that are reached during a backward computation are states that could have been reached during the computation history by just performing independent actions in a different order. In RCCS [12], Danos and Krivine achieve this with CCS without recursion (an extension dealing with recursion is presented in [57]) by attaching a memory *m* to each process *P*, in the monitored process construct *m* : *P*. A memory in RCCS is a stack of information needed for processes to backtrack. Thus, if two processes *P*₁ and *P*₂ can synchronize on a channel *a* in order to evolve into *P*'₁ and *P*'₂, respectively, (e.g., *P*₁ = *a*·*P*'₁ and *P*₂ = *a*·*P*'₂) then the parallel composition of monitored processes *m*₁ : (*P*₁ + *Q*₁) and *m*₂ : (*P*₂ + *Q*₂) can evolve, according to RCCS semantics, as follows:

$$m_1 : (P_1 + Q_1) \mid m_2 : (P_2 + Q_2) \rightarrow \langle m_2, a, Q_1 \rangle \cdot m_1 : P'_1 \mid \langle m_1, \bar{a}, Q_2 \rangle \cdot m_2 : P'_2$$

In the reduction above, a memory of the form $\langle m_2, a, Q_1 \rangle \cdot m_1$ represents the fact that its monitored process has performed an input on the channel *a* ($\bar{a}$ represents an output), interacting with a process monitored by the memory *m*₂, and discarded the alternative process *Q*₁. By exploiting all the information stored in the memories, the above synchronization can be reverted as follows:

$$\langle m_2, a, Q_1 \rangle \cdot m_1 : P'_1 \mid \langle m_1, \bar{a}, Q_2 \rangle \cdot m_2 : P'_2 \rightarrow m_1 : (P_1 + Q_1) \mid m_2 : (P_2 + Q_2)$$
Additionally, Danos and Krivine rely on the following rule:

$$m : (P | Q) \equiv \langle 1 \rangle \cdot m : P | \langle 2 \rangle \cdot m : Q$$

so as to ensure that each primitive thread, i.e. some process with no parallel composition at top level, gets its own unique identity. Since this rule stores the exact position of a process in a parallel composition, it is not compatible with the usual structural congruence rules for the parallel operator, namely associativity, commutativity, and 0 as neutral element. Danos and Krivine suggest that it could be possible to work up to tree isomorphisms on memories, but this would indeed lead to a more complex syntax, as well as additional difficulties (see Remark 5).

We adopt for rhoπ a different approach: instead of associating each thread with a stack that records, essentially, past actions and positions in parallel branches, we rely on simple thread tags, which act as unique identifiers but have little structure, and on new process terms, which we call memories, which are dedicated to undoing a single (forward) computation step.

More precisely, a forward computation step in rhoπ (denoted by arrow →) consists in the receipt of a message (rhoπ is an asynchronous calculus). The receipt of a message a(P) on channel a by a receiver process (or trigger) a(X) ▷ Q takes in rhoπ the following form:

$$(\kappa_1 : a(P)) | (\kappa_2 : a(X) \triangleright Q) \rightarrow \nu k. k : Q^{P/X} | [M; k]$$

Each thread (message and trigger) participating in the above computation step is uniquely identified by a tag: $\kappa_1$ identifies the message $a(P)$, and $\kappa_2$ identifies the trigger $a(X) \triangleright Q$. The result of the message receipt consists in a classical part and two side effects. The classical part is the launch of an instance $Q^{P/X}$ of the body of the trigger $Q$, with the formal parameter $X$ instantiated by the received value, i.e. the process $P$ (rhoπ is a higher-order calculus). The two side effects are: (i) the tagging of the newly created process $Q^{P/X}$ by a fresh new key $k$ ($\nu$ is the standard restriction operator of the π-calculus), and (ii) the creation of a memory process $[M; k]$. $M$ is simply the configuration on the left hand side of the reduction, namely $M = (\kappa_1 : a(P)) | (\kappa_2 : a(X) \triangleright Q)$.

In this setting, a backward computation step takes the form of an interaction between a memory and a process tagged with the appropriate key: when a memory $[M; k]$ is put in presence of a process tagged with $k$, a backward reduction (denoted by arrow ↪→) can take place. Such a reduction kills the
process tagged with $k$ and reinstates the configuration $M$:

$$ (k : P) \mid [M; k] \rightsquigarrow M $$

We thus have:

$$ M \to \nu k. k : Q^{\{P\}/X} \mid [M; k] \rightsquigarrow \nu k. M $$

Since $k$ is fresh, $\nu k. M$ is actually structurally equivalent to $M$. We thus have a perfect reversal of a forward computation: $M \to \rightsquigarrow M$.

**Remark 1.** Following Danos and Krivine [13], one could consider also taking into account *irreversible actions*. We do not do so in this paper for the sake of simplicity. Adding irreversible actions to $\rho\!\!\rho\pi$ would be conceptually straightforward.

**Remark 2.** Using memories as presented here to enable reversibility simplifies the formal development but leads to a space explosion of computations in $\rho\!\!\rho\pi$. We do not consider implementation and related space efficiency issues in this paper. This issue has been analysed in [22] in the context of the Oz language.

## 2.2. Syntax

*Names, keys, and variables.* We assume the existence of the following denumerable infinite mutually disjoint sets: the set $\mathcal{N}$ of names, the set $\mathcal{K}$ of keys, and the set $\mathcal{V}$ of process variables. The set $\mathcal{I} = \mathcal{N} \cup \mathcal{K}$ is called the set of identifiers. $\mathbb{N}$ denotes the set of natural integers. We let (together with their decorated, e.g. primed or indexed, variants): $a, b, c$ range over $\mathcal{N}$; $h, k, l$ range over $\mathcal{K}$; $u, v, w$ range over $\mathcal{I}$; $X, Y, Z$ range over $\mathcal{V}$. We denote by $\tilde{u}$ a finite set of identifiers $\{u_1, \dots, u_n\}$.

*Syntax.* The syntax of the $\rho\!\!\rho\pi$ calculus is given in Figure 1 (in writing $\rho\!\!\rho\pi$ terms, we freely add balanced parenthesis around terms to disambiguate them). *Processes* of the $\rho\!\!\rho\pi$ calculus, given by the $P, Q$ productions in Figure 1, are the standard processes of the asynchronous higher-order $\pi$-calculus [23]. A receiver process (or *trigger*) in $\rho\!\!\rho\pi$ takes the form $a(X) \triangleright P$, which allows the receipt of a message of the form $a\langle Q \rangle$ on channel $a$.

We call *primitive thread process*, a process that is either a message $a\langle P \rangle$ or a trigger $a(X) \triangleright P$. We let $\tau$ and its decorated variants (e.g., $\tau_1, \tau'$ and so on) range over primitive thread processes.
$$
\begin{align*}
P, Q &::= \mathbf{0} \mid X \mid \nu a. P \mid (P \mid Q) \mid a \langle P \rangle \mid a(X) \triangleright P \\
M, N &::= \mathbf{0} \mid \nu u. M \mid (M \mid N) \mid \kappa : P \mid [\mu; k] \\
\kappa &::= k \mid \langle h, \tilde{h} \rangle \cdot k \\
\mu &::= ((\kappa_1 : a \langle P \rangle) \mid (\kappa_2 : a(X) \triangleright Q)) \\
u \in \mathcal{I} \quad a \in \mathcal{N} \quad X \in \mathcal{V} \quad h, k \in \mathcal{K} \quad \kappa \in \mathcal{T}
\end{align*}
$$

<caption>Figure 1: Syntax of rhoπ</caption>

Processes in rhoπ cannot directly execute, only *configurations* can. *Configurations* in rhoπ are given by the *M*, *N* productions in Figure 1. A configuration is built up from *threads* and *memories*.

A thread $\kappa : P$ is just a tagged process $P$, where the tag $\kappa$ is either a single key $k$ or a pair of the form $\langle h, \tilde{h} \rangle \cdot k$, where $\tilde{h}$ is a set of keys, with $h \in \tilde{h}$. A tag serves as an identifier for a process. A tag $\langle h, \tilde{h} \rangle \cdot k$ brings the information that a process with key $k$ has been splitted into primitive thread processes, where $h$ identifies the particular primitive thread process and $\tilde{h}$ allows one to recover the other primitive thread processes created by the split. Indeed, all these primitive thread processes have tags of the form $\langle h_i, \tilde{h} \rangle \cdot k$ for different $h_i \in \tilde{h}$.

As we will see below, together with memories tags help capture the flow of causality in a computation.

A *memory* is a process of the form $[\mu; k]$, which keeps track of the fact that a configuration $\mu$ was reached during execution, that triggered the launch of a thread tagged with the fresh tag $k$. In a memory $[\mu; k]$, we call $\mu$ the *configuration part* of the memory, and $k$ the *thread tag* of the memory. Memories are generated by computation steps and are used to reverse them. The configuration part $\mu = (\kappa_1 : a\langle P \rangle) \mid (\kappa_2 : a(X) \triangleright Q)$ of the memory records the message $a\langle P \rangle$ and the trigger $a(X) \triangleright Q$ involved in the message receipt, together with their respective thread tags $\kappa_1, \kappa_2$.

$\mathcal{P}$ denotes the set of rho$\pi$ processes, and $\mathcal{C}$ the set of rho$\pi$ configurations.
We call *agent* an element of the set $\mathcal{A} = \mathcal{P} \cup \mathcal{C}$. We let (together with their
decorated variants) $P, Q, R$ range over $\mathcal{P}$; $L, M, N$ range over $\mathcal{C}$; and $A, B, C$
range over agents.

**Remark 3.** We have no construct for replicated processes, output prefixing, or guarded choice in rho$\pi$: as in the asynchronous HO$\pi$, also in rho$\pi$ these can be easily encoded.
*Free names and free variables.* Notions of free identifiers and free (process) variables in rhoπ are classical. It suffices to note that constructs with binders are of the forms: νa. P, which binds the name a with scope P; νu. M, which binds the identifier u with scope M; and a(X)▷P, which binds the variable X with scope P. We denote by fn(P), fn(M) and fn(κ) the set of free names, free identifiers, and free keys, respectively, of process P, of configuration M, and of tag κ. Note in particular that fn(κ : P) = fn(κ) ∪ fn(P), fn(k) = {k} and fn(⟨h, ˜h⟩ · k) = ˜h ∪ {k}. We say that a process P or a configuration M is closed if it has no free (process) variable. P• denotes the set of closed processes, C• the set of closed configurations, and A• the set of closed agents.

**Remark 4.** In the remainder of the paper, we adopt Barendregt’s *Variable Con- vention*: If terms $t_1, \dots, t_n$ occur in a certain context (e.g. definition, proof), then in these terms all bound identifiers and variables are chosen to be different from the free ones.

*Initial and consistent configurations.* Not all configurations allowed by the syntax in Figure 3 are meaningful. For instance, in a memory [μ; k], tags occurring in the configuration part μ must be different from the key k. Thus, in the following we concentrate on *consistent configurations*, defined below. We will show later on that consistent configurations indeed satisfy the syntactic property above and other relevant structural properties.

**Definition 1 (Initial and consistent configurations).**

A configuration is *initial* if it does not contain memories and all tags are distinct and simple (i.e., of the form *k*). A configuration is *consistent* if it can be derived using the rules of the calculus from an initial configuration.

## 2.3. Operational semantics

The operational semantics of the rhoπ calculus is defined via a reduction relation $→$, which is a binary relation over closed configurations $→ ⊂ C• × C•$, and a structural congruence relation $≡$, which is a binary relation over processes and configurations $≡ ⊂ P² ∪ C²$.

**Definition 2 (Contexts).** We define *configuration contexts*, also called evaluation contexts, as “configurations with one hole ·” given by the following grammar:

$$ \mathbb{E} ::= \cdot \mid (M \mid \mathbb{E}) \mid \nu u. \mathbb{E} $$
<figure><img src="image_1.png" /><figcaption>Figure 2: Structural congruence for rhoπ</figcaption></figure>

General contexts $\mathbb{C}$ are “processes or configurations with one hole .”, and are obtained from processes or configurations by replacing one occurrence of $\mathbf{0}$ (either as process or as configuration) with $\cdot$.

In general contexts, the hole may represent either a process or a configuration. Also, the term obtained by replacing the hole with the corresponding syntactic category (process or configuration) may be either a process or a configuration. General contexts where the hole stands for a configuration correspond to configuration contexts. We refer to configuration contexts also as evaluation contexts, to highlight that reductions are closed under this kind of context (see below).

A congruence on processes and configurations is an equivalence relation $\mathcal{R}$ that is closed for general contexts: $P \mathcal{R} Q \implies \mathbb{C}[P] \mathcal{R} \mathbb{C}[Q]$ and $M \mathcal{R} N \implies \mathbb{C}[M] \mathcal{R} \mathbb{C}[N]$.

The relation $\equiv$ is defined as the smallest congruence on processes and configurations that satisfies the rules in Figure 2. We write $t =_\alpha t'$ when terms $t, t'$ are equal modulo $\alpha$-conversion. If $\tilde{u} = \{u_1, \dots, u_n\}$, then $\nu \tilde{u}$. A stands for $\nu u_1$. $\dots \nu u_n$. A (there is no need to indicate the order of binders thanks to rule E.NEWC). We write $\prod_{i=1}^n A_i$ for $A_1 | \dots | A_n$ (as before, there is no need to indicate how the latter expression is parenthesized because the parallel operator is associative by rule E.PARA). In rule E.TAGP, processes $\tau_i$ are primitive thread processes (i.e., messages or triggers). Recall the use of the variable convention in these rules: for instance, in the rule $(\nu u. A) | B \equiv \nu u. (A | B)$ the variable convention makes implicit the condition $u \notin \mathit{fn}(B)$. The structural congruence rules are the usual rules for the $\pi$-calculus
$$ (\text{R.Fw}) \quad (\kappa_1 : a\langle P \rangle) | (\kappa_2 : a(X) \triangleright Q) \rightarrow \nu k. (k : Q\{P/X\}) | [(\kappa_1 : a\langle P \rangle) | (\kappa_2 : a(X) \triangleright Q); k] \\ (\text{R.Bw}) \quad (k : P) | [M; k] \rightsquigarrow M $$

<caption>Figure 3: Reduction rules for rhoπ</caption>

(E.PARC to E.α) without the rule dealing with replication, and with the addition of two new rules dealing with tags: E.TAGN and E.TAGP. Rule E.TAGN is a scope extrusion rule to push restrictions to the top level. Rule E.TAGP allows to generate unique tags for each primitive thread process in a configuration. An easy induction on the structure of terms provides us with a kind of normal form for configurations (by convention $\prod_{i \in I} A_i = 0$ if $I = \emptyset$):

**Lemma 1 (Thread normal form).** For any closed configuration M, we have:

$$ M \equiv \nu \tilde{u}. \prod_{i \in I} (\kappa_i : \rho_i) | \prod_{j \in J} [\mu_j; k_j] \\ \text{with } \rho_i = 0, \rho_i = a_i\langle P_i \rangle, \text{ or } \rho_i = a_i(X_i) \triangleright P_i. $$

We say that a binary relation $\mathcal{R}$ on closed configurations is *evaluation-closed* if it satisfies the inference rules:

$$ (\text{R.CTX}) \quad \frac{M \mathcal{R} N}{\mathbb{E}[M] \mathcal{R} \mathbb{E}[N]} \qquad (\text{R.EQV}) \quad \frac{M \equiv M' \qquad M' \mathcal{R} N' \qquad N' \equiv N}{M \mathcal{R} N} $$

The reduction relation $\rightarrow$ is defined as the union of two relations, the *forward reduction relation* $\rightarrow$ and the *backward reduction relation* $\rightsquigarrow$: $\rightarrow = \rightarrow \cup \rightsquigarrow$. Relations $\rightarrow$ and $\rightsquigarrow$ are defined to be the smallest evaluation-closed binary relations on closed configurations satisfying the rules in Figure 3 (note again the use of the variable convention: in rule R.Fw the key k is fresh).

The rule for forward reduction (R.Fw) is the standard communication rule of the higher-order $\pi$-calculus with two side effects: (i) the creation of a new memory to record the configuration that gave rise to it, namely the parallel composition of a message and a trigger, properly tagged (tags $\kappa_1$ and $\kappa_2$ in the rule); (ii) the tagging of the continuation of the message receipt with the fresh key k. The rule for backward reduction (R.Bw) is straightforward: in presence of the thread tagged with key k, memory $[M; k]$ reinstates the
configuration $M$ that gave rise to the tagged thread. We use $\to^*$, $\rightsquigarrow^*$ and $\Rightarrow$ to denote the reflexive and transitive closure of $\to$, $\rightsquigarrow$ and $\to$, respectively. With the reduction rules and the structural laws in place, we can see how the structural rule E.TAGP is used by the reduction. In particular the rule, if used from left to right after a forward step, lets the continuation of a trigger (if it is a parallel composition) continue executing in the forward direction. On the other side, when used from right to left, E.TAGP gathers back all the primitive thread processes belonging to the same parallel composition identified by a particular key. An example of execution will make it clear. Let $M = (k_1 : a\langle P\rangle) | (k_2 : a(X) \triangleright b\langle X\rangle | b(X) \triangleright 0)$, we have that:

$$M \to \nu k. k : (b\langle P\rangle | b(X) \triangleright 0) | [M; k] \qquad (1)$$

$$\equiv \nu k, h_1, h_2. (\langle h_1, \tilde{h} \rangle \cdot k : b\langle P\rangle) | (\langle h_2, \tilde{h} \rangle \cdot k : b(X) \triangleright 0) | [M; k] \qquad (2)$$

$$\to \nu k, h_1, h_2, k_3. (k_3 : 0) | [M; k] | [M_1; k_3] \qquad (3)$$

$$\rightsquigarrow \nu k, h_1, h_2. (\langle h_1, \tilde{h} \rangle \cdot k : b\langle P\rangle) | (\langle h_2, \tilde{h} \rangle \cdot k : b(X) \triangleright 0) | [M; k] \qquad (4)$$

$$\equiv \nu k. k : (b\langle P\rangle | b(X) \triangleright 0) | [M; k] \qquad (5)$$

$$\rightsquigarrow \nu k. (k_1 : a\langle P\rangle) | (k_2 : a(X) \triangleright b\langle X\rangle | b(X) \triangleright 0) \qquad (6)$$

with $\tilde{h} = \{h_1, h_2\}$, $M_1 = (\langle h_1, \tilde{h} \rangle \cdot k : b\langle P\rangle) | (\langle h_2, \tilde{h} \rangle \cdot k : b(X) \triangleright 0)$. We can note in (2) the use of the rule E.TAGP from left to right, in order to allow the two primitive processes to execute (3). On the other side, we use the rule in the opposite way in (5) in order to build back the parallel composition and enable the backward reduction in (6).

**Remark 5.** One could have thought of mimicking the structural congruence rule dealing with parallel composition in RCCS [12], using a monoid structure for tags:

$$(E.TAGP^*) \kappa : (P | Q) \equiv \nu h_1, h_2. (h_1 \cdot \kappa : P) | (h_2 \cdot \kappa : Q)$$

Note that E.TAGP* (differently from what happens in RCCS) ensures commutativity of parallel composition, since $h_1$ and $h_2$ are bound and can thus be $\alpha$-converted. However, (as in RCCS) it does not ensure associativity or having $0$ as a neutral element.

As a consequence, using E.TAGP* instead of E.TAGP would introduce some undesired non-determinism, which would later complicate our definitions (in relation to causality) and proofs. For instance, let $M = k : a\langle Q\rangle | (h : a(X) \triangleright X)$. We have:

$$M \to M' = \nu l. (l : Q) | [M; l]$$
Now, assuming ETagP*, we would have:

$$M \equiv (k : (a\langle Q \rangle | \mathbf{0})) | (h : a(X) \triangleright X) \equiv \\ \nu h_1, h_2. ((h_1 \cdot k : a\langle Q \rangle) | (h_2 \cdot k : \mathbf{0})) | (h : a(X) \triangleright X)$$

Let $M_1 = (h_1 \cdot k : a\langle Q \rangle) | (h : a(X) \triangleright X)$. We would then have: $M \to M''$, where $M'' = \nu h_1, h_2, l. (l : Q) | [M_1; l] | (h_2 \cdot k : \mathbf{0})$. Clearly $M' \neq M''$, which means that a seemingly deterministic configuration, $M$, would have in fact two (actually, an infinity of) derivations towards non structurally equivalent configurations. By insisting on tagging only primitive thread processes, E.TagP avoids this unfortunate situation.

We can characterize this by proving a kind of *determinacy lemma* for rhoπ, which fails if we replace rule E.TagP with rule E.TagP*. Since rhoπ is however non-deterministic, we need to consider only transitions where the same primitive thread processes interact. To fix them we introduce a notion of *marked* primitive thread process. Extend the grammar of rhoπ with marked primitive thread processes of the form $\tau^*$. This extended calculus has exactly the same structural congruence and reduction rules as rhoπ, but with possibly marked primitive thread processes. Now call marked a closed configuration M with exactly two marked processes of the form $a\langle P \rangle^*$ and $(a(X) \triangleright Q)^*$. By extending $\equiv$ and $\to$ to marked configurations we have:

**Lemma 2 (Determinacy).** Let $M$ be a marked configuration such that $M \equiv M_1 = E_1[\kappa_1 : a\langle P \rangle^* | \kappa_2 : (a(X) \triangleright Q)^*]$ and $M \equiv M_2 = E_2[\kappa'_1 : a\langle P \rangle^* | \kappa'_2 : (a(X) \triangleright Q)^*]$. Assume $M_1 \to M'_1$ and $M_2 \to M'_2$ are derived by applying R.Fw with configurations $\kappa_1 : a\langle P \rangle^* | \kappa_2 : (a(X) \triangleright Q)^*$, and $\kappa'_1 : a\langle P \rangle^* | \kappa'_2 : (a(X) \triangleright Q)^*$, respectively, followed by R.Ctx. Then $M'_1 \equiv M'_2$.

**PROOF.** By induction on the form of $E_1$, and case analysis on the form of $\kappa_1$ and $\kappa_2$. $\square$

We can now come back to the notion of consistent configuration. As we already said, consistent configurations are the ones which make sense for us. However, Definition 1 is difficult to work with. To simplify the following development, we define below *well-formed configurations*, which are configurations that enjoy various structural properties useful for proving our results. Then, we show that consistent configurations are well formed, thus when working with consistent configurations we can exploit these properties. Note that not all the well-formed configurations are consistent.
**Definition 3 (Well-formed configuration).**

Let $M \equiv \nu\tilde{u}$. $\prod_{i \in I}(\kappa_i : \rho_i)$ $|$ $\prod_{j \in J}[\mu_j; k_j]$, with $\rho_i = 0$ or $\rho_i$ a primitive thread process, $\mu_j = \delta_j : R_j$ $|$ $\gamma_j : T_j$, $R_j = a_j \langle P_j \rangle$, $T_j = a_j(X_j) \triangleright Q_j$ be a configuration. Let $K$ be the multiset containing all the tags $\kappa_i$ for $i \in I$, $\delta_j, \gamma_j$ for $j \in J$. $M$ is said to be *well formed* if the following conditions are met:

1. $K$ is a set (i.e., all the elements in $K$ are distinct)

2. For each $j \in J$, $k_j \neq \delta_j$ and $k_j \neq \gamma_j$

3. For all $j_1, j_2 \in J$, $j_1 \neq j_2 \implies k_{j_1} \neq k_{j_2}$

4. For each complex tag $\langle h, \tilde{h} \rangle \cdot k \in K$:

* for each $h_l \in \tilde{h}$ there is $\langle h_l, \tilde{h} \rangle \cdot k \in K$

* $k \notin K$

* for each $\tilde{h} \neq \tilde{h}'$ and for each $h'_l, \langle h'_l, \tilde{h}' \rangle \cdot k \notin K$

5. For each $j \in J$, there exist $E \subseteq I$, $D \subseteq J \setminus \{j\}$, $G \subseteq J \setminus \{j\}$, such that:

$$ \nu\tilde{u} \cdot k_j : Q_j\{^{P_j}/X_j\} \equiv \nu\tilde{u} \cdot \prod_{e \in E} \kappa_e : \rho_e \mid \prod_{d \in D} \delta_d : R_d \mid \prod_{g \in G} \gamma_g : T_g $$

Roughly, well-formed configurations enjoy two properties: (i) uniqueness of tags (conditions 1 to 4) and (ii) that for each memory $[\mu; k]$ there are processes corresponding to the continuation of $\mu$ in the configuration (condition 5). In more detail, condition 1 ensures that processes (inside or outside memory) have unique tags. Condition 2 ensures that the thread tag of a memory never occurs in its own configuration part. Condition 3 states that all thread tags of memories are distinct. Condition 4 ensures that if a process (inside or outside memory) has a complex tag $\langle h, \tilde{h} \rangle \cdot k$ then there are processes tagged with all the tags $\langle h_l, \tilde{h} \rangle \cdot k$ with $h_l \in \tilde{h}$, and that no process is tagged by $k$ or by a different complex tag with the same suffix key $k$. Condition 5 is the most tricky one. It requires that for each memory $[\delta_j : a_j \langle P_j \rangle \mid \gamma_j : a_j(X_j) \triangleright Q_j; k_j]$ there are threads in the configuration (indexed by $i \in I$ or $j \in J$) whose composition gives the continuation $\nu\tilde{u} \cdot k_j : Q_j\{^{P_j}/X_j\}$. Note that there are only two possibilities: either the continuation is a unique thread tagged with key $k_j$, or it has been splitted into many threads by one application of rule E.TAGP. In this second case, these threads have complex tags having $k_j$ as a suffix. In both the cases, each thread may be either at top level, or inside the configuration part of another memory (as participant to another communication).
To better understand well formedness let us consider a few examples:

$$k_1 : a\langle\mathbf{0}\rangle | [(k_1 : a\langle\mathbf{0}\rangle) | (k_2 : a(X) \triangleright b\langle\mathbf{0}\rangle); k] \quad (1)$$

$$k : a\langle\mathbf{0}\rangle | [(k_1 : a\langle\mathbf{0}\rangle) | (k_2 : a(X) \triangleright b\langle\mathbf{0}\rangle); k] \quad (2)$$

$$k : a\langle\mathbf{0}\rangle | [(k_1 : a\langle\mathbf{0}\rangle) | (k_2 : a(X) \triangleright a\langle X\rangle); k] \quad (3)$$

$$(\langle h_1, \tilde{h} \rangle \cdot k : a\langle\mathbf{0}\rangle) | (k : b\langle\mathbf{0}\rangle) \quad (4)$$

Configuration (1) is not well formed since it violates condition 1 on key $k_1$ and condition 5 on the memory. Indeed, the unique thread with a tag with suffix $k$, $k : a\langle\mathbf{0}\rangle$, is not structural congruent to the continuation of the memory, $k : b\langle\mathbf{0}\rangle$. Configuration (2) is not well formed because it violates condition 5. Configuration (3) is well formed since all the tags are unique and $k : a\langle X\rangle\{0/X\} \equiv k : a\langle\mathbf{0}\rangle$. In this case the continuation of the memory is a unique top-level thread tagged with $k$. Configuration (4) is not well formed since it violates condition 4. Note that well formedness is a global property, so the composition of well-formed configurations may be a non well-formed configuration, and subterms of well-formed configurations may not be well formed.

We can now show that consistent configurations are well formed.

**Lemma 3.** Each consistent configuration $M$ is well formed

**PROOF.** See Appendix A.1. □

**Remark 6.** The presented semantics and machinery for reversing $HO_\pi$ can be easily adapted to define reversibility in first order $\pi$-calculus. In general, the combination of memories and identifiers should be enough to define reversibility in calculi with implicit substitutions. Indeed, the structure of memories strongly depends on the fact that substitution is not a bijective, hence reversible, function: the only way to reverse a substitution is to record additional information to recover the exact form of the process before the substitution was applied. Actually, to apply our approach to calculi without substitutions, such as CCS, simpler memories would be enough.

## 2.4. Basic properties of reduction in rho_\pi

In this section we show two main properties of rho_\pi: (i) that rho_\pi is a conservative extension of HO_\pi, and (ii) that each rho_\pi reduction step can indeed be reversed.
We first recall HOπ syntax and semantics. The syntax of HOπ processes coincides with the syntax of rhoπ processes in Figure 1 (but HOπ has no concept of configuration). HOπ structural congruence, denoted ≡_π, is the least congruence generated by rules in Figure 2 (restricted to processes) but E.TAGN and E.TAGP. Evaluation contexts in HOπ are given by the following grammar:

$$ \mathbb{E} ::= \cdot \mid (P \mid \mathbb{E}) \mid \nu u. \mathbb{E} $$

HOπ reduction relation →_π is the least binary relation on closed processes closed under HOπ structural congruence and HOπ evaluation contexts defined by the rule:

$$ (\text{HO}\cdot\text{RED}) \quad a\langle P \rangle \mid a(X) \triangleright Q \to_{\pi} Q^{\{P/X\}} $$

In order to show (i) we define the erasing function $\gamma: C \to \mathcal{P}$, which maps a rhoπ configuration to its underlying HOπ process.

**Definition 4 (Erasing function).** The erasing function $\gamma: C \to \mathcal{P}$ is defined inductively by the following clauses:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \gamma(\mathbf{0}) = \mathbf{0} & \gamma(\nu a. M) = \nu a. \gamma(M) & \gamma(\nu k. M) = \gamma(M) \\ \gamma(M | N) = \gamma(M) | \gamma(N) & \gamma(\kappa : P) = P & \gamma([\mu; k]) = \mathbf{0} \end{array} $$

Let us note that $\gamma$ directly deletes the creation of new keys ($\nu k$) since they have no meaning in HOπ (they are not names). Moreover it deletes all the extra machinery (tags and memories) used to reverse HOπ.

Lemma 4 below shows that rhoπ forward computations are indeed decorations on HOπ reductions.

**Lemma 4.** For all closed configurations $M, N$, if $M \to N$ then $\gamma(M) \to_{\pi} \gamma(N)$

**PROOF.** See Appendix A.2. □

<figure><img src="image_2.png" /></figure>

We can prove a converse of Lemma 4. More precisely, Lemma 5 shows that for each HOπ process $R$, each HOπ reduction $R \to_{\pi} S$ and each rhoπ configuration $M$ such that $\gamma(M) = R$ we have a forward reduction in rhoπ corresponding to $R \to_{\pi} S$.
**Lemma 5.** For all closed HOπ processes R, S if $R \to_{\pi} S$ then for all closed configurations M such that $\gamma(M) = R$ there is N such that $M \to N$ and $\gamma(N) = S$.

**PROOF.** See Appendix A.2.

**Remark 7.** A canonical way of lifting a closed HOπ process P to a closed well-formed configuration in rhoπ is by defining $\delta(P) = \nu k \cdot k : P$. As a corollary of Lemma 4 we have:

**Corollary 1.** For each closed HOπ process P, if $\delta(P) \to N$ then $P \to_{\pi} \gamma(N)$.

We now prove the Loop Lemma, which shows that forward and backward reductions in rhoπ are really the inverse of each other.

**Lemma 6 (Loop Lemma).** For all closed well-formed configurations M, N if $M \to N$ then $N \rightsquigarrow M$, and if $M \rightsquigarrow N$ then $N \to M$.

**PROOF.** Let us start from the first implication. From Lemma 38 (see Appendix A.1) we have $M \equiv M'$ and $N' \equiv N$ with $M' = \nu \tilde{u} \cdot \kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$ and $N' = \nu \tilde{u} \cdot k \cdot k : Q^{\{P/X\}} | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$. Then by applying rules (R.BW), (R.Ctx) and (R.EQV) we have $N \rightsquigarrow M$, as desired.

For the other direction from Lemma 39 (see Appendix A.1) we have $M \equiv M'$ with $M' = \nu \tilde{u} \cdot k \cdot k : R | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$ and $\nu \tilde{u} \cdot \kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j] \equiv N$. Since M is a well-formed configuration and well formedness is preserved by structural congruence also $M'$ is well formed. From well formedness we know that $k : R$ is the only thread tagged by $k$ and that $\nu \tilde{u} \cdot k \cdot k : R \equiv \nu \tilde{u} \cdot k \cdot k : Q^{\{P/X\}}$. Then the result follows by applying rules (R.Fw), (R.Ctx) and (R.EQV). $\square$

An easy induction on the length $n$ of the sequence of reductions $M \Rightarrow N$ shows that:

**Corollary 2.** For all closed well-formed configurations M, N if $M \Rightarrow N$ then $N \Rightarrow M$.
## 2.5. Contextual equivalence in rhoπ

We discuss now different notions of contextual equivalence for rhoπ. The main aim of this discussion is to find a contextual equivalence suitable for proving the correctness of our encoding of rhoπ into a variant of higher-order π presented in Section 4. To better justify our choice, we consider and compare different possible notions.

**Barbed congruence.** We can classically complement the operational semantics of the rhoπ calculus with the definition of a contextual equivalence between configurations, which takes the form of a barbed congruence. We first define observables in configurations. We say that name a is observable in configuration M, noted $M \downarrow_a$, if $M \equiv \nu\tilde{u}. (\kappa : a\langle P \rangle) \mid N$, with $a \notin \tilde{u}$. Note that keys are not observable: this is because they are just an internal device used to support reversibility. We write $MR \downarrow_a$, where R is a binary relation on configurations, if there exists N such that $MRN$ and $N \downarrow_a$. The following definitions are classical:

**Definition 5 (Barbed bisimulation and congruence).** A relation $\mathcal{R} \subseteq C^\bullet \times C^\bullet$ on closed configurations is a strong (resp. weak) barbed simulation if whenever $MRN$

* $M \downarrow_a$ implies $N \downarrow_a$ (resp. $N \Rightarrow \downarrow_a$)

* $M \to M'$ implies $N \to N'$, with $M'RN'$ (resp. $N \Rightarrow N'$ with $M'RN'$)

A relation $\mathcal{R} \subseteq C^\bullet \times C^\bullet$ is a strong (resp. weak) barbed bisimulation if $\mathcal{R}$ and $\mathcal{R}^{-1}$ are strong (resp. weak) barbed simulations. We call strong (resp. weak) barbed bisimilarity and write $\sim$ (resp. $\approx$) the largest strong (resp. weak) barbed bisimulation. The largest congruence (with respect to configuration contexts) included in $\sim$ (resp. $\approx$) is called strong (resp. weak) barbed congruence and is denoted $\sim_c$ (resp. $\approx_c$).

A direct consequence of the Loop Lemma is that each closed consistent configuration $M$ is weakly barbed congruent to any of its descendants or predecessors.

**Lemma 7.** For all closed consistent configurations $M, N$, if $M \Rightarrow N$, then $M \approx_c N$.
PROOF. We show that the relation

$$ \mathcal{R} = \{(\mathbb{E}[M], \mathbb{E}[N]) \mid M \Rightarrow N, \mathbb{E} \text{ is a configuration context}\} $$

is a weak barbed bisimulation. Since $\mathcal{R}$ is symmetric by the corollary of the Loop Lemma (Corollary 2), we only need to show that it is a weak barbed simulation. Consider a pair $(\mathbb{E}[M], \mathbb{E}[N]) \in \mathcal{R}$. We have $M \Rightarrow N$, and hence by Corollary 2 $N \Rightarrow M$. Since a configuration context $\mathbb{E}$ is an evaluation context, i.e. if $M \to N$ then $\mathbb{E}[M] \to \mathbb{E}[N]$, then we also have $\mathbb{E}[N] \Rightarrow \mathbb{E}[M]$. We now check easily the two barbed simulation clauses:

* if $\mathbb{E}[M] \downarrow_a$, then $\mathbb{E}[N] \Rightarrow \mathbb{E}[M] \downarrow_a$, and hence $\mathbb{E}[N] \Rightarrow \downarrow_a$ as required.

* if $\mathbb{E}[M] \to M'$, then $\mathbb{E}[N] \Rightarrow \mathbb{E}[M] \to M'$, and hence $\mathbb{E}[N] \Rightarrow M'$, as required.

Since $\mathcal{R}$ is a congruence by construction the thesis follows. $\square$

Lemma 7 shows that weak barbed congruence is not very discriminative among configurations: if $N$ is derived from $M$ then $M \approx_c N$. Weak barbed bisimilarity is even less discriminative: a configuration $M$ is weak barbed bisimilar to a dummy configuration that shows directly all the possible barbs of $M$.

**Lemma 8.** For each closed consistent configuration $M$ let $S$ be the set of weak barbs of $M$. Then $M \approx M_D = \prod_{a \in S}(k_a : a \langle 0 \rangle)$.

PROOF. Let $\mathcal{R} = \{(N, M_D) \mid M \Rightarrow N, M_D = \prod_{a \in S}(k_a : a \langle 0 \rangle)\}$. We show that $\mathcal{R}$ is a weak barbed bisimulation. All the challenges from $N$ are matched by $M_D$ by staying idle, since it has by construction all the required barbs. $M_D$ performs no actions to be matched. Let $a$ be a barb of $M_D$. By construction $a$ is a weak barb of $M$, and also of $N$ since $N \Rightarrow M$ by Corollary 2. $\square$

As shown by the results above, weak barbed bisimilarity and congruence are not very discriminative. Thus, the correctness result for the encoding of $\rho\circ\pi$ into a variant of higher-order $\pi$ presented in [16], based on weak barbed bisimilarity, is weak. In order to improve it, we look for more discriminative equivalences, in particular to equivalences able to distinguish between backward and forward reductions.
*Back and Forth Bisimulations.* Notions of back and forth bisimulation, requiring essentially that forward moves are matched by forward moves and backward moves by backward moves, have already been studied in the literature (see [24, 25, 14, 26]). However, those works consider only strong equivalences, and use backward actions as an auxiliary tool to better understand forward calculi, while we are interested in reversible calculi. The reason why backward actions are useful to understand forward calculi is that back and forth bisimulations can distinguish *true concurrency aspects* of forward calculi while other equivalences such as classical strong bisimulation cannot. For example, the two (CCS) processes:

$$P = a \mid b \qquad Q = a.b + b.a$$

are strongly bisimilar, but they are not back and forth bisimilar. Suppose that $P$ performs the computation $ab$ and then it *undoes* $a$. This computation cannot be matched by $Q$: if $Q$ does the computation $ab$ (left part of the choice) then it cannot undo $a$ before $b$, since $b$ causally depends on $a$.

The definition of back and forth bisimulation for $\rho\circ\pi$ is the following one.

**Definition 6 (Bf barbed bisimulation and congruence).**

A relation $\mathcal{R} \subseteq \mathcal{C}^\bullet \times \mathcal{C}^\bullet$ on closed configurations is a *back and forth barbed simulation* (or *bf barbed simulation* for brevity) if whenever $M\mathcal{R}N$

* $M \downarrow_a$ implies $N \downarrow_a$

* $M \to M'$ implies $N \to N'$, with $M'\mathcal{R}N'$

* $M \rightsquigarrow M'$ implies $N \rightsquigarrow N'$, with $M'\mathcal{R}N'$

A relation $\mathcal{R} \subseteq \mathcal{C}^\bullet \times \mathcal{C}^\bullet$ is a *bf barbed bisimulation* if $\mathcal{R}$ and $\mathcal{R}^{-1}$ are *bf barbed simulations*. We call *bf barbed bisimilarity*, denoted by $\cdot\sim$, the largest *bf barbed bisimulation*. The largest congruence included in $\cdot\sim$ is called *bf barbed congruence* and is denoted by $\cdot\sim_c$.

Bf barbed bisimilarity is more discriminative than strong barbed bisimilarity (Definition 5), since it is able to distinguish the direction of reductions. In fact, one forward (backward) step has to be matched by one forward (backward) step. The same for congruences. Formally, $\cdot\sim\subseteq\sim$ and $\cdot\sim_c\subseteq\sim_c$. We show below that both the inclusions are strict.
Let us start from barbed bisimilarities. Consider:

$$M = \nu k_1, k_2. (k_1 : a\langle 0 \rangle) | (k_2 : a(X) \triangleright b\langle 0 \rangle) \\ N = \nu k_1, k_2, k. [(k_1 : b\langle 0 \rangle) | (k_2 : b(X) \triangleright a\langle 0 \rangle); k] | k : a\langle 0 \rangle$$

Both the configurations have a barb at a, a reduction to a configuration with a barb at b and its inverse, and no other reduction nor barb, thus $M \sim_N N$. However, the reduction creating the barb at b is forward in M and backward in N, thus $M \not\sim_N N$.

For congruences, consider:

$$M = \nu k_1, k_2, a, b. (k_1 : a\langle 0 \rangle) | (k_2 : a(X) \triangleright b\langle 0 \rangle) \\ N = \nu k_1, k_2, k, a, b. [(k_1 : a\langle 0 \rangle) | (k_2 : a(X) \triangleright b\langle 0 \rangle); k] | k : b\langle 0 \rangle$$

The two configurations have no barbs, and they cannot interact with their contexts. Thus $M \sim_c N$, since they can both do infinitely many steps, by doing and undoing the same action. However $M \not\sim_c N$, since M can perform a forward step while N cannot.

Back and forth barbed bisimilarity and congruence are useful equivalences to reason on reversible calculi, but they are too discriminative for our aim. Indeed, the encoding of $\rho\mathbf{h}\mathbf{o}\pi$ relies on some auxiliary steps for managing bookkeeping information, which have no correspondence in the original $\rho\mathbf{h}\mathbf{o}\pi$ computation, and are used both together with forward steps and together with backward steps. We call such steps administrative reductions.

Thus, we adapt back and forth bisimulation by defining an ad-hoc notion of behavioral equivalence, called backward, forward and administrative bisim- ulation (bfa bisimulation for short) allowing also administrative reductions. While we think that such a notion is useful for reasoning on our encoding, we do not claim that it is a good candidate to become a canonical equivalence on reversible calculi. Indeed, when used to relate processes of calculi with no administrative reductions, e.g. two $\rho\mathbf{h}\mathbf{o}\pi$ processes, then bfa bisimilarity coincides with bf bisimilarity.

In order to formally define bfa bisimulation we need to introduce ad- ministrative reductions. We consider calculi allowing forward, backward and administrative reductions. We write $\hookrightarrow$ to denote an administrative step, and $\hookrightarrow^*$ for its reflexive and transitive closure. From now on, $\rightarrow$ is $\rightarrow \cup \rightarrow \cup \rightarrow$ ($\Rightarrow$ is updated accordingly). Note that in $\rho\mathbf{h}\mathbf{o}\pi$ relation $\hookrightarrow$ is empty.
**Definition 7 (Bfa barbed bisimulation and congruence).**

A relation $\mathcal{R} \subseteq \mathcal{C}^\bullet \times \mathcal{C}^\bullet$ on closed configurations is a backward, forward and administrative barbed simulation (or bfa barbed simulation for brevity) if whenever $M\mathcal{R}N$

* $M \downarrow_a$ implies $N \hookrightarrow^* \downarrow_a$

* $M \to M'$ implies $N \hookrightarrow^* \to \to^* N'$ with $M'\mathcal{R}N'$

* $M \rightsquigarrow M'$ implies $N \hookrightarrow^* \rightsquigarrow \to^* N'$ with $M'\mathcal{R}N'$

* $M \hookrightarrow M'$ implies $N \to^* N'$ with $M'\mathcal{R}N'$

A relation $\mathcal{R} \subseteq \mathcal{C}^\bullet \times \mathcal{C}^\bullet$ is a bfa barbed bisimulation if $\mathcal{R}$ and $\mathcal{R}^{-1}$ are bfa barbed simulations. We call bfa barbed bisimilarity, denoted by $\stackrel{\cdot}{\approx}$, the largest bfa barbed bisimulation. The largest congruence included in $\stackrel{\cdot}{\approx}$ is called bfa barbed congruence and is denoted by $\stackrel{\cdot}{\approx}_c$.

Bfa barbed bisimulation requires to match forward reductions with forward reductions, and backward reductions with backward reductions, thus showing that the encoding correctly preserves the behavior of $\mathbf{rho}\pi$ processes, but allows the execution of administrative steps at any moment. Note that when comparing $\mathbf{rho}\pi$ processes, bfa barbed bisimilarity and bfa barbed bisimilarity coincide, that is $\stackrel{\cdot}{\approx} = \stackrel{\cdot}{\approx}_c$.

From the definitions, it is clear that $\stackrel{\cdot}{\approx} \subseteq \stackrel{\cdot}{\approx}$, and $\stackrel{\cdot}{\approx}_c \subseteq \stackrel{\cdot}{\approx}_c$, i.e., bfa barbed bisimilarity and congruence are more discriminative than weak barbed bisimilarity and congruence. We show below that both the inclusions are strict.

Let us start from bfa barbed bisimilarity. We can use the same counterexample used to distinguish between bfa barbed bisimilarity and strong barbed bisimilarity:

$$M = \nu k_1, k_2. (k_1 : a\langle 0 \rangle) \mid (k_2 : a(X) \triangleright b\langle 0 \rangle) \\ N = \nu k_1, k_2, k. [(k_1 : b\langle 0 \rangle) \mid (k_2 : b(X) \triangleright a\langle 0 \rangle); k] \mid k : a\langle 0 \rangle$$

Both the configurations have a barb at $a$, a reduction to a configuration with a barb at $b$ and its inverse, and no other reduction nor barb, thus $M \approx N$. However, the reduction creating the barb at $b$ is forward in $M$ and backward in $N$, thus $M \not\approx N$.
Let us consider now congruences. Consider the following configurations:

$$M = \nu k_1, k_2, k_3. (k_1 : a\langle 0 \rangle) | (k_2 : a(X) \triangleright b\langle 0 \rangle) | (k_3 : a(X) \triangleright c\langle 0 \rangle)$$

$$N = \nu k_1, k_2, k_3, k_4. (k_4 : b\langle 0 \rangle) | (k_3 : a(X) \triangleright c\langle 0 \rangle) |$$

$$[(k_1 : a\langle 0 \rangle) | (k_2 : a(X) \triangleright b\langle 0 \rangle); k_4]$$

$$M' = \nu k_1, k_2, k_3, k_5. (k_5 : c\langle 0 \rangle) | (k_2 : a(X) \triangleright b\langle 0 \rangle) |$$

$$[(k_1 : a\langle 0 \rangle) | (k_3 : a(X) \triangleright c\langle 0 \rangle); k_5]$$

Since $M \to N$ by Lemma 7 $M \approx_c N$, but $M \not\approx N$ and hence $M \not\approx_c N$. To prove this last part, assume that there exists a bfa barbed bisimulation $\mathcal{R}$ between $M$ and $N$, i.e. such that $(M, N) \in \mathcal{R}$. We have $M \to M'$, and we have no $N'$ such that $N \to N'$ nor $N \hookrightarrow N'$, thus the reduction cannot be matched.

### 3. Causality in rhoπ

We now proceed to the analysis of causality in rhoπ. We first show that reversibility in rhoπ is causally consistent. We then show that the causality information in rhoπ is at least as fine as the causality information from Boreale and Sangiorgi's causal semantics [21].

#### 3.1. Causal consistency

In order to prove causal consistency, we mostly adapt the terminology and arguments of [12].

We call transition a triplet of the form $M \xrightarrow{m_{\to}} M'$, or $M \xrightarrow{m_{\to}} M'$, where $M, M'$ are closed consistent configurations, $M \to M'$, and $m$ is the memory involved in the reduction $M \to M'$. We say that a memory $m$ is involved in a forward reduction $M \to M'$ if $M \equiv \mathbb{E}[\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q]$, $M' \equiv \mathbb{E}[\nu k. (k : Q\{P/X\}) | m]$, and $m = [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k]$. In this case, the transition involving $m$ is denoted by $M \xrightarrow{m_{\to}} M'$. Likewise, we say that a memory $m = [N; k]$ is involved in a backward reduction $M \rightsquigarrow M'$ if $M \equiv \mathbb{E}[(k : Q) | m]$, $M' \equiv \mathbb{E}[N]$. In this case, the transition involving $m$ is denoted by $M \xrightarrow{m_{\to}} M'$. We let $\eta$ and its decorated variants range over labels $m_{\to}$ and $m_{\to}$. If $\eta = m_{\to}$, we set $\eta_{\bullet} = m_{\to}$ and vice versa. In a transition $M \xrightarrow{\eta} N$, we say that $M$ is the source of the transition, $N$ is its target, and $\eta$ is its label (of the form $m_{\to}$ or $m_{\to}$, where $m$ is some memory).
**Definition 8 (Name-preserving transitions).** We say a transition $t$ is *name-preserving* if:

* $t$ is derived without using $\alpha$-conversion;

* if $t$ creates a new memory, the thread tag of the memory is chosen using a fixed function from the tags of the interacting threads;

* if $t$ is derived using rule E.TAGP from left to right, the new keys are generated and assigned to threads using a fixed function.

Intuitively, name-preserving transitions ensure that a given tag is always attached to the same process. In particular, if a memory is generated with thread tag $k$ by a forward name-preserving transition involving threads with tags $\kappa_1$ and $\kappa_2$, removed by a backward name-preserving transition, and re-generated by a forward name-preserving transition involving again the threads with tags $\kappa_1$ and $\kappa_2$, its memory tag is again $k$. Similarly, if a process is split using rule E.TAGP, the generated threads are recollected and then split again, each thread preserves its tag. In the rest of this section we only consider name-preserving transitions and "transition" used in a definition, lemma or theorem, stands for "name-preserving transition". Note that working with name-preserving transitions only is licit because of the determinacy lemma (Lemma 2) and a corresponding result that can be proved for backward transitions.

Two transitions are said to be *coinital* if they have the same source, *cofinal* if they have the same target, *composable* if the target of the first one is the source of the other. A sequence of pairwise composable transitions is called a *trace*. We let $t$ and its decorated variants range over transitions, $\sigma$ and its decorated variants range over traces. Notions of target, source and composability extend naturally to traces. We note $\epsilon_M$ the empty trace with source $M$, $\sigma_1; \sigma_2$ the composition of two composable traces $\sigma_1$ and $\sigma_2$. The stamp $\lambda(m_{\rightarrow})$ of a memory $m = [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k]$ is defined to be the set $\{\kappa_1, \kappa_2, k\}$; we set $\lambda(m_{\rightarrow}) = \lambda(m_{\leftarrow})$.

**Definition 9 (Concurrent transitions).** Two coinital transitions $t_1 = M \xrightarrow{\eta_1} M_1$ and $t_2 = M \xrightarrow{\eta_2} M_2$ are said to be *in conflict* if at least one of the following conditions holds:

* there is a tag $\kappa \in \lambda(\eta_1)$ such that $\kappa \in \lambda(\eta_2)$,
* there is a tag $\kappa \in \lambda(\eta_1)$ which is a key $k$ and there is a complex tag with suffix $k$ in $\lambda(\eta_2)$,

* the symmetric of one of the two conditions above, swapping $\eta_1$ and $\eta_2$.

Two coinitial transitions are concurrent if they are not in conflict.

**Remark 8.** Note that the stamp of a memory $[M; k]$ includes its tag $k$. This is necessary to take into account possible conflicts between a forward action and a backward action, as in the following example. The configuration

$$M = \nu l, k, h. (k : a\langle P\rangle) | [N; k] | (h : a(X) \triangleright Q)$$

has two possible transitions $t = M \xrightarrow{m} \nu l, k, h. N | (h : a(X) \triangleright Q)$, where $m = [N; k]$, and $t' = M \xrightarrow{m'} \nu l, k, h. [N; k] | m' | l : Q\{P/X\}$, where $m' = [(k : a\langle P\rangle) | (h : a(X) \triangleright Q); l]$. The two transitions $t$ and $t'$ are in conflict over the use of the resource $k : a\langle P\rangle$.

Consider now the configuration

$$M = \nu l, k, h, h_1, h_2. (\langle h_1, \tilde{h} \rangle \cdot k : a\langle P \rangle) | (\langle h_2, \tilde{h} \rangle \cdot k : b\langle 0 \rangle) | [N; k] | (h : a(X) \triangleright Q)$$

where $\tilde{h} = \{h_1, h_2\}$. Again we have a conflict, since the backward action involving memory $[N; k]$ is in conflict with any forward action by descendants of $k$, even if not all of them are involved.

The Loop Lemma ensures that each transition $t = M \xrightarrow{\eta} N$ has a reverse one $t_\bullet = N \xrightarrow{\eta_\bullet} M$. The above definition of concurrent transitions makes sense:

**Lemma 9 (Square lemma).** If $t_1 = M \xrightarrow{\eta_1} M_1$ and $t_2 = M \xrightarrow{\eta_2} M_2$ are two coinicial concurrent transitions, then there exist two cofinal transitions $t_2/t_1 = M_1 \xrightarrow{\eta_2} N$ and $t_1/t_2 = M_2 \xrightarrow{\eta_1} N$.

**PROOF.** By case analysis on the form of transitions $t_1$ and $t_2$. See Appendix B.1 for details. □

<figure><img src="image_3.png" /></figure>

We are now in a position to show that reversibility in rho$\pi$ is causally consistent. Following Lévy [27] we define first the notion of causal equivalence between traces that abstracts away from the order of causally independent
transitions. We define $\asymp$ as the least equivalence relation between traces closed under composition that obeys the following rules:

$$t_1; t_2/t_1 \asymp t_2; t_1/t_2 \qquad t; t_\bullet \asymp \epsilon_{\text{source}(t)} \qquad t_\bullet; t \asymp \epsilon_{\text{target}(t)}$$

Intuitively $\asymp$ states that if we have two concurrent transitions, then the two traces obtained by swapping the order of their execution are the same, and that a trace composed by a transition followed by its inverse is equivalent to the empty one.

The proof of causal consistency proceeds along the exact same lines as in [12], with simpler arguments because of the simpler form of our memory stamps.

**Lemma 10 (Rearranging Lemma).** Let $\sigma$ be a trace. There exist forward traces $\sigma'$ and $\sigma''$ such that $\sigma \asymp \sigma'_\bullet; \sigma''$.

**PROOF.** The proof is in Appendix B.1. $\square$

**Lemma 11 (Shortening Lemma).** Let $\sigma_1, \sigma_2$ be coinitial and cofinal traces, with $\sigma_2$ forward. Then, there exists a forward trace $\sigma'_1$ of length at most that of $\sigma_1$ such that $\sigma'_1 \asymp \sigma_1$.

**PROOF.** The proof is in Appendix B.1. $\square$

**Theorem 1 (Causal consistency).** Let $\sigma_1$ and $\sigma_2$ be coinitial traces, then $\sigma_1 \asymp \sigma_2$ if and only if $\sigma_1$ and $\sigma_2$ are cofinal.

**PROOF.** The proof is in Appendix B.1. $\square$

## 3.2. Causality in rho$\pi$ and in the causal higher-order $\pi$-calculus

From what precedes, it should be clear that the core of the reversibility machinery in rho$\pi$ is the causality information built during execution. The question therefore arises of the relationship between this notion of causality and the one found in several studies on the causal semantics of the $\pi$-calculus, e.g. [21, 28, 29, 30]. In this section we limit ourselves to the study of the relationship between the causality information used in rho$\pi$ and that used by Boreale and Sangiorgi in their analysis of causality for the $\pi$-calculus [21].

For a meaningful comparison, we first adapt the causality apparatus from that paper to the asynchronous higher-order $\pi$-calculus. We call “causal
$$ (\text{E-PAR}) \quad K ::= A \mid B \equiv K ::= A \mid K ::= B \qquad (\text{E-CAU}) \quad K_1 ::= K_2 ::= A \equiv K_1 \cup K_2 ::= A \\ (\text{E-RES}) \quad K ::= \nu a. A \equiv \nu a. K ::= A \qquad (\text{E-VOID}) \quad \emptyset ::= A \equiv A \qquad (\text{E-NIL}) \quad K ::= \mathbf{0} \equiv \mathbf{0} $$

<caption>Figure 4: Structural congruence for choπ</caption>

higher-order π" (choπ for short) the resulting calculus. Processes of choπ coincide with the processes of rhoπ (see Figure 1). Following [21], causal processes in choπ, ranged over by A, B, are processes decorated with causality information, defined by the following grammar:

$$ A ::= K ::= A \mid A \mid A \mid \nu a. A \mid P $$

where K ranges over finite sets of keys, i.e. $K \subseteq_{\text{fin}} K$. Informally, a causal process $K :: P$ identifies the set of causes K that gave rise to process P.

We denote by $k(A)$ the set of keys of a causal process A.

We define a reduction semantics<fnref n="3" /> for choπ (see Appendix B.2 for a comparison between this reduction semantics and a labelled transition system semantics directly adapted from [21]), via a reduction relation that operates modulo structural congruence. The structural congruence relation $\equiv$ is the least congruence relation on causal processes that obeys the structural congruence rules on HOπ processes given in Figure 2 and the rules in Figure 4. The reduction relation $\rightarrow$ is the least binary relation on closed causal processes that is closed under structural congruence and evaluation contexts defined by the rule:

$$ (\text{C-RED}) \quad K_1 ::= a\langle P \rangle \mid K_2 ::= a(X) \triangleright Q \rightarrow K_1 \cup K_2 ::= Q\{^P/X\} $$

Evaluation contexts for causal processes are given by the following grammar:

$$ \mathbb{E} ::= \bullet \mid A \mid \mathbb{E} \mid \nu a. \mathbb{E} $$

<footnote n="3">³Moving from the labelled semantics considered in [21] to the reduction semantics considered here makes part of the causal dependences considered in [21], the so called object dependences, unobservable.</footnote>
As for rhoπ, we can inductively define a function γ that erases the causal-
ity information from a causal process to get a standard HOπ process via the
following clauses:

$$
\gamma(P) = P
$$

$$
\gamma(A | B) = \gamma(A) | \gamma(B)
$$

$$
\gamma(\nu a. A) = \nu a. \gamma(A)
$$

$$
\gamma(K :: A) = \gamma(A)
$$

We can now present the relationship between causal information in causal
processes and in rhoπ configurations. This relationship takes the form of a
bisimulation which we call causal correspondence. Informally, causal corre-
spondence asserts that, during execution, a causal process and its “corre-
sponding” rhoπ process ascribe the same causes to the same sub-processes.

We first define causal barbs on causal processes and rhoπ configurations.

For causal processes, a causal barb K :: a corresponds to the ability to
communicate on a channel a due to causes in K. More precisely:

**Definition 10 (Causal barbs for causal processes).** A choπ causal process A has a causal barb K :: $\bar{a}$, noted $A \downarrow_{K::\bar{a}}$, if and only if $A \equiv \nu\tilde{c}. K :: a\langle P \rangle | B$, with $a \notin \tilde{c}$, for some $\tilde{c}, P, B$. A choπ causal process A has a causal barb K :: $a$, noted $A \downarrow_{K::a}$, if and only if $A \equiv \nu\tilde{c}. K :: a(X) \triangleright P | B$, with $a \notin \tilde{c}$, for some $\tilde{c}, P, B$.

For configurations, the notion of causal barb depends on a causality de-
pendence relation between tags.

**Definition 11 (Causal dependence).** Let $M$ be a configuration and let $T_M$ be the set of tags occurring in $M$. The binary relation $<_M$ on $T_M$ is defined as the smallest relation satisfying the following clauses:

$\langle h_i, \tilde{h} \rangle \cdot k <_M k;$

• $k <_M \kappa_1$ and $k <_M \kappa_2$ if $[\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k]$ occurs in $M$.

The causal dependence relation $<:M$ is the reflexive and transitive closure of
$<_M$.

$\kappa <:M \kappa'$ reads “$\kappa$ is a causal descendant of $\kappa'$ according to $M$”. When configuration $M$ is clear from the context, we write $\kappa <: \kappa'$ for $\kappa <:M \kappa'$. When $K$ is a set of keys, we write $\kappa <: K$ if for all $h \in K$, we have $\kappa <: h$. We denote by $fk(M)$ the set of free keys of a configuration $M$. Note that $fk(M) \subseteq fn(M)$.
**Definition 12 (Causal barbs for configurations).** A rhoπ configuration M has a causal barb K :: a where K ⊆ fk(M), noted M ↓$_{K}$$_{::}$$_{a}$, if and only if M ≡ ν̃u. (κ : a⟨P⟩) | N, with a /∈ ũ and κ <: K. Likewise, M ↓$_{K}$$_{::}$$_{a}$ where K ⊆ fk(M), if and only if M ≡ ν̃u. (κ : a(X) ▷ P) | N, with a /∈ ũ and κ <: K.

**Definition 13 (Causal correspondence).** A relation $\mathcal{R}$ is a causal correspondence between rhoπ configurations and choπ causal processes if the following condition holds: if $\langle M, A \rangle \in \mathcal{R}$, then

1. $\gamma(M) \equiv \gamma(A)$ and $fk(M) = k(A)$;

2. if $M \downarrow_{K::\alpha}$, then there exists $K'$ such that $K \subseteq K'$ and $A \downarrow_{K'::\alpha}$;

3. if $M \to N$, then there exists $B$ such that $A \to B$ and $\langle N, B \rangle \in \mathcal{R}$.

4. if $A \downarrow_{K::\alpha}$, then $M \downarrow_{K::\alpha}$;

5. if $A \to B$, then there exists $N$ such that $M \to N$ and $\langle N, B \rangle \in \mathcal{R}$;

A configuration $M$ and a causal process $A$ are said to be in causal correspondence if there exists a causal correspondence $\mathcal{R}$ such that $\langle M, A \rangle \in \mathcal{R}$.

A rhoπ configuration M can be mapped to a choπ causal process by applying to it the syntactic transformation χM that replaces configurations k : P in M with causal processes K :: P, where K includes all k' ∈ fk(M) such that k <:M k'. χM is defined inductively as follows:

$$
\begin{align*}
\chi_M(\mathbf{0}) &= \mathbf{0} & \chi_M(\kappa : P) &= \{k' \in \mathbf{fk}(M) \mid \kappa <:M k'\} :: P \\
\chi_M(\nu a. N) &= \nu a. \chi_M(N) & \chi_M(N_1 | N_2) &= \chi_M(N_1) | \chi_M(N_2) \\
\chi_M(\nu k. N) &= \chi_M(N)
\end{align*}
$$

We can now state our causal correspondence theorem:

**Theorem 2.** Let $M$ be a rhoπ configuration. Then $M$ and $\chi_M(M)$ are in causal correspondence.

PROOF. The proof shows that the relation

$$
\mathcal{R} = \{ \langle M, \chi_M(M) \rangle \mid M \text{ is consistent} \}
$$

is a causal correspondence. Let us consider the different conditions:

1. by construction;
2. by definition $M \downarrow_{K::\alpha}$ means that there is a trigger or a message in $M$ with key $\kappa$ such that $\kappa <_M K$ with $K \subseteq \text{fk}(M)$. From the definition of $\chi_M$, the trigger or the message are mapped to a corresponding trigger or message with set of causes $K' \supseteq K$, thus $A \downarrow_{K'::\alpha}$ as required;

3. from Lemma 38 (see Appendix A.1), we have

$$ M \equiv \nu\tilde{a}, \tilde{h}. \kappa_1 : a\langle P \rangle \mid \kappa_2 : a(X) \triangleright Q \mid \prod_{i \in I} \kappa_i : \rho_i \mid \prod_{j \in J} [\mu_j; k_j] \rightarrow \\ \nu\tilde{a}, \tilde{h}, k. k : Q\{P^P/X\} \mid [\kappa_1 : a\langle P \rangle \mid \kappa_2 : a(X) \triangleright Q; k] \mid \\ \prod_{i \in I} \kappa_i : \rho_i \mid \prod_{j \in J} [\mu_j; k_j] \equiv N $$

By definition, we have:

$$ \chi_M(M) \equiv \nu\tilde{a}. K_1 :: a\langle P \rangle \mid K_2 :: a(X) \triangleright Q \mid \prod_{i \in I} K_i :: \rho_i $$

$$ \chi_N(N) \equiv \nu\tilde{a}, k. K :: Q\{P^P/X\} \mid \prod_{i \in I} K_i : \rho_i $$

To conclude we need to show that $K = K_1 \cup K_2$. We have:

$$ K = \{k' \in \text{fk}(N) \mid k <_N k'\} $$

$$ K_1 = \{k' \in \text{fk}(M) \mid \kappa_1 <_M k'\} $$

$$ K_2 = \{k' \in \text{fk}(M) \mid \kappa_2 <_M k'\} $$

Note that $\text{fk}(N) = \text{fk}(M)$. Also, thanks to the memory $[\kappa_1 : a\langle P \rangle \mid \kappa_2 : a(X) \triangleright Q; k]$, the fact that $k$ is bound and the properties of keys we have $k <_N k'$ iff $\kappa_1 <_M k'$ or $\kappa_2 <_M k'$;

4. similar to item 2;

5. similar to item 3.

□

## 4. Encoding rhoπ in HOπ

This section shows that rhoπ can be encoded in a variant of HOπ, which we call HOπ⁺, that allows the use of bi-adic channels, join patterns [31, 32], sub-addressing, abstractions and applications. This particular variant was chosen for convenience, because it simplifies our encoding. All HOπ⁺ constructs are well understood in terms of expressive power with respect to HOπ (see [33, 34] for abstractions in π-calculus).

The encoding presented here is slightly different from the one presented in [16], in order to obtain a finer correspondence result. Indeed [16] shows that a rhoπ configuration and its translation are weak barbed bisimilar. Such result allows us to encode reversibility in an already existing calculus, without introducing any new ad-hoc primitive. Even if the result is quite surprising, because of the coarseness of weak barbed bisimilarity (as emerged in
$$
\begin{align*}
& P, Q ::= \mathbf{0} \mid X \mid \nu u. P \mid (P \mid Q) \mid u\langle F, v \rangle \mid J \triangleright P \mid (F \mid V) \\
& F ::= (u)P \mid (X)P \mid (u)F \mid (X)F \\
& V ::= u \mid F \\
& J ::= u(X, v) \mid u(X, \setminus v) \mid J \mid J \\
& u, v \in \mathcal{I}
\end{align*}
$$

<caption>Figure 5: Syntax of HOπ⁺</caption>

Section 2.5), it does not establish a strong enough correspondence between
rhoπ and its encoding. Therefore, here we base our results on a more dis-
criminative equivalence, bfa barbed bisimilarity, able to distinguish forward
reductions from backward ones.

The remainder of the section is organized as follows: first we introduce
the syntax and the semantics of HOπ⁺, then we introduce our encoding and
show that a rhoπ consistent configuration M and its translation in HOπ⁺
are bfa barbed bisimilar. To ease the reading of the section, some proofs and
auxiliary results are reported in Appendix C.

4.1. HOπ⁺

The syntax of HOπ⁺ is given in Figure 5. Channels in HOπ⁺ are bi-adic
in the sense that they carry pairs of the form *F*, *v*, that is an abstraction *F*
and a name *v*. A trigger always receives a message *F*, *w* on a given channel
*u*, but it can pose the additional constraint that the name *w* indeed coincides with the name *v* in the trigger (sub-addressing). The trigger prefix is
written *u*(*X*, *v*) if it poses no constraint on *w*, *u*(*X*, *\v*) otherwise. Actually
triggers use Join patterns, i.e. they allow to specify a set of messages that are
read atomically. Join patterns are linear, i.e. all the names of the channels
from which messages are read are distinct. HOπ⁺ supports abstractions over
names (*u*)*P* and over process variables (*X*)*P*, and applications (*F* *V*), where
a value *V* can be a name or an abstraction. We take the set of names of HOπ⁺
to be the set *I* ∪ {⋆} where *I* is the set of rhoπ identifiers (*I* = *N* ∪ *K*). Thus
both rhoπ names and rhoπ keys are names in HOπ⁺. The set of (process)
variables of HOπ⁺ is taken to coincide with the set *V* of variables of rhoπ.
Moreover we let *B* to range over processes *P* and abstractions *F*.

The structural congruence for HOπ⁺, denoted by ≡, obeys the same rules
$$ (\text{RED}) \frac{\text{match}(F_i, X_i) = \theta'_i \quad \text{match}(v_i, \psi_i) = \theta_i}{\left(\prod_{i=1}^n u_i \langle F_i, v_i \rangle\right) \mid \left(\left(\prod_{i=1}^n u_i(X_i, \psi_i)\right) \triangleright P\right) \rightarrow P \theta'_1 \dots \theta'_n \theta_1 \dots \theta_n} \\ (\text{APP}) \frac{\text{match}(V, \psi) = \theta}{((\psi)B V) \rightarrow B\theta} $$

<caption>Figure 6: Reduction rules for HOπ⁺</caption>

as those of rhoπ processes (see Figure 2), except for the rules E.TAGN and E.TAGP, which are specific to rhoπ. Evaluation contexts in HOπ⁺, as in HOπ, are given by the following grammar:

$$ \mathbb{E} ::= \cdot \mid (P \mid \mathbb{E}) \mid \nu u. \mathbb{E} $$

The reduction relation for HOπ⁺, also denoted by →, is defined as the least relation on closed processes closed under HOπ⁺ structural congruence and HOπ⁺ evaluation contexts that satisfies the rules in Figure 6, where ψ is either a name v, a process variable X or an escaped name \u. The function match in Figure 6 is the partial function which is defined in the cases given by the clauses below, and undefined otherwise:

$$ \text{match}(u, v) = \{^u/\nu\} \quad \text{match}(u, \setminus u) = \{^u/\setminus\} \quad \text{match}(F, X) = \{^F/\setminus\} $$

Note that an escaped name \u will match just with name u. Rule RED is a generalization (in the sense of join patterns) of the usual communication rule for HOπ. If there are enough messages (left-hand side of the reduction in the conclusion) satisfying a certain input process, then they are consumed at once and the continuation of the input process is triggered with the necessary substitutions. Rule APP mimics the well known β-reduction of the λ-calculus [35]. We use ⇒ to denote the reflexive and transitive closure of →.

**Remark 9.** Even if HOπ⁺ allows using arbitrary join patterns, our encoding will use just binary join patterns (and unary join patterns, i.e. normal inputs).
*Conventions.* In writing HO$\pi^+$ terms, $u\langle v\rangle$ abbreviates $u\langle(X)0, v\rangle$, $\bar{u}$ abbreviates $u\langle(X)0, \star\rangle$ and $u\langle F\rangle$ abbreviates $u\langle F, \star\rangle$. Likewise, $a(u) \triangleright P$ abbreviates $a(X, u) \triangleright P$, where $X \notin \mathbf{fv}(P)$, $a \triangleright P$ abbreviates $a(X, \star) \triangleright P$, where $X \notin \mathbf{fv}(P)$, and $a(X) \triangleright P$ abbreviates $a(X, \star) \triangleright P$. We adopt the usual conventions for writing applications and abstractions: $(F V_1 \dots V_n)$ stands for $((F V_1) \dots) V_n)$, and $(X_1 \dots X_n)F$ stands for $(X_1) \dots (X_n)F$. When there is no potential ambiguity, we often write $FV$ for $(F V)$. When defining HO$\pi^+$ processes, we freely use recursive definitions for these can be encoded using, e.g., the Turing fixed point combinator $\Theta$ defined as $\Theta = (A A)$, where $A = (X F)(F (X X F))$ (cf. [35, p. 132]).

In the rest of the paper we denote by $\mathcal{P}_{\text{HO}\pi^+}$ the set of HO$\pi^+$ processes, by $\mathcal{C}_{\text{rho}\pi}$ the set of rho$\pi$ configurations and by $\mathcal{P}_{\text{rho}\pi}$ the set of rho$\pi$ processes.

## 4.2. Encoding of rho$\pi$

The encoding $\langle\cdot|\rangle : \mathcal{P}_{\text{rho}\pi} \to \mathcal{P}_{\text{HO}\pi^+}$ of processes of rho$\pi$ in HO$\pi^+$ is defined inductively in Figure 7. It extends to an encoding $\langle\cdot|\rangle : \mathcal{C}_{\text{rho}\pi} \to \mathcal{P}_{\text{HO}\pi^+}$ of configurations of rho$\pi$ in HO$\pi^+$ as given in Figure 8. The encoding of processes features two labelled triggers, $\triangleright_b$ and $\triangleright_f$. They will be introduced later on, in Definition 14. For now, they can be considered as normal triggers $\triangleright$.

We present below the two main ideas underlying the encoding of processes, and then go deeper into its details. First, a tagged process $l : P$ is interpreted as a process equipped with a special channel $l$ (we may refer to it as its *key channel*) on which to send itself upon successful rollback. This intuition leads to the encoding of a rho$\pi$ process as an abstraction which takes this rollback channel $l$ (its own key) as a parameter. Second, each rho$\pi$ process translation generates also the *process killer*, that is a process in charge of rolling it back. We have three kinds of such processes: *KillM*, *KillT* and *KillP*, representing respectively the killer of a message, of a trigger and of a parallel composition of processes.

As we already said, all the translations of rho$\pi$ processes are abstractions over a channel, and this channel is the tag of the process (or part of it in the case of a complex tag, as we will see in the encoding of configurations). The null process 0 is translated as a message on the abstracted channel along with a *Rew* process. This translation, as well as translations of other processes, is by itself diverging. Consider the encoding of the rho$\pi$ process $l : 0$:

$$l\langle\text{Nil}\rangle | (\text{Rew } l) \to l\langle\text{Nil}\rangle | l(Z) \triangleright (Z l) \to (\text{Nil } l) \to l\langle\text{Nil}\rangle | (\text{Rew } l)$$
$$
\begin{align*}
(\mathbf{0}) &= \mathbf{Nil} & (\mathbf{X}) &= \mathbf{X} \\
(\mathbf{a}\langle\mathbf{P}\rangle) &= (l)(\mathbf{Msg}\ a\ (\mathbf{P})\ l) & (\mathbf{va.}\ \mathbf{P}) &= (l)\mathbf{va.}\ (\mathbf{P})\ l \\
(\mathbf{P} \mid \mathbf{Q}) &= (l)(\mathbf{Par}\ (\mathbf{P})\ (\mathbf{Q})\ l) \text{ if } \mathbf{P}, \mathbf{Q} \neq \mathbf{0} & (\mathbf{P} \mid \mathbf{0}) &= (\mathbf{P}) \\
(\mathbf{a}(\mathbf{X}) \triangleright \mathbf{P}) &= (l)(\mathbf{Trig}\ ((\mathbf{X}\ c)\mathbf{c}\langle(\mathbf{P})\rangle)\ a\ l) & (\mathbf{0} \mid \mathbf{P}) &= (\mathbf{P})
\end{align*}
$$

$$
\begin{align*}
\mathbf{Nil} &= (l)(l\langle\mathbf{Nil}\rangle | \mathbf{(Rew} l)) \\
\mathbf{Msg} &= (a \ X \ l)a\langle X, l\rangle | \mathbf{(KillM a} l) \\
\mathbf{KillM} &= (a \ l)(a(X, \ \l) \triangleright \l\langle(h)\mathbf{Msg} a \ X \ h\rangle | \mathbf{Rew} l) \\
\mathbf{Par} &= (X \ Y \ l)\nu h, k. X \ h \mid Y \ k \mid \mathbf{(KillP h k l)} \\
\mathbf{KillP} &= (h \ k \ l)(h(W) \mid k(Z) \triangleright \l\langle(l)\mathbf{Par} W Z \ l\rangle | \mathbf{Rew} l) \\
\mathbf{Trig} &= (Y \ a \ l)\nu t. \bar{t} \mid (a(X, h) \mid t \triangleright_f \nu k, c. (Y X c) \mid (c(Z) \triangleright (Z k)) \mid \\
& \qquad (\mathbf{Mem} Y a X h k l)) \mid \mathbf{(KillT Y t l a)} \\
\mathbf{KillT} &= (Y t l a)(t \triangleright \l\langle(h)\mathbf{Trig} Y a h\rangle | \mathbf{Rew} l) \\
\mathbf{Mem} &= (Y a X h k l)k(Z) \triangleright_b (\mathbf{Msg} a X h) \mid \mathbf{(Trig Y a} l) \\
\mathbf{Rew} &= (l)(l(Z) \triangleright Z \ l)
\end{align*}
$$

<caption>Figure 7: Encoding rhoπ processes</caption>

Divergence here could be avoided by removing the Rew process from the translation of 0, and considering it as just a message on its abstracted channel. That is:

$$
(\mathbf{0}) = (l)l\langle\mathbf{Nil}\rangle
$$

We stick however to the first translation to preserve the symmetry with the
translations of the other primitive processes (messages and triggers), since
this simplifies the statement of some invariants of our encoding, and since,
as already said, divergence here is not a relevant issue.

The translation of a message *k*: *a*⟨*P*⟩ after a few applications becomes a
process of the form:

$$
a(\langle P \rangle, k) \mid \text{(KillM a k)}
$$

consisting in a message on channel *a* carrying a pair (here we can see why we
use bi-adic channels) in parallel with its killer process. The message carries
the translation of the original message content *P* along with the abstracted
$$ (\mathbf{0}) = \mathbf{0} $$

$$ (M | N) = (M) | (N) $$

$$ (\nu u. M) = \nu u. (M) $$

$$ (k : P) = (\mathbf{P}) k $$

$$ (\langle h_i, \tilde{h} \rangle \cdot k : P) = (\mathbf{P}) h_i | \text{Kill}_{\langle h_i, \tilde{h} \rangle \cdot k} $$

$$ (\llbracket \kappa_1 : a\langle P \rangle \mid \kappa_2 : a(X) \triangleright Q; k \rrbracket) = (\text{Mem}((X c)c\langle\langle Q \rangle\rangle) a (\mathbf{P}) (\kappa_1) k (\kappa_2)) | \text{Kill}_{\kappa_1} | \text{Kill}_{\kappa_2} $$

$$ (k) = k $$

$$ (\langle h_i, \tilde{h} \rangle \cdot k) = h_i $$

$$ \text{Kill}_{\langle h_i, \tilde{h} \rangle \cdot k} = \left\{ \begin{array}{ll} \text{KillP} h_1 h_2 k & \text{if } i=1, n=2 \\ \nu \tilde{l}. (\text{KillP} h_1 l_1 k) | \prod_{i=2}^{n-2} (\text{KillP} h_i l_i l_{i-1}) | & \text{if } i=1, n > 2 \\ \mathbf{0} & \text{if } i \neq i \end{array} \right. $$

where $n$ is the size of $\tilde{h}$

$$ \text{Kill}_k = \mathbf{0} $$

<caption>Figure 8: Encoding rhoπ configurations</caption>

channel. Let us see how the message above can rollback by sending itself on channel $k$.

**Example 1 (Rollback of a message).** Let us consider the tagged message $k : a\langle P \rangle$. It can rollback as follows:

$$ \begin{aligned} (k : a\langle P \rangle) = (a\langle P \rangle)k &= (l)(\text{Msg a } (\mathbf{P}) l)k \Rightarrow a\langle (\mathbf{P}) \rangle, k \mid (\text{KillM a } k) \Rightarrow \\ & a\langle (\mathbf{P}) \rangle, k \mid (a(X, \setminus k) \triangleright l\langle (h)\text{Msg a } X h \rangle | \text{Rew } k) \Rightarrow k\langle (h)\text{Msg a } (\mathbf{P}) h \rangle | \text{Rew } k \end{aligned} $$

Since $(h)\text{Msg a } (\mathbf{P}) h = (a\langle P \rangle)$, we have that $k\langle (h)\text{Msg a } (\mathbf{P}) h \rangle = k\langle (a\langle P \rangle) \rangle$. Thus a message can rollback by sending itself on its key channel.

The abstracted channel $k$ inside the message is needed to ensure that the message will be rolled back only by its own `KillM`. Indeed, the process
(KillM a k) consumes a message on the channel a only if it carries the name k. This is why the KillM process is an abstraction over two channels, and explains the need of sub-addressing. The need for the Rew process will be explained later on.

The translation of a parallel composition is quite straightforward: two new key channels are created and given to the translations of the two sub-processes. A KillP process awaits on these two channels the rollback of the two sub-processes, in order to notify its rollback by sending the entire parallel process along its key channel. This is why we use binary join patterns (the translation of triggers uses binary join patterns too).

**Example 2 (Rollback of a parallel process).** Let us consider the parallel composition of two messages $k : (a\langle P \rangle | b\langle Q \rangle)$. We have that

$$ (k : (a\langle P \rangle | b\langle Q \rangle)) = (h)(\mathbf{Par}((a\langle P \rangle) (b\langle Q \rangle) h)k \Rightarrow \\ \nu l, r. (a\langle P \rangle)l | (b\langle Q \rangle)r | (l(W) | r(Z) \triangleright k\langle \mathbf{Par} W Z k \rangle | \mathbf{Rew} k) $$

where $l, r$ are, respectively, the left and the right process key. If both $(a\langle P \rangle)l$ and $(b\langle Q \rangle)r$ rollback (as shown in Example 1), that is

$$ (a\langle P \rangle)l \Rightarrow l\langle (h_1)\mathbf{Msga}((P)h_1) \mid \mathbf{Rew}l \\ (b\langle Q \rangle)r \Rightarrow r\langle (h_2)\mathbf{Msgb}((Q)h_2) \mid \mathbf{Rew}r $$

we have that the parallel composition can rollback too:

$$ l\langle (h_1)\mathbf{Msga}((P)h_1) \mid \mathbf{Rew}l | r\langle (h_2)\mathbf{Msgb}((Q)h_2) \mid \mathbf{Rew}r | \\ (l(W) | r(Z) \triangleright k\langle (h)\mathbf{Par} W Z h \rangle | \mathbf{Rew}k) \rightarrow \\ k\langle (h)\mathbf{Par}((h_1)\mathbf{Msga}((P)h_1) ((h_2)\mathbf{Msgb}((Q)h_2) h) \rangle | \mathbf{Rew}k | \mathbf{Rew}l | \mathbf{Rew}r $$

Note that $(h_1)\mathbf{Msga}((P)h_1 = (a\langle P \rangle)l$ and $(h_2)\mathbf{Msgb}((Q)h_2 = (b\langle Q \rangle)r$, hence we have $k\langle (h)\mathbf{Par}((h_1)\mathbf{Msga}((P)h_1) ((h_2)\mathbf{Msgb}((Q)h_2) h) = k\langle (a\langle P \rangle | b\langle Q \rangle)r$.

The translation of a trigger $l : a(X) \triangleright Q$ is a process of the form:

$$ \nu t. \bar{t} | (a(X, h) | t \triangleright_f \nu k, c. (Y X c) | (c(Z) \triangleright (Z k)) | (\mathbf{Mem} Y a X h k l)) | \\ (\mathbf{KillT} Y t l a) $$

with $Y = ((X c)c\langle (Q) \rangle)$. Here, a token $\bar{t}$ is used as a lock. Indeed either the trigger itself or its killer can acquire this lock and then execute, thus
leaving the other process blocked forever. The token allows us to avoid to use primitives such as passivation (see [36, 37]) or mixed choice to kill input processes. Since all the messages on channel $a \in \mathcal{N}$ are translated into bi-adic messages, triggers are translated in order to read such messages. The continuation of a translated trigger mimics the rho$\pi$ forward rule: it creates a new key channel $k$, and it substitutes the process variable $X$ with the message content (which is an abstraction) in the trigger continuation. This substitution is performed by the application $(Y X c)$. A memory process Mem is also created.

**Example 3 (Encoding of a communication).** Let us show how a communication is mimicked by the encoding. Take a configuration $M = k_1 : a(P) | k_2 : a(X) \triangleright Q$. We want to match the forward reduction $M \to \nu k \cdot k : Q^{\{P\}/X} | [M; k]$. With $Y = ((X c)c(\langle Q \rangle))$, we have that:

$$ 
\begin{aligned}
(\langle M \rangle) &= (\langle k_1 : a(P) \rangle) | (\langle k_2 : a(X) \triangleright Q \rangle) = (\langle a(P) \rangle)_{k_1} | (\langle a(X) \triangleright Q \rangle)_{k_2} = \\
&= (l)(\mathbf{Msg} a (\langle P \rangle) l)_{k_1} | (l)(\mathbf{Trig} Y a l)_{k_2} \Rightarrow \\
&= a(\langle P \rangle), k_1 \rangle | (\mathbf{KillM} a k_1) | (l)(\mathbf{Trig} Y a l)_{k_2} \Rightarrow \\
&= a(\langle P \rangle), k_1 \rangle | (\mathbf{KillM} a k_1) | \nu t. \bar{t} | \\
&= (a(X, h) | t \triangleright_f \nu k, c. (Y X c) | (c(Z) \triangleright (Z k)) | (\mathbf{Mem} Y a X h k k_2)) | \\
&\qquad (\mathbf{KillT} Y t k_2 a)
\end{aligned}
$$

Messages $\bar{t}$ and $a(\langle P \rangle), k_1 \rangle$ can interact with the process $(a(X, h) | t \triangleright_f R)$, leading to:

$$ 
\begin{aligned}
\nu t, k, c. (Y (\langle P \rangle) c) | (c(Z) \triangleright (Z k)) | (\mathbf{Mem} Y a (\langle P \rangle) k_1 k k_2) | \\
(\mathbf{KillM} a k_1) | (\mathbf{KillT} Y t k_2 a)
\end{aligned}
$$

By performing the application $(Y (\langle P \rangle) c)$ we obtain:

$$ 
\begin{aligned}
\nu t, k, c. c(\langle Q \rangle)\{\langle P \rangle / X\} \rangle | (c(Z) \triangleright (Z k)) | (\mathbf{Mem} Y a (\langle P \rangle) k_1 k k_2) | \\
(\mathbf{KillM} a k_1) | (\mathbf{KillT} Y t k_2 a)
\end{aligned}
$$

As one can see, the application above mimics the substitution $Q^{\{P\}/X}$. This is possible since the variable $X$ is free in $Q$ and consequently in $\langle Q \rangle$.

The next step is a communication on channel $c$. This is needed in order to instantiate the process $\langle Q \rangle\{\langle P \rangle / X\}$ with its channel key $k$, and leads to:

$$ 
\begin{aligned}
\nu t, k. \langle Q \rangle\{\langle P \rangle / X\} k | (\mathbf{Mem} Y a (\langle P \rangle) k_1 k k_2) | (\mathbf{KillM} a k_1) | (\mathbf{KillT} Y t k_2 a)
\end{aligned}
$$
Let us compare the process above with the corresponding rhoπ configuration, $νk.k: Q^{P/X} | [M;k]$. The process $(Q|^{(P)}/X)k$ is the translation of $k: Q^{P/X}$. Memory $[M;k]$ is represented by the process $(Mem((Xc)c((P|))a(P|)k_1 k_2)$. The processes $(KillM a k_1)$ and $(KillT Y tk_2 a)$ are garbage generated by the translation.

We show now how triggers rollback.

**Example 4 (Rollback of a trigger).** Let us consider the configuration $k_1: a(X)▷P$. With $Y = ((Xc)c((P|))$, we have that

$$ \begin{align*} (k_1 : a(X) \triangleright P) &= (a(X) \triangleright P)k_1 \rightarrow (\text{Trig } Y a k_1) \Rightarrow \\ & \nu t. \bar{t} | (\text{KillT } Y t k_1 a) | \\ & (a(X, h) | t \triangleright_f \nu k, c. (Y X c) | (c(Z) \triangleright (Z k)) | (\text{Mem } Y a X h k k_1)) \Rightarrow \\ & \nu t. \bar{t} | (t \triangleright k_1 \langle (h)(\text{Trig } Y a h) \rangle | \text{Rew } k_1) | \\ & (a(X, h) | t \triangleright_f \nu k, c. (Y X c) | (c(Z) \triangleright (Z k)) | (\text{Mem } Y a X h k k_1)) \rightarrow \\ & \nu t. (a(X, h) | t \triangleright_f \nu k, c. (Y X c) | (c(Z) \triangleright (Z k)) | (\text{Mem } Y a X h k k_1)) | \\ & k_1 \langle (h)(\text{Trig } Y a h) \rangle | \text{Rew } k_1 \end{align*} $$

Note that the process $\nu t. (a(X, h) | t \triangleright_f R)$ is now deadlocked, since $\bar{t}$ is no more available after the KillT consumed it. Thus we can consider it as garbage. Instead, the process $k_1 \langle (h)(\text{Trig}((Xc)c((P|))ah) \rangle$ is $k_1 \langle (a(X) \triangleright P) \rangle$ as required.

Let us now describe the encoding of configurations given in Figure 8. A null configuration **0** is encoded as the null HOπ⁺ process **0**. The parallel and the restriction operator are mapped to the corresponding operators of HOπ⁺. There are two ways of encoding a tagged process $κ: P$, depending on whether $κ$ is a key or a complex tag. If $κ$ is a key $k$, then the translation is the application of the encoding of $P$ to the name $k$, that is $((P|)k$. If $κ$ is a complex tag, of the form $\langle h_i, \tilde{h} \rangle \cdot k$, then the translation is the application of the translation of $P$ to the name $h_i$, in parallel with the killer of the complex tag. We want to generate at once a tree of killer processes able to revert an entire parallel composition made of $n$ elements, with $n$ being the size of $\tilde{h}$. The tree has root in $k$ and leaves in $h_1, \dots, h_n$. We opt for the translation of $\langle h_1, \tilde{h} \rangle \cdot k$ to generate it. Said otherwise, a killer of a complex tag $\langle h_i, \tilde{h} \rangle \cdot k$ is the null process if $i \neq 1$, otherwise it is a parallel composition of killer
processes able to rollback all the branches in which the key $k$ has been split. Hence, the killer of the complex tag $\langle h_1, \tilde{h} \rangle \cdot k$ is in charge of mimicking the behavior of the $rho\pi$ structural rule E.TAGP (see Figure 2 in Section 2.3) used (from right to left) to rebuild a tagged parallel composition from a parallel composition of related threads.

**Example 5 (Rollback of a parallel configuration).** Let us consider the following configuration (with $\tilde{h} = \{h_1, h_2, h_3\}$):

$$M = \langle h_1, \tilde{h} \rangle \cdot k : a\langle \mathbf{0} \rangle | \langle h_2, \tilde{h} \rangle \cdot k : b\langle \mathbf{0} \rangle | \langle h_3, \tilde{h} \rangle \cdot k : c\langle \mathbf{0} \rangle$$

and consider its translation:

$$\langle a\langle \mathbf{0} \rangle \rangle h_1 | \text{KillP}_{\langle h_1, \tilde{h} \rangle \cdot k} | \langle b\langle \mathbf{0} \rangle \rangle h_2 | \text{KillP}_{\langle h_2, \tilde{h} \rangle \cdot k} | \langle c\langle \mathbf{0} \rangle \rangle h_3 | \text{KillP}_{\langle h_3, \tilde{h} \rangle \cdot k} = \\ \langle a\langle \mathbf{0} \rangle \rangle h_1 | \text{KillP}_{\langle h_1, \tilde{h} \rangle \cdot k} | \langle b\langle \mathbf{0} \rangle \rangle h_2 | \langle c\langle \mathbf{0} \rangle \rangle h_3$$

since $\text{KillP}_{\langle h_2, \tilde{h} \rangle \cdot k} = \mathbf{0}$ and $\text{KillP}_{\langle h_3, \tilde{h} \rangle \cdot k} = \mathbf{0}$. From the examples above we know that a message can rollback, so we have

$$\langle a\langle \mathbf{0} \rangle \rangle h_1 \Rightarrow h_1\langle (h)\text{Msg a } (\mathbf{0}) \rangle h_1 | \text{Rew } h_1 \\ \langle b\langle \mathbf{0} \rangle \rangle h_2 \Rightarrow h_2\langle (h)\text{Msg b } (\mathbf{0}) \rangle h_2 | \text{Rew } h_2 \\ \langle c\langle \mathbf{0} \rangle \rangle h_3 \Rightarrow h_3\langle (h)\text{Msg c } (\mathbf{0}) \rangle h_3 | \text{Rew } h_3$$

From the definition of the translation we have $\text{KillP}_{\langle h_1, \tilde{h} \rangle \cdot k} = (\text{KillP} h_1 l_1 k) | (\text{KillP} h_2 h_3 l_1)$, with

$$(\text{KillP} h_1 l_1 k) = h_1(W) | l_1(Z) \triangleright k\langle (h)\text{Par } W \ Z \ h \rangle | \text{Rew } k \\ (\text{KillP} h_2 h_3 l_1) = h_2(W) | h_3(Z) \triangleright l_1\langle (h)\text{Par } W \ Z \ h \rangle | \text{Rew } l_1$$

By executing the reductions above we reach the following process

$$h_1\langle (h)\text{Msg a } (\mathbf{0}) \rangle h_1 | h_2\langle (h)\text{Msg b } (\mathbf{0}) \rangle h_2 | h_3\langle (h)\text{Msg c } (\mathbf{0}) \rangle h_3 \\ (h_1(W) | l_1(Z) \triangleright k\langle (h)\text{Par } W \ Z \ h \rangle | \text{Rew } k) | \\ (h_2(W) | h_3(Z) \triangleright l_1\langle (h)\text{Par } W \ Z \ h \rangle | \text{Rew } l_1) | \prod_{h_i \in \tilde{h}} \text{Rew } h_i$$

Note that there are two messages on channels $h_2$ and $h_3$. Thus a communication with trigger $h_2(W) | h_3(Z) \triangleright R$ can occur, leading to the following process:

$$h_1\langle (h)\text{Msg a } (\mathbf{0}) \rangle h_1 | (h_1(W) | l_1(Z) \triangleright k\langle (h)\text{Par } W \ Z \ h \rangle | \text{Rew } k) | \\ l_1\langle (h)\text{Par } (h)\text{Msg b } (\mathbf{0}) \rangle h_1 ((h)\text{Msg c } (\mathbf{0}) \rangle h_1) | \text{Rew } l_1 | \prod_{h_i \in \tilde{h}} \text{Rew } h_i$$
Let $S = ((h)\mathbf{Par}((h)\mathbf{Msg}b(\mathbf{0})h)((h)\mathbf{Msg}c(\mathbf{0})h)h)$, i.e. the translation of the parallel composition of messages on $b$ and $c$. By performing the communication on $h_1$ and $l_1$ we get:

$$k\langle (h)\mathbf{Par}((h)\mathbf{Msg}a(\mathbf{0})h)S h\rangle | \mathbf{Rew}k | \mathbf{Rew}l_1 | \prod_{h_i \in \tilde{h}} \mathbf{Rew}h_i$$

where the content of the message on $k$ is $\langle a\langle\mathbf{0}\rangle | b\langle\mathbf{0}\rangle | c\langle\mathbf{0}\rangle\rangle$ as required.

The **Mem** process mimics the backward rule of rhoπ: it awaits the rollback of its continuation (a message on the key channel $k$ that the memory bears) and then it releases again the translations of the original rhoπ message and trigger who gave rise to the communication (and to the memory).

**Example 6 (Backward reduction).** Consider the following configuration: $M = k : b\langle\mathbf{0}\rangle | [k_1 : a\langle\mathbf{Q}\rangle | k_2 : a(X)\triangleright b\langle\mathbf{0}\rangle; k]$. We have that $M \rightsquigarrow k_1 : a\langle\mathbf{Q}\rangle | k_2 : a(X)\triangleright b\langle\mathbf{0}\rangle$. Let us consider the encoding of $M$:

$$\langle\mathbf{M}\rangle = \langle\langle b\langle\mathbf{0}\rangle\rangle\rangle k | (\mathbf{Mem}((X c)c\langle\langle b\langle\mathbf{0}\rangle\rangle\rangle) a \langle\mathbf{Q}\rangle k_1 k_2)$$

since $\mathbf{Kill}_{k_1} = \mathbf{0}$ and $\mathbf{Kill}_{k_2} = \mathbf{0}$. If $\langle\langle b\langle\mathbf{0}\rangle\rangle\rangle k_1$ rollbacks we have:

$$\langle\mathbf{b}\langle\mathbf{0}\rangle\rangle k \Rightarrow k\langle (h)\mathbf{Msg}b(\mathbf{0})h\rangle | \mathbf{Rew}k$$

Thus:

$$\langle\mathbf{M}\rangle \Rightarrow k\langle (h)\mathbf{Msg}b(\mathbf{0})h\rangle | \mathbf{Rew}k | (\mathbf{Mem}((X c)c\langle\langle b\langle\mathbf{0}\rangle\rangle\rangle) a \langle\mathbf{Q}\rangle k_1 k_2) \rightarrow k\langle (h)\mathbf{Msg}b(\mathbf{0})h\rangle | \mathbf{Rew}k | (k(Z)\triangleright_b (\mathbf{Msg}a(P)k_1) | (\mathbf{Trig}(X c)c\langle\langle b\langle\mathbf{0}\rangle\rangle\rangle a k_2))$$

Since there is a message on $k$ (the rollback of the continuation of the trigger) the trigger $k(Z)\triangleright_b (\mathbf{Msg}...)$ | $(\mathbf{Trig}...)$ can consume it and re-instantiate the encoding of the message and of the trigger. We thus obtain the term:

$$(\mathbf{Msg}a(P)k_1) | (\mathbf{Trig}(X c)c\langle\langle b\langle\mathbf{0}\rangle\rangle\rangle a k_2) | \mathbf{Rew}k$$

The first part of the process is the translation of the original configuration $k_1 : a\langle\mathbf{P}\rangle | k_2 : a(X)\triangleright 0$ from which the communication took place, while $\mathbf{Rew}k$ is garbage.

Let us now explain the need for the **Rew** process, and the idea behind it. Killer processes allow a process to rollback, but we have to give also the possibility to *undo* a rollback decision. This is due to the fact that at any moment each process should be given both the possibility to go forward and to go backward. This is detailed in the example below.
**Example 7 (Why do we need Rew processes?).** Consider the configuration:

$$M = \langle h_1, \tilde{h} \rangle \cdot k : a \langle P \rangle | \langle h_2, \tilde{h} \rangle \cdot k : b \langle Q \rangle | k_1 : a(X) \triangleright \mathbf{0} | k_2 : b(X) \triangleright \mathbf{0}$$

Suppose that its translation does not include Rew processes. We then have, assuming $Y = ((X c)c(\langle \mathbf{0} \rangle))$:

$$\langle M \rangle = (l)(\mathbf{Msg} a (\langle P \rangle) l)h_1 | (l)(\mathbf{Msg} b (\langle Q \rangle) l)h_2 | \mathbf{KillP}_{\langle h_1, \tilde{h} \rangle \cdot k} | (l)(\mathbf{Trig} a Y l)k_1 | (l)(\mathbf{Trig} b Y l)k_2$$

Suppose now that the message on $a$ and the corresponding trigger interact:

$$\langle M \rangle \Rightarrow (\mathbf{KillM} a h_1) | (l)(\mathbf{Msg} b (\langle Q \rangle) l)h_2 | \mathbf{KillP}_{\langle h_1, \tilde{h} \rangle \cdot k} | (l)(\mathbf{Trig} b Y l)k_2 | \\ \nu t, k_3. (\mathbf{KillT} Y t k_1 a) | (\mathbf{Nil} k_3) | (\mathbf{Mem} Y a (\langle P \rangle) h_1 k_3 k_1)$$

Suppose now that the message on $b$ decides spontaneously to rollback. Since we are not considering Rew processes we have the following reduction:

$$(l)(\mathbf{Msg} b (\langle Q \rangle) l)h_2 \Rightarrow h_2 \langle (l)(\mathbf{Msg} b (\langle Q \rangle) l) \rangle$$

By combining the two sequences of reductions above we have:

$$\langle M \rangle \Rightarrow (\mathbf{KillM} a h_1) | h_2 \langle (l)(\mathbf{Msg} b (\langle Q \rangle) l) \rangle | \mathbf{KillP}_{\langle h_1, \tilde{h} \rangle \cdot k} | (l)(\mathbf{Trig} b Y l)k_2 | \\ \nu t, k_3. (\mathbf{KillT} Y t k_1 a) | (\mathbf{Nil} k_3) | (\mathbf{Mem} Y a (\langle P \rangle) h_1 k_3 k_1)$$

Now, the message on channel $b$, who started to rollback, cannot complete its rollback unless the communication on $a$ is undone, and cannot interact with the trigger waiting a message on $b$, since it already started to rollback. The Rew process is needed exactly in this case, allowing the message on $b$ to stop rolling back and compute forward again, performing the communication on $b$. Indeed, by adding a process Rew $h_2$ to the above configuration we enable the following computation:

$$\begin{align*}
(\mathbf{KillM} a h_1) | h_2 \langle (l)(\mathbf{Msg} b (\langle Q \rangle) l) \rangle | \mathbf{Rew} h_2 | \mathbf{KillP}_{\langle h_1, \tilde{h} \rangle \cdot k} | (l)(\mathbf{Trig} b Y l)k_2 | \\
\nu t, k_3. (\mathbf{KillT} Y t k_1 a) | (\mathbf{Nil} k_3) | (\mathbf{Mem} Y a (\langle P \rangle) h_1 k_3 k_1) &\Rightarrow \\
(\mathbf{KillM} a h_1) | (l)(\mathbf{Msg} b (\langle Q \rangle) l)h_2 | \mathbf{KillP}_{\langle h_1, \tilde{h} \rangle \cdot k} | (l)(\mathbf{Trig} b Y l)k_2 | \\
\nu t, k_3. (\mathbf{KillT} Y t k_1 a) | (\mathbf{Nil} k_3) | (\mathbf{Mem} Y a (\langle P \rangle) h_1 k_3 k_1) &\Rightarrow \\
(\mathbf{KillM} a h_1) | (\mathbf{KillM} b h_2) | \mathbf{KillP}_{\langle h_1, \tilde{h} \rangle \cdot k} | \\
\nu t, k_3. (\mathbf{KillT} Y t k_1 a) | (\mathbf{Nil} k_3) | (\mathbf{Mem} Y a (\langle P \rangle) h_1 k_3 k_1) &\Rightarrow \\
\nu t_1, k_4. (\mathbf{KillT} Y t_1 k_2 b) | (\mathbf{Nil} k_4) | (\mathbf{Mem} Y b (\langle Q \rangle) h_2 k_4 k_2) &
\end{align*}$$

which executes the communication on channel $b$.
In general, if one branch decides (spontaneously) to rollback (by interact-
ing with its killer process) while the other branches do not, then the process
rolled back would be stuck unless we add the possibility to undo its rollback
decision. This is the purpose of a process of the form (*Rew l*), whose behavior
is to read an abstraction carried in a message on the key channel *l* and then
to re-instantiate the abstraction with the same key. Naturally this makes the
encoding divergent, but, as already discussed, divergence is quite natural in
a reversible calculus. Thus the issue is not particularly relevant.

The next sections are devoted to prove that the encoding is faithful, i.e.
that it preserves the semantics of the original rhoπ configuration (proofs not
in the main part can be found in Appendix C). More precisely, we will prove
the following theorem.

**Theorem 3 (Faithfulness).** For any closed rhoπ process P, νk. k : P ≈ (νk. k : P).

Before proving the theorem we give a brief outline of our proof strategy.

PROOF OUTLINE. The main steps of the proof are the following:

* Since bfa barbed bisimilarity $\approx$ (Definition 6) distinguishes three kinds of reductions, backward, forward and administrative, we partition the reductions performed by the encoding into these three kinds (Definition 15).

* We characterize the garbage processes generated by the encoding with the function addG (Definition 17).

* We give a notion of normal form on HO$\pi^+$ processes (Definition 18). A process is in normal form if all the enabled applications have been executed.

* We define a structural congruence $\equiv_{Ex}$ on HO$\pi^+$ processes extending $\equiv$ (Definition 20), to ensure that translations of structurally congruent rho$\pi$ configurations are structurally congruent.

* We show that each process in the translation can send itself on its key channel (Lemma 23).

* We prove a kind of Loop Lemma for administrative reductions (Lemma 29).
* We show that each reduction of a rhoπ process can be matched by the translation (Theorem 4).

* We show that garbage has no impact on bfa barbed bisimilarity (Lemma 33).

* We show that $\equiv_{Ex}$ is a bfa barbed bisimulation (Proposition 1).

* We show that forward and backward steps of the translation are caused by forward and backward steps of the translated configuration (Lemma 36 and Lemma 37).

* We compose all the pieces to prove our main result.

### 4.3. Auxiliary relations

This section provides four main tools needed for proving the faithfulness of the encoding: (i) the reduction system giving to the translation a backward, forward and administrative structure, (ii) a characterization of the garbage added by the machinery in the translation, (iii) a normal form for $HO_\pi^+$ processes, and (iv) a congruence on $HO_\pi^+$ processes mimicking the one of rhoπ.

To give a backward, forward and administrative structure to the set of reductions of the translation we classify the reductions into backward, forward and administrative. The basic idea is that administrative reductions are neither forward nor backward, and complement both of them. Remember that in $HO_\pi^+$ we have two kinds of reductions: applications and communications. Applications are always administrative reductions. Communications can be either backward, forward or administrative according to the involved trigger. To distinguish the triggers, we decorate them with labels. The labels have no effect on the operational semantics of the calculus.

**Definition 14 (Labelled trigger).** A labelled trigger is a term of the form $J \vdash_b P$ or $J \vdash_f P$. They are called backward trigger and forward trigger, respectively.

Note that, in the translation of processes (Figure 7), the trigger inside the translation of a rhoπ trigger is forward, while the one inside the translation of a memory is backward.

From now on $\mathcal{R}$? will denote the reflexive closure of a relation $\mathcal{R}$, and $\mathcal{R}^*$ its reflexive and transitive closure. We now define the three reduction relations, backward $\rightsquigarrow$, forward $\rightarrow$, and administrative $\hookrightarrow$ on $HO_\pi^+$ processes.
**Definition 15 (Backward, forward and admin. HOπ⁺ reductions).**

Let $\rightarrow$ and $\rightsquigarrow$ denote HOπ⁺ reductions involving a forward and a backward trigger, respectively. Let $\mapsto$ denote HOπ⁺ reductions involving non-labelled triggers and $\rightarrow$ denote HOπ⁺ applications. Moreover, let administrative reductions be $\leftrightarrow=\mapsto \cup \rightarrow$. We define $\Rightarrow_f = \leftrightarrow^* \rightarrow \leftrightarrow^*$$ and $\Rightarrow_b = \leftrightarrow^* \leftrightarrow \Rightarrow^*$.

To prove our main result, one cannot simply prove that given a (consistent) configuration $M$, if $M \rightarrow M'$ then $(M) \Rightarrow_f (M')$, and similarly for backward reductions. In fact, this does not hold, since the results of the translation produce some garbage (in terms of additional processes) during the execution, and since structural congruent rhoπ processes do not always have structural congruent translations. Thus we need some auxiliary machinery to solve these issues.

First, we introduce a notion of *consistent* HOπ⁺ process, a process obtained by letting a process of the form $((\nu k. k : R))$ compute.

**Definition 16 (Consistent process).** A HOπ⁺ process $P$ is consistent if there is a rhoπ process $R$ such that $((\nu k. k : R)) \Rightarrow_P R$.

We note that all the applications in the encoding have the form below.

**Lemma 12 (Form of the applications in the encoding).**

Let $P$ be a consistent HOπ⁺ process. Each application in $P$ is either of the form $(h)P v$ or of the form $(X)P (Q)$ for some rhoπ process $Q$, or of the form $(X)P ((Z c)c\langle(Q)\rangle)$ for some rhoπ process $Q$. In this last case $(X)P$ is *Trig*, *KillT* or *Mem*.

**PROOF.** By inspection of the encoding definition. $\square$

<figure><img src="image_4.png" /></figure>

Then, we characterize the garbage produced by the translation by defining a function `addG(P)` allowing to add arbitrary garbage to a HOπ⁺ process `P`.

**Definition 17 (Garbage).** Let $P$ be a HOπ⁺ process such that $P \equiv \nu\tilde{a}. P'$. Then, $\text{addG}(P) = \{P_G \mid P_G \equiv \nu\tilde{a}. (P' \mid \nu\tilde{b}. Q)\}$, where $Q$ is a parallel composition (possibly empty) of processes of one of the forms below, or obtained from them by applications:

Rewl

$\nu c, t. (\text{KillT}((X)c\langle(P)\rangle) \text{ t l a})$

KillM a l

$\nu t. (a(X, k)|t \triangleright S)$
In the definition above, we have two kinds of garbage. Processes of the form $\nu c, t$. (KillT $((X)c\langle(\|P\|)\rangle)$ $t$ $l$ $a$) and $\nu t$. $(a(X, k)|t \triangleright S)$ are blocked (but for an application inside the first one), since the name $t$ is restricted and the token $\bar{t}$ has been consumed.

Let us see an example of how such garbage is generated.

**Example 8 (Generating garbage).** Consider the reductions below, where $Q = \nu l, c. (Y X c) | (c(Z) \triangleright Z l) | (\text{Mem } Y a X h l k)$ and $Y = (X c)c\langle(\|0\|)\rangle$. The translation of a trigger $k : a(X) \triangleright 0$ begins a rollback:

$$ (k : a(X) \triangleright 0) = (a(X) \triangleright 0)k = ((h)\text{Trig } Y a h) k \rightarrow (\text{Trig } Y a k) \Rightarrow \\ \nu t. \bar{t} | (a(X, h)|t \triangleright Q) | (t \triangleright k\langle(h)\text{Trig } Y a h\rangle | (\text{Rev } k)) \rightarrow \\ \nu t. (a(X, h)|t \triangleright Q) | k\langle(h)\text{Trig } Y a h\rangle | (\text{Rev } k) $$

Now, the trigger undoes its rollback decision thanks to the process (Rev $k$):

$$ \nu t. (a(X, h)|t \triangleright Q) | k\langle(h)\text{Trig } Y a h\rangle | (\text{Rev } k) \rightarrow \\ \nu t. (a(X, h)|t \triangleright Q) | k\langle(h)\text{Trig } Y a h\rangle | (k(Z) \triangleright Z k) \rightarrow \\ \nu t. (a(X, h)|t \triangleright Q) | ((h)\text{Trig } Y a h) k = R $$

The process $\nu t. (a(X, h)|t \triangleright Q)$ is indeed garbage, in fact we have $R \in \text{addG}(((h)\text{Trig } Y a h) k) = \text{addG}((k : a(X) \triangleright 0))$.

Processes of the form (Rev $l$) and (KillM $a$ $l$) are not blocked, but they are redundant. Indeed, we will show in Lemma 16 and Lemma 17 that such processes are always available when needed. However, additional copies, which have no impact on the behavior of the translation, may be created (see, e.g., Example 3 and Example 6).

We now define a notion of normal form for processes, corresponding to processes where all the enabled applications have been executed. Thus, a process in normal form has no enabled applications.

**Definition 18 (Normal form).** The function $nf(\cdot)$ from $\mathcal{P}_{\text{HO}\pi^+}$ to $\mathcal{P}_{\text{HO}\pi^+}$ computing the normal form of a given HO$\pi^+$ process is defined as follows:

$$ \text{nf}(\nu u. P) = \nu u. \text{nf}(P) $$

$$ \text{nf}(a\langle P\rangle) = a\langle P\rangle $$

$$ \text{nf}((X)P Q) = \text{nf}(P\{Q/X\}) $$

$$ \text{nf}(0) = 0 $$

$$ \text{nf}(P | Q) = \text{nf}(P) | \text{nf}(Q) $$

$$ \text{nf}(a(X) \triangleright P) = a(X) \triangleright P $$

$$ \text{nf}((h)P l) = \text{nf}(P\{l/h\}) $$
Note that, since reduction to normal form corresponds to execute some enabled applications, for each $P$, $P \to^* \mathbf{nf}(P)$. For the same reason, the reduction to normal form is the identity on triggers and messages.

We extend the congruence $\equiv$ on $\mathbf{HO}\pi^+$ processes to match the effect of $\mathbf{rho}\pi$ structural congruence after the translation, in order to show that congruent $\mathbf{rho}\pi$ processes are translated into congruent $\mathbf{HO}\pi^+$ processes.

**Definition 19.** Let $\equiv_{Ax}$ be the smallest congruence on $\mathbf{HO}\pi^+$ processes satisfying the rules for structural congruence $\equiv$ plus the axioms below.

$$ (\mathbf{Ax.C}) \quad \mathbf{KillP} l h k \equiv_{Ax} \mathbf{KillP} h l k $$

$$ (\mathbf{Ax.A}) \qquad \begin{array}{l} \nu l'. (\mathbf{KillP} l_1 l_2 l') | (\mathbf{KillP} l' l_3 l) \equiv_{Ax} \\ \qquad \nu l'. (\mathbf{KillP} l_1 l' l) | (\mathbf{KillP} l_2 l_3 l') \end{array} $$

$$ (\mathbf{Ax.P}) \quad l_1 \langle (P) \rangle | l_2 \langle (Q) \rangle | \mathbf{KillP} l_1 l_2 l \equiv_{Ax} l \langle (h) \mathbf{Par} (P) (Q) h \rangle | \mathbf{Rew} l $$

$$ (\mathbf{Ax.ADM}) \quad \nu C. (c \langle (P) \rangle | c(Z) \triangleright (Z k)) \equiv_{Ax} (P)k $$

**Definition 20.** Let $\equiv_{Ex}$ be the smallest congruence including for each axiom $L \equiv_{Ax} R$ in $\equiv_{Ax}$ both $L \equiv_{Ex} R$ and $\mathbf{nf}(L) \equiv_{Ex} \mathbf{nf}(R)$.

Axioms $\mathbf{Ax.C}$ and $\mathbf{Ax.A}$ extend respectively the commutativity and associativity of the parallel composition operator to the translation. Note that $\alpha$-conversion is not enough to simulate axiom $\mathbf{Ax.C}$. Indeed, if we have $\nu l, h. (\mathbf{KillP} l h k) | (P_1)l | (P_2)h$, we can $\alpha$-convert the term to have $\nu l, h. (\mathbf{KillP} h l k) | (P_1)h | (P_2)l$, but not $\nu l, h. (\mathbf{KillP} h l k) | (P_1)l | (P_2)h$ as we can derive with $\mathbf{Ax.C}$. Also, axioms $\mathbf{Ax.C}$ and $\mathbf{Ax.A}$ cannot be mimicked by administrative reductions since the left- and the right-hand-side do not reduce to each other. Axioms $\mathbf{Ax.P}$ and $\mathbf{Ax.ADM}$, applied from left to right, capture the effect of some administrative reductions.

We show now a few properties of the relations defined above.

The congruence $\equiv_{Ex}$ captures the effect of $\mathbf{rho}\pi$ structural congruence $\equiv$ on normal form of translations.

**Lemma 13.** Let $M, N$ be closed consistent $\mathbf{rho}\pi$ configurations. Then $M \equiv N$ implies $\mathbf{nf}((M)) \equiv_{Ex} \mathbf{nf}((N))$.

**PROOF.** By induction on the derivation of $M \equiv N$. The proof is in Appendix C.1. $\square$
Structural congruence $\equiv_{Ex}$ is preserved by normal form.

**Lemma 14.** If P and Q are consistent HO$\pi^+$ processes and $P \equiv_{Ex} Q$ then $nf(P) \equiv_{Ex} nf(Q)$.

The congruence $\equiv_{Ex}$ is not influenced by garbage introduced by function `addG(•)`.

**Lemma 15.** If $nf(P) \equiv_{Ex} nf(P')$ then for each $Q \in \text{addG}(P)$ there exists $Q' \in \text{addG}(P')$ such that $nf(Q) \equiv_{Ex} nf(Q')$.

We now prove two invariants on the form of consistent HO$\pi^+$ processes, useful to study properties of the function `addG(•)`.

For each message on a key channel $l$ contained in a translation, there is also a corresponding process `Rew l` (or the process $l(Z) \triangleright Z l$ obtained by performing the application).

**Lemma 16 (Rew Invariant).** If P is a consistent HO$\pi^+$ process and $P \equiv \mathbb{C}[l\langle R \rangle, \dots, l\langle R \rangle]$ with $l \in K$ for some n-ary context $\mathbb{C}$ then $P \equiv \mathbb{C}'[l\langle R \rangle | S_1, \dots, l\langle R \rangle | S_n]$ for some n-ary context $\mathbb{C}'$ with, for each $i \in \{1, \dots, n\}$, $S_i = \text{Rew } l$ or $S_i = l(Z) \triangleright Z l$.

For each message on a channel $a \in \mathcal{N}$ contained in the translation, there is also a corresponding process `KillM` (or the process obtained by performing the application).

**Lemma 17 (KillM Invariant).** If P is a consistent HO$\pi^+$ process and $P \equiv \mathbb{C}[a\langle\langle Q \rangle\rangle, l\rangle, \dots, a\langle\langle Q \rangle\rangle, l\rangle]$ with $a \in \mathcal{N}$ for some n-ary context $\mathbb{C}$ then $P \equiv \mathbb{C}'[a\langle\langle Q \rangle\rangle, l\rangle | S_1, \dots, a\langle\langle Q \rangle\rangle, l\rangle | S_n]$ for some n-ary context $\mathbb{C}'$ with, for each $i \in \{1, \dots, n\}$, $S_i = (\text{KillM } a \ l)$ or $S_i = (a(X, \setminus l) \triangleright l\langle\langle h \rangle\rangle \text{Msg } a \ X \ h\rangle | \text{Rew } l)$.

Function `addG(•)` does not add new behaviors.

**Lemma 18.** Let P be a consistent HO$\pi^+$ process and Q ∈ addG(P). If $nf(Q) \hookrightarrow Q'$ then there exists P' such that $P \hookrightarrow^* P'$ with $Q' \in addG(P')$.

**Lemma 19.** Let P be a consistent HO$\pi^+$ process and Q ∈ addG(P). If $nf(Q) \twoheadrightarrow Q'$ then there exists P' such that $P \twoheadrightarrow^* P'$ with $Q' \in addG(P')$.
**PROOF.** It is easy to see from the definition of function **addG** that the added processes cannot enable $\rightarrow$ reductions. Hence the reduction $\rightarrow$ can be done by **nf**(P), and it is sufficient to choose $P'$ such that $P \rightarrow^* \mathbf{nf}(P) \rightarrow P'$. $\square$

**Lemma 20.** Let P be a consistent HO$\pi^+$ process and $Q \in \mathbf{addG}(P)$. If $\mathbf{nf}(Q) \rightsquigarrow Q'$ then there exists $P'$ such that $P \rightarrow^{*\rightsquigarrow} P'$ with $Q' \in \mathbf{addG}(P')$.

**PROOF.** Similar to the one of Lemma 19. $\square$

### 4.4. Operational correspondence

This section proves a few results on the behavior of the translation, leading to the operational correspondence result at the end of the section.

We start by proving a few basic properties of the translation.

The encoding is well-behaved w.r.t. substitutions:

**Lemma 21 (Substitution).** For each pair of rho$\pi$ processes P, Q:
$$ (\mathcal{P})^{\{\mathcal{Q}\}/X} = (\mathcal{P}\{Q/X\}) $$

**PROOF.** By induction on the structure of P. $\square$

Names corresponding to keys in $\mathcal{K}$ are always bound.

**Lemma 22.** For each consistent HO$\pi^+$ process P, $\mathbf{fn}(P) \cap \mathcal{K} = \emptyset$.

**PROOF.** By definition of consistency there is a rho$\pi$ process Q such that $(\nu k \cdot k : Q) \Rightarrow P$. The proof is by induction on the number of steps in $\Rightarrow$. $\square$

We now prove that, essentially, a translation of a rho$\pi$ process P can always rollback, and the result of the rollback is a message on the process key channel. The rollback is not perfect, in the sense that the content of the message is not exactly equal to the translation of the original process P. This is due to the fact that, once a name has been created, there is no way to reverse its creation. However we can prove that the content of the message, wrapped by restrictions on extruded names, is structural congruent to the original process P, plus some garbage. Formally we have:

**Lemma 23.** For each closed rho$\pi$ process P, $(\mathcal{P})k \hookrightarrow^* \nu\tilde{u} \cdot k \langle (\mathcal{Q}) \rangle | S$ with $k \notin \tilde{u}$, $S = \coprod R_i$, $R_i = \text{Rew } k_i$ or $R_i = \text{Vt. } (a(X,h)|\mathbf{t} \triangleright R)$ and $P \equiv \nu\tilde{u} \cdot Q$.
Note that in the lemma above, $\nu\tilde{u}.k(\langle Q \rangle) | S \in \text{addG}(\nu\tilde{u}.k(\langle Q \rangle))$.

The encoding never generates two messages on the same key channel, never generates two **KillP** processes waiting for the same rollbacks and never generates a **KillP** and a **Mem** waiting for the same rollback.

**Lemma 24.** For any consistent $HO\pi^+$ process *P* the following conditions hold:

1. $P \not\equiv_C [l\langle P_1 \rangle | l\langle P_2 \rangle]$, with $l \in K$.

2. $P \not\equiv_C [(\text{KillP } l_1 l_2 l_3) | (\text{KillP } l_4 l_5 l_6)],$ with $l_1, l_2, l_3, l_4, l_5, l_6 \in K$ and $\{l_1, l_2\} \cap \{l_4, l_5\} \neq \emptyset$ or $l_3 = l_6$.

3. $P \not\equiv_C [(\text{KillP } l_1 l_2 l) | (\text{Mem } P \ a \ Q \ h \ l_3 k)],$ with $l, l_1, l_2, l_3, h, k \in K$ and $l_1 = l_3$ or $l_2 = l_3$.

Two applications can always be swapped.

**Lemma 25.** For each $HO\pi^+$ process *P*, if $P \to P_1$ and $P \to P_2$ (by executing two distinct applications) then there is a $HO\pi^+$ process $P_3$ such that $P_2 \to P_3$ and $P_1 \to P_3$.

More in general, applications can be swapped with arbitrary reductions:

**Lemma 26.** If $P \Rightarrow P'$ and $P \dashv^* P''$ then $P' \dashv^* Q$ and $P'' \Rightarrow Q$.

*PROOF.* By induction on the length of $\Rightarrow$ and $\dashv^*$, showing that if $P \to_P P'$ and $P \to_Q P''$ then $P'' \to_Q Q$ and $P' \to_Q Q$. $\square$

Processes congruent according to $\equiv_{Ex}$ have the same reductions, up to $\equiv_{Ex}$, administrative reductions and garbage.

**Lemma 27.** If $nf(P_1) \equiv_{Ex} nf(P_2)$ and $nf(P_1) \to P'_1$ then $nf(P_2) \Rightarrow nf(P'_2)$ with $nf(P_1'') \equiv_{Ex} nf(P_2')$ and $P_1'' \in \text{addG}(P_1')$. Furthermore, if $\to$ is forward then $\Rightarrow is \Rightarrow_f$, if $\to$ is backward then $\Rightarrow is \Rightarrow_b$, if $\to$ is administrative then $\Rightarrow is \dashv^*$.

*PROOF.* By case analysis on the used axiom $P \equiv_{Ex} Q$ and on the structure of $nf(P_1)$. The proof is in Appendix C.2. $\square$

We can generalize Lemma 27 to sequences of reductions as follows.
**Lemma 28.** If nf(P₁) ≡<sub>Ex</sub> nf(P₂) and nf(P₁) ⇒ P'₁ then nf(P₂) ⇒ nf(P'₂) with nf(P''₁) ≡<sub>Ex</sub> nf(P'₂) and P''₁ ∈ addG(P'₁). Furthermore, if the first ⇒ is is, ⇒<sub>f</sub>, ⇒<sub>b</sub> or ↪* then the second ⇒ is of the same form.

We now prove a form of Loop Lemma for administrative reductions. Hence, if P is a translation and P ↪* Q, Q can somehow go back to P. Reversibility of this computation is however not perfect, but it holds up to garbage and structural congruence ≡<sub>Ex</sub>.

**Lemma 29.** For each consistent HOπ⁺ process P if P ↪* Q then there exist Q' and P' such that Q ↪* Q', P' ∈ addG(P) with nf(P') ≡<sub>Ex</sub> nf(Q').

The next theorem proves a form of behavioral correctness for our encoding, showing that the encoding of a configuration can mimic the reductions of the encoded configuration.

**Theorem 4.** For each consistent rhoπ configuration M, if M → N then nf(|M|) ⇒<sub>f</sub> P and if M ↪ N then nf(|M|) ⇒<sub>b</sub> P, and there exists P' ∈ addG(|N|) such that nf(P) ≡<sub>Ex</sub> nf(P').

**PROOF.** By induction on the derivation of M → N, with a case analysis on the last rule applied.

**R.Fw:** we have that

$$M = \kappa_1 : a\langle P \rangle \mid \kappa_2 : a(X) \triangleright Q \rightsquigarrow \\ \nu k. (Q^{\{P/X\}} \mid [\kappa_1 : a\langle P \rangle \mid \kappa_2 : a(X) \triangleright Q ; k]) = N$$

Moreover we have that |M| = (|κ₁ : a(P)|) | (|κ₂ : a(X) ▷ Q|). We distinguish four cases, depending on whether κ₁, κ₂ are complex or not. Let us consider the case κ₁ = k₁ and κ₂ = k₂. Assume Y =
((X c) c⟨⟨Q⟩⟩). Then:

$$
\begin{align*}
\mathrm{nf}(\langle M \rangle) &= \mathrm{nf}((l)(\mathrm{Msg} a (\langle P \rangle) l)k_1) \mid \mathrm{nf}((l)(\mathrm{Trig} Y a l)k_2) = \\
&\quad \nu t. a\langle\langle P \rangle\rangle, k_1 \mid \mathrm{nf}(\mathrm{KillM} a k_1) \mid \bar{t} \mid \\
&\qquad (t|a(X, h) \triangleright_f \nu k, c. (Y X c) \mid (c(Z) \triangleright Z k) \mid (\mathrm{Mem} Y a X h k k_2)) \mid \\
&\qquad \mathrm{nf}(\mathrm{KillT} Y t k_1 a) \to \\
&\quad \nu c, k, t. \mathrm{nf}(\mathrm{KillM} a k_1) \mid (Y (\langle P \rangle) c) \mid (c(Z) \triangleright Z k) \mid (\mathrm{Mem} Y a X k_1 k k_2) \mid \\
&\qquad \qquad \mathrm{nf}(\mathrm{KillT} Y t k_2 a) \to \\
&\quad \nu c, k, t. \mathrm{nf}(\mathrm{KillM} a k_1) \mid c\langle\langle Q \rangle\rangle\{\langle^{(P)}\rangle/X\} \mid (c(Z) \triangleright Z k) \mid \\
&\qquad (\mathrm{Mem} Y a X k_1 k k_2) \mid \mathrm{nf}(\mathrm{KillT} Y t k_2 a) \to \\
&\quad \nu c, k, t. \mathrm{nf}(\mathrm{KillM} a k_1) \mid (\langle Q \rangle\{\langle^{(P)}\rangle/X\} k) \mid (\mathrm{Mem} Y a X k_1 k k_2) \mid \\
&\qquad \qquad \mathrm{nf}(\mathrm{KillT} Y t k_2 a) = R
\end{align*}
$$

By using Lemma 21 we have that ⟨Q⟩⟨⟨⟨P⟩⟩/X⟩ = ⟨Q{P}/X⟩, thus:

$$
R = \nu c, k, t. \mathrm{nf}(\mathrm{KillM} a k_1) \mid (\langle Q \{P \rangle / X \rangle) k) \mid \\
(\mathrm{Mem} Y a X k_1 k k_2) \mid \mathrm{nf}(\mathrm{KillT} Y t k_2 a)
$$

We can conclude by noting that:

$$
\mathrm{nf}(R) = \mathrm{nf}(\mathrm{KillM} a k_1) \mid \mathrm{nf}(\langle N \rangle) \mid \nu c, t. \mathrm{nf}(\mathrm{KillT} Y t k_2 a)
$$

Since $P' = (\text{KillM } a 
_k) \mid (\langle N \rangle) \mid \nu c, t. (\text{KillT } Y 
_t k_2 a) \in \text{addG}(\langle N \rangle)$
and $\text{nf}(R) \equiv_{Ex} \text{nf}(P')$ the thesis follows.

Let us consider the case in which $\kappa_1 = \langle h_i, \tilde{h} \rangle \cdot k$. We have that:

$$
(\langle M \rangle = (l)(\text{Msg } a \ (\langle P \rangle) l)h_i \mid \text{Kill}_{\langle h_i, \tilde{h} \rangle, k} \mid (l)(\text{Trig } Y a l)k_2
$$

Using the same reductions as above we have that:

$$
\begin{align*}
\mathrm{nf}(\langle M \rangle) &\Rightarrow_f \\
\nu c, k, t. \mathrm{nf}(\mathrm{KillM} a k_1) &\mid \mathrm{nf}(\mathrm{Kill}_{\langle h_i, \tilde{h} \rangle, k}) \mid (\langle Q \rangle \{\langle^{(P)}\rangle/X\} k) \mid \\
&\quad (\mathrm{Mem} Y a X h_i k k_2) \mid \mathrm{nf}(\mathrm{KillT} Y t k_2 a) = R
\end{align*}
$$

and by using Lemma 21 we have that

$$
R = \nu c, k, t. \mathrm{nf}(\mathrm{KillM} a h_i) \mid \mathrm{nf}(\mathrm{Kill}_{(h_i, \tilde{h}) \cdot k}) \mid (\langle Q \{\langle^{(P)}\rangle/X\} \rangle k) \mid \\
(\mathrm{Mem} Y a X h_i k k_2) \mid \mathrm{nf}(\mathrm{KillT} Y t k_2 a)
$$
We can conclude by noting that $P' = (\text{KillM } a \ h_i) \mid \text{Kill}_{\langle h_i, \tilde{h} \rangle \cdot k} \mid ((\langle Q \{\langle P \rangle \rangle_X \} \rangle k) \mid (\text{Mem } Y \ a \ X \ h_i \ k \ k_2) \mid \nu c, t. (\text{KillT } Y \ t \ k_2 \ a) \in \text{addG}(\langle N \rangle))$ and $\text{nf}(R) \equiv_{Ex} \text{nf}(P')$.

The two other cases are similar.

**R.Bw:** we have that $M = k : R \mid [\kappa_1 : a\langle P \rangle \mid \kappa_2 : a(X) \triangleright Q ; k] \rightsquigarrow \kappa_1 : a\langle P \rangle \mid \kappa_2 : a(X) \triangleright Q = N$. Assume that $Y = ((X c)c\langle\langle Q \rangle\rangle)$. Then, by definition of $\text{nf}(\bullet)$ we have:

$$ \begin{align*} \text{nf}(\langle M \rangle) &= \\ \text{nf}(\langle R \rangle k) &\mid \text{nf}(\text{Mem } Y \ a \ \langle P \rangle \ \langle \kappa_1 \rangle \ k \ \langle \kappa_2 \rangle) \mid \text{nf}(\text{Kill}_{\kappa_1}) \mid \text{nf}(\text{Kill}_{\kappa_2}) = \\ \text{nf}(\langle R \rangle k) &\mid (k(Z) \triangleright (\text{Msg } a \ \langle P \rangle \ \langle \kappa_1 \rangle)) \mid (\text{Trig } Y \ a \ \langle \kappa_2 \rangle)) \mid \text{Kill}_{\kappa_1} \mid \text{Kill}_{\kappa_2} \end{align*} $$

From Lemma 23 we know that $\langle R \rangle k \hookrightarrow^* \nu \tilde{u}. k\langle\langle R' \rangle\rangle \mid S$ with $S$ a parallel composition of garbage processes and $R \equiv \nu \tilde{u}. R'$. Thanks to Lemma 26 we have $\text{nf}(\langle R \rangle k) \hookrightarrow^* \nu \tilde{u}. k\langle\langle R' \rangle\rangle \mid \text{nf}(S)$. Hence:

$$ \begin{align*} \text{nf}(\langle R \rangle k) &\mid (k(Z) \triangleright (\text{Msg } a \ \langle P \rangle \ \langle \kappa_1 \rangle)) \mid (\text{Trig } Y \ a \ \langle \kappa_2 \rangle)) \mid \\ \text{nf}(\text{Kill}_{\kappa_1}) &\mid \text{nf}(\text{Kill}_{\kappa_2}) \hookrightarrow^* \\ \nu \tilde{u}. k\langle\langle R' \rangle\rangle &\mid \text{nf}(S) \mid (k(Z) \triangleright_b (\text{Msg } a \ \langle P \rangle \ \langle \kappa_1 \rangle)) \mid \\ &\quad (\text{Trig } Y \ a \ \langle \kappa_2 \rangle)) \mid \text{nf}(\text{Kill}_{\kappa_1}) \mid \text{nf}(\text{Kill}_{\kappa_2}) \rightsquigarrow \\ \nu \tilde{u}. (\text{Msg } a \ \langle P \rangle \ \langle \kappa_1 \rangle) &\mid (\text{Trig } Y \ a \ \langle \kappa_2 \rangle)) \mid \text{nf}(\text{Kill}_{\kappa_1}) \mid \text{nf}(\text{Kill}_{\kappa_2}) \mid \\ \text{nf}(S) &= R \end{align*} $$

We have that $P' = \nu \tilde{u}. (\text{Msg } a \ \langle P \rangle \ \langle \kappa_1 \rangle) \mid (\text{Trig } Y \ a \ \langle \kappa_2 \rangle) \mid \text{Kill}_{\kappa_1} \mid \text{Kill}_{\kappa_2} \mid S \in \text{addG}(\langle \kappa_1 : a\langle P \rangle \mid \kappa_2 : a(X) \triangleright Q \rangle))$ and $\text{nf}(R) \equiv_{Ex} \text{nf}(P')$ as desired.

**Equiv:** we have two cases, one for forward reductions and one for backward reductions. We consider the first one, the second being analogous. We have that $M \to N$ with hypothesis $M \equiv M'$, $M' \to N'$ and $N' \equiv N$. Figure 9 (numbers refers to the used lemmas, ind means that inductive hypothesis is applied and addG that garbage is added) shows the proof schema we use. By inductive hypothesis we have that $\text{nf}(\langle M' \rangle) \Rightarrow_f P$ with $\text{nf}(P) \equiv_{Ex} \text{nf}(R')$ and $R' \in \text{addG}(\langle N' \rangle)$. As a consequence also $\text{nf}(R') \in \text{addG}(\text{nf}(\langle N' \rangle))$. By Lemma 13, we have that if $M \equiv M'$ then $\text{nf}(\langle M \rangle) \equiv_{Ex} \text{nf}(\langle M' \rangle)$,
<figure><img src="image_5.png" /><figcaption>Figure 9: The encoding respects $\equiv_{Ex}$ (numbers refer to Lemmas).</figcaption></figure>

and by Lemma 28 we have that if $\mathbf{nf}(|M'|) \Rightarrow_f \mathbf{nf}(P)$ then there exists $Q$ such that $\mathbf{nf}(|M|) \Rightarrow_f \mathbf{nf}(Q)$ with $\mathbf{nf}(Q) \equiv_{Ex} \mathbf{nf}(P')$ with $P' \in \mathbf{addG}(P)$ (hence $\mathbf{nf}(P') \in \mathbf{addG}(\mathbf{nf}(P)))$. By inductive hypothesis we have that $\mathbf{nf}(P) \equiv_{Ex} \mathbf{nf}(R')$, but since by hypothesis we had $N' \equiv N$ by Lemma 13 we have that $\mathbf{nf}(|N'|) \equiv_{Ex} \mathbf{nf}(|N|)$ and by Lemma 15 we have that there exists $R \in \mathbf{addG}(|N|)$ (hence $\mathbf{nf}(R) \in \mathbf{addG}(\mathbf{nf}(|N|)))$ such that $\mathbf{nf}(R') \equiv_{Ex} \mathbf{nf}(R)$. Thanks to Lemma 15 there exists $P' \in \mathbf{addG}(P)$ (hence $\mathbf{nf}(P') \in \mathbf{addG}(\mathbf{nf}(P)))$ with $\mathbf{nf}(Q) \equiv_{Ex} \mathbf{nf}(P')$, and $R''' \in \mathbf{addG}(R') = \mathbf{addG}(|N'|)$ and $R'' \in \mathbf{addG}(R) = \mathbf{addG}(|N|)$ such that $\mathbf{nf}(P') \equiv_{Ex} \mathbf{nf}(R'') \equiv_{Ex} \mathbf{nf}(R'')$. We can conclude by saying that $\mathbf{nf}(|M|) \Rightarrow_f Q$ and that $\mathbf{nf}(Q) \equiv_{Ex} \mathbf{nf}(R'')$ with $R'' \in \mathbf{addG}(|N|)$, as desired.

**_Ctx:** by a simple induction on the structure of the context, noting that the translation of configuration contexts is isomorphic. $\square$

### 4.5. *Observations*

In this section we study the properties of the encoding from an observational point of view.

Barbs are preserved by administrative steps.
**Lemma 30.** If $M \downarrow_a$ and $|M| \to^* Q$ then $Q \to^* \downarrow_a$.

Barbs of translations are originated by barbs of the encoded configuration.

**Lemma 31.** If $|M| \to^* \downarrow_a$ then $M \downarrow_a$.

The function addG does not remove barbs, that is:

**Lemma 32.** If $P \to^* \downarrow_a$ then $\text{addG}(P) \to^* \downarrow_a$.

**PROOF.** Since $P \to^* P' \downarrow_a$, we can express $P$ as $\mathbb{E}[0]$ and $P'$ as $\mathbb{E}'[0]$ with $\mathbb{E}[0] \to^* \mathbb{E}'[0] \downarrow_a$. We can write any process in $\text{addG}(P)$ as $\mathbb{E}[R]$. We still have that $\mathbb{E}[R] \to^* \mathbb{E}'[R] \downarrow_a$, as desired. $\square$

Garbage has no impact on bfa barbed bisimilarity.

**Lemma 33.** For any consistent $\text{HO}\pi^+$ process $P$, the relation $\mathcal{R} = \{(P, R) \mid R \in \text{addG}(P)\}$ is a bfa barbed bisimulation.

Axioms in $\equiv$ are correct with respect to bfa barbed bisimilarity.

**Lemma 34.** The relation $\mathcal{R} = \{(P, Q) \mid P \equiv Q\}$ where $P, Q$ are $\text{HO}\pi^+$ processes is a bfa barbed bisimulation.

**PROOF.** By induction on the length of the derivation of $P \equiv Q$, with a case analysis on the last applied axiom. All the cases are easy. $\square$

The same holds for axioms in $\equiv_{Ex}$, when applied to consistent processes.

**Proposition 1.** The relation $\mathcal{R} = \{(P, Q) \mid P \equiv_{Ex} Q\}$ where $P, Q$ are consistent $\text{HO}\pi^+$ processes is a bfa barbed bisimulation.

### 4.6. Final proof

Before proving the theorem we show two results ensuring completeness of forward and backward transitions, respectively.

The first one relies on the result below.

**Lemma 35.** If $\text{nf}(|M|) \to P$ then $M \to M'$ with $P \to^* P'$ and $\text{nf}(P') \equiv \text{nf}(Q')$ and $Q' \in \text{addG}(|M'|)$.
<figure><img src="image_6.png" /><figcaption>Figure 10: Proof schema of the first part of Lemma 36</figcaption></figure>

**Lemma 36.** Let $M$ be a rho$\pi$ configuration. If $\langle|M|\rangle \hookrightarrow^* Q \to Q'$ then there are $M'$, $Q''$ and $Q'''$ such that $M \to M'$, $Q' \hookrightarrow^* Q''$ and $\mathrm{nf}(Q'') \equiv_{Ex} \mathrm{nf}(Q''')$ and $Q''' \in \mathrm{addG}(\langle|M'|\rangle)$.

**PROOF.** The proof schema of the first part of the proof is in Figure 10. Assume $\langle|M|\rangle \hookrightarrow^* Q \to Q'$. By definition of normal form we have $\langle|M|\rangle \to^* \mathrm{nf}(\langle|M|\rangle)$. Applying Lemma 26 to the two reduction sequences from $\langle|M|\rangle$ we have that there exists $Q_1$ with $\mathrm{nf}(\langle|M|\rangle) \to^* Q_1$ and $Q \to^* Q_1$. Moreover we have that $Q_1 \to^* \mathrm{nf}(Q_1)$ and since $\to^* \subseteq \to^*$ we also have $\mathrm{nf}(\langle|M|\rangle) \to^* \mathrm{nf}(Q_1)$. Since $Q \to Q'$ and $Q \to^* \mathrm{nf}(Q_1)$ by Lemma 26 we have that also $\mathrm{nf}(Q_1) \to Q_2$ for some $Q_2$ such that $Q' \to^* Q_2$. In order to apply Lemma 35 we have to show that also $\mathrm{nf}(\langle|M|\rangle) \to P$ for some $P$.

We want to show that we can re-arrange the trace $\mathrm{nf}(\langle|M|\rangle) \hookrightarrow^* \mathrm{nf}(Q_1) \to Q_2$ in order to obtain a trace of the form $\mathrm{nf}(\langle|M|\rangle) \to \to^* P_2$ with $Q_2 \in \mathrm{addG}(P_2)$. Consider the trace $\mathrm{nf}(\langle|M|\rangle) \hookrightarrow^* \mathrm{nf}(Q_1)$, and recall that $\to^*=\to \cup \to$. Since $\mathrm{nf}(\langle|M|\rangle)$ is in normal form, if no step in $\mathrm{nf}(\langle|M|\rangle) \hookrightarrow^* \mathrm{nf}(Q_1)$ is a communication $\mapsto$ then the trace is empty. Otherwise we want to rewrite it as $\mathrm{nf}(\langle|M|\rangle) \mapsto \to^* \mathrm{nf}(R_1) \mapsto \to^* \dots \mapsto \to^* \mathrm{nf}(R_n) \mapsto \to^* \mathrm{nf}(Q_1)$. This can be done using Lemma 25 to ensure that all the enabled applications are performed before the next administrative communication $\mapsto$.

We now proceed by induction on the length of this trace, showing that we can either remove administrative reductions or move them after the forward reduction $\mathrm{nf}(Q_1) \to Q_2$. The base case (no administrative reductions) is trivial. For the inductive case we have a case analysis on the last administrative communication $\mapsto$. By looking at the encoding one can see that there
are three kinds of non-labelled triggers, hence triggers able to generate an administrative communication:

**Internal communication in the translation of a trigger:** this case never happens. In fact, by inspecting the encoding, one can see that such a communication is enabled only after a $\rightarrow$ reduction takes place.

**Communication due to a Rew process:** a Rew process consumes a message on a key channel, and this kind of message is not present in $nf(|M|)$. Thus, back in the trace there exists an administrative communication $\mapsto$ due to a killer process producing it. Let us select the nearest such $\mapsto$. Since this is the nearest one, there are no intermediate administrative communications that consume the same message. Hence we can move the killer communication forward in order to be adjacent to the Rew one. Now, one can observe that these two communications in a row lead back to the original process, plus some garbage. Thus by removing these two communications from the trace we obtain a shorter trace, leading to a term with the same behavior but possibly less garbage. This explains why the sequence of reductions leads to $P_2$ with $Q_2 \in \text{addG}(P_2)$ and not to $Q_2$.

**Communication due to a killer process:** the administrative communication $\mapsto$ can be moved after the $\rightarrow$ reduction since it does not remove processes that contribute to the $\rightarrow$ reduction, and we obtain again a shorter trace.

The proof schema for the rest of the proof is shown in Figure 11. We have proved above that $nf(|M|) \hookrightarrow^* nf(Q_1) \rightarrow Q_2$ implies $nf(|M|) \rightarrow P \hookrightarrow^* P_2$ for some $P$, with $Q_2 \in \text{addG}(P_2)$. By applying Lemma 35 to $nf(|M|) \rightarrow P$ we have that $M \rightarrow M'$ and $P \hookrightarrow^* P'$ with $nf(P') \equiv_{Ex} nf(P'')$ and $P''' \in \text{addG}(|M'|)$. By applying Lemma 29 to $P \hookrightarrow^* P_2$ there exists $Q_3, P_3$ such that $P_2 \hookrightarrow^* P_3$ with $nf(P_3) \equiv_{Ex} nf(Q_3)$ and $Q_3 \in \text{addG}(P)$. Since $P \hookrightarrow^* nf(P')$, we have that also $Q_3 \hookrightarrow^* Q_4$ with $Q_4 \in \text{addG}(nf(P'))$. From Lemma 26 we have that there exists $Q_5$ such that $Q_4 \dashrightarrow^* Q_5$ and $nf(Q_3) \dashrightarrow^* Q_5$. However, $Q_4$ differs from a normal form (the one of $P'$) only for garbage, thus we can assume $Q_5 = Q_4$. Since then $nf(Q_3) \dashrightarrow^* Q_4$ we can use Lemma 28 to show that there exists $Q_6$ such that $nf(P_3) \dashrightarrow^* nf(Q_6)$ and $nf(Q_6) \equiv_{Ex} nf(Q_7)$ with $Q_7 \in \text{addG}(Q_4)$. By composing garbage, $Q_7 \in \text{addG}(nf(P'))$. Since $Q_2 \in \text{addG}(P_2)$ and $P_2 \dashrightarrow^* nf(Q_6)$ we have that $Q_2 \dashrightarrow^* Q''$ with $Q'' \in \text{addG}(P_2)$.
<figure><img src="image_7.png" /><figcaption>Figure 11: Proof schema of the last part of Lemma 36</figcaption></figure>

addG nf(Q₆)). By composing garbage and using transitivity of ≡ₐ we have
that there is Q''' such that Q'' ≡ₐ Q''' and Q''' ∈ addG(|M'|). The thesis
follows by noticing that Q' ↪* Q'' and that Q'' and Q''' are normal forms
(apart, possibly, for garbage). □

**Lemma 37.** Let $M$ be a rho$\pi$ configuration. If $|M| \to^* Q \rightsquigarrow Q'$ then there exists $M'$, $Q''$ and $Q'''$ such that $M \rightsquigarrow M'$, $Q' \to^* Q''$ and $nf(Q'') \equiv_E nf(Q''')$ and $Q''' \in \mathrm{addG}(|M'|)$.

PROOF. We have that $Q \rightsquigarrow Q'$ and by applying Lemma 26 we also have
that $\mathrm{nf}(Q) \rightsquigarrow Q_1$ with $Q' \to^* Q_1$. This implies that $\mathrm{nf}(Q) \equiv \nu\tilde{u}.R$
$| \mathrm{nf}(|\mathrm{Mem}\ Y \ a\ (P|)\ k_1\ k\ k_2|) | \ c\langle (|C|) \rangle$ with $Y = (X\ c)c\langle (|P_1|) \rangle$ and that $Q' \equiv$
$\nu\tilde{u}.R$ $|(\mathrm{Msg}\ a\ (P|)\ k_1)|$ $|(\mathrm{Trig}\ Y\ a\ k_2)|$. Since administrative reductions $\to$
do not remove memories, the memory needs to be already present both in
<figure><img src="image_8.png" /><figcaption>Figure 12: Proof schema of the first part of Lemma 37</figcaption></figure>

the configuration $M$ and in its normal form. Since $\langle|M|\rangle \hookrightarrow^* Q$ and $\langle|M|\rangle \dasharrow^* \mathrm{nf}(\langle|M|\rangle)$ by Lemma 26 we also have that $\mathrm{nf}(\langle|M|\rangle) \hookrightarrow^* R$ with $Q \dasharrow^* R$, hence $\langle|M|\rangle \hookrightarrow^* R$, moreover since $Q \rightsquigarrow Q'$ we also have that $R \rightsquigarrow R'$ with $Q' \dasharrow^* R'$. The proof schema for the above part of the proof is shown in Figure 12. By definition of $\langle\cdot\rangle$ and $\mathrm{nf}(\cdot)$, the process $\mathrm{nf}(\langle|M|\rangle)$ cannot contain a message on a key channel such as $k\langle\langle C\rangle\rangle$. Hence, such a message has been generated by the reductions $\mathrm{nf}(\langle|M|\rangle) \hookrightarrow^* R$. We distinguish two cases: either all the communications in $\hookrightarrow^*$ contribute to create such a message, or not. In the first case all the communications are due to killer processes, and we have that $\mathrm{nf}(\langle|M|\rangle) \equiv \nu\tilde{u}.\mathrm{nf}(\langle N\rangle) \mid \mathrm{nf}(\mathrm{Mem}\ Y\ a\ \langle P\rangle\ k_1\ k\ k_2) \mid \mathrm{nf}(\langle C\rangle k)$ for some $N$, hence $M \equiv \nu\tilde{u}.N \mid [k_1 : a\langle P\rangle \mid k_2 : a(X) \triangleright P_1; k] \mid k : C$. Since the administrative reductions just create the message on the channel $k$, by using Lemma 23 (where $S$ is garbage) we have that $\mathrm{nf}(\langle|M|\rangle) \hookrightarrow^* \nu\tilde{u}.\mathrm{nf}(\langle N\rangle) \mid (k(Z) \triangleright (\mathrm{Msg}\ a\ \langle P\rangle\ k_1) \mid (\mathrm{Trig}\ Y\ a\ k_2)) \mid k\langle\langle C\rangle\rangle \mid S \rightsquigarrow R'$ with $R' = \nu\tilde{u}.\mathrm{nf}(\langle N\rangle) \mid (\mathrm{Msg}\ a\ \langle P\rangle\ k_1) \mid (\mathrm{Trig}\ Y\ a\ k_2)) \mid S$. On the other side we have that $M \rightsquigarrow \nu\tilde{u}.N \mid k_1 : a\langle P\rangle \mid k_2 : a(X) \triangleright P_1 = M'$ and we can conclude since $\mathrm{nf}(R') = \mathrm{nf}(Q'')$ with $Q'' \in \mathrm{addG}(\langle|M'|\rangle)$.

If there are administrative reductions that do not contribute to the creation of the message on $k$, we re-arrange the trace $\mathrm{nf}(\langle|M|\rangle) \hookrightarrow^* R \rightsquigarrow R'$ so to have first all the reductions that contribute to create the message on $k$, then the $\rightsquigarrow$ reduction and finally all the unrelated reductions. We proceed by induction on the length of the reduction sequence $\mathrm{nf}(\langle|M|\rangle) \hookrightarrow^* R$, with a case analysis on the last reduction that does not contribute to the creation of the message on $k$. It can be either a communication due to a killer process unrelated to the process with tag $k$, or a communication due to a Rew $l$. In the first case the kill does not concerns the process labelled by $k$ nor a
<figure><img src="image_9.png" /><figcaption>Figure 13: Case challenge $M \to M'$ of proof of Theorem 3</figcaption></figure>

parallel composition due to the split of the key $k$. Thus, it can be moved after the $\rightsquigarrow$ reduction and we can conclude by induction on a shorter trace.

If the reduction is due to a *Rew* process we have two cases: either it deals with processes related to the one tagged by $k$, or not. In the second case we proceed as in the case above and we conclude by induction on a shorter trace. In the first case, note that a reduction due to a *Rew* process instantiates a process. Since this reduction is related to the process on channel $k$, the instantiated process must be re-killed by possibly many successive kills. Hence, we can remove the *Rew* reduction and the corresponding kills, and we can conclude by induction on a shorter trace.

At the end, we have a trace of the form $nf(|M|) \hookrightarrow^* R_1 \dashrightarrow R'_1 \hookrightarrow^* R'$ with the first trace $\hookrightarrow^*$ containing all the administrative reductions related to the creation of the message on $k$. As in the first case we know that $nf(|M|) \hookrightarrow^* R_1 \dashrightarrow R'_1$ implies that $M \dashrightarrow M'$ with $nf(R'_1) = nf(R'_2)$ and $R'_2 \in \text{addG}(|M'|)$. Moreover we have that $R'_1 \hookrightarrow^* R'$ and that $nf(R'_1) \hookrightarrow^* R''$ with $R' \dashrightarrow R''$. By using Lemma 29 we have that there exist $Q''$ such that $R'' \hookrightarrow^* Q''$ and $nf(Q'') \equiv_{Ex} nf(Q_3)$ with $Q_3 \in \text{addG}(R'_1)$. Since $nf(R'_1) = nf(R'_2)$ and applications do not change garbage we have that there is $Q'''$ such that $nf(Q_3) = nf(Q'''')$ and $Q''' \in \text{addG}(|M'|)$, as desired. $\square$

We can now prove our main result.

**PROOF OF THEOREM 3.** We prove that the following relation is a bfa barbed
<figure><img src="image_10.png" /><figcaption>Figure 14: Case challenge $R \mapsto R'$ of proof of Theorem 3</figcaption></figure>

bisimulation:

$$ \mathcal{R} = \{(M, R) \mid M \text{ is consistent } \wedge \mathbf{nf}(R) \equiv_{Ex} \mathbf{nf}(Q') \wedge Q' \in \mathbf{addG}(Q) \wedge (|M| \hookrightarrow^* Q)\} $$

We have to check the different conditions for bfa barbed bisimulation.

Assume $M \downarrow_a$. Note that from the definition of barbs only names in $\mathcal{N}$ produce barbs. From Lemma 30 $Q \hookrightarrow^* \downarrow_a$. Since $\mathbf{addG}$ never removes barbs then, thanks to Lemma 32, $Q' \hookrightarrow^* \downarrow_a$. Then also $\mathbf{nf}(Q') \hookrightarrow^* \downarrow_a$. Thanks to Proposition 1 we have that $\mathbf{nf}(R) \hookrightarrow^* \downarrow_a$ and thus also $R \hookrightarrow^* \downarrow_a$.

Assume now $R \downarrow_a$. Thanks to Lemma 22 we have that $a \in \mathcal{N}$. We also have that $\mathbf{nf}(R) \downarrow_a$. Thanks to Proposition 1 $\mathbf{nf}(Q') \hookrightarrow^* \downarrow_a$ and also $Q' \hookrightarrow^* \downarrow_a$. Then $Q \hookrightarrow^* \downarrow_a$. Finally, thanks to Lemma 31 $M \downarrow_a$.

Let us consider reductions. Figure 13 shows the proof schema we use. If $M \to M'$ then by Theorem 4 we have $\mathbf{nf}(|M|) \Rightarrow_f P$ with $\mathbf{nf}(P) \equiv_{Ex} \mathbf{nf}(P')$ and $P' \in \mathbf{addG}(|M'|)$. By hypothesis we have that $|M| \hookrightarrow^* Q$, and also $\mathbf{nf}(|M|) \hookrightarrow^* \mathbf{nf}(Q)$ and by Lemma 29 we have that there are $Q_1, Q_2$ such that $\mathbf{nf}(Q) \hookrightarrow^* \mathbf{nf}(Q_1)$ and $\mathbf{nf}(Q_1) \equiv_{Ex} \mathbf{nf}(Q_2)$ with $Q_2 \in \mathbf{addG}(\mathbf{nf}(|M|))$. Since $\mathbf{nf}(|M|) \Rightarrow_f P$ then $Q_2 \Rightarrow_f P_1$ with $P_1 \in \mathbf{addG}(P)$. Since $Q_2 \to^* \mathbf{nf}(Q_2)$ and $Q_2 \Rightarrow_f P_1$ then thanks to Lemma 26 there exists $P_3$ such that $\mathbf{nf}(Q_2) \Rightarrow_f P_3$ and $P_1 \to^* P_3$. Since $\mathbf{nf}(Q_2) \equiv_{Ex} \mathbf{nf}(Q_1)$ and $\mathbf{nf}(Q_2) \Rightarrow_f P_3$ by Lemma 27 we also have that $\mathbf{nf}(Q_1) \Rightarrow_f P_2$ and $\mathbf{nf}(P_2) \equiv_{Ex} \mathbf{nf}(P_4)$ for some $P_4 \in \mathbf{addG}(P_3)$. Now, one can go from $P$ to $\mathbf{nf}(P_4)$ by executing
<figure><img src="image_11.png" /><figcaption>Figure 15: Case challenge $R \to R'$ of proof of Theorem 3</figcaption></figure>
applications and adding garbage, thus $\mathbf{nf}(P_4) \in \mathbf{addG}(\mathbf{nf}(P))$. Also, there is $P_5$ such that $\mathbf{nf}(P_4) \equiv_{Ex} \mathbf{nf}(P_5)$ and $P_5 \in \mathbf{addG}(P')$. By composing garbage we get $P_5 \in \mathbf{addG}(\langle M' \rangle)$. Since $\mathbf{nf}(P_2) \equiv_{Ex} \mathbf{nf}(P_4)$ and $\mathbf{nf}(P_4) \equiv_{Ex} \mathbf{nf}(P_5)$ by transitivity we have $\mathbf{nf}(P_2) \equiv_{Ex} \mathbf{nf}(P_5)$. We can conclude by noting that the pair $(M', P_2) \in \mathcal{R}$ (no administrative reductions are performed from $\langle M' \rangle$). The backward case is similar.

For the other direction, assume $R \to R'$. We have a case analysis according to the kind of reduction.

If $R \to R'$ then the thesis follows trivially since $\mathbf{nf}(R) = \mathbf{nf}(R')$.

If instead $R \mapsto R'$ then by Lemma 26 $\mathbf{nf}(R) \hookrightarrow_R^* R''$ and $R' \dashrightarrow_R^* R''$ for some $R''$. Thanks to Lemma 25 from $R' \dashrightarrow_R^* R'' \dashrightarrow_R^* \mathbf{nf}(R'')$ and $R' \dashrightarrow_R^* \mathbf{nf}(R')$ we have that there are two sequences of applications closing the diagram. However, since $\mathbf{nf}(R')$ and $\mathbf{nf}(R'')$ are normal forms those sequences are empty, hence $\mathbf{nf}(R'') = \mathbf{nf}(R')$. Thus we have $\mathbf{nf}(R) \hookrightarrow_R^* \mathbf{nf}(R')$. Thanks to Proposition 1 from $\mathbf{nf}(R) \equiv_{Ex} \mathbf{nf}(Q')$ we have that there is $R_1$ such that $\mathbf{nf}(Q') \hookrightarrow_R^* R_1$ and $\mathbf{nf}(R') \equiv_{Ex} R_1$. Thanks to Lemma 18 from $\mathbf{nf}(Q') \hookrightarrow_R^* R_1$ we have that $Q \hookrightarrow_R^* R_2$ with $R_1 \in \mathbf{addG}(R_2)$. By using Lemma 14 from $\mathbf{nf}(R') \equiv_{Ex} R_1$ we obtain $\mathbf{nf}(R') \equiv_{Ex} \mathbf{nf}(R_1)$. We can conclude since $\mathbf{nf}(R') \equiv_{Ex} \mathbf{nf}(R_1)$ with $R_1 \in \mathbf{addG}(R_2)$ and $\langle M \rangle \hookrightarrow_R^* Q \hookrightarrow_R^* R_2$, thus $(M, R') \in \mathcal{R}$.

Assume now $R \twoheadrightarrow R'$. By Lemma 26 $\mathbf{nf}(R) \twoheadrightarrow R''$ and $R' \dashrightarrow_R^* R''$ for some $R''$. Thanks to Lemma 25 from $R' \dashrightarrow_R^* R'' \dashrightarrow_R^* \mathbf{nf}(R'')$ and $R' \dashrightarrow_R^* \mathbf{nf}(R')$ we have that there are two sequences of applications closing the diagram. However, since $\mathbf{nf}(R')$ and $\mathbf{nf}(R'')$ are normal forms those sequences are empty, hence $\mathbf{nf}(R'') = \mathbf{nf}(R')$. Thanks to Proposition 1 we have that $\equiv_{Ex}$ is a bfa barbed bisimulation, and from $\mathbf{nf}(R) \equiv_{Ex} \mathbf{nf}(Q')$ we have that there are $S, S', R_1$ such that $\mathbf{nf}(Q') \hookrightarrow_S^* S \twoheadrightarrow S' \hookrightarrow_S^* R_1$ and $R'' \equiv_{Ex} R_1$. From Lemma 14 also $\mathbf{nf}(R'') = \mathbf{nf}(R') \equiv_{Ex} \mathbf{nf}(R_1)$.

Since $Q' \in \mathbf{addG}(Q)$ using Lemma 18 from $\mathbf{nf}(Q') \hookrightarrow_S^* S \dashrightarrow_S^* \mathbf{nf}(S)$ we get that there exists $Q_1'' \in \mathbf{addG}(\mathbf{nf}(S))$ such that $Q \hookrightarrow_S^* Q_1''$. From Lemma 26 there is $S''$ such that $\mathbf{nf}(S) \twoheadrightarrow S''$ and $S' \dashrightarrow_S^* S''$. Now, from Lemma 19 we have that there exist $Q_1' \in \mathbf{addG}(S'')$ and $Q_1$ such that $Q_1'' \dashrightarrow_S^* Q_1 \twoheadrightarrow Q_1'$. From Lemma 26 there is $S'''$ such that $S'' \hookrightarrow_S^* S'''$ and $R_1 \dashrightarrow_S^* S''$. Since $R_1 \dashrightarrow_S^* \mathbf{nf}(R_1)$ and $R_1 \dashrightarrow_S^* S'''$ we have that $S''' \dashrightarrow_S^* \mathbf{nf}(R_1)$. Since $S'' \dashrightarrow_S^* \mathbf{nf}(S'')$ and $S'' \hookrightarrow_S^* S''' \dashrightarrow_S^* \mathbf{nf}(R_1)$ we have that $\mathbf{nf}(S'') \hookrightarrow_S^* \mathbf{nf}(R_1)$. Finally, using again Lemma 18 from $S'' \in \mathbf{addG}(Q_1')$ and $\mathbf{nf}(S'') \hookrightarrow_S^* \mathbf{nf}(R_1)$ we have that there exists $R_2$ such that $\mathbf{nf}(R_1) \in \mathbf{addG}(R_2)$ and $Q_1' \hookrightarrow_S^* R_2$.

Summarizing we have $Q \hookrightarrow_S^* Q_1 \twoheadrightarrow Q_1' \hookrightarrow_S^* R_2$ with $\mathbf{nf}(R_1) \in \mathbf{addG}(R_2)$.
By hypothesis, we have that $|M| \hookrightarrow^* Q$. By Lemma 36 we have that $|M| \hookrightarrow^* Q_1 \to Q'_1$ implies that there exist $M'$, $Q_2$ and $Q_3$ such that $M \to M'$ and $Q'_1 \hookrightarrow^* Q_2$ with $nf(Q_2) \equiv_{Ex} nf(Q_3)$ and $Q_3 \in \text{addG}(|M'|)$.

We can apply Lemma 29 to $Q'_1 \hookrightarrow^* Q_2$ obtaining $Q_4$ and $Q_5$ such that $Q_2 \hookrightarrow^* Q_4$ and $nf(Q_4) \equiv_{Ex} nf(Q_5)$ with $Q_5 \in \text{addG}(Q'_1)$. Since $Q'_1 \hookrightarrow^* R_2$ we have that there is $Q_6 \in \text{addG}(R_2)$ such that $Q_5 \hookrightarrow^* Q_6$ and, as a consequence, $nf(Q_5) \hookrightarrow^* nf(Q_6)$. Note that $nf(R_1)$ and $Q_6$ differ only because of garbage. Since garbage has no impact on the semantics we can consider them equal (this can be formalized more precisely as an up-to technique). Thus $nf(Q_6) = nf(R_1)$, and since $nf(R') \equiv_{Ex} nf(R_1)$ we also have $nf(R') \equiv_{Ex} nf(Q_6)$. We want to show that the pair $(M', R') \in \mathcal{R}$. We have that $Q_2 \hookrightarrow^* Q_4$ but also $nf(Q_2) \hookrightarrow^* nf(Q_4)$ and since $nf(Q_3) \equiv_{Ex} nf(Q_2)$ and $\equiv_{Ex}$ is a bfa barbed bisimulation there exists $R_3$ such that $nf(Q_3) \hookrightarrow^* R_3$ with $R_3 \equiv_{Ex} nf(Q_4)$. Hence by using Lemma 18 we also have that $nf(|M'|) \hookrightarrow^* R_4$ with $R_3 \in \text{addG}(R_4)$. We have $R_3 \equiv_{Ex} nf(Q_4) \equiv_{Ex} nf(Q_5)$ and $nf(Q_5) \hookrightarrow^* nf(Q_6)$. Since $\equiv_{Ex}$ is a bfa barbed bisimulation there exists $R_5$ such that $R_3 \hookrightarrow^* R_5$ with $R_5 \equiv_{Ex} nf(Q_6)$. Since $R_3 \in \text{addG}(R_4)$ we have that $R_4 \hookrightarrow^* R_6$ with $R_5 \in \text{addG}(R_6)$. Using Lemma 14 we have that $nf(R_5) \equiv_{Ex} nf(Q_6)$. To conclude we can note that $|M'| \to^* nf(|M'|) \to^* R_4 \to^* R_6$ with $R_5 \in \text{addG}(R_6)$ and $nf(R_5) \equiv_{Ex} nf(Q_6) \equiv_{Ex} nf(R')$. This implies that $(M', R') \in \mathcal{R}$, as desired.

If $R \rightsquigarrow R'$ we can use the same reasoning of the $\to$ case by using Lemma 37 and Lemma 20 instead of Lemma 36 and Lemma 19. $\square$

# 5. Related work

Research into reversible computing has already a long history, that originates in the 1960s. Bennett provides an account [1] of early research on the subject. A full review of works on reversible computing, and the closely related subjects of program inversion (see, e.g., [38] and the references therein) and bidirectional transformation and languages (see, e.g., [39, 40] and the references therein), is out of the scope of this paper but we can highlight works related to our three main contributions: (i) reversible languages and models, (ii) causal semantics and back and forth bisimulation, (iii) translating between reversible and irreversible computations.

*Reversible languages and models.* The notion of reversible Turing machine seems to date back at least to Lecerf in the early 60s [41], who provides an early encoding of irreversible Turing machines into reversible ones, rediscovered by Bennett in [42]. For a recent survey of reversible Turing machines,
their relation to reversible boolean logic, and various reversible models of computation, see [43].

Several works have tackled the problem of adding reversibility to sequen-
tial programming languages or to sequential abstract machines. Early work
focused on reversible execution [44] and adding undo capabilities to pro-
gramming languages. Leeman [45] provides an early survey as well as a gen-
eral framework for adding an *undo* capability to a sequential programming
language. Computational history is saved by means of undo-lists, storing
previous states of the execution. Primitives dealing with undo-lists are for-
malized, and different undo operators can be defined by composing them.
A way to map compositionally high-level functional programs into a certain
kind of reversible automata is given by Abramsky in [46]. In [47], Danos
and Regnier give a compositional translation of the λ-calculus into a form
of reversible abstract machine called Interaction Abstract Machine (IAM).
Other reversible abstract machines for sequential programming such as the
SEMCD machine [48] and the Reversible Virtual Machine (RVM) [49] have
been proposed.

Whereas the latter virtual machines keep an explicit track of execution
history to reconstruct backward computation, several works study natively
reversible sequential programming languages where reversibility is obtained
without the need to keep additional information to reconstruct backward
computation. These include work on the Janus language whose origin dates
back to the early 1980s [50, 51], work on sequential flow charts [52], the Inv
[53], RFUN [54], and Π [55] reversible functional languages. The key aspect
of Janus is that all its constructs, including assignments, are made *bijective*
(and hence reversible), and the language does not allow I/O. The Π language
constitutes a reversible core programming model which is claimed to be at
the heart of linear logic and quantum computation. It is shown in [55] how
to translate a conventional first-order functional language with loops to Π,
making explicit the information effects implicit in the irreversible computa-
tion of a conventional functional program as manipulations of a global heap
and garbage dump.

Reversibility in concurrent models has been considered only more re-
cently, starting with the seminal work of Danos and Krivine on RCCS [12].
In contrast to sequential settings, the notion of reversibility is less easy to
define, and the key contribution of [12] is to define the criterion of *causal
consistency* for semantic reversibility, i.e. the ability to go back in a compu-
tation along equivalent concurrent paths. This work later gave rise to several
studies (including the one reported in this paper), including [13] which shows
how to accommodate a notion of communicating transaction in the RCCS
setting, and how using RCCS as a means of specifying such transactions one
can gain both in expressivity of specifications and in ease of verification of
transactional systems. Phillips and Ulidowski show in [14] how to obtain
reversible variants of process calculi defined with GSOS inference rules. [56]
showed how the results obtained in [13] can be obtained by means of a univer-
sal categorical construction involving categories of fractions and categories
of computation paths. Extensions of Danos and Krivine's work on CCS to
the (higher-order and first-order) π-calculus appear in our own work [16],
and in the recent paper by Cristescu, Krivine and Varacca [20], which de-
fines a labelled transition semantics for a reversible variant of the first-order
π-calculus called Rπ. The latter work is closest to ours, but the reversible
machinery in Rπ is substantially different: as in RCCS, Rπ processes are
built upon simple π processes to which a stack of events, called a memory,
is added to keep track of past actions. Every entry in a memory records a
past communication event and can be used to trigger backward moves. In
contrast, in rhoπ only simple keys are associated to processes, and specific
processes are used to record the causal relationships between keys. It is easy
to define a reversible variant of the first-order π-calculus using our reversible
machinery of keys. One can also define for such a calculus a labelled tran-
sition system (LTS) semantics where actions are standard π-calculus actions
annotated with keys, but it is less easy to directly compare the two result-
ing reversible π-calculi. We surmise that the reversible π obtained via our
late LTS semantics would indeed be strongly bisimilar to Rπ, whereas the
strong back and forth bisimulation associated with the early variant LTS of
our reversible π would provide a coinductive characterization of contextual
equivalence in rhoπ, but this is left for further study.

Foundational studies of reversible and concurrent computations have been
largely inspired by areas such as chemical and biological systems where op-
erations are reversible and only an injection of energy and/or a change of en-
tropy can move the computational system in a desired direction. A reversible
variant of CCS to model biological systems is given in [57]. Frequently these
systems are *massively concurrent*, i.e. different processes of the same shape
are indistinguishable. Thus, unique tags like ours cannot be used, since there
is no way to distinguish different instances of the same molecule during in-
teraction. In these systems standard notions of causality and independence
of events need to be adapted. Reversible structures [4] allow to model such
systems. In reversible structures processes are called *gates*, and are expressed as a sequence of inputs followed by a sequence of outputs. Following the approach of [14], the past computational history of a gate is stored in the gate itself. That is, since gates are a sequence of actions, a cursor “^” is used to point to the next action of a gate. Said otherwise, the cursor ^ divides a gate into two parts: past actions and future actions. Each time a gate performs a forward (backward) action its cursor is moved forward (backward) by one position. Different output processes (called signals) on the same channel may have the same identifier, hence they are indistinguishable. So it may happen that while computing backward a gate gets back a signal that has not been generated by the gate itself, but it is indistinguishable from it. Reversibility is proven correct even in presence of indistinguishable signals. Another work considering reversible concurrent systems in relation with biological modeling is the recent work by Phillips and Ulidowski [58], which presents a reversible concurrent model where backward moves are controlled by a form of superposition construct. In this model, backward computations are not necessarily causally consistent.

Notions of reversible computation appear also in works on *reversible debuggers* [59, 60, 61? , 62] and on computer simulation tools [63]. Two techniques are commonly used in reversible debugging: *replay* and *state saving*. The first one, typical of interpreted languages, consists in re-executing the program to the point at which the programmer wants to get back. This technique can be improved by using periodic or incremental checkpoints, thus reducing the number of instructions that have to be re-played. The second technique consists in saving the entire program state during the computation, and then restoring it when needed. Usually, due to space overhead, the range of actions that can be reverted is limited and it has to be decided before launching the debugging mode. Both the techniques work fine in the sequential setting. In the concurrent setting also information about the *scheduling*, i.e. the order of execution of concurrent processes, has to be taken into account. [64] gives a technique to achieve repeatable execution of highly parallel programs. During execution, the relative order of significant events is saved. Then by imposing the same order during replay, and using the same inputs from the external environment, it is possible to reproduce the same behavior. Building on [18], which shows that one can build primitives to control rhoπ reversibility, [62] shows how to force a concurrent execution back in a causally consistent way so as to undo a specific past action in a way similar to those of reversible debuggers but without impacting non causally
related threads. This is in contrast, for instance, with [65], where the user is
asked, while debugging, to specify all the actions to be undone and the order
in which to undo them. The partial order among concurrent actions induced
by the rhoπ tag mechanism can be exploited also in re-playing techniques.

*Translating between reversible and irreversible models of computation.* Interest for translation between reversible and irreversible models of computation has centered around encoding of irreversible models into reversible ones, or between reversible ones.

As reported in [1], early interest was concerned with the encoding of
irreversible computations into a reversible computational model such as a
reversible Turing machine or reversible boolean logic. The more recent work
by Burhman et al. [66] provides a general upper bound on the tradeoff be-
tween time and space that suffices for the simulation by a reversible Turing
machine of an irreversible one. Together with a later paper by Vitanyi [67],
it provides a useful survey of prior work on this “reversible simulation” prob-
lem. The work by Cardelli and Laneve [4], already mentioned, shows that,
by disallowing indistinguishable signals, reversible structures can implement
the asynchronous version of RCCS. This is stated by a (weak) completeness
theorem but nothing is said about the correctness of the encoding. The sur-
vey paper [43] relates different reversible models, including reversible Turing
machines, reversible boolean logic and reversible cellular automata.

To the best of our knowledge, we are the first in [16] and in this paper
to study an encoding of a reversible concurrent model of computation into
an irreversible one. In our paper [16] we have defined an encoding very
similar to the one presented in this paper, but we were only able to prove
the faithfulness of the translation using a weak barbed congruence, which, as
discussed in Section 2.5, is a rather coarse equivalence. In this paper, with
a slight modification of our encoding, we have been able to prove a much
stronger result, which is optimal in the sense that the equivalence we use
is a strong back and forth simulation with weak administrative moves, i.e.
each forward or backward step in rhoπ translates into a forward or backward
step, respectively, modulo administrative moves. Both encodings faithfully
implement the reversible calculus, but, as the operational semantics of rhoπ
itself, they are rather wasteful in terms of space. To see this informally, notice
first that a forward computation step in rhoπ requires retaining in a memory
the message a(P) and the receiver process a(X) ▷ Q that participated in it.
Thus the space overhead of a computation step in reversible HOπ compared
to standard HOπ is at least ||P||, the size of the payload of message a⟨P⟩.
Now consider the following recursive programs: P = c(X)▷P | a⟨X | X⟩ and
Q = a(X)▷Q | c⟨X | X⟩. We have a⟨R⟩ | P | Q → P | Q | c⟨R | R⟩ so the
space overhead of this first step starting from a⟨R⟩ | P | Q is at least ||R||.
On the second step we have P | Q | c⟨R | R⟩ → P | Q | a⟨R | R | R | R⟩, so
the space overhead of this second step is at least 2||R||. By induction, one can
see that the space overhead associated with making the program a⟨R⟩ | P | Q
reversible is at least 2n⁻¹||R||, where n is the number of computation steps
taken from the initial state a⟨R⟩ | P | Q. Our encodings are at least as
wasteful in terms of space. However we have shown in [22] that the space
overhead required to implement a small language close to rhoπ is only linear
in the number of computation steps, and in fact only linear in the number of
non-deterministic events occurring during a computation.

*Causal semantics and back and forth simulations.* For proving the correctness of our encoding, we have used a notion of back and forth bisimulation, where both forward and backward moves are taken into account in the bisimulation game. Different forms of simulations taking into account forward and backward moves have been studied in the past but mostly in the context of verifying standard transition systems. Such notions appear in the late 80's and early 90's in works such as [24, 68]. The two survey papers [69, 70] by Lynch and Vaandrager study the relationships between different kinds of simulations between (standard, timed and untimed) transition systems, including refinements, forward and backward simulations, hybrid forward-backward and backward-forward simulations, and history and prophecy relations. More recently, notions of forward and backward simulation have been studied from a coalgebraic point of view by Hasuo [25].

More related to reversible models of computation are recent works by
Phillips and Ulidowski. The paper [71] proposes extensions to event struc-
tures to take into account reversibility in transition systems. The paper
[72] defines several forms of bisimulations mixing forward and reverse obser-
vations, and studies the relationships between various equivalences on sta-
ble configuration structures, including step bisimulation, step bisimulation
with reverse steps, interleaving bisimulation with reverse steps, and hered-
itary history-preserving bisimulation. Notably, they show that, in absence
of auto-concurrency, interleaving bisimulation with reverse steps is as strong
as hereditary history-preserving bisimulation. The latter results illustrates
the observational power gained by the ability to take into account backward
moves in a bisimulation game. It squares nicely with our result in Section 3.2 that relates our reversible machinery in rhoπ to the causal semantics for π developed by Boreale and Sangiorgi [21], and which states that a causally consistent reversible semantics essentially constitutes a causal semantics for (the forward part of) the calculus. This intuition is further compounded by the work on Rπ [20], which shows that Rπ semantics provides a non-interleaving semantics for the π-calculus that in addition agrees with the causality induced by reductions (τ transitions). Much work remains to be done, however, to better understand the relationships between our reduction semantics for (higher-order) π and the resulting barbed congruence, the LTS semantics of Rπ and its associated bisimilarity, and the various causal semantics of the π calculus that have been developed in the past, including, e.g., [21, 73, 29, 74].

# 6. Conclusion

We have presented a reversible asynchronous higher-order π-calculus, called rhoπ, which we have shown to be causally consistent. The paper gets its inspiration from Danos and Krivine work [12] and makes three original contributions. The first one is a novel way to introduce reversibility in a process calculus which preserves the classical structural congruence laws of the π-calculus, and which relies on simple name tags for identifying threads and explicit memory processes. Our approach contrasts with the two previous approaches of RCCS [12], that relied on memory stacks as thread tags, and of Phillips and Ulidowski [14], that relied on making the structure of terms in SOS rules static and on keeping track of causality by tagging actions in SOS rules, as well as with the recent work on Rπ, a reversible variant of the π calculus developed by Cristescu, Krivine and Varacca [20]. The second contribution of the paper is the analysis, by means of a bisimulation relation called causal correspondence, of the relationship between the causal semantics of the π-calculus developed by Boreale and Sangiorgi [21], and the causality tracking machinery used in our reduction semantics for rhoπ. The third contribution of the paper is a faithful encoding of our reversible HOπ calculus into a variant of HOπ, showing that adding reversibility does not change the expressive power of HOπ (up to our notion of backward and forward bisimilarity with administrative moves). The result obtained in this paper considerably strengthens that obtained in our previous work [16] by showing that, modulo administrative reduction steps, a rhoπ process and its
translation are strong back and forth bisimilar.
## References

[1] C. H. Bennett, Notes on the history of reversible computation, IBM Journal of Research and Development 32 (1) (1988) 16-23.

[2] R. Landauer, Irreversibility and heat generated in the computing process, IBM Journal of Research and Development 5 (1961) 183-191.

[3] M. P. Frank, Introduction to reversible computing: motivation, progress, and challenges, in: 2nd Conference on Computing Frontiers, ACM, 2005, pp. 385-390.

[4] L. Cardelli, C. Laneve, Reversible structures, in: CMSB, ACM, 2011, pp. 131-140.

[5] T. Akgul, V. J. Mooney III, Assembly instruction level reverse execution for debugging, ACM Trans. Softw. Eng. Methodol. 13 (2) (2004) 149-198.

[6] T. Altenkirch, J. Grattage, A functional quantum programming language, in: LICS, IEEE Computer Society, 2005, pp. 249-258.

[7] P. Bishop, Using reversible computing to achieve fail-safety, in: The Eighth International Symposium On Software Reliability Engineering, 1997, pp. 182-191.

[8] A. Avizienis, J.-C. Laprie, B. Randell, C. E. Landwehr, Basic concepts and taxonomy of dependable and secure computing, IEEE Trans. Dependable Sec. Comput. 1 (1) (2004) 11-33.

[9] B. Jacobs, F. Piessens, Failboxes: Provably safe exception handling, in: ECOOP, 2009, pp. 470-494.

[10] E. N. Elnozahy, L. Alvisi, Y.-M. Wang, D. B. Johnson, A survey of rollback-recovery protocols in message-passing systems, ACM Comput. Surv. 34 (3) (2002) 375-408.

[11] G. Weikum, G. Vossen, Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery, Morgan Kaufmann, 2002.
[12] V. Danos, J. Krivine, Reversible communicating systems, in: CONCUR, Vol. 3170 of LNCS, Springer, 2004, pp. 292–307.

[13] V. Danos, J. Krivine, Transactions in RCCS, in: CONCUR, Vol. 3653 of LNCS, Springer, 2005, pp. 398–412.

[14] I. C. C. Phillips, I. Ulidowski, Reversing algebraic process calculi, J. Log. Algebr. Program. 73 (1-2) (2007) 70–96.

[15] R. Milner, Communicating and mobile systems - the π-calculus, Cambridge University Press, 1999.

[16] I. Lanese, C. A. Mezzina, J.-B. Stefani, Reversing higher-order pi, in: CONCUR, Vol. 6269 of LNCS, Springer, 2010, pp. 478–493.

[17] D. Sangiorgi, Bisimulation for higher-order process calculi, Inf. Comput. 131 (2) (1996) 141–178.

[18] I. Lanese, C. A. Mezzina, A. Schmitt, J.-B. Stefani, Controlling reversibility in higher-order pi, in: CONCUR, Vol. 6901 of LNCS, Springer, 2011, pp. 297–311.

[19] I. Lanese, M. Lienhardt, C. A. Mezzina, A. Schmitt, J.-B. Stefani, Concurrent flexible reversibility, in: 22nd European Symposium on Programming (ESOP), Vol. 7792 of Lecture Notes in Computer Science, Springer, 2013, pp. 370–390.

[20] I. Cristescu, J. Krivine, D. Varacca, A compositional semantics for the reversible p-calculus, in: LICS, IEEE Computer Society, 2013, pp. 388–397.

[21] M. Boreale, D. Sangiorgi, A fully abstract semantics for causality in the π-calculus, Acta Informatica 35 (5) (1998) 353–400.

[22] M. Lienhardt, I. Lanese, C. A. Mezzina, J.-B. Stefani, A reversible abstract machine and its space overhead, in: FMOODS/FORTE, 2012, pp. 1–17.

[23] D. Sangiorgi, Expressing mobility in process algebras: First-order and higher-order paradigms, PhD thesis CST-99-93, University of Edinburgh (1992).
[24] R. De Nicola, U. Montanari, F. W. Vaandrager, Back and forth bisimulations, in: CONCUR, Vol. 458 of LNCS, Springer, 1990, pp. 152–165.

[25] I. Hasuo, Generic forward and backward simulations, in: CONCUR, Vol. 4137 of LNCS, Springer, 2006, pp. 406–420.

[26] I. C. C. Phillips, I. Ulidowski, A logic with reverse modalities for history-preserving bisimulations, in: EXPRESS, Vol. 64 of EPTCS, 2011, pp. 104–118.

[27] J.-J. Lévy, An algebraic interpretation of the *lambda beta* k-calculus; and an application of a labelled *lambda*-calculus, Theor. Comput. Sci. 2 (1) (1976) 97–114.

[28] G. L. Cattani, P. Sewell, Models for name-passing processes: interleaving and causal, Inf. Comput. 190 (2).

[29] S. Crafa, D. Varacca, N. Yoshida, Compositional event structure semantics for the internal pi-calculus, in: CONCUR, Vol. 4703 of LNCS, Springer, 2007, pp. 317–332.

[30] D. Varacca, N. Yoshida, Typed event structures and the linear pi-calculus, Theor. Comput. Sci. 411 (19) (2010) 1949–1973.

[31] C. Fournet, G. Gonthier, The reflexive chemical abstract machine and the join-calculus, in: POPL, ACM, 1996, pp. 372–385.

[32] C. Fournet, G. Gonthier, The join calculus: A language for distributed mobile programming, in: APPSEM, Vol. 2395 of LNCS, Springer, 2000, pp. 268–332.

[33] R. Milner, Functions as processes, Mathematical Structures in Computer Science 2 (2) (1992) 119–141.

[34] D. Sangiorgi, From lambda to pi; or, rediscovering continuations, Mathematical Structures in Computer Science 9 (4) (1999) 367–401.

[35] H. P. Barendregt, The Lambda Calculus – Its Syntax and Semantics, revised Edition, North-Holland, 1984.

[36] A. Schmitt, J.-B. Stefani, The M-calculus: a higher-order distributed process calculus, in: POPL, ACM, 2003, pp. 50–61.
[37] S. Lenglet, A. Schmitt, J.-B. Stefani, Normal bisimulations in calculi with passivation, in: FOSSACS, Vol. 5504 of LNCS, Springer, 2009, pp. 257-271.

[38] S. M. Abramov, R. Glück, Principles of inverse computation and the universal resolving algorithm, in: The Essence of Computation, Vol. 2566 of Lecture Notes in Computer Science, Springer, 2002.

[39] K. Czarnecki, J. N. Foster, Z. Hu, R. Lämmel, A. Schürr, J. F. Terwilliger, Bidirectional transformations: A cross-discipline perspective, in: 2nd Int. Conference on Theory and Practice of Model Transformations (ICMT), Vol. 5563 of Lecture Notes in Computer Science, Springer, 2009.

[40] J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, A. Schmitt, Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem, ACM Trans. Program. Lang. Syst. 29 (3).

[41] Y. Lecerf, Machines de turing réversibles. Insolubilité récursive en $n \in \mathbb{N}$ de l'équation $n = \theta^n$, où $\theta$ est un "isomorphisme de codes", Comptes-Rendus Académie des Sciences 257 (1963) 2597-2600.

[42] C. H. Bennett, Logical reversibility of computation, IBM Journal of Research and Development 17 (6) (1973) 525-532.

[43] K. Morita, Reversible computing and cellular automata - a survey, Theoretical Computer Science 395 (1) (2008) 101-131.

[44] M. Zelkowitz, Reversible execution, Commun. ACM 16 (9).

[45] G. B. Leeman Jr., A formal approach to undo operations in programming languages, ACM Trans. Program. Lang. Syst. 8 (1) (1986) 50-87.

[46] S. Abramsky, A structural approach to reversible computation, Theor. Comput. Sci. 347 (3) (2005) 441-464.

[47] V. Danos, L. Regnier, Reversible, irreversible and optimal lambda-machines, Theor. Comput. Sci. 227 (1-2) (1999) 79-97.
[48] W. E. Kluge, A reversible se(m)cd machine, in: 11th International Workshop on Implementation of Functional Languages (IFL), no. 1868 in Lecture Notes in Computer Science, Springer, 1999.

[49] B. Stoddart, R. Lynas, F. Zeyda, A virtual machine for supporting reversible probabilistic guarded command languages, Electronic Notes in Theoretical Computer Science 253 (6).

[50] T. Yokoyama, R. Glück, A reversible programming language and its invertible self-interpreter, in: PEPM, 2007, pp. 144–153.

[51] T. Yokoyama, H. B. Axelsen, R. Glück, Principles of a reversible programming language, in: 5th Conference on Computing Frontiers, ACM, 2008, pp. 43–54.

[52] T. Yokoyama, H. B. Axelsen, R. Glück, Reversible flowchart languages and the structured reversible program theorem, in: ICALP, Vol. 5126 of LNCS, Springer, 2008, pp. 258–270.

[53] S. Mu, Z. Hu, M. Takeichi, An injective language for reversible computation, in: 7th International Conference Mathematics of Program Construction (MPC), no. 3125 in Lecture Notes in Computer Science, Springer, 2004, pp. 289–313.

[54] T. Yokoyama, H. B. Axelsen, R. Glück, Towards a reversible functional language, in: 3rd International Workshop on Reversible Computation (RC), Vol. 7165 of Lecture Notes in Computer Science, Springer, 2011.

[55] R. P. James, A. Sabry, Information effects, in: 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2012, pp. 73–84.

[56] V. Danos, J. Krivine, P. Sobocinski, General reversibility, in: EXPRESS, Vol. 175, 2007, pp. 75–86.

[57] V. Danos, J. Krivine, Formal molecular biology done in CCS-R, in: Bio-Concur, Vol. 180 of Electronic Notes in Theoretical Computer Science, Elsevier, 2007, pp. 31–49.
[58] I. Phillips, I. Ulidowski, S. Yuen, A reversible process calculus and the modelling of the erk signalling pathway, in: 4th International Workshop on Reversible Computation (RC), Vol. 7581 of Lecture Notes in Computer Science, 2013.

[59] R. M. Balzer, Exdams: extendable debugging and monitoring system, in: May 14-16, 1969, Spring Joint Computer Conference, AFIPS '69 (Spring), ACM, 1969, pp. 567-580.

[60] S. I. Feldman, C. B. Brown, Igor: A system for program debugging via reversible execution, in: Workshop on Parallel and Distributed Debugging, 1988, pp. 112-123.

[61] B. Boothe, Efficient algorithms for bidirectional debugging, in: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), ACM, 2000, pp. 299-310.

[62] E. Giachino, I. Lanese, C. A. Mezzina, Causal-consistent reversible debugging, in: 17th International Conference Fundamental Approaches to Software Engineering (FASE), Vol. 8411 of Lecture Notes in Computer Science, 2014, pp. 370-384.

[63] C. D. Carothers, K. S. Perumalla, R. Fujimoto, Efficient optimistic parallel simulations using reverse computation, ACM Transactions on Modeling and Computer Simulation 9 (3) (1999) 224-253.

[64] T. LeBlanc, J. Mellor-Crummey, Debugging parallel programs with instant replay, IEEE Trans. Comput. 36 (4).

[65] J. J. Cook, Reverse execution of java bytecode, Comput. J. 45 (6).

[66] H. Buhrman, J. Tromp, P. M. B. Vitányi, Time and space bounds for reversible simulation, in: 28th International Colloquium on Automata, Languages and Programming (ICALP), Vol. 2076 of Lecture Notes in Computer Science, Springer, 2001.

[67] P. M. B. Vitányi, Time, space, and energy in reversible computing, in: 2nd Conference on Computing Frontiers, ACM, 2005.

[68] N. KLarlund, F. Schneider, Proving nondeterministically specified safety properties using progress measures, Information and Computation 107 (1) (1993) 151-170.
[69] N. A. Lynch, F. W. Vaandrager, Forward and backward simulations: I. untimed systems, Inf. Comput. 121 (2).

[70] N. A. Lynch, F. W. Vaandrager, Forward and backward simulations, ii: Timing-based systems, Inf. Comput. 128 (1).

[71] I. Phillips, I. Ulidowski, Reversibility and asymmetric conflict in event structures, in: 24th International Conference on Concurrency Theory (CONCUR), Vol. 8052 of Lecture Notes in Computer Science, 2013.

[72] I. C. C. Phillips, I. Ulidowski, Reverse bisimulations on stable configuration structures, in: Proceedings 6th Workshop on Structural Operational Semantics (SOS), Vol. 18 of EPTCS, 2009.

[73] P. Degano, C. Priami, Non-interleaving semantics for mobile processes, Theoretical Computer Science 216 (1-2) (1999) 237-270.

[74] S. Crafa, D. Varacca, N. Yoshida, Event structure semantics of the parallel extrusion in the pi-calculus, in: 15th International Conference Foundations of Software Science and Computational Structures (FOSSACS), Vol. 7213 of Lecture Notes in Computer Science, Springer, 2012, pp. 225-239.
# Appendix A. Proofs of Section 2

## Appendix A.1. Proofs of Section 2.3

We prove in this section that consistent configurations are well formed. We need a few auxiliary results first. The lemma below gives a syntactic characterization of forward reductions.

**Lemma 38.** Let $M, N$ be configurations. Then $M \to N$ iff $M \equiv M'$ and $N' \equiv N$ with:

$$M' = \nu \tilde{u} . \kappa_1 : a \langle P \rangle | \kappa_2 : a(X) \triangleright Q | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$$

$$N' = \nu \tilde{u}, k . k : Q^{\{P\}/X} | [\kappa_1 : a \langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$$

**PROOF.** Let us start with the if direction. The proof is by induction on the derivation of the reduction $\to$. We have a case analysis on the last applied rule:

**R.Fw:** by hypothesis $M = \kappa_1 : a \langle P \rangle | \kappa_2 : a(X) \triangleright Q$ and $M \to \nu k . k : Q^{\{P\}/X}$, $[\kappa_1 : a \langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] = N$. The thesis follows by choosing $M' = M$ and $N' = N$.

**R.Eqv:** the thesis follows by transitivity of structural congruence.

**R.Ctx:** the proof is by case analysis on the structure of the context. The proof for the empty context is trivial. If the context is a restriction then we have that $\nu u . M \to \nu u . N$ with $M \to N$ as hypothesis. The thesis follows by adding $u$ to $\tilde{u}$. For (left) parallel context we have that $M_1 | M \to M_1 | N$ with $M \to N$ as hypothesis. By inductive hypothesis $M \equiv M'$ and $N' \equiv N$ with:

$$M' = \nu \tilde{u} . \kappa_1 : a \langle P \rangle | \kappa_2 : a(X) \triangleright Q | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$$

$$N' = \nu \tilde{u}, k . k : Q^{\{P\}/X} | [\kappa_1 : a \langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$$
Also, from Lemma 1 $M_1 \equiv \nu\tilde{v}$. $\prod_{i \in I'}(\kappa_i : \rho_i) | \prod_{j \in J'}[\mu_j; k_j]$. Then

$$M_1 | M \equiv \nu\tilde{u}, \tilde{v}. \kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q | \prod_{i \in I \cup I'} \kappa_i : \rho_i | \prod_{j \in J \cup J'} [\mu_j; k_j]$$

$$N'' = \nu\tilde{u}, \tilde{v}, k. k : Q^{\{P/X\}} | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] |$$

$$\prod_{i \in I \cup I'} \kappa_i : \rho_i | \prod_{j \in J \cup J'} [\mu_j; k_j]$$

with $N'' \equiv M_1 | N$ as desired. The case of right parallel context is similar.

For the only if direction, the desired reduction can be derived by applying rule (R.Fw) followed by (R.Ctx):

$$\nu\tilde{u}. \kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j] \to$$

$$\nu\tilde{u}, k. k : Q^{\{P/X\}} | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$$

The thesis then follows by applying rule (R.EQV). □

<figure><img src="image_12.png" /></figure>

The following lemma is similar to Lemma 38, but it considers backward reductions.

**Lemma 39.** Let $M, N$ be configurations. Then $M \rightsquigarrow N$ iff $M \equiv M'$ and $N' \equiv N$ with:

$$M' = \nu\tilde{u}, k. k : R | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$$

$$N' = \nu\tilde{u}. \kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} [\mu_j; k_j]$$

PROOF. Similar to the proof of Lemma 38. □

<figure><img src="image_13.png" /></figure>

We can now prove Lemma 3.

**Lemma 3.** Each consistent configuration $M$ is well formed
PROOF. By definition $M$ is consistent if there is an initial configuration $M_0$ such that $M_0 \Rightarrow M$. The proof is by induction on the number $n$ of steps in $M_0 \Rightarrow M$. For the base case, $n = 0$, we have to show that initial configurations are well formed. Conditions 1 and 4 in Definition 3 hold by definition of initial configuration. Conditions 2, 3 and 5 trivially hold since there are no memories.

For the inductive case, we have to show that if $M_0 \Rightarrow M \to N$ then $N$ is well formed. We know by inductive hypothesis that $M$ is well formed. The proof proceeds by case analysis on the derivation of $M \to N$.

Let us consider the case $M \twoheadrightarrow N$. By Lemma 38 we have $M \equiv M'$ and $N' \equiv N$ with $M' = \nu\tilde{u}.\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J}[\mu_j; k_j]$ and $\nu\tilde{u}, k, k : Q^{\{P/X\}} | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J}[\mu_j; k_j] = N'$. $M'$ is well formed since $M$ is well formed (well formedness is preserved by $\equiv$ since it is defined up to $\equiv$ itself). We have to prove that $N'$ is well formed. The properties 1-4 of Definition 3 check uniqueness of keys. They are all satisfied for existing tags, and they are satisfied by the new tag $k$ since it is a fresh key. The condition 5 holds for the new memory $[\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k]$ because of the form of the continuation. It holds for the other memories by hypothesis. Note that the condition on memories that generated the two threads tagged by $\kappa_1$ and $\kappa_2$ participating to the communication still holds, since the two threads are just moved from the top level to a memory.

The case $M \rightsquigarrow N$ is similar to the previous one, using Lemma 39 instead of Lemma 38. $\square$

## Appendix A.2. Proofs of Section 2.4

We prove in this section results relating rho$\pi$ and HO$\pi$ reductions. We first prove an auxiliary result relating rho$\pi$ and HO$\pi$ structural congruences.

**Lemma 40.** For all closed configurations $M, N$ if $M \equiv N$ then $\gamma(M) \equiv_{\pi} \gamma(N)$.

PROOF. It is enough to prove that the thesis holds for each axiom (since $\gamma$ is defined by structural induction). We have a case for each axiom. For the rules E.PARC, E.PARA, E.NILM, E.NewN, E.NewC, E.NewP and E.$\alpha$ there is a corresponding rule in HO$\pi$. Rules E.TAGN and E.TAGP instead reduce to the identity. $\square$
**Lemma 4.** For all closed configurations $M, N$, if $M \rightarrow N$ then $\gamma(M) \xrightarrow{\pi} \gamma(N)$

*PROOF.* By induction on the derivation of $M \rightarrow N$.

**R.Fw:** $M = \kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q \rightarrow \nu k$. $k : Q\{P/X\} | [a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] = N$. By definition $\gamma(M) = a\langle P \rangle | a(X) \triangleright Q \rightarrow_{\pi} Q\{P/X\} = \gamma(N)$.

**R.Eqv:** $M \rightarrow N$ with hypothesis $M \equiv M'$, $M' \rightarrow N'$ and $N' \equiv N$. By using the inductive hypothesis we have that $M' \rightarrow N'$ implies that $\gamma(M') \xrightarrow{\pi} \gamma(N')$ and since structural equivalence is preserved by $\gamma$ (by Lemma 40) we can conclude.

**R.Ctx:** the proof is by induction on the context. The case of the empty context is trivial. The case of a restriction of a key is trivial since the restriction is removed by $\gamma$. The case of restriction of a name follows by induction. The case of parallel composition follows by induction since $\gamma(M | N) = \gamma(M) | \gamma(N)$.

<figure><img src="image_14.png" /></figure>

To prove Lemma 5 we need a few auxiliary results. The first one characterizes the configurations $M$ such that $\gamma(M) = P$ for a given $HO_{\pi}$ process $P$.

**Lemma 41.** Let $P$ be a $HO_{\pi}$ process. If $\gamma(M) = P$ and $P \equiv_{\pi} P'$ with $P' = \nu \tilde{a}$. $\Pi_{i \in I} \rho_i$ and $\tilde{a} \subseteq \text{fn}(\Pi_{i \in I} \rho_i)$ then $M \equiv \nu \tilde{a}, \tilde{a}', \tilde{k}$. $\Pi_{i \in I} \kappa_i : \rho_i | \Pi_{j \in J} m_j$ with $\tilde{a}' \cap \text{fn}(\Pi_{i \in I} \kappa_i : \rho_i) = \emptyset$.

*PROOF.* By Lemma 1 $M \equiv \nu \tilde{u}$. $\Pi_{i' \in I'}(\kappa_i' : \rho_i') | \Pi_{j' \in J'} m_{j'} \equiv \nu \tilde{b}, \tilde{h}$. $\Pi_{i' \in I'}(\kappa_i' : \rho_i') | \Pi_{j' \in J'} m_{j'} = M'$ where we distinguish between names $\tilde{b}$ and keys $\tilde{h}$. By definition $\gamma(M') = \nu \tilde{b}$. $\Pi_{i' \in I'} \rho_{i'}$, but since $M \equiv M'$ by Lemma 40 we also have $\gamma(M) \equiv_{\pi} \gamma(M')$. Since $\gamma(M) = P \equiv_{\pi} P'$ we have $P' \equiv_{\pi} \gamma(M')$. Thus we have to prove that if $\nu \tilde{b}$. $\Pi_{i' \in I'} \rho_{i'} \equiv_{\pi} \nu \tilde{a}$. $\Pi_{i \in I} \rho_i$ then $\nu \tilde{b}, \tilde{h}$. $\Pi_{i' \in I'}(\kappa_i' : \rho_i') | \Pi_{j' \in J'} m_{j'} \equiv \nu \tilde{a}, \tilde{a}', \tilde{k}$. $\Pi_{i \in I} \kappa_i : \rho_i | \Pi_{j \in J} m_j$. We can set $\tilde{b} = \tilde{b}_1, \tilde{b}_2$ where $\tilde{b}_1 \subseteq \text{fn}(\Pi_{i' \in I'} \rho_{i'})$ and $\tilde{b}_2 \cap \text{fn}(\Pi_{i' \in I'} \rho_{i'}) = \emptyset$. We have $\nu \tilde{b}_1$. $\Pi_{i' \in I'} \rho_{i'} \equiv_{\pi} \nu \tilde{a}$. $\Pi_{i \in I} \rho_i$ which is derived using only $\alpha$-conversion and axioms E.ParC, E.ParA and
E.NilM. Using the same axioms we can derive also $\nu\tilde{b}, \tilde{h}$. $\Pi_{i' \in I'}(\kappa_i' : \rho_i')$ $|$ $\Pi_{j' \in J'} m_{j'} \equiv \nu\tilde{b}_2, \tilde{a}, \tilde{h}$. $\Pi_{i \in I}(\kappa_i : \rho_i)$ $|$ $\Pi_{j' \in J'} m_{j'}'$ (memories may be affected by $\alpha$-conversion). The thesis follows by choosing $\tilde{a}' = \tilde{b}_2, \tilde{h} = \tilde{k}$ and $\Pi_{j' \in J'} m_{j'}' = \Pi_{j \in J} m_j$. $\square$

The next lemma is the inverse of Lemma 40.

**Lemma 42.** Let $P$ and $P'$ be HO$\pi$ processes. If $P \equiv_{\pi} P'$ then for each configuration $M$ such that $\gamma(M) = P$ there is a configuration $N$ such that $N \equiv M$ and $\gamma(N) = P'$.

**PROOF.** Since both $\equiv_{\pi}$ and $\equiv$ are equivalence relations, it is enough to show the thesis for derivations of length one. The idea is that each axiom applied on HO$\pi$ processes can be applied to each corresponding rho$\pi$ configuration. This may require additional applications of axioms to deal with the additional rho$\pi$ structure. For instance, lifting axiom E.NEWC may require additional applications of the same axiom to deal with restrictions on keys. We do not report the detailed case analysis. $\square$

We can finally prove the inverse of Lemma 4.

**Lemma 5.** For all closed HO$\pi$ processes $R, S$ if $R \to_{\pi} S$ then for all closed configurations $M$ such that $\gamma(M) = R$ there is $N$ such that $M \twoheadrightarrow N$ and $\gamma(N) = S$.

**PROOF.** By induction on the derivation of the reduction $\to_{\pi}$.

**Com:** $R = a\langle P \rangle | a(X) \triangleright Q \to_{\pi} Q\{P/X\} = S$. Since $\gamma(M) = R$ by Lemma 41 we have that $M \equiv \nu\tilde{a}', \tilde{k}.\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q | M_1$ with $\tilde{a}' \cap \text{fn}(\Pi_{i \in I} \kappa_i : \rho_i) = \emptyset$ and $M_1$ composed only by memories. We have that $M \twoheadrightarrow \nu\tilde{a}', \tilde{k}, h.h: Q\{P/X\} | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; h] | M_1 = N$. Also, $\gamma(N) = \nu\tilde{a}'.Q\{P/X\} \equiv_{\pi} Q\{P/X\} = S$ as required.

**Eqv:** we have that $R \to_{\pi} S$ with hypothesis $R \equiv_{\pi} R'$, $R' \to_{\pi} S'$ and $S' \equiv_{\pi} S$. Taken $M$ such that $\gamma(M) = R$ from Lemma 42 there is $M' \equiv M$ such that $\gamma(M') = R'$. Then by inductive hypothesis there is $M''$ such that $M' \twoheadrightarrow M''$ and $\gamma(M'') = S'$. By applying again Lemma 42 we know that there is $M'''$ such that $M''' \equiv M''$ and $\gamma(M''') = S$. The thesis follows by applying rule (R.EQV).
**_Ctx:** we have $\mathbb{C}[R] \to_{\pi} \mathbb{C}[S]$ with hypothesis $R \to_{\pi} S$. Take $M$ such that $\gamma(M) = \mathbb{C}[R]$. Then there are $\mathbb{C}'$ and $M'$ such that $M = \mathbb{C}'[M']$ and $\gamma(M') = R$. Thus the thesis follows by inductive hypothesis using rule (R.Ctx).

□

# Appendix B. Proofs of Section 3

## Appendix B.1. Proofs of Section 3.1

We prove in this section that $\rho \circ \pi$ is causal consistent.

**Lemma 9 (Square Lemma).** If $t_1 = M \xrightarrow{\eta_1} M_1$ and $t_2 = M \xrightarrow{\eta_2} M_2$ are two coinicial concurrent transitions, then there exist two cofinal transitions $t_2/t_1 = M_1 \xrightarrow{\eta_2} N$ and $t_1/t_2 = M_2 \xrightarrow{\eta_2} N$.

**PROOF.** By case analysis on the form of transitions $t_1$ and $t_2$.

* $M \xrightarrow{m_1} N_1$ and $M \xrightarrow{m_2} N_2$. By Lemma 38 if $M \to N_1$ then $M \equiv M'$, $N' \equiv N_1$ with:

$$M' = \nu \tilde{u}. (\kappa_1 : a\langle P \rangle) \mid (\kappa_2 : a(X) \triangleright Q) \mid \prod_{i \in I} \kappa_i : \rho_i \mid \prod_{j \in J} [\mu_j; k_j]$$

$$N' = \nu \tilde{u}, k. (k : Q\{P^I/X\}) \mid m_1 \mid \prod_{i \in I} \kappa_i : \rho_i \mid \prod_{j \in J} [\mu_j; k_j]$$

and $m_1 = [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k]$. Similarly, if $M \to N_2$ then $M \equiv M'', N'' \equiv N_2$ with:

$$M'' = \nu \tilde{u}. (\kappa'_1 : a'\langle P' \rangle) \mid (\kappa'_2 : a'(X) \triangleright Q') \mid \prod_{i \in I'} \kappa_i : \rho_i \mid \prod_{j \in J} [\mu_j; k_j]$$

$$N'' = \nu \tilde{u}, k'. k' : Q'\{P^I/X\} \mid m_2 \mid \prod_{i \in I'} \kappa_i : \rho_i \mid \prod_{j \in J} [\mu_j; k_j]$$

and $m_2 = [\kappa'_1 : a'\langle P' \rangle | \kappa'_2 : a'(X) \triangleright Q'; k']$. Since the two transitions are concurrent (by hypothesis) we have that $\{\kappa_1, \kappa_2, k\} \cap \{\kappa'_1, \kappa'_2, k'\} = \emptyset$. Thus, we have:

$$M \equiv \nu \tilde{u}. (\kappa_1 : a\langle P \rangle) \mid (\kappa_2 : a(X) \triangleright Q) \mid (\kappa'_1 : a'\langle P' \rangle) \mid (\kappa'_2 : a'(X) \triangleright Q') \mid \prod_{i \in I''} \kappa_i : \rho_i \mid \prod_{j \in J} m_j$$

$$N_1 \equiv \nu \tilde{u}, k. (\kappa'_1 : a'\langle P' \rangle) \mid (\kappa'_2 : a'(X) \triangleright Q') \mid \prod_{i \in I''} \kappa_i : \rho_i \mid (\prod_{j \in J} m_j) \mid m_1$$
with $m_1 = [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k]$ and

$$N_2 \equiv \nu \tilde{u}, k'. (\kappa_1 : a\langle P \rangle) | (\kappa_2 : a(X) \triangleright Q) | \prod_{i \in I''} \kappa_i : \rho_i | (\prod_{j \in J} m_j) | m_2$$

We have that $N_2 \xrightarrow{m_1 \to} \nu \tilde{u}, k', k$. $\prod_{i \in I''} \kappa_i : \rho_i | (\prod_{j \in J} m_j) | m_2 | m_1$ and $N_1 \xrightarrow{m_2 \to} \nu \tilde{u}, k', k$. $\prod_{i \in I''} \kappa_i : \rho_i | (\prod_{j \in J} m_j) | m_2 | m_1$, as desired.

• $M \xrightarrow{m_1 \to} N_1$ and $M \xrightarrow{m_2 \to} N_2$. Since $M \xrightarrow{m_1 \to} N_1$ by Lemma 39 $M \equiv M'$ with:

$$M' = \nu \tilde{u}, k. k : R | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] | \prod_{i \in I'} \kappa_i : \rho_i | \prod_{j \in J'} m_j$$

$$N_1 \equiv \nu \tilde{u}. \kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J} m_j$$

and since $M \xrightarrow{m_2 \to} N_2$ then by Lemma 38 $M \equiv M''$ with:

$$M'' = \nu \tilde{u}. \kappa_1' : a'\langle P' \rangle | \kappa_2' : a'(X) \triangleright Q' | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J'} m_j$$

$$N_2 \equiv \nu \tilde{u}, k'. k' : Q'\{P'/X\} | m_2' | \prod_{i \in I} \kappa_i : \rho_i | \prod_{j \in J'} [\mu_j; k_j]$$

and $m_2' = [\kappa_1' : a\langle P' \rangle | \kappa_2' : a(X) \triangleright Q'; k']$. By hypothesis the two transitions are concurrent so $k$ is neither equal nor a suffix of $\kappa_1'$ or $\kappa_2'$. Thus, we have that

$$M \equiv \nu \tilde{u}, k'. k : R | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] | (\kappa_1' : a'\langle P' \rangle) |$$

$$(\kappa_2' : a'(X) \triangleright Q') | \prod_{i \in I''} \kappa_i : \rho_i | \prod_{j \in J''} m_j$$

$$N_1 \equiv \nu \tilde{u}. \kappa_1' : a'\langle P' \rangle | \kappa_2' : a'(X) \triangleright Q' | \kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q |$$

$$\prod_{i \in I''} \kappa_i : \rho_i | \prod_{j \in J''} m_j$$

$$N_2 \equiv \nu \tilde{u}, k', k. m_2' | k' : Q'\{P'/X\} | [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k] |$$

$$k : R | \prod_{i \in I''} \kappa_i : \rho_i | \prod_{j \in J''} m_j$$