Yuxin Deng

Yuan Feng

Open Bisimulation for Quantum Processes

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The theory of quantum computing has attracted considerable research efforts in the past twenty years. Benefiting from the superposition of quantum states and linearity of quantum operations, quantum computing may provide considerable speedup over its classical analogue [START_REF] Shor | Algorithms for quantum computation: discrete log and factoring[END_REF][START_REF] Grover | A fast quantum mechanical algorithm for database search[END_REF][START_REF] Grover | Quantum mechanics helps in searching for a needle in a haystack[END_REF].

As is well known, it is very difficult to guarantee the correctness of classical communication protocols at the design stage, and some simple protocols were eventually found to have fundamental flaws. One expects that the design of complex quantum protocols is at least as error-prone, if not more, than in the classical case. In view of the success that classical process algebras [START_REF] Milner | Communication and Concurrency[END_REF][START_REF] Hoare | Communicating Sequential Processes[END_REF]1] achieved in analyzing and verifying classical communication protocols, several research groups proposed various quantum process algebras with the purpose of modeling quantum protocols. Jorrand and Lalire [START_REF] Jorrand | Toward a quantum process algebra[END_REF][START_REF] Lalire | Relations among quantum processes: Bisimilarity and congruence[END_REF] defined a language QPAlg (Quantum Process Algebra) by adding primitives expressing unitary transformations and quantum measurements, as well as communications of quantum states, to a CCS-like classical process algebra. An operational semantics of QPAlg is given, and further a probabilistic branching bisimulation between quantum processes is defined. Gay and Nagarajan [START_REF] Gay | Communicating quantum processes[END_REF][START_REF] Gay | Types and typechecking for communicating quantum processes[END_REF] proposed a language CQP (Communicating Quantum Processes), which is obtained from the pi-calculus [START_REF] Milner | A calculus of mobile processes, Parts I and II[END_REF] by adding primitives for measurements and transformations of quantum states, and allowing transmission of qubits. They presented a type system for CQP, and in particular proved that the semantics preserves typing and that typing guarantees that each qubit is owned by a unique process within a system. A probabilistic branching bisimulation for CQP was proposed by Davidson [3] and shown to be a congruence. The second author of the current paper, together with his colleagues, proposed a language named qCCS [START_REF] Feng | Probabilistic bisimulations for quantum processes[END_REF][START_REF] Ying | An algebra of quantum processes[END_REF]9] for quantum communicating systems by adding quantum input/output and quantum operation/measurement primitives to classical value-passing CCS [START_REF] Hennessy | A proof system for communicating processes with value-passing[END_REF][START_REF] Hennessy | A theory of communicating processes valuepassing[END_REF]. One distinctive feature of qCCS, compared to QPAlg and CQP, is that it provides a framework to describe, as well as reason about, the communication of quantum systems which are entangled with other systems. Furthermore, a bisimulation for processes in qCCS has been introduced, and the associated bisimilarity is proven to be a congruence with respect to all process constructors of qCCS. Uniqueness of the solutions to recursive process equations is also established, which provides a powerful proof technique for verifying complex quantum protocols.

In the study of quantum systems, as well as classical communicating systems, an important problem is to tell if two given systems exhibit the same behaviour, as this may allow us to replace a complex system with a simplified but equivalent one. To approach the problem we first need to give criteria for reasonable behavioural equivalence. Two systems should only be distinguished on the basis of the chosen criteria. Therefore, these criteria induce an extensional equivalence between systems, ≈ behav , namely the largest equivalence which satisfies them.

Having an independent notion of which systems should, and which should not, be distinguished, one can then justify a particular notion of equivalence, e.g. bisimulation, by showing that it captures precisely the touchstone equivalence. In other words, a particular definition of bisimulation is appropriate because the associated bisimulation equivalence, say ≈ bis , is sound with respect to the touchstone equivalence and provides for it a complete proof methodology, i.e. s 1 ≈ bis s 2 if and only if s 1 ≈ behav s 2 . This approach originated in [START_REF] Honda | On reduction-based process semantics[END_REF] but has now been widely used for different process description languages; for example, see [START_REF] Jeffrey | Contextual equivalence for higher-order pi-calculus revisited[END_REF][START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF] for its application to higher-order process languages, [START_REF] Rathke | Deriving structural labelled transitions for mobile ambients[END_REF] for mobile ambients, [START_REF] Fournet | A hierarchy of equivalences for asynchronous calculi[END_REF] for asynchronous languages and [START_REF] Deng | On the semantics of Markov automata[END_REF] for probabilistic timed languages. Moreover, in each case the distinguishing criteria are almost the same. The touchstone equivalence should be compositional (preserved by some natural operators for constructing systems), barb-preserving (equivalent processes exhibit the same observables) and reduction-closed (nondeterministic choices are in some sense preserved).

We adapt this approach to quantum processes. Using natural versions of these criteria we obtain an appropriate touchstone equivalence, which we call reduction barbed congruence, ≈ r . We then develop a theory of bisimulations which is both sound and complete for ≈ r . Moreover, we provide a modal characterisation of ≈ r in a quantum logic based on Hennessy-Milner logic [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF] by establishing the coincidence of the largest bisimulation with logical equivalence.

Due to lack of space, we omit all proofs; they can be found in [START_REF] Deng | Open bisimulation for quantum processes[END_REF]. We also refer the readers to [START_REF] Nielsen | Quantum computation and quantum information[END_REF] for the basic notions of linear algebra and quantum information theory used in this paper.

A probabilistic model

We review the model of probabilistic labelled transition systems (pLTSs). Later on we will interpret the behaviour of quantum processes in terms of pLTSs because quantum measurements give rise to probability distributions naturally.

We begin with some notations. A (discrete) probability distribution over a set S is a function ∆ : S → [0, 1] with s∈S ∆(s) = 1; the support of such a ∆ is the set ∆ = { s ∈ S | ∆(s) > 0 }. The point distribution s assigns probability 1 to s and 0 to all other elements of S, so that s = {s}. In this paper we only need to use distributions with finite support, and let Dist(S) denote the set of finite support distributions over S, ranged over by ∆, Θ etc. If k∈K p k = 1 for some collection of p k ≥ 0, and the ∆ k are distributions, then so is

k∈K p k • ∆ k with ( k∈K p k • ∆ k )(s) = k∈K p k • ∆ k (s).
Definition 1. A probabilistic labelled transition system is a triple S, Act τ , → , where S is a set of states, Act τ is a set of labels Act augmented with distinguished element τ , and → is a subset of S × Act τ × Dist(S).

We often write s α -→ ∆ for (s, α, ∆) ∈→, and s α -→ for ∃∆ : s α -→ ∆. In a pLTS actions are only performed by states, in that actions are given by relations from states to distributions. But in general we allow distributions over states to perform an action. For this purpose, we lift these relations so that they also apply to distributions [START_REF] Deng | Testing finitary probabilistic processes (extended abstract)[END_REF].

(i) s R Θ implies s R • Θ; (ii) ∆ i R • Θ i for all i ∈ I implies ( i∈I p i • ∆ i ) R • ( i∈I p i • Θ i ) for any p i ∈ [0, 1] with i∈I p i = 1
, where I is a countable index set.

We apply this operation to the relations α -→ in the pLTS for α ∈ Act τ , where we also write α -→ for ( α -→) • between distributions.

For simplicity, we combine the above two lifting operations and directly write R • for ( R)

• in the sequel, with the intention that a relation between states can be lifted to a relation between distributions via a special application of Definition 2. In this particular case, it holds that ∆ R • Θ implies Θ (R -1 )

• ∆, where s R t iff t R -1 s for any s, t ∈ S. This way of lifting relations has elegant mathematical characterisations; see [4] for more details.

Quantum CCS

We introduce a quantum extension of classical CCS (qCCS) which was originally studied in [START_REF] Feng | Probabilistic bisimulations for quantum processes[END_REF][START_REF] Ying | An algebra of quantum processes[END_REF]9]. Three types of data are considered in qCCS: as classical data we have Bool for booleans and Real for real numbers, and as quantum data we have Qbt for qubits. Consequently, two countably infinite sets of variables are assumed: cVar for classical variables, ranged over by x, y, ..., and qVar for quantum variables, ranged over by q, r, .... We assume a set Exp, which includes cVar as a subset and is ranged over by e, e , . . . , of classical data expressions over Real, and a set of boolean-valued expressions BExp, ranged over by b, b , . . . , with the usual boolean constants true, false, and operators ¬, ∧, ∨, and →.

In particular, we let e e be a boolean expression for any e, e ∈ Exp and ∈ {>, <, ≥, ≤, =}. We further assume that only classical variables can occur freely in both data expressions and boolean expressions. Two types of channels are used: cChan for classical channels, ranged over by c, d, ..., and qChan for quantum channels, ranged over by c, d,.... A relabelling function f is a map on cChan ∪ qChan such that f (cChan) ⊆ cChan and f (qChan) ⊆ qChan. Sometimes we abbreviate a sequence of distinct variables q 1 , ..., q n into q.

The terms in qCCS are given by:

P, Q ::= nil | τ.P | c?x.P | c!e.P | c?q.P | c!q.P | E[q].P | M [q; x].P | P + Q | P || Q | P [f ] | P \L | if b then P | A(q; x)
where f is a relabelling function and L ⊆ cChan ∪ qChan is a set of channels. Most of the constructors are standard as in CCS [START_REF] Milner | Communication and Concurrency[END_REF]. We briefly explain a few new constructors. The process c?q.P receives a quantum datum along quantum channel c and evolves into P , while c!q.P sends out a quantum datum along quantum channel c before evolving into P . The symbol E represents a trace-preserving super-operator applied on the systems q. The process M [ q; x].P measures the state of qubits q according to the observable M and stores the measurement outcome into the classical variable x of P . Free classical variables can be defined in the usual way, except for the fact that the variable x in the quantum measurement M [q; x] is bound. A process P is closed if it contains no free classical variable, i.e. f v(P ) = ∅.

The set of free quantum variables for process P , denoted by qv(P ) can be inductively defined as in Figure 1. For a process to be legal, we require that 1. q ∈ qv(P ) in the process c!q.P ; 2. qv(P ) ∩ qv(Q) = ∅ in the process P || Q; 3. Each constant A(q; x) has a defining equation A(q; x) := P , where P is a term with qv(P ) ⊆ q and f v(P ) ⊆ x.

The first condition says that a quantum system will not be referenced after it has been sent out. This is a requirement of the quantum no-cloning theorem.

qv(nil) = ∅ qv(τ.P ) = qv(P ) qv(c?x.P ) = qv(P ) qv(c!e.P ) = qv(P ) qv(c?q.P ) = qv(P ) -{q} qv(c!q.P ) = qv(P

) ∪ {q} qv(E[q].P ) = qv(P ) ∪ q qv(M [q; x].P ) = qv(P ) ∪ q qv(P + Q) = qv(P ) ∪ qv(Q) qv(P || Q) = qv(P ) ∪ qv(Q) qv(P [f ]) = qv(P ) qv(P \L) = qv(P ) qv(if b then P ) = qv(P ) qv(A(q; x)) = q.
Fig. 1. Free quantum variables

The second condition says that parallel composition || models separate parties that never reference a quantum system simultaneously.

Throughout the paper we implicitly assume the convention that processes are identified up to α-conversion, bound variables differ from each other and they are different from free variables.

We now give the semantics of qCCS. For each quantum variable q we assume a 2-dimensional Hilbert space H q . For any nonempty subset S ⊆ qVar we write H S for the tensor product space q∈S H q and H S for q ∈S H q . In particular, H = H qVar is the state space of the whole environment consisting of all the quantum variables, which is a countably infinite dimensional Hilbert space.

Let P be a closed quantum process and ρ a density operator on H,3 the pair P, ρ is called a configuration. We write Con for the set of all configurations, ranged over by C and D. We interpret qCCS with a pLTS whose states are all the configurations definable in the language, and whose transitions are determined by the rules in Figure 2; we have omitted the obvious symmetric counterparts to the rules (C-Com), (Q-Com), (Int) and (Sum). The set of actions Act takes the following form, consisting of classical/quantum input/output actions.

{c?v, c!v | c ∈ cChan, v ∈ Real} ∪ {c?r, c!r | c ∈ qChan, r ∈ qVar }
We use cn(α) for the set of channel names in action α. For example, we have cn(c?x) = {c} and cn(τ ) = ∅.

In the first eight rules in Figure 2, the targets of arrows are point distributions, and we use the slightly abbreviated form

C α -→ C to mean C α -→ C .
The rules use the obvious extension of the function || on terms to configurations and distributions. To be precise, C || P is the configuration Q || P, ρ where C = Q, ρ , and ∆ || P is the distribution defined by:

(∆ || P )( Q, ρ ) def = ∆( Q , ρ ) if Q = Q || P for some Q 0 otherwise.
Similar extension applies to ∆[f ] and ∆\L.

(Tau)

τ.P, ρ τ -→ P, ρ (C-Inp) v ∈ Real c?x.P, ρ c?v -→ P [v/x], ρ (C-Outp) v = [[e]]
c!e.P, ρ

c!v -→ P, ρ (C-Com) P1, ρ c?v -→ P 1 , ρ P2, ρ c!v -→ P 2 , ρ P1 || P2, ρ τ -→ P 1 || P 2 , ρ (Q-inp)
r ∈ qv(c?q.P ) c?q.P, ρ c?r 4 An extensional equivalence

-→ P [r/q], ρ (Q-Outp) c!q.P, ρ c!q -→ P, ρ (Q-Com) P1, ρ c?r -→ P 1 , ρ P2, ρ c!r -→ P 2 , ρ P1 || P2, ρ τ -→ P 1 || P 2 , ρ (Oper) E[q].P, ρ τ -→ P, Eq(ρ) (Meas) M = i∈I λiE i pi = tr(E i q ρ) M [ q; x].P, ρ τ -→ i∈I pi P [λi/x], E i q ρE i q /pi (Int) P1, ρ α -→ ∆ qbv(α) ∩ qv(P2) = ∅ P1 || P2, ρ α -→ ∆ || P2 (Sum) P1, ρ α -→ ∆ P1 + P2, ρ α -→ ∆ (Rel) P, ρ α -→ ∆ P [f ], ρ f (α) -→ ∆[f ] (Res) P, ρ α -→ ∆ cn(α) ∩ L = ∅ P \L, ρ α -→ ∆\L (Cho) P, ρ α -→ ∆ [[b]] = true if b then P , ρ α -→ ∆ (Cons) P [ v/ x, r/q], ρ α -→ ∆ A( x, q) := P A( v, r), ρ α -→ ∆
Let C = P, ρ . We use the notation qv (C) := qv(P ) for free quantum variables and env(C) := tr qv(P ) (ρ) for partial traces. Let ∆ = i∈I p i • P i , ρ i . We write E(∆) for the distribution i∈I p i • P i , E(ρ i ) .

We formally define three criteria, namely barb-preservation, reduction-closedness and compositionality, in order to judge whether two processes are equivalent. Here barb-preservation means that two related configurations have the same probability to send out values on classical channels. Reduction-closure ensures that non-deterministic choices are in some sense preserved. In the definition of compositionality, it is worth noting that we only allow the super-operator E to be applied on H qv(C) . The intuition behind this restriction is that systems in qv(C) are actually the local quantum variables of C, and they cannot be manipulated by the outer environment. With the above definition, it is difficult to prove if two given configurations are related by reduction barbed congruence. Therefore, we need to discover some proof techniques which are easy to use.

Definition 3. A relation R is -barb-preserving if C R D implies that C ⇓ ≥p c iff D ⇓ ≥p c for any p ∈ [0, 1] and any classical channel c, where C ⇓ ≥p c holds if C τ =⇒ ∆ for some ∆ with {∆(C ) | C c!v -→ for some v} ≥ p; -reduction-closed if C R D implies • whenever C τ =⇒ ∆, there exists Θ such that D τ =⇒ Θ and ∆ R • Θ, • whenever D τ =⇒ Θ, there exists ∆ such that C τ =⇒ ∆ and ∆ R • Θ; -compositional if C R D implies (C||R)

Open bisimulations

We now introduce a coinductively defined relation which will be used later on to characterise reduction barbed congruence. Here x is the set of free classical variables contained in P and Q.

The above definition is inspired by the work of Sangiorgi [START_REF] Sangiorgi | A theory of bisimulation for the pi-calculus[END_REF], where a notion of bisimulation is defined for the π-calculus by treating name instantiation in an "open" style (name instantiation happens before any transition). Here we deal with super-operator application in an "open" style, but the instantiation of variables is in an "early" style (variables are instantiated when input actions are performed) because the operational semantics given in Figure 2 is essentially an early semantics. For more variants of semantics, see e.g. [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF].

A useful proof technique

In Definition 5 super-operator application and transitions are considered at the same time. In fact, we can separate the two issues and approach the concept of open bisimulation in an incremental way, which turns out to be very useful when proving that two configurations are bisimilar. A relation R is a ground bisimulation if both R and R -1 are ground simulations.

Proposition 1. Suppose that a relation R 1. is a ground bisimulation, and 2. is closed under all super-operator application.

Then R is an open bisimulation.

Proposition 1 provides us with a useful proof technique: in order to show that two configurations C and D are open bisimilar, it suffices to exhibit a binary relation including the pair (C, D), and then to check that the relation is a ground bisimulation and is closed under all super-operator application. This is analogous to a proof technique of open bisimulation for the π-calculus [START_REF] Sangiorgi | A theory of bisimulation for the pi-calculus[END_REF], where name instantiation is playing the same role as super-operator application here. Proposition 2. ≈ o is the largest ground bisimulation that is closed under all super-operator application. In order to obtain completeness, the converse of Theorem 2, we make use of a proof technique that involves examining the barbs of processes in certain contexts; the following technical lemma enhances this technique.

Lemma 1. If ∆||c!0 (≈ r )

• Θ||c!0 where c is a fresh channel, then ∆ (≈ r )

• Θ.

We are now in a position to show that ≈ r is complete with respect to ≈ o .

Theorem 3 (Completeness). If C ≈ r D then C ≈ o D.
Proof. (Schema) Since ≈ r is closed under any super-operator application, by Proposition 1 it suffices to show that ≈ r is a ground bisimulation. The key idea is the following. For any transition C α -→ ∆, we design a test process T , depending on the form of α, such that C||T τ =⇒ Γ 1 for some distribution Γ 1 which exhibits certain barbs. Since C ≈ r D we know C||T ≈ r D||T by the compositionality of

≈ r . Since ≈ r is reduction-closed, there is some Γ 2 such that D||T τ =⇒ Γ 2 and Γ 1 (≈ r ) • Γ 2 . Since ≈ r is barb-preserving, Γ 2 must exhibit similar barbs as Γ 1 .
The careful design of T ensures that D α =⇒ Θ for some Θ with ∆ (≈ r )

• Θ, and the last step involves Proposition 1. See [START_REF] Deng | Open bisimulation for quantum processes[END_REF] for more details.

Modal characterisation

We extend the Hennessy-Milner logic by adding a probabilistic choice modality to express the behaviour of distributions, as in [START_REF] Deng | Testing finitary probabilistic processes (extended abstract)[END_REF], and a super-operator modality to express trace-preserving super-operator application, as well as atomic formulae involving projectors for dealing with density operators. Definition 7. The class L of modal formulae over Act, ranged over by φ, is defined by the following grammar:

φ := E ≥p q | i∈I φ i | α ψ | ¬φ | E.φ ψ := i∈I p i • φ i
where α ∈ Act τ , E is a super-operator, and E is a projector associated with a certain subspace of H q . We call φ a configuration formula and ψ a distribution formula. Note that a distribution formula ψ only appears as the continuation of a diamond modality α ψ.

The satisfaction relation |= ⊆ Con × L is defined by

-C |= E ≥p q if qv(C) ∩ q = ∅ and tr(E q ρ) ≥ p where C = P, ρ . -C |= i∈I φ i if C |= φ i for all i ∈ I. -C |= α ψ if for some ∆ ∈ Dist(Con), C α =⇒ ∆ and ∆ |= ψ. -C |= ¬φ if it is not the case that C |= φ. -C |= E.φ if E ∈ T SO(H qv(C) ) and E(C) |= φ. -∆ |= i∈I p i • φ i if

Examples

BB84, the first quantum key distribution protocol developed by Bennett and Brassard in 1984 [START_REF] Bennett | Quantum cryptography: Public-key distribution and coin tossing[END_REF], provides a provably secure way to create a private key between two parties, say, Alice and Bob. Its security relies on the basic property of quantum mechanics that information gain about a quantum state is only possible at the expense of changing the state, if the states to be distinguished are not orthogonal. The basic BB84 protocol goes as follows:

(1) Alice randomly creates two strings of bits Ba and Ka , each with size n.

(2) Alice prepares a string of qubits q, with size n, such that the ith qubit of q is |x y where x and y are the ith bits of Ba and Ka , respectively, and

|0 0 = |0 , |0 1 = |1 , |1 0 = |+ ,
|+ def = (|0 + |1 )/ √ 2 and |- def = (|0 -|1 )/ √ 2.
(3) Alice sends the qubit string q to Bob. (4) Bob randomly generates a string of bits Bb with size n.

(5) Bob measures each qubit received from Alice according to a basis determined by the bits he generated: if the ith bit of Bb is k then he measures with {|k 0 , |k 1 }, k = 0, 1. Let the measurement results be Kb , which is also a string of bits with size n. (6) Bob sends his choice of measurement bases Bb back to Alice, and upon receiving the information, Alice sends her bases Ba to Bob. (7) Alice and Bob determine at which positions the bit strings Ba and Bb are equal. They discard the bits in Ka and Kb where the corresponding bits of Ba and Bb do not match.

After the execution of the basic BB84 protocol above, the remaining bits of Ka and Kb , denoted by K a and K b respectively, should be the same, provided that the channels used are perfect, and no eavesdropper exists.

To detect a potential eavesdropper Eve, Alice and Bob proceed as follows:

(8) Alice randomly chooses k/2 , where k is the size of K a , bits of K a , denoted by K a , and sends Bob K a and their indexes in the original string K a . (9) Upon receiving the information from Alice, Bob sends back to Alice his substring K b of K b according to the indexes received from Alice. [START_REF] Fournet | A hierarchy of equivalences for asynchronous calculi[END_REF] Alice and Bob check if the strings K a and K b are equal. If yes, then the remaining substring Kf a (resp. Kf b ) of K a (resp. K b ) by deleting K a (resp. K b ) is the secure key shared by Alice (reps. Bob). Otherwise, an eavesdropper is detected, and the protocol halts without generating any secure keys.

For simplicity, we omit the processes of information reconciliation and privacy amplification. Now we describe the above protocol in qCCS. To ease the notations, we assume a special measurement Ran[q; x] which can create a string of n random bits, independent of the initial states of the q system, and store it to x. In effect, Ran[q

; x] = Set n + [q].M n 0,1 [q; x].Set n 0 [q]
where Set n + (resp. Set n 0 ) is the super-operator which sets each of the n qubits it applies on to |+ (resp. |0 ), M n 0,1 [q; x] is the quantum measurement on q according to the basis {|0 , |1 }, and stores the result into x. Then the basic BB84 protocol can be defined as where Set Ka [q] sets the ith qubit of q to the state | Ka (i) , H Ba [q] applies H or does nothing on the ith qubit of q depending on whether the ith bit of Ba is 1 or 0, and M Bb [q; Kb ] is the quantum measurement on q according to the basis determined by Bb , i.e., for each 1 ≤ k ≤ n, it measures q k with respect to the basis {|0 , |1 } (reps. {|+ , |-}) if Bb (k) = 0 (resp. 1), and stores the result into Kb (k). We also abuse the notation slightly by writing E B [q].P when we mean

Alice def = Ran[q; Ba ].Ran[q; Ka ].Set Ka [q].H Ba [q].A2B!q.W aitA( Ba , Ka ) W aitA( Ba , Ka ) def = b2a? Bb .a2b! Ba .
1 n x=0 n (if B = x then E x[ q]
.P ) where i n is the all i string of size n, i = 0, 1. The function cmp takes a triple of strings x, ỹ, z with the same size as inputs, and returns the substring of x where the corresponding bits of ỹ and z match. When ỹ and z match nowhere, we let cmp(x, ỹ, z) = , the empty string.

To show the correctness of this basic form of BB84 protocol, we let

BB84 spe def = Ran[q; Ba ].Ran[q; Ka ].Ran[q ; Bb ].
(key a !cmp( Ka , Ba , Bb ).nil key b !cmp( Ka , Ba , Bb ).nil). The pLTSs of BB84 and BB84 spe for the special case of n = 2 can be depicted as in Figure 3, where for simplicity, we only specify the branch where Ba = Ka = 00. Each arrow in the graph denotes a sequence of τ actions, and all probabilistic distributions are uniform. The strings at the bottom line are the outputs of the protocol. Then it can be easily checked from the pLTSs that BB84 ≈ o BB84 spe .

The key is, for each extra branch in BB84 caused by the measurement of Bob (the Kb line), the final states are bisimilar; they all output the same string. where |x| is the size of x, the function SubStr( K a , x) returns the substring of K a at the indexes specified by x, and RemStr( K a , x) returns the remaining substring of K a by deleting SubStr( K a , x). The special measurement P str m , which is similar to Ran, randomly generates a m/2 -sized string of indexes from 1, . . . , m.

To get a taste of the security of BB84, we consider a special case where Eve's strategy is to simply measure the qubits sent by Alice, according to randomly guessed bases, to get the keys. She then prepares and sends to Bob a fresh sequence of qubits, employing the same method Alice used to encode keys, but using her own guess of bases and the keys she obtained. That is, we define

Eve def = A2E?q.Ran[q ; Be ].M Be [q; Ke ].Set Ke [q].H Be [q].E2B!q.key e ! Ke , BB84 E def = (Alice [f a ] Eve Bob [f b ])\{a2b, b2a, A2E, E2B}.
where f a (A2B) = A2E, and f b (A2B) = E2B. Let T estBB84 def = (BB84 E key a ?x.key b ?ỹ.key e ?z.

(if x = ỹ then f ail!0.nil else key e !z.skey!x.nil))\K where K = {key a , key b , key e }. It is generally very complicated to prove the security of the full BB84 protocol. Here we choose to reduce T estBB84 to a simpler process which is easier for further verification. To be specific, we can show that T estBB84 is bisimilar to the following process:

T B def = Ran[q; Ba ].Ran[q; Ka ].Ran[q ; Be ].Ran Ba, Be, Ka [q; Ke ].Ran[q ; Bb ]. Ran Be, Bb , Ke [q; Kb ].P str | Kab | [q a ; x]. (if Kab = Kba then key e ! Ke .skey!RemStr( Kab , x).nil else (if K x ab = K x ba then alarm a !0.nil alarm b !0.nil else f ail!0.nil))
where to ease the notations, we let Kab = cmp( Ka , Ba , Bb ), Kba = cmp( Kb , Ba , Bb ), K x ab = SubStr( Kab , x), and K x ba = SubStr( Kba , x). Similar to Ran, the special measurement Ran here, which takes three parameters, delivers a string of n bits. For example, Ran Ba, Be, Ka [q; Ke ] will first generate a string of n -| Kae | random bits x, replace with x the substring of Ka at the positions where Ba and Be do not match, and store the string after the replacement in Ke .

Conclusion and related work

In our opinion, bisimulation should be considered as a proof methodology for demonstrating behavioural equivalence between systems, rather than providing the definition of the extensional behavioural equivalence itself. We have adapted the well-known reduction barbed congruence to obtain a touchstone extensional behavioural equivalence for quantum processes considered in [9], and equipped it with a coinductive proof technique and a modal characterisation. Below we briefly compare our open bisimulation with other bisimulations for quantum processes proposed in the literature. A branching bisimulation was defined for QPAlg [START_REF] Jorrand | Toward a quantum process algebra[END_REF][START_REF] Lalire | Relations among quantum processes: Bisimilarity and congruence[END_REF]. However, it cannot always distinguish different quantum operations, as quantum states are only compared when they are input or output. And the derived bisimilarity is not a congruence; it is not preserved by restriction. Bisimulation defined in [START_REF] Feng | Probabilistic bisimulations for quantum processes[END_REF] indeed distinguishes different quantum operations but it works well only for finite processes. Again, it is not preserved by restriction. In [START_REF] Ying | An algebra of quantum processes[END_REF], a congruent (strong) bisimulation was proposed for a special model where no classical datum is involved. However, as many important quantum communication protocols such as superdense coding and teleportation cannot be described in that model, its applicability is very limited. Furthermore, as all quantum operations are regarded as visible in [START_REF] Ying | An algebra of quantum processes[END_REF], the bisimulation is too strong to identify some intuitively equivalent quantum processes.

The first general (both classical and quantum data are involved, and recursive definition is allowed), weak (quantum operations are regarded as invisible, thus can be combined arbitrarily), and congruent bisimulation for quantum processes was defined in [9]. It differentiates quantum input from other actions because, to match a quantum input, an arbitrarily chosen super-operator should be considered. The open bisimulation in this paper makes a step further by treating the super-operator application in an open style: applying super-operators before an action to be matched is selected. This makes it possible to separate ground bisimulation and the closedness under super-operator application, and by doing so, we are able to provide not only a neater and simpler definition, but also a powerful technique for proving bisimilarity. Comparing our open bisimulation with the bisimulation in [9], there are two main differences:

1. In [9] a non-standard weak transition =⇒ c?q -→ is used to match the transition c?q -→. This is for a purely technical reason but makes possible the following example which demonstrates that open bisimulation is strictly coarser. Let P = c?q.(τ + c!0) and Q = P + c?q. Then P and Q are open bisimilar but not bisimilar in the sense of [9]. This is actually a classical example, however, as no quantum operation is included; restricting to this special form of transitions also makes classical bisimulation strictly stronger. 2. In [9] any super-operator application is performed on H qv(C )-q , provided that C c?q -→ C ; while in open bisimulation of this paper, it is performed on H qv(C) . As qv(C ) -q can be a proper subset of qv(C), there are more choices of super-operators in the former case. This observation suggests letting P = c?q.E[q, r 1 ] + I[ r 2 ] and Q = c?q.F[q, r 1 ] + I[ r 2 ]. We conjecture that by taking suitable E and F, we will have a real quantum example showing that open bisimilarity in this paper is strictly coarser than the bisimilarity in [9].

Definition 2 .

 2 Let R ⊆ S × Dist(S) be a relation from states to distributions in a pLTS. Then R • ⊆ Dist(S) × Dist(S) is the smallest relation that satisfies the two rules:

Fig. 2 .

 2 Fig. 2. Operational semantics of qCCS. Here in rule (C-Outp), [[e]] is the evaluation of e, and in rule (Meas), E i q denotes the operator E i acting on the quantum systems q.

  R (D||R) for any process R with qv(R) disjoint from qv(C) ∪ qv(D), and R is closed under super-operator application, namely C R D implies E(C) R E(D) for any E ∈ T SO(H qv(C) ), where T SO(H qv(C) ) stands for the set of trace-preserving super-operators on finite dimensional subspaces of H qv(C) .

Definition 4 (

 4 Reduction barbed congruence). Let reduction barbed congruence, written ≈ r , be the largest relation over configurations which is barbpreserving, reduction-closed and compositional, and furthermore, if C ≈ r D then qv (C) = qv (D) and env(C) = env(D).

Definition 5 .

 5 A relation R ⊆ Con × Con is an open simulation if C R D implies that qv (C) = qv (D), env(C) = env(D), and for any E ∈ T SO(H qv(C) ), whenever E(C) α -→ ∆, there is some Θ with E(D) α =⇒ Θ and ∆ R • Θ. A relation R is an open bisimulation if both R and R -1 are open simulations. We let ≈ o be the largest open bisimulation. Two quantum processes P and Q are bisimilar, denoted by P ≈ o Q, if for any quantum state ρ and any indexed set ṽ of classical values, we have P {ṽ/x}, ρ ≈ o Q{ṽ/x}, ρ .

Definition 6 .

 6 A relation R ⊆ Con × Con is a ground simulation if C R D implies that qv (C) = qv (D), env(C) = env(D), and whenever C α -→ ∆, there is some distribution Θ with D α =⇒ Θ and ∆ R • Θ.

For a sanity

  check, we can prove that ≈ o is an equivalence relation. As a relation between configurations, ≈ o is preserved by all static constructors. Proposition 3. If P, ρ ≈ o Q, σ then Theorem 1. The relation ≈ o between processes is preserved by all the constructors of qCCS except for summation. It turns out that reduction barbed congruence can be captured by open bisimulation precisely. This gives a coinductive technique to judge if two configurations are behaviourally equivalent. Theorem 2 (Soundness). If C ≈ o D then C ≈ r D.

  there are ∆ i ∈ Dist(Con) for all i ∈ I, and for allD ∈ ∆ i , with D |= φ i , such that ∆ = i∈I p i • ∆ i .With a slight abuse of notation, we write ∆ |= ψ above to mean that ∆ satisfies the distribution formula ψ. A logical equivalence arises from the logic naturally:we write C = L D if C |= φ ⇔ D |= φ for all φ ∈ L.Using the logical equivalence, we provide a modal characterisation of reduction barbed congruence as follows. Theorem 4. C ≈ r D if and only if C = L D. Proof. (Schema) In view of Theorems 2 and 3, it suffices to prove that C ≈ o D if and only if C = L D. For one direction, we show that C |= φ ⇔ D |= φ for all φ ∈ L by structural induction on φ; for the other direction, we show that = L is an open bisimulation by using Proposition 1.

  and |1 1 = |-. Here the symbols |+ and |-have their usual meaning:

  key a !cmp( Ka , Ba , Bb ).nil Bob def = A2B?q.Ran[q ; Bb ].M Bb [q; Kb ].b2a! Bb .W aitB( Bb , Kb ) W aitB( Bb , Kb ) def = a2b? Ba .key b !cmp( Kb , Ba , Bb ).nil BB84 def = (Alice Bob)\{a2b, b2a, A2B}

Fig. 3 .

 3 Fig. 3. pLTSs for BB84 and BB84spe

  Now we proceed to describe the protocol with an eavesdropper. Let Alice def = (Alice key a ? K a .P str | K a | [q a ; x].a2b!x.a2b!SubStr( K a , x).b2a? K b . (if SubStr( K a , x) = K b then key a !RemStr( K a , x).nil else alarm a !0.nil)))\{key a } Bob def = (Bob key b ? K b .a2b?x.a2b? K a .b2a!SubStr( K b , x). (if SubStr( K b , x) = K a then key b !RemStr( K b , x).nil else alarm b !0.nil))\{key b }

then there is a collection of distributions ∆ i and probabilities p i such that s

  ∆ i for each i ∈ I and ∆ = i∈I p i • ∆ i with i∈I p i = 1.

	• . Thus as source of a relation distributions. But note that s α -→ ∆ is more general than s α -→ we now also allow α -→ ∆ because if
	s
	We write s τ -→ ∆ if either s =⇒ by letting τ â =⇒ be the reflexive and transitive closure of τ τ -→ ∆ or ∆ = s. We define weak transitions -→ and writing
	∆ â =⇒ Θ for a ∈ Act whenever ∆ τ =⇒	a -→ τ =⇒ Θ. If ∆ is a point distribution, we
	often write s â =⇒ Θ instead of s â =⇒ Θ. Let R ⊆ S × S be a relation between states. It induces a special relation R ⊆
	S × Dist(S) between states and distributions by letting	R def = {(s, t) | s R t}.
	Then we can use Definition 2 to lift R to be a relation ( R)

α -→ ∆ α -→

As H is infinite dimensional, ρ should be understood as a density operator on some finite dimensional subspace of H which contains H qv (P ) .

Supported by the Natural Science Foundation of China (61173033 and 61033002). Supported by Australian Research Council (FT100100218 and DP110103473).


Alexander Kurz

Tomoyuki Suzuki

Emilio Tuosto

A Characterisation of Languages on Infinite Alphabets with Nominal Regular Expressions

We give a characterisation of languages on infinite alphabets in a variant of nominal regular expressions with permutations (p-NREs). We also introduce automata with fresh name generations and permutations (fp-automata), inspired by history-dependent automata (HDAs) and fresh-register automata. Noteworthy, permutations require to deal with dynamic context-dependent expressions. Finally, we give a Kleene theorem for p-NREs and fp-automata to formally characterise languages on infinite alphabets.

Introduction

The study of languages on infinite alphabets has been pushed by the need of formalising data structures built on top of infinite domains of values [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF]. In this context, it is natural to appeal to the theory of automata [START_REF] Kaminski | Finite-memory automata[END_REF][START_REF] Segoufin | Automata and Logics for Words and Trees over an Infinite Alphabet[END_REF][START_REF] Bojanczyk | Data monoids[END_REF][START_REF] Tzevelekos | Fresh-Register Automata[END_REF] operating on a countably infinite alphabet N of names to express languages of interest such as L 1 below, see [START_REF] Tzevelekos | Fresh-Register Automata[END_REF],

L 1 = {n 1 . . . n k ∈ N * ∀i . 1 ≤ i < k . n i = n i+1 }
In [START_REF] Kurz | On nominal regular languages with binders[END_REF], we extended this line of investigations to languages where words do not only consist of names but also of binders (e.g. lambda-calculus terms). In particular, [START_REF] Kurz | On nominal regular languages with binders[END_REF] studies a notion of regular expression for words with binders and the associated notion of finite automata, aiming at applications to the design and analysis of programming languages (as in [START_REF] Shinwell | Freshml: programming with binders made simple[END_REF] or [START_REF] Pouillard | A fresh look at programming with names and binders[END_REF]) or to verification and testing.

Here, we move back to languages of words without binders and apply the techniques of [START_REF] Kurz | On nominal regular languages with binders[END_REF] in order to obtain a novel notion of regular expression for languages on infinite alphabets. While being built from concatenation, sum, and Kleene star in the usual way, the nominal regular expressions introduced in this paper may also contain a binder

n ne m n (1)
Intuitively, n ne allocates a fresh resource within ne, whereas m n deallocates it. The crucial new ingredient, which allows us to capture for example the language L 1 above, is that m n permutes n and m before deallocating n. For example, we can read

m ( n n m n ) * m m (2)
as follows. First m allocates a name m, then n allocates a fresh (i.e. different) name n. Now the permutation specified by m n makes sure that it is the first name m that is deallocated and the second name n that is retained, before looping back to the beginning as specified by the Kleene star * . Note that permutations have a slightly subtle effect on concatenation. For example, in m n n m n • ne m m , due to the permutation specified by m n , the name m in ne semantically represents n. So it will take some care, in § 3, to describe how nominal regular expressions give rise to nominal regular languages. In § 4 we introduce the corresponding notion of automata with fresh-name generation and permutations (fp-automata). Like HD-automata they have allocation transitions, corresponding to n , but unlike HDautomata permutations only appear in special deallocation transitions corresponding to m n . In § 5 we prove a Kleene-type theorem stating that the languages accepted by fp-automata are precisely the nominal regular languages.

Finally, we argue that the work nominal languages with binders also sheds new light on well-established work on languages on infinite alphabets.

Related Work Apart from languages on infinite alphabets, our research draws on HDautomata [START_REF] Pistore | History Dependent Automata[END_REF][START_REF] Montanari | π-Calculus, Structured Coalgebras, and Minimal HD-Automata[END_REF] and nominal sets [START_REF] Gabbay | A new approach to abstract syntax involving binders[END_REF], as well as on the recent confluence of these three areas in [START_REF] Ciancia | A novel class of automata for languages on infinite alphabets[END_REF][START_REF] Tzevelekos | Fresh-Register Automata[END_REF][START_REF] Bojanczyk | Data monoids[END_REF][START_REF] Gabbay | Freshness and name-restriction in sets of traces with names[END_REF][START_REF] Bojanczyk | Automata with group actions[END_REF][START_REF] Kurz | On nominal regular languages with binders[END_REF]. Moreover, the way we deal with scope and binders is related to nested words [START_REF] Alur | Adding nesting structure to words[END_REF] and automata working on lambda-calculus terms [START_REF] Stirling | Dependency tree automata[END_REF].

Although our paper does neither require nor use the theory of nominal sets, the work on nominal sets does suggest to view automata as (co)algebras in the category of nominal sets. As nominal sets are themselves permutation algebras one would expect regular expressions, as it is the case in our work, to contain permutations, see [START_REF] Myers | Rational Coalgebraic Machines in Varieties: Languages, Completeness and Automatic Proofs[END_REF].

A form of regular expressions, called UB-expressions, for languages on infinite alphabets investigated in [START_REF] Kaminski | Regular expressions for languages over infinite alphabets[END_REF]. There it is shown that UB-expressions are as expressive as finite-state unification based automata (FSUBA), which are somewhat weaker than the finite-memory automata (FMA) of [START_REF] Kaminski | Finite-memory automata[END_REF]. In a nutshell, FSUBA do not account for freshness (they can, for example, accept the first but not the second language of Example 6 in § 3.2). Moreover, UB-expressions do not have permutations, although their device of labelling the Kleene-star allows them to accept L 1 in a similar fashion to ours.

Motivating examples: languages on infinite alphabets

Languages on infinite alphabets can suitably formalise data structures on infinite domains (take data words in [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF][START_REF] Bouyer | An algebraic approach to data languages and timed languages[END_REF] as an example). In this context, typical languages consist of finite words -that is finite sequences of symbols -whose symbols are possibly drawn from an infinite set. This is illustrated in the next example.

Example 1 ([22]

). Assume that a, a , a 1 , . . . range on an infinite set A. The language

L 1 def = {a 1 • • • a k k ≥ 0 ∧ ∀i ∈ {1, . . . , k -1}. a i = a i+1 }
consists of finite sequences on A in which all two consecutive letters are different.

In general, the infinite alphabet has a very simple structure that permits to test just for equality or inequality of symbols (see e.g., [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF]) as in Example 1 (in recent work this is being reconsidered, see § 6 for a discussion). For practical reasons, it is sometimes convenient to consider words whose letters can be taken either from an infinite alphabet or from a disjoint finite set, as in Example 2.

The next example shows how languages on infinite alphabets could be used to represent computations where resources have to be acquired and released before their usage.

Example 2. Assume that a, a , a 1 , . . . range on an infinite set A while α (for "acquire") and ρ ("for release") are two distinguished symbols not in A. The language

L αρ def = αA * ρ∪ a = a α a • • • a i≥0 times α a 1 • • • a j ρ a • • • a h≥0 times ρ j ≥ 0 ∧ ∀1 ≤ r ≤ j.a r ∈ {a, a }
represents the executions of a process that acquires, uses, and then releases either one or two resources.

Nominal regular expressions with permutations

In order to characterise languages on infinite alphabets, we extend regular expressions with name-abstraction and permutation. Let N be an infinite set of names and S a finite set of letters. We assume that N and S are disjoint. A language on N ∪ S is a subset of (N ∪ S) * , namely a collection of words on infinite alphabets.

The nominal regular expressions with permutations (p-NREs) are given by

ne ::= 1 | 0 | n | s | ne + ne | ne • ne | ne * | n ne m n
where 1 denotes the singleton with the empty word, 0 denotes the empty language, n ranges over N , s ranges over S; the operators +, •, and * are as the classical operators of regular expressions, while n ne m n is a binder. Note that the superscript m on the closing bracket is not bound unless it is the same as the subscript. Closed and bound occurrences of names are defined in the natural way and we call closed any p-NRE with no occurrence of free names.

Intuitively, n ne allocates a fresh resource within ne; as in nominal calculi, this is rendered by declaring a fresh local name n. Novel is here that m n specifies a permutation when disposing the resource denoted by n, to the effect that to the right of m n every syntactic occurrence of m is semantically read as n. One can think of n and m as registers whose contents are swapped when n is deallocated. To make this work, we assume that the superscript m on m n is in the syntactic scope of some m . For example, the p-NRE n m nm n m n n n is acceptable while n m nm l m m n n is not, because the subexpression m nm l m is not within a scope of a l , and the rightmost m is outside of the scope of m . We aim to contribute to a foundational theory of interactions based on nominal calculi. This requires to consider interactions with an environment that can be seen as a resource handler for requiring and releasing resources. In this respect, the role of the execution environment can be suitably represented using contexts. In our theory, contexts capture two fundamental notions: one notion is the fresh name generation (read the environment) and the other is the permutation action (change the environment). To generate a fresh local name, we have to know which names are already in the environment. And, to leave the permutation result, we must update the environment which could be different from the original environment.

Our contexts are finite lists of names in N . For a p-NRE ne, we call a triple L ‡ ne ‡ R an expression-in-contexts, where L and R are respectively called preand postcontext. Intuitively, L ‡ ne ‡ R is an expression ne that is interpreted in the pre-context L and modifies it to the post-context R.

Preliminaries

Given a function f , the update

f [a →b] extends dom( f ) to dom( f ) ∪ {a} with f (a) = b;
⊥ is the empty map. Let L, M, . . . range over lists of N and let lth(L) be the length of the list L. The empty list is denoted as []. For n ∈ N , write n#L (read "n is fresh for L,") when n = l for any element l in L and write L@n to be the list appending n to the tail of L. We consider only lists with no repeated elements. Given a list L we may abuse the notation and denote its underlying set by L.

The transposition of n and m, denoted by (m n), is the permutation that swaps m and n and is the identity on any other names. Given two lists of the same length k, say

N = [n 1 , . . . , n k ] and M = [m 1 , . . . , m k ], let N M be the bijection from N to M such that N M : n i → m i
for each i ∈ {1, . . . , k} and define the bijection

π [N M] on N as π [N M] (x) def =      N M(x), if x ∈ N N M(x), if x ∈ M \ N x, if otherwise
where N M(x) is a function from M \ N to N \ M recursively defined as follows:

N M(m i ) def = (N M) -1 (m i ), if (N M) -1 (m i ) ∈ N \ M N M(m j ), if (N M) -1 (m i ) = m j for some j = i For example, if M = [b, c, d] and N = [a, b, c], we have π [N M] as follows: N π [N M] • • • x _ • • • a _ b _ c _ d _ N • • • x • • • b c d a
where the target of d (defined by N M) is traced by going backwards along / / and the dashed lines. We define the action of a permutation π on p-NREs and on lists as follows. For a p-NRE ne, the permutation action of π on a p-NRE ne, denoted as π • ne, is

1. π • 1 = 1; π • 0 = 0; π • n = π(n); π • s = s 2. π • (ne 1 + ne 2 ) = (π • ne 1 ) + (π • ne 2 ) 3. π • (ne 1 • ne 2 ) = (π • ne 1 ) • (π • ne 2 ) 4. π • (ne * ) = (π • ne) * 5. π • ( n ne m n ) = π(n) (π • ne) π(m) π(n)
while, the permutation action of

π on L = [l 1 , . . . , l k ] is π • L = [π(l 1 ), . . . , π(l k )].

From p-NREs to languages on infinite alphabets

The interpretations of p-NREs depend on pre-and post-contexts, therefore we introduce the set of rules in Fig. 1.

L ‡ ne 1 + ne 2 ‡ R ( +1 ) L ‡ ne 1 ‡ R L ‡ ne 1 + ne 2 ‡ R ( +2 ) L ‡ ne 2 ‡ R L ‡ ne 1 • ne 2 ‡ R (•) L ‡ ne 1 ‡ L L ‡ ne 2 ‡ R L ‡ ne * ‡ R ( * ) L ‡ ne • • • • • ne k times ‡ R L ‡ n ne m n ‡ R m = n ( ♦ = ) (L@ ) ‡ (n ) • ne ‡ (((m ) • R) @m) L ‡ n ne m n ‡ R m = n ( ♦= ) (L@ ) ‡ (n ) • ne ‡ (R@ )

Fig. 1. Rules computing expressions-in-contexts

Given a closed p-NRE ne, we start applying the rules to the expression-in-contexts

[] ‡ ne ‡ []. In ( * ) in Fig. 1, k is a natural number; if k = 0, the conclusion of the rule is L ‡ 1 ‡ R. Also, in ( ♦=
) and ( ♦ = ), denotes a name fresh for L and for R.

[] ‡ m n m m n n nm n n m m ‡ [] ( ♦= ) [a] ‡ n a a n n na n n ‡ [a] (•) [a] ‡ n a a n ‡ [a] ( ♦ = ) [a, b] ‡ a ‡ [b, a] [a] ‡ n na n n ‡ [a] ( ♦= ) [a, c] ‡ ca ‡ [a, c] (•) [a, c] ‡ c ‡ [a, c] [a, c] ‡ a ‡ [a, c]
the derivation tree is read from top to bottom

Note that b and c are distinct from a, but b may be the same as c (Fact 1). Also, in the first step of the derivation, we can take n instead of a as a fresh name, yielding

[n] ‡ m n n m m mn m m ‡ [n] as the conclusion.
By the rules of Fig. 1, there may be more than one derivation tree for [] ‡ ne ‡ [] (one can choose either of the branches in a sum or unfold any number of times a Kleene-star). We associate a language to each derivation tree T . This is done by applying the rules in Fig. 2, starting from the leaves of T and going upwards to the root. Finally, we define the language of ne to be the union of the languages of all derivation trees for ne, and call such languages nominal regular.

To define the rules in Fig. 2, we extend the notation of expressions-in-contexts to languages and write e.g., L ‡ L(ne) ‡ R. Rules (1), (0), (n) and (s) yield the natural Also, the fact that the rule is applied on proof trees obtained by rules in Fig. 1 implies that lth(M ) = lth(M). Rule ( ♦) deallocates n. If n ∈ R, then (n )•R remembers the fresh name in the new post-context. This rule maintains the invariant that the set of names in the pre-context is in bijection to the set of names in the post-context.

L ‡ 1 ‡ R (1) L ‡ {ε} ‡ R L ‡ 0 ‡ R (0) L ‡ / 0 ‡ R L ‡ n ‡ R (n) L ‡ {n} ‡ R L ‡ s ‡ R (s) L ‡ {s} ‡ R L ‡ L(ne 1 ) ‡ M M ‡ L(ne 2 ) ‡ R (•) L ‡ {w • π [M M] • v | w ∈ L(ne 1 ), v ∈ L(ne 2 )} ‡ π [M M] • R (L@n) ‡ L(ne) ‡ (R@m) ( ♦) L ‡ {(n ) • w | ∈ N , w ∈ L(ne) and #L} ‡ ((n ) • R)
For simplicity, in Fig. 2 we do not explicitly consider e.g., rules for the + operator; when such kind of nodes are reached, the computed language is just the language of the branch and similarly for the Kleene-star (cf. Example 5 below).

Example 4. Starting from the tree in Example 3, we calculate the language of the ex-

pression m n m m n n nm n n m m [a, b] ‡ a ‡ [b, a] (a) [a, b] ‡ {a} ‡ [b, a] ( ♦) [a] ‡ {(b 1 ) • a | 1 ∈ N , 1 = a} ‡ [ 1 ] [a] ‡ {a | 1 ∈ N , 1 = a} ‡ [ 1 ] [a, c] ‡ c ‡ [a, c] (c) [a, c] ‡ {c} ‡ [a, c] [a, c] ‡ a ‡ [a, c] (a) [a, c] ‡ {a} ‡ [a, c] (•) [a, c] ‡ {ca} ‡ [a, c] ( ♦) [a] ‡ {(c 2 ) • ca | 2 ∈ N , 2 = a} ‡ [a] [a] ‡ { 2 a | 2 ∈ N , 2 = a} ‡ [a] (•) [a] ‡ {a • ((a 1 ) • 2 a) | 1 , 2 ∈ N , 1 = a, 2 = a} ‡ [ 1 ] [a] ‡ {a 2 1 | 1 , 2 ∈ N , 1 = a, 2 = 1 } ‡ [ 1 ] ( ♦) [] ‡ {(a 3 ) • a 2 1 | 1 , 2 , 3 ∈ N , 1 = a, 2 = 1 } ‡ [] [] ‡ { 3 2 1 | 1 , 2 , 3 ∈ N , 1 = 3 , 2 = 1 } ‡ []
(where the dashed lines are just simplifications of expressions) and we obtain that

L( m n m m n n nm n n m m ) def = {acb | a, b, c ∈ N . b = a and c = b}.
Interestingly, the application of rule ( ♦) in the left branch of the above derivation corresponds to the deallocation of m (which yields the name a) and the contextual renaming of the content of n with the new name chosen for n (that is 1 ) due to the permutation dictated by the subexpression n m m n . Instead, the application of ( ♦) in the right branch, simply cuts out the last names of both the left and right contexts because the subexpression n nm n n does not involve any permutation.

Example 5 below shows that the language L 1 in Example 1 is nominal regular.

Example 5. To show how the rules in Fig. 2 apply when the expressions contain a Kleene-star, we consider m ( n n m n ) * m m with the derivation tree corresponding to a threefold unfolding of the Kleene-star.

[] ‡ m ( n n m n ) * m m ‡ [] ( ♦= ) [a] ‡ ( n n a n ) * ‡ [a] ( * ) [a] ‡ n n a n n n a n n n a n ‡ [a] (•) [a] ‡ n n a n ‡ [a] ( ♦ = ) [a, b] ‡ b ‡ [b, a] [a] ‡ n n a n n n a n ‡ [a] (•) [a] ‡ n n a n ‡ [a] ( ♦ = ) [a, c] ‡ c ‡ [c, a] [a] ‡ n n a n ‡ [a] ( ♦ = ) [a, d] ‡ d ‡ [d, a] [a, b] ‡ b ‡ [b, a] (b) [a, b] ‡ {b} ‡ [b, a] ( ♦) [a] ‡ { 1 | 1 = a} ‡ [ 1 ] [a, c] ‡ c ‡ [c, a] (c) [a, c] ‡ {c} ‡ [c, a] ( ♦) [a] ‡ { 2 | 2 = a} ‡ [ 2 ] [a, d] ‡ d ‡ [d, a] (d) [a, d] ‡ {d} ‡ [d, a] ( ♦) [a] ‡ { 3 | 3 = a} ‡ [ 3 ] (•) [a] ‡ { 2 3 | 2 = a, 3 = 2 } ‡ [ 3 ] (•) [a] ‡ { 1 2 3 | 1 = a, 2 = 1 , 3 = 2 } ‡ [ 3 ] ( ♦) [] ‡ { 1 2 3 | 1 = 0 , 2 = 1 , 3 = 2 } ‡ [] [] ‡ { 1 2 3 | 2 = 1 , 3 = 2 } ‡ []
Generalising to a k-fold unfolding, we have the language

L k = {a 1 • • • a k | a 1 = a 0 , . . . , a k = a k-1 } which yields L( m ( n n m n ) * m m ) def = k∈N L k = {a 1 • • • a k | ∀k ∈ N, ∀i ∈ {1, . . . , k -1}. a i = a i+1 }
We can also express the following languages taken from [START_REF] Kaminski | Finite-memory automata[END_REF]. Note that the second is not quasi-regular in the sense of [START_REF] Kaminski | Finite-memory automata[END_REF], that is, it cannot be accepted by FMAs.

Example 6. Define N def = n n n n . Note that L(N) = N . We have L( n N * nN * n n n N * ) = {a 1 • • • a k | ∃i, j . 1 ≤ i < j ≤ k & a i = a j }, L( n N * n n n ) = {a 1 • • • a k | ∀i . 1 ≤ i < k ⇒ a i = a k }.
The language L αρ in Example 2 is nominal regular as discussed in the next example. α-conversion on p-NREs. Permutations can be used to define α-conversion on p-NREs.

Let S be a finite set of N and let π S be a bijection on N which fixes each element in S.

We say that L ‡ π L • ne ‡ R is an α-conversion of an expression-in-contexts L ‡ ne ‡ R. For a p-NRE ne, ne is an α-conversion of ne, if ne is obtained by α-converting a subexpression of ne which appears in a derivation tree from [] ‡ ne ‡ [] using the rules Fig. 1 (taking care of unfolding Kleene-stars only once and of avoiding any renamings in name abstractions). For example, a p-

NRE m n m m n n nm n n m m is α-converted to l m l l m n nl n n l l . [a] ‡ n a a n ‡ [a] (m n) [a] ‡ m a a m ‡ [a] [a] ‡ n na n n ‡ [a] (•) [a] ‡ m a a m n na n n ‡ [a] ( ♦) [] ‡ a m a a m n na n n a a ‡ [] (l a) [] ‡ l m l l m n nl n n l l ‡ []
Proposition 1. α-conversion on p-NREs is an equivalence relation on p-NREs.

Theorem 1. For p-NREs ne 1 and ne 2 , if they are α-equivalent, they define the same nominal regular languages, i.e. L(ne 1 ) = L(ne 2 ).

The above results are due to the fact that a completely fresh name is always available when applying the rules ( ♦ = ) and ( ♦= ) in Fig. 1 4 Automata with fresh-name generations and permutations

To handle binders (fresh names) and permutations, we extend automata on binders over S and N fin in [START_REF] Kurz | On nominal regular languages with binders[END_REF]. Denote the set of natural numbers with N and define i as {1, . . . , i}

for each i ∈ N.
The automata in Definition 1 below have a set (of states) Q and a map : Q → N which yield the local registers of q ∈ Q as q . Also, given q ∈ Q,

L(q) def = S ∪ q ∪ { } ∪ { i | i ∈ q },
is the set of possible labels of q. Definition 1. An automaton with fresh-name generation and permutations over S, an fp-automaton for short , is a tuple H = Q, q 0 , F, tr such that -Q is a finite set (of states) equipped with a map : Q → N q 0 ∈ Q is the initial state and q 0 = 0 -F ⊆ Q is the set of final states and q = 0 for each q ∈ F for each q ∈ Q and α ∈ L(q) ∪ {ε}, the set tr(q, α) ⊆ Q contains the successor states of q; for all q ∈ tr(q, α), the following conditions must hold:

α = =⇒ q = q + 1 α = i for i ∈ q q = q -1 α ∈ S ∪ q or α = ε =⇒ q = q
An fp-automaton is deterministic, if for each q ∈ Q and each label α ∈ L(q)

|tr(q, ε)| = 0, |tr(q, α)| = 1, otherwise.

Finally, the i-th layer of H is the subset

Q i def = {q ∈ Q | q = i} of Q.
In an fp-automaton, the i-th layer is connected only by to the (i + 1)-th layer, and only by { j | j ∈ i} to the (i -1)-th layer. Note that the i-th layer forms an automaton over S ∪ i ∪ {ε} in the classical sense. Note that each state on the 0-th layer cannot have any transition, by definition; similarly, states in the highest layer cannot have -transitions. For a technical reason, we assume every fp-automaton is accessible in the usual sense.

Hereafter we fix an fp-automaton as H = Q, q 0 , F, tr . A configuration of H is a triple q, w, σ consisting of a state q, a map σ : q → N assigning names to the local registers in q and a word w. The following definition is almost the same as the one in [START_REF] Kurz | On nominal regular languages with binders[END_REF]. The only exceptions are -transitions and i -transitions. Definition 2. Given q, q ∈ Q and two configurations t = q, w, σ and t = q , w , σ , an fp-automaton H moves from t to t (written t H → t ) if there is α ∈ L(q) ∪ {ε} such that q ∈ tr(q, α) and

           α ∈ q , w = σ(α) w and σ = σ α ∈ S, w = α w and σ = σ α = ε, w = w and σ = σ α = , w = w , n ∈ N \ Im(σ) and σ = σ [ q →n] α = i , w = w and σ = (σ • ( q i)) | q
where (σ • ( q i)) | q is the restriction on q of the function σ • ( q i), i.e. σ permuted by ( q i). A configuration q, w, σ is initial if q = q 0 , w is a word and σ = ⊥, and it is accepting if q ∈ F, w = ε and σ = ⊥.

The set reach H (t) of states reached by H from the configuration t is defined as

reach H (t) def = {q} if t = q, ε, σ t H →t reach H (t ) otherwise
A run of H on a word w is a sequence of moves of H from q 0 , w, ⊥ .

Intuitively, means "generate a fresh name" and store it in the highest register. Transitions labelled by i are meant to permute the value in highest register with the one in the i-th register and dispose the highest register. The and i transitions are performed independently of the word w and introduce some non-determinism even to deterministic fp-automata.

A Kleene Theorem

We show a Kleene theorem for nominal regular languages: Every nominal regular language is recognised by an fp-automaton (Theorem 2) and, vice versa, every language accepted by an fp-automaton is nominal regular (Theorems 3 and 4). The interpretation of p-NREs via the rules of Fig. 1 has to be extended to expressionsin-contexts and to languages-in-contexts. For example, for

[a] ‡ n n a n n n a n ‡ [a], the language-in-contexts is [a] ‡ {cd | ∀c = a, ∀d = c} ‡ [a].

From p-NREs to fp-automata

Given a p-NRE ne, we shall inductively construct an fp-automaton: Theorem 2. Given a p-NRE ne, there exists an fp-automaton H which accepts the nominal language L(ne), i.e. L(ne) = L H .

As seen in § 3, our expressions are context-dependent and the contexts are dynamic.

Similarly, we construct automata-in-contexts L ‡ H ‡ R, that is generalised fp-automata where initial and final states may have lth(L) = lth(M) registers equipped with a function η mapping the h-th register of the initial state to the h-th name of L. Abusing notation, we let H to range over automata-in-contexts.

Base cases. Let L ‡ ne ‡ R be an expression-in-contexts. By Fact 1, we can assume that L and R have the same elements (hence lth(L) = lth(R)). Since L and R are in general non-empty, we equip fp-automata with a function η that maps the local registers of the initial state to names (in L).

When ne = 1 or ne = 0, we define H 1 = Q, q 0 , tr, F, η as follows

-Q def = {q 0 } with q 0 = lth(L); -tr(q 0 , α) def = / 0 for each α ∈ L(q 0 ); -F def = {q 0 }; -η(k) def = l k , for each k ∈ {1, . . . , lth(L)}.
H 0 = Q, q 0 , tr, F, η as follows:

-Q def = {q 0 } with q 0 = lth(L); -tr(q 0 , α) def = / 0 for each α ∈ L(q 0 ); -F def = / 0; -η(k) def = l k for each k ∈ {1, . . . , lth(L)}.
When ne = n, we let H n = Q, q 0 , tr, F, η as follows:

-Q def = {q 0 , q 1 } with q 0 = lth(L) and q 1 = lth(L);

-tr(q 0 , α) def = {q 1 } α = k and l k = n / 0 otherwise and tr(q 1 , α) def = / 0 for each α ∈ L(q 1 ); -F def = {q 1 }; η(k) def = l k for each k ∈ {1, . . . , lth(L)}.
When ne = s, we let H s = Q, q 0 , tr, F, η as follows:

-Q def = {q 0 , q 1 } with q 0 = lth(L) and q 1 = lth(L);

tr(q 0 , α)

def = {q 1 } α = s / 0 otherwise and tr(q 1 , α) def = / 0 for each α ∈ L(q 1 ); -F def = {q 1 }; η(k) def = l k for each k ∈ {1, . . . , lth(L)}. Proposition 2. The automata-in-contexts L ‡ H 1 ‡ R, L ‡ H 0 ‡ R, L ‡ H n ‡ R and L ‡ H s ‡ R accept the languages-in-contexts L ‡ {ε} ‡ R, L ‡ / 0 ‡ R, L ‡ {n} ‡ R and L ‡ {s} ‡ R, respectively. Furthermore, for every final state q in L ‡ H 1 ‡ R, L ‡ H 0 ‡ R, L ‡ H n ‡ R and L ‡ H s ‡ R, we have q = lth(R).
For automata-in-contexts we consider configurations and runs as in Definition 2, with the exception that the η in the initial and final configurations q, w, η takes into account the names in the pre-and post-contexts.

Example 9. The automaton-in-contexts [m, n] ‡ H n ‡ [n, m] below 2nd layer 1 7 ! 2 7 ! n 2 m 1 7 ! 2 7 ! n m is constructed from [m, n] ‡ n ‡ [n, m] Let L ‡ H ne 1 ‡ R L ‡ H ne 2 ‡ R be automata-in-contexts
, where H ne 1 = Q 1 , q 1,0 , tr 1 , F 1 , η 1 and H ne 2 = Q 2 , q 2,0 , tr 2 , F 2 , η 2 for the corresponding expressionsin-contexts L ‡ ne 1 ‡ R and L ‡ ne 2 ‡ R. Therefore, η 1 and η 2 are identical. Then, we let H ne 1 +ne 2 = Q + , q + 0 , tr + , F + , η + as follows:

-Q + def = {q + 0 } Q 1 Q 2 with q + 0 = lth(L); -tr + (q + 0 , α) def = {q 1,0 , q 2,0 } α = ε / 0
otherwise and the others are the same as before;

-F + def = F 1 F 2 ; η def = η 1 (= η 2 ).
Proposition 3. The automaton-in-contexts L ‡ H ne 1 +ne 2 ‡ R accepts the language-incontexts L ‡ L(ne 1 + ne 2 ) ‡ R. Furthermore, for each final state q in L ‡ H ne 1 +ne 2 ‡ R, we have q = lth(R).

Concatenation. By the context calculus of Fig. 1, the post-context of the first expression must be the same as the pre-context of the second expression. Let L ‡ H ne 1 ‡ L and L ‡ H ne 2 ‡ R be automata-in-contexts with H ne 1 = Q 1 , q 1,0 , tr 1 , F 1 , η 1 and H ne 2 = Q 2 , q 2,0 , tr 2 , F 2 , η 2 , and L ‡ ne 1 ‡ L and L ‡ ne 2 ‡ R the corresponding expressions-incontexts. By the definition of the context calculus, the post-context of the first expression must be the same as the pre-context of the second expression. We let

H ne 1 •ne 2 = Q • , q • 0 , tr • , F • , η • as follows: -Q • def = Q 1 Q 2 ; q • 0 def = q 1,0 ; F • def = F 2 ; η • def = η 1 ; -tr • (q, α) def =      tr 1 (q, α) ∪ {q 2,0 } q ∈ F 1 and α = ε tr 1 (q, α) q ∈ Q 1 and either q ∈ F 1 or α = ε tr 2 (q, α) q ∈ Q 2 .
Proposition 4. The automaton-in-contexts L ‡ H ne 1 •ne 2 ‡ R accepts the language-incontexts L ‡ L(ne 1 • ne 2 ) ‡ R. Furthermore, for each final state q in L ‡ H ne 1 •ne 2 ‡ R, we have q = lth(R).

Name-abstraction. Let (L@n) ‡ H ne ‡ (R@m) be an automaton-in-contexts, where H ne = Q, q 0 , tr, F, η , and (L@n) ‡ ne ‡ (R@m) the expression-in-contexts. We let H n ne m n = Q ♦ , q ♦ 0 , tr ♦ , F ♦ , η ♦ as follows:

-Q ♦ def = Q {q s , q t } with q s = lth(L) and q t = lth(L);

-q ♦ 0 def = q s ; F ♦ def = {q t }; η ♦ def = η; -tr ♦ (q, α) def =                   
{q 0 } q = q s and α = / 0 q = q s and α = / 0 q = q t {q t } q ∈ F and α = k for k with r k = n / 0 q ∈ F and α = k for k with r k = n tr(q, α) otherwise ; where (R@m) = [r 1 , . . . , r lth(R)+1 ] (so r lth(R)+1 = m).

Proposition 5. The automaton-in-contexts L ‡ H n ne m n ‡ R recognises the languagein-contexts L ‡ L( n ne m n ) ‡ R. Furthermore, for the final state q t in L ‡ H n ne m n ‡ R, we have q t = lth(R). Kleene star. For an automaton-in-contexts L ‡ H ne ‡ R with H ne = Q, q 0 , tr, F, η and the expression-in-contexts L ‡ ne ‡ R, let H ne * = Q * , q * 0 , tr * , F * , η * as follows:

-

Q * def = Q; q * 0 def = q 0 ; F * def = {q * 0 }; η * def = η;
tr * (q, α) def = tr(q, α) ∪ {q * 0 } q ∈ F and α = ε tr(q, α)

otherwise .

Proposition 6. The automaton-in-contexts L ‡ H ne * ‡ R recognises the language-incontexts L ‡ L(ne * ) ‡ R. Furthermore, for the final state q 0 in L ‡ H ne * ‡ R, we have q 0 = lth(R). Note that q 0 ∈ Q 0 (we assume q 0 1 = q 0 ) and F ⊆ Q 0 . We fix an arbitrary order on states given by their index in (3), let s R k i, j denote the set of paths from q s i to q s j which visit only states on layers higher than s or states q s r ∈ Q s with r ≤ k, and let E i, j

def = / 0 if i = j and E i,i def = {ε}. Then, s R k i, j is defined by h R 0 i, j def = {α q h j ∈ h i , α)} ∪ E i, j h R k i, j def = h R k-1 i,k h R k-1 k,k * h R k-1 k, j ∪ h R k-1 i, j
on the highest layer h. On the other layers (s < h), it is defined by

s R 0 i, j def = {α q s j ∈ tr(q s i , α)} ∪ s ∈s+1 s+1 (i , j )∈Γ s,s i, j s+1 R m s+1 i , j s s+1 ∪ E i, j s R k i, j def = s R k-1 i,k s R k-1 k,k * s R k-1 k, j ∪ s R k-1 i, j ∪ s ∈s+1 s+1 (i , j )∈Γ s i, j s+1 R m s+1 i , j s s+1
where Γ s,s i, j def = {(i , j ) q s+1 i ∈ tr(q s i , ) & q s j ∈ tr(q s+1 j , s )} for each s ∈ s + 1. Hence,

s ∈s+1 s+1 (i , j )∈Γ s,s i, j s+1 R m s i , j s s+1
is the collection of all paths from q s i to q s j visiting only states on the higher layers. Finally, we translate all paths from the initial state to final states into a nominal regular expression, but this is analogous to the classical theory. The only distinction is how to choose fresh names for binders. However, this is done by reserving names for fresh names as a distinct subset {n 1 , . . . , n h } of N , with the Therefore, by the above theorems, we conclude that every fp-automaton H has a p-NRE ne such that L H = L(ne).

Conclusion

We have extended the nominal regular expressions and automata presented in [START_REF] Kurz | On nominal regular languages with binders[END_REF] with permutations in order to provide a notion of regular expression for languages on infinite alphabets (without binders). Our main technical contribution is a Kleene theorem that establishes an equivalence between nominal regular expressions with permutations and fp-automata.

A novelty of our approach is how to handle the environments and how permutations change the local views of the environment. This is done with the help of the context calculus in Fig. 1, which represents the views on the environments by "contexts" similar to Hoare triples. The language construction of Fig. 2 then explains how this information flow generates nominal regular languages.

Yet another delicate aspect of our theory is the subtle non-deterministic behaviour present even in deterministic automata. As highlighted by the first language of Example 6, Definition 2 does not require the automaton to consume a letter if moving on an allocation or deallocation transition. These moves are non-deterministic in the sense that they are not controlled by the word to be recognised. This is crucial to the equivalence established in Theorem 4. Indeed, non-deterministic models are more expressive than deterministic ones when considering languages on infinite alphabets [START_REF] Kaminski | Finite-memory automata[END_REF][START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF].

The natural next step to take in our research is to exploit the results presented here to compare the expressiveness of nominal regular expressions with other models featuring languages on infinite alphabets. We note that our nominal regular languages are closed under union, intersection, concatenation and Kleene-star, but not under complement. Whereas the regular languages of [START_REF] Kurz | On nominal regular languages with binders[END_REF] are closed under resource-sensitive complement, this is no longer the case here, since allocation and deallocation transitions are no longer controlled by explicit binders in the words. This situation is similar to the FMA of [START_REF] Kaminski | Finite-memory automata[END_REF] although FMA do not accept the second language of Example 6. A precise comparison with FMA and related models such as those of [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF] or [START_REF] Tzevelekos | Fresh-Register Automata[END_REF] is left for future work.

Further investigations should reveal the categorical and (co)algebraic nature of our automata. In particular, the fact that the automata work level-wise suggests a manysorted approach via presheaves (see also the two-sorted coalgebras of [START_REF] Ciancia | Stream automata are coalgebras[END_REF]). It would also be interesting to combine the work of this paper with [START_REF] Kurz | On nominal regular languages with binders[END_REF] along the lines suggested by [START_REF] Bartoletti | Hard life with weak binders[END_REF], which investigates how the implicit scope of names in words without binders interacts with binders having explicit scope. In another direction, we plan to extend our approach towards Kleene algebras (with tests) [START_REF] Kozen | On Hoare logic and Kleene algebra with tests[END_REF] and possible applications to verification. Other interpretations of the binders in the style of the research programme devised in [START_REF] Bojanczyk | Automata with group actions[END_REF] will also be of interest.

Fact 1

 1 For any derivation of L ‡ ne ‡ R from an expression-in-contexts [] ‡ ne ‡ [] using the rules in Fig. 1 we have that there is a permutation π such that R = π • L (and hence lth(L) = lth(R)) names in L are pairwise disjoint (and similarly for R) Example 3. Application of the rules in Fig. 1 to m n m m n n nm n n m m gives:

Fig. 2 .

 2 Fig. 2. Rules computing languages

Example 7 .

 7 Calculations similar to those in Examples 4 and 5 can be done to show that the p-NRE α m ((m * n (m + n) ρ m n m * ) + m * ) ρ m m (where α, ρ ∈ S) defines L αρ .

Definition 3 .Example 8 .

 38 The fp-automaton H accepts, or recognises, a word w on S ∪ N when F ∩ reach H ( q 0 , w, ⊥ ) = / 0. The language of H is the set L H of words accepted by H . The fp-automaton below

Example 10 .

 10 For [m, n] ‡ H n ‡ [n, m], the fp-automaton below is constructed according to the name-abstraction in contexts [m] ‡ H n n m n ‡ [m].

Example 11 .

 11 For [m] ‡ H n n m n ‡ [m], the fp-automaton

  generate expressions for the binding construct.

Acknowledgements We would like to thank the anonymous reviewers for their valuable comments and suggestions.

Theorem 3. Given an fp-automaton H , there is a deterministic fp-automaton which accepts the same language as L H .

Proof (Sketch). The main proof technique is a "layer-wise" powerset construction.

Since the i-th layer is basically a classical automaton over S ∪ i ∪ {ε}, the powerset construction allows us to make each layer deterministic. The only thing we have to care about is how to connect these deterministic layers by and { i | i ∈ i} in a deterministic way. This is shown below.

For each subset {q i 1 , . . . , q i k } of the i-th layer Q i , we let

for each i ∈ i. Hence we obtain a deterministic automaton of H .

Note that the powerset construction in the proof above has to be performed layer-wise due to the presence of local registers.

Theorem 4. Any language accepted by a deterministic fp-automaton H is a nominal regular language. That is, there exists a p-NRE ne such that L H = L(ne).

Proof (Sketch). The states Q of a deterministic fp-automaton H can be decomposed into h = max q∈Q q layers (where h is the highest layer of H ):