paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Probabilistic Stable Functions on Discrete Cones are Power Series

离散锥上的概率稳定函数是幂级数
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 论文研究概率编程的指称语义与范畴论,与贝叶斯程序分析的理论基础有微弱关联;但未涉及静态分析、LLM/Agent、浮点程序分析或工业落地,也与用户偏好的理论+工程结合不符,距离核心研究方向较远。引用 18 inbox
Raphaëlle Crubillé
crossref: 2026-09-12

AI 速览

一句话:证明离散锥上的概率稳定函数可视为广义幂级数,并将概率相干空间嵌入连续概率模型 Cstabm。

本文研究可测锥与可测稳定函数构成的范畴 Cstabm,它是带连续概率与完全递归的高阶语言的指称模型。作者从离散概率视角考察该模型,构造一个笛卡尔闭、全且忠实的函子,将概率相干空间——带完全递归与离散概率的高阶语言的完全抽象指称模型——嵌入 Cstabm。证明的关键是推广实分析中的 Bernstein 定理,从而把离散锥之间的稳定函数刻画为广义幂级数。该结果说明离散概率模型可被视为连续概率模型的特例,并揭示了稳定函数与幂级数表示之间的深层联系。

问题
如何将离散概率的完全抽象指称模型(概率相干空间)纳入连续概率的稳定函数模型 Cstabm,并刻画离散锥之间稳定函数的表示。
方法
在可测锥与可测稳定函数范畴中构造笛卡尔闭、全且忠实的函子,并推广 Bernstein 定理,将离散锥之间的稳定函数表示为广义幂级数。
评估
该工作为理论证明,未报告实现或实验;以函子嵌入与广义 Bernstein 定理的证明作为主要验证。
原文摘要(Abstract)

We study the category Cstabm of measurable cones and measurable stable functions---a denotational model of an higher-order language with continuous probabilities and full recursion [7]. We look at Cstabm as a model for discrete probabilities, by showing the existence of a cartesian closed, full and faithful functor which embeds probabilistic coherence spaces---a fully abstract denotational model of an higher language with full recursion and discrete probabilities [8]---into Cstabm. The proof is based on a generalization of Bernstein's theorem from real analysis allowing to see stable functions between discrete cones as generalized power series.

链接与引用

DOI 原文 ·

BibTeX
@inproceedings{paperbot4371,
  title = {Probabilistic Stable Functions on Discrete Cones are Power Series},
  author = {Raphaëlle Crubillé},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209198}
}