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