基于概率关系的推理
Probabilistic Relational Reasoning via Metrics
摘要：
Fuzz程序设计语言[Reed and Pierce，2010]使用了一个优雅的线性类型系统，结合了一个类似单子的类型来表达和推理概率敏感性属性，最著名的是$ε$ -差分隐私。我们将展示如何扩展模糊捕捉更一般的概率程序的关系属性，近似，或$(ε, δ)$ -差分隐私作为一个领先的例子。我们的技术贡献是三方面的。首先，我们引入了一个单子的共单子提升模型的概率发散的组合特性的范畴概念。然后，我们展示了如何通过一个我们称之为路径构造的附加项来表达关系属性的敏感性属性。最后，我们实例化我们的语义模型的终止片段的Fuzz扩展与类型携带信息的其他分歧之间的分布。
英文摘要：
The Fuzz programming language [Reed and Pierce, 2010] uses an elegant linear type system combined with a monad-like type to express and reason about probabilistic sensitivity properties, most notably $ε$-differential privacy. We show how to extend Fuzz to capture more general relational properties of probabilistic programs, with approximate, or $(ε, δ)$-differential privacy serving as a leading example. Our technical contributions are threefold. First, we introduce the categorical notion of comonadic lifting of a monad to model composition properties of probabilistic divergences. Then, we show how to express relational properties in terms of sensitivity properties via an adjunction we call the path construction. Finally, we instantiate our semantics to model the terminating fragment of Fuzz extended with types carrying information about other divergences between distributions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
