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.

翻译：将项演算转化为图形形式时，许多非本质细节被抽象化。在将λ-演算转化为证明网的情况下，这些非本质细节被λ-项上称为≃σ-等价关系的等价概念所捕获，无论是在直觉主义情形（由Regnier提出）还是经典情形（由Laurent提出）中均如此。本文旨在揭示Laurent为Parigot的λμ-演算所定义的≃σ-等价关系背后的强互模拟结构。这通过引入一个关系≃来实现，该关系定义在我们称为ΛM的λμ-演算修订表示上。更具体地，我们首先识别出导致Laurent的λμ-项上≃σ-等价关系未能成为强互模拟的原因。受Laurent的极化证明网启发，我们区分了项上的乘法归约步与指数归约步。其次，我们丰富了λμ的语法以允许追踪指数运算。这些技术要素为经典情形下的强互模拟奠定了基础。我们引入了演算ΛM及关系≃，并证明该关系关于ΛM中的归约是强互模拟的，即两个≃-等价的项具有完全相同的归约语义——这一结论在Regnier的λ-演算≃σ-等价性及Laurent的λμ≃σ-等价性中均不成立。尽管≃基于扩展语法定义，因此并未严格包含于Laurent的≃σ中，但我们展示了它如何被视为后者的一种限制。