paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Cones as a model of intuitionistic linear logic

锥作为直觉主义线性逻辑的模型
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 2/10 · 论文属于概率高阶计算的指称语义与线性逻辑模型,讨论锥、Scott连续函数及张量/指数对象,偏纯形式语义;与用户当前核心的静态分析、Agentic/LLM 程序分析、浮点程序分析或贝叶斯程序分析与 LLM 交叉均无直接关联。引用 4 inbox
Thomas Ehrhard
crossref: 2026-09-12

AI 速览

一句话:证明锥与线性 Scott 连续函数范畴构成直觉主义线性逻辑模型,并定义张量积与指数对象。

针对概率相干空间难以自然解释实数线等连续数据类型的问题,本文延续基于正锥的概率高阶计算模型研究,考察锥与线性且 Scott 连续函数构成的范畴。作者利用特殊伴随函子定理定义张量积,证明该张量积推广了概率相干空间的标准张量积,并证明概率相干空间在锥中稠密,从而把前者的性质提升到一般锥。进一步以同样方式定义锥的指数对象,并将可测性扩展到这些新运算,表明该范畴是直觉主义线性逻辑的一个模型。

问题
概率相干空间难以自然解释连续数据类型,因此需要为基于正锥和稳定全单调函数的概率高阶计算模型建立范畴论语义,并推广概率相干空间的性质。
方法
利用特殊伴随函子定理定义锥的张量积,借助概率相干空间在锥中的稠密性提升张量积性质,并以类似方式定义指数对象及扩展可测性。
评估
以范畴论构造与证明为主要评估方式,验证所得范畴是直觉主义线性逻辑的模型,并证明张量积扩展、稠密性以及可测性保持等理论结果。
原文摘要(Abstract)

For overcoming the limitations of probabilistic coherence spaces which do not seem to provide natural interpretations of continuous data types such as the real line, we introduced with Pagani and Tasson a model of probabilistic higher order computation based on (positive) cones, and a class of totally monotone functions that we called "stable". Then Crubillé proved that this model is a conservative extension of the earlier probabilistic coherence space model. We continue these investigations by showing that the category of cones and linear and Scott-continuous functions is a model of intuitionistic linear logic. To define the tensor product, we use the special adjoint functor theorem, and we prove that this operation is an extension of the standard tensor product of probabilistic coherence spaces. We also show that these latter are dense in cones, thus allowing to lift the main properties of the tensor product of probabilistic coherence spaces to general cones. Finally we define in the same way an exponential of cones and extend measurability to these new operations.

链接与引用

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

BibTeX
@inproceedings{paperbot5491,
  title = {Cones as a model of intuitionistic linear logic},
  author = {Thomas Ehrhard},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394758}
}