Bunched Fuzz：矢量模糊的灵敏度
Bunched Fuzz: Sensitivity for Vector Metrics
摘要：
程序灵敏度测量程序在两个相关输入上运行时输出之间的距离。这一概念在数据隐私和优化等领域起着关键作用，近年来一直是几种程序分析技术的焦点。在最成功的类型系统中，我们可以强调受线性逻辑启发的类型系统，如Reed和Pierce在Fuzz程序设计语言中开创的。在Fuzz中，每个类型都有自己的距离，敏感性分析归结为类型检查。特别是，Fuzz具有两种乘积类型，对应于两种不同的距离概念：张量积通过将每个分量的距离相加来组合它们，而with积取它们的最大值。在这项工作中，我们表明，这些产品可以推广到任意的$L^p$距离，经常用于隐私和优化的指标。原始的Fuzz乘积，张量和with，对应于特殊情况$L^1$和$L^\infty$。为了简化对此类产品的处理，我们使用束扩展了Fuzz类型系统--如在束含义的逻辑中--其中可以使用不同的$L^p$距离组合不同组变量的距离。我们表明，我们的扩展可以用来推理概率程序的定量属性。
英文摘要：
Program sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. Among the most successful ones, we can highlight type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own distance, and sensitivity analysis boils down to type checking. In particular, Fuzz features two product types, corresponding to two different notions of distance: the tensor product combines the distances of each component by adding them, while the with product takes their maximum. In this work, we show that these products can be generalized to arbitrary $L^p$ distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases $L^1$ and $L^\infty$. To ease the handling of such products, we extend the Fuzz type system with bunches -- as in the logic of bunched implications -- where the distances of different groups of variables can be combined using different $L^p$ distances. We show that our extension can be used to reason about quantitative properties of probabilistic programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
