规范锥中的线性逻辑：概率相干空间及其推广
Linear logic in normed cones: probabilistic coherence spaces and beyond
AI总结：
本文提出了规范锥对偶对范畴上的坐标无关经典线性逻辑模型，通过范数解释加性连接词，用正系数幂级数表示实解析函数建模指数连接词，克服了概率相干空间模型的基依赖缺陷。
摘要：
Ehrhard、Pagani和Tasson在规范正锥与稳定可测锥映射的范畴中提出了概率函数式编程的模型，该模型可被视为概率相干空间的坐标无关推广。然而，与概率相干空间的情形不同，该模型能否被精化为经典线性逻辑的模型仍不清楚。\n在本工作中，我们考虑了一个类似的范畴，它确实给出了完整命题线性逻辑的坐标无关模型，具有加性连接词的非退化解释和指数连接词的可靠解释。对象是满足特定完备性性质（如范数有界单调弱极限的存在性）的规范锥的对偶对，态射是有界（可伴随）正映射。范数使我们能够将加性对偶连接词区分为乘积和余积。指数连接词使用实解析函数和分布来建模，这些函数和分布具有正系数的幂级数表示。\n与概率相干空间的常见情形不同，这里没有参考或需要首选基；在这个意义上，该模型是不变的。概率相干空间形成一个全子范畴，其对象作为偏序集是格。因此，我们得到了一个符合在线性代数背景下解释线性逻辑传统的模型，可以说它摆脱了其前身的缺点。\n与Ehrhard、Pagani和Tasson工作中的构造的关系留待未来研究。
英文摘要：
Ehrhard, Pagani and Tasson proposed a model of probabilistic functional programming in a category of normed positive cones and stable measurable cone maps, which can be seen as a coordinate-free generalization of probabilistic coherence spaces. However, unlike the case of probabilistic coherence spaces, it remained unclear if the model could be refined to a model of classical linear logic. In this work we consider a somewhat similar category which gives indeed a coordinate-free model of full propositional linear logic with nondegenerate interpretation of additives and sound interpretation of exponentials. Objects are dual pairs of normed cones satisfying certain specific completeness properties, such as existence of norm-bounded monotone weak limits, and morphisms are bounded (adjointable) positive maps. Norms allow us a distinct interpretation of dual additive connectives as product and coproduct. Exponential connectives are modelled using real analytic functions and distributions that have representations as power series with positive coefficients. Unlike the familiar case of probabilistic coherence spaces, there is no reference or need for a preferred basis; in this sense the model is invariant. Probabilistic coherence spaces form a full subcategory, whose objects, seen as posets, are lattices. Thus we get a model fitting in the tradition of interpreting linear logic in a linear algebraic setting, which arguably is free from the drawbacks of its predecessors. Relations with constructions of Ehrhard, Pagani and Tasson's work are left for future research.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
