paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A categorical account of composition methods in logic

逻辑中组合方法的范畴论刻画
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 1/10 · 论文属于有限模型论与范畴论逻辑,研究组合方法与 FVM 型定理的 game comonad 语义统一,与用户关注的机器学习/Agent 静态分析、LLM 辅助形式化验证、浮点程序分析和贝叶斯程序分析均无直接关联。引用 2 inbox
Tomáš Jakl, Dan Marsden, Nihil Shah
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:用 game comonad 语义统一刻画有限模型论组合方法中的 FVM 型定理,并给出参数化构造。

有限模型论中的组合方法通过将复杂结构拆成简单组件来支持模块化推理,其核心是 Feferman–Vaught–Mostowski(FVM)型定理,刻画逻辑等价在模型组合与变换下的行为。本文将近期用于模型比较博弈的 game comonad 语义推广为范畴论框架,给出统一条件以导出 FVM 型结果。该框架对模型类、逻辑和操作保持参数化,并自然涵盖正存在片段及带计数量词的扩展;还揭示了 FVM 定理与单子论经典概念的联系。作者用该框架重新得到若干经典定理,包括对 Dawar、Severini 和 Zapata 关于三变量计数逻辑与同谱性的结果的精细化,并证明结构乘积的一族对逻辑一致的 FVM 定理,这是特定博弈论证难以做到的。

问题
如何为有限模型论中的组合方法提供统一、范畴化的理论基础,并刻画逻辑等价在模型组合与变换下的行为(FVM 型定理)。
方法
扩展用于模型比较博弈的 game comonad 语义,在范畴与单子层面给出参数化条件,统一导出 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 be-haves 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.

链接与引用

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

BibTeX
@inproceedings{abs-2304-10196,
  title = {A categorical account of composition methods in logic},
  author = {Tomáš Jakl and Dan Marsden and Nihil Shah},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175751}
}