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的≃σ中，但我们展示了如何将其视为≃σ的一种限制。