# Vortex Excitations of Dirac Bose-Einstein Condensates

Joris Schaltegger  Nordita, KTH Royal Institute of Technology and Stockholm
University 106 91 Stockholm, Sweden  A.V. Balatsky  Nordita, KTH Royal
Institute of Technology and Stockholm University 106 91 Stockholm, Sweden
Department of Physics, University of Connecticut, Storrs, Connecticut 06269,
USA

(August 27, 2024)

## Abstract

We explore vortices in non-equilibrium Dirac Bose-Einstein condensates (Dirac
BEC) described by a stationary Dirac Gross-Pitaevskii equations (GPE). We find
that the multi-component structure of Dirac equation enables the difference in
phase winding of two condensates with respective phase winding number
differing by one, $\ell_{a}-\ell_{b}=\pm 1$. We observe three classes of
vortex states distinguished by their far-field behavior: A ring soliton on
either of the two components in combination with a vortex on the other
component, and, in the case of strong inter-component interactions, a vortex
profile on both components. The latter are multiple core vortices due to the
phase winding difference between the components. We also address the role of a
Haldane gap on these vortices, which has a similar effect than inter-component
by making the occupation on either sublattice more costly. We employ a
numerical shooting method to reliably identify vortex solutions and use it to
scan large parts of the phase space. We then use a classification algorithm on
the integrated wavefunctions to establish a phase diagram of the different
topological sectors.

##  I Introduction

Dirac nodes in the excitation spectrum of a condensed matter system are the
consequence of additional symmetries present, for example sublattice symmetry
in graphene and time-reversal symmetry in topological insulators. While most
of the time, fermionic Dirac and Weyl materials hosting electrons are studied,
the notion of Dirac materials can easily be extended to systems with bosonic
quasi-particles obeying analogous symmetries [1]. Indeed, Dirac or Weyl points
have been observed in a wide variety of bosonic excitations, for example in
photonic crystals [2, 3, 4], exciton-polariton condensates [5, 6], and
hexagonal magnets [7, 8, 9, 10, 11, 12, 13]. The defining feature of Dirac
materials is the existence of low-energy excitations that are described by the
Dirac equation rather than the Schrödinger equation. In fermionic systems, it
is possible to tune the Fermi level to the Dirac nodes, for example via
doping, which means that Dirac-like excitations can be studied in or near
thermal equilibrium. In contrast, the equilibrium chemical potential for
bosonic systems is close to zero at low temperatures, i.e. the ground state is
characterized by the absence of bosonic excitations. Maintaining a non-zero
chemical potential for bosonic degrees of freedom requires a continuous
external drive, just as is the case for other non-equilibrium condensates
where bosons are produced by an external source, typically optical or
microwave light. We will refer to these cases of condensates as pumped or non-
equilibrium condensates. The pumping of bosonic quasi-particles and subsequent
condensation is well-established for magnon [14, 15, 16, 17, 18, 19, 20, 21]
and exciton-polariton condensates [22, 23, 24, 25]. Such non-equilibrium
condensates are typically generated at the minimum of the dispersion, where
the lifetime of bosonic quasiparticles is expected to be the longest. Recent
experiments on thin-film yttrium iron garnets additionally observe a magnon
condensate at higher energy bands [26]. In light of this development, the
notion of a pumped condensate of Dirac bosons, first introduced by Sukhachov
et.al. [27], seems plausible.

In this paper, we explore the nature of vortices in Dirac BEC. As a specific
example, we focus on the case of two-dimensional, hexagonal magnets, such as
$\text{Cr}\text{I}_{3}$, where Dirac nodes appear in the magnon spectrum , but
the results about multiple core components and structure of Dirac BEC vortices
is general and applicable to other systems that support Dirac BEC. Following
Ref. [27], we use a phenomenological model for the free energy density of a
Dirac BEC, taking into consideration the spinor structure and linear kinetic
energy of the underlying Dirac equation. In our minimal model, we keep only
the most important interaction terms and restrict to stationary solutions of
the resulting Dirac Gross-Pitaevskii equations. We observe the following:

  1. 1.

The linear kinetic energy of the Dirac equation leads to the unusual case of
different winding numbers for the two sublattice components, related by
$\ell_{a}=\ell_{b}\pm 1$.

  2. 2.

As the consequence of different inter- vs intra-component interactions we
observe three distinct classes of topological excitations characterized by
their far-field behavior: The first two types consist of configurations with a
locally confined ring soliton on one sublattice, in combination with a vortex
configuration on the other sublattice. Which of the two components is dominant
depends on the relative interaction strengths and the Haldane gap. The third
type is characterized by a vortex configuration for both components, which
appears for sufficiently strong inter-component interactions. This class of
solutions is of particular interest because the angular momentum jump results
in multiple cores for the two components.

  3. 3.

To reach these conclusions we employ a numerical shooting algorithm to scan
large parts of the phase space spanned by the three independent model
parameters. We then use an cluster algorithm on the integrated radial
wavefunctions to compute the phase diagram of topological excitations.

  4. 4.

We find the phase diagram for multi-component Dirac BEC that shows that the
condensate with the lower winding number is favoured, which is consistent with
the lower rotational energy. However, tuning the Haldane gap and lowering the
interaction strength on the recessive sublattice can invert the occupation of
the condensate components. For sufficiently large inter-component
interactions, a multiple core vortex can occur. The Haldane gap and decreasing
the repulsion on the recessive component facilitates the onset of the mixed
phase.

  5. 5.

The phase diagrams are qualitatively similar for the topological sectors
$\ell_{a}=0,1(\ell_{b}=1,2)$.

The structure of this paper is as follows: After the introduction in section 1
we discuss a minimal model and the general setup for the analysis of vortices
in Dirac BEC in section 2. In section 3 we present the results for the
topologically distinct vortex states present in the Dirac BEC. In section 4 we
give an outlook and conclusion. We describe the numerical methods and shooting
algorithm for solving the Dirac GPE in Appendix A.

##  II Minimal model of Dirac BEC

Following Ref. [27], we use a phenomenological ansatz for the free energy of
the Dirac BEC,

$\displaystyle\mathcal{F}$
$\displaystyle=(c_{0}-\mu)n_{tot}+\Delta\sum_{\zeta=\pm}\big{(}n_{a,\zeta}-n_{b,\zeta}\big{)}-iv\Psi^{\dagger}\big{(}\tau_{z}\otimes\vec{\sigma}\cdot\vec{\nabla}\big{)}\Psi$
$\displaystyle+\sum_{\zeta=\pm}\big{[}\frac{1}{2}g_{a}n_{a,\zeta}n_{a,\zeta}+\frac{1}{2}g_{b}n_{b,\zeta}n_{b,\zeta}+g_{ab}n_{a,\zeta}n_{b,\zeta}\big{]}.$
(1)

Here, the wavefunction is expressed as the spinor
$\Psi=\begin{pmatrix}\psi_{a,+}&\psi_{b,+}&\psi_{a,-}&\psi_{b,-}\end{pmatrix}^{T}$,
where $a,b$ is the sublattice (or, more generally, pseudo-spin) index, and
$\zeta=\pm$ is the valley index. The condensate densities are denoted by
$n_{j,\zeta}=\psi_{j,\zeta}^{\dagger}\psi_{j,\zeta}$, and
$n_{tot}=\Psi^{\dagger}\Psi$ is the total density. Furthermore, $\vec{\sigma}$
is the vector of Pauli matrices, $\tau_{z}$ is the Pauli matrix in the valley
degree of freedom, $c_{0}$ is the energy of the Dirac nodes, $\mu$ is the
effective chemical potential generated by the external drive. To keep the
discussion general, we introduce the Haldane gap $\Delta$. The velocity
$v=\left|\frac{d\epsilon}{d\vec{k}}\right|_{\vec{k}_{D}}$ is the equivalent to
the Fermi velocity at the Dirac nodes. Here, the kinetic terms are linear in
derivatives due to the expansion around the Dirac point of the energy
spectrum. Note that we have restricted to interactions between sublattices;
the valley degrees of freedom are completely decoupled in our model. We remark
that interactions between different valleys can for example occur from
microscopic Kitaev interactions. For simplicity the valley index will be
dropped from now on. The origin of inter-component pseudo-spin interactions
can be motivated by calculating the next-to-leading order Holstein-Primakoff
transform of a Heisenberg ferromagnet on a honeycomb lattice [10]. An intra-
component repulsion is required for the spatial stability of the condensate
[28]. In magnon condensates in YIG, the observed repulsion is likely a
consequence of additional dipole interactions for non-uniform densities [21].

The Dirac Gross-Pitaevskii equations follow from the free energy density by
variation of the spinor components,

$\displaystyle i\partial_{t}\psi_{a}$
$\displaystyle=\left(c_{0}-\mu+\Delta\right)\psi_{a}-iv\left(\partial_{x}-i\partial_{y}\right)\psi_{b}+g_{a}n_{a}\psi_{a}+g_{ab}n_{b}\psi_{a},$
(2a) $\displaystyle i\partial_{t}\psi_{b}$
$\displaystyle=\left(c_{0}-\mu-\Delta\right)\psi_{b}-iv\left(\partial_{x}+i\partial_{y}\right)\psi_{a}+g_{b}n_{b}\psi_{b}+g_{ab}n_{a}\psi_{b}.$
(2b)

In the presence of an external drive, the Dirac GPE should be extended to take
into consideration the source and decay terms for the Dirac bosons. However,
here we assume a stationary state where the source and decay terms cancel each
other exactly. Homogeneous solutions of the stationary GPE have been discussed
in Ref. [27], where it is shown that, depending on the model parameters, the
ground state either has a non-zero density for both pseudo-spins, or one of
the components vanishes.

We now discuss spatially non-uniform vortex solutions of the Dirac GPE, which
are an example of a self-interacting non-linear Dirac equation. This class of
differential equations has been studied extensively in the past, see e.g. Ref.
[29, 30, 31, 32, 33, 34, 35, 36, 37, 38]. While the focus has mostly been on
locally bound solitons, we instead aim to find vortex solutions that recover
to one of the homogenous ground states outlined above in the far-field limit.
We employ the vortex ansatz

$\psi_{a(b)}(r,\theta)=\rho_{a(b)}(r)e^{i\ell_{a(b)}\theta}.$ (3)

The winding numbers $\ell_{a(b)}$ must be integers to ensure single-valued
wavefunctions, and dictate the behavior at the vortex core,
$\rho_{a(b)}(r)\propto r^{\ell_{a(b)}}\ (r\rightarrow 0)$.

It is convenient to rewrite the Dirac GPE in polar coordinates, which
decouples the angular and radial parts. The linear kinetic terms yield a
factor of $e^{\pm i\theta}$, from which the condition $\ell_{a}=\ell_{b}-1$
for the winding numbers follows immediately. Decoupling the angular part gives
the radial equations

$\displaystyle\Big{[}g_{a}\big{(}n_{a}-n_{a,\infty}\big{)}+g_{ab}n_{b}\Big{]}\rho_{a}$
$\displaystyle=iv\left(\partial_{r}+\frac{l_{b}}{r}\right)\rho_{b}$ (4a)
$\displaystyle\Big{[}g_{b}\big{(}n_{b}-n_{b,\infty}\big{)}+g_{ab}n_{a}\Big{]}\rho_{b}$
$\displaystyle=iv\left(\partial_{r}+\frac{1-l_{b}}{r}\right)\rho_{a},$ (4b)

where we have introduced the effective parameters
$n_{a(b),\infty}\vcentcolon=\frac{\mu-c_{0}\mp\Delta}{g_{a(b)}}$ that can be
though of as far-field densities of condensate components. The usefulness of
these parameters becomes obvious when calculating the far-field limits of the
condensates. Indeed,
$|\rho_{a(b)}|^{2}\xrightarrow{r\rightarrow\infty}n_{a(b),\infty}\ \text{or}\
0$ in the absence of inter-component interactions ($g_{ab}=0$). We remark that
changing the winding number $\ell_{b}\rightarrow 1-l_{b}$ effectively switches
the sublattices, hence it is sufficient to consider $\ell_{b}\geq 1$.
Furthermore, the case $\ell_{b}=1,\ell_{a}=0$ is special because only one
pseudo-spin has a non-zero phase winding. Our numerical methods are less
reliable in this topological sector, hence we focus on the
$\ell_{b}=2,\ell_{a}=1$ sector.

Identifying vortex solutions of (4) is achieved by a numerical shooting
algorithm [34]: From a Taylor expansion around the vortex core, it follows
that the leading Taylor coefficient of $\rho_{a}$ is a free parameter. A
vortex solution is obtained by tuning this initial condition such that
oscillations in the far field are suppressed. Details of the shooting
algorithm are outlined in Appendix A.

We automated this process by developing a bisection algorithm that minimizes
the number of oscillations of the integrated wavefunction. This allows us to
scan large parts of the phase space spanned by the model parameters. In
practice, we rescale the radial coordinate to $r\rightarrow\frac{\mu-
c_{0}-\Delta}{v}r$ and the density to
$\rho_{a,b}\rightarrow\frac{1}{\sqrt{n_{a,\infty}}}\rho_{a,b}$. This reduces
the number of independent model parameters to three, namely the relative
interaction strengths $\frac{g_{b}}{g_{a}}$ and $\frac{g_{ab}}{g_{a}}$, and
the effective Haldane gap
$\tilde{\Delta}=\frac{c_{0}-\mu-\Delta}{c_{0}-\mu+\Delta}$.

##  III Results

###  III.1 $\ell_{b}=2,\ell_{a}=1$ sector

In the absence of inter-component interactions, $g_{ab}=0$, we observe
vortices with finite far-field density for one component, and a ring-soliton
profile on the other component. In the totally symmetric case, population of
sublattice A is preferred. This is consistent with the lower kinetic energy,
which is proportional to the square of the phase winding number,
$E_{kin}\sim\ell_{a(b)}^{2}\ln\frac{L}{\xi}$ for $\rho_{b(a)}\rightarrow 0$.
Here, $\xi$ is the healing length of the vortex and $L$ is the system size.
The logarithmic divergence is an artifact from the presence of an unpaired
vortex; introducing an anti-vortex would lift the divergence. The density and
phase of such a configuration is shown in figure 1. The density plots show the
vortex profile on component A (upper left) and a ring-soliton on component B
(lower left), while the phase corresponds to winding numbers $\ell_{a}=1$
(upper right) and $\ell_{b}=2$ (lower right). We call this configuration an
A-vortex excitation.

The occupation of sublattice B can be enhanced by either opening a Haldane
gap, which lowers the chemical potential on sublattice B, or by decreasing the
intra-component repulsion on sublattice B, $\frac{g_{b}}{g_{a}}<1$. In both
cases, the increased kinetic energy is eventually compensated by the decreased
potential energy, such that sublattice B supports a vortex, while a ring-
soliton profiles is found on sublattice A. This phase is illustrated in figure
2. We call this configuration a B-vortex excitation.

The resulting phase diagram as a function of the effective parameters
$\frac{g_{b}}{g_{a}}$ and the effective Haldane gap $\tilde{\Delta}$ is shown
in the upper left panel of Fig(4, where the red color indicates an A-vortex,
and the green color indicates a B-vortex.

For sufficiently large inter-component interactions $g_{ab}$, we also observe
a phase with co-existing vortex profiles on both components, shown in figure
3. Since the phase winding governs the vortex core behavior, $\rho(r)\sim
r^{\ell}$, we find multiple core structures in this configuration. Introducing
a Haldane gap and lowering the interaction strength $g_{b}$ facilitates the
formation of a multiple core vortex. For dominant inter-component
interactions, we find that the multiple core state is realized across a wide
range of parameters.

We show these results in figure 4, where each panel shows a slice of the
three-dimensional phase space spanned by
$\frac{g_{b}}{g_{a}},\frac{g_{ab}}{g_{a}},\tilde{\Delta}$ at fixed
$\frac{g_{ab}}{g_{a}}$. Red color represents A-vortex states with winding
number $\ell_{a}=1$. Green color indicates the opposite B-vortex phase with
$\ell_{b}=2$. Blue color indicates a multiple core state with simultaneous
vortices on both components. The multiple core state first starts to appear at
approximately $g_{ab}\approx 0.7g_{a}$ for large Haldane gaps and
$g_{b}<g_{a}$ (upper middle panel), and starts to replace the B-vortex state
upon increasing $g_{ab}$, as indicated in the lower left panel. For dominant
$g_{ab}$ the multiple core state is favored in large parts of the phase space,
as shown in the lower right panel. These results represent the main findings
of this paper. The visual artifacts in the phase diagram plots stem from the
increased core size close to the phase boundaries, which leads to longer
computation times and less reliable numerical detection of vortex states.

Figure 1: Normalized condensate density (left panels) and phase (right panels)
of the A-vortex for
$\ell_{a}=1,\ell_{b}=2,\frac{g_{b}}{g_{a}}=1,\frac{g_{ab}}{g_{a}}=0,\tilde{\Delta}=1$.
Upper (lower) panels show density and phase for sublattice A(B). Figure 2:
Normalized condensate density (left panels) and phase (right panels) of the
B-vortex for
$\ell_{a}=1,\ell_{b}=2,\frac{g_{b}}{g_{a}}=1,\frac{g_{ab}}{g_{a}}=0,\tilde{\Delta}=0.8$.
Upper (lower) panels show density and phase for sublattice A(B). Figure 3:
Normalized condensate density (left panels) and phase (right panels) of the
multiple core vortex for
$\ell_{a}=1,\ell_{b}=2,\frac{g_{b}}{g_{a}}=1,\frac{g_{ab}}{g_{a}}=1.1,\tilde{\Delta}=1$.
Upper (lower) panels show density and phase for sublattice A(B). Figure 4:
Phase diagram of vortex excitations for several values of
$\frac{g_{ab}}{g_{a}}$. Red color indicates A-vortixes with winding number
$l_{a}=1$, blue color indicates B-vortices with winding number $l_{b}=2$, and
green color indicates a mixed phase with finite support on both components.

###  III.2 $\ell_{b}=1,\ell_{a}=0$ sector

Our main results generally hold for the topological sector
$\ell_{b}=1,\ell_{a}=0$ with slight modifications. We again identify three
classes of solutions characterized by the far-field behaviors. Since
sublattice A has no phase winding, the A-dominant phase is a homogeneous
condensate on sublattice A, while sublattice B is unoccupied. The B-dominant
phase typically shows a soliton-like switch between the sublattice, as shown
in figure 5. In addition, we again observe co-existing vortices on both
sublattices for large enough $\frac{g_{ab}}{g_{a}}$.

Generally, we observe that the core size is larger compared to the
$\ell_{b}=2,\ell_{a}=1$ sector, and therefore makes the numerical detection of
vortex states more expensive and numerically unstable. We therefore omit the
computation of the corresponding phase diagram.

Figure 5: Normalized condensate density (left panels) and phase (right panels)
of the B-vortex for $\ell_{a}=0,\ell_{b}=1$. Upper (lower) panels show density
and phase for sublattice A(B).

##  IV Conclusion

There have been numerous proposals to realize real and artificial materials
hosting Bose excitations with topological nodal points, commonly known as
bosonic Dirac and Weyl materials [29, 30, 31, 32, 33, 34, 35, 27, 12].
Combining this class of materials with non-equilibrium Bose-Einstein
condensation gives access to the study of Dirac BEC, which are natural
examples of multi-band condensates and feature a linear dispersion relation
[27]. We present vortex solutions in BEC of bosons with Dirac dispersion,
Dirac BEC. Given the topological nature of the Dirac node, the phase winding
of these condensates differ by one $|\ell_{a}-\ell_{b}|=1$ [29]. Hence the
kinetic and potential energies of two components is different, resulting in a
different core structure. We find that the far field behaviors for vortices
develop different occupancies for pseudospin species (sublattices A and B). We
present the detailed phase diagram for the the vortex states in Dirac BEC
depending on the intra- and inter-component interaction strengths. We consider
both the case of pure Dirac nodal points and the Dirac spectrum with a Haldane
gap. The Haldane gap tends to favor the occupation of pseudo-spin B over A.

A successful experimental observation of the Dirac BEC and vortices would
represent an important step in the development of multi-band topological
condensates. The observation of vortices would depend on the physical system.
For the specific realizations of the Dirac BEC we use the example of Dirac BEC
in pumped Dirac magnons on Cr based trihalides. One would therefore expect a
nontrivial features in magnon population and might use, e.g. the Brilloiun
light scattering to observe Dirac BEC vortices.

## Acknowledgements

We are grateful to G. Aeppli, J. Bailey, S. Banerjee and P. Suckachov for
useful discussions. This work was supported by the European Research Council
under the European Union’s Seventh Framework Program Synergy HERO-81451, the
Knut and Alice Wallenberg Foundation KAW 2018-0104, KAW 2019.0068 and by the
University of Connecticut.

##  V Appendix: Numerical methods

Here we outline the numerical methods used to obtain our results. First, we
discuss the numerical shooting algorithm used to find vortex solutions of the
radial GPE (4). Second, we discuss the bisection algorithm used to
automatically scan the phase space for vortex solutions. Finally we outline
the classification algorithm used to establish the phase diagram.

###  V.1 Shooting algortihm

Using a global phase rotation allows us to tune $\rho_{a}(r)$ to the real
axis. For $l_{b}\geq 2$, it then follows that $\rho_{b}$ is purely imaginary.
Therefore, (4) becomes a system of two coupled, non-linear differential
equations, which may be expressed by the vector
$\vec{u}=\begin{pmatrix}R_{a}&I_{b}\end{pmatrix}^{T}$:

$\vec{u}^{\prime}(r)=\begin{pmatrix}\Big{[}\tilde{g}_{b}\big{(}u_{2}^{2}-n_{b,\infty}\big{)}+\tilde{g}_{ab}u_{1}^{2}\Big{]}u_{2}-\frac{1-l_{b}}{r}u_{1}\\\
-\Big{[}\tilde{g}_{a}\big{(}u_{1}^{2}-n_{a,\infty}\big{)}+\tilde{g}_{ab}u_{2}^{2}\Big{]}u_{1}-\frac{l_{b}}{r}u_{2}\end{pmatrix}.$
(5)

Here, the coupling terms have been divided by the magnon velocity,
$\tilde{g}_{j}=\frac{g_{j}}{v}$. Once the initial conditions are fixed, (5)
can be integrated easily using forward integration.

The initial conditions at $r=0$ are obtained from a Taylor expansion for $r\ll
1$: Let $u_{1}(r)=\sum_{j\geq 0}a_{j}r^{j}$ and $u_{2}(r)=\sum_{j\geq
0}b_{j}r^{j}$. One then finds recursive relations for the coefficients,

$\displaystyle a_{j+1}(j+2-l)$
$\displaystyle=\tilde{g}_{b}\bigg{(}\sum_{l_{1}+l_{2}+l_{3}=j}b_{l_{1}}b_{l_{2}}b_{l_{3}}-n_{b,\infty}b_{j}\bigg{)}$
$\displaystyle+\tilde{g}_{ab}\sum_{l_{1}+l_{2}+l_{3}=j}a_{l_{1}}a_{l_{2}}b_{l_{3}},$
(6a) $\displaystyle b_{j+1}(j+1+l)$
$\displaystyle=-\tilde{g}_{a}\bigg{(}\sum_{l_{1}+l_{2}+l_{3}=j}a_{l_{1}}a_{l_{2}}a_{l_{3}}-n_{a,\infty}a_{j}\bigg{)}$
$\displaystyle-\tilde{g}_{ab}\sum_{l_{1}+l_{2}+l_{3}=j}a_{l_{1}}b_{l_{2}}b_{l_{3}}.$
(6b)

In addition, we find the conditions $a_{0}=0$ unless $l_{b}=1$ and $b_{0}=0$
unless $l_{b}=0$. It can be seen that the first non-zero coefficients are
$a_{l_{b}-1}$ and $b_{l_{b}}$, hence $a_{l_{b}-1}$ is the only free parameter
of the system. Indeed, all other coefficients follow from the recursion
relations.

A vortex solution can then be found by evaluating the behavior at large $r$:
By requiring that the derivatives vanish in the far-field limit, we obtain
either $u_{1}\rightarrow 0$ or
$u_{1}\rightarrow\sqrt{n_{a,\infty}-\frac{g_{ab}}{g_{a}}u_{2}^{2}}$ resp.
$u_{2}\rightarrow\sqrt{n_{b,\infty}-\frac{g_{ab}}{g_{b}}u_{1}^{2}}$. It
follows that a vortex solution is found by tuning the free parameter $a_{l-1}$
such that $u_{1,2}$ don’t oscillate for large $r$. In practice, the
integration range is bounded and there is a finite precision of the
integration. Therefore, the onset of oscillatory behavior is the key indicator
for a vortex solution: oscillations are pushed away further from the vortex
core the closer the initial value is to $a_{l_{b}-1}^{vortex}$. Also, the
forward integration must start at a small positive value $r_{0}\ll 1$ in order
to avoid the singularity at $r=0$. We observe a negligible dependence of the
initial values $a_{l_{b}-1}^{vortex}$ on $r_{0}$, which we interpret as a
signature of the numerical stability of our approach.

###  V.2 Bisection algorithm

To automate the numerical shooting, we use a bisection algorithm to search for
the minimum number of oscillations of the integrated radial functions. Over-
and undershooting behaviour can be distinguished by determining whether the
integrated functions oscillate around the expected far-field limit or zero,
respectively. An example of this behavior is shown in figure 6. It is clearly
visible that overshooting (left panel) leads to oscillations around the far-
field limits of each component, while undershooting (right panel) leads to a
damped oscillation.

Figure 6: Convergence of the $\ell_{a}=1,\ell_{b}=2$ vortex solution. Left
panel: Overshooting behaviour for $a_{1}>a_{1}^{vortex}$. Right panel:
Undershooting behaviour for $a_{1}<a_{1}^{vortex}$. The vortex solution
obtained from the bisection algorithm is indicated by dashed lines.

We remark that our algorithm has a number of limitations: First, the core size
can become very large close to a phase boundary. We compensate for this by
allowing an adaptive integration range, which is accompanied by a loss of
numerical stability of the integration and higher computational cost. We
therefore use a cutoff for the maximal integration range. Also, the core
structure can contain extrema itself, which are hard to distinguish from
oscillations in the recovered regime. Such behavior is typically also observed
in the vicinity of a phase boundary. Second, the differential equation is
usually very sensitive to the initial condition $a_{l-1}$ in the sense that
small changes in $a_{l-1}$ drastically modify the far-field behavior. The
bisection algorithm relies on this sensitivity to find the vortex solution.
However, we observe that the sensitivity on $a_{l-1}$ is significantly reduced
if both $\frac{g_{b}}{g_{ab}}$ and $\Delta_{eff}$ are large. Therefore the
bisection algorithm is slowly convergent in this part of the phase space.

###  V.3 Classification algorithm

We employ a fuzzy clustering algorithm [39] on the integrated radial profiles
to establish the phase diagram. The fuzzy clustering algorithm is similar to
k-means clustering, but allows for partial membership of a data point to each
cluster, given by the membership matrix $W$. This is an advantage for the
problem at hand, since the integrated wavefunctions can be ambiguous in the
proximity of a phase boundary.

The algorithm minimizes the objective function

$f(c)=\sum_{i=1}^{n}\sum_{j=1}^{n_{c}}W_{ij}^{m}\norm{x_{i}-c_{j}}^{2},$

for the data set ${x_{1},\dots,x_{n}}$, where $n_{c}$ is the number of
clusters, $c$ is the array of centroids, and $m>1$ is the fuzzyness parameter.
The centroids are determined by the "fuzzy" mean of the data set:

$c_{j}=\frac{\sum_{i=1}^{n}W_{ij}^{m}x_{i}}{\sum_{i=1}^{n}W_{ij}^{m}}.$

This is achieved in the following way: First, randomly assign values to the
membership matrix and compute the centroids. For each iteration step, the
membership matrix is updated according to

$W_{ij}=\Bigg{[}\sum_{k=1}^{n_{c}}\bigg{(}\frac{\norm{x_{i}-c_{j}}^{2}}{\norm{x_{i}-c_{k}}^{2}}\bigg{)}^{\frac{2}{m-1}}\Bigg{]}^{-1}.$

Then update the centroids and repeat until convergence of the centroids is
reached. The fuzzyness parameter $m$ governs how strict the membership of a
data point to a single cluster will be; a larger value results in more
fuzzyness.

For our case, we first identify the longest slowly-varying section of the
integration range. This is necessary to exclude the vortex core for the
analysis of the far-field behavior, and also the onset of oscillations at
large $r$ present due to the numerical instability and finite accuracy of the
initial condition $a_{l_{b}-1}$. We then interpolate the slowly-varying
section to ensure the same dimensionality for each data point. This allows us
to compute the Euclidian distance norm between any two traces, which is the
basis for the clustering algorithm.

## References

  * [1] T.O. Wehling, A.M. Black-Schaffer, and A.V. Balatsky.  Dirac materials.  Advances in Physics, 63(1):1–76, 2014.
  * [2] Ling Lu, Zhiyu Wang, Dexin Ye, Lixin Ran, Liang Fu, John D. Joannopoulos, and Marin Soljačić.  Experimental observation of weyl points.  Science, 349(6248):622–624, 2015.
  * [3] HaiXiao Wang, Lin Xu, HuanYang Chen, and Jian-Hua Jiang.  Three-dimensional photonic dirac points stabilized by point group symmetry.  Phys. Rev. B, 93:235155, Jun 2016.
  * [4] Yihao Yang, Zhen Gao, Haoran Xue, Li Zhang, Mengjia He, Zhaoju Yang, Ranjan Singh, Yidong Chong, Baile Zhang, and Hongsheng Chen.  Realization of a three-dimensional photonic topological insulator.  Nature, 565(7741):622–626, Jan 2019.
  * [5] N Y Kim, K Kusudo, A Löffler, S Höfling, A Forchel, and Y Yamamoto.  Exciton–polariton condensates near the dirac point in a triangular lattice.  15(3):035032, mar 2013.
  * [6] T. Jacqmin, I. Carusotto, I. Sagnes, M. Abbarchi, D. D. Solnyshkov, G. Malpuech, E. Galopin, A. Lemaître, J. Bloch, and A. Amo.  Direct observation of dirac cones and a flatband in a honeycomb lattice for polaritons.  Phys. Rev. Lett., 112:116402, Mar 2014.
  * [7] E. J. Samuelsen, Richard Silberglitt, G. Shirane, and J. P. Remeika.  Spin waves in ferromagnetic cr${\mathrm{br}}_{3}$ studied by inelastic neutron scattering.  Phys. Rev. B, 3:157–166, Jan 1971.
  * [8] W. B. Yelon and Richard Silberglitt.  Renormalization of large-wave-vector magnons in ferromagnetic cr${\mathrm{br}}_{3}$ studied by inelastic neutron scattering: Spin-wave correlation effects.  Phys. Rev. B, 4:2280–2286, Oct 1971.
  * [9] J. Fransson, A. M. Black-Schaffer, and A. V. Balatsky.  Magnon dirac materials.  Phys. Rev. B, 94:075401, Aug 2016.
  * [10] Sergey S. Pershoguba, Saikat Banerjee, J. C. Lashley, Jihwey Park, Hans Ågren, Gabriel Aeppli, and Alexander V. Balatsky.  Dirac magnons in honeycomb ferromagnets.  Phys. Rev. X, 8:011010, Jan 2018.
  * [11] Lebing Chen, Jae-Ho Chung, Bin Gao, Tong Chen, Matthew B. Stone, Alexander I. Kolesnikov, Qingzhen Huang, and Pengcheng Dai.  Topological spin excitations in honeycomb ferromagnet ${\mathrm{cri}}_{3}$.  Phys. Rev. X, 8:041028, Nov 2018.
  * [12] Changsong Xu, Junsheng Feng, Hongjun Xiang, and Laurent Bellaiche.  Interplay between kitaev interaction and single ion anisotropy in ferromagnetic cri3 and crgete3 monolayers.  npj Computational Materials, 4(1):57, Nov 2018.
  * [13] P. A. McClarty, X.-Y. Dong, M. Gohlke, J. G. Rau, F. Pollmann, R. Moessner, and K. Penc.  Topological magnons in kitaev magnets at high fields.  Phys. Rev. B, 98:060404, Aug 2018.
  * [14] So Demokritov, V Demidov, Oleksandr Dzyapko, G. Melkov, Alexander Serga, Burkard Hillebrands, and Andrei Slavin.  Bose-einstein condensation of quasi-equilibrium magnons at room temperature under pumping.  Nature, 443:430–3, 10 2006.
  * [15] V. E. Demidov, O. Dzyapko, S. O. Demokritov, G. A. Melkov, and A. N. Slavin.  Thermalization of a parametrically driven magnon gas leading to bose-einstein condensation.  Phys. Rev. Lett., 99:037205, Jul 2007.
  * [16] V. E. Demidov, O. Dzyapko, S. O. Demokritov, G. A. Melkov, and A. N. Slavin.  Observation of spontaneous coherence in bose-einstein condensate of magnons.  Phys. Rev. Lett., 100:047205, Jan 2008.
  * [17] Alexander A. Serga, Vasil S. Tiberkevich, Christian W. Sandweg, Vitaliy I. Vasyuchka, Dmytro A. Bozhko, Andrii V. Chumak, Timo Neumann, Björn Obry, Gennadii A. Melkov, Andrei N. Slavin, and Burkard Hillebrands.  Bose–einstein condensation in an ultra-hot gas of pumped magnons.  Nature Communications, 5(1):3452, Mar 2014.
  * [18] P. Nowik-Boltyk, O. Dzyapko, V. E. Demidov, N. G. Berloff, and S. O. Demokritov.  Spatially non-uniform ground state and quantized vortices in a two-component bose-einstein condensate of magnons.  Scientific Reports, 2(1):482, Jun 2012.
  * [19] Dmytro A. Bozhko, Alexander A. Serga, Peter Clausen, Vitaliy I. Vasyuchka, Frank Heussner, Gennadii A. Melkov, Anna Pomyalov, Victor S. L’vov, and Burkard Hillebrands.  Supercurrent in a room-temperature bose–einstein magnon condensate.  Nature Physics, 12(11):1057–1062, Nov 2016.
  * [20] Dmytro A. Bozhko, Alexander J. E. Kreil, Halyna Yu. Musiienko-Shmarova, Alexander A. Serga, Anna Pomyalov, Victor S. L’vov, and Burkard Hillebrands.  Bogoliubov waves and distant transport of magnon condensate at room temperature.  Nature Communications, 10(1):2460, Jun 2019.
  * [21] I. V. Borisenko, B. Divinskiy, V. E. Demidov, G. Li, T. Nattermann, V. L. Pokrovsky, and S. O. Demokritov.  Direct evidence of spatial stability of bose-einstein condensate of magnons.  Nature Communications, 11(1):1691, Apr 2020.
  * [22] J. P. Eisenstein and A. H. MacDonald.  Bose–einstein condensation of excitons in bilayer electron systems.  Nature, 432(7018):691–694, Dec 2004.
  * [23] J. Kasprzak, M. Richard, S. Kundermann, A. Baas, P. Jeambrun, J. M. J. Keeling, F. M. Marchetti, M. H. Szymańska, R. André, J. L. Staehli, V. Savona, P. B. Littlewood, B. Deveaud, and Le Si Dang.  Bose–einstein condensation of exciton polaritons.  Nature, 443(7110):409–414, Sep 2006.
  * [24] R. Balili, V. Hartwell, D. Snoke, L. Pfeiffer, and K. West.  Bose-einstein condensation of microcavity polaritons in a trap.  Science, 316(5827):1007–1010, 2007.
  * [25] Hui Deng, Hartmut Haug, and Yoshihisa Yamamoto.  Exciton-polariton bose-einstein condensation.  Rev. Mod. Phys., 82:1489–1537, May 2010.
  * [26] Joe Bailey, Pavlo Sukhachov, Korbinian Baumgaertl, Simone Finizio, Sebastian Wintz, Carsten Dubs, Joerg Raabe, Dirk Grundler, Alexander Balatsky, and Gabriel Aeppli.  Multi-band bose-einstein condensate at four-particle scattering resonance, 2022.
  * [27] P. O. Sukhachov, S. Banerjee, and A. V. Balatsky.  Bose-einstein condensate of dirac magnons: Pumping and collective modes.  Phys. Rev. Research, 3:013002, Jan 2021.
  * [28] I. Kourakis, P. K. Shukla, M. Marklund, and L. Stenflo.  Modulational instability criteria for two-componentbose–einstein condensates.  The European Physical Journal B - Condensed Matter and Complex Systems, 46(3):381–384, Aug 2005.
  * [29] L. H. Haddad and L. D. Carr.  Relativistic linear stability equations for the nonlinear dirac equation in bose-einstein condensates.  EPL (Europhysics Letters), 94(5):56002, may 2011.
  * [30] L.H. Haddad and L.D. Carr.  The nonlinear dirac equation in bose–einstein condensates: Foundation and symmetries.  Physica D: Nonlinear Phenomena, 238(15):1413 – 1421, 2009.  Nonlinear Phenomena in Degenerate Quantum Gases.
  * [31] L H Haddad, C M Weaver, and Lincoln D Carr.  The nonlinear dirac equation in bose–einstein condensates: I. relativistic solitons in armchair nanoribbon optical lattices.  New Journal of Physics, 17(6):063033, jun 2015.
  * [32] L H Haddad and Lincoln D Carr.  The nonlinear dirac equation in bose–einstein condensates: II. relativistic soliton stability analysis.  New Journal of Physics, 17(6):063034, jun 2015.
  * [33] L H Haddad and Lincoln D Carr.  The nonlinear dirac equation in bose–einstein condensates: superfluid fluctuations and emergent theories from relativistic linear stability equations.  New Journal of Physics, 17(9):093037, sep 2015.
  * [34] L H Haddad and Lincoln D Carr.  The nonlinear dirac equation in bose–einstein condensates: vortex solutions and spectra in a weak harmonic trap.  New Journal of Physics, 17(11):113011, oct 2015.
  * [35] L. H. Haddad, K. M. O’Hara, and Lincoln D. Carr.  Nonlinear dirac equation in bose-einstein condensates: Preparation and stability of relativistic vortices.  Phys. Rev. A, 91:043609, Apr 2015.
  * [36] Alexander N. Poddubny and Daria A. Smirnova.  Ring dirac solitons in nonlinear topological systems.  Phys. Rev. A, 98:013827, Jul 2018.
  * [37] Jesús Cuevas-Maraver, Panayotis G. Kevrekidis, Avadh Saxena, Andrew Comech, and Ruomeng Lan.  Stability of solitary waves and vortices in a 2d nonlinear dirac model.  Phys. Rev. Lett., 116:214101, May 2016.
  * [38] Nabile Boussaïd and Andrew Comech.  On spectral stability of the nonlinear dirac equation.  Journal of Functional Analysis, 271(6):1462–1524, 2016.
  * [39] J. C. Dunn.  A fuzzy relative of the isodata process and its use in detecting compact well-separated clusters.  Journal of Cybernetics, 3(3):32–57, 1973.


We present next some admissible equivalences of interest. First a result on
commutation between linear contexts and explicit operators:

*  Let $t \in \Term{\calcLambdaM}$.
Then, $\fcan{\ctxtapply{\ctxt{L}}{\ctxtapply{\ctxt{LTT}}{t}}} \eqsigma
\fcan{\ctxtapply{\ctxt{LTT}}{\ctxtapply{\ctxt{L}}{t}}}$ if $\bv{\ctxt{L}}
\notin \ctxt{LTT}$ and $\fc{\ctxt{L}}{\ctxt{LTT}}$.

*  Let $c \in
\Command{\calcLambdaM}$. Then,
$\fcan{\ctxtapply{\ctxt{R}}{\ctxtapply{\ctxt{LCC}}{c}}} \eqsigma
\fcan{\ctxtapply{\ctxt{LCC}}{\ctxtapply{\ctxt{R}}{c}}}$ if $\bn{\ctxt{R}}
\notin \ctxt{LCC}$ and $\fc{\ctxt{R}}{\ctxt{LCC}}$.

Each case is proved by induction on $\ctxt{L}$ or $\ctxt{R}$ respectively, using some
auxiliary results. Details in the Appendix <ref>.

A direct consequence of this result is that rules from
Fig. <ref> that were replaced
as stated before are indeed admissible:

* $\termsubs{x}{u}{(\termabs{y}{t})} \eqsigma
\termabs{y}{\termsubs{x}{u}{t}}$ with $y \notin u$, $\ctxt{L} =
\termsubs{x}{u}{\Box}$ and $\ctxt{LTT} = \termabs{y}{\Box}$.

* $\termsubs{x}{u}{(\termapp{t}{v})} \eqsigma
\termapp{\termsubs{x}{u}{t}}{v}$ with $x \notin v$, $\ctxt{L} =
\termsubs{x}{u}{\Box}$ and $\ctxt{LTT} = \termapp{\Box}{v}$.

* $\termsubs{x}{u}{(\termcont{\beta}{\termname{\alpha}{t}})} \eqsigma
\termcont{\beta}{\termname{\alpha}{\termsubs{x}{u}{t}}}$ with $\alpha \notin
u$, $\ctxt{L} = \termsubs{x}{u}{\Box}$ and $\ctxt{LTT} =
\termcont{\beta}{\termname{\alpha}{\Box}}$.

* $\termsubs{x}{u}{\termsubs{y}{v}{t}} \eqsigma
\termsubs{y}{v}{\termsubs{x}{u}{t}}$ with $y \notin u$, $x \notin v$,
$\ctxt{L} = \termsubs{x}{u}{\Box}$ and $\ctxt{LTT} = \termsubs{y}{v}{\Box}$.

* $\termname{\alpha'}{\termcont{\alpha''}{\termrepl[\alpha'']{\alpha}{u}{(\termname{\beta'}{\termcont{\beta''}{\termrepl[\beta'']{\beta}{v}{c}}})}}}
\eqsigma
\termname{\beta'}{\termcont{\beta''}{\termrepl[\beta'']{\beta}{v}{(\termname{\alpha'}{\termcont{\alpha''}{\termrepl[\alpha'']{\alpha}{u}{c}}})}}}$
with $\alpha \notin v, \alpha'' \notin v, \beta \notin u, \beta'' \notin u,
\beta'' \neq \alpha', \alpha'' \neq \beta'$. This case is particularly
interesting since rule $\ruleEqsigRho$ plays a key role in it. It is by
applying $\ruleEqsigRho$ on both sides of the equality that it is enough to
\[
\termren{\alpha''}{\alpha'}{\termrepl[\alpha'']{\alpha}{u}{(\termren{\beta''}{\beta'}{\termrepl[\beta'']{\beta}{v}{c}})}}
\eqsigma
\termren{\beta''}{\beta'}{\termrepl[\beta'']{\beta}{v}{(\termren{\alpha''}{\alpha'}{\termrepl[\alpha'']{\alpha}{u}{c}})}}
\]
which in turn follows from Lem. <ref>
(<ref>) taking $\ctxt{R} =
\termren{\alpha''}{\alpha'}{\termrepl[\alpha'']{\alpha}{u}{\boxdot}}$ and
$\ctxt{LCC} =
\termren{\beta''}{\beta'}{\termrepl[\beta'']{\beta}{v}{\boxdot}}$.

* $\termname{\alpha'}{\termcont{\alpha''}{\termrepl[\alpha'']{\alpha}{u}{(\termname{\beta'}{\termabs{y}{\termcont{\beta}{c}}})}}}
\eqsigma
\termname{\beta'}{\termabs{y}{\termcont{\beta}{\termname{\alpha'}{\termcont{\alpha''}{\termrepl[\alpha'']{\alpha}{u}{c}}}}}}$
with $y \notin u, \beta \notin u, \beta'' \notin u, \beta'' \neq \alpha',
\alpha'' \neq \beta'$. As in the previous case, by $\ruleEqsigRho$ it is
enough to show
\[
\termren{\alpha''}{\alpha'}{\termrepl[\alpha'']{\alpha}{u}{(\termname{\beta'}{\termabs{y}{\termcont{\beta}{c}}})}}
\eqsigma
\termname{\beta'}{\termabs{y}{\termcont{\beta}{\termren{\alpha''}{\alpha'}{\termrepl[\alpha'']{\alpha}{u}{c}}}}}
\]
and we conclude by Lem. <ref>
(<ref>) taking $\ctxt{R} =
\termren{\alpha''}{\alpha'}{\termrepl[\alpha'']{\alpha}{u}{\boxdot}}$ and
$\ctxt{LCC} =
\termname{\beta'}{\termabs{y}{\termcont{\beta}{\boxdot}}}$.

As a further result, we show that $\eqsigma$ preserves the type of
$\calcLambdaM$-objects in the same way that $\eqlaurent$ does so for objects of
the $\calcLambdaMu$-calculus (Lem. <ref>).

Let $o \in \Object{\calcLambdaM}$. If
$\deriv[\pi]{\sequM{\Gamma}{\assign{o}{T}}{\Delta}}[\SysMuEx]$ and  $o \eqsigma
o'$, then there exists

The proof is by induction on  $o \eqsigma o'$
and is straightforward. It uses Lem. <ref>.

Strong Bisimulation Result

Let $u,s,o \in \Object{\calcLambdaM}$ in $\rcan$-normal form such that $o
\eqsigma o'$, $u \eqsigma u'$ and  $s \eqsigma s'$, where $u,u'$ are terms and
$s,s'$ are stacks. Then,

$\fcan{\subsapply{\subs{x}{u}}{o}} \eqsigma
\fcan{\subsapply{\subs{x}{u}}{o'}}$ and  $\fcan{\subsapply{\subs{x}{u}}{o}}
\eqsigma \fcan{\subsapply{\subs{x}{u'}}{o}}$.

$\fcan{\replapply{\repl[\alpha']{\alpha}{s}}{o}} \eqsigma
\fcan{\replapply{\repl[\alpha']{\alpha}{s}}{o'}}$ and
$\fcan{\replapply{\repl[\alpha']{\alpha}{s}}{o}} \eqsigma
\fcan{\replapply{\repl[\alpha']{\alpha}{s'}}{o}}$.

We are now able to state the promised result, namely, the fact that $\eqsigma$
is a strong bisimulation with respect to the meaningful computation relation.

Let $o \in \Object{\calcLambdaM}$. If $o \eqsigma p$ and $o \reducemean o'$,
then there exists $p'$ such that  $p \reducemean p'$  and  $o' \eqsigma p'$.

The proof is by induction on  $o \eqsigma p$ and uses
Lem. <ref>,
Lem. <ref> and
Lem. <ref>. All the details are in the
Appendix <ref>.

We illustrate the previous theorem with the following example. Let $o =
\termrepl[\alpha']{\alpha}{u}{o_0} \ruleEqsigPopPop
\termrepl[\alpha']{\alpha}{u}{p_0} = p$, where $o_0 =
\termname{\alpha}{\termabs{x}{\termcont{\gamma}{\termname{\alpha}{\termabs{y}{\termcont{\delta}{c}}}}}}
\ruleEqsigPopPop
\termname{\alpha}{\termabs{y}{\termcont{\delta}{\termname{\alpha}{\termabs{x}{\termcont{\gamma}{c}}}}}}
= p_0$. Notice in particular that  $o_0$, $o$, $p_0$ and $p$ are all
forms. We have
\[
\begin{tikzcd}[->,ampersand replacement=\&]
o = \termrepl[\alpha']{\alpha}{u}{(\termname{\alpha}{\termabs{x}{\termcont{\gamma}{\termname{\alpha}{\termabs{y}{\termcont{\delta}{c}}}}}})} \arrow[->]{d}[left]{\rRm}
\&[-25pt] \eqsigma
\&[-25pt] \termrepl[\alpha']{\alpha}{u}{(\termname{\alpha}{\termabs{y}{\termcont{\delta}{\termname{\alpha}{\termabs{x}{\termcont{\gamma}{c}}}}}})} = p \arrow[->]{d}[left]{\rRm} \\
\termname{\alpha'}{\termapp{(\termabs{x}{\termcont{\gamma}{\termname{\alpha'}{\termapp{(\termabs{y}{\termcont{\delta}{c'}})}{u}}}})}{u}} \arrow[->>]{d}[left]{\rcan}
\&[-25pt]
\&[-25pt] \termname{\alpha'}{\termapp{(\termabs{y}{\termcont{\delta}{\termname{\alpha'}{\termapp{(\termabs{x}{\termcont{\gamma}{c'}})}{u}}}})}{u}} \arrow[->>]{d}[left]{\rcan} \\
o' = \termname{\alpha'}{\termsubs{x}{u}{(\termcont{\gamma}{\termname{\alpha'}{\termsubs{y}{u}{(\termcont{\delta}{c''})}}})}}
\&[-25pt] \eqsigma
\&[-25pt] \termname{\alpha'}{\termsubs{y}{u}{(\termcont{\delta}{\termname{\alpha'}{\termsubs{x}{u}{(\termcont{\gamma}{c''})}}})}} = p'
\end{tikzcd}
\]

so that $o \reducemean o'$  and $p \reducemean p'$.
We conclude $o' \eqsigma p'$ as follows:

\[ \begin{array}{ll}
\termname{\alpha'}{\termsubs{x}{u}{(\termcont{\gamma}{\termname{\alpha'}{\termsubs{y}{u}{(\termcont{\delta}{c''})}}})}} & \ruleEqsigExSubs \\
\termname{\alpha'}{\termcont{\gamma}{\termname{\alpha'}{\termcont{\delta}{\termsubs{x}{u}{\termsubs{y}{u}{c''}}}}}}     & \ruleEqsigRho \\
\termren{\gamma}{\alpha'}{\termren{\delta}{\alpha'}{\termsubs{x}{u}{\termsubs{y}{u}{c''}}}}                             & \ruleEqsigExRen \\
\termren{\delta}{\alpha'}{\termren{\gamma}{\alpha'}{\termsubs{x}{u}{\termsubs{y}{u}{c''}}}}                             & \ruleEqsigRho \\
\termname{\alpha'}{\termcont{\delta}{\termname{\alpha'}{\termcont{\gamma}{\termsubs{x}{u}{\termsubs{y}{u}{c''}}}}}}     & \ruleEqsigExSubs \\
\termname{\alpha'}{\termsubs{y}{u}{(\termcont{\delta}{\termname{\alpha'}{\termsubs{x}{u}{(\termcont{\gamma}{c''})}}})}}
\end{array} \]

Note the use of $\ruleEqsigRho$ to swap the occurrences of
$\termname{\alpha'}{\termcont{\gamma}{\ldots}}$ and

§ THE STRONG BISIMULATION RESULT

As explained in the introduction, $\eqlaurent$-equivalence is not a
strong bisimulation with respect to the reduction notion of the
$\calcLambdaMu$-calculus. We thus set out to devise a new term calculus in
which reshuffling can be formulated as a strong bisimulation without
changing the PPN semantics. The relation we obtain, $\eqsigma$, is indeed a
strong bisimulation over canonical forms with respect to our notion of
meaningful computation, $\eqsigma$-equivalent canonical terms have exactly
the same meaningful redexes. This is the result we present in this section.

Our result relies crucially on the decomposition of the replacement reduction
$\rrule{\rR}$ into linear and non-linear replacements (Sec. <ref>), the former having no computational content
(structurally equivalent PPN modulo multiplicative cuts), and thus
corresponding to the equivalence relation $\eqsigma$, while the latter
corresponding to exponential cut elimination steps, and thus contributing to
the meaningful computation.

Before stating the bisimulation result, we mention some technical lemmas that
will be needed for its proof:

Let $o \in \Object{\calcLambdaM}$. If $o \eqsigma o'$, then for all context
$\ctxt{O}$ of appropriate sort, $\fcan{\ctxtapply{\ctxt{O}}{o}} \eqsigma
\fcan{\ctxtapply{\ctxt{O}}{o'}}$.

Let $u,s,o \in \Object{\calcLambdaM}$ in $\rcan$-normal form such that $o
\eqsigma o'$, $u \eqsigma u'$ and  $s \eqsigma s'$, where $u,u'$ are terms and
$s,s'$ are stacks. Then,

$\fcan{\subsapply{\subs{x}{u}}{o}} \eqsigma
\fcan{\subsapply{\subs{x}{u}}{o'}}$ and  $\fcan{\subsapply{\subs{x}{u}}{o}}
\eqsigma \fcan{\subsapply{\subs{x}{u'}}{o}}$.

$\fcan{\replapply{\repl[\alpha']{\alpha}{s}}{o}} \eqsigma
\fcan{\replapply{\repl[\alpha']{\alpha}{s}}{o'}}$ and
$\fcan{\replapply{\repl[\alpha']{\alpha}{s}}{o}} \eqsigma
\fcan{\replapply{\repl[\alpha']{\alpha}{s'}}{o}}$.

We are now able to state the promised result, namely, the fact that $\eqsigma$
is a strong bisimulation with respect to the meaningful computation relation.

Let $o \in \Object{\calcLambdaM}$. If $o \eqsigma p$ and $o \reducemean o'$,
then there exists $p'$ such that  $p \reducemean p'$ and  $o' \eqsigma p'$.

The proof is by induction on  $o \eqsigma p$ and uses
Lem. <ref>,
Lem. <ref> and
Lem. <ref>. All the details are in the
Appendix <ref>.

§ TWO CORRESPONDENCE RESULTS

In this section we study how structural equivalence over  forms
$\eqsigma$ (Def. <ref>) correlates with
Laurent's $\eqlaurent$  (Def. <ref>) and with structural
equivalence $\eqppn$ for polarised proof-nets
(Def. <ref>). As the reader may recall,
Laurent's $\eqlaurent$ is defined over $\calcLambdaMu$ whereas our $\eqsigma$
is defined over $\calcLambdaM$. Moreover, our $\eqsigma$ relates $\calcLambdaM$
terms in  form. The naive attempt at correlating them by simply
taking the  form would be stated as follows, where $o, p \in
\Object{\calcLambdaMu}$:

\[
o \eqlaurent p \quad\text{iff}\quad \fcan{o} \eqsigma \fcan{p}
\]

However, this does not work. The reason is that in obtaining
$\eqsigma$ we dropped the equation:

\[
\begin{array}{rcl@{\quad}l}
\termname{\beta}{\termcont{\alpha}{c}}  & \ruleEqlauRho & \renapply{\ren{\alpha}{\beta}}{c}
\end{array}
\]

since it breaks the strong bisimulation we are looking for (Diagram <ref>). At the same time, we

\[
\begin{array}{rcl@{\quad}l}
\termname{\beta}{\termcont{\alpha}{c}}  & \ruleEqsigRho & \termren{\alpha}{\beta}{c}
\end{array}
\]

motivating the introduction of the explicit renaming operator in
$\calcLambdaM$-calculus. Since   computation
(Def. <ref>) does not execute explicit renamings, taking
the  form of both sides of equation $\sigma_7$ would not necessarily
yield  $\eqsigma$-equivalent $\calcLambdaM$-terms. In order to account for this
and for the purposes of this section only, we extend $\eqsigma$ with the
following equation:

\[
\begin{array}{rcl@{\quad}l}
\termren{\alpha}{\beta}{c}  & \ruleEqsigRen & \renapply{\ren{\alpha}{\beta}}{c}
\end{array}
\]

The resulting equivalence is dubbed $\eqsigmaren$. We can now state the main
result we prove in this section
(Thm. <ref>), namely that
for all $o, p \in \Object{\calcLambdaMu}$:

\[
o \eqlaurent p \quad\text{iff}\quad \fcan{o} \eqsigmaren \fcan{p}
\]

The left-to-right direction is relatively straightforward.  We'll state it
formally since we will refer to it later:

Let $o, p \in \Object{\calcLambdaMu}$. If $o \eqlaurent p$, then $\fcan{o}
\eqsigmaren \fcan{p}$.

The reciprocal is our main focus here. It relies on first establishing a formal
relation between $\eqsigmaren$ and $\eqppn$
(Thm. <ref>).

Correspondence between $\eqsigmaren$ and $\eqppn$

This section studies the soundness and completeness of $\eqsigmaren$ with
respect to the PPN semantics. This result is based on the completeness property
for $\eqlaurent$ [25], which we describe next. The equivalence
relation $\eqlaurent$ has the interesting property that any two typable objects
$o$ and $p$ of the $\calcLambdaMu$-calculus are $\sigmalaurent$-equivalent if
and only if their corresponding type derivations are structurally equivalent
when translated using the following:

The multiplicative translation of a type derivation $\pi$ into a
polarised proof-nets, written $\toPPNMnf{\pi}$, is defined as
the multiplicative normal form of $\toPPN{\pi}$.

In other words, two
$\sigmalaurent$-equivalent objects have the same PPN representation modulo
multiplicative cuts, and vice-versa:

Let $o, p \in \Object{\calcLambdaMu}$. Then $o \eqlaurent p$ iff
$\toPPNMnf{(\pi_{o})} \eqppn \toPPNMnf{(\pi_{p})}$, where $\pi_{o}$ and
$\pi_{p}$ are the corresponding related type derivations.

Note the use of  $\toPPNMnf{\_}$ rather than $\toPPN{\_}$. For the latter, the
result does not hold. It suffices to consider equation $\ruleEqlauAbs$ from
Fig. <ref>.

A soundness result also holds for $\calcLambdaM$:

Let $o, p \in \Object{\calcLambdaM}$. Then $o \eqsigma p$ implies
$\toPPNMnf{(\pi_{o})} \eqppn \toPPNMnf{(\pi_{p})}$, where $\pi_{o}$ and
$\pi_{p}$ are the corresponding related type derivations.

By induction on $o \eqsigma p$. Details in Appendix <ref>.

The previous soundness property can be extended to the equivalence
$\ruleEqsigRen$. Indeed, the equivalence relation $\eqsigmaren$ also preserves
the multiplicative normal forms of the associated PPN.

Let $o, p \in \Object{\calcLambdaM}$ be typed. If $o \eqsigmaren p$, then
$\toPPNMnf{(\pi_{o})} \eqppn \toPPNMnf{(\pi_{p})}$, where $\pi_{o}$ and
$\pi_{p}$ are the corresponding related type derivations.

An interesting, though expected, result is that the multiplicative normal forms
of the PPN are preserved by   computation.

Let $o, p \in \Object{\calcLambdaM}$ be typed. If $o \reduce[\rcan] p$,
then $\toPPNMnf{(\pi_{o})} \eqppn \toPPNMnf{(\pi_{p})}$, where $\pi_{o}$
and $\pi_{p}$ are the corresponding  related type derivations.

By induction on $o \reduce[\rcan] p$. Details in
Appendix <ref>.

To obtain the desired completeness result of $\eqsigmaren$ with respect to
$\eqppn$, it is necessary to relate the sets $\Object{\calcLambdaM}$ and
$\Object{\calcLambdaMu}$. We do so by means of an expansion function
$\fexp{\_}$, that eliminates the explicit operators of an object by
\[
\begin{array}{c@{\qquad}c}
\begin{array}{rcll}
\fexp{x}                                & \eqdef  & x \\
\fexp{\termapp{t}{u}}                   & \eqdef  & \termapp{\fexp{t}}{\fexp{u}} \\
\fexp{\termabs{x}{t}}                   & \eqdef  & \termabs{x}{\fexp{t}} \\
\fexp{\termcont{\alpha}{c}}             & \eqdef  & \termcont{\alpha}{\fexp{c}} \\
\fexp{\termsubs{x}{u}{t}}               & \eqdef  & \termapp{(\termabs{x}{\fexp{t}})}{\fexp{u}}
\end{array}
\begin{array}{rcll}
\fexp{\termname{\alpha}{t}}             & \eqdef  & \termname{\alpha}{\fexp{t}} \\
\fexp{\termrepl[\alpha']{\alpha}{s}{c}} & \eqdef  & \termname{\alpha'}{\termconc{(\termcont{\alpha}{\fexp{c}})}{\fexp{s}}} \\
\fexp{\termren{\alpha}{\beta}{c}}       & \eqdef  & \termname{\beta}{\termcont{\alpha}{\fexp{c}}} \\
\fexp{\termpush{t}{s}}                  & \eqdef  & \termpush{\fexp{t}}{\fexp{s}}
\end{array}
\end{array}
\]
Note that $\fexp{\_}$ is not the left-inverse of $\fcan{\_}$, given
$o \in \Object{\calcLambdaMu}$, it is not necessarily the case $\fexp{\fcan{o}}
= o$. For example, take $o =
\termapp{\termapp{(\termcont{\alpha}{\termname{\alpha}{x}})}{y}}{z}$. Then,
$\fcan{o} =
\termcont{\alpha'}{\termrepl[\alpha']{\alpha}{\termpush{y}{z}}{(\termname{\alpha}{x})}}$
while $\fexp{\fcan{o}} =
\termcont{\alpha'}{\termname{\alpha'}{\termapp{\termapp{(\termcont{\alpha}{\termname{\alpha}{x}})}{y}}{z}}}$.
However, it yields an equivalent object thanks to rule $\ruleEqlauTheta$.

Let $o \in \Object{\calcLambdaM}$.

* $\deriv[\pi]{\sequM{\Gamma}{\assign{o}{T}}{\Delta}}[\SysMuEx]$
if and only if $\deriv[\pi']{\sequM{\Gamma}{\assign{\fcan o}{T}}{\Delta}}[\SysMuEx]$.

* $\deriv[\pi]{\sequM{\Gamma}{\assign{o}{T}}{\Delta}}[\SysMuEx]$
if and only if $\deriv[\pi']{\sequM{\Gamma}{\assign{\fexp o}{T}}{\Delta}}[\SysMuEx]$.

Given that the expansion steps on the $\calcLambdaM$-calculus are translated
into multiplicative cuts in the PPN, we have:

*  Let $o \in
\Object{\calcLambdaMu}$. Then, $\toPPNMnf{(\pi_{o})} \eqppn
\toPPNMnf{(\pi_{\fcan{o}})}$, where $\pi_{o}$ and $\pi_{\fcan{o}}$ are the
corresponding related type derivations.

*  Let $o \in
\Object{\calcLambdaM}$. Then, $\toPPNMnf{(\pi_{o})} \eqppn
\toPPNMnf{(\pi_{\fexp{o}})}$, where $\pi_{o}$ and $\pi_{\fexp{o}}$ are the
corresponding  related type derivations.

Item <ref> is by induction on the
length of $o \reducemany[\rcan] \fcan{o}$.
Item <ref> is by induction on $o$.
Details in Appendix <ref>.

Hence, as an immediate corollary we have:

Let $o \in \Object{\calcLambdaMu}$ and $o' \in \Object{\calcLambdaM}$ be typed. Then,
$\toPPNMnf{(\pi_{o})} \eqppn \toPPNMnf{(\pi_{\fexp{\fcan{o}}})}$ and
$\toPPNMnf{(\pi_{o'})} \eqppn \toPPNMnf{(\pi_{\fcan{\fexp{o'}}})}$.

These auxiliary results lead to the sought-for correspondence between
$\eqsigmaren$ and the structural equivalence for PPN.

Let $o, p \in \Object{\calcLambdaMu}$ be typed. Then, $\fcan{o} \eqsigmaren \fcan{p}$
iff $\toPPNMnf{(\pi_{\fcan{o}})} \eqppn \toPPNMnf{(\pi_{\fcan{p}})}$, where
$\pi_{\fcan{o}}$ and $\pi_{\fcan{p}}$ are the corresponding related type

$\Rightarrow$) First remark that given $o, p \in \Object{\calcLambdaMu}$ we have $\fcan{o}, \fcan{p} \in \Object{\calcLambdaM}$.   By
Lem. <ref>, $\fcan{o} \eqsigmaren
\fcan{p}$ implies $\toPPNMnf{(\pi_{\fcan{o}})} \eqppn
\toPPNMnf{(\pi_{\fcan{p}})}$.

$\Leftarrow$) Let $\toPPNMnf{(\pi_{\fcan{o}})} \eqppn
\toPPNMnf{(\pi_{\fcan{p}})}$. By
Lem. <ref>
$\toPPNMnf{(\pi_{\fexp{\fcan{o}}})} \eqppn \toPPNMnf{(\pi_{\fexp{\fcan{p}}})}$
and, by Cor. <ref>, $\toPPNMnf{(\pi_{o})}
\eqppn \toPPNMnf{(\pi_{p})}$. Then, by
Thm. <ref>,
$o \eqlaurent p$ and we conclude by
Lem. <ref>, $\fcan{o} \eqsigmaren
\fcan{p}$.

Correspondence between $\eqsigmaren$ and $\eqlaurent$

The correspondence between $\eqsigmaren$ and $\eqppn$
(Thm. <ref>) ends up relating
the notion of equivalence for the $\calcLambdaM$-calculus developed in this
work with the usual one in the literature for the $\calcLambdaMu$-calculus.

Let $o, p \in \Object{\calcLambdaMu}$. Then, $o \eqlaurent p$ iff $\fcan{o}
\eqsigmaren \fcan{p}$.

$\Rightarrow$) By
Lem. <ref>, $o \eqlaurent p$
implies $\fcan{o} \eqsigmaren \fcan{p}$.

$\Leftarrow$) Let $\fcan{o} \eqsigmaren \fcan{p}$. By
Lem. <ref>,
$\toPPNMnf{(\pi_{\fcan{o}})} \eqppn \toPPNMnf{(\pi_{\fcan{p}})}$ and, by
Lem. <ref>
(<ref>), $\toPPNMnf{(\pi_{o})}
\eqppn \toPPNMnf{(\pi_{p})}$.

Then, by
Thm. <ref>,
$\toPPNMnf{(\pi_{o})} \eqppn \toPPNMnf{(\pi_{p})}$ implies $o \eqlaurent p$.

This constitutes the main result of the current section, which can be
graphically depicted by the following diagram:

\[
\begin{tikzcd}
o \eqlaurent p \arrow[<->,dotted]{d}[anchor=north,left]{Thm.~\ref{t:control:preliminaries:proof-nets:translation:eqlaurent-iff-eqppn}}
\arrow[<->,dotted]{r}[anchor=north,above]{Thm.~\ref{t:control:correspondence:eqlaurent-iff-eqsigmaren}}
&[2em] \fcan{o} \eqsigmaren \fcan{p} \arrow[<->,dotted]{d}[anchor=north,right]{Thm.~\ref{t:control:correspondence:eqsigmaren-iff-eqppn}}
\\
\toPPNMnf{(\pi_{o})} \eqppn \toPPNMnf{(\pi_{p})}
&[2em] \toPPNMnf{(\pi_{\fcan{o}})} \eqppn \toPPNMnf{(\pi_{\fcan{p}})}
\end{tikzcd}
\]

It is particularly interesting to remark the fact that $\eqlaurent$
strictly contains $\eqsigma$, but the difference between these relations
resides exclusively in how they manage the renaming (implicit vs. explicit).
This is succinctly captured by rule $\ruleEqsigRen$.

§ CONCLUSION

This paper is about $\sigma$-equivalence in classical logic and
the negligible effect it has on the operational behavior of the
terms it relates.   This paperIt refines the
$\calcLambdaMu$-calculus with explicit operators for renaming,
substitution and replacement, by splitting in particular  each of
the rules $\beta$ and $\mu$ of $\calcLambdaMu$ into multiplicative and
exponential fragments, . For this purpose,thus resulting in
the introduction of a new calculus called $\calcLambdaM$.
This new presentation of $\calcLambdaMu$ allows to reformulate
$\sigmalaurent$-equivalence on $\calcLambdaMu$-terms as a strong
bisimulation relation $\eqsigma$ on $\calcLambdaM$-terms.  The main
obstacle to  extract a bisimulation on $\calcLambdaM$ from the original
Laurent's $\sigma$-equivalence on $\calcLambdaMu$-terms
is axiom $\eqsigma[\rho]$, which leads to $\sigma$-equivalence
failing to be a strong bisimulation. We learn that we cannot remove
$\eqsigma[\rho]$ entirely, since it is needed to close other
commutation diagrams in the proof of strong bisimulation. However, a
restriction of $\eqsigma[\rho]$ turns out to suffice. This
restriction is formulated thanks to the notion of explicit renaming,
which we introduce in our calculus $\calcLambdaM$. More concisely,
the use of explicit renamings allows us to show that
$\sigma$-equivalence is exactly captured by our strong bisimulation
together with a simple axiom identifying explicit with implicit
renaming (axiom $\ruleEqsigRen$). Failing to distinguish these two forms of
renaming in Laurent's $\sigma$-equivalence makes impossible the
bisimulation property.  Moreover, $\reduce[\rLM]$ is shown
to be confluent.

Besides [25], which inspired this paper and has been discussed at
length, we briefly mention further related work. In [3],
polarised MELL are represented by proof-nets without boxes, by using the
polarity information to transform explicit $\iformbang$-boxes into more compact

In [23], the $\calcLambdaMu$-calculus is refined to a
calculus $\calcLambdaMuR$ with explicit operators, together with a
linear substitution/replacement operational semantics at a
distance. At first sight $\calcLambdaMuR$ seems to be more atomic than
$\calcLambdaM$. However, $\calcLambdaMuR$ forces the explicit replacements to
be evaluated from left to right, there is no mechanism of composition.
Moreover, explicit replacements in $\calcLambdaMuR$ are defined on terms, and not on stacks, and  renamings are still implicit, thus the calculus is not able to capture an appropriate notion of bisimulation such as the one presented in this paper.

Other classical term calculi exist,  [12, 9, 30, 33], but none of these formalisms
decomposes term reduction  by means of a fine distinction between
multiplicative and exponential rules. Moreover, all these calculi
lack an  explicit renaming operation. Thus, the main ingredients
needed to build a strong bisimulation are simply not available. Of
particular interest would be to understand how to integrate
explicit renaming in $\calcLambdaMuT$ [12], a calculus
inspired from sequent calculus which is constructed as a perfectly
symmetric formalism to deal uniformly with CBN and CBV.

A further related reference
is [20], where PPNs are used to interpret processes from the $\pi$-calculus. A precise correspondence is established between PPN and a
typed version of the asynchronous $\pi$-calculus. Moreover, they show that
Laurent's $\eqlaurent$ corresponds exactly to structural equivalence of
$\pi$-calculus processes (Prop. 1 in op.cit). In [26] Laurent and
Regnier show that there is a precise correspondence between CPS translations
from classical calculi (such as $\calcLambdaMu$) into intuitionistic ones on
the one hand, and translations between LLP and LL on the other.

It would be interesting to analyse other rewriting properties of our term
language such as preservation of $\calcLambdaMu$-strong normalisation of the
reduction relations $\reduce[\rLM]$ and $\reducemean$ or confluence of

Moreover, following the computational
interpretation of deep inference provided by the intuitionistic atomic
lambda-calculus [15], it would be interesting to investigate a
classical extension and its corresponding notion of strong bisimulation. It is
also natural to wonder what would be an ideal syntax for classical logic, that
is able to capture strong bisimulation by reducing the syntactical axioms to a
small and simple set of equations.

Explicit Substitutions are a means of modeling sharing in lambda calculi and
hence well suited for capturing call-by-need [2]. We believe
$\calcLambdaM$ may prove useful in devising a notion of call-by-need for
classical computation.

Finally, our notion of $\eqsigma$-equivalence could facilitate proofs of
correctness between abstract machines and $\calcLambdaMu$
(like [2] for lambda-calculus) and help establish whether
abstract machines for $\calcLambdaMu$ are “reasonable” [2].

[1]
Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi.
A nonstandard standardization theorem.
In The 41st Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '14, San Diego, CA, USA, January
20-21, 2014, pages 659–670, 2014.

[2]
Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza.
Distilling abstract machines.
In Proceedings of the 19th ACM SIGPLAN international
conference on Functional programming, Gothenburg, Sweden, September 1-3,
2014, pages 363–376, 2014.

[3]
Beniamino Accattoli.
Compressing polarized boxes.
In 28th Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages
428–437, 2013.

[4]
Beniamino Accattoli.
Proof nets and the linear substitution calculus.
In Theoretical Aspects of Computing - ICTAC 2018 - 15th
International Colloquium, Stellenbosch, South Africa, October 16-19, 2018,
Proceedings, pages 37–61, 2018.

[5]
Beniamino Accattoli and Delia Kesner.
The structural lambda-calculus.
In Anuj Dawar and Helmut Veith, editors, Computer Science Logic,
24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL,
Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 381–395. Springer, 2010.

[6]
Beniamino Accattoli and Delia Kesner.
The permutative \(\lambda\)-calculus.
In Logic for Programming, Artificial Intelligence, and Reasoning
- 18th International Conference, LPAR-18, Mérida, Venezuela, March
11-15, 2012. Proceedings, pages 23–36, 2012.

[7]
Beniamino Accattoli and Delia Kesner.
Preservation of strong normalisation modulo permutations for the
structural lambda-calculus.
Log. Methods Comput. Sci., 8(1), 2012.

[8]
Jean-Marc Andreoli.
Proposition pour une synthèse des paradigmes de la
programmation logique et de la programmation par objets.
PhD thesis, Université Paris VI, 1990.

[9]
Philippe Audebaud.
Explicit substitutions for the lambda-mu-calculus.
Technical Report RR-1994-26, LIP, Ecole Normale Supérieure de
Lyon, Lyon, 1994.

[10]
Marc Bezem, Jan Willem Klop, and Vincent van Oostrom.
Term Rewriting Systems (TeReSe).
Cambridge University Press, 2003.

[11]
Franz Baader and Tobias Nipkow.
Term rewriting and all that.
Cambridge University Press, 1998.

[12]
Pierre-Louis Curien and Hugo Herbelin.
The duality of computation.
In Proceedings of the Fifth ACM SIGPLAN International
Conference on Functional Programming (ICFP '00), Montreal, Canada,
September 18-21, 2000., pages 233–243, 2000.

[13]
Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques
Confluence properties of weak and strong calculi of explicit
J. ACM, 43(2):362–397, 1996.

[14]
Philippe de Groote.
On the relation between the lambda-mu-calculus and the syntactic
theory of sequential control.
In Logic Programming and Automated Reasoning, 5th International
Conference, LPAR'94, Kiev, Ukraine, July 16-22, 1994, Proceedings, pages
31–43, 1994.

[15]
Tom Gundersen, Willem Heijltjes, and Michel Parigot.
Atomic lambda calculus: A typed lambda-calculus with explicit
In 28th Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages
311–320, 2013.

[16]
Jean-Yves Girard.
Linear logic.
Theoretical Computer Science, 50:1–102, 1987.

[17]
Jean-Yves Girard.
A new constructive logic: Classical logic.
Math. Struct. Comput. Sci., 1(3):255–296, 1991.

[18]
Timothy Griffin.
A formulae-as-types notion of control.
In Conference Record of the Seventeenth Annual ACM Symposium
on Principles of Programming Languages, San Francisco, California, USA,
January 1990, pages 47–58, 1990.

[19]
Hugo Herbelin.
A lambda-calculus structure isomorphic to gentzen-style sequent
calculus structure.
In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science
Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September
25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer
Science, pages 61–75. Springer, 1994.

[20]
Kohei Honda and Olivier Laurent.
An exact correspondence between a typed pi-calculus and polarised
Theor. Comput. Sci., 411(22-24):2223–2238, 2010.

[21]
Delia Kesner, Eduardo Bonelli, and Andrés Viso.
Strong bisimulation for control operators (invited talk).
In 28th EACSL Annual Conference on Computer Science Logic,
CSL 2020, January 13-16, 2020, Barcelona, Spain, pages 4:1–4:23, 2020.

[22]
Delia Kesner.
A theory of explicit substitutions with safe and full composition.
Logical Methods in Computer Science, 5(3), 2009.

[23]
Delia Kesner and Pierre Vial.
Non-idempotent types for classical calculi in natural deduction
Logical Methods in Computer Science, 16(1), 2019.

[24]
Olivier Laurent.
A study of polarization in logic.
PhD thesis, Université de la Méditerranée -
Aix-Marseille II, 2002.

[25]
Olivier Laurent.
Polarized proof-nets and lambda-\(\mathrm{\mu}\)-calculus.
Theor. Comput. Sci., 290(1):161–188, 2003.

[26]
Olivier Laurent and Laurent Regnier.
About translations of classical logic into polarized linear logic.
In 18th IEEE Symposium on Logic in Computer Science (LICS
2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pages 11–20, 2003.

[27]
Tobias Nipkow.
A critical pair lemma for higher-order rewrite systems and its
applications to $\lambda^\star$.
In Proceedings of the First Workshop on Logical Frameworks,
Antibes, France, May 1990, pages 361–376, 1990.

[28]
Michel Parigot.
Lambda-mu-calculus: An algorithmic interpretation of classical
natural deduction.
In Andrei Voronkov, editor, Logic Programming and Automated
Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July
15-20, 1992, Proceedings, volume 624 of Lecture Notes in Computer
Science, pages 190–201. Springer, 1992.

[29]
Michel Parigot.
Classical proofs as programs.
In Computational Logic and Proof Theory, Third Kurt Gödel
Colloquium, KGC'93, Brno, Czech Republic, August 24-27, 1993, Proceedings,
pages 263–276, 1993.

[30]
Emmanuel Polonovski.
Subsitutions explicites, logique et normalisation. (Explicit
substitutions, logic and normalization).
PhD thesis, Paris Diderot University, France, 2004.

[31]
Laurent Regnier.
Une équivalence sur les lambda-termes.
Theor. Comput. Sci., 126(2):281–292, 1994.

[32]
Masako Takahashi.
Parallel reductions in lambda-calculus.
Inf. Comput., 118(1):120–127, 1995.

[33]
Steffen van Bakel and Maria Grazia Vigliotti.
A fully-abstract semantics of lambda-mu in the pi-calculus.
In Proceedings Fifth International Workshop on Classical Logic
and Computation, CL&C 2014, Vienna, Austria, July 13, 2014, pages 33–47,

§ CONFLUENCE OF THE $\CALCLAMBDAM$-CALCULUS

To prove confluence of the $\calcLambdaM$-calculus we use the
interpretation method [13], where $\calcLambdaM$ is
projected into the $\calcLambdaMuRho$-calculus, introduced in what
follows. Notice that we cannot simply project the
$\calcLambdaM$-calculus into the $\calcLambdaMu$-calculus because
of our
built-in explicit renamings: indeed, it is not possible to purify our
objects w.r.t. explicit renamings since there are no operations to do
that inside the $\calcLambdaM$-calculus itself.

Given a countably infinite set of variables  $\TermVariable$ ($\termvar{x},
\termvar{y}, \ldots$) and names  $\TermName$ ($\alpha, \beta, \ldots$),
the sets of  objects $\Object{\calcLambdaMuRho}$, terms
$\Term{\calcLambdaMuRho}$, commands $\Command{\calcLambdaMuRho}$,
stacks  and  contexts  of the $\calcLambdaMuRho$-calculus
are defined by the following grammar:
\[
\begin{array}{rrcl}
\textbf{(Objects)}          & o         & \Coloneq  & t \mid c \mid s \\
\textbf{(Terms)}            & t         & \Coloneq  & x \mid \termapp{t}{t} \mid \termabs{x}{t} \mid \termcont{\alpha}{c} \\
\textbf{(Commands)}         & c         & \Coloneq  & \termname{\alpha}{t} \mid \termren{\alpha}{\beta}{c} \\
\textbf{Stacks}             & s         & \Coloneq  & t \mid \termpush{t}{s} \\
\textbf{(Contexts)}         & \ctxt{O}  & \Coloneq  & \ctxt{T} \mid \ctxt{C} \mid \ctxt{S} \\
\textbf{(Term Contexts)}    & \ctxt{T}  & \Coloneq  & \Box \mid \termapp{\ctxt{T}}{t} \mid \termapp{t}{\ctxt{T}} \mid \termabs{x}{\ctxt{T}} \mid \termcont{\alpha}{\ctxt{C}} \\
\textbf{(Command Contexts)} & \ctxt{C}  & \Coloneq  & \boxdot \mid
\termname{\alpha}{\ctxt{T}}
\mid
\termren{\alpha}{\beta}{\ctxt{C}}
\\
\textbf{(Stack Contexts)}   & \ctxt{S}  & \Coloneq  & \boxdot \mid \termpush{\ctxt{T}}{s} \mid \termpush{t}{\ctxt{S}}
\end{array}
\]
The commands of the $\calcLambdaMu$-calculus
are enriched with an explicit renaming
Notice that $\Object{\calcLambdaMuRho} \subset
\Object{\calcLambdaM}$ (similarly  $\Term{\calcLambdaMuRho} \subset
\Term{\calcLambdaM}$ and  $\Command{\calcLambdaMuRho} \subset
\Command{\calcLambdaM}$).

We write $\vec{\alpha}$ for a non-empty sequence of distinct names
$\alpha_1, \ldots, \alpha_n$ and $\fsize{\vec{\alpha}}$ for
the number of names in the sequence.
The simultaneous replacement operation
is inductively defined as follows:
\[
\begin{array}{rcll}
\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{x}                                                                       & \eqdef  & x \\
\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{(\termapp{t}{u})}                                                        & \eqdef  & \termapp{\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{t}}{\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{u}} \\
\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{(\termabs{x}{t})}                                                        & \eqdef  & \termabs{x}{\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{t}}                                                                      & x \notin s \\
\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{(\termcont{\gamma}{c})}                                                  & \eqdef  & \termcont{\gamma}{\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{c}}                                                                & \gamma \notin s, \gamma \notin \vec{\alpha}, \gamma \notin \vec{\beta} \\
\replapply{\repls[\vec{\beta_1}\beta\vec{\beta_2}]{\vec{\alpha_1}\alpha\vec{\alpha_2}}{s}}{(\termname{\alpha}{t})}        & \eqdef  & \termname{\beta}{\termconc{(\replapply{\repls[\vec{\beta_1}\beta\vec{\beta_2}]{\vec{\alpha_1}\alpha\vec{\alpha_2}}{s}}{t})}{s}} \\
\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{(\termname{\gamma}{t})}                                                  & \eqdef  & \termname{\gamma}{\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{t}}                                                                & \gamma \notin \vec{\alpha} \\
\replapply{\repls[\vec{\beta_1}\beta\vec{\beta_2}]{\vec{\alpha_1}\alpha\vec{\alpha_2}}{s}}{(\termren{\gamma}{\alpha}{c})} & \eqdef  & \termren{\delta}{\beta}{\replapply{\repls[\delta\vec{\beta_1}\beta\vec{\beta_2}]{\gamma\vec{\alpha_1}\alpha\vec{\alpha_2}}{s}}{c}}    & \delta \text{ fresh} \\
\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{(\termren{\gamma}{\beta}{c})}       & \eqdef  & \termren{\gamma}{\beta}{(\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{c})}                                                                                & \gamma \notin \vec{\alpha}, \gamma \notin \vec{\beta} \\
\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{(\termpush{t}{s'})}                 & \eqdef  & \termpush{\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{t}}{\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{s'}}
\end{array}
\]
Notice in the 7th line of the definition the
case of a replacement affecting an  explicit renaming
which causes the accumulation of
the names $\gamma$ and $\delta$ (this one fresh)
in the replacement affecting the command $c$.

The application of the substitution $\subs{x}{u}$ to an
$\calcLambdaMuRho$-object $o$ naturally extends that of the
(Sec. <ref>).

The  one-step reduction relation $\reduce[\rlmr]$
is defined as the closure by
contexts $\ctxt{O}_\TermSort$ of the rewriting rules
$\rbeta$ and $\rmus$:
\[
\begin{array}{rll}
\termapp{(\termabs{x}{t})}{u}         & \rrule{\rbeta}  & \subsapply{\subs{x}{u}}{t} \\
\termconc{(\termcont{\alpha}{c})}{s}  & \rrule{\rmus}   & \termcont{\alpha'}{\replapply{\repls[\alpha']{\alpha}{s}}{c}}
\end{array}
\]
where  $\rrule{\rmus}$ requires $\alpha'$ to be a fresh name
($\alpha' \neq \alpha$ and  $\alpha' \notin c$).

In what follows we introduce some auxiliary
results about the simultaneous replacement operation.

Let $o \in \Object{\calcLambdaMuRho}$ and let $s$ be a stack.  Then,

* $\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{o} =
\replapply{\repls[p(\vec{\beta})]{p(\vec{\alpha})}{s}}{o}$ for every
permutation $p$ on $[1,\fsize{\vec{\alpha}}]$, where $\fsize{\vec{\alpha}}$
measures the number of names in $\vec{\alpha}$.

* If $\alpha \notin \fn{o}$, then
\replapply{\repls[\vec{\beta_1}\vec{\beta_2}]{\vec{\alpha_1}\vec{\alpha_2}}{s}}{o}$.

Let $o \in \Object{\calcLambdaMuRho}$ and let $s$ be a stack. If
$\vec{\alpha} \cap \fn{o} = \emptyset$, then
$\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{o} = o$.

Let $o \in \Object{\calcLambdaMuRho}$, $u \in \Term{\calcLambdaMuRho}$ and
let $s$ be a stack.

*  If
$x \notin \fv{s}$, then
\subsapply{\subs{x}{\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{u}}}{\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{o}}$.

*  If
$\vec{\alpha} \cap \fn{u} = \emptyset$, then
\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{\subsapply{\subs{x}{u}}{s}}}{\subsapply{\subs{x}{u}}{o}}$.

Let  $o \in \Object{\calcLambdaMuRho}$ and
let $s,s'$ be  stacks. If the name sequences
$\vec{\alpha} = \vec{\alpha_1}\vec{\alpha_2}$, $\vec{\beta} =
\vec{\beta_1}\vec{\beta_2}$, $\vec{\gamma} = \vec{\gamma_1}\vec{\gamma_2}$ and
$\vec{\delta} = \vec{\delta_1}\vec{\delta_2}$ are such that
$\vec{\beta_1} =
\vec{\gamma_1}$, $\vec{\beta_2} \cap \vec{\gamma_2} = \emptyset$, $\chi \notin
s'$ for all  $\chi \in \vec{\alpha}$, and $\vec{\beta}\vec{\delta}$
are fresh names, then
\replapply{\repls[\vec{\beta_2}]{\vec{\alpha_2}}{\replapply{\repls[\vec{\delta}]{\vec{\gamma}}{s'}}{s}}}{\replapply{\repls[\vec{\delta_1}]{\vec{\alpha_1}}{\termpush{\replapply{\repls[\vec{\delta}]{\vec{\gamma}}{s'}}{s}}{s'}}}{\replapply{\repls[\vec{\delta_2}]{\vec{\gamma_2}}{s'}}{o}}}$.

Let  $o \in \Object{\calcLambdaMuRho}$ and $s$ be a stack.
If the name sequences $\vec{\alpha}$, $\vec{\beta}$, $\vec{\gamma}$
and $\vec{\delta}$ are such that $\vec{\beta} \cap \vec{\gamma} = \emptyset$
and  $\chi \notin s$ for all
$\chi \in \vec{\gamma}$, then
\replapply{\repls[\vec{\delta}\vec{\beta}]{\vec{\gamma}\vec{\alpha}}{s}}{o}$.

Confluence of the $\calcLambdaMuRho$-calculus

Confluence of $\calcLambdaMuRho$ is shown by means of Tait–Martin-Löf's
method [32]. For that, we introduce a notion of parallel
reduction on $\calcLambdaMuRho$-objects.

The parallel reduction relation $\reducesimul[\rlmr]$
$\calcLambdaMuRho$-objects is defined by induction as follows:
\[
\begin{array}{c}
\Rule{\vphantom{t}}{
x \reducesimul[\rlmr] x
\qquad
\Rule{
t \reducesimul[\rlmr] t'
\quad
u \reducesimul[\rlmr] u'
\termapp{t}{u} \reducesimul[\rlmr] \termapp{t'}{u'}
\qquad
\Rule{
t \reducesimul[\rlmr] t'
\termabs{x}{t} \reducesimul[\rlmr] \termabs{x}{t'}
\\
\\
\Rule{
c \reducesimul[\rlmr] c'
\termcont{\alpha}{c} \reducesimul[\rlmr] \termcont{\alpha}{c'}
\qquad
\Rule{
t \reducesimul[\rlmr] t'
\termname{\alpha}{t} \reducesimul[\rlmr] \termname{\alpha}{t'}
\\
\\
\Rule{
c \reducesimul[\rlmr] c'
\termren{\alpha}{\beta}{c} \reducesimul[\rlmr] \termren{\alpha}{\beta}{c'}
\qquad
\Rule{
t \reducesimul[\rlmr] t'
\quad
s \reducesimul[\rlmr] s'
\termpush{t}{s} \reducesimul[\rlmr] \termpush{t'}{s'}
\\
\\
\Rule{
t \reducesimul[\rlmr] t'
\quad
u \reducesimul[\rlmr] u'
\termapp{(\termabs{x}{t})}{u} \reducesimul[\rlmr] \subsapply{\subs{x}{t'}}{s'}
\qquad
\Rule{
c \reducesimul[\rlmr] c'
\quad
s \reducesimul[\rlmr] s'
\termconc{(\termcont{\alpha}{c})}{s} \reducesimul[\rlmr] \termcont{\alpha'}{\replapply{\repls[\alpha']{\alpha}{s'}}{c'}}
\end{array}
\]

Notice that the parallel reduction relation is reflexive.

In what follows we
study the stability of $\reducesimul[\rlmr]$
by substitution and replacement.

Let  $o,o' \in \Object{\calcLambdaMuRho}$,
$u,u' \in \Term{\calcLambdaMuRho}$
and $s,s'$
be stacks
such that  $o \reducesimul[\rlmr] o'$,
$u \reducesimul[\rlmr] u'$ and $s \reducesimul[\rlmr] s'$. Then,
$\subsapply{\subs{x}{u}}{o} \reducesimul[\rlmr] \subsapply{\subs{x}{u'}}{o'}$
and $\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s}}{o}
\reducesimul[\rlmr]
\replapply{\repls[\vec{\beta}]{\vec{\alpha}}{s'}}{o'}$.

Both  statements are by induction on $o \reducesimul[\rlmr] o'$.
The second one uses
Lem. <ref>
Lem. <ref>.

A last auxiliary result shows that
the parallel reduction starting
at a term of the form $\termconc{(\termcont{\alpha}{c})}{s}$
represents a  $\itermcont$-abstraction
consuming all, some or none of the arguments

Let $t \in \Term{\calcLambdaMuRho}$, $c \in
\Command{\calcLambdaMuRho}$ and let  $s$ be a  stack such that
$\termconc{(\termcont{\alpha}{c})}{s} \reducesimul[\rlmr] t$.  Then,

*  $t =
\termconc{(\termcont{\alpha}{c'})}{s'}$ with $c \reducesimul[\rlmr] c'$ and $s
\reducesimul[\rlmr] s'$; or

*  $t =
\termcont{\alpha'}{\replapply{\repls[\alpha']{\alpha}{s'}}{c'}}$ with $c
\reducesimul[\rlmr] c'$ and $s \reducesimul[\rlmr] s'$; or

*  $t =
\termconc{(\termcont{\alpha'}{\replapply{\repls[\alpha']{\alpha}{s'_0}}{c'}})}{s'_1}$
with  $s = \termpush{s_0}{s_1}$, $c \reducesimul[\rlmr] c'$ and $s
\reducesimul[\rlmr] \termpush{s'_0}{s'_1}$.

Confluence of the parallel reduction relation
is a consequence of the fact that
$\reducesimul[\rlmr]$  enjoys the diamond property [27, 10].
The proof uses the previous auxiliary lemmas.

The parallel reduction relation $\reducesimul[\rlmr]$
satisfies the diamond property,
and thus is confluent  (CR).

Last, in order to deduce confluence of  $\calcLambdaMuRho$
by means of Tait–Martin-Löf's method,
it is sufficient to prove that $\reducesimul[\rlmr]$ extends
$\reduce[\rlmr]$ and at the same time is included
in the reflexive-transitive closure $\reducemany[\rlmr]$.

$\reduce[\rlmr] \mathbin{\subseteq} \reducesimul[\rlmr] \mathbin{\subseteq}
\reducemany[\rlmr]$.

Confluence of  $\reduce[\rlmr]$ is an immediate
consequence of
Lem. <ref> and
Lem. <ref>.

The reduction relation
$\reduce[\rlmr]$ is confluent (CR).

Confluence of the $\calcLambdaM$-calculus

Confluence of the $\calcLambdaM$-calculus is proved by using the interpretation
method [13], which projects $\calcLambdaM$-objects into

The projection $\toLMR{\_}$ from $\calcLambdaM$-objects
to  $\calcLambdaMuRho$-objects is defined as
\[
\begin{array}{c@{\qquad}c}
\begin{array}{rcl}
\toLMR{x}                                   & \eqdef  & x \\
\toLMR{(\termapp{t}{u})}                    & \eqdef  & \termapp{\toLMR{t}}{\toLMR{u}} \\
\toLMR{(\termabs{x}{t})}                    & \eqdef  & \termabs{x}{\toLMR{t}} \\
\toLMR{(\termcont{\alpha}{c})}              & \eqdef  & \termcont{\alpha}{\toLMR{c}} \\
\toLMR{(\termsubs{x}{u}{t})}                & \eqdef  & \subsapply{\subs{x}{\toLMR{u}}}{\toLMR{t}}
\end{array}
\begin{array}{rcl}
\toLMR{(\termname{\alpha}{t})}              & \eqdef  & \termname{\alpha}{\toLMR{t}} \\
\toLMR{(\termrepl[\alpha']{\alpha}{s}{c})}  & \eqdef  & \replapply{\repls[\alpha']{\alpha}{\toLMR{s}}}{\toLMR{c}} \\
\toLMR{(\termren{\alpha}{\beta}{c})}        & \eqdef  & \termren{\alpha}{\beta}{\toLMR{c}} \\
\toLMR{(\termpush{s}{t})}                   & \eqdef  & \termpush{\toLMR{s}}{\toLMR{t}}
\end{array}
\end{array} \]

Let  $o \in \Object{\calcLambdaM}$, $u \in \Term{\calcLambdaM}$ and $s$
be a stack. Then,
$\toLMR{(\subsapply{\subs{x}{u}}{o})} =
\subsapply{\subs{x}{\toLMR{u}}}{\toLMR{o}}$
and $\toLMR{(\replapply{\repl[\alpha']{\alpha}{s}}{o})} =
\replapply{\repls[\alpha']{\alpha}{\toLMR{s}}}{\toLMR{o}}$.

Let  $o,o' \in \Object{\calcLambdaMuRho}$ and $u,u' \in \Term{\calcLambdaMuRho}$
and $s,s'$ be stacks
such that $o \reduce[\rlmr] o'$, $u \reduce[\rlmr] u'$
and $s \reduce[\rlmr] s'$. Then,

$\subsapply{\subs{x}{u}}{o} \reduce[\rlmr] \subsapply{\subs{x}{u}}{o'}$.

$\subsapply{\subs{x}{u}}{o} \reducemany[\rlmr] \subsapply{\subs{x}{u'}}{o}$.

$\replapply{\repls[\vec{\alpha'}]{\vec{\alpha}}{s}}{o} \reduce[\rlmr]
\replapply{\repls[\vec{\alpha'}]{\vec{\alpha}}{s}}{o'}$.

$\replapply{\repls[\vec{\alpha'}]{\vec{\alpha}}{s}}{o} \reducemany[\rlmr]
\replapply{\repls[\vec{\alpha'}]{\vec{\alpha}}{s'}}{o}$.

Given a stack $s$ in the $\calcLambdaMuRho$-calculus and sequence of
distinct names $\vec{\alpha}$ and $\vec{\alpha}'$ such that
$\fsize{\alpha} = \fsize{\alpha'} = n$, we denote by
$\many{\repl[\alpha'_i]{\alpha_i}{s}}{i \leq n}$
the sequence of single
replacements over each name of the sequence
$\vec{\alpha}$ (in the same order),

Let  $o \in \Object{\calcLambdaMuRho}$, let $s$ be a stack, $\vec{\alpha}$
and $\vec{\alpha}'$  be sequences of distinct names
such that  $\vec{\alpha} \cap
\fn{s} = \emptyset$. Then,
$\replapply{\many{\repl[\alpha'_i]{\alpha_i}{s}}{i \leq \fsize{\vec{\alpha}}}}{o}
\reducemany[\rLM]
\replapply{\repls[\vec{\alpha}']{\vec{\alpha}}{s}}{o}$.

Last, to apply the interpretation method
we need to relate the relations  $\reduce[\rLM]$ and $\reduce[\rlmr]$
by means the projection function  $\toLMR{\_}$.

*  Let  $o \in
\Object{\calcLambdaM}$. Then, $o \reducemany[\rLM] \toLMR{o}$.

*  Let
$o,o' \in \Object{\calcLambdaMuRho}$. If $o \reduce[\rlmr] o'$, then
$o \reducemany[\rLM] o'$.

*  Let
$o,o' \in \Object{\calcLambdaM}$. If   $o \reduce[\rLM] o'$, then
$\toLMR{o} \reducemany[\rlmr] \toLMR{o'}$.

Confluence of $\reduce[\rLM]$ is a consequence of
Lem. <ref> and
confluence of
(Thm. <ref>).

§ THE SIMPLY TYPED -CALCULUS

*  Let
and $\deriv[\pi_{s'}]{\sequM{\Gamma'}{\assign{s'}{S'}}{\Delta'}}[\SysMuEx]$.

Then, there exists

*  Let
Then, there exist
such that $S^{\ast} = \termpush{S}{S'}$, $\Gamma^{\ast} =
\envunion{\Gamma}{\Gamma'}$ and $\Delta^{\ast} = \envunion{\Delta}{\Delta'}$.

*  Let
and $\deriv[\pi_{s}]{\sequM{\Gamma'}{\assign{s}{S}}{\Delta'}}[\SysMuEx]$.

Then, there exists

*  Let
Then, there exist
such that $\Gamma^{\ast} = \envunion{\Gamma}{\Gamma'}$ and $\Delta^{\ast} =
\envunion{\Delta}{\Delta'}$.

and  $\deriv[\pi_{u}]{\sequM{\Gamma'}{\assign{u}{B}}{\Delta'}}[\SysMuEx]$. Then,
there exists
such that $\Gamma^{\ast} \subseteq \envunion{\Gamma}{\Gamma'}$ and $\Delta^{\ast}
\subseteq \envunion{\Delta}{\Delta'}$.

and  $\deriv[\pi_{s}]{\sequM{\Gamma'}{\assign{s}{S}}{\Delta'}}[\SysMuEx]$.

Then, there exists
such that  $\Gamma^{\ast} \subseteq \envunion{\Gamma}{\Gamma'}$ and  $\Delta^{\ast}
\subseteq \envunion{\envunion{\Delta}{\Delta'}}{\assign{\alpha'}{B}}$.

§ TRANSLATION TO PROOF-NETS

Given a typed object $o \in \Object{\calcLambdaM}$ and variables $x$ and $y$,
$\toPPN{(\pi_{o})}[x][y]$ denotes the polarised proof-net which
results from adding a contraction node between the wires $x$ and $y$,
assuming $x,y \in \fv{o}$. If $x \in \fv{o}$ and $y \notin \fv{o}$,
then $\toPPN{(\pi_{o})}[x][y]$ denotes the polarised proof-net that
results from simply replacing all labels $x$ with $y$. Otherwise,
$\toPPN{(\pi_{o})}[x][y] \eqdef \toPPN{(\pi_{o})}$. Similarly for names
$\alpha$ and $\beta$, respectively. Note that given a command $c$, we have
$\toPPN{(\pi_{c})}[\alpha][\beta] =
\toPPN{(\pi_{\termren{\alpha}{\beta}{c}})}$.

Let $o \in \Object{\calcLambdaM}$ be typed. Then
$\toPPN{(\pi_{\subsapply{\subs{x}{y}}{o}})} \eqppn \toPPN{(\pi_{o})}[x][y]$ and
$\toPPN{(\pi_{\renapply{\ren{\alpha}{\beta}}{o}})} \eqppn
\toPPN{(\pi_{o})}[\alpha][\beta]$.

Let $o \in \Object{\calcLambdaM}$ and $u \in \Term{\calcLambdaM}$ be typed such
that $\fv{o} \cap \fv{u} = \emptyset$ and $\fn{o} \cap \fn{u} = \emptyset$.

\[\scaleinput{.8}{proofnets/translation/substitution}\]
reduces to a
PPN structurally equivalent to

Let $o \in \Command{\calcLambdaM}$ and $s\in \Object{\calcLambdaM}$ be typed
with $s$ a stack such that $\fv{o} \cap \fv{s} = \emptyset$ and $\fn{o} \cap
\fn{s} = \emptyset$. Then

\[\scaleinput{.8}{proofnets/translation/replacement}\]
reduces to a PPN
structurally equivalent to

§ STRONG NORMALISATION OF  COMPUTATION

To show that  computation is strongly normalising we define
a measure over objects of the $\calcLambdaM$-calculus. It is worth
noticing that using the size of an object (counting all its
constructors) is not enough since it does not strictly
decrease under computation due to the following remarks:

* Rule $\rM$ discards an application while introducing a new explicit
replacement, thus preserving the number of constructors in the object.

* Rule $\rN$ discards a linear explicit replacement with a stack of $n$
elements, replacing it with $n$ applications. The number of stack
constructors in a stack of $n$ elements turns out to be $n-1$ which, together
with the discarded explicit replacement, compensates the $n$ introduced

* Rule $\rC$ discards a linear explicit replacement by combining it with
another one, appending their respective stacks. This introduces a new stack
constructor, preserving the total number of constructors in the object.

* Rule $\rW$ simply reorders the constructors of the object, pushing
explicit replacements below explicit renamings.

The first remark suggests that the application constructor should have more weight than the
replacement constructor to guarantee normalisation by means of a polynomial interpretation.
However, the second remark suggests exactly the opposite. On another note, the
third remark requires explicit replacements to have more weight than
stacks. The fourth simply suggest that explicit replacements to-the-left of an
explicit renaming should have less weight than those to-the-right.

Under these considerations we define two new measuresthe following  measure over objects of the
$\calcLambdaM$-calculus . First we define a weight function that keeps track
of the names used in the object and the weight of their potential arguments,
and second we define an interpretation of objects into multisets based on
the previous weight function. This interpretation will suffice to prove
strong normalisation for  computation.which turns out to be decreasing w.r.t. reduction $\reduce[\rcan]$.

\[
\begin{array}{c@{\qquad\qquad}c}
\begin{array}{lll}
\cmeas{x}                                 & \eqdef  & 3 \\
\cmeas{\termapp{t}{u}}                    & \eqdef  & \cmeas{t} * \cmeas{u} \\
\cmeas{\termabs{x}{t}}                    & \eqdef  & \cmeas{t} \\
\cmeas{\termcont{\alpha}{c}}              & \eqdef  & \cmeas{c} + 1 \\
\cmeas{\termsubs{x}{u}{t}}                & \eqdef  & \cmeas{t} + \cmeas{u}
\end{array}
\begin{array}{lll}
\cmeas{\termname{\alpha}{t}}              & \eqdef  & \cmeas{t}  \\
\cmeas{\termrepl[\alpha']{\alpha}{s}{c}}  & \eqdef  & \cmeas{c} * \cmeas{s} + 1 \\
\cmeas{\termren{\alpha}{\beta}{c}}        & \eqdef  & \cmeas{c} + 1 \\
\\
\cmeas{\termpush{t}{s}}                   & \eqdef  & \cmeas{t} * \cmeas{u}
\end{array}
\end{array}
\]

Notice that $\cmeas{o} \geq 3$ for every $o \in \Object{\calcLambdaM}$.
We also have $\cmeas{o} + \cmeas{o'} < \cmeas{o} * \cmeas{o'}$. The measure
$\cmeas{\_}$ can be extended to contexts as follows:
\[
\begin{array}{c@{\qquad\qquad}c}
\begin{array}{lll}
\cmeas{\Box}                                    & \eqdef  & 0 \\
\cmeas{\termapp{\ctxt{T}}{t}}                   & \eqdef  & \cmeas{\ctxt{T}} * \cmeas{t} \\
\cmeas{\termapp{t}{\ctxt{T}}}                   & \eqdef  & \cmeas{\ctxt{T}} * \cmeas{t} \\
\cmeas{\termabs{x}{\ctxt{T}}}                   & \eqdef  & \cmeas{\ctxt{T}} \\
\cmeas{\termcont{\alpha}{\ctxt{C}}}             & \eqdef  & \cmeas{\ctxt{C}} + 1 \\
\cmeas{\termsubs{x}{t}{\ctxt{T}}}               & \eqdef  & \cmeas{\ctxt{T}} + \cmeas{t} \\
\cmeas{\termsubs{x}{\ctxt{T}}{t}}               & \eqdef  & \cmeas{\ctxt{T}} + \cmeas{t}
\end{array}
\begin{array}{lll}
\cmeas{\boxdot}                                 & \eqdef  & 0 \\
\cmeas{\termname{\alpha}{\ctxt{T}}}             & \eqdef  & \cmeas{\ctxt{T}} \\
\cmeas{\termrepl[\alpha']{\alpha}{s}{\ctxt{C}}} & \eqdef  & \cmeas{\ctxt{C}} * \cmeas{s} + 1 \\
\cmeas{\termrepl[\alpha']{\alpha}{\ctxt{S}}{c}} & \eqdef  & \cmeas{c} * \cmeas{\ctxt{S}} + 1 \\
\cmeas{\termren{\alpha}{\beta}{\ctxt{C}}}       & \eqdef  & \cmeas{\ctxt{C}} + 1 \\
\cmeas{\termpush{\ctxt{T}}{s}}                  & \eqdef  & \cmeas{\ctxt{T}} * \cmeas{s} + 1 \\
\cmeas{\termpush{t}{\ctxt{S}}}                  & \eqdef  & \cmeas{t} * \cmeas{\ctxt{S}} + 1
\end{array}
\end{array}
\]

For every $\ctxt{O}$, there is $f_{\ctxt{O}}: x \mapsto a * x + b$ with $a > 0$
and $b \geq 0$, such that for every $o$, one has
$\cmeas{\ctxtapply{\ctxt{O}}{o}} = f_{\ctxt{O}}(\cmeas{o})$.

By induction on $\ctxt{O}$.

* For $\ctxt{O}=\Box$ and  $\ctxt{O}=\boxdot$ we take $f_{\ctxt{O}}(x) = 1 * x + 0$.

* For $\ctxt{O}=\termsubs{x}{t}{\ctxt{T}}$
and $\ctxt{O}=\termsubs{x}{\ctxt{T}}{t}$, we take $f_{\ctxt{O}}(x) = a' * x + (b'+\cmeas{t})$,  where $f_{\ctxt{T}}(x) = a' * x + b'$.

* For $\ctxt{O}=\termapp{\ctxt{T}}{t}$
and $\ctxt{O}=\termapp{t}{\ctxt{T}}$ we take
$f_{\ctxt{O}}(x) = (a' *\cmeas{t})* x + (b'*\cmeas{t})$, where $f_{\ctxt{T}}(x) = a' * x + b'$.

* For $\ctxt{O}=\termabs{x}{\ctxt{T}}$
and $\ctxt{O}=\termname{\alpha}{\ctxt{T}}$ we take $f_{\ctxt{O}}(x) = a'* x + b'$, where $f_{\ctxt{T}}(x) = a' * x + b'$.

* For $\ctxt{O}=\termcont{\alpha}{\ctxt{C}}$ we take $f_{\ctxt{O}}(x) = a'* x + (b'+1)$, where $f_{\ctxt{C}}(x) = a' * x + b'$.

* For $\ctxt{O}=\termrepl[\alpha']{\alpha}{s}{\ctxt{C}}$ we take $f_{\ctxt{O}}(x) = (a' * \cmeas{s})*x + (b'*\cmeas{s}+1)$, where $f_{\ctxt{C}}(x) = a' * x + b'$.

* For $\ctxt{O}=\termrepl[\alpha']{\alpha}{\ctxt{S}}{c}$ we take $f_{\ctxt{O}}(x) = (a' * \cmeas{c})*x + (b'*\cmeas{c}+1)$, where $f_{\ctxt{S}}(x) = a' * x + b'$.

* For $\ctxt{O}=\termpush{\ctxt{T}}{s}$ we take $f_{\ctxt{O}}(x) = (a' * \cmeas{s})*x + (b'*\cmeas{s}+1)$, where $f_{\ctxt{T}}(x) = a' * x + b'$.

* For $\ctxt{O}=\termpush{t}{\ctxt{S}}$ we take $f_{\ctxt{O}}(x) = (a'*\cmeas{t})*x + (b'*\cmeas{t}+1)$, where $f_{\ctxt{S}}(x) = a' * x + b'$.

* For $\ctxt{O}=\termren{\alpha}{\beta}{\ctxt{C}}$ we take $f_{\ctxt{O}}(x) = a'*x +(b'+1)$, where $f_{\ctxt{C}}(x) = a' * x + b'$.

Let $o \in \Object{\calcLambdaM}$. If
$\deriv[\pi]{\sequM{\Gamma}{\assign{o}{T}}{\Delta}}[\SysMuEx]$ and0 $o
\reduce[\rcan] o'$, then there exists

Let $o \in \Object{\calcLambdaM}$. If
$\deriv[\pi]{\sequM{\Gamma}{\assign{o}{T}}{\Delta}}[\SysMuEx]$ y $o'
\reduce[\rcan] o$, then there exists

§ STRUCTURAL EQUIVALENCE FOR THE -CALCULUS

To prove Lem. <ref> we introduce two auxiliary
results about contexts $\ctxt{LTT}$ and $\ctxt{LCC}$.

Let $\edu{u,v} \in \Term{\calcLambdaM}$ and consider the following relation:

\[
\edu{
\S \eqdef
\set{\pair{u}{v}
\mid \exists \ctxt{L}. \exists\ctxt{LTT}. \exists t. u=\ctxtapply{\ctxt{L}}{\ctxtapply{\ctxt{LTT}}{t}}\mbox{ and }v=\ctxtapply{\ctxt{LTT}}{\ctxtapply{\ctxt{L}}{t}}\mbox{ and }\bv{\ctxt{L}} \notin \ctxt{LTT}\mbox{ and }\fc{\ctxt{L}}{\ctxt{LTT}}}
\]

Then $\S$ is a strong bisimulation w.r.t. the  computation relation.

Let $\edu{d,e} \in \Command{\calcLambdaM}$ and consider the following relation

\[
\edu{\R \eqdef
\set{\pair{d}{e}
\mid \exists \ctxt{R},\ctxt{LCC},c. d=\ctxtapply{\ctxt{R}}{\ctxtapply{\ctxt{LCC}}{c}}\mbox{ and }e=\ctxtapply{\ctxt{LCC}}{\ctxtapply{\ctxt{R}}{c}}\mbox{ and }\bn{\ctxt{R}} \notin \ctxt{LCC}\mbox{ and }\fc{\ctxt{R}}{\ctxt{LCC}}}
\]

Then $\R$ is a strong bisimulation w.r.t. the   computation relation.

§ STRONG BISIMULATION RESULT

Let $o,o' \in \Object{\calcLambdaM}$ such that $o \eqsigma[\ast] o'$ with
$\eqsigma[\ast]$ any rule from Fig. <ref>. If $o =
\ctxtapply{\ctxt{LXC}}{c}$ for some $\ctxt{LXC}$ and some $c$,  with $\ctxt{X} \in \set{\ctxt{T},
\ctxt{C}}$, $\alpha \notin \ctxt{LXC}$,
$\fc{\alpha'}{\ctxt{LXC}}$ and $\fc{s}{\ctxt{LXC}}$, then there exist $\ctxt{LXC}'$ and $c'$ such that  $o' =
\ctxtapply{\ctxt{LXC}'}{c'}$ such thatwith $\alpha \notin \ctxt{LXC}'$,
$\fc{\alpha'}{\ctxt{LXC}'}$, $\fc{s}{\ctxt{LXC}'}$ and
$\fcan{\ctxtapply{\ctxt{LXC}}{\termrepl[\alpha']{\alpha}{s}{c}}} \eqsigma
\fcan{\ctxtapply{\ctxt{LXC}'}{\termrepl[\alpha']{\alpha}{s}{c'}}}$.

Let $o, o' \in \Object{\calcLambdaM}$ such that $o \eqsigma o'$.

*  If $o, o' \in
\Term{\calcLambdaM}$, then $\fcan{\termconc{o}{s}} \eqsigma
\fcan{\termconc{o'}{s}}$.

*  If $o, o' \in
\Command{\calcLambdaM}$, then $\fcan{\termrepl[\alpha']{\alpha}{s}{o}}
\eqsigma \fcan{\termrepl[\alpha']{\alpha}{s}{o'}}$.

Let $o, o' \in \Object{\calcLambdaM}$ and $u, u' \in
\Term{\calcLambdaM}$ such that $o \eqsigma o'$ and $u \eqsigma u'$.

*  Then,
$\fcan{\subsapply{\subs{x}{u}}{o}} \eqsigma
\fcan{\subsapply{\subs{x}{u}}{o'}}$.

*  Then,
$\fcan{\subsapply{\subs{x}{u}}{o}} \eqsigma
\fcan{\subsapply{\subs{x}{u'}}{o}}$.

Let $o, o', s, s' \in \Object{\calcLambdaM}$ with $s$ and $s'$ stacks such that
$o\eqsigma o'$ and  $s \eqsigma s'$.

*  Then,
$\fcan{\replapply{\repl[\alpha']{\alpha}{s}}{o}} \eqsigma
\fcan{\replapply{\repl[\alpha']{\alpha}{s}}{o'}}$.

*  Then,
$\fcan{\replapply{\repl[\alpha']{\alpha}{s}}{o}} \eqsigma
\fcan{\replapply{\repl[\alpha']{\alpha}{s'}}{o}}$.

§ TWO CORRESPONDENCE RESULTS

To show soundness of  $\eqlaurent$ w.r.t. $\eqsigmaren$, it is
necessary to previously stage a list of auxiliary results.

Let $o,o' \in \Object{\calcLambdaM}$ such that $o \eqsigma[\ast] o'$, where
$\eqsigma[\ast]$ is an axiom in Fig. <ref> or
axiom $\ruleEqsigRen$. If $o = \ctxtapply{\ctxt{LXC}}{c}$ with $\ctxt{X} \in
\set{\ctxt{T}, \ctxt{C}}$, $\alpha \notin \ctxt{LXC}$,
$\fc{\alpha'}{\ctxt{LXC}}$ and
$\fc{s}{\ctxt{LXC}}$, then $o' = \ctxtapply{\ctxt{LXC}'}{c'}$ such
that $\alpha \notin \ctxt{LXC}'$, $\fc{\alpha'}{\ctxt{LXC}'}$,
$\fc{s}{\ctxt{LXC}'}$ and
\eqsigmaren
\fcan{\ctxtapply{\ctxt{LXC}'}{\termrepl[\alpha']{\alpha}{s}{c'}}}$.

Let $o, o' \in \Object{\calcLambdaM}$ such that $o \eqsigmaren o'$.

*  If  $o, o' \in
\Term{\calcLambdaM}$, then  $\fcan{\termconc{o}{s}} \eqsigmaren
\fcan{\termconc{o'}{s}}$.

*  If  $o, o' \in
\Command{\calcLambdaM}$, then  $\fcan{\termrepl[\alpha']{\alpha}{s}{o}}
\eqsigmaren \fcan{\termrepl[\alpha']{\alpha}{s}{o'}}$.

Let $o \in \Object{\calcLambdaM}$. If $o \eqsigmaren o'$, then for
all context $\ctxt{O}$ of appropriate sort we have
$\fcan{\ctxtapply{\ctxt{O}}{o}} \eqsigmaren
\fcan{\ctxtapply{\ctxt{O}}{o'}}$.

Despite the fact that $\toPPNMnf{\_}$ was defined for a type derivation $\pi$
(Def. <ref>), we may use in what follows a
slight abuse of notation by writing $\toPPNMnf{R}$, instead of
$\toPPNMnf{\pi}$, where $R$ is the proof-net obtained by first computing

Let $t \in \Term{\calcLambdaM}$ and $s \in \Object{\calcLambdaM}$ be a stack.
Consider typing derivations  $\pi_{t}$ and $\pi_{s}$
assigning types
$\typeabs{S}{B}$ and $S$ respectively. Then  $\toPPNMnf{(\pi_{t})} \eqppn
\toPPNMnf{(\pi_{\fexp{t}})}$ and $\toPPNMnf[B]{(\pi_{s})} \eqppn
\toPPNMnf[B]{(\pi_{\fexp{s}})}$ imply  $\toPPNMnf{(\pi_{\termconc{t}{s}})}
\eqppn \toPPNMnf{(\pi_{\fexp{\termconc{t}{s}}})}$.