Courcelle 与 Feferman-Vaught-Mostowski 定理的博弈余单子刻画
计算机科学中的逻辑
2022-05-12 v1 范畴论
逻辑
摘要
由 Abramsky、Dawar 与 Wang 引入、并由 Abramsky 和 Shah 发展的博弈余单子 (game comonads)，为模型比较博弈提供了范畴语义。我们在博弈余单子框架下给出 Feferman-Vaught-Mostowski (FVM) 复合定理的公理化刻画，并以模型比较博弈为参数。我们以统一方式得到所讨论逻辑及其正存在量词与计数量词变体的组合性结果。其次，我们将博弈余单子推广至二阶情形，具体针对单子二阶 (MSO) 逻辑。随后我们将 FVM 定理推广到二阶情形。最后，利用前述进展给出 Courcelle 算法元定理的抽象表述，并实例化以恢复图上 MSO 的著名有界树宽与有界团宽 Courcelle 定理。
引用
@article{arxiv.2205.05387,
title = {A game comonadic account of Courcelle and Feferman-Vaught-Mostowski theorems},
author = {Tomáš Jakl and Dan Marsden and Nihil Shah},
journal= {arXiv preprint arXiv:2205.05387},
year = {2022}
}