Normal Form Bisimulations for Delimited-Control Operators

TL;DR

This paper introduces a simple behavioral equivalence called normal form bisimilarity for the lambda calculus with shift and reset, providing a practical tool for reasoning about program equivalence without exhaustive context testing.

Contribution

It defines and proves properties of normal form bisimilarity for shift and reset, including soundness and techniques to simplify bisimulation proofs.

Findings

Normal form bisimilarity is sound but not complete w.r.t. contextual equivalence.

Up-to techniques significantly simplify bisimulation proofs.

Several term equivalences are demonstrated using the developed techniques.

Abstract

We define a notion of normal form bisimilarity for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. Normal form bisimilarities are simple, easy-to-use behavioral equivalences which relate terms without having to test them within all contexts (like contextual equivalence), or by applying them to function arguments (like applicative bisimilarity). We prove that the normal form bisimilarity for shift and reset is sound but not complete w.r.t. contextual equivalence and we define up-to techniques that aim at simplifying bisimulation proofs. Finally, we illustrate the simplicity of the techniques we develop by proving several equivalences on terms.