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），一种用于推理概率程序的程序逻辑，它将一元推理与关系推理相结合以创建新的推理工具。一元推理风格具有极强的表达能力，其基础机制能够处理概率行为（如独立性和条件化）的推理。而关系推理风格在比较相似程序的行为特性时（例如证明差分隐私时）自然表现出色，能够避免对单个程序的输出分布进行刻画。迄今为止，在为概率程序演绎验证设计的众多程序逻辑中，这两种推理风格基本保持分离。在蓝铃花中，我们通过引入称为“联合条件化”的新模态来统一这些推理风格，该模态能够编码并阐明条件独立性与关系提升之间的丰富交互——这两种分别来自不同推理风格的核心机制。