Co-Decompositions and FO Model Checking
Abstract
Tree decompositions describe large graphs as gluings of smaller component parts. Here we study their categorical duals, tree co-decompositions, which construct large graphs via fibered products of small constituent parts. Co-decompositions are compressed representations of graphs or relational structures: the decomposed object can be exponentially larger than the space required to specify the co-decomposition. Our main contribution is an algorithmic meta-theorem for first order logic: given only a co-decomposition of a σ-structure G with b bags, each of size at most w and an FO sentence ϕ, there is an algorithm which, without ever constructing or inspecting G, operates on the co-decomposition and determines whether G ⊨ ϕ in time fσ(w,|φ|)· b. We pair this algorithm with structural results on tree co-width, including its relationship to tree-width and a separation from twin-width. Furthermore, we characterize bounded path co-width using a graph grammar. In contrast to our logical meta-theorem, we prove that (s,t)-Path becomes NP-hard on co-decomposition inputs. These results demonstrate how categorical constructions can enable efficient computation on exponentially compressed structures.
Related
- Multiple Nonlinear Waves by (Quantum) Neural Networks: Checking the AI supremacy
- First-Order Model Checking on Monadically Dependent Graph Classes
- Stochastic Mirror-Prox Optimisation of Group Distributionally Robust Multimodal Logistic Regression for Multilingual Fact-Checking Verdict Prediction
- Optimizing Both Checking and Update Costs in Random Walk Search
- KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents
BibTeX
@misc{bumpus2026codecompositions,
title = {{Co-Decompositions and FO Model Checking}},
author = {Benjamin Merlin Bumpus and Guilherme C. M. Gomes and Laura Larios-Jones and Will J. Turner},
howpublished = {arXiv},
year = {2026},
month = nov,
doi = {10.48550/arxiv.2611.04658},
eprint = {2611.04658},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2611.04658},
note = {CC BY-SA 4.0},
}
RIS
TY - UNPB
TI - Co-Decompositions and FO Model Checking
AU - Benjamin Merlin Bumpus
AU - Guilherme C. M. Gomes
AU - Laura Larios-Jones
AU - Will J. Turner
PY - 2026
DA - 2026/11/03
PB - arXiv
DO - 10.48550/arxiv.2611.04658
UR - https://arxiv.org/abs/2611.04658
AB - Tree decompositions describe large graphs as gluings of smaller component parts. Here we study their categorical duals, tree co-decompositions, which construct large graphs via fibered products of small constituent parts. Co-decompositions are compressed representations of graphs or relational structures: the decomposed object can be exponentially larger than the space required to specify the co-decomposition. Our main contribution is an algorithmic meta-theorem for first order logic: given only a co-decomposition of a σ-structure G with b bags, each of size at most w and an FO sentence ϕ, there is an algorithm which, without ever constructing or inspecting G, operates on the co-decomposition and determines whether G ⊨ ϕ in time f_σ(w,|φ|)· b. We pair this algorithm with structural results on tree co-width, including its relationship to tree-width and a separation from twin-width. Furthermore, we characterize bounded path co-width using a graph grammar. In contrast to our logical meta-theorem, we prove that (s,t)-Path becomes NP-hard on co-decomposition inputs. These results demonstrate how categorical constructions can enable efficient computation on exponentially compressed structures.
ER -