The pebbling comonad in finite model theory

TL;DR

This paper introduces a comonadic framework for pebble games in finite model theory, linking categorical structures with logical equivalences, graph properties, and semantics, thus bridging model theory and computation semantics.

Contribution

It provides a novel comonadic formulation of pebble games, characterizing logical equivalences, graph parameters, and semantics within a categorical framework.

Findings

Characterizes elementary equivalence via coKleisli morphisms.

Relates structure treewidth to coalgebra number in the comonad.

Connects pebbling comonads to semantics of a modal operator.

Abstract

Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential k-pebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for structures A and B are equivalent to morphisms from A to B in the coKleisli category for this comonad. This leads on to comonadic characterisations of a number of central concepts in Finite Model Theory: - Isomorphism in the co-Kleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers. - Symmetric games corresponding to equivalence in full k-variable logic are also characterized. - The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad. - Co-Kleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-F\"urer-Immerman construction. - The k-pebbling comonad is also used to give semantics to a novel modal operator. These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation.

Equations

$$[(p_1,a_1),\dots ,(p_n,a_n)]\mapsto [(p_1,f(a_1)),\dots ,(p_n,f(a_n))].$$

$${\delta }_A:s\mapsto [(p_1,s_1),\dots ,(p_n,s_n)].$$

$$\begin{diagram}\qquad\qquad\begin{diagram}$$

$${\epsilon }_A:{\mathbb{T}}_{k}A\text{rTo}A.$$

$$f^{\ast }:[(p_1,a_1),\dots ,(p_n,a_n)]\mapsto [(p_1,f(s_1)),\dots ,(p_n,f(s_n))]$$

$$\begin{diagram}\qquad\qquad\begin{diagram}$$

$$QA\to B⟺A{\to }_{2}B.$$

$$\gamma[p\mapsto(a,b)](q)=\left\{\begin{array}[]{lr}(a,b),&p=q\\ \gamma(q)&p\neq q\end{array}\right.$$

$${\theta }_f(s)=\mathsf{position}(s,f^{\ast }(s)).$$

$${\gamma }_0\text{rTo}\cdots \text{rTo}{\gamma }_n$$

$$S_f:=\{{\theta }_f(s)\mid s\in {\mathbb{T}}_{k}A\}\cup \{\varnothing \},$$

$$\gamma ={\theta }_f(s).$$

$$\gamma {\text{rTo}}^{(p,a):b}{\gamma }^{\prime }={\theta }_f(s[(p,a)])\in S_f.$$

$$Y:=\{b\in X\mid \exists t=t^{\prime }[(p,a)]⊑s.{\theta }_f(t^{\prime })=\gamma \wedge f(t)=b\}.$$

$$f(s[(p,a)])=\left\{\begin{array}[]{ll}\min_{B}(X\setminus Y),&X\setminus Y\neq\varnothing\\ \min_{B}(X),&\mbox{otherwise.}\end{array}\right.$$

$$R(\gamma ):=\{\gamma (p)\mid p\in \mathrm{dom}(\gamma )\}\subseteq A\times B$$

$$\gamma {\text{rTo}}^{(p,a):b}{\gamma }^{\prime }.$$

$$\Phi(U)\;=\;\left\{\begin{array}[]{l}\{\varnothing\}\;\cup\\ \{\gamma^{\prime}\mid\exists\gamma\in U,(p,a)\in[k]\times A.\,\gamma\rTo^{(p,a):\theta_{\gamma}(p,a)}\gamma^{\prime}\}\end{array}\right.$$

$$A{\equiv }^{\mathcal{L}}B\stackrel{\Delta }{⟺}\forall \phi \in \mathcal{L}.A\models \phi ⟺B\models \phi .$$

$$A{\rightleftarrows }_{k}B\stackrel{\Delta }{⟺}A{\to }_{k}B\wedge B{\to }_{k}A.$$

$$A{\rightleftarrows }_k^{i}B⟺A{\rightleftarrows }_k^{s}B⟺A{\to }_k^{b}B⟺A{\cong }_{\mathcal{K}}B.$$

$$A{\cong }_{\mathcal{K}}B⟺A{\equiv }^{C^k}B.$$

$$A{\rightleftarrows }_k^{-}B⟺A{\equiv }^{k}B.$$

$$\kappa (A)=\mathsf{tw}(A)+1.$$

$$\pi (A)=\mathsf{tw}(\mathsf{core}(A))+1.$$

$$\mathsf{tw}(\mathsf{core}(A))<k⟺\pi (a)\le k.$$

$$A\to T_{k}A\to B.$$

$$R_0=\{(a,i),(b,j),(c,k)\mid (a,b,c)\in R_0^A\wedge i\oplus j\oplus k=0\}$$

$$R_1=\{(a,i),(b,j),(c,k)\mid (a,b,c)\in R_1^A\wedge i\oplus j\oplus k=0\}.$$

$$R_0=\{(a,i),(b,j),(c,k))\mid (a,b,c)\in R_0^A\wedge i\oplus j\oplus k=0\}$$

Full text

• •

Isomorphism in the co-Kleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers.

• •

Symmetric games corresponding to equivalence in full k-variable logic are also characterized.

• •

The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad.

• •

Co-Kleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-Fürer-Immerman construction.

• •

The k-pebbling comonad is also used to give semantics to a novel modal operator.

These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation.

††publicationid: pubid: 978-1-5090-3018-7/17/$31.00  ©2017 IEEE

1 Introduction

Homomorphisms play a fundamental rôle in finite model theory, constraint satisfaction and database theory. The existence of a homomorphism $A\rightarrow B$ is an equivalent formulation of the basic CSP problem [1, 2, 3]. There is an equivalence between the existence of a homomorphism, and the property that every existential positive sentence satisfied by $A$ is also satisfied by $B$ [2]. Such sentences correspond to (disjunctions of) conjunctive queries, which are fundamental in database theory [4, 5].

One of the key tools in studying these notions is that of existential $k$-pebble games [6]. Such a game, for structures $A$, $B$, proceeds by Spoiler placing one of his $k$ pebbles on an element of the universe of $A$. Duplicator then places one of her pebbles on an element of $B$. If Duplicator is always able to move so that the partial mapping from $A$ to $B$ defined by sending $a_{i}$, the element in $A$ carrying the $i$’th Spoiler pebble, to $b_{i}$, the corresponding element of $B$ carrying the $i$’th Duplicator pebble, is a homomorphism on the induced substructures, then Duplicator has a winning strategy.

Proposition 1** ([6]).**

The following are equivalent:

• •

Duplicator has a winning strategy in the existential $k$-pebble game.

• •

Every sentence of the existential positive $k$-variable fragment of first-order logic satisfied by $A$ is also satisfied by $B$.

Our aim in this paper is to study these notions from a novel perspective, using the notion of comonad from category theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming [7, 8, 9]. We show that existential $k$-pebble games have a natural comonadic formulation. Given a structure $A$ over a relational signature $\sigma$, we shall introduce a new structure $\mathbb{T}_{k}A$ corresponding to Spoiler playing his part of an existential $k$-pebble game on $A$, with the potential codomain $B$ left unspecified. The idea is that we can exactly recover the content of a Duplicator strategy in $B$ by giving a homomorphism from $\mathbb{T}_{k}A$ to $B$. Thus the notion of local approximation built into the $k$-pebble game is internalised into the category of $\sigma$-structures and homomorphisms. Formally, this construction will be shown to give a comonad on this category, which guarantees a wealth of further structural properties. This leads to comonadic characterisations of a number of central concepts in Finite Model Theory.

In Section 2, we introduce the pebbling comonads $\mathbb{T}_{k}$, which are graded by the number of pebbles $k$, and characterize their coalgebras. $\mathbb{T}_{k}A$ is always infinite. In Section 3, we prove a no-go theorem, to rule out any finite version. In Section 4, we show that the question of whether a morphism $\mathbb{T}_{k}A\rightarrow B$ exists is equivalent to the existence of a winning strategy for the existential $k$-pebble game for $A$ and $B$. We also show how this question can be finitized, and such morphisms can be realized by deterministic finite-state transducers. In Section 5 we study various notions of equivalence of structures, and show that isomorphism in the coKleisli category for $\mathbb{T}_{k}$ coincides with elementary equivalence for $C^{k}$, the $k$-variable logic with counting quantifiers, which plays a central rôle in finite model theory. We also show that the equivalence of structures $A$ and $B$ for full $k$-variable logic is characterized by the existence of a pair of morphisms $\mathbb{T}_{k}A\rightarrow B$ and $\mathbb{T}_{k}B\rightarrow A$ satisfying a certain condition. This is important, as it shows that symmetric, back-and-forth game conditions also fall within the scope of the comonadic approach. In Section 6, we characterise treewidth, a combinatorial parameter which plays a pervasive rôle in algorithmic graph theory, in terms of the coalgebra number of a structure $A$: the least index $k$ such that there is a coalgebra $A\rightarrow\mathbb{T}_{k}A$. Section 7 characterizes the weaker condition of existence of a homomorphism from $A$ to $\mathbb{T}_{k}A$ in terms of the treewidth of the core of $A$. Section 8 discusses strong $k$-consistency, and gives a Cai-Fürer-Immerman construction in terms of coKleisli morphisms. In Section 9, we introduce the novel modality $\Box_{k}$, which can be read as “it is $k$-locally the case that”, and give its semantics using the pebbling comonad. Section 10 concludes.

Overall, these results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation.

Notation and Background

We have attempted to make this paper accessible to non-specialists in category theory. We assume only very basic background in category theory (see e.g. [10, 11]), essentially the definitions of category and functor, spelling out other definitions as needed.

We also assume only basic background in (finite) model theory (see e.g. [1]). We use the letters $A$, $B$ for $\sigma$-structures over some relational signature $\sigma$, not distinguishing notationally between the structures and their universes. The interpretation of a relation $R\in\sigma$ in a structure $A$ is denoted by $R^{A}$. Our morphisms between structures will always be homomorphisms. We use $\mathcal{L}^{k}_{\infty,\omega}$ to denote the $k$-variable fragment of first-order logic extended with infinite disjunctions and conjunctions, $\exists^{+}\mathcal{L}^{k}_{\infty,\omega}$ for its existential positive fragment (no universal quantifiers or negations), and $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$ for the corresponding fragment of first-order logic.

We use the notation $[n]:=\{1,\ldots,n\}$, and $s\sqsubseteq t$ for the prefix ordering on sequences. If $s\sqsubseteq t$, there is a unique $s^{\prime}$ such that $ss^{\prime}=t$, which we refer to as the suffix of $s$ in $t$.

2 The Pebbling Comonad

For the remainder of the paper, we fix a finite relational signature $\sigma$. Our main setting is $\mathcal{R}(\sigma)$, the category whose objects are $\sigma$-structures, and whose morphisms are homomorphisms of $\sigma$-structures. We shall work in $\mathcal{R}(\sigma)$ and various sub-categories thereof, in particular $\mathcal{R}_{f}(\sigma)$, the category of finite $\sigma$-structures. By “structure”, we always mean $\sigma$-structure.

Firstly, we can consider the set of all plays in $A$ by the Spoiler. This can be represented by $([k]\times A)^{+}$, the set of finite non-empty sequences of moves $(p,a)$, where $p\in[k]$ is a pebble index, and $a\in A$. We shall use the notation $s=[(p_{1},a_{1}),\ldots,(p_{n},a_{n})]$ for these sequences. The set of plays forms the universe of $\mathbb{T}_{k}A$.

To complete the definition of $\mathbb{T}_{k}A$, we must define the relational structure on this universe. For simplicity, we first consider the case of a binary relation $E$. We define $E^{\mathbb{T}_{k}A}$ to be the set of pairs of plays $s,t\in\mathbb{T}_{k}A$ such that

• •

$s$ and $t$ are comparable in the prefix ordering, so $s\sqsubseteq t$ or $t\sqsubseteq s$.

• •

If $s\sqsubseteq t$, then the pebble index of the last move in $s$ does not appear in the suffix of $s$ in $t$; and symmetrically if $t\sqsubseteq s$.

• •

$E^{A}(\varepsilon_{A}(s),\varepsilon_{A}(t))$, where $\varepsilon_{A}:\mathbb{T}_{k}A\rTo A$ sends a play $[(p_{1},a_{1}),\ldots,(p_{n},a_{n})]$ to $a_{n}$, the $A$-component of its last move.

To understand the second condition in this definition, note that for each pebble index $p$, only the last move with pebble index $p$ is relevant to the current position. The idea is that, in placing pebble $p$ on element $a$, Spoiler has to first remove it from its previous position. This is exactly the way in which the pebble game models bounded resources.

The extension to relations of arbitrary arity is straightforward. Given an $m$-ary relation $R\in\sigma$, $R^{\mathbb{T}_{k}A}(s_{1},\ldots,s_{m})$ if the $s_{i}$ are pairwise comparable in the prefix ordering, and hence form a chain with greatest element $s$; the pebble index of the last move in each $s_{i}$ does not appear in the suffix of $s_{i}$ in $s$; and $R^{A}(\varepsilon_{A}(s_{1}),\ldots,\varepsilon_{A}(s_{m}))$.

The following is immediate from our definition.

Proposition 2**.**

The map $\varepsilon_{A}:\mathbb{T}_{k}A\rTo A$ is a homomorphism.

We now extend $\mathbb{T}_{k}$ to a functor $\mathbb{T}_{k}:\mathcal{R}(\sigma)\rTo\mathcal{R}(\sigma)$ by defining its action on morphisms. If $f:A\rTo B$ is a homomorphism, we define $\mathbb{T}_{k}f:\mathbb{T}_{k}A\rTo\mathbb{T}_{k}B$ to be the map

[TABLE]

It is clear that this is a homomorphism from $\mathbb{T}_{k}A$ to $\mathbb{T}_{k}B$. Moreover, it is easily verified that $\mathbb{T}_{k}(g\circ f)=\mathbb{T}_{k}(g)\circ\mathbb{T}_{k}(f)$, and $\mathbb{T}_{k}(\mathsf{id}_{A})=\mathsf{id}_{\mathbb{T}_{k}A}$, so $\mathbb{T}_{k}$ is a functor.

We have already defined the homomorphism $\varepsilon_{A}:\mathbb{T}_{k}A\rTo A$ for each structure $A$. We now note that this defines a natural transformation. That is, for each homomorphism $f:A\rTo B$, the following diagram commutes. {diagram} Now for each structure $A$, we define a map $\delta_{A}:\mathbb{T}_{k}A\rTo\mathbb{T}_{k}\mathbb{T}_{k}A$, as follows. Given a play $s=[(p_{1},a_{1}),\ldots,(p_{n},a_{n})]$, define $s_{i}=[(p_{1},a_{1}),\ldots,(p_{i},a_{i})]$, $i=1,\ldots,n$. Then we define

[TABLE]

Proposition 3**.**

For each $A$, $\delta_{A}$ is a homomorphism. Moreover, $\delta$ is a natural transformation: for each homomorphism $f:A\rTo B$, the following diagram commutes. {diagram}

Proof.

This is a straightforward unfolding of the definitions. Starting with a play $[(p_{1},a_{1}),\ldots,(p_{n},a_{n})]\in\mathbb{T}_{k}A$, going either way around the diagram results in $[(p_{1},t_{1}),\ldots,(p_{n},t_{n})]$, where $t_{i}=[(p_{1},f(a_{1})),\ldots,(p_{i},f(a_{i}))]$, $i=1,\ldots,n$. ∎

The natural transformation $\varepsilon$ is the counit of the comonad, while $\delta$ is the comultiplication.

We can now gather these elements together to complete our construction.

Theorem 4**.**

The triple $(\mathbb{T}_{k},\varepsilon,\delta)$ forms a comonad on the category $\mathcal{R}(\sigma)$.

Proof.

The remaining points to be verified from the definition of a comonad are that the following diagrams commute, for all objects $A$ of $\mathcal{R}(\sigma)$.

[TABLE]

While these diagrams look somewhat formidable, verification that they commute again reduces to a straightforward diagram chase. For the first diagram, starting with a play $[(p_{1},a_{1}),\ldots,(p_{n},a_{n})]\in\mathbb{T}_{k}A$, either way around the diagram takes us to $[(p_{1},t_{1}),\ldots,(p_{n},t_{n})]$, where $s_{i}=[(p_{1},a_{1}),\dots,(p_{i},a_{i})]$, $t_{i}=[(p_{1},s_{1}),\ldots,(p_{i},s_{i})]$, $i=1,\ldots n$. ∎

2.1 The Co-Kleisli Category

We now turn to one of the fundamental constructions associated with a comonad, the co-Kleisli category [12]. We use the notation $\mathcal{K}(\mathbb{T}_{k})$ for this category. The objects are the same as those of $\mathcal{R}(\sigma)$, while a morphism from $A$ to $B$ in $\mathcal{K}(\mathbb{T}_{k})$ is a $\mathcal{R}(\sigma)$-morphism $f:\mathbb{T}_{k}A\rTo B$. Given morphisms $f:\mathbb{T}_{k}A\rTo B$ and $g:\mathbb{T}_{k}B\rTo C$, we use the comonad structure to compose them: {diagram} The identity morphisms are given by the counit of the comonad:

[TABLE]

We write $A\rightarrow_{k}B$ if there exists a morphism from $A$ to $B$ in $\mathcal{K}(\mathbb{T}_{k})$.

The Kleisli coextension

The operation $f\mapsto\mathbb{T}_{k}f\,\circ\,\delta_{A}$ which sends $f:\mathbb{T}_{k}A\rTo B$ to $f^{*}:\mathbb{T}_{k}A\rTo\mathbb{T}_{k}B$ is known as the Kleisli coextension. Comonads have an alternative presentation in terms of this operation and the counit maps [7]. For our purposes, it will be useful to have a concrete description of this operation. Given a co-Kleisli morphism $f:\mathbb{T}_{k}A\rTo B$,

[TABLE]

where $s_{i}=[(p_{1},a_{1}),\dots,(p_{i},a_{i})]$, $i=1,\ldots n$.

2.2 Grading

We have defined a comonad $\mathbb{T}_{k}$ for each positive integer $k$. We now consider how these are related.

We can think of the morphisms $f:A\rTo B$ in the co-Kleisli category for $\mathbb{T}_{k}$ as those which only have to respect the $k$-local structure of $A$. The lower the value of $k$, the less information available to Spoiler, and the easier it is for Duplicator to have a winning strategy. Equivalently by Theorem 13, the easier it is to have a homomorphism $\mathbb{T}_{k}A\rTo B$, i.e. a morphism from $A$ to $B$ in the co-Kleisli category. This leads to a natural weakening principle: if we have a morphism from $\mathbb{T}_{k}A$ to $B$, then this should yield a morphism from $\mathbb{T}_{l}A$ to $B$ when $l<k$.

This idea is directly captured in our construction. There is an inclusion $i^{l,k}_{A}:\mathbb{T}_{l}A\rinc\mathbb{T}_{k}A$ whenever $l\leq k$. The following is easily verified.

Proposition 5**.**

The inclusion maps form a natural transformation $i^{l,k}:\mathbb{T}_{l}\rTo^{\cdot}\mathbb{T}_{k}$ which is a morphism of comonads, i.e. it preserves the counit and comultiplication.

This supports the weakening principle mentioned above. Given a morphism $f:\mathbb{T}_{k}A\rTo B$, we have a morphism {diagram}

2.3 Coalgebras

Another fundamental aspect of comonads is that they have an associated notion of coalgebra. A coalgebra for $\mathbb{T}_{k}$ is a morphism $\alpha:A\rTo\mathbb{T}_{k}A$ such that the following diagrams commute:

[TABLE]

Note in particular that a coalgebra structure on $A$ makes it a retract of $\mathbb{T}_{k}A$ via the counit $\varepsilon_{A}$.

A morphism of coalgebras from $(A,\alpha)$ to $(B,\beta)$ is a morphism $h:A\rTo B$ such that the following diagram commutes: {diagram}

Coalgebras and their morphisms form a category $\mathcal{R}(\sigma)^{\mathbb{T}_{k}}$, the Eilenberg-Moore category for the comonad $\mathbb{T}_{k}$. This provides another way of looking at the co-Kleisli category. We can think of the objects in it as the cofree coalgebras $\mathbb{T}_{k}A$, with structure maps given by comultiplication. Note that the diagrams for a comonad instantiate those for a coalgebra when we take the coalgebra to be $(\mathbb{T}_{k}A,\delta_{A})$. The morphisms are then taken to be the coalgebra morphisms $h:\mathbb{T}_{k}A\rTo\mathbb{T}_{k}B$. This is equivalent to the usual presentation, since we can pass from $f:\mathbb{T}_{k}A\rTo B$ to its Kleisli coextension $f^{*}=Tf\circ\delta_{A}:\mathbb{T}_{k}A\rTo\mathbb{T}_{k}B$, and from a coalgebra morphism $h:\mathbb{T}_{k}A\rTo\mathbb{T}_{k}B$ to $\varepsilon_{A}\circ h:\mathbb{T}_{k}A\rTo B$, and these two passages are mutually inverse. This representation displays the co-Kleisli category explicitly as a full subcategory of the Eilenberg-Moore category.

Note that a coalgebra structure $\alpha$ on $A$ implies that a homomorphism exists from $A$ to $B$ whenever a homomorphism exists from $\mathbb{T}_{k}A$ to $B$. Given $h:\mathbb{T}_{k}A\rTo B$, we can form $h\circ\alpha:A\rTo B$. Thus we should only expect a coalgebra structure to exist when the $k$-local information on $A$ is sufficient to determine the structure of $A$.

Given a structure $A$, we define a $k$-traversal of $A$ to be a structure $(A,{\leq},i)$, where $\leq$ is a partial order on $A$ which is a tree order, i.e. for each $a\in A$, the predecessors of $a$ in the order form a chain; and $i:A\rightarrow[k]$ is a labelling map such that, whenever $a$ is adjacent to $b$ in the Gaifman graph of $A$, $a$ is comparable to $b$, say $a\leq b$, and for all $c$ such that $a<c\leq b$, $i(a)\neq i(c)$.

Theorem 6**.**

Let $A$ be a finite structure. There is a bijective correspondence between

coalgebras $\alpha:A\rTo\mathbb{T}_{k}A$ 2. 2.

$k$-traversals $(A,{\leq},i)$.

Proof.

Let $\alpha:A\rTo\mathbb{T}_{k}A$ be a coalgebra. Let $T\subseteq\mathbb{T}_{k}A$ be the image of $\alpha$. Unpacking the content of the two commutative diagrams for a coalgebra we see that if $\alpha(a)=[(p_{1},a_{1}),\ldots,(p_{l},a_{l})]$, then $a_{l}=a$, and $\alpha(a_{i})=[(p_{1},a_{1}),\ldots,(p_{i},a_{i})]$, $i=1,\ldots,l$. Thus $T$ is a prefix-closed subset of $\mathbb{T}_{k}A$, and moreover, for each $a\in A$, there is a unique $s\in T$ with last move of the form $(p,a)$. We can then define $a\leq b\;\;\stackrel{{\scriptstyle\Delta}}{{\Longleftrightarrow}}\;\;\alpha(a)\sqsubseteq\alpha(b)$, and $i(a)=p$ where $s[(p,a)]\in T$. Since $\alpha$ is a homomorphism, it must be the case that when $a$ and $b$ are adjacent in the Gaifman graph, $\alpha(a)$ is comparable with $\alpha(b)$, say $\alpha(a)\sqsubseteq\alpha(b)$, and the pebble index $i(a)$ must not occur in the suffix of $\alpha(a)$ in $\alpha(b)$. Thus $(A,{\leq},i)$ is a $k$-traversal of $A$.

Conversely, let $(A,{\leq},i)$ be a $k$-traversal of $A$. We define $\alpha(a)$ by induction on the number of strict predecessors of $a$: $\alpha(a)=s[(i(a),a)]$, where $s=\alpha(a^{-})$ if $a^{-}$ is the immediate predecessor of $a$, and otherwise $s=[\,]$. The $k$-traversal conditions imply that $\alpha:A\rTo\mathbb{T}_{k}A$ is a coalgebra. It is easy to see that these passages between coalgebras and $k$-traversals are mutually inverse. ∎

In the case that $k\geq n$, where $n$ is the cardinality of $A$, there is a trivial $k$-traversal of $A$ obtained by choosing a linear order $a_{1}<\ldots<a_{n}$ on $A$ and defining $i(a_{j})=j$.

We shall return to the issue of when coalgebras exist in our discussion of treewidth in Section 6.

3 Finite and infinite

Our primary focus is on finite structures. However, $\mathbb{T}_{k}A$ is always infinite. Is this necessary? As we shall see in the next section, given finite structures $A$ and $B$, the question of whether there is a homomorphism $\mathbb{T}_{k}A\rightarrow B$ can be finitized, using a positional representation. However, to give a comonadic representation of $k$-locality, we have to define a structure on a given $A$ which will allow us to characterize the situation for all choices of target $B$. Could this be done using a finite representation instead of $\mathbb{T}_{k}A$ with the same effect? The following no-go result says that this is not the case, and therefore an infinite representation cannot be avoided. We prove it for the special case $k=2$.

Theorem 7**.**

There is no construction $A\mapsto QA$ on finite structures $A$ such that $QA$ is finite, and for all finite $B$:

[TABLE]

Proof.

We assume that $\sigma$ contains a binary relation symbol $E$ and let $A$ be the structure with three elements $a,b,c$ where $E$ is interpreted as the three-element cycle, i.e. $E(a,b),E(b,c),E(c,a)$ hold and no other pairs are related by $E$. All other relations in $\sigma$ are interpreted by the empty relation on $A$.

We claim that for any finite $B$, $A\rightarrow_{2}B$ if and only if $B$ contains an $E$-cycle. In one direction, we note that $\mathbb{T}_{2}A$ contains an infinite $E$-path: $[(1,a)]$, $[(1,a),(2,b)]$, $[(1,a),(2,b),(1,c)]$, $[(1,a),(2,b),(1,c),(2,a)],\ldots$. The homomorphic image of an infinite path inside a finite structure must contain a cycle. In the other direction, assume that $B$ contains an $E$-cyle $C$. We define a map $h:\mathbb{T}_{2}A\rightarrow B$ by induction on the length of plays in $\mathbb{T}_{2}$, such that the image of $h$ is contained in the cycle $C$. For $s=[(p,x)]$ where $p\in\{1,2\}$ and $x\in\{a,b,c\}$, choose $h(s)$ to be an arbitrary element of the cycle in $B$. Suppose now that $s$ has length at least 2, the last move in $s$ is $(p,x)$ and by induction $h(s^{\prime})$ has been defined for all proper prefixes $s^{\prime}$ of $s$. Let $t$ be the longest prefix of $s$ ending in a move $(q,y)$ for $q\neq p$. We define $h(s)$ according to the three cases: if $x=y$ then $h(s)=h(t)$; if $E(x,y)$ then let $h(x)$ be the element of $C$ with an $E$-edge to $h(t)$; and if $E(y,x)$, then let $h(x)$ be the element of $C$ with an $E$-edge from $h(t)$. It is then easily checked that $h$ is a homomorphism.

Now, suppose there was a finite $QA$ as in the statement. Then, since $A\rightarrow_{2}QA$, $QA$ contains an $E$-cycle. Let $m$ be the length of the shortest cycle in $QA$. Consider the structure $C_{m+1}$ consisting of a single directed cycle of length $m+1$. Since it contains a cycle, $A\rightarrow_{2}C_{m+1}$. However, it is not the case that $QA\rightarrow C_{m+1}$, since the homomorphic image of a cycle of length $m$ must be a closed walk of length $m/l$ for some $l$, and $C_{m+1}$ contains no such walk. ∎

We can apply this result to rule out a categorical formulation of our question.

Corollary 8**.**

There is no comonad defined on $\mathcal{R}_{f}(\sigma)$ whose co-Kleisli category has the same preorder collapse as $\mathcal{K}(\mathbb{T}_{2})$.

This version of the no-go theorem is stated in purely categorical terms, while the proof uses very characteristic finite model theory arguments — indeed, essentially this argument appeared in the proof of Proposition 7.9 in [13].

We conjecture that this result extends to all higher values of $k$. Indeed, a generalization of the construction in the proof above can be used to show that for each $k$ there is a signature $\sigma$, containing a $k$-ary relation symbol, and a $\sigma$-structure $A$, for which there is no finite $QA$ with $QA\rightarrow B$ iff $A\rightarrow_{k}B$. It remains to prove the result uniformly for all signatures.

4 Positions and strategies

We now turn to the situation where finite structures $A$ and $B$ are given. We define $\Gamma_{k}(A,B)$, the set of configurations or positions for the existential $k$-pebble game from $A$ to $B$, to be the set of all partial functions $\gamma:[k]\rpfn A\times B$. The idea is that $\gamma$ represents the position left on the board after some rounds of the game. The domain of $\gamma$ is the set of pebbles used so far; $\gamma(p)=(a,b)$ means that Spoiler currently has pebble $p$ placed on $a\in A$, while Duplicator has her matching pebble on $b\in B$. We include the empty partial function, which represents the initial configuration.

We shall use the update operation $\gamma[p\mapsto(a,b)]$ on configurations. This yields the configuration with domain $\mathrm{dom}(\gamma)\cup\{p\}$, and such that

[TABLE]

There are really two cases which are covered by this update operation, both of which have natural readings in terms of the pebble game. If $p\in\mathrm{dom}(\gamma)$, then the update represents Spoiler moving pebble $p$ from its current position to mark $a$, while Duplicator moves her matching pebble to $b$. If $p\not\in\mathrm{dom}(\gamma)$, then we are extending the domain of $\gamma$, which corresponds to Spoiler placing a previously unused pebble, and Duplicator her matching pebble.

It will be convenient to use the transition notation $\gamma\rTo{(p,a):b}\gamma^{\prime}$, where $\gamma^{\prime}=\gamma[p\mapsto(a,b)]$; and $\gamma\rTo\gamma^{\prime}$ if $\gamma\rTo{(p,a):b}\gamma^{\prime}$ for some $p,a,b$.

We now relate positions to plays. A strategy for Duplicator in the existential $k$-pebble game from $A$ to $B$ can be represented by a function $f:\mathbb{T}_{k}A\rTo B$, which responds to each move of Spoiler, in the context of the previous history of the game, with a move in $B$. The coextension $f^{*}$, defined as in Section 2.1, makes explicit the sequence of responses by Duplicator, with the matching use of pebbles to those of Spoiler. Now consider a pair $(s,t)$ in the graph of $f^{*}$, i.e. $s\in\mathbb{T}_{k}A$ and $t=f^{*}(s)$. Note that $s$ and $t$ will be the same length, and have the same sequence of pebble indices. Let $p_{1},\ldots,p_{l}$ be the pebble indices occurring in $s$, with $1\leq l\leq k$. Let $(p_{i},a_{i})$ be the last occurrence of a move for pebble $p_{i}$ in $s$, $(p_{i},b_{i})$ the corresponding occurrence in $t$. We define $\mathsf{position}(s,t)$ to be the configuration $\gamma$ with domain $\{p_{1},\ldots,p_{l}\}$ and $\gamma(p_{i})=(a_{i},b_{i})$, $i=1,\ldots,l$. We write $\theta_{f}:\mathbb{T}_{k}A\rTo\Gamma_{k}(A,B)$ for the map

[TABLE]

Note that this is a map from the infinite set $\mathbb{T}_{k}A$ to the finite set $\Gamma_{k}(A,B)$.

A strategy in positional form is given by a set $S\subseteq\Gamma_{k}(A,B)$ satisfying the following conditions:

• (S0)

$\varnothing\in S$

• (S1)

For all $\gamma\in S$, $p\in[k]$ and $a\in A$, there is $b\in B$ such that $\gamma\rTo^{(p,a):b}\gamma^{\prime}\in S$.

• (S1)

$S$ is reachable: for all $\gamma\in S$, there is a sequence

[TABLE]

with $\gamma_{0}=\varnothing$, $\gamma_{n}=\gamma$, and $\gamma_{i}\in S$ for all $i$.

Given a Duplicator strategy $f:\mathbb{T}_{k}A\rTo B$, we define its representation in positional form as

[TABLE]

the set of positions which can be reached following the strategy represented by $f$.

Proposition 9**.**

For any strategy, the set of positions $S_{f}$ is a strategy in positional form. Conversely, for any strategy in positional form $S$, there is a function $f:\mathbb{T}_{k}A\rTo B$ such that $S_{f}=S$.

Proof.

Given a strategy $f$, (S0) holds by definition of $S_{f}$. For closure under (S1), suppose that

[TABLE]

If Spoiler places pebble $p$ on $a$, this leads to an extended play $s[(p,a)]$; for any such move, Duplicator has a response $b=f(s[(p,a)])$. Then

[TABLE]

Reachability of $\gamma=\theta_{f}(s)$ holds by induction on the length of $s$, since $\theta_{f}(s)\rTo\theta_{f}(s[(p,a)])$.

For the converse, given $S$ we can define $f(s)$ by induction on $|s|$. We choose a linear order on $B$. Consider a play $s[(p,a)]$. By induction, $f(s)$ has already been defined, with $\gamma=\theta_{f}(s)\in S$. We define $X:=\{b\in B\mid\gamma\rTo^{(p,a):b}\gamma^{\prime}\in S\}$,

[TABLE]

Then we define

[TABLE]

Clearly $\theta_{f}(s[(p,a)])\in S$. Note that by (S0), this definition also covers the case when $s$ is empty.

It remains to show that for all $\gamma\in S$, $\gamma\in S_{f}$. We argue by induction on the length of the shortest transition sequence from the empty configuration to $\gamma$. Consider $\gamma\rTo^{(p,a):b}\gamma^{\prime}$ with $\gamma=\theta_{f}(s)$, where $s$ is taken minimal in the prefix order in $\theta_{f}^{-1}(\gamma)$. Let $X$ be the set specified above in the definition of $f$, and let $b$ have $i$ strict predecessors in $X$ in the chosen linear order on $B$. Now consider the play $s^{\prime}=s\underbrace{[(p,a),\ldots,(p,a)]}_{i+1}$. By definition of $f$, $f(s^{\prime})=b$, so $\theta_{f}(s^{\prime})=\gamma^{\prime}$. ∎

The reason for the somewhat involved construction in the second part of the proof is that we have to construct a deterministic strategy at the level of plays which maps onto a possibly non-deterministic strategy at the level of positions. We shall return to this point in the sequel.

4.1 Winning conditions

A configuration $\gamma$ is winning for Duplicator if the relation

[TABLE]

is a partial homomorphism from $A$ to $B$.

A strategy in positional form $S$ is winning if $\gamma$ is winning for all $\gamma\in S$. A Duplicator strategy $f:\mathbb{T}_{k}A\rTo B$ is winning if $S_{f}$ is winning.

It will be convenient to make use of the following device. We consider the expansion of our relational signature $\sigma$ with an additional binary relation $I$. We turn $\sigma$-structures into $\sigma\cup\{I\}$-structures by interpreting $I$ as the identity relation. We refer to such structures as $I$-structures. Note that if we interpret $\mathbb{T}_{k}A$ over this expanded signature, it will not be an $I$-structure; however, the interpretation of the $I$ relation on $\mathbb{T}_{k}A$ where $A$ is an $I$-structure will hold when multiple pebbles have been placed by Spoiler on the same element of $A$. This will ensure that a homomorphism $\mathbb{T}_{k}A\rightarrow B$ will induce a single-valued mapping on the underlying positions.

Proposition 10**.**

Given $I$-structures $A$ and $B$, and a function $f:\mathbb{T}_{k}A\rTo B$, the following are equivalent:

$f$* is a winning strategy for Duplicator.* 2. 2.

$f$* is a homomorphism.*

Proof.

If $f$ is a homomorphism, the relation $R(\gamma)$ arising from any position in $S_{f}$ is single-valued, since $A$ and $B$ are $I$-structures, so multiple pebbles paced on the same element of $A$ must be mapped to the same element of $B$. From the definition of the relational structure on $\mathbb{T}_{k}A$, preservation of the relation instances in a play $s$ is easily seen to be equivalent to the partial homomorphism condition on $\gamma=\theta_{f}(s)$. ∎

4.2 Determinization

We can view a strategy in positional form $S$ as a finite-state transducer. The set of states is $S$, with initial state $\varnothing$. The input set is $[k]\times A$, while the output set is $B$. For each configuration $\gamma\in S$, there are transitions

[TABLE]

Note that this transducer need not be deterministic. In general, functions $f:\mathbb{T}_{k}A\rTo B$ will give rise to non-deterministic transducers $S_{f}$, since different plays mapping to the same position can give rise to different transitions for given Spoiler moves $(p,a)$. However, there is a simple determinization procedure. Given $S$, we choose a function $\theta_{\gamma}:[k]\times A\rTo B$ for each $\gamma\in S$ such that for all $(p,a)\in[k]\times A$, $\gamma\rTo^{(p,a):\theta_{\gamma}(p,a)}\gamma^{\prime}\in S$, and then define the reachable set of configurations $S_{d}$ under this choice of transitions. Explicitly, $S_{d}$ is defined as the least fixpoint of the following monotone function on sets of transitions:

[TABLE]

The following is easily verified.

Proposition 11**.**

$S_{d}$* is a strategy in positional form.* 2. 2.

It is deterministic: for each $\gamma\in S_{d}$ and $(p,a)\in[k]\times A$, there are unique $b\in B$, $\gamma^{\prime}\in S_{d}$ such that $\gamma\rTo^{(p,a):b}\gamma^{\prime}$. 3. 3.

If $S$ is winning, so is $S_{d}\subseteq S$.

For finite structures $A$, $B$, we write $A\rightarrow_{k}^{\mathsf{d}}B$ if there is a co-Kleisli morphism realized by a deterministic finite-state strategy in positional form.

Proposition 12**.**

For finite structures $A$, $B$, $A\rightarrow_{k}B\;\;\Longleftrightarrow\;\;A\rightarrow_{k}^{\mathsf{d}}B$.

Proof.

Given $f:\mathbb{T}_{k}A\rTo B$, by Proposition 9 we can pass to the positional representation $S_{f}$, then by Proposition 11 determinize $S_{f}$ to obtain $S_{d}$, then, by Proposition 9 again, pass back to a function $f_{d}:\mathbb{T}_{k}A\rTo B$ such that $S_{f_{d}}=S_{d}$. Moreover, by Proposition 10, if $f$ is a homomorphism, so is $f_{d}$. ∎

4.3 Co-Kleisli morphisms and winning strategies

The following result, which is a corollary to Propositions 9, 10, and 12, justifies our claim that the pebbling comonad captures the content of the existential $k$-pebble game.

Theorem 13**.**

Given $I$-structures $A$ and $B$, the following are equivalent:

There is a winning strategy for Duplicator in the existential $k$-pebble game from $A$ to $B$. 2. 2.

$A\rightarrow_{k}B$. 3. 3.

$A\rightarrow_{k}^{\mathsf{d}}B$.

5 Equivalences

Various notions of equivalence between relational structures play an important rôle in Finite Model Theory, in particular the elementary equivalences induced by various logics. If $\mathcal{L}$ is a logic, the corresponding equivalence is denoted $\equiv^{\mathcal{L}}$, where

[TABLE]

These equivalences can be characterized by various combinatorial games.

Our aim in this section is to characterize three important such equivalences in terms of morphisms in the co-Kleisli category. We introduced the relation $A\rightarrow_{k}B$ on structures in Section 2.1. This relation is clearly reflexive and transitive. The corresponding equivalence relation is

[TABLE]

We write $\equiv^{\exists^{+}}$ for the elementary equivalence induced by the existential-positive fragment of $\mathcal{L}^{k}_{\infty,\omega}$.

Proposition 14**.**

For all $A$, $B$: $A\rightleftarrows_{k}B\;\Longleftrightarrow\;A\equiv^{\exists^{+}}B$.

Proof.

This is an immediate consequence of Proposition 1 and Theorem 13. ∎

5.1 Counting logic equivalence

A more interesting question is posed by isomorphism in the co-Kleisli category, which we denote by $\cong_{\mathcal{K}}$. What does the equivalence this induces correspond to in logical terms? Given a morphism $f:\mathbb{T}_{k}A\rTo B$, for each $s\in\mathbb{T}_{k}A\cup\{[\,]\}$ and $p\in[k]$, there is a function $\psi_{s,p}:A\rTo B$ such that, for all $a\in A$, $f(s(p,a))=\psi_{s,p}(a)$. If these functions are all injective, respectively surjective, we write $A\rightarrow_{k}^{i}B$, respectively $A\rightarrow_{k}^{s}B$. The corresponding equivalences are denoted $A\rightleftarrows_{k}^{i}B$, $A\rightleftarrows_{k}^{s}B$. If there is a morphism $f:\mathbb{T}_{k}A\rTo B$ such that the functions $\psi_{s,p}$ are all bijective, and moreover for all $s\in\mathbb{T}_{k}A$ with $\gamma=\mathsf{position}(s,f^{*}(s))$, the relation $R(\gamma)$ is a partial isomorphism, we write $A\rightarrow_{k}^{b}B$.

It is standard that for finite structures $A$ and $B$, if there are injective homomorphisms $A\rightarrow B$ and $B\rightarrow A$, then $A\cong B$; and similarly for surjective homomorphisms. Localizing these arguments to the functions in context $\psi_{s,p}$ yields the following result.

Theorem 15**.**

For all finite $A$, $B$:

[TABLE]

Proof.

Since $A$ and $B$ are finite, if there exist injective maps from $A$ to $B$ and $B$ to $A$, the two sets have the same number of elements. It follows that any injective map is in fact surjective, and the first equivalence is immediate. Now, fix morphisms $f:\mathbb{T}_{k}A\rTo B$ and $g:\mathbb{T}_{k}B\rTo A$ witnessing $A\rightarrow_{k}^{i}B$ and $B\rightarrow_{k}^{i}A$ respectively. Then $f^{*}$ and $g^{*}$ are both injective maps. Consider the finite substructures $P_{A}$ and $P_{B}$ of $\mathbb{T}_{k}A$ and $\mathbb{T}_{k}B$ respectively induced by sequences of a length at most $n$. It is easily seen that $f^{*}$ and $g^{*}$ restricted to these substructures are injective homomorphisms $P_{A}\rightarrow P_{B}$ and $P_{B}\rightarrow P_{A}$ respectively. It follows that they are isomorphisms of these finite structures, and so $R(\gamma)$ is a partial isomorphism when $\gamma=\mathsf{position}(s,f^{*}(s))$ for any $s$. Thus, $f$ witnesses $A\rightarrow_{k}^{b}B$.

For the final equivalence, suppose we are given a homomorphism $f:\mathbb{T}_{k}A\rTo B$ witnessing $A\rightarrow_{k}^{b}B$. Then, a simple induction on the length of the sequences establishes that $f^{*}$ is a bijection between $\mathbb{T}_{k}A$ and $\mathbb{T}_{k}B$ and indeed is an isomorphism. Therefore $A\cong_{\mathcal{K}}B$. Conversely, if $h:\mathbb{T}_{k}A\rTo\mathbb{T}_{k}B$ is an isomorphism, we let $f:\mathbb{T}_{k}A\rTo B$ be given by $f=\varepsilon_{B}\circ h$ and note that this satisfies the condition that all functions $\psi_{s,p}$ are bijective. Moreover, if $t=h^{*}(s)$, then $s=k^{*}(t)$ where $k$ is the inverse of $h$ in $\mathcal{K}(\mathbb{T}_{k})$. The fact that $h$ and $k$ are both morphisms implies that $R(\gamma)$ is a partial isomorphism, where $\gamma=\mathsf{position}(s,t)$. ∎

We now recall the bijection game from [14]. This is a variant of the pebble game, in which at each round with corresponding position $\gamma$, Spoiler selects a pebble $p$, and Duplicator then selects a bijection $h$ between $A$ and $B$ such that, for all $q\neq p$ with $\gamma(q)=(a,b)$, $h(a)=b$. Duplicator wins the round if, for each $a\in A$, $R(\gamma[p\mapsto a])$ is a partial isomorphism.

The bijection game characterizes the equivalence induced by the counting logic $C^{k}$ [15], the $k$-variable logic with counting quantifiers, which plays a central rôle in finite model theory.

Theorem 16** ([14]).**

For all finite $A$, $B$, the following are equivalent:

$A\equiv^{C^{k}}B$** 2. 2.

Duplicator has a winning strategy in the bijection game.

The following is essentially immediate from the definitions:

Proposition 17**.**

For all $A$, $B$, Duplicator has a winning strategy in the bijection game if and only if $A\rightarrow_{k}^{b}B$.

Combining these results with Theorem 15, we obtain the main result of this subsection:

Theorem 18**.**

For all finite $A$, $B$:

[TABLE]

Thus isomorphism in the co-Kleisli category for the pebbling comonad $\mathbb{T}_{k}$ characterizes the elementary equivalence induced by $k$-variable counting logic.

5.2 Back-and-forth equivalence

Finally, we turn to the elementary equivalence induced by the full $k$-variable logic $\mathcal{L}^{k}_{\infty,\omega}$, which we write as $\equiv^{k}$. The standard game characterization of this uses back-and-forth pebble games, in which Spoiler can play in $B$ as well as $A$, and Duplicator has to respond in the other structure [16]. This can be defined concisely using our present notation as follows. Given $\gamma\in\Gamma_{k}(A,B)$, define $\gamma^{-}\in\Gamma_{k}(B,A)$ with $\gamma^{-}(p)=(b,a)$ iff $\gamma(p)=(a,b)$; and given $S\subseteq\Gamma_{k}(A)$, define $S^{-}=\{\gamma^{-}\mid\gamma\in S\}$. Now a positional-form winning strategy for Duplicator in the $k$-pebble game between $A$ and $B$ is $S\subseteq\Gamma_{k}(A,B)$ such that $S$ is a winning strategy in the existential $k$-pebble game from $A$ to $B$, and $S^{-}$ is a winning strategy in the existential $k$-pebble game from $B$ to $A$. Spelling this out, we see that this requires that $S$ satisfies a back-condition as well as the usual forth-condition as in the existential case; and that $R(\gamma)$ is a partial isomorphism for all $\gamma\in S$.

Theorem 19** ([16]).**

For all finite structures $A$ and $B$, there is a winning strategy for Duplicator in the $k$-pebble game between $A$ and $B$ iff $A\equiv^{k}B$.

We now define the relation $A\rightleftarrows_{k}^{-}B$ if there are co-Kleisli arrows $f:\mathbb{T}_{k}A\rTo B$ and $g:\mathbb{T}_{k}B\rTo A$ such that $S_{f}^{-}=S_{g}$.

Theorem 20**.**

For all finite structures $A$ and $B$:

[TABLE]

Proof.

The forward implication follows directly from Theorem 19. For the converse, given winning existential strategies $S$ from $A$ to $B$ and $S^{-}$ from $B$ to $A$, we obtain corresponding $f$ and $g$ from Theorem 9. ∎

An interesting point arising from this result is the necessity for non-deterministic positional strategies. While existential strategies witnessing homomorphisms can always be determinized by Proposition 11, in general a coupled pair of strategies $(S,S^{-})$ cannot both be deterministic. A simple example where this arises is given by the complete graphs $K_{k}$ and $K_{k+1}$. Note that $K_{k}\equiv^{k}K_{k+1}$, while $K_{k}{\not\equiv}^{C^{k}}K_{k+1}$.

6 Coalgebra number and treewidth

The notion of treewidth of a graph [17], extended to general relational structures in [3], plays a pervasive rôle in identifying “islands of tractability” in algorithmic graph theory. We shall write $\mathsf{tw}(A)$ for the treewidth of a structure $A$.

We now consider how the comonadic structure of $k$-pebbling can be used to characterize treewidth.

Theorem 21**.**

For all structures $A$, $\mathsf{tw}(\mathbb{T}_{k}A)<k$.

Proof.

We shall define a tree decomposition $(T,a)$ of $\mathbb{T}_{k}A$. The set of nodes of $T$ is $\mathbb{T}_{k}A\,\cup\,\{[\,]\}$, the set of plays together with the empty sequence. We say that $s$ is adjacent to $t$ if $s\prec t$ or $t\prec s$, where $\prec$ is the immediate predecessor relation induced by the prefix order; thus $s\prec t$ iff $t=s[(p,a)]$ for some $p$, $a$. The unique path between any $s$ and $t$ goes from $s$ via $\succ$-instances of the adjacency relation to $u$, and then by $\prec$-instances from $u$ to $t$, where $u$ is the greatest common prefix of $s$ and $t$. The labelling function $a(s)$ assigns the set of active prefixes of $s$ to $s$, where $t$ is an active prefix of $s$ if $t\sqsubseteq s$, and the pebble index used in the last move in $t$ does not occur in the suffix of $t$ in $s$. Clearly, the maximum size of any $a(s)$ is $k$.

We now verify the conditions for $(T,a)$ to be a tree decomposition of $\mathbb{T}_{k}A$. Firstly, $s\in a(s)$. Secondly, if $R^{\mathbb{T}_{k}A}(s_{1},\ldots,s_{n})$, then the $s_{i}$ must all be active prefixes of some $u$. Finally, suppose that $s$ is in $a(t_{1})\cap a(t_{2})$. Let $u$ be the largest common prefix of $t_{1}$ and $t_{2}$. Then we must have $s\sqsubseteq u$, and moreover $s$ active in $t_{1}$ implies that $s$ is active in all $v$ with $u\sqsubseteq v\sqsubseteq t_{1}$, and similarly for $t_{2}$. Thus $s\in a(v)$ for all $v$ in the unique path from $t_{1}$ to $t_{2}$ in $T$. ∎

Thus, although $\mathbb{T}_{k}A$ is infinite, it has bounded treewidth. As an immediate consequence of this result, we have:

Proposition 22**.**

If there is an injective homomorphism $A\rightarrow\mathbb{T}_{k}B$, then $\mathsf{tw}(A)<k$.

Proof.

If there is an injective homomorphism from $A$ to $\mathbb{T}_{k}B$, then $A$ is isomorphic to a substructure of $\mathbb{T}_{k}B$, hence $\mathsf{tw}(A)\leq\mathsf{tw}(\mathbb{T}_{k}B)<k$. ∎

In particular, if there is a coalgebra $\alpha:A\rTo\mathbb{T}_{k}A$, then $\mathsf{tw}(A)<k$. We define the coalgebra number $\kappa(A)$ of a finite structure $A$ to be the least $k$ such that there is a coalgebra $\alpha:A\rTo\mathbb{T}_{k}A$. Combining the previous Proposition and the remark after Theorem 6, we see that $\mathsf{tw}(A)<\kappa(A)\leq\mathsf{card}(A)$. In fact, $\kappa(A)$ yields an elegant, purely (co)algebraic characterization of treewidth.

Theorem 23**.**

For all finite structures $A$:

[TABLE]

Proof.

We have already seen that $\mathsf{tw}(A)<\kappa(A)$, so it suffices to show that $\kappa(A)\leq\mathsf{tw}(A)+1$. Suppose that $\mathsf{tw}(A)=k-1$. This means that there is a tree decomposition $(T,a)$ where $T$ is a tree, and for any node $t$ of $T$, $a(t)$ is a set of at most $k$ elements of $A$. By standard means, we can assume that $T$ is a rooted, directed, tree and for any node $t$ of $T$, there is at most one element of $A$ that appears in $a(t)$ that does not appear in $a(s)$ for any ancestor $s$ of $t$ (for instance, we could take $(T,a)$ to be a nice decomposition as defined in [18]).

For each $x\in A$, we can then define $t(x)$ to be the least (in the tree order) element of $T$ such that $x\in a(t(x))$. The properties of a tree decomposition guarantee that this is well defined, and our assumption that $(T,a)$ is nice ensures that $t$ is injective. The function $t$ induces a partial order on $A$: $x\leq y$ if and only if $t(x)$ is an ancestor of $t(y)$. It is easily seen that this is a tree order. We now proceed to define a map $i:A\rightarrow[k]$ by induction on this order. Suppose $i(x)$ has been defined for all $x<y$. In particular, this means (since $t$ is injective) that $i(x)$ is defined for all $x\in a(t(y))$ other than $y$. Since $a(t(y))$ has at most $k$ elements, there is at least one value $p\in[k]$ such that $i(x)\neq p$ for all $x\in a(t(y))$ other than $y$. We set $i(y)$ to be the least such $p$.

It can now be verified that $(A,\leq,i)$ is a $k$-traversal. By Theorem 6, this gives a coalgebra map $A\rightarrow\mathbb{T}_{k}A$, and establishes that $\kappa(A)\leq k$.

∎

7 Cores and pebble number

We now turn to the question of when there exists a homomorphism (not necessarily a coalgebra) $A\rightarrow\mathbb{T}_{k}A$. We define the pebble number $\pi(A)$ of a finite structure $A$ to be the least $k$ such that $A\rightarrow\mathbb{T}_{k}A$.

The core of a structure is a key notion in graph theory and finite model theory [19]. We define the core of a finite structure $A$ to be a substructure $A^{\prime}\subseteq A$ which admits a homomorphism $A\rTo A^{\prime}$, but for which no proper sub-structure does. We say that a structure is a core if it is the core of itself. The following summarizes some basic properties of cores.

Proposition 24**.**

Every finite structure has a core. 2. 2.

The core of a structure is unique up to isomorphism. 3. 3.

A substructure is a core of $A$ if and only if it is a retract of $A$, and minimal among retracts of $A$ with respect to inclusion. 4. 4.

A structure is a core if and only if it admits no proper retracts. 5. 5.

If $A^{\prime}$ is the core of $A$ and $B^{\prime}$ the core of $B$, then $A\rightarrow B\;\;\Longleftrightarrow\;\;A^{\prime}\rightarrow B^{\prime}$.

By virtue of these results, we can write $\mathsf{core}(A)$ for the core of a finite structure $A$.

We shall make use of some results from the literature. We denote the canonical conjunctive query for a finite structure $A$ by $Q^{A}$. This is a positive existential first-order sentence. We have the following classic result of Chandra and Merlin [2]:

Theorem 25**.**

The following are equivalent for finite structures $A$, $B$:

$A\rightarrow B$. 2. 2.

$Q^{B}\models Q^{A}$. 3. 3.

$B\models Q^{A}$.

We also have the following results due to Dalmau, Kolaitis and Vardi [20].

Theorem 26**.**

The following are equivalent for finite structures $A$:

• •

$\mathsf{tw}(\mathsf{core}(A))<k$.

• •

$Q^{A}$* is logically equivalent to a sentence of $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$, the existential positive fragment of $k$-variable first-order logic.*

We say that a sentence $\varphi$ of the existential positive fragment of first-order logic can be transformed to another sentence $\psi$ by standard rewriting if there are a sequence of steps, each of which is either (1) associative-commutative rewriting of conjunctions, (2) change of bound variable in an existential quantifier, or (3) replacing $\exists x.\,(\phi_{1}\wedge\phi_{2})$ by $\exists x.\,\phi_{1}\,\wedge\,\phi_{2}$, where $x$ does not occur free in $\phi_{2}$, which transform $\varphi$ into $\psi$. The following result from [20] is a refinement of the previous theorem.

Theorem 27**.**

The following are equivalent for finite structures $A$:

• •

$\mathsf{tw}(A)<k$.

• •

$Q^{A}$* can be transformed by standard rewriting to a sentence of $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$.*

The following result shows how $\mathbb{T}_{k}A$ captures the information about $A$ which is expressible in $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$.

Proposition 28**.**

Let $A$ be a finite structure. Every sentence of $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$ satisfied by $A$ is also satisfied by a finite substructure of $\mathbb{T}_{k}A$.

Proof.

We list the variables of $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$ as $x_{1},\ldots,x_{k}$. Given a formula $\varphi(\mathbf{x})$ with a list of distinct free variables $\mathbf{x}=x_{i_{1}},\ldots,x_{i_{l}}$, with $0\leq l\leq k$, and a corresponding semantic tuple $\mathbf{a}=a_{1},\ldots,a_{l}$, we define a tuple $\mathbf{s}(\mathbf{x},\mathbf{a})$ with $\mathbf{s}_{0}=[\,]$, and $\mathbf{s}_{i+1}=\mathbf{s}_{i}[(i+1,\mathbf{a}_{i})]$, for $i=0,\ldots,l-1$.

We show by induction on formulas $\varphi(\mathbf{x})\in\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$ that $A,\mathbf{a}\models\varphi(\mathbf{x})$ implies that $\mathbb{T}_{k},\mathbf{s}\models\varphi$ where $\mathbf{s}=\mathbf{s}(\mathbf{x},\mathbf{a})$. The base case is for atomic formulas $R(\mathbf{x})$. This follows immediately from the definition of the relational structure on $\mathbb{T}_{k}$. For $\exists x.\,\varphi$, $A,\mathbf{a}\models\exists x.\,\varphi$ iff for some $a$: $A,\mathbf{a}a\models\varphi$, which by induction hypothesis implies that $\mathbb{T}_{k}A,\mathbf{s}s\models\varphi$, iff $\mathbb{T}_{k}A,\mathbf{s}\models\exists x.\,\varphi$. Finally, for a conjunction $\varphi\wedge\psi$, $A,\mathbf{a}\mathbf{b}\mathbf{c}\models\varphi\wedge\psi$ iff $A,\mathbf{a}\mathbf{b}\models\phi(\mathbf{x},\mathbf{y})$, and $A,\mathbf{a}\mathbf{c}\models\psi(\mathbf{x},\mathbf{z})$, where the variables common to $\varphi$ and $\psi$ are listed as $\mathbf{x}$. By induction hypothesis, $\mathbb{T}_{k}A,\mathbf{s}\mathbf{t}\models\varphi$ and $\mathbb{T}_{k}A,\mathbf{s}\mathbf{u}\models\psi$. Then $\mathbb{T}_{k}A,\mathbf{s}^{\prime}\models\varphi\wedge\psi$, where $\mathbf{s}^{\prime}=\mathbf{s}(\mathbf{x}\mathbf{y}\mathbf{z},\mathbf{a}\mathbf{b}\mathbf{c})$. ∎

Proposition 29**.**

For all finite structures $A$, $A\equiv^{\exists^{+}}\mathbb{T}_{k}A$.

Proof.

By Proposition 14, we just need to exhibit homomorphisms $\mathbb{T}_{k}T_{k}A\rightarrow A$ and $\mathbb{T}_{k}A\rightarrow\mathbb{T}_{k}A$. For the first, we can compose the counit maps for $\mathbb{T}_{k}A$ and for $A$, and for the second, we can just take the identity. ∎

We can use these results to obtain our characterization of the relationship between treewidth and the pebble number.

Theorem 30**.**

For all finite structures $A$:

[TABLE]

Proof.

It clearly suffices to prove that:

[TABLE]

Suppose firstly that $\mathsf{tw}(\mathsf{core}(A))<k$. By Theorem 26, $Q^{A}$ is logically equivalent to a sentence of $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$. By Proposition 28, $Q^{A}$ is satisfied by a finite substructure $T$ of $\mathbb{T}_{k}A$. By Theorem 25, there is a homomorphism $A\rightarrow T\rinc\mathbb{T}_{k}A$.

Now suppose that there is a homomorphism $A\rightarrow\mathbb{T}_{k}A$. The image of this homomorphism is a finite substructure $T$ of $\mathbb{T}_{k}A$. By Theorem 25, $Q^{T}\models Q^{A}$. By Proposition 22, $\mathsf{tw}(T)<k$. Hence by Theorem 27, $Q^{T}$ can be transformed by standard rewriting to a formula in $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$. We can restrict the counit map $\varepsilon_{A}:\mathbb{T}_{k}A\rightarrow A$ to a homomorphism $T\rightarrow A$. Using Theorem 25 again, $Q^{A}\models Q^{T}$. Hence $Q^{A}$ and $Q^{T}$ are logically equivalent, which shows that $Q^{A}$ is logically equivalent to a sentence in $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$. By Theorem 26, this implies that $\mathsf{tw}(\mathsf{core}(A))<k$. ∎

This result shows that the existence of a homomorphism from $A$ to $\mathbb{T}_{k}A$ characterizes the treewidth of the core of $A$. The stronger hypothesis of having a coalgebra map $A\rightarrow\mathbb{T}_{k}A$ characterizes the treewidth of $A$ itself.

8 Strong $k$-consistency and contextuality

We now look at strong $k$-consistency, which is a fundamental notion in constraint satisfaction [21]. The non-uniform CSP problem $\mathrm{CSP}(B)$ can be posed for a fixed finite structure $B$ as the existence of a homomorphism $A\rightarrow B$ for a given finite structure $A$. An instance $A$ is $i$-consistent if for every homomorphism $h$ from an $(i-1)$-element substructure of $A$ to $B$ and every $a\in A$, there is a homomorphism on a substructure of $A$ including $\mathrm{dom}(h)\cup\{a\}$ extending $h$. It is strongly $k$-consistent if it is $i$-consistent for all $i\leq k$.

This leads us to the following notion of consistency number $\mathsf{sc}_{B}(A)$ of a finite structure $A$: the greatest $k$ such that there is a homomorphism $\mathbb{T}_{k}A\rightarrow B$, i.e. $A\rightarrow_{k}B$. Note that, if we parameterize the pebble number to define $\pi_{B}(A)$ as the smallest $k$ such that there is a homomorphism $A\rightarrow\mathbb{T}_{k}B$, then $\pi_{B}$ and $\mathsf{sc}_{B}$ are formally dual.

If $k\geq\mathsf{card}(A)$, then $A\rightarrow_{k}B$ if and only if $A\rightarrow B$, so we define $\mathsf{sc}_{B}(A)$ as the largest $k\leq n$ such that $A\rightarrow_{k}B$. Also, because of the graded structure of the monads $\mathbb{T}_{k}$, note that it is strong $k$-consistency which we are capturing. Once we have $A\rightarrow_{k}B$, then also $A\rightarrow_{l}B$ for $l\leq k$.

The interesting case is where $\mathsf{sc}_{B}(A)<\mathsf{card}(A)$. This is the case where we can get partial solutions for up to $k$ variables, but no global solutions. We note that this case covers a variety of examples of contextuality in quantum mechanics, as shown in [22]. In particular, many proofs of the Kochen-Specker theorem [23] provide examples of this phenomenon. As an illustration, we consider the Mermin Magic Square [24]:

[TABLE]

The constraints are that each row and the first two columns have even parity, and the final column has odd parity. This translates into 6 linear equations over $\mathbb{Z}_{2}$:

[TABLE]

Of course, these equations are not satisfiable in $\mathbb{Z}_{2}$. The system is $8$-consistent but not globally consistent. The significance of this construction in quantum mechanics is that we can interpret the variables with quantum observables in such a way that the specified constraints are exactly the predicted behaviour of measuring the observables. The global inconsistency corresponds to the impossibility of a non-contextual explanation for this behaviour. For more on this topic, see [25, 26].

We can also make a simple connection between pebble number and consistency number.

Proposition 31**.**

If $\pi(A)\leq\mathsf{sc}_{B}(A)$, then $A\rightarrow B$.

Proof.

If $\pi(A)\leq\mathsf{sc}_{B}(A)$, then for some $k$,

[TABLE]

∎

8.1 Cai-Fürer-Immerman construction

Fix a relational signature with two ternary relations $R_{0}$ and $R_{1}$. Consider the structure $Z2$ in this signature with universe $\{0,1\}$ where $R_{0}=\{(i,j,k)\mid i\oplus j\oplus k=0\}$ and $R_{1}=\{(i,j,k)\mid i\oplus j\oplus k=1\}$. Then, a system of equations over $\mathbb{Z}_{2}$ (as in the example above) can be seen as a structure $A$ whose universe is the set of variables and $(v_{1},v_{2},v_{3})\in R_{0}$ if $v_{1}\oplus v_{2}\oplus v_{3}=0$ is an equation in the system and $(v_{1},v_{2},v_{3})\in R_{1}$ if $v_{1}\oplus v_{2}\oplus v_{3}=1$ is an equation in the system. It is then immediate that $A\rightarrow Z2$ if and only if the system is solvable. This is the classical example of a constraint satisfaction problem that is not solvable by $k$-local consistency tests (though it is polynomial-time solvable by Gaussian elimination). Moreover, it is also known that the class of satisfiable systems of equations is not invariant under $\equiv^{C^{k}}$ for any $k$. This is shown by Atserias et al. [27], based on the construction of Cai et al. [28] of a polynomial-time decidable class of graphs not definable in fixed-point logic with counting. Here, we give an account of this construction in the categorical framework we have developed.

Proposition 32**.**

Suppose $A\rightarrow_{k}Z2$. Then there is a pair of structures $A_{0}$ and $A_{1}$ with $A_{0}\cong_{\mathcal{K}}A_{1}$, $A\rightarrow A_{0}$, and $A_{1}\rightarrow Z2$.

Proof.

We define $A_{0}$ and $A_{1}$ to both have universe $A\times\{0,1\}$. The interpretation of the relations in $A_{0}$ is given by:

[TABLE]

[TABLE]

The interpretation of the relations in $A_{1}$ is given by:

[TABLE]

[TABLE]

The homomorphism $A\rTo A_{0}$ is given by $a\mapsto(a,0)$ and the homomorphism $A_{1}\rTo Z2$ by $(a,i)\mapsto i$.

Now, suppose $f:\mathbb{T}_{k}A\rTo Z2$ is a homomorphism. We aim to use this to define an isomorphism $f^{\prime}:\mathbb{T}_{k}A_{0}\rTo\mathbb{T}_{k}A_{1}$. For any $s\in\mathbb{T}_{k}A_{0}$, we write $\pi s$ to denote the sequence in $\mathbb{T}_{k}A$ obtained by replacing each move $(p,(a,i))$ in $s$ by $(p,a)$. Let $s$ be the sequence $(p_{1},(a_{1},i_{1})),\ldots,(p_{n},(a_{n},i_{n}))$ and let $s_{1},\ldots,s_{n}$ be the sequence of its non-empty prefixes. We then define $f^{\prime}(s)$ to be the sequence in $\mathbb{T}_{k}A_{1}$ whose $j$th component is $(p_{j},a_{j},i_{j}\oplus f(\pi s_{j}))$ and verify that this is an isomorphism. ∎

9 Modalities

Another facet of monads and comonads is their rôle in categorical logic, as categorified interpretations of S4 modalities [29]. The pebbling comonad $\mathbb{T}_{k}$ provides a semantics for a modality $\Box_{k}$, which we can read as: “it is $k$-locally the case that …”. We can take e.g. first-order logic as a base, and extend it with the formation rule that if $\varphi$ is a formula with at most $k$ free variables, then $\Box_{k}\varphi$ is a formula.

We extend the usual definition of satisfaction of a formula

[TABLE]

where $A$ is a structure, and $\mathbf{a}$ a sequence of elements of $A$ providing interpretations for the free variables $\mathbf{x}$ of $\varphi$, with the following clause:

[TABLE]

where if $\mathbf{a}=\langle a_{1},\ldots,a_{l}\rangle$, $l\leq k$, $\alpha(a_{i})=[(p_{1},a_{1}),\ldots,(p_{i},a_{i})]$, $i=1,\ldots,l$.

We can read off a number of properties of this modality directly from the comonadic structure. Firstly, the S4 axioms are valid in this semantics with respect to $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$ formulas $\varphi$:

[TABLE]

We also have the grading axiom:

[TABLE]

Using Proposition 28, for formulas $\varphi$ of $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$ we also have the following:

[TABLE]

If we want to reason about structures with bounded treewidth, we can use the results of the previous section to introduce suitable assumptions.

We can also consider a modality $\Diamond$, which can be read as “it is homomorphically true that”. This has the following semantics:

[TABLE]

This satisfies the dual S4 axioms with respect to $\exists^{+}\mathcal{L}^{k}_{\omega,\omega}$ formulas:

[TABLE]

Whereas the logics usually considered in finite model theory are interpreted in one structure at a time, these modalities allows us to navigate around the category of structures, treating them as different “possible worlds”.

10 Conclusions

While we are not aware of any closely related work, the work of Bojanczyk [30] and of Adamek et al [31] on recognizable languages over monads is in a broadly kindred spirit. The aim of these works is to use monads as a unifying notion for the many variations on the theme of recognizability. Also, we can mention the use of comonads in functional programming [32, 33]. In particular, the comonadic structure of lists is studied in [34]. The forgetful functor from structures to sets carries the pebbling comonad to this list comonad (although concretely the correspondence is up to list reversal).

The ideas developed in this paper suggest a number of further developments. Firstly, can we find similar characterizations of other forms of games, and connections with the corresponding logical notions? In fact, there is a natural family of comonads corresponding to Ehrenfeucht-Fraissé games, which can be used to characterize equivalence up to given quantifier rank, using ideas analogous to those in Section 5.2. There is also an unravelling comonad, which arises in the analysis of bisimulation for modal and guarded logics [35]. Details of these constructions will appear in a sequel to the present paper.

There are many other natural lines for future investigation. Can we give categorical characterizations of key combinatorial parameters, in a similar fashion to treewidth? Can we use categorical limit and colimit constructions, possibly in an enriched form, to connect with the combinatorial developments in [36]? Can we leverage results in descriptive complexity to give categorical descriptions of complexity classes?

Another project is to analyze Rossman’s theorem on homomorphism preservation [37] from a categorical viewpoint. It seems that many of the technical notions developed in the proof of this result are susceptible of a more abstract formulation, which may lead to more conceptual proofs, and the possibility of finding wider applicability for the techniques developed there.

The ideas described in this paper provide a connection between two broad themes within the field of logic in computer science: the interaction of logic with the analysis of algorithms and computational complexity, and the study of the semantics of programs and processes. Examples of such connections are still fairly rare, and we hope that the ideas introduced here can be developed further in a fruitful fashion.

Acknowledgement: The work reported here was initiated at the programme on Logical Structures in Computation at the Simons Institute for the Theory of Computing, Berkeley.