高阶数学操作语义中的弱相似性
Weak Similarity in Higher-Order Mathematical Operational Semantics
AI总结：
本文将高阶抽象 GSOS 的同余结果从强（双）相似性推广到弱相似性，并借助关系提升与 Howe 方法证明其可实例化为 λ 演算的应用相似性。
摘要：
高阶抽象 GSOS 是 Turi 和 Plotkin 的数学操作语义框架向高阶语言的近期扩展。该框架中所有规范的基本良态性质是：其操作模型上的余代数强（双）相似性是同余。在本工作中，我们为弱相似性建立了相应的同余定理，并表明它可实例化为若干著名概念，例如 λ 演算的 Abramsky 应用相似性。在此过程中，我们在抽象范畴层面发展了若干具有独立价值的技术，包括逆变双函子与高阶 GSOS 律的关系提升，以及 Howe 方法。
英文摘要：
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 lambda-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
