Normal Form Bisimulations By Value

TL;DR

This paper introduces net bisimilarity, a new call-by-value normal form bisimilarity that better aligns with certain principles and addresses limitations of previous bisimilarities, enriching the understanding of program equivalence.

Contribution

The paper develops net bisimilarity, a novel call-by-value normal form bisimilarity that satisfies additional principles and differs from existing bisimilarities, enhancing the theoretical framework.

Findings

Net bisimilarity is incomparable with enf bisimilarity.

Net bisimilarity does not validate Moggi's laws nor η.

Analysis relates various call-by-value bisimilarities to Ehrhard's relational model.

Abstract

Normal form bisimilarities are a natural form of program equivalence resting on open terms, first introduced by Sangiorgi in call-by-name. The literature contains a normal form bisimilarity for Plotkin's call-by-value $\lambda$-calculus, Lassen's \emph{enf bisimilarity}, which validates all of Moggi's monadic laws and can be extended to validate $\eta$. It does not validate, however, other relevant principles, such as the identification of meaningless terms -- validated instead by Sangiorgi's bisimilarity -- or the commutation of $\letexp$s. These shortcomings are due to issues with open terms of Plotkin's calculus. We introduce a new call-by-value normal form bisimilarity, deemed \emph{net bisimilarity}, closer in spirit to Sangiorgi's and satisfying the additional principles. We develop it on top of an existing formalism designed for dealing with open terms in call-by-value. It turns out that enf and net bisimilarities are \emph{incomparable}, as net bisimilarity does not validate Moggi's laws nor $\eta$. Moreover, there is no easy way to merge them. To better understand the situation, we provide an analysis of the rich range of possible call-by-value normal form bisimilarities, relating them to Ehrhard's relational model.