{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:22Z","timestamp":1753894402355,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>When translating a term calculus into a graphical formalism many inessential\ndetails are abstracted away. In the case of $\\lambda$-calculus translated to\nproof-nets, these inessential details are captured by a notion of equivalence\non $\\lambda$-terms known as $\\simeq_\\sigma$-equivalence, in both the\nintuitionistic (due to Regnier) and classical (due to Laurent) cases. The\npurpose of this paper is to uncover a strong bisimulation behind\n$\\simeq_\\sigma$-equivalence, as formulated by Laurent for Parigot's\n$\\lambda\\mu$-calculus. This is achieved by introducing a relation $\\simeq$,\ndefined over a revised presentation of $\\lambda\\mu$-calculus we dub $\\Lambda\nM$.\n  More precisely, we first identify the reasons behind Laurent's\n$\\simeq_\\sigma$-equivalence on $\\lambda\\mu$-terms failing to be a strong\nbisimulation. Inspired by Laurent's \\emph{Polarized Proof-Nets}, this leads us\nto distinguish multiplicative and exponential reduction steps on terms. Second,\nwe enrich the syntax of $\\lambda\\mu$ to allow us to track the exponential\noperations. These technical ingredients pave the way towards a strong\nbisimulation for the classical case. We introduce a calculus $\\Lambda M$ and a\nrelation $\\simeq$ that we show to be a strong bisimulation with respect to\nreduction in $\\Lambda M$, ie. two $\\simeq$-equivalent terms have the exact same\nreduction semantics, a result which fails for Regnier's\n$\\simeq_\\sigma$-equivalence in $\\lambda$-calculus as well as for Laurent's\n$\\simeq_\\sigma$-equivalence in $\\lambda\\mu$. Although $\\simeq$ is formulated\nover an enriched syntax and hence is not strictly included in Laurent's\n$\\simeq_\\sigma$, we show how it can be seen as a restriction of it.<\/jats:p>","DOI":"10.46298\/lmcs-20(2:4)2024","type":"journal-article","created":{"date-parts":[[2024,4,18]],"date-time":"2024-04-18T14:45:09Z","timestamp":1713451509000},"source":"Crossref","is-referenced-by-count":0,"title":["A Strong Bisimulation for a Classical Term Calculus"],"prefix":"10.46298","volume":"Volume 20, Issue 2","author":[{"given":"Eduardo","family":"Bonelli","sequence":"first","affiliation":[]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[]},{"given":"Andr\u00e9s","family":"Viso","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,4,18]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13433\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13433\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,18]],"date-time":"2024-04-18T14:45:09Z","timestamp":1713451509000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7089"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,18]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(2:4)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2101.05754v4","asserted-by":"subject"},{"id-type":"arxiv","id":"2101.05754v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2101.05754v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2101.05754v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2101.05754","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2101.05754","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,4,18]]},"article-number":"7089"}}