A categorical framework for congruence of applicative bisimilarity in higher-order languages

TL;DR

This paper introduces a categorical framework for operational semantics that guarantees applicative bisimilarity is a congruence across various higher-order languages, extending Howe's results.

Contribution

It provides a general categorical approach ensuring applicative bisimilarity is a congruence for languages fitting Howe's format, unifying multiple language semantics.

Findings

Applicative bisimilarity is automatically a congruence in the proposed framework.

The framework applies to call-by-name, call-by-value, and non-deterministic lambda calculi.

It generalizes Howe's proof technique to a categorical setting.

Abstract

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky (1990). Howe (1996) gave a direct proof that it is a congruence, and generalised the result to all languages complying with a suitable format. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name, call-by-value, and call-by-name non-deterministic $\lambda$-calculus, and more generally all languages complying with a variant of Howe's format.