有限模型论中的卵石余单子
计算机科学中的逻辑
2017-04-19 v1
摘要
卵石游戏是研究有限模型论、约束满足和数据库理论的有力工具。单子和余单子是范畴论的基本概念，广泛用于计算语义和现代函数式编程。我们证明了存在性k-卵石游戏具有自然的余单子表述。在结构A和B的k-卵石游戏中，复制者（Duplicator）的获胜策略等价于该余单子余Kleisli范畴中从A到B的态射。这引出了对有限模型论中若干核心概念的余单子刻画：\n- 余Kleisli范畴中的同构刻画了带计数量词的k变量逻辑中的初等等价。\n- 对应于完整k变量逻辑中等价的对称游戏也得到了刻画。\n- 结构A的树宽根据其余代数数目刻画：即存在A上的余代数结构的最小k值，对应于k-卵石余单子。\n- 余Kleisli态射用于刻画强一致性，并给出Cai-Fürer-Immerman构造的一种解释。\n- k-卵石余单子还用于为一种新颖的模态算子赋予语义。\n这些结果为计算机科学逻辑中两个很大程度上不相交的领域之间一些新的且有前景的联系奠定了基础：(1) 有限与算法模型论，以及 (2) 计算的语义与范畴结构。
引用
@article{arxiv.1704.05124,
title = {The pebbling comonad in finite model theory},
author = {Samson Abramsky and Anuj Dawar and Pengming Wang},
journal= {arXiv preprint arXiv:1704.05124},
year = {2017}
}
备注
To appear in LiCS 2017