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 $\lambda$-calculi with recursive types, and to different flavours of contextual equivalence.

翻译：逻辑关系是高阶语言中程序上下文等价推理的关键方法。它们通常需针对具体案例逐一构建，每次语言变体或等价概念的变化都需要建立新的理论。本文在"高阶数学操作语义学"层面提出了一种（分步索引）逻辑关系的通用构造方法——该领域是一个高度参数化的范畴框架，用于建模高阶语言的操作语义。我们的主要结论表明：对于弱操作模型构成松双代数的语言，其逻辑关系自动满足上下文等价的可靠性。本文的抽象理论可实例化到组合逻辑和含递归类型的λ演算，并适用于不同形式的上下文等价。