References & Citations
Computer Science > Logic in Computer Science
Title: A Strong Bisimulation for a Classical Term Calculus
(Submitted on 14 Jan 2021 (v1), last revised 17 Apr 2024 (this version, v6))
Abstract: 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.
Submission history
From: Delia Kesner [view email] [via LOGICAL proxy][v1] Thu, 14 Jan 2021 17:54:22 GMT (169kb)
[v2] Sun, 5 Sep 2021 13:32:59 GMT (14413kb,D)
[v3] Thu, 2 Feb 2023 19:30:35 GMT (202kb)
[v4] Fri, 16 Jun 2023 15:09:59 GMT (982kb)
[v5] Wed, 14 Feb 2024 08:00:36 GMT (95kb,D)
[v6] Wed, 17 Apr 2024 09:25:18 GMT (97kb,D)
Link back to: arXiv, form interface, contact.