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