Bunched Fuzz: Sensitivity for Vector Metrics

TL;DR

This paper generalizes the sensitivity analysis framework in the Fuzz programming language to include arbitrary L^p distances, enabling more flexible reasoning about probabilistic programs and their quantitative properties.

Contribution

It introduces a novel extension of Fuzz's type system with bunches, allowing the combination of variable groups using various L^p distances beyond the original tensor and with products.

Findings

Extended Fuzz type system with bunches for arbitrary L^p distances

Able to reason about probabilistic program properties

Generalizes sensitivity analysis for privacy and optimization

Abstract

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.