Relating structure and power: Comonadic semantics for computational resources
Relating structure and power: Comonadic semantics for computational resources
复制标题
关联结构和能力：计算资源的共元语义
DOI：
10.1093/logcom/exab048
复制
发表时间：
2021
影响因子：
0.7
通讯作者：
Abramsky S
中科院分区：
文献类型：
--
作者：
Abramsky S
组合对策在有限模型理论、约束满足、模态逻辑和并发理论中被广泛用于刻画结构之间的逻辑等价性。特别是，Escherichfeucht-Fraïssé游戏，卵石游戏和互模拟游戏发挥了核心作用。我们展示了如何这些类型的游戏可以描述在一个索引的家庭comonads的关系结构和同态的类别。索引是一个资源参数，它限制了对底层结构的访问程度。这些comonads的coKleisli范畴可以用来给出广泛的重要逻辑等价的无语法刻画。此外，这些索引comonad的余代数可以用来表征关键的组合参数：树深度的Escherichfeucht-Fraïssé comonad，树宽度的卵石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–Fraïssé 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 indexis a resource parameter that 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–Fraïssé 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.