一句话:为带连续采样与软条件的高阶贝叶斯 λ-演算建立交互几何模型,并证明其对两类操作语义充分。
这篇论文研究高阶贝叶斯概率编程语言的语义基础。作者考虑一个带连续均匀分布采样与软条件(soft conditioning)算子的类型化 λ-演算,它是高阶贝叶斯编程的典型演算。论文在可测空间与偏可测函数构成的范畴上构造交互几何(Geometry of Interaction)模型,用以刻画采样和条件化的计算行为。作者证明该模型相对于两种操作语义——基于分布的操作语义与基于采样的操作语义——都是充分的(adequate),从而为概率程序的意义提供了范畴语义支撑,并在指称与操作视角之间建立桥梁。
We give a geometry of interaction model for a typed λ -calculus endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The model is based on the category of measurable spaces and partial measurable functions, and is proved adequate with respect to both a distribution-based and a sampling-based operational semantics.