paperbot · PL 论文追踪

全部论文 待读 收藏

P2 What Is a Monoid?

什么是 monoid?
POPL 10(POPL)2026匹配度 1/10 · 该论文属于纯范畴论/形式语义,讨论 monoid 在斜多范畴中的推广及相对单子、call-by-push-value 等例子;与用户关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析均无直接交集。引用 1 inbox
Paul Blain Levy, Morgan Rogers
crossref: 2026-09-10

AI 速览

一句话:通过左斜与双斜多范畴统一 monoid 概念,涵盖相对单子与 call-by-push-value 等例子。

许多结构看似 monoid:有载体、类似单位与乘法的运算,并满足结合律与左右单位律。但传统 monoidal category 或 multicategory 中的 monoid 无法覆盖相对单子、call-by-push-value sequencing 等需要区分乘法最左和最右因子的例子。本文分两步推广 multicategory:先采用 Bourke 与 Lack 的左斜多范畴,再提出新的双斜多范畴。左斜框架中的 monoid 可涵盖相对单子;双斜框架则涵盖 span 上的范畴与 call-by-push-value sequencing。作者证明在双斜框架中 monoid 等价于无偏 monoid,即从终止双斜多范畴出发的映射。

问题
论文追问:在什么范畴论框架下,那些看似 monoid 且乘法或结合律区分最左、最右因子的结构也能被理解为 monoid?
方法
分两步推广 multicategory:先使用左斜多范畴,再提出新的双斜多范畴,并在这些框架中定义 monoid。
评估
通过相对单子、span 上的范畴与 call-by-push-value sequencing 等例子说明覆盖范围,并证明双斜框架下 monoid 与无偏 monoid 对应的一致性定理。
原文摘要(Abstract)

In many situations one encounters an entity that resembles a monoid. It consists of a carrier and two operations that resemble a unit and a multiplication, subject to three equations that resemble associativity and left and right unital laws. The question then arises whether this entity is, in fact, a monoid in a suitable sense. Category theorists have answered this question by providing a notion of monoid in a monoidal category, or more generally in a multicategory. While these encompass many examples, there remain cases which do not fit into these frameworks, such as the notion of relative monad and the modelling of call-by-push-value sequencing. In each of these examples, the leftmost and/or the rightmost factor of a multiplication or associativity law seems to be distinguished. To include such examples, we generalize the multicategorical framework in two stages. Firstly, we move to the framework of a left-skew multicategory (due to Bourke and Lack), which generalizes both multicategory and left-skew monoidal category. The notion of monoid in this framework encompasses examples where only the leftmost factor is distinguished, such as the notion of relative monad. Secondly, we consider monoids in the novel framework of a bi-skew multicategory. This encompasses examples where both the leftmost and the rightmost factor are distinguished, such as the notion of a category on a span, and the modelling of call-by-push-value sequencing. In the bi-skew framework (which is the most general), we give a coherence result saying that a monoid corresponds to an unbiased monoid, i.e. a map from the terminal bi-skew multicategory.

链接与引用

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

BibTeX
@article{abs-2504-12158,
  title = {What Is a Monoid?},
  author = {Paul Blain Levy and Morgan Rogers},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3776727}
}