paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A categorical account of composition methods in logic (extended version)

逻辑中组合方法的范畴论视角(扩展版)
LMCS vol.Volume 21, Issue 42025匹配度 1/10 · 该论文是纯范畴论与有限模型论的理论工作,围绕逻辑组合方法与 FVM 型定理展开,与用户关注的静态分析、LLM/Agent 交叉、浮点程序分析及贝叶斯程序分析均无直接关联。引用 0 inbox
Tomáš Jakl, Dan Marsden, Nihil Shah
crossref: 2026-09-10

AI 速览

一句话:用扩展的博弈余单子语义统一刻画 FVM 型定理,为有限模型论中的组合方法提供参数化范畴论基础。

本文建立有限模型论中组合方法的范畴论理论。组合方法通过由简单组件构造复杂结构来实现模块化推理,其核心是 Feferman–Vaught–Mostowski(FVM)型定理,用以刻画逻辑等价在组合与变换下的行为。作者扩展用于模型比较博弈的博弈余单子语义,在范畴抽象下给出统一条件,参数化地导出 FVM 型定理;参数涵盖模型类、逻辑与操作,并自然处理存在/正存在片段及计数量词扩展。文中还揭示 FVM 型定理与单子论经典概念的联系。方法可恢复多个经典定理,细化 Dawar 等人关于三变量计数逻辑与同谱性的结果,并证明乘积结构的一族 FVM 定理,而特定博弈论证无法做到。

问题
有限模型论中的组合方法需要 FVM 型定理来支持模块化推理,但已有结果通常针对特定逻辑与模型类,缺乏统一、参数化的理论。
方法
论文扩展模型比较博弈的博弈余单子语义,用范畴论给出统一条件,以参数化方式导出 FVM 型定理,并处理存在片段、计数量词及单子论联系。
评估
通过范畴学推导恢复多个经典 FVM 定理,细化 Dawar 等人关于三变量计数逻辑与同谱性的结果,并证明乘积结构的一族统一 FVM 定理;这些定理无法用特定博弈论证得到。
原文摘要(Abstract)

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 existential and positive existential fragments, 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. This is an extended version of the LiCS 2023 conference paper of the same name.arXiv admin note: substantial text overlap with arXiv:2304.10196

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3360,
  title = {A categorical account of composition methods in logic (extended version)},
  author = {Tomáš Jakl and Dan Marsden and Nihil Shah},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 4},
  year = {2025},
  doi = {10.46298/lmcs-21(4:10)2025}
}