成束的模糊度：矢量度量的敏感性
摘要：程序灵敏度衡量了一个程序在两个相关输入上运行时输出之间的距离。这个概念在数据隐私和优化等领域起着关键作用，并在近年来引入的几种程序分析技术中得到了关注。其中最成功的技术之一是受线性逻辑启发的类型系统，如Reed和Pierce在Fuzz编程语言中的先驱工作。在Fuzz中，每种类型都配有自己的距离，并且灵敏度分析归结为类型检查。特别是，Fuzz具有两种乘积类型，对应于两种不同的距离概念：张量积通过将每个组成部分的距离相加来组合它们，而“with”积取它们的最大值。 在这项工作中，我们展示了这些乘积可以推广到任意$L^p$距离，这些度量通常用于隐私和优化方面。原始的Fuzz乘积，张量和“with”，对应于特殊情况$L^1$和$L^\infty$。为了简化处理这些乘积，我们在Fuzz类型系统中引入了束——类似于束联想逻辑——其中可以使用不同的$L^p$距离组合不同组变量的距离。我们证明了我们的扩展可以用于推理概率程序的定量属性。
作者：june wunder, Arthur Azevedo de Amorim, Patrick Baillot, Marco Gaboardi
论文ID：2202.01901
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-02-03