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$-演算转换为证明网的案例中，这些非本质细节由$\lambda$-项上的一种等价关系$\simeq_\sigma$所捕获——该关系在直觉主义情形（源于Regnier）和经典情形（源于Laurent）中均成立。本文旨在揭示Laurent针对Parigot的$\lambda\mu$-演算所表述的$\simeq_\sigma$-等价背后隐藏的强互模拟结构。这通过引入定义于我们称之为$\Lambda M$的$\lambda\mu$-演算修订表示上的关系$\simeq$实现。具体而言，我们首先识别了Laurent的$\lambda\mu$-项上的$\simeq_\sigma$-等价未能成为强互模拟的原因。受Laurent的《极化证明网》启发，这促使我们区分项上的乘法归约步与指数归约步。其次，我们丰富$\lambda\mu$的语法以追踪指数运算。这些技术要素为经典情形下的强互模拟铺平了道路。我们引入演算$\Lambda M$和关系$\simeq$，并证明$\simeq$关于$\Lambda M$中的归约构成强互模拟——即两个$\simeq$-等价的项具有完全相同的归约语义，该结论对于Regnier在$\lambda$-演算中的$\simeq_\sigma$-等价以及Laurent在$\lambda\mu$-演算中的$\simeq_\sigma$-等价均不成立。尽管$\simeq$基于扩展语法构建，因而并非严格包含于Laurent的$\simeq_\sigma$中，但我们展示它可被视为后者的一个限制形式。