paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Recipe for State-and-Effect Triangles

状态-效应三角（state-and-effect triangles）的构造配方
LMCS vol.Volume 13, Issue 22017匹配度 3/10 · 该论文属于范畴论形式语义，系统构造状态-效应三角并统一程序语义单子，涉及状态/谓词变换器与概率幂域，与静态分析和贝叶斯程序分析仅有间接理论基础关联；不涉及 LLM/Agent、机器学习系统、浮点分析或工业落地。引用 43 inbox
Bart Jacobs
形式语义
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：利用 Beck 单子性定理，从伴随系统化构造状态-效应三角，统一多种程序语义单子。

在程序语言语义中，程序既可视为状态变换器，也可视为谓词变换器。作者此前引入的 state-and-effect triangle 用范畴论刻画二者关系，其核心是状态变换器与谓词变换器之间的伴随。本文利用 Jon Beck 单子性定理中的经典结果，给出一种从任意伴随系统系统化构造此类三角的通用配方。该方法的力量通过大量实例得到展示，覆盖程序语义中出现的多种单子，包括（概率）幂域。

问题
如何在范畴语义中统一刻画程序作为状态变换器与谓词变换器这两种视角及其关系。
方法
基于 Jon Beck 单子性定理的一部分，从给定的伴随系统出发，系统化地构造 state-and-effect triangle。
评估
通过覆盖多种程序语义单子（包括概率幂域）的丰富实例说明该构造配方的适用性与威力。
原文摘要（Abstract）

In the semantics of programming languages one can view programs as state transformers, or as predicate transformers. Recently the author has introduced state-and-effect triangles which capture this situation categorically, involving an adjunction between state- and predicate-transformers. The current paper exploits a classical result in category theory, part of Jon Beck's monadicity theorem, to systematically construct such a state-and-effect triangle from an adjunction. The power of this construction is illustrated in many examples, covering many monads occurring in program semantics, including (probabilistic) power domains.

链接与引用

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

BibTeX 
@article{Jacobs15,
  title = {A Recipe for State-and-Effect Triangles},
  author = {Bart Jacobs},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 2},
  year = {2017},
  doi = {10.23638/lmcs-13(2:6)2017}
}