Bluebell：关系提升与独立性的结合用于概率推理

我们提出Bluebell，一种用于推理概率程序的程序逻辑，其中一元和关系推理风格结合在一起，创造出新的推理工具。一元风格推理非常具有表现力，并由基础机制驱动，以推理概率行为，如独立性和条件化。另一方面，关系风格推理在比较相似程序行为（例如证明差分隐私）时自然表现出色，避免了描述各个程序输出分布的需要。到目前为止，这两种推理风格在众多为概率程序演绎验证设计的程序逻辑中基本上保持分离。在Bluebell中，我们通过引入一种称为“联合条件化”的新模态来统一这些推理风格，该模态可以编码并阐明条件独立性与关系提升之间的丰富交互；这两种推理风格的两大支柱。