Program Equivalence in Linear Contexts

TL;DR

This paper introduces linear contextual equivalence for programs in linear contexts, providing a sound and complete method based on labeled transition systems, applicable to both deterministic and non-deterministic higher-order functional languages.

Contribution

It proposes a formal notion of linear contextual equivalence and a general approach using labeled transition systems, addressing limitations of previous techniques in linear and non-deterministic settings.

Findings

Linear contextual equivalence coincides with trace equivalence.

The approach is sound and complete for both deterministic and non-deterministic linear languages.

Technique is demonstrated on linear PCF and its non-deterministic extension.

Abstract

Program equivalence in linear contexts, where programs are used or executed exactly once, is an important issue in programming languages. However, existing techniques like those based on bisimulations and logical relations only target at contextual equivalence in the usual (non-linear) functional languages, and fail in capturing non-trivial equivalent programs in linear contexts, particularly when non-determinism is present. We propose the notion of linear contextual equivalence to formally characterize such program equivalence, as well as a novel and general approach to studying it in higher-order languages, based on labeled transition systems specifically designed for functional languages. We show that linear contextual equivalence indeed coincides with trace equivalence - it is sound and complete. We illustrate our technique in both deterministic (a linear version of PCF) and non-deterministic (linear PCF in Moggi's framework) functional languages.