A Strong Bisimulation for a Classical Term Calculus

TL;DR

The paper tackles the challenge of identifying a strong, bisimulation-preserving structural equivalence for classical lambda-calculus with control by refining Parigot's lm-calculus into an LM-calculus with explicit substitutions and explicit replacements. It decomposes reduction into multiplicative and exponential components (dB/dM, N/C, and their non-linear variants) to reveal a plain-forms-based strong bisimulation ⪰ that preserves reduction semantics on LM plain forms. A precise correspondence with Laurent's σ-equivalence on lm-terms is established via expansion and projection mechanisms, clarifying how classical and intuitionistic notions align under a refined framework. These results pave the way for robust program equivalence reasoning in classical calculi and have potential applications to abstract machines and optimization by exposing which permutations are semantically inert. The work also opens avenues for further normalisation, confluence analyses, and connections to proof-nets and polarized formalisms.

Abstract

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 $\simeq_σ$-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_σ$-equivalence, as formulated by Laurent for Parigot's $λμ$-calculus. This is achieved by introducing a relation $\simeq$, defined over a revised presentation of $λμ$-calculus we dub $ΛM$. More precisely, we first identify the reasons behind Laurent's $\simeq_σ$-equivalence on $λμ$-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 $λμ$ 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 $\simeq$ that we show to be a strong bisimulation with respect to reduction in $ΛM$, ie. two $\simeq$-equivalent terms have the exact same reduction semantics, a result which fails for Regnier's $\simeq_σ$-equivalence in $λ$-calculus as well as for Laurent's $\simeq_σ$-equivalence in $λμ$. Although $\simeq$ is formulated over an enriched syntax and hence is not strictly included in Laurent's $\simeq_σ$, we show how it can be seen as a restriction of it.

Figures (6)

• Figure 1: $\sigma$-Equivalence for $\lambda$-terms
• Figure 2: Strong Bisimulation $\simeq_{\tilde{\sigma}_{}}$ for $\lambda$-Terms
• Figure 3: $sigma$-equivalence for $lm$-objects
• Figure 4: $\tilde{\sigma}$-equivalence on $LM$-objects.
• Figure 5: Structural equivalence $\simeq_{}$ on $LM$-objects.

Theorems & Definitions (72)

• Theorem 1.1: Strong Bisimulation for the Intuitionistic Case I
• Theorem 1.2: Strong Bisimulation for the Intuitionistic Case II
• Definition 3.1
• Definition 4.1
• Lemma 4.2
• proof
• Theorem 4.3
• proof
• Definition 5.1
• Theorem 5.2