操作逻辑关系的纤维态叙事：纯的、带效应的与微分的
计算机科学中的逻辑
2024-08-07 v6
摘要
构建在操作语义之上的逻辑关系，是编程语言语义中最成功的证明方法之一。近年来，越来越多富有表达力的基于操作的逻辑关系概念被设计出来，并应用于特定语言族。然而，基于操作的逻辑关系的统一抽象框架仍然缺失。我们展示纤维束如何能为操作逻辑关系提供一致处理，以带有泛型效应的 lambda 演算为参考示例，该演算被赋予定义在一大类范畴上的新颖抽象操作语义。此外，这一抽象视角使我们也能为微分逻辑关系——一种近期引入的程序间高阶距离概念——奠定坚实数学基础，无论其为纯的还是带效应的，从而将它们与传统逻辑关系带回同一图景。
引用
@article{arxiv.2303.03271,
title = {A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential},
author = {Francesco Dagnino and Francesco Gavazzo},
journal= {arXiv preprint arXiv:2303.03271},
year = {2024}
}