A Strong Bisimulation for Control Operators by Means of Multiplicative and Exponential Reduction

The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation ≃, defined over a revised presentation of Parigot’s λμ-calculus we dub ΛM . Our result builds on three main ingredients which guide our semantical development: (1) factorization of Parigot’s λμ-reduction into multiplicative and exponential steps by means of explicit operators, (2) adaptation of Laurent’s original ≃σ-equivalence to ΛM , and (3) interpretation of ΛM into Laurent’s polarized proof-nets (PPN). More precisely, we first give a translation of ΛM -terms into PPN which simulates the reduction relation of our calculus via cut elimination of PPN. Second, we establish a precise correspondence between our relation ≃ and Laurent’s ≃σ -equivalence for λμ-terms. Moreover, ≃-equivalent terms translate to structurally equivalent PPN. Most notably, ≃ is shown 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 λμ.