Higher-Order Behavioural Conformances via Fibrations
Henning Urbat
TL;DR
This work introduces Abstract Higher-Order Specifications (AHOS), a categorical framework that unifies operational semantics for higher-order languages with fibrational notions of behavioural conformances (including probabilistic distances). By lifting both syntax and behaviour along suitable fibrations and employing a fibrational adaptation of Howe's method, the authors derive a general congruence theorem: under monotone/continuous rule morphisms, the greatest behavioural conformance on a language model forms a congruence. The framework subsumes both qualitative bisimilarity and quantitative behavioural distances, and is instantiated to probabilistic higher-order languages pSKI and pBCKI, yielding congruence results and connections to contextual distances. The paper also shows the limitations in certain non-affine settings, and outlines how to extend to languages with variables via presheaf models. Overall, AHOS provides a modular, principled approach to deriving congruence results across a spectrum of higher-order probabilistic languages, with clear pathways to broader features and continuous distributions.
Abstract
Coinduction is a widely used technique for establishing behavioural equivalence of programs in higher-order languages. In recent years, the rise of languages with quantitative (e.g.~probabilistic) features has led to extensions of coinductive methods to more refined types of behavioural conformances, most notably notions of behavioural distance. To guarantee soundness of coinductive reasoning, one needs to show that the behavioural conformance at hand forms a program congruence, i.e. it is suitably compatible with the operations of the language. This is usually achieved by a complex proof technique known as \emph{Howe's method}, which needs to be carefully adapted to both the specific language and the targeted notion of behavioural conformance. We develop a uniform categorical approach to Howe's method that features two orthogonal dimensions of abstraction: (1) the underlying higher-order language is modelled by an \emph{abstract higher-order specification} (AHOS), a novel and very general categorical account of operational semantics, and (2) notions of behavioural conformance (such as relations or metrics) are modelled via fibrations over the base category of an AHOS. Our main result is a fundamental congruence theorem at this level of generality: Under natural conditions on the categorical ingredients and the operational rules of a language modelled by an AHOS, the greatest behavioural (bi)conformance on its operational model forms a congruence. We illustrate our theory by deriving congruence of bisimilarity and behavioural pseudometrics for probabilistic higher-order languages.