一句话：为存在式 k-卵石游戏引入余单子，用 coKleisli 态射统一刻画有限模型论多个核心概念。
论文研究有限模型论、约束满足与数据库理论中核心的卵石游戏，如何用计算语义中的范畴结构（monad/comonad）自然表述，并建立有限模型论与计算语义的联系。作者为存在式 k-卵石游戏引入 k-卵石余单子，证明 Duplicator 获胜策略等价于 coKleisli 范畴中的态射，并用该余单子给出若干概念的范畴刻画：k-变量计数逻辑初等等价、全 k-变量逻辑等价、结构树宽的 coalgebra 数、强一致性与 Cai-Fürer-Immerman 构造，并为新模态算子提供语义。评估为理论性证明与范畴刻画，展示统一框架能刻画多个中心概念，非实证实验。
Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential k-pebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for structures A and B are equivalent to morphisms from A to B in the coKleisli category for this comonad. This leads on to comonadic characterisations of a number of central concepts in Finite Model Theory: • Isomorphism in the co-Kleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers. • Symmetric games corresponding to equivalence in full k-variable logic are also characterized. • The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad. • Co-Kleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-Fürer-Immerman construction. • The k-pebbling comonad is also used to give semantics to a novel modal operator. These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation.