We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

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

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 three main ingredients which guide our semantical development: (1) factorization of Parigot's $\lambda\mu$-reduction into multiplicative and exponential steps by means of explicit operators, (2) adaptation of Laurent's original $\simeq_\sigma$-equivalence to $\Lambda M$, and (3) interpretation of $\Lambda M$ into Laurent's polarized proof-nets (PPN). More precisely, we first give a translation of $\Lambda 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 $\simeq$ and Laurent's $\simeq_\sigma$-equivalence for $\lambda\mu$-terms. Moreover, $\simeq$-equivalent terms translate to structurally equivalent 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 $\simeq_\sigma$-equivalence in $\lambda$-calculus as well as for Laurent's $\simeq_\sigma$-equivalence in $\lambda\mu$.
Comments: arXiv admin note: text overlap with arXiv:1906.09370
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2101.05754 [cs.LO]
  (or arXiv:2101.05754v1 [cs.LO] for this version)

Submission history

From: Andrés Ezequiel Viso [view email]
[v1] Thu, 14 Jan 2021 17:54:22 GMT (169kb)
[v2] Sun, 5 Sep 2021 13:32:59 GMT (14413kb,D)

Link back to: arXiv, form interface, contact.