Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Pebble-Relation Comonad in Finite Model Theory

Yoàv Montacute, Nihil Shah

TL;DR

This work defines the pebble-relation comonad $\mathbb{PR}_{k}$ to categorically capture pathwidth, paralleling the established pebbling comonad for treewidth. It shows that coalgebras for $\mathbb{PR}_{k}$ correspond to path decompositions of width $<k$, and that coKleisli morphisms/isomorphisms encode Duplicator strategies in Dalmau’s pebble-relation and related all-in-one games, connecting these games to the restricted conjunction fragment of $k$-variable infinitary logic with counting quantifiers. A bijective variant yields a new characterization of equivalence in $\#{\curlywedge}\mathscr{L}^{k}$, while a Lovász-type theorem links pathwidth-based counting of homomorphisms to logical indistinguishability in this fragment. The results synthesize category-theoretic, combinatorial, and logical perspectives, opening avenues for algorithmic and complexity analyses of pathwidth-related properties and CSPs.

Abstract

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ász-type theorem relating pathwidth to the restricted conjunction fragment of k-variable infinitary logic with counting quantifiers.

The Pebble-Relation Comonad in Finite Model Theory

TL;DR

This work defines the pebble-relation comonad to categorically capture pathwidth, paralleling the established pebbling comonad for treewidth. It shows that coalgebras for correspond to path decompositions of width , and that coKleisli morphisms/isomorphisms encode Duplicator strategies in Dalmau’s pebble-relation and related all-in-one games, connecting these games to the restricted conjunction fragment of -variable infinitary logic with counting quantifiers. A bijective variant yields a new characterization of equivalence in , while a Lovász-type theorem links pathwidth-based counting of homomorphisms to logical indistinguishability in this fragment. The results synthesize category-theoretic, combinatorial, and logical perspectives, opening avenues for algorithmic and complexity analyses of pathwidth-related properties and CSPs.

Abstract

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ász-type theorem relating pathwidth to the restricted conjunction fragment of k-variable infinitary logic with counting quantifiers.

Paper Structure

This paper contains 18 sections, 19 theorems, 36 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Outline
  3. Preliminaries
  4. Set notation
  5. Category theory
  6. Finite model theory
  7. Logical fragments
  8. Spoiler-Duplicator games
  9. Spoiler-Duplicator game comonads
  10. Morphism and Isomorphism Power Theorems
  11. Coalgebras and Adjunctions
  12. Pebble-Relation Comonad
  13. Coalgebras and Path Decompositions
  14. Morphism and Isomorphism Power Theorems
  15. Morphism power theorem
  16. ...and 3 more sections

Key Result

Theorem 2.1

For all $\sigma$-structures $\mathcal{A}$ and $\mathcal{B}$, the following are equivalent:

Figures (2)

  • Figure 1: Separating example between the $k$-pebble game and the all-in-one $k$-pebble game for $k=2$.
  • Figure :

Theorems & Definitions (38)

  • Theorem 2.1: Morphism Power Theorem
  • Theorem 2.2: Isomorphism Power Theorem
  • Theorem 2.3: coalgebra characterisation
  • Proposition 3.1
  • proof
  • Proposition 3.2
  • proof
  • Definition 4.1: path decomposition
  • Definition 4.2: pathwidth
  • Definition 4.3: $k$-pebble linear forest cover
  • ...and 28 more