paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Modular Models of Monoids with Operations

带操作幺半群的模块化模型
ICFP 7(ICFP)2023匹配度 2/10 · 论文属于纯范畴论/形式语义,讨论带操作幺半群与代数效应的模块化理论模型,未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向;仅在广义 PL 理论上与形式化验证背景有微弱关联,与具体研究问题的匹配度低。引用 7 inbox
Zhixuan Yang, Nicolas Wu
crossref: 2026-09-10

AI 速览

一句话:提出一个范畴框架,模块化地刻画带操作的幺半群的理论与模型,统一代数操作与作用域/绑定操作。

论文研究带操作的幺半群的等式理论与模型,旨在统一处理代数操作以及带作用域和变量绑定的操作,并支持理论与模型的模块化组合。受代数效应和“计算即幺半群”启发,作者建立范畴框架,证明代数操作的理论范畴与幺半群范畴等价,并表明更复杂的操作可核心反射为代数操作且保持初始代数。在模型侧,提出 modular models,使其可在存在其他操作时解释抽象语法,并给出由 monoid transformer、自由代数、复合以及对称幺半范畴构造模块化模型的方法。

问题
如何为同时包含代数操作和带作用域/变量绑定操作的等式理论提供统一语义,并让理论与模型可模块化组合。
方法
在范畴论框架下建立幺半群与理论的对应,将复杂操作核心反射为代数操作,并定义 modular models 及其构造。
评估
通过范畴等价、保持初始代数的核心反射,以及四类模块化模型构造进行理论证明,而非实验评估。
原文摘要(Abstract)

Inspired by algebraic effects and the principle of notions of computations as monoids, we study a categorical framework for equational theories and models of monoids equipped with operations. The framework covers not only algebraic operations but also scoped and variable-binding operations. Appealingly, in this framework both theories and models can be modularly composed. Technically, a general monoid-theory correspondence is shown, saying that the category of theories of algebraic operations is equivalent to the category of monoids. Moreover, more complex forms of operations can be coreflected into algebraic operations, in a way that preserves initial algebras. On models, we introduce modular models of a theory, which can interpret abstract syntax in the presence of other operations. We show constructions of modular models (i) from monoid transformers, (ii) from free algebras, (iii) by composition, and (iv) in symmetric monoidal categories.

链接与引用

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

BibTeX
@article{paperbot1917,
  title = {Modular Models of Monoids with Operations},
  author = {Zhixuan Yang and Nicolas Wu},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {ICFP},
  year = {2023},
  doi = {10.1145/3607850}
}