Homomorphism Indistinguishability and Game Comonads for Restricted Conjunction and Requantification

A fundamental result in graph theory due to Lovász [25] states that two graphs $G$ and $H$ are isomorphic if and only if for every graph $F$ it holds $\mathrm{hom}(F,G)=\mathrm{hom}(F,H)$, where $\mathrm{hom}(F,G)$ denotes the number of homomorphisms from $F$ to $G$. More generally, $G$ and $H$ are said to be homomorphism indistinguishable over a graph class $ℱ$, denoted by $G{\equiv }_{ℱ}H$, if $\mathrm{hom}(F,G)=\mathrm{hom}(F,H)$ for all $F\in ℱ$. In this formulation, the seminal result of Lovász states that the equivalence relation ${\equiv }_{𝒢}$ is the same as graph isomorphism, where $𝒢$ is the class of all graphs. Understanding characterizations of the homomorphism indistinguishability relation ${\equiv }_{ℱ}$ not only deepens our understanding of various graph invariants but also informs algorithmic approaches to problems like graph isomorphism [32], subgraph counting [9], and counting answers to conjunctive queries [19]. In recent years, the relation ${\equiv }_{ℱ}$ was characterized for several graph classes $ℱ$ as a natural equivalence relation arising from logic and algebra. Notable examples include graphs of bounded treewidth [12, 13], bounded pathwidth [21, 27], bounded tree-depth [20, 21], and planar graphs [26]. Two central questions have emerged in this line of research and attract ongoing interest:

1. (1)

   How do structural properties of the class $ℱ$ relate to the semantics of the relation ${\equiv }_{ℱ}$?

This first question often admits elegant characterizations in terms of mathematical logic, particularly when the graph classes are defined via graph decompositions. In this context, logical equivalence provides a natural way to express homomorphism indistinguishability. For a logic on graphs $𝖫$, two graphs $G$ and $H$ are said to be $𝖫$-equivalent if they satisfy exactly the same sentences from $𝖫$. In [13] Dvořák shows that two graphs are homomorphism indistinguishable over the class of graphs of treewidth at most $k$ if and only if they are equivalent in the $k$-variable fragment ${𝖢}^k$ of first-order counting logic $𝖢$. The techniques developed in [13] have been refined in [17] to prove that homomorphism indistinguishability over the class ${𝒯}_q^k$ of graphs admitting tree-decompositions of width $k$ and depth $q$ is the same as equivalence in ${𝖢}_q^k$, the fragment of ${𝖢}^k$ of quantifier-rank at most $q$. The general technique is to directly translate between formulas in ${𝖢}_q^k$ and graphs from ${𝒯}_q^k$ by induction on the structure of formulas and tree decompositions in both directions.

Beyond the characterization of homomorphism indistinguishability relations, the following natural question is fundamental to understand these relations:

1. (2)

   When do different graph classes $ℱ$ induce the same indistinguishability relation ${\equiv }_{ℱ}$?

This second question was approached methodically by Roberson [31] via introducing the notion of homomorphism distinguishing closedness. A graph class $ℱ$ is called homomorphism distinguishing closed (also h.d. closed) if for every graph $F\notin ℱ$ there exist graphs $G,H$ with $G{\equiv }_{ℱ}H$ and $\mathrm{hom}(F,G)\ne \mathrm{hom}(F,H)$, i.e., if no graphs can be added to $ℱ$ without changing the relation ${\equiv }_{ℱ}$. The significance of this notion is that any two distinct homomorphism distinguishing closed classes must induce distinct homomorphism indistinguishability relations. In turn, equivalence relations on graphs characterized by homomorphism indistinguishability can be separated by separating the underlying graph classes, given they are homomorphism distinguishing closed. In general, it appears to be a hard task to establish that a given class is homomorphism distinguishing closed, leading to only a short list of known examples. These include the class of graphs of bounded degree [31], bounded tree-depth [17], bounded treewidth [29], bounded depth treewidth [5], and essentially profinite classes [35]. Beyond the investigation of specific graph classes, in [35] the relation between closure properties of $ℱ$ and preservation properties of ${\equiv }_{ℱ}$ was studied systematically guided by the two aforementioned main questions. In [31] Roberson conjectures that every graph class which is closed under taking disjoint unions and minors is homomorphism distinguishing closed. For certain such graph classes $ℱ$, homomorphism distinguishing closedness has been successfully proven when ${\equiv }_{ℱ}$ is characterized by a model-comparison game and membership in $ℱ$ is determined by a pursuit-evasion game. A key tool in such proofs is the CFI-construction [8], which has been instrumental in separating the homomorphism indistinguishability relations of ${𝖢}^k$-equivalence and ${𝖢}^{k+1}$-equivalence. For a graph $G$, the construction yields two CFI-graphs $X(G)$ and $\tilde{X}(G)$ for which their distinguishability by ${𝖢}^k$ depends on the structural complexity of $G$. Crucial technical challenges arise, particularly in proving the connection between pursuit-evasion and model-comparison games for the CFI-construction (see [29]) and establishing the monotonicity of pursuit-evasion games (see [5]). The monotonicity of a game ensures that when searchers have a winning strategy, the reachable positions for the evading player only decreases as the game progresses.

For many logics of interest in finite model theory, like ${𝖢}_q^k$, their equivalence can be characterized in terms of model-comparison games such as Ehrenfeucht–Fraïssé or pebble games (see [15]). This correspondence was utilized in [2] to give a novel approach to logical resources in terms of game comonads. The central observation is that model-comparison games induce comonads on categories of relational structures. In this framework, several essential constructions from finite model theory can be given a categorical account, see [3] for a survey. In particular, coalgebras for some game comonads encode combinatorial parameters of structures [4] leading to a uniform approach to homomorphism indistinguishability developed in [11]. There, the first characterization of ${𝖢}_q^k$-equivalence by homomorphism counts was shown for graphs admitting pebble forest covers. The comonadic approach was recently used to show a categorical characterization of the graph parameter pathwidth and prove that homomorphism indistinguishability over graphs of pathwidth at most $k$ is logical equivalence in the restricted conjunction logic $\wedge {𝖢}^k$ [27] by building on previous work of Dalmau [10].

The concept of requantification, recently introduced in [30], allows for a more refined view on stratification by logical resources in finite variable counting logics. The logic ${𝖢}^{(k_1,k_2)}$ is defined as the fragment of $𝖢$ using at most $k_1+k_2$ distinct variables of which only $k_1$ may be requantified, i.e. quantified within scopes of their own quantification. To analyze the expressive power of ${𝖢}^{(k_1,k_2)}$, the bijective $(k_1,k_2)$-pebble game ${\mathrm{BP}}^{(k_1,k_2)}$ and the $q$-round $(k_1,k_2)$-cops-and-robber game ${\mathrm{CR}}_q^{(k_1,k_2)}$ were introduced, incorporating reusability into model-comparison and pursuit-evasion games, respectively. In the context of Question (1), it is only natural to ask whether logics with restricted conjunction and requantification admit homomorphism indistinguishability characterizations. Subsequently, Question (2) asks whether the corresponding graph classes are homomorphism distinguishing closed.

We write $\mathbb{N}=\{0,1,2,\mathrm{\dots }\}$ for the set of natural numbers, ${\mathbb{N}}_{+}=\mathbb{N}\setminus \{0\}$ for the set of positive integers, and for $n\in {\mathbb{N}}_{+}$ we define $[n]≔\{1,\mathrm{\dots },n\}$. Unless stated explicitly otherwise, we let $k_1,k_2\in \mathbb{N}$ throughout the paper. We fix the variable sets (also called pebble sets) $[x_{k_1}]≔\{x_1,\mathrm{\dots },x_{k_1}\}$, $[y_{k_2}]≔\{y_1,\mathrm{\dots },y_{k_2}\}$, and $[x_{k_1},y_{k_2}]≔\{x_1,\mathrm{\dots },x_{k_1},y_1,\mathrm{\dots },y_{k_2}\}$. For the following definitions we let $V$ be a set. We write $2^V$ for the power set of $V$ and set $\left(\genfrac{}{}{0pt}{}{V}{2}\right)=\{U\in 2^V:|U|=2\}$. A partial function $\alpha :[x_{k_1},y_{k_2}]\rightharpoonup V$ assigns to every variable $z\in [x_{k_1},y_{k_2}]$ at most one element $\alpha (z)\in V$. If $\alpha$ does not assign an element to $z$, we write $\alpha (z)=\perp$. Also, we write $\mathrm{im}(\alpha )$ and $\mathrm{dom}(\alpha )$ for the image and domain of $\alpha$ respectively. We write $V^{+}$, $V^n$ and $V^{\le n}$ for the sets of non-empty finite sequences, sequences of length $n$, and sequences of length at most $n$ over $V$ respectively. We denote sequences of elements $s_1,\mathrm{\dots },s_n\in V$ by $\overline{s}=[s_1,\mathrm{\dots },s_n]\in V^n$ and for $\overline{s},\overline{t}\in V^{+}$ we write $\overline{s}⊑\overline{t}$ if $\overline{s}$ is a prefix of $\overline{t}$. The concatenation of $\overline{s}$ and $\overline{t}$ is denoted by $\overline{s}\overline{t}$. For $i,j\in [n]$ with $i\le j$ we define $\overline{s}[i,j]≔[s_i,s_{i+1},\mathrm{\dots },s_j]$ and $\overline{s}[i]≔s[i,i]$. Also, we indicate that $s_i$ occurs in $\overline{s}$ by writing $s_i\in \overline{s}$. For a variable $z\in [x_{k_1},y_{k_2}]$ and $v\in V$ we write $\alpha [z/v]$ for the partial function that is obtained from $\alpha$ by replacing the image $\alpha (z)$ by $v$. Given a sequence $\overline{s}=[(z_1,v_1),\mathrm{\dots },(z_n,v_n)]\in {([x_{k_1},y_{k_2}]\times V)}^n$ and $z\in [x_{k_1},y_{k_2}]$ we denote by ${\mathrm{last}}_z(\overline{s})$ the $v_i$ with the largest index $i$ such that $(z,v_i)\in \overline{s}$. We call the first entry of each element in $\overline{s}$ a pebble index or variable index. For a proposition $P$, we use the Iverson bracket $[P]\in \{0,1\}$ to indicate whether $P$ is satisfied.

In this section, we introduce several graph decompositions that incorporate constraints on reusability of vertices within the parts of each decomposition. Specifically, we define four distinct types of decompositions, each of which comes in two variants corresponding to two underlying structural models: the path model and the (bounded-depth) tree model. Each decomposition is parameterized by two values: $k_1$, representing the number of reusable resources, and $k_2$, representing the number of non-reusable resources. Our goal is to show that, for each of the two models, the corresponding decompositions define the same graph class with aligned parameters. This equivalence allows us to explore the concept of reusability in graph decompositions from multiple, yet consistent, perspectives. The motivation for each decomposition arises from its significance in homomorphism indistinguishability over the associated graph class, establishing a unifying theme for our study. In Table 1 we summarize the significance of the various decompositions introduced in this section for our results on homomorphism indistinguishability.

We begin by introducing the notion of exception sets for tree decompositions of bounded depth and for path decompositions. The key idea is to generalize the concept of a tree decomposition of width $k_1$ by permitting up to $k_2$ exceptions along each branch of the underlying tree. However, there is an important restriction: if a vertex is designated as an exception at some node $t$ in the rooted tree decomposition, then it must remain fixed, i.e., cannot be replaced by a different vertex at any descendant of $t$. In this sense, the exception status is not reusable along the subtree rooted at $t$.

For $k_2=0$ we recover the class ${𝒯}^{(k_1+1,0)}$ of graphs of treewidth at most $k_1$ but for $k_2>0$ we allow the technical nuisance of having $k_1=-1$ in order to avoid a case distinction.

Note that for the width of a path decomposition we only require the existence of one single set $S$ of exceptions. Thus, for fixed $k_1$ the class of graphs admitting a path decomposition of width $(k_1,k_2)$ can be seen as an approximation of the class of graphs of pathwidth at most $k_1$ up to deleting $k_2$ vertices.

Next, we extend the notion of pebble forest covers to incorporate the concept of reusability. Originally introduced in [2] as $k$-traversals, these structures provide a combinatorial characterization of coalgebras over the pebbling comonad ${\mathbb{P}}^k$, finally demonstrating how the comonadic structure of ${\mathbb{P}}^k$ can be used to characterize treewidth. Our aim is to follow a similar approach to characterize reusability (specifically, width $(k_1,k_2)$) within tree decompositions of bounded depth via comonadic methods. To this end, we use non-reusable pebbles $y_1,\mathrm{\dots },y_{k_2}$, which mark fixed positions in a forest cover that cannot be reassigned, thereby encoding the non-reusability constraint directly into the structure.

The tree-depth of a graph $G$ is the minimum $q$ such that $G$ has a forest cover of depth at most $q$ (see [28]). The class of graphs of tree-depth at most $q$ is denoted by ${𝒯}_q$.

The classes ${𝒫}^{(k,0)}$, ${𝒯}^{(k,0)}$, and ${𝒯}_q$ admit characterizations in terms of pursuit-evasion games by [37], [6, 22], and [18] respectively. The characterization of ${𝒯}^{(k,0)}$ was refined to ${𝒯}_q^{(k,0)}$ in [17]. In [30] a cops-and-robber game with constraints on the reusability of cops and the number of rounds was introduced. We recall its definition and also modify it to match the game-theoretic characterization of ${𝒫}^{(k,0)}$.

A winning strategy of the searchers in the game ${\mathrm{NS}}^{(k_1,k_2)}(G)$ can be specified as a sequence of positions ${\gamma }_1,\mathrm{\dots },{\gamma }_m:[x_{k_1},y_{k_2}]\rightharpoonup V(G)$ while in the game ${\mathrm{CR}}^{(k_1,k_2)}$ the cop strategy depends on the moves of the robber and therefore each position ${\gamma }_i$ additionally depends on the robber position $v_i$ in round $i$. The proof of [30, Theorem 15] hinges on this fact and shows that in the game ${\mathrm{CR}}^{(k_1,k_2)}$ the use of non-reusable cops is restricted to a pattern involving arbitrarily long sequences of reusing all reusable cops before utilizing a new non-reusable cop. We show that the situation is entirely different for ${\mathrm{NS}}^{(k_1,k_2)}$ due to the invisibility of the fugitive.

To prove the characterization of a graph parameter by a pursuit-evasion game an important step often is to establish that the respective game is monotone. Alongside this, in some cases proving the monotonicity of a game is the crucial step in establishing homomorphism distinguishing closedness of the associated graph class, see [5, 17] for a discussion. Our goal is to show monotonicity of the games introduced here in order to utilize this property to prove game-theoretic characterizations of ${𝒫}^{(k_1,k_2)}$ and ${𝒯}_q^{(k_1,k_2)}$ towards homomorphism distinguishing closedness. The monotonicity of ${\mathrm{NS}}^{(k_1,0)}$ was proven in [23] and recently [5] established the monotonicity of ${\mathrm{CR}}_q^{(k_1,0)}(G)$. We build on top of these results to show that reusability is compatible with monotonicity by replacing parts of winning strategies by monotone strategies. The notion of monotonicity we use here is usually referred to as robber-monotonicity in the literature.

To characterize homomorphism indistinguishability over the class ${𝒯}_q^{(k,0)}$, in [17] the notion of construction trees was introduced, building on techniques from [13]. We extend this concept to accommodate the classes ${𝒯}_q^{(k_1,k_2)}$ and ${𝒫}^{(k_1,k_2)}$. This generalized definition forms the basis of our framework for analyzing homomorphism indistinguishability over these broader classes.

We obtain the following characterizations for the classes ${𝒯}_q^{(k_1,k_2)}$ and ${𝒫}^{(k_1,k_2)}$, showing that all previous definitions are equivalent for unlabeled graphs.

We observe that classes the ${𝒯}_q^{(k_1,k_2)}$ and ${𝒫}^{(k_1,k_2)}$ admit usual closure properties, except that ${𝒫}^{(k_1,k_2)}$ is not closed under taking disjoint unions.

The class ${𝒫}^{(k_1,k_2)}$ formalizes the notion of reusability for path decompositions in an appropriate sense as exemplified by the characterization through ${\mathrm{NS}}^{(k_1,k_2)}$. However, to overcome the obstacle that this class is not closed under disjoint unions we define the class $\dot{\cup }{𝒫}^{(k_1,k_2)}$ as the closure of ${𝒫}^{(k_1,k_2)}$ under disjoint unions. This class formalizes the notion of restricted reusability componentwise on a graph. The next proposition, which follows directly from Theorem 3.7, makes this explicit.

In this section, we characterize homomorphism indistinguishability over the classes ${𝒫}^{(k_1,k_2)}$ and ${𝒯}_q^{(k_1,k_2)}$ by logics with restricted requantification. We start by giving the definition of finite variable counting logic with restricted conjunction and requantification, extending a definition from [27].