paperbot · PL 论文追踪

全部论文 待读 收藏

P1 The Geometry of Bayesian Programming

贝叶斯编程的交互几何
LICS 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2019匹配度 5/10 · 论文研究高阶贝叶斯编程的几何交互模型与操作语义充分性,属于概率/贝叶斯编程的形式语义基础,与用户对贝叶斯程序分析及形式化的兴趣有部分交集;但不涉及静态分析、LLM/Agent、浮点分析或工程落地与 benchmark,因此匹配度中等。引用 8 inbox
Ugo Dal Lago, Naohiko Hoshino
crossref: 2026-09-12

AI 速览

一句话:为带连续采样与软条件的高阶贝叶斯 λ-演算建立交互几何模型,并证明其对两类操作语义充分。

这篇论文研究高阶贝叶斯概率编程语言的语义基础。作者考虑一个带连续均匀分布采样与软条件(soft conditioning)算子的类型化 λ-演算,它是高阶贝叶斯编程的典型演算。论文在可测空间与偏可测函数构成的范畴上构造交互几何(Geometry of Interaction)模型,用以刻画采样和条件化的计算行为。作者证明该模型相对于两种操作语义——基于分布的操作语义与基于采样的操作语义——都是充分的(adequate),从而为概率程序的意义提供了范畴语义支撑,并在指称与操作视角之间建立桥梁。

问题
如何为带连续采样和软条件的高阶概率编程语言提供范畴语义模型,并使指称语义与操作行为一致。
方法
在可测空间与偏可测函数范畴中构造交互几何模型,对类型化 λ-演算进行解释。
评估
证明模型相对于基于分布和基于采样的两种操作语义均满足充分性(adequacy)。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot5020,
  title = {The Geometry of Bayesian Programming},
  author = {Ugo Dal Lago and Naohiko Hoshino},
  booktitle = {LICS},
  year = {2019},
  doi = {10.1109/lics.2019.8785663}
}