When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of $\lambda$-calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on $\lambda$-terms known as $\simeq_\sigma$-equivalence, in both the intuitionistic (due to Regnier) and classical (due to Laurent) cases. The purpose of this paper is to uncover a strong bisimulation behind $\simeq_\sigma$-equivalence, as formulated by Laurent for Parigot's $\lambda\mu$-calculus. This is achieved by introducing a relation $\simeq$, defined over a revised presentation of $\lambda\mu$-calculus we dub $\Lambda M$. More precisely, we first identify the reasons behind Laurent's $\simeq_\sigma$-equivalence on $\lambda\mu$-terms failing to be a strong bisimulation. Inspired by Laurent's \emph{Polarized Proof-Nets}, this leads us to distinguish multiplicative and exponential reduction steps on terms. Second, we enrich the syntax of $\lambda\mu$ to allow us to track the exponential operations. These technical ingredients pave the way towards a strong bisimulation for the classical case. We introduce a calculus $\Lambda M$ and a relation $\simeq$ that we show to be a strong bisimulation with respect to reduction in $\Lambda M$, ie. two $\simeq$-equivalent terms have the exact same reduction semantics, a result which fails for Regnier's $\simeq_\sigma$-equivalence in $\lambda$-calculus as well as for Laurent's $\simeq_\sigma$-equivalence in $\lambda\mu$. Although $\simeq$ is formulated over an enriched syntax and hence is not strictly included in Laurent's $\simeq_\sigma$, we show how it can be seen as a restriction of it.

翻译：将项演算转换为图形形式时，许多非本质细节被抽象化。在$\lambda$-演算转换为证明网的情况下，无论是直觉主义情形（归因于Regnier）还是经典情形（归因于Laurent），这些非本质细节均由$\lambda$-项上的等价概念——即$\simeq_\sigma$-等价——所刻画。本文旨在揭示Laurent针对Parigot的$\lambda\mu$-演算所阐述的$\simeq_\sigma$-等价背后隐藏的强互模拟关系。为此，我们引入关系$\simeq$，该关系定义于我们称为$\Lambda M$的$\lambda\mu$-演算修正表示之上。更具体地，我们首先识别导致Laurent的$\lambda\mu$-项$\simeq_\sigma$-等价未能成为强互模拟的原因。受Laurent的《极化证明网》启发，这促使我们区分项上的乘性规约步与指数规约步。其次，我们丰富$\lambda\mu$的语法以追踪指数运算。这些技术要素为经典情形建立强互模拟铺平了道路。我们引入演算$\Lambda M$和关系$\simeq$，并证明该关系在$\Lambda M$规约下构成强互模拟，即两个$\simeq$-等价的项具有完全相同的规约语义——这一结果在$\lambda$-演算的Regnier $\simeq_\sigma$-等价与$\lambda\mu$的Laurent $\simeq_\sigma$-等价中均不成立。尽管$\simeq$基于扩充语法定义因而未被严格包含于Laurent的$\simeq_\sigma$中，但我们展示了如何将其视作后者的限制。