English

Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings

Logic in Computer Science 2022-04-25 v1

Abstract

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 RR, which are ring-like structures with partially-defined countable sums, and show that morphisms in the above models are actually RR-linear maps in the standard algebraic sense for appropriate RR. An advantage of our algebraic treatment is that the category of RR-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.

Keywords

Cite

@article{arxiv.2204.10589,
  title  = {Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings},
  author = {Takeshi Tsukada and Kazuyuki Asada},
  journal= {arXiv preprint arXiv:2204.10589},
  year   = {2022}
}