We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

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

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.
Comments: arXiv admin note: text overlap with arXiv:1906.09370
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2101.05754 [cs.LO]
  (or arXiv:2101.05754v2 [cs.LO] for this version)

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.