Relating Structure to Power: An Invitation to Game Comonads

A week 1 course of ESSLLI 2022, sponsored by the European Association for Computer Science Logic (EACSL)

Taught jointly by Tomáš Jakl and Luca Reggio.

This course will introduce the emerging theory of game comonads, recently put forward by Abramsky, Dawar and their collaborators. Game comonads offer a novel approach to relating categorical semantics to finite model theory.

We will develop their basic theory and illustrate how they provide a structural and intrinsic account of several concrete notions that play a central role in finite model theory. These range from equivalence with respect to logic fragments (e.g., finite-variable, bounded quantifier rank, and modal fragments), to combinatorial parameters of structures (e.g., tree-width and tree-depth, or the height of a synchronization tree), and model comparison games (e.g., pebble, Ehrenfeucht-Fraïssé, and bisimulation games).

Course material

• Day 1 slides (Overview, Syntax vs Semantics)
• Day 2 slides (Games and Game Comonads)
• Day 3 slides (Coalgebras and Combinatorial Parameters)
• Day 4 slides (Logical Equivalences)
• Day 5 slides:
  • Future work + Lovasz’ homomorphism counting theorems
  • Arboreal categories and HPT
• Review of Category Theory
• Lecture notes, Chapter 1

Course overview

Lecture 1: Syntax and semantics: a fruitful duality

• 1.1 Theories and structures
• 1.2 Resource-bounded logics
• 1.3 On modal logic

Lecture 2: Games and game comonads

• 2.1 Ehrenfeucht-Fraïssé games
• 2.2 Pebble games
• 2.3 Bisimulation games
• 2.4 Game comonads
• 2.5 Strategies as co-Kleisli morphisms

Lecture 3: Coalgebras and combinatorial parameters

• 3.1 Forest covers and tree decompositions
• 3.2 Eilenberg–Moore coalgebras
• 3.3 Coalgebra numbers

Lecture 4: Game comonads and logical equivalences

• 4.1 The existential positive fragments
• 4.2 Bisimilarity
• 4.3 Equivalence in the full fragments
• 4.4 The equality symbol

Lecture 5: Advanced topics

• 5.1 Counting fragments
• 5.2 Lovász-type counting theorems
• 5.3 Arboreal categories

Prerequisites

Generally speaking, a certain degree of mathematical maturity is expected from the students. This includes familiarity with basic notions of discrete mathematics, such as sets, functions, relations, partial orders, and mathematical induction. Familiarity with more advanced topics in order theory, such as Galois connections between posets, would be useful but is not essential as the relevant notions will be recalled in the course. With regard to logic and category theory, the prerequisites are detailed below:

Logic: Basic familiarity with (classical) propositional and first-order logics is assumed, as well as with the concepts of syntax and semantics, as can be found in any textbook on the subject (a self-contained, albeit terse, account can be found in Section 2.1 of (Libkin, 2004). This includes, in particular, the ability to read a formula in first-order logic and interpret it in a model. A similar degree of acquaintance with modal logic (corresponding roughly to Sections 1.1–1.3 of (Blackburn–de Rijke–Venema, 2001) is desirable, although the relevant concepts will be reviewed.

Category theory: Familiarity with basic notions of category theory is a prerequisite for the course. These include the concepts of categories, functors, natural transformations, isomorphisms, monomorphisms, and epimorphisms. This material (and much more) can be found in the first two chapters of (Adámek–Herrlich–Strecker, 1990), or in Sections 1.1–1.5 of (Abramsky–Tzevelekos, 2011). Some familiarity with more advanced notions, such as adjunctions, limits, colimits, universal constructions, and comonads, is useful but not essential: these concepts will be motivated and introduced during the course through the examples of game comonads.

We provide a Review of Category Theory, for a quick reference of the basic topics that we will need throughout the course.

Guided Bibliography

Game comonads represent a recent advance in relating categorical semantics to finite model theory, and their study has gathered considerable momentum. As such, there is no single reference for their basic theory, which has been developed in a series of research articles. As a guide through the emerging theory of game comonads, we indicate some references relevant to the course, for those who might wish to explore some of the topics more fully.

For a gentle introduction to the fundamental ideas of game comonads, we warmly recommend the following survey:

• Abramsky, Whither semantics?, Theoretical Computer Science, Vol. 807, 2020. Preprint available at https://arxiv.org/abs/2010.13328.

The core of the course, focussing on game comonads, is based on the following research articles (in particular, we recommend (Abramsky–Shah, 2021) as the gateway to the basic results on game comonads):

• Abramsky, Dawar, Wang, The pebbling comonad in finite model theory, in the proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LiCS), 2017. Preprint available at https://arxiv.org/abs/1704.05124.
• Abramsky, Shah, Relating Structure and Power: Comonadic semantics for computational resources, in the proceedings of the 27th EACSL Annual Conference on Computer Science Logic (CSL), 2018. Freely available at https://drops.dagstuhl.de/opus/volltexte/2018/9669.
• Abramsky, Shah, Relating Structure and Power: Extended version, Journal of Logic and Computation, 31(6):1390–1428, 2021. Preprint available at https://arxiv.org/abs/2010.06496

The following more advanced articles on game comonads are also relevant, and at the end of the course the students will have the necessary background to undertake self-study:

• Paine, A pebbling comonad for finite rank and variable logic, and an application to the equirank-variable homomorphism preservation theorem, Electronic Notes in Theoretical Computer Science, 352:191–209, 2020. Freely available at https://doi.org/10.1016/j.entcs.2020.09.010.
• Abramsky, Marsden, Comonadic semantics for guarded fragments, in the proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LiCS), 2021. Preprint available at https://arxiv.org/abs/2008.11094.
• Abramsky, Reggio, Arboreal categories and resources, in the proceedings of the 48th International Colloquium on Automata, Languages and Programming (ICALP), 2021. Freely available at https://drops.dagstuhl.de/opus/volltexte/2021/14184/.
• Ó Conghaile, Dawar, Game comonads & generalised quantifiers, in the proceedings of the 29th EACSL Annual Conference on Computer Science Logic (CSL), 2021. Freely available at https://drops.dagstuhl.de/opus/volltexte/2021/13450.
• Dawar, Jakl, Reggio, Lovász-type theorems and game comonads, in the proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LiCS), 2021. Preprint available at https://arxiv.org/abs/2105.03274.
• Abramsky, Jakl, Paine, Discrete Density Comonads and Graph Parameters, In: H.H. Hansen, F. Zanasi (eds) Coalgebraic Methods in Computer Science. CMCS 2022. Lecture Notes in Computer Science, vol 13225. Springer, 2022. Preprint available at https://arxiv.org/abs/2205.06589.
• Montacute, Shah, The Pebble-Relation Comonad in Finite Model Theory, to appear (won the Kleene student paper award at LiCS 2022). Preprint available at https://arxiv.org/abs/2110.08196.
• Reggio, Polyadic sets and homomorphism counting, Preprint available at https://arxiv.org/abs/2110.11061.
• Jakl, Marsden, Shah, A game comonadic account of Courcelle and Feferman-Vaught-Mostowski theorems, Preprint available at https://arxiv.org/abs/2205.05387.
• Abramsky, Structure and Power: an emerging landscape, Preprint available at https://arxiv.org/abs/2206.07393.

The following monographs on category theory, finite model theory, and modal logic, are meant to guide the interested reader who may wish to learn more about these topics. Familiarity with these texts is not a prerequisite for the course (except for some basic concepts of logic and category theory, as detailed in the Prerequisites).

• Adámek, Herrlich, Strecker, Abstract and concrete categories, The joy of cats, Pure and Applied Mathematics, John Wiley & Sons, Inc., New York, 1990. xiv+482 pp. Online edition freely available at http://katmat.math.uni-bremen.de/acc/acc.pdf
• Abramsky, Tzevelekos, Introduction to categories and categorical logic, New Structures for Physics, B. Coecke (ed). Lecture Notes in Physics Vol. 813, pp. 3–94, Springer-Verlag, 2011. Preprint available at https://arxiv.org/abs/1102.1313
• Libkin, Elements of finite model theory, Texts in Theoretical Computer Science. An EATCS Series, Springer-Verlag, Berlin, 2004. xiv+315 pp. Freely available at https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf
• Blackburn, de Rijke, Venema, Modal logic, Cambridge Tracts in Theoretical Computer Science, Vol. 53, Cambridge University Press, Cambridge, 2001. xxii+554 pp.