Nothing Special   »   [go: up one dir, main page]

Eduardo Bonelli ; Delia Kesner ; Andrés Viso - A Strong Bisimulation for a Classical Term Calculuslmcs:7089 - Logical Methods in Computer Science, April 18, 2024, Volume 20, Issue 2 - https://doi.org/10.46298/lmcs-20(2:4)2024
A Strong Bisimulation for a Classical Term CalculusArticle

Authors: Eduardo Bonelli ; Delia Kesner ; Andrés Viso

    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.


    Volume: Volume 20, Issue 2
    Published on: April 18, 2024
    Accepted on: February 8, 2024
    Submitted on: January 15, 2021
    Keywords: Computer Science - Logic in Computer Science

    Classifications

    Mathematics Subject Classification 20201

    Consultation statistics

    This page has been seen 1570 times.
    This article's PDF has been downloaded 446 times.