Ivan Lanese

Jorge A Pérez

Davide Sangiorgi

Alan Schmitt

On the Expressiveness and Decidability of Higher-Order Process Calculi $,$$

Keywords: Process calculi, Higher-order communication, Bisimulation, Expressiveness

In higher-order process calculi, the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process output, and parallel composition. By exhibiting a deterministic encoding of Minsky machines, the calculus is shown to be Turing complete. Therefore its termination problem is undecidable. Strong bisimilarity, however, is shown to be decidable. Furthermore, the main forms of strong bisimilarity for higher-order processes (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide. They also coincide with their asynchronous versions. A sound and complete axiomatization of bisimilarity is given. Finally, bisimilarity is shown to become undecidable if at least four static (i.e., top-level) restrictions are added to the calculus.

Introduction

Higher-order process calculi are calculi in which processes (more generally, values containing processes) can be communicated. Higher-order process calculi have been put forward in the early 1990s, with CHOCS [START_REF] Thomsen | A calculus of higher order communicating systems[END_REF] and Plain CHOCS [START_REF] Thomsen | Plain CHOCS: A second generation calculus for higher order processes[END_REF], the Higher-Order π-calculus [START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higherorder paradigms[END_REF], and others. The basic operators are usually those of CCS: parallel composition, input and output prefix, and restriction. Replication and recursion are often omitted as they can be encoded. However, the possibility of exchanging processes has strong consequences on semantics: in most higher-order process calculi, labeled transition systems must deal with higher-order substitutions and scope extrusion, and ordinary definitions of bisimulation and behavioral equivalences become unsatisfactory as they are over-discriminating (this point is discussed later in more detail). Higherorder, or process-passing, concurrency is often presented as an alternative paradigm to the first order, or name-passing, concurrency of the π-calculus for the description of mobile systems. Higher-order calculi are inspired by, and are formally closer to, the λ-calculus, whose basic computational step -β-reduction -involves term instantiation. As in the λ-calculus, a computational step in higher-order calculi results in the instantiation of a variable with a term, which is then copied as many times as there are occurrences of the variable, resulting in potentially larger terms.

The expressiveness of higher-order communication has received little attention in the literature. Higher-order calculi (both sequential and concurrent) have been compared with first-order calculi, but mainly as a way of investigating the expressiveness of π-calculus and similar formalisms. Thomsen [START_REF] Thomsen | Calculi for higher order communicating systems[END_REF] and Xu [START_REF] Xu | On the bisimulation theory and axiomatization of higher-order process calculi[END_REF] have proposed encodings of π-calculus into Plain CHOCS. These encodings make essential use of the relabeling operator of Plain CHOCS. Sangiorgi and Walker's encoding of a variant of π-calculus into Higher-Order π-calculus [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF] relies on the abstraction mechanism of the Higher-Order π-calculus (it needs ω-order abstractions). Another strand of work on expressiveness (see, e.g., [START_REF] Phillips | Symmetric electoral systems for ambient calculi[END_REF][START_REF] Gorla | On the relative expressive power of calculi for mobility[END_REF]) has looked at calculi for distributed systems and compared different primitives for migration and movement of processes (or entire locations), which can be seen as higher-order constructs.

The goal of this paper is to shed light on the expressiveness of higher-order process calculi, and related questions of decidability and of behavioral equivalence.

We consider a core calculus of Higher-Order processes (briefly HOcore), whose grammar is: P ::= a(x). P | a P | P P | x | 0 An input prefixed process a(x). P can receive on name (or channel) a a process that will be substituted in the place of x in the body P ; an output message a P can send P on a; parallel composition allows processes to interact. We can view the calculus as a kind of concurrent λ-calculus, where a(x). P is a function, with formal parameter x and body P , located at a; and a P is the argument for a function located at a. HOcore is minimal, in that only the operators strictly necessary to obtain higher-order communications are retained. For instance, continuations following output messages have been left out. More importantly, HOcore has no restriction operator. Thus all channels are global, and dynamic creation of new channels is impossible. This makes the absence of recursion/replication also relevant, as known encodings of fixed-point combinators in higher-order process calculi exploit the restriction operator to avoid harmful interferences (notably for nested recursion).

Even though HOcore is minimal, it remains non-trivial: in Section 3, we show that it is Turing complete, therefore its termination problem is undecidable, by exhibiting a deterministic encoding of Minsky machines [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF]. The cornerstone of the encoding, counters that may be tested for zero, consist of nested higher-order outputs. Each register is made of two mutually recursive behaviors capable of spawning processes incrementing and decrementing its counter.

We then turn to the question of definability and decidability of bisimilarity. As hinted at above, the definition of a satisfactory notion of bisimilarity is a hard problem for a higher-order process language, and the "term-copying" feature inherited from the λ-calculus can make the proof that bisimilarity is a congruence difficult. In ordinary bisimilarity, as in CCS, two processes are bisimilar if any action by one of them can be matched by an equal action from the other in such a way that the resulting derivatives are again bisimilar. The two matching actions must be syntactically identical. This condition is unacceptable in higher-order concurrency; for instance it breaks fundamental algebraic laws such as the commutativity of parallel composition. Alternative proposals of labeled bisimilarity for higher-order processes have been put forward. In higher-order bisimilarity [START_REF] Thomsen | Calculi for higher order communicating systems[END_REF][START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higherorder paradigms[END_REF], one requires bisimilarity, rather than identity, of the processes emitted in a higher-order output action. This weakening is natural for higher-order calculi and the bisimulation checks involved are simple. However, higher-order bisimilarity is often over-discriminating as a behavioral equivalence [START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higherorder paradigms[END_REF], and basic properties, such as congruence, may be very hard to establish. Context bisimilarity [START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higherorder paradigms[END_REF][START_REF] Jeffrey | Contextual equivalence for higher-order pi-calculus revisited[END_REF] avoids the separation between the argument and the continuation of an output action, this continuation being either syntactically present or consisting of other processes running in parallel. To this end, it explicitly takes into account the context in which the emitted process is supposed to go. Context bisimilarity yields more satisfactory process equalities and coincides with contextual equivalence (i.e., barbed congruence). A drawback of this approach is the universal quantification over contexts in the clause for output actions, which can hinder its use in practice to check equivalences. Normal bisimilarity [START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higherorder paradigms[END_REF][START_REF] Jeffrey | Contextual equivalence for higher-order pi-calculus revisited[END_REF][START_REF] Cao | More on bisimulations for higher order pi-calculus[END_REF] is a simplification of context bisimilarity without universal quantifications in the output clause. The input clause is simpler too: normal bisimilarity can indeed be viewed as a form of open bisimilarity [START_REF] Sangiorgi | The lazy lambda calculus in a concurrency scenario[END_REF], where the formal parameter of an input is not substituted in the input clause, and free variables of terms are observable during the bisimulation game. However, the definition of the bisimilarity may depend on the operators in the calculus, and the correspondence with context bisimilarity may be hard to prove.

In Sections 4 and 5 we show that HOcore has a unique reasonable relation of strong bisimilarity: all the above forms (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide, and they also coincide with their asynchronous versions. Furthermore, we show that such a bisimilarity relation is decidable.

In the concurrency literature, there are examples of formalisms which are not Turing complete and where nevertheless (strong) bisimilarity is undecidable (e.g., Petri nets [START_REF] Jančar | Undecidability of bisimilarity for Petri nets and some related problems[END_REF] or lossy channel systems [START_REF] Schnoebelen | Bisimulation and other undecidable equivalences for lossy channel systems[END_REF]). We are not aware however of examples of the opposite situation: formalisms that, as HOcore, are Turing complete but at the same time maintain decidability of bisimilarity. The situation in HOcore may indeed seem surprising, if not even contradictory: one is able to tell whether two processes are bisimilar, but in general one cannot tell whether the processes will terminate or even whether the sets of their τ -derivatives (the processes obtained via reductions) are finite or not. The crux to obtaining decidability is a further characterization of bisimilarity in HOcore, as a form of open bisimilarity, called IO bisimilarity, in which τ -transitions are ignored.

For an upper bound to the complexity of the bisimilarity problem, we can adapt Dovier et al.'s algorithm [START_REF] Dovier | An efficient algorithm for computing bisimulation equivalence[END_REF] to infer that bisimilarity is decidable in time which is linear in the size of the (open and higher-order) transition system underlying IO bisimilarity. In general however, this transition system is exponential with respect to the size of the root process. We show in Section 6 that bisimilarity in HOcore can actually be decided in time that is polynomial with respect to the size of the initial pair of processes. We obtain this through an axiomatization of bisimilarity, where we adapt to a higher-order setting both Moller and Milner's unique decomposition of processes [START_REF] Milner | Unique decomposition of processes[END_REF] and Hirschkoff and Pous' axioms for a fragment of (finite) CCS [START_REF] Hirschkoff | A distribution law for CCS and a new congruence result for the π-calculus[END_REF].

The decidability result for bisimilarity breaks down with the addition of restriction, as full recursion can then be faithfully encoded (the resulting calculus subsumes, e.g., CCS without relabeling). This however requires the ability of generating unboundedly many new names (for instance, when a process that contains restrictions is communicated and copied several times). In Section 7, we consider the addition of static restrictions to HOcore. Intuitively, this means allowing restrictions only as the outermost constructs, so that processes take the form νa 1 . . . νa n P where the inner process P is restriction-free. Via an encoding of the Post correspondence problem [START_REF] Post | A variant of a recursively unsolvable problem[END_REF][START_REF] Sipser | Introduction to the Theory of Computation[END_REF], we show that the addition of four static restrictions is sufficient to produce undecidability. We do not know what happens with fewer restrictions.

In the final part of the paper we examine the impact of some extensions to HOcore on our decidability results (Section 8), give some concluding remarks, and discuss related work (Section 9).

The Calculus

We now introduce HOcore, the core of calculi for higher-order concurrency such as CHOCS [START_REF] Thomsen | A calculus of higher order communicating systems[END_REF], Plain CHOCS [START_REF] Thomsen | Plain CHOCS: A second generation calculus for higher order processes[END_REF], and Higher-Order π-calculus [START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higherorder paradigms[END_REF][START_REF] Sangiorgi | Bisimulation for Higher-Order Process Calculi[END_REF][START_REF] Sangiorgi | π-calculus, internal mobility and agent-passing calculi[END_REF]. We use a, b, c to range over names (also called channels), and x, y, z to range over variables; the sets of names and variables are disjoint.

P, Q ::= a P output | a(x). P input prefix | x process variable | P Q parallel composition | 0 nil
An input a(x). P binds the free occurrences of x in P ; this is the only binder in HOcore.

We write fv(P ) for the set of free variables in P , and bv(P ) for the bound variables. We identify processes up to a renaming of bound variables. A process is closed if it does not have free variables. In a statement, a name is fresh if it is not among the names of the objects (processes, actions, etc.) of the statement. As usual, the scope of an input a(x). P extends as far to the right as possible. For instance, a(x). P Q stands for a(x). (P Q). We abbreviate the input a(x). P , with x ∈ fv(P ), as a. P ; the output a 0 as a; and the composition P 1 . . . P k as k i=1 P i . Similarly, we write n 1 P as an abbreviation for the parallel composition of n copies of P . Further, P { Q / x} denotes the simultaneous substitution of variables x with processes Q in P (we assume members of x are distinct).

The size of a process is defined as follows.

Definition 2.1. The size of a process P , written #(P ), is inductively defined as:

#(0) = 0 #(P Q) = #(P ) + #(Q) #(x) = 1 #(a P ) = 1 + #(P )
#(a(x). P ) = 1 + #(P )

We now describe the Labeled Transition System, which is defined on open processes. There are three forms of transitions: internal transitions P τ -→ P ; input transitions P a(x) ---→ P , meaning that P can receive at a a process that will replace x in the continuation P ; and output transitions P a P ----→ P meaning that P emits P at a, and in doing so evolves to P . We use α to denote a generic label of a transition. The notion of free variables extends to labels as expected: fv(a P ) = fv(P ). For bound variables in labels, we have bv(a(x)) = {x} and bv(a P ) = ∅.

INP a(x). P a(x) ---→ P OUT a P a P ---→ 0 ACT1 P 1 α -→ P 1 bv(α) ∩ fv(P 2 ) = ∅ P 1 P 2 α -→ P 1 P 2 TAU1 P 1 a P ---→ P 1 P 2 a(x)
---→ P 2 P 1 P 2 τ -→ P 1 P 2 { P /x} (We have omitted ACT2 and TAU2, the symmetric counterparts of the last two rules.) Definition 2.2. The structural congruence relation is the smallest congruence generated by the following laws: P 0 ≡ P , P 1 P 2 ≡ P 2 P 1 , P 1 (P 2 P 3 ) ≡ (P 1 P 2 ) P 3 .

Reductions P -→ P are defined as P ≡ τ -→≡ P . We now state a few results which will be important later. Definition 2.4. A variable x is guarded in P ∈ HOcore (or simply guarded, when P is clear from the context) iff x only occurs free in an output or in subexpressions of P of the form π. P , where π is any prefix. A process P ∈ HOcore is guarded (or has guarded variables) iff all its free variables are guarded.

In particular, notice that if x is guarded in P , then x does not appear in evaluation contexts (i.e., contexts which allow transitions in the hole position), and if x is not free in P then it is guarded in P . For the next lemma, we recall that an output action from an open process may contain free variables, thus α{ R / x} is the action obtained from α by applying the substitution { R / x}. Lemma 2.5. Suppose that P ∈ HOcore and consider some variables x. Then, for all R ∈ HOcore we have:

1. If P α -→ P , with free variables in R disjoint from the variables in P , α, and x, Proof. By induction on the transitions. Lemma 2.6. For every P ∈ HOcore and variable x, there are P ∈ HOcore with x guarded in P and an integer n ≥ 0 such that

then P { R / x} α{ R / x} -----→ P { R / x}; 2. if P { R / x} α --→ M ,
1. P ≡ P n 1 x; 2. P { R /x} ≡ P { R /x} n 1 R, for every R ∈ HOcore.
Proof. By induction on the structure of processes.

HOcore is Turing Complete

We present in this section an encoding of Minsky machines [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF] into HOcore. The encoding shows that HOcore is Turing complete and, as the encoding preserves termination, it also shows that termination in HOcore is undecidable. The encoding is deterministic, i.e., at any step the encoding of any Minsky machine has at most one reduction.

M-INC

i : INC(r j ) m j = m j + 1 m 1-j = m 1-j (i, m 0 , m 1 ) -→ M (i + 1, m 0 , m 1 ) M-DEC i : DECJ(r j , k) m j = 0 m j = m j -1 m 1-j = m 1-j (i, m 0 , m 1 ) -→ M (i + 1, m 0 , m 1 ) M-JMP i : DECJ(r j , k) m j = 0 (i, m 0 , m 1 ) -→ M (k, m 0 , m 1 )

Minsky machines

A Minsky machine is a model composed of a set of sequential, labeled instructions, and two registers. Minsky machines have been shown to be a Turing complete model (see [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF], Chapters 11 and 14), hence termination is undecidable for Minsky machines. Registers r j (j ∈ {0, 1}) can hold arbitrarily large natural numbers. Instructions (1 : I 1 ), . . . , (n : I n ) can be of two kinds: INC(r j ), which adds 1 to register r j and proceeds to the next instruction; DECJ(r j , k), which jumps to instruction k if r j is zero, otherwise it decreases register r j by 1 and proceeds to the next instruction.

A Minsky machine includes a program counter p indicating the label of the instruction being executed. In its initial state, the machine has both registers set to 0 and the program counter p set to the first instruction. The Minsky machine stops whenever the program counter is set to a non-existent instruction, i.e., p > n.

A configuration of a Minsky machine is a tuple (i, m 0 , m 1 ); it consists of the current program counter and the values of the registers. Formally, the reduction relation over configurations of a Minsky machine, denoted -→ M , is defined in Table 1.

Encoding Minsky machines into HOcore

The encoding of a Minsky machine into HOcore is denoted as [[•]] M . In order to simplify the presentation of the encoding, we introduce two useful notations that represent limited forms of guarded choice and guarded replication. Then we show how to count and test for zero in HOcore and present the main encoding, depicted in Table 2.

Guarded choice. We introduce here a notation for a simple form of guarded choice to choose between different behaviors. Assume, for instance, that a i should trigger P i , for i ∈ {1, 2}. This is written as a 1 . P 1 + a 2 . P 2 , whereas the choice of the behavior P i is written as a i .

The notation can be seen as a shortcut for HOcore terms as follows:

Definition 3.1. Let σ = {(a 1 , a 2 ) | a 1 = a 2 } be a fixed set of pairs of distinct names.
The notation for guarded choice can be defined as follows:

INSTRUCTIONS (i : Ii) [[(i : INC(rj))]] M = !pi. ( incj ack. pi+1) [[(i : DECJ(rj, k))]] M = !pi. ( decj ack. (zj. p k + nj. pi+1) REGISTERS rj [[rj = 0]] M = (incj. r S j (| 0 |)j + decj. (r 0 j zj)) REGj [[rj = m]] M = (incj. r S j (| m |)j + decj. (| m -1 |)j) REGj where: REGj = !r 0 j . (ack incj. r S j (| 0 |)j + decj. (r 0 j zj)) !r S j (Y ). (ack incj. r S j r S j Y nj + decj. Y ) (| k |)j = r 0 j nj if k = 0 r S j (| k -1 |)j nj if k > 0.
a 1 . P 1 + a 2 . P 2 a 1 P 1 a 2 P 2 a 1 a 2 (x 2 ). a 1 (x 1 ). x 1 a 2 a 1 (x 1 ). a 2 (x 2 ). x 2
where, in all cases, (a 1 , a 2 ) ∈ σ.

We consider only binary guarded choice as it is sufficient to encode Minsky machines. This way, given a pair (a 1 , a 2 ) ∈ σ and the process a 1 . P 1 + a 2 . P 2 , the trigger a i (with i ∈ {1, 2}) consumes both P i 's and spawns the one chosen, i.e., (a 1 . P 1 + a 2 . P 2 ) a i τ -→ τ -→ P i . This notation has the expected behavior as long as there is at most one message at a guard ( a 1 or a 2 in the previous example) enabled at any given time, and as long as concurrently running guarded choices use distinct names.

Input-guarded replication. We follow the standard definition of replication in higher-order process calculi, adapting it to input-guarded replication so as to make sure that diverging behaviors are not introduced. As there is no restriction in HOcore, the definition is not compositional and replications cannot be nested. Definition 3.2. Assume a fresh name c. The definition of input-guarded replication in HOcore is: !a(z). P (a(z). c(x). x c x P ) c a(z). c(x). x c x P where P contains no replications (nested replications are forbidden).

After having been activated by an output message, replication requires an additional τ step to enable the continuation P , i.e., !a(z). P a(z) ---→ τ -→ (!a(z). P ) P .

Counting in HOcore. The cornerstone of our encoding is the definition of counters that may be tested for zero. Numbers are represented as nested higher-order processes: the encoding of a number k + 1 stored in register j, denoted (| k + 1 |) j , is the parallel composition of two processes: r S j (| k |) j (the successor of (| k |) j ) and a flag n j . The encoding of zero comprises such a flag, as well as the message r 0 j . This way, for instance, (| 2 |) j is r S j r S j r 0 j n j n j n j .

Registers. Registers are counters that may be incremented and decremented. They consist of two parts: their current state and two mutually recursive processes used to generate a new state after an increment or decrement of the register. The state depends on whether the current value of the register is zero or not, but in both cases it consists of a choice between an increment and a decrement. In case of an increment, a message on r S j is sent containing the current register value, for instance m. This message is then received by the recursive definition of r S j that creates a new state with value m + 1, ready for further increment or decrement. In case of a decrement, the behavior depends on the current value, as specified in the reduction relation in Table 1. If the current value is zero, then it stays at zero, recreating the state corresponding to zero for further operations using the message on r 0 j , and it spawns a flag z j indicating that a decrement on a zero-valued register has occurred. If the current value m is strictly greater than zero, then the process (| m -1 |) j is spawned. If m was equal to 1, this puts the state of the register to zero (using a message on r 0 j ). Otherwise, it keeps the message in a non-zero state, with value m -1, using a message on r S j . In both cases a flag n j is spawned to indicate that the register was not equal to zero before the decrement. When an increment or decrement has been processed, that is when the new current state has been created, an acknowledgment is sent to proceed with the execution of the next instruction.

Instructions. The encoding of instructions goes hand in hand with the encoding of registers. Each instruction (i : I i ) is a replicated process guarded by p i , which represents the program counter when p = i. Once p i is consumed, the instruction is active and an interaction with a register occurs. In case of an increment instruction, the corresponding choice is sent to the relevant register and, upon reception of the acknowledgment, the next instruction is spawned. In case of a decrement, the corresponding choice is sent to the register, then an acknowledgment is received followed by a choice depending on whether the register was zero, resulting in a jump to the specified instruction, or the spawning of the next instruction otherwise.

The encoding of a configuration of a Minsky machine thus requires a finite number of fresh names (linear on n, the number of instructions). Definition 3.3. Let N be a Minsky machine with registers r 0 = m 0 , r 1 = m 1 and instructions (1 : I 1 ), . . . , (n : I n ). Suppose fresh, pairwise different names r 0 j , r S j , p 1 , . . . , p n , inc j , dec j , ack (for j ∈ {0, 1}). Given the encodings in Table 2, a configuration (i, m 0 , m 1 ) of N is encoded as

p i [[r 0 = m 0 ]] M [[r 1 = m 1 ]] M n i=1 [[(i : I i )]] M .
In HOcore, we write -→ * for the reflexive and transitive closure of -→, and P ⇑ if P has an infinite sequence of reductions. Similarly, in Minsky machines -→ * M is the reflexive and transitive closure of -→ M , and N ⇑ M means that N has an infinite sequence of reductions. Lemma 3.4. Let N be a Minsky machine. We have:

1. N -→ * M N iff [[N ]] M -→ * [[N ]] M ; 2. if [[N ]] M -→ * P 1 , P 1 -→ P 2 , and P 1 -→ P 3 then P 2 ≡ P 3 ; 3. if [[N ]] M -→ * P 1 then there exists N such that P 1 -→ * [[N ]] M and N -→ * M N ; 4. N ⇑ M iff [[N ]] M ⇑.
Proof. The proof of the lemma, which is detailed in Appendix Appendix A, relies on two properties. The first one ensures that for every computation of the Minsky machine the encoding can perform a finite, non-empty sequence of reductions that correspond to the one made by the machine. The second property ensures that if the process encoding a Minsky machine has a reduction to P then (i) the machine also has a reduction to N , and (ii) P has a finite deterministic sequence of reductions to the encoding of N .

The results above guarantee that HOcore is Turing complete, and since the encoding preserves termination, it entails the following corollary.

Corollary 3.5. Termination in HOcore is undecidable.

Bisimilarity in HOcore

In this section we prove that the main forms of strong bisimilarity for higher-order process calculi coincide in HOcore, and that such a relation is decidable. As a key ingredient for our results, we introduce open Input/Output (IO) bisimulation, in which the variable of input prefixes is never instantiated and τ -transitions are not observed. We are not aware of other results on process calculi where processes can perform τtransitions and yet a bisimulation that does not mention τ -transitions is discriminating enough. (One of the reasons that make this possible is that bisimulation in HOcore is very discriminating.)

We define different kinds of bisimulations by appropriate combinations of the clauses below.

1. a τ -bisimulation if P R Q and P τ -→ P imply that there is Q such that Q τ -→ Q and P R Q ; 2. a higher-order output bisimulation if P R Q and P a P ----→ P imply that there are Q , Q such that Q a Q ----→ Q with P R Q and P R Q ;
3. an output normal bisimulation if P R Q and P a P ----→ P imply that there are

Q , Q such that Q a Q ----→ Q with m. P P R m. Q Q , where m is fresh;
4. an open bisimulation if whenever P R Q: ----→ P imply that there are

• P a(x) ---→ P implies that there is Q such that Q a(x) ---→ Q and P R Q , • P ≡ x P implies that there is Q such that Q ≡ x Q and P R Q .
Q , Q such that Q a Q ----→ Q and for all S with fv(S) ⊆ {x}, it holds that S{ P /x} P R S{ Q /x} Q ; 2. an input normal bisimulation if P R Q and P a(x) ---→ P imply that there is Q such that Q a(x) ---→ Q and P { m /x} R Q { m /x},
where m is fresh;

3. closed if P R Q and P a(x) ---→ P imply that there is Q such that Q a(x) ---→ Q and for all closed R, it holds that P { R /x} R Q { R /x}.
A combination of the bisimulation clauses in Definitions 4.1 and 4.2 is complete if it includes exactly one clause for input and output transitions (in contrast, it needs not include a clause for τ -transitions). 1 We will show that all complete combinations coincide. We only give a name to those combinations that represent known forms of bisimulation for higher-order processes or that are needed in our proofs. In each case, as usual, a bisimilarity is the union of all bisimulations, and is itself a bisimulation (the functions from relations to relations that represent the bisimulation clauses in Definitions 4.1 and 4.2 are all monotonic). Definition 4.3. Higher-order bisimilarity, written ∼ HO , is the largest relation on closed HOcore processes that is a τ -bisimulation, a higher-order output bisimulation, and is closed.

Context bisimilarity, written ∼ CON , is the largest relation on closed HOcore processes that is a τ -bisimulation, an output context bisimulation, and is closed.

Normal bisimilarity, written ∼ NOR , is the largest relation on closed HOcore processes that is a τ -bisimulation, an output normal bisimulation, and an input normal bisimulation.

IO bisimilarity, written ∼ o IO , is the largest relation on HOcore processes that is a higher-order output bisimulation and is open.

Open normal bisimilarity, written ∼ o NOR , is the largest relation on HOcore processes that is a τ -bisimulation, an output normal bisimulation, and is open.

Environmental bisimilarity [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF], a recent proposal of bisimilarity for higher-order calculi, in HOcore roughly corresponds to (and indeed coincides with) the complete combination that is a τ -bisimulation, an output normal bisimulation, and is closed. 3) is in the late style. It is known [START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higherorder paradigms[END_REF] that in calculi of pure higher-order concurrency early and late clauses are equivalent.

Remark 4.5. In contrast with normal bisimulation (as defined in, e.g., [START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higherorder paradigms[END_REF][START_REF] Jeffrey | Contextual equivalence for higher-order pi-calculus revisited[END_REF]), our clause for output normal bisimulation does not use a replication in front of the introduced fresh name. Such a replication would be needed in extensions of the calculus (e.g., with recursion or restriction).

A bisimilarity on closed processes is extended to open processes as follows.

Definition 4.6 (Extension of bisimilarities).

Let R be a bisimilarity on closed HOcore processes. The extension of R to open HOcore processes, denoted R , is defined by

R = {(P, Q) : a(x 1 ). • • • . a(x n ). P R a(x 1 ). • • • . a(x n ). Q}
where fv(P ) ∪ fv(Q) = {x 1 , . . . , x n }, and a is fresh in P, Q.

The simplest complete form of bisimilarity is ∼ o IO . Not only ∼ o IO is the less demanding for proofs; it also has a straightforward proof of congruence. This is significant because congruence is usually a hard problem in bisimilarities for higher-order calculi. Before describing the proof of congruence for ∼ o IO , we first define an auxiliary up-to technique that will be useful later.

≡ if P R Q implies: 1. if P a(x) ---→ P then Q a(x) ---→ Q and P ≡R≡ Q ; 2. if P a P ----→ P then Q a Q ----→ Q with P ≡R≡ Q and P ≡R≡ Q ; 3. if P ≡ x P then Q ≡ x Q and P ≡R≡ Q . Lemma 4.8. If R is an open IO bisimulation up-to ≡ and (P, Q) ∈ R then P ∼ o IO Q. Proof.
The proof proceeds by a standard diagram-chasing argument (as in, e.g., [START_REF] Milner | Comunication and Concurrency[END_REF]): using Lemma 2.3 one shows that ≡R ≡ is a ∼ o IO -bisimulation.

We now give the congruence result for ∼ o IO . Lemma 4.9 (Congruence of ∼ o IO ). Let P 1 , P 2 be open HOcore processes. P 1 ∼ o IO P 2 implies: 1) and ( 3) are straightforward by showing the appropriate ∼ o IO -bisimulations. We consider only [START_REF] Thomsen | Plain CHOCS: A second generation calculus for higher order processes[END_REF]. We show that, for every R, P 1 , and

1. a(x). P 1 ∼ o IO a(x). P 2 ; 2. P 1 R ∼ o IO P 2 R, for every R; 3. a P 1 ∼ o IO a P 2 . Proof. Items (
P 2 S = {(P 1 R, P 2 R) : P 1 ∼ o IO P 2 }
is a ∼ o IO -bisimulation. We first suppose P 1 R α -→ P ; we need to find a matching action from P 2 R. We proceed by case analysis on the rule used to infer α. There are two cases. In the first one P 1 α -→ P 1 and P = P 1 R is inferred using rule ACT1 (by α-conversion we can ensure that R respects the side condition of the rule).

By definition of ∼

o IO -bisimulation, P 2 α -→ P 2 with P 1 ∼ o IO P 2 .
Using rule ACT1 we infer that also P 2 R α -→ P 2 R. We conclude that (P 1 R, P 2 R) ∈ S. The second case follows by an analogous argument and occurs when R α -→ R so that P = P 1 R by rule ACT2.

The last thing to consider is when P 1 R ≡ x P ; we need to show that P 2 R ≡ x Q and that (P , Q ) ∈ S. We distinguish two cases, depending on the shape of P . First, assume that P ≡ P 1 R, that is, x is a subprocess of P 1 . Since P 1 ∼ o IO P 2 , then it must be that P 2 ≡ x P 2 for some P 2 , with P 1 ∼ o IO P 2 . Taking Q ≡ P 2 R we thus have (P , Q ) ∈ S. Second, assume x is a subprocess of R, and we have P ≡ P 1 R , we then take Q ≡ P 2 R . Since S is defined over every R, then (P , Q ) ∈ S.

Lemma 4.10 (∼ o

IO is preserved by substitutions). If P ∼ o IO Q then for all x and R, also

P { R /x} ∼ o IO Q{ R /x}. Proof.
We first show the property for processes P, Q in which x is guarded, namely

R = {(P { R /x} L, Q{ R /x} L) : P ∼ o IO Q} is a ∼ o IO -bisimulation up-to ≡ (Definition 4.7). Take a pair (P { R /x} L, Q{ R /x} L) ∈ R.
We shall concentrate on the possible moves from P { R /x}, say P { R /x} α -→ P ; transitions from L, if any, can be handled analogously. We proceed by case analysis on the rule used to infer α.

We only detail the case in which α is an input action a(y) inferred using rule INP; the case in which α is an output is similar (there may be a substitution on the label), and the case where α is a(x) is simpler (the substitution does not occur under the prefix). Since x is guarded in P , using Lemma 2.5(2), there is P 1 such that P a(y) ---→

P 1 and P = P 1 { R /x}. By definition of ∼ o IO -bisimulation, also Q a(y) ---→ Q 1 with P 1 ∼ o IO Q 1 . Hence, by Lemma 2.5(1), Q{ R /x} a(y) ---→ Q 1 { R /x}. It remains to show that P 1 { R /x} and Q 1 { R /x}
can be rewritten into the form required in the bisimulation. Using Lemma 2.6(1), we have

P 1 ≡ P 1 n x and Q 1 ≡ Q 1 m x for P 1 , Q 1 in which x is guarded. As P 1 ∼ o IO Q 1 , it must be n = m and P 1 ∼ o IO Q 1 .
Finally, using Lemmas 2.6(2) and 4.9 we have

P 1 { R /x} ≡ P 1 { R /x} n R and Q 1 { R /x} ≡ Q 1 { R /x} n R
which closes up the bisimulation up-to ≡. We then conclude by Lemma 4.8 For processes where x is not guarded, we proceed exactly as above: first we rewrite P into P n x and Q into Q m x using Lemma 2.6(1), then we show that m = n and P ∼ o IO Q by definition of ∼ o IO , and we conclude using the previous result for guarded processes and Lemmas 2.6(2) and 4.9.

The most striking property of ∼ o

IO is its decidability.

Lemma 4.11. Relation ∼ o IO is decidable.

Proof. We have to check whether P ∼ o IO Q. We show that this is decidable by induction on #(P ). The base case #(P ) = 0 is trivial since in this case P has no transitions and no free variables. Let us consider the inductive case. We have one check to perform for each possible output transition, input transition, and unguarded variable (thus, a finite number of checks): P ∼ o IO Q iff all the checks succeed. We show that the checks are decidable:

• if P a P ----→ P then we have to verify that Q a Q ----→ Q with P ∼ o IO Q and P ∼ o
IO Q (otherwise the check fails). We have P ≡ a P P , thus #(P ) < #(P ) and #(P ) < #(P ) and we can decide P ∼ o IO Q and P ∼ o IO Q by inductive hypothesis. Thus the check is decidable.

• if P a(x)
---→ P then we have to verify that Q

a(x)
---→ Q with P ∼ o IO Q . We have P ≡ a(x). R R and P ≡ R R , thus #(P ) < #(P ) and we can decide

P ∼ o IO Q by inductive hypothesis. • if P ≡ x P then we have to verify that Q ≡ x Q with P ∼ o IO Q . Since #(P ) < #(P ) we can decide P ∼ o IO Q by inductive hypothesis.
Next we show that ∼ o IO is also a τ bisimulation. This will allow us to prove that ∼ o IO coincides with other bisimilarities, and to transfer to them its properties, in particular congruence and decidability.

Lemma 4.12. Relation ∼ o IO is a τ -bisimulation.

Proof. Suppose (P, Q) ∈ ∼ o IO and P τ -→ P ; we have to find a matching transition Q τ -→ Q . We proceed by induction on the derivation P τ -→ P . The cases ACT1 and ACT2 are immediate by induction. The remaining cases are using either rule TAU1 or TAU2. We consider only the first one as the second is symmetric. If rule TAU1 was used, then we can decompose P 's transition into an output P a R ---→ P 1 followed by an input P 1 a(x) ---→ P 2 P 3 , with P = P 2 { R /x} P 3 (that is, the structure of P is P ≡ a R a(x). P 2 P 3 ). By definition of ∼ o IO , Q is capable of matching these two transitions, and the final derivative is a process Q 2 with Q 2 ∼ o IO P 2 P 3 . Further, as HOcore has no output prefixes (i.e., it is an asynchronous calculus) the two transitions from Q can be combined into a τ -transition. Finally, since ∼ o IO is preserved by substitutions (Lemma 4.10), we can use rule TAU1 to derive a process

Q = Q 2 { R /x} Q 3 that matches the τ -transition from P , with (P , Q ) ∈ ∼ o IO .
Next lemmas prove useful properties of higher-order bisimulations.

Lemma 4.13. Let P, Q be two processes and {x 1 , . . . , x n } be their free variables. We have P ∼ HO Q iff P { Ri / xi} ∼ HO Q{ Ri / xi} for any tuple of closed processes R i .

Proof. First assume that P ∼ HO Q, and let a be a fresh name. By definition of ∼ HO , we thus have a(x 1 ).

• • • . a(x n ). P ∼ HO a(x 1 ). • • • . a(x n ). Q. Let R 1 , • • • , R n be closed processes.
By a repeated application of the input clause for ∼ HO , we conclude that

P { Ri / xi} ∼ HO Q{ Ri / xi}.
For the other direction, by definition we have to prove a(x 1 ). • • • . a(x n ). P ∼ HO a(x 1 ). • • • . a(x n ). Q. The only possible transitions of a(x 1 ). • • • . a(x n ). P are the inputs, which lead to P { Ri / xi} for some R i , and are matched by corresponding inputs from a(x 1 ). We proceed by case on P α -→ P (we also have an additional case for unguarded variables). Let {y 1 , . . . , y n } be the free guarded variables of P { mi / xi} and Q{ mi / xi}, and let R 1 , . . . , R n be closed processes. By Lemma 4.13, P { mi / xi}{ Rj / yj} ∼ HO Q{ mi / xi}{ Rj / yj}. As the R j are closed, by Lemma 2.5(1), we can deduce that

P { mi / xi}{ Rj / yj} α{ mi / xi}{ Rj / yj} ------------→ P { mi / xi}{ Rj / yj}. By definition of ∼ HO , we have Q{ mi / xi}{ Rj / yj} α{ mi / xi}{ Rj / yj} ------------→ Q { mi / xi}{ Rj / yj}. By Lemma 2.5(2) we have Q{ mi / xi} α{ mi / xi} -------→ Q { mi / xi}
as the y j are guarded. Finally, by Lemma 2.5(3), we have Q α -→ Q , as the m i are fresh thus α{ mi / xi} = m i is impossible. In the output case, by ∼ HO , we have directly P { mi / xi}{ Rj / yj} ∼ HO Q { mi / xi}{ Rj / yj} and we conclude by Lemma 4.13 that P { mi / xi} ∼ HO Q { mi / xi} since this is true for any R j , thus P and Q are still in the relation. We apply the same approach to the contents S P and S Q of the messages:

S P { mi / xi}{ Rj / yj} ∼ HO S Q { mi / xi}{ Rj / yj} for ar- bitrary R j , thus S P { mi / xi} ∼ HO S Q { mi / xi},
thus S P and S Q are in the relation. In the case of an input a(x), P and Q may have an additional free variable x. In this case, by definition of ∼ HO we have

P { mi / xi}{ Rj / yj}{ R /x} ∼ HO Q { mi / xi}{ Rj / yj}{ R /
--→ Q { mi / xi}.
As m i is fresh in relation to P and Q, it means that x is free in Q, thus that Q ≡ x Q . Moreover, as we showed this for arbitrary R j , by Lemma 4.13, we have

P { mi / xi} ∼ HO Q { mi / xi}.
We thus conclude by noting that we have (P , Q ) in the relation.

To conclude, we remark that if P ∼ HO Q then (P, Q) is in the relation defined above (with no variable substituted), thus

P ∼ o IO Q. We next show that ∼ o IO is a ∼ HO -bisimulation. Suppose (P 1 , Q 1 ) ∈ ∼ o IO
, and let a be a fresh name, fv(P 1 ) ∪ fv(Q 1 ) = {x 1 , . . . , x n }. We consider the pair of closed processes P = a(x 1 ).

• • • . a(x n ). P 1 and Q = a(x 1 ). • • • . a(x n ). Q 1 .
By Lemma 4.9, we still have P ∼ o IO Q. We proceed by case on the transition P α -→ P . The case α = b R is immediate, as it means that n = 0 (P 1 and Q 1 were already closed), and

we conclude by Q = Q 1 b S ---→ Q with P ∼ o IO Q and R ∼ o IO S.
Similarly, in the case of a τ transition, we also have P = P 1 and Q = Q 1 and we conclude by Lemma 4.12. We now turn to the input case, i.e.,

P b(x) ---→ P . By ∼ o IO , we have Q b(x) ---→ Q and P ∼ o IO Q . We conclude by Lemma 4.10 that P { R /x} ∼ o IO Q { R /x} for any closed process R.
We now move to the relationship between ∼ HO , ∼ o NOR , and ∼ CON . We begin by establishing a few properties of normal bisimulation. Proof. We show that for any countable set of fresh names m 1 , . . ., the relation

S = ∞ j=1 {(P, Q) : P k∈1..j m k . P k ∼ o NOR Q k∈1..j m k . Q k }
is a ∼ o NOR -bisimulation. Suppose (P, Q) ∈ S and that P α -→ P ; we need to show a matching action from Q. We have different cases depending on the shape of α. We consider only the case α = a P , the others being simpler. By ACT1 we have

P k∈1..j m k . P k a P ----→ P k∈1..j m k . P k . Since P k∈1..j m k . P k ∼ o NOR Q k∈1..j m k . Q k , there should exist a Q * such that Q k∈1..j m k . Q k a Q ----→ Q * , with P k∈1..j m k . P k m . P ∼ o NOR Q * m . Q . As m 1 , .
. . , m j are fresh, they do not occur in P , thus a P does not mention them. For the same reason, there cannot be any communication between k∈1..j m k . Q k and Q; so, we infer that the only possible transition is

Q k∈1..j m k . Q k a Q ----→ Q * = Q k∈1..j m k . Q k , applying rule ACT1 to Q a Q ----→ Q . Since P k∈1..j m k . P k m . P ∼ o NOR Q k∈1..j m k . Q k m . Q , we have (P , Q ) ∈ S as needed. We now show that if P k∈1..j m k . P k ∼ o NOR Q k∈1..j m k . Q k then P 1 ∼ o NOR Q 1 .
To this end, we first detail a procedure for consuming ∼ o NOR -bisimilar processes. Given a process P , let o(P ) denote the number of output actions in P . Let m(P ) = #(P ) + o(P ) be the measure that considers both the (syntactical) size of P and the number of output actions in it. Consider now two ∼ o NOR -bisimilar processes P and Q. The procedure consists in consuming one of them by performing its actions completely; the other process can match these actions (as it is ∼ o NOR -bisimilar) and will be consumed as well. We will show that m(P ) decreases at each step of the bisimulation game; at the end, we will obtain processes P n and

Q n with m(P n ) = m(Q n ) = 0.
To illustrate the procedure, suppose, w.l.o.g., process P has the following shape:

P ≡ h∈1..t x h i∈1..k a i (x i ). P i j∈1..l b j P j
where we have t top-level variables, k input actions, and l output actions. We use a i and b j for channels in input and output actions, respectively. The first step is to remove top-level variables; this relies on the fact ∼ o NOR is an open bisimilarity. One thus obtains processes P 1 and Q 1 with only input and output actions, and both m(P 1 ) < m(P ) and m(Q 1 ) < m(Q) hold. As a second step, the procedure exercises every output action in P 1 . By definition of ∼ o NOR , Q 1 should be able to match those actions. Call the resulting processes P 2 and Q 2 . Recall that when an output a P j is consumed in the bisimulation game, process m j . P j is added in parallel. Thus since #(a P j ) = #(m j . P j ) and the number of outputs decreases, measure m decreases as well. More precisely, one has that

P 2 ≡ i∈1..k a i (x i ). P i j∈1..l m j . P j
where m j stands for a fresh name. Then, one has to consider the k + l input actions in each process; their consumption proceeds as expected. One obtains processes P 3 and Q 3 that are bisimilar, with strictly decreasing measures for both processes. The procedure concludes by iterating the above steps on P 3 and Q 3 . In fact, we have shown that at each step measure m strictly decreases; this guarantees that eventually one will reach processes P n and Q n , with m(P n ) = m(Q n ) = 0 as desired. Consider now the following ∼ o NOR -bisimilar processes: P k∈1..j m k . P k and Q k∈1..j m k . Q k . Using the procedure above over P until it becomes 0, we obtain k∈1..j m k . P k ∼ o NOR k∈1..j m k . Q k . This is because fresh names m 1 , . . . , m j do not occur in P and Q, and hence they do not intervene in P 's consumption, so the bisimilar process must still mention them and cannot mention anything else. Similarly, we can consume k ∈2..j m k . P k (i.e., all the components excepting m 1 . P 1 ) which is match by the consumption of the corresponding k ∈2..j m k . Q k . We thus end up with m 1 . P 1 ∼ o NOR m 1 . Q 1 , and we observe that the only possible action on each side is the input on m 1 , which can be trivially matched by the other. We then infer that (P 1 , Q 1 ) ∈ S 1 , as desired.

Lemma 4.16. ∼ HO implies ∼ CON .

Proof. We only need to prove that ∼ HO implies ∼ CON by definition of open extension. We suppose (P, Q) ∈ ∼ HO and P α -→ P ; we need to show a matching action from Q. We proceed by case analysis on the form α can take. The only interesting case is when α is a higher-order output; the remaining clauses are the same in both relations.

By definition of ∼ HO , if

P a P ----→ P then Q a Q
----→ Q , with both P ∼ HO Q and P ∼ HO Q . We need to show that, for every S such that fv(S) = {x}, S{ P /x} P ∼ HO S{ Q /x} Q ; this follows from P ∼ HO Q and P ∼ HO Q and the fact that ∼ HO is both a congruence and preserved by substitutions. Lemma 4.17. ∼ CON implies ∼ NOR .

Proof. Straightforward by showing an appropriate bisimulation. The result is immediate by noticing that (i) both relations are τ -bisimulations, and that (ii) the input and output clauses of ∼ NOR are instances of those of ∼ CON . In the output case, by selecting a process S = m. x (with m fresh) one obtains the desired form for the clause. The input clause is similar, and follows from the definition of closed bisimulation, which holds for every closed process R; in particular, it also holds for R = m (with m fresh) as required by the clause of ∼ NOR . We first suppose P ∼ NOR Q and P α -→ P ; we need to find a matching transition Q α -→ Q . We perform a case analysis on the shape α can take. The τ and output cases are immediate by using Lemma 2.5(1 and 3). We now detail the case in which

α = a(x). If P a(x)
---→ P then by Lemma 2.5(1)

P { m1 /x1, . . . , mn /xn} a(x) ---→ P { m1 /x1, . . . , mn /xn}.
In turn, by definition of ∼ NOR , such an action guarantees that there exists a Q that matches that input action, i.e., ---→ Q , and we conclude by the equivalence above that P ∼ NOR Q .

Q{
The last thing to consider are those variables in evaluation context in the open processes. This is straightforward by noting that by definition of ∼ NOR , all such variables have been closed with a trigger. So, suppose P ∼ NOR Q and

P { m1 /x1, . . . , mn /x} ≡ m 1 P { m1 /x1, . . . , mn /xn}
where m 1 is fresh. We need to show that Q has a similar structure, i.e., that Q ≡ x Q , with P ∼ NOR Q . P can perform an output action on m 1 , thus evolving to P { m1 /x1, . . . , mn /xn}. By definition of ∼ NOR , Q can match this action, and evolves to some process Q * , with m . 0 P { m1 /x1, . . . , mn /xn} ∼ NOR m . 0 Q * , where m is a fresh name (obtained from the definition of ∼ NOR for output actions). The input on m can be trivially consumed on both sides, and one has P { m1 /x1, . . . , mn /xn} ∼ NOR Q * . At this point, since m 1 is a fresh name, we know that Q involves a variable in evaluation context. Furthermore, since there is a correspondence between P and Q * , they should involve substitutions in the very same fresh names. More precisely, we have that there should be a Q such that We thus infer that ∼ HO and ∼ CON are congruence relations. Direct proofs of these results proceed by exhibiting an appropriate bisimulation and are usually hard (a sensible aspect being proving congruence for parallel composition). Congruence of higherorder bisimilarity is usually proved by appealing to, and adapting, Howe's method for the λ-calculus [START_REF] Howe | Proving congruence of bisimulation in functional programming languages[END_REF]. This is the approach followed in, e.g., [START_REF] Baldamus | Congruence proofs for weak bisimulation equivalences on higher-order process calculi[END_REF][START_REF] Bundgaard | Bisimulation congruences for homer -a calculus of higher order mobile embedded resources[END_REF][START_REF] Godskesen | Extending howe's method to early bisimulations for typed mobile embedded resources with local names[END_REF]; very recent uses of Howe's method are reported in [START_REF] Lenglet | Normal bisimulations in calculi with passivation[END_REF][START_REF] Lenglet | Howe's method for calculi with passivation[END_REF] for higher-order process calculi with passivation constructs.

Q ≡ m 1 Q { m1 /
We then extend the result to all complete combinations of the HOcore bisimulation clauses (Definitions 4.1 and 4.2). Theorem 4.21. All complete combinations of the HOcore bisimulation clauses coincide, and are decidable.

Proof. In Lemma 4.20 we have proved that the least demanding combination (∼ o IO ) coincides with the most demanding ones (∼ HO and ∼ CON ). Decidability then follows from Lemma 4.11.

We find this "collapsing" of bisimilarities in HOcore significant; the only similar result we are aware of is by Cao [START_REF] Cao | More on bisimulations for higher order pi-calculus[END_REF], who showed that strong context bisimulation and strong normal bisimulation coincide in higher-order π-calculus.

Barbed Congruence and Asynchronous Equivalences

We now show that the labeled bisimilarities of Section 4 coincide with barbed congruence, the form of contextual equivalence used in concurrency to justify bisimulationlike relations. Below we use reduction-closed barbed congruence [START_REF] Honda | On reduction-based process semantics[END_REF][START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF], as this makes some technical details simpler; however the results also hold for ordinary barbed congruence as defined in [START_REF] Milner | Barbed bisimulation[END_REF]. It is worth recalling that the main difference between reduction-closed barbed congruence and the barbed congruence of [START_REF] Milner | Barbed bisimulation[END_REF] is quantification over contexts (see [START_REF] Thomsen | Plain CHOCS: A second generation calculus for higher order processes[END_REF] in Definition 5.1 below). More importantly, we consider the asynchronous version of barbed congruence, where barbs are only produced by output messages; we call barbed congruence synchronous when inputs contribute too, as in, e.g., [START_REF] Milner | Barbed bisimulation[END_REF]. We use the asynchronous version for two reasons. First, asynchronous barbed congruence is a weaker relation, which makes the results stronger (they imply the corresponding results for the synchronous relation). Second, asynchronous barbed congruence is more natural in HOcore because it is an asynchronous calculus -it has no output prefix.

Note also that the labeled bisimilarities of Section 4 have been defined in the synchronous style. In an asynchronous labeled bisimilarity (see, e.g., [START_REF] Amadio | On bisimulations for the asynchronous pi-calculus[END_REF]) the input clause is weakened so as to allow, in certain conditions, an input action to be matched also by a τ -action. For instance, input normal bisimulation (Definition 4.2(2)) would become:

• if P a(x)
---→ P then, for some fresh name m,

1. either Q a(x) ---→ Q and P { m /x} R Q { m /x}; 2. or Q τ -→ Q and P { m /x} R Q a m .
We now define asynchronous barbed congruence. We write P ↓ a (resp. P ↓ a ) if P can perform an output (resp. input) transition at a. In synchronous barbed congruence, input barbs P ↓ a are also observable. Lemma 5.2. Asynchronous barbed congruence coincides with normal bisimilarity.

Proof. We first show that ∼ NOR implies , and then its converse, which is harder. The relation ∼ NOR satisfies the conditions in Definition 5.1 as follows. First, both relations are τ -bisimulations so condition (1) above trivially holds. Second, the context-closure condition follows from the fact that ∼ NOR is a congruence. Finally, the barb-preserving condition is seen to hold by definition of ∼ NOR : having P ∼ NOR Q implies that an output action of P on a has to be matched by an output action of Q on a; hence, we have that if P ↓ a , then also Q ↓ a . Now the converse. We show that relation satisfies the three conditions for ∼ NOR in Definition 4.3. Suppose P Q and P α -→ P ; we have to show a matching transition Q α -→ Q . We proceed by a case analysis on the form α can take.

Case α = τ . Since by definition is a τ -bisimulation, then there is a Q such that Q τ -→ Q and P Q and we are done.

Case α = a P . We have P a P ----→ P : it can be shown that is an output normal bisimulation by showing a suitable context. Let C a o [•] be the context

C a o [•] = [•] a(x). (m. x n n. 0)
where m, n are fresh names. We then have C a o [P ] τ -→ P 1 with P 1 ↓ n . Indeed, we have P 1 ≡ P m. P n n. 0. By definition of , we have also

C a o [Q] τ -→ Q 1 and necessarily, Q 1 ↓ n .
Since n is a fresh name, we infer that Q also has an output on a, such that

Q a Q ----→ Q and hence Q 1 ≡ Q m. Q n n. 0. Note that (P 1 , Q 1 ) is in .
They can consume the actions on n; since it is a fresh name, only the corresponding τ action of Q 1 can match it. As a result, both processes evolve to processes P m. P and Q m. Q that are still in . We then conclude that is an output normal bisimulation.

Case α = a(x). We have P a(x) ---→ P . Again, to show that is an input normal bisimulation, we define a suitable context. Here, the asynchronous nature of HOcore (more precisely, the lack of output prefixes, which prevents the control of output actions by modifying their continuation) and the input clause for ∼ NOR it induces (reported above) result in a more involved definition of these contexts. Notice that simply defining a context with an output action on a so as to force synchronization with the input action does not work here: process P itself could contain other output actions on a that could synchronize with the input we are interested in, and as output actions have no continuation, it is not possible to put a fresh barb indicating it has been consumed. We overcome this difficulty by (i) renaming every output in P , so as to avoid the possibility of τ actions (including those coming from synchronizations on channels different from a), (ii) consuming the input action on a (by placing the renamed process in a suitable context) and then (iii) restoring the initial outputs.

We define a context for (i) above, i.e., to rename every output in a process so as to prevent τ actions. We start by denoting by out(P ) the multiset of names in output subject position in a process P . Further, let σ denote an injective relation between each occurrence of name in out(P ) and a fresh name. Let C[•] be the context

C[•] = [•] (bi,ci)∈σ b i (x). c i x
which uniquely renames every output b i S i as c i S i . (We shall use c i (i ∈ 1. . n) to denote the fresh names for the renamed outputs.) Consider now processes C[P ] and C[Q]: since the renaming is on fresh channels, it can be ensured that the τ action due to the renaming of one output on one process is matched by the other process with a τ action that corresponds to the renaming of the same output. At the end, after a series of n τ actions, C[P ] and C[Q] become processes P 1 and Q 1 that have no τ actions arising from their subprocesses and that are in . At this point it is then possible to use a context for (ii), to capture the input action on a in P 1 . Let C a i [•] be the context

C a i [•] = [•] a m
where m is a fresh name. We then have

C a i [P 1 ] τ -→ c 1 S 1 • • • c n S n P a { m /x} P = P 2
which, by definition of , implies that also it must be the case that, for some process

Q 2 , C a i [Q 1 ] τ -→ Q 2 .
In fact, since there is a synchronization at a, it implies that Q 1 must have at least one input action on a. More precisely, we have

Q 2 ≡ c 1 S 1 • • • c n S n Q a { m /x} Q .
We notice that P 2 and Q 2 are still in ; it remains however to perform (iii), i.e., to revert the renaming made by C[•]. To do so, we proceed analogously as before and define the context

C [•] = [•] (ci,bi)∈σ -1 c i (x). b i x .
We have that each of C [P 2 ] and C [Q 2 ] produces n τ steps that exactly revert the renaming done by context C[•] above and lead to P 3 and Q 3 , respectively. This renaming occur in lockstep (and no other τ action may be performed by Q 2 ), as each one removes a barb on a fresh name, thus the other process has to remove the same barb by doing the renaming. Hence, P 3 and Q 3 have the same output actions as the initial P and Q, and since is a τ -bisimulation we have P 3 Q 3 . To conclude, we remark that C a i [P ] τ -→ P 3 in one step. Indeed, we have

C a i [P ] ≡ T a(x). P a P a m τ -→ P 3 = P { m /x}
where T stands for all the output actions in P (on which the renaming took place). By doing and undoing the renaming on every output, we were able to infer that Q has an analogous structure

C a i [Q] ≡ T a(x). Q a Q a m τ -→ Q 3
where T stands for all the output actions in

Q. Let Q = T Q a Q , we then have Q a(x) ---→ Q and Q 3 = Q { m /x}.
To summarize, we have P

a(x) ---→ P , Q a(x)
---→ Q , and P { m /x} Q { m /x} with m fresh. Hence we conclude that is an input normal bisimulation.

Remark 5.3. The proof relies on the fact that HOcore has no operators of choice and restriction. In fact, choice would prevent the renaming to be reversible, and restriction would prevent the renaming using a context as some names may be hidden. The higherorder aspect of HOcore does not really play a role. The proof could indeed be adapted to CCS-like, or π-calculus-like, languages in which the same operators are missing.

Corollary 5.4. In HOcore asynchronous and synchronous barbed congruence coincide, and they also coincide with all complete combinations of the HOcore bisimulation clauses of Theorem 4.21.

Further, Corollary 5.4 can be extended to include the asynchronous versions of the labeled bisimilarities in Section 4 (precisely, the complete asynchronous combinations of the HOcore bisimulation clauses; that is, complete combinations that make use of an asynchronous input clause as outlined before Definition 5.1). This holds because: (i) all proofs of Section 4 can be easily adapted to the corresponding asynchronous labeled bisimilarities; (ii) using standard reasoning for barbed congruences, one can show that asynchronous normal bisimilarity coincides with asynchronous barbed congruence; (iii) via Corollary 5.4 one can then relate the asynchronous labeled bisimilarities to the synchronous ones.

Axiomatization and Complexity

We have shown in the previous section that the main forms of bisimilarity for higher-order process calculi coincide in HOcore. We therefore simply call bisimilarity such a relation, and write it as ∼. Here we present a sound and complete axiomatization of bisimilarity. We do so by adapting to a higher-order setting results by Moller and Milner on unique decomposition of processes [START_REF] Milner | Unique decomposition of processes[END_REF][START_REF] Moller | Axioms for concurrency[END_REF], and by Hirschkoff and Pous on an axiomatization for a fragment of (finite) CCS [START_REF] Hirschkoff | A distribution law for CCS and a new congruence result for the π-calculus[END_REF]. We then exploit this axiomatization to derive complexity bounds for bisimilarity checking.

Axiomatization

Lemma 6.1. P ∼ Q implies #(P ) = #(Q).
Proof. Suppose, for a contradiction, that there exist P, Q such that P ∼ Q with #(P ) < #(Q) and choose a P with a minimal size. If Q has no transition enabled, then it must be 0, thus #(Q) = 0, which is impossible as #(Q) > #(P ) ≥ 0.

We thus have Q α -→ Q , hence there is a P such that P α -→ P with P ∼ Q . We consider two cases, depending on the shape of α (we do not consider τ actions, as such an action implies both an input and an output).

If α is an input action, we have Q

a(x)
---→ Q , and since P ∼ Q, then also P a(x) ---→ P . We then have that #(P ) = #(P ) -1 and #(Q ) = #(Q) -1, so it follows that #(P ) < #(Q ). Further, one has #(P ) < #(P ), which contradicts the minimality hypothesis. Now suppose α is an output action: we have Q a Q ----→ Q , and by definition of ∼, also that P a P ----→ P with both P ∼ Q and P ∼ Q . By the definition of size, we have that #(P ) = #(P ) -(1 + #(P )) and

#(Q ) = #(Q) -(1 + #(Q )).
Notice that P , Q are strict subterms of P and Q, respectively. If their size is not the same, we have a contradiction. Otherwise, we have #(P ) < #(Q ) and also #(P ) < #(P ), which is also a contradiction.

Following [START_REF] Milner | Unique decomposition of processes[END_REF][START_REF] Moller | Axioms for concurrency[END_REF] we prove a result of unique prime decomposition of processes. Definition 6.2 (Prime decomposition). A process P is prime if P ∼ 0 and P ∼ P 1 P 2 imply P 1 ∼ 0 or P 2 ∼ 0. When P ∼ n i=1 P i where each P i is prime, we call n i=1 P i a prime decomposition of P . Proposition 6.3 (Cancellation). For all P , Q, and R, if P R ∼ Q R then also P ∼ Q.

Proof. The proof, which proceeds by induction on #(P ) + #(Q) + #(R), is a simple adaptation of the one in [START_REF] Milner | Unique decomposition of processes[END_REF].

We detail it below. We simultaneously prove the following by induction on #(P ) + #(Q) + #(R):

1. if P R ∼ Q R then P ∼ Q; 2. if R α -→ R and P R ∼ Q R , then Q α -→ Q for some P ∼ Q .
Note that every reduction P α -→ P decreases the size of P if α is not a τ transition.

1. Assume that P R ∼ Q R and suppose that P α -→ P , for some input or output action α (we do not consider τ transitions as we rely on the fact that ∼ o IO characterizes barbed congruence). We then have P R α -→ P R, which can be matched by either:

(a)

Q α -→ Q and P R ∼ Q R; or (b) R α -→ R and P R ∼ Q R .
For case (1a), by induction hypothesis (1) we have P ∼ Q . For case (1b), by induction hypothesis (2) we have Q α -→ Q and P ∼ Q . The last case to consider is for when P contains a variable. If R also contains a variable, then it may be removed from both sides from R and we conclude by induction hypothesis [START_REF] Thomsen | A calculus of higher order communicating systems[END_REF]. If there is no variable in R, then it occurs in both P and Q and we also conclude by induction hypothesis [START_REF] Thomsen | A calculus of higher order communicating systems[END_REF]. The case when starting from Q is symmetric, thus we have P ∼ Q. 2. Assume that R α -→ R and P R ∼ Q R . We thus have P R α -→ P R , and there exists some S such that Q R α -→ S with P R ∼ S. As before, we distinguish the source of the action. We either have:

(a) Q α -→ Q and P R ∼ Q R ; or (b) R α -→ R and P R ∼ Q R .
For case (2a), we have P ∼ Q by induction hypothesis (1). For case (2b), we apply induction hypothesis ( 2) and thus we have

Q α -→ Q with P ∼ Q .
Proposition 6.4 (Unique decomposition). Any process P admits a prime decomposition n i=1 P i which is unique up to bisimilarity and permutation of indices (i.e., given two prime decompositions n i=1 P i and m j=1 Q j , then n = m and there is a permutation σ of {1, . . . , n} such that P i ∼ Q σ(i) for each i ∈ {1, . . . , n}).

Proof. The proof is also similar to the one in [START_REF] Milner | Unique decomposition of processes[END_REF]. We also detail this proof.

We proceed by induction on #(P ). Assume there are two prime decompositions, P ∼ n i=1 P i and P ∼ Q = m j=1 Q j . First, if some P k ∼ Q l (w.l.o.g assume that P 1 ∼ Q 1 ), then we have the following two prime decompositions for P : P ∼ P 1 n i=2 P i and P ∼ P 1 m j=2 Q j . By Proposition 6.3, we have

n i=2 P i ∼ m j=2 Q j .
As these are prime decomposition of a smaller process, by induction they are also unique (up to bisimilarity and permutation of indices). Thus the two decompositions n i=1 P i and m j=1 Q j are also identical up to bisimilarity and permutation of indices. We now assume, for a contraction, that for every i, j we have P i ∼ Q j . If either n = 1 or m = 1, then (by definition of a prime process) n = m = 1 and P 1 ∼ Q 1 , a contradiction.

We thus assume that n, m ≥ 2 and that (w.l.o.g.) that #(P 1 ) ≤ #(P i ) and #(P 1 ) ≤ #(Q j ) for every i and j. As P 1 is not empty, it contains either a variable or can do an input or output action.

In the case it contains a variable, then we must have P 1 ∼ x (the only prime process that contains a variable is one that is equivalent to a variable). As P ∼ m j=1 Q j , then one of the Q j must be equivalent to x, which is a contradiction.

Let us now consider the case where P 1 does an input or output action α: P 1 α -→ R. We necessarily have #(R) < #(P 1 ) ≤ #(P ), thus R has a unique prime decomposition, which we write l k=1 R k . We thus have P α -→ P with unique decomposition (as

#(P ) < #(P )) P ∼ l k=1 R k n i=2 P i . Since P ∼ Q, we thus have Q α -→ Q ∼ P , thus for some Q j (w.l.o.g. Q 1 ), we have Q 1 α -→ T and Q = T m j=2 Q j .
As the decomposition P ∼ Q is unique, and as m ≥ 2, there is some process Q 2 and it must be equivalent to some process in l k=1 R k n i=2 P i . It cannot be one of the R k as #(R k ) < #(P 1 ) ≤ #(Q 2 ) (and their size have to match by Lemma 6.1), so it must be one of P 2 , . . . , P n , a contradiction.

Both the key law for the axiomatization and the following results are inspired by similar ones by Hirschkoff and Pous [START_REF] Hirschkoff | A distribution law for CCS and a new congruence result for the π-calculus[END_REF] for pure CCS. Using their terminology, we call distribution law, briefly (DIS), the axiom schema below (recall that

k 1 Q denotes the parallel composition of k copies of Q). a(x). (P k-1 1 a(x). P ) = k 1 a(x). P (DIS)
We then call extended structural congruence, written ≡ E , the extension of the structural congruence relation (≡, Definition 2.2) with the axiom schema (DIS). We write P Q when there are processes P and Q such that P ≡ P , Q ≡ Q and Q is obtained from P by rewriting a subterm of P using law (DIS) from left to right. Below we prove that ≡ E provides an algebraic characterization of ∼ in HOcore. Establishing the soundness of ≡ E is easy; below we discuss completeness. Definition 6.5. A process P is in normal form if it cannot be further simplified in the system ≡ E by using .

Any process P has a normal form that is unique up to ≡, and which will be denoted by n(P ). Below A and B range over normal forms, and a process is said to be nontrivial if its size is not 0. Lemma 6.6. If P Q, then P ∼ Q. Also, for any P , P ∼ n(P ).

Proof. The proof proceeds by showing that ( ∪ ( ) -1 ∪ ≡) is a bisimulation (as

∼ o IO , for instance). Lemma 6.7. If a(x). P ∼ Q Q with Q, Q ∼ 0, then a(x). P ∼ k 1 a(x). A,
where k > 1 and a(x). A is in normal form.

Proof. By Lemma 6.6, a(x). P ∼ n(Q Q ). Furthermore, by Proposition 6.4, we have that

n(Q Q ) ≡ i≤k a i (x i ). A i j≤l b j B j h≤m x h ,
where the processes a i (x i ). A i and b j B j and x h are in normal form and prime. Since the prefix a(x) must be triggered to answer any challenge from the right-hand side, we have a i = a, and x i = x (this can be obtained via α-conversion, but we can suppose that a i (x i ). A i was already α-converted to the correct form), and we have l = 0 and m = 0 (there are no output nor toplevel variables in the prime decomposition). As there are at least two processes that are not 0, we have k > 1. To summarize: a(x). P ∼ i≤k a(x). A i .

If P i is an output, B must contain an output on the same channel. The thesis then follows by applying the induction hypothesis twice, to the arguments and to the other parallel components. The last case is when A ≡ i≤k a i (x i ). A i with k > 1. We know by the induction hypothesis (property (1)) that each component a i (x i ). A i is prime. Similarly, it must be B ≡ i≤l b i (x i ). B i with b i (x i ). B i prime for all i ≤ l. By Proposition 6.4 (unique decomposition), we infer k = l and a i (x i ). A i ∼ b i (x i ). B i (up to a permutation of indices). Thus a i = b i and A i ∼ B i ; then by induction A i ≡ B i for all i, which finally implies

A ≡ B.
The theorem below follows from Lemmas 6.6 and 6.8. Theorem 6.9. For any processes P and Q, we have

P ∼ Q iff n(P ) ≡ n(Q).
Corollary 6.10. ≡ E is a sound and complete axiomatization of bisimilarity in HOcore.

Complexity of bisimilarity checking

To analyze the complexity of deciding whether two processes are bisimilar, one could apply the technique from [START_REF] Dovier | An efficient algorithm for computing bisimulation equivalence[END_REF], and derive that bisimilarity is decidable in time which is linear in the size of the LTS for ∼ o IO (which avoids τ transitions). This LTS is however exponential in the size of the process. A more efficient solution exploits the axiomatization above: one can first normalize processes and then reduce bisimilarity to syntactic equivalence of the obtained normal forms.

For simplicity, we assume a process P is represented as an ordered tree (but we will transform it into a DAG during normalization). In the following, let us denote with t[m 1 , . . . , m k ] the ordered tree with root labeled t and with (ordered) descendants m 1 , . . . , m k . We write t[] for a tree labeled t and without descendants (i.e., a leaf). Definition 6.11 (Tree representation). Let P be a HOcore process. Its associated ordered tree representation is labeled and defined inductively by

• Tree(0) = 0[] • Tree(x) = db(x)[] • Tree(a Q ) = ā[Tree(Q)] • Tree(a(x). Q) = a[Tree(Q)] • Tree( n i=1 P i ) = n i=1 [Tree(P 1 ), . . . , Tree(P n )]
where db is a function assigning De Bruijn indices [START_REF] De Bruijn | Lambda calculus notation with nameless dummies: A tool for automatic formula manipulation, with application to the church-rosser theorem[END_REF] to variables. Parallel composition is n-ary, thus we can assume without loss of generality that children of parallel composition nodes are not parallel composition nodes (i.e., we can always flatten them).

We now describe the normalization steps by characterizing them as reductions as well as pseudocode descriptions. The first step deals with parallel composition nodes: it removes all unnecessary 0 nodes, and relabels the nodes when the parallel composition has only one or no descendants.

Normalization step 1. Let N1 be a transformation rule over trees associated to HOcore processes defined by:

1. 0 i=1 [] N1 0[] 2. 1 i=1 [Tree(P 1 )] N1 T if Tree(P 1 ) N1 T 3. n i=1 [Tree(P 1 ), . . . , Tree(P n )] N1 m i=1 [T σ(1) , . . . , T σ(m) ], if Tree(P i ) N1
T i for each i, where m < n is the number of trees in T 1 , . . . , T n that are different from 0[], and where σ is a bijective function from {1, . . . , m}

to {i | i ∈ {1, . . . , n} ∧ T i = 0[]}.
After this first step, the tree is traversed bottom-up, applying the following two normalization steps.

Normalization step 2. Let N2 be a transformation rule over trees associated to HOcore processes, defined as follows. If the node is a parallel composition, sort all the children lexicographically. If n children are equal, leave just one and make n references to it.

The last normalization step applies DIS from left to right if possible: Normalization step 3. Let N3 be a transformation rule over trees associated to HOcore processes, defined by:

a k+1 i=1
[Tree(P ), Tree(a(x). P ), . . . , Tree(a(x). P )]

N3 k+1 j=1
[Tree(a(x). P ), . . . , Tree(a(x). P )]

where Tree(a(x). P ) appears k times in the left-hand side, and k + 1 times in the right-hand side.

We now present the pseudocode for the three normalization steps. We use a rather standard pointer-based implementation of trees, with the following notational conventions. A node of a tree is a record with four attributes (or fields). Given a node n, we use n. attr to refer to the attribute attr of n. Each node has an attribute type, which represents the type of node; possible values are zero (for a nil process node); par (for a parallel composition node); inp and out (for nodes for input and output actions, respectively); and var (for nodes associated to variables). Each node n has also an attribute children, an array of pointers to the children of node n. Hence, n. children[i] stands for the pointer to the i-th children of n. We use * for dereferencing. Furthermore, we assume an operation delete for node deletion (freeing the allocated memory). The length of children is stored as attribute numChildren. Nodes aux = n. children [START_REF] Thomsen | A calculus of higher order communicating systems[END_REF] 6:

n = * (n. children[1]) 7:
delete(aux) if * (n. children[i]). type = zero then 14:

8: NS1 (n) 9:
n. children[j] = n. children[i]
15:

j = j + 1 16: else 17: delete(n. children[i]) 18: end if 19: end for 20:
n. numChildren = j -1

end if 22: else 23:

for i = 1 to n. numChildren do end for 26: end if may also have an attribute info, containing the subject name for input and output nodes and the De Bruijn indices for variable nodes. When we use assignment n 1 = n 2 on record types we assume that all the fields are copied.

Consider the pseudocode for Normalization Step 1. The step performs a visit of the tree rooted at n applying the normalization rules. Item (1) of the normalization step is represented by lines 2-3, while item (2) is represented by lines 4-7. Item (3) is represented by lines 10-21.

In the pseudocode for Normalization Step 2 we assume auxiliary operations comp for comparing the subtrees rooted at two nodes, sortChildren for lexicographic ordering of children of a node (e.g., using MERGESORT) and deleteRec for deleting a subtree.

The pseudocode for Normalization Step 3 exploits an auxiliary operation too. Operation subtree(p 1 , p 2 , c) takes as arguments two pointers to nodes p 1 and p 2 and a name c. It checks whether p 2 points to an input node with label c and with a subtree equal to p 1 . The De Bruijn indices in p 1 must differ by 1 w.r.t. the corresponding ones of p 2 for the comparison to succeed. This is required to take into account the additional Normalization Step 2 NS2(n) Require: A tree node n 1: for i = 1 to n. numChildren do end for 12: end if input prefix in front of p 2 .

In Normalization Step 3, lines 9-18 check whether node n is the root of a subtree to which the axiom schema DIS can be applied. There are two possibilities to consider, since the subtree P can be either the first child in the parallel composition or the last one (remember that children of the parallel composition have been sorted by Normalization Step 2). If variable ok is true then the axiom schema can be applied, and variables small and big point to the child containing P and to one of the other children, respectively (all the other children correspond to the same node). Lines 20-25 apply the axiom schema if needed. Line 23 makes all the children point to the same node, the one indexed by big, by changing the only different pointer, the one indexed by small. Then the child of this node is deleted together with its subtree, and replaced by pointing to the node that was pointed by small, which is pointed now by aux. This is needed to have the correct De Bruijn indices. In fact, De Bruijn indices of the child indexed by small already have the values needed for the final term.

We relate now normalization and bisimilarity. Lemma 6.12. Let T P , T Q be two tree representations of processes P and Q (as in Definition 6.11), normalized according to normalization steps 1 and 2. Then P ≡ Q iff T P = T Q .

Proof. Immediate from Definitions 2.2 and 6.11, and from normalization steps 1 and 2. In particular, N1 corresponds to the elimination of all occurrences of 0 in parallel, and N2 corresponds to the choice of a representative process, up to associativity and commutativity.

Lemma 6.13. Let P, Q be processes and T P , T Q their tree representations normalized according to steps 1, 2 and 3. Then P ∼ Q iff T P = T Q .

Proof. Immediate using Lemmas 6.12 and 6.6 (P Q implies P ∼ Q).

We now give a lemma on the cost of sorting the tree representation of a process.

depth is equal to 1: the first two recursive calls, each one having half of the original list. In general, at every slice one finds a partition of the list in 2 d sublists, where d is the recursion depth. Each recursive call in every slice is going to merge two sublists, with a complexity of the sum of the sizes of these sublists. Summing everything, we get a cost of t = i∈1..n size(P i ) at each recursion depth. Therefore, as there are log n different depths, the total complexity is O(t log n). Theorem 6.15. Consider two HOcore processes P and Q. P ∼ Q can be decided in time O(n 2 log m) where n = max (size(P ), size(Q)) (i.e., the maximum number of nodes in the tree representations of P and Q) and m is the maximum branching factor in them (i.e., the maximum number of components in a parallel composition).

Proof. Bisimilarity check proceeds as follows: first normalize the tree representations of the two processes, then check them for syntactic equality.

Normalization step 1 can be performed in time O(n), as can be seen from the corresponding pseudocode. Normalization step 2 performs a visit of the tree, sorting and removing duplicates from the children of parallel composition nodes. By Lemma 6.14 sorting can be done in O(n log m) for each parallel composition node. Removing duplicates requires just O(n) time. Normalization step 3 visits the tree too, possibly reconfiguring input nodes. The check for applicability requires one comparison (O(n)) and the check that all the other components coincide (simply check that the subtrees have been merged by Normalization step 2: O(n)). Applying N3 simply entails collapsing the trees (O(n)). Other nodes require no operations.

Thus the normalization for a single node can be done in O(n log m), and the whole normalization can be done in O(n 2 log m).

Bisimilarity is Undecidable with Four Static Restrictions

If the restriction operator is added to HOcore, as in Plain CHOCS or Higher-Order π-calculus, then recursion can be encoded [START_REF] Thomsen | Calculi for higher order communicating systems[END_REF][START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF] and most of the results in Sections 4-6 would break. In particular, higher-order and context bisimilarities are different and both undecidable [START_REF] Sangiorgi | Expressing mobility in process algebras: First-order and higherorder paradigms[END_REF][START_REF] Sangiorgi | Bisimulation for Higher-Order Process Calculi[END_REF].

We discuss here the addition of a limited form of restriction, which we call static restriction. These restrictions may not appear inside output messages: in any output a P , P is restriction-free. This limitation is important: it prevents for instance the above-mentioned encoding of recursion from being written. Static restrictions could also be defined as top-level restrictions since, by means of standard structural congruence laws (or similar laws allowing to swap input and restriction), any static restriction can be pulled out at the top-level. Thus the processes would take the form νa 1 . . . νa n P , where νa i indicates the restriction on the name a i , and where restriction cannot appear inside P itself. The operational semantics-LTS and bisimilarities-are extended as expected. For instance, one would have bounded outputs as actions, as well as rules

STRES P α -→ P z ∈ fn(α) νzP α -→ νzP STOPEN P ν v a R -----→ P z ∈ fn(R) \ v νzP νz v a R
------→ P defining static restriction and extrusion of restricted names, respectively. Note that there is no need to define how a bounded output interacts with input as every τ transition takes place under the restrictions. Also, structural congruence (Definition 2.2) would be extended with the axioms for restriction νz νwP ≡ νw νzP and νz0 ≡ 0. (In contrast, notice that we do not require the axiom: νz(P Q) ≡ P (νzQ), where z does not occur in P .) We sometimes write νa 1 , . . . , a n to stand for νa 1 , . . . , νa n .

We show that four static restrictions are enough to make undecidable any bisimilarity that has little more than a clause for τ -actions. For this, we reduce the Post correspondence problem (PCP) [START_REF] Post | A variant of a recursively unsolvable problem[END_REF][START_REF] Sipser | Introduction to the Theory of Computation[END_REF] to the bisimilarity of some processes. We call complete τ -bisimilarity any complete combination of the HOcore bisimulation clauses (as defined in Section 4) that includes the clause for τ actions (Definition 4.1(1)); the bisimilarity can even be asynchronous (Section 5). Definition 7.1 (PCP). An instance of PCP consists of an alphabet A containing at least two symbols, and a finite list T 1 , . . . , T n of tiles, where each tile is a pair of words over A. We use T i = (u i , l i ) to denote a tile T i with upper word u i and lower word l i . A solution to this instance is a non-empty sequence of indices i 1 , . . . , i k ,

1 ≤ i j ≤ n (j ∈ 1 • • • k), such that u i1 • • • u i k = l i1 • • • l i k .
The decision problem is then to determine whether such a solution exists or not.

Having (static) restrictions, we can refine the notation for non-nested replications (Definition 3.2) and define it in the unguarded case:

!P νc (Q c c Q c )
where Q c = c(x). (x c x P ) and P is a HOcore process (i.e., it is restriction-free). It is easy to see that !P τ -→ !P P . Now, !0 is a purely divergent process, as it can only make τ -transitions, indefinitely; it is written using only one static restriction. Given an instance of PCP we build a set of processes P 1 , . . . , P n , one for each tile T 1 , . . . , T n , and show that, for each i, P i is bisimilar to !0 iff the instance of PCP has no solution ending with T i . Thus PCP is solvable iff there exists j such that P j is not bisimilar to !0.

The processes P 1 , . . . , P n execute in two distinct phases: first they build a possible solution of PCP, then they non-deterministically stop building the solution and execute it. If the chosen composition is a solution then a signal on a free channel success is sent, thus performing a visible action, which breaks bisimilarity with !0.

The precise encoding of PCP into HOcore is shown in Table 3, and described below. We consider an alphabet of two letters, a 1 and a 2 . The upper and lower words of a tile are treated as separate strings, which are encoded letter by letter. The encoding of a letter is then a process whose continuation encodes the rest of the string, and varies depending on whether the letter occurs in the upper or in the lower word. We use a single channel to encode both letters: for the upper word, a 1 is encoded as a P and a 2 as a(x). (x P ), where P is the continuation and x does not occur in P ; for the lower word the encodings are switched. In Table 3, [[a i , P ]] w denotes the encoding of the ]] w , i.e., the first letter with the encoding of the rest as continuation. Notice that the encoding of an a i in the upper word can synchronize only with the encoding of a i for the lower word.

(up [[u k , x]]u low [[l k , y]] l ) STARTERS S k = up [[u k , b]]u low [[l k , b. success]] l EXECUTOR E = up(x). low(y). (x y) SYSTEM Pj = νup νlow νa νb ( Sj ! k C k E)
The whole system P j is composed by a (replicated) creator C k for each tile T k , a starter S j that launches the building of a tile composition ending with (u j , l j ), and an executor E. The starter makes the computation begin; creators non-deterministically add their tile to the beginning of the composition. Also non-deterministically, the executor blocks the building of the composition and starts its execution. This proceeds if no difference is found: if both strings end at the same character, then synchronization on channel b can be performed, which in turn, makes action success visible. Notice that without synchronizing on b, action success could be visible even in the case in which one of the strings is a prefix of the other one.

The encoding of replication requires another restriction, thus P j has five restrictions. However, names low and a are used in different phases; thus choosing low = a does not create interferences, and four restrictions are enough. Theorem 7.2. Given an instance of PCP and one of its tiles T j , there is a solution of the instance of PCP ending with T j iff P j is not bisimilar to !0 according to any complete τ -bisimilarity.

Proof. We start by proving the left to right implication. Note that !0 has a unique possible computation, that is infinite and includes only τ actions. Let T i1 , . . . , T im be a solution of the instance of the PCP problem such that T im = T j . Then P j can perform the computation described below, which contains the action success, thus it is not bisimilar to !0. The computation is as follows:

1. P j τ -→ * νup, a, b. S j h=1..m-1 C i h C ! k C k E = P 1
, by replication unfolding (the C is the parallel composition of the creators that have been replicated and will not be used);

2. P 1 τ -→ * νup, a, b. up [[u, b]] u a [[l, b. success]] l C ! k C k E = P 2
, where (u, l) is the solution of the instance of the PCP problem, by making the starter S j interact with the creators C im-1 . . C i1 ; 3.

P 2 τ -→ τ -→ νup, a, b. C ! k C k [[u, b]] u [[l, b.
success]] l = P 3 , by making the starter interact with the executor (note that as every creator starts by an input on up, none of them my be triggered by messages on a); For the other implication, first notice that all the computations of P j are infinite since one can always unfold recursion, and action success is the only possible visible action. Thus the only possibility for having P j not bisimilar to !0 is that P j has a computation executing success. The only computations that may produce success are structured as follows: they build two strings by concatenating the tiles, and then they execute them. One can prove by induction on the minimum length of the strings that if the two strings are different then either their execution gets stuck, or synchronization at b is not possible (this last case occurs if one of the strings is a prefix of the other). Thus, the two strings must be equal and they are the solution of the instance of the PCP problem.

Corollary 7.3. Barbed congruence and any complete τ -bisimilarity are undecidable in HOcore with four static restrictions. Theorem 7.2 actually shows that even asynchronous barbed bisimilarity (defined as the largest τ -bisimilarity that is output-barb preserving, and used in the definition of ordinary-as opposed to reduction-closed-barbed congruence) is undecidable. The corollary above then follows from the fact that all the relations there mentioned are at least as demanding as asynchronous barbed bisimilarity.

Other Extensions

We now examine the impact on decidability of bisimilarity of some extensions of HOcore. We omit the details, including precise statements of the results.

Abstractions. An abstraction is an expression of the form (x)P ; it is a parametrized process. An abstraction has a functional type. Applying an abstraction (x)P of type T → ♦ (where ♦ is the type of all processes) to an argument W of type T yields the process P { W /x}. The argument W can itself be an abstraction; therefore the order of an abstraction, that is, the level of arrow nesting in its type, can be arbitrarily high. The order can also be ω, if there are recursive types. By setting bounds on the order of the types of abstractions, one can define a hierarchy of subcalculi of the Higher-Order π-calculus [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]; and when this bound is ω, one obtains a calculus capable of representing the π-calculus (for this all operators of the Higher-Order π-calculus are needed, including full restriction).

Allowing the communication of abstractions, as in the Higher-Order π-calculus, one then also needs to add in the grammar for processes an application construct of the form P 1 P 2 , as a destructor for abstractions. Extensions in the LTS would be as follows. Suppose, as in [START_REF] Sangiorgi | π-calculus, internal mobility and agent-passing calculi[END_REF], that beta-conversion is the least precongruence on HOcore processes generated by the rule

(x)P 1 P 2 P 1 { P2 /x}.
The LTS could be then extended with a rule

BETA P P 1 P 1 α -→ Q P α -→ Q
Notice that with these additions, the characterization of bisimilarity as IO bisimilarity still holds. For a HOcore extended with abstractions and applications, ∼ o IO is still a congruence and is preserved by substitutions (by straightforward extensions of the proofs of Lemmas 4.9 and 4.10). Note that, however, abstraction application may increase the size of processes. If abstractions are of finite type (i.e., their order is smaller than ω) then only a finite number of such applications is possible, and decidability of bisimilarity is preserved. Decidability fails if the order is ω, intuitively because in this case it is possible to simulate the λ-calculus.

Output prefix. If we add an output prefix construct a P . Q to HOcore, then the proof of the characterization as IO bisimilarity breaks and, with it, the proof of decidability. Decidability proofs can however be adjusted by appealing to results on unique decomposition of processes and axiomatization (along the lines of Section 6).

Choice. Decidability remains with the addition of a choice operator to HOcore. The proofs require little modifications. The addition of both choice and output prefix is harder. It might be possible to extend the decidability proof for output prefix mentioned above so to accommodate also choice, but the details become much more complex.

Recursion. We do not know whether decidability is maintained by the addition of recursion (or similar operators such as replication).

Concluding Remarks

Process calculi are usually Turing complete and have an undecidable bisimilarity (and barbed congruence). Subcalculi have been studied where bisimilarity becomes decidable but then one loses Turing completeness. Examples are BPA and BPP (see, e.g., [START_REF] Kučera | Equivalence-checking on infinite-state systems: Techniques and results[END_REF]) and CCS without restriction and relabeling [START_REF] Christensen | Decidable subsets of CCS[END_REF]. In this paper we have identified a Turing complete formalism, HOcore, for which bisimilarity is decidable. We do not know other concurrency formalisms where the same happens. Other peculiarities of HOcore are:

1. it is higher-order, and contextual bisimilarities (barbed congruence) coincide with higher-order bisimilarity (as well as with others, such as context and normal bisimilarities); and 2. it is asynchronous (in that there is no continuation underneath an output), yet asynchronous and synchronous bisimilarities coincide.

We do not know other non-trivial formalisms in which properties (1) or ( 2) hold (of course (1) makes sense only on higher-order models).

We have also given an axiomatization for bisimilarity. From this we have derived polynomial upper bounds to the decidability of bisimilarity. The axiomatization also intuitively explains why results such as decidability, and the collapse of many forms of bisimilarity, are possible even though HOcore is Turing complete: the bisimilarity relation is very discriminating.

We have used encodings of Minsky machines and of the Post correspondence problem (PCP) for our undecidability results. The encodings are tailored to analyze different problems: undecidability of termination, and undecidability of bisimilarity with static restrictions. The PCP encoding is always divergent, and therefore cannot be used to reason about termination. On the other hand, the encoding of Minsky machines would require at least one restriction for each instruction of the machine, and therefore would have given us a (much) worse result for static restrictions. We find both encodings interesting: they show different ways to exploit higher-order communications for modeling.

We have shown that bisimilarity becomes undecidable with the addition of four static restrictions. We do not know what happens with one, two, or three static restrictions. We also do not know whether the results presented would hold when one abstracts from τ -actions and moves to weak equivalences. The problem seems much harder; it reminds us of the situation for BPA and BPP, where strong bisimilarity is decidable but the decidability of weak bisimilarity is a long-standing open problem [START_REF] Kučera | Equivalence-checking on infinite-state systems: Techniques and results[END_REF].

Related Work. Recent progresses to the behavioral theory of higher-order processes are related to the results of this paper. Some of them, such as environmental bisimulations [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF] and the bisimilarities for calculi with passivation constructs [START_REF] Lenglet | Normal bisimulations in calculi with passivation[END_REF][START_REF] Lenglet | Howe's method for calculi with passivation[END_REF], have been already mentioned. Koutavas and Hennessy [START_REF] Koutavas | First-order reasoning for higher-order concurrency[END_REF] have proposed a first-order behavioral theory for higher-order processes, based on the combination of the principles of environmental bisimulations and the improvements to normal bisimilarity proposed by Jeffrey and Rathke in [START_REF] Jeffrey | Contextual equivalence for higher-order pi-calculus revisited[END_REF]. At the heart of the proposed theory is a novel treatment of name extrusions, which is formalized as an LTS in which configurations not only contain a process and the current knowledge of its environment, but also information on the names that have been extruded by it. As a consequence, the labels of such an LTS have a very simple structure. This is the simplest presentation of an LTS for a higher-order process calculus we are aware of. The weak bisimilarity derived from the proposed LTS is shown to be a congruence, fully abstract with respect to contextual equivalence, and to have a logic characterization using a propositional Hennessy-Milner logic. These results are shown to scale up to (higher-order) languages with distribution, such as the one introduced in [START_REF] Vivas | From higher-order pi-calculus to pi-calculus in the presence of static operators[END_REF], for which practical translations into first-order calculi do not exist.

As mentioned in the Introduction, in expressiveness studies for higher-order process calculi the usual yardstick for comparison is given by first-order languages such as the π-calculus. A representative work is [START_REF] Sangiorgi | π-calculus, internal mobility and agent-passing calculi[END_REF], where a hierarchy of HOπ fragments (obtained by varying the degree of the abstractions allowed) is shown to match the expressiveness of a hierarchy of first-order calculi with only internal mobility. In the same vein is [START_REF] Bundgaard | On encoding the pi-calculus in higher-order calculi[END_REF], which, inspired by the encoding given in [START_REF] Thomsen | Plain CHOCS: A second generation calculus for higher order processes[END_REF], presents an encoding of the π-calculus into Homer, a higher-order process calculus with locations [START_REF] Bundgaard | Bisimulation congruences for homer -a calculus of higher order mobile embedded resources[END_REF]. Such an encoding is exploited in [START_REF] Bundgaard | Decidable fragments of a higher order calculus with locations[END_REF] as a way of characterizing finite-control fragments of Homer in which barbed bisimilarity is decidable.

The encoding of Turing complete models (such as Minsky and Random Access Machines, RAMs [START_REF] Shepherdson | Computability of recursive functions[END_REF]) is a common proof technique for carrying out expressiveness studies. Our encoding of Minsky machines into HOcore resembles in structure those in [START_REF] Busi | Replication vs. recursive definitions in channel based calculi[END_REF][START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF], where RAMs are used to investigate the expressive power of restriction and replication in name-passing calculi, and those in [START_REF] Busi | On the expressive power of movement and restriction in pure mobile ambients[END_REF], where the impact of restriction and movement on the expressiveness of Ambient calculi is studied. All these encodings share the same guiding principle: representing counting as the nesting of suitable components. Those components are restricted names in CCS [START_REF] Busi | Replication vs. recursive definitions in channel based calculi[END_REF][START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF], recursive definitions in π-calculus [START_REF] Busi | Replication vs. recursive definitions in channel based calculi[END_REF], ambients themselves in Ambient calculus [START_REF] Busi | On the expressive power of movement and restriction in pure mobile ambients[END_REF], and higher-order messages in our case. Note that by combining our encoding with the one of higherorder π into π-calculus in [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF], we obtain an encoding very similar to the one in [START_REF] Busi | Replication vs. recursive definitions in channel based calculi[END_REF]. Reductions from the PCP to prove undecidability results have been used in other settings. For instance, suitable reductions are used in [START_REF] Nielsen | On the expressive power of temporal concurrent constraint programming languages[END_REF] to show the undecidability of equivalences in timed concurrent constraint languages, and in [START_REF] Charatonik | The decidability of model checking mobile ambients[END_REF] to show undecidability of the model checking problem for the Ambient calculus without restriction but with replication.

A number of expressiveness and decidability results for variants/extensions of HOcore that complement the results here presented have been reported in [START_REF] Pérez | Higher-Order Concurrency: Expressiveness and Decidability Results[END_REF][START_REF] Di Giusto | On the expressiveness of forwarding in higher-order communication[END_REF][START_REF] Lanese | On the expressiveness of polyadic and synchronous communication in higher-order process calculi[END_REF]. In an attempt to understand the source of expressive power in HOcore, [START_REF] Di Giusto | On the expressiveness of forwarding in higher-order communication[END_REF] studies the fragment of HOcore in which nested higher-order output actions are disallowed. Hence, the encoding of Minsky machines in Section 3 is not expressible in such a fragment. The focus of [START_REF] Di Giusto | On the expressiveness of forwarding in higher-order communication[END_REF] is in the (un)decidability of termination (i.e., the absence of divergent computation) and convergence (i.e., the existence of a non-diverging computation) in the mentioned fragment. The main result in [START_REF] Di Giusto | On the expressiveness of forwarding in higher-order communication[END_REF] is that, in contrast to HOcore, in the fragment without nested higher-order outputs termination becomes decidable, while convergence remains undecidable (as in HOcore). While the latter result is shown by means of a non-deterministic encoding of Minsky machines, the former result is obtained by appealing to the theory of well-structured transition systems, following the approach in [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF]. This result is then strengthened in [START_REF] Pérez | Higher-Order Concurrency: Expressiveness and Decidability Results[END_REF]Chapter 5] where it is shown that when the fragment of HOcore considered in [START_REF] Di Giusto | On the expressiveness of forwarding in higher-order communication[END_REF] is extended with a passivation operator (as in Homer and the Kell calculus [START_REF] Schmitt | The kell calculus: A family of higher-order distributed process calculi[END_REF]) full Turing completeness (as in HOcore) is recovered, and hence termination is undecidable. Finally, [START_REF] Lanese | On the expressiveness of polyadic and synchronous communication in higher-order process calculi[END_REF][START_REF] Pérez | Higher-Order Concurrency: Expressiveness and Decidability Results[END_REF]Chapter 6] studies the expressiveness of (a)synchronous and polyadic communication in the context of strictly higher-order process calculi (roughly, variants of HOcore with restriction). Three main results are obtained. First, similarly to first-order calculi, synchronous process passing is shown to be encodable into asynchronous process passing. Then, it is shown that the absence of name passing leads to a hierarchy of higher-order process calculi based on the arity allowed in polyadic communication, thus revealing a striking point of contrast with respect to first-order calculi. Finally, the passing of abstractions is shown to be more expressive than process passing alone.

Lemma 2 . 3 .

 23 If P α -→ P and P ≡ Q then there exists Q such that Q α -→ Q and P ≡ Q . Proof. By induction on the derivation of P ≡ Q, then by case analysis on P α -→ Q.

  with variables x guarded in P , and free variables in R disjoint from the variables in P and x, then there are P and α such that P α -→ P , M = P { R / x}, α = α{ R / x}, and the free variables in R are disjoint from the variables in α. 3. if P { m / x} α --→ M with m fresh in P and α = m i for any m i ∈ m, then P α -→ P , M = P { m / x}, and α = α{ m / x}.

Definition 4 . 1 (

 41 HOcore bisimulation clauses, open processes). A symmetric relation R on HOcore processes is

Definition 4 . 2 (

 42 HOcore bisimulation clauses, closed processes). A symmetric relation R on closed HOcore processes is 1. an output context bisimulation if P R Q and P a P

Remark 4 . 4 .

 44 The input clause of Definition 4.2(

Definition 4 . 7 .

 47 A symmetric relation R on HOcore is an open IO bisimulation up-to

Lemma 4 . 15 .

 415 If m. P 1 P ∼ o NOR m. Q 1 Q, for some fresh m, then we have P 1 ∼ o NOR Q 1 and P ∼ o NOR Q.

Lemma 4 .

 4 18. ∼ NOR implies ∼ o NOR . Proof. Remember that ∼ NOR is the extension of ∼ NOR to open processes (see Definition 4.6). Notice that since ∼ NOR is an input normal bisimulation (Definition 4.2(2)), we can easily show that P ∼ NOR Q iff P { m1 /x1, . . . , mn /xn} ∼ NOR Q{ m1 /x1, . . . , mn /xn} where {x 1 , . . . , x n } = fv(P ) ∪ fv(Q) and m 1 , . . . , m n are fresh names. We now show that ∼ NOR is an open normal bisimulation.

  m1 /x1, . . . , mn /xn} a(x) ---→ Q { m1 /x1, . . . , mn /xn} with (for some fresh m) P { m1 /x1, . . . , mn /xn}{ m /x} ∼ NOR Q { m1 /x1, . . . , mn /xn}{ m /x}. By Lemma 2.5(3), we have Q a(x)

Definition 5 . 1 .

 51 Asynchronous barbed congruence, , is the largest symmetric relation on closed processes that is 1. a τ -bisimulation (Definition 4.1(1)); 2. context-closed (i.e., P Q implies C[P ] C[Q], for all closed contexts C[•]); 3. barb preserving (i.e., if P Q and P ↓ a , then also Q ↓ a ).

29 Normalization Step 1 2 : 3 :n. type = zero 4 :

 291234 NS1(n) Require: A tree node n 1: if n. type = par then if n. numChildren = 0 then else if n. numChildren = 1 then 5:

  for i = 1 to n. numChildren do 12: NS1( * (n. children[i])) 13:

6 : 7 :

 67 n. children[i])) 3: end for 4: if n. type = par then for i = 1 to n. numChildren -1 do if comp( * (n. children[i]), * (n. children[i + 1])) = true then 8: deleteRec(n. children[i + 1]) 9: n. children[i + 1] = n. children[i]

LETTERS[

  [a1, P ]]u = [[a2, P ]] l = a P [[a2, P ]]u = [[a1, P ]] l = a(x). (x P ) STRINGS [[ai • s, P ]]w = [[ai, [[s, P ]]w]]w [[ , P ]]w = P ( is the empty word) CREATORS C k = up(x). low(y).

4. P 3 τ

 3 -→ * νup, a, b. C ! k C k b b. success = P 4 , by executing the encodings of the two strings, exploiting the fact that they are equal; 5. P 4 τ -→ νup, a, b. C ! k C k success = P 5 , by synchronizing on b; 6. P 5 success -----→ νup, a, b. C ! k C k .

Table 1 :

 1 Reduction of Minsky machines

Table 2 :

 2 Encoding of Minsky machines

  • • • . a(x n ). Q leading to Q{ Ri / xi}. These last are bisimilar for any choice of the R i by hypothesis, thus the thesis follows. Lemma 4.14. ∼ o IO and ∼ HO coincide. Proof. To show that ∼ HO is a IO bisimulation we show a slightly more general result: the relation {(P, Q) | P { mi / xi} ∼ HO Q{ mi / xi}, m i fresh in relation to P, Q} is a IO bisimulation. Note that we still use the open extension ∼ HO , and do not require every variable of P and Q to be substituted by fresh names. Let P, Q be two processes such that P { mi / xi} ∼ HO Q{ mi / xi}. If either P or Q has an unguarded variable x, we let m stand for a fresh variable and consider P { mi / xi}{ m /x} and Q{ mi / xi}{ m /x}. We easily show that P { mi / xi}{ m /x} ∼ HO Q{ mi / xi}{ m /x}. To keep notations short, we still write P { mi / xi} and Q{ mi / xi} for the saturated processes with no unguarded variable.

  x} for any closed R, and we also conclude by Lemma 4.13 that P { mi / xi} ∼ HO Q { mi / xi}, thus P and Q are still in the relation.The final case is for when P ≡ x P . By hypothesis, we have P { mi / xi} ∼ HO Q{ mi / xi} and we know that x = x i for some i. We thus haveP { mi / xi} = m i P { mi / xi} ∼ HO Q{ mi / xi}. Let{y 1 , . . . , y n } be the free guarded variables of P { mi / xi} and Q{ mi / xi}, and let R 1 , . . . , R n be closed processes. By Lemma 4.13, we have P { mi / xi}{ Rj / yj} ∼ HO Q{ mi / xi}{ Rj / yj}. As the R j are closed, by Lemma 2.5(1), we have P { mi / xi}{ Rj / yj} mi --→ P { mi / xi}{ Rj / yj}. We have Q{ mi / xi}{ Rj / yj} Q { mi / xi}{ Rj / yj} by definition of ∼ HO , and by Lemma 2.5(2) we have Q{ mi / xi}

	mi

mi

--→

  x1, . . . , mn /xn} = m 1 Q * Lemma 4.15 we conclude that P ∼ o NOR Q and P ∼ o NOR Q . Lemma 4.20. In HOcore, relations ∼ HO , ∼ o NOR and ∼ CON coincide on closed processe. Proof. This is an immediate consequence of previous results. In fact, we have proved (on open processes) the following implications: 1. ∼ o IO implies ∼ HO (Lemma 4.14). 2. ∼ HO implies ∼ CON (Lemma 4.16); 3. ∼ CON implies ∼ NOR (Lemma 4.

	as desired.
	Lemma 4.19. ∼ o NOR implies ∼ o IO .
	a Q ----→ Q , with m. P	P ∼ o NOR m. Q	Q .
	Using this and 17);
	4. ∼ NOR implies ∼ o NOR (Lemma 4.18);
	5. ∼ o NOR implies ∼ o IO (Lemma 4.19).

Proof. The only difference between the bisimilarities is their output clause: they are both open bisimulations. We analyze directly the case for output action. Suppose P ∼ o NOR Q and P a P ----→ P ; we need to show a matching action from Q. By definition of ∼ o NOR , if P a P

----→ P then also Q

Table 3 :

 3 Encoding of PCP letter a i with continuation P , with w = u if the encoding is on the upper word, w = l otherwise. Hence, given a string s = a i •s , its encoding [[s, P ]] w is [[a i , [[s , P ]] w

The clauses of Definition 4.2 are however tailored to closed processes, therefore combining them with clause 4 in Definition 4.1 has little interest.

Acknowledgments. This research was initiated by some remarks and email exchange with Naoki Kobayashi. We also benefited from exchanges with Jesús Aranda, Cinzia Di Giusto, Maurizio Gabbrielli, Antonín Kučera, Sergueï Lenglet, Nobuko Yoshida, and Gianluigi Zavattaro, from feedback of the readers of the Moca and Concurrency mailing lists, and from the comments and remarks of the anonymous referees.

$$ Research partially supported by European projects FET-GC II IST-2005-16004 SENSORIA and FP7-231620 HATS and by French ANR project "CHOCO".

After an input action on the right-hand side, we derive P ∼ A i l =i a(x). A l for every i ≤ k. In particular, when i = j, we have P ∼ A i a(x). A j l / ∈{i,j} a(x). A l P ∼ A j a(x). A i l / ∈{i,j} a(x). A l and, by Proposition 6.3, A i a(x). A j ∼ A j a(x). A i . Since a(x). A i is prime and it has larger size than A i (and any of its components), it should correspond in the prime decomposition to a(x). A j , i.e., a(x). A i ∼ a(x). A j . As this was shown for every i = j, we thus have a(x). P ∼ k 1 a(x). A 1 with k > 1 and a(x). A 1 in normal form. Lemma 6.8. For A, B in normal form, if A ∼ B then A ≡ B.

Proof. We show, simultaneously, the following two properties:

1. if A is a prefixed process in normal form, then A is prime; 2. for any B in normal form, A ∼ B implies A ≡ B.

We proceed by induction on n, for all A with #(A) = n. The case n = 0 is immediate as the only process of this size is 0. Suppose that the property holds for all i < n, with n ≥ 1. In the reasoning below, we exploit the characterization of ∼ as ∼ o IO . 1. Process A is of the form a(x). A . Suppose, as a contradiction, that A is not prime. Then we have A ∼ P 1 P 2 with P 1 and P 2 non-trivial. By Lemma 6.7, then A ∼ Π k 1 a(x). B with k > 1 and a(x). B in normal form. By consuming the prefix on the left-hand side, we have A ∼ B Π k-1 1 a(x). B. It follows by induction (using property (2)) that A ≡ B Π k-1 1 a(x). B, and hence also A ≡ a(x). (B Π k-1 1 a(x). B). This is impossible, as A is in normal form. 2. Suppose A ∼ B. We proceed by case analysis on the structure of A.

• Case A = x. We have that B should be the same variable, so A ≡ B trivially.

• Case A = a P . We have that B = a P with P ∼ P by definition of ∼ o IO . By the induction hypothesis, P ≡ P , thus a P ≡ a P . end if 28: end if Given a process P , we define the size of its tree representation T P to be the number of nodes of the tree, and denote it as size(P ). Lemma 6.14. Consider n HOcore processes P 1 , . . . , P n and their tree representations T P1 , . . . , T Pn . Their sorting has complexity O(t log n), where t = i∈1..n size(P i ).

Proof. Let us assume MERGESORT as sorting algorithm. MERGESORT sorts a list of elements by (i) splitting the list to be sorted in two; (ii) recursing on both sublists; and (iii) merging the sorted sublists. A merge function starts by comparing the first element of each list and then copies the smallest one to the new list. Comparing two elements P i , P j costs min (size(P i ), size(P j )). As each T Pi is considered once (when it is copied to the new list) the cost of merging two lists is the sum of the size of their elements (the actual copying of an element has constant cost since it is just a pointer operation). Let us call a slice of MERGESORT the juxtaposition of every recursive call at the same depth. In this way, e.g., the first slice considers the lists when recursion Appendix A. Proof of Lemma 3.4 This appendix is devoted to the proof of correctness of the encoding of Minsky machines into HOcore. In what follows we assume a Minsky machine N with instructions (1 : I 1 ), . . . , (n : I n ) and with registers r 0 = m 0 and

We use -→ j to stand for a sequence of j reductions.

Lemma (Soundness). Let (i, m 0 , m 1 ) be a configuration of a Minsky machine N . If (i, m 0 , m 1 ) -→ M (i , m 0 , m 1 ) then there exist a finite j and a process P such that [[(i, m 0 , m 1 ) N ]] M -→ j P and P = [[(i , m 0 , m 1 ) N ]] M .

Proof. We proceed by case analysis on the instruction performed by the Minsky machine. Hence, we distinguish three cases corresponding to the behaviors associated to rules M-JMP, M-DEC, and M-INC.

Case M-JMP. We have a Minsky configuration (i, m 0 , m 1 ) with m 0 = 0 and (i : DECJ(r 0 , k)). By Definition 3.3, its encoding in HOcore is as follows:

We begin by noting that the program counter p i is consumed by the encoding of the instruction i. The content of the instruction is thus exposed, and we then have

stands for the rest of the system. The only transition possible at this point is the behavior selection on dec 0 , which yields the following:

Now there is a synchronization between r 0 0 and REG 0 for reconstructing the register (with an extra step to unfold the recursion again)

Once the register has been re-created, register and instruction can now synchronize on ack:

At this point, the only possible transition is the behavior selection on z 0 , which indicates that the content of r 0 was indeed zero:

Using the definitions of [[•]]

M and S, and some reordering, we note that P 5 can be equivalently written as

which, in turn, corresponds to the encoding of [[(k, 0, m 1 ) N ]] M , as desired.

Case M-DEC. We have a Minsky configuration (i, m 0 , m 1 ) with m 0 = c (for some c > 0) and (i : DECJ(r 0 , k)). By Definition 3.3, its encoding in HOcore is as follows:

We begin by noting that the program counter p i is consumed by the encoding of the instruction i. The content of the instruction is thus exposed, and we then have

] M stands for the rest of the system. The only transition possible at this point is the behavior selection on dec 0 , which yields the following:

Considering this, now there is a synchronization between r S 0 and REG 0 for decrementing the value of the register (with an extra step to unfold the recursion again)

Once the register has been re-created, register and instruction can now synchronize on ack:

At this point, the only possible transition is the behavior selection on n 0 , which indicates that the content of r 0 was greater than zero:

Using the definitions of [[•]] M and S, and some reordering, we note that P 5 can be equivalently written as

Case M-INC. We have a Minsky configuration (i, m 0 , m 1 ) with (i : INC(r 0 )). Its encoding in HOcore is as follows:

We begin by noting that the program counter p i is consumed by the encoding of the instruction i:

] M stands for the rest of the system. The only transition possible at this point is the behavior selection on inc 0 . After such a selection we have

Now there is a synchronization between r S 0 and REG 0 for incrementing the value of the register

Once the register has been re-created, a synchronization on ack is possible

Using the definition of (| • |) j we note that P 4 actually corresponds to

which in turn can be written as

Lemma (Completeness). Let (i, m 0 , m 1 ) be a configuration of a Minsky machine N .

If [[(i, m 0 , m 1 ) N ]] M -→ P 1 then

• if P 1 contain inc j (j ∈ {0, 1}) then the only computation possible is P 1 -→ 4 P J ;

• if P 1 contain dec j (j ∈ {0, 1}) then the only computation possible is P 1 -→ 5 P J .

In both cases, we have

An analysis of the structure of process [[(i, m 0 , m 1 ) N ]] M reveals that, in all cases, the only possibility for the first step corresponds to the consumption of the program counter p i , releasing either inc j or dec j (j ∈ {0, 1}). This implies that there exists an instruction labeled with i, that can be executed from the configuration (i, m 0 , m 1 ). We proceed by a case analysis on the possible instruction, considering also the fact that the register on which the instruction acts can hold a value equal or greater than zero. In all cases, it can be shown that computation evolves deterministically, until reaching a process in which a new program counter (that is, some p i ) appears. The program counter p i is inside a process that corresponds to [[(i , m 0 , m 1 ) N ]] M , where (i, m 0 , m 1 ) -→ M (i , m 0 , m 1 ). The analysis follows the same lines as the one reported for the proof of the soundness lemma above, and we omit it.

Lemma. Let N be a Minsky machine. We have that N M if and only if

Proof. Straightforward from the soundness and completeness lemmas given above.