一句话：提出高阶数学操作语义下逻辑关系的通用构造，并证明其对上下文等价自动可靠。
逻辑关系是证明高阶语言上下文等价的核心方法，但通常需针对每种语言或等价概念单独构建理论。本文将（步进索引）逻辑关系的构造提升到高阶数学操作语义（HOMOS）这一高度参数化的范畴框架中，给出通用构造。主要结果：若语言的弱操作模型构成 lax 双代数，则所构造的逻辑关系对上下文等价自动可靠。该抽象理论可实例化到组合逻辑、带递归类型的 λ 演算，以及不同风格的上下文等价。
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 higherorder languages. Our main result states 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.