一句话：用纤维化统一基于操作语义的逻辑关系，覆盖纯、效应与微分情形。
基于操作语义的逻辑关系是编程语言语义学中最成功的证明方法之一，但现有工作多面向特定语言族，缺乏统一抽象框架。本文提出用纤维化（fibration）来统一处理操作逻辑关系。作者以一个带泛型效应的 λ 演算为参照，引入了在大类范畴上定义的抽象操作语义，并在此框架下重构纯逻辑关系、效应逻辑关系以及新近提出的微分逻辑关系——即程序间的高阶距离。该抽象视角为纯与效应情形下的微分逻辑关系提供了坚实的数学基础，使其与传统逻辑关系纳入同一图景，展示了纤维化作为统一语义工具的表达力。
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.
@article{paperbot2767,
title = {A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential},
author = {Francesco Dagnino and Francesco Gavazzo},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 2},
year = {2024},
doi = {10.46298/lmcs-20(2:1)2024}
}