基于同态不可区分性的博弈余单子局限性
计算机科学中的逻辑
2023-09-14 v2
摘要
Abramsky、Dawar 与 Wang（2017）为 k 变量计数逻辑引入了卵石余单子，从而开创了一条将范畴论工具引入有限模型论的研究路线。此类博弈余单子已针对多种逻辑得到发展，给出了相关余 Kleisli 范畴中同构意义上的逻辑等价刻画。我们通过研究线性代数逻辑展示了该方法的首个局限性；线性代数逻辑严格比一阶计数逻辑更具表达力，其 k 变量逻辑等价关系称为可逆映射等价（IM）。我们证明，在图范畴上不存在有限秩余单子，其 co-Kleisli 同构能刻画 IM 等价，从而回答了 'O Conghaile 与 Dawar（CSL 2021）的一个问题。我们通过排除用同态不可区分性刻画 IM 等价，并借助 Dawar、Jakl 与 Reggio（2021）建立的博弈余单子的 Lovász 型定理，得到该结果。两个图若在某个图类上同态不可区分，是指它们从该类中每个图出发所接纳的同态数目相同。IM 等价无法以这种方式刻画，无论是在自然数中计数同态，还是在任意有限素域中计数同态均如此。
引用
@article{arxiv.2308.05693,
title = {Limitations of Game Comonads via Homomorphism Indistinguishability},
author = {Moritz Lichter and Benedikt Pago and Tim Seppelt},
journal= {arXiv preprint arXiv:2308.05693},
year = {2023}
}
备注
Minor corrections in Section 6