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.
翻译:游戏余单子为有限模型论提供了一种无句法依赖的范畴论方法,其艾伦伯格-摩尔余代数通常编码结构的重要组合参数。本文建立了一个框架,通过纯粹的公理化方式捕捉这些余代数范畴的本质属性。为此,我们引入具有内在过程结构的树状范畴,使得双模拟、往返博弈等动态概念,以及博弈轮数等资源概念得以定义。这些概念通过树状覆盖(一种以资源为索引的余单子伴随)与外延或"静态"结构相联系。我们在一般公理化框架下发展这些思想,并将其应用于关系结构,恢复了阿布拉姆斯基等人最近引入的用于小石子博弈、埃伦费赫特-弗拉塞博弈和模态双模拟博弈的余单子构造,表明有限模型论和描述复杂性的许多基本概念均可源于树状覆盖的实例。