Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intrinsic process structure, allowing dynamic notions such as bisimulation and back-and-forth games, and resource notions such as number of rounds of a game, to be defined. These are related to extensional or "static" structures via arboreal covers, which are resource-indexed comonadic adjunctions. These ideas are developed in a general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fra\"iss\'e and modal bisimulation games recently introduced by Abramsky et al. are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.
翻译:博弈余单子提供了一种无需语法的范畴论方法来处理有限模型理论,其Eilenberg-Moore余代数通常编码结构的重要组合参数。本文发展了一个框架,通过纯粹的公理化方式捕捉这些余代数范畴的本质属性。为此,我们引入树状范畴,该类范畴具有内在的过程结构,可定义诸如互模拟和来回博弈等动态概念,以及博弈轮数等资源概念。这些结构通过资源索引的余单子伴随——即树状覆盖——与外延式或"静态"结构相关联。我们在一般公理化设定下发展这些思想,并将其应用于关系结构,恢复了由Abramsky等人近期引入的针对打牌博弈、Ehrenfeucht-Fraïssé博弈和模态互模拟博弈的余单子构造,表明有限模型理论和描述复杂性的许多基本概念均源于树状覆盖的实例。