论文标题
相关结构和力量：扩展版本
Relating Structure and Power: Extended Version
论文作者
论文摘要
组合游戏被广泛用于有限模型理论，约束满意度，模态逻辑和并发理论，以表征结构之间的逻辑等价。尤其是Ehrenfeucht-Fraisse游戏，卵石游戏和三拟合游戏起着核心作用。我们展示了如何根据关系结构和同构类别的索引家族的索引家族来描述这些类型的游戏。索引$ k $是一个资源参数，它范围界限了对基础结构的访问程度。这些comoNADS的Cokleisli类别可用于给出广泛的重要逻辑等价范围的无语法特征。此外，这些索引共同体的膜桥可用于表征关键组合参数：Ehrenfeucht-Fraisse Comonad的树深度，卵石Comonad的树宽度，以及同步 - 树的模态型号。这些结果为计算机科学领域的两个主要分支之间的系统连接铺平了道路，迄今几乎是不相关的：分类语义，以及有限和算法模型理论。
Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraisse games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index $k$ is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraisse comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory.
