paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Commutative Monads for Probabilistic Programming Languages

面向概率编程语言的可交换单子
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 3/10 · 论文研究概率编程语言的形式语义与可交换单子,属于概率编程基础理论;但未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析的应用与交叉,与研究画像的核心方向距离较远。引用 18 inbox
Xiaodong Jia, Bert Lindenhovius, Michael Mislove, Vladimir Zamdzhiev
crossref: 2026-09-12

AI 速览

一句话:在 DCPO 范畴上构造三种概率可交换单子,并为概率不动点演算给出可靠且充分的指称语义。

概率编程语言的指称语义长期缺少 DCPO 范畴上的概率可交换单子。本文构造了三种这样的单子,并给出可继续生成更多单子的通用构造。作者用这些单子为概率不动点演算(PFPC)建立可靠且充分的指称语义;PFPC 是带混合变型递归类型、项递归与概率选择的按值调用简单类型 lambda 演算。文章进一步证明,在连续 dcpo 的特殊情形下,三种单子都等同于 Jones 的 valuation 单子,并完整刻画其诱导的 Eilenberg-Moore 范畴,证明它们均同构于 Keimel 与 Plotkin 的连续 Kegelspitzen 范畴。

问题
如何为含概率选择的编程语言在 DCPO 上找到合适的可交换单子,并据此给出其指称语义。
方法
构造三种概率可交换单子及通用构造,并将其用于 PFPC 的指称语义与 Eilenberg-Moore 范畴分析。
评估
通过证明 PFPC 语义的可靠性与充分性、与 Jones valuation 单子在连续 dcpo 上一致,以及 EM 范畴同构于连续 Kegelspitzen 范畴来评估。
原文摘要(Abstract)

A long-standing open problem in the semantics of programming languages supporting probabilistic choice is to find a commutative monad for probability on the category DCPO. In this paper we present three such monads and a general construction for finding even more. We show how to use these monads to provide a sound and adequate denotational semantics for the Probabilistic FixPoint Calculus (PFPC) - a call-by-value simply-typed lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. We also show that in the special case of continuous dcpo's, all three monads coincide with the valuations monad of Jones, and we fully characterise the induced Eilenberg-Moore categories by showing that they are all isomorphic to the category of continuous Kegelspitzen of Keimel and Plotkin.

链接与引用

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

BibTeX
@inproceedings{paperbot6183,
  title = {Commutative Monads for Probabilistic Programming Languages},
  author = {Xiaodong Jia and Bert Lindenhovius and Michael Mislove and Vladimir Zamdzhiev},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470611}
}