BRICS

Basic Research in Computer Science

New-HOPLA A Higher-Order Process Language with Name Generation

Glynn Winskel Francesco Zappa Nardelli BRICS Report Series RS-04-21 ISSN 0909-0878 October 2004 BRICS RS-04-21 Winskel & Zappa Nardelli: New-HOPLA—A Higher-Order Process Language with Name Generation Copyright \begin{matrix}c \\ ◯ \end{matrix} 2004, Glynn Winskel & Francesco Zappa Nardelli.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/04/21/

new-HOPLA

a higher-order process language with name generation

Glynn Winskel

Computer Laboratory University of Cambridge, UK

      Glynn.Winskel@cl.cam.ac.uk

Francesco Zappa Nardelli

INRIA Rocquencourt France

                                        Francesco.Zappa Nardelli@inria.fr

October 2004

Abstract

This paper introduces new-HOPLA, a concise but powerful language for higherorder nondeterministic processes with name generation. Its origins as a metalanguage for domain theory are sketched but for the most part the paper concentrates on its operational semantics. The language is typed, the type of a process describing the shape of the computation paths it can perform. Its transition semantics, bisimulation, congruence properties and expressive power are explored. Encodings are given of well-known process algebras, including π-calculus, Higher-Order π-calculus and Mobile Ambients.

1 The origins of new-HOPLA

This work is part of a general programme (reported in [8]), to develop a domain theory which scales up to the intricate languages, models and reasoning techniques used in distributed computation. This ambition led to a concentration on path based models, and initially on presheaf models because they can even encompass causal dependency models like event structures; so ‘domains’ is being understood more broadly than usual, to include presheaf categories.

The general methodology has been to develop domain theories with a rich enough life of their own to suggest powerful metalanguages. The point to emphasise is that in this way informative domain theories can have a pro-active role; they can yield new metalanguages, by their nature very expressive, accompanied by novel ways to deconstruct existing notions into more primitive ones, as well as new analysis techniques. A feature of presheaf models has been very useful: in key cases there is often a strong correspondence between elements of the presheaf denotation and derivations in an operational semantics. In the cases of HOPLA and new-HOPLA the presheaf models have led not only the core operations of the language, and a suitable syntax, but also to their operational semantics.

This paper reports on new-HOPLA, a compact but expressive language for higherorder nondeterministic processes with name generation. It extends the language HOPLA of Nygaard and Winskel [7] with name generation, and like its predecessor has its origins in a domain theory for concurrency. Specifically it arose out of the metalanguage implicitly being used in giving a presheaf semantics to the π-calculus [2]. But a sketch of its mathematical origins and denotational semantics does not require that heavy an investment, and can be based on path sets rather than presheaves.^{1}

The key features of new-HOPLA hinge on its types and these can be understood independently of their origin as objects, and constructions on objects, in a category of domains—to be sketched shortly within the simple domain theory of path sets. A type ℙ specifies the computations possible with respect to a given current set of names; if a process has type ℙ, then any computation path it performs with the current set of names s will be an element of ℙ(s).

A central type constructor is that of prefix type !ℙ; at a current set of names s, a process of this type !ℙ, if it is to do anything, is constrained to first doing a prototypical action ! before resuming as a process of type ℙ. (Actions within sum or tensor types will come to be tagged by injections and so of a less anonymous character.)

In the category of domains, domains can be tensored together, a special case of which gives us types of the form ℕ ⊗ ℙ, a kind of dynamic sum which at current names s comprises paths of ℙ(s) tagged by a current name which serves as an injection function. There is also a more standard sum Σ_{i∈I}ℙ_{i} of an indexed family of types ℙ_{i} where i ∈ I; this time paths are tagged by indices from the fixed set I rather than the dynamic set of names.

The remaining type constructions are the formation of recursive types, and three forms of function space. One is a ‘linear function space’ ℕ → ℙ, the type of processes which given a name return a process of type ℙ. Another is a ‘continuous function space’ ℙ → ℚ, the type of processes which given a process of type ℙ return a process of type ℚ. There is also a type δℙ associated directly with new-name generation. A process of type δℙ takes any new name (i.e. a name not in the current set of names) as input and returns a process of type ℙ. Name generation is represented by new name abstraction, to be thought of as picking a new name (any new name will do as well as any other), and resuming as a process in which that new name is current.

This summarises the rather economical core of new-HOPLA. Very little in the way of standard process algebra operations are built in—nothing beyond a prefix operation and nondeterministic sum. By being based on more fundamental primitives than usual, the language of new-HOPLA is remarkably expressive. As additional motivation we now turn to how these primitives arise from a mathematical model refining the intuitions we have just presented.

A domain theory If for the moment we ignore name generation, a suitable category of domains is that of Lin. Its objects, path orders, are preorders ℙ consisting of computation paths with the order p ≤ p′ expressing how a path p extends to a path p′. A path order ℙ determines a domain ℙ̂, that of its path sets, left-closed sets w.r.t. ≤_{ℙ}, ordered by inclusion. (Such a domain is a prime-algebraic complete lattice, in which the complete primes are precisely those path sets generated by individual paths.) The arrows of Lin, linear maps, from ℙ to ℚ are join-preserving functions from ℙ̂ to ℚ̂. The category Lin is monoidal-closed with a tensor given by the product ℙ × ℚ of path orders and a corresponding function space by ℙ^{op} × ℚ—it is easy to see that join-preserving functions from ℙ̂ to ℚ̂ correspond to path sets of ℙ^{op} ×ℚ. In fact Lin has enough structure to form a model of Girard’s classical linear logic [4]. To exhibit its exponential ! we first define the category Cts to consist, like Lin, of path orders as objects but now with arrows the Scott-continuous functions between the domains of path sets. The inclusion functor Lin ↪ Cts has a left adjoint ! : Cts → Lin which takes a path order ℙ to a path order consisting of finite subsets of ℙ with order

1Path sets arise by ‘flattening’ presheaves, which can be viewed as characteristic functions to truth values given in the category of sets, as sets of realisers, to simpler characteristic functions based on truth values 0 ≤ 1 [8].

P ≤_{!ℙ} P′ iff ∀p ∈ P ∃p′ ∈ P′. p ≤_{ℙ} p′

—so !ℙ can be thought of as consisting of compound paths associated with several runs.

The higher-order process language HOPLA is built around constructions in the category Lin. Types of HOPLA, which may be recursively defined, denote objects of Lin, path orders circumscribing the computation paths possible. As such all types support operations of nondeterministic sum and recursive definitions, both given by unions. Sum types are provided by coproducts, and products, of Lin, both given by the disjoint juxtaposition of path orders; they provide injection and projection operations. There is a type of functions from ℙ to ℚ given by (!ℙ)^{op} × ℚ, the function space of Cts; this gives the operation of application and lambda abstraction. To this the adjunction yields a primitive prefix operation, a continuous map ℙ → !ℙ, given by the unit at ℙ; it is accompanied by a destructor, a prefix-match operation, obtained from the adjunction’s natural isomorphism. For further details, encodings of traditional process calculi in HOPLA and a full abstraction result, the reader is referred to [7, 9].

A domain theory for name generation We are interested in extending HOPLA to allow name generation. We get our inspiration from the domain theory. As usual a domain theory for name generation is obtained by moving to a category in which standard domains are indexed functorially by the current set of names. The category I consists of finite sets of names related by injective functions. The functor category Lin^{I} has as objects functors ℙ : I → Lin, so path orders ℙ(s), indexed by finite sets of names s, standing for the computation paths possible with that current set of names; its arrows are natural transformations α = ⟨α_{s}⟩_{s∈I} : ℙ → ℚ, with components in Lin. One important object in Lin^{I} is the object of names ℕ providing the current set of names, so ℕ(s) = s regarded as a discrete order, at name set s. Types of new-HOPLA will denote objects of Lin^{I}.

The category has coproducts and products, both given by disjoint juxtaposition at each component. These provide a sum type Σ_{i∈I}ℙ_{i} from a family of types (ℙ_{i})_{i∈I}. It has injections producing a term i:t of type Σ_{i∈I}ℙ_{i} from a term t of type ℙ_{i}, for i ∈ I. Projections produce a term π_{i}t of type ℙ_{i} from a term t of the sum type.

There is a tensor got pointwise from the tensor of Lin. Given ℙ and ℚ in Lin^{I} we define ℙ ⊗ ℚ in Lin^{I} so that (ℙ ⊗ ℚ)(s) = ℙ(s) × ℚ(s) at s ∈ I. We will only use a special case of this construction to form tensor types ℕ ⊗ ℙ, so (ℕ ⊗ ℙ)(s) = s × ℙ(s) at s ∈ I. These are a form of ‘dynamic sum’, referred to earlier, in which the components and the corresponding injections grow with the availability of new names. There are term constructors producing a term n · t of type ℕ ⊗ ℙ from a term t of type ℙ and a name n. There are projections π_{n}t forming a term of type ℙ from a term t of tensor type.

At any stage s, the current set of names, a new name can be generated and used in a term in place of a variable over names. This leads to the central idea of new-name abstractions of type δℙ where δℙ(s) = ℙ(s ∪^{.} {⋆}) at name set s. As observed by Stark [13] the construction δℙ can be viewed as a space of functions from ℕ to ℙ but with the proviso that the input name is fresh. A new-name abstraction is written newα.t and has type δℙ, where t is a term of type ℙ. New-name application is written t[n], where t has type δℙ, and requires that the name n is fresh w.r.t. the names of t.

The adjunction \xymatrix{Lin \ar@{^{(}->}[r]|{⊥} & Cts \ar[l]_{!}} induces an adjunction \xymatrix{Lin^{I} \ar@{^{(}->}[r]|{⊥} & Cts^{I} \ar[l]_{!}} where the left adjoint is got by extending the original functor ! : Cts → Lin in a pointwise fashion. The unit of the adjunction provides a family of maps from ℙ to !ℙ in Cts^{I}. As with HOPLA, these yield a prefix operation !t of type !ℙ for a term t of type ℙ. A type of the form !ℙ is called a prefix type; its computation paths at any current name set first involve performing a prototypical action, also called ‘!’.

To support higher-order processes we need function spaces ℙ ⊸ ℚ such that

Lin^{I}(ℝ, ℙ ⊸ ℚ) ≅ Lin^{I}(ℝ ⊗ ℙ, ℚ)

natural in ℝ and ℚ. Such function spaces do not exist in general—the difficulty is in getting a path order ℙ ⊸ ℚ(s) at each name set s. However a function space does exist in the case where both ℙ and ℚ satisfy certain ‘type axioms’ inherited through all the type operations and, in addition, ℙf preserves complete primes for each map f : s → s′ in I.^{2} This suggests limiting the syntax of types to special function spaces ℕ ⊸ ℚ and !ℙ ⊸ ℚ, the function space in Cts^{I}. The function spaces are associated with operations of application and lambda abstraction.

Related work and contribution The above domain theoretic constructions provide the basis of new-HOPLA. It resembles, and indeed has been inspired by, the metalanguages for domain theories with name generation used implicitly in earlier work [3, 13, 2], as well as the language of FreshML [11]. The language new-HOPLA is distinguished through the path-based domain theories to which it is fitted and, as we will see, in itself forming a process language with an operational semantics.

2 The language

Types The type of names is denoted by ℕ. The types of processes are defined by the grammar below.

ℙ ::= 0 | ℕ ⊗ ℙ | !ℙ | δℙ | ℕ → ℙ | ℙ → ℚ | Σ_{i∈I}ℙ_{i} | μ_{j}P_{1} … P_{k}.(ℙ_{1} … ℙ_{k}) | P

2The type axioms, for ℚ : I → Lin, comprise: For every map f : s → s′ in I, the function ℚf preserves finiteness and non-empty meets; preservation of non-empty meets ensures that whenever y ⊆ ℚf(x) for some x, then there is a minimum x_{0} = min(ℚf, y) for which y ⊆ ℚf(x_{0}). For every pullback h_{1} : s_{0} → s_{1}, h_{2} : s_{0} → s_{2} of g_{1} : s_{1} → s_{3}, g_{2} : s_{2} → s_{3} in I and x_{1} ∈ ℚ̂s_{1}, if min(ℚg_{2}, ℚg_{1}(x_{1}))

exists, then it is required that min(ℚh_{1}, x_{1}) exists and ℚh_{2}(min(ℚh_{1}, x_{1})) = min(ℚg_{2}, ℚg_{1}(x_{1})).

The sum type Σ_{i∈I}ℙ_{i} where I is a finite set, is most often written i_{1}:ℙ + ⋯ + i_{k}:ℙ. The symbol P is drawn from a set of type variables used in defining recursive types; closed type expressions are interpreted as path orders. The type μ_{j}P_{1} … P_{k}.(ℙ_{1} … ℙ_{k}) is interpreted as the j-component, for 1 ≤ j ≤ k, of the ‘least’ solution to the defining equations P_{1} = ℙ_{1}, …, P_{k} = ℙ_{k}, where the expressions ℙ_{1} … ℙ_{k} may contain the P_{j}’s.

Terms and actions We assume a countably infinite set of name constants, ranged over by a, b, … and a countably infinite set of name variables, ranged over by α, β, … Names, either constants or variables, are ranged over by m, n, . . .. We assume an infinite, countable, set of process variables, ranged over by x, y, …

Every type is associated with actions processes of that type may do. The actions are defined by the grammar below:

p, q, r ::= x | !p | n · p | i:p | newα.p | n ↦ p | u ↦ p | p[n] .

As we will see shortly, well-typed actions are constructed so that they involve exactly one prototypical action ! and exactly one ‘resumption variable’ x. Whenever a term performs the action, the variable of the action matches the resumption of the term: the typings of an action thus relates the type of a term with the type of its resumption. According to the transition rules a process of prefix type !ℙ may do actions of the form !p, while a process of tensor or sum type may do actions of the form n · p or i:p respectively. A process of type δℙ does actions of the form newα.p meaning that at the generation of a new name, a say, as input the action p[a/α] is performed. Actions of function type n ↦ p or u ↦ p express the dependency of the action on the input of a name n or process u respectively. The final clause is necessary in building up actions because we sometimes need to apply a resumption variable to a new name.

The terms are defined by the grammar below:

t, u, v ::= 0  | !t  inactive process and prototypical action
| n · t  | π_{n}t  tensor and projection
| λx.t  | tu  process abstraction and application
| λα.t  | tn  name abstraction and application
| newα.t | t[n]  new name abstraction and application
| recx.t | x  recursive definition and process variables
| i:t  | π_{i}t  injection and projection
| Σ_{i∈I}t_{i}  | Σ_{α∈ℕ}t sum and sum over names
| [t > p(x) ⇒ u]  pattern matching

In new-HOPLA actions are used as patterns in terms [t > p(x) ⇒ u] where we explicitly note the resumption variable x. If the term t can perform the action p the resumption of t is passed on to u via the variable x.

We assume an understanding of the free name variables (the binders of name variables are λα.−, newα.−, and Σ_{α∈ℕ}−) and of the free process variables (the binders of process variables are λx.−, and [t > p(x) ⇒ −]) of a term. The support of a term, denoted n(t), is the set of the its free names, that is, the set of its name constants and of its free name variables.

We say that a name n is fresh for a term t if n ∉ n(t).

2.1 Transition rules

The behaviour of terms is defined by a transition relation of the form

s ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → t′

where s is a finite set of name constants such that n(t) ⊆ s. The transition above should be read as ‘with current names s the term t can perform the action p and resume as t′’. We generally note the action’s resumption variable in the transitions; this simplifies the transition rules in which the resumption variable must be explicitly manipulated.

So the transition relation is given at stages indexed by the set of current names s. The body of an abstraction over names λα.t can only be instantiated with a name in s, and an abstraction over processes λx.t can only be instantiated with a process whose support is contained in s. As the transition relation is indexed by the current set of names, it is possible to generate new names at run-time. Indeed, the transition rule for new-name abstraction newα.t extends the set s of current names with a new name a ∉ s; this name a is then passed to t via the variable α. The transition rules must respect the typings of actions and terms given in the next section. Formally:

Definition 2.1 (Transition relation) For closed terms t such that s ⊢ t : ℙ and path patterns such that s; ; x:ℚ ⊩ p : ℙ the rules reported in Table 1 define a relation ℙ; s ⊢

t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → u, called the transition relation.

To help familiarise the reader with the transition semantics, we present some derivations.

— The operational semantics validates β-equivalence:

{ℚ; s ⊢ t[u/x] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → t′ \atop ℙ → ℚ; s ⊢ λx.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{u↦p (y)} → t′} ; ℚ; s ⊢ (λx.t)u \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → t′  {ℚ; s ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → t′ \atop ℕ → ℚ; s ⊢ λα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{a↦p (y)} → t′} ; ℚ; s ⊢ (λα.t)a \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → t′

These derivations illustrate how β-equivalence is validated by the transition relation in the sense that a term (λx.t)u (resp. (λα.t)a) has the same transition capabilities as the term t[u/x] (resp. t[a/α]): for example, a term (λx.t)u performs an action p and resumes as t′ iff the term t[u/x] performs the same action p resuming as t′—the ‘only if’ part follows by the uniqueness of the derivations.

— The action of the tensor and sum type:

{ℙ; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → t′ \atop ℕ ⊗ ℙ; s ⊢ a · t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{a·p (y)} → t′} ; ℙ; s ⊢ π_{a}(a · t) \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → t′  {ℙ_{i}; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → t′ \atop Σ_{i∈I}ℙ_{i}; s ⊢ i:t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{i:p (y)} → t′} ; ℙ_{i}; s ⊢ π_{i}(i:t) \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → t′

By uniqueness of the derivations, a term t has the same transition capabilites as the terms π_{a}(a · t) and π_{i}(i:t).

\overline{!ℙ; s ⊢ !t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{!x (x)} → t}  \frac{ℙ; s ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → t′ a ∈ s}{ℕ ⊗ ℙ; s ⊢ a · t \begin{matrix}− \\ − \\ − \end{matrix}^{a·p} → t′}  \frac{ℕ ⊗ ℙ; s ⊢ t \begin{matrix}− \\ − \\ − \end{matrix}^{a·p} → t′}{ℙ; s ⊢ π_{a}t \begin{matrix}− \\ − \end{matrix}^{p} → t′}

\frac{ℙ; s ⊢ t_{i} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → t′}{ℙ; s ⊢ Σ_{i∈I}t_{i} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → t′}  \frac{ℙ; s ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → u a ∈ s}{ℙ; s ⊢ Σ_{α∈ℕ}t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → u}  \frac{ℙ; s ⊢ t[recy.t/y] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → u}{ℙ; s ⊢ recy.t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → u}

\frac{ℙ_{i}; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → t′}{Σ_{i∈I}ℙ_{i}; s ⊢ i:t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{i:p (x)} → t′}  \frac{Σ_{i∈I}ℙ_{i}; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{i:p (x)} → t′}{ℙ_{i}; s ⊢ π_{i}t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → t′}  \frac{ℚ; s ⊢ t[u/x] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → v s ⊢ u : ℙ}{ℙ → ℚ; s ⊢ λx.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{u↦p (x)} → v}

\frac{ℙ → ℚ; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{u↦p (x)} → v}{ℚ; s ⊢ tu \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → v}  \frac{ℙ; s ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → v a ∈ s}{ℕ → ℙ; s ⊢ λα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{a↦p (x)} → v}  \frac{ℕ → ℙ; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{a↦p (x)} → v}{ℙ; s ⊢ ta \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → v}

\frac{ℙ; s ∪^{.} \{a\} ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α] (x)} → u[a/α]}{δℙ; s ⊢ newα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.p[x′[α]/x] (x′)} → newα.u}  \frac{δℙ; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.p[x′[α]/x] (x′)} → u}{ℙ; s ∪^{.} \{a\} ⊢ t[a] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α] (x)} → u[a]}

\frac{ℙ; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → t′ ℚ; s ⊢ u[t′/x] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{q (x′)} → v}{ℚ; s ⊢ [t > p(x) ⇒ u] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{q (x′)} → v}

In the rule for new name abstraction, the conditions a ∉ n(p) and a ∉ n(u) must hold.

Table 1: new-HOPLA: transition rules

— New name abstraction and β-equivalence:

ℚ; s ∪^{.} \{a\} ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α] (y)} → t′[a/α]

δℚ; s ⊢ newα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.α↦p[y′[α]/y] (y′)} → newα.t′

ℚ; s ∪^{.} \{a\} ⊢ (newα.t)[a] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α] (y)} → (newα.t′)[a]

Again by uniqueness of the derivation, (newα.t)[a] and t[a/α] have the same transition capabilities for a fresh name a.

— Matching the prefix action:

{!ℙ; s ⊢ !t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{!x (x)} → t ℚ; s ⊢ u[t/x] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → u′ \atop ℚ; s ⊢ [!t > !x(x) ⇒ u] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → u′}

The derivation above illustrates the simplest case of pattern matching. The term being tested !t emits the prototypical action ! and continues as t. Then the computation path !x is matched against the path pattern !x; matching is successful and the continuation t is bound to x in u, which then executes. Pattern matching allows for the testing of arbitrary actions, even if a little care is needed when new names are involved.

— Matching and new name abstraction:

!ℙ; s ∪^{.} \{a\} ⊢ !t[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{!x′ (x′)} → t[a/α] δ!ℙ; s ⊢ newα.!t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.!x[α] (x)} → newα.t ℚ; s ⊢ u[newα.t/x] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → u′

ℚ; s ⊢ [newα.!t > newα.!x[α](x) ⇒ u] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (y)} → u′

The resumption of a term of type δℙ after a transition is always a new name abstraction, and the new name generated in testing a pattern (above it is a) is local to the test.

2.2 Typing judgements

Consider a term t = t′[α]. As we have discussed in the previous section, the square brackets denote new-name application: any name instantiating α should be fresh for the term t′. Consider now the context C[−] = λα.−. In the term C[t] = λα.(t′[α]), the variable α is abstracted via a lambda abstraction, and may be instantiated with any current name. In particular it may be instantiated with names that belong to the support of t′, thus breaking the hypothesis that t′ has been applied to a fresh name. The same problem arises with contexts of the form C[−] = Σ_{α∈ℕ}−. Moreover, if the process variable x is free in t, a context like C[−] = λx.− might instantiate x with an arbitrary term u. As the name instantiating α might belong to the support of u, nothing ensures it is still fresh for the term t[u/x].

The type system must sometimes ensure that name variables are instantiated by fresh names. To impose this restriction, the typing context contains not only typing assumptions about name and process variables, such as α:ℕ and x:ℙ, but also freshness assumptions (or distinctions) about them, written (α, β) or (α, x). Here the intended meaning of (α, β) is that, in any environment, the names instantiating the variables α and β must be distinct. A freshness assumption like (α, x), where x is a process variable, records that in any environment the name instantiating α must be fresh for the term instantiating x.

Using this auxiliary information, the type system assumes that it is safe to abstract a variable, using lambda abstraction or sum over names, only if no freshness assumptions have been made on it.

The type system of new-HOPLA terms can be specified using judgements of the form:

A; Γ; d ⊢ t : ℙ

where

• A ≡ α_{1}:ℕ, …, α_{k}:ℕ is a collection of name variables;

• Γ ≡ x_{1}:ℙ_{1}, …, x_{k}:ℙ_{k} is a partial function from of process variables, together with their types;

\overline{A; Γ; d; ; x:ℝ ⊩ !x : !ℝ}  \frac{A; Γ; d; ; x:ℝ ⊩ p : ℙ}{A; Γ; d; ; x:ℝ ⊩ α · p : ℕ ⊗ ℙ}α ∈ A

\frac{α:ℕ, A; Γ; d; ; x:ℝ ⊩ p : ℙ}{A; Γ; (d \ α); ; x′:δℝ ⊩ newα.p[x′[α]/x] : δℙ} \frac{A; Γ; d; ; x:ℝ ⊩ p : ℙ}{A; Γ; d; ; x:ℝ ⊩ α ↦ p : ℙ}α ∈ A

\frac{A; Γ; d ⊢ u : ℚ A; Γ; d; ; x:ℝ ⊩ p : ℙ}{A; Γ; d; ; x:ℝ ⊩ u ↦ p : ℚ → ℙ}  \frac{A; Γ; d; ; x:ℝ ⊩ p : ℙ_{j} j ∈ I}{A; Γ; d; ; x:ℝ ⊩ (j:p) : Σ_{i∈I}ℙ_{i}}

\frac{A; Γ; d; ; x:ℝ ⊩ t : ℙ_{j}[μP⃗ .ℙ⃗/P⃗]}{A; Γ; d; ; x:ℝ ⊩ t : μ_{j}P : ℙ⃗}  \frac{A; Γ; d; ; x:ℝ ⊩ p : ℙ}{A′; Γ′; d′; ; x:ℝ ⊩ p : ℙ} \begin{matrix}A ⊆ A′ \\ Γ ⊆ Γ′ \\ d ⊆ d′ \end{matrix}

Table 2: new-HOPLA: typing rules for actions

• d is a set of pairs (α, x) ∈ A × Γ, and (α, β) ∈ A × A, keeping track of the freshness assumptions.

Notation: We write d\α for the set of freshness assumptions obtained from d by deleting all pairs containing α. The order in which variables appear in a distinction is irrelevant; we will write (α, β) ∈ d as a shorthand for (α, β) ∈ d or (β, α) ∈ d. When we write Γ ∪ Γ′ we allow the environments to overlap; the variables need not be disjoint provided the environments are consistent.

Actions are typed along the same lines, even if type judgements explicitly report the resumption variable:

A; Γ; d; ; x:ℝ ⊩ p : ℙ .

The meaning of the environment A; Γ; d is exactly the same as above. The variable x is the resumption variable of the pattern p, and its type is ℝ.

The type system of new-HOPLA is reported in Table 2 and Table 3.

The rule responsible for generating freshness assumptions is the rule for new-name application. If the term t has been typed in the environment A; Γ; d and α is a new name variable (that is, α ∉ A), then the term t[α] is well-typed under the hypothesis that any name instantiating the variable α is distinct from all the names in terms instantiating the variables that can appear in t. This is achieved adding the set of freshness assumptions {α} × (Γ ∪ A) to d (when convenient, as here, we will confuse an environment with its domain).

The rule for pattern matching also modifies the freshness assumptions. The operational rule of pattern matching substitutes a subterm of t, whose names are contained in A′, for x. Accordingly, the typing rule initially checks that no name in A′ belongs to the set of the variables supposed fresh for x. Our attention is then drawn to the term u[t′/x], where t′ is a subterm of t. A name variable α ∈ A supposed fresh from x when typing u, must now be supposed fresh from all the free variables of t′. This justifies the freshness assumptions {{α} × (A′ ∪ Γ′) | (α, x) ∈ d}.

\overline{A; Γ; d ⊢ ∅ : ℙ}  \overline{A; x:ℙ, Γ; d ⊢ x : ℙ}  \frac{A; Γ; d ⊢ t : ℙ}{A′; Γ′; d′ ⊢ t : ℙ} \begin{matrix}A ⊆ A′ \\ Γ ⊆ Γ′ \\ d ⊆ d′ \end{matrix}

\frac{α:ℕ, A; Γ; d ⊢ t : ℙ}{A; Γ; d ⊢ Σ_{α∈ℕ}t : ℙ}α ∉ d  \frac{α:ℕ, A; Γ; d ⊢ t : ℙ}{A; Γ; d ⊢ λα.t : ℕ → ℙ}α ∉ d

\frac{A; x:ℚ, Γ; d ⊢ t : ℙ}{A; Γ; d ⊢ λx.t : ℚ → ℙ}x ∉ d  \frac{A; x:ℙ, Γ; d ⊢ t : ℙ}{A; Γ; d ⊢ recx.t : ℙ}x ∉ d

\frac{α:ℕ, A; Γ; d ⊢ t : ℙ}{A; Γ; (d \ α) ⊢ newα.t : δℙ}  \frac{A; Γ; d ⊢ t : δℙ}{α:ℕ, A; Γ; d ∪ (\{α\} × (Γ ∪ A)) ⊢ t[α] : ℙ}

\frac{A; Γ; d ⊢ t : ℕ → ℙ}{A; Γ; d ⊢ tα : ℙ}α ∈ A  \frac{A; Γ; d ⊢ t : ℙ → ℚ A; Γ; d ⊢ u : ℙ}{A; Γ; d ⊢ tu : ℚ}

\frac{A; Γ; d ⊢ t_{i} : ℙ ∀i ∈ I}{A; Γ; d ⊢ Σ_{i∈I}t_{i} : ℙ}  \frac{A; Γ; d ⊢ t : ℙ_{i}}{A; Γ; d ⊢ i:t : Σ_{i∈I}ℙ_{i}}  \frac{A; Γ; d ⊢ t : Σ_{i∈I}ℙ_{i}}{A; Γ; d ⊢ π_{i}t : ℙ_{i}}  \frac{A; Γ; d ⊢ t : ℙ}{A; Γ; d ⊢ !t : !ℙ}

\frac{A; Γ; d ⊢ t : ℙ}{A; Γ; d ⊢ α · t : ℕ ⊗ ℙ}α ∈ A  \frac{A; Γ; d ⊢ t : ℕ ⊗ ℙ}{A; Γ; d ⊢ π_{α}t : ℙ}α ∈ A  \frac{A; Γ; d ⊢ t : ℙ_{j}[μP⃗ .ℙ⃗/P⃗]}{A; Γ; d ⊢ t : μ_{j}P : ℙ⃗}

\frac{A′; Γ′; d′ ⊢ t : ℙ A′; Γ′; d′; ; x:ℝ ⊩ p : ℙ A; x:ℝ, Γ; d ⊢ u : ℚ}{A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ [t > p(x) ⇒ u] : ℚ}A′∩\{α | (α, x) ∈ d\} = ∅

where \overline{d} = (d \ x) ∪ d′ ∪ \{\{α\} × (A′ ∪ Γ′) | (α, x) ∈ d\}

Table 3: new-HOPLA: typing rules for processes

The rest of the type system follows along the lines of type systems for the simply typed λ-calculus.

The type system assumes that terms do not contain name constants. This is to avoid the complications in a type system coping with both name variables and constants at the same time. We write s ⊢ t : ℙ when there is a judgement A; ∅; d ⊢ σt′ : ℙ and a substitution σ for A respecting the distinctions d such that t is σt′. In particular, s ⊢ t : ℙ iff there is a canonical judgement A; ∅; {(α, β) | α ≠ β} ⊢ t′ : ℙ, in which the substitution σ is a bijection between name variables and names and t is σt′. Similarly for patterns.

We can now prove that the operational rules are type correct.

Lemma 2.2 (Substitution Lemma)

1. Suppose that A′; Γ′; d′ ⊢ t : ℚ and A; x:ℚ, Γ; d; ; y:ℝ ⊩ p : ℙ, where Γ ∪ Γ′ is consistent and A′ ∩ {α | (α, x) ∈ d} = ∅. Then,

A ∪ A′; Γ ∪ Γ′; \overline{d}; ; y:ℝ ⊩ p[t/x] : ℙ

where \overline{d} = (d \ x) ∪ d′ ∪ \{\{α\} × (A′ ∪ Γ′) | (α, x) ∈ d\}.

2. Suppose that A′; Γ′; d′ ⊢ t : ℚ and A; x:ℚ, Γ; d ⊢ u : ℙ, where Γ ∪ Γ′ is consistent and A′ ∩ {α | (α, x) ∈ d} = ∅. Then,

A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ u[t/x] : ℙ

where \overline{d} = (d \ x) ∪ d′ ∪ \{\{α\} × (A′ ∪ Γ′) | (α, x) ∈ d\}.

Lemma 2.3 (Contraction Rules) The rules below can be derived (also for patterns):

\frac{α:ℕ, β:ℕ, A; Γ; d ⊢ p : ℙ}{α:ℕ, A; Γ; d[α/β] ⊢ p[α/β] : ℙ}(α, β) ∉ d \frac{A; y:ℚ, z:ℚ, Γ; d ⊢ p : ℙ}{A; y:ℚ, Γ; d[y/z] ⊢ p[y/z] : ℙ}

Theorem 2.4 (Transitions preserve types) If s ⊢ t : ℙ and s; ; x:ℝ ⊩ p : ℙ and

ℙ; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → t′, then s ⊢ t′ : ℝ.

Some simple results follow. They can be proved by routine inductions on derivations of transition.

Lemma 2.5 If n(t) ⊆ s and ℙ; s ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → t′, then n(t′) ⊆ s.

Lemma 2.6 If ℙ; s ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → t′, then n(t) ∪ n(p) ∪ n(t′) ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → t′.

Lemma 2.7 (Injective renaming) If ℙ; s ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → t′ and f : s → s′ is injective, then

ℙ; s′ ⊢ ft \begin{matrix}− \\ − \\ − \end{matrix}^{fp} → ft′.

Lemma 2.8 (Converse of injective renaming) Let f : s → s′ injective. If ℙ; s′ ⊢

ft \begin{matrix}− \\ − \end{matrix}^{p′} → u′, then there exists p, u and g : s′′ → n(p′, u′) \ ran(f) bijective, with s′′ ∩ s = ∅, such that ℙ; s, s′′ ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → u and p′ = (f + g)p and u′ = (f + g)u.

Observe that if s′ ⊢ ft \begin{matrix}− \\ − \end{matrix}^{p′} → u′ then ft can chose nondeterministically some names in (s′ \ s) before performing p′ (because of the semantics of the sum over names). This motivates the need for s′′ in the Lemma above. As a consequence, bisimulation techniques based on injective renaming cannot be applied to new-HOPLA.

3 Equivalences

After introducing some notations regarding relations, we explore the bisimulation equivalence that arises from the transition semantics.

A relation R between typing judgements is said to respect types if, whenever R relates E_{1} ⊢ t_{1} : ℙ_{1} and E_{2} ⊢ t_{2} : ℙ_{2}, we have E_{1} = E_{2} and ℙ_{1} = ℙ_{2}. We are mostly interested in relations between closed terms, and we write s ⊢ t R u : ℙ to denote (s ⊢ t : ℙ, s ⊢ q : ℙ) ∈ R.

Definition 3.1 (Bisimilarity) A type-respecting relation on closed terms, R, is a bisimulation if 1. s ⊢ t R u : ℙ and ℙ; s′ ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ for s′ ⊇ s imply that there exists a term u′ such

that ℙ; s′ ⊢ u \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → u′ and s′ ⊢ t′ R u′ : ℝ;

2. s ⊢ t R u : ℙ and ℙ; s′ ⊢ u \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → u′ for s′ ⊇ s imply that there exists a term t′ such

that ℙ; s′ ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ and s′ ⊢ t′ R u′ : ℝ;

where ℝ is the type of the resumption variable x in p. Let bisimilarity, denoted ∼, be the largest bisimulation.

We say that two closed terms t and q are bisimilar if s ⊢ t ∼ q : ℙ for some s and ℙ.

In the definition of bisimulation, the universal quantification on sets of names s′ is required, otherwise we would relate

{a} ⊢ λα.[α!0 > a!x ⇒ !0] : ℕ ⊗ !0  and  {a} ⊢ λα.!0 : ℕ ⊗ !0

while the two terms above behave differently in a world where a is not the only current name.

Using an extension of Howe’s method [6] as adapted by Gordon and Pitts to a typed setting [5, 10], we show that bisimilarity is preserved by well typed contexts. Theorem 3.2 Bisimilarity ∼ is an equivalence relation and a congruence.

Proposition 3.3 For closed, well-formed, terms we have

s ⊢ (λx.t)u ∼ t[u/x] : ℙ  s ⊢ (λα.t)a ∼ t[a/α] : ℙ
s ⊢ λx.(tx) ∼ t : ℙ → ℚ  s ⊢ λα.(tα) ∼ t : ℕ → ℙ
s ⊢ λx.(Σ_{i∈I}t_{i}) ∼ Σ_{i∈I}(λx.t_{i}) : ℙ → ℚ  s ⊢ λα.(Σ_{i∈I}t_{i}) ∼ Σ_{i∈I}(λα.t_{i}) : ℕ → ℙ
s ⊢ (Σ_{i∈I}t_{i})u ∼ Σ_{i∈I}(t_{i}u) : ℙ  s ⊢ (Σ_{i∈I}t_{i})a ∼ Σ_{i∈I}(t_{i}a) : ℙ
s ⊢ π_{β}(β · t) ∼ t : ℙ  s ⊢ π_{β}(α · t) ∼ 0 : ℙ
s ⊢ t ∼ Σ_{α∈ℕ}α · (π_{α}t) : ℕ ⊗ ℙ
s ⊢ β · (Σ_{i∈I}t_{i}) ∼ Σ_{i∈I}β · t_{i} : ℙ  s ⊢ π_{β}(Σ_{i∈I}t_{i}) ∼ Σ_{i∈I}π_{β}t_{i} : ℙ
s ⊢ [!u > !x ⇒ t] ∼ t[u/x] : ℙ  s ⊢ [Σ_{i∈I}u_{i} > !x ⇒ t] ∼ Σ_{i∈I}[u_{i} > !x ⇒ t] : ℙ

Proposition 3.4 Bisimilarity validates β-reduction on new-name abstraction:

s ∪^{.} {a} ⊢ (newα.t)[a] ∼ t[a/α] : ℙ .

Corollary 3.5 If s ⊢ newα.t ∼ newα.u : δℙ then s ∪^{.} {a} ⊢ t[a/α] ∼ u[a/α] : ℙ for all a ∉ n(t, u).

Proposition 3.6 (β-equivalence on new names) Let t be a term with α free, that is A, α; ∅; A, d ⊢ t : ℙ. Let σ : s → A be a bijection. Then

s ∪^{.} {a} ⊢ (newα.t)[a] ∼ t[a/α] : ℙ .

Corollary 3.7 If s ⊢ newα.t ∼ newα.u : δℙ, then s ∪^{.} {a} ⊢ t[a/α] ∼ u[a/α] : ℙ.

Corollary 3.8 Let t and u be terms such that A, α:ℕ; ∅; A, d ⊢ t : ℙ, let σ : s → A be a bijection, and let a, a′ be names not in s. If s ∪^{.} {a} ⊢ t[a/α] ∼ u[a/α] : ℙ then

s ∪^{.} {a′} ⊢ t[a′/α] ∼ u[a′/α] : ℙ.

Proof By Proposition 3.5 s ⊢ newα.t ∼ newα.u : δℙ. The result follows by Corollary 3.7. □

4 Examples

In this section, we illustrate how new-HOPLA can be used to give semantics to well-known process algebras. We define a ‘fully abstract’ encoding of π-calculus that preserves and reflects both the reduction relation and strong bisimilarity. We also report an encoding of Higher-Order π-calculus and of Mobile Ambients.

We introduce an useful product type ℙ & ℚ, which is not primitive in new-HOPLA. It is definable as 1:ℙ + 2:ℚ. The projections are given by fst(t) = π_{1}(t) and snd(t) = π_{2}(t), while pairing is defined as (t, u) = 1:t + 2:u. For actions (p, −) = 1:p, (−, q) = 2:q. It is then easy to verify that s ⊢ fst(t, u) ∼ t : ℙ, that s ⊢ snd(t, u) ∼ u : ℚ, and that s ⊢ (fst(t, u), snd(t, u)) ∼ (t, u) : ℙ & ℚ, for all s ⊇ n(t) ∪ n(u).

4.1 π-calculus

We denote name constants with a, b, …, and name variables with α, β, …; the letters n, m, … range over both name constants and name variables. The terms of the language are constructed according the following grammar:

P, Q ::= 0 | P | Q | (να)P | \overline{n}m.P | n(α).P .

The late labelled transition system (denoted \begin{matrix}− \\ − \end{matrix}^{α} →_{l}) and the definition of strong late bisimulation (denoted ∼_{l}) are standard [12], and for reference are reported in Appendix A.3.

We can specify a type ℙ as

ℙ = τ:!ℙ + out:ℕ ⊗ ℕ ⊗!ℙ + bout:ℕ ⊗!(δℙ) + inp:ℕ ⊗!(ℕ → ℙ) .

The terms of π-calculus can be expressed in new-HOPLA as the following terms of type ℙ:

⟦0⟧ = 0 ⟦\overline{n}m.P ⟧ = out:n · m ·!⟦P ⟧ ⟦n(β).P ⟧ = inp:n ·!(λβ.⟦P ⟧)
⟦(να)P ⟧ = Res (newα.⟦P ⟧) ⟦P | Q⟧ = ⟦P ⟧ || ⟦Q⟧

Here, Res : δℙ → ℙ and || : ℙ&ℙ → ℙ (we use infix notation for convenience) and are abbrevations for the following recursively defined processes:

Res t = [t > newα.τ:!(x[α])) ⇒ τ:!Res x]
+ Σ_{β∈ℕ}Σ_{γ∈ℕ}[t > newα.out:β · γ ·!(x[α]) ⇒ out:β · γ ·!Res x]
+ Σ_{β∈ℕ}[t > newα.out:β · α ·!(x[α]) ⇒ bout:β ·!x]
+ Σ_{β∈ℕ}[t > newα.bout:β ·!(x[α]) ⇒ bout:β ·!newγ · Res (newη.x[η][γ])]
+ Σ_{β∈ℕ}[t > newα.inp:β ·!(x[α]) ⇒ inp:β ·!λγ.Res (newη.x[η](γ))]
t || u = [t > τ:!x ⇒ τ:!(x || u)]
+ Σ_{β∈ℕ}Σ_{γ∈ℕ}[t > out:(β · γ ·!x) ⇒ [u > inp:(β ·!y) ⇒ τ:!(x || yγ)]]
+ Σ_{β∈ℕ}[t > bout:(β ·!x) ⇒ [u > inp:(β ·!y) ⇒ τ:!Res (newη.(x[η] || yη))]]
+ Σ_{β∈ℕ}Σ_{γ∈ℕ}[t > out:β · γ ·!x ⇒ out:β · γ ·!(x || u)]
+ Σ_{β∈ℕ}[t > bout:β ·!x ⇒ bout:β ·!newη.(x[η] || u)]
+ Σ_{β∈ℕ}[t > inp:β ·!x ⇒ inp:β ·!λη.(x(η) || u)]
+ symmetric cases

where η is chosen such that η ∉ n(u). Informally, the restriction map Res : δℙ → ℙ pushes restrictions inside processes as far as possible. The five summands corresponds to the five equations below:

(να)τ.P ∼_{l} τ.(να)P
(να)\overline{m}n.P ∼_{l} \overline{m}n.(να)P if α ≠ m, n (να)\overline{m}α.P ∼_{l} \overline{m}(α).P if α ≠ m
(να)\overline{m}(β).P ∼_{l} \overline{m}(β).(να)P if α ≠ m (να)mβ.P ∼_{l} mβ.(να)P if α ≠ m

where \overline{m}(α) is an abbreviation to express bound-output, that is, (να)\overline{m}α. The map Res implicitly also ensures that (να)P ∼_{l} 0 if none of the above cases applies. The parallel composition map || captures the (late) expansion law of π-calculus. There is a strong correspondence between actions performed by a closed π-calculus process and the actions of its encoding.

Theorem 4.1 Let P a closed π-calculus process. If P \begin{matrix}− \\ − \end{matrix}^{τ} →_{l} P′ is derivable in π-calculus, then n(⟦P ⟧) ⊢ ⟦P ⟧ \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} →∼ ⟦P′⟧. Conversely, if n(⟦P ⟧) ⊢ ⟦P ⟧ \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} → t in new-HOPLA, then P \begin{matrix}− \\ − \end{matrix}^{τ} →_{l} P′ for some P′, and n(t) ⊢ t ∼ ⟦P′⟧ : ℙ.

The encoding also preserves and reflects late strong bisimulation.

Theorem 4.2 Let P and Q be two closed π-calculus processes. If P ∼_{l} Q then n(P) ∪ n(Q) ⊢ ⟦P ⟧ ∼ ⟦Q⟧ : ℙ. Conversely, if n(⟦P ⟧) ∪ n(⟦Q⟧) ⊢ ⟦P ⟧ ∼ ⟦Q⟧ : ℙ, then P ∼_{l} Q.

Early semantics Along the same lines, new-HOPLA can encode the early semantics of π-calculus. The type of the input action assigned to π-calculus terms captures the difference between the two semantics. In the late semantics a process performing an input action has type inp:ℕ ⊗!(ℕ → ℙ): the type of the continuation (ℕ → ℙ) ensures that the continuation is actually an abstraction that will be instantiated with the received name when interaction takes place. In the early semantics, the type of a process performing an input action is changed into inp:ℕ ⊗ ℕ → !ℙ. Performing an input action now involves picking up a name before executing the prototypical action, and in the continuation (whose type is ℙ) the formal variable has been instantiated with the received name. Details can be found in [15].

Polyadic π-calculus A natural and convenient extension to π-calculus is to admit processes that pass tuples of names: polyadicity is a good testing ground for the expressivity of our language.

We can specify a type for polyadic π-calculus processes as:

ℙ = τ:!ℙ + out:ℕ ⊗ ℂ + inp:ℕ ⊗!𝔽
ℂ = 0:ℕ ⊗ ℂ + 1:δℂ + 2:!ℙ
𝔽 = 3:ℕ → 𝔽 + 4:ℙ

Recursive types are used to encode tuples of (possibly new) names in concretions, and sequences of name abstractions in abstractions.

Just as with the π-calculus, it is possible to write a restriction map Res : δℙ → ℙ that pushes restrictions inside processes as far as possible, and a parallel map that captures the expansion law. The resulting semantics coincides with the standard late semantics of polyadic π-calculus. Details can be found in [15].

4.2 Higher-Order π-calculus

The language we consider can be found in [12], with one main difference: rather than introducing a unit value, we allow processes in addition to abstractions to be communicated. For brevity, we gloss over typing issues. The syntax of terms and values is defined below.

P, Q ::= V • W | n(x).P | \overline{n}(V).P | P | Q | x | (να)P | 0
V, W ::= P | (x).P

The reduction semantics for the language is standard [12]; we only recall the axioms that define the reduction relation:

(x).P • V ⇾ P [V/x] \overline{n}(V).P | n(x).Q ⇾ P | Q[V/x] .

Types for HOπ are given recursively by

ℙ = τ:!ℙ + out:ℕ⊗!ℂ + inp:ℕ⊗!(𝔽 → ℙ) ℂ = 0:𝔽&ℙ+ 1:δℂ 𝔽 = 2:ℙ+3:𝔽 → ℙ .

Concretions of the form (να̃)⟨V ⟩P correspond to terms of type ℂ; recursion on types is used to encode the tuple of restricted names α̃. The function ⟦−⟧_{v} translates values into the following terms of type 𝔽:

⟦P ⟧_{v} = 2:⟦P ⟧ ⟦(x).P ⟧_{v} = 3:λx.⟦P ⟧

while the function ⟦−⟧ translates processes into terms of type ℙ:

⟦V •W ⟧ = τ:!(π_{3}⟦V ⟧_{v})(π_{2}⟦W ⟧_{v}+π_{3}⟦W ⟧_{v}) ⟦P | Q⟧ = ⟦P ⟧ || ⟦Q⟧ ⟦x⟧ = x ⟦0⟧ = 0

⟦n(x).P ⟧ = inp:n·!(λx.⟦P ⟧) ⟦\overline{n}(V)⟧ = out:n·!(⟦V ⟧_{v}, ⟦P ⟧) ⟦(να)P ⟧ = Res newα.⟦P ⟧ .

The restriction map Res : δℙ → ℙ filters the actions that a process emits, blocking actions that refer to the name that is being restricted. Output actions cause names to be extruded: the third summand records these names in the appropriate concretion.

Res t = [t > newα.τ:!x[α] ⇒ τ:!Res x]
+ Σ_{β∈ℕ}[t > newα.inp:(β ·!x[α]) ⇒ inp:(β ·!λy.Res (newγ.x[γ](y)))]
+ Σ_{β∈ℕ}[t > newα.out:(β ·!x[α]) ⇒ out:(β ·!3:x)]

Parallel composition is a family of mutually dependent operations also including components such as ||_{i} of type ℂ&𝔽 → ℙ to say how values compose in parallel with concretions etc. All these components can be tupled together in a product and parallel composition defined as a simultaneous recursive definition:

— Processes in parallel with processes:

t || u = Σ_{β∈ℕ}[t > out:β ·!x ⇒ [u > inp:β ·!y ⇒ τ:!(x || y)]]
+ Σ_{β∈ℕ}[u > inp:β ·!y ⇒ inp:β ·!(t ||_{a} y)]
+ Σ_{β∈ℕ}[u > out:β ·!y ⇒ out:β ·!(t ||_{c} y)]
+ [u > τ:!y ⇒ τ:!(t || y)]
+ symmetric cases

— Concretions in parallel with values

c ||_{i} f = snd(π_{0}c) || (π_{3}f)(π_{2}(fst(π_{0}c))+π_{3}(fst(π_{0}c)))+Res (newα.(((π_{1}c)[α]) ||_{i} f))

— Concretions in parallel with processes

c ||_{c} t = 0:(fst(π_{0}c), snd(π_{0}c) || t) + 1:(newα.((π_{1}c)[α] ||_{c} t))

— Values in parallel with processes

f ||_{a} t = λx.(((π_{3}f)x) || u)

The remaining cases are given symmetrically. The proposed encoding agrees with the reduction semantics of HOπ. The resulting bisimulation is analogous to the so called higher-order bisimulation [1, 14], and as such it is strictly finer than observational equivalence. It is an open problem whether it is possible to provide an encoding of HOπ that preserves and reflects the natural observational equivalence.

4.3 Mobile Ambients

We sketch an encoding of the mobility core of the Ambient Calculus, extending the encoding of Mobile Ambients with public names into HOPLA given in [7].

Again, we denote name constants with a, b, …, name variables with α, β, …, and we let n, m, … range over both name constants and name variables. The terms of the language are constructed according the following grammar:

P ::= 0 | n[P] | P | P | (να)P | in n.P | out n.P | open n.P .

With respect to the HOPLA encoding, the syntax has been enriched with the restriction operator.

Types reflect the actions that ambient processes can perform, and can be given recursively by:

ℙ = τ:!ℙ + in:ℕ ⊗!ℙ + out:ℕ ⊗!ℙ + open:ℕ ⊗!ℙ
+ mvin:ℕ ⊗!ℂ + mvout:ℕ ⊗!ℂ
+ \overline{open}:ℕ ⊗!ℙ + \overline{mvın}:ℕ ⊗!𝔽
ℂ = 0:ℙ&ℙ + 1:δℂ
𝔽 = ℙ → ℙ

The injections in, out, and open correspond to the basic capabilities a process can exercise, while their action on the enclosing ambients is registered by the components mvin and mvout. The injections \overline{open} and \overline{mvın} record the receptive interactions that an ambient can (implicitly) have with the environment. Again, recursive types are used in concretions to record the sequence of names that must be extruded. In the HOPLA encoding, the type of concretions was ℂ = ℙ&ℙ: it has been changed to reflect that mobility can cause extrusion of names, along the lines of our treatment of HOπ.^{3}

3Note a minor notational change: the meaning of actions-coactions mvin, \overline{mvın} and open, \overline{open} has been swapped with respect to the encoding of MA into HOPLA.

The translation of terms is inherited from the HOPLA paper, with the addition of the rule for the restriction operator.

⟦0⟧ = 0  ⟦in n.P ⟧ = in n ·!⟦P ⟧
⟦n[P]⟧ = Amb (n, ⟦P ⟧)  ⟦out n.P ⟧ = out n ·!⟦P ⟧
⟦P | Q⟧ = ⟦P ⟧ || ⟦Q⟧  ⟦open n.P ⟧ = open n ·!⟦P ⟧
⟦(να)P ⟧ = Res (newα.⟦P ⟧)

The restriction map Res : δℙ → ℙ filters the actions that a process emit, and blocks actions that refer to the name that is restricted. In fact, in Pure Mobile Ambients, the only scope extrusions are caused by mobility, and not by pre-actions.

Res : δℙ → ℙ
Res t = [t > newα.τ:x[α] ⇒ τ:Res x)]
+ Σ_{β∈ℕ}[t > newα.in:(β ·!x[α]) ⇒ in:(β ·!Res x)]
+ Σ_{β∈ℕ}[t > newα.out:(β ·!x[α]) ⇒ out:(β ·!Res x)]
+ Σ_{β∈ℕ}[t > newα.open:(β ·!x[α]) ⇒ open:(β ·!Res x)]
+ Σ_{β∈ℕ}[t > newα.mvin:(β ·!x[α]) ⇒ mvin:(β ·!1:x)
+ Σ_{β∈ℕ}[t > newα.mvout:(β ·!x[α]) ⇒ mvout:(β ·!1:x)
+ Σ_{β∈ℕ}[t > newα.\overline{open}:(β ·!x[α]) ⇒ \overline{open}:(β ·!Res x)]
+ Σ_{β∈ℕ}[t > newα.\overline{mvın}:(β ·!x[α]) ⇒ \overline{mvın}:(β ·!λy.Res (newγ.x[γ](y)))]

Parallel composition is a family of operations, one of which is a binary operation between processes, ||_{ℙ&ℙ}: ℙ&ℙ → ℙ. The family is defined in a simultaneous recursive definition below.

• Processes in parallel with processes:

t || u = Σ_{β∈ℕ}[t > \overline{open}: β ·!x ⇒ [u > open: β ·!y ⇒ τ:·!(x || y)]]
+ Σ_{β∈ℕ}[t > \overline{mvın}: β ·!f ⇒ [u > mvin: β ·!c ⇒ τ:·!(c || f)]]
+ [t > τ:!x ⇒ τ:!(x || u)]
+ Σ_{β∈ℕ}[t > in:β ·!x ⇒ in:β ·!(x || u)]
+ Σ_{β∈ℕ}[t > out:β ·!x ⇒ out:β ·!(x || u)]
+ Σ_{β∈ℕ}[t > open:β ·!x ⇒ open:β ·!(x || u)]
+ Σ_{β∈ℕ}[t > mvin:β ·!x ⇒ mvin:β ·!(x || u)]
+ Σ_{β∈ℕ}[t > mvout:β ·!x ⇒ mvout:β ·!(x || u)]
+ Σ_{β∈ℕ}[t > \overline{open}:β ·!x ⇒ \overline{open}:β ·!(x || u)]
+ Σ_{β∈ℕ}[t > \overline{mvın}:β ·!x ⇒ \overline{mvın}:β ·!(x || u)]
+ symmetric cases.

All summands except the first two correspond to congruence rules.

• Concretions in parallel with abstractions:

c ||_{i} f = snd(π_{0}c) || f(fst(π_{0}c)) + Res (newα.(((π_{1}c)[α]) ||_{i} f))

• Concretions in parallel with processes:

c ||_{c} t = 0:(fst(π_{0}c), snd(π_{0}c) || t) + 1:(newα.((π_{1}c)[α] ||_{c} t))

• Abstractions in parallel with processes:

f ||_{a} t = λx.((fx) || u)

Remaining cases are given symmetrically.

Finally, ambient creation can be defined recursively in new-HOPLA as an operation Amb : ℕ&ℙ → ℙ:

Amb (m, t) = [t > τ:!x ⇒ τ:!Amb (m, x)]
+ Σ_{β∈ℕ}[t > in:β ·!x ⇒ mvin:β ·!(Amb (m, x), 0)
+ Σ_{β∈ℕ}[t > out:β ·!x ⇒ mvout:β ·!(Amb (m, x), 0)
+ [t > mvout:m ·!c ⇒ τ:!Extr (m, c)]
+ \overline{open}:m ·!t + \overline{mvın}:m ·!λy.Amb (m, t || y)

where the map Extr : ℕ&ℂ → ℙ extrudes names across ambient’s boundary after an mvout action:

Extr(m, c) = fst(π_{0}c) || Amb (m, snd(π_{0}c)) + Res (newα.(Extr (m, (π_{1}c)[α]))) .

The denotations of ambients are determined by their capabilities: an ambient m[t] can perform the internal (τ) actions of t, enter a brother ambient (mvin n) if called upon to do so by an in n action of t, exit its parent ambient (mvout n) if called upon to do so by an out n action of t, be exited if t so requests through an mvout m action, be opened (\overline{open} m), or be entered by an ambient (\overline{mvın} m); other pre-actions are restricted away. The tree-containment structure of ambients is captured in the chain of \overline{open} m’s that they can perform.

The semantics given above agrees with the reduction semantics of Mobile Ambients, possibly up to structural congruence. It is easy to prove that if the encodings of two processes are bisimilar in new-HOPLA, then they are strong reduction barbed congruent. We do not know if the converse is true (it is false if we add recursive definition of processes to the fragment of MA we consider). Yet, in MA, strong reduction barbed congruence is an extremely discriminating relation and its interest is very limited.

References

[1] G. Boudol. Towards a lambda calculus for concurrent and communicating systems. In Proc. TAPSOFT ’89, volume 351 of LNCS, pages 149–161. Springer Verlag, 1989.

[2] G. L. Cattani, I. Stark, and G. Winskel. Presheaf models for the π-calculus. In Proc. CTCS’97, volume 1290 of LNCS. Springer Verlag, 1997.

[3] M. Fiore, E. Moggi, and D. Sangiorgi. A fully-abstract model for the π-calculus. In Proc. 11th LICS. IEEE Computer Society Press, 1996.

[4] J.Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[5] A. D. Gordon. Bisimilarity as a theory of functional programming: mini-course. Notes Series BRICS-NS-95-3, BRICS, Department of Computer Science, University of Aarhus, July 1995.

[6] D. J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103–112, 1996.

[7] M. Nygaard and G. Winskel. Hopla—a higher-order process language. In Proc. CONCUR’02, volume 2421 of LNCS. Springer Verlag, 2002.

[8] M. Nygaard and G. Winskel. Domain theory for concurrency. To appear in Theoretical Computer Science, special issue on domain theory, 2003.

[9] M. Nygaard and G. Winskel. Full abstraction for HOPLA. In Proc. CONCUR’03, LNCS. Springer Verlag, 2003.

[10] A. M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation, Publications of the Newton Institute, pages 241–298. Cambridge University Press, 1997.

[11] A. M. Pitts and M. J. Gabbay. A metalanguage for programming with bound names modulo renaming. In Proc. MPC 2000, volume 1837 of LNCS. Springer Verlag, 2000.

[12] D. Sangiorgi and D. Walker. The π-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001.

[13] I. Stark. A fully-abstract domain model for the π-calculus. In Proc. 11th LICS. IEEE Computer Society Press, 1996.

[14] B. Thomsen. Calculi for Higher Order Communicating Systems. PhD thesis, Department of Computing, Imperial College, 1990.

[15] F. Zappa Nardelli. De la sémantique des processus d’ordre supérieur. PhD thesis, Université de Paris 7, 2003. Available in English from

http://www.di.ens.fr/~zappa.

A Proofs

A.1 Proofs from Section 2

Proof of Lemma 2.2, page 10 By rule induction.

Inaction. Suppose A; x:ℚ, Γ; d ⊢ 0 : ℙ. As 0[t/x] = 0, we derive A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ 0[t/x] : ℙ by the rule for inactive process.

Variable. Suppose A; x:ℚ, Γ; d ⊢ y : ℙ. If y ≠ x then y[t/x] = y and we derive A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ y[t/x] : ℙ by the rule for identity. If y = x, then y[t/x] = t and ℙ = ℚ: we derive and A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ y[t/x] : ℙ from A′; Γ′; d′ ⊢ t : ℚ by weakening.

Weakening. Suppose that A′′; x:ℚ, Γ′′; d′′ ⊢ u : ℙ has been derived from A; Γ; d ⊢ u : ℙ for A′′ ⊇ A, Γ′′ ⊇ Γ, d′′ ⊇ d. As Γ′′ ∪ Γ′ is consistent, then Γ ∪ Γ′ is consistent as well. If x:ℚ ∈ Γ, then by the induction hypothesis we have A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ u[t/x] : ℙ where \overline{d} = (d \ x) ∪ d′ ∪ \{\{α\} × (A′ ∪ Γ′) | (α, x) ∈ d\}. By weakening we conclude A′′ ∪ A′; Γ′′ ∪ Γ′; (d′′ \ x) ∪ d′ ∪ {{α} × (A′ ∪ Γ′) | (α, x) ∈ d′′} ⊢ u[t/x] : ℙ. If x:ℚ ∉ Γ, then x ∉ fv(u) and u[t/x] = u. The result follows from A; Γ; d ⊢ u : ℙ by weakening.

Tensor. Suppose that A; x:ℚ; d ⊢ α · u : ℙ has been derived from A; x:ℚ; d ⊢ u : ℙ for α ∈ A. By the induction hypothesis we have A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ α · u[t/x] : ℙ. As α ∈ A, α ∈ A ∪ A′ as well, and we conclude by the rule for tensor.

Name projection. Analogous to tensor.

Name abstraction. Suppose that A; x:ℚ, Γ; d ⊢ λα.u : ℕ → ℙ has been derived from α:ℕ, A; x:ℚ, Γ; d ⊢ u : ℙ with α ∉ d. By the induction hypothesis we get (α:ℕ, A)∪A′; Γ∪ Γ′; \overline{d} ⊢ u[t/x] : ℙ. As substitution is capture-avoiding, α:ℕ ∉ A′, and (α:ℕ, A) ∪ A′ = α:ℕ, (A ∪ A′). It remains to show that α ∉ \overline{d}. But α ∉ d′ because α ∉ A′, and α ∉ d because of the hypothesis. Thus, we can conclude by the rule for name abstraction.

Name application. Suppose that A; x:ℚ, Γ; d ⊢ uα : ℙ has been derived from A; x:ℚ, Γ; d ⊢ u : ℕ → ℙ, with α ∈ A. By the induction hypothesis we get A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ u[t/x] : ℕ → ℙ. As α ∈ A, α ∈ (A ∪ A′). As u[t/x]α = uα[t/x], by the rule for name application we get A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ uα[t/x] : ℙ, as required.

New name abstraction. Suppose that A; x:ℚ, Γ; (d \ α) ⊢ newα.u : δℙ has been derived from α:ℕ, A; x:ℚ, Γ; d ⊢ u : ℙ with α ∉ d. By the induction hypothesis we get (α:ℕ, A) ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ u[t/x] : ℙ. As substitution is capture-avoiding, α:ℕ ∉ A′, and (α:ℕ, A) ∪ A′ = α:ℕ, (A ∪ A′). It also holds \overline{d} \ α = ((d \ x) ∪ d′ ∪ \{(α, z) | z ∈ Γ′ and (α, x) ∈ d} ∪ {(α, β) | β ∈ A′ and (α, x) ∈ d}) \ α = ((d \ α) \ x) ∪ d′ ∪ {(α, z) | z ∈ Γ′ and (α, x) ∈ (d \ α)} ∪ {(α, β) | β ∈ A′ and (α, x) ∈ (d \ α)}. Then we can conclude by the rule for new name abstraction.

New name application. Suppose that α:ℕ, A; x:ℚ, Γ; d∪({α}×((x:ℚ, Γ)∪A)) ⊢ u[α] : ℙ has been derived A; x:ℚ, Γ; d ⊢ u : δℙ. We want to show that α:ℕ, (A ∪ A′); Γ ∪ Γ′; \overline{d} ⊢ u[α][t/x] : ℙ where \overline{d} is the set of distinctions:

((d∪({α}×((x:ℚ, Γ)∪A)))\x)∪d′∪{{β}×(A′∪Γ′) | (β, x) ∈ (d∪({α}×((x:ℚ, Γ)∪A)))} .

By the induction hypothesis we get A∪A′; Γ∪Γ′; (d\x)∪d′∪{{β}×(A′∪Γ′) | (β, x) ∈ d} ⊢ u[t/x] : δℙ. As (α, x) ∈ (d∪({α}×((x:ℚ, Γ)∪A))), the hypothesis guarantee that α ∉ A′. By the rule for new name application we derive α:ℕ, (A ∪ A′); Γ ∪ Γ′; d_{1} ⊢ u[t/x][α] : ℙ, where the set of distinctions d_{1} is

(d \ x) ∪ d′ ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ d} ∪ ({α} × (Γ ∪ A)) .

Now, u[t/x][α] = u[α][t/x]. A little care is needed to show that d_{1} is equal to \overline{d}. The set \overline{d} can be rewritten as

(d \ x) ∪ (({α} × ((x:ℚ, Γ) ∪ A)) \ x) ∪ d′ ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ d} ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ ({α} × ((x:ℚ, Γ) ∪ A))}

and in turn as

(d \ x) ∪ ({α} × (Γ ∪ A)) ∪ d′ ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ d} ∪ ({α} × (A′ ∪ Γ′))

and this is equal to d_{1}, as required.

Process abstraction. Suppose that A; x:ℚ, Γ; d ⊢ λy.u : ℝ → ℙ has been derived from A; y:ℝ, x:ℚ, Γ; d ⊢ u : ℙ with y ∉ d. By the induction hypothesis we get A ∪ A′; (y:ℝ, Γ) ∪ Γ′; \overline{d} ⊢ u[t/x] : ℙ. As substitution is capture-avoiding, y:ℝ ∉ Γ′, and (x:ℚ, Γ) ∪ Γ′ = x:ℚ, (Γ ∪ Γ′). It remains to show that x ∉ \overline{d}. But x ∉ d′ because x ∉ Γ′, and x ∉ d because of the hypothesis. Thus, we can conclude by the rule for process abstraction.

Process application. Suppose that A; x:ℚ, Γ; d ⊢ u : ℙ has been derived from A; x:ℚ, Γ; d ⊢ u : ℝ → ℙ and A; x:ℚ, Γ; d ⊢ v : ℝ. By the induction hypothesis we get A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ u[t/x] : ℝ → ℙ and A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ v[t/x] : ℝ. As u[t/x]v[t/x] = uv[t/x], by the rule for process application we get A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ uv[t/x] : ℙ, as required.

Recursion. Analogous to process abstraction.

Sum. Suppose that A; x:ℚ, Γ; d ⊢ Σ_{i∈I}u_{i} : ℙ has been derived from A; x:ℚ, Γ; d ⊢ u_{i} : ℙ for all i ∈ I. By the induction hypothesis we get A∪A′; Γ∪Γ′; \overline{d} ⊢ u_{i}[t/x] : ℙ for all i ∈ I. As Σ_{i∈I}(u_{i}[t/x]) = Σ_{i∈I}u_{i}[t/x], by the rule for sum we get A∪A′; Γ∪Γ′; \overline{d}Σ_{i∈I} ⊢ u_{i}[t/x] : ℙ, as required.

Injection, projection, lifting, recursive type. Straightforward use of the induction hypothesis, along the lines of the case of tensor.

Pattern matching. A little care is required to avoid getting confused by the type environments and the sets of distinctions. We detail the case in which the variable x belongs both to the type environment of the matched term, and to the type environment of the continuation. The other cases are simpler.

Suppose that

B ∪ B; (x:ℚ, Δ) ∪ (x:ℚ, Δ′); d ⊢ [w > p(y) ⇒ v] : ℙ

has been derived from

B′; x:ℚ, Δ′; δ′ ⊢ w : ℝ B′; x:ℚ, Δ′; δ′; ; y:𝕊 ⊢ p : ℝ B; y:𝕊, x:ℚ, Δ; δ ⊢ v:ℙ

where

d = (δ \ y) ∪ δ′ ∪ {{β} × (B′ ∪ (Δ′, x:ℚ)) | (β, y) ∈ δ}

and

B′ ∩ {β | (β, y) ∈ δ} = ∅ .  (1)

With respect to the hypothesis of the Lemma, A = B ∪ B′ and x:ℚ, Γ = (x:ℚ, Δ) ∪ (x:ℚ, Δ′). Also remember that A′; Γ′; d′ ⊢ t:ℚ and

A′ ∩ {β | (β, x) ∈ d} = ∅ .  (2)

We want to show that B ∪ B′ ∪ A′; Δ ∪ Δ′ ∪ Γ′; \overline{d} ⊢ [w > p(y) ⇒ v][t/x] : ℙ where \overline{d} = (d \ x) ∪ d′ ∪ \{β × (A′, Γ′) | (β, x) ∈ d\}.

By the induction hypothesis we have:

B′ ∪ A′; Δ′ ∪ Γ′; d_{1} ⊢ w[t/x] : ℝ B′ ∪ A′; Δ′ ∪ Γ′; d_{1}; ; y:𝕊 ⊢ p[t/x] : ℝ

where

d_{1} = (δ′ \ x) ∪ d′ ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ δ′} .

We also have:

B ∪ A′; (y:𝕊, Δ) ∪ Γ′; d_{2} ⊢ v[t/x] : ℙ

where

d_{2} = (δ \ x) ∪ d′ ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ δ} .

We show now that (B′ ∪ A′) ∩ {γ | (γ, y) ∈ d_{2}} = ∅. For that, we rewrite the set {γ | (γ, y) ∈ d_{2}} can be rewritten as the union of the sets S_{i} defined as

\begin{matrix}S_{1} = \{γ | (γ, y) ∈ (δ \ x)\} S_{2} = \{γ | (γ, y) ∈ d′\} \\ S_{3} = \{γ | (γ, y) ∈ \{\{β\} × (A′ ∪ Γ′) | (β, x) ∈ δ\}\} . \end{matrix}

Now, B′ ∩ S_{1} = ∅ because of hypothesis (1), and A′ ∩ S_{1} = ∅ because of (2). This implies (A′ ∪ B′) ∩ S_{1} = ∅. The sets S_{2} and S_{3} are empty because y is a bound variable and without loss of generality we can suppose y ∉ Γ′.

Then, we can apply the pattern matching typing rule to obtain

B′ ∪ A′ ∪ B; Δ′ ∪ Γ′ ∪ Δ; d_{3} ⊢ [w[t/x] > p[t/x](y) ⇒ v[t/x]] : ℙ

where

d_{3} = (d_{2} \ y) ∪ d_{1} ∪ {{β} × (B′ ∪ A′ ∪ Δ′ ∪ Γ′) | (β, y) ∈ d_{2}} .

By definition of substitution [w[t/x] > p[t/x](y) ⇒ v[t/x]] = [w > p(y) ⇒ v][t/x]. It remains to prove that d_{3} = \overline{d}. With a lot of patience, we see that

\overline{d} = (d \ x) ∪ d′ ∪ \{\{β\} × (A′ ∪ Γ′) | (β, x) ∈ d\}
= (((δ \ y) ∪ δ′ ∪ {{β} × (B′ ∪ (Δ′, x:ℚ)) | (β, y) ∈ δ}) \ x) ∪ d′∪
{{β} × (A′ ∪ Γ′) | (β, x) ∈ (δ \ y)} ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ δ′}∪
{{β} × (A′ ∪ Γ′) | (β, x) ∈ {γ × (B′ ∪ (Δ′, x:ℚ)) | (γ, y) ∈ δ}}
= (δ \ y \ x) ∪ (δ′ \ x) ∪ {β × (B′ ∪ Δ′) | (β, y) ∈ δ} ∪ d′∪
{{β} × (A′ ∪ Γ′) | (β, x) ∈ (δ \ y)} ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ δ′}∪
{{β} × (A′ ∪ Γ′) | (β, y) ∈ δ}
= (δ \ y \ x) ∪ (δ′ \ x) ∪ d′∪
{{β} × (A′ ∪ Γ′) | (β, x) ∈ (δ \ y)} ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ δ′}∪
{{β} × (B′ ∪ Δ′ ∪ A′ ∪ Γ′) | (β, y) ∈ δ}

In the last expression, the set {{β} × (A′ ∪ Γ′) | (β, x) ∈ (δ \ y)} can be rewritten as {{β} × (A′ ∪ Γ′) | (β, x) ∈ (δ \ y)}. With more patience, we calculate:

d_{3} = (d_{2} \ y) ∪ d_{1} ∪ {{β} × (B′ ∪ A′ ∪ Δ′ ∪ Γ′) | (β, y) ∈ d_{2}}
= (((δ \ x) ∪ d′ ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ δ}) \ y) ∪ (δ′ \ x) ∪ d′∪
{{β} × (A′ ∪ Γ′) | (β, x) ∈ δ′}∪
{{β} × (B′ ∪ A′ ∪ Δ′ ∪ Γ′) | (β, y) ∈ (δ \ x)}∪
{{β} × (B′ ∪ A′ ∪ Δ′ ∪ Γ′) | (β, y) ∈ d′}
{{β} × (B′ ∪ A′ ∪ Δ′ ∪ Γ′) | (β, y) ∈ {γ × (A′ ∪ Γ′) | (γ, x) ∈ δ}}

As (d′ \ y) ⊆ d′, and since y is a bound variable an without loss of generality we can suppose y ∉ Γ′ (and in turn y ∉ d′), we have

d_{3} = (δ \ x \ y) ∪ (δ′ \ x) ∪ d′∪
{{β} × (A′ ∪ Γ′) | (β, x) ∈ δ} ∪ {{β} × (A′ ∪ Γ′) | (β, x) ∈ δ′}∪
{{β} × (B′ ∪ A′ ∪ Δ′ ∪ Γ′) | (β, y) ∈ (δ \ x)} .

We conclude that \overline{d} = d_{3} because they are union of the same subsets.

Typing rules for patterns follow along the same lines (they are easier). The induction is now complete. □

Proof of Theorem 2.4, page 11 By rule induction on the derivation of ℙ; s ⊢

t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → u.

Prefixing. Suppose that !ℙ; s ⊢ !t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{!x (x)} → t. Then s ⊢ !t : !ℙ and so by the typing rules, s ⊢ t : ℙ as wanted.

Process abstraction. Suppose that ℙ → ℚ; λy.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{u↦p (x)} → t′ with s; ; x:ℝ ⊢ u ↦ p : ℙ → ℚ. By typing of patterns, we have s ⊢ u : ℙ and s; ; x:ℝ ⊢ p : ℚ. The induction hypothesis then yields s ⊢ t′ : ℝ as wanted. Note that the substitution t[u/x] is wellformed because A; y:ℚ; A ⊢ t : ℙ follows from s ⊢ λy.t : ℙ → ℚ, for a bijection σ : s → A.

Process application. Suppose that ℚ; s ⊢ tu \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p (x)} → t′ has been derived from ℙ →

ℚ : s ⊢ t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{u↦p(x)} → t′ with s; ; x:ℝ ⊢ p(x) : ℚ. By the premise and the typing rules, we have s ⊢ t : ℙ → ℚ and s ⊢ u : ℙ, such that s; ; x:ℝ ⊢ u ↦ p : ℙ → ℚ. The induction hypothesis then yields s ⊢ t′ : ℝ as wanted.

New name abstraction. Suppose that δℙ; s ⊢ newα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.p[x′[α]/x] (x′)} → newα.t′ has

been derived from ℙ; s ∪^{.} \{a\} ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α] (x)} → t′[a/α] with s; ; x′:δℝ ⊢ newα.p[x′[α]/x] :

δℙ. By the typing rules, we get A, α:ℕ; ∅; A, d ⊢ t : ℙ, for σ : s + {a} → A + {α}. This implies s ∪^{.} {a} ⊢ t[a/α] : ℙ. Again, by typing rules we get A, α:ℕ; ∅; A, d; ; x:ℝ ⊢ p : ℙ and then s ∪^{.} {a}; ; x:ℝ ⊢ p[a/α] : ℙ. By the induction hypothesis we have s ∪^{.} {a} ⊢ t′[a/α] : ℝ. This implies that A, α:ℕ; ∅; A, α ⊢ t′ : ℝ and we get s ⊢ newα.t′ : δℝ by the typing rules, as wanted.

New name application. Suppose that ℙ; s ∪^{.} \{a\} ⊢ t[a] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α] (x)} → t′[a] has been

derived from δℙ; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.p[x′[α]/x] (x′)} → t′, with s ∪^{.} \{a\}; ; x:ℝ ⊢ p[a/α] : ℙ. By the

typing rules we get s ⊢ t : δℙ. Also, as the pattern is well-typed, A, α:ℕ; ∅; A, α; ; x:ℝ ⊢ p : ℙ must hold for σ : s + {a} → A + {α}. By the typing rules we get s; ; x′:δℝ ⊢ newα.p[x′[α]/x] : δℙ. By the induction hypothesis, s ⊢ t′ : δℝ, and by the typing rules we conclude s ∪^{.} {a} ⊢ t′[a] : ℝ.

Pattern matching. Suppose that ℚ; s ⊢ [t > p(y) ⇒ u] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q (x)} → u′ has been derived

from ℙ; s ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(y)} → t′ and ℚ; s ⊢ u[t′/y] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → u′ with s; ; y:𝕊 ⊢ p : ℙ and s; ; x:ℝ ⊢ q : ℚ.

By the induction hypothesis applied to the first premise, we get s ⊢ t′ : 𝕊. Thus, as A; x:ℝ; A ⊢ u : ℚ for σ : s → A, the substitution u[t′/x] is well-formed. By the induction hypothesis applied to the second premise, we get s ⊢ u′ : ℝ, as wanted.

The remaining cases are handled similarly. □

A.2 Proofs from Section 3

To prove that bisimilarity is a congruence relation we need some auxiliary lemmas and definitions.

Lemma A.1 If s ⊢ t ∼ u : ℙ, then for all s′ ⊇ s it holds s′ ⊢ t ∼ u : ℙ. Proof Suppose s ⊢ t ∼ u : ℙ and s′ ⊇ s. We want to show that s′ ⊢ t ∼ u : ℙ. For that let s′′ ⊇ s′ and suppose s′′ ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → t′. As s ⊢ t ∼ u : ℙ and s′′ ⊇ s, there exists a term u′ such that s′′ ⊢ u \begin{matrix}− \\ − \end{matrix}^{p} → u′ and s′′ ⊢ t′ ∼ u′, as required. The symmetric case is handled similarly. □

Lemma A.2 Bisimilarity is an equivalence relation. Proof It is easy to see that bisimilarity is reflexive and symmetric. For transitivity, suppose s ⊢ t ∼ u : ℙ and s ⊢ u ∼ v : ℙ. We want to show that s ⊢ t ∼ v : ℙ. Let s′ ⊇ s and suppose s′ ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → t′. As s ⊢ t ∼ u : ℙ, there exists a term u′ such that s′ ⊢ u −^{t} → u′ and s′ ⊢ t′ ∼ u′ : ℙ. In turn, as s ⊢ u ∼ v : ℙ, there exists a term v′ such that s′ ⊢ v −^{t} → v′ and s′ ⊢ u′ ∼ v′ : ℙ. The result follows by coinduction. □

Definition A.3 (Closure) A (A; Γ; d)-closure is a triple (s, ρ, [u⃗/x⃗]), where

1. s is a set of names;

2. ρ : A → s is a map such that ρ(α) ≠ ρ(β) whenever (α, β) ∈ d, and ρ(α) ∉ n(u_{i}) whenever (α, u_{i}) ∈ d (that is, ρ substitutes name constants in s for name variables in A and respects distinctions);

3. [u⃗/x⃗] is a substitution assigning closed terms to the process variables in Γ such that s ⊢ u_{i} : Γ(x_{i}) for all i.

Closures are ranged over by Ξ. Given a type judgement A; Γ; d ⊢ t : ℙ and a (A; Γ; d)- closure Ξ = (s, ρ, [u⃗/x⃗]), we write t[Ξ] for the term ρt[u⃗/x⃗] and s_{Ξ} for s. Remark that s ⊢ ρt[u⃗/x⃗] : ℙ is a valid type judgement.

Definition A.4 (Open extension) If R relates closed terms, we write R^{∘} for its open extension, relating A; Γ; d ⊢ t : ℙ and A; Γ; d ⊢ u : ℙ if s_{Ξ} ⊢ t[Ξ] R u[Ξ] : ℙ holds for all (A; Γ; d)-closures Ξ.

We write R_{c} for the restriction of a type-respecting relation to closed terms. For a type-respecting relation R we write R also for the relation induced on actions, given inductively by

\frac{A; Γ; d; ; x:ℝ ⊢ p R q : ℙ}{A′; Γ′; d′; ; x:ℝ ⊢ p R q : ℙ} \begin{matrix}A ⊆ A′ \\ Γ ⊆ Γ′ \\ d ⊆ d′ \end{matrix}  \overline{E; ; x:ℝ ⊢ !x R !x : !ℝ}

\frac{A; Γ; d; ; x:ℝ ⊢ p R q : ℙ α ∈ A}{A; Γ; d; ; x:ℝ ⊢ α · p R α · q : ℕ ⊗ ℙ}  \frac{E; ; x:ℝ ⊢ p R q : ℙ_{j} j ∈ I}{E; ; x:ℝ ⊢ j:p R j:q : Σ_{i∈I}ℙ_{i}}

\frac{A; Γ; d; ; x:ℝ ⊢ p R q : ℙ α ∈ A}{A; Γ; d; ; x:ℝ ⊢ α ↦ p R α ↦ q : ℙ}  \frac{A; Γ; d ⊢ u R v : ℙ A; Γ; d; ; x:ℝ ⊢ p R q : ℚ}{A; Γ; d; ; x:ℝ ⊢ u ↦ p R v ↦ q : ℙ}

\frac{α : ℕ, A; Γ; d; ; x:ℝ ⊢ p R q : ℙ}{A; Γ; (d \ α); ; x′:δℝ ⊢ newα.p[x′[α]/x] R newα.q[x′[α]/x] : δℙ}

The open extension of ∼ is closed under weakening:

Lemma A.5 If A; Γ; d ⊢ t ∼^{∘} u : ℙ, then for all A′ ⊇ A, Γ′ ⊇ Γ, d′ ⊇ d we have A′; Γ′; d′ ⊢ t ∼^{∘} u : ℙ. Proof Follows from the definition of open extension and from Lemma A.1. □

Some terminology: a type respecting relation is said operator respecting if it is preserved by all the operators of the language. A congruence is an operator respecting relation that is also an equivalence.

Following Howe, we define an auxiliary relation, called the precongruence candidate, that, by construction, contains ∼^{∘} and is operator preserving. In what follows, we omit the ℕ type in the environment of name variables, and we occasionally use E as a concise abbreviation for a typing environment A; Γ; d. Also, when no ambiguity arises, we use commas to denote the disjoint union of sets.

Definition A.6 (The precongruence candidate) The precongruence candidate, ˆ∼, is the smallest type-respecting relation closed under the rules reported in Figure 1.

We need several technical lemmas. The lemma below is fundamental to show that in a derivation of s ⊢ newα.t ˆ∼_{c} u : δℙ the choice of the name a used to derive s ∪^{.} {a} ⊢ t[a/α] ˆ∼_{c} v : ℙ is irrelevant, as far as it is fresh.

Lemma A.7 If there is a derivation of A, α; Γ; d, ({α} × (A ∪ Γ)) ⊢ t ˆ∼ u : ℙ, then there is a derivation of the same height of A, β; Γ; d, ({β} × (A, Γ)) ⊢ t[β/α] ˆ∼ u[β/α] : ℙ.

We then prove that the precongruence candidate is closed under substitutions.

Lemma A.8

1. if A; Γ, x:ℚ; d ⊢ u ˆ∼ u′ : ℙ and A′; Γ′; d′ ⊢ t ˆ∼ t′ : ℚ with A′ ∩ {γ | (γ, x) ∈ d} = ∅, then A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ u[t/x] ˆ∼ u′[t′/x] : ℙ, where \overline{d} = (d \ x) ∪ d′ ∪ \{\{β\} × (A′, Γ′) | (β, x) ∈ d};

2. if A, α; Γ; d ⊢ u ˆ∼ u′ : ℙ, and N = {γ | (α, γ) ∈ d}, then for all name variables

β ∈ (A \ N) it holds A; Γ; d[β/α] ⊢ u[β/α] ˆ∼ u′[β/α] : ℙ. Proof Both parts are proved by induction on the depth of the derivation respectively of A; Γ, x:ℙ; d ⊢ u ˆ∼ u′ : ℙ and A, α; Γ; d ⊢ u ˆ∼ u′ : ℙ.

To illustrate the proof, we focus on part 1, and we detail the case when the last rule of the derivation is new-name abstraction. Suppose that the conclusion of the derivation is A; Γ, x:ℚ; d ⊢ newα.u ˆ∼ u′ : δℙ. This must have been derived from A, β; Γ, x:ℚ; d, ({β} × (A ∪ (Γ, x:ℚ))) ⊢ u[β/α] ˆ∼ v[β/α] : ℙ and A; Γ, x:ℚ; d ⊢ newα.v ∼^{∘} u′ : δℙ for some term v and for some fresh name β. As α is bound in newα.u, we assume without loss of generality that α ∉ A′. More interestingly, as a consequence of Lemma A.7, we can also

\frac{A; Γ; d ⊢ t ˆ∼ w : ℙ}{A′; Γ′; d′ ⊢ t ˆ∼ w : ℙ} \begin{matrix}A′ ⊇ A \\ Γ′ ⊇ Γ \\ d′ ⊇ d \end{matrix} \frac{E ⊢ t ˆ∼ w : ℙ_{j}[μP⃗ .ℙ⃗/P⃗]}{E ⊢ t ˆ∼ w : μ_{j}P : ℙ⃗} \frac{E ⊢ 0 ∼^{∘} w : ℙ}{E ⊢ 0 ˆ∼ w : ℙ} \frac{E ⊢ x ∼^{∘} w : ℙ}{E ⊢ x ˆ∼ w : ℙ}

\frac{E ⊢ t ˆ∼ t′ : ℙ E ⊢ !t′ ∼^{∘} w : !ℙ}{E ⊢ !t ˆ∼ w : !ℙ}  \frac{A; Γ, x:ℙ; d ⊢ t ˆ∼ t′ : ℙ A; Γ; d ⊢ recx.t′ ∼^{∘} w : ℙ}{A; Γ; d ⊢ recx.t ˆ∼ w : ℙ}

\frac{E ⊢ t ˆ∼ t′ : ℙ E ⊢ n · t′ ∼^{∘} w : ℕ ⊗ ℙ}{E ⊢ n · t ˆ∼ w : ℕ ⊗ ℙ}  \frac{E ⊢ t ˆ∼ t′ : ℕ ⊗ ℙ E ⊢ π_{n}t′ ∼^{∘} w : ℙ}{E ⊢ π_{n}t ˆ∼ w : ℙ}

\frac{A; Γ, x:ℙ; d ⊢ t ˆ∼ t′ : ℚ A; Γ; d ⊢ λx.t′ ∼^{∘} w : ℙ → ℚ}{A; Γ; d ⊢ λx.t ˆ∼ w : ℙ → ℚ}

\frac{E ⊢ t ˆ∼ t′ : ℙ → ℚ E ⊢ u ˆ∼ u′ : ℙ E ⊢ t′u′ ∼^{∘} w : ℙ}{E ⊢ tu ˆ∼ w : ℙ}

\frac{A, α; Γ; d ⊢ t ˆ∼ t′ : ℙ A; Γ; d ⊢ λα.t′ ∼^{∘} w : ℕ → ℙ}{A; Γ; d ⊢ λα.t ˆ∼ w : ℕ → ℙ} \frac{E ⊢ t ˆ∼ t′ : ℕ → ℙ E ⊢ t′α ∼^{∘} w : ℙ}{E ⊢ tα ˆ∼ w : ℙ}

\frac{A, β; Γ; d, (\{β\} × (A, Γ)) ⊢ t[β/α] ˆ∼ t′[β/α] : ℙ A; Γ; d ⊢ newα.t′ ∼^{∘} w : δℙ}{A; Γ; d ⊢ newα.t ˆ∼ w : δℙ}

\frac{A; Γ; d ⊢ t ˆ∼ t′ : δℙ A, α; Γ; d ∪ (\{α\} × (A, Γ)) ⊢ t′[α] ∼^{∘} w : ℙ}{A, α; Γ; d ∪ (\{α\} × (A, Γ)) ⊢ t[α] ˆ∼ w : ℙ}

\frac{E ⊢ t ˆ∼ t′ : ℙ_{i} E ⊢ i:t′ ∼^{∘} w : Σ_{i}ℙ_{i}}{E ⊢ i:t ˆ∼ w : Σ_{i}ℙ_{i}}  \frac{E ⊢ t ˆ∼ t′ : Σ_{i∈I}ℙ_{i} E ⊢ π_{i}t′ ∼^{∘} w : ℙ_{i}}{E ⊢ π_{i}t ˆ∼ w : ℙ_{i}}

\frac{∀i E ⊢ t_{i} ˆ∼ t′_{i} : ℙ E ⊢ Σ_{i∈I}t′_{i} ∼^{∘} w : ℙ}{E ⊢ Σ_{i∈I}t_{i} ˆ∼ w : ℙ} \frac{A, α; Γ; d ⊢ t ˆ∼ t′ : ℙ A; Γ; d ⊢ Σ_{α∈ℕ}t′ ∼^{∘} w : ℙ}{A; Γ; d ⊢ Σ_{α∈ℕ}t ˆ∼ w : ℙ}

\frac{A′; Γ′; d′ ⊢ t ˆ∼ t′ : ℙ A; Γ, x:ℝ; d ⊢ u ˆ∼ u′ : ℚ A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ [t′ > p(x) ⇒ u′] ∼^{∘} w : ℚ}{A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ [t > p(x) ⇒ u] ˆ∼ w : ℚ}

In the last rule, \overline{d} stands for (d \ x) ∪ d′ ∪ \{\{α\} × (A′, Γ′) | (α, x) ∈ d\}. Also, the pattern p is supposed to be well-type, with resumption type ℝ. In the rule for new-name abstraction, we assume A, α; Γ; d′ ⊢ t : ℙ, with d = d′ \ α. In particular, this implies that α ∉ A.

Figure 1: The precongruence candidate suppose β ∉ A′. By the induction hypothesis we get (A, β)∪A′; Γ∪Γ′; d_{1} ⊢ u[β/α][t/x] ˆ∼ v[β/α][t′/x] : ℙ, where d_{1} = ((d, ({β} × (A ∪ (Γ, x:ℚ)))) \ x) ∪ d′ ∪ {{α} × (A′ ∪ Γ′) | (α, x) ∈ (d, (β × (A ∪ (Γ, x:ℚ))))}. The set of distinctions d′ can be rearranged so that it is of the form d_{1} = d_{2}, ({β} × (A ∪ A′ ∪ Γ ∪ Γ′)) for a set of distinctions d_{2}. Then we have (A ∪ A′), β; Γ ∪ Γ′; d_{1} ⊢ u[t/x][β/α] ˆ∼ v[t′/x][β/α] : ℙ. Since ∼^{∘} is defined as the open extension of ∼, and because of Lemma A.5, it holds A ∪ A′; Γ ∪ Γ′; d_{2} ⊢ (newα.v)[t/x] ∼^{∘} u′[t′/x] : δℙ and hence A; Γ; \overline{d} ⊢ newα.(v[t/x]) ∼^{∘} u′[t′/x] : δℙ, where \overline{d} = d_{2} \ α. We conclude A ∪ A′; Γ ∪ Γ′; \overline{d} ⊢ (newα.u)[t/x] ˆ∼ u′[t′/x] : δℙ. □

Part 2 of Lemma A.8 (closure under name substitutions) allows us to prove some basic properties of the precongruence candidate. The proof of these properties involves the closure under name substitution to deal with the rule of new-name abstraction: we will detail one case to illustrate the proof strategy.

Lemma A.9 Some properties of the precongruence candidate:

1. ˆ∼ is reflexive;

2. ˆ∼ is operator respecting;

3. ∼^{∘} ⊆ ˆ∼;

4. if E ⊢ t ˆ∼ u : ℙ and E ⊢ u ∼^{∘} v : ℙ then E ⊢ t ˆ∼ v : ℙ. Proof

1. follows from reflexivity of ∼^{∘} (by induction on the structure of the term t).

2. follows from the definition of ˆ∼, from the definition of operator respecting relation, and from reflexivity of ∼^{∘}. The case of new-name abstraction deserves to be detailed. Suppose A, α; Γ; d ⊢ t ˆ∼ u : ℙ. We want to conclude that A; Γ; (d \ α) ⊢ newα.t ˆ∼ newα.u : δℙ. As A, α; Γ; d ⊢ t ˆ∼ u : ℙ, by Lemma A.5 we have A, α, β; Γ; d, ({β} × (A ∪ Γ)) ⊢ t ˆ∼ u : ℙ. Then, by Lemma A.8 we have A, β; Γ; (d, ({β} × (A ∪ Γ)))[β/α] ⊢ t[β/α] ˆ∼ u[β/α] : ℙ. Now, (d ∪ ({β} × (A ∪ Γ)))[β/α] = (d \ α) ∪ ({β} × (A ∪ Γ)). As ∼^{∘} is reflexive, A; Γ; (d \ α) ⊢ newα.u ∼^{∘} newα.u : δℙ. Hence A; Γ; (d\α) ⊢ newα.t ˆ∼ newα.u : δℙ follows from the definition of ˆ∼.

3. follows from the reflexivity of ˆ∼ and the definition of ˆ∼.

4. induction on the derivation of E ⊢ t ˆ∼ u, using the fact that ∼ (and ∼^{∘}) is transitive. □

Lemma A.10 If s ⊢ t ˆ∼_{c} u : ℙ, then for all s′ ⊇ s we have s′ ⊢ t ˆ∼_{c} u : ℙ. Proof Consequence of the weakening rule in the definition of the precongruence candidate. □

Proposition A.11 Since ∼ is an equivalence relation, the transitive closure ˆ∼^{∗} of ˆ∼ is symmetric, and therefore so is ˆ∼_{c}^{∗}.

In the next lemma, we heavily rely on the correspondence between the type judgement s ⊢ t : ℙ and the judgement A; ∅; A ⊢ σt : ℙ for A a set of fresh name variables and σ : s → A a bijection between s and A.

Lemma A.12 ˆ∼_{c} is a simulation. Proof We prove that ˆ∼_{c} is a simulation by induction on the derivations of the operational semantics. Actually, we prove a stronger property:

if s ⊢ t ˆ∼_{c} u : ℙ and s′ ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → t′ for some s′ ⊇ s, then for all p′ with
s′; ; x:ℝ ⊢ p ˆ∼ p′ : ℙ, there exists a term u′ such that s′ ⊢ u \begin{matrix}− \\ − \end{matrix}^{p′} → u′ and
s′ ⊢ t′ ˆ∼_{c} u′.

Since ˆ∼ is reflexive, s′; ; x:ℝ ⊢ p ˆ∼ p : ℙ for all actions, and so ˆ∼_{c} is a simulation if the above holds. This stronger induction hypothesis is needed in the case of process application.

Most of the cases are proved in the same way. Consider E ⊢ t : ℙ and s ⊢ C(t) ∼_{c} u : ℚ for some term constructor C, possibly involving binding. From the definition of ˆ∼ we obtain the existence of a term v with E ⊢ t ˆ∼ v : ℙ and s ⊢ C(v) ∼ u : ℚ. Under the

assumption s′ ⊢ C(t) \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ with s′ ⊇ s and with q any action such that s′; ; x:ℝ ⊢

p ∼ q : ℚ, we show that there is a transition s′ ⊢ C(v) \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ. Having showed this, in all cases we conclude as follows: since s ⊢ C(v) ∼ u : ℚ, there

is a transition s′ ⊢ u \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → u′ with s′ ⊢ v′ ∼ u′. Hence s′ ⊢ t′ ˆ∼_{c} u′ : ℝ follows from s′ ⊢ t′ ˆ∼_{c} v′ : ℝ by Lemma A.9.4. To avoid repetition, this latter part will be left out below.

Cases sum, process application, and pattern matching differ from the above pattern because the constructor C takes more than one term: apart from this, their proof follows the aforementioned pattern.

Prototypical action (prefixing). Suppose s ⊢ !t ˆ∼_{c} u : !ℙ, and s′ ⊢ !t \begin{matrix}− \\ − \\ − \end{matrix}^{!(x)} → t for s′ ⊇ s. Since s ⊢ !t ˆ∼_{c} u : ℙ there exists a term v such that s ⊢ t ˆ∼_{c} v : ℙ and s ⊢ !v ∼ u : !ℙ. By Corollary A.10 we have s′ ⊢ t ˆ∼_{c} v : ℙ. We get a transition s′ ⊢ !v \begin{matrix}− \\ − \\ − \end{matrix}^{!(x)} → v from the operational rules.

Tensor. Suppose s ⊢ a · t ˆ∼_{c} u : ℕ ⊗ ℙ and that s′ ⊢ a · t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{a·p(x)} → t′ because

s′ ⊢ t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ for some s′ ⊇ s. Let q be any action such that s′; ; x:ℝ ⊢ p ˆ∼ q : ℙ. This implies s′; ; x:ℝ ⊢ a · p ˆ∼ a · q : ℕ ⊗ ℙ. Since s ⊢ a · t ˆ∼_{c} u : ℕ ⊗ ℙ there exists a term v such that s ⊢ t ˆ∼_{c} v : ℙ and s ⊢ a · v ∼ u : ℕ ⊗ ℙ. By the induction hypothesis we get

s′ ⊢ v \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence s′ ⊢ a · v \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{a·q(x)} → v′.

Projection over names. Suppose s ⊢ π_{a}t ˆ∼_{c} u : ℙ and that s′ ⊢ π_{a}t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ because

s′ ⊢ t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{a·p(x)} → t′ for some s′ ⊇ s. Let q be any action such that s′; ; x:ℝ ⊢ p ˆ∼ q : ℙ. This implies s′; ; x:ℝ ⊢ a · p ˆ∼ a · q : ℕ ⊗ ℙ. Since s ⊢ π_{a}t ˆ∼_{c} u : ℙ there exists a term v such that s ⊢ t ˆ∼_{c} v : ℕ ⊗ ℙ and s ⊢ π_{a}v ∼ u : ℙ. By the induction hypothesis we get

s′ ⊢ v \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{a·q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence s′ ⊢ π_{a}v \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′.

Sum. Suppose s ⊢ Σ_{i∈I}t_{i} ˆ∼_{c} u : ℙ and that s′ ⊢ Σ_{i∈I}t_{i} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ is derived from

s′ ⊢ t_{i} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′, for some s′ ⊇ s. Let q be any action such that s′; ; x:ℝ ⊢ p ˆ∼ q : ℙ. Since s ⊢ Σ_{i∈I}t_{i} ˆ∼_{c} u : ℙ, there is a family of terms {v_{i}}_{i∈I} such that s ⊢ t_{i} ˆ∼_{c} v_{i} : ℙ for each

i ∈ I, and s ⊢ Σ_{i∈I}v_{i} ∼ u : ℙ. By the induction hypothesis we get s′ ⊢ v_{i} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′ with

s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence s′ ⊢ Σ_{i∈I}v_{i} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′.

Sum over names. Suppose s ⊢ Σ_{α∈ℕ}t ˆ∼_{c} u : ℙ and that s′ ⊢ Σ_{α∈ℕ}t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ is derived

from s′ ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ where a ∈ s′, for some s′ ⊇ s. Let q be any action such that s′; ; x:ℝ ⊢ p ˆ∼ q : ℙ. Since s ⊢ Σ_{α∈ℕ}t ˆ∼_{c} u : ℙ, there exists a term v such that A, α; ∅; A ⊢ σt ˆ∼ σv : ℙ for a bijection σ : s → A, and s ⊢ Σ_{α∈ℕ}v ∼ u : ℙ. Using weakening and Lemma A.8.2, we obtain s′ ⊢ t[a/α] ˆ∼_{c} v[a/α]. By the induction hypothesis we get

s′ ⊢ v[a/α] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence s′ ⊢ Σ_{α∈ℕ}v \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′.

Recursion. Suppose s ⊢ recy.t ˆ∼_{c} u : ℙ and that s′ ⊢ recy.t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ is derived

from s′ ⊢ t[recy.t/y] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′. Let q be any action with s′; ; x:ℝ ⊢ p ˆ∼ q : ℙ. Since s ⊢ recy.t ˆ∼_{c} u : ℙ there exists a term v such that A; y:ℙ; A ⊢ σt ˆ∼ σv : ℚ for a bijection σ : s → A, and s ⊢ recy.v ∼ u : ℙ → ℚ. As ˆ∼ is operator respecting, we have s ⊢ recy.t ˆ∼_{c} recy.v : ℙ, and using Lemma A.8.1 we obtain s ⊢ t[recy.t/y] ˆ∼_{c} v[recy.v/y] : ℙ.

By the induction hypothesis we get s′ ⊢ v[recy.v/y] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and

hence also s′ ⊢ recy.v \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′.

Process abstraction. Suppose s ⊢ λy.t ˆ∼_{c} u : ℙ → ℚ and that s′ ⊢ λy.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{w_{1}↦p(x)} → t′ is

derived from s′ ⊢ t[w_{1}/y] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′. Let w_{2} ↦ q be any action with s′; ; x:ℝ ⊢ w_{1} ↦ p ˆ∼ w_{2} ↦ q : ℙ → ℚ. This implies s′ ⊢ w_{1} ˆ∼_{c} w_{2} : ℙ. Since s ⊢ λy.t ˆ∼_{c} u : ℙ → ℚ there exists a term v such that A; y:ℙ; A ⊢ σt ˆ∼ σv : ℚ for σ : s → A, and s ⊢ λy.v ∼ u : ℙ → ℚ. Using weakening and Lemma A.8.1 we have s′ ⊢ t[w_{1}/y] ˆ∼_{c} v[w_{2}/y] : ℚ. By the

induction hypothesis we get s′ ⊢ v[w_{2}/y] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence also

s′ ⊢ λy.v \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{w_{2}↦q(x)} → v′.

Process application. Suppose s ⊢ t_{1}t_{2} ˆ∼_{c} u : ℚ and that s′ ⊢ t_{1}t_{2} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ is derived

from s′ ⊢ t_{1} \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{t_{2}↦p(x)} → t′ for some s′ ⊇ s. Let q be any action such that s′; ; x:ℝ ⊢ p ˆ∼ q : ℚ. Since s ⊢ t_{1}t_{2} ˆ∼_{c} u : ℚ there exists terms v_{1} and v_{2} such that s ⊢ t_{1} ˆ∼_{c} v_{1} : ℙ → ℚ and s ⊢ t_{2} ˆ∼_{c} v_{2} : ℙ and s ⊢ v_{1}v_{2} ∼ u : ℚ. By the induction hypothesis we get

s′ ⊢ v_{1} \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{v_{2}↦q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence s′ ⊢ v_{1}v_{2} \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{v_{2}↦q(x)} → v′. Notice

how the stronger induction hypothesis allows us to choose the label v_{2} ↦ q rather than u_{2} ↦ p, so that we could obtain a transition from v_{1}v_{2}.

Name abstraction. Suppose s ⊢ λα.t ˆ∼_{c} u : ℕ → ℚ and that s′ ⊢ λα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{a↦p(x)} → t′ is

derived from s′ ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′. Let a ↦ q be any action with s′; ; x:ℝ ⊢ a ↦ p ˆ∼ a ↦ q : ℕ → ℚ. Since s ⊢ λα.t ˆ∼_{c} u : ℕ → ℚ there exists a term v such that A, α; ∅; A ⊢ σt ˆ∼ σv : ℚ for a bijection σ : s → A, and s ⊢ λα.v ∼ u : ℕ → ℚ. Using weakening and Lemma A.8.2 we have s′ ⊢ t[a/α] ˆ∼_{c} v[a/α] : ℚ. By the induction hypothesis we get

s′ ⊢ v[a/α] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence also s′ ⊢ λα.v \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{a↦q(x)} → v′.

Name application. Suppose s ⊢ ta ˆ∼_{c} u : ℚ and that s′ ⊢ ta \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ is derived from

s′ ⊢ t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{a↦p(x)} → t′ for some s′ ⊇ s. Let q be any action such that s′; ; x:ℝ ⊢ p ˆ∼ q : ℚ. Since s ⊢ ta ˆ∼_{c} u : ℚ there exists a term v such that s ⊢ t ˆ∼_{c} v : ℕ → ℚ and s ⊢ va ∼ u : ℚ. By the induction hypothesis we get s′ ⊢ v \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{a↦q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence

s′ ⊢ va \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{a↦q(x)} → v′.

Injection. Suppose s ⊢ i:t ˆ∼_{c} u : Σ_{i∈I}ℙ_{i} and that s′ ⊢ i:t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{i:p(x)} → t′ because s′ ⊢

t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ for some s′ ⊇ s. Let q be any action such that s′; ; x:ℝ ⊢ p ˆ∼ q : ℙ_{i}. This implies s′; ; x:ℝ ⊢ i:p ˆ∼ i:q : Σ_{i∈I}ℙ_{i}. Since s ⊢ i:t ˆ∼_{c} u : Σ_{i∈i}ℙ_{i} there exists a term v such that s ⊢ t ˆ∼_{c} v : ℙ_{i} and s ⊢ i:v ∼ u : Σ_{i∈I}ℙ_{i}. By the induction hypothesis we get

s′ ⊢ v \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence s′ ⊢ a · v \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{i:q(x)} → v′.

Projection. Suppose s ⊢ π_{i}t ˆ∼_{c} u : ℙ_{i} and that s′ ⊢ π_{i}t \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′ because s′ ⊢

t \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{i:p(x)} → t′ for some s′ ⊇ s. Let q be any action such that s′; ; x:ℝ ⊢ p ˆ∼ q : ℙ_{i}. This implies s′; ; x:ℝ ⊢ i:p ˆ∼ i:q : Σ_{i∈I}ℙ_{i}. Since s ⊢ π_{i}t ˆ∼_{c} u : ℙ_{i} there exists a term v such that s ⊢ t ˆ∼_{c} v : Σ_{i∈I}ℙ_{i} and s ⊢ π_{i}v ∼ u : ℙ_{i}. By the induction hypothesis we get

s′ ⊢ v \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{i:q(x)} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : ℝ, and hence s′ ⊢ π_{i}v \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′.

New-name abstraction. Suppose s ⊢ newα.t ˆ∼_{c} u : δℙ. Suppose also that s′ ⊢

newα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.p[x′[α]/x](x′)} → newα.t′ is derived from s′ ∪^{.} \{a\} ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α](x)} → t′[a/α]

for some s′ ⊇ s. Let q be any action such that A′, α; ∅; A′, d; ; x : ℝ ⊢ σp ˆ∼ σq : ℙ for a bijection σ : s′ → A′. This implies s′ ∪^{.} {a}; ; x:ℝ ⊢ p[a/α] ˆ∼ q[a/α] : ℙ and s′; ; x′:δℝ ⊢ newα.p ˆ∼ newα.q : δℙ. Since s ⊢ newα.t ˆ∼_{c} u : δℙ there exists a

term v such that s ∪^{.} {a} ⊢ t[a/α] ˆ∼_{c} v[a/α] : ℙ and s ⊢ newα.v ∼ u : δℙ. As

s′ ∪ \{a\} ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α](x)} → t′[a/α], by the induction hypothesis we have s′ ∪ \{a\} ⊢

v[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{q[a/α](x)} → v′[a/α] with s′ ∪^{.} \{a\} ⊢ t′[a/α] ˆ∼_{c} v′[a/α] : ℙ. By the operational rules

s′ ⊢ newα.v \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.q[x′[α]/x](x′)} → newα.v′. As ∼ is reflexive, we can deduce s′ ⊢ newα.t′ ˆ∼_{c}

newα.v′ : δℙ from s′ ∪^{.} {a} ⊢ t′[a/α] ˆ∼_{c} v′[a/α] : ℙ, as desired.

New name application. Suppose s ∪^{.} {a} ⊢ t[a] ˆ∼_{c} u : ℙ. Suppose also that s′ ∪^{.}

\{a\} ⊢ t[a] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α](x)} → t′[a] is derived from s′ ⊢ t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.p[x′[α]/x](x′)} → t′, for some s′ ⊇ s.

Let q be any action such that A′, α; ∅; A′, d; ; x : ℝ ⊢ σp ˆ∼ σq : ℙ for a bijection σ : s′ → A′. This implies s′; ; x′ : δℝ ⊢ newα.p[x′[α]/x] ˆ∼ newα.q[x′[α]/x] : δℙ, and also

s′ ∪^{.} {a}; ; x : ℝ ⊢ p[a/α] ˆ∼ q[a/α] : ℙ. Since s ∪^{.} {a} ⊢ t[a] ˆ∼_{c} u : ℙ there exists

a term v such that s ⊢ t ˆ∼ v : δℙ and s ∪^{.} {a} ⊢ v[a] ∼ u : ℙ. By the induction

hypothesis we have s′ ⊢ v \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.q[x′[α]/x]} → v′ with s′ ⊢ t′ ˆ∼_{c} v′ : δℝ. As ˆ∼ is operator

respecting (Lemma A.9.2), we obtain s′ ∪^{.} {a} ⊢ t′[a] ˆ∼_{c} v′[a] : ℙ. We get a transition

s′ ∪^{.} \{a\} ⊢ v[a] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{q[a/α]} → v′[a] by the operational rules.

Pattern matching. Suppose s ⊢ [t_{1} > p(x) ⇒ t_{2}] ˆ∼_{c} u : ℚ and that s′ ⊢ [t_{1} > p(x) ⇒

t_{2}] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{p′(x′)} → t_{3} is derived from s′ ⊢ t_{1} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{p(x)} → t′_{1} and s′ ⊢ t_{2}[t′_{1}/x] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{p′(x′)} → t_{3}, for some s′ ⊇ s.

Let q and q′ be actions such that s′; ; x:ℝ ⊢ p ˆ∼ q : ℙ and s′; ; x′:ℝ′ ⊢ p′ ˆ∼_{c} q′ : ℚ. Since s ⊢ [t_{1} > p(x) ⇒ t_{2}] ˆ∼_{c} u : ℚ, there exist two terms v_{1} and v_{2} such that s_{1} ⊢ t_{1} ˆ∼_{c} v_{1} : ℙ and A; x:ℝ; A, d ⊢ σt_{2} ˆ∼_{c} σv_{2} : ℚ for a bijection σ : s_{2} → A, where s_{1} ∪ s_{2} = s and s′ ∩ σ({α | (α, x) ∈ d}) = ∅. It also holds s ⊢ [v_{1} > p(x) ⇒ v_{2}] ∼ u : ℚ. By the

induction hypothesis we have s′ ⊢ v_{1} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q(x)} → v′_{1} with s′ ⊢ t′_{1} ˆ∼_{c} v′_{1} : ℝ. By weakening and by Lemma A.8.1 we get s′ ⊢ t_{2}[t′_{1}/x] ˆ∼_{c} v_{2}[v′_{1}/x] : ℚ. Applying the induction

hypothesis in this case yields s′ ⊢ v_{2}[v′_{1}/x] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q′(x′)} → v_{3} with s′ ⊢ t_{3} ˆ∼_{c} v_{3}, and hence

s′ ⊢ [v_{1} > p(x) ⇒ v_{2}] \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{q′(x′)} → v_{3}.

The induction is complete. □

At last, we prove that bisimilarity ∼ is a congruence. Proof of Theorem 3.2, page 12 As shown in Lemma A.12, ˆ∼_{c} is a simulation. Then ˆ∼_{c}^{∗} is a bisimulation by Property A.11, and so ˆ∼_{c}^{∗} ⊆ ∼. In particular ˆ∼_{c} ⊆ ∼. By Lemma A.9.1 and Lemma A.8, it follows that ˆ∼ ⊆ ∼^{∘}, and so by Lemma A.9.3, ˆ∼ = ∼^{∘}. Hence, ∼ is a congruence because it is an equivalence relation and by Lemma A.9.2 is operator respecting. □

A remark on the definition of the precongruence candidate: the more standard rule

\frac{A, α; Γ; d ⊢ t ˆ∼ t′ : ℙ A; Γ; (d \ α) ⊢ newα.t′ ∼^{∘} w : δℙ}{A; Γ; (d \ α) ⊢ newα.t ˆ∼ w : δℙ}

does not seem to capture the essence of new-name abstraction. In fact, this rule does not allow to prove Lemma A.12 (at least not in a handy way). Proof of Proposition 3.3, page 12 Let I be the identical type respecting relation over closed terms. In each postulated case s ⊢ lhs ∼ rhs : ℙ, the relation S = { (s′ ⊢ lhs : ℙ, s′ ⊢ rhs : ℙ) | s′ ⊇ s } ∪ I is a bisimulation. □

Proof of Lemma 3.5, page 12 Let

R = { (s ⊢ newα.t : δℙ, s ⊢ newα.u : δℙ) | s ∪^{.} {a} ⊢ t[a/α] ∼ u[a/α] : ℙ } .

We show that R is a bisimulation. Suppose s′ ⊢ newα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.p} → newα.t′ for some

s′ ⊇ s. This must have been derived from s′ ∪^{.} \{a\} ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α]} → t′[a/α] for some a.

By bisimulation, we have s′ ∪^{.} \{a\} ⊢ u[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α]} → u′[a/α] with s′ ∪^{.} \{a\} ⊢ t′[a/α] ∼

u′[a/α] : ℙ. By the operational rules, we have s′ ⊢ newα.u \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.p} → newα.u′, and by definition of R we conclude s ⊢ newα.t′ ∼ newα.u′ : δℙ. □

Proof of Proposition 3.6, page 12 Let

R = { (s ∪^{.} {a} ⊢ (newα.t)[a] : ℙ, s ∪^{.} {a} ⊢ t[a/α] : ℙ) |

A, α; ∅; A, d ⊢ t : ℙ for σ : s →_{bij} A } .

We show that R is a bisimulation. Consider s ∪^{.} {a} ⊢ (newα.t)[a] R t[a/α] : ℙ.

Suppose that s′ ∪^{.} \{a\} ⊢ (newα.t)[a] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α](x)} → (newα.t′)[a] for some s′ ⊇ s. This

must have been derived from s′ ⊢ newα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.α↦p[x′[α]/x](x′)} → newα.t′. In turn, this must

Actions: ℓ ::= \overline{n}m | \overline{n}(α) | nα | τ

\overline{\overline{n}m.P \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{n}m} →_{l} P}  \overline{n(α) \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{n(α)} →_{l} P}  \frac{P \begin{matrix}− \\ − \end{matrix}^{ℓ} →_{l} P′ α ∉ fv(ℓ)}{(να)P \begin{matrix}− \\ − \end{matrix}^{ℓ} →_{l} (να)P′}  \frac{P \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{n}α} →_{l} P′}{(να)P \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{n}(α)} →_{l} P′}

\frac{P \begin{matrix}− \\ − \end{matrix}^{ℓ} →_{l} P′}{P | Q \begin{matrix}− \\ − \end{matrix}^{ℓ} →_{l} P′ | Q}  \frac{P \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{n}m} →_{l} P′ Q \begin{matrix}− \\ − \\ − \end{matrix}^{nα} →_{l} Q′}{P | Q \begin{matrix}− \\ − \end{matrix}^{τ} →_{l} P′ | Q′[m/α]}  \frac{P \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{n}(β)} →_{l} P′ Q \begin{matrix}− \\ − \\ − \end{matrix}^{nα} →_{l} Q′}{P | Q \begin{matrix}− \\ − \end{matrix}^{τ} →_{l} (νβ)(P′ | Q′[β/α])}

Figure 2: π-calculus: the late labelled transition system

have derived from s′ ∪^{.} \{a\} ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α](x)} → t′[a/α]. So we have a matching transition, and s′ ∪^{.} {a} ⊢ (newα.t′)[a] R t′[a/α] : ℝ follows from the construction of R, where ℝ is the type of the resumption variable in p.

Suppose now that s′ ∪^{.} \{a\} ⊢ t[a/α] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α](x)} → t′[a/α] for some s′ ⊇ s. By the opera-

tional rules we get s′ ⊢ newα.t \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα.α↦p[x′[α]/x](x′)} → newα.t′. In turn, by the operational

rules we get s ∪^{.} \{a\} ⊢ (newα.t)[a] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{p[a/α](y)} → (newα.t′)[a]. So we have a matching transition, and s′ ∪^{.} {a} ⊢ (newα.t′)[a] R t′[a/α] : ℝ follows from the construction of R. □

Proof of Corollary 3.7, page 12 By weakening, s ∪^{.} {a} ⊢ newα.t ∼ newα.u : δℙ. By congruence, s ∪^{.} {a} ⊢ (newα.t)[a] ∼ new(α.u)[a] : ℙ. By Proposition 3.6, we have

s ∪^{.} {a} ⊢ (newα.t)[a/α] ∼ t[a/α] : ℙ and s ∪^{.} {a} ⊢ (newα.u)[a/α] ∼ u[a/α] : ℙ. The

result follows from transitivity of ∼. □

Proof of Corollary 3.8, page 12 By Proposition 3.5 s ⊢ newα.t ∼ newα.u : δℙ. The result follows by Corollary 3.7. □

A.3 Proofs from Section 4

We first introduce a basic up-to proof technique.

Definition A.13 (Bisimulation up to bisimilarity) A symmetric type respecting relation on closed terms, R, is a bisimulation up to bisimilarity if s ⊢ t R u : ℙ and s′ ⊢ t \begin{matrix}− \\ − \end{matrix}^{p} → t′ for s′ ⊇ s imply that there exists a term u′ such that s′ ⊢ u \begin{matrix}− \\ − \end{matrix}^{p} → u′ and s′ ⊢ t′ ∼R∼ u′ : ℙ.

Proposition A.14 If R is a bisimulation up to bisimilarity, then R ⊆ ∼. Proof Let S = {(s ⊢ t : ℙ, s ⊢ u : ℙ) | s ⊢ t ∼R∼ u : ℙ}. The relation S is a bisimulation (simple diagram chasing argument). □

For reference, the late labelled transition system is reported in Figure 2 (we omit the symmetric rules).

Definition A.15 (Late strong bisimilarity) Late strong bisimilarity is the largest symmetric relation, ∼_{l}, such that whenever P ∼_{l} Q,

1. P \begin{matrix}− \\ − \\ − \end{matrix}^{nβ} →_{l} P′ implies there is Q′ such that Q \begin{matrix}− \\ − \\ − \end{matrix}^{nβ} →_{l} Q′ and P′[m/α] ∼_{l} Q′[m/α] for

every m;

2. if ℓ is not an input action then P −^{ℓ} →_{l} P′ implies Q −^{ℓ} →_{l}∼_{l} Q′. It is well-known that late strong bisimilarity is preserved by all operators except

input prefix. In particular, both transitions and late strong bisimilarity are preserved by injective renaming. Lemma A.16 (Basic properties of ⟦−⟧)

1. fv(P) = fv(⟦P ⟧);

2. n(P) = n(⟦P ⟧);

3. ⟦P ⟧[a/α] = ⟦P [a/α]⟧. To prove Theorem 4.2, we introduce here a theorem stronger than Theorem 4.1.

Theorem A.17 Let P a closed π-calculus process. Then,

1. P \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{α}β} →_{l} P′ if and only if n(P) ⊢ ⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{out:a·b·!} → ⟦P′⟧;

2a. P \begin{matrix}− \\ − \\ − \end{matrix}^{αβ} →_{l} P′ implies n(P) ⊢ ⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{inp:a!} →∼ (λβ.⟦P′⟧);

2b. n(P) ⊢ ⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{inp:a!} → t implies P \begin{matrix}− \\ − \\ − \end{matrix}^{αβ} →_{l} P′ and t ∼ (λβ.⟦P′⟧);

3a. P \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{α}(β)} →_{l} P′ implies n(P) ⊢ ⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{bout:a!} →∼ (newβ.⟦P′⟧);

3b. n(P) ⊢ ⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{bout:a!} → t implies P \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{α}(β)} →_{l} P′ and t ∼ (newβ.⟦P′⟧);

4a. P \begin{matrix}− \\ − \end{matrix}^{τ} →_{l} P′ implies n(P) ⊢ ⟦P ⟧ \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} →∼ ⟦P′⟧;

4b. n(P) ⊢ ⟦P ⟧ \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} → t implies P \begin{matrix}− \\ − \end{matrix}^{τ} →_{l} P′ and t ∼ ⟦P′⟧

We introduce some notations useful in the proofs of the next two theorems:

• we write α⃗_{n} or simply α⃗ for the set {α_{1}, …, α_{n}} where the α_{i} are all distinct. We write newα⃗_{n}.t for newα_{1}. . . . .newα_{n}.t. Also δ^{n}ℙ stands for δ … δℙ where the δ is replicated n times;

• most of the substitutions we use in the next two theorems are bijections involving fresh name constants. So, whenever a is fresh for P, we write P [a/α] \begin{matrix}− \\ − \end{matrix}^{τ} → P′[a/α] as a shorthand for P [a/α] \begin{matrix}− \\ − \end{matrix}^{τ} → P′_{1} and P′ = P′_{1}[α/a]. Same with terms and transitions of new-HOPLA;

• we write ⟶ instead of ⟶_{l}. We prove separately the two implications of Theorem 4.2.

Theorem A.18 Let P and Q be two closed π-calculus processes. If P ∼_{l} Q then n(P, Q) ⊢ ⟦P ⟧ ∼ ⟦Q⟧ : ℙ. Proof We actually prove a stronger theorem:

Let P and Q be two π-calculus processes such that fv(P) = fv(Q) = α⃗_{n}.

1. If P ∼_{l} Q, then n(lhs,rhs) ⊢ newα⃗_{n}.⟦P ⟧ ∼ newα⃗_{n}.⟦Q⟧ : δ^{n}ℙ, and

2. if γ ∈ α⃗ and for all m it holds P [m/γ] ∼_{l} Q[m/γ], then n(lhs,rhs) ⊢

new(α⃗_{n} \ γ).λγ.⟦P ⟧ ∼ new(α⃗_{n} \ γ).λγ.⟦Q⟧ : δ^{n−1}(ℕ → ℙ).

Let

R = { (s ⊢ newα⃗_{n}.⟦P ⟧ : δ^{n}ℙ , s ⊢ newα⃗_{n}.⟦Q⟧ : δ^{n}ℙ) | P ∼_{l} Q and fv(P) = fv(Q) = α⃗ }
∪ { (s ⊢ newα⃗_{n}.λγ.⟦P ⟧ : δ^{n}(ℕ → ℙ) , s ⊢ newα⃗_{n}.λγ.⟦Q⟧ : δ^{n}(ℕ → ℙ)) |

∀m.P [m/γ] ∼_{l} Q[m/γ] and fv(P) = fv(Q) = α⃗ ∪^{.} {γ} }

where s ⊇ n(lhs,rhs). We prove that R is a bisimulation up to bisimulation; the result will follows from the soundness of the up-to bisimulation proof technique (Proposition A.14).

First consider

s ⊢ newα⃗_{n}.⟦P ⟧ R newα⃗_{n}.⟦Q⟧ : δ^{n}ℙ

with P ∼_{l} Q and fv(P) = fv(Q) = α⃗. We perform a case analysis on the actions performed by newα⃗_{n}.⟦P ⟧.

• Suppose that s′ ⊢ newα⃗_{n}.⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.τ:!} → newα⃗_{n}.t for some s′ ⊇ s. This must

have been derived from s′ ∪^{.} a⃗ ⊢ ⟦P ⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} → t[a⃗/α⃗]. As ⟦P ⟧[a⃗/α⃗] = ⟦P [a⃗/α⃗]⟧,

by Lemma A.17, there is a term P′[a⃗/α⃗] such that P [a⃗/α⃗] \begin{matrix}− \\ − \end{matrix}^{τ} → P′[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ ⟦P′⟧[a⃗/α⃗] : ℙ. Late strong bisimulation is preserved by injective substitution, so P [a⃗/α⃗] ∼_{l} Q[a⃗/α⃗]. Then, by bisimulation there is Q′[a⃗/α⃗] such

that Q[a⃗/α⃗] \begin{matrix}− \\ − \end{matrix}^{τ} → Q′[a⃗/α⃗] and P′[a⃗/α⃗] ∼_{l} Q′[a⃗/α⃗]. By Lemma A.17, s′ ∪^{.} a⃗ ⊢

⟦Q⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} → u[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ ⟦Q′⟧[a⃗/α⃗] : ℙ. By the opera-

tional rules we have s′ ⊢ newα⃗_{n}.⟦Q⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.τ:!} → newα⃗_{n}.u. We must still show s′ ⊢ newα⃗_{n}.t ∼R∼ newα⃗_{n}.u : δ^{n}ℙ. By multiple applications of Lemma 3.5 we

derive s′ ⊢ newα⃗.t ∼ newα⃗.⟦P′⟧ : δ^{n}ℙ from s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ ⟦P′⟧[a⃗/α⃗] : ℙ. We also

derive s′ ⊢ newα⃗.u ∼ newα⃗.⟦Q′⟧ : δ^{n}ℙ from s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ ⟦Q′⟧[a⃗/α⃗] : ℙ. Again,

late strong bisimulation is preserved by injective substitution, so P′[a⃗/α⃗] ∼_{l} Q′[a⃗/α⃗] implies P′ ∼_{l} Q′. By construction of R, we finally have

s′ ⊢ newα⃗.t ∼ newα⃗.⟦P′⟧ R newα⃗.⟦Q′⟧ ∼ newα⃗.u : δ^{n}ℙ .

as wanted.

• The case newα⃗.out:a · b ·! is similar to the previous one.

• Suppose that for some s′ ⊇ s, s′ ⊢ newα⃗_{n}.⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.bout:b·!} → newα⃗_{n}.t. This

must have been derived from s′ ∪^{.} a⃗ ⊢ ⟦P ⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{bout:i·!} → t[a⃗/α⃗], where i = a_{i} if b = α_{i}, and i = b otherwise. By Lemma A.17, there is a term P′[a⃗/α⃗]

such that P [a⃗/α⃗] \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{i}(γ)} → P′[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ (newγ.⟦P′⟧)[a⃗/α⃗] : δℙ.

Observe that γ ∉ α⃗. Now, by late strong bisimulation, there is Q′[a⃗/α⃗] such

that Q[a⃗/α⃗] \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{i}(γ)} → Q′[a⃗/α⃗] and P′[a⃗/α⃗] ∼_{l} Q′[a⃗/α⃗]. By Lemma A.17, s′ ∪^{.} a⃗ ⊢

⟦Q⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{bout:i·!} → u[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ (newγ.⟦Q′⟧)[a⃗/α⃗] : δℙ. By the

operational rules we have s′ ⊢ newα⃗_{n}.⟦Q⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.bout:b·!} → newα⃗_{n}.u. We must conclude s′ ⊢ newα⃗_{n}.t ∼R∼ newα⃗_{n}.u : δ^{n}δℙ. Multiple applications of Lemma 3.5 allow us to derive s′ ⊢ newα⃗.t ∼ newα⃗.newγ.⟦P′⟧ : δ^{n}δℙ from s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ (newγ.⟦P′⟧)[a⃗/α⃗] : δℙ. We also derive s′ ⊢ newα⃗.u ∼ newα⃗.newγ.⟦Q′⟧ : δ^{n}δℙ from s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ (newγ.⟦Q′⟧)[a⃗/α⃗] : δℙ. Since P′ ∼_{l} Q′, by construction of R, we have

s′ ⊢ newα⃗.t ∼ newα⃗.newγ.⟦P′⟧ R newα⃗.newγ.⟦Q′⟧ ∼ newα⃗.u : δ^{n}δℙ .

• Suppose that for some s′ ⊇ s, s′ ⊢ newα⃗_{n}.⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.inp:b·!} → newα⃗_{n}.t. This must

have been derived from s′ ∪^{.} a⃗ ⊢ ⟦P ⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{inp:i·!} → t[a⃗/α⃗], where i = a_{i} if b = α_{i}, and i = b otherwise. By Lemma A.17, there is a term P′[a⃗/α⃗] such that

P [a⃗/α⃗] \begin{matrix}− \\ − \end{matrix}^{iγ} → P′[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ (λγ.⟦P′⟧)[a⃗/α⃗] : ℕ → ℙ. Now, by late

strong bisimulation, there is Q′[a⃗/α⃗] such that Q[a⃗/α⃗] \begin{matrix}− \\ − \end{matrix}^{iγ} → Q′[a⃗/α⃗] and for all m,

P′[a⃗/α⃗][m/γ] ∼_{l} Q′[a⃗/α⃗][m/γ]. By Lemma A.17, s′ ∪^{.} a⃗ ⊢ ⟦Q⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{inp:i·!} → u[a⃗/α⃗]

and s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ (λγ.⟦Q′⟧)[a⃗/α⃗] : ℕ → ℙ. By the operational rules we

have the transition s′ ⊢ newα⃗_{n}.⟦Q⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.inp:b·!} → newα⃗_{n}.u. We must conclude s′ ⊢ newα⃗_{n}.t ∼R∼ newα⃗_{n}.u : δ^{n}ℕ → ℙ. By multiple applications of Lemma 3.5

we derive s′ ⊢ newα⃗.t ∼ newα⃗.λγ.⟦P′⟧ : δ^{n}(ℕ → ℙ) from s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼

(λγ.⟦P′⟧)[a⃗/α⃗] : ℕ → ℙ. We also derive s′ ⊢ newα⃗.u ∼ newα⃗.λγ.⟦Q′⟧ : δ^{n}(ℕ → ℙ)

from s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ (λγ.⟦Q′⟧)[a⃗/α⃗] : ℕ → ℙ. Since P′ ∼_{l} Q′, we have

s′ ⊢ newα⃗.t ∼ newα⃗.λγ.⟦P′⟧ R newα⃗.λγ.⟦Q′⟧ ∼ newα⃗.u : δ^{n}(ℕ → ℙ) .

Consider now

s ⊢ newα⃗_{n}.λγ.⟦P ⟧ R newα⃗_{n}.λγ.⟦Q⟧ : δ^{n}(ℕ → ℙ)

because for all m, P [m/γ] ∼_{l} Q[m/γ]. We perform a case analysis on the actions performed by newα⃗_{n}.λγ.⟦P ⟧.

• Suppose that s′ ⊢ newα⃗_{n}.λγ.⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.n↦τ:!} → newα⃗_{n}.t for some s′ ⊇ s. This must

have been derived from s′ ∪^{.} a⃗ ⊢ ⟦P ⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{e↦τ:!} → t[a⃗/α⃗], that in turn must have been derived from s′ ∪^{.} a⃗ ⊢ ⟦P ⟧[a⃗/α⃗][e/γ] \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} → t[a⃗/α⃗] for e ∈ s′ ∪^{.} a⃗. Observe that e = a_{i} if n = α_{i} for some i, and e = n otherwise. By Lemma A.17, there is a term

P′[a⃗/α⃗] such that P [a⃗/α⃗][e/γ] \begin{matrix}− \\ − \end{matrix}^{τ} → P′[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ ⟦P′⟧[a⃗/α⃗] : ℙ.

As for all m it holds P [m/γ] ∼_{l} Q[m/γ], by bisimulation there is Q′[a⃗/α⃗] such

that Q[a⃗/α⃗][e/γ] \begin{matrix}− \\ − \end{matrix}^{τ} → Q′[a⃗/α⃗] and P′[a⃗/α⃗] ∼_{l} Q′[a⃗/α⃗]. By Lemma A.17, s′ ∪^{.} a⃗ ⊢

⟦Q⟧[a⃗/α⃗][e/γ] \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} → u[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ ⟦Q′⟧[a⃗/α⃗] : ℙ. By the operational

rules we have s′ ⊢ newα⃗_{n}.λγ.⟦Q⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.n↦τ:!} → newα⃗_{n}.u. We must conclude s′ ⊢

newα⃗_{n}t ∼R∼ newα⃗_{n}u : δ^{n}ℙ. By multiple applications of Lemma 3.5 we derive

s′ ⊢ newα⃗.t ∼ newα⃗.⟦P′⟧ : δ^{n}ℙ from s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ ⟦P′⟧[a⃗/α⃗] : ℙ. We also derive

s′ ⊢ newα⃗.u ∼ newα⃗.⟦Q′⟧ : δ^{n}ℙ froms′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ ⟦Q′⟧[a⃗/α⃗] : ℙ. Late strong

bisimulation is preserved by injective substitution, so P′[a⃗/α⃗] ∼_{l} Q′[a⃗/α⃗] implies P′ ∼_{l} Q′. By construction of R, we finally have

s′ ⊢ newα⃗.t ∼ newα⃗.⟦P′⟧ R newα⃗.⟦Q′⟧ ∼ newα⃗.u : δ^{n}ℙ .

as wanted.

• The case newα⃗.out:a · b ·! is similar to the previous one.

• Suppose that s′ ⊢ newα⃗_{n}.λγ.⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.n↦bout:b·!} → newα_{n}.t for some s′ ⊇ s. This

must have been derived from s′ ∪^{.} a⃗ ⊢ ⟦P ⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{e↦bout:i·!} → t[a⃗/α⃗], that in turn

must have been derived from s′ ∪^{.} a⃗ ⊢ ⟦P ⟧[a⃗/α⃗][e/γ] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{bout:i·!} → t[a⃗/α⃗] for e ∈ s′ ∪^{.} a⃗.

Observe that e = a_{i} if n = α_{i} and e = n otherwise. Observe also that i = a_{j} if b = α_{j} and i = b otherwise. By Lemma A.17, there is a term P′[a⃗/α⃗] such

that P [a⃗/α⃗][e/γ] \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{i}(ζ)} → P′[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ (newζ.⟦P′⟧)[a⃗/α⃗] : δℙ. As

for all m it holds P [m/γ] ∼_{l} Q[m/γ], by bisimulation there is Q′[a⃗/α⃗] such that

Q[a⃗/α⃗][e/γ] \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{i}(ζ)} → Q′[a⃗/α⃗] and P′[a⃗/α⃗] ∼_{l} Q′[a⃗/α⃗]. By Lemma A.17, s′ ∪^{.} a⃗ ⊢

⟦Q⟧[a⃗/α⃗][e/γ] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{bout:i·!} → u[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ (newζ.⟦Q′⟧)[a⃗/α⃗] : δℙ. By

the operational rules we have s′ ⊢ newα⃗_{n}.λγ.⟦Q⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.n↦bout:b·!} → newα⃗_{n}.u. We must conclude s′ ⊢ newα⃗_{n}t ∼R∼ newα⃗_{n}u : δ^{n}δℙ. By multiple applications of Lemma 3.5 we derive s′ ⊢ newα⃗.t ∼ newα⃗.newζ.⟦P′⟧ : δ^{n}δℙ from s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ (newζ.⟦P′⟧)[a⃗/α⃗] : δℙ. We also derive s′ ⊢ newα⃗.u ∼ newα⃗.newζ.⟦Q′⟧ : δ^{n}δℙ from s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ (newζ.⟦Q′⟧)[a⃗/α⃗] : δℙ. Since P′ ∼_{l} Q′, by construction of R, we finally have

s′ ⊢ newα⃗.t ∼ newα⃗.newζ.⟦P′⟧ R newα⃗.newζ.⟦Q′⟧ ∼ newα⃗.u : δ^{n}δℙ .

• Suppose that s′ ⊢ newα⃗_{n}.λγ.⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.n↦inp:b·!} → newα_{n}.t for some s′ ⊇ s. This

must have been derived from s′ ∪^{.} a⃗ ⊢ ⟦P ⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{e↦inp:i·!} → t[a⃗/α⃗], that in turn

must have been derived from s′ ∪^{.} a⃗ ⊢ ⟦P ⟧[a⃗/α⃗][e/γ] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{inp:i·!} → t[a⃗/α⃗] for e ∈ s′ ∪^{.} a⃗.

Observe that e = a_{i} if n = α_{i} and e = n otherwise. Observe also that i = a_{j} if b = α_{j} and i = b otherwise. By Lemma A.17, there is a term P′[a⃗/α⃗] such

that P [a⃗/α⃗][e/γ] \begin{matrix}− \\ − \end{matrix}^{iζ} → P′[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ (λζ.⟦P′⟧)[a⃗/α⃗] : ℕ → ℙ.

As for all m it holds P [m/γ] ∼_{l} Q[m/γ], by bisimulation there is Q′[a⃗/α⃗] such

that Q[a⃗/α⃗][e/γ] \begin{matrix}− \\ − \end{matrix}^{iζ} → Q′[a⃗/α⃗] and P′[a⃗/α⃗] ∼_{l} Q′[a⃗/α⃗]. By Lemma A.17, s′ ∪^{.} a⃗ ⊢

⟦Q⟧[a⃗/α⃗][e/γ] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{inp:i·!} → u[a⃗/α⃗] and s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ (λζ.⟦Q′⟧)[a⃗/α⃗] : ℕ → ℙ. By

the operational rules we have s′ ⊢ newα⃗_{n}.λγ.⟦Q⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗_{n}.n↦inp:b·!} → newα⃗_{n}.u. We must conclude s′ ⊢ newα⃗_{n}.t ∼R∼ newα⃗_{n}.u : δ^{n}ℕ → ℙ. By multiple applications of Lemma 3.5 we derive s′ ⊢ newα⃗.t ∼ newα⃗.λζ.⟦P′⟧ : δ^{n}(ℕ → ℙ) from s′ ∪^{.} a⃗ ⊢ t[a⃗/α⃗] ∼ (λζ.⟦P′⟧)[a⃗/α⃗] : ℕ → ℙ. We also derive s′ ⊢ newα⃗.u ∼ newα⃗.λζ.⟦Q′⟧ :

δ^{n}(ℕ → ℙ) from s′ ∪^{.} a⃗ ⊢ u[a⃗/α⃗] ∼ (λζ.⟦Q′⟧)[a⃗/α⃗] : ℕ → ℙ. Since P′ ∼_{l} Q′, by

construction of R, we finally have

s′ ⊢ newα⃗.t ∼ newα⃗.λζ.⟦P′⟧ R newα⃗.λζ⟦Q′⟧ ∼ newα⃗.u : δ^{n}(ℕ → ℙ) .

This concludes the analysis. □

Theorem A.19 Let P and Q two closed π-calculus processes. If n(P, Q) ⊢ ⟦P ⟧ ∼ ⟦Q⟧ : ℙ, then P ∼_{l} Q. Proof We prove a stronger theorem:

Let P and Q two π-calculus processes such that fv(P) = fv(Q) = α⃗_{n}. If n(lhs,rhs) ⊢ newα⃗_{n}.⟦P ⟧ ∼ newα⃗_{n}.⟦Q⟧ : δ^{n}ℙ, then P ∼_{l} Q.

Let

R = {(P, Q) | n(lhs, rhs) ⊢ newα⃗_{n}.⟦P ⟧ ∼ newα⃗_{n}.⟦Q⟧ : δ^{n}ℙ and fv(P) = fv(Q) = α_{n}} .

We prove that R is a strong late bisimulation. Suppose P R Q and P −^{ℓ} → P′. We perform a case analysis on ℓ.

• Suppose that P \begin{matrix}− \\ − \end{matrix}^{τ} → P′. Since transition are preserved by bijective substitution, we have P [a⃗/α⃗] \begin{matrix}− \\ − \end{matrix}^{τ} → P′[a⃗/α⃗], for a set a⃗ of names fresh for both for P and Q. By Lemma A.17, n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ ⟦P ⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} → t[a⃗/α⃗], with n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ t[a⃗/α⃗] ∼ ⟦P′⟧[a⃗/α⃗] : ℙ. By the operational rules we get the transition n(lhs, rhs) ⊢ newα⃗.⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗.τ:!} → newα⃗.t, and by multiple applications of Lemma 3.5 we have n(lhs, rhs) ⊢ newα⃗.t ∼ newα⃗.⟦P′⟧ : δ^{n}ℙ. By bisimulation, there is a transition n(lhs, rhs) ⊢ newα⃗.⟦Q⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗.τ:!} → newα⃗.u, with n(lhs, rhs) ⊢ newα⃗.t ∼ newα⃗.u : δℙ. This must have been derived from n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ ⟦Q⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \end{matrix}^{τ:!} → u[a⃗/α⃗], and by Corollary 3.7 we have n(lhs, rhs) ∪^{.} {a⃗} ⊢ t[a⃗/α⃗] ∼ u[a⃗/α⃗] : ℙ. By Lemma A.17,

Q[a⃗/α⃗] \begin{matrix}− \\ − \end{matrix}^{τ} → Q′[a⃗/α⃗], with n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ u[a⃗/α⃗] ∼ ⟦Q′⟧[a⃗/α⃗] : ℙ. In turn Q \begin{matrix}− \\ − \end{matrix}^{τ} →

Q′, and by multiple applications of Lemma 3.5 we have n(lhs, rhs) ⊢ newα⃗.u ∼ newα⃗.⟦Q′⟧ : δ^{n}ℙ. As ∼ is transitive, by construction of R we conclude P′ R Q′.

• The case P \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{n}m} → is similar to the previous one.

• Suppose P \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{n}(ζ)} → P′. Since transition are preserved by bijective substitution, we

have P [a⃗/α⃗] \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{e}(ζ)} → P′[a⃗/α⃗], for α = fn(P), a⃗ a set of names fresh for both for P and Q, and e = a_{i} if n = α_{i} and e = n otherwise. Observe that ζ ∉ α⃗.

By Lemma A.17, n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ ⟦P ⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{bout:e·!} → t[a⃗/α⃗], with n(lhs, rhs) ∪^{.} {a⃗} ⊢ t[a⃗/α⃗] ∼ (newζ.⟦P′⟧)[a⃗/α⃗] : δℙ. By the operational rules we get n(lhs, rhs) ⊢

newα⃗.⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗.bout:n·!} → newα⃗.t, and by multiple applications of Lemma 3.5 we have n(lhs, rhs) ⊢ newα⃗.t ∼ newα⃗.newζ.⟦P′⟧ : δ^{n}δℙ. By bisimulation, n(lhs, rhs) ⊢

newα⃗.⟦Q⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗.bout:n·!} → newα⃗.u, with n(lhs, rhs) ⊢ newα⃗.t ∼ newα⃗.u : δ^{n}δℙ. This

must have been derived from n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ ⟦Q⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}^{bout:e·!} → u[a⃗/α⃗], and by Corollary 3.7 we have n(lhs, rhs) ⊢ t[a⃗/α⃗] ∼ u[a⃗/α⃗] : δℙ. By Lemma A.17,

Q[a⃗/α⃗] \begin{matrix}− \\ − \\ − \end{matrix}^{\overline{e}(ζ)} → Q′[a⃗/α⃗], with n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ u[a⃗/α⃗] ∼ (newζ.⟦Q′⟧)[a⃗/α⃗] : δℙ. In

turn Q \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{\overline{n}(ζ)} → Q′, and by multiple applications of Lemma 3.5 we have n(lhs, rhs) ⊢ newα⃗.u ∼ newα⃗.newζ.⟦Q′⟧ : δ^{n}δℙ. As ∼ is transitive, by construction of R we conclude P′ R Q′.

• Suppose P \begin{matrix}− \\ − \\ − \end{matrix}^{nζ} → P′. Since transition are preserved by bijective substitution, we have P [a⃗/α⃗] \begin{matrix}− \\ − \end{matrix}^{eζ} → P′[a⃗/α⃗], for α = fn(P), a⃗ a set of names fresh for both for P and Q, and e = a_{i} if n = α_{i} and e = n otherwise. Observe that ζ ∉ α⃗. By

Lemma A.17, n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ ⟦P ⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{inp:e·!} → t[a⃗/α⃗], with n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ t[a⃗/α⃗] ∼ (λζ.⟦P′⟧)[a⃗/α⃗] : ℕ → ℙ. By the operational rules we get n(lhs, rhs) ⊢

newα⃗.⟦P ⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗.inp:n·!} → newα⃗.t, and by multiple applications of Lemma 3.5 we have n(lhs, rhs) ⊢ newα⃗.t ∼ newα⃗.λζ.⟦P′⟧ : δ^{n}ℕ → ℙ. By bisimulation, n(lhs, rhs) ⊢

newα⃗.⟦Q⟧ \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ − \\ − \end{matrix}^{newα⃗.inp:n·!} → newα⃗.u, with n(lhs, rhs) ⊢ newα⃗.t ∼ newα⃗.u : δ^{n}ℕ → ℙ.

This must have been derived from n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ ⟦Q⟧[a⃗/α⃗] \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{inp:e·!} → u[a⃗/α⃗], and by Corollary 3.7 we have n(lhs, rhs) ∪^{.} {a⃗} ⊢ newα⃗.t ∼ newα⃗.u : δ^{n}ℕ → ℙ. By Lemma A.17, Q[a⃗/α⃗] \begin{matrix}− \\ − \end{matrix}^{eζ} → Q′[a⃗/α⃗], with n(lhs, rhs) ∪^{.} \{a⃗\} ⊢ u[a⃗/α⃗] ∼ (λζ.⟦Q′⟧)[a⃗/α⃗] : ℕ → ℙ. In turn Q \begin{matrix}− \\ − \\ − \end{matrix}^{nζ} → Q′, and by multiple applications of Lemma 3.5 we have n(lhs, rhs) ⊢ newα⃗.λζ.P′ ∼ newα⃗.λζ.⟦Q′⟧ : δ^{n}(ℕ → ℙ). It remains to prove that for all m it holds P′[m/ζ] R Q′[m/ζ]. By transitivity of ∼ we have n(lhs, rhs) ⊢ newα⃗.λζ.⟦P′⟧ ∼ newα⃗.λζ.⟦Q′⟧ : δ^{n}ℕ → ℙ and by multiple applications of Corollary 3.7 we derive n(lhs, rhs) ∪^{.} {a⃗} ⊢ (λζ.⟦P′⟧)[a⃗/α⃗] ∼ (λζ.⟦Q′⟧)[a⃗/α⃗] : ℕ → ℙ. We perform a case analysis on m.

– If m is a name constant, then by Lemma A.1, (repeated applications of) Corollary 3.8, and Proposition 3.3, there is a a′ such that m ∩ a′ = ∅ and

(n(lhs, rhs) ∪ {m}) ∪^{.} {a′} ⊢ ⟦P′⟧[a′/α⃗][m/ζ] ∼ ⟦Q′⟧[a′/α⃗][m/ζ] : ℙ. By multi-

ple applications of Lemma 3.5 we obtain n(lhs, rhs)∪{m} ⊢ newα⃗.⟦P′[m/ζ]⟧ ∼ newα⃗.⟦Q′[m/ζ]⟧ : δ^{n}ℙ and by construction of R we get P′[m/ζ] ∼_{l} Q′[m/ζ].

– Suppose that m is a name variable and m ∉ α⃗. By congruence, the equation

(n(lhs, rhs)) ∪^{.} {a′} ⊢ newm.((λζ.⟦P′⟧)m)[a′/α⃗] ∼ newm.((λζ.⟦Q′⟧)m)[a′/α⃗] :

δℙ holds. By Proposition 3.3 and by by multiple applications of Lemma 3.5 we obtain n(lhs, rhs) ⊢ newα⃗.newm.⟦P′[m/ζ]⟧ ∼ newα⃗.newm.⟦Q′[m/ζ]⟧ : δ^{n}δℙ and by construction of R we get P′[m/ζ] ∼_{l} Q′[m/ζ].

– Finally, suppose that m is a name variable and m = α_{i}. By Proposition 3.3 we

have n(lhs, rhs) ∪^{.} {a⃗} ⊢ ⟦P′⟧[a′/α⃗][a_{i}/ζ] ∼ ⟦Q′⟧[a′/α⃗][a_{i}/ζ] : ℙ. By multiple

applications of Lemma 3.5 we obtain n(lhs, rhs) ∪ {m} ⊢ newα⃗.⟦P′[α_{i}/ζ]⟧ ∼ newα⃗.⟦Q′[α_{i}/ζ]⟧ : δ^{n}ℙ and by construction of R we get P′[m/ζ] ∼_{l} Q′[m/ζ].

This concludes the analysis. □

Recent BRICS Report Series Publications

RS-04-21 Glynn Winskel and Francesco Zappa Nardelli. New-HOPLA— A Higher-Order Process Language with Name Generation. October 2004. 38 pp.

RS-04-20 Mads Sig Ager. From Natural Semantics to Abstract Machines. October 2004. 21 pp. Presented at the International Symposium on Logic-based Program Synthesis and Transformation, LOP-STR 2004, Verona, Italy, August 26–28, 2004.

RS-04-19 Bolette Ammitzbøll Madsen and Peter Rossmanith. Maximum Exact Satisfiability: NP-completeness Proofs and Exact Algorithms. October 2004. 20 pp.

RS-04-18 Bolette Ammitzbøll Madsen. An Algorithm for Exact Satisfiability Analysed with the Number of Clauses as Parameter. September 2004. 4 pp.

RS-04-17 Mayer Goldberg. Computing Logarithms Digit-by-Digit. September 2004. 6 pp.

RS-04-16 Karl Krukow and Andrew Twigg. Distributed Approximation of Fixed-Points in Trust Structures. September 2004. 25 pp.

RS-04-15 Jesús Fernando Almansa. Full Abstraction of the UC Framework in the Probabilistic Polynomial-time Calculus ppc. August 2004.

RS-04-14 Jesper Makholm Byskov. Maker-Maker and Maker-Breaker Games are PSPACE-Complete. August 2004. 5 pp.

RS-04-13 Jens Groth and Gorm Salomonsen. Strong Privacy Protection in Electronic Voting. July 2004. 12 pp. Preliminary abstract presented at Tjoa and Wagner, editors, 13th International Workshop on Database and Expert Systems Applications, DEXA ’02 Proceedings, 2002, page 436.

RS-04-12 Olivier Danvy and Ulrik P. Schultz. Lambda-Lifting in Quadratic Time. June 2004. 34 pp. To appear in Journal of Functional and Logic Programming. This report supersedes the earlier BRICS report RS-03-36 which was an extended version of a paper appearing in Hu and Rodríguez-Artalejo, editors, Sixth International Symposium on Functional and Logic Programming, FLOPS ’02 Proceedings, LNCS 2441, 2002, pages 134–151.