线性逻辑在带范数锥中：概率一致空间及更多
摘要：用双重范数锥对的某些特定完备性质来建模完全命题线性逻辑，具有零化附加项的非退化解释和指数项的可靠解释。对象是满足特定完备性质的双重范数锥对，比如存在范数有界的单调弱极限，而态射是有界（可调节的）正态射。范数允许我们将双重加性连结词解释为积和余积。指数连结用具有正系数的幂级数表示的实解析函数和分布进行建模。与概率相干空间不同的是，这里没有参考或需要首选基础；从这个意义上说，这个模型是不变的。概率相干空间形成一个子范畴，其对象作为偏序集是格。因此，我们得到了一个符合将线性逻辑在线性代数设置中解释的传统模型，这可以认为免于其前任的缺点。与Ehrhard、Pagani和Tasson的工作的关系留待将来研究。
作者：Sergey Slavnov
论文ID：1803.06005
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22