paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Integration in Cones

锥上的积分
LMCS vol.Volume 21, Issue 12025匹配度 3/10 · 论文为概率编程语言提供基于可测锥的指称语义与积分理论,与概率/贝叶斯程序分析的形式基础有间接关联,但不涉及静态分析、LLM/Agent、浮点分析或工业落地,与画像核心方向距离较远。引用 4 inbox
Thomas Ehrhard, Guillaume Geoffroy
crossref: 2026-09-10

AI 速览

一句话:为可测锥建立积分理论,使概率编程语言的抽样原语可在锥语义模型中获得解释,并构造线性逻辑的两个指数余单子。

可测锥此前可建模直觉主义线性逻辑与按名调用概率 PCF,并支持实数线等连续数据类型,但缺少对以锥为陪域的函数的积分理论,因而无法解释更一般概率语言(尤其按值调用与 call-by-push-value)中的抽样原语。本文把拓扑向量空间中的 Pettis 积分推广到锥上,定义了锥值函数的积分与可积锥,并以保积分线性映射为态射。作者证明由此得到的范畴是线性逻辑的模型,并构造两个指数余单子:其一基于已有的稳定可测函数概念,其二基于新提出的锥上可积解析函数概念。

问题
如何为可测锥语义模型补上以锥为陪域的函数积分理论,以解释概率编程语言中的抽样原语,并覆盖按值调用和 call-by-push-value 等更一般的语言。
方法
将拓扑向量空间中的 Pettis 积分适配到锥上,定义可积锥及保积分线性映射,并证明该范畴构成线性逻辑模型;进一步构造基于稳定可测函数与可积解析函数的两个指数余单子。
评估
采用数学定义与定理证明进行理论评估,证明新范畴是线性逻辑模型并给出两个指数余单子的构造;没有实验或实现评估。
原文摘要(Abstract)

Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of call-by-name probabilistic PCF which accommodates "continuous data types" such as the real line. So far however, they lacked a major feature to make them a model of more general probabilistic programming languages (notably call-by-value and call-by-push-value languages): a theory of integration for functions whose codomain is a cone, which is the key ingredient for interpreting the sampling programming primitives. The goal of this paper is to develop such a theory: our definition of integrals is an adaptation to cones of Pettis integrals in topological vector spaces. We prove that such integrable cones, with integral-preserving linear maps as morphisms, form a model of Linear Logic for which we develop two exponential comonads: the first based on a notion of stable and measurable functions introduced in earlier work and the second based on a new notion of integrable analytic function on cones.

链接与引用

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

BibTeX
@article{EhrhardG25,
  title = {Integration in Cones},
  author = {Thomas Ehrhard and Guillaume Geoffroy},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 1},
  year = {2025},
  doi = {10.46298/lmcs-21(1:1)2025}
}