# 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.

## Key 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$.

---
Source: https://tomesphere.com/paper/1906.09370