paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Backtracking with cut via a distributive law and left-zero monoids

通过分配律与左零幺半群实现带 cut 的回溯
JFP vol.272017匹配度 1/10 · 论文研究 Prolog cut 的代数效应与单子语义，属于程序语言形式语义和逻辑编程理论，与用户核心关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析无直接关联。引用 12 inbox
MACIEJ PIRÓG, SAM STATON
形式语义逻辑与约束编程
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话：用代数效应为列表单子加入 Prolog 的 cut，并给出自由左零幺半群与分配律复合两种单子刻画。

该文关注如何在回溯计算中形式化逻辑编程里的 cut 剪枝操作。作者在代数效应框架下扩展列表单子，使其支持 Prolog 风格的 cut。核心结果是给出所得单子的两种描述：一是自由左零幺半群单子，二是列表单子与“一元幂等操作”单子通过分配律复合而成。此外，cut 的作用域界定子被解释为一个 handler。这一工作用范畴论与代数效应工具统一了回溯、剪枝和效应处理，为带 cut 的回溯提供语义基础。

问题
如何用代数效应与单子为回溯计算加入 Prolog 的 cut 剪枝操作，并刻画其语义模型。
方法
将列表单子与一元幂等操作单子通过分配律复合，并用自由左零幺半群给出所得单子的刻画；cut 的作用域界定子由 handler 解释。
评估
以范畴论与代数效应语义构造给出两种单子描述，并展示 cut 作用域作为 handler 的语义；摘要未报告实验评估。
原文摘要（Abstract）

Abstract We employ the framework of algebraic effects to augment the list monad with the pruning cut operator known from Prolog. We give two descriptions of the resulting monad: as the monad of free left-zero monoids, and as a composition via a distributive law of the list monad and the ‘unary idempotent operation’ monad. The scope delimiter of cut arises as a handler.

链接与引用

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

BibTeX 
@article{PirogS17,
  title = {Backtracking with cut via a distributive law and left-zero monoids},
  author = {MACIEJ PIRÓG and SAM STATON},
  journal = {Journal of Functional Programming},
  volume = {27},
  year = {2017},
  doi = {10.1017/s0956796817000077}
}