Comonadic semantics for guarded fragments
Comonadic semantics for guarded fragments
复制标题
受保护片段的共元语义
DOI：
10.1109/lics52264.2021.9470594
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Abramsky S
中科院分区：
文献类型：
--
作者：
Abramsky S
在之前的工作（[1],[2],[3]）中，已经展示了如何在有限模型理论中发挥核心作用的一系列模型比较游戏，包括Ehrenfeucht-Fraïssé，卵石和双模拟游戏，可以根据关系结构类别上的资源索引公共元素来捕获。此外，这些共通点的余代数捕获了重要的组合参数，如树宽度和树深度。本文将这一分析推广到一阶逻辑的量词保护片段。我们给出了一个系统的说明，包括原子的，松散的和集团的警卫。在每种情况下，我们都表明coKleisli多态性在存在保护双模拟博弈中捕获复制者的制胜策略，而前后双模拟，因此在完全保护片段中的等价，是由开放多态性的范围捕获的。我们研究了这些共通体的余代数，并证明了它们对应于守卫树分解。我们将这些结构与一个无语法的设置联系起来，在超图的范畴上有一个共同点。
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.