paperbot · PL 论文追踪

全部论文 待读 收藏

P2 No-Go Theorems for Distributive Laws

分配律的不可能性定理
LMCS vol.Volume 18, Issue 12022匹配度 2/10 · 该文属纯范畴论/形式语义范畴,研究两个 monad 之间分配律不存在性的 no-go 定理,虽与 monad 组合这一 PL 基础理论相关,但既不涉及静态分析、LLM/Agent、浮点程序分析,也不涉及贝叶斯程序分析,与用户四大研究问题均无直接交集。引用 6 inbox
Maaike Zwart, Dan Marsden
crossref: 2026-09-10

AI 速览

一句话:提出三类判定两个 monad 间不存在分配律的定理,统一既有 no-go 结果并解决 list monad 自分配等开放问题。

Monad 在计算机科学中广泛使用,并可通过 Beck 分配律复合,但构造分配律困难且易错,已有工作多给出存在性构造,缺乏判定不存在的一般技术。本文提出三类 no-go 定理,用于证明两个 monad 之间不存在分配律。第一类推广了归因于 Plotkin 的反例,覆盖此前所有针对特定 monad 对的 no-go 结果并产生大量新结论;第二、三类为全新方法,适用于多种实际情形。作者据此否定了 list monad 是否可自分配的开放问题,指出文献中的一处错误,并证实 Beck 的猜想。文章还给出两个 monad 至多存在一个分配律的条件,证明若干已知分配律的唯一性。

问题
Monad 可通过 Beck 分配律复合,但如何判定两个 monad 之间不存在分配律缺乏一般方法。
方法
提出三类 no-go 定理:第一类推广 Plotkin 反例,另两类给出全新判定技术,并建立分配律唯一性条件。
评估
通过覆盖既有 no-go 结果、解决 list monad 自分配开放问题、发现文献错误并证实 Beck 猜想来验证定理的有效性。
原文摘要(Abstract)

Monads are commonplace in computer science, and can be composed using Beck's distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some general principles for constructing distributive laws. However, until now there have been no such techniques for establishing when no distributive law exists. We present three families of theorems for showing when there can be no distributive law between two monads. The first widely generalizes a counterexample attributed to Plotkin. It covers all the previous known no-go results for specific pairs of monads, and includes many new results. The second and third families are entirely novel, encompassing various new practical situations. For example, they negatively resolve the open question of whether the list monad distributes over itself, reveal a previously unobserved error in the literature, and confirm a conjecture made by Beck himself in his first paper on distributive laws. In addition, we establish conditions under which there can be at most one possible distributive law between two monads, proving various known distributive laws to be unique.

链接与引用

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

BibTeX
@article{paperbot1738,
  title = {No-Go Theorems for Distributive Laws},
  author = {Maaike Zwart and Dan Marsden},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 1},
  year = {2022},
  doi = {10.46298/lmcs-18(1:13)2022}
}