Bialgebraic Reasoning on Higher-Order Program Equivalence
Sergey Goncharov, Stefan Milius, Stelios Tsampas, Henning Urbat
TL;DR
The paper develops a language-generic theory of step-indexed logical relations within the Higher-Order Abstract GSOS framework, addressing the fragmentation problem in contextual equivalence proofs for higher-order languages. It shows that when a language’s weak operational model forms a lax bialgebra, the constructed generic logical relations are sound for contextual equivalence, reducing the proof burden to language-specific checks. The theory is instantiated to higher-order functional languages with recursive types, notably the combinatory logic $\boldsymbol\mu\text{TCL}$ and the typed $\lambda$-calculus fragment $\text{FPC}$, illustrating both congruence and ground-contextual soundness results. This approach unifies and extends existing techniques (including Howe’s method and step-indexed relations) in a categorical setting, offering a scalable path toward automation and cross-language reasoning about program equivalence and contextual properties.
Abstract
Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higher-order languages. Our main result asserts that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and $λ$-calculi with recursive types, and to different flavours of contextual equivalence.