度量保持的语义阐释
编程语言
2022-10-25 v3 计算机科学中的逻辑
摘要
程序敏感性衡量程序对其输入微小变化的鲁棒性，是从差分隐私到信息物理系统等领域的根本概念。将程序敏感性形式化的一种自然方式是基于输入与输出空间上的度量，要求一个 -敏感函数将距离为 的输入映射为距离至多为 的输出。因此，程序敏感性是程序版 Lipschitz 连续性的类比。Reed 和 Pierce 引入了 Fuzz，一种具有线性类型系统、可表达程序敏感性的函数式语言。他们以度量保持属性的形式在操作上证明了可靠性。受他们工作的启发，我们从指称语义的角度研究程序敏感性与度量保持。特别地，我们通过为 CPO 赋予兼容的距离概念，引入了度量 CPO（metric CPOs），一种用于推理度量空间上计算的新型语义结构。该结构有助于推理程序的度量性质，特别是程序敏感性。我们通过为 Fuzz 的确定性片段给出模型来展示度量 CPOs。
引用
@article{arxiv.1702.00374,
title = {A Semantic Account of Metric Preservation},
author = {Arthur Azevedo de Amorim and Marco Gaboardi and Justin Hsu and Shin-ya Katsumata and Ikram Cherigui},
journal= {arXiv preprint arXiv:1702.00374},
year = {2022}
}