论（微分）逻辑关系的度量性质
计算机科学中的逻辑
2025-05-05 v1
摘要
微分逻辑关系是一种度量高阶程序间距离的方法。它们与基于程序度量的标准方法不同，因为函数式程序之间的差异本身也是函数，将输入误差与输出误差关联起来，从而提供更细粒度、更具上下文的信息。本文旨在阐明微分逻辑关系的度量性质。尽管先前的研究表明，这些关系通常既不构成（拟）度量空间，也不构成部分度量空间，但我们证明，由此类关系产生的距离函数——我们称之为拟-拟度量——可以与拟度量和偏度量相关联，后者也可通过适当的关系定义来刻画。此外，我们利用这些联系推导出一些新的、用于程序差异的组合推理原则。
引用
@article{arxiv.2505.00939,
title = {On The Metric Nature of (Differential) Logical Relations},
author = {Ugo Dal Lago and Naohiko Hoshino and Paolo Pistone},
journal= {arXiv preprint arXiv:2505.00939},
year = {2025}
}