paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Comonadic semantics for guarded fragments

守卫片段(guarded fragments)的余单子语义
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 1/10 · 该论文属于纯形式语义、逻辑与自动机方向,研究守卫片段的余单子语义和模型比较游戏,未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析。虽与形式化方法有理论层面的间接联系,但不在用户研究画像的核心方向上。引用 17 inbox
Samson Abramsky, Dan Marsden
crossref: 2026-09-12

AI 速览

一句话:用资源索引余单子统一刻画量词守卫一阶逻辑片段的模型比较游戏,并用余代数对应守卫树分解。

本文把此前用资源索引余单子刻画 Ehrenfeucht–Fraïssé、pebbling 与 bisimulation 等模型比较游戏的方法,推广到一阶逻辑的量词守卫片段。作者系统处理原子守卫、宽松守卫与团守卫,证明 coKleisli 态射刻画存在式守卫双模拟游戏中 Duplicator 的获胜策略,而往返双模拟及完整守卫片段等价则由开态射的 span 刻画。论文进一步研究这些余单子的余代数,证明它们对应守卫树分解,并在无语法框架下用超图范畴上的余单子统一构造。

问题
如何为量词守卫的一阶逻辑片段提供范畴论/余单子语义,并统一解释其模型比较游戏与树分解参数。
方法
在关系结构范畴上使用资源索引余单子,覆盖原子、宽松和团守卫;以 coKleisli 态射、开态射 span 和余代数分析守卫双模拟与守卫树分解,并给出超图上的无语法版本。
评估
通过证明 coKleisli 态射对应 Duplicator 获胜策略、余代数对应守卫树分解等数学定理,建立与既有模型比较游戏和组合参数结果的对应。
原文摘要(Abstract)

In previous work ([1], [2], [3]), it has been shown how a range of model comparison games which play a central role in finite model theory, including Ehrenfeucht-Fraïssé, pebbling, and bisimulation games, can be captured in terms of resource-indexed comonads on the category of relational structures. Moreover, the coalgebras for these comonads capture important combinatorial parameters such as tree-width and tree-depth.The present paper extends this analysis to quantifier-guarded fragments of first-order logic. We give a systematic account, covering atomic, loose and clique guards. In each case, we show that coKleisli morphisms capture winning strategies for Duplicator in the existential guarded bisimulation game, while back-and-forth bisimulation, and hence equivalence in the full guarded fragment, is captured by spans of open morphisms. We study the coalgebras for these comonads, and show that they correspond to guarded tree decompositions. We relate these constructions to a syntax-free setting, with a comonad on the category of hypergraphs.

链接与引用

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

BibTeX
@inproceedings{paperbot6228,
  title = {Comonadic semantics for guarded fragments},
  author = {Samson Abramsky and Dan Marsden},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470594}
}