度量保持的语义解释
A Semantic Account of Metric Preservation
摘要：
程序敏感性衡量程序对其输入的微小变化的鲁棒性，并且是从差分隐私到网络物理系统的领域中的基本概念。形式化程序敏感性的一种自然方式是根据输入和输出空间上的度量，要求$r$敏感函数将距离为$d$的输入映射到距离最多为$r \cdot d$的输出.因此，程序灵敏度是程序的Lipschitz连续性的类似物。Reed和Pierce介绍了Fuzz，一种具有线性类型系统的函数式语言，可以表达程序敏感性。它们在操作上以度量保持属性的形式显示出稳健性。他们的工作的启发，我们研究程序的敏感性和度量保存从指称的角度来看。特别是，我们通过赋予CPO兼容的距离概念，引入了度量CPO，这是一种用于推理度量空间上计算的新型语义结构。这种结构对于推理程序的度量属性，特别是程序敏感性非常有用。我们证明度量CPOs的模糊的确定性片段的模型。
英文摘要：
Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that an $r$-sensitive function map inputs that are at distance $d$ to outputs that are at distance at most $r \cdot d$. Program sensitivity is thus an analogue of Lipschitz continuity for programs. Reed and Pierce introduced Fuzz, a functional language with a linear type system that can express program sensitivity. They show soundness operationally, in the form of a metric preservation property. Inspired by their work, we study program sensitivity and metric preservation from a denotational point of view. In particular, we introduce metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, by endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity. We demonstrate metric CPOs by giving a model for the deterministic fragment of Fuzz.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
