paperbot · PL 论文追踪

全部论文 待读 收藏

P2 String Diagrams for Premonoidal Categories

前幺半范畴的弦图
LMCS vol.Volume 21, Issue 22025匹配度 2/10 · 该论文是纯范畴论/形式语义研究，讨论弦图作为 premonoidal、effectful 与 Freyd 范畴的内部语言，与用户关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析没有直接交集。仅在最宽泛的程序语言形式语义基础上可能与 PL 理论相关，但不触及核心研究方向。引用 3 inbox
Mario Román, Paweł Sobociński
形式语义
crossref: 2026-09-10

AI 速览

一句话：证明带 runtime object 的弦图是 effectful 范畴的内部语言，并可用于前幺半、Freyd 等范畴。

前幺半范畴（premonoidal categories）是去掉交换律的幺半范畴；effectful 范畴则是在其上选定一个由可交换态射组成的幺半子范畴。已有工作表明弦图可作为幺半范畴的内部语言，而 Jeffrey 引入的带 runtime object 的弦图被用于描述有副作用计算。本文证明这类扩展弦图同样是 effectful 范畴的内部语言，从而为 effectful、premonoidal 以及 Freyd 范畴提供统一的弦图演算与语法表示。该结果将范畴结构与图形语法对应起来，便于以图形方式推理非交换/有副作用语境中的态射组合。

问题
如何为前幺半范畴、effectful 范畴以及 Freyd 范畴提供统一的内部语言与图形演算。
方法
在弦图中加入 runtime object，并证明该扩展弦图语言与 effectful 范畴之间的范畴论对应关系。
评估
通过范畴论刻画与内部语言定理进行理论论证，说明该弦图语言可用于 effectful、premonoidal 和 Freyd 范畴；摘要未提及实验评估。
原文摘要（Abstract）

Premonoidal categories are monoidal categories without the interchange law while effectful categories are premonoidal categories with a chosen monoidal subcategory of interchanging morphisms. In the same sense that string diagrams, pioneered by Joyal and Street, are an internal language for monoidal categories, we show that string diagrams with an added "runtime object", pioneered by Alan Jeffrey, are an internal language for effectful categories and can be used as string diagrams for effectful, premonoidal, and Freyd categories.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{RomanS25,
  title = {String Diagrams for Premonoidal Categories},
  author = {Mario Román and Paweł Sobociński},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 2},
  year = {2025},
  doi = {10.46298/lmcs-21(2:9)2025}
}