Strong Bisimulation for Control Operators

TL;DR

This paper introduces a strong bisimulation relation for control operators in the lambda-mu calculus, ensuring exact correspondence in reduction semantics through a novel relation and translation to proof-nets.

Contribution

It defines a new relation $$ that characterizes structural equivalence and acts as a strong bisimulation, improving understanding of control operators' semantics.

Findings

$$ characterizes structural equivalence in polarized proof-nets.

$$ is a strong bisimulation for $$-equivalent terms.

The relation ensures exact reduction semantics correspondence.

Abstract

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