paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads

双范畴中的效应语义:强、交换与并发伪单子
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 1/10 · 该论文属于纯范畴论/形式语义,研究双范畴中的强单子与并发伪单子,与用户核心关注的静态分析、LLM/Agent、浮点程序分析和贝叶斯程序分析均无直接关联。虽然涉及并发函数式程序的效应语义,但不涉及用户研究画像中的分析工具、benchmark或LLM交叉方向。引用 7 inbox
Hugo Paquet, Philip Saville
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:在双范畴中建立强/交换单子理论并提出并发伪单子,为并发函数式程序的效应语义提供统一框架。

许多近年出现的效应模型(如基于 profunctor、span 或博弈策略的模型)自然构成双范畴而非普通范畴,传统强单子与交换单子难以直接刻画其效应结构。本文在双范畴的二维设定中发展强单子与交换单子理论,并仔细研究结构 2-胞的相干律。作者提出并发伪单子,用以刻画并行复合与顺序复合之间的弱交换律,揭示一个严格介于强性与交换性之间的中间层级。文章给出大量例子,并在并发博弈语义中用 continuation 伪单子加以说明,同时证明若干基础性与实用性结果,为并发函数式程序的效应语义提供新框架。

问题
论文关注非普通范畴、尤其双范畴模型中的计算效应语义问题:现有强单子/交换单子理论不足以刻画并行与顺序复合的交互。
方法
在双范畴中重新发展强、交换单子及伪单子理论,系统处理结构 2-胞的相干律,并提出并发伪单子作为中间层概念。
评估
评估以范畴学证明与案例分析为主:给出 profunctor、span、博弈等模型中的实例,并在并发博弈语义中构造 continuation 伪单子,证明若干基础结果。
原文摘要(Abstract)

We develop the theory of strong and commutative monads in the 2-dimensional setting of bicategories. This provides a framework for the analysis of effects in many recent models which form bicategories and not categories, such as those based on profunctors, spans, or strategies over games. We then show how the 2-dimensional setting provides new insights into the semantics of concurrent functional programs. We introduce concurrent pseudomonads, which capture the fundamental weak interchange law connecting parallel composition and sequential composition. This notion brings to light an intermediate level, strictly between strength and commutativity, which is invisible in traditional categorical models. We illustrate the concept with the continuation pseudomonad in concurrent game semantics. In developing this theory, we take care to understand the coherence laws governing the structural 2-cells. We give many examples and prove a number of practical and foundational results.

链接与引用

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

BibTeX
@inproceedings{PaquetS24,
  title = {Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads},
  author = {Hugo Paquet and Philip Saville},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662130}
}