paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore Categories

将余代数模态和 MELL 模型结构提升到 Eilenberg-Moore 范畴
LMCS vol.Volume 15, Issue 42019匹配度 1/10 · 该论文属于线性逻辑的范畴语义与形式语义,讨论MELL模型结构和Eilenberg-Moore代数,与静态分析、Agentic程序、LLM辅助形式化验证、浮点或贝叶斯程序分析均无直接关系。虽属PL理论外围,但不在用户当前研究画像的核心或交叉范围内。引用 0 inbox
Jean-Simon Pacaud Lemay
crossref: 2026-09-10

AI 速览

一句话:证明线性范畴结构可提升到 MELL 提升单子的 Eilenberg-Moore 代数范畴,并给出由余代数群诱导提升单子的来源。

本文研究直觉主义线性逻辑的乘法与指数片段(MELL)的范畴模型。已知模型为线性范畴,即带幺半余代数模态(线性指数余单子)的对称幺半闭范畴。受 Blute 与 Scott 关于 Hopf 代数模范畴作为线性逻辑模型的工作启发,作者将单子的代数范畴(Eilenberg-Moore 范畴)视为 MELL 模型。论文定义线性范畴上的 MELL 提升单子:它是 Bruguières-Lack-Virelizier 意义的 Hopf 单子,并对幺半余代数模态满足特殊混合分配律。主要结果是线性范畴结构可提升到这类单子的代数范畴。作者进一步说明幺半余代数模态的余代数范畴中的群如何诱导 MELL 提升单子,并从阿贝尔群富集给出此类群的来源;还定义了相关混合分配律与微分范畴结构的提升。

问题
如何将 MELL 的线性范畴模型结构从基范畴提升到单子的 Eilenberg-Moore 代数范畴。
方法
引入带特殊混合分配律的 MELL 提升单子,即 Hopf 单子,并利用范畴论中的混合分配律与 Hopf 单子理论构造提升。
评估
以范畴论证明为主要评估方式,给出线性范畴结构可提升的主要定理,并说明由余代数群和阿贝尔群富集构造提升单子的来源。
原文摘要(Abstract)

A categorical model of the multiplicative and exponential fragments of intuitionistic linear logic ($\mathsf{MELL}$), known as a \emph{linear category}, is a symmetric monoidal closed category with a monoidal coalgebra modality (also known as a linear exponential comonad). Inspired by Blute and Scott's work on categories of modules of Hopf algebras as models of linear logic, we study categories of algebras of monads (also known as Eilenberg-Moore categories) as models of $\mathsf{MELL}$. We define a $\mathsf{MELL}$ lifting monad on a linear category as a Hopf monad -- in the Brugui{\`e}res, Lack, and Virelizier sense -- with a special kind of mixed distributive law over the monoidal coalgebra modality. As our main result, we show that the linear category structure lifts to the category of algebras of $\mathsf{MELL}$ lifting monads. We explain how groups in the category of coalgebras of the monoidal coalgebra modality induce $\mathsf{MELL}$ lifting monads and provide a source for such groups from enrichment over abelian groups. Along the way we also define mixed distributive laws of symmetric comonoidal monads over symmetric monoidal comonads and lifting differential category structure.Comment: An extend abstract version of this paper appears in the conference proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), under the title "Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore Categories"

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot744,
  title = {Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore Categories},
  author = {Jean-Simon Pacaud Lemay},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 4},
  year = {2019},
  doi = {10.23638/lmcs-15(4:8)2019}
}