### References & Citations

# Computer Science > Logic in Computer Science

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

(Submitted on 14 Jan 2021 (v1), last revised 5 Sep 2021 (this version, v2))

Abstract: 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.

## Submission history

From: Andrés Ezequiel Viso [view email]**[v1]**Thu, 14 Jan 2021 17:54:22 GMT (169kb)

**[v2]**Sun, 5 Sep 2021 13:32:59 GMT (14413kb,D)

Link back to: arXiv, form interface, contact.