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.

翻译：我们提出有限模型理论中组合方法的范畴理论——该关键技术通过从简单组件构建复杂结构，实现了模块化推理。组合方法所需的关键结果是Feferman-Vaught-Mostowski (FVM)类型定理，该定理刻画了逻辑等价性在模型组合与变换下的行为规律。通过扩展最近引入的模型比较博弈博弈伴随语义，我们建立了相关结论。这种抽象层次使我们能以统一方式给出产生FVM类型结果的条件。我们的定理在模型类、逻辑及所涉及的操作上具有参数化特性。此外，这些定理自然地解释了正存在片段及这些逻辑的计数量词扩展。我们还揭示了FVM类型定理与单子理论中经典概念之间的惊人联系。通过重构多个具有实际意义的经典定理（包括Dawar、Severini和Zapata关于三变量计数逻辑与共谱性先前结果的精炼版本），我们展示了方法的有效性。为突显技术参数化于目标逻辑的重要性，我们证明了结构积上的一族FVM定理——该定理在相关逻辑中具有统一性，这是无法通过具体博弈论证实现的。