From game comonads to dynamical systems: property-preserving maps as a logical unifying principle

Abstract

Logic and computer science share a subtle relationship that depends on both syntax and semantics. While structural generalisations often rely on semantics alone, computational aspects such as complexity and decidability hinge on the syntactic properties of formal languages. This interplay frequently manifests through relations between structures, which establish their similarity in various ways and for different purposes. In this work, we focus on three distinct forms of relations between structures: coKleisli morphisms, games, and truth-preserving maps. By coordinating these concepts and proving their equivalence, we apply them across diverse contexts, selecting the appropriate framework for each scenario. CoKleisli morphisms are used to derive generalised theorems, which can then be applied to specific instances; games are used as algorithmic descriptions, crucial when discussing computational complexity; and truth-preserving maps between structures are essential for achieving results such as the finite model property, completeness, and decidability. To a large extent, one must control all manners of structural relations in order to achieve all types of results. We contribute to each of these areas: We extend the use of coKleisli morphisms to ‘linear’ variants of previously studied comonads. Using these results, we derive a novel homomorphism counting theorem for pathwidth. We further establish preservation and characterisation theorems for non-branching variants of the modal comonad. Additionally, using event structures from concurrency theory, we propose a structural alternative to games, providing a more specialised framework for deriving the underlying comonads. For games and computational complexity, we define new model comparison games and establish complexity results for an all-in-one variant of the k-pebble game. Finally, we employ truth-preserving maps to prove completeness and decidability for highly expressive spatiotemporal languages within the context of dynamical systems.