# Causal Consistent Replication in Reversible Concurrent Calculi

Clément Aubert

► To cite this version:

Clément Aubert. Causal Consistent Replication in Reversible Concurrent Calculi. 2021. hal-03384482

HAL Id: hal-03384482

https://hal.science/hal-03384482

Preprint submitted on 22 Oct 2021

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.

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

Distributed under a Creative Commons Attribution 4.0 International License
# Causal Consistent Replication in Reversible Concurrent Calculi

Clément Aubert[0000-0001-6346-3043]

School of Computer & Cyber Sciences, Augusta University, Augusta, USA
aubert@augusta.edu, https://spots.augusta.edu/caubert/

**Abstract.** Reversible computation is key in developing new, energy-efficient paradigms, but also in providing forward-only concepts with broader definitions and finer frames of study. Among other fields, the algebraic specification and representation of networks of agents have been greatly impacted by the study of reversible phenomena: reversible definitions of the calculus of communicating systems (CCSK and RCCS) offer new semantic models, finer congruence relations, original properties, and revisits existing theories and results in a finer light. However, much remains to be done: concurrency, a central notion in establishing *causal consistency*—a crucial property for reversibly systems—, was never given a clear and syntactical definition in CCSK. While recursion was mentioned as a possible mechanism to inject infinite behaviors into the systems, replication was never studied. This work offers a solution to both problems, by leveraging a definition of concurrency developed for forward-only calculi using proved transition systems, by endowing CCSK with a replication operator, and by studying the interplay of both notions. The system we obtain is the first reversible system capable of representing infinite behaviors that enjoys causal consistency, for our simple and purely syntactical notion of reversible concurrency.

**Keywords:** Formal semantics · Process algebras and calculi · Reversible Computation · Concurrency · Replication

## 1 Introduction: Reversibility, Concurrency–Interplays

**Reversibility** has recently been dubbed “the future of life on earth” [45] in one of the National Science Foundation’s *Idea Machine*, as it “promote[s] a paradigm shift in the framing of research questions”, trying to locate “tipping points for irreversibility”. The study of bi-directional computation led to breakthroughs such as the design of CMOS adiabatic circuits [25] that will leverage Landauer’s principle [30, 31] to obtain “a greater level of energy efficiency than any other semiconductor[...] known today”. It also led to revisit established fields of computer science to obtain more general definitions, models, or tools, e.g. regarding complexity [40, 47], category [32], and automata [10, 29] theories, or “time-travel” debugging [54], to name a few.

**Concurrency Theory** has been re-shaped by reversibility as well: fine distinctions between causality and causation [48] contradicted Milner’s expansion
laws [38, Example 4.11], and the study of causal models for reversible computation led to novel correction criteria for causal semantics–both reversible and irreversible [16]. “Traditional” equivalence relations have been captured syntactically [5], while original observational equivalences were developed [38]: reversibility triggered a global reconsideration of established theories and tools, with the clear intent of providing actionable methods for reversible systems [34], novel axiomatic foundations [39] and original non-interleaving models [3, 16, 27].

**Two Systems** extend the Calculus of Communicating Systems (CCS) [44]–the godfather of π- [51], Ambient [42], applied [1] and distributed [28] calculi, among others–with reversible features. Reversible CCS (RCCS) [17] and CCS with keys (CCSK) [48] are similarly the source of most [2, 16, 41, 43]–if not all–of later systems developed to enhance reversible systems with some respect (roll-back operator, name-passing abilities, probabilistic features). Even if those two systems share a lot of similarities [36], they diverge in some respects that are not fully understood–typically, it seems that different notions of “contexts with history” led to establish the existence of congruences for CCSK [38, Proposition 4.9] or the impossibility thereof for RCCS [8, Theorem 2]. However, they also share some shortcomings, and we offer to tackle two of them for CCSK: a clear, syntactical, definition of concurrency that coincides with its forward-only counterpart, and the capacity of representing infinite behaviors.

**Reversible Concurrency** is of course a central notion in the study of RCCS and CCSK, as it enables the definition of “causal consistency”–a principle that, intuitively, states that backward reductions can undo an action only if its consequences have already been undone–and to obtain models where concurrency and causation are decorrelated [50]. As such, it have been studied from multiple angles, but, in our opinion, never in a fully satisfactory manner. Ad-hoc definitions relying on memory inclusion [33, Definition 3.11] or disjointness [17, Definition 7] for RCCS, and semantical notions for both RCCS [3–5] and CCSK [27, 49, 53] have been proposed, but, to our knowledge, have never been 1. compared to each other, 2. proven to be extensions of pre-existing forward-only definitions of concurrency. Our contribution starts by introducing the first purely syntactical definition of concurrency for CCSK, by extending the “universal” concurrency developed for forward-only CCS [19], that leveraged *proved* transition systems [22].

**Infinite Behaviors** can be captured in CCS using recursion ($CCS_D$), replication ($CCS_!$) or iteration, three strategies that are not equivalent [46] w.r.t. decidability of divergence [26] or termination [13]. Causal semantics for $CCS_!$ are scarce: aside from a multiset semantics for the π-calculus with replication [24], the only work [19] we are aware of that addresses $CCS_!'$s causal semantics remained unnoticed, despite its interest: it leverages an original notion of concurrency that was proven to be “universal” as it conservatively extends or agrees with pre-existing causal semantics of CCS and $CCS_D$ [19, Theorem 1]. In reversible concurrent systems, only recursion have been investigated [27, 33] or mentioned [17, 18], but without discussing causal consistency (with one exception [27, Lemma F.3]). Our contribution endows CCSK with the first reversible notion
of replication, and studies expected properties–such as the square diamond–as well as “reversible properties” for this infinite, reversible and concurrent system.

**Our Contribution** is in two parts: after briefly recalling CCS, its extensions to infinite behaviors and CCSK (Sect. 2), we define and study in detail our new causal semantics (Sect. 3.1). We make crucial use of the loop lemma (Lemma 3) to define concurrency between coinital traces in terms of concurrency between composable traces–a simple but ingenious mechanism that considerably reduces the definition and proof burdens. We then prove the “usual” sanity checks–the square and diamond properties (Sect. 3.2)–and discuss other important properties–among which causal consistency (Sect. 3.3).

We then discuss the interactions between extensions to infinite behavior and reversibility (Sect. 4.1), and justify our choice of endowing CCSK with replication (Sect. 4.2). Our definition of concurrency is then extended to accommodate infinite behaviors, and most of our sanity checks are still valid (Sect. 4.3), even if our processes can now sometimes have two conflicting backward reductions–a phenomenon not observed in any other reversible system, to our knowledge. This oddity is then taken care of thanks to a simple restriction on identifiers, and causal consistency is restored (Sect. 4.4).

Our construction is built from simple definitions that are originally combined to obtain elegantly results–typically, the square property is derived from what we called the forward and sideways diamonds by leveraging the loop lemma–in the vein of the “axiomatic approach” to reversibility [39]. We also briefly discuss structural congruence (Remark 2), and sketch possible strategies to study infinite behaviors that duplicate their past. All proofs are included in Sect. A for completeness, with their main arguments given in the body of the paper. A small technical lemma, intuitively explained in the body of the paper, is added in Sect. B for completeness.

# 2 Infinite and Reversible Process Calculi

## 2.1 CCS with Infinite Behaviors

**Finite Core CCS** We briefly recall the (forward-only) “finite fragment” of the core of CCS (simply called CCS) following a standard presentation [13]. The three different strategies to extend CCS with infinite behavior–excluding recursion expressions and parametric definitions [26]–will come in a second moment.

**Definition 1 ((Co-)names and labels).** Let $N = \{a, b, c, \dots\}$ be a set of names and $\overline{N} = \{\overline{a}, \overline{b}, \overline{c}, \dots\}$ its set of co-names. The set of labels $L$ is $N \cup \overline{N} \cup \{\tau\}$, and we use $\alpha, \beta$ (resp. $\lambda$) to range over $L$ (resp. $L \setminus \{\tau\}$). A bijection $\tau: N \to \overline{N}$, whose inverse is also written $\overline{\tau}$, gives the complement of a name.

**Definition 2 (Operators).** CCS processes are defined as usual:
$$P, Q := P \setminus \alpha \qquad (\text{Restriction}) \qquad \alpha.P \qquad (\text{Prefix})$$
$$P + Q \qquad (\text{Sum}) \qquad P | Q \qquad (\text{Parallel composition})$$

The inactive process 0 is omitted when preceded by a prefix, and the biding power of the operators, from highest to lowest, is $\setminus\alpha$, $\alpha$, ! (replication, introduced next), + and |, so that e.g. $\alpha.P + Q\setminus\alpha |!P + a$ is to be read as $((\alpha.P) + (Q\setminus\alpha)) | ((!P) + (a.0))$. In a process $P | Q$, we call $P$ and $Q$ threads.

The labeled transition system (LTS) for CCS, denoted $\xrightarrow{\alpha}$, is reminded in Fig. 1, where the “Infinite Group” should be ignored for now.

<figure><img src="image_2.png" /><figcaption>Fig. 1. Rules of the labeled transition system (LTS) for CCS, $CCS_D$, $CCS_!$ and $CCS_*$</figcaption></figure>

**Infinite CCS** Usually, the following three alternative approaches to the addition of infinite behaviors to CCS are explored and compared [12, 13].

**Definition 3.** $CCS_D$ (“CCS with recursion”) is obtained by adding a denumerable set of constants, ranged over by $D$, the production rule $P := D$ to Definition 2, and the rule $\text{const.}$ to the LTS.

$CCS_!$ (“CCS with replication”) is obtained by adding the production rule $P := !P$ to Definition 2, and the rule $\text{repl.}_0$ to the LTS.
CCS\* ("CCS with iteration") is obtained by adding the production rules $P := P^*$ and $P := P; Q$ to Definition 2, and the rule iter. to the LTS.

The complete definition of CCS\* is more involved, as the sequential composition $P; Q$ requires its own rules and an auxiliary predicate [13, pp. 1195–1196].

*Remark 1.* Adopting the rules repl.₁ and repl.₂ instead of repl.₀ does not change the computational nor decisional power, but gives a finitely branching transition system [13, Section 4.3.1], among other benefits [51, pp. 42-43]. We will use those rules instead of repl.₀ in CCS₁, as commonly done [13, 19].

## 2.2 CCSK: A “Keyed” Reversible Concurrent Calculus

CCSK captures uncontrolled reversibility using two symmetric LTS—one for forward computation, one for backward computation—that manipulates keys marking executed prefixes, to guarantee that reverting synchronizations cannot be done without both parties agreeing. We use the syntax of the latest paper on the topic [38], that slightly differs [38, Remark 4.2] with the classical definition [48]. However, those changes have no impact since we refrain from using CCSK’s newly introduced structural congruence, as discussed in Remark 2, p. 15.

**Definition 4 (Keys, prefixes and CCSK processes).** Let $K = \{m, n, \dots\}$ be a set of keys, we let $k$ range over them. Prefixes are of the form $\alpha[k]$—we call them keyed labels—or $\alpha$. CCSK processes are CCS processes where the prefix can also be of the form $\alpha[k]$, we let $X, Y$ range over them.

The forward LTS for CCSK, that we denote $\xrightarrow{\alpha[k]}$, is given in Fig. 2—with key and std defined below. The reverse LTS $\xleftarrow{\alpha[k]}$ is the exact symmetric of $\xrightarrow{\alpha[k]}$ [38, Figure 2] (it can also be read from Fig. 3), and we write $X \xrightarrow{\alpha[k]} Y$ if $X \xleftarrow{\alpha[k]} Y$ or $X \xrightarrow{\alpha[k]} Y$. For all three types of arrows, we sometimes omit the label and keys when they are not relevant, and mark with \* their transitive closures. As usual, we restrict ourselves to reachable processes, defined below.

**Definition 5 (Standard and reachable processes).** Given a CCSK process $X$, key($X$) is the set of keys occurring in $X$, and $X$ is standard-std($X$)—iff $\text{key}(X) = \emptyset$. If there exists a process $O_X$ s.t. std($O_X$) and $O_X \dashv\!* X$, then $X$ is reachable.

The reader eager to see this system in action can fast-forward to Example 1, p. 9, but should be aware that this example uses proved labels, introduced next.

## 3 A New Causal Semantics for CCSK

As discussed in the introduction, the only causal semantics for CCS₁ we are aware of [19] remained unnoticed, despite some interesting qualities: 1. it enables the definition of causality for replication while agreeing with pre-existing causal
Action, Prefix and Restriction

$$
\begin{array}{ccc}
\text{std}(X) & \xrightarrow[\alpha.X \xrightarrow{\alpha[k]} \alpha[k].X]{\alpha[k]} \text{act.} & k \neq k' \xrightarrow[\alpha[k'.X \xrightarrow{\alpha[k]} \alpha[k'.X]]{X \xrightarrow{\beta[k]} X'} \text{pre.} \\
& & \\
& a \notin \{\alpha, \bar{\alpha}\} \xrightarrow[X \setminus a \xrightarrow{\alpha[k]} X']{X \xrightarrow{\alpha[k]} X'} \text{res.} \\
& &
\end{array}
$$

Parallel Group

$$
\begin{array}{ccc}
k \notin \text{key}(Y) & \frac{X \xrightarrow{\alpha[k]} X'}{X \mid Y \xrightarrow{\alpha[k]} X' \mid Y} \mid_L & k \notin \text{key}(X) \frac{Y \xrightarrow{\alpha[k]} Y'}{X \mid Y \xrightarrow{\alpha[k]} X \mid Y'} \mid_R \\
& & \\
& \frac{X \xrightarrow{\lambda[k]} X' \quad Y \xrightarrow{\bar{\lambda}[k]} Y'}{X \mid Y \xrightarrow{\tau[k]} X' \mid Y'} \text{syn.}
\end{array}
$$

Sum Group

$$
\text{std}(Y) \quad \frac{X \xrightarrow{\alpha[k]} X'}{X + Y \xrightarrow{\alpha[k]} X' + Y} +_L \quad \text{std}(X) \quad \frac{Y \xrightarrow{\alpha[k]} Y'}{X + Y \xrightarrow{\alpha[k]} X + Y'} +_R
$$

<caption>Fig. 2. Rules of the forward labeled transition system (LTS) for CCSK</caption>

semantics of CCS and CCS<sub>D</sub> [19, Theorem 1] 2. it leverages the technique of
proved transition systems that encodes information about the derivation in the
labels [22], 3. it was instrumental in one of the first result connecting implicit
computational complexity and distributed processes [23], 4. last but not least, as
we will see below, it allows to define an elegant notion of causality for CCSK with
“built-in” reversibility, as *the exact same definition will be used for forward and
backward transitions*, without making explicit mentions of the keys or directions.
We comment on existing causal semantics for CCS-like reversible process calculi
before diving into the technical details.

In RCCS, the definition of concurrency fluctuated between a condition on
memory inclusion for composable transitions [33, Definition 3.11] and a condi-
tion on disjointness of memories on coinital transitions [17, Definition 7], both
requiring the entire memory of the thread to label the transitions. Concurrency
have also been studied using configuration structures for RCCS semantics [3–5].
We conjecture (an adaptation of) our definition (to RCCS) to be equivalent to
those three definitions, that have not been proven themselves equivalent. In any
case, whether those definitions conservatively extend CCS’s causality have not
been proven, and they do not account for infinite behaviors.

In CCSK, forward and reverse diamond properties were proven using con-
ditions on keys and “joinable” transitions [48, Propositions 5.10 and 5.19], but
to our knowledge no “definitive” definition of concurrency was proposed. No-
tions of concurrency could probably be “imported” from semantical models of CCSK [27, 49, 53], but have not been to our knowledge.

Those takes on concurrency impacted all the extensions to RCCS and CCSK, e.g. reversible higher-order π-calculus [37, Definition 9], reversible π-calculus [15, Definition 4.1] or croll-π [35, Definition 1], where similar definitions of concurrency were adopted. One of the downside of those syntactical definitions is, in our opinion, that too much importance is given to keys or identifiers, that should only be technical annotations disallowing processes that have been synchronized to backtrack independently. We have previously defended that identifier should be considered only up to isomorphisms [5, p. 13], or explicitly generated by a built-in mechanism [8, p. 152], and re-inforce this point of view by providing CCSK with a concurrency mechanism that does not need to consider keys.

We believe our choice is additionally compact, elegant and suited for reversible computation: defining concurrency on composable transitions first allows not to consider keys or identifiers in our definition, as the LTS guarantees that the same key will not be re-used. Then, the loop lemma allows to “reverse” transitions so that concurrency on coinitial transitions can be defined from concurrency on composable transitions. This allows to carry little information in the labels–the direction is not needed–and to have a definition insensible to keys and identifiers for the very modest cost of prefixing labels with some annotation tracing back the thread(s) performing the transition.

## 3.1 Proved Labeled Transition System for CCSK

We adapt the proved transition system [14, 19, 20] to CCSK: this technique enriches the transitions label with prefixes that describe parts of their derivation, to keep track of their dependencies or lack thereof. We adapt an earlier formalism [21] that does not record information about sums [19, footnote 2], but extend the concurrency relation to internal (i.e. τ-) transitions, omitted from recent work [19, Definition 3] but present in older articles [14, Definition 2.3].

**Definition 6 (Enhanced keyed labels).** Let $v$ range over strings in $\{|_L, |_R\}^*$, enhanced keyed labels are defined as

$$ \theta := v\alpha[k] \parallel v\langle|_L v_L\alpha[k], |_R v_R\bar{\alpha}[k]\rangle $$

We write $E$ the set of enhanced keyed labels, and define $\ell: E \to L$ and $\bar{\ell}: E \to K$:

$$ \ell(v\alpha[k]) = \alpha $$

$$ \ell(v\langle|_L v_L\alpha[k], |_R v_R\bar{\alpha}[k]\rangle) = \tau $$

$$ \bar{\ell}(v\alpha[k]) = k $$

$$ \bar{\ell}(v\langle|_L v_L\alpha[k], |_R v_R\bar{\alpha}[k]\rangle) = k $$

We present in Fig. 3 the rules for the proved forward and backward LTS for CCSK. The rules $|_R, |_R, +_R$ and $+|_R$ are omitted but can easily be inferred.

**Definition 7 (Dependency relation).** The dependency relation on enhanced keyed labels is induced by the axioms below, for $d \in \{L, R\}$:

$$ \alpha[k] \ll \theta \qquad |_d \theta \ll |_d \theta' \qquad \text{if } \theta \ll \theta' \qquad \langle\theta_L, \theta_R\rangle \ll \theta \qquad \text{if } \exists d \text{ s.t. } \theta_d \ll \theta \\ \theta \ll \langle\theta_L, \theta_R\rangle \qquad \text{if } \exists d \text{ s.t. } \theta \ll \theta_d \qquad \langle\theta_L, \theta_R\rangle \ll \langle\theta'_L, \theta'_R\rangle \qquad \text{if } \exists d \text{ s.t. } \theta_d \ll \theta'_d $$
Action, Prefix and Restriction

Forward

$$
\text{std}(X) \xrightarrow{\alpha \cdot X \xrightarrow{\alpha[k]} \alpha[k].X} \text{act.}
$$

$$
\mathcal{K}(\theta) \neq k \quad \frac{X \xrightarrow{\theta} X'}{\alpha[k].X \xrightarrow{\theta} \alpha[k].X'} \text{ pre.}
$$

$$
\ell(\theta) \notin \{\alpha, \bar{\alpha}\} \frac{X \xrightarrow{\theta} X'}{X \setminus a \xrightarrow{\theta} X' \setminus a} \text{res.}
$$

Backward

$$
\text{std}(X) \xrightarrow{\alpha[k].X \xrightarrow{\alpha[k]} \alpha \cdot X} \text{act.}
$$

$$
\mathcal{K}(\theta) \neq k \quad \frac{X' \xrightarrow{\theta} X}{\alpha[k].X' \xrightarrow{\theta} \alpha[k].X} \text{ pre.}
$$

$$
\ell(\theta) \notin \{\alpha, \bar{\alpha}\} \frac{X' \xrightarrow{\theta} X}{X' \setminus a \xrightarrow{\theta} X \setminus a} \text{res.}
$$

Parallel Group

Forward

$$
\mathcal{K}(\theta) \notin \text{key}(Y) \quad \frac{X \xrightarrow{\theta} X'}{X | Y \xrightarrow{|_L \theta} X' | Y}
$$

$$
\frac{X \xrightarrow{\theta_L \lambda[k]} X' \quad Y \xrightarrow{\theta_R \bar{\lambda}[k]} Y'}{X | Y \xrightarrow{\langle |_L \theta_L \lambda[k], |_R \theta_R \bar{\lambda}[k] \rangle} X' | Y'} \text{syn.}
$$

Backward

$$
\mathcal{K}(\theta) \notin \text{key}(Y) \quad \frac{X' \xrightarrow{\theta} X}{X' | Y \xrightarrow{\theta} X | Y} \mathbf{|_L}
$$

$$
\frac{X' \xrightarrow{\theta_L \lambda[k]} X \quad Y' \xrightarrow{\theta_R \bar{\lambda}[k]} Y}{X' | Y' \xrightarrow{\langle |_L \theta_L \lambda[k], |_R \theta_R \bar{\lambda}[k] \rangle} X | Y} \text{syn.}
$$

Sum Group

Forward

$$
\text{std}(Y) \frac{X \xrightarrow{\theta} X'}{X + Y \xrightarrow{\theta} X' + Y} +_L
$$

Backward

$$
\text{std}(Y) \frac{X' \xrightarrow{\theta} X}{X' + Y \xrightarrow{\theta} X + Y} +_{L}^{\bullet}
$$

<caption>Fig. 3. Rules of the *proved* LTS for CCSK</caption>

A dependency $\theta_0 < \theta_1$ means “whenever there is a trace in which $\theta_0$ occurs before $\theta_1$, then the two associated transitions are causally related”. The following definitions will enable more formal examples, but we can stress that 1. the first rule enforces the fact that executing or reversing a prefix at top level, e.g. $\alpha.X \xrightarrow{\alpha[k]} \alpha[k].X$ or $\alpha[k].X \rightsquigarrow \alpha.X$, makes the prefix $(\alpha[k])$ a dependency of all further transitions; 2. as the forward and backward versions of the same rule share the same enhanced keyed labels, a trace where a transition and its reverse both occur will have the first occurring be a dependency of the second, as $<$ is reflexive; 3. whenever reasoning by case over $\theta$, we can assume w.l.o.g. that e.g. an enhanced key label $|_R \theta$ was “ultimately” produced by a transition from a process of the form $X | Y$: while the actual process may have $+$, $\setminus a$ and $\alpha[k]$ operators “wrapping” $X | Y$, they have no impact on the dependencies nor on the properties we will be proving, and thus we can assume w.l.o.g. that a term capable of performing a transition labeled by a prefix (resp. prefixed by $|_L$, $|_R$, $\langle \theta_L, \theta_R \rangle$) can always be assumed to have for primary connector the same prefix
(resp. a parallel composition). This is made formal in Sect. B, for the calculus including the replication operator as well, and formally used only in Lemma 4.

**Definition 8 (Transitions and traces).** In a transition $t: X \xrightarrow{\theta} X'$, $X$ is the source, and $X'$ is the target of $t$. Two transitions are coinitial (resp. cofinal) if they have the same source (resp. target). Transitions $t_1$ and $t_2$ are composable, $t_1; t_2$, if the target of $t_1$ is the source of $t_2$. The reverse of $t: X' \xrightarrow{\theta} X$ is $t^\bullet: X \xrightarrow{\theta} X'$, and similarly if $t$ is backward, letting $(t^\bullet)^\bullet = t'^\bullet = t$.<fnref n="1" />

A sequence of pairwise composable transitions $t_1; \dots; t_n$ is called a trace, denoted $T$, and $\epsilon$ is the empty trace.

**Definition 9 (Causality relation).** Let $T$ be a trace $X_1 \xrightarrow{\theta_1} \dots \xrightarrow{\theta_n} X_n$ and $i, j \in \{1, \dots, n\}$ with $i < j$, $\theta_i$ causes $\theta_j$ in $T$ ($\theta_i \prec_T \theta_j$) iff $\theta_i \prec \theta_j$.

**Definition 10 (Concurrency).** Let $T$ be a trace $X_1 \xrightarrow{\theta_1} \dots \xrightarrow{\theta_n} X_n$ and $i, j \in \{1, \dots, n\}$, $\theta_i$ is concurrent with $\theta_j$ ($\theta_i \prec_T \theta_j$, or simply $\theta_i \prec \theta_j$) iff neither $\theta_i \prec_T \theta_j$ nor $\theta_j \prec_T \theta_i$.

*Example 1.* Consider the following trace, dependencies, and concurrent transitions, where the subscripts to $\prec$ and $\succ$ have been omitted:

$$ \begin{array}{l@{\quad}l} (a.\bar{b}) | (b+c) & \phantom{\text{and, as a consequence,}} \\ \xrightarrow{|_L a[m]} a[m].\bar{b} | b+c & \text{and we have, e.g.} \\ \xrightarrow{|_L \bar{b}[n]} a[m].\bar{b}[n] | b+c & \qquad |_L \bar{b}[n] \prec |_L \bar{b}[n] \\ \xrightarrow{|_R c[n']} a[m].\bar{b}[n] | b+c[n'] & \qquad |_L a[m] \prec |_L \bar{b}[n] \qquad \text{as } a[m] \prec \bar{b}[n] \\ \xrightarrow{\sim|_L \bar{b}[n]} a[m].\bar{b} | b+c[n'] & \text{and, as a consequence,} \\ \xrightarrow{\sim|_R c[n']} a[m].\bar{b} | b+c & \qquad |_L a[m] \prec \langle |_L \bar{b}[n], |_R b[n] \rangle \\ \xrightarrow{\sim|_L \bar{b}[n], |_R b[n]} a[m].\bar{b}[n] | b[n] + c & \text{but} \\ \xrightarrow{\langle |_L \bar{b}[n], |_R b[n] \rangle} a[m].\bar{b}[n] | b[n] + c & \qquad |_L \bar{b}[n] \succ |_R c[n] \\ & \qquad \text{as labels prefixed by } |_L \text{ and } |_R \text{ are never} \\ & \qquad \text{causes of each others.} \end{array} $$

$$ |_L \bar{b}[n] \prec |_L \bar{b}[n] \qquad \text{as } \bar{b}[n] \prec \bar{b}[n] $$

$$ |_L a[m] \prec |_L \bar{b}[n] \qquad \text{as } a[m] \prec \bar{b}[n] $$

$$ |_L a[m] \prec \langle |_L \bar{b}[n], |_R b[n] \rangle $$

$$ |_L \bar{b}[n] \succ |_R c[n] $$

To prove the results in the next section, we need a convoluted but straightforward lemma that decomposes concurrent traces involving two threads into one trace involving one thread while maintaining concurrency, i.e. proving that transitions e.g. of the form $T: X | Y \xrightarrow{|_L \theta} X' | Y \xrightarrow{|_L \theta'} X'' | Y$ with $|_L \theta \prec_T |_L \theta'$ can be decomposed into transitions $T': X \xrightarrow{\theta} X' \xrightarrow{\theta'} X''$ with $\theta \prec_T \theta'$.

**Lemma 1 (Decomposing concurrent transitions).** Let $i \in \{1, 2\}$ and $\theta_i \in \{|_L \theta'_i, |_R \theta''_i, \langle |_L \theta'_i, |_R \theta''_i \rangle\}$, and define $\pi_L(X_L | X_R) = X_L$, $\pi_L(|_L \theta) = \theta$, $\pi_L(\langle |_L \theta_L, |_R \theta_R \rangle) = \theta_L$, $\pi_L(|_R \theta) = \text{undefined}$, and define similarly $\pi_R$.

<footnote n="1">¹ The existence and uniqueness of the reverse transition is immediate in CCSK. This property, known as the loop lemma (Lemma 3) is sometimes harder to obtain.</footnote>
Whenever $T: X_L | X_R \xrightarrow{\theta_1} Y_L | Y_R \xrightarrow{\theta_2} Z_L | Z_R$ with $\theta_1 \prec_T \theta_2$, then for $d \in \{\text{L, R}\}$, if $\pi_d(\theta_1)$ and $\pi_d(\theta_2)$ are both defined, then, $\pi_d(\theta_1) \prec_{\pi_d(T)} \pi_d(\theta_2)$ with $\pi_d(T): \pi_d(X_L | X_R) \xrightarrow{\pi_d(\theta_1)} \pi_d(Y_L | Y_R) \xrightarrow{\pi_d(\theta_2)} \pi_d(Z_L | Z_R)$.

*Proof.* The trace $\pi_d(T)$ exists by virtue of the rule $|_d$, syn. or their reverses. That $\pi_d(\theta_1) \prec_{\pi_d(T)} \pi_d(\theta_2)$ essentially comes from the fact that if one was causing the other, then $\theta_1 \prec_T \theta_2$ would not hold, a contradiction. $\square$

## 3.2 Diamonds and Squares: Concurrency in Action

Square properties and concurrency diamonds express that concurrent transitions are *actually* independent, in the sense that they can “later on” agree (the square property, Theorem 3) or be swapped (the forward diamond, Theorem 1, if both transitions are forward, or “sideways” diamond, Theorem 2, if they have opposite directions). That our definition of concurrency enables those, and allows to inter-prove them, is a good indication that it is resilient and convenient to use.

**Theorem 1 (Forward diamond).** For all $X \xrightarrow{\theta_1} X_1 \xrightarrow{\theta_2} Y$ with $\theta_1 \prec \theta_2$, there exists $X_2$ s.t. $X \xrightarrow{\theta_2} X_2 \xrightarrow{\theta_1} Y$.

The proof, p. 11, requires a particular care when $X$ is not standard. Using pre. is transparent from the perspective of enhanced keyed labels, as no “memory” of its usage is stored in the label of the transition. This is essentially because–exactly like for act.-all the dependency information is already present in the term or its enhanced keyed label. To make this more formal, we introduce a function that “removes” a keyed label, and prove that it does not affect derivability.

**Definition 11.** Given $\alpha$ and $k$, we define $\text{rm}_{\alpha[k]}$ by $\text{rm}_{\alpha[k]}(0) = 0$ and

$$ \text{rm}_{\alpha[k]}(\beta.X) = \beta.X \qquad \text{rm}_{\alpha[k]}(X|Y) = \text{rm}_{\alpha[k]}(X) | \text{rm}_{\alpha[k]}(Y) $$

$$ \text{rm}_{\alpha[k]}(X \setminus a) = (\text{rm}_{\alpha[k]}(X) \setminus a) \qquad \text{rm}_{\alpha[k]}(X+Y) = \text{rm}_{\alpha[k]}(X) + \text{rm}_{\alpha[k]}(Y) $$

$$ \text{rm}_{\alpha[k]}(\beta[m].X) = \begin{cases} X & \text{if } \alpha = \beta \text{ and } k = m \\ \beta[m].\text{rm}_{\alpha[k]}(X) & \text{otherwise} \end{cases} $$

We let $\text{rm}_k^\lambda = \text{rm}_{\lambda[k]} \circ \text{rm}_{\lambda[k]}$ if $\lambda \in L \setminus \{\tau\}$, $\text{rm}_k^\tau = \text{rm}_{\tau[k]}$ otherwise.

The function $\text{rm}_{\alpha[k]}$ simply looks for an occurrence of $\alpha[k]$ and removes it: as there is at most one, there is no need for a recursive call when it is found. This function preserves derivability of transitions that do not involve the key removed:

**Lemma 2.** For all $X$, $\alpha$ and $k$, $X \xrightarrow{\theta} Y$ with $\mathcal{K}(\theta) \neq k$ iff $\text{rm}_k^\alpha(X) \xrightarrow{\theta} \text{rm}_k^\alpha(Y)$.
**Proof.** Assume $\alpha[k]$ or $\bar{\alpha}[k]$ (if $\alpha \neq \tau$) occur in $X$ (otherwise the result is straightforward), as $\mathcal{R}(\theta) \neq k$, the same holds for $Y$. As keys occur at most twice, attached to complementary names, in reachable processes [38, Lemma 3.4], $k \notin \text{key}(\text{rm}_k^\alpha(X)) \cup \text{key}(\text{rm}_k^\alpha(Y))$. Then the proof follows from simple induction on the length of the derivation for $X \xrightarrow{\theta} Y$: as neither pre. nor pre.\textbullet change the enhanced keyed label, we can simply “take out” the occurrences of those rules when they concern $\alpha[k]$ or $\bar{\alpha}[k]$ and still obtain a valid derivation, with the same enhanced keyed label, hence yielding $\text{rm}_k^\alpha(X) \xrightarrow{\theta} \text{rm}_k^\alpha(Y)$. For the converse direction, pre. or pre.\textbullet can be re-added to the derivation tree and in the same location, as $k$ is fresh in $\text{rm}_k^\alpha(X)$ and $\text{rm}_k^\alpha(Y)$. $\square$

**Proof (of Theorem 1).** The proof proceeds by induction on the length of the deduction for the derivation for $X_1 \xrightarrow{\theta_1} X_2$, using Lemma 1 to enable the induction hypothesis if $\theta_1 = |_L \theta'_1$, $|_R \theta'_1$ or $\langle |_L \theta'_L, |_R \theta'_R \rangle$. The only delicate case is if the last rule is pre.: in this case, there exists $\alpha, k, X'$ and $X'_1$ s.t. $X = \alpha[k].X' \xrightarrow{\theta_1} \alpha[k].X'_1 = X_1$ and $\mathcal{R}(\theta_1) \neq k$. As $\alpha[k].X'_1 \xrightarrow{\theta_2} Y$, $\mathcal{R}(\theta_2) \neq k$ [38, Lemma 3.4], and since $\theta_1 \prec \theta_2$, we apply Lemma 2 twice to obtain the trace $T$:

$$ \text{rm}_k^\alpha(\alpha[k].X') = X' \xrightarrow{\theta_1} \text{rm}_k^\alpha(\alpha[k].X'_1) = X'_1 \xrightarrow{\theta_2} \text{rm}_k^\alpha(Y) $$

with $\theta_1 \prec_T \theta_2$, and we can use the induction hypothesis to obtain $X_2$ s.t. $X' \xrightarrow{\theta_2} X_2 \xrightarrow{\theta_1} \text{rm}_k^\alpha(Y)$. Since $\mathcal{R}(\theta_2) \neq k$, we can append pre. to the derivation of $X' \xrightarrow{\theta_2} X_2$ to obtain $\alpha[k].X' = X \xrightarrow{\theta_2} \alpha[k].X_2$. Using Lemma 2 one last time, we obtain that $\text{rm}_k^\alpha(\alpha[k].X_2) = X_2 \xrightarrow{\theta_1} \text{rm}_k^\alpha(Y)$ implies $\alpha[k].X_2 \xrightarrow{\theta_1} Y$, which concludes this case. $\square$

**Example 2.** Re-using Example 1, since $|_L \bar{b}[n] \prec |_R c[n']$ in

$$ a[m].\bar{b} \mid b + c \xrightarrow{|_L \bar{b}[n]} a[m].\bar{b}[n] \mid b + c \xrightarrow{|_R c[n']} a[m].\bar{b}[n] \mid b + c[n'], $$

Theorem 1 allows to re-arrange this trace as

$$ a[m].\bar{b} \mid b + c \xrightarrow{|_R c[n']} a[m].\bar{b} \mid b + c[n'] \xrightarrow{|_L \bar{b}[n]} a[m].\bar{b}[n] \mid b + c[n'], $$

**Theorem 2 (Sideways diamond).** For all $X \xrightarrow{\theta_1} X_1 \xrightarrow{\theta_2} Y$ with $\theta_1 \prec \theta_2$, there exists $X_2$ s.t. $X \xrightarrow{\theta_2} X_2 \xrightarrow{\theta_1} Y$.

It should be noted that in the particular case of $t; t^\bullet : X \xrightarrow{\theta_1} X_1 \xrightarrow{\theta_1} X$, $\theta_1 \prec \theta_1$ by reflexivity of $\prec$ and hence the sideways diamond cannot apply.

**Proof.** We can re-use the proof of Theorem 1 almost as it is: Lemmas 1 and 2 hold for both directions, so we can use them for backward transitions. The only case that slightly diverges is if the deduction for $X \xrightarrow{\theta_1} X_1$ have for last rule pre. In this case, $\alpha[k].X' \xrightarrow{\theta_1} \alpha[k].X'_1 \xrightarrow{\theta_2} Y$, but we cannot deduce that $\mathcal{R}(\theta_2) \neq k$ immediately. However, if $\mathcal{R}(\theta_2) = k$, then we would have $\alpha[k].X'_1 \xrightarrow{\alpha[k]} \alpha.Y$, but this application of pre.\textbullet is not valid, as $\text{std}(X'_1)$ does not hold, since $X'_1$ was obtained from $X'$ after it made a *forward* transition. Hence, we obtain that $\text{key}(\theta_2) \neq k$ and we can carry out the rest of the proof as before. $\square$
*Example 3.* Re-using Example 1, since $|_R c[n'] \frown |_L \bar{b}[n]$ in

$$a[m].\bar{b}[n] \mid b + c \xrightarrow{|_R c[n']|} a[m].\bar{b}[n] \mid b + c[n'] \rightsquigarrow a[m].\bar{b} \mid b + c[n'],$$

Theorem 2 allows to re-arrange this trace as

$$a[m].\bar{b}[n] \mid b + c \rightsquigarrow a[m].\bar{b} \mid b + c \xrightarrow{|_R c[n']|} a[m].\bar{b} \mid b + c[n'],$$

Concurrency on coinital traces is defined using concurrency on composable traces and the loop lemma, immediate in CCSK.

**Lemma 3 (Loop lemma [48, Prop. 5.1]).** For all $t: X \xrightarrow{\theta} X'$, there exists a unique $t^\bullet: X' \rightsquigarrow X$, and reciprocally.

**Definition 12 (Coinital concurrency).** Let $t_1: X \xrightarrow{\theta_1} Y_1$ and $t_2: X \xrightarrow{\theta_2} Y_2$ be two coinital transitions, $\theta_1$ is concurrent with $\theta_2$ ($\theta_1 \prec \theta_2$) iff $\theta_1 \prec \theta_2$ in the trace $t_1^\bullet; t_2: Y_1 \xrightarrow{\theta_1} X \xrightarrow{\theta_2} Y_2$.

**Theorem 3 (Square property).** For all $t_1: X \xrightarrow{\theta_1} X_1$ and $t_2: X \xrightarrow{\theta_2} X_2$ with $\theta_1 \prec \theta_2$, there exist $t_1': X_1 \xrightarrow{\theta_2} Y$ and $t_2': X_2 \xrightarrow{\theta_1} Y$.

*Proof.* Since $t_1$ and $t_2$ are concurrent, by Definition 12 we have that $\theta_1 \prec \theta_2$ in $t_1^\bullet; t_2: X_1 \xrightarrow{\theta_1} X \xrightarrow{\theta_2} X_2$. Hence, depending on the direction of the arrows, and possibly using the loop lemma, we obtain by the forward or sideways diamond (Theorems 1 and 2) $t_1''; t_2'': X_1 \xrightarrow{\theta_2} Y \xrightarrow{\theta_1} X_2$, and we let $t_1' = t_1''$ and $t_2' = t_2''$:

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

□

*Example 4.* Following Example 1, we can get e.g. from $a[m].\bar{b}[n] \mid b + c \xrightarrow{|_R b[n']|} a[m].\bar{b}[n] \mid b[n'] + c$ and $a[m].\bar{b}[n] \mid b + c \rightsquigarrow a[m].\bar{b} \mid b + c$ the transitions converging to $a[m].\bar{b} \mid b[n'] + c$.

### 3.3 Sanity Checks: Causal Consistency, Optimality and More

Causality for a semantics of concurrent computations should satisfy a variety of critera, the squares and diamonds only being the starting point generally. Optimality with respect to the reduction semantics was discussed for the π-calculus [15, Theorem 5.6], and later refined along other criteria [16], for notions of concurrency defined respectively in terms of memory inclusion and rigid families. For reversible systems in particular, other criteria have emerged, along which causal consistency-arguably the most important-that guarantees that transitions cannot be undone unless their consequences have been too.
**Causal Consistency** Formally, causal consistency states that any two coinitial and cofinal traces are causally equivalent:

**Definition 13 (Causally equivalence).** Two traces $T_1, T_2$ are causally equivalent, if they are in the least equivalence relation closed by composition satisfying $t; t' \sim \epsilon$ and $t_1; t'_2 \sim t_2; t'_1$ for any $t_1; t'_2: X \xrightarrow{\theta_1} \theta_2 \xrightarrow{\theta_2} Y$, $t_2; t'_1: X \xrightarrow{\theta_2} \theta_1 \xrightarrow{\theta_1} Y$.

**Theorem 4 (Causal consistency).** All coinitial and cofinal traces are causally equivalent.

The “axiomatic approach” to reversible computation [39] allows to obtain causal consistency from other properties that are generally easier to prove.

**Lemma 4 (Backward transitions are concurrent).** Any two different coinitial backward transitions $t_1: X \xrightarrow{\theta_1} X_1$ and $t_2: X \xrightarrow{\theta_2} X_2$ are concurrent.

*Proof.* The proof is by induction on the size of $\theta_1$ and easier once noted that the backward LTS imposes $\mathcal{K}(\theta_1) \neq \mathcal{K}(\theta_2)$ for both transitions to be possible. □

**Lemma 5 (Well-foundedness).** For all $X$ there exists $n \in \mathbb{N}$, $X_0, \dots, X_n$ s.t. $X \rightsquigarrow X_n \rightsquigarrow \dots \rightsquigarrow X_1 \rightsquigarrow O_X$ and $\text{std}(O_X)$.

This lemma forbids infinite reverse computation, and is obvious in CCSK as any backward transition strictly decreases the number of occurrences of keys.

*Proof (of Theorem 4).* We can re-use the results of the axiomatic approach [39] since our forward LTS is the symmetric of our backward LTS, and as our concurrency relation (that the authors call the independence relation, following a common usage [52, Definition 3.7]) is indeed an irreflexive symmetric relation: symmetry is immediate by definition, irreflexivity follows from the fact that $\ll$ is reflexive. Then, by Theorem 3 and Lemma 4, the parabolic lemma holds [39, Proposition 3.4], and since the parabolic lemma and well-foundedness hold (Lemma 5), causal consistency holds as well [39, Proposition 3.5]. □

**Example 5.** Re-using the full trace presented in Example 1, we can re-organize the transitions using the diamonds so that every undone transition is undone immediately, and we obtain up to causal equivalence the trace

$$a.b | b + c \xrightarrow{|_L a[m]} a[m].b | b + c \xrightarrow{\langle |_L b[n], |_R b[n] \rangle} a[m].b[n] | b[n] + c$$

**Optimality and Other Criteria** An optimality criteria was defined in terms of adequation of the concurrency definitions for the LTS and for the reduction semantics [15, Theorem 5.6]. While this criteria requires a reduction semantics and a notion of reduction context to be formally proven, we believe it is easy to convince oneself that the gist of this property—the fact that non-$\tau$-transitions are concurrent iff there exists a “closing” context in which the resulting $\tau$-transitions
are still concurrent-holds in our system: as concurrency on $\tau$-transitions is defined in terms of concurrency of its elements (e.g., $\langle\theta_R^1, \theta_L^1\rangle \prec \langle\theta_R^2, \theta_L^2\rangle$ iff $\theta_d^1 \prec \theta_d^2$ for at least one $d \in \{L, R\}$), the optimality criteria is obtained “for free”.

Other properties [16, Section 6] have been investigated but would require a richer system to be truly meaningful: typically, “denotationality” requires for structural congruence to be preserved by the causal semantics, and hold vacuously in our structural-congruence-free system. However, properties such as the parabolic lemma [17, Lemma 10]–“any trace is equivalent to a backward trace followed by a forward trace”–or “RPI” [39, Definition 3.3]–“reversing preserves independence”, i.e. concurrency is insensible to directions–follow immediately.

# 4 Adding Infinite Behaviours to Reversible Systems

## 4.1 Initial Considerations: Which to Pick?

To endow CCSK with infinite behaviors, the obvious choices are recursion, replication or iteration. Carelessly adding the rules from $CCS_D$, $CCS_!$ or $CCS_*$ to CCSK would result in the rules presented in Fig. 4 that, if $X$ is not standard, would duplicate keys, voiding most of the propositions we have established so far.

<figure><img src="image_4.png" /><figcaption>**Fig. 4.** Adding infinite behaviors to CCSK</figcaption></figure>

For the replication and iteration operator, however, it is immediate to observe that $!X$ or $X^*$ are reachable if and only if $\text{std}(X)$: indeed, in iter. or the repl. rules, $X$ is unchanged, and hence can never reduce “under” the $!$ connector. Similarly, if constants are required to be standard, then no memory can be duplicated using recursion: if they are not, then chances are that the LTS would disallow using the const. rule twice with the same constant, as it would allow to duplicate its keys.

It seems that all three forms of infinite behavior have “built-in mechanisms” to disallow duplication of keys in CCSK, thus preventing the study of the replication of processes with a past. On the other hand, RCCS seems to be able to accommodate duplication of the memory, at least on the surface of it [7, Section 4.1].
Indeed, one could have a process P endowed with a memory m-written $m \triangleright P$-use a rule similar to repl.₁ to obtain e.g. $!(m \triangleright P) \rightarrow! (m \triangleright P) \mid m' \triangleright P'$: while this term would certainly be problematic and require mechanisms to not duplicate the memory events in m, or at least to disallow both threads from backtracking independently, RCCS's syntax certainly lends itself more naturally to express such behavior, that we reserve for future study.

Declensions of the const. rule, where X has to be standard, have been studied or mentioned for RCCS [17, 18, 33] and CCSK [27], but as far as we know, recursion and iterations have never been studied for distributed reversible systems. As recursion, iteration and replication constitute a strict expressiveness hierarchy w.r.t. e.g. weak bisimulation [13] in forward-only CCS, we believe studying all three of them to understand if the same distinction holds in the presence of reversibility is a worthwhile task. We propose to start this task by studying replication, as it is more commonly used when extending CCS with name-passing abilities, in a way more convenient [51, p. 12], and as it has already been discussed for RCCS in an unpublished draft [7, Section 4.1].

## 4.2 Adding Replication to CCSK ...

Adding replication to CCSK requires the following adjustments:

1. The replication operator ! is added to Definition 2,

2. In enhanced keyed labels (Definition 6), v can now range over $\{|_L, |_R, !\}^*$, and $\ell$ and $\mathcal{K}$ are extended straightforwardly,

3. The dependency relation (Definition 7) now include

$$ !\theta \leq !\theta \qquad !\theta \leq |_R \theta' \quad \text{if} \quad \left\{ \begin{array}{ll} \theta = \langle \theta_L, \theta_R \rangle \text{ and } \theta' = |_L \theta'' & \text{or} \quad (1) \\ \theta = \langle \theta_L, \theta_R \rangle \text{ and } \theta' = |_R \theta'' & \text{or} \quad (2) \end{array} \right. $$

$$ !\theta \leq |_L \theta' \qquad !\theta \leq |_R \theta' \quad \text{if} \quad \left\{ \begin{array}{ll} \theta = \langle \theta_L, \theta_R \rangle \text{ and } \theta' = |_L \theta'' & \text{or} \quad (1) \\ \theta = \langle \theta_L, \theta_R \rangle \text{ and } \theta' = |_R \theta'' & \text{or} \quad (2) \\ \theta \leq \theta' & \text{otherwise,} \quad (3) \end{array} \right. $$

which immediately implies $!\theta \leq \langle |_L \theta_L, |_R \theta_R \rangle$, as $\theta \leq \langle \theta_L, \theta_R \rangle$ if $\exists d. \theta \leq \theta_d$, but since $!\theta \leq |_L \theta_L$ this is always the case.

4. The forward and backward proved LTS (Fig. 3) now have the rules

$$ \frac{X \xrightarrow{\theta} X'}{!X \xrightarrow{!\theta} !X \mid X'} \text{ repl.}_1 \qquad \frac{X \xrightarrow{\theta_L \lambda[k]} X' \quad X \xrightarrow{\theta_R \bar{\lambda}[k]} X''}{!X \xrightarrow{!\langle |_L \theta_L[k], |_R \theta_R[k] \rangle} !X \mid (X' \mid X'')} \text{ repl.}_2 $$

and their reverses. Note that !X is reachable only if std(X).

**Remark 2 (On structural congruence, and the lack thereof).** The equations (1) and (2) of the dependency relation comes from the absence of structural congruence: indeed, assuming e.g. $X \xrightarrow{\theta_L} X_1 \xrightarrow{\theta'_L} X'_1$ with $\theta_L \prec \theta'_L$ and $X \xrightarrow{\theta_R} X_2$, we cannot let $!\langle |_L \theta_L, |_R \theta_R \rangle$ and $|_R|_L \theta'_L$ be concurrent in

$$ !X \xrightarrow{!\langle |_L \theta_L, |_R \theta_R \rangle} !X \mid (X_1 \mid X_2) \xrightarrow{|_R|_L \theta'_L} !X \mid (X'_1 \mid X_2), $$
as we cannot re-organize this trace. Indeed, while an extended version of the
forward diamond lemma could allow us to obtain an $X_1''$ and something like

$$ !X \xrightarrow{!\theta_L'} !X | X_1'' \xrightarrow{\langle |_R!\theta_R, |_L\theta_L \rangle} (!X | X_2) | X_1', $$

we can not make the target processes equal without a structural congruence
making the parallel composition associative and commutative.

The “usual” structural congruence is missing from all the proved transition
systems [14, 20, 22, 23], or missing the associativity and commutativity of the
parallel composition [21, p. 242]. While adding such a congruence would benefits
the expressiveness, making it interact nicely with the derived proof system and
the reversible features [38, Section 4; 6] is a challenge we prefer to postpone.

Notions such as transition, trace, reachability and concurrency remain defined
the same way, and Lemma 1 still holds, as it is not impacted by our changes.

*Example 6.* Consider the transition $X_1 = a.\bar{a} + \bar{a} \xrightarrow{a[m]} a[m].\bar{a} + \bar{a} = X_2$, while we can obtain the derivation $\pi_0$ below, it should be noted that $!X_2$ is not reach-able and thus can be discarded. Indeed, as both repl. rules leave the term $X$ unchanged, there is no transition that allows to reduce “under” the ! connective.

$$ \pi_0 = \frac{X_2 \xrightarrow{\bar{a}[n]} a[m].\bar{a}[n] + \bar{a}}{!X_2 \xrightarrow{!\bar{a}[n]} !X_2 | a[m].\bar{a}[n] + \bar{a}} \text{ repl.}_1 $$

However, $!X_1$ have two different $\tau$-transitions, corresponding respectively to $!X_1$ synchronizing with its “future self” $(\pi_1)$ or with itself $(\pi_2)$.

$$ \pi_1 = \frac{X_1 \xrightarrow{a[n]} a[n].\bar{a} + \bar{a}}{!X_1 \xrightarrow{!a[n]} !X_1 | a[n].\bar{a} + \bar{a}} \text{ repl.}_1 \\ \qquad \frac{X_2 \xrightarrow{\bar{a}[n]} a[m].\bar{a}[n] + \bar{a}}{!X_1 | X_2 \xrightarrow{\langle |_L!a[n], |_R\bar{a}[n] \rangle} !X_1 | (a[n].\bar{a} + \bar{a} | a[m].\bar{a}[n] + \bar{a})} \text{ syn.} $$

$$ \pi_2 = \frac{X_1 \xrightarrow{a[m]} X_2 \quad X_1 \xrightarrow{\bar{a}[m]} a.\bar{a} + \bar{a}[m]}{!X_1 \xrightarrow{!\langle |_L a[m], |_R \bar{a}[m] \rangle} !X_1 | (X_2 | a.\bar{a} + \bar{a}[m])} \text{ repl.}_2 $$

## 4.3 ... While Preserving Diamonds and Squares ...

We now revisit Sect. 3.2's results and prove they carry over this extended calculus, up to a collapsing function $\sigma$ that identifies ! and $|_R$ prefixes on labels: while those labels behave differently w.r.t. the dependency relation, they should be identified when re-organizing traces in e.g. the extended forward diamond (Theorem 5).

**Definition 14 (Collapsing function).** We define, for $d \in \{\text{L}, \text{R}\}$:

$$ \sigma(\alpha[k]) = \alpha[k] $$

$$ \sigma(|_d \upsilon) = |_d \sigma(\upsilon) $$

$$ \sigma(!\upsilon) = |_R \sigma(\upsilon) $$

$$ \sigma(\langle \theta_L, \theta_R \rangle) = \langle \sigma(\theta_L), \sigma(\theta_R) \rangle $$
**Theorem 5 (Forward diamond (extd)).** For all $X \xrightarrow{\theta_1} X_1 \xrightarrow{\theta_2} Y$ with $\theta_1 \prec \theta_2$, there exists $X_2$ s.t. $X \xrightarrow{\hat{\theta}_2} X_2 \xrightarrow{\hat{\theta}_1} Y$, and $\sigma(\hat{\theta}_i) = \sigma(\theta'_i)$ for $i \in \{1, 2\}$.

*Proof.* We can re-use the proof for Theorem 1 immediately, since $\sigma(\theta) = \theta$ in all the cases we had, and since $\theta_2$ cannot be of the form $!\theta$ in the cases where we have to decompose it. But we now need to consider the case where repl.₁ or repl.₂ is the last rule of $\theta_1$'s derivation. Those cases offer little resistance, but echoes back to Remark 2 to impose some dependencies between transitions that would require structural congruence to be able to re-order the resulting processes. □

**Theorem 6 (Sideways diamond (extd)).** For all $X \xrightarrow{\theta_1} X_1 \rightsquigarrow Y$ with $\theta_1 \prec \theta_2$, there exists $X_2$ s.t. $X \rightsquigarrow Y \xrightarrow{\theta_2} X_2 \xrightarrow{\theta_1} Y$, and $\sigma(\theta_i) = \sigma(\theta'_i)$ for $i \in \{1, 2\}$.

*Proof.* As for the (non-extended) sideways diamond (Theorem 2), we can reuse the proof of the extended forward diamond almost as it is. An important case is if $X$ is of the form $!X'$, then $!X' \xrightarrow{!\theta'_1} !X' | X'_1$ and std($X'$), so the only transition $X'_1$ can backtrack on is $\theta'_1$. But $\theta_2 = !\theta'_1$ or $|_R \theta'_1$ contradicts $\theta_1 \prec \theta_2$, hence there are no backward transition following $!\theta'_1$ not concurrent with it. □

Finally, the loop lemma (Lemma 3) and hence the square property (Theorem 3)– under $\sigma$-image–are straightforward in our extended calculus, thanks to the same argument as in the non-extended case.

## 4.4 ... as Well as Causal Consistency

Causal consistency (Theorem 4) follows from the square property–established previously–, well-foundedness–which still holds, as ! introduces infinite *forward* behaviors but let the number of keys decreases strictly when *backtracking*–, but also that backward transitions are concurrent, a property we are missing in our extended calculus. Indeed, consider e.g. the reachable process $X =!a.P \mid a[m].P$, we have $X \rightsquigarrow !a.P$ and $X \rightsquigarrow |_R a[m] \rightsquigarrow !a.P \mid a.P$, and since $!a[m] \le |_R a[m]$, those two different traces are *not* concurrent–this dependency was actually useful in proving Theorem 6. There are two ways of restoring this needed property:

1. One could argue that, since $\sigma(!a[m]) = |_R a[m]$, those two transitions are the same up to the structural congruence $!P \mid P \equiv!P$ [13, Definition 12],

2. One could “mark” the key $m$ so that it cannot backtrack independently, thus forbidding the $|_R a[m]$-transition.

We implement here the second solution, but would like the reader to appreciate that in all the development we carried so far, processes that can perform two conflicting backward transitions were not an issue. We believe this leeway could enable other formalisms or solutions to restore causal consistency. Implementing this “marking” of keys resulting from a replication requires some adjustments:

1. A key can now be either *unmarked* $\{m, n, \dots\}$ or *marked* $\{m', n', \dots\}$

2. The forward and backward proved LTS (Fig. 3) now have the rules
$$ \frac{X \xrightarrow{\theta} X'}{!X \xrightarrow{!\theta} !X \mid m(X')} \text{repl.}_1 \qquad \frac{X \xrightarrow{\theta_L \lambda[k]} X' \qquad X \xrightarrow{\theta_R \bar{\lambda}[k]} X''}{!X \xrightarrow{!\{\mid_L \theta_L \lambda[k]\}, \mid_R \theta_R \bar{\lambda}[k]\}} !X \mid m(X' \mid X'')} \text{repl.}_2 $$

and their inverses, for $m(\alpha[m].P) = \alpha[m^1].P$, $m(0) = 0$ and $m(X)$ being simply $m$ applied to the sub-term(s) of $X$ recursively.

3. Transitions $X \xrightarrow{\theta} X'$ are admissible only if $\kappa(\theta)$ is un-marked in $X'$, and we reason only on admissible transitions in our lemmas and theorems.

This forbids “just enough” to restore concurrency between all coinitial backward transitions, without altering anything else. As a consequence, we can use again the axiomatic approach [39, Proposition 3.5] to obtain causal consistency (up to $\sigma$-image) for our extended system. A possible drawback is that this solution comes at the price of compositionality: it is possible that e.g. $a[m^1].X$ does not have an admissible backward reduction, but $!(a.X) \mid a[m^1].X$ does. There seems to be no way of avoiding this “global” dimension of backtracking on replication.

# 5 Conclusion and Perspectives

Our two mains contributions are intertwined: infinite behaviors are a good test for concurrency definitions, which in turns should preserve the independence of !-transitions w.r.t. other transitions. In this sense, finding definitions for concurrency and the replication operator that are suited for reversible systems was challenging, but we believe this work offers a solid, motivated answer to both questions. By adapting a forward-only definition of concurrency, extending it to backward transitions “for free” and proving that expected properties such as the diamonds and squares hold, we provided an ingenious solution to a problem that have been left up in the air for too long. Natural follow-ups include proving that this definition coincide with semantics-inspired [27] and other syntactical [8, Definition 20] representations of concurrency for other reversible systems.

Infinite behaviors in the presence of reversibility is not well-understood nor studied. Even if reversible primitive functions allowed a first exploration of the interplay of both notions [47], to our knowledge no systematic study of how replication can or cannot preserve e.g. causal consistency had been led until this work. Some attempts to extend algebras of communicating processes [11], including recursion, seems to have been unsuccessful [55]. An interesting follow-up would be to define recursion and iteration as well in CCSK, and to attempt to reconstruct the separation results from the forward-only paradigm [46]: whether finer, “reversible”, equivalences can preserve this distinction despite the greater flexibility provided by backward transitions is an open problem. Another interesting point is the study of infinite behaviors that duplicate past events, including their keys or memories: whether this formalism could preserve causal consistency, or what benefits there would be in tinkering this property, is also an open question.

Last but not least, both investigations would require to define relevant properties. In the forward world, termination or convergence were used to compare
infinite behavior [46], and additional criteria were introduced to study causal semantics [16]. Those properties may or may not be suited for reversible systems, but it is difficult to decide as they sometimes even lack a definition. This could help in solving the more general question of deciding *what* it is that we want to observe and assess when evaluating reversible, concurrent systems [9].
References

1. Abadi, M., Blanchet, B., Fournet, C.: The applied pi calculus: Mobile values, new names, and secure communication. J. ACM 65(1), 1:1–1:41 (2018). https://doi.org/10.1145/3127586

2. Arpit, Kumar, D.: Calculus of concurrent probabilistic reversible processes. In: ICCCT-2017: Proceedings of the 7th International Conference on Computer and Communication Technology. p. 34–40. ICCCT-2017, ACM, New York, NY, USA (2017). https://doi.org/10.1145/3154979.3155004

3. Aubert, C., Cristescu, I.: Reversible barbed congruence on configuration structures. In: Knight, S., Lluch Lafuente, A., Lanese, I., Vieira, H.T. (eds.) ICE 2015. EPTCS, vol. 189, pp. 68–95 (2015). https://doi.org/10.4204/EPTCS.189.7

4. Aubert, C., Cristescu, I.: Contextual equivalences in configuration structures and reversibility. J. Log. Algebr. Methods Program. 86(1), 77–106 (2017). https://doi.org/10.1016/j.jlamp.2016.08.004

5. Aubert, C., Cristescu, I.: How reversibility can solve traditional questions: The example of hereditary history-preserving bisimulation. In: Konnov, I., Kovács, L. (eds.) 31st International Conference on Concurrency Theory, CONCUR 2020, September 1–4, 2020, Vienna, Austria. LIPIcs, vol. 2017, pp. 13:1–13:24. Schloss Dagstuhl (2020). https://doi.org/10.4230/LIPIcs.CONCUR.2020.13

6. Aubert, C., Cristescu, I.: Structural equivalences for reversible calculi of communicating systems (oral communication). Research report, Augusta University (2020), https://hal.archives-ouvertes.fr/hal-02571597, communication at ICE 2020

7. Aubert, C., Medić, D.: Enabling Replications and Contexts in Reversible Concurrent Calculus (May 2021), https://hal.archives-ouvertes.fr/hal-03183053, research report

8. Aubert, C., Medić, D.: Explicit identifiers and contexts in reversible concurrent calculus. In: Yamashita, S., Yokoyama, T. (eds.) Reversible Computation - 13th International Conference, RC 2021, Virtual Event, July 7-8, 2021, Proceedings. LNCS, vol. 12805, pp. 144–162. Springer (2021). https://doi.org/10.1007/978-3-030-79837-6_9

9. Aubert, C., Varacca, D.: Processes, systems & tests: Defining contextual equivalences. In: Lange, J., Mavridou, A., Safina, L., Scalas, A. (eds.) Proceedings 14th Interaction and Concurrency Experience, Online, 18th June 2021. EPTCS, vol. 347, pp. 1–21. Open Publishing Association (2021). https://doi.org/10.4204/EPTCS.347.1

10. Axelsen, H.B.: Reversible multi-head finite automata characterize reversible logarithmic space. In: Dediu, A.H., Martín-Vide, C. (eds.) Language and Automata Theory and Applications - 6th International Conference, LATA 2012, A Coruña, Spain, March 5-9, 2012. Proceedings. LNCS, vol. 7183, pp. 95–105. Springer (2012). https://doi.org/10.1007/978-3-642-28332-1_9

11. Baeten, J.C.M.: A brief history of process algebra. Theor. Comput. Sci. 335(2-3), 131–146 (2005). https://doi.org/10.1016/j.tcs.2004.07.036

12. Busi, N., Gabbrielli, M., Zavattaro, G.: Replication vs. recursive definitions in channel based calculi. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings. LNCS, vol. 2719, pp. 133–144. Springer (2003). https://doi.org/10.1007/3-540-45061-0_12
13. Busi, N., Gabbrielli, M., Zavattaro, G.: On the expressive power of recursion, replication and iteration in process calculi. MSCS 19(6), 1191-1222 (2009).
https://doi.org/10.1017/S096012950999017X

14. Carabetta, G., Degano, P., Gadducci, F.: CCS semantics via proved transition systems and rewriting logic. In: Kirchner, C., Kirchner, H. (eds.) 1998 International Workshop on Rewriting Logic and its Applications, WRLA 1998, Abbaye des Prémontrés at Pont-à-Mousson, France, September 1998. Electron. Notes Theor. Comput. Sci., vol. 15, pp. 369-387. Elsevier (1998).
https://doi.org/10.1016/S1571-0661(05)80023-4,
https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/15/suppl

15. Cristescu, I., Krivine, J., Varacca, D.: A compositional semantics for the reversible p-calculus. In: LICS. pp. 388-397. IEEE Computer Society (2013).
https://doi.org/10.1109/LICS.2013.45

16. Cristescu, I., Krivine, J., Varacca, D.: Rigid families for CCS and the π-calculus. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings. LNCS, vol. 9399, pp. 223-240. Springer (2015).
https://doi.org/10.1007/978-3-319-25150-9_14

17. Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings. LNCS, vol. 3170, pp. 292-307. Springer (2004).
https://doi.org/10.1007/978-3-540-28644-8_19

18. Danos, V., Krivine, J.: Transactions in RCCS. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings. LNCS, vol. 3653, pp. 398-412. Springer (2005).
https://doi.org/10.1007/11539452_31

19. Degano, P., Gadducci, F., Priami, C.: Causality and replication in concurrent processes. In: Broy, M., Zamulin, A.V. (eds.) Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia, July 9-12, 2003, Revised Papers. LNCS, vol. 2890, pp. 307-318. Springer (2003).
https://doi.org/10.1007/978-3-540-39866-0_30

20. Degano, P., Priami, C.: Proved trees. In: Kuich, W. (ed.) Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings. LNCS, vol. 623, pp. 629-640. Springer (1992).
https://doi.org/10.1007/3-540-55719-9_110

21. Degano, P., Priami, C.: Non-interleaving semantics for mobile processes. Theor. Comput. Sci. 216(1-2), 237-270 (1999).
https://doi.org/10.1016/S0304-3975(99)80003-6

22. Degano, P., Priami, C.: Enhanced operational semantics. ACM Comput. Surv. 33(2), 135-176 (2001).
https://doi.org/10.1145/384192.384194

23. Demangeon, R., Yoshida, N.: Causal computational complexity of distributed processes. In: Dawar, A., Grädel, E. (eds.) LICS. pp. 344-353. ACM (2018).
https://doi.org/10.1145/3209108.3209122

24. Engelfriet, J., Gelsema, T.: Multisets and structural congruence of the pi-calculus with replication. Theor. Comput. Sci. 211(1-2), 311-337 (1999).
https://doi.org/10.1016/S0304-3975(97)00179-5

25. Frank, M.P., Brocato, R.W., Tierney, B.D., Missert, N.A., Hsia, A.H.: Reversible computing with fast, fully static, fully adiabatic CMOS. In: International Conference on Rebooting Computing, ICRC 2020, Atlanta, GA, USA, December 1-3, 2020. pp. 1-8. IEEE (2020).
https://doi.org/10.1109/ICRC2020.2020.00014
26. Giambiagi, P., Schneider, G., Valencia, F.D.: On the expressiveness of infinite behavior and name scoping in process calculi. In: Walukiewicz, I. (ed.) Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. LNCS, vol. 2987, pp. 226-240. Springer (2004). https://doi.org/10.1007/978-3-540-24727-2_17

27. Graversen, E., Phillips, I.C.C., Yoshida, N.: Event structure semantics of (controlled) reversible CCS. J. Log. Algebr. Methods Program. **121**, 100686 (2021). https://doi.org/10.1016/j.jlamp.2021.100686

28. Hennessy, M.: A distributed Pi-calculus. CUP (2007). https://doi.org/10.1017/CBO9780511611063

29. Holzer, M., Kutrib, M.: Reversible nondeterministic finite automata. In: Phillips, I., Rahaman, H. (eds.) Reversible Computation - 9th International Conference, RC 2017, Kolkata, India, July 6-7, 2017, Proceedings. LNCS, vol. 10301, pp. 35-51. Springer (2017). https://doi.org/10.1007/978-3-319-59936-6_3

30. Hong, J., Lambson, B., Dhuey, S., Bokor, J.: Experimental test of Landauer's principle in single-bit operations on nanomagnetic memory bits. Science Advances **2**(3), e1501492 (2016). https://doi.org/10.1126/sciadv.1501492

31. Jun, Y., Gavrilov, M., Bechhoefer, J.: High-precision test of Landauer's principle in a feedback trap. Phys. Rev. Lett. **113**, 190601 (Nov 2014). https://doi.org/10.1103/PhysRevLett.113.190601

32. Kaarsgaard, R., Axelsen, H.B., Glück, R.: Join inverse categories and reversible recursion. J. Log. Algebr. Methods Program. **87**, 33-50 (2017). https://doi.org/10.1016/j.jlamp.2016.08.003

33. Krivine, J.: Algèbres de Processus Réversible - Programmation Concurrente Déclarative. Ph.D. thesis, Université Paris 6 & INRIA Rocquencourt (2006), https://tel.archives-ouvertes.fr/tel-00519528

34. Lanese, I.: From reversible semantics to reversible debugging. In: Kari, J., Ulidowski, I. (eds.) Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14, 2018, Proceedings. LNCS, vol. 11106, pp. 34-46. Springer (2018). https://doi.org/10.1007/978-3-319-99498-7_2

35. Lanese, I., Lienhardt, M., Mezzina, C.A., Schmitt, A., Stefani, J.: Concurrent flexible reversibility. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. LNCS, vol. 7792, pp. 370-390. Springer (2013). https://doi.org/10.1007/978-3-642-37036-6_21

36. Lanese, I., Medić, D., Mezzina, C.A.: Static versus dynamic reversibility in CCS. Acta Inform. (Nov 2019). https://doi.org/10.1007/s00236-019-00346-6

37. Lanese, I., Mezzina, C.A., Stefani, J.: Reversibility in the higher-order π-calculus. Theor. Comput. Sci. **625**, 25-84 (2016). https://doi.org/10.1016/j.tcs.2016.02.019

38. Lanese, I., Phillips, I.: Forward-reverse observational equivalences in CCSK. In: Yamashita, S., Yokoyama, T. (eds.) Reversible Computation - 13th International Conference, RC 2021, Virtual Event, July 7-8, 2021, Proceedings. LNCS, vol. 12805, pp. 126-143. Springer (2021). https://doi.org/10.1007/978-3-030-79837-6_8

39. Lanese, I., Phillips, I.C.C., Ulidowski, I.: An axiomatic approach to reversible computation. In: Goubault-Larrecq, J., König, B. (eds.) Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, https://doi.org/10.1007/978-3-642-37036-6_21
Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. LNCS, vol. 12077, pp. 442-461. Springer (2020). https://doi.org/10.1007/978-3-030-45231-5_23

40. Lange, K.J., McKenzie, P., Tapp, A.: Reversible space equals deterministic space. J. Comput. Syst. Sci. 60(2), 354-367 (2000). https://doi.org/10.1006/jcss.1999.1672

41. Medić, D., Mezzina, C.A., Phillips, I., Yoshida, N.: A parametric framework for reversible π-calculi. Inf. Comput. 275, 104644 (2020). https://doi.org/10.1016/j.ic.2020.104644

42. Merro, M., Zappa Nardelli, F.: Behavioral theory for mobile ambients. J. ACM 52(6), 961-1023 (2005). https://doi.org/10.1145/1101821.1101825

43. Mezzina, C.A., Koutavas, V.: A safety and liveness theory for total reversibility. In: Mallet, F., Zhang, M., Madelaine, E. (eds.) 11th International Symposium on Theoretical Aspects of Software Engineering, TASE 2017, Sophia Antipolis, France, September 13-15. pp. 1-8. IEEE (2017). https://doi.org/10.1109/TASE.2017.8285635, https://ieeexplore.ieee.org/xpl/conhome/8277122/proceeding

44. Milner, R.: A Calculus of Communicating Systems. LNCS, Springer-Verlag (1980). https://doi.org/10.1007/3-540-10235-3

45. Reversibility: Future of Life on Earth | The NSF 2026 Idea Machine (Oct 2018), https://nsf2026imgallery.skild.com/entries/reversibility-future-of-life-on-earth

46. Palamidessi, C., Valencia, F.D.: Recursion vs replication in process calculi: Expressiveness. Bull. EATCS 87, 105-125 (2005), http://eatcs.org/images/bulletin/beatcs87.pdf

47. Paolini, L., Piccolo, M., Roversi, L.: On a class of reversible primitive recursive functions and its turing-complete extensions. New Generation Comput. 36(3), 233-256 (2018). https://doi.org/10.1007/s00354-018-0039-1

48. Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. In: Aceto, L., Ingólfsdóttir, A. (eds.) Foundations of Software Science and Computation Structures, 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006, Proceedings. LNCS, vol. 3921, pp. 246-260. Springer (2006). https://doi.org/10.1007/11690634_17

49. Phillips, I., Ulidowski, I.: Reversibility and models for concurrency. Electron. Notes Theor. Comput. Sci. 192(1), 93-108 (2007). https://doi.org/10.1016/j.entcs.2007.08.018

50. Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. J. Log. Algebr. Program. 73(1-2), 70-96 (2007). https://doi.org/10.1016/j.jlap.2006.11.002

51. Sangiorgi, D., Walker, D.: The Pi-calculus. CUP (2001)

52. Sassone, V., Nielsen, M., Winskel, G.: Models for concurrency: Towards a classification. Theor. Comput. Sci. 170(1-2), 297-348 (1996). https://doi.org/10.1016/S0304-3975(96)80710-9

53. Ulidowski, I., Phillips, I., Yuen, S.: Concurrency and reversibility. In: Yamashita, S., Minato, S. (eds.) Reversible Computation - 6th International Conference, RC 2014, Kyoto, Japan, July 10-11, 2014. Proceedings. LNCS, vol. 8507, pp. 1-14. Springer (2014). https://doi.org/10.1007/978-3-319-08494-7_1

54. Visan, A.M., Arya, K., Cooperman, G., Denniston, T.: URDB: a universal reversible debugger based on decomposing debugging histories. In: Proceedings of the 6th Workshop on Programming Languages and Operating Systems, PLOS@SOSP 2011, Cascais, Portugal, October 23, 2011. pp. 8:1-8:5. ACM (2011). https://doi.org/10.1145/2039239.2039251
55. Wang, Y.: Retracted article: An algebra of reversible computation. SpringerPlus 5(1), 1659 (Sep 2016). https://doi.org/10.1186/s40064-016-3229-7

A Omitted Proofs

**Lemma 1 (Decomposing concurrent transitions).** Let $i \in \{1,2\}$ and $\theta_i \in \{|_L \theta'_i, |_R \theta''_i, \langle |_L \theta'_i, |_R \theta''_i \rangle\}$, and define $\pi_L(X_L | X_R) = X_L$, $\pi_L(|_L \theta) = \theta$, $\pi_L(\langle |_L \theta_L, |_R \theta_R \rangle) = \theta_L$, $\pi_L(|_R \theta) = \text{undefined}$, and define similarly $\pi_R$.

Whenever $T: X_L \mid X_R \xrightarrow{\theta_1} Y_L \mid Y_R \xrightarrow{\theta_2} Z_L \mid Z_R$ with $\theta_1 \prec_T \theta_2$, then for $d \in \{L,R\}$, if $\pi_d(\theta_1)$ and $\pi_d(\theta_2)$ are both defined, then, $\pi_d(\theta_1) \prec \pi_d(T)$, $\pi_d(\theta_2)$ with $\pi_d(T): \pi_d(X_L \mid X_R) \xrightarrow{\pi_d(\theta_1)} \pi_d(Y_L \mid Y_R) \xrightarrow{\pi_d(\theta_2)} \pi_d(Z_L \mid Z_R)$.

*Proof.* The trace $\pi_d(T)$ exists by virtue of the rule $|_d$, syn. or their reverses. What remains to prove is that $\pi_d(\theta_1) \prec \pi_d(T)$, $\pi_d(\theta_2)$ holds.

The proof is by case on $\theta_1$ and $\theta_2$, but always follows the same pattern. As we know that both $\pi_d(\theta_1)$ and $\pi_d(\theta_2)$ need to be defined, there are 7 cases:

$$ \frac{\theta_1 \parallel_{|_L \theta'_1} |_L \theta'_1 \parallel_{|_R \theta'_1} |_R \theta'_1 \parallel_{|_L \theta'_1, |_R \theta''_1} \langle |_L \theta'_1, |_R \theta''_1 \rangle \parallel_{|_L \theta'_1, |_R \theta''_1} \langle |_L \theta'_1, |_R \theta''_1 \rangle \parallel_{|_L \theta'_1, |_R \theta''_1} \langle |_L \theta'_1, |_R \theta''_1 \rangle}{\theta_2 \parallel_{|_L \theta'_2} \langle |_L \theta'_2, |_R \theta''_2 \rangle \parallel_{|_R \theta'_2} \langle |_L \theta'_2, |_R \theta''_2 \rangle \parallel_{|_L \theta'_2, |_R \theta''_2} \langle |_L \theta'_2, |_R \theta''_2 \rangle} $$

By symmetry, we can bring this number down to three:

$$ \begin{array}{c|c|c} \text{(case letter)} & \text{a)} & \text{b)} \\ \hline \theta_1 & |_L \theta'_1 & \langle |_L \theta'_1, |_R \theta''_1 \rangle \\ \hline \theta_2 & |_L \theta'_2 & |_L \theta'_2 \\ \hline \end{array} \quad \begin{array}{c|c|c} \text{c)} & & \\ \hline \langle |_L \theta'_1, |_R \theta''_1 \rangle & & \\ \hline \langle |_L \theta'_2, |_R \theta''_2 \rangle & & \\ \hline \end{array} $$

In each case, assume $\pi_L(\theta_1) = \theta'_1 \prec \pi_L(T)$, $\theta'_2 = \pi_L(\theta_2)$ does not hold. Then it must be the case that either $\theta'_1 \prec \pi_L(T)$, $\theta'_2$ or $\theta'_2 \prec \pi_L(T)$, $\theta'_1$, and the two can be treated the same way, thanks to symmetry, and we detail this case for each of our three cases:

a) If $\theta'_1 \prec \pi_L(T)$, then $\theta'_1 \prec \theta'_2$, and it is immediate that $\theta_1 = |_L \theta'_1 \prec_T |_L \theta'_2 = \theta_2$, contradicting $\theta_1 \prec_T \theta_2$.

b) If $\theta'_1 \prec \pi_L(T)$, then $\theta'_1 \prec \theta'_2$, $|_L \theta'_1 \prec |_L \theta'_2$ and $\langle |_L \theta'_1, |_R \theta''_1 \rangle \prec |_L \theta'_2$, from which we can deduce $\theta_1 \prec_T \theta_2$, contradicting $\theta_1 \prec_T \theta_2$.

c) If $\theta'_1 \prec \pi_L(T)$, then $\theta'_1 \prec \theta'_2$, $|_L \theta'_1 \prec |_L \theta'_2$ and $\langle |_L \theta'_1, |_R \theta''_1 \rangle \prec \langle |_L \theta'_2, |_R \theta''_2 \rangle$, from which we can deduce $\theta_1 \prec_T \theta_2$, contradicting $\theta_1 \prec_T \theta_2$.

Hence, in all cases, assuming that $\pi_d(\theta_1) \prec \pi_d(T)$, $\pi_d(\theta_2)$ does not hold leads to a contradiction. $\square$

**Theorem 1 (Forward diamond).** For all $X \xrightarrow{\theta_1} X_1 \xrightarrow{\theta_2} Y$ with $\theta_1 \prec \theta_2$, there exists $X_2$ s.t. $X \xrightarrow{\theta_2} X_2 \xrightarrow{\theta_1} Y$.

*Proof.* The proof proceeds by induction on the length of the deduction for the derivation for $X \xrightarrow{\theta_1} X_1$.
**Length 1** In this case, the derivation is a single application of act., and $\theta_1$ is of the form $\alpha[k]$. But $\alpha[k] \not\sim \theta_2$ cannot hold, as $\alpha[k] \ll \theta_2$ always holds, and this case is vacuously true.

**Length > 1** We proceed by case on the last rule.

**pre.** There exists $\alpha, k, X'$ and $X'_1$ s.t. $X = \alpha[k].X' \xrightarrow{\theta_1} \alpha[k].X'_1 = X_1$ and that $\mathfrak{k}(\theta_1) \neq k$. As $\alpha[k].X'_1 \xrightarrow{\theta_2} Y$ we know that $\mathfrak{k}(\theta_2) \neq k$ [38, Lemma 3.4], and we can apply Lemma 2 twice to obtain

$$ \mathrm{rm}_k^\alpha(\alpha[k].X') = X' \xrightarrow{\theta_1} \mathrm{rm}_k^\alpha(\alpha[k].X'_1) = X'_1 \xrightarrow{\theta_2} \mathrm{rm}_k^\alpha(Y) $$

As $\theta_1 \not\sim \theta_2$ by hypothesis, we can use the induction hypothesis to obtain that there exists $X_2$ s.t. $X' \xrightarrow{\theta_2} X_2 \xrightarrow{\theta_1} \mathrm{rm}_k^\alpha(Y)$. Since $\mathfrak{k}(\theta_2) \neq k$, we can append pre. to the derivation of $X' \xrightarrow{\theta_2} X_2$ to obtain $\alpha[k].X' = X \xrightarrow{\theta_2} \alpha[k].X_2$. Using Lemma 2 one last time, we obtain that $\mathrm{rm}_k^\alpha(\alpha[k].X_2) = X_2 \xrightarrow{\theta_1} \mathrm{rm}_k^\alpha(Y)$ implies $\alpha[k].X_2 \xrightarrow{\theta_1} Y$, which concludes this case.

**res.** This is immediate by induction hypothesis.

$|_L$ There exists $X_L, X_R, \theta, X_{1_L}$, and $Y_L, Y_R$ s.t. $X \xrightarrow{\theta_1} X_1 \xrightarrow{\theta_2} Y$ is

$$ X_L | X_R \xrightarrow{|_L \theta} X_{1_L} | X_R \xrightarrow{\theta_2} Y_L | Y_R. $$

Then, $X_L \xrightarrow{\theta} X_{1_L}$ and the proof proceeds by case on $\theta_2$:

$\theta_2$ is $|_R \theta'$ Then $X_R \xrightarrow{\theta'} Y_R, X_{1_L} = Y_L$ and the occurrences of the rules $|_L$ and $|_R$ can be “swapped” to obtain

$$ X_L | X_R \xrightarrow{|_R \theta'} X_L | Y_R \xrightarrow{|_L \theta} Y_L | Y_R. $$

$\theta_2$ is $|_L \theta'$ Then, $X_L \xrightarrow{\theta} X_{1_L} \xrightarrow{\theta'} Y_L$ and $X_R = Y_R$. As $|_L \theta = \theta_1 \not\sim \theta_2 = |_L \theta'$, it is the case that $\theta \not\sim \theta'$ in $X_L \xrightarrow{\theta} X_{1_L} \xrightarrow{\theta'} Y_L$ by Lemma 1, and we can use induction to obtain $X_2$ s.t. $X_L \xrightarrow{\theta'} X_2 \xrightarrow{\theta} Y_L$, from which it is immediate to obtain $X_L | X_R \xrightarrow{|_L \theta'} X_2 | X_R \xrightarrow{|_L \theta} Y_L | X_R = Y_L | Y_R$

$\theta_2$ is $\langle|_L \theta_L, |_R \theta_R\rangle$ Since $|_L \theta = \theta_1 \not\sim \theta_2 = \langle|_L \theta_L, |_R \theta_R\rangle$, we have that $\theta \not\sim \theta_L$ in $X_L \xrightarrow{\theta} X_{1_L} \xrightarrow{\theta_L} Y_L$ by Lemma 1. Hence, we can use induction to obtain $X_L \xrightarrow{\theta_L} X_2 \xrightarrow{\theta} Y_L$. Since we also have that $X_R \xrightarrow{\theta_R} Y_R$, we can compose both traces using first syn., then $|_L$ to obtain

$$ X_L | X_R \xrightarrow{\langle|_L \theta_L, |_R \theta_R\rangle} X_2 | Y_R \xrightarrow{|_L \theta} Y_L | Y_R. $$

$|_R$ This is symmetric to $|_L$.

**syn.** There exists $X_L, X_R, \theta_L, \theta_R, X_{1_L}, X_{1_R}, Y_L$ and $Y_R$ s.t. $X \xrightarrow{\theta_1} X_1 \xrightarrow{\theta_2} Y$ is

$$ X_L | X_R \xrightarrow{\langle|_L \theta_L, |_R \theta_R\rangle} X_{1_L} | X_{1_R} \xrightarrow{\theta_2} Y_L | Y_R. $$

Then, $X_L \xrightarrow{\theta_L} X_{1_L}, X_R \xrightarrow{\theta_R} X_{1_R}$ and the proof proceeds by case on $\theta_2$:
$\theta_2$ is $|_R \theta'_R$ Then $X_{1_R} \xrightarrow{\theta'_R} Y_R$, $X_{1_L} = Y_L$ and $\langle |_L \theta_L, |_R \theta_R \rangle \frown |_R \theta'_R$ implies $\theta_R \frown \theta'_R$ in $X_R \xrightarrow{\theta'_R} X_{1_R} \xrightarrow{\theta'_R} Y_R$ by Lemma 1. We can then use the induction hypothesis to obtain $X_R \xrightarrow{\theta'_R} X_{2_R} \xrightarrow{\theta'_R} Y_R$ from which it is immediate to obtain $X_L | X_R \xrightarrow{|_R \theta'_R} X_L | X_{2_R} \xrightarrow{\langle |_L \theta_L, |_R \theta_R \rangle} X_{1_L} | Y_R = Y_L | Y_R$.

$\theta_2$ is $|_L \theta'_L$ This is symmetric to the previous one.

$\theta_2$ is $\langle |_L \theta'_L, |_R \theta'_R \rangle$ This case is essentially a combination of the two previous cases. Since $\langle |_L \theta'_L, |_R \theta'_R \rangle = \theta_1 \frown \theta_2 = \langle |_L \theta_L, |_R \theta_R \rangle$, Lemma 1 gives us two traces

$$X_L \xrightarrow{\theta_L} X_{1_L} \xrightarrow{\theta'_L} Y_L \quad \text{and} \quad X_R \xrightarrow{\theta_R} X_{1_R} \xrightarrow{\theta'_R} Y_R$$

where $\theta_L \frown \theta'_L$ and $\theta_R \frown \theta'_R$, respectively. By induction hypothesis, we obtain two traces

$$X_L \xrightarrow{\theta'_L} X_{2_L} \xrightarrow{\theta_L} Y_L \quad \text{and} \quad X_R \xrightarrow{\theta'_R} X_{2_R} \xrightarrow{\theta_R} Y_R$$

that we can then re-combine using syn. twice to obtain, as desired,

$$X_L | X_R \xrightarrow{\langle |_L \theta'_L, |_R \theta'_R \rangle} X_{2_L} | X_{2_R} \xrightarrow{\langle |_L \theta_L, |_R \theta_R \rangle} Y_L | Y_R.$$

+L There exists $X_L, X_R, X_L^1$, and $Y_L$ s.t. $X \xrightarrow{\theta_1} X_1 \xrightarrow{\theta_2} Y$ is

$$X_L + X_R \xrightarrow{\theta_1} X_L^1 + X_R \xrightarrow{\theta_2} Y_L + X_R.$$

Note that we know all transitions happen on "$X_L$'s side" and $X_R$ remains unchanged as otherwise we could not sum two non-standard terms. Then, $X_L \xrightarrow{\theta_1} X_L^1 \xrightarrow{\theta_2} Y_L$, and as $\theta_1 \frown \theta_2$ in this transition as well, we can use the induction hypothesis to obtain $X_2$ s.t. $X_L \xrightarrow{\theta_2} X_2 \xrightarrow{\theta_1} Y_L$. From this, it is easy to obtain $X_L + X_R \xrightarrow{\theta_2} X_2 + X_R \xrightarrow{\theta_1} Y_L + X_R$ and this concludes this case.

+R This is symmetric to +L.

□

**Lemma 4 (Backward transitions are concurrent).** Any two different coinitial backward transitions $t_1 : X \xrightarrow{\theta_1} X_1$ and $t_2 : X \xrightarrow{\theta_2} X_2$ are concurrent.

*Proof.* The first important fact to note is that $\mathcal{K}(\theta_1) \neq \mathcal{K}(\theta_2)$: by a simple inspection of the backward rules in Fig. 3, it is easy to observe that if a reachable process $X$ can perform two different backward transitions, then they must have different keys. Then, the proof is by induction on the length of $\theta_1$: while the lengths of the prefix and of the terms are not correlated, the result exposed in Sect. B-and briefly reminded in the proof below- allows to infer the structure of $X$ from that of $\theta_1$ and $\theta_2$.
$\theta_1$ is of length 1 Then, $\theta_1$ is a prefix and $X$ is either

- of the form $\alpha[k].X'$ with $\text{std}(X')$, but in that case $X$ cannot have two different backward transitions, so this case is vacuously true,

- of the form $X' + Y$ with $\text{std}(Y)$ (or the symmetric), of the form $X'\backslash a$, or of the form $\alpha[k].X'$ with $X'$ not standard: in all those cases, one can simply “extract” from the derivations the sub-trees that actually produce the $\theta_1$ or $\theta_2$ labels–as opposed to the rules that simply propagate it–, reason about it, and then restore the rest of the tree. As the concerned rules $(+_{\bullet}, +_{\bullet}, \text{res}.\bullet$ and $\text{pre}.\bullet)$ do not change the label, the dependencies or the derivability of the sub-tree, we can safely remove them, apply the previous reasoning to the act.\bullet rules that actually introduced the $\theta_1$ and $\theta_2$ labels, and restore the tree.

$\theta_1$ is of length greater than 1 We proceed by case on the structure of $\theta_1$, and use freely the previous remark–again, made formal in Sect. B–that makes it possible to “skip over” $+$, $\backslash a$ and $\alpha[k]$ operators to focus on the sub-tree that actually produces the labels: as an example, it is immediate that reasoning on a term $X$ of the form $Y_L + Y_R$ amounts to reasoning on $Y_L$ or $Y_R$, whichever is not standard, and that the other part of the process play no significant role in the proof.

$\theta_1$ is of the form $|_L \theta'_1$ Then we proceed by case on $\theta_2$.

$\theta_2$ is $|_L \theta'_2$ Then, it holds by induction hypothesis after decomposing and re-composing both traces: we have

$$X_L | X_R \underset{\sim}{\overset{|_L \theta'_1}{\rightleftharpoons}} X_{1_L} | X_R \quad \text{and} \quad X_L | X_R \underset{\sim}{\overset{|_L \theta'_2}{\rightleftharpoons}} X_{2_L} | X_R$$

and since $\mathcal{R}(\theta_1) \neq \mathcal{R}(\theta_2)$, $\theta'_1 \neq \theta'_2$, so we can use the induction hypothesis to obtain that $X_L \underset{\sim}{\overset{\theta'_1}{\rightleftharpoons}} X_{1_L}$ and $X_L \underset{\sim}{\overset{\theta'_2}{\rightleftharpoons}} X_{2_L}$ are concurrent, from which we easily deduce that $t_1 : X \underset{\sim}{\overset{\theta'_1}{\rightleftharpoons}} X_1$ and $t_2 : X \underset{\sim}{\overset{\theta'_2}{\rightleftharpoons}} X_2$ are concurrent.

$\theta_2$ is $|_R \theta'_2$ Then, it is immediate, as $|_L \theta'_1 \ll |_R \theta'_2$ never hold.

$\theta_2$ is $\langle|_L \theta'_2, |_R \theta''_2\rangle$ Then we must prove that

$$X_L | X_R \underset{\sim}{\overset{|_L \theta'_1}{\rightleftharpoons}} X_{1_L} | X_R \quad \text{and} \quad X_L | X_R \underset{\sim}{\overset{\langle|_L \theta'_2, |_R \theta''_2\rangle}{\rightleftharpoons}} X_{2_L} | X_{2_R}$$

are concurrent. As we know that $\mathcal{R}(\theta_1) \neq \mathcal{R}(\theta_2)$, $\theta'_1 \neq \theta'_2$, and we can use the induction hypothesis to get that

$$X_L \underset{\sim}{\overset{\theta'_1}{\rightleftharpoons}} X_{1_L} \quad \text{and} \quad X_L \underset{\sim}{\overset{\theta'_2}{\rightleftharpoons}} X_{2_L},$$

are concurrent It is obvious that $|_L \theta'_1 \ll |_R \theta''_2$ does not hold, hence $|_L \theta'_1 \sim \langle|_L \theta'_2, |_R \theta''_2\rangle$ in $X_{1_L} | X_R \xrightarrow{|_L \theta} X_L | X_R \underset{\sim}{\overset{\langle|_L \theta'_2, |_R \theta''_2\rangle}{\rightleftharpoons}} X_{2_L} | X_{2_R}$, and this concludes this case by Definition 12.

$\theta_1$ is of the form $|_R \theta'_1$ This case is similar to the previous one.

$\theta_1$ is of the form $\langle|_L \theta'_1, |_R \theta''_1\rangle$ Then we proceed by case on $\theta_2$ in a similar fashion, and this case offers no resistance.

□
**Theorem 5 (Forward diamond (extd)).** For all $X \xrightarrow{\theta_1} X_1 \xrightarrow{\theta_2} Y$ with $\theta_1 \prec \theta_2$, there exists $X_2$ s.t. $X \xrightarrow{\hat{\theta}_2} X_2 \xrightarrow{\hat{\theta}_1} Y$, and $\sigma(\hat{\theta}_i) = \sigma(\theta'_i)$ for $i \in \{1, 2\}$.

*Proof.* We can re-use the proof for Theorem 1 immediately, since $\sigma(\theta) = \theta$ in all the cases we had, and since $\theta_2$ cannot be of the form $!\theta$ in the cases where we have to decompose it. But we now need to consider the case where repl.₁ or repl.₂ is the last rule of $\theta_1$'s derivation.

For repl.₁, in a nutshell, if $!X \xrightarrow{!\theta'_1}!X$ $| X_1 \xrightarrow{\theta_2} Y_L$ $| Y_R$ with $!\theta'_1 \prec \theta_2$, then $\theta_2$ cannot be of the form $|_L \theta'_2$ nor $\langle \theta_L, \theta_R \rangle$, as $!\theta'_1 \prec \theta_2$ would not hold in those cases, by (3) on p. 15. Since $\theta_2$ cannot be of the form $!\theta'_2$ either (as $!X$ $| X_1$ cannot make such a transition), it must be of the form $|_R \theta'_2$, with $\theta'_2 \prec \theta'_1$ in $X \xrightarrow{\theta'_1} X_1 \xrightarrow{\theta'_2} Y_R$—otherwise, $!\theta'_1 = \theta_1 \prec \theta_2 = |_R \theta'_2$ would not hold—, and hence $Y_L =!X$. By induction hypothesis, we obtain a transition $X \xrightarrow{\hat{\theta}'_2} X_2 \xrightarrow{\hat{\theta}'_1} Y_R$ with $\sigma(\hat{\theta}'_2) = \sigma(\theta'_2)$ and $\sigma(\hat{\theta}'_1) = \sigma(\theta'_1)$, from which it is easy to obtain $!X \xrightarrow{!\hat{\theta}'_2}!X$ $| X_2 \xrightarrow{|_R \hat{\theta}'_1}!X$ $| Y_R$ as desired, with

$$ \sigma(!\hat{\theta}'_2) = |_R \sigma(\hat{\theta}'_2) = |_R \sigma(\theta'_2) = \sigma(|_R \theta'_2) = \sigma(\theta_2) $$

and

$$ \sigma(|_R \hat{\theta}'_1) = |_R \sigma(\hat{\theta}'_1) = |_R \sigma(\theta'_1) = \sigma(!\theta'_1) = \sigma(\theta_1) $$

For repl.₂, if $!X \xrightarrow{!\langle|_L \theta_L, |_R \theta_R\rangle}!X$ $| (X_1 | X_2) \xrightarrow{\theta_2} Y_L$ $| Y_R$, then observe that $\theta_2$ cannot be of the form $|_L \theta'_2$ nor $\langle \theta'_L, \theta'_R \rangle$ without contradicting $\theta_1 \prec \theta_2$, and that it cannot be of the form $!\theta'_2$ neither as the top connector in $!X$ $| (X_1 | X_2)$ is not $. Hence, it must be of the form $|_R \theta'_R$, with $\theta'_R$ not of the form $|_L \theta''_R$ nor $|_R \theta''_R$ (following Remark 2), nor $!\theta''_R$ (as the top connector of $X_1 | X_2$ is not !). Hence, $\theta_2$ is of the form $|_R \langle|_L \theta'_L, |_R \theta'_R\rangle$, and it follows by induction hypothesis: as $\theta_1 \prec \theta_2$ in

$$ !X \xrightarrow{!\langle|_L \theta_L, |_R \theta_R\rangle}!X \mid (X_1 \mid X_2) \xrightarrow{|_R \langle|_L \theta'_L, |_R \theta'_R\rangle}!X \mid (X'_1 \mid X'_2) $$

it must be the case that $\theta_L \prec \theta'_L$ and $\theta_R \prec \theta'_R$ in

$$ X \xrightarrow{\theta_L} X_1 \xrightarrow{\theta'_L} X'_1 \quad \text{and} \quad X \xrightarrow{\theta_R} X_2 \xrightarrow{\theta'_R} X'_2 $$

using the induction hypothesis twice gives us $X_1'', X_2'', \hat{\theta}_L, \hat{\theta}'_L, \hat{\theta}_R$ and $\hat{\theta}'_R$ s.t.

$$ X \xrightarrow{\hat{\theta}'_L} X_1'' \xrightarrow{\hat{\theta}_L} X'_1 \quad \text{and} \quad X \xrightarrow{\hat{\theta}'_R} X_2'' \xrightarrow{\hat{\theta}_R} X'_2 $$

from which we can obtain

$$ !X \xrightarrow{!\langle|_L \hat{\theta}'_L, |_R \hat{\theta}'_R\rangle}!X \mid (X_1'' \mid X_2'') \xrightarrow{|_R \langle|_L \hat{\theta}_L, |_R \hat{\theta}_R\rangle}!X \mid (X'_1 \mid X'_2) $$

and as $\sigma(!\theta) = |_R \sigma(\theta)$, the condition on $\sigma$ follows easily. $\square$
## B Technical Lemma on Sub-terms

This brief section exposes why we can, w.l.o.g., assume that a term capable of performing a transition labeled by a prefix (resp. prefixed by $|_L$, $|_R$, $\langle\theta_L, \theta_R\rangle$, resp. prefixed by !) can always be assumed to have for primary connector the same prefix (resp. a parallel composition, resp. a replication). The lemma is not very insightful, but easy and critical in conducting the proof of Lemma 4.

**Definition 15 (Sub-term).** Given $X, Y, X$ is a subterm of $Y, X \subseteq Y$ if

$$X = Y \quad X = Y + Y' \quad X = Y' + Y \quad X = Y \setminus \alpha \quad X = a[k].Y$$

**Lemma 6.** If $X \xrightarrow{\theta_1} Y$, then $\exists X', Y' \text{ s.t. } X' \subseteq X, Y' \subseteq Y, X' \xrightarrow{\theta_1} Y'$, and

- if $\theta_1$ is of the form $\alpha[k]$, then the primary connector of $X'$ is the prefix $\alpha$ if the transition is forward, $\alpha[k]$ if it is backward,

- if $\theta_1$ is of the form $|_L \theta'_1, |_R \theta'_1$, or $\langle |_L \theta_L, |_R \theta_R \rangle$, then the primary connector of $X'$ is the parallel composition,

- if $\theta_1$ is of the form $!\theta'_1$, then the primary connector of $X'$ is the replication.

Furthermore, if $Y \xrightarrow{\theta_2} Z$ with $\theta_1 \frown \theta_2$ in $X \xrightarrow{\theta_1} Y \xrightarrow{\theta_2} Z$, then $\exists Z' \text{ s.t. } Y' \xrightarrow{\theta_2} Z'$ with $Z' \subseteq Z$ and $\theta_1 \frown \theta_2$ in $X' \xrightarrow{\theta_1} Y' \xrightarrow{\theta_2} Z'$.

*Proof.* The first part is by case on $\theta_1$, and on the primary connector of $X$:

$\theta_1$ is $\alpha[k]$ We reason by induction on the size of $X$, and sometimes on the direction of the transition:

If $X$ is $\beta.X''$ Then it must be the case that $\beta = \alpha$, otherwise $X \xrightarrow{\alpha[k]} Y$ would not hold, and we take $X' = X$.

If $X$ is $\beta[m].X''$ If $\beta[m].X'' \xrightarrow{\alpha[k]} \beta[m].Y''$, then we apply the induction hypothesis to $X'' \xrightarrow{\alpha[k]} Y''$, otherwise there are two cases: if $X \xrightarrow{\alpha[k]} Y$ and $\beta[m] \neq \alpha[k]$, then we use the induction hypothesis, otherwise we let $X' = X$ and $Y' = Y$.

If $X$ is $X_1 + X_2$ Then if $X_1 + X_2 \xrightarrow{\alpha[k]} X_1'' + X_2''$ with $\text{std}(X_1)$ (resp. $\text{std}(X_2)$), we use the induction hypothesis on $X_2 \xrightarrow{\alpha[k]} X_2''$ (resp. $X_1 \xrightarrow{\alpha[k]} X_1''$). If the transition is forward we use the induction hypothesis on $X_1 \xrightarrow{\alpha[k]} X_1''$ (resp. $X_2 \xrightarrow{\alpha[k]} X_2''$) if the last rule of the derivation for the transition is $+L$ (resp. $+R$).

If $X$ is $X'' \setminus \alpha$ Then $Y = Y'' \setminus \alpha$ and we use the induction on $X'' \xrightarrow{\alpha[k]} Y''$.

If $X$ is $X_L | X_R$ Then $X \xrightarrow{\alpha[k]} Y$ is not possible.

If $X$ is $!X'$ Then $X \xrightarrow{\alpha[k]} Y$ is not possible.

$\theta_1$ is $|_L \theta'_1, |_R \theta'_1$, or $\langle |_L \theta_L, |_R \theta_R \rangle$ We reason by case on the primary connector of $X$, and sometimes on the direction of the transition:

If $X$ is $\beta.X''$ Then $\beta.X'' \xrightarrow{\theta_1} Y$ is not possible.
If $X$ is $\beta[m].X''$ If $\beta[m].X'' \xrightarrow{\theta_1} \beta[m].Y''$, then we apply the induction hypothesis to $X'' \xrightarrow{\theta_1} Y''$.

If $X$ is $X_1 + X_2$ or $X'' \setminus \alpha$ This is the same reasoning as the sum and prefix cases whenever $\theta_1 = \alpha[k]$, we apply the induction hypothesis to the subterm.

If $X$ is $X_L | X_R$ Then $X' = X$.

If $X$ is $!X'$ Then $X \xrightarrow{\theta_1} Y$ is not possible.

$\theta_1$ is $!\theta'_1$ We reason by case on the primary connector of $X$, and sometimes on the direction of the transition:

If $X$ is $\beta.X''$ Then $\beta.X'' \xrightarrow{!\alpha'_1} Y$ is not possible.

If $X$ is $\beta[m].X''$ If $\beta[m].X'' \xrightarrow{!\theta'_1} \beta[m].Y''$, then we apply the induction hypothesis to $X'' \xrightarrow{!\theta'_1} Y''$.

If $X$ is $X_1 + X_2$ or $X'' \setminus \alpha$ This is the same reasoning as the sum and prefix cases whenever $\theta_1 = !\theta'_1$, we apply the induction hypothesis to the subterm.

If $X$ is $X_L | X_R$ Then $X \xrightarrow{!\theta'_1} Y$ is not possible.

If $X$ is $!X'$ Then $X' = X$.

For the second part, it amounts to observe that as "extracting" the sub-terms does not change the labels of the transitions, if $\theta_1 \prec \theta_2$ in $X \xrightarrow{\theta_1} Y \xrightarrow{\theta_2} Z$, then applying the first part of this lemma to $Y \xrightarrow{\theta_2} Z$ gives us the very same $Y'$ as we obtain after applying the first part of this lemma to $X \xrightarrow{\theta_1} Y$: we simply "go under" the $+$, $\setminus \alpha$ and $a[k]$ connectors whenever possible, and the exact same structure is stripped from the target of the transition. The condition $\theta_1 \prec \theta_2$ is required for the structures stripped away from $X$ and $Y$ to match: without this condition, we can get e.g. $(a[m].X + b.Y) \setminus c \stackrel{a[m]}{\rightsquigarrow} (a.X + b.Y) \setminus c \xrightarrow{b[m]} (a.X + b[m].Y) \setminus c$ whose subterms $a[m].X$ and $b.Y$ are not equal, hence violating the second part of the lemma. $\square$