[a] [b,c]

# Extensional and Non-extensional
Functions as Processes

Ken Sakayori0000-0003-3238-9279  and  Davide Sangiorgi0000-0001-5823-3235  The
University of Tokyo, Japan  Università di Bologna, Italy  Inria, France

###### Abstract.

Following Milner’s seminal paper, the representation of functions as processes
has received considerable attention. For pure $\lambda$-calculus, the process
representations yield (at best) _non-extensional_ $\lambda$-theories (i.e.,
$\beta$ rule holds, whereas $\eta$ does not).

In the paper, we study how to obtain _extensional_ representations, and how to
move between extensional and non-extensional representations. Using Internal
$\pi$, I$\pi$ (a subset of the $\pi$-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 $\lambda$-theory. Exploiting the symmetries and dualities of
I$\pi$, 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 $\lambda$-theory; in fact, it yields an equality
that coincides with that of Böhm trees with infinite $\eta$. In contrast, the
other two classes of wires yield non-extensional $\lambda$-theories whose
equalities are those of the Lévy-Longo and Böhm trees.

##  1\. Introduction

Milner’s work [Mil90, Mil92] on the encoding of the pure $\lambda$-calculus
into the $\pi$-calculus is generally considered a landmark paper in the area
of semantics and programming languages. The encoding of the $\lambda$-calculus
is a significant test of expressiveness for the $\pi$-calculus. The encoding
also gives an interactive semantics to the $\lambda$-calculus, which allows
one to analyse it using the instruments available in the $\pi$-calculus. After
Milner’s seminal work, a number of encoding variants have been put forward
(e.g. [SW01] and references therein) by modifying the target language (often
to a subcalculus of the $\pi$-calculus) or the encoding itself. The
correctness of these encodings is usually supported by the operational
correspondence against a certain evaluation strategy of the $\lambda$-calculus
and by the validity of the $\beta$-rule, $(\lambda
x.M)N=M\\{\raisebox{2.15277pt}{\small$N$}\\!/\\!\mbox{\small$x$}\\}$. (In this
paper, by validity of a $\lambda$-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 $\lambda$-terms induced by the encoding has also been
investigated; in this equality two $\lambda$-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 [San93, San00] (the result is by large independent of the
behavioural equivalence adopted for the processes [SX18]). It has also been
shown how to recover the Böhm tree (BT) equality [SW01], by modifying Milner’s
encoding — allowing reductions underneath a $\lambda$-abstraction — and
selecting divergence-sensitive behavioural equivalences on processes such as
must-testing.

Tree structures play a pivotal role in the $\lambda$-calculus. For instance,
trees allow one to unveil the computational content hidden in a
$\lambda$-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 $\lambda$-calculus, such as Plotkin and Scott’s
$P_{\omega}$ [Plo72, Sco76], and the _free lazy Plotkin-Scott-Engeler models_
[Lév76, Eng81, Lon83].

In BTs and LTs, the computational content of a $\lambda$-term is unveiled
using the $\beta$-rule alone. Such structures are sometimes called _non-
extensional_ , as opposed to the _extensional_ structures, in which the
$\beta$-rule is coupled with the $\eta$-rule, $M=\lambda x.M\,x$ (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 $\eta$, shortly
$\text{BT}_{\eta\infty}$s. The equality of $\text{BT}_{\eta\infty}$s coincides
with that of Scott’s $D_{\infty}$ model [Sco76], historically the first model
of the untyped $\lambda$-calculus. A seminal result by Wadsworth [Wad76] 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
$\eta$-rule, even in their most basic form, have always appeared out of reach.
For instance, in Milner’s encoding, $x$ and $\lambda y.x\,y$ have quite
different behaviours: the former process is a single output particle, whereas
the latter 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 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).\overline{b}\langle{u}\rangle$ (or
$a(u).\overline{b}\langle{u}\rangle$, if only needed once), and sometimes
called a _forwarder_ [HY95, Mer01]. 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, $\text{BT}_{\eta\infty}$s. Precisely, we obtain BTs when
adopting the ordinary I-O wires; LTs when adopting the O-I wires; and
$\text{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 1, where $\mathcal{A}_{\tt{X}}$
is the concrete encoding in which the X wires are used.

Table 1. Instances of the abstract encoding Encoding | Parameter (wires) | Characterises
---|---|---
$\mathcal{A}_{\tt{IO}}$ | I-O wires | BT
$\mathcal{A}_{\tt{P}}$ | P wires | $\text{BT}_{\eta\infty}$
$\mathcal{A}_{\tt{OI}}$ | O-I wires | LT

We are not aware of results in the literature that produce an _extensional_
$\lambda$-theory from a processes model, let alone that derive the
$\text{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
[Bor98] 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):

$\overline{a}\langle{p}\rangle\mapsto{\boldsymbol{\nu}}q\>\left(\overline{a}\langle{q}\rangle\mid
q(\widetilde{y}).\overline{p}\langle{\widetilde{y}}\rangle\right).$ (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 [MS04], 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\widetilde{y}.\overline{p}\langle{\widetilde{y}}\rangle$.

A possible connection between I$\pi$ and $\eta$-expansion may also be found in
papers such as [CPT16], 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 1) 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) [Abr94, BS94, Fu97, PV98, Mer01, MS04, SW01],
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 2 recalls background material on
$\lambda$-calculus and I$\pi$. Section 3 introduces wires and permeable
prefixes. In Section 4, 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 $\lambda$-theory. Section 5 defines an
optimised abstract encoding, which will be useful for later proofs. In Section
6, we introduce the three classes of concrete wires, and show that they
satisfy the required assumptions for wires. In Section 7, we pick the I-O
wires and O-I wires, and prove full abstraction for LTs and BTs. In Section 8,
we do the same for the P wires and $\text{BT}_{\eta\infty}$s. Section 9
discusses further related work and possible future developments. For
readability, some proofs are only given in the Appendixes.

##  2\. Background

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

###  2.1. The $\lambda$-calculus

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

$M\Coloneqq\;x\;\;\mbox{\Large{$\mid$}}\;\;\lambda
x.M\;\;\mbox{\Large{$\mid$}}\;\;M_{1}\,M_{2}\,.$

Free variables, closed terms, substitution, $\alpha$-conversion etc. are
defined as usual [Bar84]; the set of free variables of $M$ is
${{\rm\sf{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}.\cdots.\lambda x_{n}.M$ as $\lambda x_{1}\cdots
x_{n}.M$, or $\lambda\widetilde{x}.M$.

A number of reduction relations are mentioned in this paper. The (standard)
_$\beta$ -reduction_ relation $M\xrightarrow{\ }N$ is the relation on
$\lambda$-terms induced by the following rules:

$\begin{array}[]{ll}[\beta]\;\infer{}{(\lambda x.M)\,N\xrightarrow{\
}M\\{\raisebox{1.93748pt}{\small$N$}\\!/\\!\mbox{\small$x$}\\}}&\qquad[\mu]\;\infer{N\xrightarrow{\
}N^{\prime}}{M\,N\xrightarrow{\ }M\,N^{\prime}}\\\
{[\nu]}\;\infer{M\xrightarrow{\ }M^{\prime}}{M\,N\xrightarrow{\
}M^{\prime}\,N}&\quad[\xi]\;\infer{M\xrightarrow{\ }M^{\prime}}{\lambda
x.M\xrightarrow{\ }\lambda x.M^{\prime}}\end{array}$

The (weak) _call-by-name reduction_ relation uses only the $\beta$ and $\nu$
rules, whereas _strong call-by-name_ , written $\xrightarrow{\ }_{\tt{sn}}$,
also has $\xi$; the _head reduction_ , written $\xrightarrow{\ }_{\tt{h}}$, is
a deterministic variant of $\xrightarrow{\ }_{\tt{sn}}$ in which the redex
contracted is the head one, i.e., $(\lambda y.M_{0})\,M_{1}$ of
$\lambda\widetilde{x}.(\lambda y.M_{0})\,M_{1}\cdots M_{n}$. _Head normal
forms_ are of the form $\lambda\widetilde{x}.y\,\widetilde{M}$. As usual, we
use a double arrow to indicate the reflexive and transitive closure of a
reduction relation, as in $\Longrightarrow$ and
$\mathrel{\Longrightarrow_{\tt{h}}}$. A term $M$ _has a head normal form_ $N$
if $M\mathrel{\Longrightarrow_{\tt{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\mathrel{\Longrightarrow_{\tt{h}}}\lambda
x_{1}\ldots x_{n}.M^{\prime}$, for $n\geq 0$, and some
$x_{1},\ldots,x_{n},M^{\prime}$. If there is no such largest number, then $M$
is _of order $\omega$_. For instance, if $\Delta$ is $\lambda x.x\,x$, and
$\Omega$ is $\Delta\,\Delta$, and $\Xi$ is $(\lambda xy.x\,x)\,(\lambda
xy.x\,x)$, then we have $\Omega\xrightarrow{\ }_{\tt{h}}\Omega$, therefore
$\Omega$ is an unsolvable of order $0$, and $\lambda x.\Omega$ is of order
$1$; whereas $\Xi\xrightarrow{\ }_{\tt{h}}\lambda y.\Xi$, indeed for any $n$
we have $\Xi\mathrel{\Longrightarrow_{\tt{h}}}\lambda y_{1}\ldots y_{n}.\Xi$,
therefore $\Xi$ is an unsolvable of order $\omega$.

We recall the (informal) definitions of Lévy-Longo trees and Böhm trees, and
of Böhm trees up-to infinite $\eta$-expansion. The _Lévy-Longo tree_ of $M$ is
the labelled tree, $\text{LT}(M)$, defined coinductively as follows:

  1. (1)

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

  2. (2)

$\text{LT}(M)=\lambda x_{1}\ldots x_{n}.\bot$ if $M$ is an unsolvable of order
$n<\omega$;

  3. (3)

$\text{LT}(M)$ is the tree with $\lambda\widetilde{x}.y$ as the root and
$\text{LT}(M_{1})\ldots\text{LT}(M_{n})$ as the children, if $M$ has head
normal form $\lambda\widetilde{x}.y\,M_{1}\cdots M_{n}$ with $n\geq 0$.

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

An $\eta$-expansion of a BT, whose root is $\lambda\widetilde{x}.y$ and
children are $\text{BT}(M_{1}),\ldots\text{BT}(M_{n})$, is given by a tree
whose root is $\lambda\widetilde{x}z.y$ and children are
$\text{BT}(M_{1}),\ldots\text{BT}(M_{n}),z$. Intuitively, an infinite
$\eta$-expansion of a BT is obtained by allowing this expansion at each step
of the clause (3). Thus, an (informal) coinductuive definition of the _Böhm
trees up-to infinite $\eta$-expansion_ of $M$, $\text{BT}_{\eta\infty}(M)$, is
given as follows:

  1. (1)

$\text{BT}_{\eta\infty}(M)=\bot$ if $M$ is unsolvable, and

  2. (2)

if $M\mathrel{\Longrightarrow_{\tt{h}}}\lambda x_{1}\ldots
x_{n}.y\,M_{1}\cdots M_{n}$, then

    1. (a)

$\text{BT}_{\eta\infty}(M)=\text{BT}_{\eta\infty}(\lambda x_{1}\ldots
x_{n-1}.y\,M_{1}\cdots M_{n-1})$, if $x_{n}\notin{{\rm\sf{fv}}}(y\,M_{1}\cdots
M_{n-1})$ and $\text{BT}_{\eta\infty}(M_{n})=\text{BT}_{\eta\infty}(x_{n})$;
and otherwise

    2. (b)

$\text{BT}_{\eta\infty}(M)=$ $\lambda x_{1}\ldots
x_{n}.y$$\text{BT}_{\eta\infty}(M_{1})$$\cdots$$\text{BT}_{\eta\infty}(M_{n})$

In the equality induced by the above trees, two terms are related if their
trees are the same (as usual modulo $\alpha$-conversion). These equalities may
be defined coinductively as forms of bisimilarity on $\lambda$-terms
([San93]), in the expected manner. We only present _$\text{BT}_{\eta\infty}$
-bisimilarity_, because it is the most delicate one and also because it will
be used in a few important proofs. In such a bisimilarity, first introduced by
Lassen [Las99], a (finite) $\eta$-expansion is allowed at each step of the
bisimulation game.

[[Las99]] A symmetric relation $\mathrel{\mathcal{R}}$ on $\lambda$-terms is a
_$\text{BT}_{\eta\infty}$ -bisimulation_ if, whenever
$M\mathrel{\mathcal{R}}N$, either one of the following holds:

  1. (1)

$M$ and $N$ are unsolvable

  2. (2)

$M\mathrel{\Longrightarrow_{\tt{h}}}\lambda x_{1}\ldots x_{l+m}.y\,M_{1}\cdots
M_{n+m}$ and $N\mathrel{\Longrightarrow_{\tt{h}}}\lambda x_{1}\ldots
x_{l}.y\,N_{1}\cdots N_{n}$, where the variables $x_{l+1},\ldots,x_{l+m}$ are
not free in $y$ $N_{1},\ldots,N_{n}$, and $M_{i}\mathrel{\mathcal{R}}N_{i}$
for $1\leq i\leq n$, and also $M_{n+j}\mathrel{\mathcal{R}}x_{l+j}$ for $1\leq
j\leq m$

  3. (3)

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

The largest $\text{BT}_{\eta\infty}$-bisimulation is called
_$\text{BT}_{\eta\infty}$ -bisimilarity_. We also write
$\text{BT}_{\eta\infty}(M)=\text{BT}_{\eta\infty}(N)$ when $M$ and $N$ are
$\text{BT}_{\eta\infty}$-bisimilar. We provide some examples of Böhm trees and
Lévy-Longo trees, using the terms $\Delta$, $\Omega$, and $\Xi$ introduced
earlier.

$\begin{array}[]{llll}\text{BT}(\Delta)=\leavevmode\hbox to28.37pt{\vbox
to32.21pt{\pgfpicture\makeatletter\hbox{\hskip
14.18716pt\lower-25.40271pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.85416pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\lambda x.x$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.85762pt}{-22.0697pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-7.00522pt}\pgfsys@lineto{0.00002pt}{-14.23116pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&\text{BT}(\Omega)=\bot&\text{BT}(\lambda
x.\Omega)=\bot&\text{BT}(\Xi)=\bot\\\ \text{LT}(\Delta)=\leavevmode\hbox
to28.37pt{\vbox to32.21pt{\pgfpicture\makeatletter\hbox{\hskip
14.18716pt\lower-25.40271pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.85416pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\lambda x.x$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.85762pt}{-22.0697pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-7.00522pt}\pgfsys@lineto{0.00002pt}{-14.23116pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&\text{LT}(\Omega)=\bot&\text{BT}(\lambda
x.\Omega)=\lambda x.\bot&\text{LT}(\Xi)=\top\end{array}$

For all the terms $M$ used in this example, we have
$\text{BT}(M)=\text{BT}_{\eta\infty}(M)$.

Let $J$ be a term such that $J\,z\mathrel{\Longrightarrow_{\tt{h}}}\lambda
y.z\,(Jy)$, which is easy to define using a fixed-point combinator.
Intuitively, the term $J\,z$ can be considered as the ‘limit of the sequence
of $\eta$-expansions’

$z\xrightarrow{\ }_{\eta}\lambda z_{1}.z\,z_{1}\xrightarrow{\ }_{\eta}\lambda
z_{1}.z\,(\lambda z_{2}.z_{1}\,z_{2})\xrightarrow{\ }_{\eta}\cdots$

In other words, $J\,z$ is a term that represents an ‘infinite
$\eta$-expansion’ of $z$. The terms $z$ and $J\,z$ have different Böhm trees:

$\text{BT}(J\,z)=\leavevmode\hbox to32.72pt{\vbox
to88.09pt{\pgfpicture\makeatletter\hbox{\hskip
16.36218pt\lower-80.38754pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.62918pt}{-2.56999pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\lambda z_{1}.z$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.02917pt}{-26.75484pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\lambda
z_{2}.z_{1}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{ {}{}{}}}}{}{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-7.90744pt}\pgfsys@lineto{0.00002pt}{-16.2774pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.02916pt}{-50.93968pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\lambda
z_{3}.z_{2}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{ {}{}{}}}}{}{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.00002pt}{-32.09229pt}\pgfsys@lineto{0.00003pt}{-40.46225pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.74995pt}{-75.05453pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\vdots$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.00003pt}{-56.27713pt}\pgfsys@lineto{0.00005pt}{-64.52153pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\qquad\text{BT}(z)=z.$

However, $\text{BT}_{\eta\infty}(J\,z)=\text{BT}_{\eta\infty}(z)$ as the two
terms can be equated using an infinite form of $\eta$-expansion.

###  2.2. 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{\widetilde{a}}\rangle$. We use
$P,Q$ for processes, $F$ for abstractions. Processes and abstractions form the
set of $\pi$-agents (or simply _agents_), ranged over by $A$. Small letters
$a,b,\ldots,x,y,\ldots$ range over the infinite set of names. The grammar of
I$\pi$ is thus:

$\begin{array}[]{ccll}A&\Coloneqq&P\;\;\mbox{\Large{$\mid$}}\;\;F&\mbox{(agents)}\\\\[4.0pt]
P&\Coloneqq&{\boldsymbol{0}}\;\;\mbox{\Large{$\mid$}}\;\;a(\widetilde{b}).P\;\;\mbox{\Large{$\mid$}}\;\;\overline{a}(\widetilde{b}).P\;\;\mbox{\Large{$\mid$}}\;\;{\boldsymbol{\nu}}a\>P&\mbox{(processes)}\\\\[1.0pt]
&&\;\;\mbox{\Large{$\mid$}}\;\;P_{1}|P_{2}\;\;\mbox{\Large{$\mid$}}\;\;!a(\widetilde{b}).P\;\;\mbox{\Large{$\mid$}}\;\;F\langle{\widetilde{a}}\rangle\\\\[4.0pt]
F&\Coloneqq&({\widetilde{a}})~{}P\;\;\mbox{\Large{$\mid$}}\;\;\mathtt{K}&\mbox{(abstractions)}\end{array}$

The operators used have the usual meanings. In prefixes $a(\widetilde{b})$ and
$\overline{a}(\widetilde{b})$, we call $a$ the subject. We often abbreviate
${\boldsymbol{\nu}}a\>{\boldsymbol{\nu}}b\>P$ as $({\boldsymbol{\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 $\mathsf{fn}(-)$, $\mathsf{bn}(-)$, and
${{\rm\sf{n}}}(-)$, as well as that of $\alpha$-conversion. An agent is _name-
closed_ if it does not contain free names. In the grammar, $\mathtt{K}$ is a
_constant_ , used to write recursive definitions. Each constant $\mathtt{K}$
has a defining equation of the form
$\mathtt{K}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}({\widetilde{x}})~{}P$, where $({\widetilde{x}})~{}P$ is name-
closed; $\widetilde{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.

For convenience, we set some conventions. An application redex
$((\widetilde{x})P)\langle{\widetilde{a}}\rangle$ can be normalised as
$P\\{\raisebox{2.15277pt}{\small$\widetilde{x}$}\\!/\\!\mbox{\small$\widetilde{a}$}\\}$.
An agent is _normalised_ if all such application redexes have been contracted.
When reasoning on behaviours it is useful to assume that all expressions are
normalised, in the above sense. Thus in the remainder of the paper _we
identify an agent with its normalised expression_. As in the
$\lambda$-calculus, following the usual Barendregt convention we identify
processes or actions which only differ on the choice of the bound names. The
symbol $=$ will mean ‘syntactic identity modulo $\alpha$-conversion’.

Since the calculus is polyadic, we assume a _sorting system_ [Mil93] 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,...$ for location names, and
$x,y,z,...$ for variable names, the forms of the possible prefixes are:

$p(x,q).P\;\;\mbox{\Large{$\mid$}}\;\;x(p).P\;\;\mbox{\Large{$\mid$}}\;\;\overline{p}(x,q).P\;\;\mbox{\Large{$\mid$}}\;\;\overline{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 [SW01], and reported in Figure
1. Transitions are of the form
$P\mathrel{\stackrel{{\scriptstyle{\mu}}}{{\longrightarrow}}}P^{\prime}$,
where the set of _actions_ is given by

$\mu\Coloneqq
a(\widetilde{b})\;\;\mbox{\Large{$\mid$}}\;\;\overline{a}(\widetilde{b})\;\;\mbox{\Large{$\mid$}}\;\;\tau$

and bound names of $\mu$ are _fresh_ , i.e., they do not appear free in $P$.
The meaning of actions is the usual one: $a(\widetilde{b})$ and
$\overline{a}(\widetilde{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
$\overline{a(\widetilde{b})}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\overline{a}(\widetilde{b})$ and
$\overline{\overline{a}(\widetilde{b})}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}a(\widetilde{b})$. Since we are using the Barendregt convention, in
par, we have an implicit side condition
$\mathsf{bn}(\mu)\cap\mathsf{fn}(Q)=\emptyset$. The
$(\widetilde{y})\,Q=(\widetilde{x})\,P$ in the premise of rule com merely
means that the two agents are equal up-to $\alpha$-conversion. As usual, we
write $\xRightarrow{\mu}$ for $\xRightarrow{\ }\xrightarrow{\mu}\xRightarrow{\
}$, and $\xRightarrow{\hat{\mu}}$ is $\xRightarrow{\mu}$ for $\mu\neq\tau$ and
$\xRightarrow{\ }$ otherwise.

[pre] |  μ.P ⟶μP | [par] P ⟶μP’ P | Q ⟶μP’| Q
---|---|---
[res] |  P ⟶μP’ x ／∈n(μ) ν x P ⟶μ ν x P’ |  [com] P ⟶μ P’ Q ⟶¯μ Q’ μ≠τ, ~x= bn(μ) P | Q ⟶τ ν ~x (P’| Q’)
[rep] |  μ. P ⟶μ P’ !μ. P ⟶μ P’ | !μ. P |  [con] P ⟶μP’ K=def(~y) Q (~y) Q =(~x) P K ⟨~x⟩ ⟶μP’
Figure 1. The standard LTS for I$\pi$.

The reference behavioural equivalence for I$\pi$ is (weak) bisimilarity. It is
known that, in I$\pi$, bisimilarity coincides with barbed congruence (for
processes that are image-finite up to weak bisimilarity; all the agents
obtained as encodings of $\lambda$-terms will be image-finite up to weak
bisimilarity).

[Bisimilarity] A symmetric relation $\mathrel{\mathcal{R}}$ over processes is
a _(weak) bisimulation_ , if, whenever $P\mathrel{\mathcal{R}}Q$,

  * •

$P\xrightarrow{\mu}P^{\prime}$ implies $Q\xRightarrow{\hat{\mu}}Q^{\prime}$
for some $Q^{\prime}$ such that $P^{\prime}\mathrel{\mathcal{R}}Q^{\prime}$.

Processes $P$ and $Q$ are _(weakly) bisimilar_ , written $P\approx Q$ if there
exists a bisimulation $\mathrel{\mathcal{R}}$ such that
$P\mathrel{\mathcal{R}}Q$.

In a few places we will also use _strong bisimilarity_ , written $\sim$; this
is defined analogous to $\approx$, but $Q$ must respond with a (strong)
transition $Q\xrightarrow{\mu}Q^{\prime}$.

We also use the _expansion_ preorder, written $\lesssim$, an asymmetric
variant of $\approx$ in which, intuitively, $P\lesssim Q$ holds if $P\approx
Q$ but also $Q$ has at least as many $\tau$-moves as $P$. [Expansion] A
relation $\mathrel{\mathcal{R}}$ over processes is an _expansion_ if
$P\mathrel{\mathcal{R}}Q$ implies:

  1. (1)

Whenever $P\xrightarrow{\mu}P^{\prime}$, there exists $Q^{\prime}$ such that
$Q\mathrel{\stackrel{{\scriptstyle{\mu}}}{{\Longrightarrow}}}Q^{\prime}$ and
$P^{\prime}\mathrel{\mathcal{R}}Q^{\prime}$;

  2. (2)

whenever
$Q\mathrel{\stackrel{{\scriptstyle{\mu}}}{{\longrightarrow}}}Q^{\prime}$,
there exists $P^{\prime}$ such that
$P\>\stackrel{{\scriptstyle{\widehat{\mu}}}}{{\longrightarrow}}\>P^{\prime}$
and $P^{\prime}\mathrel{\mathcal{R}}Q^{\prime}$.

Here $\>\stackrel{{\scriptstyle{\widehat{\mu}}}}{{\longrightarrow}}\>$ is the
strong version of $\xRightarrow{\hat{\mu}}$, that is,
$\>\stackrel{{\scriptstyle{\widehat{\mu}}}}{{\longrightarrow}}\>$ is
$\mathrel{\stackrel{{\scriptstyle{\mu}}}{{\longrightarrow}}}$ if $\mu\neq\tau$
and is $=$ or $\xrightarrow{\tau}$ if $\mu=\tau$. We say that $Q$ _expands_
$P$, written $P\lesssim Q$, if $P\mathrel{\mathcal{R}}Q$, for some expansion
$\mathrel{\mathcal{R}}$.

Finally, we sometimes use _structural congruence_ , when we need to emphasize
that two processes are the same modulo some structural rewriting of their
syntax.

[Structural congruence] The _structural congruence_ $\equiv$ is the smallest
congruence relation over processes that includes the $\alpha$-equivalence and
the following equivalence:

$\displaystyle P\mid{\boldsymbol{0}}\equiv P\quad P\mid Q\equiv Q\mid
P\quad(P\mid Q)\mid R\equiv P\mid(Q\mid R)$
$\displaystyle{\boldsymbol{\nu}}x\>{\boldsymbol{\nu}}y\>P\equiv{\boldsymbol{\nu}}y\>{\boldsymbol{\nu}}x\>P\quad(x\neq
y)$ $\displaystyle{\boldsymbol{\nu}}x\>(P\mid
Q)\equiv{\boldsymbol{\nu}}x\>P\mid Q\quad(x\notin{{\rm\sf{fv}}}(Q)).$

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

${\equiv}\subsetneq{\sim}\subsetneq{\lesssim}\subsetneq{\approx}.$

In I$\pi$, _all the relations above are (pre)congruences_ [San96b]. All
behavioural relations are extended to abstractions by requiring ground
instantiation of the parameters. For instance, $(x)P\approx(x)Q$ if $P\approx
Q$. Appendix A summarises notations used in the paper (term relations,
encodings, etc.).

####  2.2.1. Proof techniques

Here we review known proof-techniques for I$\pi$ that we will use in this
paper. These are well-known algebraic laws, notably laws for private
replications, up-techniques for bisimilarity, and unique solutions of
equations.

#### Algebraic laws

We will often use a group of laws about private replication. That is, laws for
processes of the form ${\boldsymbol{\nu}}a\>(P\mid{!}a(\widetilde{b}).Q)$,
where $a$ only appears free only in output position of $P$ and $Q$. Since the
process ${!}a(\widetilde{b}).Q$ is replicated and private it can be
distributed or pushed inside prefixes. These laws are known as the replication
theorems [SW01].

######  Lemma 1.

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

  1. (1)

${\boldsymbol{\nu}}x\>(Q\mid
R\mid{!}x(p).P)\sim{\boldsymbol{\nu}}x\>(Q\mid{!}x(p).P)\mid{\boldsymbol{\nu}}x\>(R\mid{!}x(p).P)$;

  2. (2)

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

  3. (3)

${\boldsymbol{\nu}}x\>({!}y(q).Q\mid{!}x(p).P)\sim{!}y(q).{\boldsymbol{\nu}}x\>(Q\mid{!}x(p).P)$;

  4. (4)

${\boldsymbol{\nu}}x\>(Q\mid{!}x(p).P)\sim Q$, if $x\notin\mathsf{fn}(Q)$;

  5. (5)

${\boldsymbol{\nu}}x\>(\overline{x}(p).Q\mid{!}x(p).P)\gtrsim{\boldsymbol{\nu}}x\>(Q\mid
P\mid{!}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_ [San96a], which
admits the use of contexts and of behavioural equivalences such as expansion
to achieve the closure of a relation in the bisimulation game. [Bisimulation
up-to context and $\lesssim$] A symmetric relation ${\mathrel{\mathcal{R}}}$
on I$\pi$-processes is a _bisimulation up-to context and up-to $\lesssim$ if
$P\mathrel{\mathcal{R}}Q$ and
$P\mathrel{\stackrel{{\scriptstyle{\mu}}}{{\longrightarrow}}}P^{\prime\prime}$
imply that there are a (possibly multi-hole) context $C$ and processes
$\widetilde{P}^{\prime}$ and $\widetilde{Q}^{\prime}$ such that
$P^{\prime\prime}\gtrsim C[\widetilde{P}^{\prime}]$,
$Q\>\stackrel{{\scriptstyle{\widehat{\mu}}}}{{\Longrightarrow}}\>\gtrsim
C[\widetilde{Q}^{\prime}]$ and
$\widetilde{P}^{\prime}\mathrel{\mathcal{R}}\widetilde{Q}^{\prime}$. Here
$\widetilde{P}^{\prime}\mathrel{\mathcal{R}}\widetilde{Q}^{\prime}$ means
$P^{\prime}_{i}\mathrel{\mathcal{R}}Q^{\prime}_{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 2.

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

We refer the readers to [San96a] for the proof. (Adapting the proof to I$\pi$
and non-static multi-hole contexts is straightforward.) We also use the
technique of _expansion_ up-to context and $\lesssim$, which is defined
analogously to Definition 2.2, as a proof technique to prove expansion results
(the main difference is that one now requires $P^{\prime\prime}\lesssim
C[\widetilde{P}^{\prime}]$).

#### Unique solution of equations

We briefly recall the ‘unique solution of equations’ technique [DHS19].
_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{\widetilde{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.

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 $\widetilde{X}=\widetilde{E}$)
is a _system of equations_. (There is one equation for each variable $X_{i}$.)
A system of equations is _guarded_ if each occurrence of a variable in the
body of an equation is underneath a prefix.

We write $E[\widetilde{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 $(\widetilde{x})P$ in $X\langle\widetilde{a}\rangle$ amounts to
replacing $X\langle\widetilde{a}\rangle$ with the process
$P\\{\raisebox{2.15277pt}{\small$\widetilde{a}$}\\!/\\!\mbox{\small$\widetilde{x}$}\\}$.

Suppose $\\{X_{i}=E_{i}\\}_{i\in I}$ is a system of equations. We say that:

  * •

$\widetilde{F}$ is a _solution of the system of equations for $\approx$_ if
for each $i$ it holds that $F_{i}\approx E_{i}[\widetilde{F}]$.

  * •

The system has _a unique solution for $\approx$_ if whenever $\widetilde{F}$
and $\widetilde{G}$ are both solutions for $\approx$, we have
$\widetilde{F}\approx\widetilde{G}$.

[Syntactic solutions] The _syntactic solutions_ of a system of equations
$\\{X_{i}=E_{i}\\}_{i\in I}$ are the recursively defined constants
$\mathtt{K}_{\widetilde{E},i}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}E_{i}[\widetilde{\mathtt{K}}_{\widetilde{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\geq 0$, and some $n$ such that
$P=P_{0}\mathrel{\stackrel{{\scriptstyle{\mu_{0}}}}{{\longrightarrow}}}P_{1}\mathrel{\stackrel{{\scriptstyle{\mu_{1}}}}{{\longrightarrow}}}P_{2}\mathrel{\stackrel{{\scriptstyle{\mu_{2}}}}{{\longrightarrow}}}\dots$
and for all $i>n$, $\mu_{i}=\tau$. We call a _divergence of $P$_ the sequence
of transitions
$\big{(}P_{i}\mathrel{\stackrel{{\scriptstyle{\mu_{i}}}}{{\longrightarrow}}}P_{i+1}\big{)}_{i\geq
0}$. An abstraction $F$ has a divergence if the process
$F\langle{\widetilde{a}}\rangle$ has a divergence, where $\widetilde{a}$ are
fresh names.

[[DHS22]] A guarded system of equations whose syntactic solutions are agents
with no divergences has a unique solution for $\approx$.

##  3\. 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.

#### Wires

We use the notation $a\leftrightarrow\bar{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 $b$ (thus $a\leftrightarrow\bar{b}$ itself will
use $a$ in input and $b$ in output). We call such wires ‘abstract’ because we
will not give a definition for them. We only state (Section 4) some
behavioural properties that are expected to hold, and that have mainly to do
with substitutions; approximately:

  1. (1)

if $P$ uses $b$ only in input, then
${\boldsymbol{\nu}}b\>(a\leftrightarrow\bar{b}|P)\gtrsim
P\\{\raisebox{2.15277pt}{\small$a$}\\!/\\!\mbox{\small$b$}\\}$

  2. (2)

dually, if $P$ uses $a$ only in output, then
${\boldsymbol{\nu}}a\>(a\leftrightarrow\bar{b}|P)\gtrsim
P\\{\raisebox{2.15277pt}{\small$b$}\\!/\\!\mbox{\small$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:

  1. (3)

${\boldsymbol{\nu}}b\>(a\leftrightarrow\bar{b}\mid
b\leftrightarrow\bar{c})\gtrsim(b\leftrightarrow\bar{c})\\{\raisebox{2.15277pt}{\small$a$}\\!/\\!\mbox{\small$b$}\\}=(a\leftrightarrow\bar{b})\\{\raisebox{2.15277pt}{\small$c$}\\!/\\!\mbox{\small$b$}\\}=a\leftrightarrow\bar{c}$.

When (1) holds we say that $P$ is _I-respectful with respect to
$a\leftrightarrow\bar{b}$_; similarly when (2) holds we say that $P$ is _O-
respectful with respect to $a\leftrightarrow\bar{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. Thus
when, in Section 6, we consider _concrete_ instantiations of the location
wires, the corresponding definitions of the variable wires will be adjusted so
to maintain the expected properties of the location wires.

#### Permeable prefixes

We write $a(\widetilde{b})\colon P$ and $\bar{a}(\widetilde{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(\widetilde{b})\colon P$, as an ordinary input, is capable
of producing action $a(\widetilde{b})$ thus yielding the derivative $P$.
However, in contrast with the ordinary input, in $a(\widetilde{b})\colon 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 $\widetilde{b}$ cannot fire for as long as the top prefix
$a(\widetilde{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)\colon
P\;\;\mbox{\Large{$\mid$}}\;\;\bar{p}(x,q)\\!:P\;\;\mbox{\Large{$\mid$}}\;\;x(p)\colon
P\;\;\mbox{\Large{$\mid$}}\;\;\bar{x}(p)\\!:P$

Moreover, it will always be the case that in a prefix $p(x,q)\colon 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)\colon 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

$\displaystyle p(x,q)\colon P$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}({\boldsymbol{\nu}}x,q)\>\left(p(x^{\prime},q^{\prime}).\left(x\leftrightarrow\bar{x}^{\prime}\mid
q^{\prime}\leftrightarrow\bar{q}\right)\mid P\right)$ $\displaystyle
x(p)\colon P$ $\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{\boldsymbol{\nu}}p\>\left(x(p^{\prime}).p^{\prime}\leftrightarrow\bar{p}\mid
P\right)$ $\displaystyle\bar{p}(x,q)\\!:P$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}({\boldsymbol{\nu}}x,q)\>\left(\overline{p}(x^{\prime},q^{\prime}).\left(x^{\prime}\leftrightarrow\bar{x}\mid
q\leftrightarrow\bar{q}^{\prime}\right)\mid P\right)$
$\displaystyle\bar{x}(p)\\!:P$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{\boldsymbol{\nu}}p\>\left(\overline{x}(p^{\prime}).p\leftrightarrow\bar{p}^{\prime}\mid
P\right)$

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

$\displaystyle p(x,q)\colon
P\xrightarrow{p(x,q)}\equiv({\boldsymbol{\nu}}x^{\prime},q^{\prime})\>\left(x^{\prime}\leftrightarrow\bar{x}\mid
q\leftrightarrow\bar{q}^{\prime}\mid
P\\{\raisebox{2.15277pt}{\small$x^{\prime},q^{\prime}$}\\!/\\!\mbox{\small$x,q$}\\}\right)\gtrsim
P$

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

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.

We end this section by introducing some algebraic laws for permeable prefixes.
These laws allow us to avoid desugaring while proving the properties of the
encodings.

######  Lemma 3.

  1. (1)

${\boldsymbol{\nu}}p\>(p(x,q)\colon P\mid\bar{p}(x,q)\\!:Q)\gtrsim P\mid Q$ if
either $P$ is I-respectful with $q\leftrightarrow\bar{q}^{\prime}$ and
O-respectful with $x^{\prime}\leftrightarrow\bar{x}$ or $P$ is O-respectful
with $q\leftrightarrow\bar{q}^{\prime}$ and I-respectful with
$x^{\prime}\leftrightarrow\bar{x}$.

  2. (2)

${\boldsymbol{\nu}}x\>({!}x(p).P\mid\bar{x}(p)\\!:Q\mid
R)\gtrsim{\boldsymbol{\nu}}x\>({!}x(p).P\mid P\mid Q\mid R)$ if
$p\notin\mathsf{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}^{\prime}$
or $Q$ is O-respectful with $p^{\prime}\leftrightarrow\bar{p}$.

######  Lemma 4.

Suppose that wires, which are used to define the permeable prefixes, are
transitive. Then the following laws hold.

  1. (1)

If $a\neq b$ and $a\notin\widetilde{c}$ then
${\boldsymbol{\nu}}a\>b(\widetilde{c})\colon P\equiv
b(\widetilde{c})\colon{\boldsymbol{\nu}}a\>P$ and
${\boldsymbol{\nu}}a\>\bar{b}(\widetilde{c})\\!:P\equiv\bar{b}(\widetilde{c})\\!:{\boldsymbol{\nu}}a\>P$

  2. (2)

If $\widetilde{b}\cap\mathsf{fn}(Q)=\emptyset$ then $Q\mid
a(\widetilde{b})\colon P\equiv a(\widetilde{b})\colon(Q\mid P)$ and
$Q\mid\bar{a}(\widetilde{b})\\!:P\equiv\bar{a}(\widetilde{b})\\!:(Q\mid P)$.

Lemma 3 expresses a property of a restricted interaction consuming permeable
prefixes. Lemma 4 shows two structural laws for permeable prefixes, one
concerning restriction, the other concerning parallel composition. These
lemmas simply follow from the syntactic definition of the permeable prefixes.
The assumption about the transitivity of wires, in Lemma 4, is harmless as all
the wires we use in this paper are transitive. In what follows, we will use
these structural rules without explicitly mentioning Lemma 4.

##  4\. Abstract Encoding

This section introduces the abstract encoding of $\lambda$-terms into
I$\pi$-processes. We call the encoding ‘abstract’ because 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.

###  4.1. 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 [Mil92, Mil93]:

$\displaystyle\mathcal{M}\llbracket x\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\overline{x}\langle{p}\rangle$
$\displaystyle\mathcal{M}\llbracket\lambda x.M\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}p(x,q).\mathcal{M}\llbracket M\rrbracket_{q}$
$\displaystyle\mathcal{M}\llbracket M\,N\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}({\boldsymbol{\nu}}q,x)\>\left(\mathcal{M}\llbracket
M\rrbracket_{q}\mid\overline{q}\langle{x,p}\rangle\mid{!}x(r).\mathcal{M}\llbracket
N\rrbracket_{r}\right)$

The encoding of a $\lambda$-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, $\mathcal{M}$ (as well as all the encodings in the paper)
is a function from $\lambda$-terms to abstractions of the form $(p)\,P$. We
write $\mathcal{M}\llbracket M\rrbracket_{p}$ as a shorthand for
$\mathcal{M}\llbracket M\rrbracket\langle{p}\rangle$. A function application
of the $\lambda$-calculus becomes, in the $\pi$-calculus, a particular form of
parallel combination of two agents, the function and its argument;
$\beta$-reduction is then modelled as process interaction. 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.

$\displaystyle\mathcal{A}\llbracket x\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\bar{x}(p^{\prime})\\!:p\leftrightarrow\bar{p}^{\prime}$
$\displaystyle\mathcal{A}\llbracket\lambda x.M\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}p(x,q)\colon\mathcal{A}\llbracket M\rrbracket_{q}$
$\displaystyle\mathcal{A}\llbracket M\,N\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{\boldsymbol{\nu}}q\>(\mathcal{A}\llbracket
M\rrbracket_{q}\mid\bar{q}(x,p^{\prime})\\!:({!}x(r).\mathcal{A}\llbracket
N\rrbracket_{r}\mid p\leftrightarrow\bar{p}^{\prime}))$ Figure 2. The abstract
encoding $\mathcal{A}$.

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

  1. (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 (as hinted in
the Introduction).

  2. (2)

A permeable input is used, in place of an ordinary input, in the translation
of abstraction so to allow reductions underneath a $\lambda$-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.

[Wires] As a convention, we assume that names $a,b,c$ are of the same sort,
either location names or variable names. _Wires_ $a\leftrightarrow\bar{b}$ are
processes that satisfy the following properties:

  1. (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. (2)

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

  3. (3)

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

  4. (4)

${\boldsymbol{\nu}}q\>(p\leftrightarrow\bar{q}\mid q(x,r)\colon P)\gtrsim
p(x,r)\colon P$, provided that
$({\boldsymbol{\nu}}x,r\>)(x\leftrightarrow\bar{x}^{\prime}\mid
r^{\prime}\leftrightarrow\bar{r}\mid P)\gtrsim
P\\{\raisebox{2.15277pt}{\small$x^{\prime},r^{\prime}$}\\!/\\!\mbox{\small$x,r$}\\}$,
where $x^{\prime},r^{\prime}$ are fresh names.

  5. (5)

${\boldsymbol{\nu}}p\>\left(p\leftrightarrow\bar{q}\mid\bar{p}(x,r)\\!:P\right)\gtrsim\bar{q}(x,r)\\!:P$,
provided that $({\boldsymbol{\nu}}x,r\>)(x^{\prime}\leftrightarrow\bar{x}\mid
r\leftrightarrow\bar{r}^{\prime}\mid P)\gtrsim
P\\{\raisebox{2.15277pt}{\small$x^{\prime},r^{\prime}$}\\!/\\!\mbox{\small$x,r$}\\}$,
where $x^{\prime},r^{\prime}$ are fresh names.

  6. (6)

${\boldsymbol{\nu}}y\>(x\leftrightarrow\bar{y}\mid{!}y(p).P)\gtrsim{!}x(p).P$,
provided that $y\notin\mathsf{fn}(P)$ and
${\boldsymbol{\nu}}p\>(p^{\prime}\leftrightarrow\bar{p}\mid P)\gtrsim
P\\{\raisebox{2.15277pt}{\small$p^{\prime}$}\\!/\\!\mbox{\small$p$}\\}$, where
$p^{\prime}$ is fresh.

  7. (7)

${\boldsymbol{\nu}}x\>(x\leftrightarrow\bar{y}\mid\bar{x}(p)\\!:P)\gtrsim\bar{y}(p)\\!:P$,
provided that $x\notin\mathsf{fn}(P)$ and
${\boldsymbol{\nu}}p\>(p\leftrightarrow\bar{p}^{\prime}\mid P)\gtrsim
P\\{\raisebox{2.15277pt}{\small$p^{\prime}$}\\!/\\!\mbox{\small$p$}\\}$, where
$p^{\prime}$ is fresh.

  8. (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

${\boldsymbol{\nu}}p\>\left(p\leftrightarrow\bar{q}\mid\overline{p}(x,r).P\right)\gtrsim\overline{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\leftrightarrow\bar{y}$
to be an input replicated processes, and is useful so to be able to use the
replication laws (Lemma 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 2_. We can therefore exploit such requirements to
derive properties of the abstract encoding.

Lemma 5 shows that the processes encoding functions are I-respectful with
respect to the location wires, and O-respectful with respect to the variable
wires.

######  Lemma 5.

  1. (1)

${\boldsymbol{\nu}}q\>(p\leftrightarrow\bar{q}\mid\mathcal{A}\llbracket
M\rrbracket_{q})\gtrsim\mathcal{A}\llbracket M\rrbracket_{p}$

  2. (2)

${\boldsymbol{\nu}}x\>(x\leftrightarrow\bar{y}\mid\mathcal{A}\llbracket
M\rrbracket_{p})\gtrsim\mathcal{A}\llbracket
M\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p}$

######  Proof 4.1.

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

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

$\displaystyle{\boldsymbol{\nu}}p\>(\llbracket x\rrbracket_{p}\mid
q\leftrightarrow\bar{p})$
$\displaystyle={\boldsymbol{\nu}}p\>(\bar{x}(p^{\prime})\\!:p\leftrightarrow\bar{p}^{\prime}\mid
q\leftrightarrow\bar{p})$
$\displaystyle\equiv\bar{x}(p^{\prime})\\!:{\boldsymbol{\nu}}p\>(p\leftrightarrow\bar{p}^{\prime}\mid
q\leftrightarrow\bar{p})$
$\displaystyle\gtrsim\bar{x}(p^{\prime})\\!:q\leftrightarrow\bar{p}^{\prime}$
(3 of Definition 2) $\displaystyle=\llbracket x\rrbracket_{q}$

Next we show that ${\boldsymbol{\nu}}x\>(\llbracket M\rrbracket_{p}\mid
x\leftrightarrow\bar{y})=\llbracket
M\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$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
2, it follows that
${\boldsymbol{\nu}}x\>(x\leftrightarrow\bar{y})\sim{\boldsymbol{0}}$, and this
concludes this case. If $M=x$, then

$\displaystyle{\boldsymbol{\nu}}x\>(\llbracket x\rrbracket_{p}\mid
x\leftrightarrow\bar{y})$
$\displaystyle={\boldsymbol{\nu}}x\>(\bar{x}(p^{\prime})\\!:p\leftrightarrow\bar{p}^{\prime}\mid
x\leftrightarrow\bar{y})$
$\displaystyle\gtrsim\bar{y}(p^{\prime})\\!:p\leftrightarrow\bar{p}^{\prime}$
(7 of Definition 2) $\displaystyle=\llbracket y\rrbracket_{p}$

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

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

$\displaystyle{\boldsymbol{\nu}}p\>(\llbracket\lambda x.N\rrbracket_{p}\mid
q\leftrightarrow\bar{p})$
$\displaystyle={\boldsymbol{\nu}}p\>(p(x,r)\colon\llbracket
N\rrbracket_{r}\mid q\leftrightarrow\bar{p})$ $\displaystyle\gtrsim
q(x,r)\colon\llbracket N\rrbracket_{r}$ (4 of Definition 2 together with the
i.h.) $\displaystyle=\llbracket\lambda x.N\rrbracket_{r}$

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

$\displaystyle{\boldsymbol{\nu}}y\>(\llbracket\lambda x.N\rrbracket_{p}\mid
y\leftrightarrow\bar{z})$
$\displaystyle={\boldsymbol{\nu}}y\>(p(x,q)\colon\llbracket
N\rrbracket_{q}\mid y\leftrightarrow\bar{z})$ $\displaystyle\equiv
p(x,q)\colon{\boldsymbol{\nu}}y\>(\llbracket N\rrbracket_{q}\mid
y\leftrightarrow\bar{z})$ $\displaystyle\gtrsim p(x,q)\colon(\llbracket
N\\{\raisebox{2.15277pt}{\small$z$}\\!/\\!\mbox{\small$y$}\\}\rrbracket_{q})$
(i.h.) $\displaystyle=\llbracket(\lambda
x.N)\\{\raisebox{2.15277pt}{\small$z$}\\!/\\!\mbox{\small$y$}\\}\rrbracket_{p}$

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

$\displaystyle{\boldsymbol{\nu}}p\>\left(\bar{r}(x,p^{\prime})\\!:({!}x(r^{\prime}).\llbracket
L\rrbracket_{r^{\prime}}\mid p\leftrightarrow\bar{p}^{\prime})\mid
q\leftrightarrow\bar{p}\right)$
$\displaystyle\equiv({\boldsymbol{\nu}}p,x,p^{\prime}\>)(\overline{r}(x^{\prime},p^{\prime\prime}).(x^{\prime}\leftrightarrow\bar{x}\mid
p^{\prime}\leftrightarrow\bar{p}^{\prime\prime})\mid{!}x(r^{\prime}).\llbracket
L\rrbracket_{r^{\prime}}\mid p\leftrightarrow\bar{p}^{\prime}\mid
q\leftrightarrow\bar{p})$
$\displaystyle\gtrsim({\boldsymbol{\nu}}x,p^{\prime}\>)(\overline{r}(x^{\prime},p^{\prime\prime}).(x^{\prime}\leftrightarrow\bar{x}\mid
p^{\prime}\leftrightarrow\bar{p}^{\prime\prime})\mid{!}x(r^{\prime}).\llbracket
L\rrbracket_{r^{\prime}}\mid q\leftrightarrow\bar{p}^{\prime})$ (3 of
Definition 2)
$\displaystyle=\bar{r}(x,p^{\prime})\\!:({!}x(r^{\prime}).\llbracket
L\rrbracket_{r^{\prime}}\mid q\leftrightarrow\bar{p}^{\prime})$

Using this, we get

$\displaystyle{\boldsymbol{\nu}}p\>\left(\llbracket N\,L\rrbracket_{p}\mid
p\leftrightarrow\bar{q}\right)$
$\displaystyle\equiv{\boldsymbol{\nu}}r\>\left(\llbracket
N\rrbracket_{r}\mid{\boldsymbol{\nu}}p\>\left(\bar{r}(x,p^{\prime})\\!:({!}x(r^{\prime}).\llbracket
L\rrbracket_{r^{\prime}}\mid p\leftrightarrow\bar{p}^{\prime})\mid
q\leftrightarrow\bar{p}\right)\right)$
$\displaystyle\gtrsim{\boldsymbol{\nu}}r\>\left(\llbracket
N\rrbracket_{r}\mid\bar{r}(x,p^{\prime})\\!:({!}x(r^{\prime}).\llbracket
L\rrbracket_{r^{\prime}}\mid q\leftrightarrow\bar{p}^{\prime})\right)$
$\displaystyle=\llbracket N\,L\rrbracket_{q}$

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 2. We, therefore,
can apply the replication theorem to $x\leftrightarrow\bar{y}$. Hence, we have

$\displaystyle{\boldsymbol{\nu}}x\>({!}z(p).\llbracket L\rrbracket_{p}\mid
x\leftrightarrow\bar{y})$
$\displaystyle\sim{!}z(p).{\boldsymbol{\nu}}x\>(\llbracket L\rrbracket_{p}\mid
x\leftrightarrow\bar{y})$ (replication theorem)
$\displaystyle\gtrsim{!}z(p).\llbracket
L\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p}$
(i.h.)

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

$\displaystyle{\boldsymbol{\nu}}x\>(\llbracket N\,L\rrbracket_{p}\mid
x\leftrightarrow\bar{y})$
$\displaystyle\equiv({\boldsymbol{\nu}}x,r\>)\left(\llbracket
N\rrbracket_{r}\mid\bar{r}(z,p^{\prime})\\!:({!}z(r^{\prime}).\llbracket
L\rrbracket_{r^{\prime}}\mid p\leftrightarrow\bar{p}^{\prime})\mid
x\leftrightarrow\bar{y}\right)$
$\displaystyle\sim{\boldsymbol{\nu}}r\>\begin{aligned}
(&{\boldsymbol{\nu}}x\>\left(\llbracket N\rrbracket_{r}\mid
x\leftrightarrow\bar{y}\right)\\\
&\mid\bar{r}(z,p^{\prime})\\!:({\boldsymbol{\nu}}x\>\left({!}z(r^{\prime}).\llbracket
L\rrbracket_{r^{\prime}}\mid x\leftrightarrow\bar{y}\right)\mid
p\leftrightarrow\bar{p}^{\prime}))\end{aligned}$ (replication theorem)
$\displaystyle\gtrsim{\boldsymbol{\nu}}r\>\left(\llbracket
N\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{r}\mid\bar{r}(z,p^{\prime})\\!:({!}z(r^{\prime}).\llbracket
L\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{r^{\prime}}\mid
p\leftrightarrow\bar{p}^{\prime})\right)$ (i.h. and the above expansion
relation) $\displaystyle=\llbracket
N\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$x$}\\}\,L\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p}$
$\displaystyle=\llbracket(N\,L)\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p}.$

###  4.2. Validity of $\beta$-reduction

The abstract encoding $\mathcal{A}$ validates $\beta$-reduction with respect
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$. The proof is similar to that for Milner’s encoding, except that
we exploit Lemma 5. We recall that $M\xrightarrow{\ }N$ is the _full_
$\beta$-reduction.

######  Lemma 6 (Substitution).

If $x\notin{{\rm\sf{fv}}}(N)$, then
${\boldsymbol{\nu}}x\>(\mathcal{A}\llbracket
M\rrbracket_{p}\mid{!}x(q).\mathcal{A}\llbracket
N\rrbracket_{q})\gtrsim\mathcal{A}\llbracket
M\\{\raisebox{2.15277pt}{\small$N$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p}$.

######  Proof 4.2.

By induction on the structure of $M$ using the replication theorem.

For the base case, we consider the case $M=x$; if $x\notin{{\rm\sf{fv}}}(M)$,
then we just need to apply the garbage collection law.

$\displaystyle{\boldsymbol{\nu}}x\>(\llbracket
x\rrbracket_{p}\mid{!}x(q).\llbracket M\rrbracket_{q})$
$\displaystyle={\boldsymbol{\nu}}x\>(\bar{x}(p^{\prime})\\!:p\leftrightarrow\bar{p}^{\prime}\mid{!}x(q).\llbracket
M\rrbracket_{q})$
$\displaystyle\gtrsim{\boldsymbol{\nu}}p^{\prime}\>(p\leftrightarrow\bar{p}^{\prime}\mid\llbracket
N\rrbracket_{p^{\prime}})$ (Lemma 3, and garbage collection on $x$)
$\displaystyle\gtrsim\llbracket M\rrbracket_{p}.$ (Lemma 5)

The case $M=\lambda x.M^{\prime}$ 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

$\displaystyle{\boldsymbol{\nu}}x\>\left(\llbracket
M_{1}\,M_{2}\rrbracket_{p}\mid{!}x(q).\llbracket N\rrbracket_{q}\right)$
$\displaystyle\equiv({\boldsymbol{\nu}}x,q)\>(\llbracket
M_{1}\rrbracket_{q}\mid\bar{q}(y,p^{\prime})\\!:\left({!}y(r).\llbracket
M_{2}\rrbracket_{r}\mid
p\leftrightarrow\bar{p}^{\prime}\right)\mid{!}x(q).\llbracket
N\rrbracket_{q})$ $\displaystyle\sim{\boldsymbol{\nu}}q\>\begin{aligned}
(&{\boldsymbol{\nu}}x\>\left(\llbracket
M_{1}\rrbracket_{q}\mid{!}x(q).\llbracket N\rrbracket_{q}\right)\mid\\\
&\bar{q}(y,p^{\prime})\\!:\left({\boldsymbol{\nu}}x\>\left({!}y(r).\llbracket
M_{2}\rrbracket_{r}\mid{!}x(q).\llbracket N\rrbracket_{q}\right)\mid
p\leftrightarrow\bar{p}^{\prime}\right))\end{aligned}$ (replication theorem
for parallel composition)
$\displaystyle\sim{\boldsymbol{\nu}}q\>\begin{aligned}
(&{\boldsymbol{\nu}}x\>\left(\llbracket
M_{1}\rrbracket_{q}\mid{!}x(q).\llbracket N\rrbracket_{q}\right)\mid\\\
&\bar{q}(y,p^{\prime})\\!:\left({!}y(r).{\boldsymbol{\nu}}x\>\left(\llbracket
M_{2}\rrbracket_{r}\mid{!}x(q).\llbracket N\rrbracket_{q}\right)\mid
p\leftrightarrow\bar{p}^{\prime}\right))\end{aligned}$ (replication theorem
for replicated input)
$\displaystyle\gtrsim{\boldsymbol{\nu}}q\>\left(\llbracket
M_{1}\\{\raisebox{2.15277pt}{\small$N$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{q}\mid\bar{q}(y,p^{\prime})\\!:\left({!}y(r).\llbracket
M_{2}\\{\raisebox{2.15277pt}{\small$N$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{r}\mid
p\leftrightarrow\bar{p}^{\prime}\right)\right)$ (i.h.)
$\displaystyle=\llbracket(M_{1}\,M_{2})\\{\raisebox{2.15277pt}{\small$N$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p}$

######  Theorem 7.

If $M\xrightarrow{\ }N$, then $\mathcal{A}\llbracket
M\rrbracket_{p}\gtrsim\mathcal{A}\llbracket N\rrbracket_{p}$.

######  Proof 4.3.

It suffices to show that $\llbracket(\lambda
x.M)\,N\rrbracket_{p}\gtrsim\llbracket
M\\{\raisebox{2.15277pt}{\small$N$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p}$
because the other cases follow from the precongruence of $\gtrsim$. We have

$\displaystyle\llbracket(\lambda x.M)\,N\rrbracket_{p}$
$\displaystyle={\boldsymbol{\nu}}q\>\left(q(x,r)\colon\llbracket
M\rrbracket_{r}\mid\bar{q}(y,p^{\prime})\\!:\left({!}y(r^{\prime}).\llbracket
N\rrbracket_{r^{\prime}}\mid
p\leftrightarrow\bar{p}^{\prime}\right)\right)\qquad(\text{$q$ is fresh})$
$\displaystyle\gtrsim({\boldsymbol{\nu}}y,p^{\prime}\>)\left(\llbracket
M\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p^{\prime}}\mid{!}y(r^{\prime}).\llbracket
N\rrbracket_{r^{\prime}}\mid p\leftrightarrow\bar{p}^{\prime}\right)$ (Lemma 3
and 5) $\displaystyle\gtrsim{\boldsymbol{\nu}}y\>\left(\llbracket
M\\{\raisebox{2.15277pt}{\small$y$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p}\mid{!}y(r^{\prime}).\llbracket
N\rrbracket_{r^{\prime}}\right)$ (Lemma 5) $\displaystyle\gtrsim\llbracket
M\\{\raisebox{2.15277pt}{\small$N$}\\!/\\!\mbox{\small$x$}\\}\rrbracket_{p}$
(Lemma 6)

as desired.

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 8.

Let ${=_{\pi}}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\\{(M,N)\mid\mathcal{A}\llbracket
M\rrbracket\approx\mathcal{A}\llbracket N\rrbracket\\}$. Then $=_{\pi}$ is a
$\lambda$-theory, that is, a congruence on $\lambda$-terms that contains
$\beta$-equivalence.

######  Remark 9.

From a $\lambda$-theory, a $\lambda$-model can be extracted [Bar84], hence
Corollary 8 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 [San00], as opposed to the processes
in the image of the encoding) because our proofs rely on Lemma 5, and such a
lemma cannot be extended to the set of all processes.

##  5\. 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 2.

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

$({\boldsymbol{\nu}}p_{0},p_{1})\>(\begin{aligned}
&\bar{x}(p_{0}^{\prime})\\!:p_{0}^{\prime}\leftrightarrow\bar{p}_{0}\\\
&\mid\bar{p}_{0}(x_{1}.p_{1}^{\prime})\\!:\left({!}x_{1}(r_{1}).\llbracket
M\rrbracket_{r_{1}}\mid p_{1}\leftrightarrow\bar{p}_{1}^{\prime}\right)\\\
&\mid\bar{p}_{1}(x_{2},p_{2})\\!:\left({!}x_{2}(r_{2}).\llbracket
N\rrbracket_{r_{2}}\mid p\leftrightarrow\bar{p}_{2}\right))\end{aligned}$

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}^{\prime}$.

$\displaystyle\mathcal{O}\llbracket x\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\bar{x}(p^{\prime})\\!:p\leftrightarrow\bar{p}^{\prime}$
$\displaystyle\mathcal{O}\llbracket\lambda x.M\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}p(x,q)\colon\mathcal{O}\llbracket M\rrbracket_{q}$
$\displaystyle\mathcal{O}\llbracket x\,M_{1}\cdots M_{n}\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
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$ $\displaystyle\mathcal{O}\llbracket(\lambda
x.M_{0})\,M_{1}\cdots M_{n}\rrbracket_{p}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{\boldsymbol{\nu}}p_{0}\>\left(p_{0}(x,q)\colon\mathcal{O}\llbracket
M_{0}\rrbracket_{q}\mid\mathcal{O}^{n}\langle p_{0},p,\mathcal{O}\llbracket
M_{1}\rrbracket\cdots\mathcal{O}\llbracket M_{n}\rrbracket\rangle\right)$
$\displaystyle\mathcal{O}^{n}\langle p_{0},p,\mathcal{O}\llbracket
M_{1}\rrbracket\cdots\mathcal{O}\llbracket M_{n}\rrbracket\rangle$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\begin{array}[t]{l}\bar{p}_{0}(x_{1},p_{1})\\!:\cdots\bar{p}_{n-1}(x_{n},p_{n})\\!:\\\
\left({!}x_{1}(r_{1}).\mathcal{O}\llbracket
M_{1}\rrbracket_{r_{1}}\mid\cdots\mid{!}x_{n}(r_{n}).\mathcal{O}\llbracket
M_{n}\rrbracket_{r_{n}}\mid p\leftrightarrow\bar{p}_{n}\right)\end{array}$
Figure 3. Optimised encoding. (The number $n$ is greater than $0$ in the last
three cases.)

In the optimised encoding $\mathcal{O}$, in Figure 3, 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\geq 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}\langle
p_{0},p,\mathcal{O}\llbracket M_{1}\rrbracket\cdots\mathcal{O}\llbracket
M_{n}\rrbracket\rangle$ is used for a compact representation of the encoding
of the trailing arguments $M_{1},\ldots,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 4 for the unoptimised encoding
$\mathcal{A}$ hold for $\mathcal{O}$. For instance, $\mathcal{O}$ validates
$\beta$-reduction (Lemma 10). 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 10.

If $M\xrightarrow{\ }N$, then $\mathcal{O}\llbracket
M\rrbracket_{p}\gtrsim\mathcal{O}\llbracket N\rrbracket_{p}$.

######  Lemma 11.

$\mathcal{A}\llbracket M\rrbracket_{p}\gtrsim\mathcal{O}\llbracket
M\rrbracket_{p}$.

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

######  Lemma 12.

If $\mathcal{O}\llbracket M\rrbracket_{p}\xrightarrow{\tau}P$ then there
exists $N$ such that $M\xrightarrow{\ }_{\tt{sn}}N$ and
$P\gtrsim\mathcal{O}\llbracket N\rrbracket_{p}$.

######  Lemma 13.

If $\mathcal{O}\llbracket M\rrbracket_{p}\xrightarrow{\mu}P$ and $\mu$ is an
input action, then $\mu$ is an input at $p$.

If $M=\lambda x.M^{\prime}$, then its process encoding $\mathcal{O}\llbracket
M\rrbracket_{p}$ can always do an input at $p$, as the encoding of a
abstraction begins with an input at its location name. Lemma 13 says that such
an input at $p$ is indeed the only possible input; that is, we cannot observe
an inner $\lambda$-abstraction (i.e., a $\lambda$-abstraction in
$M^{\prime}$).

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 14.

Let $M$ be a $\lambda$-term. If $\mathcal{O}\llbracket
M\rrbracket_{p}\xrightarrow{\overline{x}(q)}P$ for some $P$, then $M$ has a
head normal form $\lambda\widetilde{y}.x\,\widetilde{M}$, for some (possibly
empty) sequence of terms $\widetilde{M}$ and variables $\widetilde{y}$ with
$x\notin\widetilde{y}$.

######  Lemma 15.

Let $M$ be an unsolvable term. Then there does not exist an output action
$\mu$ such that $\mathcal{O}\llbracket M\rrbracket_{p}\xRightarrow{\mu}P$ for
some $P$.

######  Corollary 16.

$M$ is solvable then there are input actions $\mu_{1},\ldots,\mu_{n}$ ($n\geq
0$) and an output action $\mu$ such that $\mathcal{O}\llbracket
M\rrbracket_{p}\xRightarrow{\mu_{1}}\ldots\xRightarrow{\mu_{n}}\xRightarrow{\mu}P$,
for some $P$.

By Lemma 11, Corollary 16 also holds for $\mathcal{A}$. The converse of
Corollary 16 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 2.

We conclude by looking, as an example, at the unsolvable term
$\Omega\stackrel{{\scriptstyle\mbox{\scriptsize def}}}{{=}}(\lambda
x.x\,x)\,(\lambda x.x\,x)\,$. The process
$\mathcal{O}\llbracket\Omega\rrbracket_{p}$ is

${\boldsymbol{\nu}}p_{0}\>(\begin{aligned}
&p_{0}(x,q)\colon\bar{x}(q_{0})\\!:\bar{q}_{0}(y_{1},q_{1})\\!:\left({!}y_{1}(r_{1}).\mathcal{O}\llbracket
x\rrbracket_{r_{1}}\mid q\leftrightarrow\bar{q}_{1}\right)\\\
&\mid\bar{p}_{0}(x_{1},p_{1})\\!:\left({!}x_{1}(r_{1}).\mathcal{O}\llbracket\lambda
x.x\,x\rrbracket_{r_{1}}\mid p\leftrightarrow\bar{p}_{1}\right))\end{aligned}$

The only action $\mathcal{O}\llbracket\Omega\rrbracket_{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.

##  6\. 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 in which the input and output of the location wires
are performed.

###  6.1. Definition of the concrete wires

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
($\mathtt{IO}$, $\mathtt{OI}$, $\mathtt{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\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{b}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}P$ rather than
${\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}(a,b)\,P$).

#### I-O wires

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

$\displaystyle
p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}p(y,p_{1}).\bar{q}(x,q_{1})\\!:(p_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q}_{1}\mid
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{y})$
$\displaystyle
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{y}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{!}x(p).\bar{y}(q)\\!:p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q}$

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

$\displaystyle
p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}p(y,p_{1}).\begin{aligned}
({\boldsymbol{\nu}}x,q_{1})\>(&\overline{q}(x^{\prime},q_{1}^{\prime}).(q_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q}_{1}^{\prime}\mid
x^{\prime}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{x})\\\
&\mid
p_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q}_{1}\mid
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{y})\end{aligned}$
$\displaystyle
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{y}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{!}x(p).{\boldsymbol{\nu}}q\>(\overline{y}(q^{\prime}).q\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q}^{\prime}\mid
p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q})$

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) [HY95, Mer01, MS04, Bor98]. 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}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\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 3), 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 2) 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’:

$\displaystyle
p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{OI}$}}}}{\leftrightarrow}\overline{q}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{\overline{q}(x,q_{1}).p(y,p_{1})\colon}({p_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{OI}$}}}}{\leftrightarrow}\overline{q_{1}}}\mid{x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{OI}$}}}}{\leftrightarrow}\overline{y}})$
$\displaystyle
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{OI}$}}}}{\leftrightarrow}\overline{y}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{!}x(p).\bar{y}(q)\\!:p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{OI}$}}}}{\leftrightarrow}\overline{q}$

######  Remark 17 (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(\widetilde{b})$ is made into an output
$\overline{p}{(\widetilde{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.

$\displaystyle
p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}p(y,p_{1})\colon\bar{q}(x,q_{1})\\!:(p_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{1}\mid
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{y})$
$\displaystyle
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{y}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{!}x(p).\bar{y}(q)\\!:p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}$

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

$\displaystyle
p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}({\boldsymbol{\nu}}p_{1},q_{1}x,y)\>\begin{aligned}
(&p(y^{\prime},p_{1}^{\prime}).(p_{1}^{\prime}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{1}\mid
y\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{y}^{\prime})\mid\\\
&\overline{q}(q_{1}^{\prime},x^{\prime}).(q_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{1}^{\prime}\mid
x^{\prime}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x})\mid\\\
&p_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{1}\mid
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{y})\end{aligned}$
$\displaystyle
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{y}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{!}x(p).{\boldsymbol{\nu}}q\>(\overline{y}(q^{\prime}).q\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}^{\prime}\mid
p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q})$

The wire
$p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}$
is dual of itself: due to the use of permeable prefixes, swapping input and
output prefixes has no behavioural effect.

###  6.2. Transitivity and well-definedness of the concrete wires

All three wires introduced in the previous subsection are well defined:

######  Lemma 18.

The I-O wires, O-I wires and P wires are indeed wires; that is, they satisfy
the laws of Definition 2.

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 algebraic reasoning is done in a similar manner
for all the three wires.

Here, _we shall only give the proof of the transitivity of P wires_ since it
is the most delicate one, because of the concurrency allowed by permeable
prefixes and because permeable prefixes are defined in terms of the wires
themselves. The proofs of the transitivity of the other two wires, and the
proofs for the other laws are reported in Appendix C.

To illustrate the difficulty of P wires, let us consider the wires
${\boldsymbol{\nu}}q\>(p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}\mid
q\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{r})$.
This process can immediately reduce at the internal name $q$. Moreover, the
derivative

$p(p_{1},y)\colon\bar{r}(q_{1},x)\\!:\begin{aligned}
(&({\boldsymbol{\nu}}z_{1},z_{2})\>(x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{z}_{1}\mid
z_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{z}_{2}\mid
z_{2}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{y})\mid\\\
&({\boldsymbol{\nu}}s_{1},s_{2})\>(p_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{s}_{1}\mid
s_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{s}_{2}\mid
s_{2}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{1}))\end{aligned}$

shows that the reduction has made the chain of wires longer. To deal with
these cases, we strengthen the claim and show the transitivity of chains of
wires. In doing so, we crucially rely on up-to proof techniques for I$\pi$,
notably ‘expansion up-to expansion and context’, and several algebraic laws
(cf. Section 2.2.1). The ‘up-to context’ is used to cut out common contexts
such as $p(p_{1},y)\colon\bar{r}(q_{1},x)\\!:([\cdot]\mid[\cdot])$. The
algebraic laws are used to transform the processes so to be able to apply the
‘up-to context’, mainly by performing internal interactions. It is unclear how
the proof could be carried out without such proof techniques.

As we need to consider chains of P wires of arbitrary length, we introduce a
notation for them. We thus set:

$\displaystyle\mathrm{chain}_{\mathtt{P}}^{1}(p,q)$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q}$
$\displaystyle\mathrm{chain}_{\mathtt{P}}^{n+1}(p,q)$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{\boldsymbol{\nu}}r\>(\mathrm{chain}_{\mathtt{P}}^{n}(p,r)\mid
r\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{q})$
$\displaystyle\mathrm{chain}_{\mathtt{P}}^{1}(x,y)$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{y}$
$\displaystyle\mathrm{chain}_{\mathtt{P}}^{n+1}(x,y)$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}{\boldsymbol{\nu}}z\>(\mathrm{chain}_{\mathtt{P}}^{n}(x,z)\mid
z\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{y})$

where $r\notin\\{p,q\\}$ and $z\notin\\{x,y\\}$.

Now we are ready to show the transitivity of P wires.

######  Lemma 19.

The P wires
$p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}$
and
$x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{y}$
are transitive, that is,
${\boldsymbol{\nu}}q\>(p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}\mid
q\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{r})\gtrsim
p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{r}$
and
${\boldsymbol{\nu}}y\>(x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{y}\mid
y\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{z})\gtrsim
x\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{z}$.

######  Proof 6.1.

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

$\displaystyle{\mathrel{\mathcal{R}}_{1}}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\left\\{\left(p_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{n},\mathrm{chain}_{\mathtt{P}}^{n}(p_{0},p_{n})\right)\;\mathbin{}\middle|\mathbin{}\;n\geq
2\right\\}$ $\displaystyle{\mathrel{\mathcal{R}}_{2}}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\left\\{\left(x_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{n},\mathrm{chain}_{\mathtt{P}}^{n}(x_{0},x_{n})\right)\;\mathbin{}\middle|\mathbin{}\;n\geq
2\right\\}$

We show that ${\mathrel{\mathcal{R}}_{1}}\cup{\mathrel{\mathcal{R}}_{2}}$ is
an expansion up-to $\lesssim$ and context.

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}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{i+1}$
is of the form

$\displaystyle({\boldsymbol{\nu}}x_{i}^{+},q_{i}^{+},x_{i+1}^{-},q_{i+1}^{-}\>)$
$\displaystyle($ $\displaystyle
p_{i}(x_{i},q_{i}).(x_{i}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{i}\mid
q_{i}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{i}^{+})$
$\displaystyle\mid\overline{p_{i+1}}(x_{i+1},q_{i+1}).(x_{i+1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{i+1}^{-}\mid
q_{i+1}^{-}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{i+1})$
$\displaystyle\mid
x_{i+1}^{-}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{i}^{+}\mid
q_{i}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{i+1}^{-})$

Therefore, given

$\mathrm{chain}_{\mathtt{P}}^{n}(p_{0},p_{n})\equiv({\boldsymbol{\nu}}p_{1},\ldots,p_{n-1})\>(p_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{1}\mid\cdots\mid
p_{n-1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{n})\,,$

reducing the process by executing all the (internal) interactions at the
$p_{i}$’s, gives us a process of the form

$\displaystyle({\boldsymbol{\nu}}x_{0}^{+},x_{1}^{-},x_{1},x_{1}^{+},\ldots,x_{n-1}^{-},x_{n-1},x_{n-1}^{+},x_{n}^{-}\>)$
$\displaystyle({\boldsymbol{\nu}}q_{0}^{+},q_{1}^{-},q_{1},q_{1}^{+},\ldots,q_{n-1}^{-},q_{n-1},q_{n-1}^{+},q_{n}^{-}\>)$
$\displaystyle(p_{0}(x_{0},q_{0}).(x_{0}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{0}\mid
q_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{0}^{+})$
$\displaystyle\mid\overline{p_{n}}(x_{n},q_{n}).(x_{n}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{n}^{-}\mid
q_{n}^{-}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{n})$
$\displaystyle\mid
q_{0}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{1}^{-}\mid
q_{1}^{-}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{1}\mid
q_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{1}^{+}\mid\cdots$
$\displaystyle\mid
q_{n-1}^{-}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{n-1}\mid
q_{n-1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{n-1}^{+}\mid
q_{n-1}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{n}^{-}$
$\displaystyle\mid
x_{n}^{-}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{n-1}^{+}\mid
x_{n-1}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{n-1}\mid
x_{n-1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{n-1}^{-}\mid\cdots$
$\displaystyle\mid
x_{1}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{1}\mid
x_{1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{1}^{-}\mid
x_{1}^{-}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{0}^{+})$

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

$\displaystyle({\boldsymbol{\nu}}x_{0}^{+},x_{n}^{-}\>)({\boldsymbol{\nu}}q_{0}^{+},q_{n}^{-}\>)$
$\displaystyle(p_{0}(x_{0},q_{0}).(x_{0}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{0}\mid
q_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{0}^{+})$
$\displaystyle\mid\overline{p_{n}}(x_{n},q_{n}).(x_{n}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{n}^{-}\mid
q_{n}^{-}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{n})$
$\displaystyle\mid\mathrm{chain}_{\mathtt{P}}^{3n+1}(q_{0}^{+},q_{n+1}^{-})\mid\mathrm{chain}_{\mathtt{P}}^{3n+1}(x_{n+1}^{-},x_{0}^{+}))$
$\displaystyle\equiv
p_{0}(x_{0},q_{0})\colon\bar{p}_{n+1}(x_{n+1},q_{n+1})\\!:(\mathrm{chain}_{\mathtt{P}}^{3n-2}(x_{n},x_{0})\mid\mathrm{chain}_{\mathtt{P}}^{3n-2}(q_{0},q_{n}))$

Moreover, since the reductions performed are all at restricted linear names,
in each reduction the initial process is in the relation $\gtrsim$ with the
derivative process; that is, for any $n\geq 2$, we have

$\displaystyle\mathrm{chain}_{\mathtt{P}}^{n}(p_{0},p_{n})$
$\displaystyle\gtrsim
p_{0}(x_{0},q_{0})\colon\bar{p}_{n}(x_{n},q_{n})\\!:(\mathrm{chain}_{\mathtt{P}}^{3n-2}(x_{n},x_{0})\mid\mathrm{chain}_{\mathtt{P}}^{3n-2}(q_{0},q_{n}))$
(2)

Exploiting this property, we can prove that
${\mathrel{\mathcal{R}}_{1}}\cup{\mathrel{\mathcal{R}}_{2}}$ is an expansion
up-to expansion and context. We first consider the case where
$p_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{n}\mathrel{\mathcal{R}}_{1}\mathrm{chain}_{\mathtt{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 right-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

$({\boldsymbol{\nu}}p_{1},\ldots,p_{n-1}\>)(p_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{1}\mid\cdots\mid
p_{n-1}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\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\leq i\leq n-1$. We can execute the interactions at the
remaining $p_{i}$’s, and then, using the property (2) above, we have

$\displaystyle P\gtrsim
p_{0}(x_{0},q_{0})\colon\bar{p}_{n+1}(x_{n},q_{n})\\!:(\mathrm{chain}_{\mathtt{P}}^{3n-2}(x_{n},x_{0})\mid\mathrm{chain}_{\mathtt{P}}^{3n-2}(q_{0},q_{n})).$

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

$\displaystyle
p_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{n}=p_{0}(x_{0},q_{0})\colon\bar{p}_{n}(x_{n},q_{n})\\!:(x_{n}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{0}\mid
q_{n}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{0})\;,$
$\displaystyle
x_{n}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{0}\mathrel{\mathcal{R}}_{2}\mathrm{chain}_{\mathtt{P}}^{3n-2}(x_{n},x_{0})\;,$
$\displaystyle
q_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{n}\mathrel{\mathcal{R}}_{1}\mathrm{chain}_{\mathtt{P}}^{3n-2}(q_{0},q_{n})$

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

$\mathrm{chain}_{\mathtt{P}}^{n}(p_{0},p_{n})\xrightarrow{p_{0}(x_{0},q_{0})}P,$

then we can show that

$P\gtrsim({\boldsymbol{\nu}}x_{0}^{+},q_{0}^{+}\>)(x_{0}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{0}\mid
q_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{0}^{+}\mid\bar{p}_{n}(x_{n},q_{n})\\!:(\mathrm{chain}_{\mathtt{P}}^{3n-2}(x_{n},x_{0}^{+})\mid\mathrm{chain}_{\mathtt{P}}^{3n-2}(q_{0}^{+},q_{n}))).$

We can match this transition with

$\displaystyle
p_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{n}\xrightarrow{p_{0}(x_{0},q_{0})}({\boldsymbol{\nu}}x_{0}^{+},q_{0}^{+}\>)(x_{0}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{0}\mid
q_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{0}^{+}\mid\bar{p}_{n}(x_{n},q_{n})\\!:(x_{n}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{0}^{+}\mid
q_{0}^{+}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{n})).$

Once again, since

$\displaystyle
x_{n}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{0}\mathrel{\mathcal{R}}_{2}\;,$
$\displaystyle
q_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{q}_{n}\mathrel{\mathcal{R}}_{1}\mathrm{chain}_{\mathtt{P}}^{3n-2}(q_{0},q_{n})$

we can appeal to the up-to expansion and context technique to finish the case.

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

Now we sketch the case for variable names. Take

$x_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{n}\mathrel{\mathcal{R}}_{2}\mathrm{chain}_{\mathtt{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}$. By a reasoning similar to that of the location
wires, we can show that if

$\mathrm{chain}_{\mathtt{P}}^{n}(x_{0},x_{n})\xrightarrow{x_{0}(p_{0})}P$

then

$P\gtrsim\begin{aligned}
&\mathrm{chain}_{\mathtt{P}}^{n}(x_{0},x_{n})\mid\bar{x}_{n}(p_{n})\\!:\mathrm{chain}_{\mathtt{P}}^{2n-1}(p_{0},p_{n})\end{aligned}$

by executing the interactions at the $x_{i}$’s. The above transition can be
matched by the transition
$x_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{n}\xrightarrow{x_{0}(p_{0})}x_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{x}_{n}\mid\bar{x}_{n}(p_{n})\\!:p_{0}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{P}$}}}}{\leftrightarrow}\bar{p}_{n}$,
and we can conclude by using the up-to context technique.

######  Remark 20.

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 2 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 2) with
the I-O wires, O-I wires, and P wires. We denote the resulting (concrete)
encodings as $\mathcal{A}_{\tt{IO}}$, $\mathcal{A}_{\tt{OI}}$, and
$\mathcal{A}_{\tt{P}}$, respectively. Similarly $\mathcal{O}_{\tt{IO}}$,
$\mathcal{O}_{\tt{OI}}$, and $\mathcal{O}_{\tt{P}}$ are the instantiations of
the abstract optimised encoding $\mathcal{O}$. For instance, in
$\mathcal{A}_{\tt{IO}}$ and $\mathcal{O}_{\tt{IO}}$ an abstract wire
$a\leftrightarrow\bar{b}$ is instantiated with the corresponding concrete wire
$a\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{b}$;
and similarly for O-I wires and P wires.

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

##  7\. Full Abstraction for LTs and BTs

In this section we consider $\mathcal{A}_{\tt{IO}}$ and
$\mathcal{A}_{\tt{OI}}$, and prove full abstraction with respect to the BTs
and LTs, respectively. The main proof is given in Section 7.2. Before that, in
Section 7.1, we discuss the difference between $\mathcal{A}_{\tt{IO}}$ and
$\mathcal{A}_{\tt{OI}}$ on the encoding of unsolvable terms because it
highlights the difference between the two encodings. Some lemmas about the
encoding of unsolvable terms given in Section 7.1 will also play key roles in
the main proof. In the proofs we exploit the optimised encodings
$\mathcal{O}_{\tt{OI}}$ and $\mathcal{O}_{\tt{IO}}$.

###  7.1. Encoding of unsolvable terms

We recall that the differences between BTs and LTs are due to the treatment of
unsolvable terms (cf. Section 2.1). 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 16, in the abstract optimised
encoding $\mathcal{O}$ process $\mathcal{O}\llbracket\Omega\rrbracket_{p}$ is:

$\displaystyle{\boldsymbol{\nu}}p_{0}\>($ $\displaystyle
p_{0}(x,q)\colon\bar{x}(q_{0})\\!:\bar{q}_{0}(y_{1},q_{1})\\!:\left({!}y_{1}(r_{1}).\mathcal{O}\llbracket
x\rrbracket_{r_{1}}\mid q\leftrightarrow\bar{q}_{1}\right)$
$\displaystyle\mid\bar{p}_{0}(x_{1},p_{1})\\!:\left({!}x_{1}(r_{1}).\mathcal{O}\llbracket\lambda
x.x\,x\rrbracket_{r_{1}}\mid p\leftrightarrow\bar{p}_{1}\right)).$

Its instantiation with O-I wires,
$\mathcal{O}_{\tt{OI}}\llbracket\Omega\rrbracket_{p}$, cannot do any input
action: as $p\leftrightarrow\bar{p}_{1}$ becomes the O-I wire
$p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{OI}$}}}}{\leftrightarrow}\overline{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}_{\tt{OI}}\llbracket\Omega\rrbracket_{p}$ can perform is (up-to
expansion)
$\mathcal{O}_{\tt{OI}}\llbracket\Omega\rrbracket_{p}\xrightarrow{\tau}\gtrsim\mathcal{O}_{\tt{OI}}\llbracket\Omega\rrbracket_{p}$,
which corresponds to the reduction $\Omega\xrightarrow{\ }\Omega$. Hence,
$\mathcal{O}_{\tt{OI}}\llbracket\Omega\rrbracket_{p}$ cannot match the input
action $\mathcal{O}_{\tt{OI}}\llbracket\lambda
x.\Omega\rrbracket_{p}\xrightarrow{p(x,q)}\mathcal{O}_{\tt{OI}}\llbracket\Omega\rrbracket_{q}$,
and the two processes are distinguished.

In contrast, with I-O wires, processes $\mathcal{O}_{\tt{IO}}\llbracket\lambda
x.\Omega\rrbracket_{p}$ and
$\mathcal{O}_{\tt{IO}}\llbracket\Omega\rrbracket_{p}$ are indistinguishable.
As before, the former process can exhibit an input transition
$\mathcal{O}_{\tt{IO}}\llbracket\lambda
x.\Omega\rrbracket_{p}\xrightarrow{p(x,q)}\mathcal{O}_{\tt{IO}}\llbracket\Omega\rrbracket_{q}$.
However, now $\mathcal{O}_{\tt{IO}}\llbracket\Omega\rrbracket_{p}$ has a
matching input transition, because when $p\leftrightarrow\bar{p}_{1}$ is the
I-O wire
$p\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{p}_{1}$,
the input at $p$ is not guarded. The derivative of the input $p(y,q)$ is

$\displaystyle\begin{aligned}
{\boldsymbol{\nu}}p_{0}\>(&p_{0}(x,q)\colon\mathcal{O}_{\tt{IO}}\llbracket
x\,x\rrbracket_{q}\\\
&\mid\bar{p}_{0}(x_{1},p_{1})\\!:({!}x_{1}(r_{1}).\mathcal{O}_{\tt{IO}}\llbracket\lambda
x.x\,x\rrbracket_{r_{1}}\\\
&\mid\bar{p}_{1}(x_{2},p_{2})\\!:(x_{2}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{y}\mid
q\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{p}_{2})))\end{aligned}$
$\displaystyle\begin{aligned}
={\boldsymbol{\nu}}p_{0}\>(&p_{0}(x,q)\colon\mathcal{O}_{\tt{IO}}\llbracket
x\,x\rrbracket_{q}\\\
&\mid\bar{p}_{0}(x_{1},p_{1})\\!:({!}x_{1}(r_{1}).\mathcal{O}_{\tt{IO}}\llbracket\lambda
x.x\,x\rrbracket_{r_{1}}\\\
&\mid\bar{p}_{1}(x_{2},p_{2})\\!:({!}x_{2}(r_{2}).\mathcal{O}_{\tt{IO}}\llbracket
y\rrbracket_{r_{2}}\mid
q\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{p}_{2})))\end{aligned}$
$\displaystyle\equiv\mathcal{O}_{\tt{IO}}\llbracket\Omega\,y\rrbracket_{q}$

(exploiting the definitions of $\mathcal{O}_{\tt{IO}}\llbracket
y\rrbracket_{r_{2}}$ and
$x_{2}\underset{\text{\raisebox{2.15277pt}[0.0pt][0.0pt]{\scalebox{0.9}{$\mathtt{IO}$}}}}{\leftrightarrow}\bar{y}$).
In a similar manner, one then shows that
$\mathcal{O}_{\tt{IO}}\llbracket\Omega\rrbracket_{q}$ and
$\mathcal{O}_{\tt{IO}}\llbracket\Omega\,y\rrbracket_{q}$ can match each
other’s transitions, and iteratively so, on the resulting derivatives. These
observations are not limited to $\Omega$ and $\lambda x.\Omega$, but can be
said against general unsolvable terms. Below we state these properties as
lemmas. Some of the proofs of the lemmas are given in Appendix D.

Only in $\mathcal{O}_{\tt{OI}}$ a term $\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p}$ can perform an input transition if and only if $M$ is, or may
reduce to, a function, say $M=\lambda x.M^{\prime}$, and the input action
intuitively corresponds to consuming the outermost ‘$\lambda x$’.

######  Lemma 21.

Let $M$ be an unsolvable term of order $n$, where $0<n\leq\omega$. Then
$\mathcal{O}_{\tt{OI}}\llbracket M\rrbracket_{p}$ can do a weak input
transition at $p$. Moreover, if $\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p}\xRightarrow{p(x,q)}P$, then there exists $N$ such that
$P\gtrsim\mathcal{O}_{\tt{OI}}\llbracket N\rrbracket_{q}$ and $N$ is an
unsolvable of order $n-1$ (under the assumption $\omega-1=\omega$).

In addition, only with $\mathcal{O}_{\tt{OI}}$ a process
$\mathcal{O}_{\tt{OI}}\llbracket M\rrbracket_{p}$ is bisimilar to
${\boldsymbol{0}}$ iff the term $M$ is an unsolvable of order $0$.

######  Lemma 22.

Let $M$ be an unsolvable term of order $0$. Then the only action
$\mathcal{O}_{\tt{OI}}\llbracket M\rrbracket_{p}$ can do is a $\tau$-action.

Therefore, we have:

######  Lemma 23.

Let $M$ and $N$ be unsolvables of order $m$ and $n$ respectively, where $0\leq
m,n\leq\omega$. Then $\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p}\approx\mathcal{O}_{\tt{OI}}\llbracket N\rrbracket_{p}$ iff
$m=n$.

######  Proof 7.1.

The only if direction is proved by contraposition. 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}_{\tt{OI}}\llbracket
M\rrbracket_{p}$ and $\mathcal{O}\llbracket N\rrbracket_{p}$ can do. By Lemmas
21 and 22, it follows that $\mathcal{O}_{\tt{OI}}\llbracket M\rrbracket_{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}_{\tt{OI}}\llbracket M\rrbracket_{p}$ can do is unbounded.

We now prove the if direction. We first prove the case for $n=m=0$, and use
that result to give the proof for arbitrary $n$.

For the case $n=m=0$, we show that the relation $\mathrel{\mathcal{R}}$
defined as

$\bigcup_{p}\\{(\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p},\mathcal{O}_{\tt{OI}}\llbracket N\rrbracket_{p})\mid\text{
$M,N$ unsolvables of order $0$}\\}$

is a bisimulation up-to expansion. Suppose that
$\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p}\mathrel{\mathcal{R}}\mathcal{O}_{\tt{OI}}\llbracket
N\rrbracket_{p}$. If $\mathcal{O}_{\tt{OI}}\llbracket M\rrbracket_{p}$ makes a
transition $\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p}\xrightarrow{\mu}P$, then $\mu=\tau$ by Lemma 22. Hence, we
have $P\gtrsim\mathcal{O}\llbracket M^{\prime}\rrbracket_{p}$ with
$M\xrightarrow{\ }M^{\prime}$ by Lemma 12. 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}_{\tt{OI}}\llbracket
M^{\prime}\rrbracket_{p}\mathrel{\mathcal{R}}\mathcal{O}_{\tt{OI}}\llbracket
N\rrbracket_{p}$. In other words, we can take $\mathcal{O}_{\tt{OI}}\llbracket
N\rrbracket_{p}\xRightarrow{}\mathcal{O}_{\tt{OI}}\llbracket N\rrbracket_{p}$
as the matching transition.

To conclude we show that the relation $\mathrel{\mathcal{R}}$ defined as

$\bigcup_{p}\left\\{(\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p},\mathcal{O}_{\tt{OI}}\llbracket
N\rrbracket_{p})\;\mathbin{}\middle|\mathbin{}\;\text{ $M,N$ are unsolvables
of the same order}\right\\}$

is a bisimulation up-to expansion. Suppose that
$\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p}\mathrel{\mathcal{R}}\mathcal{O}_{\tt{OI}}\llbracket
N\rrbracket_{p}$. The order $0$ case is exactly what we proved above, so let
us assume that $M$ and $N$ are unsolvable terms whose order is $n\neq 0$
(where $n$ may be $\omega$). Assume that $\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p}$ makes a transition $\mathcal{O}_{\tt{OI}}\llbracket
M\rrbracket_{p}\xrightarrow{\mu}P$. If $\mu=\tau$, then we can reason as we
did for the order 0 case. The only other possibility is the case where
$\mu=p(x,q)$ with $x,q$ being fresh. Then, by Lemmas 21, there exists
$M^{\prime}$ such that $P\gtrsim\mathcal{O}_{\tt{OI}}\llbracket
M^{\prime}\rrbracket_{q}$ and $M^{\prime}$ is an unsolvable of order $n-1$. By
Lemma 21, we have $\mathcal{O}_{\tt{OI}}\llbracket
N\rrbracket_{p}\xRightarrow{p(x,q)}Q\gtrsim\mathcal{O}_{\tt{OI}}\llbracket
N^{\prime}\rrbracket_{q}$ for some unsolvable term whose order coincides with
that of $M^{\prime}$. Since $M^{\prime}$ and $N^{\prime}$ are unsolvables of
the same order, we have $\mathcal{O}_{\tt{OI}}\llbracket
M^{\prime}\rrbracket_{q}\mathrel{\mathcal{R}}\mathcal{O}_{\tt{OI}}\llbracket
N^{\prime}\rrbracket_{q}$.

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

######  Lemma 24.

  1. (1)

If $M$ is an unsolvable of order $0$, then $\mathcal{O}_{\tt{IO}}\llbracket
M\rrbracket_{p}$ can do an input at $p$. Moreover, if
$\mathcal{O}_{\tt{IO}}\llbracket M\rrbracket_{p}\xrightarrow{p(x,q)}P$, then
$P\gtrsim\mathcal{O}_{\tt{IO}}\llbracket M\,x\rrbracket_{q}$.

  2. (2)

If $M$ is unsolvable, then $\mathcal{O}_{\tt{IO}}\llbracket M\rrbracket_{p}$
can do an input at $p$. Moreover, if $\mathcal{O}_{\tt{IO}}\llbracket
M\rrbracket_{p}\xrightarrow{p(x,q)}P$, then there exists an unsolvable term
$M^{\prime}$ such that $P\gtrsim\mathcal{O}_{\tt{IO}}\llbracket
M^{\prime}\rrbracket_{q}$.

######  Lemma 25.

For any unsolvable term $M$, we have $\mathcal{O}_{\tt{IO}}\llbracket
M\rrbracket_{p}\approx\mathcal{O}_{\tt{IO}}\llbracket\Omega\rrbracket_{p}$.

######  Proof 7.2.

We show that the relation $\mathrel{\mathcal{R}}$ defined as

$\bigcup_{p}\left\\{(\mathcal{O}_{\tt{IO}}\llbracket
M\rrbracket_{p},\mathcal{O}_{\tt{IO}}\llbracket N\rrbracket_{p})\mid\text{$M$
and $N$ are unsolvables}\right\\}$

is a bisimulation up-to expansion.

Suppose that $\mathcal{O}_{\tt{IO}}\llbracket
M\rrbracket_{p}\mathrel{\mathcal{R}}\mathcal{O}_{\tt{IO}}\llbracket
N\rrbracket_{p}$. We consider the case where $\mathcal{O}_{\tt{IO}}\llbracket
M\rrbracket_{p}$ makes the challenge; we omit the opposite case as it is
symmetrical. By Lemma 15 and 13, the only actions $P$ can do is either a
$\tau$-action or an input at $p$.

If $\mathcal{O}_{\tt{IO}}\llbracket M\rrbracket_{p}\xrightarrow{\tau}P$ then
we can take $\mathcal{O}_{\tt{IO}}\llbracket
N\rrbracket_{p}\xRightarrow{}\mathcal{O}_{\tt{IO}}\llbracket N\rrbracket_{p}$
as the matching transition because we have
$P\gtrsim\mathcal{O}_{\tt{IO}}\llbracket
M^{\prime}\rrbracket_{p}\mathrel{\mathcal{R}}\mathcal{O}_{\tt{IO}}\llbracket
N\rrbracket_{p}$ for some unsolvable term $M^{\prime}$ such that
$M\xrightarrow{\ }M^{\prime}$ by Lemma 12.

Assume that $\mathcal{O}_{\tt{IO}}\llbracket
M\rrbracket_{p}\xrightarrow{p(x,q)}P$. Then, thanks to 2 of Lemma 24, there
exists an unsolvable term $M^{\prime}$ such that
$P\gtrsim\mathcal{O}_{\tt{IO}}\llbracket M^{\prime}\rrbracket_{q}$. Similarly,
by 2 of Lemma 24, we have $\mathcal{O}_{\tt{IO}}\llbracket
N\rrbracket_{p}\xrightarrow{p(x,q)}\gtrsim\mathcal{O}_{\tt{IO}}\llbracket
N^{\prime}\rrbracket_{q}$ for some unsolvable term $N^{\prime}$. The claim
follows because $\mathcal{O}_{\tt{IO}}\llbracket
M^{\prime}\rrbracket_{q}\mathrel{\mathcal{R}}\mathcal{O}_{\tt{IO}}\llbracket
N^{\prime}\rrbracket_{q}$.

###  7.2. Full abstraction proofs

The goal of this subsection is to prove the following two theorems:

######  Theorem 26.

[Full abstraction for LT] $\text{LT}(M)=\text{LT}(N)$ if and only if
$\mathcal{A}_{\tt{OI}}\llbracket
M\rrbracket\approx\mathcal{A}_{\tt{OI}}\llbracket N\rrbracket$.

######  Theorem 27.

[Full abstraction for BT] $\text{BT}(M)\\!=\\!\text{BT}(N)$ if and only if
$\mathcal{A}_{\tt{IO}}\llbracket
M\rrbracket\approx\mathcal{A}_{\tt{IO}}\llbracket N\rrbracket$.

The proofs exploit work by Sangiorgi and Xu [SX18], which sets conditions for
obtaining full abstraction with respect to LTs and BTs in an encoding of the
$\lambda$-calculus into a process calculus. Our proofs go through each such
condition, showing that it is satisfied.

The rest of this sections is organised as follows. We first review the general
conditions given in [SX18] (Section 7.2.1). Then we show that
$\mathcal{A}_{\tt{OI}}$ satisfies the conditions for LTs and
$\mathcal{A}_{\tt{IO}}$ satisfies that for BTs (Section 7.2.2).

####  7.2.1. General conditions

Here we present a simplified version of the conditions given in [SX18],
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$ (the
conditions in [SX18] are parametric with respect to the calculus and its
behavioural relations). We also show that some conditions can be proved at the
level of the abstract (optimised) encoding $\mathcal{O}{}$.

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}\llbracket\lambda x.[\cdot]\rrbracket$ (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,\ldots,n\\}$, there exists a $\pi$-context
$D_{i}$ such that
$D_{i}[C[\widetilde{A}]]\gtrsim\overline{a}(\widetilde{b}).b(z).A\,_{i}\langle
z\rangle$ for fresh names $a,b,z$ such that $b\in\widetilde{b}$.

[[SX18]] Let $\mathcal{E}$ be an encoding of the $\lambda$-calculus into
I$\pi$. Suppose that the encoding satisfies the following conditions.

  1. (1)

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

  2. (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}\llbracket M\rrbracket$ for some
$\lambda$-term $M$;

  3. (3)

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

  4. (4)

If $M$ is an unsolvable of order $0$ then $\mathcal{E}\llbracket
M\rrbracket\approx\mathcal{E}\llbracket\Omega\rrbracket$;

  5. (5)

The terms $\mathcal{E}\llbracket\Omega\rrbracket$, $\mathcal{E}\llbracket
x\,\widetilde{M}\rrbracket$, $\mathcal{E}\llbracket
x\,\widetilde{M}^{\prime}\rrbracket$, and $\mathcal{E}\llbracket
y\,\widetilde{M}^{\prime\prime}\rrbracket$ are pairwise unrelated by
$\approx$, assuming that $x\neq y$ and that tuples $\widetilde{M}$ and
$\widetilde{M^{\prime}}$ have different lengths.

Then we have:

(LT):

if

  1. (1):

$M$, $N$ unsolvable of order $\omega$ implies that $\mathcal{E}\llbracket
M\rrbracket\approx\mathcal{E}\llbracket N\rrbracket$ and

  2. (2):

for any $M$ the term $\mathcal{E}\llbracket\lambda x.M\rrbracket$ is unrelated
by $\approx$ to $\mathcal{E}\llbracket\Omega\rrbracket$ and to any term of the
form $\mathcal{E}\llbracket x\,\widetilde{M}\rrbracket$,

then $\mathcal{E}$ and $\approx$ are fully abstract for LT equality;

(BT):

if

  1. (1):

$M$ solvable implies that the term $\mathcal{E}\llbracket\lambda
x.M\rrbracket$ is unrelated by $\approx$ to
$\mathcal{E}\llbracket\Omega\rrbracket$ and to any term of the form
$\mathcal{E}\llbracket x\,\widetilde{M}\rrbracket$, and

  2. (2):

$\mathcal{E}\llbracket
M\rrbracket\approx\mathcal{E}\llbracket\Omega\rrbracket$ whenever $M$ is
unsolvable of order $\omega$,

then $\mathcal{E}$ and $\approx$ are fully abstract for BT equality.

######  Remark 28.

The condition (2) is weaker than the original condition used in [SX18] (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
[SX18], whenever this condition about the inverse context is used, the holes
are indeed filled with encodings of $\lambda$-terms.

The existence of the inverse context can be proved at the abstract level
(i.e., for $\mathcal{O}$ and $\mathcal{A}$), and hence, it need not be proved
independently for $\mathcal{A}_{\tt{OI}}$ and $\mathcal{A}_{\tt{IO}}$.

######  Lemma 29.

The abstraction and variable contexts of $\mathcal{O}$ have inverse with
respect to $\lesssim$, _under the assumption that the every abstraction $F$
that fills the context satisfies $F=\mathcal{O}\llbracket M\rrbracket$ for
some $\lambda$-term $M$_.

The proof is by simple algebraic reasonings such as I- and O-respectfulness;
details are given in Appendix D.2.

####  7.2.2. Checking conditions for LT and BT

Thanks to the general conditions we described, to prove the full-abstraction
results, we only need to show that $\mathcal{A}_{\tt{OI}}$ and
$\mathcal{A}_{\tt{IO}}$ satisfy the required conditions. We first show that
$\mathcal{A}_{\tt{OI}}$ indeed satisfies the conditions for LT. See 26

######  Proof 7.3.

We check the conditions given in Theorem 7.2.1. It suffices to give the proof
for the optimised encoding $\mathcal{O}_{\tt{OI}}$.

Some conditions are trivial or have already been checked. The variable
contexts of $\mathcal{O}_{\tt{OI}}$ is clearly guarded, the condition about
the inverse context is Lemma 29, the validity of $\beta$ is Lemma 10 and we
have proved that unsolvable terms of order $0$ are equated (Lemma 23).

We first see that $\mathcal{O}_{\tt{OI}}\llbracket\Omega\rrbracket$,
$\mathcal{O}_{\tt{OI}}\llbracket x\,\widetilde{M}\rrbracket$,
$\mathcal{O}_{\tt{OI}}\llbracket x\,\widetilde{M}^{\prime}\rrbracket$ and
$\mathcal{O}_{\tt{OI}}\llbracket y\,\widetilde{M}^{\prime\prime}\rrbracket$
are pairwise unrelated under the assumption that $x\neq y$ and $\widetilde{M}$
and $\widetilde{M}^{\prime}$ have different lengths. Since
$\mathcal{O}_{\tt{OI}}\llbracket\Omega\rrbracket_{p}$ cannot do an output
action (Lemma 15), this process is different from the rest of the processes.
It is also obvious that $\mathcal{O}\llbracket
y\,\widetilde{M}^{\prime\prime}\rrbracket_{p}$ is different from
$\mathcal{O}_{\tt{OI}}\llbracket x\,\widetilde{M}\rrbracket$ and
$\mathcal{O}_{\tt{OI}}\llbracket x\,\widetilde{M}^{\prime}\rrbracket$. We are
left with checking that $\mathcal{O}_{\tt{OI}}\llbracket
x\,\widetilde{M}\rrbracket$ and $\mathcal{O}_{\tt{OI}}\llbracket
x\,\widetilde{M}^{\prime}\rrbracket$ are not bisimilar. Let
$m\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\mathopen{|}\widetilde{M}\mathclose{|}$ and
$n\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}\mathopen{|}\widetilde{M}^{\prime}\mathclose{|}$, and without loss
of generality, assume that $m<n$. Then $\mathcal{O}_{\tt{OI}}\llbracket
x\,\widetilde{M}\rrbracket_{p}$ can do an input at $p$ after $m+2$ outputs.
More concretely, we have $\mathcal{O}_{\tt{OI}}\llbracket
x\,\widetilde{M}\rrbracket_{p}\xrightarrow{\overline{x}(p_{0})}\xrightarrow{\overline{p_{0}}(x_{1},p_{1})}\cdots\xrightarrow{\overline{p_{n}}(x_{n+1},p_{n+1})}\xrightarrow{p(y,q)}P$
for some $P$. However, $\mathcal{O}_{\tt{OI}}\llbracket
x\,\widetilde{M^{\prime}}\rrbracket_{p}$ cannot do an input at $p$ after $m+2$
outputs, and thus these two processes are not bisimilar.

Now we look at the conditions in (LT) of Theorem 7.2.1. The condition 1 holds
because we have proved that unsolvable terms of order $\omega$ are equated
(Lemma 23). It remains to show the condition (2). Clearly,