操作逻辑关系的纤维化叙事：纯、带效应与微分
A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential
AI总结：
本文利用纤维化理论为基于操作的逻辑关系建立统一抽象框架，并将其扩展到纯与带效应的微分逻辑关系，从而统一传统与高阶距离概念。
摘要：
建立在操作语义之上的逻辑关系是编程语言语义学中最成功的证明方法之一。近年来，越来越多具有更强表达能力的基于操作的逻辑关系概念被设计出来，并应用于特定的语言族。然而，一个统一的、面向基于操作的逻辑关系的抽象框架仍然缺失。我们展示了纤维化如何能够为操作逻辑关系提供一种统一的处理方式，并以一个带有一般效应的lambda演算作为参考示例，该演算配备了一种新颖的、定义在一大类范畴之上的抽象操作语义。此外，这种抽象视角还使我们能够为微分逻辑关系——一种最近引入的用于刻画程序之间高阶距离的概念——提供坚实的数学基础，无论其是纯的还是带效应的，从而将它们与传统逻辑关系纳入同一幅统一图景之中。
英文摘要：
Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a lambda-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations -- a recently introduced notion of higher-order distance between programs -- both pure and effectful, bringing them back to a common picture with traditional ones.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
