# Extensional and Non-extensional Functions as Processes

Ken Sakayori, Davide Sangiorgi

► To cite this version:

Ken Sakayori, Davide Sangiorgi. Extensional and Non-extensional Functions as Processes. 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2023, Boston, United States. 10.1109/LICS56636.2023.10175686. hal-04081885

HAL Id: hal-04081885

https://hal.science/hal-04081885

Submitted on 26 Apr 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Extensional and Non-extensional Functions as Processes

Ken Sakayori

University of Bologna and Inria

Davide Sangiorgi

University of Bologna and Inria

*Abstract*—Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure λ-calculus, the process representations yield (at best) non-extensional λ-theories (i.e., β rule holds, whereas η does not).

In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal π, Iπ (a subset of the π-calculus in which all outputs are bound), we develop a refinement of Milner's original encoding of functions as processes that is parametric on certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels. We show that when a few algebraic properties of wires hold, the encoding yields a λ-theory. Exploiting the symmetries and dualities of Iπ, we isolate three main classes of wires. The first two have a sequential behaviour and are dual of each other; the third has a parallel behaviour and is the dual of itself. We show the adoption of the parallel wires yields an extensional λ-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite η. In contrast, the other two classes of wires yield non-extensional λ-theories whose equalities are those of the Lévy-Longo and Böhm trees.

# I. INTRODUCTION

Milner's work [1], [2] on the encoding of the pure λ-calculus into the π-calculus is generally considered a landmark paper in the area of semantics and programming languages. The encoding of the λ-calculus is a significant test of expressiveness for the π-calculus. The encoding also gives an interactive semantics to the λ-calculus, which allows one to analyse it using the instruments available in the π-calculus. After Milner's seminal work, a number of encoding variants have been put forward (e.g. [3] and references therein) by modifying the target language (often to a subcalculus of the π-calculus) or the encoding itself. The correctness of these encodings is usually supported by the operational correspondence against a certain evaluation strategy of the λ-calculus and by the validity of the β-rule, $(\lambda x.M)N = M\{N/x\}$. (In this paper, by validity of a λ-calculus rule with respect to a certain process encoding $\{[\cdot]\}$, we mean that $\{[M]\} \approx \{[N]\}$ for all instances $M=N$ of (the congruence closure of) the rule, where $\approx$ is a basic behavioural equivalence for the pure processes, such as ordinary bisimilarity.)

The equality on λ-terms induced by the encoding has also been investigated; in this equality two λ-terms $M$ and

$N$ are equal when their images are behaviourally equivalent processes. For Milner's original (call-by-name) encoding, such an equality coincides with the Lévy-Longo tree (LT) equality [4], [5] (the result is by large independent of the behavioural equivalence adopted for the processes [6]). It has also been shown how to recover the Böhm tree (BT) equality [3], by modifying Milner's encoding — allowing reductions underneath a λ-abstraction — and selecting divergence-sensitive behavioural equivalences on processes such as must-testing.

Tree structures play a pivotal role in the λ-calculus. For instance, trees allow one to unveil the computational content hidden in a λ-term, with respect to some relevant minimal information. In BTs the information is the head normal forms, whereas in LTs it is the weak head normal forms. BT and LT equalities coincide with the local structures of well-known models of the λ-calculus, such as Plotkin and Scott's $P_\omega$ [7], [8], and the free lazy Plotkin-Scott-Engeler models [9], [10], [11].

In BTs and LTs, the computational content of a λ-term is unveiled using the β-rule alone. Such structures are sometimes called non-extensional, as opposed to the extensional structures, in which the β-rule is coupled with the η-rule, $M = \lambda x.Mx$ (for $x$ not free in $M$). In extensional theories two functions are equated if, whenever applied to the same argument, they yield equal results. A well-known extensional tree-structure are BTs with infinite η, shortly $\text{BT}_{\eta\infty}$s. The equality of $\text{BT}_{\eta\infty}$s coincides with that of Scott's $D_\infty$ model [8], historically the first model of the untyped λ-calculus. A seminal result by Wadsworth [12] shows that the $\text{BT}_{\eta\infty}$s are intimately related to the head normal forms, as the $\text{BT}_{\eta\infty}$ equality coincides with contextual equivalence in which the head normal forms are the observables.

In representations of functions as processes, extensionality and the η-rule, even in their most basic form, have always appeared out of reach. For instance, in Milner's encoding, $x$ and $\lambda y. xy$ have quite different behaviours: the former process is a single output particle, whereas the latter process has an infinite behaviour and, moreover, the initial action is an input.

The general goal of this paper is to study extensionality in the representation of functions as processes. In particular, we wish to understand if and how one can derive extensional representations, and the difference between
<table><caption>TABLE I
INSTANCES OF THE ABSTRACT ENCODING</caption><thead><tr><th>Encoding</th><th>Parameter (wires)</th><th>Characterises</th></tr></thead><tbody><tr><td>A<sub>10</sub></td><td>I-O wires</td><td>BT</td></tr><tr><td>A<sub>P</sub></td><td>P wires</td><td>BT<sub>η∞</sub></td></tr><tr><td>A<sub>01</sub></td><td>O-I wires</td><td>LT</td></tr></tbody></table>

extensional and non-extensional representations from a process perspective.

We outline the main technical contributions. We develop a refinement of Milner’s original encoding of functions, using Internal $\pi$ ($I\pi$), a subcalculus of the $\pi$-calculus in which only bound names may be exported. The encoding makes use of certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels; and when one of the two end-points is restricted, the wires behave as substitutions. In the encoding, wires are called ‘abstract’ because their definitions are not made explicit. We show that assuming a few basic algebraic properties of wires (having to do with transitivity of wires and substitution) is sufficient to obtain a $\lambda$-theory, i.e. the validity of the $\beta$-rule.

We then delve into the impact of the concrete definition of the wires, notably on the equivalence on $\lambda$-terms induced by the encoding. In the $\pi$-calculus literature, the most common form of wire between two channels $a$ and $b$ is written $!a(u).\bar{b}\langle u\rangle$ (or $a(u).\bar{b}\langle u\rangle$, if only needed once), and sometimes called a *forwarder* [13], [14]. In $I\pi$, free outputs are forbidden and such a wire becomes a recursively-defined process. We call this kind of wires *I-O wires*, because of their ‘input before output’ behaviour. Exploiting the properties of $I\pi$, e.g., its symmetries and dualities, we identify two other main kinds of wires: the *O-I wires*, with an ‘output before input’ behaviour and which are thus the dual of the I-O wires; and the *P wires*, or *parallel wires*, where input and output can fire concurrently (hence such wires are behaviourally the same as their dual).

We show that moving among these three kinds of wire corresponds to moving among the three above-mentioned tree structures of the $\lambda$-calculus, namely BTs, LTs, $BT_{\eta\infty}$s. Precisely, we obtain BTs when adopting the ordinary I-O wires; LTs when adopting the O-I wires; and $BT_{\eta\infty}$s when adopting the P wires. This also implies that P wires allow us to validate the $\eta$-rule (in fact both $\eta$ and infinite $\eta$). The results are summarised in Table I, where $A_X$ is the concrete encoding in which the X wires are used.

We are not aware of results in the literature that produce an extensional $\lambda$-theory from a processes model, let alone that derive the $BT_{\eta\infty}$ equality. We should also stress that the choice of the wire is the only modification needed for switching among the three tree structures: the encoding of the $\lambda$-calculus is otherwise the same, nor does it change the underlying calculus and its behavioural equivalence (namely, $I\pi$ and bisimilarity).

There are various reasons for using $I\pi$ in our study. The first and most important reason has to do with the symmetries and dualities of $I\pi$, as hinted above. The second reason is proof techniques: in the paper we use a wealth of proof techniques, ranging from algebraic laws to forms of ‘up-to bisimulation’ and to unique solutions of equations; not all of them are available in the ordinary $\pi$-calculus. The third reason has to do with $\eta$-rule. In studies of the expressiveness of $I\pi$ in the literature [15] the encoding of the free-output construct into $I\pi$ resembles an (infinite) $\eta$-expansion. The essence of the encoding is the following transformation (which needs to be recursively applied to eliminate all free outputs):

$$ \bar{a}\langle p\rangle \mapsto \nu q \; (\bar{a}\langle q\rangle | q(\tilde{y}).\bar{p}\langle \tilde{y}\rangle). \quad (1) $$

A free output of $p$ is replaced by a bound output, that is, an output of a freshly created name $q$ (for simplicity, we assume that $p$ is meant to be used only once by the recipient). The transformation requires *localised calculi* [16], in which the recipient of a name may only use it in output, and resembles an $\eta$-expansion of a variable of the $\lambda$-calculus in that, intuitively, direct access to the name $p$ is replaced by access to the function $\lambda\tilde{y}.\bar{p}\langle \tilde{y}\rangle$.

A possible connection between $I\pi$ and $\eta$-expansion may also be found in papers such as [17], where $\eta$-expanded proofs (proofs in which the identity rule is only applied to atomic formulas) are related to (session-typed) processes with bound outputs only. Yet, the technical link with our works appears weak because the wires that we use to achieve extensionality (the P wires of Table I) are behaviourally quite different from the process structures mentioned above.

We derive the encoding into $I\pi$ in two steps. The first step consists, intuitively, in transplanting Milner’s encoding into $I\pi$, by replacing free outputs with bound outputs plus wires, following the idea in (1) above. However, (1) is only valid in localised calculi, whereas Milner’s encoding also requires the *input* capability of names to be transmitted. Therefore we have to modify the wire in (1), essentially inverting the two names $p$ and $q$. The correctness of the resulting transformation relies on properties about the usage of names that are specific to the representation of functions. The second step adopted to derive the encoding consists of allowing reductions underneath a $\lambda$ abstraction; that is, implementing a *strong reduction strategy*. This transformation is necessary in order to mimic the computation required to obtain head normal forms.

Encodings of strong reduction strategies have appeared in the literature; they rely on the possibility of encoding non-blocking prefixes (sometimes called *delayed* in the literature) [18], [19], [20], [21], [14], [16], [3], i.e., prefixes $\mu: P$ in which actions from $P$ may fire before $\mu$, as long as $\mu$ does not bind names of the action. The encodings of non-blocking prefixes in the literature require the names bound in $\mu$ to be localised. Here again, the difficulty was
to adapt the schema to non-localised names. Similar issues arise within wires, as their definition also requires certain prefixes to be non-blocking.

*Structure of the paper* Section II recalls background material on λ-calculus and Iπ. In Section III, we introduce wires and permeable prefixes. In Section IV, we present the abstract encoding, using the abstract wires, and the assumptions we make on wires; we then verify that such assumptions are sufficient to obtain a λ-theory. Section V defines an optimised abstract encoding, which will be useful for later proofs. In Section VI, we introduce the three classes of concrete wires, and show that they satisfy the required assumptions for wires. In Section VII, we pick the I-O wires and O-I wires, and prove full abstraction for LTs and BTs. In Section VIII, we do the same for the P wires and BT<sub>η∞</sub>s. Section IX discusses further related work and possible future developments. For lack of space, proofs of the main results are only sketched. The reader may find the details in the Appendixes.

## II. BACKGROUND

A tilde represents a tuple. The *i*-th element of a tuple $\tilde{P}$ is referred to as $P_i$. All notations are extended to tuples componentwise.

### A. The λ-calculus

We let $x$ and $y$ range over the set of λ-calculus variables. The set $\Lambda$ of λ-terms is defined by the grammar

$$M ::= x \mid \lambda x. M \mid M_1 M_2.$$

Free variables, closed terms, substitution, α-conversion etc. are defined as usual [22]; the set of free variables of $M$ is $fv(M)$. Here and in the rest of the paper (including when reasoning about processes), we adopt the usual ‘Barendregt convention’. This will allow us to assume freshness of bound variables and names whenever needed. We group brackets on the left; therefore $MNL$ is $(MN)L$. We abbreviate $\lambda x_1 \dots \lambda x_n. M$ as $\lambda x_1 \dots x_n. M$, or $\lambda \tilde{x}. M$. Symbol $\Omega$ stands for the always-divergent term $(\lambda x. xx)(\lambda x. xx)$.

A number of reduction relations are mentioned in this paper. The (standard) *β-reduction* relation $M \to N$ is the relation on λ-terms induced by the following rules:

$$ \begin{align*} [\beta] \quad & \frac{\lambda x. M \quad N \to M \{N/x\}}{M \quad N \to M N'} \\ [\nu] \quad & \frac{M \to M'}{M N \to M' N} \qquad [\xi] \quad \frac{M \to M'}{\lambda x. M \to \lambda x. M'} \end{align*} $$

The (weak) *call-by-name reduction* relation uses only the $\beta$ and $\nu$ rules, whereas *strong call-by-name*, written $\to_{sn}$, also has $\xi$; the *head reduction*, written $\to_h$, is a deterministic variant of $\to_{sn}$ in which the redex contracted is the head one, i.e., $(\lambda y. M_0) M_1$ of $\lambda \tilde{x}. (\lambda y. M_0) M_1 \dots M_n$. *Head normal forms* are of the form $\lambda \tilde{x}. y \tilde{M}$. As usual, we use a double arrow to indicate the reflexive and transitive closure of a reduction relation, as in $\Rightarrow$ and $\Rightarrow_h$. A term $M$ has a head normal form $N$ if $M \Rightarrow_h N$ and $N$ is the (unique) head normal form. Terms that do not have a head

normal form are called *unsolvable*. An unsolvable $M$ has an order of unsolvability $n$, if $n$ is the largest natural number such that $M \Rightarrow_h \lambda x_1 \dots x_n. M'$, for $n \ge 0$, and some $x_1, \dots, x_n, M'$. If there is no such largest number, then $M$ is of order $\omega$. For instance, $\Omega$ is an unsolvable of order 0 and $\lambda x. \Omega$ of order 1.

We recall the definitions of Lévy-Longo trees and Böhm trees; then in the equality induced by such trees two terms are related if their trees are the same (as usual modulo α-conversion). In contrast, we present the definition of Böhm tree equality up-to infinite η-expansion as a bisimilarity, as the proofs exploit this bisimulation-based definition.

**Definition II.1** (Lévy-Longo trees and Böhm trees). The *Lévy-Longo tree* of $M$ is the labelled tree, $LT(M)$, defined coinductively as follows:

1) $LT(M) = \top$ if $M$ is an unsolvable of order $\omega$;

2) $LT(M) = \lambda x_1 \dots x_n. \bot$ if $M$ is an unsolvable of order $n < \omega$;

3) $LT(M)$ is the tree with $\lambda \tilde{x}. y$ as the root and $LT(M_1) \dots LT(M_n)$ as the children, if $M$ has head normal form $\lambda \tilde{x}. y M_1 \dots M_n$ with $n \ge 0$.

The definition of Böhm trees (BTs) is obtained from that of LTs using BT in place of LT, and demanding that $BT(M) = \bot$ whenever $M$ is unsolvable (in place of clauses (1) and (2)).

An η-expansion of a BT, whose root is $\lambda \tilde{x}. y$ and children are $BT(M_1), \dots, BT(M_n)$, is given by a tree whose root is $\lambda \tilde{x} z. y$ and children are $BT(M_1), \dots, BT(M_n), z$. Informally, an infinite η-expansion of a BT is obtained by allowing this expansion at each step of the clause (3). Equality over such trees can be formalised as a bisimilarity in which (finite) η-expansion is allowed at each step of the bisimulation game.

**Definition II.2** ([23]). A symmetric relation $\mathcal{R}$ on λ-terms is a $BT_{η\infty}$-bisimulation if, whenever $M \mathcal{R} N$, either one of the following holds:

1) $M$ and $N$ are unsolvable

2) $M \Rightarrow_h \lambda x_1 \dots x_{l+m}. y M_1 \dots M_{n+m}$ and $N \Rightarrow_h \lambda x_1 \dots x_l. y N_1 \dots N_n$, where $x_{l+1}, \dots, x_{l+m}$ are not free in $y N_1, \dots, N_n$, and $M_i \mathcal{R} N_i$ for $1 \le i \le n$, and also $M_{n+j} \mathcal{R} x_{l+j}$ for $1 \le j \le m$

3) the symmetric case, where $N$ reduces to a head normal form with more leading $\lambda s$.

The largest $BT_{η\infty}$-bisimulation is called $BT_{η\infty}$-bisimilarity. We also write $BT_{η\infty}(M) = BT_{η\infty}(N)$ when $M$ and $N$ are $BT_{η\infty}$-bisimilar.

**Example II.1.** We have $LT(\lambda x. \Omega) = \lambda x. \bot$, whereas $BT(\lambda x. \Omega) = \bot$. For $\Xi \stackrel{\text{def}}{=} (\lambda xy. xx)(\lambda xy. xx)$ we have $LT(\Xi) = \top$, whereas $BT(\Xi) = \bot$.

**Example II.2.** Let $J$ be a term such that $J z \Rightarrow_h \lambda y. z$ ($Jy$), which is easy to define using a fixed-point
combinator. Intuitively, the term $Jz$ can be considered as the 'limit of the sequence of $\eta$-expansions'

$$z \to_{\eta} \lambda z_1. z z_1 \to_{\eta} \lambda z_1. z (\lambda z_2. z_1 z_2) \to_{\eta} \dots$$

The terms $z$ and $Jz$ have different Böhm trees, as $\text{BT}(z) = z$ whereas $\text{BT}(Jz)$ has infinitely many nodes, the root being $\lambda z_1. z$. However, $\text{BT}_{\eta\infty}(Jz) = \text{BT}_{\eta\infty}(z)$ as the two terms can be equated using an infinite form of $\eta$-expansion.

## B. Internal $\pi$-calculus

In all encodings we consider, the encoding of a $\lambda$-term is parametric on a name, i.e., it is a function from names to $\pi$-calculus processes. We also need parametric processes (over one or several names) for writing recursive process definitions and equations. We call such parametric processes *abstractions*. The actual instantiation of the parameters of an abstraction $F$ is done via the *application* construct $F\langle\tilde{a}\rangle$. Processes and abstractions form the set of *agents*. Small letters $a, b, \dots, x, y, \dots$ range over the infinite set of names. The grammar of $I\pi$ is thus:

$$A ::= P \mid F \qquad (\text{agents})$$

$$P ::= \mathbf{0} \mid a(\tilde{b}).P \mid \bar{a}(\tilde{b}).P \mid \nu a P \quad (\text{processes}) \\ \qquad \mid P_1 | P_2 \mid !a(\tilde{b}).P \mid F\langle\tilde{a}\rangle$$

$$F ::= (\tilde{a}) P \mid K \qquad (\text{abstractions})$$

The operators used have the usual meanings. In prefixes $a(\tilde{b})$ and $\bar{a}(b)$, we call $a$ the *subject*. We often abbreviate $\nu a \nu b P$ as $(\nu a, b) P$. Prefixes, restriction, and abstraction are binders and give rise in the expected way to the definition of *free names*, *bound names*, and *names* of an agent, respectively indicated with $\text{fn}(-)$, $\text{bn}(-)$, and $\text{n}(-)$, as well as that of $\alpha$-conversion. An agent is *name-closed* if it does not contain free names. In the grammar, $K$ is a *constant*, used to write recursive definitions. Each constant $K$ has a defining equation of the form $K \stackrel{\text{def}}{=} (\tilde{x}) P$, where $(\tilde{x}) P$ is name-closed; $\tilde{x}$ are the formal parameters of the constant (replaced by the actual parameters whenever the constant is used). Replication could be avoided in the syntax since it can be encoded with recursion. However its semantics is simple, and it is a useful construct for encodings; thus we chose to include it in the grammar.

Since the calculus is polyadic, we assume a *sorting system* [24] to avoid disagreements in the arities of the tuples of names carried by a given name and in applications of abstractions. In Milner's encoding (written in the polyadic $\pi$-calculus) as well as in all encodings in the paper, there are only two sorts of names: *location names*, and *variable names*. Location names carry a pair of a variable name and a location name; variable names carry a single location name. Using $p, q, r, \dots$ for location names, and $x, y, z, \dots$ for variable names, the forms of the possible prefixes are:

$$p(x, q).P \mid x(p).P \mid \bar{p}(x, q).P \mid \bar{x}(p).P$$

This sorting will be maintained throughout the paper. Hence process transformations and algebraic laws will be given with reference to such a sorting.

The operational semantics of $I\pi$ is standard [3] (Appendix B.2). The reference behavioural equivalence for $I\pi$ is (weak) bisimilarity; it coincides with barbed congruence, assuming image-finiteness. We also use the *expansion* pre-order, written $\leqsim$, an asymmetric variant of $\approx$ in which, intuitively, $P \leqsim Q$ holds if $P \approx Q$ but also $Q$ has at least as many $\tau$-moves as $P$. As usual, $\stackrel{\mu}{\Rightarrow}$ is $\Rightarrow \stackrel{\mu}{\Rightarrow} \Rightarrow$, and $\stackrel{\mu}{\Rightarrow}$ is $\stackrel{\mu}{\Rightarrow}$ for $\mu \neq \tau$ and $\Rightarrow$ otherwise.

**Definition II.3 (Bisimilarity and Expansion).** A symmetric relation $\mathcal{R}$ on $I\pi$-processes is a *bisimulation*, if whenever $P \mathcal{R} Q$ and $P \stackrel{\mu}{\Rightarrow} P'$, then $Q \stackrel{\hat{\mu}}{\Rightarrow} Q'$ for some $Q'$ with $P' \mathcal{R} Q'$. Processes $P$ and $Q$ are *bisimilar*, written $P \approx Q$, if $P \mathcal{R} Q$ for some bisimulation $\mathcal{R}$.

A relation $\mathcal{R}$ over processes is an *expansion* if $P \mathcal{R} Q$ implies, whenever $P \stackrel{\mu}{\Rightarrow} P'$ (resp. $Q \stackrel{\mu}{\Rightarrow} Q'$), there exists $Q'$ (resp. $P'$) such that $Q \stackrel{\mu}{\Rightarrow} Q'$ (resp. $P \stackrel{\hat{\mu}}{\Rightarrow} P'$) and $P' \mathcal{R} Q'$. Here, $\stackrel{\hat{\mu}}{\Rightarrow}$ is $\stackrel{\mu}{\Rightarrow}$ if $\mu \neq \tau$ and is or $\stackrel{\tau}{\Rightarrow}$ if $\mu = \tau$. We say that $Q$ *expands* $P$, written $P \leqsim Q$, if $P \mathcal{R} Q$, for some expansion $\mathcal{R}$.

All behavioural relations are extended to abstractions by requiring ground instantiation of the parameters.

1) *Proof techniques:* In the proofs, we often use well-known algebraic laws, notably laws for private replications, and up-techniques for bisimilarity, notably bisimulations up-to expansion and contexts; we use up-to expansion rather than up-to weak bisimulation as the latter is known to be unsound. Again, we refer to Appendix B.4 for details.

We briefly recall the 'unique solution of equations' technique [25]. Equation variables $X, Y, Z$ are used to write equations. The body of an equation is a name-closed abstraction possibly containing equation variables (that is, applications can also be of the form $X\langle\tilde{a}\rangle$). We use $E$ to range over expression bodies; and $\mathcal{E}$ to range over systems of equations, defined as follows. In all the definitions, the indexing set $I$ can be infinite.

**Definition II.4.** Assume that, for each $i$ of a countable indexing set $I$, we have a variable $X_i$, and an expression $E_i$, possibly containing variables. Then $\{X_i = E_i\}_{i \in I}$ (sometimes written $\tilde{X} = \tilde{E}$) is a *system of equations*. (There is one equation for each variable $X_i$.) A system of equations is *protected* if each occurrence of a variable in the body of an equation is underneath a prefix.

We write $E[\tilde{F}]$ for the abstraction obtained by replacing in $E$ each occurrence of the variable $X_i$ with the abstraction $F_i$. This is a syntactic replacement, with instantiation of the parameters: e.g., replacing $X$ with $(\tilde{x})P$ in $X\langle\tilde{a}\rangle$ amounts to replacing $X\langle\tilde{a}\rangle$ with $P\{\tilde{a}/\tilde{x}\}$.
**Definition II.5.** Suppose {$X_i = E_i$}$_{i \in I}$ is a system of equations. We say that:

* $\tilde{F}$ is a solution of the system of equations for $\approx$ if for each $i$ it holds that $F_i \approx E_i[\tilde{F}]$.

* The system has a unique solution for $\approx$ if whenever $\tilde{F}$ and $\tilde{G}$ are both solutions for $\approx$, we have $\tilde{F} \approx \tilde{G}$.

**Definition II.6 (Syntactic solutions).** The syntactic solutions of a system of equations {$X_i = E_i$}$_{i \in I}$ are the recursively defined constants $K_{\tilde{E},i} \stackrel{\text{def}}{=} E_i[\tilde{K}_{\tilde{E}}]$, for $i \in I$.

The syntactic solutions of a system of equations are indeed solutions of it. The unique-solution technique relies on an analysis of divergences. A process $P$ diverges if it can perform an infinite sequence of internal moves, possibly after some visible ones (i.e., actions different from $\tau$). Formally, this holds if there are processes $P_i$, $i \ge 0$, and some $n$ such that $P = P_0 \xrightarrow{\mu_0} P_1 \xrightarrow{\mu_1} P_2 \xrightarrow{\mu_2} \dots$ and for all $i > n$, $\mu_i = \tau$. We call a divergence of $P$ the sequence of transitions $(P_i \xrightarrow{\mu_i} P_{i+1})_{i \ge 0}$. An abstraction $F$ has a divergence if the process $F\langle\tilde{a}\rangle$ has a divergence, where $\tilde{a}$ are fresh names.

**Theorem II.1 ([26]).** A guarded system of equations whose syntactic solutions are agents with no divergences has a unique solution for $\approx$.

### III. WIRES AND PERMEABLE PREFIXES

We introduce the abstract notion of wire process; and, as a syntactic sugar, the process constructs for permeable prefixes. Wires and permeable prefixes will play a central role in the technical development in the following sections. We use the notation $a \leftrightarrow \tilde{b}$ for an abstract wire; this is, intuitively, a special process whose purpose is to connect the output-end of $a$ with the input-end of $\tilde{b}$ (thus $a \leftrightarrow \tilde{b}$ itself will use $a$ in input and $\tilde{b}$ in output). We call such wires ‘abstract’ because we will not give a definition for them. We only state (Section IV) some behavioural properties that are expected to hold, and that have mainly to do with substitutions; approximately:

1) if $P$ uses $b$ only in input, then
   $\nu b (a \leftrightarrow \tilde{b} | P) \gtrsim P\{a/b\}$

2) dually, if $P$ uses $a$ only in output, then
   $\nu a (a \leftrightarrow \tilde{b} | P) \gtrsim P\{b/a\}$

Further conditions will however be needed on $P$ for such properties to hold (e.g., in (1), the input at $b$ in $P$ should be ‘at the top-level’, and in (2), the outputs at $a$ in $P$ should be ‘asynchronous’.) Special cases of (1) and (2) are forms of transitivity for wires, with the common name restricted:

3) $\nu b (a \leftrightarrow \tilde{b} | b \leftrightarrow \tilde{c}) \gtrsim (b \leftrightarrow \tilde{c})\{a/b\} = (a \leftrightarrow \tilde{b})\{c/b\} = a \leftrightarrow \tilde{c}$.

When (1) holds we say that $P$ is I-respectful with respect to $a \leftrightarrow b$; similarly when (2) holds we say that $P$ is O-respectful with respect to $a \leftrightarrow \tilde{b}$. When (3) holds, for any $a, b, c$ of the same sort, we say that wires are transitive.

As we have two sorts of names in the paper (location names and variable names), we will correspondingly deal with two sorts of wires, location wires and variable wires. In fact, location wires will be the key structures: definitions and properties for the variable wires will be adjusted accordingly, so to guarantee the desired properties of the location wires.

We write $a(\tilde{b}) : P$ and $\bar{a}(\tilde{b}) : P$ for a permeable input and a permeable output. Intuitively, a permeable prefix only blocks actions involving the bound names of the prefix. For instance, a permeable input $a(\tilde{b}) : P$, as an ordinary input, is capable of producing action $a(\tilde{b})$ thus yielding the derivative $P$. However, in contrast with the ordinary input, in $a(\tilde{b}) : P$ the process $P$ is active and running, and can thus interact with the outside environment; the only constraint is that the actions from $P$ involving the bound names $\tilde{b}$ cannot fire for as long as the top prefix $a(\tilde{b})$ is not consumed.

Given the two sorts of names that will be used in the paper, the possible forms of permeable prefixes are:

$$p(x, q) : P \mid \bar{p}(x, q) : P \mid x(p) : P \mid \bar{x}(p) : P$$

Moreover, it will always be the case that in a prefix $p(x, q) : P$ process $P$ uses $x$ only in output and $q$ only once in input, and conversely for $\bar{p}(x, q) : P$; and in $x(p) : P$ process $P$ uses $p$ only once in input, and conversely for $\bar{x}(p) : P$.

We stress that permeable prefixes should be taken as syntactic sugar; formally they are defined from ordinary prefixes and wires as follows

$$p(x, q) : P \stackrel{\text{def}}{=} (\nu x, q) (p(x', q'). (x \leftrightarrow \tilde{x}' | q' \leftrightarrow \tilde{q}) | P)$$

$$x(p) : P \stackrel{\text{def}}{=} \nu p (x(p'). p' \leftrightarrow \bar{p} | P)$$

$$\bar{p}(x, q) : P \stackrel{\text{def}}{=} (\nu x, q) (\bar{p}(x', q'). (x' \leftrightarrow \bar{x} | q \leftrightarrow \bar{q}') | P)$$

$$\bar{x}(p) : P \stackrel{\text{def}}{=} \nu p (\bar{x}(p'). p \leftrightarrow \bar{p}' | P)$$

Such definitions thus depend on the concrete forms of wires adopted. The definitions behave as intended only when the processes underneath the permeable prefixes are respectful. For example, we have

$$p(x, q) : P \xrightarrow{p(x, q)} (\nu x', q') (x' \leftrightarrow \bar{x} | q \leftrightarrow \bar{q}' | P\{x', q'/x, q\}) \gtrsim P$$

if $P$ is I-respectful with respect to $q' \leftrightarrow \bar{q}$ and O-respectful with respect to $x \leftrightarrow \bar{x}'$, for fresh $q'$ and $x'$.

Later, when the abstract wires will be instantiated to concrete wires, we will study properties of I-respectfulness and O-respectfulness, as well as, correspondingly, properties of permeable prefixes, in the setting of encodings of functions.

### IV. ABSTRACT ENCODING

This section introduces the abstract encoding of $\lambda$-terms into $\Pi$-processes. We call the encoding ‘abstract’ because
$$
\begin{align*}
\mathcal{A}[\llbracket x \rrbracket]_p &\stackrel{\text{def}}{=} \bar{x}(p') : p \leftrightarrow \bar{p}' \\
\mathcal{A}[\lambda x. M]_p &\stackrel{\text{def}}{=} p(x, q) : \mathcal{A}[\llbracket M \rrbracket]_q \\
\mathcal{A}[MN]_p &\stackrel{\text{def}}{=} \nu q ( \mathcal{A}[\llbracket M \rrbracket]_q | \\
&\qquad \bar{q}(x, p') : (!x(r). \mathcal{A}[\llbracket N \rrbracket]_r | p \leftrightarrow \bar{p}') )
\end{align*}
$$

<caption>Fig. 1. The abstract encoding $\mathcal{A}$.</caption>

it uses the abstract wires discussed in the previous section.
In other words, the encoding is *parametric* with respect to
the concrete definition of the wires. We then prove that,
whenever the wires satisfy a few basic laws, the encoding
yields a $\lambda$-theory.

A. *Definition of the abstract encoding*

We begin by recalling Milner’s original encoding $\mathcal{M}$ of
(call-by-name) $\lambda$-calculus into the $\pi$-calculus [2], [24]:

$$
\begin{align*}
\mathcal{M}[\llbracket x \rrbracket]_p &\stackrel{\text{def}}{=} \bar{x}\langle p \rangle \\
\mathcal{M}[\lambda x. M]_p &\stackrel{\text{def}}{=} p(x, q). \mathcal{M}[\llbracket M \rrbracket]_q \\
\mathcal{M}[MN]_p &\stackrel{\text{def}}{=} (\nu q, x) (\mathcal{M}[\llbracket M \rrbracket]_q | \bar{q}\langle x, p \rangle | !x(r). \mathcal{M}[\llbracket N \rrbracket]_r)
\end{align*}
$$

The encoding of a λ-term M is parametric over a port p, which can be thought of as the location of M, for p represents the unique port along which M may be called by its environment, thus receiving two names: (a trigger for) its argument and the location to be used for the next interaction. Hence, M (as well as all the encodings in the paper) is a function from λ-terms to abstractions of the form (p) P. We write M[[M]p as a shorthand for M[[M]]p. A function application of the λ-calculus becomes, in the π-calculus, a particular form of parallel combination of two agents, the function and its argument. An argument of an application is translated as a replicated server, that can be used as many times as needed, each time providing a name to be used as location for the following computation.

In Figure 1 we report the abstract encoding $\mathcal{A}$. There
are two main modifications from Milner’s encoding $\mathcal{M}$:

1) The encoding uses $I_\pi$, rather than $\pi$-calculus; for this, all free outputs are replaced by a combination of bound outputs and wires.

2) A permeable input is used, in place of an ordinary input, in the translation of abstraction so to allow reductions underneath a λ-abstraction. (We thus implement a strong call-by-name strategy.)

We report a few basic conditions that will be required
on wires. The main ones concern the behaviour of wires
as substitutions and transitivity of wires.

**Definition IV.1 (Wires).** As a convention, we assume that names *a*, *b*, *c* are of the same sort, either location names or variable names. *Wires* *a* ↔ *b* are processes that satisfy the following properties:

1) The free names of $a \leftrightarrow \bar{b}$ are $a$ and $b$. Furthermore, $a \leftrightarrow \bar{b}$ only uses $a$ in input and $b$ in output.

2) If $a \leftrightarrow \bar{b} \xrightarrow{\mu} P$ for some $P$, then $\mu \neq \tau$.

3) $\nu b$ ($a \leftrightarrow \bar{b} \mid b \leftrightarrow \bar{c}) \gtrsim a \leftrightarrow \bar{c}$.

4) $\nu q$ ($p \leftrightarrow \bar{q} \mid q(x,r): P \gtrsim p(x,r): P$, provided that $(\nu x, r)(x \leftrightarrow \bar{x}' \mid r' \leftrightarrow \bar{r} \mid P) \gtrsim P\{x', r'/x, r\}$, where $x', r'$ are fresh names.

5) $\nu p$ ($p \leftrightarrow \bar{q} \mid \bar{p}(x,r): P \gtrsim \bar{q}(x,r): P$, provided that $(\nu x, r)(x' \leftrightarrow \bar{x} \mid r \leftrightarrow \bar{r}' \mid P) \gtrsim P\{x', r'/x, r\}$, where $x', r'$ are fresh names.

5) $\nu p$ ($p \leftrightarrow \bar{q} \mid \bar{p}(x,r): P \gtrsim \bar{q}(x,r): P$, provided that $(\nu x, r)(x' \leftrightarrow \bar{x} \mid r \leftrightarrow \bar{r}' \mid P) \gtrsim P\{x', r'/x, r\}$, where $x', r'$ are fresh names.

6) $\nu y$ ($x \leftrightarrow \bar{y} \mid !y(p). P \gtrsim !x(p). P$, provided that $y \notin \text{fn}(P)$ and $\nu p(p' \leftrightarrow \bar{p} \mid P) \gtrsim P\{p'/p\}$, where $p'$ is fresh.

7) $\nu x$ ($x \leftrightarrow \bar{y} \mid \bar{x}(p) : P \gtrsim \bar{y}(p) : P$, provided that $x \notin \text{fn}(P)$ and $\nu p$ ($p \leftrightarrow \bar{p}' \mid P) \gtrsim P\{p'/p\}$, where $p'$ is fresh.

8) $x \leftrightarrow \bar{y}$ is a replicated input process at $x$, i.e. $x \leftrightarrow \bar{y} = !x(p). P$ for some $P$.

Condition 1 is a simple syntactic requirement. Condition 2 says that wires are ‘optimised’ in that they cannot do any immediate internal interaction (this requirement, while not mandatory, facilitates a few proofs). Law 3 is about the transitivity of wires. Laws 4-7 show that wires act as substitutions for permeable inputs, permeable outputs and replicated input prefixes. We do not require similar laws for ordinary prefixes, e.g., as in

$$
\nu p (p \leftrightarrow \bar{q} | \bar{p}(x, r). P) \gtrsim \bar{q}(x, r). P
$$

because wires break the strict sequentiality imposed by
such prefixes (essentially transforming an ordinary prefix
into a permeable one: only for the process on the right any
action from P is blocked until the environment accepts an
interaction at q). Condition 8 requires x ↔ y to be an
input replicated processes, and is useful so to be able to
use the replication laws (Lemma B.1).

Hereafter we assume that $p \leftrightarrow \bar{q}$ and $x \leftrightarrow \bar{y}$ are indeed wires, i.e., processes that satisfy the requirements of Definition IV.1. We can therefore exploit such requirements to derive properties of the abstract encoding.

Lemma IV.1 shows that the processes encoding func-
tions are I-respectful with respect to the location wires,
and O-respectful with respect to the variable wires.

**Lemma IV.1.**

1) $\nu q$ ($p \leftrightarrow \bar{q} \mid \mathcal{A}[\llbracket M \rrbracket]_q \gtrsim \mathcal{A}[\llbracket M \rrbracket]_p$

2) $\nu x$ ($x \leftrightarrow \bar{y} \mid \mathcal{A}[\llbracket M \rrbracket]_p \gtrsim \mathcal{A}[\llbracket M\{y/x\} \rrbracket]_p$

B. Validity of $\beta$-reduction

The abstract encoding $\mathcal{A}$ validates $\beta$-reduction with re-
spect to the expansion relation. This is proved by showing
that substitution of a $\lambda$-term $M$ is implemented as a
communication to a replicated server that owns $M$. In
the proofs of the following statements, Lemma IV.1 is
frequently used.
**Lemma IV.2.** If $x \notin \text{fv}(N)$, then
$$ \nu x (A[[M]]_p | !x(q). A[[N]]_q) \gtrsim A[[M\{N/x\}]_p $$

**Theorem IV.3.** If $M \to N$, then $A[[M]]_p \gtrsim A[[N]]_p$.

Since bisimilarity is a congruence in $I\pi$ and our encoding is compositional, the validity of $\beta$-reduction implies that the equivalence induced by the encoding is a $\lambda$-theory.

**Corollary IV.4.** Let $=_{\pi} \stackrel{\text{def}}{=} \{(M, N) | A[[M]] \approx A[[N]]\}$. Then $=_{\pi}$ is a $\lambda$-theory, that is, a congruence on $\lambda$-terms that contains $\beta$-equivalence.

*Remark IV.1.* From a $\lambda$-theory, a $\lambda$-model can be extracted [22], hence Corollary IV.4 implies that we can construct a $\lambda$-model out of the process terms. The domain of the model would be the processes that are in the image of the encoding, quotiented with bisimilarity. We could not define the domain of the model out of all process terms (as in [5], as opposed to the processes in the image of the encoding) because our proofs rely on Lemma IV.1, and such a lemma cannot be extended to the set of all processes.

## V. OPTIMISED ENCODING

We introduce an optimised version of the abstract encoding, which removes certain 'administrative steps' on the process terms. This will allow us to have a sharper operational correspondence between $\lambda$-terms and processes, which will be needed in proofs in later sections. As in the previous section, we work with abstract wires, only assuming the requirements in Definition IV.1.

To motivate the need of the optimised encoding, let us consider the encoding of a term $(x M) N$:

$$ (\nu p_0, p_1) ( \begin{array}{l} \bar{x}(p'_0): p'_0 \leftrightarrow \bar{p}_0 \\ | \bar{p}_0(x_1, p'_1): (!x_1(r_1). \llbracket M \rrbracket_{r_1} | p_1 \leftrightarrow \bar{p}'_1) \\ | \bar{p}_1(x_2, p_2): (!x_2(r_2). \llbracket N \rrbracket_{r_2} | p \leftrightarrow \bar{p}_2) \end{array} ) $$

This process has, potentially (i.e., depending on the concrete instantiations of the wires), some initial administrative reductions. For instance, the output at $p_1$ may interact with the input end of the wire $p_1 \leftrightarrow \bar{p}'_1$.

In the optimised encoding $\mathcal{O}$, in Figure 2, any initial reduction of a process has a direct correspondence with a (strong call-by-name) reduction of the source $\lambda$-term. With respect to the unoptimised encoding $\mathcal{A}$, the novelties are in the clauses for application, where the case of a head normal form $x M_1 \cdots M_n$ (for $n \ge 1$) and of an application $(\lambda x. M_0) M_1 \cdots M_n$ with a head redex are distinguished. In both cases, $\mathcal{O}^n(p_0, p, \mathcal{O}[[M_1]] \cdots \mathcal{O}[[M_n]])$ is used for a compact representation of the encoding of the trailing arguments $M_1, \dots, M_n$, as a sequence of nested permeable prefixes and a bunch of replications embracing the terms $M_i$.

Analogous properties to those in Section IV for the unoptimised encoding $\mathcal{A}$ hold for $\mathcal{O}$. Using such properties, and reasoning by induction of the structure of a $\lambda$-term, we can prove that $\mathcal{O}$ is indeed an optimisation.

**Lemma V.1.** $A[[M]]_p \gtrsim \mathcal{O}[[M]]_p$.

The details about the operational behaviour of $\mathcal{O}[[M]]_p$, and its operational correspondence with $M$, are described in Appendix E. We only report here the statements of a few important lemmas.

**Lemma V.2.** If $\mathcal{O}[[M]]_p \xrightarrow{\tau} P$ then there exists $N$ such that $M \to_{\text{sn}} N$ and $P \gtrsim \mathcal{O}[[N]]_p$.

**Lemma V.3.** If $\mathcal{O}[[M]]_p \xrightarrow{\mu} P$ and $\mu$ is an input action, then $\mu$ is an input at $p$.

Later, when we relate our encoding to trees of the $\lambda$-calculus, the notions of head normal form and (un)solvable term will be important. Hence some of our operational correspondence results concern them.

**Lemma V.4.** Let $M$ be a $\lambda$-term. If $\mathcal{O}[[M]]_p \xrightarrow{\bar{x}(q)} P$ for some $P$, then $M$ has a head normal form $\lambda\tilde{y}. x \tilde{M}$, for some (possibly empty) sequence of terms $\tilde{M}$ and variables $\tilde{y}$ with $x \notin \tilde{y}$.

Thus, if $\mathcal{O}[[M]]_p$ can perform an output action, then $M$ is solvable.

**Corollary V.5.** $M$ is solvable then there are input actions $\mu_1, \dots, \mu_n$ ($n \ge 0$) and an output action $\mu$ such that $\mathcal{O}[[M]]_p \stackrel{\mu_1}{\implies} \dots \stackrel{\mu_n}{\implies} P$, for some $P$.

By Lemma V.1, Corollary V.5 also holds for $\mathcal{A}$. The converse of Corollary V.5 will also hold, in all three concrete encodings that will be studied in the next section. However we believe the result cannot be derived from the assumptions on wires in Definition IV.1.

We conclude by looking, as an example, at the unsolvable term $\Omega \stackrel{\text{def}}{=} (\lambda x. x x) (\lambda x. x x)$.

*Example V.1.* The process $\mathcal{O}[[\Omega]]_p$ is

$$ \nu p_0(p_0(x, q): \bar{x}(q_0): \bar{q}_0(y_1, q_1): (!y_1(r_1). \mathcal{O}[[x]]_{r_1} | q \leftrightarrow \bar{q}_1) | \bar{p}_0(x_1, p_1): (!x_1(r_1). \mathcal{O}[[\lambda x. x x]]_{r_1} | p \leftrightarrow \bar{p}_1)) $$

The only action $\mathcal{O}[[\Omega]]_p$ can do is a $\tau$-action or an input at $p$. Whether the input can be performed or not will depend on the concrete definition of the wire $p \leftrightarrow \bar{q}$. The possibility of an input action from an unsolvable of order 0 such as $\Omega$ is a major difference between our encoding and encodings in the literature, where the encoding of such unsolvables are usually purely divergent processes.

## VI. CONCRETE WIRES

We now examine concrete instantiations of the abstract wires in the encoding $\mathcal{A}$ (and its optimisation $\mathcal{O}$). In each case we have to define the wires for location and variable names. The location wires are the important ones: the definition of the variable wires will follow from them, with the goal of guaranteeing their expected properties. We consider three concrete wires: *I-O wires*, *O-I wires*, and *P wires*. The main difference among them is in the order
$$
\begin{align*}
\mathcal{O}[\!\llbracket x \rrbracket_p \stackrel{\text{def}}{=} \bar{x}(p') : p \leftrightarrow \bar{p}'
\end{align*}
\begin{align*}
\mathcal{O}[\!\llbracket \lambda x \cdot M \rrbracket_p \stackrel{\text{def}}{=} p(x, q) : \mathcal{O}[\!\llbracket M \rrbracket_q
\end{align*}
\begin{align*}
\mathcal{O}[\!\llbracket x M_1 \cdots M_n \rrbracket_p \stackrel{\text{def}}{=} \bar{x}(p_0) : \mathcal{O}^n \langle p_0, p, \mathcal{O}[\!\llbracket M_1 \rrbracket] \cdots \mathcal{O}[\!\llbracket M_n \rrbracket] \rangle
\end{align*}
\begin{align*}
\mathcal{O}[\!\llbracket (\lambda x \cdot M_0) M_1 \cdots M_n \rrbracket_p \stackrel{\text{def}}{=} \nu p_0 (p_0(x, q) : \mathcal{O}[\!\llbracket M_0 \rrbracket_q | \mathcal{O}^n \langle p_0, p, \mathcal{O}[\!\llbracket M_1 \rrbracket] \cdots \mathcal{O}[\!\llbracket M_n \rrbracket] \rangle)
\end{align*}
\begin{align*}
\mathcal{O}^n \langle p_0, p, \mathcal{O}[\!\llbracket M_1 \rrbracket] \cdots \mathcal{O}[\!\llbracket M_n \rrbracket] \rangle \stackrel{\text{def}}{=} \bar{p}_0(x_1, p_1) : \cdots \bar{p}_{n-1}(x_n, p_n) : \\
\phantom{\mathcal{O}^n \langle p_0, p, \mathcal{O}[\!\llbracket M_1 \rrbracket] \cdots \mathcal{O}[\!\llbracket M_n \rrbracket] \rangle \stackrel{\text{def}}{=} } (!x_1(r_1) \cdot \mathcal{O}[\!\llbracket M_1 \rrbracket]_{r_1} | \cdots | !x_n(r_n) \cdot \mathcal{O}[\!\llbracket M_n \rrbracket]_{r_n} | p \leftrightarrow \bar{p}_n)
\end{align*}
$$

<caption>Fig. 2. Optimised encoding. (The number *n* must be greater than 0 in the last three cases.)</caption>

in which the input and output of the location wires are
performed.

Location and variable wires will be defined by means
of mutual recursion. In contrast with the variable wires,
the location wires are non-replicated processes, reflecting
the linear usage of such names. We recall that the choice
of a certain kind of concrete wires (I-O wires, O-I wires,
or P wires) also affects the definition of the permeable
prefixes (as it refers to the wires), including the permeable
prefixes that may be used within the wires themselves.
We will also show de-sugared definitions of the concrete
wires, i.e., without reference to permeable prefixes. We
add a subscript (I0, OI, P) to indicate a concrete wire
(as opposed to an abstract one). For readability, in the
definitions of the concrete wires the name parameters
are instantiated (e.g., writing $a \leftrightarrow_{I0} \bar{b} \stackrel{\text{def}}{=} P$ rather than
$\leftrightarrow_{I0} \stackrel{\text{def}}{=} (a, b) P$).

I-O wires: In the I-O wires, the input of a wire precedes the output.

$$
\begin{align*}
p \leftrightarrow_{10} \bar{q} \stackrel{\text{def}}{=} p(y, p_1) \cdot \bar{q}(x, q_1) : (p_1 \leftrightarrow_{10} \bar{q}_1 | x \leftrightarrow_{10} \bar{y}) \\
x \leftrightarrow_{10} \bar{y} \stackrel{\text{def}}{=} !x(p) \cdot \bar{y}(q) : p \leftrightarrow_{10} \bar{q}
\end{align*}
$$

Inlining the abbreviations for permeable prefixes (as they
are, in turn, defined using wires, in this specific case, the
I-O wires), we obtain:

$$
\begin{align*}
p \stackrel{\text{def}}{\leftrightarrow}_{10} \bar{q} &= p(y, p_1) \cdot (\nu x, q_1) (\bar{q}(x', q_1')) \cdot (q_1 \stackrel{\text{def}}{\leftrightarrow}_{10} \bar{q}'_1 | x' \stackrel{\text{def}}{\leftrightarrow}_{10} \bar{x}) \\
&\qquad | p_1 \stackrel{\text{def}}{\leftrightarrow}_{10} \bar{q}_1 | x \stackrel{\text{def}}{\leftrightarrow}_{10} \bar{y}) \\
x \stackrel{\text{def}}{\leftrightarrow}_{10} \bar{y} &= !x(p) \cdot \nu q (\bar{y}(q')) \cdot q \stackrel{\text{def}}{\leftrightarrow}_{10} \bar{q}' | p \stackrel{\text{def}}{\leftrightarrow}_{10} \bar{q}
\end{align*}
$$

I-O wires, beginning with an input and proceeding with an
output, are similar to the ordinary wires in the literature,
sometimes called *forwarders*, and used to prove properties
about asynchronous and localised $\pi$-calculi (or encodings
of them) [13], [14], [16], [15]. An important technical
difference, within location wires, is the appearance of a
permeable prefix, in place of an ordinary prefix, and the
inner wire $p_1 \leftrightarrow_{10} \bar{q}_1$ that, in a forwarder, would have
$p_1$ and $q_1$ swapped. The reason for these differences is
that location wires are used with processes that are not

localised (the recipient of a location name will use it in
input, rather than in output). The difference also shows
up in the semantic properties: forwarders in the literature
are normally used to obtain properties of O-respectfulness
(Section III), with the input-end of the wire restricted; in
contrast, I-O wires will be used to obtain properties of I-
respectfulness, with the output-end of the wire restricted.

In the definition above of location wires, the permeable prefix cannot be replaced by an ordinary prefix: the transitivity of the wires (property 3 in Definitions IV.1) would be lost.

O-I wires: The symmetry of $I\pi$ enable us to consider
the dual form of (location) wire, with the opposite control
flow, namely 'from output to input':

$$
\begin{align*}
p \stackrel{\text{def}}{\leftrightarrow_{\bar{I}'} \bar{q}} &= \bar{q}(x, q_1) \cdot p(y, p_1) : (p_1 \stackrel{\text{def}}{\leftrightarrow_{\bar{I}'} \bar{q}_1} | x \stackrel{\text{def}}{\leftrightarrow_{\bar{I}'} \bar{y}}) \\
x \stackrel{\text{def}}{\leftrightarrow_{\bar{I}'} \bar{y}} &= !x(p) \cdot \bar{y}(q) : p \stackrel{\text{def}}{\leftrightarrow_{\bar{I}'} \bar{q}}
\end{align*}
$$

Remark VI.1 (Duality). If duality is taken to mean the exchange between input and output prefixes, then the set of location I-O wires is the dual of the set of O-I wires. Indeed, the location O-I wires are obtained from the corresponding location I-O wires by swapping input and output particles; variable wires, in contrast are left unchanged. This means that we obtain an O-I wire from an I-O wire if any input $p(\bar{b})$ is made into an output $\bar{p}(\bar{b})$, and conversely (moreover, accordingly, the parameters of the variable wires are swapped).

P wires: In the third form of wire, the sequentiality
in location wires is broken: input and output execute
concurrently. This is achieved by using, in the definition
of location wires, only permeable prefixes.

$$
\begin{align*}
p \stackrel{\text{def}}{\leftrightarrow_P \bar{q}} &= p(y, p_1) : \bar{q}(x, q_1) : (p_1 \stackrel{\text{def}}{\leftrightarrow_P \bar{q}_1} | x \stackrel{\text{def}}{\leftrightarrow_P \bar{y}}) \\
x \stackrel{\text{def}}{\leftrightarrow_P \bar{y}} &= !x(p) \cdot \bar{y}(q) : p \stackrel{\text{def}}{\leftrightarrow_P \bar{q}}
\end{align*}
$$

Without the syntactic sugar of permeable prefixes, the
definition of the location and variable P wires are thus:

$$
\begin{align*}
p \stackrel{\text{def}}{\leftrightarrow_P \bar{q}} &= (\nu p_1, q_1 x, y) (p(y', p'_1)) \cdot (p'_1 \stackrel{\text{def}}{\leftrightarrow_P \bar{p}_1} | y \stackrel{\text{def}}{\leftrightarrow_P \bar{y}'} | \\
& \qquad \bar{q}(q'_1, x')) \cdot (q_1 \stackrel{\text{def}}{\leftrightarrow_P \bar{q}'_1} | x' \stackrel{\text{def}}{\leftrightarrow_P \bar{x}}) | \\
& \qquad p_1 \stackrel{\text{def}}{\leftrightarrow_P \bar{q}_1} | x \stackrel{\text{def}}{\leftrightarrow_P \bar{y}})
\end{align*}
$$
$$x \underset{\bar{p}}{\leftrightarrow} \bar{y} \stackrel{\text{def}}{=} !x(p). \nu q (\bar{y}(q'). q \underset{\bar{p}}{\leftrightarrow} \bar{q}' | p \underset{\bar{p}'}{\leftrightarrow} \bar{q})$$

The wire $p \underset{\bar{p}}{\leftrightarrow} \bar{q}$ is dual of itself: due to the use of permeable prefixes, swapping input and output prefixes has no behavioural affect.

**Lemma VI.1.** The I-O wires, O-I wires and P wires satisfy the laws of Definition IV.1.

*Proof.* [Sketch] For each kind of wires, the proof is carried out in two steps. First, we show that the wires are transitive, using up-to techniques for bisimilarity. Then, the other laws are proved by algebraic reasoning (including the use of transitivity of wires). The proofs of transitivity are the most delicate ones, because of the concurrency allowed by permeable prefixes, especially in the case of P wires, and because permeable prefixes are defined in terms of the wires themselves. For example, unlike for forwarders in the literature, a wire $\nu q(p \underset{\bar{p}}{\leftrightarrow} \bar{q} | q \underset{\bar{p}}{\leftrightarrow} \bar{r})$ can immediately reduce at the internal name $q$. Moreover, the derivative

$$p(p_1, y) : \bar{r}(q_1, x) : ((\nu z_1, z_2) (x \underset{\bar{p}}{\leftrightarrow} \bar{z}_1 | z_1 \underset{\bar{p}}{\leftrightarrow} \bar{z}_2 | z_2 \underset{\bar{p}}{\leftrightarrow} \bar{y}) | (\nu s_1, s_2) (p_1 \underset{\bar{p}}{\leftrightarrow} \bar{s}_1 | s_1 \underset{\bar{p}}{\leftrightarrow} \bar{s}_2 | s_2 \underset{\bar{p}}{\leftrightarrow} \bar{q}_1))$$

shows that the reduction has made the chain of wires longer.

To prove transitivity, we crucially rely on up-to proof techniques for $I\pi$, notably ‘expansion up-to expansion and context’, and several algebraic laws. Thus we show that the relation with pairs of the form

$$(a_0 \underset{\bar{p}}{\leftrightarrow} \bar{a}_{n+1}, (\nu a_1, \dots, a_n) (a_0 \underset{\bar{p}}{\leftrightarrow} \bar{a}_1 | \dots | a_n \underset{\bar{p}}{\leftrightarrow} \bar{a}_{n+1}))$$

is an expansion up-to expansion and context. It is unclear how the proof could be carried out without such proof techniques. □

**Remark VI.2.** The duality between I-O wires and O-I wires also shows up in proofs. For instance, for I-O wires the proof of law 4 of Definitions IV.1 does not use the premise of the law (i.e., the respectfulness of P), whereas the proof of the dual law 5 does. In the case of O-I wires, the opposite happens: the proof of law 5 uses the premise, whereas that of law 4 does not.

In the following sections we examine the concrete encodings obtained by instantiating the wires of the abstract encoding $\mathcal{A}$ (Figure 1) with the I-O wires, O-I wires, and P wires. We denote the resulting (concrete) encodings as $\mathcal{A}_{I0}$, $\mathcal{A}_{0I}$, and $\mathcal{A}_P$, respectively. Similarly $\mathcal{O}_{I0}$, $\mathcal{O}_{0I}$, and $\mathcal{O}_P$ are the instantiations of the abstract optimised encoding $\mathcal{O}$. For instance, in $\mathcal{A}_{I0}$ and $\mathcal{O}_{I0}$ an abstract wire $a \leftrightarrow \bar{b}$ is instantiated with the corresponding concrete wire $a \underset{\bar{I0}}{\leftrightarrow} \bar{b}$; and similarly for O-I wires and P wires.

Having shown that all the wires satisfy the requirements of Axiom IV.1, we can use, in the proofs about all concrete encodings (optimised and not) the results in Sections IV and V for the abstract encoding and its abstract optimisation.

## VII. FULL ABSTRACTION FOR LTs AND BTs

In this section we consider $\mathcal{A}_{I0}$ and $\mathcal{A}_{0I}$, and prove full abstraction with respect to the BTs and LTs, respectively. Before that, we discuss the difference between $\mathcal{A}_{I0}$ and $\mathcal{A}_{0I}$ on the encoding of unsolvable terms. In the proofs we exploit the optimised encodings $\mathcal{O}_{0I}$ and $\mathcal{O}_{I0}$. Details of the proofs are given in Appendix G.

We recall that the differences between BTs and LTs are due to the treatment of unsolvable terms (cf. Section II-A). BTs equate all the unsolvable terms, whereas LTs distinguish unsolvables of different order, such as $\Omega$ and $\lambda x. \Omega$. We begin, as an example, with the terms $\Omega$ and $\lambda x. \Omega$. As we have seen in Example V.1, in the abstract optimised encoding $\mathcal{O}$ process $\mathcal{O}[\Omega]_p$ is:

$$\nu p_0 (p_0(x, q) : \bar{x}(q_0) : \bar{q}_0(y_1, q_1) : (!y_1(r_1). \mathcal{O}[x]_{r_1} | q \leftrightarrow \bar{q}_1) | \bar{p}_0(x_1, p_1) : (!x_1(r_1). \mathcal{O}[\lambda x. x x]_{r_1} | p \leftrightarrow \bar{p}_1)).$$

Its instantiation with O-I wires, $\mathcal{O}_{0I}[\Omega]_p$, cannot do any input action: as $p \leftrightarrow \bar{p}_1$ becomes the O-I wire $p \underset{\bar{I0}}{\leftrightarrow} \bar{p}_1$, the input occurrence of the free name $p$ is guarded by $p_1$, which in turn is bound by the (permeable) prefix at $p_0$. Indeed, the only action that $\mathcal{O}_{0I}[\Omega]_p$ can perform is (up-to expansion) $\mathcal{O}_{0I}[\Omega]_p \xrightarrow{\tau} \mathcal{O}_{0I}[\Omega]_p$, which corresponds to the reduction $\Omega \to \Omega$. Hence, $\mathcal{O}_{0I}[\Omega]_p$ cannot match the input action $\mathcal{O}_{0I}[\lambda x. \Omega]_p \xrightarrow{p(x,q)} \mathcal{O}_{0I}[\Omega]_q$, and the two processes are distinguished.

In contrast, with I-O wires, processes $\mathcal{O}_{I0}[\lambda x. \Omega]_p$ and $\mathcal{O}_{I0}[\Omega]_p$ are indistinguishable. As before, the former process can exhibit an input transition $\mathcal{O}_{I0}[\lambda x. \Omega]_p \xrightarrow{p(x,q)} \mathcal{O}_{I0}[\Omega]_q$. However now $\mathcal{O}_{I0}[\Omega]_p$ has a matching input transition, because when $p \leftrightarrow \bar{p}_1$ is the I-O wire $p \underset{\bar{I0}}{\leftrightarrow} \bar{p}_1$, the input at $p$ is not guarded. The derivative is

$$\begin{align*}
\nu p_0 (p_0(x, q) : \mathcal{O}_{I0}[x x]_q \\
& | \bar{p}_0(x_1, p_1) : (!x_1(r_1). \mathcal{O}_{I0}[\lambda x. x x]_{r_1} \\
& | \bar{p}_1(x_2, p_2) : (x_2 \underset{\bar{I0}}{\leftrightarrow} \bar{y} | q \underset{\bar{I0}}{\leftrightarrow} \bar{p}_2))) \\
& = \nu p_0 (p_0(x, q) : \mathcal{O}_{I0}[x x]_q \\
& | \bar{p}_0(x_1, p_1) : (!x_1(r_1). \mathcal{O}_{I0}[\lambda x. x x]_{r_1} \\
& | \bar{p}_1(x_2, p_2) : (!x_2(r_2). \mathcal{O}_{I0}[y]_{r_2} | q \underset{\bar{I0}}{\leftrightarrow} \bar{p}_2))) \\
& = \mathcal{O}_{I0}[\Omega y]_q
\end{align*}$$

(exploiting the definitions of $\mathcal{O}_{I0}[y]_{r_2}$ and $x_2 \underset{\bar{I0}}{\leftrightarrow} \bar{y}$). In a similar manner, one then shows that $\mathcal{O}_{I0}[\Omega]_q$ and $\mathcal{O}_{I0}[\Omega y]_q$ can match each other's transitions, and iteratively so, on the resulting derivatives.

More generally, only in $\mathcal{O}_{0I}$ a term $\mathcal{O}_{0I}[M]_p$ can perform an input transition if and only if $M$ is, or may reduce to, a function, say $M = \lambda x. M'$, and the input action intuitively corresponds to consuming the outermost '$\lambda x'$. In addition, only with $\mathcal{O}_{0I}$ a process $\mathcal{O}_{0I}[M]_p$ is bisimilar to 0 iff the term $M$ is an unsolvable of order 0. Therefore, we have:
**Lemma VII.1.** Let $M$ and $N$ be unsolvables of order $m$ and $n$ respectively, where $0 \le m, n \le \omega$. Then $\mathcal{O}_{0I}[M]_p \approx \mathcal{O}_{0I}[N]_p$ iff $m = n$.

We have discussed above why, in contrast, $\mathcal{O}_{I0}$ equates $\lambda x.\Omega$ and $\Omega$. Similarly, $\mathcal{O}_{I0}$ equates all the unsolvable terms.

**Lemma VII.2.** For any unsolvable term $M$, we have $\mathcal{O}_{I0}[M]_p \approx \mathcal{O}_{I0}[\Omega]_p$.

*Proof.* [Sketch] We show that the relation defined as $\{(\mathcal{O}_{I0}[M]_p, \mathcal{O}_{I0}[N]_p) | M, N \text{ are unsolvable}\}$ is a bisimulation up-to expansion. For this, we use Lemmas V.2, and V.3, and exploit the property that, for any unsolvable $M$, it holds that $\mathcal{O}_{I0}[M]_p \xrightarrow{p(x,q)} \mathcal{O}_{I0}[Mx]_q$, where $Mx$ is unsolvable since $M$ is so. $\square$

**Theorem VII.3.** [Full abstraction for LT and BT] For every $\lambda$-terms $M$ and $N$, we have:

1) $\mathrm{LT}(M) = \mathrm{LT}(N)$ if and only if $\mathcal{A}_{0I}[M] \approx \mathcal{A}_{0I}[N]$.

2) $\mathrm{BT}(M) = \mathrm{BT}(N)$ if and only if $\mathcal{A}_{I0}[M] \approx \mathcal{A}_{I0}[N]$.

*Proof.* [Sketch] The proofs exploit [6], which sets conditions for obtaining full abstraction with respect to LTs and BTs in an encoding of the $\lambda$-calculus into a process calculus. The conditions refer to the behavioural equivalence of the process calculus and to an auxiliary behavioural preorder contained in the equivalence. Our proofs go through each such condition, showing that it is satisfied. Below we report some of the conditions, tailored to our setting, where the encodings are $\mathcal{A}_{0I}$ and $\mathcal{A}_{I0}$, the calculus is $I\pi$, behavioural equivalence is $\approx$, and the auxiliary preorder is $\lesssim$. Then, we briefly comment on their proof. We refer to Appendix G for more details. Some conditions are common to LTs and BTs, and include:

(i) the encoding validates the $\beta$ rule with respect to $\lesssim$;

(ii) the encodings of the terms $\Omega$, $x \tilde{M}$, $x \tilde{M}'$, and $y \tilde{M}''$ are pairwise unrelated by $\approx$, assuming that $x \neq y$ and that tuples $\tilde{M}$ and $\tilde{M}'$ have different lengths.

The conditions specific to LTs are:

LT-i) $\mathcal{A}_{0I}[M] \approx \mathcal{A}_{0I}[N]$, for all unsolvables $M, N$ of order $\omega$;

LT-ii) for any $M$, the term $\mathcal{A}_{0I}[\lambda x. M]$ is unrelated by $\approx$ to $\mathcal{A}_{0I}[\Omega]$ and to any term of the form $\mathcal{A}_{0I}[x \tilde{M}]$.

The corresponding conditions for BTs are:

BT-i) $\mathcal{A}_{I0}[M] \approx \mathcal{A}_{I0}[\Omega]$ for all unsolvable $M$ of order $\omega$;

BT-ii) $M$ solvable implies that the term $\mathcal{A}_{I0}[\lambda x. M]$ is unrelated by $\approx$ to $\mathcal{A}_{I0}[\Omega]$ and to any term of the form $\mathcal{A}_{I0}[x \tilde{M}]$.

Some of the common conditions can be proved at the abstract level, for $\mathcal{A}$ or its optimisation $\mathcal{O}$, and are therefore valid for both $\mathcal{A}_{0I}$ and $\mathcal{A}_{I0}$: for instance, validity of $\beta$-reduction for $\lesssim$ is Theorem IV.3; and the behavioural

difference among (the encodings of) $\Omega$, $x \tilde{M}$, and $y \tilde{M}''$ is obtained from the operational correspondence results for the optimised abstract encoding $\mathcal{O}$.

The conditions (LT-i) and (BT-i) are about unsolvable terms. We have seen (Lemmas VII.1 and VII.2) that $\mathcal{O}_{0I}$ (hence also $\mathcal{A}_{0I}$) satisfies (LT-i) and that $\mathcal{O}_{I0}$ (hence also $\mathcal{A}_{I0}$) satisfies (BT-i). A delicate condition to check is (BT-ii) for $\mathcal{A}_{I0}$. For this, once more we exploit the optimised encoding $\mathcal{O}_{I0}$ and reason on the number of consecutive outputs that the processes can perform. $\square$

*Remark VII.1.* Neither $\mathcal{A}_{I0}$ nor $\mathcal{A}_{0I}$ validates the $\eta$-rule (i.e., the $\lambda$-theories induced are not extensional); this follows from Theorem VII.3 (specifically, conditions (LT-ii) and (BT-ii) mentioned in its proof).

## VIII. FULL ABSTRACTION FOR BT$_{η∞}$S

In this section we show that the encoding $\mathcal{A}_P$ obtained by instantiating the wires of the abstract encoding $\mathcal{A}$ of Section IV with the parallel wires (the P wires) yields an encoding that is fully abstract with respect to BT$_{η∞}$S (Böhm trees with infinite $\eta$-expansion).

We begin by showing that $\mathcal{A}_P$ induces an extensional $\lambda$-theory. As we know (Section VI) that $\mathcal{A}_P$ induces a $\lambda$-theory, we remain to check the validity of $\eta$-expansion.

**Theorem VIII.1.** For every $M$ and $x \notin \mathrm{fv}(M)$, we have $\mathcal{A}_P[M]_p \lesssim \mathcal{A}_P[\lambda x. M x]_p$.

*Proof.* The process $\mathcal{A}_P[\lambda x. M x]_p$ is

$$p(x, q): \nu r (\mathcal{A}_P[M]_r | \bar{r}(x', q')): (!x'(r') . \mathcal{A}_P[x]_{r'} | q \leftrightarrow_P \bar{q})).$$

As $!x'(r')$. $\mathcal{A}_P[x]_{r'} = x' \leftrightarrow_P \bar{x}$, we have:

$$\begin{align*}
\mathcal{A}_P[\lambda x. M x]_p \\
&= \nu r (\mathcal{A}_P[M]_r | p(x, q): \bar{r}(x', q')): (x' \leftrightarrow_P \bar{x} | q \leftrightarrow_P \bar{q}') \\
&= \nu r (\mathcal{A}_P[M]_r | p \leftrightarrow_P \bar{r}) \gtrsim \mathcal{A}_P[M]_p
\end{align*}$$

using Lemma IV.1 (and identifying processes 'up-to structure'). $\square$

The above result relies on the use of permeable prefixes, both in the encoding of $\lambda$-abstraction, and within the P wires.

**Corollary VIII.2.** Let $=_{\pi} \stackrel{\mathrm{def}}{=} \{(M, N) | \mathcal{A}_P[M] \approx \mathcal{A}_P[N]\}$. Then $=_{\pi}$ is an extensional $\lambda$-theory; that is, a congruence on $\lambda$-terms that contains $\beta$ and $\eta$-equivalence.

We are now ready to prove that $\mathcal{A}_P$ is fully abstract with respect to BT$_{η∞}$S. We focus on completeness: if BT$_{η∞}$(M) = BT$_{η∞}$(N) then $\mathcal{A}_P[M] \approx \mathcal{A}_P[N]$. Soundness will then be essentially derived from completeness, as BT$_{η∞}$ equality is the maximal consistent sensible $\lambda$-theory (see e.g. [22]). To show completeness, we rely on the 'unique solution of equation' technique, reviewed in Section II-B1.
**Remark VIII.1** (Unique solutions versus up-to techniques). Results about encodings of $\lambda$-calculus into process calculi, in previous sections of this paper and in the literature, usually employ up-to techniques for bisimilarity, notably up-to context and expansion. In the techniques, expansion is used to manipulate the derivatives of two transitions so to bring up a common context. Such techniques do not seem powerful enough for $BT_{\eta\infty}$. The reason is that some of the required transformations would violate expansion (i.e., they would require to replace a term by a 'less efficient' one), for instance 'η-expanding' a term $A_P[[z]]_p$ into $A_P[[\lambda y. z y]]_p$. A similar problem has been observed in the case of Milner's call-by-value encoding [26].

Suppose $\mathcal{R}$ is a $BT_{\eta\infty}$-bisimulation (Definition II.2). We define a (possibly infinite) system of equations $\mathcal{E}_\mathcal{R}$, solutions of which will be obtained from the encodings of the pairs in $\mathcal{R}$. There is one equation for each pair $(M, N) \in \mathcal{R}$. We describe how each equation is defined, following the clauses of $BT_{\eta\infty}$-bisimulation. Take $(M, N) \in \mathcal{R}$ and assume $\tilde{y} = \text{fv}(M, N)$.

1) If $M$ and $N$ are unsolvable, then, for the right-hand side of the equation, we pick a non-divergent process that is bisimilar to the encoding of $\Omega$:

$$X_{M,N} \tilde{y} = K_{\Omega}$$

For instance, we may choose $K_{\Omega} \stackrel{\text{def}}{=} (p) p(x, q) : K_{\Omega} \langle q \rangle$.

2) If $M \implies_h \lambda x_1 \dots x_{l+m} \cdot z M_1 \dots M_{n+m}$ and $N \implies_h \lambda x_1 \dots x_l \cdot z N_1 \dots N_n$, then the equation is:

$$X_{M,N} \tilde{y} p \stackrel{\text{def}}{=} p(x_1, p_1) : \dots : p_{l+m-1}(x_{l+m}, p_{l+m}) : \bar{z}(w, q) : \\ \mathcal{O}_P^{n+m} \left\langle \begin{array}{l} q, p_{l+m}, X_{M_1, N_1} \langle \tilde{y}_1 \rangle, \dots, X_{M_n, N_n} \langle \tilde{y}_n \rangle, \\ X_{M_{n+1}, x_{l+1}} \langle \tilde{y}_{n+1} \rangle, \dots, X_{M_{n+m}, x_{l+m}} \langle \tilde{y}_{n+m} \rangle \end{array} \right\rangle$$

where $\tilde{y}_i = \text{fv}(M_i, N_i)$ for $1 \le i \le n$, $\tilde{y}_i = \text{fv}(M_i, x_{i-n+l})$ for $n+1 \le i \le n+m$. and where $\mathcal{O}_P^r$ is the instantiation with $P$ wires of $\mathcal{O}^r$ in Figure 2.

3) For the case symmetric to (2), where $N$ reduces to a head normal form with more leading $\lambda$-abstractions, the equation is defined similarly to (2).

In (1), the use of a divergent-free term $K_{\Omega}$ allows us to meet the condition about divergence of the unique-solution technique. The right-hand side of (2) intuitively amounts to having, as a body of the equation, the process $\mathcal{O}_P[[\lambda x_1 \dots x_{l+m} \cdot z X_{M_1, N_1} \dots X_{M_{n+m}, x_{l+m}}]]$.

**Lemma VIII.3.** For any $M$ unsolvable, we have: $\mathcal{O}_P[[M]]_p \approx \mathcal{O}_P[[\Omega]]_p \approx K_{\Omega} \langle p \rangle$.

**Lemma VIII.4.** Let $\mathcal{R}$ be a $BT_{\eta\infty}$-bisimulation and $\mathcal{E}_\mathcal{R}$ be the system of equations defined from $\mathcal{R}$ as above. For each $(M, N) \in \mathcal{R}$, we define $F_{M,N} \stackrel{\text{def}}{=} (\tilde{x}, p) \mathcal{O}_P[[M]]_p$ and $G_{M,N} \stackrel{\text{def}}{=} (\tilde{x}, p) \mathcal{O}_P[[N]]_p$, where $\tilde{x} = \text{fv}(M, N)$. Then $\{F_{M,N}\}_{(M,N) \in \mathcal{R}}$ and $\{G_{M,N}\}_{(M,N) \in \mathcal{R}}$ are solutions of $\mathcal{E}_\mathcal{R}$.

**Proof.** [Sketch] There are three cases to consider, following Definition II.2. The case of $M$ and $N$ unsolvables is handled via Lemma VIII.3. The case of solvable term is reported in Appendix H and exploits validity of the $\eta$-expansion (Theorem VIII.1), the results of operational correspondence for the optimised encoding discussed in Section V, and other algebraic reasoning. $\square$

We also have to show that the system $\mathcal{E}_\mathcal{R}$ of equations we defined has a unique solution.

**Lemma VIII.5.** The system of equations $\mathcal{E}_\mathcal{R}$ is guarded and the syntactic solution of $\mathcal{E}_\mathcal{R}$ is divergence-free. Therefore, $\mathcal{E}_\mathcal{R}$ has a unique solution.

**Proof.** The system $\mathcal{E}_\mathcal{R}$ is guarded because all the occurrences of a variable in the right-hand side of an equation are underneath a replicated input prefixing. Divergence-freedom follows from the fact that the use of each name (bound or free) is strictly polarised in the sense that a name is either used as an input or as an output. In a strictly polarised setting, no $\tau$-transitions can be performed even after some visible actions because in $I\pi$ only fresh names may be exchanged. $\square$

**Theorem VIII.6** (Completeness for $BT_{\eta\infty}$). If $BT_{\eta\infty}(M) = BT_{\eta\infty}(N)$ then $A_P[[M]] \approx A_P[[N]]$.

**Proof.** Consider a $BT_{\eta\infty}$-bisimulation that equates $M$ and $N$. Take the system of equations $\mathcal{E}_\mathcal{R}$ corresponding to $\mathcal{R}$ as defined above. By Lemma VIII.4, $\mathcal{O}_P[[M]]$ and $\mathcal{O}_P[[N]]$ are (components) of the solutions of $\mathcal{E}_\mathcal{R}$. Since the solution is unique (Lemma VIII.5), we derive $\mathcal{O}_P[[M]] \approx \mathcal{O}_P[[N]]$. We also have $A_P[[M]] \approx A_P[[N]]$ (equivalence on the non-optimised encodings) because of Lemma V.1. $\square$

**Theorem VIII.7** (Soundness for $BT_{\eta\infty}$). If $A_P[[M]] \approx A_P[[N]]$ then $BT_{\eta\infty}(M) = BT_{\eta\infty}(N)$.

**Proof.** Let $=_{\pi}$ be the equivalence induced by $A_P$ and $I\pi$ bisimilarity. The equivalence $=_{\pi}$ is a sensible $\lambda$-theory by Corollary IV.4 and Lemma VIII.3. This theory is consistent: for example we have $A_P[[x]]_p \not\approx A_P[[\Omega]]_p$. By completeness (Theorem VIII.6), it contains $BT_{\eta\infty}$ equality. Then it must be equal to $BT_{\eta\infty}$ equality because the latter is the maximal consistent sensible $\lambda$-theory [22]. $\square$

## IX. CONCLUDING REMARKS

In the paper we have presented a refinement of Milner's original encoding of functions as processes that is parametric on certain abstract components called wires. Whenever wires satisfy a few algebraic properties, the encoding yields a $\lambda$-theory. We have studied instantiations of the abstract wires with three kinds of concrete wires, that differ on the direction and/or sequentiality of the control flow produced. We have shown that such instantiations allow us to obtain full abstraction results for LTs, BTs, and $BT_{\eta\infty}$s, (and hence for $\lambda$-models such as $P_\omega$, free lazy Plotkin-Scott-Engeler models, $D_\infty$). In the case of $BT_{\eta\infty}$,
this implies that the encoding validates the $\eta$-rule, i.e., it
yields an extensional $\lambda$-theory.

Following Milner’s seminal paper [1], the topic of func-
tions as processes has produced a rich bibliography. Below
we comment on the works that seem closest to ours. We
have mentioned in the Introduction related work con-
cerning LTs and BTs. We are unaware of results about
validity of the $\eta$-rule, let alone $BT_{\eta\infty}$, in encodings of
functions as processes. The only exception is [27], where a
type system for the $\pi$-calculus is introduced so to derive
full abstraction for an encoding of PCF (which implies
that $\eta$-expansion for PCF is valid). However, in [27],
types are used to constrain process behaviours, so to
remain with processes that represent ‘sequential functional
computations’. Accordingly, the behavioural equivalence
for processes is a typed contextual equivalence in which
the legal contexts must respect the typing discipline and
are therefore ‘sequential’. In contrast, in our work $\eta$ is vali-
dated under ordinary (unconstrained) process equivalence
in which, for instance, equalities are preserved by arbitrary
process contexts. (We still admit polyadic communications
and hence a sorting system, for readability — we believe
that the same results hold in a monadic setting.)

In the paper we have considered the theory of the
pure untyped $\lambda$-calculus. Hence, our encodings model the
call-by-name reduction strategy. A study of the theory
induced by process encodings of the call-by-value strategy
is [26].

Our definitions and proofs about encodings of permeable prefixes using wires follows, and is inspired by, encodings of forms of permeable prefixes in asynchronous and localised variants of the $\pi$-calculus using forwarders, e.g. [16], [28]. As commented in the main text, the technicalities are however different, both because our processes not localised, and because we employ distinct kinds of wires.

We have worked with bisimilarity, as it is the standard
behavioural equivalence in $\Pi\tau$; moreover, we could then use
some powerful proof techniques for it (up-to techniques,
unique solution of equations). The results presented also
hold for other behavioural equivalences (e.g., may testing),
since processes encoding functions are confluent. It would
be interesting to extend our work to preorders, i.e., looking
at preorder relations for $\lambda$-trees and $\lambda$-models.

In our work, we derived our abstract encoding from
Milner’s original encoding of functions. It is unclear how
to transport the same methodology to other variants of
Milner’s encoding in the literature, in particular those that
closely mimics the CPS translations [29], [30].

We have derived $\lambda$-tree equalities, in parametric man-
ner, by different instantiations of the abstract wires.
Van Bakel et al. [31] use an intersection type system,
parametric with respect to the subtyping relations, to
(almost) uniformly characterise $\lambda$-tree equalities (the trees
considered are those in our paper together with Böhm
trees up-to *finite* $\eta$-expansion and Beraducci trees).

We would like to investigate the possible relationship

between our work and game semantics. In particular, we
are interested in the ‘HO/N style’ as it is known to be
related to process representations (e.g., [32], [33], [34],
[35]). HO/N game semantics for the three trees considered
in this paper have been proposed [36], [37], [38]. The
technical differences with our work are substantial. For
instance, the game semantics are not given in a parametric
manner; and the $D_\infty$ equality is obtained via Nakajima
trees rather than $BT_{\eta\infty}$. Nakajima trees are a different
‘infinite $\eta$-expansion’ of Böhm trees, in the sense that
$\lambda\tilde{x}. y \tilde{M}$ is expanded to $\lambda\tilde{x}z_0z_1\dots y \tilde{M} z_0z_1\dots$; that is,
trees may be infinitely branching. In processes, this would
mean, for instance, having input prefixes that receive
infinitely-many names at the same time. We would like to
understand whether the three kinds of wires we considered
are meaningful in game semantics. The game semantic
counterpart of process wires are the *copycat strategies*,
and they intuitively correspond to I-O wires, in that they
begin with an O-move (i.e., an input action). This does
not change even in concurrent game semantics [39], [40].
We are not aware of game models that use strategies
corresponding to the O-I wires or the P wires studied in
our paper.

Similarly, we would like to investigate relationships with
call-by-name translations of the $\lambda$-calculus into (pure)
proof-nets [41]. We think that our encoding could be
factorised into the translation from $\lambda$-calculus into proof-
nets and a variant of Abramsky translation [18], [19]. In
this way, a P wire for location names would correspond
to an infinitely $\eta$-expanded form of the axiom link for the
type $o$ according to its recursive equation $o \cong (!o)^\perp \mathcal{J} o$.
Infinite $\eta$-expansions of the identity axioms have also been
considered in Girard’s ludics [42], where they are called
faxes. Faxes are different from P wires because faxes satisfy
an alternation condition akin to the locality of $\pi$-calculi.

Processes like wires (often called *links*) appear in
session-typed process calculi focusing on the Curry-
Howard isomorphism, as primitive process constructs used
to represent the identity axiom [43]. Some of our assump-
tions for wires, cf. the substitution-like behaviour when
an end-point of the wire is restricted, are then given as
explicit rules of the operational semantics of such links.

We have studied the properties of the concrete wires
used in the paper on processes encoding functions. We
would like to establish more general properties, on ar-
bitrary processes, possibly subject to constraints on the
usage of the names of the wires. We would also like to see
if other kinds of wires are possible, and which properties
they yield.

ACKNOWLEDGMENT

We thank the anonymous referees for useful com-
ments. This work was supported by the MIUR-PRIN
project ‘Analysis of Program Analyses’ (ASPRA, ID
201784YSZ5_004) and by the European Research Council
(ERC) Grant DLV-818616 DIAPASoN.
REFERENCES

[1] R. Milner, "Functions as processes," INRIA, Research Report RR-1154, 1990. [Online]. Available: https://hal.inria.fr/inria-00075405

[2] —, "Functions as processes," *Math. Struct. Comput. Sci.*, vol. 2, no. 2, pp. 119–141, 1992.

[3] D. Sangiorgi and D. Walker, *The π-calculus—A Theory of Mobile Processes*. Cambridge University Press, 2001.

[4] D. Sangiorgi, "An investigation into functions as processes," in *Mathematical Foundations of Programming Semantics (MFPS), ser. Lecture Notes in Computer Science, S. D. Brookes, M. G. Main, A. Melton, M. W. Mislove, and D. A. Schmidt, Eds.*, vol. 802. Springer, 1993, pp. 143–159.

[5] —, "Lazy functions and mobile processes," in *Proof, Language, and Interaction, Essays in Honour of Robin Milner*, G. D. Plotkin, C. Stirling, and M. Tofte, Eds. The MIT Press, 2000, pp. 691–720.

[6] D. Sangiorgi and X. Xu, "Trees from functions as processes," *Log. Methods Comput. Sci.*, vol. 14, no. 3, 2018.

[7] G. Plotkin, "A set theoretical definition of application," School of A.I., Univ. of Edinburgh, Tech. Rep. Tech. Rep. MIP-R-95, 1972.

[8] D. S. Scott, "Data types as lattices," *SIAM J. Comput.*, vol. 5, no. 3, pp. 522–587, 1976.

[9] J. Lévy, "An algebraic interpretation of the lambda beta k-calculus; and an application of a labelled lambda -calculus," *Theor. Comput. Sci.*, vol. 2, no. 1, pp. 97–114, 1976.

[10] E. Engeler, "Algebras and combinators," *Algebra Universalis*, vol. 13, pp. 389–392, 1981.

[11] G. Longo, "Set theoretical models of lambda calculus: Theory, expansions and isomorphisms," *Annales of Pure and Applied Logic*, vol. 24, pp. 153–188, 1983.

[12] C. P. Wadsworth, "The relation between computational and denotational properties for scott's $d_{infty}$-models of the lambda-calculus," *SIAM J. Comput.*, vol. 5, no. 3, pp. 488–521, 1976.

[13] K. Honda and N. Yoshida, "On reduction-based process semantics," *Theor. Comput. Sci.*, vol. 152, no. 2, pp. 437–486, 1995.

[14] M. Merro, "Locality in the π-calculus and applications to object-oriented languages," 2001, PhD thesis, Ecoles des Mines de Paris.

[15] M. Boreale, "On the expressiveness of internal mobility in name-passing calculi," *Theor. Comput. Sci.*, vol. 195, no. 2, pp. 205–226, 1998.

[16] M. Merro and D. Sangiorgi, "On asynchrony in name-passing calculi," *Mathematical Structures in Computer Science*, vol. 14, no. 5, pp. 715–767, 2004, a preliminary version in Proc. ICALP'98.

[17] L. Caires, F. Pfenning, and B. Toninho, "Linear logic propositions as session types," *Mathematical Structures in Computer Science*, vol. 26, no. 3, pp. 367–423, 2016.

[18] S. Abramsky, "Proofs as processes," *Theor. Comput. Sci.*, vol. 135, no. 1, pp. 5–9, 1994.

[19] G. Bellin and P. J. Scott, "On the pi-calculus and linear logic," *Theor. Comput. Sci.*, vol. 135, no. 1, pp. 11–65, 1994.

[20] Y. Fu, "A proof theoretical approach to communication," in *24th ICALP*, ser. Lecture Notes in Computer Science, vol. 1256. Springer Verlag, 1997.

[21] J. Parrow and B. Victor, "The fusion calculus: Expressiveness and symmetry in mobile processes," in *13th LICS Conf. IEEE Computer Society Press*, 1998.

[22] H. Barendregt, *The Lambda Calculus: Its Syntax and Semantics*, ser. North-Holland Linguistic Series. North-Holland, 1984.

[23] S. B. Lassen, "Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context," in *Mathematical Foundations of Programming Semantics MFPS 1999*, ser. Electronic Notes in Theoretical Computer Science, S. D. Brookes, A. Jung, M. W. Mislove, and A. Scedrov, Eds., vol. 20. Elsevier, 1999, pp. 346–374.

[24] R. Milner, "The polyadic π-calculus: a tutorial," in *Logic and Algebra of Specification*, ser. NATO ASI Series, F. Bauer, W. Brauer, and H. Schwichtenberg, Eds. Springer Berlin Heidelberg, 1993, vol. 94, pp. 203–246.

[25] A. Durier, D. Hirschkoff, and D. Sangiorgi, "Divergence and unique solution of equations," *Log. Methods Comput. Sci.*, vol. 15, no. 3, 2019.

[26] —, "Eager functions as processes," *Theor. Comput. Sci.*, vol. 913, pp. 8–42, 2022.

[27] M. Berger, K. Honda, and N. Yoshida, "Sequentiality and the pi-calculus," in *Typed Lambda Calculi and Applications TLCA 2001*, ser. Lecture Notes in Computer Science, S. Abramsky, Ed., vol. 2044. Springer, 2001, pp. 29–45.

[28] N. Yoshida, "Minimality and separation results on asynchronous mobile processes - representability theorems by concurrent combinators," *Theor. Comput. Sci.*, vol. 274, no. 1-2, pp. 231–276, 2002.

[29] D. Sangiorgi, "From $\lambda$ to $\pi$; or, Rediscovering continuations," *Mathematical Structures in Computer Science*, vol. 9, no. 4, pp. 367–401, 1999.

[30] H. Thielecke, "Categorical structure of continuation passing style," Ph.D. dissertation, University of Edinburgh, UK, 1997.

[31] S. van Bakel, F. Barbanera, M. Dezani-Ciancaglini, and F. de Vries, "Intersection types for lambda-trees," *Theor. Comput. Sci.*, vol. 272, no. 1-2, pp. 3–40, 2002.

[32] J. M. E. Hyland and C. L. Ong, "Pi-calculus, dialogue games and PCF," in *Proceedings of conf. on Functional programming languages and computer architecture (FPCA)*, J. Williams, Ed. ACM, 1995, pp. 96–107.

[33] K. Honda and N. Yoshida, "Game-theoretic analysis of call-by-value computation," *Theor. Comput. Sci.*, vol. 221, no. 1-2, pp. 393–456, 1999.

[34] S. Castellan and N. Yoshida, "Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side," *Proc. ACM Program. Lang.*, vol. 3, no. POPL, pp. 27:1–27:29, 2019.

[35] G. Jaber and D. Sangiorgi, "Games, mobile processes, and functions," in *30th EACSL Annual Conference on Computer Science Logic, CSL 2022*, ser. LIPIcs, F. Manea and A. Simpson, Eds., vol. 216. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, pp. 25:1–25:18.

[36] A. D. Ker, H. Nickau, and C. L. Ong, "Innocent game models of untyped lambda-calculus," *Theor. Comput. Sci.*, vol. 272, no. 1-2, pp. 247–292, 2002.

[37] —, "Adapting innocent game models for the böhm treelambda -theory," *Theor. Comput. Sci.*, vol. 308, no. 1-3, pp. 333–366, 2003.

[38] C. L. Ong and P. D. Gianantonio, "Games characterizing levy-longo trees," *Theor. Comput. Sci.*, vol. 312, no. 1, pp. 121–142, 2004.

[39] P. Melliès and S. Mimram, "Asynchronous games: Innocence without alternation," in *CONCUR 2007 - Concurrency Theory, 18th International Conference*, ser. Lecture Notes in Computer Science, L. Caires and V. T. Vasconcelos, Eds., vol. 4703. Springer, 2007, pp. 395–411.

[40] S. Castellan, P. Clairambault, S. Rideau, and G. Winskel, "Games and strategies as event structures," *Log. Methods Comput. Sci.*, vol. 13, no. 3, 2017.

[41] V. Danos, "La logique linéaire appliquée à l'étude de divers processus de normalisation (principalement du lambda-calcul)," Ph.D. dissertation, Université Paris 7, France, 1990.

[42] J. Girard, "Locus solum: From the rules of logic to the logic of rules," *Math. Struct. Comput. Sci.*, vol. 11, no. 3, pp. 301–506, 2001.

[43] P. Wadler, "Propositions as sessions," *J. Funct. Program.*, vol. 24, no. 2-3, pp. 384–418, 2014. [Online]. Available: https://doi.org/10.1017/S095679681400001X

[44] D. Sangiorgi, "Locality and interleaving semantics in calculi for mobile processes," *Theor. Comput. Sci.*, vol. 155, no. 1, pp. 39–83, 1996.
# APPENDIX A
## LIST OF NOTATIONS

The following tables summarise the notations (for encodings, equivalence etc.) used in this paper. Some of the notations are only used in Appendix.

### Encodings

<table><tr><td>A</td><td>Abstract encoding</td><td>Figure 1</td></tr><tr><td>A<sub>I0</sub></td><td>A instantiated with I-O wires</td><td>Section VII</td></tr><tr><td>A<sub>0I</sub></td><td>A instantiated with O-I wires</td><td>Section VII</td></tr><tr><td>A<sub>P</sub></td><td>A instantiated with P wires</td><td>Section VIII</td></tr><tr><td>O</td><td>(Abstract) Optimised encoding</td><td>Figure 2</td></tr><tr><td>O<sup>n</sup></td><td>'Optimised encoding of arguments'</td><td>Figure 2</td></tr><tr><td>O<sub>I0</sub></td><td>O instantiated with I-O wires</td><td>Section VII</td></tr><tr><td>O<sub>0I</sub></td><td>O instantiated with O-I wires</td><td>Section VII</td></tr><tr><td>O<sub>P</sub></td><td>O instantiated with P wires</td><td>Section VII</td></tr><tr><td>M</td><td>Milner's encoding</td><td>Section IV-A</td></tr><tr><td>E</td><td>Metavariable for encodings</td><td>—</td></tr></table>

### Wires

<table><tr><td>a &leftrightarrow; b&#773;</td><td>(Abstract) Wire</td><td>Definition IV.1</td></tr><tr><td>a &leftrightarrow; b&#773;<sub>I0</sub></td><td>I-O wire</td><td>Section VI</td></tr><tr><td>b &leftrightarrow; a&#773;<sub>0I</sub></td><td>O-I wire</td><td>Section VI</td></tr><tr><td>a &leftrightarrow; b&#773;<sub>P</sub></td><td>P wire</td><td>Section VI</td></tr></table>

### Equivalence and Preorders

<table><tr><td>≈</td><td>Weak bisimilarity for Iπ</td><td>Definition II.3</td></tr><tr><td>~</td><td>Strong bisimilarity for Iπ</td><td>Definition B.2</td></tr><tr><td>~<sub>~</sub></td><td>Expansion relation for Iπ</td><td>Definition ??</td></tr><tr><td>≡</td><td>Structural congruence for Iπ</td><td>Definition B.1</td></tr><tr><td>≡α</td><td>α-equivalence</td><td>Section B.3</td></tr></table>

### λ-trees

<table><tr><td>LT</td><td>Lévy-Longo tree</td><td>Definition II.1</td></tr><tr><td>BT</td><td>Böhm tree</td><td>Definition II.1</td></tr><tr><td>BT<sub>η∞</sub></td><td>Böhm tree up-to infinite η-expansion</td><td>Section B.1</td></tr></table>

### Reduction of λ-calculus

<table><tr><td>→</td><td>β-reduction</td><td>Section II-A</td></tr><tr><td>→<sub>sn</sub></td><td>strong call-by-name reduction</td><td>Section II-A</td></tr><tr><td>→<sub>h</sub></td><td>head reduction</td><td>Section II-A</td></tr></table>

# APPENDIX B
## SUPPLEMENTARY MATERIALS FOR BACKGROUND

This section provides additional background material for Section II. These include the labelled transition system of Iπ, (full) definition of ~, and the details of the proof techniques.

### 1. Böhm trees up-to Infinite η-expansion

We present the Böhm trees up-to infinite η-expansion because, in the main-part of the paper, we only introduced the equality over BT<sub>η∞</sub>s.

Informally, BT<sub>η∞</sub>(M), is defined coinductively by

1) $\mathrm{BT}_{\eta\infty}(M) = \perp$ if $M$ is unsolvable, and

2) if $M \implies_h \lambda x_1 \dots x_n \cdot y M_1 \dots M_n$, then

a) $\mathrm{BT}_{\eta\infty}(M) = \mathrm{BT}_{\eta\infty}(\lambda x_1 \dots x_{n-1} \cdot y M_1 \dots M_{n-1})$, if $x_n \notin \mathrm{fv}(y M_1 \dots M_{n-1})$ and $\mathrm{BT}_{\eta\infty}(M_n) = \mathrm{BT}_{\eta\infty}(x_n)$; and otherwise

b) $\mathrm{BT}_{\eta\infty}(M) = \lambda x_1 \dots x_n \cdot y \quad \begin{array}{@{}c@{\,}c@{\,}r} & & \\ \diagup & \diagdown & \mathrm{BT}_{\eta\infty}(M_1) \dots \mathrm{BT}_{\eta\infty}(M_n) \end{array}$

The similarity between the definition of $\mathrm{BT}_{\eta\infty}$ and $\mathrm{BT}_{\eta\infty}$-bisimilarity should be clear. A $\mathrm{BT}_{\eta\infty}$-bisimulation is a relation that relates the children of the trees of $\mathrm{BT}_{\eta\infty}(M)$ and $\mathrm{BT}_{\eta\infty}(N)$ according to the above definition of the tree.

Example B.1. Recall $Jz$, the ‘infinite η-expansion of z’, that we used in Example II.2. The BT and $\mathrm{BT}_{\eta\infty}$ of $Jz$ are

$$ \mathrm{BT}(Jz) = \begin{array}{@{}c@{\,}c@{\,}r} & \lambda z_1 \cdot z & \\ | & \lambda z_2 \cdot z_1 & \\ \vdots & \lambda z_3 \cdot z_2 & \\ & \vdots & \end{array} \qquad \mathrm{BT}_{\eta\infty}(Jz) = z. $$

For each term $M$ used in Example II.1, we have $\mathrm{BT}_{\eta\infty}(M) = \mathrm{BT}(M)$.

### 2. LTS

In Figure 3, we report the standard labelled transition system (LTS) of Iπ. In the LTS, transitions are of the form $P \xrightarrow{\mu} P'$, where the set of actions is given by

$$ \mu ::= a(\tilde{b}) | \bar{a}(\tilde{b}) | \tau $$

and bound names of $\mu$ are fresh, i.e., they do not appear free in $P$. The meanings of the actions are as usual: $a(\tilde{b})$ and $\bar{a}(\tilde{b})$ are bound input and outputs, respectively, and $\tau$ is the internal action. The co-action $\bar{\mu}$ of $\mu$ used in the rule com is defined by $\bar{a}(\tilde{b}) \stackrel{\mathrm{def}}{=} \bar{a}(\tilde{b})$ and $\bar{a}(\tilde{b}) \stackrel{\mathrm{def}}{=} a(\tilde{b})$. Since we are using the Barendregt convention, in par, we have an implicit side condition $\mathrm{bn}(\mu) \cap \mathrm{fn}(Q) = \emptyset$. We use = for ‘syntactic identity modulo α-conversion’, and thus $(\tilde{y}) Q = (\bar{x}) P$ in the premise of rule com merely means that the two agents are equal up-to α-conversion.

When reasoning behaviours of agents it is useful to assume that all the expressions are normalised. An application redex $((\tilde{x})P)\langle\bar{a}\rangle$ can be normalised as $P\{\tilde{a}/\bar{x}\}$. An agent is normalised if all such application redexes have been contracted. Thus, in the paper, we identify an agent with its normalised expression.

### 3. Relations on processes

Here we state the definition of structural congruence and strong bisimilarity.

**Definition B.1** (Structural congruence). The structural congruence $\equiv$ is the smallest congruence relation over processes that includes the α-equivalence and the following equivalence:

$$ \begin{array}{l} P \mid \mathbf{0} \equiv P \qquad P \mid Q \equiv Q \qquad P \mid (P \mid Q) \mid R \equiv P \mid (Q \mid R) \\ \qquad \nu x \nu y P \equiv \nu y \nu x P \quad (x \neq y) \\ \qquad \nu x (P \mid Q) \equiv \nu x P \mid Q \quad (x \notin \mathrm{fv}(Q)). \end{array} $$

We also write $\equiv_α$ for α-equivalence, and will use this notation when we want to clarify that the processes are equal only modulo the renaming of bound variables.
<figure><img src="image_2.png" /><figcaption>Fig. 3. The standard LTS for $I_\pi$.</figcaption></figure>

As usual, the strong bisimilarity is a bisimilarity, in which the matching transitions are strong transitions.

**Definition B.2 (Strong bisimilarity).** A symmetric relation $\mathcal{R}$ on $I_\pi$-processes is a strong bisimulation, if whenever $P\mathcal{R}Q$ and $P \xrightarrow{\mu} P'$, then $Q \xrightarrow{\mu} Q'$ for some $Q'$ with $P'\mathcal{R}Q'$.

Processes $P$ and $Q$ are strongly bisimilar, written $P \sim Q$, if $P\mathcal{R}Q$ for some strong bisimulation $\mathcal{R}$.

We summarise the inclusion order between the process relations that we use:

$$ \equiv \subsetneq \sim \subsetneq \leq \approx. $$

In $I_\pi$, all the relations above are (pre)congruences.

## 4. Details of the proof techniques

### Laws for private replications:

**Lemma B.1.** Suppose $x$ only occurs free in $P$, $Q$ and $R$ only in output subject position. Then we have

1) $\nu x (Q | R | !x(p).P) \sim \nu x (Q | !x(p).P) | \nu x (R | !x(p).P)$;

2) $\nu x (\pi.Q | !x(p).P) \sim \pi.\nu x (Q | !x(p).P)$, if $\pi$ is a non-replicated prefix, subject of $\pi$ is not $x$ and $\text{bn}(\pi) \cap \text{fn}(!x(p).P) = \emptyset$;

3) $\nu x (!y(q).Q | !x(p).P) \sim !y(q).\nu x (Q | !x(p).P)$;

4) $\nu x (Q | !x(p).P) \sim Q$, if $x \notin \text{fn}(Q)$;

5) $\nu x (\bar{x}(p).Q | !x(p).P) \gtrsim \nu x (Q | P | !x(p).P)$.

We often call the law (4) the ‘garbage collection law’.

**Up-to techniques:** Our main up-to technique will be up-to context and expansion [44], which admits the use of contexts and of behavioural equivalences such as expansion to achieve the closure of a relation in the bisimulation game.

**Definition B.3 (Bisimulation up-to context and $\lesssim$).** A symmetric relation $\mathcal{R}$ on $I_\pi$-processes is a bisimulation up-to context and up-to $\lesssim$ if $P\mathcal{R}Q$ and $P \xrightarrow{\mu} P''$ imply that there are a (possibly multi-hole) context $C$ and processes $\tilde{P}'$ and $\tilde{Q}'$ such that $P'' \gtrsim C[\tilde{P}']$, $Q \xrightarrow{\mu} \gtrsim C[\tilde{Q}']$ and $\tilde{P}'\mathcal{R}\tilde{Q}'$. Here $\tilde{P}'\mathcal{R}\tilde{Q}'$ means $P'_i\mathcal{R}Q'_i$ for each component.

A special instance of this technique is the up-to expansion technique where the common context $C$ is taken as the empty-context.

**Theorem B.2.** If $\mathcal{R}$ is a bisimulation up-to context and expansion then $\mathcal{R} \subseteq \approx$.

We refer the readers to [44] for the proof. We also use the technique of expansion up-to context and $\lesssim$, which is defined analogously to Definition B.3, as a proof technique to prove expansion results (the main difference is that one now requires $P'' \lesssim C[\tilde{P}']$).

# APPENDIX C

## SOME PROPERTIES OF PERMEABLE PREFIXES

We introduce some algebraic laws for permeable prefixes since they allow us to avoid desugaring while proving the properties of the encodings. Lemma C.1 expresses a property of a restricted interaction consuming permeable prefixes. Lemma C.2 shows two structural laws for permeable prefixes, one concerning restriction, the other concerning parallel composition; in what follows we will use these structural rules without explicitly mentioning Lemma C.2.

### Lemma C.1.

1) $\nu p (p(x, q): P | \bar{p}(x, q): Q) \gtrsim P | Q$ if either $P$ is I-respectful with $q \leftrightarrow \bar{q}'$ and O-respectful with $x' \leftrightarrow \bar{x}$ or $P$ is O-respectful with $q \leftrightarrow \bar{q}'$ and I-respectful with $x' \leftrightarrow \bar{x}$.

2) $\nu x (!x(p).P | \bar{x}(p): Q | R) \gtrsim \nu x (!x(p).P | P | Q | R)$ if $p \notin \text{fn}(R)$, $x$ does not appear in an input subject position of $P, Q, R$ and either $P$ is I-respectful with $p \leftrightarrow \bar{p}'$ or $Q$ is O-respectful with $p' \leftrightarrow \bar{p}$.

### Lemma C.2.

1) If $a \neq b$ and $a \notin \tilde{c}$ then $\nu a b(\tilde{c}): P \equiv b(\tilde{c}): \nu a P$ and $\nu a \tilde{b}(\tilde{c}): P \equiv \tilde{b}(\tilde{c}): \nu a P$

2) If $\tilde{b} \cap \text{fn}(Q) = \emptyset$ then $Q | a(\tilde{b}): P \equiv a(\tilde{b}): (Q | P)$ and $Q | \bar{a}(\tilde{b}): P \equiv \bar{a}(\tilde{b}): (Q | P)$.

Most of the wire properties of Definition IV.1 are not used to prove the above lemmas, which simply follow from the syntactic definition of the permeable prefixes. The only exception is the transitivity of wires, used in the proofs of Lemma C.1.

# APPENDIX D

## PROOFS OF SECTION IV

We present the proofs for the properties of the abstract encoding $\mathcal{A}$ that have been omitted. The main goal of this
section is to prove that $\mathcal{A}$ validates $\beta$-reduction (Theorem IV.3). To simplify the notation, we often write $\llbracket - \rrbracket$ for $\mathcal{A}\llbracket - \rrbracket$ in the proofs.

**Lemma IV.1.**

1) $\nu q (p \leftrightarrow \bar{q} | \mathcal{A}\llbracket M \rrbracket_q) \gtrsim \mathcal{A}\llbracket M \rrbracket_p$

2) $\nu x (x \leftrightarrow \bar{y} | \mathcal{A}\llbracket M \rrbracket_p) \gtrsim \mathcal{A}\llbracket M\{y/x\} \rrbracket_p$

*Proof.* We prove 1 and 2 simultaneously by induction on the structure of $M$.

**Case M = x:** We begin with the case of location names.

$$
\begin{align*}
\nu p (\llbracket x \rrbracket_p | q \leftrightarrow \bar{p}) \\
&= \nu p (\bar{x}(p')): p \leftrightarrow \bar{p}' | q \leftrightarrow \bar{p}) \\
&\equiv \bar{x}(p') : \nu p (p \leftrightarrow \bar{p}' | q \leftrightarrow \bar{p}) \\
&\gtrsim \bar{x}(p') : q \leftrightarrow \bar{p}' \tag{3 of Definition IV.1} \\
&= \llbracket x \rrbracket_q
\end{align*}
$$

Next we show that $\nu x (\llbracket M \rrbracket_p | x \leftrightarrow \bar{y}) = \llbracket M\{y/x\} \rrbracket_p$ holds when $M$ is a variable. First, we consider the case where $M = z \neq x$. Since $x \leftrightarrow \bar{y}$ is of the form $!x(p)$. $P$ by 8 of Definition IV.1, it follows that $\nu x (x \leftrightarrow \bar{y}) \sim 0$, and this concludes this case. If $M = x$, then

$$
\begin{align*}
\nu x (\llbracket x \rrbracket_p | x \leftrightarrow \bar{y}) \\
&= \nu x (\bar{x}(p')): p \leftrightarrow \bar{p}' | x \leftrightarrow \bar{y}) \\
&\gtrsim \bar{y}(p') : p \leftrightarrow \bar{p}' \tag{7 of Definition IV.1} \\
&= \llbracket y \rrbracket_p
\end{align*}
$$

The premise of 7 of Definition IV.1 is satisfied because of the transitivity of wires (3 of Definition IV.1).

**Case M = $\lambda x$. N:** We first show that 1 holds. This is a direct consequence of 4 of Definition IV.1.

$$
\begin{align*}
\nu p (\llbracket \lambda x. N \rrbracket_p | q \leftrightarrow \bar{p}) \\
&= \nu p (p(x, r) : \llbracket N \rrbracket_r | q \leftrightarrow \bar{p}) \\
&\gtrsim q(x, r) : \llbracket N \rrbracket_r \\
&\quad (4 \text{ of Definition IV.1 together with the i.h.}) \\
&= \llbracket \lambda x. N \rrbracket_r
\end{align*}
$$

The proof for 2 is a direct consequence of the induction hypothesis, i.e.

$$
\begin{align*}
\nu y (\llbracket \lambda x. N \rrbracket_p | y \leftrightarrow \bar{z})
  &= \nu y (p(x, q) : \llbracket N \rrbracket_q | y \leftrightarrow \bar{z}) \\
  &\equiv p(x, q) : \nu y (\llbracket N \rrbracket_q | y \leftrightarrow \bar{z}) \\
  &\gtrsim p(x, q) : (\llbracket N\{z/y\} \rrbracket_q) \quad \text{(i.h.)} \\
  &= \llbracket (\lambda x. N)\{z/y\} \rrbracket_p
\end{align*}
$$

Here we assumed that $x$, $y$ and $z$ are pairwise distinct; the general case can be proved using $\alpha$-conversion.

**Case M = N L:** The case for location names follows from the transitivity of wires. Observe that

$$
\begin{align*}
\nu p (\bar{r}(x, p')): (&!x(r'). \llbracket L \rrbracket_{r'} | p \leftrightarrow \bar{p}') | q \leftrightarrow \bar{p}) \\
&\equiv (\nu p, x, p')(\bar{r}(x', p''). (x' \leftrightarrow \bar{x} | p' \leftrightarrow \bar{p}'') \\
&\phantom{\equiv (\nu p, x, p'} | !x(r'). \llbracket L \rrbracket_{r'} | p \leftrightarrow \bar{p}' | q \leftrightarrow \bar{p}) \\
&\gtrsim (\nu x, p')(\bar{r}(x', p''). (x' \leftrightarrow \bar{x} | p' \leftrightarrow \bar{p}'') \\
&\phantom{\gtrsim (\nu x, p'} | !x(r'). \llbracket L \rrbracket_{r'} | q \leftrightarrow \bar{p}') \\
&= \bar{r}(x, p'): (\!x(r'). \llbracket L \rrbracket_{r'} | q \leftrightarrow \bar{p}') \tag{3 of Definition IV.1}
\end{align*}
$$

Using this, we get

$$
\begin{align*}
\nu p (\llbracket N L \rrbracket_p | p \leftrightarrow \bar{q}) \\
&\equiv \nu r (\llbracket N \rrbracket_r | \nu p (\bar{r}(x, p')): (\!x(r'). \llbracket L \rrbracket_{r'} | p \leftrightarrow \bar{p}') | q \leftrightarrow \bar{p})) \\
&\gtrsim \nu r (\llbracket N \rrbracket_r | \bar{r}(x, p'): (\!x(r'). \llbracket L \rrbracket_{r'} | q \leftrightarrow \bar{p}')) \\
&= \llbracket N L \rrbracket_q
\end{align*}
$$

The proof for $x \leftrightarrow \bar{y}$ follows from the replication theorem and the induction hypothesis. First, observe that $x \leftrightarrow \bar{y}$ must be of the form $!x(p)$. $P$ because of 8 of Definition IV.1. We, therefore, can apply the replication theorem to $x \leftrightarrow \bar{y}$. Hence, we have

$$
\begin{align*}
\nu x (\!z(p). \llbracket L \rrbracket_p | x \leftrightarrow \bar{y}) \quad \text{(replication theorem)} \\
\gtrsim \!z(p). \llbracket L\{y/x\} \rrbracket_p \quad \text{(i.h.)}
\end{align*}
$$

The claim follows by applying this expansion relation, the replication theorem for parallel composition and the induction hypothesis:

$$
\begin{align*}
\nu x (\llbracket N L \rrbracket_p | x \leftrightarrow \bar{y}) \\
&\equiv (\nu x, r) (\llbracket N \rrbracket_r | \bar{r}(z, p')): (\!z(r'). \llbracket L \rrbracket_{r'} | p \leftrightarrow \bar{p}') | x \leftrightarrow \bar{y}) \\
&\sim \nu r (\nu x (\llbracket N \rrbracket_r | x \leftrightarrow \bar{y}) \\
&\phantom{\sim \nu r (\nu x (\llbracket N \rrbracket_r | x \leftrightarrow \bar{y})} | \bar{r}(z, p')): (\nu x (\!z(r'). \llbracket L \rrbracket_{r'} | x \leftrightarrow \bar{y}) | p \leftrightarrow \bar{p}')) \tag*{(replication theorem)} \\
&\gtrsim \nu r (\llbracket N\{y/x\} \rrbracket_r | \bar{r}(z, p'): (\!z(r'). \llbracket L\{y/x\} \rrbracket_{r'} | p \leftrightarrow \bar{p}')) \tag*{(i.h. and the above expansion relation)} \\
&= \llbracket N\{y/x\} L\{y/x\} \rrbracket_p \\
&= \llbracket (N L)\{y/x\} \rrbracket_p.
\end{align*}
$$

□

**Lemma D.1.** If $x \notin f\nu(M)$, then $\nu x (\mathcal{A}\llbracket x \rrbracket_p | !x(q). \mathcal{A}\llbracket M \rrbracket_q) \gtrsim \mathcal{A}\llbracket M \rrbracket_p$

*Proof.*

$$
\begin{align*}
\nu x (\llbracket x \rrbracket_p | !x(q). \llbracket M \rrbracket_q) \\
&= \nu x (\bar{x}(p')): p \leftrightarrow \bar{p}' | !x(q). \llbracket M \rrbracket_q) \\
&\gtrsim \nu p' (p \leftrightarrow \bar{p}' | \llbracket N \rrbracket_{p'}) \\
&\quad \text{(reduction, i.e. Lemma C.1, and garbage collection on $x$)} \\
&\gtrsim \llbracket M \rrbracket_p. \tag*{(Lemma IV.1)}
\end{align*}
$$

□
**Lemma IV.2.** If $x \notin \text{fv}(N)$, then
$$ \nu x (A[[M]]_p | !x(q). A[[N]]_q) \gtrsim A[[M\{N/x\}]_p $$

*Proof.* By induction on the structure of $M$ using the replication theorem. The base case is Lemma D.1; if $x \notin \text{fv}(M)$, then we just need to apply the garbage collection law. The case $M = \lambda x. M'$ is a straightforward consequence of the induction hypothesis. It is the case where $M = M_1 M_2$ that needs the replication theorem. If $M = M_1 M_2$, we have

$$
\begin{align*}
\nu x ([[M_1 M_2]]_p | !x(q). [[N]]_q) \\
&\equiv (\nu x, q) (([M_1]]_q | \bar{q}(y, p')): (!y(r). [[M_2]]_r | p \leftrightarrow \bar{p}') \\
&\phantom{\equiv} | !x(q). [[N]]_q) \\
&\sim \nu q (\nu x ([[M_1]]_q | !x(q). [[N]]_q) | \\
&\phantom{\sim \nu q (\nu x ([[M_1]]_q | !x(q. [[N]]_q) | p \leftrightarrow \bar{p}'))} \bar{q}(y, p'): (\nu x (!y(r). [[M_2]]_r | !x(q). [[N]]_q) | p \leftrightarrow \bar{p}')) \\
&\phantom{\sim \nu q (\nu x ([[M_1]]_q | !x(q. [[N]]_q) | p \leftrightarrow \bar{p}'))} \text{(replication theorem for parallel composition)} \\
&\sim \nu q (\nu x ([[M_1]]_q | !x(q). [[N]]_q) | \\
&\phantom{\sim \nu q (\nu x ([[M_1]]_q | !x(q. [[N]]_q) | p \leftrightarrow \bar{p}'))} \bar{q}(y, p'): (!y(r). \nu x ([[M_2]]_r | !x(q). [[N]]_q) | p \leftrightarrow \bar{p}')) \\
&\phantom{\sim \nu q (\nu x ([[M_1]]_q | !x(q. [[N]]_q) | p \leftrightarrow \bar{p}'))} \text{(replication theorem for replicated input)} \\
&\gtrsim \nu q ([[M_1\{N/x\}]_q | \bar{q}(y, p'): (!y(r). [[M_2\{N/x\}]_r | p \leftrightarrow \bar{p}'))) \\
&\phantom{\gtrsim \nu q ([[M_1\{N/x\}]_q | \bar{q}(y, p'): (!y(r). [[M_2\{N/x\}]_r | p \leftrightarrow \bar{p}')))} \text{(i.h.)} \\
&= [[(M_1 M_2)\{N/x\}]_p]
\end{align*}
$$

**Theorem IV.3.** If $M \to N$, then $A[[M]]_p \gtrsim A[[N]]_p$.

*Proof.* It suffices to show that $\llbracket (\lambda x. M) N \rrbracket_p \gtrsim \llbracket M\{N/x\} \rrbracket_p$ because the other cases follow from the precongruence of $\gtrsim$. We have

$$
\begin{align*}
\llbracket (\lambda x. M) N \rrbracket_p \\
&= \nu q (q(x, r): [[M]]_r | \bar{q}(y, p'): (!y(r'). [[N]]_{r'} | p \leftrightarrow \bar{p}')) \\
&\qquad (q \text{ is fresh}) \\
&\gtrsim (\nu y, p') (\llbracket M\{y/x\} \rrbracket_{p'} | !y(r'). \llbracket N \rrbracket_{r'} | p \leftrightarrow \bar{p}') \\
&\qquad \text{(Lemma C.1 and IV.1)} \\
&\gtrsim \nu y (\llbracket M\{y/x\} \rrbracket_p | !y(r'). \llbracket N \rrbracket_{r'}) \\
&\qquad \text{(Lemma IV.1)} \\
&\gtrsim \llbracket M\{N/x\} \rrbracket_p \\
&\qquad \text{(Lemma IV.2)}
\end{align*}
$$

as desired.

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

# APPENDIX E
PROOFS FOR SECTION V

We present the proofs of properties of the abstract optimised encoding $\mathcal{O}$.

## 1. Proofs for the basic properties of $\mathcal{O}$

This section first proves the properties of $\mathcal{O}$ that are analogous to those for the unoptimised encoding $\mathcal{A}$. Then, using these properties, we prove that $\mathcal{O}$ is indeed an optimisation of $\mathcal{A}$.

Lemma E.1 and E.2 say that $\mathcal{O}[[M]]_p$ and $\mathcal{O}^n\langle p_0, p, \mathcal{O}[[M_1]] \cdots \mathcal{O}[[M_n]] \rangle$ are respectful.

### Lemma E.1.

$1) \nu q (p \leftrightarrow \bar{q} | \mathcal{O}[[M]]_q) \gtrsim \mathcal{O}[[M]]_p.$

$2) \nu x (x \leftrightarrow \bar{y} | \mathcal{O}[[M]]_p) \gtrsim \mathcal{O}[[M\{y/x\}]_p].$

*Proof.* Similar to Lemma IV.1

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

**Lemma E.2.** For $n \ge 1$, we have

$$
\begin{align*}
\nu p_0 (p_0 \leftrightarrow \bar{q} | \mathcal{O}^n \langle p_0, p, \mathcal{O}[M_1], \dots, \mathcal{O}[M_n] \rangle) \\
\gtrsim \mathcal{O}^n \langle q, p, \mathcal{O}[M_1], \dots, \mathcal{O}[M_n] \rangle.
\end{align*}
$$

*Proof.* By induction on $n$. First observe that

$$ \nu y (x \leftrightarrow \bar{y} | !y(p). \mathcal{O}[[M]]_p) \gtrsim !x(p). \mathcal{O}[[M]]_p \quad (2) $$

under the assumption that $y \notin \text{fv}(M)$. This is derived from 6 of Definition IV.1 together with Lemma E.1.

The base case is the case where $n = 1$. In this case, we need to show

$$
\begin{align*}
\nu p_0 (p_0 \leftrightarrow \bar{q} | \bar{p}_0(x_1, p_1): (!x_1(r_1). \mathcal{O}[[M_1]]_{r_1} | p \leftrightarrow \bar{p}_1)) \\
\gtrsim \bar{q}(x_1, p_1): (!x_1(r_1). \mathcal{O}[[M_1]]_{r_1} | p \leftrightarrow \bar{p}_1).
\end{align*}
$$

Using (2) and the transitivity of wires, we derive the expansion by applying 5 of Definition IV.1.

Now we consider the case $n \ge 1$. We apply 5 of Definition IV.1. The premise of this law is satisfied because of (2) and the induction hypothesis.

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

We now prove that the optimised encoding validates $\beta$-reduction.

**Lemma E.3.** Let $m, n \ge 0$. Then

$$
\begin{align*}
\nu q (\mathcal{O}^m \langle p, q, \mathcal{O}[M_1], \dots, \mathcal{O}[M_m] \rangle \\
\phantom{\nu q (\mathcal{O}^m \langle p, q, \mathcal{O}[M_1], \dots, \mathcal{O}[M_m] \rangle} | \mathcal{O}^n \langle q, r, \mathcal{O}[N_1], \dots, \mathcal{O}[N_n] \rangle) \\
\phantom{\nu q (\mathcal{O}^m \langle p, q, \mathcal{O}[M_1], \dots, \mathcal{O}[M_m] \rangle} \gtrsim \mathcal{O}^{m+n} \langle p, r, \mathcal{O}[M_1], \dots, \mathcal{O}[M_m], \mathcal{O}[N_1], \dots, \mathcal{O}[N_n] \rangle.
\end{align*}
$$

*Proof.* Follows from Lemma E.2.

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

**Lemma E.4.** Suppose that $x \notin \text{fv}(N)$. Then $\nu x (\mathcal{O}[[M]]_p | !x(q). \mathcal{O}[[N]]_q) \gtrsim \mathcal{O}[[M\{N/x\}]_p$

*Proof.* By induction on the structure of $M$. The proof is similar to that of the unoptimised case (Lemma IV.2). Indeed the proof for the base case, namely the case $M = x$, is exactly the same as that of Lemma D.1 since $\mathcal{O}[[x]]_p = \mathcal{A}[[x]]_p$. The inductive case follows from the induction hypothesis and the replication theorems.

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

**Lemma E.5.** If $n \ge 1$, then

$$
\begin{align*}
\nu q (\mathcal{O}[M_0]_q | \mathcal{O}^n \langle q, p, \mathcal{O}[M_1], \dots, \mathcal{O}[M_n] \rangle) \\
\gtrsim \mathcal{O}[M_0 M_1 \cdots M_n]_p.
\end{align*}
$$

*Proof.* Case $M_0 = x$: This case follows from Lemma E.2. More precisely, we have

$$
\begin{align*}
\nu q (\mathcal{O}[x]_q | \mathcal{O}^n \langle q, p, \mathcal{O}[M_1], \dots, \mathcal{O}[M_n] \rangle) \\
&= \nu q (\bar{x}(q'): q \leftrightarrow \bar{q}' | \mathcal{O}^n \langle q, p, \mathcal{O}[M_1], \dots, \mathcal{O}[M_n] \rangle) \\
&\equiv \bar{x}(q'): \nu q (q \leftrightarrow \bar{q}' | \mathcal{O}^n \langle q, p, \mathcal{O}[M_1], \dots, \mathcal{O}[M_n] \rangle) \\
&\gtrsim \bar{x}(q'): \mathcal{O}^n \langle q', p, \mathcal{O}[M_1], \dots, \mathcal{O}[M_n] \rangle. \quad (\text{Lemma E.2}) \\
&= \mathcal{O}[x M_1 \cdots M_n]_p.
\end{align*}
$$
$$
\begin{align*}
&\gtrsim (\nu x_1, p_1) (\mathcal{O}[\mathcal{M}_0\{x_1/x\}]_q | !x_1(r_1). \mathcal{O}[\mathcal{M}_1]_{p_1} \\
&\phantom{\gtrsim (\nu x_1, p_1) (\mathcal{O}[\mathcal{M}_0\{x_1/x\}]_q |} | \bar{p}_1(x_2, p_2): \dots \bar{p}_{n-1}(x_n, p_n): \\
&\phantom{\gtrsim (\nu x_1, p_1) (\mathcal{O}[\mathcal{M}_0\{x_1/x\}]_q |} (!x_2(r_2). \mathcal{O}[\mathcal{M}_2]_{p_2} | \dots \\
&\phantom{\gtrsim (\nu x_1, p_1) (\mathcal{O}[\mathcal{M}_0\{x_1/x\}]_q |} | !x_n(r_1). \mathcal{O}[\mathcal{M}_n]_{r_n} | p \leftrightarrow \bar{p}_n)) \tag{Lemma C.1}
\end{align*}
$$

$$
\begin{align*}
&\gtrsim \nu p_1 (\mathcal{O}[M_0\{M_1/x\}]_{p_1} \\
&\phantom{\gtrsim \nu p_1 (\mathcal{O}[M_0\{M_1/x\}]_{p_1} } | \bar{p}_1(x_2, p_2): \cdots \bar{p}_{n-1}(x_n, p_n): \\
&\phantom{\gtrsim \nu p_1 (\mathcal{O}[M_0\{M_1/x\}]_{p_1} } (!x_2(r_2). \mathcal{O}[M_2]_{r_2} | \cdots | !x_n(r_1). \mathcal{O}[M_n]_{r_n} | p \leftrightarrow \bar{p}_n)) \tag{Lemma E.4}
\end{align*}
$$

If $n \ge 2$, we can apply Lemma E.5 and obtain $P \gtrsim \mathcal{O}[M_0\{M_1/x\} M_2 \cdots M_n]_p$. If $n=1$, the subprocess of the form $\bar{p}_1(x_2, p_2) : \cdots$ is simply $p \leftrightarrow \bar{p}_1$. Hence, by Lemma E.1, we have

$$
\begin{align*}
\mathcal{O}[(\lambda x. M_0) M_1]_p &\gtrsim \nu p_1 (\mathcal{O}[M_0\{M_1/x\}]_{p_1} | p \leftrightarrow \bar{p}_1) \\
&\gtrsim \mathcal{O}[M_0\{M_1/x\}]_{p_1}
\end{align*}
$$

as desired.

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

The next thing we prove is the property about input
actions.

**Lemma V.3.** If $\mathcal{O}[M]_p \xrightarrow{\mu} P$ and $\mu$ is an input action, then $\mu$ is an input at $p$.

*Proof.* By induction on $M$ with a case analysis on the shape of $M$.

**Case M = x:** In this case, $\mathcal{O}[M]_p = \bar{x}(p') : p \leftrightarrow \bar{p}'$. Since the only free name that appears in an input occurrence is $p$ (because of 1 of Definition IV.1), the only possible input action $\mathcal{O}[M]_p$ can do is an input on $p$. (Note that whether the process can do an input on $p$ will depend on the concrete instantiation of $p \leftrightarrow \bar{q}$.)

**Case M = λx. M₀:** Since $\mathcal{O}[M]_p = p(x, q): \mathcal{O}[M_0]_q$, if $\mathcal{O}[M]_p \xrightarrow{\mu} P$ and $\mu$ is an input action, then this action must either be an input on $p$ or an input that originates from $\mathcal{O}[M_0]_q$. In the latter case, $\mu$ must be an input on $q$ by the induction hypothesis. Since $q$ is bound by $p(x, q)$, this action cannot induce an input action of $\mathcal{O}[M]_p$.

**Case M = x M₁ ... Mₙ:** In this case, $\mathcal{O}[M]_p$ is

$$
\begin{align*}
\bar{x}(p_0) : \bar{p}_0(x_1, p_1) : \dots &\bar{p}_{n-1}(x_n, p_n) \\
(\!x_1(r_1). \mathcal{O}[M_1]_{r_1} | \dots | &\!x_n(r_n). \mathcal{O}[M_n]_{r_n} | p \leftrightarrow \bar{p}_n)
\end{align*}
$$

Since the only free name that may appear in an input
occurrence which is not guarded by a (non-permeable)
prefixing is $p$, the only possible input action $\mathcal{O}[M]_p$ can
do is an input on $p$.

**Case M = (λx. M₀) M₁ ... Mₙ:** By combining the argument we made in the previous two cases. □

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

We now consider the relationship between output ac-
tions and head normal forms. As an auxiliary definition,
we introduce a special form of a context.

**Definition E.1.** *H-contexts* are contexts defined by the
following grammar:

$$
H ::= [\cdot] | (\lambda x. H) M_1 \cdots M_n \quad (n \ge 0)
$$

**Lemma E.7.** Let $M \stackrel{\text{def}}{=} H[x \tilde{M}]$, where $\tilde{M}$ is a possibly empty sequence of terms, and assume that $x \in \text{fv}(M)$. Then $M \implies_h \lambda \tilde{y} \cdot x \tilde{N}$ for some possibly empty sequences of variables $\tilde{y}$ and terms $\tilde{N}$.

**Lemma E.8.** Let $M$ be a $\lambda$-term and suppose that $\mathcal{O}[M]_p \xrightarrow{\mu} P$ for an output action $\mu$. Then the action $\mu$ must be of the form $\bar{x}(p)$ for a fresh $p$ and a variable $x \in \text{fv}(M)$, and there exists a H-context $H$ such that $H[x \tilde{M}] = M$ for some possibly empty sequence $\tilde{M} = M_1, \dots, M_n$.

*Proof.* By induction on $M$ with a case analysis on the
shape of $M$.

**Case M = x:** In this case, $\mathcal{O}[M]_p = \bar{x}(p') : p \leftrightarrow \bar{p}'$, and the only output action $\mathcal{O}[M]_p$ can do is $\bar{x}(p')$ (cf. 1 of Definition IV.1). We can take the empty context $[\cdot]$ for $H$ and the empty sequence for $\tilde{M}$.

**Case M = λx. M₀:** Since we have $\mathcal{O}[M]_p = p(x, q): \mathcal{O}[M_0]_q$, if $\mathcal{O}[M]_p \xrightarrow{\bar{y}(r)} P$ then this action must originate from $\mathcal{O}[M_0]_q$ and we must have $x \neq y$. Hence, by the induction hypothesis, there is a H-context $H'$ and a sequence of terms $\tilde{M}$ such that $M_0 = H'[y \tilde{M}]$ with $y \in \text{fv}(M_0)$. We can take $H$ as $\lambda x. H'$, and since $y \neq x$ we also have $y \in \text{fv}(M)$.

**Case M = x M₁ ... Mₙ:** In this case, $\mathcal{O}[M]_p$ is

$$
\begin{align*}
\bar{x}(p_0) : \bar{p}_0(x_1, p_1) : \dots & \bar{p}_{n-1}(x_n, p_n) \\
(\!x_1(r_1). \mathcal{O}[M_1]_{r_1} | \dots | \!x_n(r_n). \mathcal{O}[M_n]_{r_n} | p \leftrightarrow \bar{p}_n).
\end{align*}
$$

Obviously, the only output $\mathcal{O}[M]_p$ can do is $\bar{x}(p_0)$. Hence,
the claim holds by taking $H = [\cdot]$ and $\tilde{M} = M_1, \dots, M_n$.

**Case M = (λx. M₀) M₁ ... Mₙ:** Recall that $\mathcal{O}[M]_p$ is

$$
\nu p_0 (p_0(x, q) : \mathcal{O}[M_0]_q | \\
\phantom{\nu p_0 (p_0(x, q) : \mathcal{O}[M_0]_q |} | \bar{p}_0(x_1, p_1) : \cdots \bar{p}_{n-1}(x_n, p_n) : \\
\phantom{\nu p_0 (p_0(x, q) : \mathcal{O}[M_0]_q |} (!x_1(r_1). \mathcal{O}[M_1]_{r_1} | \cdots | !x_n(r_n). \mathcal{O}[M_n]_{r_n} | p \leftrightarrow \bar{p}_n))
$$

If $\mathcal{O}[M]_p$ does an output action, then this action must originate from $\mathcal{O}[M_0]_q$ and the subject of the action must be different from $x$. Assume that $\mathcal{O}[M_0]_q \xrightarrow{\mu} P'$ for an output action $\mu$ whose subject is not $x$. By the induction hypothesis, $\mu = \bar{y}(r)$ and there is a H-context $H'$ and a sequence of terms $\tilde{M}'$ such that $M_0 = H'[y \tilde{M}]$ with $y \in \text{fv}(M_0)$. We can take $H = (\lambda x. H') M_1 \cdots M_n$. Since $M = H[y \tilde{M}]$ and $y \in \text{fv}(M)$ the claim follows. $\square$

**Lemma V.4.** Let $M$ be a $\lambda$-term. If $\mathcal{O}[M]_p \xrightarrow{\bar{x}(q)} P$ for some $P$, then $M$ has a head normal form $\lambda \tilde{y} \cdot x \tilde{M}$, for some (possibly empty) sequence of terms $\tilde{M}$ and variables $\tilde{y}$ with $x \notin \tilde{y}$.

*Proof.* By Lemma E.7 and Lemma E.8. □

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

**Lemma E.9.** Let $M$ be an unsolvable term. Then there does not exist an output action $\mu$ such that $\mathcal{O}[M]_p \xrightarrow{\mu} P$ for some $P$.
**Proof.** Since $M$ is an unsolvable term, by Lemma V.4, $O[M]_p$ cannot do an output action. Hence, if $O[M]_p \stackrel{\mu}{\Rightarrow} P$, where $\stackrel{\mu}{P}$ is an output action, we must have $O[M]_p(\stackrel{\tau}{\Rightarrow}) \stackrel{\mu}{\Rightarrow} P'$ for $n \ge 1$. Assume that such an $n$ exist. Then, by repeatedly applying Lemma V.2, we get $P \gtrsim O[M']_p$ for some term $M'$ such that $M \to^n M'$. Note that $M'$ is also an unsolvable term. However, this is a contradiction since $P \stackrel{\mu}{\Rightarrow} P'$ for an output action $\mu$, but $O[M']_p \stackrel{\not\cong}{\Rightarrow}$ by Lemma V.4. $\square$

# APPENDIX F

## SUPPLEMENTARY MATERIALS FOR SECTION VI

In this section, we prove that the three concrete wires we introduced satisfy the properties of Definition IV.1. As explained in the main text, we first show that the wires are transitive, and then the other laws are proved by algebraic reasoning exploiting the transitivity of wires.

### 1. Proofs for transitivity

We prove that I-O wires, O-I wires and P wires are all transitive. (The transitivity of each type of wires is given as an individual lemma.) The reasoning is similar in all three cases; we use bisimulation up-to context and expansion. The proofs for the I-O wires and O-I wires are essentially the same because of the 'duality', whereas the proof for the P wires is more delicate.

Before giving the proof, we introduce a notation for chains of wires, which will be used in the proofs. Let

$$ \mathrm{chain}_{10}^{n}(p, q) \stackrel{\mathrm{def}}{=} p \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q} $$

$$ \mathrm{chain}_{10}^{n+1}(p, q) \stackrel{\mathrm{def}}{=} \nu r (\mathrm{chain}_{10}^{n}(p, r) \mid r \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}) $$

$$ \mathrm{chain}_{10}^{1}(x, y) \stackrel{\mathrm{def}}{=} x \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{y} $$

$$ \mathrm{chain}_{10}^{n+1}(x, y) \stackrel{\mathrm{def}}{=} \nu z (\mathrm{chain}_{10}^{n}(x, z) \mid z \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{y}) $$

where $r \notin \{p, q\}$ and $z \notin \{x, y\}$. Chains of O-I wires and P wires, denoted by $\mathrm{chain}_{01}^n(a, b)$ and $\mathrm{chain}_P^n(a, b)$, respectively, are defined in similar manners. (Only for the $\mathrm{chain}_{01}^n(p, q)$, we assume that $p$ is an output name and $q$ is an input name so that the 'direction of the chain' becomes from output to input.)

**Lemma F.1.** The wires $p \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}$ and $x \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{y}$ are transitive. That is, we have $\nu q (p \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q} \mid q \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{r}) \gtrsim p \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{r}$ and $\nu y (x \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{y} \mid y \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{z}) \gtrsim x \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{z}$.

**Proof.** We strengthen the statement and prove the transitivity for chains of wires of any length. The relations we consider for the proof are

$$ \begin{aligned} \mathcal{R}_1 \stackrel{\mathrm{def}}{=} & \{ (p_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{p}_n, \mathrm{chain}_{10}^n(p_0, p_n)) \mid n \ge 2 \} \\ \mathcal{R}_2 \stackrel{\mathrm{def}}{=} & \{ (x_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_n, \mathrm{chain}_{10}^n(x_0, x_n)) \mid n \ge 2 \}. \end{aligned} $$

We show that $\mathcal{R}_1 \cup \mathcal{R}_2$ is an expansion up-to $\lesssim$ and context (cf. Section B.4).

We first consider the case for location names. Suppose $p_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{p}_m \in \mathcal{R}_1$ chain$_{10}^m(p_0, p_m)$ for some $m \ge 2$. We only consider the case where the process on the right-hand side makes the challenge; the opposite direction can be proved similarly. There is only one possible actions the process can do, namely an input at $p_0$.

First we prove the following auxiliary statement by induction on $n$.

$$ \begin{array}{l} \text{For any } n \ge 2, \text{ if } \mathrm{chain}_{10}^n(p_0, p_n) \xrightarrow{p_0(x_0, q_0)} P, \\ \text{then } P \gtrsim \bar{p}_n(x_n, q_n) : (\mathrm{chain}_{10}^{2n-1}(x_n, x_0) \mid \\ \qquad \mathrm{chain}_{10}^{2n-1}(q_0, q_n)) \end{array} $$

The base case is $n=2$. Recall that $p_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{p}_1$ and $p_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{p}_0$ are of the form

$$ p_0(x_0, q_0). (\nu x'_1, q'_1) (\overline{p_1}(x_1, q_1). (x_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}'_1 | q'_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}_1) \\ | x_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_0 | q_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}'_1) $$

and

$$ p_1(x_1, q_1). (\nu x'_2, q'_2) (\overline{p_2}(x_2, q_2). (x_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}'_2 | q'_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}_2) \\ | x'_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_1 | q_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}'_2)). $$

Hence the derivative of the transition $\xrightarrow{p_0(x_0, q_0)}$ is

$$ \begin{align*} & (\nu x'_1, q'_1, p_1) \\ & (\overline{p_1}(x_1, q_1). (x_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}'_1 | q'_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}_1) | x'_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_0 | q_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}'_1 \\ & | p_1(x_1, q_1). (\nu x'_2, q'_2) (\overline{p_2}(x_2, q_2). (x_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}'_2 | q'_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}_2) \\ & | x'_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_1 | q_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}'_2)) \\ & \gtrsim (\nu x'_1, x_1, x'_2, q'_1, q'_2) \quad \text{(interaction at } p_1) \\ & (x'_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_1 | x_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}'_1 | x'_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_0 \\ & | q_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}'_1 | q'_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}_1 | q_1 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}'_2 \\ & | \overline{p_2}(x_2, q_2). (x_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}'_2 | q'_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}_2)) \\ & \equiv (\nu x'_2, q'_2) (\mathrm{chain}_{10}^3(x'_2, x_0) | \mathrm{chain}_{10}^3(q_0, q'_2) \\ & | \overline{p_2}(x_2, q_2). (x_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}'_2 | q'_2 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}_2)) \\ & = \bar{p}_2(x_2, q_2) : (\mathrm{chain}_{10}^3(x_2, x_0) | \mathrm{chain}_{10}^3(q_0, q_2)) \end{align*} $$

as desired. The inductive case can be proved similarly.

Hence if $\mathrm{chain}_{10}^m(p_0, p_m) \xrightarrow{p_0(x_0, q_0)} P$, we have $P \gtrsim \bar{p}_m(x_m, q_m) : (\mathrm{chain}_{10}^{2m-1}(x_m, x_0) | \mathrm{chain}_{10}^{2m-1}(q_0, q_m))$. For the matching transition, we pick

$$ p_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{p}_m \xrightarrow{p_0(x_0, q_0)} \bar{p}_m(x_m, q_m) : (x_m \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_0 | q_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}_m). $$

We can take $C \stackrel{\mathrm{def}}{=} \bar{p}_m(x_m, q_m) : (|\cdot| \mid |\cdot|)$ as the common context and conclude this case because $q_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{q}_m \in \mathcal{R}_1$ chain$_{10}^{2m-1}(q_0, q_m)$ and $x_m \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_0 \in \mathcal{R}_2$ chain$_{10}^{2m-1}(x_m, x_0)$.

The case for the variable name is proved similarly. Suppose $x_0 \stackrel{\leftrightarrow}{\xleftarrow{\phantom{0}10}} \bar{x}_m \in \mathcal{R}_2$ chain$_{10}^m(x_0, x_m)$ for some $m \ge 2$. The only action the two processes can do is the input at $x_0$. As in the case for location names, we can show that
For any $n \ge 2$, if $\text{chain}_{10}^n(x_0, x_n) \xrightarrow{x_0(p_0)} P$, then
$P \gtrsim \text{chain}_{10}^n(x_0, x_n) | \bar{x}_n(p_n) : \text{chain}_{10}^{2n-1}(p_0, p_n)$

by induction on $n$. We omit the proof as it is similar to the case for location names; instead of the expansion relation for interactions among linear names, the proof uses replication theorems (the laws (1), (4) and (5) of Lemma B.1). So if $\text{chain}_{10}^m(x_0, x_m) \xrightarrow{x_0(p_0)} P$, we can take $x_0 \leftrightarrow_{10} \bar{x}_m \xrightarrow{x_0(p_0)} x_0 \leftrightarrow_{10} \bar{x}_m | \bar{x}_m(p_m) : p_0 \leftrightarrow_{10} \bar{p}_m$ as the matching transition. We have $P \gtrsim \text{chain}_{10}^n(x_0, x_m) | \bar{x}_m(p_m) : \text{chain}_{10}^{2n-1}(p_0, p_m)$; $x_0 \leftrightarrow_{10} \bar{x}_m \mathcal{R}_2 \text{chain}_{10}^m(x_0, p_m)$; and $p_0 \leftrightarrow_{10} \bar{p}_m \mathcal{R}_1 \text{chain}_{10}^{2n-1}(p_0, p_m)$. We can apply the up-to context technique with the context being $[\cdot] | \bar{x}_m(p_m): [\cdot]$ to conclude the case. $\square$

Now we prove the transitivity for the O-I wires. Since the proof is almost identical to that of the IOwires, we omit the details and only present the key points.

**Lemma F.2.** The wires $q \leftrightarrow_{01} \bar{p}$ and $x \leftrightarrow_{01} \bar{y}$ are transitive. That is, we have $\nu q (q \leftrightarrow_{01} \bar{p} | r \leftrightarrow_{01} \bar{q}) \gtrsim r \leftrightarrow_{01} \bar{p}$ and $\nu y (x \leftrightarrow_{01} \bar{y} | y \leftrightarrow_{01} \bar{z}) \gtrsim x \leftrightarrow_{01} \bar{z}$.

*Proof.* As in the case of the I-O wires, we consider the following relations.

$$ \mathcal{R}_1 \stackrel{\text{def}}{=} \left\{ (p_n \leftrightarrow_{01} \overline{p_0}, \text{chain}_{01}^n(p_0, p_n)) \mid n \ge 2 \right\} $$

$$ \mathcal{R}_2 \stackrel{\text{def}}{=} \left\{ (x_0 \leftrightarrow_{01} \overline{x_n}, \text{chain}_{01}^n(x_0, x_n)) \mid n \ge 2 \right\}. $$

We show that $\mathcal{R}_1 \cup \mathcal{R}_2$ is an expansion up-to $\lesssim$ and context. Observe that $\text{chain}_{01}^n(p_0, p_n)$ and $\text{chain}_{01}^n(x_0, x_n)$ can only do an output at $p_0$ and input at $x_0$, respectively. We can show that, for any $n \ge 2$,

1) if $\text{chain}_{01}^n(p_0, p_n) \xrightarrow{\bar{p}_0(x_0, q_0)} P$, then $P \gtrsim p_n(x_n, q_n) : (\text{chain}_{01}^{2n-1}(x_0, x_n) | \text{chain}_{01}^{2n-1}(q_n, q_0))$

2) if $\text{chain}_{01}^n(x_0, x_n) \xrightarrow{x_0(p_0)} P$, then $P \gtrsim \text{chain}_{01}^n(x_0, x_n) | \bar{x}_n(p_n) : \text{chain}_{01}^{2n-1}(p_n, p_0)$

by induction on $n$.

The rest of the proof follows that of Lemma F.1. $\square$

**Lemma F.3.** The P wires $p \leftrightarrow_{P} \bar{q}$ and $x \leftrightarrow_{P} \bar{y}$ are transitive, that is, $\nu q (p \leftrightarrow_{P} \bar{q} | q \leftrightarrow_{P} \bar{r}) \gtrsim p \leftrightarrow_{P} \bar{r}$ and $\nu y (x \leftrightarrow_{P} \bar{y} | y \leftrightarrow_{P} \bar{z}) \gtrsim x \leftrightarrow_{P} \bar{z}$.

*Proof.* For the proof, we strengthen the statement and prove transitivity for chains of wires of arbitrary length $n$. Let

$$ \mathcal{R}_1 \stackrel{\text{def}}{=} \left\{ (p_0 \leftrightarrow_{P} \bar{p}_n, \text{chain}_P^n(p_0, p_n)) \mid n \ge 2 \right\} $$

$$ \mathcal{R}_2 \stackrel{\text{def}}{=} \left\{ (x_0 \leftrightarrow_{P} \bar{x}_n, \text{chain}_P^n(x_0, x_n)) \mid n \ge 2 \right\} $$

We show that $\mathcal{R}_1 \cup \mathcal{R}_2$ is an expansion up-to $\lesssim$ and context (cf. Section B.4).

Before considering how processes in the relation can match each other's transition, we present some useful

observations that will be used throughout the proof. Recall that $p_i \leftrightarrow_{P} \bar{p}_{i+1}$ is of the form

$$ \begin{aligned} & (\nu x_i^+, q_i^+, x_{i+1}^-, \bar{q}_{i+1}^-) \\ & (p_i(x_i, q_i) \cdot (x_i^+ \leftrightarrow_P \bar{x}_i | q_i \leftrightarrow_P \bar{q}_i^+) \\ & \qquad | \overline{p_{i+1}}(x_{i+1}, q_{i+1}) \cdot (x_{i+1} \leftrightarrow_P \bar{x}_{i+1}^- | q_{i+1}^- \leftrightarrow_P \bar{q}_{i+1}^-) \\ & \qquad | x_{i+1}^- \leftrightarrow_P \bar{x}_i^+ | q_i^+ \leftrightarrow_P \bar{q}_{i+1}^-) \end{aligned} $$

Therefore, given $(\nu p_1, \dots, p_{n-1}) (p_0 \leftrightarrow_P \bar{p}_1 | \dots | p_n \leftrightarrow_P \bar{p}_{n-1})$, reducing the process by executing all the interaction at $p_i$ gives us a process of the form

$$ \begin{aligned} & (\nu x_0^+, x_1^-, x_1, x_1^+, \dots, x_{n-1}^-, x_{n-1}, x_{n-1}^+, \bar{x}_n^-) \\ & (\nu q_0^+, \bar{q}_1^-, q_1, q_1^+, \dots, q_{n-1}^-, q_{n-1}, q_{n-1}^+, \bar{q}_n^-) \\ & (p_0(x_0, q_0) \cdot (x_0^+ \leftrightarrow_P \bar{x}_0 | q_0 \leftrightarrow_P \bar{q}_0^+) \\ & \qquad | \overline{p_n}(x_n, q_n) \cdot (x_n \leftrightarrow_P \bar{x}_n^- | \bar{q}_n^- \leftrightarrow_P \bar{q}_n) \\ & \qquad | q_0^+ \leftrightarrow_P \bar{q}_1^- | q_1^- \leftrightarrow_P \bar{q}_1 | q_1 \leftrightarrow_P \bar{q}_1^+ | \dots \\ & \qquad | q_{n-1}^- \leftrightarrow_P \bar{q}_{n-1}^- | q_{n-1}^- \leftrightarrow_P \bar{q}_{n-1}^- | q_{n-1}^+ \leftrightarrow_P \bar{q}_n^- \\ & \qquad | x_n^- \leftrightarrow_P \bar{x}_{n-1}^+ | x_{n-1}^+ \leftrightarrow_P \bar{x}_{n-1}^- | x_{n-1}^- \leftrightarrow_P \bar{x}_{n-1}^- | \dots \\ & \qquad | x_1^+ \leftrightarrow_P \bar{x}_1 | x_1 \leftrightarrow_P \bar{x}_1^- | x_1^- \leftrightarrow_P \bar{x}_0^+) \end{aligned} $$

Up to structural congruence, the above process can also be written as

$$ \begin{aligned} & (\nu x_0^+, x_n^-) (\nu q_0^+, \bar{q}_n^-) \\ & (p_0(x_0, q_0) \cdot (x_0^+ \leftrightarrow_P \bar{x}_0 | q_0 \leftrightarrow_P \bar{q}_0^-) \\ & \qquad | \overline{p_n}(x_n, q_n) \cdot (x_n \leftrightarrow_P \bar{x}_n^- | \bar{q}_n^- \leftrightarrow_P \bar{q}_n) \\ & \qquad | \text{chain}_P^{3n+1}(q_0^+, \bar{q}_{n+1}^-) | \text{chain}_P^{3n+1}(\bar{x}_{n+1}^-, x_0^+) \\ & \equiv p_0(x_0, q_0) : \bar{p}_{n+1}(x_{n+1}, q_{n+1}) \\ & \qquad (\text{chain}_P^{3n-2}(x_n, x_0) | \text{chain}_P^{3n-2}(q_0, q_n)) \end{aligned} $$

Since the reductions we made are all interactions of linearly used names, for any $n \ge 2$, we have

$$ \begin{aligned} & \text{chain}_P^n(p_0, p_n) \\ & \gtrsim p_0(x_0, q_0) : \bar{p}_n(x_n, q_n) \\ & \qquad (\text{chain}_P^{3n-2}(x_n, x_0) | \text{chain}_P^{3n-2}(q_0, q_n)) \end{aligned} $$

Now we prove that $\mathcal{R}_1 \cup \mathcal{R}_2$ is an expansion up-to expansion and context. We first consider the case where $p_0 \leftrightarrow_P \bar{p}_n \mathcal{R}_1 \text{chain}_P^n(p_0, p_n)$. We only consider the case where the process on the right-hand side makes the challenge; the opposite direction can be proved similarly. There are three possible actions that the process on the left-hand side can make: (1) $\tau$-action, (2) input at $p_0$ and (3) output at $p_{n+1}$. We start by proving the first case. If $(\nu p_1, \dots, p_{n-1}) (p_0 \leftrightarrow_P \bar{p}_1 | \dots | p_{n-1} \leftrightarrow_P \bar{p}_n) \xrightarrow{\tau} P$, then the action must have been caused by an interaction at $p_i$
for some $i$ such that $1 \le i \le n-1$. Since we can execute
the interaction at the remaining $p_i$, we have

$$
P \gtrsim p_0(x_0, q_0): \bar{p}_{n+1}(x_n, q_n):
\quad (\mathrm{chain}_{\mathrm{P}}^{3n-2}(x_n, x_0) | \mathrm{chain}_{\mathrm{P}}^{3n-2}(q_0, q_n)).
$$

For the matching transition we take the 0-step transition,
i.e. the identity relation. Since

$$
\begin{align*}
p_0 \leftrightarrow_P \bar{p}_n \\
&= p_0(x_0, q_0) : \bar{p}_n(x_n, q_n) : (x_n \leftrightarrow_P \bar{x}_0 | q_n \leftrightarrow_P \bar{q}_0); \\
x_n \leftrightarrow_P \bar{x}_0 & \quad \mathrm{chain}_P^{3n-2}(x_n, x_0); \\
q_0 \leftrightarrow_P \bar{q}_n & \quad \mathrm{chain}_P^{3n-2}(q_0, q_n)
\end{align*}
$$

we conclude this case using the up-to expansion and
context technique. Similarly, if

$$
\mathrm{chain}_{\mathrm{P}}^{n}(p_0, p_n) \xrightarrow{p_0(x_0, q_0)} P,
$$

then we can show that

$$
\begin{align*}
P \gtrsim & (\nu x_0^+, q_0^+) (x_0^+ \leftrightarrow_P \bar{x}_0 | q_0 \leftrightarrow_P \bar{q}_0^+ \\
& | \bar{p}_n(x_n, q_n) : (\mathrm{chain}_P^{3n-2}(x_n, x_0^+) \\
& | \mathrm{chain}_P^{3n-2}(q_0^+, q_n))).
\end{align*}
$$

We can match this transition with

$$
\begin{align*}
p_0 \leftrightarrow_P \bar{p}_n \xrightarrow{p_0(x_0, q_0)} \\
& (\nu x_0^+, q_0^+) (x_0^+ \leftrightarrow_P \bar{x}_0 | q_0 \leftrightarrow_P \bar{q}_0^+ | \\
& \qquad \bar{p}_n(x_n, q_n) : (x_n \leftrightarrow_P \bar{x}_0^+ | q_0^+ \leftrightarrow_P \bar{q}_n)).
\end{align*}
$$

Once again, since

$$
\begin{align*}
x_n \leftrightarrow_P \bar{x}_0 & \quad \mathcal{R}_2; \\
q_0 \leftrightarrow_P \bar{q}_n & \quad \mathcal{R}_1 \mathrm{chain}_P^{3n-2}(q_0, q_n)
\end{align*}
$$

we can appeal to the up-to expansion and context tech-
nique to finish this case.

The remaining case (the case where process makes an
output at $p_n$) can be proved by the same reasoning.

Now we prove the case for variable names. Suppose that

$x_0 \leftrightarrow_P \bar{x}_n \mathcal{R}_2 \mathrm{chain}_P^n(x_0, x_n).$

There is only one possible action that the process on the
right-hand side can make: an input at $x_0$. This case is
essentially the same as the that of the other wires. That
is, if

$$
\mathrm{chain}_{\mathrm{P}}^{n}(x_0, x_n) \xrightarrow{x_0(p_0)} P
$$

then we can show that

$$
P \gtrsim \mathrm{chain}_{\mathrm{P}}^{n}(x_0, x_n) | \bar{x}_n(p_n) : \mathrm{chain}_{\mathrm{P}}^{2n-1}(p_0, p_n)
$$

by ‘executing the interactions at $x_i$. This can be matched
by the transition $x_0 \leftrightarrow_P \bar{x}_n \xrightarrow{x_0(p_0)} x_0 \leftrightarrow_P \bar{x}_n | \bar{x}_n(p_n) : p_0 \leftrightarrow_P \bar{p}_n$, and we can conclude by using the up-to context technique. $\square$

2. *Proofs for laws other than transitivity*

We now show the remaining properties holds for all the
three concrete wires. Again, the reasoning is similar in all
the three cases, but not identical.

**Lemma F.4.** The I-O wires $p \underset{10}{\leftrightarrow} \bar{q}$ and $x \underset{10}{\leftrightarrow} \bar{y}$ satisfy the laws of Definition IV.1.

*Proof.* Requirements 1, 2, and 8 hold by definition. Transitivity of the wires has already been proved (Lemma F.1). Hence, we only check the remaining laws.

We start by checking laws 4 and 5. The law 4 holds
because

$$
\begin{align*}
& \nu q (p \underset{10}{\leftrightarrow} \bar{q} | q(x, r) : P) \\
& \quad = (\nu q, x, r) (p(x'', r''). \bar{q}(x', r'): (x' \underset{10}{\leftrightarrow} \bar{x}'' | r'' \underset{10}{\leftrightarrow} \bar{r}') \\
& \qquad \qquad | q(x', r'). (x \underset{10}{\leftrightarrow} \bar{x}' | r' \underset{10}{\leftrightarrow} \bar{r}) | P) \\
& \quad \sim (\nu x, r) (p(x'', r''). \nu q (\bar{q}(x', r'): (x' \underset{10}{\leftrightarrow} \bar{x}'' | r'' \underset{10}{\leftrightarrow} \bar{r}') \\
& \qquad \qquad | q(x', r'). (x \underset{10}{\leftrightarrow} \bar{x}' | r' \underset{10}{\leftrightarrow} \bar{r}) | P) \\
& \quad \gtrsim (\nu x, r) (p(x'', r''). (\nu x', r') (x' \underset{10}{\leftrightarrow} \bar{x}'' | x \underset{10}{\leftrightarrow} \bar{x}' \\
& \qquad \qquad | r'' \underset{10}{\leftrightarrow} \bar{r}' | r' \underset{10}{\leftrightarrow} \bar{r}) | P) \tag{Lemma C.1} \\
& \quad \gtrsim (\nu x, r) (p(x'', r''). (x \underset{10}{\leftrightarrow} \bar{x}'' | r'' \underset{10}{\leftrightarrow} \bar{r}) | P) \\
& \qquad \qquad \qquad \qquad \qquad \qquad \text{(transitivity of wires)} \\
& \quad = p(x, r) : P
\end{align*}
$$

Note that the assumption of Lemma C.1 (interaction of
permeable prefixes) is fulfilled by the transitivity of wires.
Next we consider law 5:

$$
\begin{align*}
& \nu p (p \underset{10}{\leftrightarrow} \bar{q} | \bar{p}(x, r) : P) \\
& \quad = (\nu p, x, r) (p(x', r'). \bar{q}(x'', r'')) : (x'' \underset{10}{\leftrightarrow} \bar{x}' | r' \underset{10}{\leftrightarrow} \bar{r}'') \\
& \qquad \qquad | \bar{p}(x', r'). (x' \underset{10}{\leftrightarrow} \bar{x} | r \underset{10}{\leftrightarrow} \bar{r}') | P) \\
& \quad \gtrsim (\nu x, r, x', r') (\bar{q}(x'', r'')) : (x'' \underset{10}{\leftrightarrow} \bar{x}' | r' \underset{10}{\leftrightarrow} \bar{r}'') \\
& \qquad \qquad | x' \underset{10}{\leftrightarrow} \bar{x} | r \underset{10}{\leftrightarrow} \bar{r}' | P) \tag{Lemma C.1} \\
& \quad \gtrsim (\nu x, r, x', r', x'', r'') (\bar{q}(x''', r''')) : (x''' \underset{10}{\leftrightarrow} \bar{x}'' | r'' \underset{10}{\leftrightarrow} \bar{r}'') \\
& \qquad \qquad | x'' \underset{10}{\leftrightarrow} \bar{x}' | x' \underset{10}{\leftrightarrow} \bar{x} \\
& \qquad \qquad | r' \underset{10}{\leftrightarrow} \bar{r}'' | r \underset{10}{\leftrightarrow} \bar{r}' | P) \\
& \qquad \qquad \qquad \text{(def. of } \bar{q}(x'', r'') : ) \\
& \quad \gtrsim (\nu x, r, x'', r'') (\bar{q}(x''', r''')) : (x''' \underset{10}{\leftrightarrow} \bar{x}'' | r'' \underset{10}{\leftrightarrow} \bar{r}'') \\
& \qquad \qquad | x'' \underset{10}{\leftrightarrow} \bar{x} | r \underset{10}{\leftrightarrow} \bar{r}'' | P) \\
& \qquad \qquad \qquad \text{(transitivity of wires)} \\
& \quad \gtrsim (\nu x'', r'') (\bar{q}(x''', r''')) : (x''' \underset{10}{\leftrightarrow} \bar{x}'' | r'' \underset{10}{\leftrightarrow} \bar{r}'') \\
& \qquad \qquad | P\{x'', r''/x, r\}) \tag{assumption on $P$} \\
& \quad \equiv_{\alpha} (\nu x, r) (\bar{q}(x', r'). (x' \underset{10}{\leftrightarrow} \bar{x} | r \underset{10}{\leftrightarrow} \bar{r}') | P)
\end{align*}
$$
$$= \bar{q}(x, r): P$$

We conclude by checking laws 6 and 7. We have

$$
\begin{align*}
& \nu y (x \underset{10}{\stackrel{\leftrightarrow}{\bar{y}}} | !y(p). P) \\
&= \nu y (!x(p'). \bar{y}(p): p' \underset{10}{\stackrel{\leftrightarrow}{\bar{p}}} | !y(p). P) \\
&\sim !x(p'). \nu y (\bar{y}(p): p' \underset{10}{\stackrel{\leftrightarrow}{\bar{p}}} | !y(p). P) \\
&\geq !x(p'). \nu p (p \underset{10}{\stackrel{\leftrightarrow}{\bar{p}'}}} | P) \\
&\qquad \text{(replication theorem)} \\
&\geq !x(p'). P\{p/p'\} \quad \text{(assumption on P)} \\
&\equiv_{\alpha} !x(p). P
\end{align*}
$$

and

$$
\begin{align*}
& \nu x (x \underset{10}{\stackrel{\leftrightarrow}{\bar{y}}} | \bar{x}(p): P) \\
&\equiv (\nu x, p) (!x(p'). \bar{y}(p')): p' \underset{10}{\stackrel{\leftrightarrow}{\bar{p}''}} | \bar{x}(p'). p \underset{10}{\stackrel{\leftrightarrow}{\bar{p}'}}} | P) \\
&\geq (\nu p, p') (\bar{y}(p')): p' \underset{10}{\stackrel{\leftrightarrow}{\bar{p}''}} | p \underset{10}{\stackrel{\leftrightarrow}{\bar{p}'}}} | P) \\
&\qquad \text{(interaction at $x$ and garbage collection on)} \\
&\geq (\nu p, p', p'') (\bar{y}(p')): p'' \underset{10}{\stackrel{\leftrightarrow}{\bar{p}'''}} | p' \underset{10}{\stackrel{\leftrightarrow}{\bar{p}''}}} | p \underset{10}{\stackrel{\leftrightarrow}{\bar{p}'}}} | P) \\
&\qquad \text{(def. of $\bar{y}(p')$):} \\
&\geq (\nu p, p'') (\bar{y}(p')): p'' \underset{10}{\stackrel{\leftrightarrow}{\bar{p}'''}} | p \underset{10}{\stackrel{\leftrightarrow}{\bar{p}''}}} | P) \\
&\qquad \text{(transitivity of wires)} \\
&\geq \nu p'' (\bar{y}(p')): p'' \underset{10}{\stackrel{\leftrightarrow}{\bar{p}'''}} | P\{p''/p\}) \quad \text{(assumption on P)} \\
&\equiv_{\alpha} \nu p (\bar{y}(p'). p \underset{10}{\stackrel{\leftrightarrow}{\bar{p}'}}} | P) \\
&= \bar{y}(p): P.
\end{align*}
$$

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

The proof for the O-I wires is 'symmetric' to that of the I-O wires.

**Lemma F.5.** The O-I wires $p \underset{01}{\stackrel{\leftrightarrow}{\bar{q}}}$ and $x \underset{01}{\stackrel{\leftrightarrow}{\bar{y}}}$ satisfy the laws of Definition IV.1.

*Proof.* We already proved transitivity in Lemma F.2. The requirement 1 and 8 immediately follow from the definition.

The law 4 holds because

$$
\begin{align*}
& \nu q (p \underset{01}{\stackrel{\leftrightarrow}{\bar{q}}} | q(x, r): P) \\
&= \nu q (p \underset{01}{\stackrel{\leftrightarrow}{\bar{q}}} | (\nu x, r)(q(x', r'). (x \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'}} | r' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}}}) | P)) \\
&\equiv (\nu q, x, r) (\bar{q}(x', r'). p(x'', r'')): (x' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}''}} | r'' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}'}}) \\
&\qquad | q(x', r'). (x \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'}} | r' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}}}) | P) \\
&\geq (\nu x, x', r, r') (p(x'', r'')): (x' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}''}} | r'' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}'}}) \\
&\qquad | x \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'}} | r' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}}} | P) \\
&\qquad \text{(communication on a linear name)}
\end{align*}
$$

$$
\begin{align*}
& \gtrsim (\nu x, x', x'', r, r', r'') \\
& \qquad (p(x''', r'''). (x'' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'''}} | r''' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}''}}) \\
& \qquad | x \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'}} | x' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}''}} | r' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}}} | r'' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}'}} | P) \\
& \qquad \text{(def. of } p(x'', r'')\text{:) } \\
& \gtrsim (\nu x, x'', r, r'') (p(x''', r'''). (x'' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'''}} | r''' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}''}}) \\
& \qquad | x \underset{01}{\stackrel{\leftrightarrow}{\bar{x}''}} | r'' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}}} | P) \\
& \qquad \text{(transitivity of wires)} \\
& \gtrsim (\nu x'', r'') (p(x''', r'''). (x'' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'''}} | r''' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}''}}) \\
& \qquad | P\{x'', r''/x, r\}) \\
& \qquad \text{(assumption on P)} \\
& \equiv_{\alpha} (\nu x, r) (p(x', r'). (x \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'}} | r' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}}}) | P) \\
&= p(x, r): P
\end{align*}
$$

The proof of law 5 is similar to that of 4, but does not use the respectfulness of $P$:

$$
\begin{align*}
& \nu p (p \underset{01}{\stackrel{\leftrightarrow}{\bar{q}}} | \bar{p}(x, r): P) \\
&\equiv (\nu p, x, r) (\bar{q}(x'', r''). p(x', r'): (x'' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'}} | r' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}''}}) \\
& \qquad | \bar{p}(x', r'). (x' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}}} | r \underset{01}{\stackrel{\leftrightarrow}{\bar{r}'}}) | P) \\
&\sim (\nu x, r) (\bar{q}(x'', r''). \nu p (p(x', r'): (x'' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'}} | r' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}''}}) \\
& \qquad | \bar{p}(x', r'). (x' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}}} | r \underset{01}{\stackrel{\leftrightarrow}{\bar{r}'}})) \\
& \qquad | P) \\
&\geq (\nu x, r) (\bar{q}(x'', r''). (\nu x', r') (x'' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}'}} | x' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}}}) \\
& \qquad | r' \underset{01}{\stackrel{\leftrightarrow}{\bar{r}''}} | r \underset{01}{\stackrel{\leftrightarrow}{\bar{r}'}}) | P) \\
& \qquad \text{(Lemma C.1)} \\
& \geq (\nu x, r) (\bar{q}(x'', r''). (x'' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}}} | r \underset{01}{\stackrel{\leftrightarrow}{\bar{r}''}}) | P) \\
& \qquad \text{(transitivity of wires)} \\
&= \bar{q}(x, r): P
\end{align*}
$$

The proofs for laws 6 and 7 are the same as those for I-O wires. Law 6 holds because:

$$
\begin{align*}
& \nu y (x \underset{01}{\stackrel{\leftrightarrow}{\bar{y}}} | !y(p). P) \\
&= \nu y (!x(p'). \bar{y}(p): p' \underset{01}{\stackrel{\leftrightarrow}{\bar{p}}} | !y(p). P) \\
&\sim !x(p'). \nu y (\bar{y}(p): p' \underset{01}{\stackrel{\leftrightarrow}{\bar{p}}} | !y(p). P) \\
&\qquad \text{(replication theorem)} \\
&\geq !x(p'). \nu p (p' \underset{01}{\stackrel{\leftrightarrow}{\bar{p}}} | P) \\
&\qquad \text{(Lemma C.1 and garbage collection)} \\
&\geq !x(p'). P\{p'/p\}. \quad \text{(assumption on P)}
\end{align*}
$$

Finally, law 7 holds because:

$$
\begin{align*}
& \nu x (x \underset{01}{\stackrel{\leftrightarrow}{\bar{y}}} | \bar{x}(p): P) \\
&\equiv (\nu x, p) (!x(p'). \bar{y}(p''): p' \underset{01}{\stackrel{\leftrightarrow}{\bar{x}''}} | \bar{x}(p'). p \underset{01}{\stackrel{\leftrightarrow}{\bar{p}'}} | P) \\
&\geq (\nu p, p') (\bar{y}(p''): p' \underset{01}{\stackrel{\leftrightarrow}{\bar{p}''}} | p \underset{01}{\stackrel{\leftrightarrow}{\bar{p}'}} | P) \\
&\qquad \text{(reduction and garbage collection on $x$)}
\end{align*}
$$
$$ \begin{aligned} & \gtrsim (\nu p, p', p'') (\bar{y}(p'''). p'' \underset{01}{\leftrightarrow} \overline{p'''} | p' \underset{01}{\leftrightarrow} \overline{p''} | p \underset{01}{\leftrightarrow} \overline{p'} | P) \\ & \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{(def. of } \bar{y}(p'')\text{):} \end{aligned} $$

$$ \gtrsim (\nu p, p'') (\bar{y}(p'''). p'' \underset{01}{\leftrightarrow} \overline{p'''} | p \underset{01}{\leftrightarrow} \overline{p''} | P) \text{ (transitivity)} $$

$$ \gtrsim \nu p'' (\bar{y}(p'''). p'' \underset{01}{\leftrightarrow} \overline{p'''} | P\{p''/p\}) \text{ (assumption on } P) $$

$$ \equiv_{\alpha} \nu p (\bar{y}(p'). p \underset{01}{\leftrightarrow} \overline{p'} | P) $$

$$ = \bar{y}(p): P $$

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

We conclude the section by checking that also P wires satisfy the desired properties.

**Lemma F.6.** The P wires $q \leftrightarrow \bar{p}$ and $x \leftrightarrow \bar{y}$ satisfy the laws of Definition IV.1.

*Proof.* Transitivity has already been proved in Lemma F.3, and the requirements on free names and the shape of $x \leftrightarrow \bar{y}$ follow from the definition. So we only check the remaining laws.

We now show the law 4. Although the definition of $p \leftrightarrow \bar{q}$ is more complex than that for the other wires, the proof is similar; we can remove the wires using transitivity and the assumption on P.

$$ \nu q (p \leftrightarrow \bar{q} | q(x, r): P) $$

$$ = (\nu x, y, q, r, s) $$

$$ (p(x', r'). (x \leftrightarrow \bar{x}' | r' \leftrightarrow \bar{r})) $$

$$ | \bar{q}(y', s'). (y' \leftrightarrow \bar{y} | s \leftrightarrow \bar{s}') $$

$$ | y \leftrightarrow \bar{x} | r \leftrightarrow \bar{s} $$

$$ | (\nu x, r)(q(x', r'). (x \leftrightarrow \bar{x}' | r' \leftrightarrow \bar{r}) | P)) $$

$$ \gtrsim (\nu x, y, y', r, s, s')(p(x', r'). (x \leftrightarrow \bar{x}' | r' \leftrightarrow \bar{r})) $$

$$ | y' \leftrightarrow \bar{y} | s \leftrightarrow \bar{s}' | y \leftrightarrow \bar{x} | r \leftrightarrow \bar{s} $$

$$ | (\nu x, r)(x \leftrightarrow \bar{y}' | s' \leftrightarrow \bar{r} | P)) $$

(communication on $q$)

$$ \gtrsim (\nu x, y', r, s')(p(x', r'). (x \leftrightarrow \bar{x}' | r' \leftrightarrow \bar{r})) $$

$$ | y' \leftrightarrow \bar{x} | r \leftrightarrow \bar{s}' $$

$$ | (\nu x, r)(x \leftrightarrow \bar{y}' | s' \leftrightarrow \bar{r} | P)) $$

(transitivity of wires)

$$ \equiv_{\alpha} (\nu x'', y', r'', s')(p(x', r'). (x'' \leftrightarrow \bar{x}' | r' \leftrightarrow \bar{r}'')) $$

$$ | y' \leftrightarrow \bar{x}'' | r'' \leftrightarrow \bar{s}' $$

$$ | (\nu x, r)(x \leftrightarrow \bar{y}' | s' \leftrightarrow \bar{r} | P)) $$

$$ \gtrsim (\nu x, x'', r, r'')(p(x', r'). (x'' \leftrightarrow \bar{x}' | r' \leftrightarrow \bar{r}'')) $$

$$ | x \leftrightarrow \bar{x}'' | r'' \leftrightarrow \bar{r} | P $$

(transitivity of wires)

$$ \gtrsim (\nu x'', r'')(p(x', r'). (x'' \leftrightarrow \bar{x}' | r' \leftrightarrow \bar{r}'') | P\{x'', r''/x, r\}) $$

(assumption on P)

$$ \equiv_{\alpha} (\nu x, r)(p(x', r'). (x \leftrightarrow \bar{x}' | r' \leftrightarrow \bar{r}) | P) $$

$$ = p(x, r): P $$

The proof for law 5 is the dual of the previous case.

Now we check law 6. The reasoning is identical to the case for I-O wires and O-I wires.

$$ \nu y (x \leftrightarrow \bar{y} | !y(p). P) $$

$$ = \nu y (!x(p'). \bar{y}(p): p' \leftrightarrow \bar{p} | !y(p). P) $$

$$ \sim !x(p'). \nu y (\bar{y}(p): p' \leftrightarrow \bar{p} | !y(p). P) $$

(replication theorem)
$$ \gtrsim !x(p'). \nu p (p' \leftrightarrow \bar{p} | P) $$

(Lemma C.1 and garbage collection)

$$ \gtrsim !x(p'). P\{p'/p\} $$

(assumption on P)

$$ \equiv_{\alpha} !x(p). P $$

The last thing to check is law 7. Again, the reasoning is identical to the case for I-O wires and O-I wires.

$$ \nu x (x \leftrightarrow \bar{y} | \bar{x}(p): P) $$

$$ = \nu x (!x(p). \bar{y}(q): p \leftrightarrow \bar{q} | \nu p (\bar{x}(p'). p \leftrightarrow \bar{p}' | P)) $$

$$ \gtrsim (\nu p, p'q)(\bar{y}(q'). q \leftrightarrow \bar{q}' | p' \leftrightarrow \bar{q} | p \leftrightarrow \bar{p}' | P) $$

(interaction at $x$ and garbage collection)

$$ \gtrsim (\nu p, q)(\bar{y}(q'). q \leftrightarrow \bar{q}' | p \leftrightarrow \bar{q} | P) $$

(transitivity)

$$ \gtrsim \nu q (\bar{y}(q'). q \leftrightarrow \bar{q}' | P\{q/p\}) $$

(assumption on P)

$$ \equiv_{\alpha} \nu p (\bar{y}(p'). p \leftrightarrow \bar{p}' | P) $$

$$ = \bar{y}(p): P $$

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

## APPENDIX G

### SUPPLEMENTARY MATERIALS FOR SECTION VII

We present the proofs of full abstraction for the LT and BT equalities. As mentioned, our proof is carried out by checking the conditions introduced by Sangiorgi and Xu [6]. We first review these conditions in Section G.1. Then, in Section G.2, we show how $\mathcal{A}_{10}$ and $\mathcal{A}_{01}$ treat unsolvable terms in different manners. Using the conditions and the results concerning the unsolvable terms, we prove the full abstraction results in Section G.3.

#### 1. General conditions by Sangiorgi & Xu

Here we present a simplified version of the conditions given in [6], tailored to our needs, where the calculus is $I\pi$, and the relations to be considered are bisimilarity and the expansion relation for $I\pi$.

We begin with reviewing some needed terminology. An *abstraction context* of an encoding $\mathcal{E}$ is the context obtained by encoding the $\lambda$-calculus context $\lambda x. [\cdot]$, that is, $\mathcal{E}[[\lambda x. [\cdot]]]$ (assuming that $\lambda$-calculus holes are mapped onto identical process holes); similarly, a *variable context* of $\mathcal{E}$ is the encoding of the $\lambda$-calculus $n$-hole context
$x[\cdot]_1 \cdots [\cdot]_n$. A context is *guarded* if each hole appears underneath some proper (i.e., non-permeable) prefix. A $n$-hole context $C$ has an inverse with respect to $\lesssim$, if, for every $i \in \{1, \dots, n\}$, there exists a $\pi$-context $D_i$ such that $D_i[C[\tilde{A}]] \gtrsim \bar{a}(\tilde{b}). b(z)$. $A_i(z)$ for fresh names $a, b, z$ such that $b \in \tilde{b}$.

**Theorem G.1** ([6]). Let $\mathcal{E}$ be an encoding of the $\lambda$-calculus into $I\pi$. Suppose that the encoding satisfies the following conditions.

1) The variable contexts of $\mathcal{E}$ are guarded;

2) The abstraction and variable contexts of $\mathcal{E}$ have an inverse with respect to $\lesssim$, provided that the every abstraction $F$ that fills the holes of the context satisfies $F = \mathcal{E}[M]$ for some $\lambda$-term $M$;

3) $\mathcal{E}$ and $\lesssim$ validate the $\beta$ rule;

4) If $M$ is an unsolvable of order 0 then $\mathcal{E}[M] \approx \mathcal{E}[\Omega]$;

5) The terms $\mathcal{E}[\Omega]$, $\mathcal{E}[x \tilde{M}]$, $\mathcal{E}[x \tilde{M}']$, and $\mathcal{E}[y \tilde{M}'']$ are pairwise unrelated by $\approx$, assuming that $x \neq y$ and that tuples $\tilde{M}$ and $\tilde{M}'$ have different lengths.

Then we have:

(i) if

a) $M, N$ unsolvable of order $\omega$ implies that $\mathcal{E}[M] \approx \mathcal{E}[N]$ and

b) for any $M$ the term $\mathcal{E}[\lambda x.M]$ is unrelated by $\approx$ to $\mathcal{E}[\Omega]$ and to any term of the form $\mathcal{E}[x \tilde{M}]$, then $\mathcal{E}$ and $\approx$ are fully abstract for LT equality;

(ii) if

a) $M$ solvable implies that the term $\mathcal{E}[\lambda x.M]$ is unrelated by $\approx$ to $\mathcal{E}[\Omega]$ and to any term of the form $\mathcal{E}[x \tilde{M}]$, and

b) $\mathcal{E}[M] \approx \mathcal{E}[\Omega]$ whenever $M$ is unsolvable of order $\omega$, then $\mathcal{E}$ and $\approx$ are fully abstract for BT equality.

**Remark G.1.** The condition 2) is weaker than the original condition used in [6] (i.e., the new condition does not imply the old one). The original condition did not have the assumption that ‘abstractions that fills the hole must be encodings of $\lambda$-terms’. However, this does not cause a problem because, in [6], whenever this condition about the inverse context is used, the holes are indeed filled with encodings of $\lambda$-terms.

## 2. *Proofs for the properties of encoding of unsolvable terms*

We show that $\mathcal{A}_{01}$ differentiates (the encoding of) unsolvable terms of different orders, whereas $\mathcal{A}_{10}$ equates all the unsolvables. In the proofs, we make use of the optimised encodings $\mathcal{O}_{01}$ and $\mathcal{O}_{10}$. It is worth recalling that if $M$ is an unsolvable term, then the only visible action that $\mathcal{O}[M]_p$ can do is an input at $p$ because of Lemmas V.3 and E.9.

*Results for* $\mathcal{A}_{01}$: For $\mathcal{A}_{01}$, our goal is to show that two unsolvables are equated if and only if they have the same order.

**Lemma G.2.** Let $M$ be an unsolvable term of order 0. Then the only action $\mathcal{O}_{01}[M]_p$ can do is a $\tau$-action.

*Proof.* If $M$ is unsolvable of order 0 then it must be of the form $(\lambda x. M_0) \tilde{M}$, with $\tilde{M}$ non-empty. Therefore, by definition of $\mathcal{O}_{01}$, if $M$ is unsolvable of order 0, $\mathcal{O}_{01}[M]_p$ cannot do an input at $p$. This implies that the only transition $\mathcal{O}_{01}[M]_p$ can do is a $\tau$-transition. $\square$

**Lemma G.3.** Let $M$ be an unsolvable term of order $n$, where $0 < n < \omega$. Then $\mathcal{O}_{01}[M]_p$ can do a weak input transition at $p$. Moreover, if $\mathcal{O}_{01}[M]_p \xrightarrow{p(x,q)} P$, then there exists $N$ such that $P \gtrsim \mathcal{O}_{01}[N]_q$ and $N$ is an unsolvable of order $n-1$.

*Proof.* By definition of the order of unsolvables, we have $M \implies_{\lambda x. M'}$ for some $M'$ whose order is $n-1$. By validity of $\beta$-reduction (Lemma E.6), we have $\mathcal{O}_{01}[M]_p \gtrsim \mathcal{O}_{01}[\lambda x. M']_p$.

First, we show that $M$ can do a weak input transition at $p$. Since $\mathcal{O}_{01}[\lambda x. M']_p \xrightarrow{p(x,q)} \mathcal{O}_{01}[M']_q$, we must have a matching transition $\mathcal{O}_{01}[M]_p \xrightarrow{p(x,q)} P$ for some $P$.

We remain to show that for every $\mathcal{O}_{01}[M]_p \xrightarrow{p(x,q)} P$ there is a suitable $N$ with $P \gtrsim \mathcal{O}_{01}[N]_q$. Assume that $\mathcal{O}_{01}[M]_p (\xrightarrow{\tau})^n Q \xrightarrow{p(x,q)} P$. Then we have $\mathcal{O}_{01}[\lambda x. M']_p (\xrightarrow{\tau})^n Q'$ such that $Q \gtrsim Q'$. By Lemma V.2, we have $Q' \gtrsim \mathcal{O}_{01}[\lambda x. M'']_p$ for a $\lambda$-term $\lambda x. M''$ such that $\lambda x. M' \implies \lambda x. M''$. Since $M'$ is unsolvable of order $n-1$, so is $M''$. We also have $P \gtrsim \mathcal{O}[M'']_q$, because $Q \gtrsim \mathcal{O}_{01}[\lambda x. M'']_p$ and $\mathcal{O}_{01}[\lambda x. M'']_p \xrightarrow{p(x,q)} \mathcal{O}_{01}[M'']_q$ is the only input transition that $\mathcal{O}_{01}[\lambda x. M'']_p$ can do. $\square$

**Lemma G.4.** Let $M$ be an unsolvable of order $\omega$. Then $\mathcal{O}_{01}[M]_p$ can do a weak input transition at $p$. Moreover, if $\mathcal{O}_{01}[M]_p \xrightarrow{p(x,q)} P$, then there exists $N$ such that $P \gtrsim \mathcal{O}_{01}[N]_q$ and $N$ is an unsolvable of order $\omega$.

*Proof.* Similar to G.3. Note that if an unsolvable term $M$ of order $\omega$ reduces to $\lambda x. M'$ then $M'$ must also be an unsolvable of order $\omega$. $\square$

**Lemma G.5.** If $M$ and $N$ are unsolvable terms of order 0, then $\mathcal{O}_{01}[M]_p \approx \mathcal{O}_{01}[N]_p$.

*Proof.* We show that the relation $\mathcal{R}$ defined as

$$ \bigcup_p \{(\mathcal{O}_{01}[M]_p, \mathcal{O}_{01}[N]_p) \mid M, N \text{ unsolvables of order } 0\} $$

is a bisimulation up-to expansion. Suppose that $\mathcal{O}_{01}[M]_p \mathcal{R} \mathcal{O}_{01}[N]_p$. If $\mathcal{O}_{01}[M]_p$ makes a transition $\mathcal{O}_{01}[M]_p \xrightarrow{\mu} P$, then $\mu = \tau$ by Lemma G.2. Hence, we have $P \gtrsim \mathcal{O}[M']_p$ with $M \to M'$ by Lemma V.2. Since a term obtained by reducing an unsolvable term of order 0 must also be an unsolvable of order 0, we have $P \gtrsim \mathcal{O}_{01}[M']_p \mathcal{R} \mathcal{O}_{01}[N]_p$. In other words, we can take $\mathcal{O}_{01}[N]_p \Rightarrow \mathcal{O}_{01}[N]_p$ as the matching transition. $\square$
**Lemma VII.1.** Let $M$ and $N$ be unsolvables of order $m$ and $n$ respectively, where $0 \le m, n \le \omega$. Then $\mathcal{O}_{0I}[M]_p \approx \mathcal{O}_{0I}[N]_p$ iff $m = n$.

*Proof.* We first show that unsolvables of the same order are equated. We show that the relation $\mathcal{R}$ defined as

$$ \bigcup_p \left\{ (\mathcal{O}_{0I}[M]_p, \mathcal{O}_{0I}[N]_p) \mid \begin{array}{l} M, N \text{ are unsolvables} \\ \text{of the same order} \end{array} \right\} $$

is a bisimulation up-to expansion.

Suppose that $\mathcal{O}_{0I}[M]_p \mathcal{R} \mathcal{O}_{0I}[N]_p$. The order 0 case is exactly what we proved in Lemma G.5, so let us assume that $M$ and $N$ are unsolvable terms whose order is $n \ne 0$ (where $n$ may be $\omega$). Suppose that $\mathcal{O}_{0I}[M]_p$ makes a transition $\mathcal{O}_{0I}[M]_p \xrightarrow{\mu} P$. If $\mu = \tau$, then we can reason as we did in Lemma G.5. The only other possibility is the case where $\mu = p(x, q)$ with $x, q$ being fresh. Then, by Lemmas G.3 and G.4, there exists $M'$ such that $P \gtrsim \mathcal{O}_{0I}[M']_q$ and $M'$ is an unsolvable of order $n-1$ if $n$ is a natural number, or else $\omega$. By Lemmas G.3 and G.4, we have $\mathcal{O}_{0I}[N]_p \xrightarrow{p(x,q)} Q \gtrsim \mathcal{O}_{0I}[N']_q$ for some unsolvable term whose order coincides with that of $M'$. Since $M'$ and $N'$ are unsolvables of the same order, we have $\mathcal{O}_{0I}[M']_q \mathcal{R} \mathcal{O}_{0I}[N']_q$ as desired.

To see that unsolvable terms $M$ and $N$ with different orders are distinguished, we just need to count the number of consecutive inputs that $\mathcal{O}_{0I}[M]_p$ and $\mathcal{O}[N]_p$ can do. By Lemmas G.3, G.4 and G.2, it follows that $\mathcal{O}_{0I}[M]_p$ can do $n$ consecutive weak input transitions if the order of $M$ is $n$; if $n = \omega$, the number of consecutive inputs that $\mathcal{O}_{0I}[M]_p$ can do is unbounded. $\square$

*Results for $\mathcal{O}_{10}$:* Now we prove that all the unsolvable terms are equated to $\Omega$ in the encoding $\mathcal{O}_{10}$.

**Lemma G.6.** We have

$$ x \stackrel{\leftrightarrow}{\bar{y}} = !x(p). \mathcal{A}_{10}[y]_p = !x(p). \mathcal{O}_{10}[y]_p. $$

*Proof.* Follows from the definition. $\square$

**Lemma G.7.**

1) If $M$ is an unsolvable of order 0 then $\mathcal{O}_{10}[M]_p$ can do an input at $p$. Moreover, if $\mathcal{O}_{10}[M]_p \xrightarrow{p(x,q)} P$, then $P \gtrsim \mathcal{O}_{10}[M]_q$.

2) If $M$ is an unsolvable term then $\mathcal{O}_{10}[M]_p$ can do an input at $p$. Moreover, if $\mathcal{O}_{10}[M]_p \xrightarrow{p(x,q)} P$ then there exists an unsolvable term $M'$ such that $P \gtrsim \mathcal{O}_{10}[M']_q$.

*Proof.* To prove 1, first observe that $M$, an unsolvable term of order 0, must be of the form $(\lambda x. M_0) M_1 \cdots M_n$

for $n \ge 0$. Hence, we have

$$ \begin{align*} \mathcal{O}_{10}[M]_p &= \nu p_0 (p_0(x, r) : \mathcal{O}_{10}[M_0]_r | \bar{p}_0(x_1, p_1) : \cdots \bar{p}_{n-1}(x_n, p_n) : \\ & \qquad (!x_1(r_1). \mathcal{O}_{10}[M_1]_{r_1} | \cdots | !x_n(r_n). \mathcal{O}_{10}[M_n]_{r_n} \\ & \qquad | p \stackrel{\leftrightarrow}{\bar{\iota}} \bar{p}_n)) \\ \mathcal{O}_{10}[M]_p &\equiv \nu p_0 (p_0(x, r) : \mathcal{O}_{10}[M_0]_r | \\ & \qquad \bar{p}_0(x_1, p_1) : \cdots \bar{p}_{n-1}(x_n, p_n) : \bar{p}_n(x_{n+1}, p_{n+1}) : \\ & \qquad (!x_1(r_1). \mathcal{O}_{10}[M_1]_{r_1} | \cdots | !x_n(r_n). \mathcal{O}_{10}[M_n]_{r_n} \\ & \qquad | x_{n+1} \stackrel{\leftrightarrow}{\bar{\iota}} \bar{x} | q \stackrel{\leftrightarrow}{\bar{\iota}} \bar{p}_{n+1})) \\ &= \nu p_0 (p_0(x, r) : \mathcal{O}_{10}[M_0]_r | \\ & \qquad \bar{p}_0(x_1, p_1) : \cdots \bar{p}_{n-1}(x_n, p_n) : \bar{p}_n(x_{n+1}, p_{n+1}) : \\ & \qquad ((!x_1(r_1). \mathcal{O}_{10}[M_1]_{r_1} | \cdots | !x_n(r_n). \mathcal{O}_{10}[M_n]_{r_n} \\ & \qquad | !x_{n+1}(r_{n+1}). \mathcal{O}_{10}[x]_{r_{n+1}} | q \stackrel{\leftrightarrow}{\bar{\iota}} \bar{p}_{n+1})) \tag{Lemma G.6} \end{align*} $$

$$ = \mathcal{O}_{10}[(\lambda x. M_0) M_1 \cdots M_n x]_p $$

as desired.

We prove (2) by a case analysis on the order of $M$. If $M$ is an unsolvable of order 0, the claim follows from (1) because $Mx$ is also an unsolvable of order 0.

Now assume that $M$ is an unsolvable of order $n > 0$ ($n$ may be $\omega$). The fact that $\mathcal{O}_{10}[M]_p$ can do an input at $p$ follows by the definition of $\mathcal{O}_{10}$. We remain to prove the latter claim. Observe that we have $M \Rightarrow_{\lambda} \lambda x. M'$, and $M'$ must be an unsolvable. By Lemma E.6, we have $\mathcal{O}_{10}[M]_p \gtrsim \mathcal{O}_{10}[\lambda x. M']_p$. Thus, if $\mathcal{O}_{10}[M]_p \xrightarrow{p(x,q)} P$, we have a matching transition $\mathcal{O}_{10}[\lambda x. M']_p \xrightarrow{p(x,q)} Q$ such that $P \gtrsim Q$. By definition of $\mathcal{O}_{10}$ and of permeable inputs, and by Lemma E.1, we have $Q \gtrsim \mathcal{O}_{10}[M']_q$. Hence, $P \gtrsim \mathcal{O}_{10}[M']_q$ as desired. $\square$

**Lemma VII.2.** For any unsolvable term $M$, we have $\mathcal{O}_{10}[M]_p \approx \mathcal{O}_{10}[\Omega]_p$.

*Proof.* We show that the relation $\mathcal{R}$ defined as

$$ \bigcup_p \left\{ (\mathcal{O}_{10}[M]_p, \mathcal{O}_{10}[N]_p) \mid M \text{ and } N \text{ are unsolvables} \right\} $$

is a bisimulation up-to expansion.

Suppose that $\mathcal{O}_{10}[M]_p \mathcal{R} \mathcal{O}_{10}[N]_p$. We consider the case where $\mathcal{O}_{10}[M]_p$ makes the challenge; we omit the opposite case as it is symmetrical. By Lemma E.9 and V.3, the only actions $P$ can do is either a $\tau$-action or an input at $p$.

If $\mathcal{O}_{10}[M]_p \xrightarrow{\tau} P$ then we can take $\mathcal{O}_{10}[N]_p \Rightarrow \mathcal{O}_{10}[N]_p$ as the matching transition because we have $P \gtrsim \mathcal{O}_{10}[M']_p \mathcal{R} \mathcal{O}_{10}[N]_p$ for some unsolvable term $M'$ such that $M \to M'$ by Lemma V.2.

Assume that $\mathcal{O}_{10}[M]_p \xrightarrow{p(x,q)} P$. Then, thanks to 2 of Lemma G.7, there exists an unsolvable term $M'$ such that $P \gtrsim \mathcal{O}_{10}[M']_q$. Similarly, by 2 of Lemma G.7, we have
remains to show the condition (ib). Clearly, $\mathcal{O}_{\text{IO}}[\lambda x. M]_p$ is not bisimilar to $\mathcal{O}_{\text{IO}}[\Omega]_p$ or to the encoding of any term of the form $x \tilde{M}$ because $\mathcal{O}_{\text{IO}}[\lambda x. M]_p$ can do an input at $p$, but the others cannot. $\square$

**Theorem G.10** (Full abstraction for BT). For every $\lambda$-terms $M$ and $N$, $\text{BT}(M) = \text{BT}(N)$ if and only if $\mathcal{A}_{\text{IO}}[M] \approx \mathcal{A}_{\text{IO}}[N]$.

*Proof.* Conditions 1-5 of Theorem G.1 are checked similarly as in the proof of the previous theorem. One difference is that for the encoding $\mathcal{O}_{\text{IO}}$ we use Lemma VII.2 to say that unsolvable terms of order 0 are equated. Another (minor) difference is how to show that $x \tilde{M}$ and $x \tilde{N}$ are different when the length of $\tilde{M}$, say $m$, and the length of $\tilde{N}$, say $n$, are different. Without loss of generality suppose that $m < n$. Then $\mathcal{O}_{\text{IO}}[x \tilde{M}]_p$ can only do $m+1$ consecutive outputs:

$$ \mathcal{O}_{\text{IO}}[x \tilde{M}]_p \xrightarrow{\bar{x}(p_0)} \bar{p_0}(x_1, p_1) \rightarrow \dots \rightarrow \bar{p_n}(x_{n+1}, p_{n+1}) \rightarrow \\ \geq !x(r_1) \cdot \mathcal{O}_{\text{IO}}[M_1]_{r_1} | \dots | !x(r_n) \cdot \mathcal{O}_{\text{IO}}[M_n]_{r_n} | p \leftrightarrow \tilde{p}_n \qquad (3) $$

because $p \leftrightarrow \tilde{p}_n$ cannot make an output action. On the other hand, $\mathcal{O}_{\text{IO}}[x \tilde{N}]_p$ can do $n+1$ consecutive outputs.

Now we look at the conditions in (ii) of Theorem G.1. Condition (iia) holds because we proved that all the unsolvable terms are equated (Lemma VII.2). So we are left with checking condition (iib). Let $M$ be a solvable term. We need to check that $\lambda x. M$ is unrelated to $\Omega$ and any term of the form $w \tilde{N}$. Since $M$ is solvable, we have $\lambda x. M \Rightarrow \lambda x. \lambda \tilde{y}. z \tilde{M}$, where $\tilde{y}$ and $\tilde{M}$ are possibly empty. Since the encoding is valid with respect to $\beta$-reduction (Lemma E.6), it suffices to show that the encoding of $\lambda x. \lambda \tilde{y}. z \tilde{M}$ is not bisimilar with the encoding of $\Omega$ and $w \tilde{N}$. The process $\mathcal{O}_{\text{IO}}[\lambda x. \lambda \tilde{y}. z \tilde{M}]_p$ can do an output on $z$ after doing some inputs that correspond to the leading $\lambda s$. However, $\mathcal{O}_{\text{IO}}[\Omega]_p$ cannot do an output action even after some $\tau$ or input actions. Hence, the encoding of $\lambda x. M$ and $\Omega$ are not bisimilar. Finally, we show that the encodings of $\lambda x. \lambda \tilde{y}. z \tilde{M}$ and $w \tilde{N}$ are not related by $\approx$. First, note that $z$ needs to be a free variable and equal to $w$, otherwise $\mathcal{O}_{\text{IO}}[\lambda x. \lambda \tilde{y}. z \tilde{M}]_p$ is not bisimilar with $\mathcal{O}_{\text{IO}}[w \tilde{N}]_p$. Second, $\tilde{N}$ and $\tilde{M}$ must have the same length. Otherwise we can show that the two processes are not bisimilar by investigating the number of outputs that the two process can do as we did in (3); the fact that we have a leading $\lambda$ in $\lambda x. \lambda \tilde{y}. w \tilde{M}$ does not change the argument, as $w$ must be a free variable and $\lambda x$ is encoded as a permeable input. So, we need to show that $\mathcal{O}_{\text{IO}}[\lambda x \tilde{y}. w \tilde{M}]_p$ and $\mathcal{O}_{\text{IO}}[w \tilde{N}]_p$ are not equated when $\tilde{M}$ and $\tilde{N}$ have the same length. Observe that $\mathcal{O}_{\text{IO}}[\lambda x \tilde{y}. w \tilde{M}]_p \xrightarrow{p(x,q)} \mathcal{O}_{\text{IO}}[\lambda \tilde{y}. w \tilde{M}]_q$. The only matching transition $\mathcal{O}_{\text{IO}}[w \tilde{N}]_p$ can do is

$$ \mathcal{O}_{\text{IO}}[w \tilde{N}]_p \xrightarrow{p(x,q)} \\ \equiv \bar{w}(p_0): \mathcal{O}^n(p_0, q, \mathcal{O}_{\text{IO}}[N_1], \dots, \mathcal{O}_{\text{IO}}[N_n], \mathcal{O}_{\text{IO}}[x]) $$

$$ = \mathcal{O}_{\text{IO}}[w \tilde{M} x]_q $$

where $\tilde{N} = N_1, \dots, N_n$. Here we used Lemma G.6. Once again, we look at the number of consecutive outputs these process can do. The process $\mathcal{O}_{\text{IO}}[\lambda \tilde{y}. w \tilde{M}]_q$ can do $n+1$ outputs whereas $\mathcal{O}_{\text{IO}}[w \tilde{M} x]_q$ can do $n+2$ outputs. We therefore conclude that $\lambda x. \lambda \tilde{y}. z \tilde{M}$ can never be equated to a term of the form $w \tilde{N}$. $\square$

## APPENDIX H
PROOFS FOR SECTION VIII

We present the proofs that were omitted from Section VIII. There are only two proofs that were sketched or omitted: (i) the proof that $\mathcal{O}_P$ equates the encodings of unsolvable terms, and (ii) the proof that the equations built from a $\text{BT}_{\eta\infty}$-bisimulation have the desired solution.

The fact that $\mathcal{O}_P$ equates unsolvables can be proved as in the case for $\mathcal{O}_{\text{IO}}$.

**Lemma H.1.** We have

$$ x \leftrightarrow_{\text{IO}} \bar{y} = !x(p). \mathcal{A}_P[\bar{y}]_p = !x(p). \mathcal{O}_P[\bar{y}]_p. $$

*Proof.* Follows from the definition. $\square$

**Lemma VIII.3.** For any $M$ unsolvable, we have: $\mathcal{O}_P[M]_p \approx \mathcal{O}_P[\Omega]_p \approx K_\Omega \langle p \rangle$.

*Proof.* The reasoning is similar to that in Lemma VII.2 (whose proof is given in Section G.2). $\square$

Now we prove the key lemma for the full abstraction with respect to $\text{BT}_{\eta\infty}$ equality. The following lemma says that $\mathcal{E}_R$, the system of equations built from a $\text{BT}_{\eta\infty}$-bisimulation $\mathcal{R}$, has two solutions corresponding to the first and the second projection of $\mathcal{R}$. (See Section VIII for the definition of $\mathcal{E}_R$.)

**Lemma VIII.4.** Let $\mathcal{R}$ be a $\text{BT}_{\eta\infty}$-bisimulation and $\mathcal{E}_R$ be the system of equations defined from $\mathcal{R}$ as above. For each $(M, N) \in \mathcal{R}$, we define $F_{M,N} \stackrel{\text{def}}{=} (\tilde{x}, p) \mathcal{O}_P[M]_p$ and $G_{M,N} \stackrel{\text{def}}{=} (\tilde{x}, p) \mathcal{O}_P[N]_p$, where $\tilde{x} = f\nu(M, N)$. Then $\{F_{M,N}\}_{(M,N)\in\mathcal{R}}$ and $\{G_{M,N}\}_{(M,N)\in\mathcal{R}}$ are solutions of $\mathcal{E}_R$.

*Proof.* Take $(M, N) \in \mathcal{R}$. There are three cases to consider following Definition II.2.

If $M$ and $N$ are unsolvables then we have

$$ F_{M,N} \approx (\tilde{y}, p) \mathcal{O}_P[\Omega]_p \approx G_{M,N} $$

by Lemma VIII.3.
If the second clause of Definition II.2 holds, then we
have

$$
\begin{align*}
& F_{M,N} \tilde{y} p \\
&= \mathcal{O}_{\mathbb{P}}[\![M]\!]_{p} \\
&\ge \mathcal{O}_{\mathbb{P}}[\![\lambda x_1 \dots x_{l+m} \cdot y M_1 \dots M_{n+m}]\!]_{p} \quad \text{(Lemma E.6)} \\
&= p(x_1, p_1): \dots p_{l+m-1}(x_{l+m}, p_{l+m}): \bar{y}(w, q): \\
& \qquad \mathcal{O}_{\mathbb{P}}^{n+m} \langle q, p_{l+m}, \mathcal{O}_{\mathbb{P}}[\![M_1]\!] , \dots , \mathcal{O}_{\mathbb{P}}[\![M_{n+m}]\!] \rangle \\
&= p(x_1, p_1): \dots p_{l+m-1}(x_{l+m}, p_{l+m}): \bar{y}(w, q): \\
& \qquad \mathcal{O}_{\mathbb{P}}^{n+m} \langle q, p_{l+m}, F_{M_1,N_1} \langle \tilde{y}_1 \rangle, \dots, F_{M_{n+m},x_{l+m}} \langle \tilde{y}_{n+m} \rangle \rangle \\
& \qquad \qquad \text{(by def. of } F_{M,N}) \\
&= p(x_1, p_1): \dots p_{l+m-1}(x_{l+m}, p_{l+m}): \bar{y}(w, q): \\
& \qquad \mathcal{O}_{\mathbb{P}}^{n+m} \langle q, p_{l+m}, X_{M_1,N_1} \langle \tilde{y}_1 \rangle, \dots, X_{M_{n+m},x_{l+m}} \langle \tilde{y}_{n+m} \rangle \rangle \\
& \qquad \{F_{M_1,N_1}/X_{M_1,N_1}, \dots, F_{M_{n+m},x_{l+m}}/X_{M_{n+m},x_{l+m}}\}
\end{align*}
$$

as desired. The proof for $G_{M,N}$ is similar, but we need
validity of $\eta$-expansion (Theorem VIII.1). In detail, we
have

$$
\begin{align*}
& G_{M,N} \tilde{y} p \\
&= \mathcal{O}_{\mathbb{P}}[\![N]\!]_{p} \\
&\ge \mathcal{O}_{\mathbb{P}}[\![\lambda x_1 \dots x_l \cdot y N_1 \dots N_n]\!]_{p} \quad \text{(Lemma E.6)} \\
&= p(x_1, p_1): \dots p_{l-1}(x_l, p_l): \bar{y}(w, q): \\
& \quad \mathcal{O}_{\mathbb{P}}^{n} \langle q, p_l, \mathcal{O}_{\mathbb{P}}[\![N_1]\!] , \dots , \mathcal{O}_{\mathbb{P}}[\![N_n]\!] \rangle \\
&\approx p(x_1, p_1): \dots p_{l-1}(x_l, p_l): \\
& \quad p_l(x_{l+1}, p_{l+1}): \dots p_{l+m-1}(x_{l+m}, p_{l+m}): \bar{y}(w, q): \\
& \quad \mathcal{O}_{\mathbb{P}}^{n+m} \langle q, p_{l+m}, \mathcal{O}_{\mathbb{P}}[\![N_1]\!] , \dots , \mathcal{O}_{\mathbb{P}}[\![N_n]\!] , \mathcal{O}_{\mathbb{P}}[\![x_{l+1}]\!] , \dots , \mathcal{O}_{\mathbb{P}}[\![x_{l+m}]\!] \rangle \\
& \quad \qquad \text{(Theorem VIII.1)} \\
&= p(x_1, p_1): \dots p_{l+m-1}(x_{l+m}, p_{l+m}): \bar{y}(w, q): \\
& \quad \mathcal{O}_{\mathbb{P}}^{n+m} \langle q, p_{l+m}, G_{M_1,N_1} \langle \tilde{y}_1 \rangle, \dots, G_{M_{n+m},x_{l+m}} \langle \tilde{y}_{n+m} \rangle \rangle \\
& \quad \qquad \text{(by def. of } G_{M,N}) \\
&= (p(x_1, p_1): \dots p_{l+m-1}(x_{l+m}, p_{l+m}): \bar{y}(w, q): \\
& \quad \mathcal{O}_{\mathbb{P}}^{n+m} \langle q, p_{l+m}, X_{M_1,N_1} \langle \tilde{y}_1 \rangle, \dots, X_{M_{n+m},x_{l+m}} \langle \tilde{y}_{n+m} \rangle \rangle) \\
& \quad \{G_{M_1,N_1}/X_{M_1,N_1}, \dots, G_{M_{n+m},x_{l+m}}/X_{M_{n+m},x_{l+m}}\}.
\end{align*}
$$

The case where the third clause of Definition II.2 holds
can be proved similarly. $\square$