一句话：在高阶 abstract GSOS 框架下证明弱相似性的同余定理，并实例化为 λ-演算的 applicative similarity。
高阶 abstract GSOS 是 Turi 与 Plotkin 的数学操作语义（Mathematical Operational Semantics）框架向高阶语言的近期扩展，其良好行为性体现为：操作模型上的余代数强（双）相似性是同余。本文为该框架建立相应的弱相似性同余定理，从而补上了弱等价情形下的关键理论缺口。技术路线上，作者在抽象范畴层面发展了若干具有独立价值的方法，包括混合变型双函子（mixed-variance bifunctor）的关系提升、高阶 GSOS 法则（higher-order GSOS laws），以及 Howe 方法的高阶推广。作为验证，该定理可实例化为若干已知概念，例如 Abramsky 为 λ-演算提出的 applicative similarity，说明结果具有一般性与可重用性。
Higher-order abstract GSOS is a recent extension of Turi and Plotkin’s framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky’s applicative similarity for the λ-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe’s method.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{Urbat00MS23,
title = {Weak Similarity in Higher-Order Mathematical Operational Semantics},
author = {Henning Urbat and Stelios Tsampas and Sergey Goncharov and Stefan Milius and Lutz Schröder},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175706}
}