一句话:引入卵石关系余单子,以其余代数刻画路径宽度,并建立其与 k 变量无穷逻辑受限合取片段的 Lovász 型定理。
Abramsky、Dawar 与 Wang 的卵石余单子为有限模型论中的 k-卵石游戏给出范畴解释:其余 Kleisli 范畴刻画无穷 k 变量逻辑不同片段的等价,余代数则对应树分解并刻画树宽度。本文引入卵石关系余单子,用其余代数对应路径分解并刻画路径宽度。作者证明该余单子中存在 coKleisli 态射当且仅当受限合取片段保持真值,证明借助 Dalmau 的卵石关系游戏及等价的 all-in-one 卵石游戏;并用双射版 all-in-one 游戏处理 coKleisli 同构。作为推论,得到将路径宽度与带计数量词的 k 变量无穷逻辑受限合取片段相联系的新 Lovász 型定理。
The pebbling comonad, introduced by Abramsky, Dawar and Wang, provides a categorical interpretation for the k-pebble games from finite model theory. The coKleisli category of the pebbling comonad specifies equivalences under different fragments and extensions of infinitary k-variable logic. Moreover, the coalgebras over this pebbling comonad characterise treewidth and correspond to tree decompositions. In this paper we introduce the pebble-relation comonad, which characterises pathwidth and whose coalgebras correspond to path decompositions. We further show that the existence of a coKleisli morphism in this comonad is equivalent to truth preservation in the restricted conjunction fragment of k-variable infinitary logic. We do this using Dalmau's pebble-relation game and an equivalent all-in-one pebble game. We then provide a similar treatment to the corresponding coKleisli isomorphisms via a bijective version of the all-in-one pebble game. Finally, we show as a consequence a new Lov\'asz-type theorem relating pathwidth to the restricted conjunction fragment of k-variable infinitary logic with counting quantifiers.