Ivan Lanese

Claudio Antares Mezzina

Jean-Bernard Stefani

Reversibility in the higher-order π-calculus

Keywords: reversible computation, process algebra, π-calculus

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

Introduction

Motivation. The notion of reversible computation has already a long history [START_REF] Bennett | Notes on the history of reversible computation[END_REF]. It has its origin in physics with the observation by Landauer that only irreversible computations need to consume energy [START_REF] Landauer | Irreversibility and heat generated in the computing process[END_REF]. It has since attracted interest in diverse fields, including e.g. hardware design [START_REF] Frank | Introduction to reversible computing: motivation, progress, and challenges[END_REF], computational biology [START_REF] Cardelli | Reversible structures[END_REF], program debugging [START_REF] Akgul | Assembly instruction level reverse execution for debugging[END_REF], and quantum computing [START_REF] Altenkirch | A functional quantum programming language[END_REF]. Of particular interest is its application to the study of programming abstractions for reliable systems. For instance, Bishop advocates using reversible computing as a means to achieve fail-safety in a sequential setting [START_REF] Bishop | Using reversible computing to achieve fail-safety[END_REF]. Moreover, most fault-tolerant schemes exploiting system recovery techniques [START_REF] Avizienis | Basic concepts and taxonomy of dependable and secure computing[END_REF], including exception handling [START_REF] Jacobs | Failboxes: Provably safe exception handling[END_REF], checkpoint/rollback [START_REF] Elnozahy | A survey of rollback-recovery protocols in message-passing systems[END_REF] and transaction management [START_REF] Weikum | Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery[END_REF], rely on some form of undo or another. All this suggests it can be worthwhile to formally investigate reversibility in concurrent systems, with the hope that reversible computing ideas can lead us to more systematic and more composable abstractions for the design and construction of recoverable systems.

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

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

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

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

The rhoπ calculus

Informal presentation

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

m 1 : (P 1 + Q 1 ) | m 2 : (P 2 + Q 2 ) → m 2 , a, Q 1 • m 1 : P ′ 1 | m 1 , a, Q 2 • m 2 : P ′ 2
In the reduction above, a memory of the form m 2 , a, Q 1 • m 1 represents the fact that its monitored process has performed an input on the channel a (a represents an output), interacting with a process monitored by the memory m 2 , and discarded the alternative process Q 1 . By exploiting all the information stored in the memories, the above synchronization can be reverted as follows: Danos and Krivine rely on the following rule:

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

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

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

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

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

(k : P ) | [M ; k] M
We thus have:

M ։ νk. k : Q{ P / X } | [M ; k] νk. M
Since k is fresh, νk. M is actually structurally equivalent to M . We thus have a perfect reversal of a forward computation: M ։ M .

Remark 1. Following Danos and Krivine [START_REF] Danos | [END_REF], one could consider also taking into account irreversible actions. We do not do so in this paper for the sake of simplicity.

Adding irreversible actions to rhoπ would be conceptually straightforward.

Remark 2. Using memories as presented here to enable reversibility simplifies the formal development but leads to a space explosion of computations in rhoπ. We do not consider implementation and related space efficiency issues in this paper. This issue has been analysed in [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF] in the context of the Oz language.

Syntax

Names, keys, and variables. We assume the existence of the following denumerable infinite mutually disjoint sets: the set N of names, the set K of keys, and the set V of process variables. The set I = N ∪ K is called the set of identifiers. N denotes the set of natural integers. We let (together with their decorated variants): a, b, c range over N ; h, k, l range over K; u, v, w range over I; X, Y, Z range over V. We denote by ũ a finite set of identifiers {u 1 , . . . , u n }.

Syntax. The syntax of the rhoπ calculus is given in Figure 1 (in writing rhoπ terms, we freely add balanced parenthesis around terms to disambiguate them). Processes of the rhoπ calculus, given by the P, Q productions in Figure 1, are the standard processes of the asynchronous higher-order πcalculus [START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higher-order paradigms[END_REF]. A receiver process (or trigger ) in rhoπ takes the form a(X) ⊲ P , which allows the receipt of a message of the form a Q on channel a.

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

A thread κ : P is just a tagged process P , where the tag κ is either a single key k or a pair of the form h, h • k, where h is a set of keys, with h ∈ h. A tag serves as an identifier for a process. As we will see below, together with memories tags help capture the flow of causality in a computation.

P ) | (κ 2 : a(X) ⊲ Q)) u ∈ I a ∈ N X ∈ V h, k ∈ K κ ∈ T Figure 1: Syntax of rhoπ
A memory is a process of the form [µ; k], which keeps track of the fact that a configuration µ was reached during execution, that triggered the launch of a thread tagged with the fresh tag k. In a memory [µ; k], we call µ the configuration part of the memory, and k the thread tag of the memory. Memories are generated by computation steps and are used to reverse them. The configuration part µ = (κ 1 : a P ) | (κ 2 : a(X) ⊲ Q) of the memory records the message a P and the trigger a(X) ⊲ Q involved in the message receipt, together with their respective thread tags κ 1 , κ 2 .

P denotes the set of rhoπ processes, and C the set of rhoπ configurations. We call agent an element of the set A = P ∪ C. We let (together with their decorated variants) P, Q, R range over P; L, M, N range over C; and A, B, C range over agents. We call primitive thread process, a process that is either a message a P or a trigger a(X) ⊲ P . We let τ and its decorated variants range over primitive thread processes.

Remark 3. We have no construct for replicated processes, output prefixing, or guarded choice in rhoπ: as in the asynchronous HOπ, also in rhoπ these can be easily encoded.

Free names and free variables. Notions of free identifiers and free (process) variables in rhoπ are classical. It suffices to note that constructs with binders are of the forms: νa. P , which binds the name a with scope P ; νu. M , which binds the identifier u with scope M ; and a(X)⊲P , which binds the variable X with scope P . We denote by fn(P ), fn(M ) and fn(κ) the set of free names, free identifiers, and free keys, respectively, of process P , of configuration M , and of tag κ. Note in particular that fn(κ : P ) = fn(κ) ∪ fn(P ), fn(k) = {k} and fn( h, h • k) = h ∪ {k}. We say that a process P or a configuration M is closed if it has no free (process) variable. P • denotes the set of closed processes, C • the set of closed configurations, and A • the set of closed agents.

Remark 4.

In the remainder of the paper, we adopt Barendregt's Variable Convention: If terms t 1 , . . . , t n occur in a certain context (e.g. definition, proof), then in these terms all bound identifiers and variables are chosen to be different from the free ones.

Consistent configurations. Not all configurations allowed by the syntax in Figure 1 are meaningful. In a memory [µ; k], tags occurring in the configuration part µ must be different from the thread tag k. This is because the key k is freshly generated when a computation step (a message receipt) takes place, and it is used to identify the newly created thread. Tags appearing in the configuration part identify threads (message and trigger) which have participated in the computation step. In a configuration M , we require all the threads to be uniquely identified by their tag, and we require consistency between threads and memories: if M contains a memory [µ; k] (i.e. [µ; k] occurs as a subterm of M ), we require M to also contain a thread tagged with k: components of this thread, i.e. threads whose tags have k as a suffix, can occur either directly in parallel with [µ; k] or in the configuration part of another memory contained in M (because they may have interacted with other threads). We call consistent a configuration that obeys these constraints. We defer the formal definition of consistent configurations to Section 2.3.

Operational semantics

The operational semantics of the rhoπ calculus is defined via a reduction relation →, which is a binary relation over closed configurations → ⊂ C • × C • , and a structural congruence relation ≡, which is a binary relation over processes and configurations ≡ ⊂ P 2 ∪ C 2 . We define evaluation contexts as "configurations with a hole •" given by the following grammar:

E ::= • | (M | E) | νu. E
General contexts C are just processes or configurations with a hole replacing a 0 (process or configuration). A congruence on processes and configurations is an equivalence relation R that is closed for general contexts:

P R Q =⇒ C[P ] R C[Q] and M R N =⇒ C[M ] R C[N ].
The relation ≡ is defined as the smallest congruence on processes and configurations that satisfies the rules in Figure 2. We write t = α t ′ when terms t, t ′ are equal modulo α-conversion. If ũ = {u 1 , . . . , u n }, then ν ũ. A stands for νu 1 . . . . νu n . A (there is no need to indicate the order of binders

(E.ParC) A | B ≡ B | A (E.ParA) A | (B | C) ≡ (A | B) | C (E.NilM) A | 0 ≡ A (E.NewN) νu. 0 ≡ 0 (E.NewC) νu. νv. A ≡ νv. νu. A (E.NewP) (νu. A) | B ≡ νu. (A | B) (E.α) A = α B =⇒ A ≡ B (E.TagN) κ : νa. P ≡ νa. κ : P (E.TagP) k : n i=1 τ i ≡ ν h. n i=1 ( h i , h • k : τ i ) h = {h 1 , . . . , h n } n > 1
Figure 2: Structural congruence for rhoπ thanks to rule E.NewC). We write n i=1 A i for A 1 | . . . | A n (as before, there is no need to indicate how the latter expression is parenthesized because the parallel operator is associative by rule E.ParA). In rule E.TagP, processes τ i are primitive thread processes (i.e., messages or triggers). Recall the use of the variable convention in these rules: for instance, in the rule (νu. A) | B ≡ νu. (A | B) the variable convention makes implicit the condition u ∈ fn(B). The structural congruence rules are the usual rules for the π-calculus (E.ParC to E.α) without the rule dealing with replication, and with the addition of two new rules dealing with tags: E.TagN and E.TagP. Rule E.TagN is a scope extrusion rule to push restrictions to the top level. Rule E.TagP allows to generate unique tags for each primitive thread process in a configuration. An easy induction on the structure of terms provides us with a kind of normal form for configurations (by convention i∈I A i = 0 if I = ∅):

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

M ≡ ν ũ. i∈I (κ i : ρ i ) | j∈J [µ j ; k j ] with ρ i = 0, ρ i = a i P i , or ρ i = a i (X i ) ⊲ P i .
We say that a binary relation R on closed configurations is evaluationclosed if it satisfies the inference rules: Relations ։ and are defined to be the smallest evaluation-closed binary relations on closed configurations satisfying the rules in Figure 3 (note again the use of the variable convention: in rule R.Fw the key k is fresh).

(R.Ctx) M R N E[M ] R E[N ] (R.Eqv) M ≡ M ′ M ′ R N ′ N ′ ≡ N M R N (R.Fw) (κ 1 : a P ) | (κ 2 : a(X) ⊲ Q) ։ νk. (k : Q{ P / X }) | [(κ 1 : a P ) | (κ 2 : a(X) ⊲ Q); k] (R.Bw) (k : P ) | [M ; k] M
The rule for forward reduction (R.Fw) is the standard communication rule of the higher-order π-calculus with two side effects: (i) the creation of a new memory to record the configuration that gave rise to it, namely the parallel composition of a message and a trigger, properly tagged (tags κ 1 and κ 2 in the rule); (ii) the tagging of the continuation of the message receipt with the fresh key k. The rule for backward reduction (R.Bw) is straightforward: in presence of the thread tagged with key k, memory [M ; k] reinstates the configuration M that gave rise to the tagged thread. We use ։ * , * and ⇒ to denote the reflexive and transitive closure of ։, and →, respectively. With the reduction rules and the structural laws in place, we can see how the structural rule E.TagP is used by the reduction. In particular the rule, if used from left to right after a forward step, lets the continuation of a trigger (if it is a parallel composition) continue executing in the forward direction. On the other side, when used from right to left, E.TagP gathers back all the primitive thread processes belonging to the same parallel composition identified by a particular key. An example of execution will make it clear.

Let M = (k 1 : a P ) | (k 2 : a(X) ⊲ b X | b(X) ⊲ 0), we have that: M ։ νk. k : (b P | b(X) ⊲ 0) | [M ; k] (1)
≡ νk, h 1 , h 2 . ( h 1 , h • k : b P ) | ( h 2 , h • k : b(X) ⊲ 0) | [M ; k] (2)
։ νk, h 1 , h 2 , k 3 . (k 3 : 0) | [M ; k] | [M 1 ; k 3 ] (3) νk, h 1 , h 2 . ( h 1 , h • k : b P ) | ( h 2 , h • k : b(X) ⊲ 0) | [M ; k] (4) ≡ νk. k : (b P | b(X) ⊲ 0) | [M ; k] (5) νk. (k 1 : a P ) | (k 2 : a(X) ⊲ b X | b(X) ⊲ 0) (6) with h = {h 1 , h 2 }, M 1 = ( h 1 , h • k : b P ) | ( h 2 , h • k : b(X) ⊲ 0)
. We can note in (2) the use of the rule E.TagP from left to right, in order to allow the two primitive processes to execute [START_REF] Frank | Introduction to reversible computing: motivation, progress, and challenges[END_REF]. On the other side, we use the rule in the opposite way in [START_REF] Akgul | Assembly instruction level reverse execution for debugging[END_REF] in order to build back the parallel composition and enable the backward reduction in [START_REF] Altenkirch | A functional quantum programming language[END_REF].

Remark 5. One could have thought of mimicking the structural congruence rule dealing with parallel composition in [START_REF] Danos | Reversible communicating systems[END_REF], using a monoid structure for tags:

(E.TagP * ) κ : (P | Q) ≡ νh 1 , h 2 . (h 1 • κ : P ) | (h 2 • κ : Q)
Unfortunately using E.TagP * instead of E.TagP would introduce some undesired non-determinism, which would later complicate our definitions (in relation to causality) and proofs. For instance, let M = k : a Q | (h : a(X) ⊲ X). We have:

M → M ′ = νl. (l : Q) | [M ; l]
Now, assuming ETagP * , we would have:

M ≡ (k : (a Q | 0)) | (h : a(X) ⊲ X) ≡ νh 1 , h 2 . ((h 1 • k : a Q ) | (h 2 • k : 0)) | (h : a(X) ⊲ X) Let M 1 = (h 1 • k : a Q ) | (h : a(X) ⊲ X).
We would then have: M → M ′′ , where

M ′′ = νh 1 , h 2 , l. (l : Q) | [M 1 ; l] | (h 2 • k : 0). Clearly M ′ ≡ M ′′ ,
which means that a seemingly deterministic configuration, M , would have in fact two (actually, an infinity of) derivations towards non structurally equivalent configurations. By insisting on tagging only primitive thread processes, E.TagP avoids this unfortunate situation. We can characterize this by proving a kind of determinacy lemma for rhoπ, which fails if we replace rule E.TagP with rule E.TagP * . Extend the grammar of rhoπ with marked primitive thread processes of the form τ * . This extended calculus has exactly the same structural congruence and reduction rules as rhoπ, but with possibly marked primitive thread processes. Now call primed a closed configuration M with exactly two marked processes of the form a P * and (a(X) ⊲ Q) * . By extending ≡ and → to marked processes we have:

Lemma 2 (Determinacy). Let M be a primed configuration such that M ≡ M 1 = E 1 [κ 1 : a P * | κ 2 : (a(X) ⊲ Q) * ] and M ≡ M 2 = E 2 [κ ′ 1 : a P * | κ ′ 2 : (a(X) ⊲ Q) * ]. Assume M 1 → M ′ 1 and M 2 → M ′ 2 are derived by applying R.Fw with configurations κ 1 : a P * | κ 2 : (a(X) ⊲ Q) * , and κ ′ 1 : a P * | κ ′ 2 : (a(X) ⊲ Q) * , respectively, followed by R.Ctx. Then M ′ 1 ≡ M ′ 2 .
Proof. By induction on the form of E 1 , and case analysis on the form of κ 1 and κ 2 .

We can now formally define the notion of consistent configuration.

Definition 1 (Consistent configuration).

Let M ≡ ν ũ. i∈I (κ i : ρ i ) | j∈J [µ j ; k j ],
with ρ i = 0 or ρ i a primitive thread process, µ j = δ j : R j | γ j : T j , R j = a j P j , T j = a j (X j ) ⊲ Q j be a configuration. Let K be the multiset containing all the tags κ i for i ∈ I, δ j , γ j for j ∈ J. M is said to be consistent if the following conditions are met:

1. K is a set (i.e. all the elements in K are distinct) 2. For all j ∈ J, k j = δ j and k j = γ j 3. For all j 1 , j 2 ∈ J,

j 1 = j 2 =⇒ k j 1 = k j 2 4.
If there exists a tag κ ∈ K of the form h, h • k then:

• for each h l ∈ h there is κ ′ ∈ K of the form h l , h • k • k / ∈ K • there is no κ ′ ∈ K of the form h ′ l , h′ • k with h = h′ 5.
For all j ∈ J, there exist E ⊆ I, D ⊆ J \ {j}, G ⊆ J \ {j}, such that: Roughly, consistent configurations enjoy two properties: (i) uniqueness of tags and (ii) that for each memory [µ; k] there are processes corresponding to the continuation of µ in the configuration. In more detail, condition 1 ensures that processes (inside or outside memory) have unique tags. Condition 2 ensures that the thread tag of a memory never occurs in its own configuration part. Condition 3 states that all thread tags of memories are distinct. Condition 4 ensures that if a process (inside or outside memory) has a complex tag h, h • k then there are processes tagged with all the tags h l , h • k with h l ∈ h, and that no process is tagged by k or by a different complex tag with the same suffix key k. Condition 5 is the most tricky one. It requires that for each memory [δ j : a j P j | γ j : a j (X j ) ⊲ Q j ; k j ] there are threads in the configuration whose composition gives the continuation ν ũ. k j : Q j { P j / X j }. Note that because of the use of ≡ there are only two possibilities: either there is a unique thread corresponding to the continuation tagged with k j , or there are many of them, all tagged with complex tags having k j as a suffix, generated by one application of rule E.TagP. These threads may be at top level or inside the configuration parts of other memories (as participants to other communications).

ν ũ. k j : Q j { P j / X j } ≡ ν ũ.
Consistency is a global property, so the composition of consistent configurations may lead to a non consistent configuration, and subterms of consistent configurations may not be consistent. To better understand consistency let us consider a few examples:

k 1 : a 0 | [(k 1 : a 0 ) | (k 2 : a(X) ⊲ b 0 ); k] (1) k : a 0 | [(k 1 : a 0 ) | (k 2 : a(X) ⊲ b 0 ); k] (2) k : a 0 | [(k 1 : a 0 ) | (k 2 : a(X) ⊲ a X ); k] (3)
( h 1 , h • k : a 0 ) | (k : b 0 ) (4)
Configuration ( 1) is not consistent since it violates condition 1 on key k 1 and condition 5 on the memory. Configuration (2) is not consistent because it violates condition 5. Configuration (3) is consistent since all the tags are unique and k : a X { 0 / X } ≡ k : a 0 . Configuration (4) is not consistent since it violates condition 4. Consistent configurations are closed under reduction:

Lemma 3 (Consistency preservation). Let M be a consistent configuration. If M → N then N is a consistent configuration.

Proof. See Appendix A.1.

Remark 6. The presented semantics and machinery for reversing HOπ can be easily adapted to define reversibility in first order π-calculus. In general, the combination of memories and identifiers should be enough to define reversibility in calculi with implicit substitutions. Indeed, the need for memories stems from the fact that substitution is not a bijective, hence reversible, function: the only way to reverse a substitution is to record additional information to recover the exact form of the process before the substitution was applied.

Basic properties of reduction in rhoπ

In this section we show two main properties of rhoπ: (i) that rhoπ is a conservative extension of HOπ, and (ii) that each rhoπ reduction step can indeed be reversed.

We first recall HOπ syntax and semantics. The syntax of HOπ processes coincides with the syntax of rhoπ processes in Figure 1 (but HOπ has no concept of configuration). HOπ structural congruence, denoted ≡ π , is the least congruence generated by rules in Figure 2 (restricted to processes) but E.TagN and E.TagP. Evaluation contexts in HOπ are given by the following grammar:

E ::= • | (P | E) | νu. E
HOπ reduction relation → π is the least binary relation on closed processes closed under HOπ structural congruence and HOπ evaluation contexts defined by the rule:

(HO.Red) a P | a(X) ⊲ Q → π Q{ P / X }
In order to show (i) we define the erasing function γ : C → P, which maps a rhoπ configuration to its underlying HOπ process.

Definition 2 (Erasing function). The erasing function γ : C → P is defined inductively by the following clauses:

γ(0) = 0 γ(νa. M ) = νa. γ(M ) γ(νk. M ) = γ(M ) γ(M | N ) = γ(M ) | γ(N ) γ(κ : P ) = P γ([µ; k]) = 0
Let us note that γ directly deletes the creation of new keys (νk) since they have no meaning in HOπ (they are not names). Moreover it deletes all the extra machinery (tags and memories) used to reverse HOπ. Lemma 4 below shows that rhoπ forward computations are indeed decorations on HOπ reductions.

Lemma 4. For all closed configurations M, N , if M ։ N then γ(M ) → π γ(N ) Proof. See Appendix A.2.
We can prove a converse of Lemma 4. More precisely, Lemma 5 shows that for each HOπ process R, each HOπ reduction R → π S and each rhoπ configuration M such that γ(M ) = R we have a forward reduction in rhoπ corresponding to R → π S.

Lemma 5. For all closed HOπ processes R, S if R → π S then for all closed configurations M such that γ(M ) = R there is N such that M ։ N and γ(N ) = S.

Proof. See Appendix A.2.

Remark 7.

A canonical way of lifting a closed HOπ process P to a closed consistent configuration in rhoπ is by defining δ(P ) = νk. k : P . As a corollary of Lemma 4 we have:

Corollary 1. For each closed HOπ process P , if δ(P ) ։ N then P → π γ(N ).

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

Lemma 6 (Loop Lemma). For all closed consistent configurations M, N if M ։ N then N M , and if M N then N ։ M .
Proof. Let us start from the first implication. From Lemma 36 (see Appendix A.1) we have M ≡ M ′ and N ′ ≡ N with

M ′ = ν ũ. κ 1 : a P | κ 2 : a(X) ⊲ Q | i∈I κ i : ρ i | j∈J [µ j ; k j ] and N ′ = ν ũ, k. k : Q{ P / X } | [κ 1 : a P | κ 2 : a(X) ⊲ Q; k] | i∈I κ i : ρ i | j∈J [µ j ; k j ].
Then by applying rules (R.Fw), (R.Ctx) and (R.Eqv) we have N M , as desired. For the other direction from Lemma 37 (see Appendix A.1) we have

M ≡ M ′ with M ′ = ν ũ, k. k : R | [κ 1 : a P | κ 2 : a(X) ⊲ Q; k] | i∈I κ i : ρ i | j∈J [µ j ; k j ] and ν ũ. κ 1 : a P | κ 2 : a(X) ⊲ Q | i∈I κ i : ρ i | j∈J [µ j ; k j ] ≡ N .
Since M is a consistent configuration and consistency is preserved by structural congruence also M ′ is consistent. From consistency we know that k : R is the only thread tagged by k and that ν ũ, k. k : R ≡ ν ũ, k. k : Q{ P / X }. Then the result follows by applying rules (R.Bw), (R.Ctx) and (R.Eqv).

An easy induction on the length n of the sequence of reductions M ⇒ N shows that:

Corollary 2. For all closed consistent configurations M, N if M ⇒ N then N ⇒ M .

Contextual equivalence in rhoπ

Barbed congruence. We can classically complement the operational semantics of the rhoπ calculus with the definition of a contextual equivalence between configurations, which takes the form of a barbed congruence. We first define observables in configurations. We say that name a is observable in configuration M , noted M ↓ a , if M ≡ ν ũ. (κ : a P ) | N , with a ∈ ũ. Note that keys are not observable: this is because they are just an internal device used to support reversibility. We write M R ↓ a , where R is a binary relation on configurations, if there exists N such that M RN and N ↓ a . The following definitions are classical: Definition 3 (Barbed bisimulation and congruence).

A relation R ⊆ C • × C • on closed configurations is a strong (resp. weak ) barbed simulation if whenever M R N • M ↓ a implies N ↓ a (resp. N ⇒↓ a ) • M → M ′ implies N → N ′ , with M ′ RN ′ (resp. N ⇒ N ′ with M ′ RN ′ ) A relation R ⊆ C • × C • is a strong (resp. weak ) barbed bisimulation if R and R -1
are strong (resp. weak) barbed simulations. We call strong (resp. weak ) barbed bisimilarity and write ∼ (resp. ≈) the largest strong (resp. weak) barbed bisimulation. The largest congruence included in ∼ (resp. ≈) is called strong (resp. weak ) barbed congruence and is denoted ∼ c (resp. ≈ c ).

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

Lemma 7. For all closed consistent configurations M, N , if M ⇒ N , then M ≈ c N .
Proof. We show that the relation

R = {(C[M ], C[N ]) | M ⇒ N, C is a configuration context}
• if C[M ] ↓ a , then C[N ] ⇒ C[M ] ↓ a , and hence C[N ] ⇒↓ a as required. • if C[M ] → M ′ , then C[N ] ⇒ C[M ] → M ′ , and hence C[N ] ⇒ M ′ , as required.
Since R is a congruence by construction the thesis follows.

Lemma 7 shows that barbed congruence is not very discriminative among configurations: if N is derived from M then M ≈ c N . Barbed bisimilarity is even less discriminative: a configuration M is weak barbed bisimilar to a dummy configuration that shows directly all the possible barbs of M . Lemma 8. For each closed consistent configuration M let S be the set of weak barbs of M . Then M ≈ M D = a∈S (k a : a 0 ).

Proof. Let R = {(N, M D ) | M ⇒ N, M D = a∈S (k a : a 0 }.
We show that R is a weak barbed bisimilarity. All the challenges from N are matched by M D by staying idle, since it has by construction all the required barbs. M D performs no actions to be matched. Let a be a barb of M D . By construction a is a weak barb of M , and also of N since N ⇒ M by the Loop Lemma.

We will leave finding a general notion of observational equivalence for rhoπ, and for reversible calculi in general, for further study. For our purposes, i.e. proving the correctness of our encoding of rhoπ in a variant of higher-order π, it is enough to consider a custom notion of back and forth bisimulation.

Back and Forth Bisimulations. Notions of back and forth bisimulation, requiring essentially that forward moves are matched by forward moves and backward moves by backward moves, have already been studied in the literature (see [START_REF] De Nicola | Back and forth bisimulations[END_REF][START_REF] Hasuo | Generic forward and backward simulations[END_REF][START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Phillips | A logic with reverse modalities for historypreserving bisimulations[END_REF]). However, those works consider only strong equivalences, and use backward actions to better understand calculi with only forward actions, while we use them to study reversible calculi. Indeed, this kind of back and forth bisimulations can distinguish true concurrency aspects of forward calculi better than other equivalences such as classical strong bisimulation. For example, the two (CCS) processes:

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

We adapt this idea of back and forth bisimulation by defining an adhoc notion of weak behavioral equivalence allowing also reductions which are neither forward nor backward. They are needed since the encoding of rhoπ needs some auxiliary steps for managing bookkeeping information. We call such reductions administrative reductions. The equivalence we present below works up to administrative reductions. While we think that such a notion is useful for reasoning on our encoding, we do not claim that it is a good candidate to become a canonical equivalence on reversible calculi. Indeed, if it is used to relate processes of calculi with no administrative reductions, then this relation becomes a strong back and forth bisimulation.

We write ֒→ for the reduction relation composed by administrative steps, and ֒→ * for its reflexive and transitive closure. Note that in rhoπ relation ֒→ is empty.

Definition 4 (Bf barbed bisimulation and congruence).

A relation R ⊆ C • × C • on closed configurations is a strong (resp. weak ) backward and forward barbed simulation (or bf barbed simulation for brevity) if whenever M R N

• M ↓ a implies N ↓ a (resp. N ֒→ * ↓ a ) • M ։ M ′ implies N ։ N ′ , with M ′ RN ′ (resp. N ֒→ * ։֒→ * N ′ with M ′ RN ′ ) • M M ′ implies N N ′ , with M ′ RN ′ (resp. N ֒→ * ֒→ * N ′ with M ′ RN ′ ) • M ֒→ M ′ implies N ֒→ N ′ , with M ′ RN ′ (resp. N ֒→ * N ′ with M ′ RN ′ ) A relation R ⊆ C • × C • is a strong (resp. weak ) bf barbed bisimulation if R and
• ∼ c (resp. • ≈ c ).
Weak bf barbed bisimulation is actually strong with respect to forward and backward reductions, thus showing that the encoding correctly matches the behavior of rhoπ processes, but weak with respect to administrative steps ֒→, thus allowing the encoding to perform them at any moment. If bf barbed bisimulation is used to compare rhoπ processes, the strong version and the weak one coincide, that is

• ≈ = • ∼.
Hence, in rhoπ, weak bf barbed bisimulation becomes stronger than (classical) strong barbed bisimulation, since it is able to distinguish the direction of reductions. In fact, one forward (backward) step has to be matched by one forward (backward) step.

From the definitions, it is clear that

• ∼⊆∼, • ≈⊆≈, • ∼ c ⊆∼ c ,

and

• ≈ c ⊆≈ c , i.e., backward and forward equivalences are more discriminating than the corresponding standard counterparts. We show below that all these inclusions are strict.

Let us start from strong equivalences. Consider:

M = νk 1 , k 2 . (k 1 : a 0 ) | (k 2 : a(X) ⊲ b 0 ) N = νk 1 , k 2 , k. [(k 1 : b 0 ) | (k 2 : b(X) ⊲ a 0 ); k] | k : a 0
Both the configurations have a barb at a, a reduction to a configuration with a barb at b and its inverse, and no other reduction nor barb, thus M ∼ N . However, the reduction creating the barb at b is forward in M and backward in N , thus M

• ∼ N . The same counterexample and the same reasoning can be used also for weak equivalences.

Let us consider now congruences, starting from the weak ones. Consider the following configurations:

M = νk 1 , k 2 , k 3 . (k 1 : a 0 ) | (k 2 : a(X) ⊲ b 0 ) | (k 3 : a(X) ⊲ c 0 ) N = νk 1 , k 2 , k 3 , k 4 . (k 4 : b 0 ) | (k 3 : a(X) ⊲ c 0 ) | [(k 1 : a 0 ) | (k 2 : a(X) ⊲ b 0 ); k 4 ] M ′ = νk 1 , k 2 , k 3 , k 5 . (k 5 : c 0 ) | (k 2 : a(X) ⊲ b 0 ) | [(k 1 : a 0 ) | (k 3 : a(X) ⊲ c 0 ); k 5 ] Since M ։ N by Lemma 7 M ≈ c N , but M • ≈ N and hence M • ≈ c N .
To prove this last part, assume that there exists a weak bf barbed bisimulation R between M and N , i.e. such that (M, N ) ∈ R. We have M ։ M ′ , and we have no N ′ such that N ։ N ′ nor N ֒→ N ′ , thus the reduction cannot be matched.

For the strong congruences, consider:

M = νk 1 , k 2 , a, b. (k 1 : a 0 ) | (k 2 : a(X) ⊲ b 0 ) N = νk 1 , k 2 , k, a, b. [(k 1 : a 0 ) | (k 2 : a(X) ⊲ b 0 ); k] | k : b 0
The two configurations have no barbs, and they cannot interact with their contexts. Thus M ∼ c N , since they can both do infinite reductions. However M

• ∼ c N , since M can perform a forward step while N cannot perform forward nor administrative steps.

Causality in rhoπ

We now proceed to the analysis of causality in rhoπ. We first show that reversibility in rhoπ is causally consistent. We then show that the causality information in rhoπ is at least as fine as the causality information from [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF].

Causal consistency

In order to prove causal consistency, we mostly adapt the terminology and arguments of [START_REF] Danos | Reversible communicating systems[END_REF].

We call transition a triplet of the form

M m։ --→ M ′ , or M m --→ M ′ , where M, M ′ are closed consistent configurations, M → M ′ , and m is the memory involved in the reduction M → M ′ . We say that a memory m is involved in a forward reduction M ։ M ′ if M ≡ E[κ 1 : a P | κ 2 : a(X) ⊲ Q], M ′ ≡ E[νk. (k : Q{ P / X }) | m], and m = [κ 1 : a P | κ 2 : a(X) ⊲ Q; k]. In this case, the transition involving m is denoted by M m։ --→ M ′ . Likewise, we say that a memory m = [N ; k] is involved in a backward reduction M M ′ if M ≡ E[(k : Q) | m], M ′ ≡ E[N ].
In this case, the transition involving m is denoted by M m --→ M ′ . We let η and its decorated variants range over labels m ։ and m . If η = m ։ , we set η • = m and vice versa. In a transition M η -→ N , we say that M is the source of the transition, N is its target, and η is its label (of the form m ։ or m , where m is some memory).

Definition 5 (Name-preserving transitions). We say a transition t : M η -→ M ′ is name-preserving if M and M ′ are in thread normal form and if one of the following assumptions holds:

1. M = ν ũ. i∈I (κ i : ρ i ) | j∈J [µ j ; k j ] and M ′ = ν ũ. i∈I ′ (κ i : ρ i ) | j∈J ′ [µ j ; k j ], with J ′ = J ∪ {j ′ }, I ′ ⊂ I and η = m ։ with m = [µ j ′ ; k j ′ ]; 2. M = ν ũ. i∈I (κ i : ρ i ) | j∈J [µ j ; k j ] and M ′ = ν ũ. i∈I ′ (κ i : ρ i ) | j∈J ′ [µ j ; k j ], with J = J ′ ∪ {j ′ }, I ⊂ I ′ and η = m with m = [µ j ′ ; k j ′ ].
Intuitively, a name-preserving transition keeps track of the set of restricted identifiers of its configurations (and especially the tag of memory m). In the rest of this section we only consider name-preserving transitions and "transition" used in a definition, lemma or theorem, stands for "namepreserving transition". Note that working with name-preserving transitions only is licit because of the determinacy lemma (Lemma 5).

Two transitions are said to be coinitial if they have the same source, cofinal if they have the same target, composable if the target of one is the source of the other. A sequence of pairwise composable transitions is called a trace. We let t and its decorated variants range over transitions, σ and its decorated variants range over traces. Notions of target, source and composability extend naturally to traces. We note ǫ M the empty trace with source M , σ 1 ; σ 2 the composition of two composable traces σ 1 and σ 2 . The stamp

λ(m ։ ) of a memory m = [κ 1 : a P | κ 2 : a(X) ⊲ Q; k] is defined to be the set {κ 1 , κ 2 , k}; we set λ(m ) = λ(m ։ ). Definition 6 (Concurrent transitions). Two coinitial transitions t 1 = M η 1 -→ M 1 and t 2 = M η 2 -→ M 2 are said to be in conflict if there is a tag κ ∈ λ(η 1 ) such that κ ∈ λ(η 2 )
or κ is a key k and there is a complex tag with suffix k in λ(η 2 ) or there is a tag κ ∈ λ(η 2 ) such that κ ∈ λ(η 1 ) or κ is a key k and there is a complex tag with suffix k in λ(η 1 ). Two coinitial transitions are concurrent if they are not in conflict.

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

M = νl, k, h. (k : a P ) | [N ; k] | (h : a(X) ⊲ Q) has two possible transitions t = M m --→ νl, k, h. N | (h : a(X) ⊲ Q), where m = [N ; k], and t ′ = M m ′ ։ --→ νl, k, h. [N ; k] | m ′ | l : Q{ P / X }, where m ′ = [(k : a P ) | (h : a(X) ⊲ Q); l].
The two transitions t and t ′ are in conflict over the use of the resource k : a P .

Consider now the configuration

M = νl, k, h, h 1 , h 2 . ( h 1 , h • k : a P ) | ( h 2 , h • k : b 0 ) | [N ; k] | (h : a(X) ⊲ Q)
where h = {h 1 , h 2 }. Again we have a conflict, since the backward action involving memory [N ; k] is in conflict with any forward action by descendants of k, even if not all of them are involved.

The Loop Lemma ensures that each transition

t = M η - → N has a reverse one t • = N η• -→ M .
The above definition of concurrent transitions makes sense:

Lemma 9 (Square lemma). If t 1 = M η 1 -→ M 1 and t 2 = M η 2 -→ M 2 are two coinitial concurrent transitions, then there exist two cofinal transitions t 2 /t 1 = M 1 η 2 -→ N and t 1 /t 2 = M 2 η 1 -→ N .
Proof. By case analysis on the form of transitions t 1 and t 2 . See Appendix B.1 for details.

We are now in a position to show that reversibility in rhoπ is causally consistent. Following Lévy [START_REF] Lévy | An algebraic interpretation of the lambda beta k-calculus; and an application of a labelled lambda-calculus[END_REF] we define first the notion of causal equivalence between traces that abstracts away from the order of causally independent reductions. We define ≍ as the least equivalence relation between traces closed under composition that obeys the following rules:

t 1 ; t 2 /t 1 ≍ t 2 ; t 1 /t 2 t; t • ≍ ǫ source(t) t • ; t ≍ ǫ target(t)
Intuitively ≍ states that if we have two concurrent transitions, then the two traces obtained by swapping the order of their execution are the same, and that a trace composed by a transition followed by its inverse is equivalent to the empty one.

The proof of causal consistency proceeds along the exact same lines as in [START_REF] Danos | Reversible communicating systems[END_REF], with simpler arguments because of the simpler form of our memory stamps.

Lemma 10 (Rearranging Lemma). Let σ be a trace. There exists forward traces σ ′ and σ ′′ such that σ ≍ σ ′

• ; σ ′′ .

Proof. The proof is in Appendix B.1.

Lemma 11 (Shortening Lemma). Let σ 1 , σ 2 be coinitial and cofinal traces, with σ 2 forward. Then, there exists a forward trace

σ ′ 1 of length at most that of σ 1 such that σ ′ 1 ≍ σ 1 .
Proof. The proof is in Appendix B.1.

Theorem 1 (Causal consistency). Let σ 1 and σ 2 be coinitial traces, then σ 1 ≍ σ 2 if and only if σ 1 and σ 2 are cofinal.

Proof. The proof is in Appendix B.1.

Causality in rhoπ and in the causal higher-order π-calculus

From what precedes, it should be clear that the core of the reversibility machinery in rhoπ is the causality information built during execution. The question therefore arises of the relationship between this notion of causality and the one found in several studies on the causal semantics of the π-calculus, e.g. [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF][START_REF] Cattani | Models for name-passing processes: interleaving and causal[END_REF][START_REF] Crafa | Compositional event structure semantics for the internal pi-calculus[END_REF][START_REF] Varacca | Typed event structures and the linear picalculus[END_REF]. In this section we limit ourselves to the study of the relationship between the causality information used in rhoπ and that used by Boreale and Sangiorgi in their analysis of causality for the π-calculus [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF].

For a meaningful comparison, we first adapt the causality apparatus from that paper to the asynchronous higher-order π-calculus. We call "causal higher-order π" (choπ for short) the resulting calculus. Processes of choπ are exactly the processes in Figure 1. Following [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF], causal processes in choπ, ranged over by A, B, are processes decorated with causality information, defined by the following grammar:

A ::= K :: A | A | A | νa. A | P
where K ranges over finite sets of keys, i.e. K ⊆ fin K. Informally, a causal process K :: P identifies the set of causes K that gave rise to process P .

We denote by fk(A) the set of free keys of a causal process A.

We define a reduction semantics for choπ (see Appendix B.2 for a comparison between this reduction semantics and a labelled transition system semantics directly adapted from [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF]), via a reduction relation that operates modulo structural congruence. The structural congruence relation ≡ is the least congruence relation on causal processes that obeys the structural congruence rules on HOπ processes given in Figure 2

(C-red) K 1 :: a P | K 2 :: a(X) ⊲ Q → K 1 ∪ K 2 :: Q{ P / X }
Evaluation contexts for causal processes are given by the following grammar:

E ::= • | E | A | A | E | νa. E
An easy induction on the structure of a causal process gives us a normal form for closed causal processes. For any closed causal process A we have

(E-par) K :: A | B ≡ K :: A | K :: B (E-cau) K 1 :: K 2 :: A ≡ K 1 ∪ K 2 :: A (E-res) K :: νa. A ≡ νa. K :: A (E-void) ∅ :: A ≡ A (E-nil) K :: 0 ≡ 0
A ≡ νc. i∈I K i :: τ i
where each τ i is of the form a P or the form a(X) ⊲ P .

As for rhoπ, we can inductively define a function γ that erases the causality information from a causal process to get a standard HOπ process via the following clauses:

γ(P ) = P γ(νa. A) = νa. γ(A) γ(A | B) = γ(A) | γ(B) γ(K :: A) = γ(A)
We can now present the relationship between causal information in causal processes and in rhoπ configurations. This relationship takes the form of a bisimulation which we call causal correspondence. Informally, causal correspondence asserts that during execution, a causal process and its "corresponding" rhoπ process ascribe the same causes to the same sub-processes.

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

For causal processes, a causal barb K :: a corresponds to the ability to communicate on a channel a due to causes in K. More precisely: Definition 7 (Causal barbs for causal processes). A choπ causal process A has a causal barb K :: a, noted A ↓ K::a , if A ≡ νc. K :: a P | B, with a ∈ c, for some c, P, B. A choπ causal process A has a causal barb K :: a, noted A ↓ K::a , if A ↓ K::a implies A ≡ νc. K :: a(X) ⊲ P | B, with a ∈ c, for some c, P, B.

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

Definition 8 (Causal dependence).

Let M be a configuration and let T M be the set of tags occurring in M . The binary relation > M on T M is defined as the smallest relation satisfying the following clauses:

• k > M h i , h • k; • κ ′ > M k if κ ′ occurs in µ for some memory [µ; k] that occurs in M .
The causal dependence relation :> M is the reflexive and transitive closure of > M .

κ :> M κ ′ reads "κ is a causal antecedent of κ ′ according to M ". We also write κ <: M κ ′ for κ ′ :> M κ. When configuration M is clear from the context, we write κ :> κ ′ for κ :> M κ ′ , and κ <: κ ′ for κ <: M κ ′ . When K is a set of keys, we write κ <: K if for all h ∈ K, we have κ <: h. We denote by fk(M ) the set of free keys of a configuration M . Note that fk(M ) ⊆ fn(M ).

Definition 9 (Causal barbs for configurations).

A rhoπ configuration M has a causal barb K :: a where K ⊆ fk(M ), noted M ↓ K::a , if and only if M ≡ ν ũ. (κ : a P ) | N , with a ∈ ũ and κ <: K. Likewise, M ↓ K::a where K ∈ fk(M ), if and only if M ≡ ν ũ. (κ : a(X) ⊲ P ) | N , with a ∈ ũ and κ <: K.

Definition 10 (Causal correspondence). A relation R is a causal correspondence between choπ causal processes and rhoπ configurations if the following condition holds

: if A, M ∈ R, then • γ(A) ≡ γ(M ) and fk(A) = fk(M ) • if A ↓ K::α , then M ↓ K::α • if A → B, then there exists N such that M → N and B, N ∈ R • if M ↓ K::α and (M ↓ K ′ ::α =⇒ K ′ ⊆ K), then A ↓ K::α • if M → N , then there exists B such that A → B and B, N ∈ R
A causal process A and a configuration M are said to be in causal correspondence if there exists a causal correspondence R such that A, M ∈ R.

Consider now a rhoπ configuration M with the following constraints: M has no bound key and no memory, and all tags in M are simple keys, i.e. if M ≡ ν ũ. i∈I k i : τ i , where each τ i is of the form a P or a(X) ⊲ P for some a, P , with k i ∈ K and ũ∩K = ∅. We will call initial such a configuration. An initial configuration M can easily be seen as a choπ causal process if we apply to it the syntactic transformation χ that replaces configurations k : P in M , with causal processes {k} :: P , i.e. that is defined inductively as follows:

χ(0) = 0 χ(k : P ) = {k} :: P χ(νa. M ) = νa. χ(M ) χ(M | N ) = χ(M ) | χ(N )
We can now state our causal correspondence theorem:

Theorem 2. Let M be an initial configuration. Then χ(M ) and M are in causal correspondence.

Proof. The proof consists in showing that the relation R, defined below, is a causal correspondence. We first define the predicate corr that relates choπ closed causal processes with rhoπ closed configurations: we have corr(A, M ) if the following conditions hold:

• A ≡ νc. i∈I K i :: τ i • M ≡ νc, h. ( i∈I κ i : τ i ) | N
• for each i ∈ I, τ i is of the form a i P i or a i (X) ⊲ P i for some a i , P i

• for each i∈ I, κ i <: M K i and for all k, κ i <:

M k =⇒ k ∈ K i • γ(N ) ≡ 0 and h ⊂ K The relation R is defined as: R = { U, V | A → n U, M → n V, M initial, A = χ(M ), corr(U, V )} where A → n U (resp. M → n N ) denotes the fact that A reduces to U (resp. M reduces to N ) in n steps.
If M is initial, we have χ(M ), M ∈ R by construction. We now check the different clauses of causal correspondence.

Let U, V ∈ R. Since corr(U, V ) we can write

U ≡ νc. i∈I K i :: τ i V ≡ νc, h. i∈I κ i : τ i | N
with γ(N ) = 0 and for all i ∈ I, κ i <: M K i .

• Since γ(N ) = 0, we have γ(U ) ≡ νc. i∈I τ i ≡ γ(V ). Now by induction on the length n of the derivations A → n U and M → n V , it is easy to check that fk(U ) = fk(A) and fk(M ) = fk(V ). Since A = χ(M ), we have fk(A) = fk(M ) and thus fk(U ) = fk(V ).

• Assume that U ↓ K::α , then we must have U ↓ K i ::a i or U ↓ K i ::a i for some i ∈ I. Since corr(U, V ), we must then have

V ↓ κ i :a i or V ↓ κ i :a i with κ i <: V K i .
• Assume that U → U ′ . Then, we must have j, l ∈ I such that a j = a l and τ j = a P , τ l = a(X) ⊲ Q and

U ′ ≡ νc. (K j ∪ K l :: Q{ P / X }) | i∈I\{j,l} K i :: τ i
for some P, Q. But then we have

V → νc, h, k. k : Q{ P / X } | ( i∈I\{j,l} κ i : τ i ) | [m; k] | N = V ′ where m = κ j : a P | κ l : a(X) ⊲ Q. We have k <: V ′ κ i and k <: V ′ κ l , thus k <: V ′ K j ∪ K l .
We check that U ′ , V ′ ∈ R, which amounts to proving that corr(U ′ , V ′ ). Assume, without loss of generality, that Q ≡ ν ẽ. i∈J τ i , with J ∩ I = ∅. Then

U ′ ≡ νc, ẽ.
i∈(I∪J)\{j,l}

K i :: τ i V ′ ≡ νc, ẽ, h, k, l. i∈(I∪J)\{j,l} κ i : τ i | [m; k] | N where l = {l i | i ∈ J} and, for all i ∈ J, K i = K j ∪K l , κ i = l i , l •k. We have γ([m; k] | N ) ≡ 0,
and for all i ∈ J κ i <: V ′ k, and thus κ i <: V ′ K i . Therefore U ′ , V ′ have the required form and thus corr(U ′ , V ′ ).

• Assume that V ↓ K::α , with K maximal, then we must have

V ↓ K i ::a i or V ↓ K i ::a i for some i ∈ I and K = K i . Since corr(U, V ), we must then have U ↓ K i :a i or V ↓ K i :a i .
• Assume that V → V ′ . Then, we must have j, l ∈ I such that a j = a l and τ j = a P , τ l = a(X) ⊲ Q,

V ′ ≡ νc, h, k. k : Q{ P / X } | ( i∈I\{j,l} κ i : τ i ) | [m; k] | N where m = κ j : a P | κ j : a(X) ⊲ Q. Assume that Q ≡ ν ẽ. i∈J τ i , with J ∩ I = ∅. Then V ′ ≡ νc, ẽ, h, k, l.
i∈(I∪J)\{j,l}

κ i : τ i | [m; k] | N
where l = {l i | i ∈ J} and for all i ∈ J, κ i = l i , l • k. Notice that we have for all i ∈ J κ i <: V ′ k and thus κ i <:

V ′ K j ∪ K l . Now, we have U → νc. (K j ∪ K l :: Q{ P / X }) | i∈I\{j,l} K i :: τ i = U ′
Setting for all i ∈ J K i = K j ∪ K l , we obtain

U ′ ≡ νc, ẽ.
i∈(I∪J)\{j,l} K i :: τ i and thus corr(U ′ , V ′ ), as required.

Encoding rhoπ in HOπ

This section shows that rhoπ can be encoded in a variant of HOπ, which we call HOπ + , that allows the use of bi-adic channels, join patterns [START_REF] Fournet | The reflexive chemical abstract machine and the join-calculus[END_REF][START_REF] Fournet | The join calculus: A language for distributed mobile programming[END_REF], sub-addressing, abstractions and applications. This particular variant was chosen for convenience, because it simplifies our encoding. All HOπ + constructs are well understood in terms of expressive power with respect to HOπ (see [START_REF] Milner | Functions as processes[END_REF][START_REF] Sangiorgi | From lambda to pi; or, rediscovering continuations[END_REF] for abstractions in π-calculus).

The encoding presented here is slightly different from the one presented in [START_REF] Lanese | Reversing higher-order pi[END_REF], in order to obtain a finer correspondence result. Indeed [START_REF] Lanese | Reversing higher-order pi[END_REF] shows that a rhoπ configuration and its translation are weak barbed bisimilar. Such result allows us to encode reversibility in an already existing calculus, without introducing any new ad-hoc primitive. Even if the result is quite surprising, because of the coarseness of weak barbed bisimulation (as emerged in Section 2.5), it does not establish a strong enough correspondence between rhoπ and its encoding. Therefore, here we base our results on a stronger equivalence, weak bf barbed bisimulation, able to distinguish forward reductions from backward ones. The remainder of the section is organized as follows: first we introduce the syntax and the semantics of HOπ + , then we introduce our encoding and show that a rhoπ consistent configuration M and its translation in HOπ + are weak bf barbed bisimilar. To ease the reading of the section, some proofs and auxiliary results are reported in Appendix C.

P, Q ::= 0 | X | νu. P | (P | Q) | u F, v | J ⊲ P | (F V ) F ::= (u)P | (X)P | (u)F | (X)F V ::= u | F J ::= u(X, v) | u(X, \v) | J | J u, v ∈ I

HOπ +

The syntax of HOπ + is given in Figure 5. Channels in HOπ + are bi-abic in the sense that they carry pairs of the form F, v, that is an abstraction and a name; a trigger can receive a message on a given channel, or on a given channel provided that the received message carries some given name (subaddressing). Actually triggers use Join patterns, i.e. they allow to specify a set of messages that are read atomically. Join patterns are linear. HOπ + supports abstractions over names (u)P and over process variables (X)P , and applications (P V ), where a value V can be a name or an abstraction. We take the set of names of HOπ + to be the set I ∪{⋆} where I is the set of rhoπ identifiers (I = N ∪ K). Thus both rhoπ names and rhoπ keys are names in HOπ + . The set of (process) variables of HOπ + is taken to coincide with the set V of variables of rhoπ. Moreover we let B to range over processes P and functions F .

The structural congruence for HOπ + , denoted by ≡, obeys the same rules as those of rhoπ processes (see Figure 2), except for the rules E.TagN and E.TagP, which are specific to rhoπ. Evaluation contexts in HOπ + , as in HOπ, are given by the following grammar:

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

(Red) match(F i , X i ) = θ ′ i match(v i , ψ i ) = θ i n i=1 u i F i , v i | ( n i=1 u i (X i , ψ i ) ⊲ P ) → P θ ′ 1 . . . θ ′ n θ 1 . . . θ n (App) match(V, ψ) = θ ((ψ)B V ) → Bθ
match(u, v) = { u / v } match(u, \u) = { u / u } match(F, X) = { F / X }
Note that an escaped name \u will match just with name u. Rule Red is a generalization (in the sense of join patterns) of the usual communication rule for HOπ. If there are enough messages (left-hand side of the reduction in the conclusion) satisfying a certain input process, then they are consumed at once and the continuation of the input process is triggered with the necessary substitutions. Rule App mimics the well known β-reduction of the λ-calculus [START_REF] Barendregt | The Lambda Calculus -Its Syntax and Semantics[END_REF]. We use ⇒ to denote the reflexive and transitive closure of →.

Remark 9. Even if HOπ + allows using arbitrary join patterns, our encoding will use just binary join patterns.

Conventions. In writing HOπ + terms, u v abbreviates u (X)0, v , u abbreviates u (X)0, ⋆ and u F abbreviates u F, ⋆ . Likewise, a(u) ⊲ P abbreviates a(X, u) ⊲ P , where X ∈ fv(P ), a ⊲ P abbreviates a(X, ⋆) ⊲ P , where X ∈ fv(P ), and a(X) ⊲ P abbreviates a(X, ⋆) ⊲ P . We adopt the usual conventions for writing applications and abstractions:

(F V 1 . . . V n ) stands for (((F V 1 ) . . .) V n ), and (X 1 . . . X n )F stands for (X 1 ) . . . (X n )F .
When there is no potential ambiguity, we often write F V for (F V ). When defining HOπ + processes, we freely use recursive definitions for these can be encoded using e.g. the Turing fixed point combinator Θ defined as Θ = (A A), where A = (X F )(F (X X F )) (cf. [35, p. 132]).

In the rest of the paper we denote by P HOπ + the set of HOπ + processes, by C rhoπ the set of rhoπ configurations and by P rhoπ the set of rhoπ processes.

rhoπ encoding

The encoding • : P rhoπ → P HOπ + of processes of rhoπ in HOπ + is defined inductively in Figure 7. It extends to an encoding • : C rhoπ → P HOπ + of configurations of rhoπ in HOπ + as given in Figure 8 (the encoding for 0 in Figure 8 is the encoding for the null configuration). The two main ideas behind the encoding are given now. First, a tagged process l : P is interpreted as a process equipped with a special channel l (sometimes we will refer to it as its key channel ) on which to report that it has successfully rolled back. This intuition leads to the encoding of a rhoπ process as an abstraction which takes this reporting channel l (its own key) as a parameter. Second, each rhoπ process translation generates also the process killer, that is a process in charge of rolling it back. We have three kinds of such processes: KillM, KillT and KillP representing respectively the killer of a message, of a trigger and of a parallel composition of processes.

Let us now describe the encoding of configurations given in Figure 8. A null configuration 0 is encoded as the null HOπ + process 0. The parallel and the restriction operator are mapped to the corresponding operators of HOπ + . There are two ways of encoding a tagged process κ : P depending on the kind of the tag. If the tag is a key, then the translation is the application of the encoding of P to the name k, that is P k. If the tag is complex, of the form h i , h • k, then the translation is the application of the translation of P to the name h i , in parallel with the killer of the complex tag. Since we want to generate at once a tree of killer processes able to revert an entire parallel composition made of n elements, with n being the size of h, we opt for the first element of the sequence to generate it. Said otherwise, a killer of a complex tag h i , h • k is the null process if i = 1, otherwise it is a parallel composition of killer processes able to rollback all the branches in which the key k has been split. Hence, the killer of the complex tag h 1 , h • k is in charge of mimicking the behavior of the rhoπ structural rule E.TagP (see Figure 2 in Section 2.3) used (from right to left) to build back a tagged parallel composition from a parallel composition of related threads. The encoding of a memory will be explained later. Before commenting the encoding of rhoπ processes in more detail, let us introduce the Rew process, and the idea behind it. Killer processes allow a process to rollback, but we have to give also the possibility to undo a rollback decision. This is due to the fact that at any moment each process should be given both the possibility to go forward and to go backward. Assume this is not the case, and consider a parallel composition of processes. If one branch decides (spontaneously) to rollback (by interacting with its killer process) while the other branches do not, then the rolled-back process would be stuck unless we add the possibility to undo its rollback decision. This is the purpose of a process of the form (Rew l), whose behavior is to read an abstraction carried in a message on the key channel l and then to re-instantiate the abstraction with the same key. Naturally this makes the encoding divergent, but divergence is quite natural in a reversible calculus. In fact, each rhoπ configuration which is not stuck can diverge by continuously doing and Let us now comment on the encoding of rhoπ processes in Figure 7. As we already said, all the translations of rhoπ processes are abstractions over a channel, and this channel is the tag of the process (or part of it in the case of a complex tag). The zero process 0 is translated as a message on the abstracted channel along with a Rew process. This translation, as well as translations of other processes, is by itself diverging. Consider the encoding of the rhoπ process l : 0:

0 = Nil X = X a P = (l)(Msg a P l) νa. P = (l)νa. P l P | Q = (l)(Par P Q l) if P, Q ≡ 0 P | 0 = P a(X) ⊲ P = (l)(Trig ((X c)c P ) a l) 0 | P = P Nil = (l)(l Nil | (Rew l)) Msg = (a X l)a X, l | (KillM a l) KillM = (a l)(a(X, \l) ⊲ l (h)Msg a X h | Rew l) Par = (X Y l)νh, k. X h | Y k | (KillP h k l) KillP = (h k l)(h(W ) | k(Z) ⊲ l (l)Par W Z l | Rew l) Trig = (Y a l)νt. t | (a(X, h) | t ⊲ f νk, c. (Y X c) | (c(Z) ⊲ (Z k)) | (Mem Y a X h k l)) | (KillT Y t l a) KillT = (Y t l a)(t ⊲ l (h)Trig Y a h | Rew l) Mem = ( Y a X h k l)k(Z) ⊲ b (Msg a X h) | (Trig Y a l) Rew = (l)(l(Z) ⊲ Z l)
0 = 0 M | N = M | N νu. M = νu. M k : P = ( P k) h i , h • k : P = ( P h i ) | Kill h i , h •k [κ 1 : a P | κ 2 : a(X) ⊲ Q; k] = (Mem ((X c)c Q ) a P κ 1 k κ 2 ) | Kill κ 1 | Kill κ 2 k = k h i , h • k = h i Kill h 1 , h •k = ν l. (KillP h 1 l 1 k) | n-2 i=2 (KillP h i l i l i-1 ) | (KillP h n-1 h n l n-2 ) Kill κ = 0 otherwise
l Nil | (Rew l) → l Nil | l(Z) ⊲ (Z l) → (Nil l) → l Nil | (Rew l)
Divergence here could be avoided by removing the Rew process from the translation of 0, and considering it as just a message on its abstracted channel. That is:

0 = (l)l Nil
We stick however to the first translation to preserve the symmetry with the translations of the other primitive processes (messages and triggers), since this simplifies the statement of some invariants of our encoding, and since, as already said, divergence here is not a relevant issue. The translation of a message k : a P after a few applications becomes a process of the form:

a P , k | (KillM a k)
consisting in a message on channel a carrying a pair (here we can see why we use bi-adic channels) in parallel with its killer process. The message carries the translation of the original message content P along with the abstracted channel. The abstracted channel k is needed to ensure that the message will be rolled back only by its own KillM. Indeed, the process (KillM a k) consumes a message on the channel a only if it carries the name k. This is why the KillM process is an abstraction over two channels, and explains the need of sub-addressing. The translation of a parallel composition is quite straightforward: two new key channels are created and given to the translations of the two subprocesses. A KillP process will await on these two channels the rollback of the two sub-processes, in order to notify its rollback by building back the entire parallel process into its key channel. This is why we use binary join patterns (the translation of triggers uses join patterns too).

The translation of a trigger l : a(X) ⊲ Q is a process of the form:

νt. t | (a(X, h) | t ⊲ f νk, c. (Y X c) | (c(Z) ⊲ (Z k)) | (Mem Y a X h k l)) | (KillT Y t l a) with Y = ((X c)c Q ).
Here, a token t is used as a lock. In this way either the trigger itself or its killer can acquire this lock and then execute by letting the other process blocked forever. Since all the messages on channel a ∈ N are translated into bi-adic messages, triggers are translated in order to read such messages. The continuation of a translated trigger mimics exactly the rhoπ forward rule: it creates a new key channel k, it substitutes the process variable X with the message content (which is an abstraction) in the trigger continuation. This substitution is mimicked by the application (Y X c). For example, assume that after a communication we obtain the following process k : Q{ P / X } where Q is the body of the trigger. Then this substitution is mimicked in our encoding by the following application:

((X d)d Q ) P c → c Q { P / X }
The trigger continuation, resulting from the substitution, is then applied to the new key channel as follows:

c Q { P / X } | c(Z) ⊲ Z k → ( Q { P / X })k
obtaining the process corresponding to the translation of k : Q{ P / X }. A memory process Mem is also created. The Mem process mimics exactly the backward rule of rhoπ: it awaits the rollback of its continuation (a message on the key channel k that the memory bears) and then it releases again the translations of the original rhoπ message and trigger who gave rise to the communication (and to the memory).

The next sections are devoted to prove that the encoding is faithful, i.e. that it preserves the semantics of the original rhoπ configuration. More precisely, we will prove the following theorem.

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

• ≈ νk. k : P .
Before proving the theorem we give a brief outline of our proof strategy.

Proof outline. Since the relation • ≈ (see Definition 4) distinguishes three kinds of reductions, forward, backward and administrative, we first divide all the reductions induced by the encoding into these three kinds. Then we give a notion of normal form on HOπ + processes, whose intent is to consider processes equivalent up to applications in active contexts. Then we characterize the garbage processes generated by the encoding, because of the machinery added to simulate reversibility, with the function addG, and we define a new congruence ≡ Ex to ensure that translations of structurally congruent rhoπ configurations are structurally congruent. We then study the interplay between reduction in normal form and structural congruence ≡ Ex , and between reduction in normal form and administrative steps. We then show that a rhoπ reduction can be matched by the encoding, and that ≡ Ex is itself a weak bf barbed bisimulation. We also prove that the garbage produced by the encoding (characterized by addG) does not induce unwanted behaviors. That is, if P is a process derived from the encoding, then P and (any process in) addG(P ) are weakly bf barbed bisimilar. We then show that all the reductions of the encoding are matched by rhoπ and finally compose all the obtained results to prove our faithfulness theorem.

Auxiliary relations

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

To give to the reduction system a backward and forward structure we partition the reductions of the translation into forward, backward and administrative. The basic idea is that administrative reductions can be used both as forward and as backward. Remember that in HOπ + we have two kinds of reductions: applications and communications. All applications are administrative reductions. Communications can be either administrative, forward or backward according to the involved trigger. To distinguish the different triggers, we decorate them with labels. This will not change the operational semantics of the calculus.

A labelled trigger is a trigger of the form J ⊲ b P or J ⊲ f P . Triggers like the first one will be referred to as backward while triggers like the second one will be referred to as forward. From now on we will denote with R ? the reflexive closure of a relation R, and with R * its reflexive and transitive closure. We now define the two reduction relations ։ and on HOπ + processes.

Definition 11 (Forward and backward HOπ + reductions). Let ։ be a reduction involving a forward trigger and a reduction involving a backward trigger. Moreover let ֒→ be the reduction relation composed by applications and communications involving non labelled triggers. We define ⇒ f =֒→ * ։֒→ * and ⇒ b =֒→ * ֒→ * . Definition 12 (Administrative communications). Let → be the reduction relation involving communications due to non labelled triggers.

All the applications in the encoding have the form below.

Definition 13 (Applications in the encoding). Let ⇁ be the least evaluation closed relation including the pairs:

{ (h)P v, P { v / h } | P ∈ P} ∪ {(X)P Q , P { Q / X } | P, Q ∈ P}.
From the definitions above it is clear that →⊆֒→.

One cannot simply prove that given a (consistent) configuration M , if M ։ M ′ then M ⇒ f M ′ , and similarly for backward reductions. In fact, this does not hold, since the translated processes produce some garbage (in terms of additional processes) due to the execution, and since structural congruent rhoπ processes do not always have structural congruent translations. Thus we need some auxiliary machinery.

First, we introduce a notion of well formed process, a HOπ + process obtained by letting a process of the form R l compute. Definition 14 (Well formed process). A HOπ + process P is well formed if there is a rhoπ process R such that R l ⇒ P .

Then, we characterize the garbage described above by defining a function addG(P ) allowing to add arbitrary garbage to a HOπ + process P .

Definition 15. Let P be a HOπ + process such that P ≡ νã. P ′ . Then,

addG(P ) = {P G | P G ≡ νã. (P ′ | ν b. Q)},
where Q is a parallel composition (possibly empty) of processes of one of the forms below, or obtained from them by applications:

Rew l

KillM a l νc, t. (KillT ((X)c P ) t l a) νt. (a(X, k)|t ⊲ S)

The last two closures of the addG function characterize the garbage processes produced by the consumption of the token t in the translation of the trigger process. Both processes are blocked (but for an application of the first one), since the name t is restricted and the token t has been consumed. To better understand how the token t is used and how garbage can be created, let us consider the following reductions, where a trigger begins a rollback and then undoes it, producing some garbage:

k : a(X) ⊲ 0 = a(X) ⊲ 0 k = ((h)Trig Y a h) k → (Trig Y a k) ⇒ νt. t | (a(X, \h)|t ⊲ Q) | (t ⊲ k (h)Trig Y a h | (Rew k)) → νt. (a(X, \h)|t ⊲ Q) | k (h)Trig Y a h | (Rew k) → νt. (a(X, \h)|t ⊲ Q) | k (h)Trig Y a h | (k(Z) ⊲ Z k) → νt. (a(X, \h)|t ⊲ Q) | ((h)Trig Y a h) k ∈ addG( k : a(X) ⊲ 0 ) where Q = νl, c. (Y X c) | (c(Z) ⊲ Z l) | (Mem Y a X h l k) and Y = (X c)c 0 .
The token allows us to avoid to use primitives such as passivation (see [START_REF] Schmitt | The M-calculus: a higher-order distributed process calculus[END_REF][START_REF] Lenglet | Normal bisimulations in calculi with passivation[END_REF]) or mixed choice to kill input processes. We now define a notion of normal form for processes, corresponding to processes where all the enabled applications have been executed. Thus, a process in normal form has no enabled applications.

Definition 16 (Normal form). Let nf(.) be a function from P HOπ + to P HOπ + defined as follows:

nf(νu. P ) = νu. nf(P ) nf(P | Q) = nf(P ) | nf(Q) nf(a P ) = a P nf(a(X) ⊲ P ) = a(X) ⊲ P nf((X)P Q) = nf(P { Q / X }) nf((h)P l) = nf(P { l / h }) nf(0) = 0
Since reduction to normal form applies only applications in active context, the reduction to normal form is the identity on triggers and messages.

We extend the congruence ≡ on HOπ + processes to match the effect of rhoπ structural congruence after the translation, in order to show that congruent rhoπ processes are translated into congruent HOπ + processes. Definition 17. Let ≡ Ax be the smallest congruence on HOπ + processes satisfying the rules for structural congruence ≡ plus the axioms below.

(Ax.C) KillP l h k ≡ Ax KillP h l k (Ax.A) νl ′ . (KillP l 1 l 2 l ′ ) | (KillP l ′ l 3 l) ≡ Ax νl ′ . (KillP l 1 l ′ l) | (KillP l 2 l 3 l ′ ) (Ax.P) P, Q closed l 1 P | l 2 Q | KillP l 1 l 2 l ≡ Ax l (h)P ar P Q h | Rew l (Ax.Unfold) P l ≡ Ax ν ũ. l Q | (Rew l) with P ≡ ν ũ. Q (Ax.Adm) νc. (c P | c(Z) ⊲ (Z k)) ≡ Ax P k Definition 18. Let ≡ Ex be the smallest congruence including for each axiom L ≡ Ax R in ≡ Ax both L ≡ Ex R and nf(L) ≡ Ex nf(R).
If a process contains a message on a channel a ∈ N , then the process contains also a corresponding KillM process.

Lemma 17 (KillM Invariant). If P ′ is well formed and P ′ ≡ C[a P , l ] with a ∈ N for some n-ary context C then

P ′ ≡ C ′ [a P , l | S] with S = (KillM a l) or S = (a(X, \l)⊲l (h)Msg a X h | Rew l) for some n-ary context C ′ . Proof. See Appendix C.1.
Function addG(•) does not add new behaviors.

Lemma 18. Let P be a well formed HOπ + process and Q ∈ addG(P ). If nf(Q) ֒→ Q ′ then there exists P ′ such that P ֒→ * P ′ with Q ′ ∈ addG(P ′ ).

Proof. See Appendix C.1.

Lemma 19. Let P be a well formed HOπ + process and Q ∈ addG(P ). If nf(Q) ։ Q ′ then there exists P ′ such that P ⇁ * ։ P ′ with Q ′ ∈ addG(P ′ ).

Proof. It is easy to see from the definition of function addG that the added processes cannot enable ։ reductions. Hence the reduction ։ can be done by nf(P ), and it is sufficient to chose P ′ such that P ֒→ * nf(P ) ։ P ′ . Lemma 20. Let P be a well formed HOπ + process and Q ∈ addG(P ). If nf(Q) Q ′ then there exists P ′ such that P ⇁ * P ′ with Q ′ ∈ addG(P ′ ).

Proof. Similar to the one of Lemma 19

Operational correspondance

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

We start by proving a few basic properties of the translation. The encoding is well-behaved w.r.t. substitutions:

Lemma 21 (Substitution). For each rhoπ process P, Q:

P { Q / X } = P { Q / X } .
Proof. By induction on the structure of P .

Names corresponding to keys in K are always bound.

Lemma 22. If νk. k : P ⇒ P ′ then fn(P ′ ) ∩ K = ∅.

Proof. By induction on the number of steps in ⇒.

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

Lemma 23. For each closed rhoπ process P , P k ֒→ * ν ũ. k Q | Rew k | S with k ∈ ũ, S = R i , R i = Rew k i or R i = νt. (a(X, h)|t⊲R) and P ≡ ν ũ. Q. Proof. See Appendix C.2.
The encoding never generates two messages on the same key channel, never generates two KillP processes waiting for the same rollbacks or never generates a KillP and a Mem waiting for the same rollback signal.

Lemma 24. For any rhoπ process R, if R l ⇒ P then the following conditions hold:

1. P ≡ C[l 1 P 1 | l 1 P 2 ], with l 1 ∈ K. 2. P ≡ C[(KillP l 1 l 2 l 3 ) | (KillP l 4 l 5 l 6 )], with l 1 , l 2 , l 3 , l 4 , l 5 , l 6 ∈ K and {l 1 , l 2 } ∩ {l 4 , l 5 } = ∅ or l 3 = l 6 . 3. P ≡ C[(KillP l 1 l 2 l) | (Mem P a Q h l 3 k)], with l, l 1 , l 2 , l 3 , h, k ∈ K and l 1 = l 3 or l 2 = l 3 . Proof. See Appendix C.2.
Processes congruent according to ≡ Ex have the same weak reductions (up to ≡ Ex ).

Lemma 25. If nf(P 1 ) ≡ Ex nf(P 2 ) and nf(P 1 ) → P ′ 1 then nf(P 2 ) ⇒ nf(P ′ 2 ) with nf(P ′′ 1 ) ≡ Ex nf(P ′ 2 ) and

P ′′ 1 ∈ addG(P ′ 1 ). Furthermore, if → is forward then ⇒ is ⇒ f , if → is backward then ⇒ is ⇒ b , if → is administrative then ⇒ is ֒→ * .
Proof. By case analysis on the used axiom P ≡ Ex Q and on the structure of nf(P 1 ). The proof is in Appendix C.2.

Two applications can always be swapped.

Lemma 26. For each HOπ + process P , if P ⇁ P 1 and P ⇁ P 2 then there is a HOπ + process P 3 such that P 2 ⇁ P 3 and P 1 ⇁ P 3 .

More in general, applications can be swapped with arbitrary reductions, but they can disappear becuase of the swap.

Reductions and applications commute.

Lemma 27. If P ⇒ P ′ and P ⇁ * P ′′ then P ′ ⇁ * Q and P ′′ ⇒ Q.

Proof. By induction on the length of ⇒ and ⇁ * , showing that if P → ? P ′ and P ⇁ ? P ′′ then P ′′ → ? Q and P ′ ⇁ ? Q.

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

Lemma 28. For any consistent configuration M , if M ⇒ P and P ֒→ * Q then there exist Q ′ and P ′ such that Q ֒→ * Q ′ , P ′ ∈ addG(P ) with nf(P ′ ) ≡ Ex nf(Q ′ ).

Proof. See Appendix C.2.

The next theorem proves a form of behavioral correctness for our encoding, showing that the encoding of a process can mimic the process reductions. Proof. By induction on the derivation of M → N , with a case analysis on the last rule applied.

R.Fw: we have that

M = κ 1 : a P | κ 2 : a(X) ⊲ Q ։ νk. (Q{ P / X } | [κ 1 : a P | κ 2 : a(X) ⊲ Q ; k]) = N
Moreover we have that M = κ 1 : a P | κ 2 : a(X) ⊲ Q . We distinguish four cases, depending on whether κ 1 , κ 2 are complex or not. Let us consider the case

κ 1 = k 1 and κ 2 = k 2 . Assume Y = ((X c)c Q ). Then: nf( M ) = nf((l)(Msg a P l)k 1 ) | nf((l)(Trig Y a l)k 2 ) = νt. a P , k 1 | nf(KillM a k 1 ) | t | (t|a(X, h) ⊲ f νk, c. (Y X c) | c(Z) ⊲ Z k | (Mem Y a X h k k 2 )) | nf(KillT Y t k 1 a) ։ νc, k, t. nf(KillM a k 1 ) | (Y P c) | (c(Z) ⊲ Z k) | (Mem Y a X k 1 k k 2 ) | nf(KillT Y t k 2 a) ⇁ νc, k, t. nf(KillM a k 1 ) | c Q { P / X } | (c(Z) ⊲ Z k) | (Mem Y a X k 1 k k 2 ) | nf(KillT Y t k 2 a) ֒→ νc, k, t. nf(KillM a k 1 ) | ( Q { P / X } k) | (Mem Y a X k 1 k k 2 ) | nf(KillT Y t k 2 a) = R
By using Lemma 21 we have that Q { P / X } = Q{ P / X } , thus:

R = νc, k, t. nf(KillM a k 1 ) | ( Q{ P / X } k) | (Mem Y a X k 1 k k 2 ) | nf(KillT Y t k 2 a)
We can conclude by noting that:

nf(R) = nf(KillM a k 1 ) | nf( N ) | νc, t. nf(KillT Y t k 2 a) Since P ′ = (KillM a k 1 ) | N | νc, t. (KillT Y t k 2 a) ∈ addG( N )
and nf(R) ≡ Ex nf(P ′ ) the thesis follows.

Let us consider the case in which κ 1 = h i , h • k. We have that:

M = (l)(Msg a P l)h i | Kill h i , h •k | (l)(Trig Y a l)k 2
Using the same reductions as above we have that:

nf( M ) ⇒ f νc, k, t. nf(KillM a k 1 ) | nf(Kill h i , h •k ) | Q { P / X } k | (Mem Y a X h i k k 2 ) | nf(KillT Y t k 2 a) = R
and by using Lemma 21 we have that

R = νc, k, t. nf(KillM a h i ) | nf(Kill h i , h •k ) | ( Q{ P / X } k) | (Mem Y a X h i k k 2 ) | nf(KillT Y t k 2 a)
We can conclude by noting that

P ′ = (KillM a h i ) | Kill h i , h •k | ( Q{ P / X } k) | (Mem Y a X h i k k 2 ) | νc, t. (KillT Y t k 2 a) ∈ addG( N ) and nf(R) ≡ Ex nf(P ′ ).
The two other cases are similar.

R.Bw: we have that

M = k : R | [κ 1 : a P | κ 2 : a(X) ⊲ Q ; k] κ 1 : a P | κ 2 : a(X) ⊲ Q = N . Assume that Y = ((X c)c Q ).
Then, by definition of nf(•) we have:

nf( M ) = nf( R k) | nf(Mem Y a P κ 1 k κ 2 ) | nf(Kill κ 1 ) | nf(Kill κ 2 ) = nf( R k) | (k(Z) ⊲ (Msg a P κ 1 ) | (Trig Y a κ 2 )) | Kill κ 1 | Kill κ 2
From Lemma 23 we know that R k ֒→ * ν ũ. k R ′ | nf(S) | Rew k with S a parallel composition of garbage processes and R ≡ ν ũ. R ′ . Thanks to Lemma 27 we have nf Equiv: we have two cases, one for forward reductions and one for backward reductions. We consider the first one, the second being analogous.

( R k) ֒→ * ν ũ. k R ′ | nf(S) | nf(Rew k). Hence: nf( R k) | (k(Z) ⊲ (Msg a P κ 1 ) | (Trig Y a κ 2 )) | nf(Kill κ 1 ) | nf(Kill κ 2 ) ֒→ * ν ũ. k R ′ | nf(S) | nf(Rew k) | (k(Z) ⊲ b (Msg a P κ 1 ) | (Trig Y a κ 2 )) | nf(Kill κ 1 ) | nf(Kill κ 2 ) ν ũ. (Msg a P κ 1 ) | (Trig Y a κ 2 ) | nf(Kill κ 1 ) | nf(Kill κ 2 ) | nf(S) | nf(Rew k) = R We have that P ′ = ν ũ. (Msg a P κ 1 ) | (Trig Y a κ 2 ) | Kill κ 1 | Kill κ 2 | S | Rew k ∈ addG( κ 1 : a P | κ 2 : a(X) ⊲ Q ) and nf(R) ≡ Ex nf(P ′ ) as desired. M ≡ 13 M ′ nf( M ) f ≡ Ex 25 nf( M ′ ) f N ′ ≡ 13 N P ind * nf( N ′ ) ≡ Ex addG nf( N ) addG 15 Q * nf(P ) ≡ Ex nf(R ′ ) ≡ Ex nf(R) nf(Q) ≡ Ex nf(P ′ ) ≡ Ex
We have that M ։ N with hypothesis M ≡ M ′ , M ′ ։ N ′ and N ′ ≡ N . Figure 9 (numbers refers to the used lemmas, ind means that inductive hypothesis is applied and addG that garbage is added) shows the proof schema we use. By inductive hypothesis we have that nf( M ′ ) ⇒ f P with nf(P ) ≡ Ex nf(R ′ ) and R ′ ∈ addG( N ′ ). By Lemma 13, we have that if M ≡ M ′ then nf( M ) ≡ Ex nf( M ′ ), and by Lemma 25 we have that if nf( M ′ ) ⇒ f nf(P ) then nf( M ) ⇒ f nf(Q ′ ) with Q ′ ∈ addG(Q) and with nf(Q) ≡ Ex nf(P ). By inductive hypothesis we have that nf(P ) ≡ Ex nf(R ′ ), but since by hypothesis we had N ′ ≡ N by Lemma 13 we have that nf( N ′ ) ≡ Ex nf( N ) and by Lemma 15 we have that there exists R ∈ addG( N ) such that nf(R ′ ) ≡ Ex nf(R). Thanks to Lemma 15 there exists P ′ ∈ addG(P ) with nf(Q ′ ) ≡ Ex nf(P ′ ), and

R ′′′ ∈ addG(R ′ ) = addG( N ′ ) and R ′′ ∈ addG(R) = addG( N ) such that nf(P ′ ) ≡ Ex nf(R ′′′ ) ≡ Ex nf(R ′′ ).
We can conclude by saying that nf( M ) ⇒ f Q ′ and that nf(Q ′ ) ≡ Ex nf(R ′′ ) with R ′′ ∈ addG( N ), as desired.

Ctx: by simply induction on the structure of the context, noting that the translation of active contexts is isomorphic.

Final proof

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

The first one relies on the result below.

Lemma 33. If nf( M ) ։ P then M ։ M ′ with P ֒→ * P ′ and nf(P

′ ) ≡ nf(Q ′ ) and Q ′ ∈ addG( M ′ ).
Proof. See Appendix C.4.

Lemma 34. Let M be a rhoπ configuration. If M ֒→ * Q ։ Q ′ then there are M ′ , Q ′′ and Q ′′′ such that M ։ M ′ , Q ′ ֒→ * Q ′′ and nf(Q ′′ ) ≡ Ex nf(Q ′′′ ) and Q ′′′ ∈ addG( M ′ ).
Proof. Assume M ֒→ * Q ։ Q ′ . By definition of normal form using Lemma 27 we have that

M ֒→ * Q implies that nf( M ) ֒→ * Q 1 with Q ⇁ * Q 1 . Moreover we have that Q 1 ⇁ * nf(Q 1 ) and that nf( M ) ֒→ * nf(Q 1 ). Since Q ։ Q ′ and Q ⇁ * nf(Q 1 )
by Lemma 27 we have that also

nf(Q 1 ) ։ Q 2 for some Q 2 such that Q ′ ⇁ * Q 2 .
In order to apply Lemma 33 we have to show that also nf( M ) ։ P for some P . We want to show that we can re-arrange the trace nf( M ) ֒→ * nf(Q 1 ) ։ Q 2 in order to obtain a trace of the form nf( M ) ։֒→ * P 2 with Q 2 ∈ addG(P 2 ). Using Lemma 26 we can write nf( M )

֒→ * nf(Q 1 ) as nf( M ) →⇁ * nf(R 1 ) →⇁ * . . . →⇁ * nf(R n ) →⇁ * nf(Q 1 ).
We now proceed by induction on the length of this trace, showing that we can either remove reductions or move them after the forward reduction nf(Q 1 ) ։ Q 2 . The base case (no auxiliary reductions) is trivial. For the inductive case we have a case analysis on the last reduction →.

Internal reduction in a trigger: this case never happens. In fact, by inspecting the encoding, one can see that such a reduction is enabled only after a ։ reduction takes place.

Reduction due to a Rew process: a Rew process consumes a message on a key channel, and this kind of message is not present in nf( M ). Thus, back in the trace there exists a → reduction due to a killer process producing it. Let us select the nearest such →. Since this is the nearest one, there are no intermediate reductions that consume the same message. Hence we can move the killer reduction forward in order to be adjacent to the Rew one, and we can then eliminate both the reductions obtaining a shorter trace. Since garbage may be produced by this pair of reductions, the process obtained by eliminating the two reductions may contain less garbage.

Reduction due to a killer process: the → reduction can be moved after the ։ reduction since it does not remove processes that contribute to the ։ reduction, and we obtain again a shorter trace.

Since nf( M ) ֒→ * nf(Q 1 ) ։ Q 2 implies nf( M ) ։ P ֒→ * P 2 for some P we can apply Lemma 33 and we have that M ։ M ′ and P ֒→ * P ′ with nf(P ′ ) ≡ Ex nf(P ′′′ ) and P ′′′ ∈ addG( M ′ ). By using Lemma 28 there exists Q 3 such that P 2 ֒→ * Q 3 with nf(P ) ≡ Ex nf(P 3 ) and P 3 ∈ addG(Q 3 ). Since P ֒→ * P ′ we have that nf(P ) ֒→ * nf(P ′ ) and from Proposition 1 we have that nf(P 3 ) ֒→ * Q 4 ≡ Ex nf(P ′ ). By definition of addG and by transitivity we have that

Q ′ ֒→ * Q ′′ with Q ′′ ∈ addG(Q 4 ) and Q 4 ≡ Ex nf(P ′′′ ) and P ′′′ ∈ addG( M ′ ). Then Q ′′ ≡ Ex nf(Q ′′′ ) for a Q ′′′ ∈ addG( M ′
) by adding further garbage. This concludes the proof.

Lemma 35. Let M be a rhoπ configuration. If M ֒→ * Q Q ′ then there exists M ′ , Q ′′ and Q ′′′ such that M M ′ , Q ′ ֒→ * Q ′′ and nf(Q ′′ ) ≡ Ex nf(Q ′′′ ) and Q ′′′ ∈ addG( M ′ ).
Proof. We have that Q Q ′ and by applying Lemma 27 we also have that nf(Q)

Q 1 with Q ′ ⇁ * Q 1 . This implies that nf(Q) ≡ ν ũ. R | nf( Mem Y a P k 1 k k 2 ) | k C with Y = (X c)c P 1 and that Q ′ ≡ ν ũ. R | (Msg a P k 1 ) | (Trig Y a k 2 )
. Since administrative reductions ֒→ do not remove memories, the memory needs to be already present both in the configuration M and in its normal form. Since M ֒→ * Q and M ⇁ * nf( M ) by Lemma 27 we also have that nf

( M ) ֒→ * R with Q ⇁ * R, hence M ֒→ * R, moreover since Q Q ′ we also have that R R ′ with Q ′ ⇁ * R ′ .
By definition of and nf( ), the process nf( M ) cannot contain a message on a key channel such as k C . Hence, such a message has been generated by the reductions nf( M ) ֒→ * R. We distinguish two cases: either all the communications in ֒→ * contribute to create such a message, or not. In the first case all the communications are due to killer processes, and we have that nf(

M ) ≡ ν ũ. nf( N ) | nf(Mem Y a P k 1 k k 2 ) | nf( C k) for some N , hence M ≡ ν ũ. N | [k 1 : a P | k 2 : a(X) ⊲ P 1 ; k] | k : C.
Since the administrative reductions just create the message on the channel k, by using Lemma 23 (where S is garbage) we have that nf

( M ) ֒→ * ν ũ. nf( N ) | (k(Z) ⊲ (Msg a P k 1 ) | (Trig Y a k 2 )) | k C | S R ′ with R ′ = ν ũ. nf( N ) | (Msg a P k 1 ) | (Trig Y a k 2 )) | S. On the other side we have that M ν ũ. N | k 1 : a P | k 2 : a(X) ⊲ P 1 = M ′ and we can conclude since nf(R ′ ) = nf(Q ′′′ ) with Q ′′′ ∈ addG( M ′ ).
If there are administrative reductions that do not contribute to the creation of the message on k, we re-arrange the trace nf( M ) ֒→ * R R ′ so to have first all the reductions that contribute to create the message on k, then the reduction and finally all the unrelated reductions. We proceed by induction on the length of the reduction nf( M ) ֒→ * R, with a case analysis on the last reduction that does not contribute to the creation of the message on k. It can be either a communication due to a killer process unrelated to the process with tag k, or a communication due to a Rew l. In the first case the kill does not concerns the process labelled by k nor a parallel composition due to the split of the key k. Thus, it can be moved after the reduction and we can conclude by induction on a shorter trace.

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

At the end, we have a trace of the form nf( M ) ֒→ * R 1 R ′ 1 ֒→ * R ′ with the first trace ֒→ * containing all the administrative reductions related to the creation of the message on k. As in the first case we know that nf

( M ) ֒→ * R 1 R ′ 1 implies that M M ′ with nf(R ′ 1 ) = nf(R ′ 2 ) and R ′ 2 ∈ addG( M ′ ). Moreover we have that R ′ 1 ֒→ * R ′ and that nf(R ′ 1 ) ֒→ * R ′′ with R ′ ⇁ * R ′′ .
By using Lemma 28 we have that there exist

Q ′′ such that R ′′ ֒→ * Q ′′ and nf(Q ′′ ) ≡ Ex nf(Q 3 ) with Q 3 ∈ addG(R ′ 1 ). Since nf(R ′ 1 ) = nf(R ′
2 ) and applications do not change garbage we have that there is

Q ′′′ such that nf(Q 3 ) = nf(Q ′′′ ) and Q ′′′ ∈ addG( M ′ ), as desired.
We can now prove our main result.

Proof of Theorem 3. We prove that the following relation is a weak backward and forward barbed bisimulation:

R = {(M, R) | νk. k : P ⇒ M ∧ nf(R) ≡ Ex nf(Q ′ ) ∧ Q ′ ∈ addG(Q) ∧ M ֒→ * Q}
We have to check the different conditions for weak backward and forward barbed bisimulation. Assume M ↓ a . Note that from the definition of barbs only names in N produce barbs. From Lemma 29 Q ֒→ * ↓ a . Since addG never removes barbs then, thanks to Lemma 31, Q ′ ֒→ * ↓ a . Then also nf(Q ′ ) ֒→ * ↓ a . Thanks to Proposition 1 we have that nf(R) ֒→ * ↓ a and thus also R ֒→ * ↓ a .

Assume now R ↓ a . Thanks to Lemma 22 we have that a ∈ N . We also have that nf(R) ↓ a . Thanks to Proposition 1 nf(Q ′ ) ֒→ * ↓ a and also Q ′ ֒→ * ↓ a . Then Q ֒→ * ↓ a . Finally, thanks to Lemma 30 M ↓ a .

Let us consider reductions. If M ։ M ′ then by Theorem 4 we have nf( M ) ⇒ f P with nf(P ) ≡ Ex nf(P ′ ) and P ′ ∈ addG( M ′ ). By hypothesis we have that M ֒→ * Q, but also nf( M ) ֒→ * nf(Q) and by Lemma 28 we have that there are

Q 1 , Q 2 such that nf(Q) ֒→ * nf(Q 1 ) and nf(Q 1 ) ≡ Ex nf(Q 2 ) with Q 2 ∈ addG(nf( M )). Since nf( M ) ⇒ f P then Q 2 ⇒ f P 1 with P 1 ∈ addG(P ). Since nf(Q 2 ) ≡ Ex nf(Q 1 )
by Lemma 25 we also have that nf(Q 1 ) ⇒ f P 2 and nf(P 2 ) ≡ Ex nf(P 1 ). Since nf(P ) ≡ Ex nf(P ′ ) by transitivity we have that there is P 3 ∈ addG( M ′ ) such that nf(P 2 ) ≡ Ex nf(P 3 ). We can conclude by noting that the pair (M ′ , P 2 ) ∈ R (no administrative reductions are performed from M ′ ). The backward case is similar.

For the other direction, assume R → R ′ . We have a case analysis according to the kind of reduction.

If R ⇁ R ′ then the thesis follows trivially since nf

(R) = nf(R ′ ). If instead R → R ′ then by Lemma 27 nf(R) ֒→ * R ′′ and R ′ ⇁ * R ′′ for some R ′′ . Thanks to Lemma 26 nf(R ′′ ) = nf(R ′ ). Thus we have nf(R) ֒→ * nf(R ′ ). Thanks to Proposition 1 from nf(R) ≡ Ex nf(Q ′ ) we have that there is R 1 such that nf(Q ′ ) ֒→ * R 1 and nf(R ′ ) ≡ Ex R 1 . Thanks to Lemma 18 from nf(Q ′ ) ֒→ * R 1 we have that Q ֒→ * R 2 with R 1 ∈ addG(R 2 ). By using Lemma 14 from nf(R ′ ) ≡ Ex R 1 we obtain nf(R ′ ) ≡ Ex nf(R 1 ). We can conclude since nf(R ′ ) ≡ Ex nf(R 1 ) with R 1 ∈ addG(R 2 ) and M ֒→ * Q ֒→ * R 2 , thus (M, R ′ ) ∈ R.
Assume now R ։ R ′ . By Lemma 27 nf(R) ։ R ′′ and R ′ ⇁ * R ′′ for some R ′′ . Thanks to Lemma 26 nf(R ′′ ) = nf(R ′ ). Thanks to Proposition 1 we have that ≡ Ex is a weak bf barbed bisimulation, and from nf(R)

≡ Ex nf(Q ′ ) we have that there is R 1 such that nf(Q ′ ) ֒→ * ։֒→ * R 1 and R ′′ ≡ Ex R 1 .
From Lemma 14 also nf(R ′′ ) = nf(R ′ ) ≡ Ex nf(R 1 ). From Lemma 18 and Lemma 19 we have that there are R 2 , Q 1 and

Q ′ 1 such that Q ֒→ * Q 1 ։ Q ′ 1 ֒→ * R 2 and nf(R 1 ) = nf(R ′′′ ) with R ′′′ ∈ addG(R 2 )
. By hypothesis, we have that M ֒→ * Q. By Lemma 34 we have that

M ֒→ * Q 1 ։ Q ′ 1 implies that there exist M ′ , Q 2 and Q 3 such that M ։ M ′ and Q ′ 1 ֒→ * Q 2 with nf(Q 2 ) ≡ Ex nf(Q 3 ) and Q 3 ∈ addG( M ′ ).
We can apply Lemma 28 obtaining

Q 4 and Q 5 such that Q 2 ֒→ * Q 4 and nf(Q 4 ) ≡ Ex nf(Q 5 ) with Q 5 ∈ addG(Q ′ 1 ). Since Q ′ 1 ֒→ * R 2 we have that nf(Q 5 ) ֒→ * nf(Q 6 ) with Q 6 ∈ addG(R 2 )
. Note that R ′′′ and Q 6 differ only because of garbage. Since garbage has no impact on the semantics we can consider them equal (this can be formalized more precisely as an up-to technique). Thus nf(Q 6 ) = nf(R 1 ), and since nf(R ′ ) ≡ Ex nf(R 1 ) we also have nf(R ′ ) ≡ Ex nf(Q 6 ). We want to show that the pair

(M ′ , R ′ ) ∈ R. We have that Q 2 ֒→ * Q 4 but also nf(Q 2 ) ֒→ * nf(Q 4 ) and since nf(Q 3 ) ≡ Ex nf(Q 2 ) and ≡ Ex is a weak bf barbed bisimulation there exists R 3 such that nf(Q 3 ) ֒→ * R 3 with R 3 ≡ Ex nf(Q 4 ).
Hence by using Lemma 18 we also have that nf( M ′ ) ֒→ * R 4 with R 3 ∈ addG(R 4 ). We have nf(Q 4 ) ≡ Ex nf(Q 5 ) and nf(Q 5 ) ֒→ * nf(Q 6 ). Since ≡ Ex is a weak bf barbed bisimulation there exists R 5 such that nf(Q 4 ) ֒→ * R 5 with R 5 ≡ Ex nf(Q 6 ). Using the same reasoning we have that R 3 ֒→ * R 6 with R 6 ≡ Ex R 5 . Since R 3 ∈ addG(R 4 ) we have that R 4 ֒→ * R 7 with R 6 ∈ addG(R 7 ). Using Lemma 15 and Lemma 14 we have that nf(R 5 ) ≡ Ex nf(Q 6 ) and nf(R 6 ) ≡ Ex nf(R 5 ). To conclude we can note that

M ′ ⇁ * nf( M ′ ) ֒→ * R 4 ֒→ * R 7 with R 6 ∈ addG(R 7 ) and nf(R 6 ) ≡ Ex nf(Q 6 ) ≡ Ex nf(R ′ ). This implies that (M ′ , R ′ ) ∈ R, as desired.
If R R ′ we can use the same reasoning of the ։ case by using Lemma 35 and Lemma 20 instead of Lemma 34 and Lemma 19.

Related work

Research into reversible computing has already a long history, that originates in the 1960s. Bennett provides an account [START_REF] Bennett | Notes on the history of reversible computation[END_REF] of early research on the subject. A full review of works on reversible computing, and the closely related subjects of program inversion (see, e.g., [START_REF] Abramov | Principles of inverse computation and the universal resolving algorithm[END_REF] and the references therein) and bidirectional transformation and languages (see, e.g., [START_REF] Czarnecki | Bidirectional transformations: A cross-discipline perspective[END_REF][START_REF] Foster | Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem[END_REF] and the references therein), is out of the scope of this paper but we can highlight works related to our three main contributions: (i) reversible languages and models, (ii) causal semantics and back and forth bisimulation, (iii) translating between reversible and irreversible computations.

Reversible languages and models. The notion of reversible Turing machine seems to date back at least to Lecerf in the early 60s [START_REF] Lecerf | Machines de turing réversibles. Insolubilité récursive en n ∈ n de l'équation n = θ n , où θ est un "isomorphisme de codes[END_REF], who provides an early encoding of irreversible Turing machines into reversible ones, rediscovered by Bennett in [START_REF] Bennett | Logical reversibility of computation[END_REF]. For a recent survey of reversible Turing machines, their relation to reversible boolean logic, and various reversible models of computation, see [START_REF] Morita | Reversible computing and cellular automata -a survey[END_REF].

Several works have tackled the problem of adding reversibility to sequential programming languages or to sequential abstract machines. Early work focused on reversible execution [START_REF] Zelkowitz | Reversible execution[END_REF] and adding undo capabilities to programming languages. Leeman [START_REF] Leeman | A formal approach to undo operations in programming languages[END_REF] provides an early survey as well as a general framework for adding an undo capability to a sequential programming language. Computational history is saved by means of undo-lists, storing previous states of the execution. Primitives dealing with undo-lists are formalized, and different undo operators can be defined by composing them. A way to map compositionally high-level functional programs into a certain kind of reversible automata is given by Abramsky in [START_REF] Abramsky | A structural approach to reversible computation[END_REF]. In [START_REF] Danos | Reversible, irreversible and optimal lambdamachines[END_REF], Danos and Regnier give a compositional translation of the λ-calculus into a form of reversible abstract machine called Interaction Abstract Machine (IAM). Other reversible abstract machines for sequential programming such as the SEMCD machine [START_REF] Kluge | A reversible se(m)cd machine[END_REF] and the Reversible Virtual Machine (RVM) [START_REF] Stoddart | A virtual machine for supporting reversible probabilistic guarded command languages[END_REF] have been proposed.

Whereas the latter virtual machines keep an explicit track of execution history to reconstruct backward computation, several works study natively reversible sequential programming languages where reversibility is obtained without the need to keep additional information to reconstruct backward computation. These include work on the Janus language whose origin dates back to the early 1980s [START_REF] Yokoyama | A reversible programming language and its invertible self-interpreter[END_REF][START_REF] Yokoyama | Principles of a reversible programming language[END_REF], work on sequential flow charts [START_REF] Yokoyama | Reversible flowchart languages and the structured reversible program theorem[END_REF], the Inv [START_REF] Mu | An injective language for reversible computation[END_REF], RFUN [START_REF] Yokoyama | Towards a reversible functional language[END_REF], and Π [START_REF] James | Information effects[END_REF] reversible functional languages. The key aspect of Janus is that all its constructs, including assignments, are made bijective (and hence reversible), and the language does not allow I/O. The Π language constitutes a reversible core programming model which is claimed to be at the heart of linear logic and quantum computation. It is shown in [START_REF] James | Information effects[END_REF] how to translate a conventional first-order functional language with loops to Π, making explicit the information effects implicit in the irreversible computation of a conventional functional program as manipulations of a global heap and garbage dump.

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

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

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

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

As reported in [START_REF] Bennett | Notes on the history of reversible computation[END_REF], early interest was concerned with the encoding of irreversible computations into a reversible computational model such as a reversible Turing machine or reversible boolean logic. The more recent work by Burhman et al. [START_REF] Buhrman | Time and space bounds for reversible simulation[END_REF] provides a general upper bound on the tradeoff between time and space that suffices for the simulation by a reversible Turing machine of an irreversible one. Together with a later paper by Vitanyi [START_REF] Vitányi | Time, space, and energy in reversible computing[END_REF], it provides a useful survey of prior work on this "reversible simulation" problem. The work by Cardelli and Laneve [START_REF] Cardelli | Reversible structures[END_REF], already mentioned, shows that, by disallowing indistinguishable signals, reversible structures can implement the asynchronous version of RCCS. This is stated by a (weak) completeness theorem but nothing is said about the correctness of the encoding. The survey paper [START_REF] Morita | Reversible computing and cellular automata -a survey[END_REF] relates different reversible models, including reversible Turing machines, reversible boolean logic and reversible cellular automata.

To the best of our knowledge, we are the first in [START_REF] Lanese | Reversing higher-order pi[END_REF] and in this paper to study an encoding of a reversible concurrent model of computation into an irreversible one. In our paper [START_REF] Lanese | Reversing higher-order pi[END_REF] we have defined an encoding very similar to the one presented in this paper, but we were only able to prove the faithfulness of the translation using a weak barbed congruence, which, as discussed in Section 2.5, is a rather coarse equivalence. In this paper, with a slight modification of our encoding, we have been able to prove a much stronger result, which is optimal in the sense that the equivalence we use is a strong back and forth simulation with weak administrative moves, i.e. each forward or backward step in rhoπ translates into a forward or backward step, respectively, modulo administrative moves. Both encodings faithfully implement the reversible calculus, but, as the operational semantics of rhoπ itself, they are rather wasteful in terms of space. To see this informally, notice first that a forward computation step in rhoπ requires retaining in a memory the message a P and the receiver process a(X) ⊲ Q that participated in it. Thus the space overhead of a computation step in reversible HOπ compared to standard HOπ is at least P , the size of the payload of message a P . Now consider the following recursive programs:

P = c(X) ⊲P | a X | X and Q = a(X) ⊲ Q | c X | X . We have a R | P | Q → P | Q | c R | R so the space overhead of this first step starting from a R | P | Q is at least R . On the second step we have P | Q | c R | R → P | Q | a R | R | R | R ,
so the space overhead of this second step is at least 2 R . By induction, one can see that the space overhead associated with making the program a R | P | Q reversible is at least 2 n-1 R , where n is the number of computation steps taken from the initial state a R | P | Q. Our encodings are at least as wasteful in terms of space. However we have shown in [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF] that the space overhead required to implement a small language close to rhoπ is only linear in the number of computation steps, and in fact only linear in the number of non-deterministic events occurring during a computation.

Causal semantics and back and forth simulations. For proving the correctness of our encoding, we have used a notion of back and forth bisimulation, where both forward and backward moves are taken into account in the bisimulation game. Different forms of simulations taking into account forward and backward moves have been studied in the past but mostly in the context of verifying standard transition systems. Such notions appear in the late 80's and early 90's in works such as [START_REF] De Nicola | Back and forth bisimulations[END_REF][START_REF] Klarlund | Proving nondeterministically specified safety properties using progress measures[END_REF]. The two survey papers [START_REF] Lynch | Forward and backward simulations: I. untimed systems[END_REF][START_REF] Lynch | Forward and backward simulations, ii: Timing-based systems[END_REF] by Lynch and Vaandrager study the relationships between different kinds of simulations between (standard, timed and untimed) transition systems, including refinements, forward and backward simulations, hybrid forwardbackward and backward-forward simulations, and history and prophecy relations. More recently, notions of forward and backward simulation have been studied from a coalgebraic point of view by Hasuo [START_REF] Hasuo | Generic forward and backward simulations[END_REF].

More related to reversible models of computation are recent works by Phillips and Ulidowski. The paper [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF] proposes extensions to event structures to take into account reversibility in transition systems. The paper [START_REF] Phillips | Reverse bisimulations on stable configuration structures[END_REF] defines several forms of bisimulations mixing forward and reverse observations, and studies the relationships between various equivalences on sta-ble configuration structures, including step bisimulation, step bisimulation with reverse steps, interleaving bisimulation with reverse steps, and hereditary history-preserving bisimulation. Notably, they show that, in absence of auto-concurrency, interleaving bisimulation with reverse steps is as strong as hereditary history-preserving bisimulation. The latter results illustrates the observational power gained by the ability to take into account backward moves in a bisimulation game. It squares nicely with our result in Section 3.2 that relates our reversible machinery in rhoπ to the causal semantics for π developed by Boreale and Sangiorgi [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF], and which states that a causally consistent reversible semantics essentially constitutes a causal semantics for (the forward part of) the calculus. This intuition is further compounded by the work on Rπ [START_REF] Cristescu | A compositional semantics for the reversible p-calculus[END_REF], which shows that Rπ semantics provides a noninterleaving semantics for the π-calculus that in addition agrees with the causality induced by reductions (τ transitions). Much work remains to be done, however, to better understand the relationships between our reduction semantics for (higher-order) π and the resulting barbed congruence, the LTS semantics of Rπ and its associated bisimilarity, and the various causal semantics of the π calculus that have been developed in the past, including, e.g., [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF][START_REF] Degano | Non-interleaving semantics for mobile processes[END_REF][START_REF] Crafa | Compositional event structure semantics for the internal pi-calculus[END_REF][START_REF] Crafa | Event structure semantics of the parallel extrusion in the pi-calculus[END_REF]].

Conclusion

We have presented a reversible asynchronous higher-order π-calculus, called rhoπ, which we have shown to be causally consistent. The paper gets its inspiration from Danos and Krivine work [START_REF] Danos | Reversible communicating systems[END_REF] and makes three original contributions. The first one is a novel way to introduce reversibility in a process calculus which preserves the classical structural congruence laws of the π-calculus, and which relies on simple name tags for identifying threads and explicit memory processes. Our approach contrasts with the two previous approaches of RCCS [START_REF] Danos | Reversible communicating systems[END_REF], that relied on memory stacks as thread tags, and of Phillips and Ulidowski [START_REF] Phillips | Reversing algebraic process calculi[END_REF], that relied on making the structure of terms in SOS rules static and on keeping track of causality by tagging actions in SOS rules, as well as with the recent work on Rπ, a reversible variant of the π calculus developed by Cristescu, Krivine and Varacca [START_REF] Cristescu | A compositional semantics for the reversible p-calculus[END_REF]. The paper by Danos et al. [START_REF] Danos | General reversibility[END_REF] provides an abstract categorical analysis of the RCCS constructions, but it leaves intact the question of devising an appropriate "syntactic representation of the reversible history category" for the target formalism (in our case, asynchronous HOπ), which is not entirely trivial. The second contribution of the paper is the analysis, by means of a bisimulation relation called causal correspondence, of the relationship between the causal semantics of the π-calculus developed by Boreale and Sangiorgi [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF], and the causality tracking machinery used in our reduction semantics for rhoπ. The third contribution of the paper is a faithful encoding of our reversible HOπ calculus into a variant of HOπ, showing that adding reversibility does not change substantially the expressive power of HOπ. The result obtained in this paper considerably strengthens that obtained in our previous work [START_REF] Lanese | Reversing higher-order pi[END_REF] by showing that, modulo administrative reduction steps, a rhoπ process and its translation are strong back and forth bisimilar. R.Eqv: M ։ N with hypothesis M ≡ M ′ , M ′ ։ N ′ and N ′ ≡ N . By using the inductive hypothesis we have that M ′ ։ N ′ implies that γ(M ′ ) → π γ(N ′ ) and since structural equivalence is preserved by γ (by Lemma 38) we can conclude.

R.Ctx: the proof is by induction on the context. The case of the empty context is trivial. The case of a restriction of a key is trivial since the restriction is removed by γ. The case of restriction of a name follows by induction. The case of parallel composition follows by induction since

γ(M | N ) = γ(M ) | γ(N ).
To prove Lemma 5 we need a few auxiliary results. The first one characterizes the configurations M such that γ(M ) = P for a given HOπ process P .

Lemma 39. Let P be a HOπ process. If γ(M ) = P and P ≡ π P ′ with P ′ = νã. i∈I ρ i and ã ⊆ fn

( i∈I ρ i ) then M ≡ νã, ã′ , k. i∈I κ i : ρ i | j∈J m j with ã′ ∩ fn( i∈I κ i : ρ i ) = ∅. Proof. By Lemma 1 M ≡ ν ũ. i ′ ∈I ′ (κ ′ i : ρ ′ i ) | j ′ ∈J ′ m j ′ ≡ ν b, h. i ′ ∈I ′ (κ ′ i : ρ ′ i ) | j ′ ∈J ′ m j ′ = M ′
where we distinguish between names b and keys h. By definition γ(M ′ ) = ν b. i ′ ∈I ′ ρ i ′ , but since M ≡ M ′ by Lemma 38 we also have γ(M ) ≡ π γ(M ′ ). Since γ(M ) = P ≡ π P ′ we have

P ′ ≡ π γ(M ′ ). Thus we have to prove that if ν b. i ′ ∈I ′ ρ i ′ ≡ π νã. i∈I ρ i then ν b, h. i ′ ∈I ′ (κ ′ i : ρ ′ i ) | j ′ ∈J ′ m j ′ ≡ νã, ã′ , k. i∈I κ i : ρ i | j∈J m j . We can set b = b1 , b2 where b1 ⊆ fn( i ′ ∈I ′ ρ i ′ ) and b2 ∩fn( i ′ ∈I ′ ρ i ′ ) = ∅. We have ν b1 . i ′ ∈I ′ ρ i ′ ≡ π νã. i∈I ρ i
which is derived using only α-conversion and axioms E.ParC, E.ParA and E.NilM. Using the same axioms we can derive also ν b, h.

i ′ ∈I ′ (κ ′ i : ρ ′ i ) | j ′ ∈J ′ m j ′ ≡ ν b2 , ã, h. i∈I (κ i : ρ i ) | j ′ ∈J ′ m ′ j ′ (

memories may be affected by α-conversion). The thesis follows by choosing ã′ = b2 , h = k and j

′ ∈J ′ m ′ j ′ = j∈J m j .
The next lemma is the inverse of Lemma 38.

Lemma 40. Let P and P ′ be HOπ processes. If P ≡ π P ′ then for each configuration M such that γ(M ) = P there is a configuration N such that N ≡ M and γ(N ) = P ′ .

• M m 1 ---→ N 1 and M m 2։ ---→ N 2 . Since M m 1 ---→ N 1 by Lemma 37 M ≡ M ′ with: M ′ = ν ũ, k. k : R | [κ 1 : a P | κ 2 : a(X) ⊲ Q; k] | i∈I ′ κ i : ρ i | j∈J ′ m j N 1 ≡ ν ũ. κ 1 : a P | κ 2 : a(X) ⊲ Q | i∈I κ i : ρ i | j∈J m j and since M m 2։
---→ N 2 then by Lemma 36 M ≡ M ′′ with:

M ′′ = ν ũ. κ ′ 1 : a ′ P ′ | κ ′ 2 : a ′ (X) ⊲ Q ′ | i∈I κ i : ρ i | j∈J ′ m j N 2 ≡ ν ũ, k ′ . k ′ : Q ′ { P ′ / X } | m ′ 2 | i∈I κ i : ρ i | j∈J ′ [µ j ; k j ] and m ′ 2 = [κ ′ 1 : a P ′ | κ ′ 2 : a(X) ⊲ Q ′ ; k ′ ].
By hypothesis the two transitions are concurrent so k is neither equal nor a suffix of κ ′ 1 or κ ′ 2 . Thus, we have that

M ≡ ν ũ, k ′ . k : R | [κ 1 : a P | κ 2 : a(X) ⊲ Q; k] | (κ ′ 1 : a ′ P ′ ) | (κ ′ 2 : a ′ (X) ⊲ Q ′ ) | i∈I ′′ κ i : ρ i | j∈J ′′ m j N 1 ≡ ν ũ. κ ′ 1 : a ′ P ′ | κ ′ 2 : a ′ (X) ⊲ Q ′ | κ 1 : a P | κ 2 : a(X) ⊲ Q | i∈I ′′ κ i : ρ i | j∈J ′′ m j N 2 ≡ ν ũ, k ′ , k. m ′ 2 | k ′ : Q ′ { P ′ / X } | [κ 1 : a P | κ 2 : a(X) ⊲ Q; k] | k : R | i∈I ′′ κ i : ρ i | j∈J ′′ m j
We have that:

N 2 m 1 ---→ ν ũ, k ′ . (κ 1 : a P ) | (κ 2 : a(X) ⊲ Q) | m ′ 2 | k ′ : Q ′ { P ′ / X } | i∈I ′′ κ i : ρ i | j∈J ′′ m j N 1 m 2։ ---→ ν ũ, k ′ . (κ 1 : a P ) | (κ 2 : a(X) ⊲ Q) | m ′ 2 | k ′ : Q ′ { P ′ / X } | i∈I ′′ κ i : ρ i | j∈J ′′ m j as desired. • M m 1։ ---→ N 1 and M m 2
---→ N 2 , similar to the case above.

• M m 1 ---→ N 1 and M m 2
---→ N 2 , similar to the first case.

Lemma 10 (Rearranging lemma). Let σ be a trace. There exist forward traces σ ′ and σ ′′ such that σ ≍ σ ′ • ; σ ′′ .

Proof. The proof is by lexicographic induction on the length of σ and on the distance between the beginning of σ and the earliest pair of transitions in σ of the form t; t ′ • (where t and t ′ are forward). If there is no such pair we are done. If there is one, we have two possibilities: either t and t ′ are concurrent, or they are in conflict. In the first case, we can swap them by using Lemma 9, resulting in a later earliest contradicting pair, and by induction the result follows since swapping transitions keeps the total length constant. In the second case we have that there is a conflict on a tag κ. We have two cases: either the memory involved in the two transitions is the same or not. In the first case we have t = t ′ , and we can apply the Loop lemma removing t; t • . Hence the total length of σ decreases and again by induction the result follows. In the second case thanks to the property of consistent configurations the only possible conflict is between the thread tag of a memory and a tag in the configuration part of the other memory. Assume a conflict between the thread tag of memory m of transition t and a tag in the configuration part of memory m ′ of transition t ′ • . In this case t has created a memory of the form [δ 1 : a P | γ 1 : a(X) ⊲ Q; k 1 ] and a process k 1 : R. Thus from conditions 1 and 4 in the definition of consistent configuration this case never happens. Assume now the opposite case: a conflict between the thread tag of memory m ′ and a tag in the configuration part of memory m. In this case transition t ′

• deletes a memory of the form [δ 2 : a P | γ 2 : a(X) ⊲ Q; k 2 ], but this requires having a process k 2 : R. Again from conditions 1 and 4 this case never happens.

Lemma 11 (Shortening lemma). Let σ 1 , σ 2 be coinitial and cofinal traces, with σ 2 forward. Then, there exists a forward trace σ ′ 1 of length at most that of σ 1 such that σ ′ 1 ≍ σ 1 .

Proof. We prove this lemma by induction on the length of σ 1 . If σ 1 is a forward trace we are already done.

Otherwise by Lemma 10 we can write σ 1 as σ • ; σ ′ (with σ and σ ′ forward). Let t • ; t ′ be the only two successive transitions in σ 1 with opposite direction, with m 1 belonging to t • . Since m 1 is removed by t • then m 1 has to be put back by another forward transition otherwise this difference will stay visible since σ 2 is a forward trace. Let t 1 be the earliest such transition in σ 1 . Since it is able to put back m 1 it has to be the exact opposite of t • , so t 1 = t. Now we can swap t 1 with all the transitions between t 1 and t • , in order to obtain a trace in which t 1 and t • are adjacent. To do so we use the Square Lemma (Lemma 9), since all the transitions in between are concurrent. Assume in fact that there is a transition involving memory m 2 which is not concurrent to t 1 , with λ(m 1 ) = {δ 1 , γ 1 , k 1 }, λ(m 2 ) = {δ 2 , γ 2 , k 2 }. Thanks to consistency conditions the only possible conflicts are (1) between k 1 and δ 2 or between k 1 and γ 2 or (2) between k 2 and δ 1 or k 2 and γ 1 . The first case can never happen since k 1 is fresh (generated by the forward rule) and thus cannot coincide nor been a prefix of γ 2 or δ 2 . Similarly the second case can never happen since k 2 is fresh and thus cannot occur in m 1 . When t • and t are adjacent we can remove both of them using ≍. The resulting trace is shorter, thus the thesis follows by inductive hypothesis.

Theorem 1 (Causal consistency). Let σ 1 and σ 2 be coinitial traces, then σ 1 ≍ σ 2 if and only if σ 1 and σ 2 are cofinal.

Proof. By construction of ≍, if σ 1 ≍ σ 2 then σ 1 and σ 2 must be coinitial and cofinal, so this direction of the theorem is verified. Now we have to prove that σ 1 and σ 2 being coinitial and cofinal implies that σ 1 ≍ σ 2 . By Lemma 10 we know that the two traces can be written as composition of a backward trace and a forward one. The proof is by lexicographic induction on the sum of the lengths of σ 1 and σ 2 and on the distance between the end of σ 1 and the earliest pair of transitions t 1 in σ 1 and t 2 in σ 2 which are not equal. If all the transitions are equal then we are done. Otherwise we have to consider three cases depending on the direction of the two transitions. t 1 forward and t 2 backward: we have σ 1 = σ • ; t 1 ; σ ′ and σ 2 = σ • ; t 2 ; σ ′′ . Moreover we know that t 1 ; σ ′ is a forward trace, so we can apply the Lemma 11 to the traces t 1 ; σ ′ and t 2 ; σ ′′ (since σ 1 and σ 2 are coinitial and cofinal by hypothesis, also t 1 ; σ ′ and t 2 ; σ ′′ are coinitial and cofinal)

and we obtain that t 2 ; σ ′′ has a shorter equivalent forward trace and so also σ 2 has a shorter equivalent forward trace. We can conclude by induction.

t 1 and t 2 forward: by assumption the two transitions are different. If they are not concurrent then they should conflict on a thread process κ : P that they both consume and store in different memories. Since the two traces are cofinal there should be t ′ 2 in σ 2 creating the same memory as t 1 . However no other process κ : P is ever created in σ 2 thus this is not possible. So we can assume that t 1 and t 2 are concurrent. Again let t ′ 2 be the transition in σ 2 creating the same memory of t 1 . We have to prove that t ′ 2 is concurrent to all the previous transitions. This holds since no previous transition can remove one of the processes needed for triggering t ′ 2 and since forward transitions can never conflict on k. Thus we can repetitively apply the Square Lemma to derive a trace equivalent to σ 2 where t 2 and t ′ 2 are consecutive. We can apply a similar transformation to σ 1 . Now we can apply the Square Lemma to t 1 and t 2 to have two traces of the same length as before but where the first pair of different transitions is closer to the end. The thesis follows by inductive hypothesis. t 1 and t 2 backward: t 1 and t 2 cannot remove the same memory. Let m 1 be the memory removed by t 1 . Since the two traces are cofinal, either there is another transition in σ 1 putting back the memory or there is a transition t ′ 1 in σ 2 removing the same memory. In the first case, t 1 is concurrent to all the backward transitions following it, but the ones that consume processes generated by it. All the transitions of this kind have to be undone by corresponding forward transitions (since they are not possible in σ 2 ). Consider the last such transition: we can use the Square Lemma to make it the last backward transition. The forward transition undoing it should be concurrent to all the previous forward transitions (the reason is the same as in the previous case). Thus we can use the Square Lemma to make it the first forward transition. Finally we can apply the simplification rule t • ; t ≍ ǫ target(t) to remove the two transitions, thus shortening the trace. The thesis follows by inductive hypothesis. • (Out): in this case A = a P , K = ∅ and C = P 0, thus A ≡ ∅ : a P | 0, as required.

(Out) a P a --→ ∅;k P 0 (In) a(X) ⊲ P a --→ ∅;k {k} :: (X)P (Cau) A α --→ K;k A ′ K ′ :: A α -----→ K∪K ′ ;k K ′ :: A ′ (Res) A α --→ K;k A ′ fn(α) = a νa. A α --→ K;k νa. A ′ (Parl) A 1 α --→ K;k A ′ 1 A 1 | A 2 α --→ K;k A ′ 1 | A 2 (Parr) A 1 α --→ K;k A ′ 1 A 2 | A 1 α --→ K;k A 2 | A ′ 1 (T-cau) A τ -→ A ′ K :: A τ -→ K :: A ′ (T-res) A τ -→ A ′ νa. A τ -→ νa. A ′ (T-parl) A 1 τ -→ A ′ 1 A 1 | A 2 τ -→ A ′ 1 | A 2 (T-parr) A 1 τ -→ A ′ 1 A 2 | A 1 τ -→ A 2 | A ′ 1 (Coml) A 1 a ---→ K1;k C A 2 a ---→ K2;k F k ∈ fk(A 1 , A 2 ) A 1 | A 2 τ -→ (F • C){ K1 / k } (Comr) A 1 a ---→ K1;k C A 2 a ---→ K2;k F k ∈ fk(A 1 , A 2 ) A 2 | A 1 τ -→ (F • C){ K1 / k }
• (Cau): in this case A = K 1 :: • (In): in this case, A = a(X) ⊲ Q, K = ∅, and F = {k} :: (X)Q. Thus we have A ≡ ∅ :: a(X) ⊲ Q and F ≡ ∅ ∪ {k} :: (X)Q, as required.

A 1 , K = K 1 ∪ K 2 , C = K 1 :: C 1 ,
• (Cau): in this case, A = K 1 :: • (Parl): in this case, We prove property 3 by induction on the derivation of

A 1 , A 1 a --→ K 2 ;k F 1 , k = K 1 ∪ K 2 , F = K 1 ::
A = A 1 | A 2 , A 1 a --→ K;k F 1 , F = F 1 | A 2 .
A τ - → A ′ . • (T-Cau): in this case, A = K :: A 1 , A 1 τ - → A ′ 1 and A ′ = K :: A ′ 1 . By induction assumption A 1 ≡ νc. K 1 :: a P | K 2 :: a(X) ⊲ Q | B, A ′ 1 ≡ νc. K 1 ∪ K 2 :: Q{ P / X } | B for some c, K 1 , K 2 , a, P, Q, B. Thus A ≡ νc. (K ∪ K 1 :: a P ) | (K ∪ K 2 :: a(X) ⊲ Q) | (K :: B) and A ′ ≡ νc. (K ∪ K 1 ∪ K 2 :: Q{ P / X }) | (K :: B)
as required.

• (T-res), (T-parl), (T-parr): the proof is similar to the one of the (T-Cau) case.

• (Coml): in this case, we have

A = A 1 | A 2 , A 1 a --→ K 1 ;k C, A 2 a --→ K 2 ;k
F , and

A ′ = F { K 1 / k } • C.
Using property 1, we have A 1 ≡ νc. K 1 :: a P | B 1 for some c, P, B 1 , and C = νc. P | B 1 Using property 2, we have

A 2 ≡ ν ẽ. K 2 :: a(X) ⊲ Q | B 2 for some ẽ, Q, B 2 , and F ≡ ν ẽ. (K 2 ∪ {k} :: Q) | B 2 Thus, A ≡ νc, ẽ. (K 1 :: a P ) | (K 2 :: a(X) ⊲ Q) | (B 1 | B 2 )
and

A ′ ≡ νc, ẽ. (((K 2 ∪ {k} :: Q) | B 2 ){ P / X } | B 1 ){ K 1 / k } ≡ νc, ẽ. (K 2 ∪ K 1 :: Q{ P / X }) | (B 1 | B 2 ) k : n i=1 τ i ≡ ν h. n i=1 ( h i , h • k : τ i ). By definition: nf( k : n i=1 τ i ) = nf( n i=1 τ i k) = νh 1 , l 1 . nf( τ 1 h 1 ) | nf( n i=2 τ i l 1 ) | nf(KillP h 1 l 1 k) = νh 1 , h 2 , l 1 , l 2 . nf( τ 1 h 1 ) | nf( τ 2 h 2 ) | nf( n i=2 τ i l 1 ) | nf(KillP h 1 l 1 k) | nf(KillP h 2 l 2 l 1 ) = ν h, l. n-1 i=1 nf( τ i h i ) | nf( τ n l n-1 ) | nf(KillP h 1 l 1 k) | n-1 i=2 nf(KillP h i l i l i-1 )
Now by α-converting the key of the last τ n from l n-1 into h n we obtain a term of the form ν h, l.

n i=1 nf( τ i h i ) | nf(KillP h 1 l 1 k) | n-2 i=2 nf(KillP h i l i l i-1 ) | nf(KillP h n-1 h n l i-2 ) = nf( ν h. n i=1 h i , h • k : τ i )
Note that in this case we assumed that the | is right associative, in order to unroll the parallel composition from n i=1 τ i to τ 1 | n i=2 τ i .

Before proving Lemma 14 below, we show a few auxiliary results. First, we characterize the effect of reduction to normal form on a term of the form C[P ]. To this end we define normal form on contexts, which also computes the substitution applied to the hole •. To work with contexts with one hole only, we require that for all the higher-order applications (X)P C 1 [•] either P is linear or P is already in normal form. In the first case the bullet is not replicated, and single-hole contexts are enough. In the second case, no inductive call is required.

(E[R]) = E 1 [nf(R)] and nf(E ′ [nf(R)]) = E 2 [nf(R)]. By hypothesis we have that nf(E[0]) ≡ Ex nf(E ′ [0]). We also have E 1 [nf(0σ)] = E 1 [0] ≡ Ex E 2 [0] = E 2 [nf(0σ ′ )],
and we can conclude by saying that also Proof. By definition of well formedness there exists a rhoπ process P such that νk. k : P ⇒ P ′ . The proof is by induction on the number of steps in ⇒. The base case is when νk. k : P = P ′ . The proof is easy by inspection on the rules defining the encoding, since all messages on key channels are created together with the corresponding Rew l.

E 1 [nf(R)] ≡ Ex E 2 [nf(R)], that is nf(Q) ≡ Ex nf(Q ′ ),
In the inductive case we have that P ⇒ P ′′ → P ′ with P ′ ≡ C[l R ]. For simplicity we consider just one instance of a message l R at the time. Note that messages cannot appear, but existing messages may be duplicated because of communications or applications. We proceed by case analysis on P ′′ → P ′ . If the reduction does not involve the message l R nor the corresponding S the thesis follows easily. If the message l R is inside a communicated message or the argument of an application, then the corresponding S is inside the same message or the same argument and they are deleted, moved, or replicated together. If the message is read, it disappears and nothing has to be proved. If the message is inside a trigger or in the body of an abstraction on a process then a substitution may be applied to it, but this has no effect on the corresponding S, and the thesis holds by inductive hypothesis. If the reduction is an abstraction of the name l, then the same renaming is done on the corresponding Rew l, and the thesis holds by inductive hypothesis. If the reduction is the application of Rew l we move from the first case of the thesis to the second one. If instead the reduction is the communication of l(Z) ⊲ Z l, this removes the corresponding message and nothing has to be proved (if it removes another message this means that there were two parallel messages on the same channel l, and we may simply exchange them in the correspondence).

Lemma 17. If P ′ is well formed and P ′ ≡ C[a P , l ] with a ∈ N for 2. P ≡ C[(KillP l 1 l 2 l 3 ) | (KillP l 4 l 5 l 6 )], with l 1 , l 2 , l 3 , l 4 , l 5 , l 6 ∈ K and {l 1 , l 2 } ∩ {l 4 , l 5 } = ∅ or l 3 = l 6 .

3. P ≡ C[(KillP l 1 l 2 l) | (Mem P a Q h l 3 k)], with l, l 1 , l 2 , l 3 , h, k ∈ K
and l 1 = l 3 or l 2 = l 3 .

Proof. By inspecting the encoding of Figure 7.

For condition 1 the proof is by structural induction on R, using as inductive hypothesis that messages are created only on the key channel passed to the process or on fresh key channels. In basic cases (0 process, message or trigger), one message is created on the received channel, plus one if the Rew l is executed, but this consumes a message on the same channel thus preserving the invariant. For restriction, the thesis follows by inductive hypothesis. For Par, two distinct fresh names are passed to the parallel processes, thus by inductive hypothesis their messages will not be on the same channel as the one created by the KillP. For Trig, a fresh name is passed to the continuation, thus by inductive hypothesis its messages will not conflict with the one created by the KillT or by the one created by the Trig in the Mem. Note that these last two messages may not conflict since for them to be created the token t is needed, and either KillT or the Trig may read it, but not both of them.

For condition 2, note that KillP is generated only by a Par process. The first two arguments are fresh, thus they cannot be used by different KillP. For the last argument, we can reason as above to show that at most one KillP for each name may be created.

For condition 3 we can see that the channel used by the Mem is fresh, and the same for the ones used by KillP, thus they may not coincide.

Before proving Lemma 25 below we show a few auxiliary results.

Lemma 54 (Input key invariant). For each rhoπ process R and key l we have:

1. R l ⇒ E[l(X) ⊲ P ], unless the trigger has been generated by an application of Rew l.

2. R l ⇒ E[l(X)|l ′ (W ) ⊲ P ]. 3. R l ⇒ E[l ′ (X) ⊲ P | l ′ (X) ⊲ Q] for each l ′ ∈ K and l ′ = l, unless one
of the triggers has been generated by an application of a Rew l ′ .

Proof. All the cases are proved by induction on n, showing that no such derivation with less than n steps exists. All the base cases are trivial, since the starting term has no trigger in an active position. Let us consider the different inductive cases.

(1) We reason by contradiction. Suppose that R l ⇒ E[l(X) ⊲ P ] in n steps. By looking at the encoding in Figure 7 we note that a trigger on a key channel can only occur inside a Mem term. However the subject k is generated fresh in the clause defining the Trig process, thus it cannot be l. This contradiction concludes the proof.

(2) Suppose towards a contradiction that R l ⇒ E[l(X)|l ′ (Z) ⊲ P ] in n steps. By looking at the encoding we note that a trigger reading two messages can only be generated by a KillP process. However, the two names are generated fresh in the clause defining the Par process, against the hypothesis that one of them can be l.

(3) We use the same proof strategy as in ( 1) and ( 2). Triggers on keys l ′ ∈ K with l = l may be generated only by Mem processes, but since the used key is fresh two triggers may not have the same key.

Messages on channels l ∈ K carry translations of processes with no toplevel restrictions.

Lemma 55. For each rhoπ process R, R l ⇒ C[l Q ] implies Q = Q ′ where Q ′ has no toplevel restriction.
Proof. We proceed by induction on the number of reductions in ⇒. The proof of the base case is by structural induction on R. We show a few cases as examples. R = a P : by definition

a P h = (l)((a X l)Msg a X l)h = (l)((a X l)(a X, \l | (KillM a l)) a P l)h = (l)(((a X l)(a X, \l | (((a l)a(X, \l) ⊲ l (h)Msg a X h | (Rew l)) a l))a P l)h as desired since (h)Msg a X h = a X .
Q , hence E[nf(KillP l h k)] ≡ E ′ [l P | h Q | l(Z)|h(W ) ⊲ k (h)Par Z W l ] → E ′ [k (h)Par P Q l ],
and by expanding the definition of Par we have that nf(P

1 ) → E ′ [k (h)(νl 1 , l 2 . (P l 1 ) | (Q l 2 ) | KillP l 1 l 2 l) ] ≡ Ex E ′ [k (h)(νl 1 , l 2 . (Q l 1 ) | (P l 2 ) | KillP l 2 l 1 l) ]. Since nf(P 2 ) → E ′ [k (h)(νl 1 , l 2 . (Q l 1 ) | (P l 2 ) | KillP l 2 l 1 l)
] the thesis follows.

Ax.P. We have nf(

P 1 ) = E[l 1 P | l 2 Q | nf(KillP l 1 l 2 l)].
) ≡ E ′ [l 1 (Z) ⊲ Z l 1 | l 1 P | l 2 Q | nf(KillP l 1 l 2 l)] → E ′ [ P l 1 | l 2 Q | nf(KillP l 1 l 2 l)]
. By using Lemma 55 and the axiom Ex.Unfold we have that P l 1 ≡ Ex Rew l 1 | l 1 P , and then

E ′ [ P l 1 | l 2 Q | nf(KillP l 1 l 2 l)] ≡ Ex E ′ [Rew l 1 | l 1 P | l 2 Q | nf(KillP l 1 l 2 l)]. So E[Rew l 1 | l 1 P | l 2 Q | nf(KillP l 1 l 2 l)] ≡ Ex nf(E[Rew l 1 | l (h)Par P Q h | Rew l]
), as desired. The case of a KillP corresponds to a reduction inside the hole, since no other message on the same channel can exist thanks to condition 1 of Lemma 24, and no other KillP may read the same messages thanks to condition 2 of Lemma 24. In this case we have that nf

(P 1 ) = E[l 1 P | l 2 Q | (l 1 (Z)|l 2 (W ) ⊲ (l)Par Z W h | Rew l)] → E[(l)Par P Q h | Rew l]
and the thesis banally follows. The case of a Mem can never happen thanks to condition 3 of Lemma 24.

Reductions from the right member of the axiom are trivially matched since the left member reduces to the right one.

Ax.A. We have that nf(P

1 ) = E[νl ′ . l 1 (Z)|l 2 (W )⊲l ′ (h)Par Z W h | Rew l ′ | l ′ (Z ′ )|l 3 (W ′ ) ⊲ l (h)Par Z ′ W ′ h | Rew l ].
The hole may perform a communication only if there are two messages on l 1 , l 2 in the context. In this case, we have that nf(P

1 ) ≡ E ′ [νl ′ . l 1 P | l 2 Q | (l 1 (Z)|l 2 (W ) ⊲ l ′ (h)Par Z W h | Rew l ′ ) | nf(KillP l ′ l 3 l)] → E ′ [l ′ (h)Par P Q h | Rew l ′ | nf(KillP l ′ l 3 l)] ≡ Ex E[νl ′ . l 1 P | l 2 Q | (l 1 (Z)|l 2 (W ) ⊲ l ′ (h)Par Z W h | Rew l ′ ) | nf(KillP l ′ l 3 l)]
using axiom Ax.P, as desired.

Ax.Unfold. Since P ≡ ν ũ. Q we have that nf

( P l) ≡ nf( ν ũ. Q l) = ν ũ. nf( Q l), hence nf(P 1 ) = E[ν ũ. nf( Q l)]. If E[ν ũ. nf( Q l)] → R then also nf(P 2 ) = E[ν ũ. l Q | l(Z) ⊲ Z l] → E[ν ũ. Q l] ⇁ * E[ν ũ. nf( Q l)] → R, as desired. Similarly, if nf(P 2 ) = E[ν ũ. l Q | l(Z) ⊲ Z l] → R ′ from Lemma 23 we have nf(P 1 ) = E[ν ũ. nf( Q l)] ֒→ * E[ν ũ. nf(ν ũ′ . l Q ′ | Rew l | S)]
where S is garbage. Thanks to Lemma 55 ũ′ is empty and

Q ′ = Q, thus E[ν ũ. nf(ν ũ′ . l Q ′ | Rew l | S)] = E[ν ũ. l Q | l(Z) ⊲ Z l | S] → R ′ with R ′ ∈ addG(R) as desired.
Note that this is the only case where garbage is generated.

Ax.Adm. By noting that the left member of the axiom can only perform a communication, reducing to the right member of the axiom.

Before proving Lemma 28 below we show some auxiliary results. In particular, we have to study where in a configuration a key may occur. We call l-process, denoted by P l , a process of a specific form.

Definition 20. Let Y = (X c)c Q . An l-process is an HOπ + process of one of the forms below, or obtained from them via one or more applications. Essentially, each key l occurs at most twice (apart from occurrences in Rew), once in an l-process and possibly once in a killer process or a memory process.

We call primitive context a context originated during the translation of a process.

Definition 21. A context C is called a primitive context if it is generated by: C ::= • | (l ′ )Msg a C l ′ | (l ′ )Trig (X c)c C a l ′ | (l ′ )νa. (C l ′ ) | (l ′ )Par C Q l ′ | (l ′ )Par P C l ′
Let us consider the condition (1). Reductions involving only E leave the process in the same form. For other reductions we proceed by case analysis on the form of P l (we consider applied forms together with the form they derive from). For simplicity we do not write addG if it does not change. Adding it is however straightforward.

If P l = P l we proceed by case analysis on the structure of P . If P = 0 then we have E[νl. which again satisfies the conditions. If the message on l is read by S then there are two cases: either it is read by a memory, or by a KillP. In the first case we have that:

P l | S] ⇁ E[νl. l Nil | Rew l | S], which sat- isfies again condition (1). Similarly, if P = a Q then E[νl. a Q | S] ⇁ E[νl. Msg a Q l],
E[νl. l P | Rew l | (l(Z) ⊲ Msg a Q l 1 | Trig(X c)c R a l 2 ) | S] ֒→ E[νl. Rew l | (Msg a Q l 1 ) | (Trig(X c)c R a l 2 ) | S] ≡ E ′ [νl. 0 | Rew l | S]
which satisfies again condition (1) since νl. 0 | Rew l ∈ addG(νl. 0). If the message is read by a KillP then the context contains also a message on channel h such that:

E[νl. l P | Rew l | S] ≡ E 1 [νl. h Q | l P | (l(Z)|h(W ) ⊲ k (h)Par Z W h | Rew k) | S] ֒→ E 1 [(νl. 0 | S) | k (h)Par Q P h | Rew k] ≡ E 2 [νl. 0 | S]
which satisfies again condition [START_REF] Bennett | Notes on the history of reversible computation[END_REF].

If P l = Msg a Q l or P l = Trig Y a l we have a few cases. If P l reduces alone then it is simply applied, and its applied form is still an l-process. Note that neither S nor the context can interact with such a P l before application.

Let us consider applied forms of P l = Msg a Q l. With one application we get P l = a Q , l | KillM a l. In this case E[νl. P l | S] can perform several reductions. If KillM is not in its applied form and it is applied, then the thesis banally follows. If KillM is in its applied form, then it can interact with the message. In this case, we have that

E[νl. a Q , l | a(X, \l) ⊲ l (h)Msg a Q h | Rew l | S] ֒→ E[νl. l (h)Msg a Q h | (Rew l) | S]
and condition (1) still holds. If the message is read by the context, then it is read either by a KillM (in its applied form) or by a Trig (in its applied form). The first case has been treated just above. In the second case (we only need to consider the trigger, and the token t needed for its activation) we have that

E[νl. a Q , l | (KillM a l) | S] ≡ E 1 [νl. a Q , l | t | (a(X, h)|t ⊲ νk, c. (((X c)c P ) X c) | (c(Z) ⊲ Z k) | (Mem Y a X h k l)) | (KillM a l)| | S] ֒→ E 1 [νl, k, c. (((X c)c P ) Q c) | c(Z) ⊲ Z k | (Mem Y a P l k l 1 ) | S] ≡ E 2 [νl. (Mem Y a P l k l 1 ) | S]
E[νl, t. t | (a(X, h)|t ⊲ f R) | (t ⊲ l (h)Trig Y a h) | Rew l) | S] ֒→ E[νl, t. (a(X, h)|t ⊲ f R) | l (h)Trig Y a h | Rew l | S] ≡ E 1 [νl. l (h)Trig Y a h | Rew l | S] as desired since l (h)Trig Y a h | Rew l ∈ addG( a(X) ⊲ Q ).
The only other possibility is that the trigger reads a message from the context. Thanks to Lemma 57 the message should be of the form a P , l 1 for some P and some l 1 . Therefore,

E[νl, t. t | (a(X, h)|t ⊲ f R) | KillT Y t l a | S] ≡ E 1 [νl, t. t | a P , l 1 | (a(X, h)|t ⊲ f R) | KillT Y t l a | S] ։ E 1 [νl, k, t, c. (((X c)c Q ) P c) | c(Z) ⊲ Z k | (Mem Y a P l 1 k l) | S] ≡ E 2 [νk. (((X c)c Q ) P c) | c(Z) ⊲ Z k | νl. (Mem Y a P l 1 k l) | S] ≡ E 3 [νl. (Mem Y a P l 1 k l) | S]
If P l = Mem Y a P l k h and the Mem is applied, then the thesis banally follows. If the Mem process is already in its applied form, then it may only interact with the context via a message on k. Hence, we have

E[νl. k(Z) ⊲ b (Msg a P l) | (Trig Y a h)] ≡ E 1 [νl. k R | k(Z) ⊲ b (Msg a P l) | (Trig Y a h)] E 1 [(νl. (Msg a P l)) | Trig Y a h] ≡ E 2 [νl. (Msg a P l))]
and condition (1) still holds.

The case P l = (Mem Y a P h k l) is similar. Since 0 has no reduction, in the case P l = 0 there is nothing to prove. Let us consider conditions (2), ( 3) and ( 4). If the context evolves by itself, then they are still satisfied. For the hole to contribute, the only possibility is that the context is an active context. For condition (2), we have a case analysis on the form of C Lemma 28. For any consistent configuration M , if M ⇒ P and P ֒→ * Q then there exist Q ′ and P ′ such that Q ֒→ * Q ′ , P ′ ∈ addG(P ) with nf(P ′ ) ≡ Ex nf(Q ′ ).

′ . If C ′ = •, then C[νh. ((l)P l )h] ⇁ C[νh. P h ], the name l disappears and the thesis trivially holds. If C ′ = (l ′ )Msg a C ′′ [•] l ′ then we have C[νh. ((l ′ )Msg a C ′′ [(l)P l ] l ′ )h] ⇁ C[νh. Msg a C ′′ [(l)P l ] h].
Proof. By induction on the number n of steps in P ֒→ * Q. In the base case (n = 0) the thesis banally follows. For the inductive case, consider the first step P ֒→ Q 1 of P ֒→ * Q. There are two cases to distinguish: whether ֒→ is an application ⇁ or a non labelled communication →. Let us consider the first case. We have that P ⇁ Q 1 and Q 1 ֒→ * Q. By inductive hypothesis there exist

Q ′ , Q ′ 1 such that Q ֒→ * Q ′ , Q ′ 1 ∈ addG(Q 1 )
and nf(Q ′ 1 ) ≡ Ex nf(Q ′ ). Since the added garbage does not forbid reductions we have that there exists P ′ ∈ addG(P ) such that P ′ ⇁ Q ′ 1 . Thus nf(P ′ ) = nf(Q ′ 1 ) ≡ Ex nf(Q ′ ) as desired.

If the step is a non labelled communication → then we have three cases, corresponding to the three kinds of non labelled trigger processes: a Rew process, a killer process and the trigger in the translation of the continuation of a rhoπ trigger.

Let us consider the case of a Rew process. We have that P ≡ E[l P 1 | l(Z) ⊲ Z l] → E[ P 1 l]. By using Lemma 23 we have that P 1 l ֒→ * l P 2 | Rew l | S with S a parallel composition of garbage processes. Thanks to Lemma 55, P 1 has no toplevel restrictions (since it was argument of a message), thus P 2 = P 1 . So, we have that E[ P 1 l] ֒→ * E[l P 1 | Rew l | S] ∈ addG(P ). Now from E[ P 1 l] ֒→ * Q we have that by inductive hypothesis Q ֒→ * Q ′ and there is P ′ ∈ addG(E[ P 1 l]) such that nf(P ′ ) ≡ Ex nf(Q ′ ). Since the garbage does not forbid reductions we have that there exists P ′′ ∈ addG(E[l P 1 | Rew l | S]) such that P ′ ֒→ * P ′′ . From Lemma 27 nf(P ′ ) ֒→ * nf(P ′′ ). Thanks to Lemma 25 from nf(P ′ ) ≡ Ex nf(Q ′ ) and P ′ ֒→ * P ′′ we have that nf(Q ′ ) ֒→ * nf(Q ′′ ) with P ′′′ ∈ addG(P ′′ ) and nf(P ′′′ ) ≡ Ex nf(Q ′′ ). By composing garbage we also have P ′′′ ∈ addG(P ). The thesis follows.

Let us consider the case of a killer process. We have a few subcases, corresponding to the killer processes KillM, KillP and KillT. The main idea here is that the communication is undone by a Rew. Let us consider a KillM process. We have that P ≡ E[a P We proceed by case analysis on the reduction ֒→. Since Q ′ is generated from nf( M ) via administrative steps, then applications of the form (((X c)c P ) Q c) or communications of the form c P | (c(Z) ⊲ Z l) or with a trigger of the form (k(Z) ⊲ (Msg a P l 1 ) | (Trig ((X c)c P ) a l 2 )) are never enabled. Thus, only communications involving a killer or a Rew process may happen. A communication involving a killer does not add barbs (since fn(Q ′ ) ∩ K = ∅). A communication involving a Rew process does not add barbs since it produces an application. Similarly, all the applications involving killer, Rew and Mem processes do not add barbs. Nevertheless, other applications, such as the application of a Msg process, may create barbs. However, no such application is enabled in nf( M ). The only way they may become enabled is via a kill followed by a Rew. However, the created barb was already present in nf( M ) before the kill. This completes the proof.

We now show that barbs of nf( M ) come from barbs of M . Lemma 62. For each consistent configuration M , if nf( M ) ↓ a then M ↓ a .

Proof. By structural induction on M . Note that only rhoπ names may be free, since all the names coming from rhoπ keys are bound (by Lemma 22). Since sub-terms of consistent configurations are not consistent in general, we have to consider in the induction both consistent configurations and their sub-terms. If M = κ : P , we proceed by structural induction on P and by case analysis on κ. We will consider just the case in which κ = k, the other case with κ = h i , h • k is similar. If P = 0 then we have that nf( k : 0 ) = k Nil | Rew k, but since k ∈ N the process nf( k : 0 ) does not show any relevant barb. If P = a Q then we have that nf( k : a Q ) = a Q , k | (a(X, \k) ⊲ k (h)Msg a Q h | Rew k), which shows a barb on a. Since also M ↓ a , we are done. If P = a(X) ⊲ Q,we have that nf( k : a(X) ⊲ Q ) = νt. t | (a(X, h)|t ⊲ R) | (t ⊲ S) (for some R and S). Since t is restricted then the entire process does not show any barb, and we are done. If P = Q 1 | Q 2 , the tag κ has to be a key, since we are dealing with consistent configurations. So, we have that nf( k : (Q 1 | Q 2 ) ) = νh, l. nf( Q 1 h) | nf( Q 2 l) | (h(W )|l(Z) ⊲ S). The process may show a barb because of either nf( Q 1 h) or nf( Q 2 l) (or both). Let us suppose that it is because of nf( Q 1 h), that is nf( Q 1 h) ↓ a . By definition of we have that nf( Q 1 h) = nf( h : Q 1 ) and hence nf( h : Q 1 ) ↓ a . Now, by applying the inductive hypothesis we have that (h : Q 1 ) ↓ a and then also k : (Q 1 | Q 2 ) ↓ a , as desired. The other cases are similar.

If M = 0, we have that 0 = 0 and the thesis banally follows. If

M = M 1 | M 2 we have that nf( M 1 | M 2 ) = nf( M 1 | M 2 ) = nf( M 1 ) | nf( M 2
) and we can conclude by applying the inductive hypothesis on nf( M 1 ) and nf( M 2 ). If M = νu. M 1 we have that nf( νu. M 1 ) = νu. nf(M 1 ) and we can conclude by applying the inductive hypothesis on nf(M 1 ) . If M = [κ 1 : a P | κ 2 : a(X) ⊲ Q; k], then nf( M ) = k(Z) ⊲ R (for some R), that shows no barbs and we can conclude. Before proving Proposition 1 below, we prove some auxiliary results. Each of the lemmas below shows that one of the axioms in ≡ Ex is correct with respect to weak bf barbed bisimulation (actually, the statement for axiom Ex.P is slightly weaker). We consider together each axiom L ≡ Ax R from ≡ Ax and its normal form nf(L) ≡ Ex nf(R), since this is obtained via applications. Below, we denote a multi-holes context as C. Lemma 63. Axiom Ex.C and its normal form are correct with respect to weak bf barbed bisimulation.

Proof. We show that the relation R below is a weak bf barbed bisimulation.

R 1 ={((KillP l h k), (KillP h l k)) | h, l, k ∈ K} R 2 ={((a(X)|b(Y ) ⊲ R), (b(Y )|a(X) ⊲ R)) | a, b ∈ N ∧ X, Y ∈ V ∧ R ∈ P} R ′ =R 1 ∪ R 2 R ={(C[P 1 , .., P n ], C[Q 1 , .., Q n ]) | n ∈ N ∧ ∀i ∈ {1 . . . n}.(P i , Q i ) ∈ R ′ }
Let us consider the barbs. Since the context is the same on both the sides, and the processes in the holes show no barbs, the barbs coincide.

form E[νl 1 , l 2 . R ′ ] with R ′ ∈ addG(R ′′ ) where R ′′ is obtained via zero or more applications from l 1 P | l 2 Q | (KillP l 1 l 2 l 3 ). On the right side we can assume l 1 and l 2 do not occur.

Let S(l 1 , l 2 , l 3 ) denote a process of one of the following forms: We now prove that the relation R is a weak bf barbed bisimulation. The thesis will follow since in well formed processes all the contexts where the axiom can be applied have this form.

Let us consider barbs. On both sides barbs shown by the contexts C are banally matched. The process νl 1 , l 2 . addG(l 1 P | l 2 Q | S(l 1 , l 2 , l)) does not show any barb, since addG does not add any barb thanks to Lemma 64. On the other side, the process νl 1 , l 2 . addG(l (h)Par P Q h | T l ) shows only a barb at l. We have that: showing a barb at l as well.

Let us consider reductions. If C[P 1 , . . . , P n ] reduces it is because the context reduces by itself or because of the hole processes. The first case is banally matched by the process C[Q 1 , .., Q n ]. In the second case, the process νl 1 , l 2 . addG(l 1 P | l 2 Q | S(l 1 , l 2 , l)) reduces. We have three cases: the processes added by addG are not involved, the processes added by addG reduce alone or they interact with the other processes. In the first case, if the reduction is the application of the process S(l 1 , l 2 , l) then the right process can match the reduction by staying idle. If it is a communication on the channels l 1 and l 2 then we have that: This step is matched by the right process by staying idle, since the process in the i-th hole on the two sides become equal, and we can put them in the context since the identity belongs to the relation (actually, processes added by addG may be different, but they have no impact). The case where processes inside addG reduce alone is banally matched. In the third case, since the process νl 1 , l 2 . addG(l 1 P | l 2 Q | S(l 1 , l 2 , l)) is well formed then the only processes inside addG( ) able to interact are a (l 1 (Z) ⊲ Z l 1 ) and/or a (l 2 (Z) ⊲ Z l 2 ). The two cases are similar, so we consider just the first one. Assume since all the garbage can be moved to addG and since Q does not contain restrictions thanks to Lemma 55. Now, using α-conversion to swap names l 1 and l 2 with h and k and exploiting the fact that addG is closed under αconversion we get νh, k. addG(νl 1 , l 2 . P l 1 | l 2 Q | (KillP l 1 l 2 l)). Since h, k are just used by the addG( ) context we can rewrite the process as νl 1 , l 2 . addG( P l 1 | l 2 Q | (KillP l 1 l 2 l)), where the restriction on k, h has been moved to the context.

Let us consider now the reductions of C[Q 1 , . . . , Q n ]. We have three cases: the context reduces by itself, the hole reduces by itself or the hole and the context interact. The first case is trivial. In the second case, if the reduction is the application of T l then the step is matched by C[P 1 , . . . , P n ] by staying idle, and we are still in the same relation. If T l is already in its applied form then we have: Proof. By induction on the number of parallel components inside Q. The base case Q = 0 reduces to the identity since we can can garbage collect via structural congruence names contained in b (and structural congruence is a weak bf barbed bisimulation by Lemma 32). In the inductive case, we do a case analysis on the last process Q n of the parallel composition.

P

  , Q ::= 0 | X | νa. P | (P | Q) | a P | a(X) ⊲ P M, N ::= 0 | νu. M | (M | N ) | κ : P | [µ; k] κ ::= k | h, h • k µ ::= ((κ 1 : a

Figure 3 :

 3 Figure 3: Reduction rules for rhoπ

  e∈E κ e : ρ e | d∈D δ d : R d | g∈G γ g : T g

  is a weak barbed bisimulation. Since R is symmetric by the corollary of the Loop Lemma (Corollary 2), we only need to show that it is a weak barbed simulation. Consider a pair (C[M ], C[N ]) ∈ R. We have M ⇒ N , and hence by Corollary 2 N ⇒ M . Noting that a configuration context C is an execution context, i.e. if M → N then C[M ] → C[N ], then we also have C[N ] ⇒ C[M ]. We now check easily the two barbed simulation clauses:

  and the rules in Figure 4. The reduction relation → is the least binary relation on closed causal processes that is closed under structural congruence and evaluation contexts defined by the rule:

Figure 4 :

 4 Figure 4: Structural congruence for choπ

Figure 5 :

 5 Figure 5: Syntax of HOπ +

Figure 6 :

 6 Figure 6: Reduction rules for HOπ +

Figure 7 :

 7 Figure 7: Encoding rhoπ processes

Figure 8 :

 8 Figure 8: Encoding rhoπ configurations

Theorem 4 .

 4 For each consistent rhoπ configuration M , if M ։ N then nf( M ) ⇒ f P and if MN then nf( M ) ⇒ b P , and there exists P ′ ∈ addG( N ) such that nf(P ) ≡ Ex nf(P ′ ).

Figure 9 :

 9 Figure 9: The encoding respects ≡ Ex (numbers refer to Lemmas).

Figure B. 10 :Figure B. 11 :

 1011 Figure B.10: Transition system rules for choπ

and A 1 aC 1 . 1 aC 1 , 1 aC 1 ,

 111111 Assume C 1 = νc. P B, then C = νc. P K 1 :: B.By induction assumption, we haveA 1 ≡ νc. (K 2 :: a P ) | B. Thus A = K 1 :: A 1 ≡ νc. (K 1 ∪ K 2 :: a P ) | (K 1 :: B), as required. • (Parl): in this case, A = A 1 | A 2 , A and C = C 1 | A 2 . Assume C 1 = νc. P B, then C = νc. P (B | A 2 ). By induction assumption, we have A 1 ≡ νc. K :: a P | B. Thus, A = A 1 | A 2 ≡ νc. (K :: a P ) | (B | A 2 ),as required. • (Parr): this case is similar to the (Parl) one. • (Res): in this case, A = νe. A 1 , e = a, A and C = νe. C 1 . Assume C 1 = νc. P B, then C = νe. νc. P B. By induction assumption A 1 ≡ νc. K :: a P | B. Thus A = νe. A 1 ≡ νe, c. K :: a P | B. We now have two cases to consider, according to whether e ∈ fn(P ) or not. If e ∈ fn(P ), we have C = νe, c. P B, and we are done. If not, we have C = νc. P νe. B and A ≡ νc. K :: a P | νe. B, as required.We prove property 2 by induction on the derivation of A a

F 1 .

 1 By induction assumption, we haveA 1 ≡ νc. (K 2 :: a(X) ⊲ Q) | B for some c, Q, B, and F 1 ≡ (X)νc. (K 2 ∪ {k} :: Q) | B. Thus, A ≡ νc. (K 1 ∪ K 2 :: a(X) ⊲ Q) | (K 1 :: B), and F ≡ (X)νc. (K 1 ∪ K 2 ∪ {k} :: Q) | (K 1 :: B) as required.

1 aF 1 ,

 11 Byinduction assumption, we have A 1 ≡ νc. (K :: a(X) ⊲ Q) | B for some c, Q, B, andF 1 ≡ (X)νc. (K ∪ {k} :: Q) | B. Thus, A ≡ νc. (K :: a(X) ⊲ Q) | (B | A 2 ), and F ≡ (X)νc. (K ∪ {k} :: Q) | (B | A 2 ) as required.• (Parr): this case is handled as the (Parl) one.• (Res): in this caseA = νe. A 1 , e = a, A F = νe. F 1 . By induction assumption, we have A 1 ≡ νc. (K :: a(X) ⊲ Q) | B for some c, Q, B, and F 1 ≡ (X)νc. (K ∪ {k} :: Q) | B. Thus, A ≡ νe, c. (K :: a(X) ⊲ Q) | B for some c, Q, B, and F ≡ (X)νe, c. (K ∪ {k} :: Q) | B, as required.

Definition 19 (

 19 Context normal form). The context normal form function nfc(C[•]) is defined as nfc(C[•], ∅), where the second parameter is usednf(E[R]) = E 1 [nf(Rσ)] and nf(E ′ [R]) = E 2 [nf(Rσ ′ )]. Since all the processes added by the function addG are closed we have that Rσ = Rσ ′ = R and nf

  as desired.Lemma 16. If P ′ is well formed andP ′ ≡ C[l R ] with l ∈ K for some n-ary context C then P ′ ≡ C ′ [l R | S] with S = Rew l or S = l(Z) ⊲ Z l for some n-ary context C ′ .

R

  = νa. P : by definition νa. P h = (l)(νa. P )h and we can conclude by inductive hypothesis on P . then the thesis banally follows. If the communication involves the hole, we should have in the context two messages of the form l P and h

  Msg a Q l Trig Y a l Par P Q l KillP h k l νc. (Y P c) | (c(Z) ⊲ Z l) | (Mem Y a P l 1 l l 2 ) νu. P l νc. c P | (c(Z) ⊲ Z l) | (Mem Y a P l 1 l l 2 ) 0 Mem Y a P h k l Mem Y a P l k h

and condition ( 1 )

 1 still holds. Let us consider applied forms of P l = Trig Y a l, i.e., P l = νt. t | (a(X, h)|t ⊲ R) | (KillT Y t l a) where R = νk, c. (Y X c) | (c(Z) ⊲ (Z k)) | (Mem Y a X h k l) and Y = (X c)c Q . In this case E[νl. P l | S] can perform several reductions. If the KillT is applied then the thesis banally follows. If the KillT is in its applied form then it can interact with t:

  Name l disappears, thus the thesis holds trivially. Note that condition[START_REF] Landauer | Irreversibility and heat generated in the computing process[END_REF] holds for name h. The other cases for contexts in non applied form are analogous.Let us now consider contexts where the toplevel application has been performed. Again we have a case analysis on the form of the context. If the context has the form C[νh. Msg a C ′ [(l)P l ] h], then we have that C[νh. Msg a C ′ [(l)P l ] h] ⇁ C[νh. a C ′ [(l)P l ], h | KillM a h] and condition (2) still holds. The other cases are similar. If condition (3) holds, we have that C[νl. ((h)P h )l] ⇁ C[νl. P l ], and condition (1) holds for name l.If condition (4) holds, we have that:C[νl, c. (((X c)c P ) Q c) | (c(Z) ⊲ Z l) | (Mem (X c)c P ) a Q h l k)] ⇁ C[νl, c. c P { Q / X }] | (c(Z) ⊲ Z l) | (Mem (X c)c P ) a Q h l k)] = C[νl, c. c P { Q / X } ] | (c(Z) ⊲ Z l) | (Mem (X c)c P ) a Q h l k)]by applying Lemma 21. Condition (1) holds for the name l. If the reduction involves the application of the Mem process, then condition (1) for name l is still satisfied.

27 Q

 27 Figure C.13: Barbs with respect to administrative steps (numbers refer to Lemmas).

Lemma 30 .

 30 If M ֒→ * ↓ a then M ↓ a .Proof. By concatenating Lemma 61 and Lemma 62.

S(l 1

 1 , l 2 , l 3 ) = (KillP l 1 l 2 l 3 ) S(l 1 , l 2 , l 3 ) = (l 1 (Z)|l 2 (W ) ⊲ l 3 (h)Par Z W h | Rew l)Let T l be either a process of the form T l = Rew l or of the form T l = (l(Z) ⊲ Z l). Let us write addG(P ) for any process Q ∈ addG(P ). LetR ′ = {(νl 1 , l 2 . addG(l 1 P | l 2 Q | S(l 1 , l 2 , l))), (νl 1 , l 2 . addG(l (h)Par P Q h | T l ))} R = {(C[P 1 , . . . , P n ], C[Q 1 , . . . , Q n ]) | (P i , Q i ) ∈ R ′ ∧ C[P 1 , . . . , P n ], C[Q 1 , . . . , Q n ] well f ormed}

νl 1 , l 2 .

 12 addG(l 1 P | l 2 Q | S(l 1 , l 2 , l)) ֒→ * νl 1 , l 2 . addG(l (h)Par P Q h | Rew l)

νl 1 , l 2 .

 12 addG(l 1 P | l 2 Q | (l 1 (W )|l 2 (Z) ⊲ l (h)Par P Q h | Rew l)) → νl 1 , l 2 . addG(l (h)Par P Q h | Rew l))

νl 1 ,

 1 l 2 . addG((l 1 (Z) ⊲ Z l 1 ) | l 1 P | l 2 Q | S(l 1 , l 2 , l)) ֒→ νl 1 , l 2 . addG(( P l 1 | l 2 Q | S(l 1 , l 2 , l))We haveνl 1 , l 2 . addG(l (h)Par P Q h | T l ) ֒→ * νl 1 , l 2 . addG(νh, k. P h | Q k | (KillP h k l))Using Lemma 23:νl 1 , l 2 . addG(νh, k. P h | Q k | (KillP h k l)) ֒→ * νl 1 , l 2 . addG(νh, k. P h | k Q | (KillP h k l))

νl 1 , l 2 .

 12 addG(l (h)Par P Q h | l(Z) ⊲ Z l) → νl 1 , l 2 . addG(Par P Q l) Proof. Let us consider the barbs. Since a process of the form (KillM a l) or (a(X, \l) ⊲ l (h)Msg a X h | Rew l) does not show any barbs, then the barbs of C[T (l, a)] and C[0] coincide.Let us consider the reductions. If the context evolves by itself, the reduction is banally matched. If T (l, a) = (KillM a l) then the only possible reduction is the applicationC[(KillM a l)] ⇁ C[(a(X, \l) ⊲ l (h)Msg a X h | Rew l)] which is matched by C[0] by staying idle. If in C[(a(X, \l)⊲l (h)Msg a X h | Rew l)]the hole process and the context interact, it is because there is a message of the form a P , l in the context. HenceC[(a(X, \l) ⊲ l (h)Msg a X h | Rew l)] ≡ C ′ [a P , l | (a(X, \l) ⊲ l (h)Msg a X h | Rew l)]This implies that also C[0] ≡ C ′ [a P , l ], and by Lemma 17 we know thatC ′ [a P , l ] ≡ C ′′ [a P , l | S] with S = (KillM a l) or S = (a(X, \l) ⊲ l (h)Msg a X h | Rew l). Then C ′ [a P , l | (a(X, \l) ⊲ l (h)Msg a X h | Rew l)] ≡ C ′′ [a P , l | (a(X, \l) ⊲ l (h)Msg a X h | Rew l) | S] ֒→ C ′′ [l (h)Msg a P h | Rew l) | S] ≡ C ′′′ [S]and on the other side we have thatC ′′ [a P , l | S] ֒→ * C ′′ [l (h)Msg a P h | Rew l] ≡ C ′′′ [0]and we remain in the same relation, as desired.Lemma 68. For any HOπ + process P ≡ νã. P ′ , the relation R = {νã. P ′ , νã. (P ′ | ν b. Q)} with Q a parallel composition of processes as in Definition 15 is a weak bf barbed bisimulation.

  R -1 are strong (resp. weak) bf barbed simulations. We call strong (resp. weak ) bf barbed bisimilarity, denoted by

	• ∼ (resp. (resp. weak) bf barbed bisimulation. The largest congruence included in • ≈), the largest strong • ∼ (resp. • ≈) is called strong (resp. weak ) bf barbed congruence and is denoted
	by

  The context can interact with the hole by reading messages on l 1 or l 2 . By Lemma 54 only processes generated by a Rew, by a KillP, or by a Mem can read this kind of messages. Let us consider the Rew case. We have that nf(P 1

  which satisfies again condition[START_REF] Bennett | Notes on the history of reversible computation[END_REF]. The other cases are similar.IfP l = l P | Rew l then E[νl. l P | Rew l | S]can perform several reductions. If Rew l is applied, then we stay in the same case. If Rew l is already in its applied form then E[νl. l P | l(Z)⊲Z l | S] ֒→ E[νl. P l | S],

Partly funded by the ANR-11-INSE-007 project REVER.

Partly funded by the ANR-2010-BLAN-0305-01 project PiCoq.

Axioms Ax.C and Ax.A extend respectively the commutativity and associativity of the parallel composition operator to the translation. Axioms Ax.P and Ax.Adm capture the effect of some auxiliary reductions. Axiom Ax.Unfold captures the property of the translation of rhoπ processes of being able to rollback by sending their own code on their key channel.

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

The congruence ≡ Ex captures the effect of rhoπ structural congruence ≡ on normal form of translations. The congruence ≡ Ex is not influenced by garbage introduced by function addG(•).

Lemma 15. If nf(P ) ≡ Ex nf(P ′ ) then for each Q ∈ addG(P ) there exists Q ′ ∈ addG(P ′ ) such that nf(Q) ≡ Ex nf(Q ′ ).

Proof. See Appendix C.1.

We now prove two invariants on the form of well formed HOπ + processes, useful to study properties of the function addG(•).

If a translation contains a message on a key channel l, then the process contains also the term Rew l.

Lemma 16 (Rew Invariant). If P ′ is well formed and P ′ ≡ C[l R ] with l ∈ K for some n-ary context C then P ′ ≡ C ′ [l R | S] with S = Rew l or S = l(Z) ⊲ Z l for some n-ary context C ′ .

Proof. See Appendix C.1.

Observations

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

Barbs are preserved by administrative steps. Proof. By induction on the length of the derivation of P ≡ Q, with a case analysis on the last applied axiom. All the cases are easy.

The same holds for axioms in ≡ Ex .

Proposition 1. The relation R = {(P, Q) | P ≡ Ex Q} where P, Q are HOπ + processes is a weak bf barbed bisimulation.

Proof. See Appendix C.3.

Appendix A.1. Proofs of Section 2. [START_REF] Frank | Introduction to reversible computing: motivation, progress, and challenges[END_REF] We prove in this section the Consistency Preservation Lemma. We need a few auxiliary results first. The lemma below gives a syntactic characterization of forward reductions.

Lemma 36. Let M , N be configurations. Then M ։ N iff M ≡ M ′ and N ′ ≡ N with:

Proof. Let us start with the if direction. The proof is by induction on the derivation of the reduction ։. We have a case analysis on the last applied rule:

with N ′′ ≡ M 1 | N as desired. The case of right parallel context is similar.

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

The thesis then follows by applying rule (R.Eqv).

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

Lemma 37. Let M , N be configurations. Then M N iff M ≡ M ′ and N ′ ≡ N with:

Proof. Similar to the proof of Lemma 36.

We can now prove Lemma 3.

Lemma 3 (Consistency preservation).

Let M be a consistent configuration. If M → N then N is a consistent configuration.

Proof. The proof proceeds by case analysis on the derivation of M → N .

Let us consider the case M ։ N . By Lemma 36 we have M ≡ M ′ and

. By hypothesis M is a consistent configuration, thus M ′ is also consistent (consistency is preserved by ≡ since it is defined up to ≡ itself). have to prove that N ′ is consistent. The properties 1-4 of Definition 1 check uniqueness of keys. They are all satisfied for existing tags, and they are satisfied by the new tag k since it is a fresh key. The condition 5 holds for the new memory [κ 1 : a P | κ 2 : a(X) ⊲ Q; k] because of the form of the continuation. It holds for the other memories by hypothesis. Note that the condition on memories that generated the two threads identified by κ 1 and κ 2 participating to the communication still holds, since the two threads are just moved from an active context to a memory.

The case M N is similar to the previous one, using Lemma 37 instead of Lemma 36.

Appendix A.2. Proofs of Section 2.4

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

Proof. It is enough to prove that the thesis holds for each axiom (since γ is defined by structural induction). We have a case for each axiom. For the rules E.ParC, E.ParA, E.NilM, E.NewN, E.NewC, E.NewP and E.α there is a corresponding rule in HOπ. Rules E.TagN and E.TagP instead reduce to the identity.

Proof. Since both ≡ π and ≡ are equivalence relations, it is enough to show the thesis for derivations of length one. The idea is that each axiom applied on HOπ processes can be applied to each corresponding rhoπ configuration. This may require additional applications of axioms to deal with the additional rhoπ structure. For instance, lifting axiom E.NewC may require additional applications of the same axiom to deal with restrictions on keys. We do not report the detailed case analysis.

We can finally prove the inverse of Lemma 4.

Lemma 5. For all closed HOπ processes R, S if R → π S then for all closed configurations M such that γ(M ) = R there is N such that M ։ N and γ(N ) = S.

Proof. By induction on the derivation of the reduction → π .

Then by inductive hypothesis there is M ′′ such that M ′ ։ M ′′ and γ(M ′′ ) = S ′ . By applying again Lemma 40 we know that there is M ′′′ such that M ′′′ ≡ M ′′ and γ(M ′′′ ) = S. The thesis follows by applying rule (R.Eqv).

Ctx:

Thus the thesis follows by inductive hypothesis using rule (R.Ctx).

Appendix B.1. Proofs of Section 3.1

We prove in this section that rhoπ is causal consistent.

Lemma 9 (Square Lemma).

-→ M 2 are two coinitial concurrent transitions, then there exist two cofinal transitions

Proof. By case analysis on the form of transitions t 1 and t 2 .

Since the two transitions are concurrent (by hypothesis) we have that {κ 1 , κ 2 , k} ∩ {κ ′ 1 , κ ′ 2 , k ′ } = ∅. Thus, we have:

as desired. Appendix B.2.1. Labelled transition system semantics for choπ In [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF], Boreale and Sangiorgi do not define their causal π-calculus via a reduction semantics but with a labelled transition system. To show that our notion of causal process indeed corresponds to that of Boreale and Sangiorgi, we present here a labelled transition system semantics for choπ directly adapted from [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF] to our higher-order context. We then prove that the labelled transition system semantics and the reduction semantics for choπ are in agreement.

The labelled transition system semantics of choπ is given in Figure B.10, where α ranges over channel names a and their complements of the form a. The rules in Figure B.10 are a direct adaptation of the rules in [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF] to the asynchronous higher-order π, with the use of concretions and abstractions, following Milner and Sangiorgi [START_REF] Milner | Communicating and mobile systems -the π-calculus[END_REF][START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF]. A concretion takes the form νã. P A, where ã ⊆ fn(P ). An abstraction takes the form (X)A. We use C, D and their decorated variants to range over concretions, and F, G and ther decorated variants to range over abstractions. We call agent an abstraction, a concretion or a causal process, and by abuse of notation, we also use A, B and their decorated variants to range over agents. The application operator • is defined by the following rule (where by convention ã ∩ fn(A) = ∅):

The agreement between the two semantics is given by the following result.

The proof of this proposition is long but completely standard. We give details below.

Note that, thanks to the agreement with the reduction semantics, A ↓ α if and only if

We prove in this section the equivalence between the labelled transition system semantics and the reduction semantics for choπ. We start with a few additional notions used in the proofs.

We extend the structural congruence relation ≡ to agents using the additional rules below (considering that rule E.α extends to agents as well):

An easy induction on the derivation of A ≡ B gives us the following lemmas.

Lemma 41. For all agents A, B and process P , if A ≡ B then A{ P / X } ≡ B{ P / X }.

Lemma 42. For all agents A, B, A ≡ B implies A{ K / k } ≡ B{ K / k }.

Using Lemma 42, an easy induction on the structure of a causal process gives us the following lemma: Lemma 43. For all causal processes A, k ∈ K, (K ::

Proof. Let F = (X)A and C = νc. P B. We compute:

A ′ gives us the following lemma:

Lemma 46. For any causal process A, and any keys

We can then prove the main lemmas towards the agreement proposition:

Proof. The proof is lengthy but completely standard. It proceeds by induction on the derivation of B ≡ A. We just detail the non-classical cases arising from the rules in Figure 4.

• (E-par): in this case, A = K ′ ::

A ′′ can only have been derived via (E-parl) or (E-parr). We check only the case (E-parl) as the other is similar. We thus have

Using rule (Cau), we now have

By (E-par), we have K ′ ::

, and thus we have found

• (E-Cau): in this case, A = K 1 ::

A ′ can only have been derived via (Cau), with K 2 ::

In turn, the latter transition can only have been obtained via (Cau), with

, and thus we have found

• (E-res): in this case, A = K ′ :: νa. A 1 and B = νa. K ′ ::

In turn, the latter transition can only have been derived via (Res), with

1 , and using (Res) we get

By (E-res) we get νa. K ′ ::

, and thus we have found B ′ = νa. K ′ ::

• (E-nil): in this case, A = ∅ ::

Proof. The proof proceeds by induction on the derivation of A ≡ B. Again, we give details only for the non-classical cases arising from the rules in Fig- • (E.par): in this case, A = K ::

and A ′ = K :: A ′′ . In turn, the latter transition could only have been derived via (T-parl), (T-parr), (Coml), or (Comr). We check the different cases:

-(T-parr): this case is similar to the (T-parl) one. Lemma 42 and Lemma 45, we get B ′ ≡ (K :: F • C){ K∪K 1 / k } and by Lemma 43 (note that k ∈ K for k must not be in fk(K :: A 1 , K :: A 2 ) for applying (Coml), a condition which can always be met thanks to Lemma 46)

-(Comr): this case is similar to the (Coml) one.

• (E-Cau): in this case, A = K 1 :: K 2 ::

1 and by (E-cau) we get B ≡ K 1 :: K 2 :: A ′ 1 = A ′ , as required.

• (E-res): the reasoning proceeds like above, exploiting (Res) and (Eres).

• (E-nil): immediate.

Lemma 49. For all causal processes A, the following properties hold:

as required (noting that X is not free in B 2 and that k ∈ fk(B 1 , B 2 ) for k ∈ fk(A 1 , A 2 )).

• (Comr): this case is proved like the (Coml) one.

We can finally prove the agreement proposition itself:

Proof. The only if part is a direct consequence of Lemma 49 [START_REF] Frank | Introduction to reversible computing: motivation, progress, and challenges[END_REF]. For the if part, we reason by induction on the derivation of A → A ′ :

We can apply (Out) followed by (Cau) to get

We can apply (In) followed by (Cau)

and applying (Coml) we get: • closure by evaluation context: in this case we reason by induction on the form of evaluation context E:

-E = •: this is the case (C-red) above.

- Before proving Lemma 13 below, which concerns configurations, we prove a corresponding result on processes.

Lemma 50. For all names k and rhoπ processes P , Q, if

Proof. By induction on the derivation of P ≡ Q. The only interesting case is the base one, corresponding to the application of an axiom. We have a case analysis on the applied axiom. We consider just the most interesting cases.

Otherwise

as desired, where we used axiom Ax.C.

If at least one among P , Q and R is equivalent to 0 the thesis banally follows. Otherwise

as desired, where we used axiom Ax.A.

Proof. By induction on the derivation of M ≡ N . The only interesting case is the base one, corresponding to the application of an axiom. If the axiom is applied to a process only, the thesis follows from Lemma 50 and from the observation that processes are always applied to keys. We show below the most interesting of the other cases:

κ : νa. P ≡ νa. κ : P . We distinguish two cases, depending on the form of κ.

The other case is simpler.

for computing the substitution applied to the bullet. The result is also a pair (C ′ [•], σ). The function nfc(C[•], σ) is defined as follows:

This definition enables the lemma below.

The notions of normal form for processes and for contexts are compatible.

Proof. By structural induction on C[•]. We show a few cases as examples:

By inductive hypothesis we have that nf(C

1 , σ, and we can conclude by noting that nfc

). By inductive hypothesis we have that nf(C

/ X }, and we can conclude by stating that

X }, since the substitution will take place in non active contexts.

Substitutions preserve structural congruence ≡ Ex .

Lemma 53. For any substitution

Proof. The proof is trivial for name substitutions. For higher-order ones the proof is by induction on the derivation of M ≡ Ex N , with a case analysis on the last applied axiom of ≡ Ex . All the cases are easy. Lemma 14. If P and Q are well formed and P ≡ Ex Q then nf(P ) ≡ Ex nf(Q).

Proof. Let us consider P and Q generated by the encoding of Figure 7 where instead of having Trig processes, we substitute them with their normal form. Thus we can apply Lemma 52. Let us consider one application of an axiom. We have that P

Lemma 15. If nf(P ) ≡ Ex nf(P ′ ) then for each Q ∈ addG(P ) there exists

Proof. By definition of addG we have that P ≡ E[0] and

. By using Lemma 52 we have that some n-ary context C then P ′ ≡ C ′ [a P , l | S] with S = (KillM a l) or S = (a(X, \l) ⊲ l (h)Msg a X h | Rew l) for some n-ary context C ′ .

Proof. By inspection of the encoding of Figure 7 we note that a message of the form a P , l is only generated in the Msg process, together with the corresponding KillM. Also, interaction with a KillM is the only way to remove such a message. The case analysis is similar to the one in Lemma 16.

Lemma 18. Let P be a well formed HOπ + process and Q ∈ addG(P ). If nf(Q) ֒→ Q ′ then there exists P ′ such that P ֒→ * P ′ with Q ′ ∈ addG(P ′ ).

Proof. The reduction nf(Q) ֒→ Q ′ is due to a communication since processes in normal form have no enabled applications.

We distinguish two cases: either the reduction ֒→ is due to the process nf(P ) only or it involves garbage added by addG.

Let us consider the first case. By definition we have

where R is the garbage added by the function addG. The form of Q is preserved by the nf(•) function, where all the applications are executed.

Moreover we have that P ⇁ * E ′ [0] ֒→ E ′′ [0] and we are done.

In the second case, the only garbage processes that may interact with the context are either a (Rew l) process or a (KillM a l) process (the other garbage processes are inactive). If the administrative step is due to the applied form of (Rew l) then by Lemma 16 the context E contains a message on the channel l, that is nf

But since P is well formed and since the process l(Z) ⊲ Z l has been added by the addG function, by Lemma 16 we have that also

Proof. By induction on the structure of P . We show only the most interesting cases: P = a(X) ⊲ P ′ : be Y = (X c)c P ′ , we have that

By inductive hypothesis we have that P 1 h ֒→ * ν ũ. h P ′

1

| S 1 with P 1 ≡ ν ũ. P ′ 1 and P 2 l ֒→ * ν ṽ. l P ′

2

| S 2 with P 2 ≡ ν ṽ. P ′ 2 . Hence we have

, and by garbage collecting names h, l we have P ≡ ν ũ, ṽ. (P ′ 1 | P ′ 2 ) as desired.

Lemma 24. For any rhoπ process R, if R l ⇒ P then the following conditions hold:

and we can conclude since (l)(Par

For the inductive case, either the message we are considering disappears, and then there is nothing to prove, or the message remains in the context and we can conclude by applying the inductive hypothesis. Note, in fact, that higher order variables are always replaced by translations of rhoπ processes, and that variables are never at top level inside the messages with subject l above.

Lemma 25. If nf(P 1 ) ≡ Ex nf(P 2 ) and nf(P 1 ) → P ′ 1 then nf(P 2 ) ⇒ nf(P ′ 2 ) with nf(P ′′ 1 ) ≡ Ex nf(P ′ 2 ) and

Proof. By case analysis on the used axiom P ≡ Ex Q and on the structure of nf(P 1 ). Since we are dealing with processes in normal form, → is a communication. Hence we can express nf(P 1 ) as an active context E[a R | a(X) ⊲ S] (the cases where the trigger has different forms are similar). We will just consider a few interesting cases, the remaining ones are similar. The second part follows by noticing that in the proofs below the same trigger is used to mimic the reduction (possibly together with some auxiliary reductions).

There are four places where the axiom could be applied: in the context, inside the message content, inside the trigger continuation, or to the context hole. We will consider the second case as an example.

We have that nf(P 1 ) can be written as

and we can conclude by applying Lemma 14.

Ax.C. We have that nf

Lemma 56. For any rhoπ process P and any l ∈ n( P ) ∩ K, we have P = C[(l)P l ] for some primitive context C and some l-process P l .

Proof. By structural induction on P .

All the messages on channels a ∈ N carry a pair whose first element is the translation of a process. Lemma 57. For any rhoπ process P , if

Proof. By induction on the number of steps in ⇒. The base case is proved by inspection. The inductive case is easy.

We can now prove the invariant on the use of keys.

Lemma 58. For any configuration νk. k : P if k : P ⇒ R then for any key l occurring in R one of the following statements holds:

where P l is an l-process and S is obtained from one of the following terms via 0 or more applications: (KillP l l ′ h), (KillP l ′ l h), (Mem Y a P l 1 l l 2 ), 0. 2. R ≡ C[νh. C ′ [(l)P l ]h] where P l is an l-process and C ′ is generated from a primitive context via 0 or more applications.

R ≡ C[νl. ((h)P h )l]

where P h is an h-process.

Proof. By induction on the number of steps in k : P ⇒ R. For the base case (n = 0) we have that νk. k : P = νk. P k. By Lemma 56 we have that for any l ∈ n( P ) ∩ K we have P = C ′ [(l)P l ], that is for any l we can write νk. P k ≡ νk. C ′ [(l)P l ]k, and condition (2) holds.

In the inductive case we distinguish two possibilities: either name l did not exist at the previous step, or it existed. By inspection of the encoding one can see that the first case may only happen when recursive definitions for Par or Trig are unfolded. In both the cases condition (1) is satisfied for new names, with P l = P l in the first case and P l = νc. c P | (c(Z)⊲Z l) | (Mem Y a P l 1 l l 2 ) in the second case.

For the second possibility we have a case analysis according to which condition holds before the additional step is done.

where condition (1) holds for name l. Note that condition (1) holds also for the new name k.

If P l = Par P Q l then we have that E[νl.

and we have that condition (1) is still satisfied by name l and also by the new names h and k.

If P l = KillP h k l and it reduces alone then it is applied, and condition (1) still holds. P l may interact with the context only if it is in its applied form and there are two messages, one on h and one on k. Thanks to Lemma 55 they should contain translations of processes, thus:

and condition (1) still holds.

If P l = νu. P l then we can move the restriction into the context and reduce to the case P l = P l.

] then E[νl. (P l | S)] can perform several reductions. If the Mem process is applied then condition (1) is still satisfied. Since c and l are restricted, the only other possible reduction is the application of Y = (X c)c Q . Thus:

and condition (1) still holds. The case where the memory is in its applied form is analogous.

If P l = νc. c P | (c(Z) ⊲ Z l) | (Mem Y a P l 1 l l 2 ) and the Mem process is applied then condition (1) holds. Since c and l are restricted, the only possible communication is the internal one along c:

where condition (1) still holds. The case where the memory is in its applied form is analogous.

Then we have:

and by using Lemma 23 and Lemma 55 (to ensure that processes P 1 and Q have no toplevel restrictions) we have:

To have a correspondence with P , we have to show that names h and l were restricted also in P , and with the same scope. By using Lemma 58 we have that

If the communication is an internal communication in a trigger, we have that

Before proving Lemma 29 we show that barbs are preserved by the encoding.

Proof. Easy, by definition of barbs and of the encoding.

.12: Correspondence schema of barbs (numbers refer to Lemmas).

Proof. By Lemma 59 we have that if M ↓ a then nf( M ) ↓ a . By definition of normal form we have that M ⇁ * nf( M ), and by hypothesis we have that M ֒→ * Q. Using Lemma 27 we have that nf(M

Moreover, by Lemma 28 there exist Q ′′ and P ′ such that Q ′ ֒→ * Q ′′ , P ′ ∈ addG(nf( M )) and nf(P ′ ) ≡ Ex nf(Q ′′ ). Since addG and ≡ Ex do not remove barbs we have nf(Q ′′ ) ↓ a as desired. The proof is graphically depicted in Figure C.12.

Before proving Lemma 30 below we prove some auxiliary results. Applications never remove barbs.

Lemma 60. For any HOπ + process P , if P ↓ a and P ⇁ Q, then also Q ↓ a .

Proof. From the definition of ↓ a and of ⇁.

Administrative steps do not add barbs.

Lemma 61. For each consistent configuration M such that νk. k :

Proof. By hypothesis M ֒→ * Q with Q ↓ a , and by definition M ⇁ * nf( M ). By applying Lemma 27 we get

Since Q ↓ a , and since applications (⇁) do not remove barbs (by Lemma 60), we also have that Q ′ ↓ a . The above reasoning is depicted in Figure C.13.

We have to show that if Q ′ has a barb then nf( M ) has the same barb. Since νk. k : P ⇒ M then fn(M ) ∩ K = ∅ and also fn(Q) ∩ K = ∅ (by Lemma 22). Thus we have no need to consider barbs in K.

Let us consider reductions. We consider only challenges from the left, since the reasoning is analogous for challenges from the right. If the process C[P 1 , .., P n ] does a reduction, it is because either the context evolves by itself, or one of the hole processes reduces by itself, or because of an interaction between the context and one hole (no interaction between holes is possible).

If the context performs a reduction by itself, that is

Note that the number of holes may change because of the reduction.

Let us consider reductions in one hole. If C[P 1 , .., (KillP l h k), ..,

and we are still in the same relation.

Let us consider interactions between the context and one hole. For C[P 1 , .., a(X)|b(Y )⊲R, .., P n ] to reduce, we need in the context two messages of the form a S 1 and b S 2 . If so, we have that

Since identity is included in R (it suffices to consider a 0-ary context), and since (S i , S ′ i ) ∈ R (since they are subterms) we have (R{

Before proving the lemma concerning axiom Ex.P we prove as auxiliary result that the function addG does not introduce barbs.

Lemma 64. For any HOπ + process P , if addG(P ) ↓ a then P ↓ a .

Proof. Easy, by looking at the definition of addG (Definition 15). Lemma 65. Applications of axiom Ex.P and of its normal form to well formed HOπ + processes are correct with respect to weak bf barbed bisimulation.

Proof. Note that the axiom Ex.P alone is not correct, since the left term has barbs at l 1 and l 2 which are not matched by the right term. However, in well formed processes keys are always bound. We show below that applications of the axiom and of its normal form to well formed processes are always correct.

Thanks to Lemma 58 restrictions on l 1 and l 2 may occur only in processes of some forms. In particular, the only possibility is that for both l 1 and l 2 case (1) applies. Thus the process to which the axiom is applied is of the and on the other side we have that:

and since the identity is contained in the relation, we are still in the same relation. In the last case, since we only consider well formed processes, thanks to Lemma 24 there are no two KillP processes waiting on the same channels. Thus the context may not interact with the hole, and this case will never happen.

Before proving the lemma concerning axiom Ex.A we prove as auxiliary result that the function addG has no impact on weak bf barbed bisimulation. We show the result for each form of garbage, and compose the partial results together in Lemma 68. Q n = KillM a l: similar to the case above, using Lemma 67 instead of Lemma 66.

Q n = νt. (a(X, k)|t ⊲ Q): trivial, since the process cannot interact.

Q n = νc, t. (KillT ((X)c P )) t l a): trivial, since the process reduces to a process that cannot interact.

Lemma 69. Axiom Ex.A and its normal form are correct with respect to weak bf barbed bisimulation.

Proof. Let S(l 1 , l 2 , l 3 ) denote either a process of the form S(l 1 , l 2 , l 3 ) = (KillP l 1 l 2 l 3 ) or of the form S(l Let us now consider reductions. All the reductions performed by the context are banally matched. Also, since all the relations are closed under the applications of auxiliary processes such as T l or S(l 1 , l 2 , l 3 ) we will not mention them. Let us consider the different relations.

In R 1 the only possibility is that the process S(l 1 , l 2 , l ′ ) = (l 1 (Z)|l 2 (W ) ⊲ l ′ (h)Par Z W h ) interacts with two messages on l 1 and l 2 in the context. We can assume they are of the form l 1 P and l 2 Q , thus the reduction leads to R 2 . From R 2 two reductions are possible: the process can interact with the context by reading a message on l 3 of the form l 3 R , or the message on l ′ may interact with T l ′ . In the first case we obtain l (h)Par P | Q R h | T l . On the right side we obtain T l | l (h)Par P Q | R h . We can move to the context T l , which occurs on both the sides, and also the message context, the application context and the abstraction context going to R 6 . In the second case we go directly to R 3 .

In R 3 the only possible reduction is the application of the Par, leading to R 4 .

Also in R 4 the only possible reduction is an application, leading to R 5 .

In R 5 both P h 1 and Q h 2 may reduce by means of an application. Note that the right process weakly reduces to the left one. In fact, since contexts are well formed there exist in the term two Rew processes, one on l 1 and one on l 2 . Hence we have that

Since each process R is weak bf barbed bisimilar to addG(R) (by Lemma 68), we conclude by transitivity, noting that by removing the addG function we get back to the relation R 1 .

From R 6 we can only move to R 7 by applications. From R 7 there are two possible reductions, either the application of P | Q l 1 or the application of R l 2 . In the first case we get back to the relation R 1 (by using α-conversion). In the second case we can execute on the right the application Q | R l 2 , and obtain a process of the form R l 2 (using α-conversion) also on the right. We can thus move these processes to the context, going to the relation R 8 .

From R 8 , the left process can only perform the application on P | Q , and we get back to the relation R 1 (the right process matches this challenge by a 0 steps computation). Lemma 70. Axiom Ex.U nf old and its normal form are correct with respect to weak bf barbed bisimulation.

Proof. Let T l denote a process of the form

We now show that the relation R is a weak bf barbed bisimulation.

Let us consider barbs. Since P l is an application then the only barbs shown by a process of the form C[P 1 , .., P n ] are those shown by the context. The same barbs are shown also by the process C[Q 1 , .., Q n ]. On the other hand, a process of the form l Q shows a barb at l. By using Lemma 23 we have that P l ֒→ * ν ṽ. l Q | Rew l | S, with S a parallel composition of garbage processes and l ∈ ṽ. Thus, P l has a weak barb at l too.

Let us consider reductions. On both sides, reductions done by the context are trivially matched. The only possible reduction for a hole process of the form P l is an application. Then, we have a case analysis on the form of P . If P = νa. P ′ , then C[P 1 , .., νa. P ′ l, .., P n ] ⇁ * C[P 1 , .., νa. P ′ l, .., P n ], and this step is mimicked by the process C[Q 1 , .., ν ũ. l Q , .., Q n ] by staying idle, since we can extract name a from the set ũ. If P = P ′ | P ′′ , we have that

This step can be matched by

and we are still in the same relation since:

The other cases are similar.

If the step is performed by the process on the right, we have three cases. The application of a process Rew l can be matched by the left process by staying idle. An interaction between (l(Z)⊲Z l) and a message on l is matched since C[Q 1 , .., ν ũ. l Q | l(Z) ⊲ Z l, .., Q n ] → C[Q 1 , .., ν ũ. Q l, .., Q n ] and we are still in the same relation. For applications of Q l we proceed by case analysis as before and we remain in the same relation, as desired. Proof. By definition P ≡ Ex Q iff there are P 1 , . . . P n such that P ≡ Ex P 1 ≡ Ex . . . ≡ Ex P n ≡ Ex Q where each equivalence is obtained by applying just one axiom. The proof is by induction on n. The base case is banally verified. In the inductive case we proceed by case analysis on the last applied axiom.

Let us consider axiom Ex.C. By inductive hypothesis we have that P ≡ Ex P n implies that P Proof. By structural induction on M . If M is a simple process such as 0, a message or a trigger there is nothing to verify since nf( M ) ։.

In the inductive case, if M is of the form νa. M 1 then by definition of nf(•) and • we have that nf( M ) = νa. nf( M 1 ) and by applying the inductive hypothesis on nf( M 1 ) we have that nf( M 1 ) ։ P implies M 1 ։ M ′ 1 with P ֒→ * P ′ and nf(P ′ ) = nf(Q ′ ) with Q ′ ∈ addG( M ′ 1 ). If νa. M 1 ։ νa. P then also M 1 ։ P and using inductive hypothesis we obtain νa. M 1 ։ νa. M ′ 1 with νa. P ֒→ * νa. P ′ and since nf(P ′ ) = nf(Q ′ ) with Q ′ ∈ addG( M ′ 1 ) we also have that νa. nf(P ′ ) = νa. nf(Q ′ ) that is nf(νa. P ′ ) = nf(Q ′′ ) with Q ′′ ∈ addG( νa. M ′ 1 ), as desired. The case of parallel context M = M 1 | M 2 also follows by inductive hypothesis if the 117 reduction is done inside either M 1 or M 2 . If both M 1 and M 2 contribute to the reduction then we can assume that there is a message in M 1 and a trigger in M 2 able to communicate. For the sake of brevity, we consider just the case in which both message and trigger are tagged by a key. The other cases are similar. We can write

Hence, we have

Let Y = (X c)c Q , then we have that

By using Lemma 21 (Substitution Lemma) the process above is equal to:

We have that M ։ M ′ with M ′ = M ′ 1 | νk. k : Q{ R / X } | M ′ 2 and we can easily see that P ⇁ * nf(

2 ) ≡ nf(Q ′′ ) with Q ′′ ∈ addG( M ′ ), as desired.