TY - JOUR
T1 - A STRONG BISIMULATION FOR A CLASSICAL TERM CALCULUS
AU - Bonelli, Eduardo
AU - Kesner, Delia
AU - Viso, Andrés
N1 - Publisher Copyright:
© E. Bonelli, D. Kesner, and A. Viso ⃝CC Creative Commons.
PY - 2024
Y1 - 2024
N2 - When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of λ-calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on λ-terms known as ≃σ-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 ≃σ-equivalence, as formulated by Laurent for Parigot’s λµ-calculus. This is achieved by introducing a relation ≃, defined over a revised presentation of λµ-calculus we dub ΛM. More precisely, we first identify the reasons behind Laurent’s ≃σ-equivalence on λµ-terms 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 enrich the syntax of λµ 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 ΛM and a relation ≃ that we show to be a strong bisimulation with respect to reduction in ΛM, i.e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s ≃σ-equivalence in λ-calculus as well as for Laurent’s ≃σ-equivalence in λµ. Although ≃ is formulated over an enriched syntax and hence is not strictly included in Laurent’s ≃σ, we show how it can be seen as a restriction of it.
AB - When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of λ-calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on λ-terms known as ≃σ-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 ≃σ-equivalence, as formulated by Laurent for Parigot’s λµ-calculus. This is achieved by introducing a relation ≃, defined over a revised presentation of λµ-calculus we dub ΛM. More precisely, we first identify the reasons behind Laurent’s ≃σ-equivalence on λµ-terms 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 enrich the syntax of λµ 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 ΛM and a relation ≃ that we show to be a strong bisimulation with respect to reduction in ΛM, i.e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s ≃σ-equivalence in λ-calculus as well as for Laurent’s ≃σ-equivalence in λµ. Although ≃ is formulated over an enriched syntax and hence is not strictly included in Laurent’s ≃σ, we show how it can be seen as a restriction of it.
UR - http://www.scopus.com/inward/record.url?scp=85192151253&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85192151253&partnerID=8YFLogxK
U2 - 10.46298/lmcs-20(2:4)2024
DO - 10.46298/lmcs-20(2:4)2024
M3 - Article
AN - SCOPUS:85192151253
VL - 20
SP - 4:1-4:52
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
IS - 2
ER -