摘要：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 âf, defined over a revised presentation of Parigotâs λμ-calculus we dub Î>M. Our result builds on two fundamental ingredients: (1) factorization of λμ-reduction into multiplicative and exponential steps by means of explicit term operators of Î>M, and (2) translation of Î>M-terms into Laurentâs polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation âf is shown to characterize structural equivalence in PPN. Most notably, âf is shown to be a strong bisimulation with respect to reduction in Î>M, i.e. two âf-equivalent terms have the exact same reduction semantics, a result which fails for Regnierâs Ïf-equivalence in λ-calculus as well as for Laurentâs Ïf-equivalence in λμ.
