A STRONG BISIMULATION FOR A CLASSICAL TERM CALCULUS

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.