paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Pebble-Relation Comonad in Finite Model Theory

有限模型论中的 pebble-relation 余单子
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 1/10 · 该论文属于有限模型论与范畴论的形式语义研究,讨论 pebble-relation 余单子、路径宽度与 k 变量无穷逻辑片段,与用户关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析均无直接关联。引用 27 inbox
Yoàv Montacute, Nihil Shah
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:引入 pebble-relation 余单子,用余Kleisli 映射刻画 k 变量无穷逻辑受限合取片段,余代数对应 pathwidth 与路径分解。

Abramsky–Dawar–Wang 的 pebbling 余单子为有限模型论中的 k-pebble 游戏提供范畴解释:其余Kleisli 范畴刻画无穷 k 变量逻辑不同片段的等价,其余代数表征 treewidth 并对应树分解。本文引入 pebble-relation 余单子,表征 pathwidth,并使其余代数对应路径分解。作者证明该余单子的余Kleisli 态射等价于 k 变量无穷逻辑受限合取片段的真值保持,证明使用 Dalmau 的 pebble-relation 游戏及等价的 all-in-one pebble 游戏;又用带隐藏 pebble 放置的双射版 all-in-one 游戏处理余Kleisli 同构。推论给出联系 pathwidth 与带计数量词的该逻辑片段的新 Lovász 型定理。

问题
如何用范畴论余单子统一刻画有限模型论中 pebble 游戏所对应的逻辑片段,并将 treewidth 与树分解的结论推广到 pathwidth 与路径分解。
方法
引入 pebble-relation 余单子,建立其余Kleisli 态射/同构与 k 变量无穷逻辑受限合取片段的真值保持之间的等价;证明使用 Dalmau 的 pebble-relation 游戏、all-in-one pebble 游戏及其双射版本。
评估
评估为纯理论证明:通过游戏等价和范畴构造证明余代数对应路径分解,并导出带计数量词的 Lovász 型定理,不涉及实验。
原文摘要(Abstract)

The pebbling comonad, introduced by Abramsky, Dawar and Wang, provides a categorical interpretation for the k-pebble games from finite model theory. The coKleisli category of the pebbling comonad specifies equivalences under different fragments and extensions of infinitary k-variable logic. Moreover, the coalgebras over this pebbling comonad characterise treewidth and correspond to tree decompositions. In this paper we introduce the pebble-relation comonad, which characterises pathwidth and whose coalgebras correspond to path decompositions. We further show that the existence of a coKleisli morphism in this comonad is equivalent to truth preservation in the restricted conjunction fragment of k-variable infinitary logic. We do this using Dalmau’s pebble-relation game and an equivalent all-in-one pebble game. We then provide a similar treatment to the corresponding coKleisli isomorphisms via a bijective version of the all-in-one pebble game with a hidden pebble placement. Finally, we show as a consequence a new Lovász-type theorem relating pathwidth to the restricted conjunction fragment of k-variable infinitary logic with counting quantifiers.

链接与引用

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

BibTeX
@inproceedings{MontacuteS24,
  title = {The Pebble-Relation Comonad in Finite Model Theory},
  author = {Yoàv Montacute and Nihil Shah},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533335}
}