A number of models of linear logic are based on or closely related to linear algebra, in the sense that morphisms are "matrices" over appropriate coefficient sets. Examples include models based on coherence spaces, finiteness spaces and probabilistic coherence spaces, as well as the relational and weighted relational models. This paper introduces a unified framework based on module theory, making the linear algebraic aspect of the above models more explicit. Specifically we consider modules over Sigma-semirings $R$, which are ring-like structures with partially-defined countable sums, and show that morphisms in the above models are actually $R$-linear maps in the standard algebraic sense for appropriate $R$. An advantage of our algebraic treatment is that the category of $R$-modules is locally presentable, from which it easily follows that this category becomes a model of intuitionistic linear logic with the cofree exponential. We then discuss constructions of classical models and show that the above-mentioned models are examples of our constructions.
翻译:一些线性逻辑模型基于或与线性代数密切相关的线性逻辑模型,即形态学是相对于适当系数组的“矩阵”,举例而言包括基于一致性空间、有限空间和概率一致性空间以及关系和加权关系模型的模型。本文介绍了基于模块理论的统一框架,使上述模型的线性代数方面更加清晰。具体地说,我们考虑Sigma-semirings $R$的模块,这些模块是环形结构,有部分界定的可计算数字,并表明上述模型中的形态学实际上是标准代数感值值值值值值值值值值的线性地图。我们的代数处理的一个优点是,$R$-moules的类别可以在当地出现,从中可以很容易地看出,这一类别会变成直觉学线性逻辑模型和共线性指数。我们然后讨论古典模型的构造,并显示上述模型是我们构造的范例。