一句话:提出以 Σ-半环上模范畴统一线性逻辑的线性代数模型,并得到带余自由指数的直觉主义线性逻辑模型。
许多线性逻辑模型都基于或密切关联线性代数,其态射可视为带适当系数的“矩阵”,例如相干空间、有限性空间、概率相干空间以及关系与加权关系模型。本文引入基于模理论的统一框架,使这些模型的线性代数特征更显式:考虑 Σ-半环 R 上的模,其中 Σ-半环是带有部分定义可数和的环状结构,并证明上述模型中的态射对于合适的 R 正是标准代数意义下的 R-线性映射。该代数处理的一个优势是 R-模范畴是局部可表的,由此容易推出该范畴在余自由指数下构成直觉主义线性逻辑的模型。文章还讨论经典模型的构造,并表明这些已有模型是其所给构造的实例。
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 Σ-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.