We present a categorical theory of the composition methods in finite model theory -- a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the composition methods are Feferman-Vaught-Mostowski (FVM) type theorems, which characterize how logical equivalence behaves under composition and transformation of models. Our results are developed by extending the recently introduced game comonad semantics for model comparison games. This level of abstraction allow us to give conditions yielding FVM type results in a uniform way. Our theorems are parametric in the classes of models, logics and operations involved. Furthermore, they naturally account for the positive existential fragment, and extensions with counting quantifiers of these logics. We also reveal surprising connections between FVM type theorems, and classical concepts in the theory of monads. We illustrate our methods by recovering many classical theorems of practical interest, including a refinement of a previous result by Dawar, Severini, and Zapata concerning the 3-variable counting logic and cospectrality. To highlight the importance of our techniques being parametric in the logic of interest, we prove a family of FVM theorems for products of structures, uniformly in the logic in question, which cannot be done using specific game arguments.

翻译：我们提出了一种关于有限模型理论中组合方法的范畴论——这是一种关键的技术，能够通过从更简单的组件构建复杂结构来实现模块化推理。组合方法所需的关键结果是费弗曼-沃特-莫斯托夫斯基型定理，该定理刻画了逻辑等价性在模型的组合与变换下的行为。我们的结果通过扩展最近引入的用于模型比较博弈的游戏余单子语义来发展。这种抽象层次使我们能够以统一的方式给出产生费弗曼-沃特-莫斯托夫斯基型结果的条件。我们的定理在模型类、逻辑和所涉及的操作上是参数化的。此外，它们自然地解释了这些逻辑的正存在片段以及带有计数量词的扩展。我们还揭示了费弗曼-沃特-莫斯托夫斯基型定理与单子理论中经典概念之间的惊人联系。通过恢复许多具有实际意义的经典定理来说明我们的方法，包括对达瓦尔、塞韦里尼和萨帕塔先前关于三变量计数逻辑与共谱性结果的改进。为了强调我们的技术在所关注逻辑上的参数化重要性，我们证明了关于结构乘积的一族费弗曼-沃特-莫斯托夫斯基定理，该族定理在所讨论的逻辑上是一致的，而这无法使用特定的博弈论证来实现。