Game comonads in Finite Model Theory
Tomáš Jakl, 4 Apr 2022
In recent years we have seen a growing number of examples of model comparison games (such as pebble games or Ehrenfreucht-Fraisse games) represented semantically, in terms of concrete operations on the class of graphs. Moreover, these operations satisfy the axioms of comonads. Comonads are a standard notion from category theory, with typical applications in programming language semantics and algebraic topology.
Apart from the connections with logic (via the model comparison games), game comonads can also express a range of important parameters in finite model theory and combinatorics, such as tree-width and tree-depth.
In my talk I will give an overview of the emerging theory of game comonads. To demonstrate the potential of combining tools from category theory and finite model theory, I will overview my recent work with Dan Marsden and Nihil Sham. We give a comonadic account of Courcelle’s theorem. As the main ingredient, we provide a toolkit for showing Feferman–Vaught-Mostowski-type theorems by lifting the tested constructions to the categories of coalgebras for our comonads.