paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Natural Transformations as Rewrite Rules and Monad Composition

自然变换作为重写规则与 Monad 复合
LMCS vol.Volume 15, Issue 12019匹配度 2/10 · 该论文属于范畴论、monad 复合与字符串重写/合流性的形式语义基础研究,虽与形式化验证和 PL 理论有松散关联,但与用户核心关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析均无直接关系。引用 3 inbox
Dexter Kozen
crossref: 2026-09-10

AI 速览

一句话:用字符串重写与合流性刻画 monad 与伴随,简化 monad 复合验证。

本文关注范畴论构造,尤其是 monad 复合的验证问题。Eklund 等人曾提出图形化技巧来简化此类验证;作者转而采用字符串重写方法,将自然变换视为重写规则。论文证明:三元组 (T, μ, η) 构成 monad 当且仅当 T 是某个由字符串与重写规则构成的范畴中的终对象,并且这一事实可通过证明重写系统的合流性来建立。作者用 monad 复合问题说明该技术,并给出用重写范畴刻画伴随(adjunction)的方式。工作以理论证明和示例展示为主,未报告实现或实验评估。

问题
如何简化范畴论构造,特别是 monad 复合的验证,是论文关注的核心问题。
方法
将自然变换编码为字符串重写规则,构造重写范畴,并用合流性证明 monad 刻画;同时以重写范畴刻画伴随。
评估
通过理论证明和 monad 复合问题的示例说明方法,未包含实现或实验评估。
原文摘要(Abstract)

Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving string rewriting. We show that a given tuple $(T,\mu,\eta)$ is a monad if and only if $T$ is a terminal object in a certain category of strings and rewrite rules, and that this fact can be established by proving confluence of the rewrite system. We illustrate the technique on the monad composition problem. We also give a characterization of adjunctions in terms of rewrite categories.

链接与引用

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

BibTeX
@article{paperbot838,
  title = {Natural Transformations as Rewrite Rules and Monad Composition},
  author = {Dexter Kozen},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 1},
  year = {2019},
  doi = {10.23638/lmcs-15(1:1)2019}
}