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

TL;DR

This paper presents a unified algebraic framework for various models of linear logic using modules over Sigma-semirings, clarifying their linear algebraic structure and establishing their categorical properties.

Contribution

It introduces a module-theoretic approach over Sigma-semirings, unifying and generalizing existing linear logic models with explicit linear algebraic structure.

Findings

Models are shown to be R-linear maps over Sigma-semirings.

The category of R-modules is locally presentable, forming a model of linear logic.

Classical models are constructed within this algebraic framework.

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 $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.