Higher-Order Bialgebraic Semantics
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat
TL;DR
The paper addresses the challenge of achieving compositional operational semantics for higher-order languages by extending the abstract GSOS framework to higher-order settings through $V$-pointed higher-order GSOS laws. It shows that such laws induce an operational model as the initial higher-order bialgebra and a denotational model on a final coalgebra, and under mild regularity assumptions, yield a kernel-pair congruence guaranteeing compositionality. The framework is instantiated for SKI combinatory logic and for both call-by-name and call-by-value $\lambda$-calculi within presheaf-based semantic domains, connecting to strong applicative bisimilarity. Typed extensions and future directions (effects, environment-based techniques, and law-morphism notions) are discussed, highlighting a path toward systematic, high-level reasoning for higher-order languages.
Abstract
Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term \emph{(pointed) higher-order GSOS laws}. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of combinatory logics and the $λ$-calculus w.r.t.\ a strong variant of Abramsky's applicative bisimilarity are obtained as instances.