一句话：提出贝叶斯分离逻辑 BaSL，为贝叶斯概率编程提供逻辑基础与公理语义，并支持贝叶斯更新等模块化推理。
贝叶斯概率编程语言（BPPL）以代码表示统计模型并推断后验，但其语义复杂，难以推理期望值和独立性。现有概率分离逻辑（PSL、Lilac）将分离合取解释为随机变量独立性，却无法处理贝叶斯更新。本文提出贝叶斯分离逻辑 BaSL，为 BPPL 提供逻辑基础与公理语义，并用 Rokhlin-Simmons 分解定理证明内部版贝叶斯定理。BaSL 基于 Hilbert 立方上的 σ-有限测度空间实例化 Kripke 资源幺半群，其 Hoare 三元组语义与 s-有限核范畴的指称语义兼容。它可建模贝叶斯更新、条件分布、软约束和共轭先验等，通过 frame rule 保持模块化；作者验证了贝叶斯掷硬币、collider 网络、burglar alarm、参数估计和高斯混合模型等性质。
Bayesian probabilistic programming languages (BPPLs) let users denote statistical models as code while the interpreter infers the posterior distribution. The semantics of BPPLs are usually mathematically complex and unable to reason about desirable properties such as expected values and independence of random variables. To reason about these properties in a non-Bayesian setting, probabilistic separation logics such as PSL and Lilac interpret separating conjunction as probabilistic independence of random variables. However, no existing separation logic can handle Bayesian updating, which is the key distinguishing feature of BPPLs. To close this gap, we introduce Bayesian separation logic ( BaSL ), a probabilistic separation logic that gives semantics to BPPL. We prove an internal version of Bayes’ theorem using a result in measure theory known as the Rokhlin-Simmons disintegration theorem. Consequently, BaSL can model probabilistic programming concepts such as Bayesian updating, unnormalised distribution, conditional distribution, soft constraint, conjugate prior and improper prior while maintaining modularity via the frame rule. The model of BaSL is based on a novel instantiation of Kripke resource monoid via 𝜎-finite measure spaces over the Hilbert cube, and the semantics of Hoare triple is compatible with an existing denotational semantics of BPPL based on the category of s-finite kernels. Using BaSL , we then prove properties of statistical models such as the expected value of Bayesian coin flip, correlation of random variables in the collider Bayesian network, the posterior distributions of the burglar alarm model, a parameter estimation algorithm, and the Gaussian mixture model.
@article{HoWR26,
title = {Bayesian Separation Logic: A Logical Foundation and Axiomatic Semantics for Probabilistic Programming},
author = {Shing Hin Ho and Nicolas Wu and Azalea Raad},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776696}
}