Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone function of the distance between the corresponding inputs. When programs are probabilistic, the distance between outputs is a distance between distributions. The Kantorovich lifting provides a general way of defining a distance between distributions by lifting the distance of the underlying sample space; by choosing an appropriate distance on the base space, one can recover other usual probabilistic distances, such as the Total Variation distance. We develop a relational pre-expectation calculus to upper bound the Kantorovich distance between two executions of a probabilistic program. We illustrate our methods by proving algorithmic stability of a machine learning algorithm, convergence of a reinforcement learning algorithm, and fast mixing for card shuffling algorithms. We also consider some extensions: using our calculus to show convergence of Markov chains to the uniform distribution over states and an asynchronous extension to reason about pairs of program executions with different control flow.

@article{paperbot1163,
  title = {A pre-expectation calculus for probabilistic sensitivity},
  author = {Alejandro Aguirre and Gilles Barthe and Justin Hsu and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {POPL},
  year = {2021},
  doi = {10.1145/3434333}
}