paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱

线性逻辑的线性代数模型:作为 Σ-半环上模范畴
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10 · 论文属于纯形式语义/范畴论研究,讨论线性逻辑的线性代数模型与Σ-半环上的模范畴,与用户核心关注的方向(面向ML/Agentic程序的静态分析、LLM改进静态分析/形式化验证、浮点程序分析、贝叶斯程序分析)没有直接关联。虽然涉及形式化方法,但既非程序分析工具,也不涉及LLM/Agent或浮点/贝叶斯分析。引用 5 inbox
Takeshi Tsukada, Kazuyuki Asada
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出以 Σ-半环上模范畴统一线性逻辑的线性代数模型,并得到带余自由指数的直觉主义线性逻辑模型。

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

问题
许多线性逻辑模型(如相干空间、有限性空间、概率相干空间、关系与加权关系模型)本质上具有线性代数结构,但其态射与系数集合的代数性质缺乏统一解释。
方法
引入 Σ-半环上的模范畴作为统一框架,将上述模型态射解释为 R-线性映射,并利用 R-模范畴的局部可表性构造带余自由指数的直觉主义线性逻辑模型,进而讨论经典模型构造。
评估
理论结果为证明:上述具体模型被证明是所构造 R-模范畴模型的实例;R-模范畴局部可表性给出模型构造,无需经验评估。
原文摘要(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 Σ-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.

链接与引用

DOI 原文 · arXiv · DBLP

BibTeX
@inproceedings{TsukadaA22,
  title = {Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱},
  author = {Takeshi Tsukada and Kazuyuki Asada},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533373}
}