Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning

Jialu Bao, Emanuele D'Osualdo, Azadeh Farzan

TL;DR

In BlueBell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools, a new modality called “joint conditioning” is introduced that can encode and illuminate the rich interaction between conditional independence and relational liftings.

Abstract

We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behaviour of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In Bluebell, we unify these styles of reasoning through the introduction of a new modality called "joint conditioning" that can encode and illuminate the rich interaction between conditional independence and relational liftings; the two powerhouses from the two styles of reasoning.

Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning

TL;DR

In BlueBell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools, a new modality called “joint conditioning” is introduced that can encode and illuminate the rich interaction between conditional independence and relational liftings.

Abstract

We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behaviour of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In Bluebell, we unify these styles of reasoning through the introduction of a new modality called "joint conditioning" that can encode and illuminate the rich interaction between conditional independence and relational liftings; the two powerhouses from the two styles of reasoning.
Paper Structure (68 sections, 79 theorems, 171 equations, 17 figures)

This paper contains 68 sections, 79 theorems, 171 equations, 17 figures.

Table of Contents

  1. Introduction
  2. A Tour of Bluebell
  3. The Alliance
  4. Joint Conditioning and Relational Lifting
  5. The Laws of Joint Conditioning
  6. Outside the Box of Relational Lifting
  7. Preliminaries: Programs and Probability Spaces
  8. Indexed tuples
  9. Programs
  10. The Bluebell Logic
  11. A Model of (Probabilistic) Resources
  12. Probabilistic Hyper-Assertions
  13. The meaning of owning $\Ip{x}{1} \sim \mu$
  14. Permissions
  15. Relevant indices
  16. ...and 53 more sections

Key Result

proposition 1

All the assertions in fig:assertions are upward-closed.

Figures (17)

  • Figure 1: A stochastic dominance example: composing Monte Carlo algorithms two different ways. $N\in\mathbb{N}$ is some fixed constant, and all variables are initially 0.
  • Figure 2: One time pad.
  • Figure 3: Syntax of program terms.
  • Figure 4: Primitive Conditioning Laws.
  • Figure 5: Von Neumann extractor.
  • ...and 12 more figures

Theorems & Definitions (95)

  • definition 1: Probability spaces
  • definition 2: Product and union spaces
  • definition 3: Independent product lilac
  • definition 4: Ordered Unital Resource Algebra
  • definition 5: Probability Spaces RA
  • definition 6
  • definition 7: Compatibility
  • definition 8
  • definition 9: Bluebell RA
  • definition 10: Almost-measurability
  • ...and 85 more