A Strong Bisimulation for a Classical Term Calculus by Means of Multiplicative and Exponential Reduction

It is well-known that when translating terms into graphical formalisms many innessential details are abstracted away. In the case of $\lambda$-calculus and proof-nets, these innessential 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 failing to be a strong bisimulation. Inspired by Laurent's Polarized Proof-Nets, this leads us to distinguish multiplicative and exponential reduction steps on terms. Second, we provide an enriched syntax that allows to keep track of the renaming operation. These technical ingredients are crucial to pave the way towards a strong bisimulation for the classical case. We thus introduce a calculus $\Lambda M$ and a relation $\simeq$ that we show to be a strong bisimulation with respect to reduction in $\Lambda M$, i.e. 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$. We also show that two $\simeq$-equivalent terms translate to equivalent Polarized Proof-Nets. Although $\simeq$ is not strictly included in Laurent's $\simeq_\sigma$, it can be seen as a restriction of it.