# On the Correspondence Between Monotonic Max-Sum GNNs and Datalog

David Tena Cucala1 Bernardo Cuenca Grau1 Boris Motik1 Egor V. Kostylev2
1 Department of Computer Science, University of Oxford, UK
2 Department of Informatics, University of Oslo, Norway
{david.tena.cucala, bernardo.cuenca.grau<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Although there has been significant interest in applying machine learning
techniques to structured data, the _expressivity_ (i.e., a description of what
can be learned) of such techniques is still poorly understood. In this paper,
we study data transformations based on _graph neural networks_ (GNNs). First,
we note that the choice of how a dataset is encoded into a numeric form
processable by a GNN can obscure the characterisation of a model’s
expressivity, and we argue that a _canonical_ encoding provides an appropriate
basis. Second, we study the expressivity of _monotonic max-sum_ GNNs, which
cover a subclass of GNNs with max and sum aggregation functions. We show that,
for each such GNN, one can compute a Datalog program such that applying the
GNN to any dataset produces the same facts as a single round of application of
the program’s rules to the dataset. Monotonic max-sum GNNs can sum an
unbounded number of feature vectors which can result in arbitrarily large
feature values, whereas rule application requires only a bounded number of
constants. Hence, our result shows that the unbounded summation of monotonic
max-sum GNNs does not increase their expressive power. Third, we sharpen our
result to the subclass of _monotonic max_ GNNs, which use only the max
aggregation function, and identify a corresponding class of Datalog programs.

##  1 Introduction

Data management tasks such as query answering or logical reasoning can be
abstractly seen as transforming an input dataset into an output dataset. A key
aspect of such transformations is their _expressivity_ , which is often
established by identifying a logic-based language that realises the same class
of transformations. For example, core aspects of the SQL and SPARQL query
languages have been characterised using fragments of first-order logic (?; ?),
and logical deduction over RDF datasets has been described using the rule-
based language _Datalog_ (?). Such correspondences enable rigorous
understanding and comparison of different data management languages.

Recently, there has been an increasing interest in applying machine learning
techniques to data management tasks. A key benefit is that the desired
transformation between datasets can be induced from examples, rather than
specified explicitly. Many models have been proposed for this purpose, such as
recurrent (?), fibring (?), and feed-forward networks (?), architectures that
simulate forward (?; ?) and backward chaining (?), and architectures for rule
learning (?; ?). _Graph neural networks_ (GNNs) have proved particularly
popular since they can express graph transformations and have been widely
applied to link prediction and node classification tasks in structured
datasets (?; ?; ?; ?; ?; ?; ?; ?; ?).

Characterising the expressivity of ML models for data management has thus
steadily gained importance, and computational logic provides a well-
established methodology: we can describe conditions under which ML-induced
models become equivalent to logical formalisms in the sense that applying the
ML model to an arbitrary dataset produces the same result as applying a
specific logical formula. In a pioneering study, ? (?) showed that each GNN-
induced transformation expressible in first-order logic is equivalent to a
concept query of the $\mathcal{ALCQ}$ _description logic_ (?)—a popular KR
formalism. ? (?) proved an analogous result for a class of GNNs with a
dedicated vertex and colour. ? (?) showed that GNNs can express certain types
of graph isomorphism tests. ? (?) characterised the expressivity of GNNs using
a hybrid language where each Datalog rule is annotated with a tensor. ? (?)
characterised the expressivity of _monotonic GNNs_ (MGNNs), which use the max
aggregation function and require all weights in the matrices to be
nonnegative, in terms of a class of Datalog programs. Finally, ? (?)
characterised the expressivity of the Neural-LP model of rule learning.

In this paper, we take a next step in the study of the expressivity of GNN-
based transformations of structured data. A key technical challenge can be
summarised as follows. GNNs typically use summation to aggregate feature
vectors of all vertices adjacent to a given vertex in the input graph. The
number of adjacent vertices in the input is unbounded (i.e., there is no a
priori limit on the number of neighbours a vertex can have), and so the
summation result can be unbounded as well; hence, it appears that arbitrarily
many vertices can influence whether a fact is derived. This seems
fundamentally different to reasoning in fragments of first-order logic such as
Datalog: the number of constants that need to be jointly considered in an
application of a Datalog rule is determined by the number of rule variables,
and _not_ by the structure of the input dataset. Thus, at first glance, one
might expect GNNs with summation to be fundamentally different from Datalog
rules. To shed light on this issue, we present several novel contributions.

In Section 3 we focus on a key obstacle: to apply a GNN to a dataset, the
latter must be encoded as a graph where each vertex is assigned a numeric
feature vector; but then, the expressivity of the transformation inevitably
depends on the details of the encoding, which obscures the contribution of the
GNN itself. To overcome this, we adopt a _canonical_ encoding, variants of
which have already been considered by ? (?), ? (?), and ? (?). We define a GNN
to be _equivalent_ to a Datalog program if applying the GNN to any dataset
while using the canonical encoding produces the same facts as applying the
program’s rules to the dataset _once_ (i.e., without fixpoint iteration).
Finally, we observe that noncanonical encodings by ? (?), ? (?), or ? (?) can
be described using well-known extensions of Datalog, and so the expressivity
of transformations based on such encodings can be characterised by composing
all relevant programs.

In Section 4 we present our main technical contribution. First, we introduce a
class of _monotonic max-sum_ GNNs. Similarly to the MGNNs by ? (?), monotonic
max-sum GNNs require matrix weights to be be nonnegative; however, they allow
for the max or sum aggregation functions in each network layer, and they place
certain restrictions on the activation and classification functions (ReLU and
threshold functions are allowed). ? (?) showed that the performance of such
GNNs with just max aggregation on tasks such as knowledge graph completion is
on a par with that of other recent approaches. Hence, monotonic max-sum GNNs
are practically relevant, but they also allow their predictions to be
explained using logical proofs. Second, we prove that each monotonic max-sum
GNN is equivalent to a Datalog program of a certain shape possibly containing
inequalities in rule bodies. Strictly speaking, such a program can be
recursive in the sense that the same predicate can occur in both rule bodies
and heads; however, our notion of equivalence does not involve fixpoint
iteration (i.e., the program’s rules are applied just once). Thus, monotonic
max-sum GNNs can derive facts with predicates from the input, but they cannot
express true recursive properties such as reachability; moreover, the ability
to produce unbounded feature values does not lead to a fundamental increase in
expressivity. Our equivalence proof is quite different from the analogous
result for MGNNs: when aggregation is limited to just max, the value of each
feature of a vertex clearly depends on only a fixed number of neighbours of
the vertex. Third, we prove that the equivalent Datalog program can be
computed from the GNN itself. This result is interesting because it requires
enumerating potentially infinite sets of real-valued candidate feature values
in a way that guarantees termination. This provides a starting point for
future development of practical techniques for extracting Datalog programs
from monotonic max-sum GNNs.

Finally, in Section 5 we sharpen our results to _monotonic max_ GNNs, which
allow only for max aggregation. We show that, analogously to MGNNs, each
monotonic max GNN is equivalent to a positive Datalog program; however, we
also present a converse result: we identify a class Datalog programs such
that, for each program in the class, there exists an equivalent monotonic max
GNN. In this way, we obtain an exact characterisation of an interesting class
of GNN-based transformations using logical formalisms.

The proofs of all theorems are given in full in Appendices A and B.

##  2 Preliminaries

We next recapitulate the basics of Datalog and GNNs.

Datasets and Datalog. We fix a signature consisting of countably infinite,
disjoint sets of _predicates_ and _constants_. Each predicate is associated
with a nonnegative integer arity. We also consider a countably infinite set of
_variables_ that is disjoint with the sets of predicates and constants.

A _term_ is a variable or a constant. An _atom_ is of the form
${P(t_{1},\dots,t_{n})}$ where $P$ is a predicate of arity $n$ and
${t_{1},\cdots,t_{n}}$ are terms. An _inequality_ is an expression of the form
${t_{1}\not\approx t_{2}}$ where $t_{1}$ and $t_{2}$ are terms. A _literal_ is
an atom or an inequality. A term or a literal is _ground_ if it is variable-
free. A _fact_ is a ground atom and a _dataset_ is a finite set of facts;
thus, datasets cannot contain inequalities. A conjunction $\alpha$ of facts is
true in a dataset $D$, written ${D\models\alpha}$, if ${A\in D}$ for each fact
$A$ in $\alpha$. A ground inequality ${s\not\approx t}$ is true if ${s\neq
t}$; for uniformity with facts, we often write ${D\models s\not\approx t}$
even though the truth of ${s\not\approx t}$ does not depend on $D$. A
(Datalog) _rule_ is of the form (1) where ${n\geq 0}$, ${B_{1},\dots,B_{n}}$
are _body_ literals, and $H$ is the _head_ atom:

$\displaystyle B_{1}\wedge\dots\wedge B_{n}\rightarrow H.$ (1)

A (Datalog) _program_ is a finite set of rules. A _substitution_ $\nu$ is a
mapping of finitely many variables to ground terms; for $\alpha$ a literal,
$\alpha\nu$ is the result of replacing in $\alpha$ each variable $x$ with
$\nu(x)$ provided the latter is defined. Each rule $r$ of form (1) defines an
_immediate consequence_ operator $T_{r}$ on datasets: for $D$ a dataset,
$T_{r}(D)$ is the dataset that contains the fact $H\nu$ for each substitution
$\nu$ mapping all variables of $r$ to terms occurring in $D$ such that
${D\models B_{i}\nu}$ for each ${1\leq i\leq n}$. For $\mathcal{P}$ a program,
${T_{\mathcal{P}}(D)=\bigcup_{r\in\mathcal{P}}T_{r}(D)}$.

To simplify the formal treatment, we do not make the usual _safety_
requirement where each variable in a rule must occur in a body atom; in fact,
the body can be empty, which we denote by $\top$. For example, rule
${r=\top\rightarrow R(x,y)}$ is syntactically valid; moreover, the definition
of $T_{r}$ ensures that $T_{r}(D)$ contains exactly each fact $R(s,t)$ for all
(not necessarily distinct) terms $s$ and $t$ occurring in $D$.

Conjunctions $\alpha$ and $\beta$ of literals are _equal up to variable
renaming_ if there exists a bijective mapping $\nu$ from the set of all
variables of $\alpha$ to the set of all variables of $\beta$ such that
$\alpha\nu$ and $\beta$ contain exactly the same conjuncts; this notion is
extended to rules in the obvious way. A set $S$ _contains_ a conjunction
$\alpha$ of literals _up to variable renaming_ if there exists ${\beta\in S}$
such that $\alpha$ and $\beta$ are equal up to variable renaming.

Graph Neural Networks. We use $\mathbb{R}$ and $\mathbb{R}^{+}_{0}$ for the
sets of real and nonnegative real numbers, respectively. Also, we use
$\mathbb{N}$ for the set of natural numbers, and
${\mathbb{N}_{0}=\mathbb{N}\cup\\{0\\}}$.

A function ${\sigma:\mathbb{R}\to\mathbb{R}}$ is _monotonically increasing_ if
${x<y}$ implies ${\sigma(x)\leq\sigma(y)}$. Function $\sigma$ is _Boolean_ if
its range is ${\\{0,1\\}}$. Finally, $\sigma$ is _unbounded_ if, for each
${y\in\mathbb{R}}$, there exists ${x\in\mathbb{R}}$ such that ${\sigma(x)>y}$.

A real _multiset_ is a function ${S:\mathbb{R}\to\mathbb{N}_{0}}$ that assigns
to each ${x\in\mathbb{R}}$ the number of occurrences $S(x)$. Such $S$ is
_finite_ if ${S(x)>0}$ for finitely many ${x\in\mathbb{R}}$; the _cardinality_
of such $S$ is ${|S|=\sum_{x\in\mathbb{R}}S(x)}$; and
$\mathcal{F}(\mathbb{R})$ is the set of all finite real multisets. We often
write a finite $S$ as a list of possibly repeated real numbers in double-
braces ${\\{\\!\\!\\{\,\dots\,\\}\\!\\!\\}}$. Finally, we treat a set as a
multiset where each element occurs just once.

We consider vectors and matrices over $\mathbb{R}$ and $\mathbb{R}^{+}_{0}$.
For $\mathbf{v}$ a vector and $i$ a natural number, $(\mathbf{v})_{i}$ is the
$i$-th element of $\mathbf{v}$. We apply scalar functions to vectors element-
wise; for example, given $n$ vectors ${\mathbf{v}_{1},\dots,\mathbf{v}_{n}}$
of equal dimension, ${\max\\{\mathbf{v}_{1},\dots,\mathbf{v}_{n}\\}}$ is the
vector whose $i$-th element is equal to
${\max\\{(\mathbf{v}_{1})_{i},\dots,(\mathbf{v}_{n})_{i}\\}}$.

For $\mathsf{Col}$ a finite set of _colours_ and ${\delta\in\mathbb{N}}$ a
_dimension_ , a $(\mathsf{Col},\delta)$-graph is a tuple
${\mathcal{G}=\langle\mathcal{V},\\{\mathcal{E}^{c}\\}_{c\in\mathsf{Col}},\lambda\rangle}$
where $\mathcal{V}$ is a finite set of _vertices_ ; for each
${c\in\mathsf{Col}}$, ${\mathcal{E}^{c}\subseteq\mathcal{V}\times\mathcal{V}}$
is a set of directed _edges_ ; and _labelling_ $\lambda$ assigns to each
${v\in\mathcal{V}}$ a _feature_ vector $\mathbf{v}_{\lambda}$ of dimension
$\delta$. Graph $\mathcal{G}$ is _symmetric_ if ${\langle
v,u\rangle\in\mathcal{E}^{c}}$ implies ${\langle
u,v\rangle\in\mathcal{E}^{c}}$ for each ${c\in\mathsf{Col}}$, and it is
_Boolean_ if ${(\mathbf{v}_{\lambda})_{i}\in\\{0,1\\}}$ for each
${v\in\mathcal{V}}$ and ${i\in\\{1,\dots,\delta\\}}$. To improve readability,
we abbreviate $\mathbf{v}_{\lambda}$ to just $\mathbf{v}$ when the labelling
function is clear from the context; analogously, we abbreviate
$\mathbf{v}_{\lambda_{\ell}}$ to $\mathbf{v}_{\ell}$.

A $(\mathsf{Col},\delta)$-_graph neural network_ (_GNN_) $\mathcal{N}$ with
${L\geq 1}$ _layers_ is a tuple

$\displaystyle\begin{array}[]{@{}l@{}}\langle\\{\mathbf{A}_{\ell}\\}_{1\leq\ell\leq
L},\\{\mathbf{B}_{\ell}^{c}\\}_{c\in\mathsf{Col}\text{ and }1\leq\ell\leq
L},\\\\[2.15277pt] \hskip 71.13188pt\\{\mathbf{b}_{\ell}\\}_{1\leq\ell\leq
L},\\{\mathsf{agg}_{\ell}\\}_{1\leq\ell\leq
L},\sigma,\mathsf{cls}\rangle,\end{array}$ (4)

where, for each ${\ell\in\\{1,\dots,L\\}}$ and ${c\in\mathsf{Col}}$,
$\mathbf{A}_{\ell}$ and $\mathbf{B}_{\ell}^{c}$ are matrices over $\mathbb{R}$
of dimension $\delta_{\ell}\times\delta_{\ell-1}$ with
${\delta_{0}=\delta_{L}=\delta}$, $\mathbf{b}_{\ell}$ is a vector over
$\mathbb{R}$ of dimension $\delta_{\ell}$,
${\mathsf{agg}_{\ell}:\mathcal{F}(\mathbb{R})\to\mathbb{R}}$ is an
_aggregation_ function, ${\sigma:\mathbb{R}\to\mathbb{R}}$ is an _activation_
function, and ${\mathsf{cls}:\mathbb{R}\to\\{0,1\\}}$ is a _classification_
function.

Applying $(\mathsf{Col},\delta)$-GNN $\mathcal{N}$ to
$(\mathsf{Col},\delta)$-graph $\mathcal{G}$ induces the sequence
${\lambda_{0},\dots,\lambda_{L}}$ of vertex labelling functions such that
${\lambda_{0}=\lambda}$ and, for each ${\ell\in\\{1,\ldots,L\\}}$ and ${v\in
V}$, the value of $\mathbf{v}_{\ell}$ is given by

$\displaystyle\begin{array}[]{@{}l@{}}\mathbf{v}_{\ell}=\sigma\Big{(}\mathbf{A}_{\ell}\mathbf{v}_{\ell-1}+\\\
\qquad\quad\;\sum\limits_{c\in\mathsf{Col}}\\!\mathbf{B}_{\ell}^{c}\;\mathsf{agg}_{\ell}\big{(}\\{\\!\\!\\{\,\mathbf{u}_{\ell-1}\mid\langle
v,u\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\}\big{)}+\mathbf{b}_{\ell}\Big{)}.\end{array}$
(7)

The result $\mathcal{N}(\mathcal{G})$ of applying $\mathcal{N}$ to
$\mathcal{G}$ is the Boolean $(\mathsf{Col},\delta)$-graph with the same
vertices and edges as $\mathcal{G}$, but where each vertex ${v\in\mathcal{V}}$
is labelled by $\mathsf{cls}(\mathbf{v}_{L})$.

##  3 Choosing an Encoding/Decoding Scheme

To realise a dataset transformation using a GNN, we must first encode the
input dataset into a graph that can be processed by a GNN, and subsequently
decode the GNN’s output back into a dataset. Several encoding/decoding schemes
have been proposed in the literature, and their details differ considerably.
As a result, when characterising GNN-based transformations of datasets using
logic, it can be hard to understand which properties of the characterisation
are due to the chosen encoding/decoding scheme, and which are immanent to the
GNN used to realise the transformation. In this paper we consider primarily
the encoding scheme that straightforwardly converts a dataset into a graph,
but we also discuss how to take other encoding schemes into account.

###  3.1 Canonical Encoding/Decoding Scheme

A straightforward way to encode a dataset containing only unary and binary
facts into a Boolean $(\mathsf{Col},\delta)$-graph is to transform terms into
vertices, use vertex connectivity to describe binary facts, and encode
presence of unary facts in feature vectors. Such encoding/decoding schemes,
which we call _canonical_ , have already been widely used in the literature
with minor variations (?; ?; ?). They establish a direct syntactic
correspondence between datasets and coloured graphs and are thus a natural
starting point for studying the expressivity of GNNs.

We next describe one such scheme. In particular, we introduce
$(\mathsf{Col},\delta)$-datasets, which naturally correspond to a large class
of $(\mathsf{Col},\delta)$-graphs. Our definitions provide the foundation
necessary to formulate our expressivity results in Section 4. In Section 3.2
we discuss how to combine our expressivity results with more complex encoding
schemes.

######  Definition 1.

Let $\mathsf{Col}$ be a set of colours and let ${\delta\in\mathbb{N}}$ be a
dimension. A $(\mathsf{Col},\delta)$-_signature_ contains

  * •

a binary predicate $E^{c}$ for each colour ${c\in\mathsf{Col}}$, and

  * •

a unary predicate $U_{i}$ for each ${i\in\\{1,\dots,\delta\\}}$.

A $(\mathsf{Col},\delta)$-_fact_ has a predicate from the
$(\mathsf{Col},\delta)$-signature, and a $(\mathsf{Col},\delta)$-_dataset_
contains only $(\mathsf{Col},\delta)$-facts.

We assume that terms occurring in datasets correspond one-to-one to vertices
of coloured graphs—that is, each term $t$ is paired with a unique vertex
$v_{t}$. This is again without loss of generality since the result of applying
a GNN to a coloured graph does not depend on the identity of vertices, but
only on the graph structure and the feature vectors.

We are now ready to define the canonical GNN-based transformations of
$(\mathsf{Col},\delta)$-datasets.

######  Definition 2.

The _canonical encoding_ $\mathsf{enc}(D)$ of a
$(\mathsf{Col},\delta)$-dataset $D$ is the Boolean
$(\mathsf{Col},\delta)$-graph
${\langle\mathcal{V},\\{\mathcal{E}^{c}\\}_{c\in\mathsf{Col}},\lambda\rangle}$
defined as follows:

  * •

$\mathcal{V}$ contains the vertex $v_{t}$ for each term $t$ occurring in $D$;

  * •

${\langle v_{t},v_{s}\rangle\in\mathcal{E}^{c}}$ if ${E^{c}(t,s)\in D}$ for
each ${c\in\mathsf{Col}}$; and

  * •

${(\mathbf{v}_{t})_{i}=1}$ if ${U_{i}(t)\in D}$, and
${(\mathbf{v}_{t})_{i}=0}$ otherwise.

The _canonical decoding_ $\mathsf{dec}(\mathcal{G})$ of a Boolean
$(\mathsf{Col},\delta)$-graph
${\mathcal{G}=\langle\mathcal{V},\\{\mathcal{E}^{c}\\}_{c\in\mathsf{Col}},\lambda\rangle}$
is the dataset that contains

  * •

the fact $E^{c}(t,s)$ for each ${\langle
v_{t},v_{s}\rangle\in\mathcal{E}^{c}}$ and ${c\in\mathsf{Col}}$, and

  * •

the fact $U_{i}(t)$ for each ${v_{t}\in\mathcal{V}}$ and
${i\in\\{1,\dots,\delta\\}}$ such that ${(\mathbf{v}_{t})_{i}=1}$.

Each $(\mathsf{Col},\delta)$-GNN $\mathcal{N}$ induces the _canonical_
transformation $T_{\mathcal{N}}$ on $(\mathsf{Col},\delta)$-datasets where
${T_{\mathcal{N}}(D)=\mathsf{dec}(\mathcal{N}(\mathsf{enc}(D)))}$ for each
$(\mathsf{Col},\delta)$-dataset $D$.

This encoding neither introduces nor omits any information from the input
dataset, so a $(\mathsf{Col},\delta)$-dataset $D$ and its canonical encoding
$\mathsf{enc}(D)$ straightforwardly correspond to one another. Since datasets
are directional, $(\mathsf{Col},\delta)$-graphs must be directed as well to
minimise the discrepancy between the two representations. The canonical
decoding is analogous to the encoding, and the two are inverse operations on
graphs that are regular as per Definition 3.

######  Definition 3.

A $(\mathsf{Col},\delta)$-graph
${\mathcal{G}=\langle\mathcal{V},\\{\mathcal{E}^{c}\\}_{c\in\mathsf{Col}},\lambda\rangle}$
is _regular_ if $\mathcal{G}$ is Boolean and each vertex ${v\in\mathcal{V}}$
either occurs in $\mathcal{E}^{c}$ for some ${c\in\mathsf{Col}}$, or
${(\mathbf{v})_{i}=1}$ for some ${i\in\\{1,\dots,\delta\\}}$.

Our canonical encoding produces only regular graphs, and there is a one-to-one
correspondence between $(\mathsf{Col},\delta)$-datasets and regular
$(\mathsf{Col},\delta)$-graphs. Our results from the following sections can be
equivalently framed as characterising expressivity of GNN transformations of
regular graphs in terms of Datalog programs. Graphs that are not Boolean do
not correspond to encodings of datasets, so we do not see a natural way to
view GNN transformations over such graphs in terms of logical formalisms.
Finally, a $(\mathsf{Col},\delta)$-graph $\mathcal{G}$ that is Boolean but not
regular contains ‘isolated’ vertices that are not connected to any other
vertex and are labelled by zeros only. When such $\mathcal{G}$ is decoded into
a $(\mathsf{Col},\delta)$-dataset, such ‘isolated’ vertices do not produce any
facts in $\mathsf{dec}(\mathcal{G})$ and thus several non-regular Boolean
graphs can produce the same $(\mathsf{Col},\delta)$-dataset. Note, however,
that each ‘isolated’ zero-labelled vertex is transformed by a GNN in the same
way—that is, the vector labelling the vertex in the GNN’s output does not
depend on any other vertices but only on the matrices of the GNN.
Consequently, such vertices are not interesting for our study of GNN
expressivity.

We are now ready to formalise our central notion of equivalence between a GNN
and a Datalog program.

######  Definition 4.

A $(\mathsf{Col},\delta)$-GNN $\mathcal{N}$ _captures_ a rule or a Datalog
program $\alpha$ if ${T_{\alpha}(D)\subseteq T_{\mathcal{N}}(D)}$ for each
$(\mathsf{Col},\delta)$-dataset $D$. Moreover, $\mathcal{N}$ and $\alpha$ are
_equivalent_ if ${T_{\mathcal{N}}(D)=T_{\alpha}(D)}$ for each
$(\mathsf{Col},\delta)$-dataset $D$.

The key question we address in Sections 4 and 5 is the following: under what
conditions is a given $(\mathsf{Col},\delta)$-GNN $\mathcal{N}$ equivalent to
a Datalog program, and can this program (at least in principle) be computed
from $\mathcal{N}$?

###  3.2 Noncanonical Encoding/Decoding Schemes

For each $(\mathsf{Col},\delta)$-dataset $D$, the binary facts of $D$ and
$T_{\mathcal{N}}(D)$ coincide, and so applying $T_{\mathcal{N}}$ to $D$ cannot
derive any binary facts. To overcome this limitation, more complex,
noncanonical encodings have been proposed (?; ?; ?). These introduce vertices
representing combinations of several constants so that facts of higher arity
can be encoded in appropriate feature vectors, but there is no obvious
canonical way to achieve this. Expressivity results based on such encodings
are less transparent because it is not obvious which aspects of expressivity
are due to the encoding/decoding scheme and which are immanent to the GNN
itself.

We argue that noncanonical encoding/decoding schemes can often be described by
a pair of programs $\mathcal{P}_{\mathsf{enc}}$ and
$\mathcal{P}_{\mathsf{dec}}$, possibly expressed in a well-known extension of
Datalog, which convert an input dataset into a $(\mathsf{Col},\delta)$-dataset
and vice versa. Thus, given an arbitrary dataset $D$, the result of applying
the end-to-end transformation that uses a GNN $\mathcal{N}$ and the respective
encoding/decoding scheme is
$T_{\mathcal{P}_{\mathsf{dec}}}(T_{\mathcal{N}}(T_{\mathcal{P}_{\mathsf{enc}}}(D)))$.
Furthermore, if $\mathcal{N}$ is equivalent to a Datalog program
$\mathcal{P}_{\mathcal{N}}$, then the composition of
$\mathcal{P}_{\mathsf{enc}}$, $\mathcal{P}_{\mathcal{N}}$, and
$\mathcal{P}_{\mathsf{dec}}$ characterises the end-to-end transformation. This
allows us to clearly separate the contribution of the GNN from the
contributions of the encoding and decoding.

? (?) recently presented a dataset transformation based on a class of
_monotonic_ GNNs (MGNNs). Their approach is applicable to a dataset $D$ that
uses unary predicates ${A_{1},\dots,A_{\epsilon}}$ and binary predicates
${R_{\epsilon+1},\dots,R_{\delta}}$, and $D$ is encoded into a symmetric
$(\mathsf{Col},\delta)$-graph over the set of colours
${\mathsf{Col}=\\{c_{1},c_{2},c_{3},c_{4}\\}}$. The encoding introduces a
vertex $v_{a}$ for each constant $a$ in $D$ as well as vertices $v_{a,b}$ and
$v_{b,a}$ for each pair of constants $a,b$ occurring together in a binary fact
in $D$. Predicates are assigned fixed positions in vectors so that the value
of a component of a vector labelling a vertex indicates the presence or
absence of a specific fact in $D$. For example, if ${A_{i}(a)\in D}$, then
$(\mathbf{v}_{a})_{i}$ is set to $1$; analogously, if ${R_{j}(a,b)\not\in D}$
but $a$ and $b$ occur in $D$ in a binary fact, then $(\mathbf{v}_{a,b})_{j}$
is set to $0$. Moreover, the edges of the coloured graph indicate different
types of ‘connections’ between constants; for example, vertices $v_{a}$ and
$v_{a,b}$ are connected by an edge of colour $c_{1}$ to indicate that constant
$a$ occurs first in the constant pair $(a,b)$. A variant of this approach was
also proposed by ? (?) in the context of knowledge graph completion.

We next show how to capture this encoding using rules. Note that the encoder
introduces vertices of the form $v_{a,b}$ for pairs of constants $a$ and $b$,
so the encoding program $\mathcal{P}_{\mathsf{enc}}$ requires value invention.
This can be conveniently realised using functional terms. For example, we can
represent vertex $v_{a,b}$ using term $g(a,b)$, and we can represent each
vertex of the form $v_{a}$ using a term $f(a)$ for uniformity. Applying the
encoding program $\mathcal{P}_{\mathsf{enc}}$ to a dataset thus produces a
$(\mathsf{Col},\delta)$-dataset with functional terms, which should be
processed by the GNN as if they were constants; for example, the canonical
encoding should transform $g(a,b)$ into vertex $v_{g(a,b)}$. Based on this
idea, the encoding program $\mathcal{P}_{\mathsf{enc}}$ contains rule (8)
instantiated for each ${i\in\\{1,\dots,\epsilon\\}}$, and rules (9)–(17)
instantiated for each ${j\in\\{\epsilon+1,\dots,\delta\\}}$.

$\displaystyle A_{i}(x)$ $\displaystyle\rightarrow U_{i}(f(x))$ (8)
$\displaystyle R_{j}(x,y)$ $\displaystyle\rightarrow U_{j}(g(x,y))$ (9)
$\displaystyle R_{j}(x,y)$ $\displaystyle\rightarrow E^{c_{1}}(f(x),g(x,y))$
(10) $\displaystyle R_{j}(x,y)$ $\displaystyle\rightarrow
E^{c_{1}}(g(x,y),f(x))$ (11) $\displaystyle R_{j}(x,y)$
$\displaystyle\rightarrow E^{c_{2}}(f(y),g(x,y))$ (12) $\displaystyle
R_{j}(x,y)$ $\displaystyle\rightarrow E^{c_{2}}(g(x,y),f(y))$ (13)
$\displaystyle R_{j}(x,y)$ $\displaystyle\rightarrow E^{c_{3}}(g(x,y),g(y,x))$
(14) $\displaystyle R_{j}(x,y)$ $\displaystyle\rightarrow
E^{c_{3}}(g(y,x),g(x,y))$ (15) $\displaystyle R_{j}(x,y)$
$\displaystyle\rightarrow E^{c_{4}}(f(x),f(y))$ (16) $\displaystyle
R_{j}(x,y)$ $\displaystyle\rightarrow E^{c_{4}}(f(y),f(x))$ (17)

Rules (8) and (9) ensure that all unary and binary facts in the input dataset
are encoded as facts of the form $U_{i}(f(a))$ and $U_{j}(g(a,b))$; thus, when
these are further transformed into a $(\mathsf{Col},\delta)$-graph, the
vectors labelling vertices $v_{f(a)}$ and $v_{g(a,b)}$ encode all input facts
of the form $A_{i}(a)$ and $R_{j}(a,b)$ for ${i\in\\{1,\dots,\epsilon\\}}$ and
${j\in\\{\epsilon+1,\dots,\delta\\}}$. In addition, rules (10)–(17) encode the
adjacency relationships between terms: colour $c_{1}$ connects terms $g(a,b)$
and $f(a)$, colour $c_{2}$ connects $g(a,b)$ and $f(b)$, colour $c_{3}$
connects $g(a,b)$ and $g(b,a)$, and colour $c_{4}$ connects terms $f(a)$ and
$f(b)$ provided that $a$ and $b$ occur jointly in a binary fact.

Program $\mathcal{P}_{\mathsf{dec}}$ capturing the decoder contains rule (18)
instantiated for each ${i\in\\{1,\dots,\epsilon\\}}$, as well as rule (19)
instantiated for each ${j\in\\{\epsilon+1,\dots,\delta\\}}$.

$\displaystyle U_{i}(f(x))$ $\displaystyle\rightarrow A_{i}(x)$ (18)
$\displaystyle U_{j}(g(x,y))$ $\displaystyle\rightarrow R_{j}(x,y)$ (19)

Intuitively, these rules just ‘read off’ the facts from the labels of vertices
such as $v_{f(a)}$ and $v_{g(a,b)}$. The composition of these three programs
is a (function-free) Datalog program.

It is straightforward to show that, for each dataset $D$, the graph obtained
by applying the encoder by ? (?) is isomorphic to the graph obtained by
applying the canonical encoding from Definition 2 to
$T_{\mathcal{P}_{\mathsf{enc}}}(D)$ and thus program
$\mathcal{P}_{\mathsf{enc}}$ correctly captures their encoder.

A limitation of this encoding is that the transformation’s output can contain
a fact of the form $R(a,b)$ only if the input dataset contains a fact of the
form $S(a,b)$ or $S(b,a)$. Intuitively, the presence of $S(a,b)$ or $S(b,a)$
in the input ensures that the resulting $(\mathsf{Col},\delta)$-graph contains
a vertex $v_{g(a,b)}$ for representing binary facts of the form $R(a,b)$. An
obvious way to overcome this limitation is to introduce terms $g(a,b)$ for all
constants $a$ and $b$ occurring in the input, without requiring $a$ and $b$ to
occur jointly in a binary fact. While this increases the expressivity of the
end-to-end transformation, the increase is due to the encoding step, rather
than the GNN. Our framework makes this point clear. For example, we can extend
$\mathcal{P}_{\mathsf{enc}}$ with rules such as (20)–(23) and so on for all
other combinations of unary and binary predicates and colours. The chaining of
$\mathcal{P}_{\mathsf{enc}}$, $\mathcal{P}_{\mathcal{N}}$, and
$\mathcal{P}_{\mathsf{dec}}$ can now capture different transformations even if
$\mathcal{P}_{\mathcal{N}}$ remains the same.

$\displaystyle A_{i}(x)\wedge A_{j}(y)$ $\displaystyle\rightarrow
E^{c_{1}}(f(x),g(x,y))$ (20) $\displaystyle A_{i}(x)\wedge A_{j}(y)$
$\displaystyle\rightarrow E^{c_{1}}(g(x,y),f(x))$ (21) $\displaystyle
R_{i}(x,z)\wedge A_{j}(y)$ $\displaystyle\rightarrow E^{c_{1}}(g(x,y),f(x))$
(22) $\displaystyle R_{i}(z,x)\wedge A_{j}(y)$ $\displaystyle\rightarrow
E^{c_{1}}(g(x,y),f(x))$ (23)

? (?) introduced $k$-GNNs and showed them to be more expressive than standard
GNNs. The input to a $k$-GNN is a symmetric $(\mathsf{Col},\delta_{1})$-graph
$\mathcal{G}_{1}$ without self-loops where $\mathsf{Col}$ contains a single
colour $c$ and, for each vertex $v$ of $\mathcal{G}_{1}$,
${(\mathbf{v})_{i}=1}$ for exactly one ${1\leq i\leq\delta_{1}}$. To apply a
$k$-GNN to $\mathcal{G}_{1}$, the latter is transformed into another
$(\mathsf{Col},\delta_{2})$-graph $\mathcal{G}_{2}$ that contains one vertex
for each set of $k$ distinct vertices of $\mathcal{G}_{1}$, and then a
standard $(\mathsf{Col},\delta_{2})$-GNN is applied to $\mathcal{G}_{2}$.

We next show that the transformation of $\mathcal{G}_{1}$ into
$\mathcal{G}_{2}$ can be captured by a program $\mathcal{P}_{\mathsf{enc}}$
that transforms a $(\mathsf{Col},\delta_{1})$-dataset over unary predicates
$A_{1},\dots,A_{\delta_{1}}$ and a binary predicate $R$ into a
$(\mathsf{Col},\delta_{2})$-dataset. Thus, the increase in expressivity of
$k$-GNNs does not come from the GNN model itself, but rather from the encoding
implicit in their approach. For readability, we make several simplifying
assumptions. First, while ? (?) consider sets of $k$ distinct vertices in
order to ensure practical scalability, we consider $k$-tuples instead and
limit our presentation to just $k=2$. Second, we consider just the _local
neighbourhood_ approach to connecting vertices in $\mathcal{G}_{2}$. Finally,
our encoding requires extending Datalog not only with function symbols, but
also with stratified negation-as-failure $\mathsf{not}$ (?).

Program $\mathcal{P}_{\mathsf{enc}}$ consists of rules (27)–(37) instantiated
for all ${i,j,k,\ell\in\\{1,\dots,\delta_{1}\\}}$.

$\displaystyle\begin{array}[]{@{}r@{\;}l@{}}A_{i}(x)\wedge A_{j}(y)\wedge
x\not\approx y&\wedge\\\ A_{k}(x)\wedge A_{\ell}(z)\wedge x\not\approx
z&\wedge\\\ R(y,z)\wedge y\not\approx z&\rightarrow
E^{c}(g(x,y),g(x,z))\end{array}$ (27)
$\displaystyle\begin{array}[]{@{}r@{\;}l@{}}A_{i}(y)\wedge A_{j}(x)\wedge
y\not\approx x&\wedge\\\ A_{k}(z)\wedge A_{\ell}(x)\wedge z\not\approx
x&\wedge\\\ R(y,z)\wedge y\not\approx z&\rightarrow
E^{c}(g(y,x),g(z,x))\end{array}$ (31)
$\displaystyle\begin{array}[]{@{}l@{}}A_{i}(x)\wedge A_{j}(y)\wedge
x\not\approx y\wedge\mathsf{not}~{}R(x,y)\\\ \hskip 128.0374pt\rightarrow
U_{i,j,0}(g(x,y))\end{array}$ (34)
$\displaystyle\begin{array}[]{@{}l@{}}A_{i}(x)\wedge A_{j}(y)\wedge
x\not\approx y\wedge R(x,y)\\\ \hskip 128.0374pt\rightarrow
U_{i,j,1}(g(x,y))\end{array}$ (37)

Conjunctions of the form ${A_{i}(x)\wedge A_{j}(y)\wedge x\not\approx y}$ in
these rules identify pairs of distinct constants $a$ and $b$ (corresponding to
the vertices of $\mathcal{G}_{1}$) in the input dataset, and, for each such
pair, $g(x,y)$ introduces a term $g(a,b)$ (corresponding to a vertex of
$\mathcal{G}_{2}$). Rules (27) and (31) encode the _local neighbourhood_
approach: terms $g(a,b)$ and $g(d,e)$ are connected in $\mathcal{G}_{2}$ if
either ${a=b}$ and ${d\neq e}$, or ${a\neq b}$ and ${d=e}$, and additionally
the two constants in the inequality are connected in $\mathcal{G}_{1}$.
Finally, rules (34) and (37) identify the type of the subgraph of
$\mathcal{G}_{1}$ that $a$ and $b$ participate in. Specifically, a fact of the
form $U_{i,j,0}(g(a,b))$ says that $a$ and $b$ are labelled in
$\mathcal{G}_{1}$ by $A_{i}$ and $A_{j}$ respectively, but they are not
connected in $\mathcal{G}_{1}$. A fact of the form $U_{i,j,1}(g(a,b))$ is
analogous, but with the difference that $a$ and $b$ are connected in
$\mathcal{G}_{1}$.

##  4 GNNs with Max-Sum Aggregation

In this section, we introduce monotonic max-sum GNNs and prove that each such
GNN corresponds to a Datalog program (possibly with inequalities in the rule
bodies) that can be computed from the GNN’s definition. Monotonic max-sum GNNs
can use the following aggregation function in all layers, which generalises
both max and sum.

######  Definition 5.

For ${k\in\mathbb{N}_{0}\cup\\{\infty\\}}$, a finite real multiset
${S\in\mathcal{F}(\mathbb{R})}$, and ${\ell=\min{(k,|S|)}}$, let

$\mathrm{max}\text{-}{k}\text{-}\mathrm{sum}(S)=\begin{cases}0&\text{if
}\ell=0,\\\\[4.30554pt]
\sum\limits_{i=1}^{\ell}s_{i}&\begin{array}[]{@{}l@{}}\text{where
}s_{1},\dots,s_{\ell}\text{ are the }\\\ \ell\text{ largest numbers of }S.\\\
\end{array}\end{cases}$

Each occurrence of a number is counted separately; for example,
${\mathrm{max}\text{-}{3}\text{-}\mathrm{sum}(\\{\\!\\!\\{\,0,1,1,2,2,5\,\\}\\!\\!\\})=9}$
because the three largest numbers in $S$ are $5$ and the two occurrences of
$2$. Also, $\mathrm{max}\text{-}{1}\text{-}\mathrm{sum}$ is equivalent to
$\max$, and $\mathrm{max}\text{-}{\infty}\text{-}\mathrm{sum}$ is equivalent
to $\mathrm{sum}$; hence, $\mathrm{max}\text{-}{k}\text{-}\mathrm{sum}$
generalises both the $\max$ and $\mathrm{sum}$ aggregation functions. While
the ability to sum just the $k$ maximal elements may not be relevant in
practice, it will allow us to formalise a key technical result. We next
introduce monotonic max-sum GNNs.

######  Definition 6.

A _monotonic max-sum_ $(\mathsf{Col},\delta)$-GNN is a GNN of form (4)
satisfying the following conditions:

  * •

for each ${\ell\in\\{1,\dots,L\\}}$ and each ${c\in\mathsf{Col}}$, all
elements of matrices $\mathbf{A}_{\ell}$ and $\mathbf{B}_{\ell}^{c}$ are
nonnegative;

  * •

for each ${\ell\in\\{1,\dots,L\\}}$, the aggregation function
$\mathsf{agg}_{\ell}$ is $\mathrm{max}\text{-}{k_{\ell}}\text{-}\mathrm{sum}$
for some $k_{\ell}\in\mathbb{N}_{0}\cup\\{\infty\\}$;

  * •

the activation function $\sigma$ is monotonically increasing and unbounded,
and the range of $\sigma$ is $\mathbb{R}^{+}_{0}$; and

  * •

the classification function $\mathsf{cls}$ is a step function—that is, there
exists a _threshold_ ${t\in\mathbb{R}}$ such that
${\mathsf{cls}(t^{\prime})=0}$ for each ${t^{\prime}<t}$, and
${\mathsf{cls}(t^{\prime})=1}$ for each ${t^{\prime}\geq t}$.

Monotonic max-sum GNNs are closely related to, but incomparable with MGNNs by
? (?): MGNNs do not require the activation function to be unbounded, but they
support only the $\max$ aggregation function in all layers. While ReLU
satisfies Definition 6, neither ELU nor the sigmoid function is compatible.

In Section 4.1, we show that, in each monotonic max-sum GNN $\mathcal{N}$, one
can replace each function $\mathrm{max}\text{-}{k_{\ell}}\text{-}\mathrm{sum}$
where ${k_{\ell}=\infty}$ with
$\mathrm{max}\text{-}{C_{\ell}}\text{-}\mathrm{sum}$ for some
${C_{\ell}\in\mathbb{N}_{0}}$ without changing the canonical transformation
induced by $\mathcal{N}$—that is, to apply a GNN to a dataset, we need to
consider only a bounded number of vertices for aggregation. Number $C_{\ell}$
depends solely on $\mathcal{N}$ (i.e., it is independent of any dataset to
which $\mathcal{N}$ is applied) and is called the _capacity_ of layer $\ell$.
In Section 4.2, we use this result to show that $T_{\mathcal{N}}$ is
equivalent to the immediate consequence operator of a Datalog program
$\mathcal{P}_{\mathcal{N}}$ that depends only on $\mathcal{N}$. Finally, in
Section 4.3, we show that the numbers $C_{\ell}$ can be computed from
$\mathcal{N}$, and hence program $\mathcal{P}_{\mathcal{N}}$ is computable.
Our objective is to show that extracting $\mathcal{P}_{\mathcal{N}}$ from
$\mathcal{N}$ is possible in principle, but further work is needed to devise a
practical procedure.

###  4.1 Limiting Neighbour Aggregation

Throughout the rest of Section 4, we fix a monotonic max-sum
$(\mathsf{Col},\delta)$-GNN $\mathcal{N}$ of form (4) and dimensions
${\delta_{0},\dots,\delta_{L}}$ as specified in Section 2, and we fix
${k_{1},\dots,k_{L}}$ as the numbers defining the aggregation functions of
$\mathcal{N}$. We next show that each ${k_{\ell}=\infty}$ can be replaced with
a natural number $C_{\ell}$. We first introduce several auxiliary definitions.

######  Definition 7.

A _$(\mathsf{Col},\ell)$ -multiset family_, where ${0\leq\ell\leq L}$, is a
mapping $\mathbf{Y}$ that assigns to each colour ${c\in\mathsf{Col}}$ a finite
multiset $\mathbf{Y}^{c}$ of vectors of dimension $\delta_{\ell}$.

For each ${1\leq\ell\leq L}$, each ${1\leq i\leq\delta_{\ell}}$, each vector
$\mathbf{x}$ of dimension $\delta_{\ell-1}$, and each
$(\mathsf{Col},\ell-1)$-multiset family $\mathbf{Y}$, let

$\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})=(\mathbf{A}_{\ell}\mathbf{x}+\sum_{c\in\mathsf{Col}}\mathbf{B}_{\ell}^{c}\;\mathrm{max}\text{-}{k_{\ell}}\text{-}\mathrm{sum}(\mathbf{Y}^{c})+\mathbf{b}_{\ell})_{i}.$

Sets $\mathcal{X}_{\ell,i}$ with ${0\leq\ell\leq L}$ and ${1\leq
i\leq\delta_{\ell}}$ are defined by induction on $\ell$ as follows.

  * •

For each ${1\leq i\leq\delta_{0}}$, let ${\mathcal{X}_{0,i}=\\{0,1\\}}$.

  * •

For each ${\ell\geq 1}$ and each ${1\leq i\leq\delta_{\ell}}$, set
$\mathcal{X}_{\ell,i}$ is the least set that contains
${\sigma(\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y}))}$ for each vector
$\mathbf{x}$ of dimension $\delta_{\ell-1}$ such that
${(\mathbf{x})_{j}\in\mathcal{X}_{\ell-1,j}}$ for each $j$, and each
$(\mathsf{Col},\ell-1)$-multiset family $\mathbf{Y}$ such that
${(\mathbf{y})_{j}\in\mathcal{X}_{\ell-1,j}}$ for all ${c\in\mathsf{Col}}$,
${\mathbf{y}\in\mathbf{Y}^{c}}$, and $j$.

Intuitively, sets $\mathcal{X}_{\ell,i}$ contain all real numbers that can
occur in the $i$-th position of a vector labelling a vertex at layer $\ell$
when $\mathcal{N}$ is applied to a canonical encoding of some
$(\mathsf{Col},\ell)$-dataset. Indeed, by the base case of the definition,
$\mathcal{X}_{0,i}$ contains all values that can be produced by the canonical
encoding, and the inductive step considers all possible ways in which a vector
in layer $\ell$ can be computed from vectors in layer $\ell-1$ using
propagation equation (7). In the latter case, a $(\mathsf{Col},\ell)$-multiset
family $\mathbf{Y}$ represents a collection of possible neighbour vectors, and
$\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})$ is the argument of the activation
function used to compute some $(\mathbf{v}_{\ell})_{i}$.

Note that sets $\mathcal{X}_{\ell,i}$ are nonempty, and they can be infinite.
However, Theorem 8 shows that $\mathcal{X}_{\ell,i}$ can be enumerated as a
countable, monotonically increasing sequence of numbers. This is important
because it shows that the notion of a least nonzero element of
$\mathcal{X}_{\ell,i}$ is correctly defined. In the following, for each
${\alpha\in\mathbb{R}}$, let
${\mathcal{X}_{\ell,i}^{>\alpha}=\\{\alpha^{\prime}\in\mathcal{X}_{\ell,i}\mid\alpha^{\prime}>\alpha\\}}$.

######  Theorem 8.

Each set $\mathcal{X}_{\ell,i}$ satisfies
${\mathcal{X}_{\ell,i}\subseteq\mathbb{R}^{+}_{0}}$, and, for each
${\alpha\in\mathbb{R}}$, set
${\mathcal{X}_{\ell,i}\setminus\mathcal{X}_{\ell,i}^{>\alpha}}$ is finite.

Theorem 8 ensures that, for each ${\alpha\in\mathbb{R}}$, set
$\mathcal{X}_{\ell,i}^{>\alpha}$ is either empty or it contains a smallest
number strictly larger than $\alpha$. The proof uses the fact that the
activation function $\sigma$ is unbounded. We are now ready to define the
capacity of $\mathcal{N}$.

######  Definition 9.

The _capacity_ of each layer $\ell$ of $\mathcal{N}$ is defined in Algorithm
1. Moreover, the _capacity_ of $\mathcal{N}$ is defined as
${C_{\mathcal{N}}=\max\\{C_{1},\dots,C_{L}\\}}$.

Sets $\mathcal{X}_{\ell,i}$ can be infinite, so Algorithm 1 can perhaps be
better understood as inductively defining sequences of numbers
$\alpha_{\ell}$, $\beta_{\ell}$, $C_{\ell}$ and so on. However, in Section 4.3
we show that the smallest positive elements of $\mathcal{X}_{\ell,i}$ can in
fact be computed, which justifies our usage of the term ‘algorithm’.

Algorithm 1 capacity$(\mathcal{N})$

1:let $\alpha_{L}$ be the threshold of $\mathsf{cls}$

2:for $\ell$ from $L$ down to $1$ do

3: $w_{\ell}:=$ the least non-zero element of $\mathbf{A}_{\ell}$ and all
$\mathbf{B}_{\ell}^{c}$

4: $\epsilon_{\ell}:=$ the least non-zero number in
$\bigcup_{i}\mathcal{X}_{\ell-1,i}$

5: if either $w_{\ell}$ or $\epsilon_{\ell}$ does not exist then

6: $C_{\ell}:=C_{\ell-1}:=C_{1}:=0$

7: return

8: $\beta_{\ell}:=$ the least natural number such that
$\sigma(\beta_{\ell})\geq\alpha_{\ell}$

9: $b_{\ell}:=$ the least element of $\mathbf{b}_{\ell}$

10:
$C_{\ell}:=\min(k_{\ell},\lceil\frac{\beta_{\ell}-b_{\ell}}{w_{\ell}\cdot\epsilon_{\ell}}\rceil)$

11: $\alpha_{\ell-1}:=\frac{\beta_{\ell}-b_{\ell}}{w_{\ell}}$

Theorem 10 shows that, in each layer of $\ell$, every $k_{\ell}$ that is
larger than $C_{\ell}$ can be replaced by $C_{\ell}$ without affecting the
result of applying $\mathcal{N}$ to any dataset.

######  Theorem 10.

Let $\mathcal{N}^{\prime}$ be the $(\mathsf{Col},\delta)$-GNN obtained from
$\mathcal{N}$ by replacing $k_{\ell}$ with $C_{\ell}$ for each ${1\leq\ell\leq
L}$. Then, ${T_{\mathcal{N}}(D)=T_{\mathcal{N}^{\prime}}(D)}$ for each
$(\mathsf{Col},\delta)$-dataset $D$.

Theorem 10 can be intuitively understood as follows. Let
$\mathbf{v}_{\lambda_{\ell}}$ and $\mathbf{v}_{\lambda_{\ell}^{\prime}}$ be
vectors labelling a vertex $v$ in layer $\ell$ when $T_{\mathcal{N}}$ and
$T_{\mathcal{N}^{\prime}}$ are applied to some $D$. We prove the theorem by
showing that either
${(\mathbf{v}_{\lambda_{\ell}})_{i}=(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$
or
${(\mathbf{v}_{\lambda_{\ell}})_{i}>(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}\geq\alpha_{\ell}}$
for each layer ${\ell\geq\ell_{\mathsf{st}}}$, where $\ell_{\mathsf{st}}$ is
either the layer where Algorithm 1 performs an early return (via line 7) or
$0$ if this does not happen. Indeed, assume that
${\mathsf{cls}((\mathbf{v}_{\lambda_{L}})_{i})=1}$ for some $v$. If
$\mathbf{A}_{L}$ and all $\mathbf{B}_{L}^{c}$ contain only zeros, or if all
$\mathcal{X}_{L,i}$ contain only zeros, then $L=\ell_{\mathsf{st}}$; no
neighbours of $v$ are needed so we can set all $C_{\ell}$ to $0$ and the
equality above holds. Otherwise, $\mathsf{cls}$ is a threshold function, so
${(\mathbf{v}_{\lambda_{L}})_{i}\geq\alpha_{L}}$ holds for $\alpha_{L}$ the
threshold of $\mathsf{cls}$, and so the argument to the activation function
when computing $(\mathbf{v}_{\lambda_{L}})_{i}$ is at least $\beta_{L}$.
Moreover, $(\mathbf{v}_{\lambda_{L}})_{i}$ is produced from
$(\mathbf{v}_{\lambda_{L-1}})_{i}$ and the values of
$(\mathbf{u}_{\lambda_{L-1}})_{j}$ where $u$ ranges over the neighbours of
$v$. If we assume that ${(\mathbf{v}_{\lambda_{L-1}})_{i}=0}$ and that
$\epsilon_{\ell}$ is the least nonzero value that each $u$ can contribute to
$(\mathbf{v}_{\lambda_{L}})_{i}$, it suffices to have at least
${\lceil\frac{\beta_{\ell}-b_{\ell}}{w_{\ell}\cdot\epsilon_{\ell}}\rceil}$
nonzero neighbours to reach $\beta_{L}$. Thus, we can replace $k_{\ell}$ with
this number whenever this number is smaller than $k_{\ell}$; in contrast, if
$k_{\ell}$ is smaller, we need to keep $k_{\ell}$ so that
$\mathcal{N}^{\prime}$ does not derive any new consequences. Finally,
$\alpha_{L-1}$ is the value of $(\mathbf{v}_{\lambda_{L-1}})_{i}$ in layer
$L-1$ to which we can apply analogous reasoning.

###  4.2 Equivalence with Datalog Programs

We next show that there exists a Datalog program $\mathcal{P}_{\mathcal{N}}$
that is equivalent to $\mathcal{N}$ in the sense described in Definition 4.
Towards this goal, in Definition 11 we capture the syntactic structure of the
rules in $\mathcal{P}_{\mathcal{N}}$ as rules of form (39) where $\varphi$ is
a _tree-like_ formula for $x$. To understand the intuition, assume that we
construct from $\varphi$ a graph whose vertices are the variables in
$\varphi$, and where a directed edge from $x$ to $y$ is introduced for each
$E^{c}(x,y)$ in $\varphi$; then, such graph must be a directed tree. Moreover,
if variable $x$ has children $y_{1}$ and $y_{2}$ in this graph, then $\varphi$
is allowed to contain inequalities of the form ${y_{1}\not\approx y_{2}}$,
which provide $\varphi$ with a limited capability for counting; for example,
formula ${E^{c}(x,y_{1})\wedge E^{c}(x,y_{2})\wedge y_{1}\not\approx y_{2}}$
is true precisely for those values of $x$ that are connected via the $E^{c}$
predicate to at least two distinct constants. We also introduce intuitive
notions of a _fan-out_ (i.e., the number of children) and _depth_ of a
variable. Tree-like formulas contain all concepts of the $\mathcal{ALCQ}$
description logic (?) constructed from $\top$, atomic concepts, and concepts
of the form ${\geq nR.C}$ and ${C_{1}\sqcap C_{2}}$; however, our definition
also allows for formulas such as ${E^{c}(x,y_{1})\wedge E^{c}(x,y_{2})\wedge
U(y_{1})\wedge y_{1}\not\approx y_{2}}$, which do not correspond to the
translation of $\mathcal{ALCQ}$ concepts.

######  Definition 11.

A _tree-like formula for a variable_ is defined inductively as follows.

  * •

For each variable $x$, formula $\top$ is tree-like for $x$.

  * •

For each variable $x$ and each unary predicate $U$, atom $U(x)$ is tree-like
for $x$.

  * •

For each variable $x$ and all tree-like formulas $\varphi_{1}$ and
$\varphi_{2}$ for $x$ that share no variables other than $x$, formula
${\varphi_{1}\wedge\varphi_{2}}$ is tree-like for $x$.

  * •

For each variable $x$, each binary predicate $E^{c}$, and all tree-like
formulas ${\varphi_{1},\dots,\varphi_{n}}$ for distinct variables
${y_{1},\dots,y_{n}}$ where no $\varphi_{i}$ contains $x$ and no $\varphi_{i}$
and $\varphi_{j}$ with ${i\neq j}$ share a variable, formula (38) is tree-like
for $x$.

$\displaystyle\bigwedge_{i=1}^{n}\Big{(}E^{c}(x,y_{i})\wedge\varphi_{i}\Big{)}\wedge\bigwedge_{1\leq
i<j\leq n}y_{i}\not\approx y_{j}$ (38)

Let $\varphi$ be a tree-like formula and let $x$ be a variable in $\varphi$.
The _fan-out_ of $x$ in $\varphi$ is the number of distinct variables $y_{i}$
for which $E^{c}(x,y_{i})$ is a conjunct of $\varphi$. The _depth_ of $x$ is
the maximal $n$ for which there exist variables ${x_{0},\dots,x_{n}}$ and
predicates ${E^{c_{1}},\dots,E^{c_{n}}}$ such that ${x_{n}=x}$ and
$E^{c_{i}}(x_{i-1},x_{i})$ is a conjunct of $\varphi$ for each ${1\leq i\leq
n}$. The _depth_ of $\varphi$ is the maximum depth of a variable in $\varphi$.

For $d$ and $f$ natural numbers, a tree-like formula $\varphi$ is _$(d,f)$
-tree-like_ if, for each variable $x$ in $\varphi$, the depth $i$ of $x$ is at
most $d$ and the fan-out of $x$ is at most $f(d-i)$. Moreover, a Datalog rule
is _$(d,f)$ -tree-like_ if it is of form (39), where $\varphi$ is a
$(d,f)$-tree-like formula for $x$.

$\displaystyle\varphi\rightarrow U(x)$ (39)

Note that $\varphi$ is allowed to be $\top$ in a rule of form (39); for
example, ${\top\rightarrow U(x)}$ is a valid $(0,0)$-tree-like rule. As
explained in Section 2, when applied to a dataset $D$, such a rule derives
$U(t)$ for each term $t$ occurring in $D$.

Now let ${\delta_{\mathcal{N}}=\max(\delta_{0},\dots,\delta_{L})}$. To
construct $\mathcal{P}_{\mathcal{N}}$, we proceed as follows: we compute
${f=|\mathsf{Col}|\cdot\delta_{\mathcal{N}}\cdot C_{\mathcal{N}}}$, we
enumerate all $(L,f)$-tree-like rules (up to variable renaming), and we add to
$\mathcal{P}_{\mathcal{N}}$ each such rule that is captured by $\mathcal{N}$.
Lemma 12 shows that this latter test can, at least in principle, be
operationalised. In particular, to test whether a rule ${\varphi\rightarrow
U(x)}$ with $n$ variables is captured by $\mathcal{N}$, we consider each
possible dataset $D$ obtained from the atoms of $\varphi$ by substituting the
variables with up to $n$ distinct constants, and we check whether applying
$\mathcal{N}$ to $D$ derives the analogously instantiated rule head; if this
is the case for all such $D$, then the rule is captured by $\mathcal{N}$. ?
(?) used a similar test for MGNNs, but their approach was simpler since it did
not need to support inequalities. Theorem 13 then shows that program
$\mathcal{P}_{\mathcal{N}}$ is indeed equivalent to $\mathcal{N}$.

######  Lemma 12.

Let $r$ be a constant-free Datalog rule with head $H$, let $V$ be the set of
variables in $r$, and let $A$ be the set of body atoms of $r$. Then,
$\mathcal{N}$ captures $r$ if and only if ${H\nu\in T_{\mathcal{N}}(A\nu)}$
for each substitution ${\nu:V\to S}$ such that ${H\nu\in T_{r}(A\nu)}$, where
$S$ is a set of $|V|$ distinct constants.

######  Theorem 13.

Let $\mathcal{P}_{\mathcal{N}}$ be the Datalog program containing, up to
variable renaming, each ${(L,|\mathsf{Col}|\cdot\delta_{\mathcal{N}}\cdot
C_{\mathcal{N}})}$-tree-like rule captured by $\mathcal{N}$, where
${\delta_{\mathcal{N}}=\max(\delta_{0},\dots,\delta_{L})}$. Then,
$\mathcal{N}$ and $\mathcal{P}_{\mathcal{N}}$ are equivalent.

To understand this result intuitively, assume that $\mathcal{N}$ is applied to
a dataset $D$. The fact that all rules of $\mathcal{P}_{\mathcal{N}}$ are
captured by $\mathcal{N}$ clearly implies
$T_{\mathcal{P}_{\mathcal{N}}}(D)\subseteq T_{\mathcal{N}}(D)$. Furthermore,
by equation (7), the value of $(\mathbf{v}_{L})_{i}$ for some $i$ is computed
from the values of $(\mathbf{v}_{L-1})_{i}$ and $(\mathbf{u}_{L-1})_{j}$ for
$k\leq C_{L}$ distinct neighbours $u$ of $v$ per colour and position; but
then, if $t$ and $s$ are terms represented by $v$ and $u$, respectively, the
canonical encoding ensures ${E^{c}(t,s)\in D}$ for some ${c\in\mathsf{Col}}$.
Also, $(\mathbf{u}_{L-1})_{j}$ are computed using the neighbours of $u$ and so
on. Hence, each term $w$ in $D$ that can possibly influence $\mathbf{v}_{L}$
must be connected in $D$ to $t$ by at most $L$ such facts, so all relevant
neighbours of $t$ can be selected by a $(d,f)$-tree-like formula. The
inequalities can be used to check for the existence of at least $k$ distinct
neighbours of $t$ in $D$. Now let $D^{\prime}$ be the subset of $D$ containing
precisely the facts that contribute to the value of $(\mathbf{v}_{L})_{i}$. We
can unfold $D^{\prime}$ into another tree-like dataset $D^{\prime\prime}$ that
corresponds to the body of an instantiated tree-like rule $r$. Since the
elements of all $\mathbf{A}_{\ell}$ and $\mathbf{B}_{\ell}^{c}$ are
nonnegative, applying $\mathcal{N}$ to $D$ and $D^{\prime\prime}$ derives the
same value for $\mathsf{cls}((\mathbf{v}_{L})_{i})$. If this value is $1$,
then applying the rule $r$ to $D$ produces the same fact as $\mathcal{N}$.
Furthermore, by definition, $\mathcal{N}$ captures $r$ and so
${r\in\mathcal{P}_{\mathcal{N}}}$. Thus, $T_{\mathcal{P}_{\mathcal{N}}}(D)$
contains all facts derived by $\mathcal{N}$ on $D$.

###  4.3 Enumerating Sets $\mathcal{X}_{\ell,i}$

The results we presented thus far show that program
$\mathcal{P}_{\mathcal{N}}$ exists, but it is not yet clear that
$\mathcal{P}_{\mathcal{N}}$ is computable: the definition of $C_{\ell}$ in
Algorithm 1 uses sets $\mathcal{X}_{\ell,i}$, which can be infinite. We next
show that each $\mathcal{X}_{\ell,i}$ can be enumerated algorithmically using
function $\mathsf{Next}(\ell,i,\alpha)$ from Algorithm 2 as follows: for
$\alpha$ a special symbol ${\vartriangleright}$, function
$\mathsf{Next}(\ell,i,{\vartriangleright})$ returns the smallest element of
$\mathcal{X}_{\ell,i}$; moreover, for ${\alpha\in\mathbb{R}}$, function
$\mathsf{Next}(\ell,i,\alpha)$ returns the smallest element of
$\mathcal{X}_{\ell,i}^{>\alpha}$ if
${\mathcal{X}_{\ell,i}^{>\alpha}\neq\emptyset}$, or ${\vartriangleleft}$
otherwise. For example, $\mathsf{Next}(\ell,i,0)$ returns the smallest nonzero
element of $\mathcal{X}_{\ell,i}$, if one exists.

Algorithm 2 $\mathsf{Next}(\ell,i,\alpha)$

1:if $\ell=0$ then

2: if $\alpha={\vartriangleright}$ or $\alpha<0$ then return $0$

3: else if $\alpha<1$ then return $1$

4: else return ${\vartriangleleft}$

5:let $\mathbf{Y}_{\emptyset}$ be such that
$\mathbf{Y}^{c}_{\emptyset}=\emptyset$ for each $c\in\mathsf{Col}$

6:$z:=\mathsf{Val}(\ell,i,\mathsf{Start}(\ell),\mathbf{Y}_{\emptyset})$

7:if $\alpha={\vartriangleright}$ then return $\sigma(z)$

8:$F:=\\{\langle\mathsf{Start}(\ell),\mathbf{Y}_{\emptyset},z\rangle\\}$

9:while $F\neq\emptyset$ do

10: choose and remove $\langle\mathbf{x},\mathbf{Y},z\rangle$ in $F$ with
least $z$

11: if $\sigma(z)>\alpha$ then return $\sigma(z)$

12: for $\mathbf{x}^{\prime}\in\mathsf{Expand}(\ell,\mathbf{x})$ do

13: $z^{\prime}:=\mathsf{Val}(\ell,i,\mathbf{x}^{\prime},\mathbf{Y})$

14: if $z^{\prime}>z$ then add
$\langle\mathbf{x}^{\prime},\mathbf{Y},z^{\prime}\rangle$ to $F$

15: for $c\in\mathsf{Col}$ do

16: for $\mathbf{y}\in\mathbf{Y}^{c}$ and
$\mathbf{y}^{\prime}\in\mathsf{Expand}(\ell,\mathbf{y})$ do

17: $\mathbf{Y}^{\prime}:=\mathbf{Y}$ and $\mathbf{Y}^{\prime
c}:=(\mathbf{Y}^{\prime
c}\setminus\\{\mathbf{y}\\})\cup\\{\mathbf{y}^{\prime}\\}$

18: $z^{\prime}:=\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y}^{\prime})$

19: if $z^{\prime}>z$ then add
$\langle\mathbf{x},\mathbf{Y}^{\prime},z^{\prime}\rangle$ to $F$

20: if $\mathsf{Start}(\ell)$ contains a nonzero then

21: $V:=\\{\mathsf{Start}(\ell)\\}$

22: else

23: $V:=\mathsf{Expand}(\ell,\mathsf{Start}(\ell))$

24: for $\mathbf{y}^{\prime}\in V$ do

25: $\mathbf{Y}^{\prime}:=\mathbf{Y}$ and $\mathbf{Y}^{\prime
c}:=\mathbf{Y}^{\prime c}\cup\\{\mathbf{y}^{\prime}\\}$

26: $z^{\prime}:=\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y}^{\prime})$

27: if $z^{\prime}>z$ then add
$\langle\mathbf{x},\mathbf{Y}^{\prime},z^{\prime}\rangle$ to $F$

28:return ${\vartriangleleft}$

29:function $\mathsf{Start}$($\ell$)

30: return the vector $\mathbf{x}$ of dimension $\delta_{\ell-1}$ where

31: $(\mathbf{x})_{j}=\mathsf{Next}(\ell-1,j,{\vartriangleright})$ for $1\leq
j\leq\delta_{\ell-1}$

32:function $\mathsf{Expand}$($\ell,\mathbf{v}$)

33: $V:=\emptyset$

34: for $1\leq j\leq\delta_{\ell-1}$ do

35: $v^{\prime}:=\mathsf{Next}(\ell-1,j,(\mathbf{v})_{j})$

36: if $v^{\prime}\neq{\vartriangleleft}$ then
$V:=V\cup\\{\mathbf{v}[j\leftarrow v^{\prime}]\\}$

37: return $V$

In the presentation of Algorithm 2, we use the following notation: for
$\mathbf{x}$ a vector, $j$ an index, and $v$ a real number,
$\mathbf{x}[j\leftarrow v]$ is the vector obtained from $\mathbf{x}$ by
replacing its $j$-th component with $v$. The algorithm is based on the
observation that, since $\mathbf{A}_{\ell}$ and $\mathbf{B}_{\ell}^{c}$
contain only nonnegative elements, and the activation function is
monotonically increasing, we can enumerate the values computed by equation (7)
in some $\mathbf{v}_{\ell}$ in a monotonically increasing fashion. To achieve
this, the algorithm maintains a _frontier_ $F$ of triples
$\langle\mathbf{x},\mathbf{Y},z\rangle$, each describing one way to compute a
value of $(\mathbf{v}_{\ell})_{i}$: vector $\mathbf{x}$ reflects the values of
$(\mathbf{v}_{\ell-1})_{i}$, the $(\mathsf{Col},\ell-1)$-multiset family
$\mathbf{Y}$ describes multisets $\mathbf{Y}^{c}$ reflecting the values of
$(\mathbf{u}_{\ell-1})_{i}$, and $z$ is
$\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})$—that is, the argument to the
activation function when computing $(\mathbf{v}_{\ell})_{i}$. The starting
point for the exploration (line 8) is provided by $\mathsf{Start}(\ell)$,
which returns $\mathbf{v}_{\ell}$ for a vertex $v$ with no neighbours. To
enumerate all candidate values for $(\mathbf{v}_{\ell})_{i}$ in an increasing
order, the algorithm selects a triple in the frontier with the smallest $z$
(line 10), and considers ways to modify $\mathbf{x}$ or $\mathbf{Y}$ that
increase $z$; each such combination is added to the frontier (lines 14, 19,
and 27). Modifications involve replacing some component of $\mathbf{x}$ with
the next component (lines 12–14), choosing some
${\mathbf{y}\in\mathbf{Y}^{c}}$ for some ${c\in\mathsf{Col}}$ and replacing
some component of $\mathbf{y}$ with the next component (lines 16–19), or
expanding some $\mathbf{Y}^{c}$ with an additional vector (lines 20–27). In
the latter case, if $\mathsf{Start}(\ell)$ contains just zeros, then adding
$\mathsf{Start}(\ell)$ to $\mathbf{Y}^{c}$ is not going to change the computed
value of $z$ so the algorithm considers vectors obtained by expanding
$\mathsf{Start}(\ell)$ in order to allow $z$ to increase. This process
produces values of $z$ in an increasing order and it guarantees that
${\sigma(z)\in\mathcal{X}_{\ell,i}}$. If ${\alpha={\vartriangleright}}$, the
algorithm stops when the first such value is produced (line 7). For
${\alpha\in\mathbb{R}}$, Theorem 8 guarantees that set
${\mathcal{X}_{\ell,i}\setminus\mathcal{X}_{\ell,i}^{>\alpha}}$ is finite;
since $F$ is extended only if the value of $z$ increases, either $F$
eventually becomes empty or $\sigma(z)$ exceeds $\alpha$ so the algorithm
terminates (line 11 or 28). Theorem 14 captures the formal properties of the
algorithm.

######  Theorem 14.

Algorithm 2 terminates on all inputs. Moreover, for ${0\leq\ell\leq L}$ and
${1\leq i\leq\delta_{\ell}}$,

  * •

$\mathsf{Next}(\ell,i,{\vartriangleright})$ returns the smallest element of
$\mathcal{X}_{\ell,i}$, and

  * •

for each ${\alpha\in\mathbb{R}}$, $\mathsf{Next}(\ell,i,\alpha)$ returns
${\vartriangleleft}$ if ${\mathcal{X}_{\ell,i}^{>\alpha}=\emptyset}$, and
otherwise it returns the smallest element of $\mathcal{X}_{\ell,i}^{>\alpha}$.

The complexity of Algorithm 14 depends on the number of recursive calls to
$\mathsf{Next}$, which in turn depends on the matrices of $\mathcal{N}$. We
leave investigating this issue to future work.

##  5 Limiting Aggregation to Max

In this section we study the expressivity of _monotonic max GNNs_ , which
follow the same restrictions as monotonic max-sum GNNs but additionally allow
only for the max aggregation function. Theorem 16 shows that each such GNN
corresponds to a Datalog program without inequalities. Consequently, monotonic
max GNNs cannot count the connections of a constant in a dataset.

######  Definition 15.

A _monotonic max_ $(\mathsf{Col},\delta)$_-GNN_ is a monotonic max-sum GNN
that uses the $\mathrm{max}\text{-}{1}\text{-}\mathrm{sum}$ aggregation
function in all layers.

######  Theorem 16.

For each monotonic max $(\mathsf{Col},\delta)$-GNN $\mathcal{N}$ with $L$
layers, let ${\delta_{\mathcal{N}}=\max(\delta_{0},\dots,\delta_{L})}$, and
let $\mathcal{P}_{\mathcal{N}}$ be the Datalog program containing up to
variable renaming each $(L,|\mathsf{Col}|\cdot\delta_{\mathcal{N}})$-tree-like
rule without inequalities captured by $\mathcal{N}$. Then, $\mathcal{N}$ and
$\mathcal{P}_{\mathcal{N}}$ are equivalent.

? (?) presented a closely related characterisation for MGNNs, and the main
difference is that we use the canonical encoding. The latter allows us to
describe the target Datalog class more precisely, which in turn allows us to
prove the converse: each Datalog program with only tree-like rules and without
inequalities is equivalent to a monotonic max GNN.

In what follows, we fix a program $\mathcal{P}$ consisting of $(d,f)$-tree-
like rules without inequalities. Recall that the signature of $\mathcal{P}$
consists of unary predicates ${U_{1},\dots,U_{\delta}}$ and binary predicates
$E^{c}$ for ${c\in\mathsf{Col}}$. Now let ${\tau_{1},\dots,\tau_{n}}$ be a
sequence containing up to variable renaming each $(d,f)$-tree-like formula for
variable $x$ without inequalities ordered by increasing depth—that is, for all
${i<j}$, the depth of $\tau_{i}$ is less than or equal to the depth of
$\tau_{j}$. Each $\tau_{i}$ can be written as

$\displaystyle\tau_{i}=\varphi_{i,0}\wedge\bigwedge_{k=1}^{m_{i}}\Big{(}E^{c_{k}}(x,y_{k})\wedge\varphi_{i,k}\Big{)},$
(40)

where $\varphi_{i,0}$ is a conjunction of unary atoms using only variable $x$,
each $\varphi_{i,k}$ with $1\leq k\leq m_{i}$ is a $(d-1,f)$-tree-like formula
for $y_{k}$, and, for all ${1\leq k<k^{\prime}\leq m_{i}}$, formulas
$\varphi_{i,k}$ and $\varphi_{i,k^{\prime}}$ do not have variables in common.
Note that formulas $\varphi_{i,k}$ can be $\top$, and that colours $c_{k}$
need not be distinct.

We define $\mathcal{N}_{\mathcal{P}}$ as the monotonic max
$(\mathsf{Col},\delta)$-GNN of form (4) satisfying the following conditions.
The number of layers is ${L=d+2}$, the activation function is ReLU, and the
classification function $\mathsf{cls}$ is the step function with threshold
$1$. For ${1\leq\ell<L}$, dimension $\delta_{\ell}$ is defined as the number
of formulas in the above sequence of depth at most ${\ell-1}$. The elements of
$\mathbf{A}_{\ell}$, $\mathbf{B}_{\ell}^{c}$, and $\mathbf{b}_{\ell}$ are
defined as follows, for ${c\in\mathsf{Col}}$, ${1\leq\ell\leq L}$, ${1\leq
i\leq\delta_{\ell}}$, and ${1\leq j\leq\delta_{\ell-1}}$.

$\displaystyle(\mathbf{A}_{\ell})_{i,j}=\left\\{\begin{array}[]{@{\;\;}l@{\;\;}l@{\;}l@{}}1&\text{if}&\\\
&\text{\textbullet}&\ell=1\text{ and }\tau_{i}\text{ contains }U_{j}(x);\text{
or}\\\ &\text{\textbullet}&2\leq\ell<L\text{ and}\\\ &&-\;1\leq
i\leq\delta_{\ell-1}\text{ and }i=j,\text{ or }\\\
&&-\;\delta_{\ell-1}<i\leq\delta_{\ell}\text{ and
}\varphi_{i,0}=\tau_{j};\text{ or}\\\ &\text{\textbullet}&\ell=L\text{ and
}\mathcal{P}\text{ contains rule}\\\ &&\tau_{j}\rightarrow U_{i}(x)\text{ up
to variable renaming;}\\\\[4.30554pt]<EMAIL_ADDRESS>\end{array}\right.$
$\displaystyle(\mathbf{B}_{\ell}^{c})_{i,j}=\left\\{\begin{array}[]{@{\;\;}l@{\;\;}l@{}}1&\text{if
}2\leq\ell<L\text{ and there exists }1\leq k\leq m_{i}\\\ &\text{such that
}c=c_{k}\text{ and }\varphi_{i,k}\text{ and }\tau_{j}\\\ &\text{are equal up
to variable renaming;}\\\\[4.30554pt] 0&\text{otherwise.}\\\
\end{array}\right.$
$\displaystyle(\mathbf{b}_{\ell})_{i}=\left\\{\begin{array}[]{@{}l@{\;}l@{}}1-\sum\limits_{j=1}^{\delta_{\ell-1}}((\mathbf{A}_{\ell})_{i,j}+\\!\sum\limits_{c\in\mathsf{Col}}(\mathbf{B}_{\ell}^{c})_{i,j})&\begin{array}[]{@{}l@{}}\text{if
}\ell=1,\text{ or }\\\ 1\leq\ell<L\text{ and }\\\
\delta_{\ell-1}<i\leq\delta_{\ell};\\\ \end{array}\\\\[17.22217pt]
0&\text{otherwise.}\\\ \end{array}\right.$

To understand the intuition behind the construction of
$\mathcal{N}_{\mathcal{P}}$, assume that $\mathcal{N}_{\mathcal{P}}$ is
applied to a dataset $D$, and consider a vector $\mathbf{v}_{\ell}$ labelling
in layer $\ell$ a vertex corresponding to some term $t$ of $D$. Then, the
$i$-th component of $\mathbf{v}_{\ell}$ is paired with formula $\tau_{i}$ from
the above enumeration, and it indicates whether it is possible to evaluate
$\tau_{i}$ over $D$ by mapping variable $x$ to $t$. This is formally captured
by Lemma 17. To ensure that $\mathcal{N}_{\mathcal{P}}$ and $\mathcal{P}$ are
equivalent, layer $L$ of $\mathcal{N}_{\mathcal{P}}$ simply realises a
disjunction over all rules in the program.

######  Lemma 17.

For each $(\mathsf{Col},\delta)$-dataset $D$, layer ${1\leq\ell<L}$ of
$\mathcal{N}_{\mathcal{P}}$, position ${1\leq i\leq\delta_{\ell}}$, and term
$t$ in $D$, and for $\mathbf{v}_{\ell}$ the labelling of the vertex
corresponding to $t$ when $\mathcal{N}_{\mathcal{P}}$ is applied to the
canonical encoding of $D$,

  * •

${(\mathbf{v}_{\ell})_{i}=1}$ if there exists a substitution $\nu$ mapping $x$
to $t$ such that ${D\models\tau_{i}\nu}$, and

  * •

${(\mathbf{v}_{\ell})_{i}=0}$ otherwise.

Note that each $\delta_{\ell}$ with ${1\leq\ell<L}$ is determined by the
number of $(d,f)$-tree-like formulas of depth $\ell-1$, and that
$\delta_{L-1}$ is the largest such number. We next determine an upper bound on
$\delta_{L-1}$. By Definition 11, the fan-out of a variable of depth $i$ is at
most $f(d-i)$. The number of variables of depth $i$ is at most the number of
variables of depth $i-1$ times the fan-out of each variable, which is
${f^{i}\cdot d\dots(d-i+1)}$ and is bounded by ${f^{i}\cdot d!}$. By adding up
the contribution for each depth, there are at most ${f^{d}\cdot(d+1)!}$
variables. Each variable is labelled by one of the ${2^{\delta}}$ conjunctions
of depth zero, and each non-root variable is connected by one of the
$|\mathsf{Col}|$ predicates to its parent. Hence, there are at most
${(|\mathsf{Col}|\cdot 2^{\delta})^{f^{d}\cdot(d+1)!}}$ tree-like formulas.

######  Theorem 18.

Program $\mathcal{P}$ and GNN $\mathcal{N}_{\mathcal{P}}$ are equivalent, and
moreover ${\delta_{L-1}\leq(|\mathsf{Col}|\cdot
2^{\delta})^{f^{d}\cdot(d+1)!}}$.

##  6 Conclusion

We have shown that each monotonic max-sum GNN (i.e., a GNN that uses max and
sum aggregation functions and satisfies certain properties) is equivalent to a
Datalog program with inequalities in the sense that applying the GNN or a
single round of the rules of the program to any dataset produces the same
result. We have also sharpened this result to monotonic max GNNs and shown the
converse: each tree-like Datalog program without inequalities is equivalent to
a monotonic max GNN. We see many avenues for future work. First, we aim to
completely characterise monotonic max-sum GNNs. Second, we intend to implement
rule extraction. Third, we shall investigate the empirical performance of
monotonic max-sum GNNs on tasks other than link prediction, such as node
classification.

## Acknowledgements

This work was supported by the SIRIUS Centre for Scalable Data Access
(Research Council of Norway, project number 237889), and the EPSRC projects
ConCur (EP/V050869/1), UK FIRES (EP/S019111/1), and AnaLOG (EP/P025943/1). For
the purpose of Open Access, the author has applied a CC BY public copyright
licence to any Author Accepted Manuscript (AAM) version arising from this
submission.

## References

  * 1995 Abiteboul, S.; Hull, R.; and Vianu, V.  1995\.  Foundations of Databases.  Addison Wesley.
  * 2007 Baader, F.; Calvanese, D.; McGuinness, D.; Nardi, D.; and Patel-Schneider, P. F., eds.  2007\.  The Description Logic Handbook: Theory, Implementation and Applications.  Cambridge University Press, 2nd edition.
  * 2007 Bader, S.; Hitzler, P.; Hölldobler, S.; and Witzel, A.  2007\.  A Fully Connectionist Model Generator for Covered First-Order Logic Programs.  In Proc. IJCAI, 666–671.
  * 2005 Bader, S.; d’Avila Garcez, A. S.; and Hitzler, P.  2005\.  Computing First-Order Logic Programs by Fibring Artificial Neural Networks.  In Proc. FLAIRS, 314–319.  AAAI Press.
  * 2020 Barceló, P.; Kostylev, E. V.; Monet, M.; Pérez, J.; Reutter, J. L.; and Silva, J. P.  2020\.  The Logical Expressiveness of Graph Neural Networks.  In Proc. ICLR.
  * 2018 Campero, A.; Pareja, A.; Klinger, T.; Tenenbaum, J.; and Riedel, S.  2018\.  Logical rule induction and theory learning using neural theorem proving.  CoRR abs/1809.02193.
  * 2001 Dantsin, E.; Eiter, T.; Gottlob, G.; and Voronkov, A.  2001\.  Complexity and expressive power of logic programming.  ACM Comput. Surv. 33(3):374–425.
  * 2019 Dong, H.; Mao, J.; Lin, T.; Wang, C.; Li, L.; and Zhou, D.  2019\.  Neural Logic Machines (Poster).  In Proc. ICLR.
  * 1999 Hölldobler, S.; Kalinke, Y.; and Störr, H.-P.  1999\.  Approximating the Semantics of Logic Programs by Recurrent Neural Networks.  Applied Intelligence 11(1):45–58.
  * 2023 Huang, X.; Orth, M. A. R.; Ceylan, İ. İ.; and Barceló, P.  2023\.  A theory of link prediction via relational weisfeiler-leman.  CoRR abs/2302.02209.
  * 2019 Ioannidis, V. N.; Marques, A. G.; and Giannakis, G. B.  2019\.  A recurrent graph neural network for multi-relational data.  In Proc. ICASSP, 8157–8161.  IEEE.
  * 2017 Kipf, T. N., and Welling, M.  2017\.  Semi-supervised classification with graph convolutional networks.  In Proc. ICLR.
  * 2021 Liu, S.; Cuenca Grau, B.; Horrocks, I.; and Kostylev, E. V.  2021\.  INDIGO: gnn-based inductive knowledge graph completion using pair-wise encoding.  In Proc. NeurIPS, 2034–2045.
  * 2019 Morris, C.; Ritzert, M.; Fey, M.; Hamilton, W. L.; Lenssen, J. E.; Rattan, G.; and Grohe, M.  2019\.  Weisfeiler and Leman Go Neural: Higher-Order Graph Neural Networks.  In Proc. AAAI, 4602–4609.  AAAI Press.
  * 2012 Motik, B.; Cuenca Grau, B.; Horrocks, I.; Wu, Z.; Fokoue, A.; and Lutz, C.  2012\.  OWL 2 Web Ontology Language: Profiles (2nd Edition).  World Wide Web Consortium.
  * 2009 Pérez, J.; Arenas, M.; and Gutierrez, C.  2009\.  Semantics and complexity of SPARQL.  ACM Trans. Database Syst. 34(3):16:1–16:45.
  * 2022 Pflueger, M.; Tena Cucala, D. J.; and Kostylev, E. V.  2022\.  GNNQ: A neuro-symbolic approach to query answering over incomplete knowledge graphs.  In Proc. ISWC, volume 13489 of Lecture Notes in Computer Science, 481–497.  Springer.
  * 2019 Qu, M.; Bengio, Y.; and Tang, J.  2019\.  GMNN: graph markov neural networks.  In Proc. ICML, volume 97 of Proceedings of Machine Learning Research, 5241–5250.
  * 2017 Rocktäschel, T., and Riedel, S.  2017\.  End-to-end Differentiable Proving.  In Proc. NeurIPS, 3788–3800.
  * 2019 Sadeghian, A.; Armandpour, M.; Ding, P.; and Wang, D. Z.  2019\.  DRUM: End-To-End Differentiable Rule Mining On Knowledge Graphs.  In Proc. NeurIPS, 15321–15331.
  * 2018 Schlichtkrull, M. S.; Kipf, T. N.; Bloem, P.; van den Berg, R.; Titov, I.; and Welling, M.  2018\.  Modeling relational data with graph convolutional networks.  In Proc. ESWC, volume 10843 of LNCS, 593–607.  Springer.
  * 2021 Sourek, G.; Zelezný, F.; and Kuzelka, O.  2021\.  Beyond graph neural networks with lifted relational neural networks.  Mach. Learn. 110(7):1695–1738.
  * 2022 Tena Cucala, D.; Cuenca Grau, B.; Kostylev, E. V.; and Motik, B.  2022\.  Explainable GNN-Based Models over Knowledge Graphs.  In Proc. ICLR.
  * 2022 Tena Cucala, D.; Cuenca Grau, B.; and Motik, B.  2022\.  Faithful Approaches to Rule Learning.  In Proc. KR, 484–493.
  * 2020 Teru, K. K.; Denis, E. G.; and Hamilton, W. L.  2020\.  Inductive relation prediction by subgraph reasoning.  In Proc. ICML, volume 119 of Proceedings of Machine Learning Research, 9448–9457.  PMLR.
  * 2016 Yang, Z.; Cohen, W. W.; and Salakhutdinov, R.  2016\.  Revisiting semi-supervised learning with graph embeddings.  In Proc. ICML, volume 48 of JMLR Workshop and Conference Proceedings, 40–48.
  * 2017 Yang, F.; Yang, Z.; and Cohen, W. W.  2017\.  Differentiable Learning of Logical Rules for Knowledge Base Reasoning.  In Proc. NeurIPS, 2319–2328.
  * 2018 Zhang, M., and Chen, Y.  2018\.  Link prediction based on graph neural networks.  In Proc. NeurIPS, 5171–5181.

##  Appendix A Proofs for Section 4

Throughout this appendix, we fix a max-sum GNN $\mathcal{N}$, dimensions
${\delta_{0},\dots,\delta_{L}}$, and aggregation functions
${k_{1},\dots,k_{L}}$ as specified in Section 4.1. As in Section 4.3, for
$\mathbf{x}$ a vector, $j$ an index, and $v$ a real number,
$\mathbf{x}[j\leftarrow v]$ is the vector obtained from $\mathbf{x}$ by
replacing its $j$th component with $v$.

To prove our results, we shall define a nonempty sequence
$\mathcal{S}_{\ell,i}$ for each ${0\leq\ell\leq L}$ and ${1\leq
i\leq\delta_{\ell}}$; intuitively, each $\mathcal{S}_{\ell,i}$ enumerates
$\mathcal{X}_{\ell,i}$ in ascending order. Our definition is inductive and
uses two auxiliary notions that we define next. In particular, consider an
arbitrary $\ell$ with ${0<\ell\leq L}$ and assume that
$\mathcal{S}_{\ell-1,i}$ have been defined for all ${1\leq
i\leq\delta_{\ell}}$. Then, $\mathbf{s}_{\ell-1}$ is the vector of dimension
$\delta_{\ell-1}$ such that $(\mathbf{s}_{\ell-1})_{i}$ is the first element
of $\mathcal{S}_{\ell,i}$ for each ${1\leq i\leq\delta_{\ell-1}}$. Moreover, a
_$(\ell,i)$ -triple_ is a triple of the form
$\langle\mathbf{x},\mathbf{Y},z\rangle$ whose components satisfy the following
conditions:

  * •

$\mathbf{x}$ is a vector of dimension $\delta_{\ell-1}$ such that
${(\mathbf{x})_{j}\in\mathcal{S}_{\ell-1,j}}$ holds for all ${1\leq
j\leq\delta_{\ell-1}}$;

  * •

$\mathbf{Y}$ is a $(\mathsf{Col},\ell-1)$-multiset family such that
${(\mathbf{y})_{j}\in\mathcal{S}_{\ell-1,j}}$ holds for all
${c\in\mathsf{Col}}$, ${\mathbf{y}\in\mathbf{Y}^{c}}$, and ${1\leq
j\leq\delta_{\ell-1}}$; and

  * •

${z=\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})}$.

An $(\ell,i)$-triple $\langle\mathbf{x}_{2},\mathbf{Y}_{2},z_{2}\rangle$ is a
successor of an $(\ell,i)$-triple
$\langle\mathbf{x}_{1},\mathbf{Y}_{1},z_{1}\rangle$ if exactly one of the
following conditions holds:

  * •

${\mathbf{Y}_{1}=\mathbf{Y}_{2}}$ and
${\mathbf{x}_{2}=\mathbf{x}_{1}[j\leftarrow x^{\prime}]}$ for some ${1\leq
j\leq\delta_{\ell-1}}$ and $x^{\prime}$ the element that succeeds
$(\mathbf{x})_{j}$ in $\mathcal{S}_{\ell-1,j}$; or

  * •

${\mathbf{x}_{2}=\mathbf{x}_{1}}$ and there exist a colour
${c\in\mathsf{Col}}$, vector ${\mathbf{y}\in\mathbf{Y}^{c}_{1}}$, and index
${1\leq j\leq\delta_{\ell-1}}$ such that
${\mathbf{Y}^{c^{\prime}}_{2}=\mathbf{Y}^{c^{\prime}}_{1}}$ for each colour
${c^{\prime}\in\mathsf{Col}\setminus\\{c\\}}$, and
${\mathbf{Y}^{c}_{2}=(\mathbf{Y}^{c}_{1}\setminus\\{\mathbf{y}\\})\cup\\{\mathbf{y}[j\leftarrow
y^{\prime}]\\}}$ where $y^{\prime}$ is the element that succeeds
$(\mathbf{y})_{j}$ in $\mathcal{S}_{\ell-1,j}$; or

  * •

${\mathbf{x}_{2}=\mathbf{x}_{1}}$ and there exist a colour
${c\in\mathsf{Col}}$ and index ${1\leq j\leq\delta_{\ell-1}}$ such that
${\mathbf{Y}^{c^{\prime}}_{2}=\mathbf{Y}^{c^{\prime}}_{1}}$ for each colur
${c^{\prime}\in\mathsf{Col}\setminus\\{c\\}}$, and
${\mathbf{Y}^{c}_{2}=\mathbf{Y}^{c}_{1}\cup\\{\mathbf{s}_{\ell-1}[j\leftarrow
y^{\prime}]\\}}$ where $y^{\prime}$ is the first positive element of
$\mathcal{S}_{\ell-1,j}$.

We are now ready to define sequences $\mathcal{S}_{\ell,i}$ for all
${0\leq\ell\leq L}$ and ${1\leq i\leq\delta_{\ell}}$.

  * •

For the base case ${\ell=0}$, let ${\mathcal{S}_{0,i}=(0,1)}$ for each ${1\leq
i\leq\delta_{0}}$.

  * •

For the inductive step, assume that $\mathcal{S}_{\ell-1,i}$ has been defined
for each ${1\leq i\leq\delta_{\ell-1}}$, and consider arbitrary ${1\leq
i\leq\delta_{\ell}}$. To define $\mathcal{S}_{\ell,i}$, we first define an
auxiliary sequence $\mathcal{F}_{\ell,i}$ of finite sets of $(\ell,i)$-triples
as follows.

    * –

For the base case, the first element of $\mathcal{F}_{\ell,i}$ is
${f_{0}=\\{\langle\mathbf{s}_{\ell-1},\mathbf{Y}_{\emptyset},z_{0}\rangle\\}}$,
where $\mathbf{Y}_{\emptyset}$ is such that
${\mathbf{Y}^{c}_{\emptyset}=\emptyset}$ for each ${c\in\mathsf{Col}}$ and
${z_{0}=\sigma(\mathsf{Val}(\ell,i,\mathbf{s}_{\ell-1},\mathbf{Y}_{\emptyset}))}$.

    * –

For the inductive step, assuming that $f_{n-1}$ with $n>0$ has been defined
and is not empty, let

$\begin{array}[]{@{}l@{\;\;}l@{}}f_{n}=&\\{\langle\mathbf{x},\mathbf{Y},z\rangle\in
f_{n-1}\mid z>\min(f_{n-1})\\}\;\cup\\\\[4.30554pt]
&\\{\langle\mathbf{x},\mathbf{Y},z\rangle\mid z>\min(f_{n-1})\text{ and
}\langle\mathbf{x},\mathbf{Y},z\rangle\mbox{ is a successor of some
}\langle\mathbf{x}^{\prime},\mathbf{Y}^{\prime},\min(f_{n-1})\rangle\in
f_{n-1}\\},\\\ \end{array}$

where $\min(f_{n})$ is the minimum number appearing in the third position of
an $(\ell,i)$-triple in $f_{n-1}$; such a number always exists since $f_{n-1}$
is never empty and it contains a finite number of triples. Then,
$\mathcal{S}_{\ell,i}$ is the sequence of real numbers whose $n$-th element is
$\sigma(\min(f_{n}))$ if $f_{n}$ is defined and ${f_{n}\neq\emptyset}$. Since
$f_{0}$ is always defined and not empty, $\mathcal{S}_{\ell,i}$ is not empty.

The following lemma shows that sequences $\mathcal{S}_{\ell,i}$ capture our
intuition mentioned above.

######  Lemma A.1.

For each ${1\leq\ell\leq L}$ and each ${1\leq i\leq\delta_{\ell}}$, sequence
$\mathcal{S}_{\ell,i}$ satisfies the following conditions:

  1. (S1)

each element of $\mathcal{S}_{\ell,i}$ is nonnegative;

  2. (S2)

$\mathcal{S}_{\ell,i}$ is strictly monotonically increasing;

  3. (S3)

$\mathcal{S}_{\ell,i}$ is either finite or it converges to $\infty$; and

  4. (S4)

the set of elements in $\mathcal{S}_{\ell,i}$ is $\mathcal{X}_{\ell,i}$.

###### Proof.

We prove all four conditions by induction over $\ell$. For the base case
$\ell=0$, sequence $\mathcal{S}_{0,i}$ is by definition is equal to $(0,1)$
for each ${1\leq i\leq\delta_{\ell}}$, so conditions (S1)–(S4) hold trivially.
Now consider arbitrary ${1\leq\ell\leq L}$ such that each
$\mathcal{S}_{\ell-1,j}$ with ${1\leq j\leq\delta_{\ell-1}}$ satisfies
conditions (S1)–(S4), and consider arbitrary ${1\leq i\leq\delta_{\ell}}$.

Condition (S1) follows straightforwardly from the fact that each element of
$\mathcal{S}_{\ell,i}$ for ${\ell\geq 1}$ is the image of $\sigma$ for some
real number $z$, and $\sigma(z)\geq 0$ for all $z\in\mathbb{R}$, since the
range of $\sigma$ is $\mathbb{R}^{+}_{0}$. Condition (S2) follows from the
fact that, for each ${n\in\mathbb{N}}$, each triple
${\langle\mathbf{x},\mathbf{Y},z\rangle\in f_{n}\setminus f_{n-1}}$ satisfies
$z>\min(f_{n-1})$, and so ${\min(f_{n})>\min(f_{n-1})}$ holds.

We prove Condition (S3) by contradiction—that is, we assume that
$\mathcal{S}_{\ell,i}$ is infinite, and that there exists some
$\bar{\alpha}\in\mathbb{R}$ such that each element of $\mathcal{S}_{\ell,i}$
is smaller than $\bar{\alpha}$.

Consider an arbitrary element $\alpha$ in $\mathcal{S}_{\ell,i}$. By the
definition of $\mathcal{S}_{\ell,i}$, there exists a triple
$\langle\mathbf{x},\mathbf{Y},z\rangle$ such that
${z=\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})}$, $\sigma(z)=\alpha$, and, for
each ${c\in\mathsf{Col}}$ and ${\mathbf{y}\in\mathbf{Y}^{c}}$, vector
$\mathbf{y}$ contains a nonzero element. Let $\bar{\beta}$ be the smallest
natural number such that ${\sigma(\bar{\beta})\geq\bar{\alpha}}$; such
$\bar{\beta}$ exists since $\sigma$ is unbounded. For each ${1\leq
j\leq\delta_{\ell-1}}$ and each ${c\in\mathsf{Col}}$, let $w_{j}$,
$\alpha_{j}$, and $n_{j,c}$ be as follows:

$\displaystyle w_{j}=$
$\displaystyle\min\\{(\mathbf{A}_{\ell})_{i,j}\\}\cup\\{(\mathbf{B}_{\ell}^{c})_{i,j}\mid
c\in\mathsf{Col}\\};$ (41) $\displaystyle\alpha_{j}=$
$\displaystyle\begin{cases}\frac{\bar{\beta}-(\mathbf{b}_{\ell})_{i}}{w_{\ell}}&\text{if
}w_{\ell}\neq 0,\\\ \text{undefined}&\text{otherwise};\\\ \end{cases}$ (42)
$\displaystyle\epsilon_{j}=$ $\displaystyle\begin{cases}\text{the first
positive value of }\mathcal{S}_{\ell-1,j}&\text{if such a value exists},\\\
\text{undefined}&\text{otherwise};\\\ \end{cases}$ (43) $\displaystyle
n_{j,c}=$
$\displaystyle\begin{cases}\lceil\frac{\bar{\beta}-(\mathbf{b}_{\ell})_{i}}{(\mathbf{B}_{\ell}^{c})_{i,j}\cdot\epsilon_{j}}\rceil&\text{if
}(\mathbf{B}_{\ell}^{c})_{i,j}\neq 0\text{ and }\epsilon_{j}\text{ is
defined};\\\ 0&\text{otherwise}.\\\ \end{cases}$ (44)

We next show the following properties:

  1. 1.

if ${(\mathbf{A}_{\ell})_{i,j}>0}$, then ${(\mathbf{x})_{j}<\alpha_{j}}$;

  2. 2.

for each ${c\in\mathsf{Col}}$, if ${(\mathbf{B}_{\ell}^{c})_{i,j}>0}$, then
${(\mathbf{y})_{j}<\alpha_{j}}$ for each ${\mathbf{y}\in\mathbf{Y}^{c}}$;

  3. 3.

for each ${c\in\mathsf{Col}}$, if ${(\mathbf{B}_{\ell}^{c})_{i,j}>0}$, then
there exist fewer than $n_{j,c}$ elements in $\mathbf{Y}^{c}$ whose $j$-th
element is not zero.

To see the first property, note that if ${(\mathbf{x})_{j}\geq\alpha_{j}}$,
then condition (S1) of the inductive hypothesis ensures that all elements of
$\mathbf{x}$ and vectors in $\mathbf{Y}$ are nonnegative; since the weights of
$\mathbf{A}_{\ell}$ and $\mathbf{B}_{\ell}^{c}$ are also nonnegative, we have

$\alpha=\sigma\Big{(}\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})\Big{)}\geq\sigma\Big{(}w_{j}\alpha_{j}+(\mathbf{b}_{\ell})_{i}\Big{)}=\sigma(\bar{\beta})\geq\bar{\alpha},$

which contradicts our assumption that all elements of $\mathcal{S}_{\ell,i}$
are smaller than $\bar{\alpha}$. The second property follows analogously. To
see the third property, assume that there exist at least $n_{j,c}$ vectors
$\mathbf{y}$ in $\mathbf{Y}^{c}$ such that $(\mathbf{y})_{j}>0$. Then,

$\alpha=\sigma\Big{(}\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})\Big{)}\geq\sigma\Big{(}(\mathbf{B}_{\ell}^{c})_{i,j}\sum_{\mathbf{y}\in\mathbf{Y}^{c}}(\mathbf{y})_{j}+(\mathbf{b}_{\ell})_{i}\Big{)}\geq\sigma\Big{(}(\mathbf{B}_{\ell}^{c})_{i,j}\cdot
n_{j}\cdot\epsilon_{j}+(\mathbf{b}_{\ell})_{i}\Big{)}\geq\sigma(\bar{\beta})\geq\bar{\alpha},$

which again contradicts our assumption that all elements of
$\mathcal{S}_{\ell,i}$ are smaller than $\bar{\alpha}$.

By conditions (S2) and (S3) of the inductive hypothesis, each
$\mathcal{S}_{\ell-1,j}$ is countable, monotonically increasing, and either
finite or converges to infinity; hence, set
${\\{s\in\mathcal{S}_{\ell-1,j}\mid s\leq\bar{\alpha}\\}}$ is finite. Thus, by
the three properties shown above, if $(\mathbf{A}_{\ell})_{i,j}>0$, then
$(\mathbf{x})_{j}$ can only take finitely many values; similarly, for all
${c\in\mathsf{Col}}$ and ${\mathbf{y}\in\mathbf{Y}^{c}}$, if
${(\mathbf{B}_{\ell}^{c})_{i,j}>0}$, then, $(\mathbf{y})_{j}$ can only take
finitely many values. Notice also that each $\mathbf{Y}^{c}$ cannot have
infinitely many elements, since it does not contain any vector where all
elements are $0$, and, for each ${1\leq j\leq\delta_{\ell-1}}$, there exist
fewer than $n_{j,c}$ elements in $\mathbf{Y}^{c}$ whose $j$-th component’s
value is positive, and none for which it is negative. Hence, there are only
finitely many values that $\sigma(z)$ can take. Thus, $\mathcal{S}_{\ell,i}$
is finite, which contradicts our initial assumption.

Finally, we show condition (S4). To this end, we first show that all elements
of $\mathcal{S}_{\ell,i}$ are in $\mathcal{X}_{\ell,i}$. Consider an arbitrary
element $\alpha\in\mathcal{S}_{\ell,i}$; by definition, there exists an
$(\ell,i)$-triple of the form $\langle\mathbf{x},\mathbf{Y},z\rangle$ such
that $\sigma(z)=\alpha$. Now, for all ${1\leq j\leq\delta_{\ell-1}}$,
${c\in\mathsf{Col}}$, and ${\mathbf{y}\in\mathbf{Y}^{c}}$, the definition of
an $(\ell,i)$-triple ensures ${(\mathbf{x})_{j}\in\mathcal{S}_{\ell-1,j}}$ and
${(\mathbf{y})_{j}\in\mathcal{S}_{\ell-1,j}}$; thus, our inductive hypothesis
implies ${(\mathbf{x})_{j}\in\mathcal{X}_{\ell-1,j}}$ and
${(\mathbf{y})_{j}\in\mathcal{X}_{\ell-1,j}}$. But then, the definition of an
$(\ell,i)$-triple ensures ${z=\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})}$,
and the definition of $\mathcal{X}_{\ell,i}$ ensures
${\sigma(z)\in\mathcal{X}_{\ell,i}}$, as required.

To prove that each element of $\mathcal{X}_{\ell,i}$ appears in
$\mathcal{S}_{\ell,i}$, consider arbitrary ${\alpha\in\mathcal{X}_{\ell,i}}$.
By Definition 7, there exists a vector $\mathbf{x}_{\alpha}$ of dimension
$\delta_{\ell-1}$ where $(\mathbf{x}_{\alpha})_{j}\in\mathcal{X}_{\ell-1,j}$
for each ${1\leq j\leq\delta_{\ell-1}}$, and there also exists a
$(\mathsf{Col},\ell-1)$-multiset family $\mathbf{Y}_{\alpha}$ such that
${(\mathbf{y})_{j}\in\mathcal{X}_{\ell-1,j}}$ holds for each
$c\in\mathsf{Col}$, each ${\mathbf{y}\in\mathbf{Y}^{c}_{\alpha}}$, and each
${1\leq j\leq\delta_{\ell-1}}$; moreover, ${\sigma(z_{\alpha})=\alpha}$ for
${z_{\alpha}=\mathsf{Val}(\ell,i,\mathbf{x}_{\alpha},\mathbf{Y}_{\alpha})}$.
By induction hypothesis, all elements in $\mathcal{X}_{\ell-1,j}$ are in
$\mathcal{S}_{\ell-1,j}$. Hence, there exists at least one finite sequence
${\langle\mathbf{s}_{\ell-1},\mathbf{Y}_{\emptyset},\mathsf{Val}(\ell,i,\mathbf{s}_{\ell-1},\mathbf{Y}_{\emptyset})\rangle=t_{0},\dots,t_{K}=\langle\mathbf{x}_{\alpha},\mathbf{Y}_{\alpha},z_{\alpha}\rangle}$
such that $t_{n}$ is a successor of $t_{n-1}$ for each ${1\leq n\leq K}$.
Indeed, each multiset $\mathbf{Y}^{c}_{\alpha}$ is finite and, starting from
$t_{0}$, we can reach $t_{K}$ by, in each step, changing some vector component
to the next element in $\mathcal{S}_{\ell-1,j}$ or adding a new vector to some
multiset of the $(\mathsf{Col},\ell-1)$-multiset family. We now show by
induction over ${0\leq n\leq K}$ the following statement ($\ast$): for each
${t_{n}=\langle\mathbf{x}_{n},\mathbf{Y}_{n},z_{n}\rangle}$ in this sequence,
some element of $\mathcal{F}_{\ell,i}$ contains a $(\ell,i)$-triple
$\langle\mathbf{x},\mathbf{Y},z\rangle$, called a _witness_ of $t_{n}$, such
that

  * •

if ${(\mathbf{A}_{\ell})_{i,j}>0}$, then
${(\mathbf{x}_{n})_{j}=(\mathbf{x})_{j}}$,

  * •

for each colour ${c\in\mathsf{Col}}$ and each index ${1\leq
j\leq\delta_{\ell-1}}$, if ${(\mathbf{B}_{\ell}^{c})_{i,j}>0}$, then multisets
${\\{\\!\\!\\{\,(\mathbf{y})_{j}\mid\mathbf{y}\in\mathbf{Y}^{c}_{n}\mbox{ and
}(\mathbf{y})_{j}>0\,\\}\\!\\!\\}}$ and
${\\{\\!\\!\\{\,(\mathbf{y})_{j}\mid\mathbf{y}\in\mathbf{Y}^{c}\mbox{ and
}(\mathbf{y})_{j}>0\,\\}\\!\\!\\}}$ are equal.

Observe that these properties imply ${z=z_{n}}$. For the base case,
${\langle\mathbf{s}_{\ell-1},\mathbf{Y}_{\emptyset},\mathsf{Val}(\ell,i,\mathbf{s}_{\ell-1},\mathbf{Y}_{\emptyset})\rangle\in
f_{0}}$ holds by definition, so $t_{0}$ is its own witness in
$\mathcal{F}_{\ell,i}$. For the induction step, we assume that
${t_{n-1}=\langle\mathbf{x}_{n-1},\mathbf{Y}_{n-1},z_{n-1}\rangle}$ with
${0<n\leq K}$ has a witness in $\mathcal{F}_{\ell,i}$, and we show that let
${t_{n}=\langle\mathbf{x}_{n},\mathbf{Y}_{n},z_{n}\rangle}$ then has a witness
in $\mathcal{F}_{\ell,i}$ as well. Let
${t=\langle\mathbf{x},\mathbf{Y},z\rangle}$ be a witness of $t_{n-1}$ in
$\mathcal{F}_{\ell,i}$. We first show that there exists ${m\in\mathbb{N}_{0}}$
such that $f_{m}$ is defined, $f_{m-1}$ contains $t$, but $f_{m}$ does not
contain $t$. If $\mathcal{F}_{\ell,i}$ is finite, the last element of
$\mathcal{F}_{\ell,i}$ is empty so the claim clearly holds. Thus, assume that
$\mathcal{F}_{\ell,i}$ is infinite. For the sake of a contradiction, assume
that there exists some ${m^{\prime}\in\mathbb{N}_{0}}$ such that $t$ appears
in all elements of $\mathcal{F}_{\ell,i}$ after $f_{m^{\prime}}$. By the
definition of $\mathcal{S}_{\ell,i}$, this implies that the elements of
$\mathcal{S}_{\ell,i}$ after $s_{m^{\prime}}$ form an infinite sequence that
is strictly monotonic and whose values are always smaller than $\sigma(z)$;
however, this contradicts condition (S3). Thus, there exists
${m\in\mathbb{N}_{0}}$ such that $f_{m-1}$ contains $t$, but $f_{m}$ does not.
The definition of $\mathcal{S}_{\ell,i}$ ensures that the $m-1$-th element of
$\mathcal{S}_{\ell,i}$ is precisely $\sigma(z_{n-1})$. If $z_{n}=z_{n-1}$,
then the change from $t_{n-1}$ to $t_{n}$ can only take place in either the
$j$-th component of $\mathbf{x}_{n-1}$ for $j$ such that
${(\mathbf{A}_{\ell})_{i,j}=0}$, or in the $j$-th component of some
${\mathbf{y}\in\mathbf{Y}^{c}_{n-1}}$ for some $c\in\mathsf{Col}$ with
${(\mathbf{B}_{\ell}^{c})_{i,j}=0}$, so the statement holds since
$\langle\mathbf{x},\mathbf{Y},z\rangle$ is a witness for $t_{n}$. If
${z_{n}>z_{n-1}}$, then the change from $t_{n-1}$ to $t_{n}$ can only take
place in either the $j$-th component of $\mathbf{x}_{n-1}$ for $j$ such that
${(\mathbf{A}_{\ell})_{i,j}>0}$, or in the $j$-th component of some
${\mathbf{y}\in\mathbf{Y}^{c}_{n-1}}$ for some ${c\in\mathsf{Col}}$ with
${(\mathbf{B}_{\ell}^{c})_{i,j}>0}$, or by adding a new vector to some
$\mathbf{Y}^{c}_{n-1}$ with the smallest positive value from
$\mathcal{S}_{\ell-1,j}$ in the $j$-th component, for some $j$ such that
${(\mathbf{B}_{\ell}^{c})_{i,j}>0}$. By the definition of a witness, both
$t_{n-1}$ and $t$ agree on the components of vectors where the change from
$t_{n-1}$ to $t_{n}$ takes place, and so the same change can be applied to the
witness $\langle\mathbf{x},\mathbf{Y},z\rangle$, leading to a triple
${t^{\prime}=\langle\mathbf{x}^{\prime},\mathbf{Y}^{\prime},z^{\prime}\rangle}$
such that $z^{\prime}=z_{n}$ and by definition of $\mathcal{F}_{\ell,i}$,
$t^{\prime}$ must appear in $f_{m+1}$. Thus, $t^{\prime}$ is clearly a witness
of $t_{n}$ in $\mathcal{F}_{\ell,i}$. This concludes the proof of ($\ast$).

Now, ($\ast$) ensures that
$\langle\mathbf{x}_{\alpha},\mathbf{Y}_{\alpha},z_{\alpha}\rangle$ has a
witness in $\mathcal{F}_{\ell,i}$, and as we have already shown, there exists
some element $f_{m}$ of $\mathcal{F}_{\ell,i}$ such that this triple appears
in $f_{m}$ but not in $f_{m+1}$. But then, the definition of
$\mathcal{S}_{\ell,i}$ ensures that $\sigma(z_{\alpha})$ is the $m$-th element
of $\mathcal{S}_{\ell,i}$; since ${\sigma(z_{\alpha})=\alpha}$, numner
$\alpha$ appears in $\mathcal{S}_{\ell,i}$, as desired. ∎

See 8

###### Proof.

By condition (S4) of Lemma A.1, for each ${1\leq\ell\leq L}$ and each ${1\leq
i\leq\delta_{\ell}}$, the elements of $\mathcal{X}_{\ell,i}$ are precisely the
elements of the sequence $\mathcal{S}_{\ell,i}$. By condition (S1), all
elements in $\mathcal{S}_{\ell,i}$ are nonnegative, so
${\mathcal{X}_{\ell,i}\subseteq\mathbb{R}^{+}_{0}}$ holds. Moreover, assume
that set ${\mathcal{X}_{\ell,i}\setminus\mathcal{X}_{\ell,i}^{>\alpha}}$ is
infinite; then, by condition (S4) of Lemma A.1, set $\mathcal{S}_{\ell,i}$
contains infinitely many numbers that are smaller or equal than $\alpha$.
However, by condition (S2) ensures that $\mathcal{S}_{\ell,i}$ is strictly
monotonically increasing, and so $\alpha$ is an upper bound of the sequence.
This, in turn, contradicts condition (S3). Consequently, set
${\mathcal{X}_{\ell,i}\setminus\mathcal{X}_{\ell,i}^{>\alpha}}$ is finite. ∎

######  Lemma A.2.

For each $(\mathsf{Col},\delta)$-dataset $D$, each ${0\leq\ell\leq L}$, each
vector $\mathbf{v}_{\ell}$ labelling a vertex when $\mathcal{N}$ is applied to
$D$, and each ${1\leq i\leq\delta_{\ell}}$, it holds that
${(\mathbf{v}_{\ell})_{i}\in\mathcal{X}_{\ell,i}}$.

###### Proof.

The proof is by a straightforward induction on ${0\leq\ell\leq L}$. For the
base case, Definition 2 ensures
${(\mathbf{v}_{0})_{i}\in\\{0,1\\}=\mathcal{X}_{0,i}}$ for each $i$. For the
induction step, consider some $1\leq\ell\leq L$ and $1\leq i\leq\delta_{\ell}$
and notice that the value of $(\mathbf{v}_{\ell})_{i}$ is given by expression
(45). Consider the triple $\langle\mathbf{x},\mathbf{Y},z\rangle$ where
${\mathbf{x}=\mathbf{v}_{\ell-1}}$, $\mathbf{Y}$ is the multiset family such
that, for each $c\in\mathsf{Col}$, $\mathbf{Y}^{c}$ is the multiset
${\\{\\!\\!\\{\,\mathbf{u}_{\ell}\mid\langle
v,u\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\}}$, and
${z=\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})}$. By the inductive hypothesis,
${(\mathbf{x})_{j}\in\mathcal{X}_{\ell-1,j}}$, and
${(\mathbf{y})_{j}\in\mathcal{X}_{\ell-1,j}}$ for each ${c\in\mathsf{Col}}$
and each ${\mathbf{y}\in\mathbf{Y}^{c}}$. Finally, by comparing (45) with the
definition of $\mathsf{Val}(\ell,i,\mathbf{x},\mathbf{Y})$ in Definition 7, we
can see that ${z=(\mathbf{v}_{\ell})_{i}}$. By the definition of
$\mathcal{X}_{\ell,i}$, then ${z\in\mathcal{X}_{\ell,i}}$, and thus
${(\mathbf{v}_{\ell})_{i}\in\mathcal{X}_{\ell,i}}$, as desired. ∎

See 10

###### Proof.

Consider an arbitrary $(\mathsf{Col},\delta)$-dataset $D$ and let
${\mathcal{G}=\langle\mathcal{V},\\{\mathcal{E}^{c}\\}_{c\in\mathsf{Col}},\lambda\rangle}$
be the canonical encoding of $D$. Let ${\lambda_{0},\dots,\lambda_{L}}$ and
${\lambda_{0}^{\prime},\dots,\lambda_{L}^{\prime}}$ be the functions labelling
the vertices of $\mathcal{G}$ induced by applying $\mathcal{N}$ and
$\mathcal{N}^{\prime}$ to $D$, respectively.

We first prove by induction on $0\leq\ell\leq L$ that for all
${v\in\mathcal{V}}$ and ${1\leq i\leq\delta_{\ell}}$, it holds that
${(\mathbf{v}_{\lambda_{\ell}})_{i}\geq(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$.
The base case holds trivially since ${\lambda_{0}=\lambda_{0}^{\prime}}$. For
the induction step, consider ${1\leq\ell\leq L}$, ${v\in\mathcal{V}}$, and
${1\leq i\leq\delta_{\ell}}$, and suppose that both claims hold for $\ell-1$.
The formulas for $(\mathbf{v}_{\lambda_{\ell}})_{i}$ and
$(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}$ are given by equations (45) and
(46).

$\displaystyle(\mathbf{v}_{\lambda_{\ell}})_{i}=$
$\displaystyle\;\sigma\left(\sum_{j=1}^{\delta_{\ell-1}}(\mathbf{A}_{\ell})_{i,j}(\mathbf{v}_{\lambda_{\ell-1}})_{j}+\sum_{c\in\mathsf{Col}}\sum_{j=1}^{\delta_{\ell-1}}(\mathbf{B}_{c}^{\ell})_{i,j}\>\mathrm{max}\text{-}{k_{\ell}}\text{-}\mathrm{sum}(\\{\\!\\!\\{\,(\mathbf{u}_{\lambda_{\ell}})_{j}\mid\langle
v,u\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\})+(\mathbf{b}_{\ell})_{i}\right)$
(45) $\displaystyle(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}=$
$\displaystyle\;\sigma\left(\sum_{j=1}^{\delta_{\ell-1}}(\mathbf{A}_{\ell})_{i,j}(\mathbf{v}_{\lambda_{\ell-1}^{\prime}})_{j}+\sum_{c\in\mathsf{Col}}\sum_{j=1}^{\delta_{\ell-1}}(\mathbf{B}_{c}^{\ell})_{i,j}\>\mathrm{max}\text{-}{C_{\ell}}\text{-}\mathrm{sum}(\\{\\!\\!\\{\,(\mathbf{u}_{\lambda_{\ell}^{\prime}})_{j}\mid\langle
v,u\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\})+(\mathbf{b}_{\ell})_{i}\right)$
(46)

In both equations, all summands except $(\mathbf{b}_{\ell})_{i}$ are
nonnegative: the weights of $\mathcal{N}$ and $\mathcal{N}^{\prime}$ are
nonnegative by Definition 6, and the feature vectors labelling vertices of
$\mathcal{V}$ are also nonnegative by Theorem 8 and Lemma A.2. Note that the
inductive hypothesis ensures
${(\mathbf{u}_{\lambda_{\ell-1}})_{j}\geq(\mathbf{u}_{\lambda_{\ell-1}^{\prime}})_{j}}$
for all ${u\in\mathcal{V}}$ and ${1\leq j\leq\delta_{\ell-1}}$. Furthermore,
Algorithm 1 ensures that $C_{\ell}\leq k_{\ell}$. Since the weights of
$\mathbf{A}_{\ell}$ and each $\mathbf{B}_{\ell}^{c}$ are nonnegative,
subtracting (46) from (45) yields a positive value, and so
$(\mathbf{v}_{\lambda_{\ell}})_{i}\geq(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}$.
This concludes the proof by induction.

Now let $\ell_{\mathsf{st}}$ be the largest ${1\leq\ell\leq L}$ such that
either all elements of $\mathbf{A}_{\ell}$ and $\mathbf{B}_{\ell}^{c}$ for
each $c\in\mathsf{Col}$ are $0$, or ${\mathcal{X}_{\ell-1,j}=\\{0\\}}$ for
each ${1\leq j\leq\delta_{\ell-1}}$; if such $\ell$ does not exist, let
${\ell_{\mathsf{st}}=0}$. To complete the proof of the theorem, we prove by
induction on ${\ell_{\mathsf{st}}\leq\ell\leq L}$ that, for all
${v\in\mathcal{V}}$ and ${1\leq i\leq\delta_{\ell}}$, exactly one of the
following two properties holds:

  * •

${(\mathbf{v}_{\lambda_{\ell}})_{i}=(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$
or

  * •

${(\mathbf{v}_{\lambda_{\ell}})_{i}>(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}\geq\alpha_{\ell}}$.

For the base case, if ${\ell_{\mathsf{st}}=0}$, then the first property holds
trivially since ${\lambda_{0}=\lambda_{0}^{\prime}}$. If
${\ell_{\mathsf{st}}>0}$, consider an arbitrary ${1\leq i\leq\delta_{\ell}}$.
We have two possibilities. First, if all elements of
$\mathbf{A}_{\ell_{\mathsf{st}}}$ and $\mathbf{B}_{\ell_{\mathsf{st}}}^{c}$
for each $c\in\mathsf{Col}$ are all zero, equations (45) and (46) and the fact
that the matrices of $\mathcal{N}$ and $\mathcal{N}^{\prime}$ are the same
ensure that
${(\mathbf{v}_{\lambda_{\ell_{\mathsf{st}}}})_{i}=(\mathbf{v}_{\lambda_{\ell_{\mathsf{st}}}^{\prime}})_{i}=\sigma((\mathbf{b}_{\ell_{\mathsf{st}}})_{i})}$.
Second, if $\mathcal{X}_{\ell-1,j}=\\{0\\}$ for each ${1\leq
j\leq\delta_{\ell-1}}$; equation (45) ensure
${(\mathbf{v}_{\lambda_{\ell_{\mathsf{st}}}})_{i}=\sigma((\mathbf{b}_{\ell_{\mathsf{st}}})_{i})}$;
moreover, we have shown that
${(\mathbf{v}_{\lambda_{\ell_{\mathsf{st}}}})_{i}\geq(\mathbf{v}_{\lambda_{\ell_{\mathsf{st}}^{\prime}}})_{i}}$,
and since the elements in the sum in (46) other than $(\mathbf{b}_{\ell})_{i}$
are not negative, we again have
${(\mathbf{v}_{\lambda_{\ell_{\mathsf{st}}}^{\prime}})_{i}=\sigma((\mathbf{b}_{\ell_{\mathsf{st}}})_{i})}$.
Hence,
${(\mathbf{v}_{\lambda_{\ell}})_{i}=(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$
and the first property holds.

For the induction step, we consider arbitrary layer
${\ell_{\mathsf{st}}<\ell\leq L}$, vertex ${v\in\mathcal{V}}$, and position
${1\leq i\leq\delta_{\ell}}$. We assume that
${(\mathbf{v}_{\lambda_{\ell}})_{i}\neq(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$;
together with
${(\mathbf{v}_{\lambda_{\ell}})_{i}\geq(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$,
this implies
${(\mathbf{v}_{\lambda_{\ell}})_{i}>(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$,
so we next show
${(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}\geq\alpha_{\ell}}$. Since
${\ell>\ell_{\mathsf{st}}}$, Algorithm 1 defines $\epsilon_{\ell}$,
$\beta_{\ell}$, $w_{\ell}$, $b_{\ell}$, $C_{\ell}$, $\alpha_{\ell}$, and
$\alpha_{\ell-1}$. Furthermore, let
${k_{\ell}^{\prime}=\lceil\frac{\beta_{\ell}-b_{\ell}}{w_{\ell}\cdot\epsilon_{\ell}}\rceil}$,
so ${C_{\ell}=\min(k_{\ell},k_{\ell}^{\prime})}$. We have already shown that
${(\mathbf{u}_{\lambda_{\ell-1}})_{j}\geq(\mathbf{u}_{\lambda_{\ell-1}^{\prime}})_{j}}$
for all ${u\in\mathcal{V}}$ and ${1\leq j\leq\delta_{\ell-1}}$. We next
consider the following four possibilities.

Case 1. There exists ${1\leq j\leq\delta_{\ell-1}}$ such that
${(\mathbf{A}_{\ell})_{i,j}>0}$ and
$(\mathbf{v}_{\lambda_{\ell-1}^{\prime}})_{j}\geq\alpha_{\ell-1}$. Since all
summands in (46) except $(\mathbf{b}_{\ell})_{i}$ are nonnegative, the
argument of $\sigma$ in (46) is greater or equal to
$(\mathbf{A}_{\ell})_{i,j}(\mathbf{v}_{\lambda_{\ell-1}^{\prime}})_{j}+(\mathbf{b}_{\ell})_{i}\geq
w_{\ell}\alpha_{\ell-1}+b_{\ell}=\beta_{\ell}$; since
$\sigma(\beta_{\ell})\geq\alpha_{\ell}$ and $\sigma$ is monotonically
increasing, we have
$(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}\geq\alpha_{\ell}$, as desired.

Case 2. Case 1 does not hold and ${C_{\ell}=0}$. If ${C_{\ell}=k_{\ell}=0}$,
the sum over ${c\in\mathsf{Col}}$ in both (45) and (46) is always equal to
$0$. Furthermore, since case 1 does not hold, the induction hypothesis ensures
that for any $1\leq j\leq\delta_{\ell-1}$ such that $A^{\ell}_{i,j}>0$, we
have
${(\mathbf{v}_{\lambda_{\ell-1}^{\prime}})_{j}=(\mathbf{v}_{\lambda_{\ell-1}})_{j}}$.
Thus, it follows that
$(\mathbf{v}_{\lambda_{\ell}})_{i}=(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}$.
If $C_{\ell}=k_{\ell}^{\prime}=0$, Algorithm 1 ensures that
$\beta_{\ell}=b_{\ell}$. Then, since all summands in the argument of $\sigma$
other than $(\mathbf{b}_{\ell})_{i}$ are nonnegative, we have that the
argument of $\sigma$ in (46) is greater or equal than
$(\mathbf{b}_{\ell})_{i}\geq b_{\ell}=\beta_{\ell}$, and since $\sigma$ is
monotonically increasing and $\sigma(\beta_{\ell})\geq\alpha_{\ell}$, we have
that $(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}\geq\alpha_{\ell}$, as
desired.

Case 3. $C_{\ell}>0$ and there exist ${c\in\mathsf{Col}}$, ${1\leq
j\leq\delta_{\ell-1}}$, and $\langle v,u\rangle\in\mathcal{E}^{c}$ such that
$(\mathbf{B}_{c}^{\ell})_{i,j}>0$ and
$(\mathbf{u}_{\lambda_{\ell-1}^{\prime}})_{j}\geq\alpha_{\ell-1}$. All
summands in the argument of $\sigma$ in (46) except $(\mathbf{b}_{\ell})_{i}$
are nonnegative and
${\mathrm{max}\text{-}{C_{\ell}}\text{-}\mathrm{sum}(\\{\\!\\!\\{\,(\mathbf{u}_{\lambda_{\ell-1}^{\prime}})_{j}\mid\langle
v,w\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\})\geq(\mathbf{u}_{\lambda_{\ell-1}^{\prime}})_{j}}$
due to ${C_{\ell}>0}$, so the argument of $\sigma$ in (46) is greater or equal
to
${(\mathbf{B}_{c}^{\ell})_{i,j}(\mathbf{u}_{\lambda_{\ell-1}^{\prime}})_{j}+(\mathbf{b}_{\ell})_{i}\geq
w_{\ell}\alpha_{\ell-1}+(\mathbf{b}_{\ell})_{i}=\beta_{\ell}}$. Since
${\sigma(\beta_{\ell})\geq\alpha_{\ell}}$ and $\sigma$ is monotonically
increasing, we have
${(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}\geq\alpha_{\ell}}$.

Case 4. None of cases 1–3 hold. Since case 1 does not hold, the induction
hypothesis ensures that for any $1\leq j\leq\delta_{\ell-1}$ such that
$A^{\ell}_{i,j}>0$, we have
$(\mathbf{v}_{\lambda_{\ell-1}^{\prime}})_{j}=(\mathbf{v}_{\lambda_{\ell-1}})_{j}$.
Furthermore, since case 2 does not hold, we have ${C_{\ell}>0}$. Finally, case
3 does not hold, so, for each ${c\in\mathsf{Col}}$ and ${1\leq
j\leq\delta_{\ell-1}}$ such that ${(\mathbf{B}_{\ell}^{c})_{i,j}>0}$, we have
$(\mathbf{u}_{\lambda_{\ell-1}^{\prime}})_{j}=(\mathbf{u}_{\lambda_{\ell-1}})_{j}$
for each $u$ such that ${\langle v,u\rangle\in\mathcal{E}^{c}}$, and so
${\\{\\!\\!\\{\,(\mathbf{u}_{\lambda_{\ell}})_{j}\mid\langle
v,u\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\}=\\{\\!\\!\\{\,(\mathbf{u}_{\lambda_{\ell}^{\prime}})_{j}\mid\langle
v,u\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\}}$ holds. By these observations, our
assumption that
${(\mathbf{v}_{\lambda_{\ell}})_{i}\neq(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$,
and equations (45) and (46), then ${C_{\ell}=k_{\ell}^{\prime}<k_{\ell}}$ and
there must exist at least one ${1\leq j\leq\delta_{\ell-1}}$ such that
${(\mathbf{B}_{\ell}^{c})_{i,j}>0}$ and the number of distinct $u$ such that
${\langle v,u\rangle\in\mathcal{E}^{c}}$ and
${(\mathbf{u}_{\lambda_{\ell-1}})_{j}>0}$ is greater than $C_{\ell}$. For such
$j$, and since all summands in the argument of $\sigma$ in (46) except
$(\mathbf{b}_{\ell})_{i}$ are nonnegative, it holds that the argument is
greater or equal than

$\displaystyle(\mathbf{B}_{\ell}^{c})_{i,j}\mathrm{max}\text{-}{C_{\ell}}\text{-}\mathrm{sum}(\\{\\!\\!\\{\,(\mathbf{u}_{\lambda_{\ell}^{\prime}})_{j}\mid\langle
v,u\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\})+(\mathbf{b}_{\ell})_{i}.$ (47)

However, as we have already observed, we know that there exist at least
$C_{\ell}$ elements different from zero in the multiset in (47), and Lemma A.2
and the definitions of $\epsilon_{\ell}$ amd $\mathcal{X}_{\ell-1,j}$ ensure
that each of these elements is greater or equal than $\epsilon_{\ell}$. Thus,
the value in (47) is greater or equal than
$w_{\ell}C_{\ell}\epsilon_{\ell}+b_{\ell}\geq\beta_{\ell}$. However,
${\sigma(\beta_{\ell})\geq\alpha_{\ell}}$ since $\sigma$ is monotonic, we have
${(\mathbf{v}_{\lambda_{\ell}})_{i}\geq\alpha_{\ell}}$, which concludes the
proof.

To complete the proof of the theorem, we consider an arbitrary term $t$ in $D$
and an arbitrary unary predicate $U_{i}$ in the
$(\mathsf{Col},\delta)$-signature, where $1\leq i\leq\delta$, and we show that
$U_{i}(t)\in T_{\mathcal{N}}(D)$ if and only if $U_{i}(t)\in
T_{\mathcal{N}^{\prime}}(D)$; this implies the theorem since
$T_{\mathcal{N}}(D)$ and $T_{\mathcal{N}^{\prime}}(D)$ can only contain atoms
of this form. By definition of the canonical encoder/decoder scheme and the
definitions of both $\mathcal{N}$ and $\mathcal{N}^{\prime}$, it suffices to
show that

$\mathsf{cls}((\mathbf{v}_{\lambda_{L}})_{i})=1\mbox{ if and only if
}\mathsf{cls}((\mathbf{v}_{\lambda_{L}^{\prime}})_{i})=1,$ (48)

for $v$ the vertex of the form $v_{t}$ in $\mathcal{V}$. By the first result
shown above by induction, we have that
$(\mathbf{v}_{\lambda_{L}})_{i}\geq(\mathbf{v}_{\lambda_{L}^{\prime}})_{i}$,
and the second result ensures that either
$(\mathbf{v}_{\lambda_{L}})_{i}=(\mathbf{v}_{\lambda_{L}^{\prime}})_{i}$ or
$(\mathbf{v}_{\lambda_{L}^{\prime}})_{i}\geq\alpha_{L}$, since
$L\geq\ell_{\mathsf{st}}$. If
$(\mathbf{v}_{\lambda_{L}})_{i}=(\mathbf{v}_{\lambda_{L}^{\prime}})_{i}$, (48)
holds trivially. If $(\mathbf{v}_{\lambda_{L}^{\prime}})_{i}\geq\alpha_{L}$,
then the definition of $\alpha_{L}$ in Algorithm 1 ensures that
$\mathsf{cls}((\mathbf{v}_{\lambda_{L}^{\prime}})_{i})=1$, and since
$(\mathbf{v}_{\lambda_{L}})_{i}\geq(\mathbf{v}_{\lambda_{L}^{\prime}})_{i}$,
then $\mathsf{cls}((\mathbf{v}_{\lambda_{L}})_{i})=1$, so (48) holds. ∎

For a dataset $D$, let $\mathsf{tms}(D)$ be the set containing each term $t$
such that $D$ contains an atom of the form $U(t)$, $E^{c}(t,s)$, or
$E^{c}(s,t)$, for $U$ and $E^{c}$ arbitrary unary and binary predicates,
respectively, and $s$ an arbitrary term. An _isomorphism_ from a
$(\mathsf{Col},\delta)$-dataset $D$ to a $(\mathsf{Col},\delta)$-dataset
$D^{\prime}$ is an injective mapping $h$ of terms to terms that is defined (at
least) on all $\mathsf{tms}(D)$ and satisfies ${h(D)=D^{\prime}}$, where
$h(D)$ is the dataset obtained by replacing each fact of the form $U(t)$ in
$D$ with $U(h(t))$, and each fact of the form $E^{c}(t,s)\in D$ with
$E^{c}(h(t),h(s))$.

######  Lemma A.3.

For all $(\mathsf{Col},\delta)$ datasets $D$ and $D^{\prime}$, the following
properties holds:

  1. (M1)

each isomorphism from $D$ to $D^{\prime}$ is also an isomorphism from
$T_{\mathcal{N}}(D)$ to $T_{\mathcal{N}}(D^{\prime})$; and

  2. (M2)

${D\subseteq D^{\prime}}$ implies ${T_{\mathcal{N}}(D)\subseteq
T_{\mathcal{N}}(D^{\prime})}$.

###### Proof.

It is straightforward to see that property (M1) holds: for any two
$(\mathsf{Col},\delta)$-datasets, an isomorphism $h$ from $D$ to $D^{\prime}$
induces a bijective mapping between the vertices of $\mathsf{enc}{D}$ and
$\mathsf{enc}{D^{\prime}}$; moreover, the result of applying $\mathcal{N}$ to
a $(\mathsf{Col},\delta)$-graph depends only on the graph structure and not on
the vertex names, so it is straightforward to show that the vectors labelling
the corresponding vertices are identical.

To see that property (M2) holds, consider arbitrary datasets $D$ and
$D^{\prime}$ such that ${D\subseteq D^{\prime}}$. Let
${\mathcal{G}=\langle\mathcal{V},\\{\mathcal{E}^{c}\\}_{c\in\mathsf{Col}},\lambda\rangle}$
and ${\mathcal{G}^{\prime}=\langle\mathcal{V}^{\prime},\\{\mathcal{E}^{\prime
c}\\}_{c\in\mathsf{Col}},\lambda^{\prime}\rangle}$ be the canonical encodings
of $D$ and $D^{\prime}$, respectively, and ${\lambda_{0},\dots,\lambda_{L}}$
and ${\lambda_{0}^{\prime},\dots,\lambda_{L}^{\prime}}$ be the functions
labelling the vertices of $\mathcal{G}$ and $\mathcal{G}^{\prime}$ when
$\mathcal{N}$ is applied to these graphs. By a straightforward induction on
${0\leq\ell\leq L}$ we show that
${(\mathbf{v}_{\lambda_{\ell}})_{i}\leq(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$
holds for each vertex ${v\in\mathcal{V}}$ and each ${1\leq
i\leq\delta_{\ell}}$. The base case for ${\ell=0}$ follows immediately from
the canonical encoding and the fact that ${D\subseteq D^{\prime}}$. For the
induction step, the canonical encoding and ${D\subseteq D^{\prime}}$ imply
${\mathcal{E}^{c}\subseteq\mathcal{E}^{\prime c}}$. The values of
$(\mathbf{v}_{\lambda_{\ell}})_{i}$ and
$(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}$ are computed by equation (7). Now
by the inductive hypothesis,
${(\mathbf{u}_{\lambda_{\ell-1}})_{j}\leq(\mathbf{u}_{\lambda_{\ell}^{\prime}})_{j}}$
holds for each ${u\in\mathcal{V}}$ and ${1\leq j\leq\delta_{\ell-1}}$, which
ensures

$\mathrm{max}\text{-}{k_{\ell}}\text{-}\mathrm{sum}(\\{\\!\\!\\{\,(\mathbf{u}_{\lambda_{\ell-1}})_{j}\mid\langle
v,u\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\})\leq\mathrm{max}\text{-}{k_{\ell}}\text{-}\mathrm{sum}(\\{\\!\\!\\{\,(\mathbf{u}_{\lambda_{\ell-1}^{\prime}})_{j}\mid\langle
v,u\rangle\in\mathcal{E}^{\prime c}\,\\}\\!\\!\\}).$

All elements of $\mathbf{A}_{\ell}$ and all $\mathbf{B}_{\ell}^{c}$ with
${c\in\mathsf{Col}}$ are nonnegative, and $\sigma$ is monotonically
increasing, which implies
${(\mathbf{v}_{\lambda_{\ell}})_{i}\leq(\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i}}$.
Finally, $\mathsf{cls}$ is a step function, so
${\mathsf{cls}((\mathbf{v}_{\lambda_{\ell}})_{i})\leq\mathsf{cls}((\mathbf{v}_{\lambda_{\ell}^{\prime}})_{i})}$
holds as well, which ensures ${T_{\mathcal{N}}(D)\subseteq
T_{\mathcal{N}}(D^{\prime})}$. ∎

See 12

###### Proof.

If there exists a substitution ${\nu:V\to S}$ such that ${H\nu\in
T_{r}(A\nu)}$ but ${H\nu\notin T_{\mathcal{N}}(A\nu)}$, then by definition
$T_{\mathcal{N}}$ does not capture $r$. To conclude the proof of the lemma, it
only remains to show the converse implication: if ${H\nu\in
T_{\mathcal{N}}(A\nu)}$ for each substitution ${\nu:v\to S}$ such that
${H\nu\in T_{r}(A\nu)}$, then $T$ captures $r$. To this end, we consider an
arbitrary $(\mathsf{Col},\delta)$-dataset $D$, and we prove that
${T_{r}(D)\subseteq T_{\mathcal{N}}(D)}$. If $T_{r}(D)$ is empty, then the
claim holds vacuously, so suppose $T_{r}(D)\neq\emptyset$. Consider an
arbitrary element $\alpha$ in $T_{r}(D)$; clearly, $\alpha$ is of the form
$H\mu$ for some substitution $\mu$ such that ${A\mu\subseteq D}$ and ${H\mu\in
T_{r}(A\mu)}$. Let $h$ be an injective mapping from $\mathsf{tms}(A\mu)$ to
the constants in $S$; such a mapping exists because the body of $r$ contains
at most $|V|$ variables, and so $\mathsf{tms}(A\mu)$ contains at most $|V|$
terms. Then, ${\nu=h\circ\mu}$ is a substitution mapping all variables in $r$
to constants in $|V|$. Mapping $h$ is injective, rule $r$ is constant-free,
and ${H\mu\in T_{r}(A\mu)}$, so the semantics of Datalog rule application
ensure that ${h(H\mu)\in T_{r}(h(A\mu))}$, and so ${H\nu\in T_{r}(A\nu)}$. The
latter implies ${H\nu\in T_{\mathcal{N}}(A\nu)}$ by the lemma assumption.
Moreover, $h$ is an isomorphism from $A\mu$ to $A\nu$, so property (M1) of
Lemma A.3 implies ${H\mu\in T_{\mathcal{N}}(A\mu)}$. Finally, property (M2) of
Lemma A.3 and ${A\mu\subseteq D}$ imply ${\alpha=H\mu\in T_{\mathcal{N}}(D)}$,
as required. ∎

See 13

###### Proof.

We prove the theorem by showing that
${T_{\mathcal{N}}(D)=T_{\mathcal{P}_{\mathcal{N}}}(D)}$ holds for each
$(\mathsf{Col},\delta)$-dataset $D$. GNN $\mathcal{N}$ captures every rule in
$\mathcal{P}_{\mathcal{N}}$ and thus ${T_{r}(D)\subseteq T_{\mathcal{N}}(D)}$
for each ${r\in\mathcal{P}_{\mathcal{N}}}$; since
${T_{\mathcal{P}_{\mathcal{N}}}(D)=\bigcup_{r\in\mathcal{P}_{\mathcal{N}}}T_{r}(D)}$,
we have ${T_{\mathcal{P}_{\mathcal{N}}}(D)\subseteq T_{\mathcal{N}}(D)}$.

To prove ${T_{\mathcal{N}}(D)\subseteq T_{\mathcal{P}_{\mathcal{N}}}(D)}$, we
consider an arbitrary fact ${\alpha\in T_{\mathcal{N}}(D)}$, and we construct
a ${(L,|\mathsf{Col}|\cdot\delta_{\mathcal{N}}\cdot C_{\mathcal{N}})}$-tree-
like rule $r$ such that ${\alpha\in T_{r}(D)}$ and $r$ is captured by
$T_{\mathcal{N}}$, which together imply $\alpha\in
T_{\mathcal{P}_{\mathcal{N}}}(D)$. To find $r$, we consider the GNN
$\mathcal{N}^{\prime}$ obtained from $\mathcal{N}$ by replacing $k_{\ell}$
with $C_{\ell}$ for each ${1\leq\ell\leq L}$. Theorem 10 ensures
$T_{\mathcal{N}}(D)=T_{\mathcal{N}^{\prime}}(D)$, and so ${\alpha\in
T_{\mathcal{N}^{\prime}}(D)}$. Let
${\mathcal{G}=\langle\mathcal{V},\\{\mathcal{E}^{c}\\}_{c\in\mathsf{Col}},\lambda\rangle}$
be the canonical encoding of $D$, and let ${\lambda_{0},\dots,\lambda_{L}}$ be
the functions labelling the vertices of $\mathcal{G}$ when
$\mathcal{N}^{\prime}$ is applied to it. We next construct an atom $H$, a
conjunction $\Gamma$, a substitution $\nu$ from the variables in $\Gamma$ to
$\mathsf{tms}(D)$, a graph $U$ (without vertex labels) with fresh vertices not
occurring in $\mathcal{G}$ of the form $u_{x}$ for $x$ a variable and edges
with colours in $\mathsf{Col}$, and mappings ${M_{c,\ell,j}:U\to
2^{\mathcal{V}}}$ for each ${c\in\mathsf{Col}}$, ${1\leq\ell\leq L}$, and
${1\leq j\leq\delta_{\ell-1}}$. We also assign to each vertex in $U$ a level
between $0$ and $L$, and we identify a single vertex from $U$ as the _root_
vertex. In the rest of this proof, we use letters $t$ and $s$ for terms in
$\mathsf{tms}(D)$, letters $x$ and $y$ for variables, letters $v$, $w$ for the
vertices in $\mathcal{V}$, and (possibly indexed) letter $u$ for the vertices
in $U$. Our construction is by induction from level $L$ down to level $1$. The
base case defines a vertex of level $L$. Then, for each $1\leq\ell\leq L$, the
induction step considers the vertices of level $\ell$ and defines new vertices
of level $\ell-1$.

We initialise $\Gamma$ as the empty conjunction, and we initialise $\nu$ and
each $M_{c,\ell,j}$ as the empty mappings. For the base case, we note that
$\alpha$ must be of the form $U_{i}(t)$, and so $\mathcal{V}$ contains a
vertex $v_{t}$. We introduce a fresh variable $x$, and define ${\nu(x)=t}$; we
define ${H=U_{i}(x)}$; we introduce vertex $u_{x}$ of level $L$; and we make
$u_{x}$ the root vertex. Finally, we extend $\Gamma$ with atom $U(x)$ for each
${U(t)\in D}$. For the induction step, consider $1\leq\ell\leq L$ and assume
that all vertices of level greater than $\ell$ have been already defined. We
then consider each vertex of the form $u_{x}$ of level $\ell$. Let
${t=\nu(x)}$. For each colour $c\in\mathsf{Col}$, each layer
$1\leq\ell^{\prime}<\ell$, and each dimension
$j\in\\{1,\dots,\delta_{\ell^{\prime}-1}\\}$, let

$\displaystyle M_{c,\ell^{\prime},j}(u_{x})=\left\\{w\mid\langle
v_{t},w\rangle\in\mathcal{E}^{c}\text{ and
}(\mathbf{w}_{\lambda_{\ell^{\prime}}})_{j}\text{ contributes to the result of
}\mathrm{max}\text{-}{C_{\ell^{\prime}}}\text{-}\mathrm{sum}\big{(}\\{\\!\\!\\{\,(\mathbf{w}_{\lambda_{\ell^{\prime}}})_{j}\mid\langle
v_{t},w\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\}\big{)}\right\\}.$ (49)

At least one such set exists, but it may not be unique; however, any set
satisfying (49) can be chosen. Each vertex of $M_{c,\ell^{\prime},j}(u_{x})$
must be of the form $v_{s_{n}}$ for some term $s_{n}\in\mathsf{tms}(D)$, where
$s_{n}\neq s_{m}$ for all $1\leq n<m\leq|M_{c,\ell^{\prime},j}(u_{x})|$. We
then introduce a fresh variable $y_{n}$ and define ${\nu(y_{n})=s_{n}}$; we
introduce a vertex $u_{y_{n}}$ of level ${\ell-1}$ and an edge
$E^{c}(u_{x},u_{y_{n}})$ to $U$; and we append to $\Gamma$ the conjunction

$\bigwedge_{n=1}^{|W|}\Big{(}E^{c}(x,y_{n})\wedge
B_{D}(y_{n})\Big{)}\wedge\bigwedge_{1\leq n<m\leq|W|}y_{n}\not\approx y_{m},$
(50)

where ${W=M_{c,\ell^{\prime},j}(u_{x})}$ and $B_{D}(y_{n})$ is the conjunction
consisting of an atom $U(y_{n})$ for each ${U(s_{n})\in D}$. Since each
$M_{c,\ell,j}(u_{x})$ contains at most $C_{\ell^{\prime}}$ elements, this step
adds at most $|\mathsf{Col}|\cdot\delta_{\ell^{\prime}-1}\cdot
C_{\ell^{\prime}}\cdot\ell^{\prime}$ new successors of $u_{x}$. This completes
our inductive construction. At this point, $H=U_{i}(x)$ and $\Gamma$ is a
$(L,|\mathsf{Col}|\cdot\delta_{\mathcal{N}}\cdot C_{\mathcal{N}})$-tree-like
formula for $x$. Thus, rule ${H\leftarrow\Gamma}$ is a
$(L,|\mathsf{Col}|\cdot\delta_{\mathcal{N}}\cdot C_{\mathcal{N}})$-tree-like
rule. Furthermore, the construction of $\nu$ ensures $D\models\Gamma\nu$ so
$H\nu\in T_{r}(D)$, but $H\nu=\alpha$, so $\alpha\in T_{r}(D)$, as required.

To complete the proof, we next show that $r$ is captured by $T_{\mathcal{N}}$,
which is equivalent to showing that $r$ is captured by
$T_{\mathcal{N}^{\prime}}$. To do this, we consider an arbitrary dataset
$D^{\prime}$ and an arbitrary ground atom $\alpha^{\prime}$ such that
$\alpha^{\prime}\in T_{r}(D^{\prime})$. This implies that there exists some
substitution $\nu^{\prime}$ such that $D^{\prime}\models\Gamma\nu^{\prime}$
and and $\alpha^{\prime}=H\nu^{\prime}$. Consider the encoding of $D^{\prime}$
into a $(\mathsf{Col},\delta)$-graph
${\mathcal{G}=\langle\mathcal{V}^{\prime},\\{\mathcal{E}^{\prime
c}\\}_{c\in\mathsf{Col}},\lambda^{\prime}\rangle}$, and let
${\lambda_{0}^{\prime},\dots,\lambda_{L}^{\prime}}$ be the functions labelling
the vertices of $\mathcal{G}^{\prime}$ when $\mathcal{N}^{\prime}$ is applied
to it. We use letters $p$, $q$, and $q^{\prime}$ for the vertices of
$\mathcal{V}^{\prime}$.

We now prove the following statement by induction: for each ${0\leq\ell\leq
L}$ and each vertex $u_{x}$ of $U$ whose level is at least $\ell$, we have
$(\mathbf{v}_{\lambda_{\ell}})_{i}\leq(\mathbf{p}_{\lambda_{\ell}^{\prime}})_{i}$
for each $i\in\\{1,\dots,\delta_{\ell}\\}$, where $v=v_{\nu(x)}$ and
$p=v_{\nu^{\prime}(x)}$. For the base case, ${\ell=0}$, consider an arbitrary
$1\leq i\leq\delta_{0}$ and $u_{x}\in U$, and let $v=v_{\nu(x)}$ and
$p=v_{\nu^{\prime}(x)}$. Note that
$(\mathbf{v}_{\lambda_{0}})_{i}\in\\{0,1\\}$ and
$(\mathbf{p}_{\lambda_{0}^{\prime}})\in\\{0,1\\}$, so we only need to prove
that $(\mathbf{v}_{\lambda_{0}})_{i}=1$ implies
$(\mathbf{p}_{\lambda_{0}^{\prime}})_{i}=1$. By Definition 2,
$(\mathbf{v}_{\lambda_{0}})_{i}=1$ implies $U_{i}(x\nu)\in D$. The
construction of $\Gamma$ ensures that ${U_{i}(x)\in\Gamma}$, and
$D^{\prime}\models\Gamma\nu^{\prime}$ implies $U_{i}(x\nu^{\prime})\in
D^{\prime}$, and so $(\mathbf{p}_{\lambda_{0}})_{i}=1$, as required.

For the induction step, assume that the property holds for some ${\ell-1}$,
and consider an arbitrary vertex ${u_{x}\in U}$ whose level is at least
$\ell$; consider an arbitrary $c\in\mathsf{Col}$,
$i\in\\{1,\dots,\delta_{i}\\}$, and let $v=v_{\nu(x)}$ and
$p=v_{\nu^{\prime}(x)}$. Note that the following holds.

$\displaystyle(\mathbf{v}_{\lambda_{\ell}})_{i}=\,$
$\displaystyle\sigma\left(\sum_{j=1}^{\delta_{\ell-1}}(\mathbf{A}_{\ell})_{i,j}(\mathbf{v}_{\lambda_{\ell-1}})_{j}+\sum_{c\in\mathsf{Col}}\sum_{j=1}^{\delta_{\ell-1}}(\mathbf{B}_{\ell-1}^{c})_{i,j}\;\mathrm{max}\text{-}{C_{\ell}}\text{-}\mathrm{sum}\\{\\!\\!\\{\,(\mathbf{w}_{\lambda_{\ell-1}})_{j}\mid\langle
v,w\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\}+(\mathbf{b}_{\ell})_{i}\right)$
(51) $\displaystyle(\mathbf{p}_{\lambda_{\ell}^{\prime}})_{i}=\,$
$\displaystyle\sigma\left(\sum_{j=1}^{\delta_{\ell-1}}(\mathbf{A}_{\ell})_{i,j}(\mathbf{p}_{\lambda_{\ell-1}^{\prime}})_{j}+\sum_{c\in\mathsf{Col}}\sum_{j=1}^{\delta_{\ell-1}}(\mathbf{B}_{\ell-1}^{c})_{i,j}\;\mathrm{max}\text{-}{C_{\ell}}\text{-}\mathrm{sum}\\{\\!\\!\\{\,(\mathbf{q}_{\lambda_{\ell-1}^{\prime}})_{j}\mid\langle
p,q\rangle\in\mathcal{E}^{\prime
c}\,\\}\\!\\!\\}+(\mathbf{b}_{\ell})_{i}\right)$ (52)

The induction assumption ensures
${(\mathbf{v}_{\lambda_{\ell-1}})_{j}\leq(\mathbf{p}_{\lambda_{\ell-1}^{\prime}})_{j}}$
for each ${1\leq j\leq\delta_{\ell-1}}$. Also, for each colour
${c\in\mathsf{Col}}$ and each ${1\leq j\leq\delta_{\ell-1}}$, we have that
$\mathrm{max}\text{-}{C_{\ell}}\text{-}\mathrm{sum}\\{\\!\\!\\{\,(\mathbf{w}_{\lambda_{\ell-1}})_{j}\mid\langle
v,w\rangle\in\mathcal{E}^{c}\,\\}\\!\\!\\}$ is equal to ${\sum_{w\in
W}(\mathbf{w}_{\lambda_{\ell-1}})_{j}}$, where ${W=M_{c,\ell-1,j}(u_{x})}$.
Recall that the elements of $W$ are of the form
${v_{s_{1}},\cdots,v_{s_{|W|}}}$ where ${s_{1},\cdots,s_{|W|}}$ are terms in
$\mathsf{tms}(D)$. Furthermore, by the construction of $U$, there are $W$
distinct vertices ${u_{y_{1}},\cdots,u_{y_{|W|}}}$ in $U$ of level $\ell-1$
such that ${\nu(y_{n})=s_{n}}$ and $E^{c}(u_{x},u_{y_{n}})$ is in $U$ for each
${1\leq n\leq|W|}$. Furthermore, $\Gamma$ contains atoms
${E^{c}(x,y_{1}),\dots,E^{c}(x,y_{|W|})}$ as well as inequalities
${y_{n}\not\approx y_{m}}$ for ${1\leq n<m\leq|W|}$. We then have
${E^{c}(\nu^{\prime}(x),\nu^{\prime}(y_{n}))\in D^{\prime}}$ and
${\nu^{\prime}(y_{n})\neq\nu^{\prime}(y_{m})}$ for ${1\leq n<m\leq|W|}$. Thus,
${W^{\prime}=\\{v_{\nu^{\prime}(y_{1})},\dots,v_{\nu^{\prime}(y_{|W|})}\\}}$
is a set of $|W|$ _distinct_ $c$-neighbours of $v_{\nu(x)}$ in
$\mathcal{G}^{\prime}$. The induction assumption ensures that
${w=v_{\nu(y_{n})}}$ and ${q=v_{\nu^{\prime}(y_{n})}}$ imply
${(\mathbf{w}_{\lambda_{\ell-1}})_{j}\leq(\mathbf{q}_{\lambda_{\ell-1}^{\prime}})_{j}}$,
and so ${\sum_{w\in W}(\mathbf{w}_{\lambda_{\ell-1}})_{j}\leq\sum_{q\in
W^{\prime}}(\mathbf{q}_{\lambda_{\ell-1}^{\prime}})_{j}}$. Thus, by equations
(51) and (52), the fact that the elements from $\mathbf{A}_{\ell}$ and all
$\mathbf{B}_{\ell}^{c}$ are nonnegative, and $\sigma$ is monotonically
increasing, we have
$(\mathbf{v}_{\lambda_{\ell}})_{i}\leq(\mathbf{p}_{\lambda_{\ell}^{\prime}})_{i}$,
as required.

Recall that ${\alpha^{\prime}=H\nu^{\prime}}$ is of the form
$U_{i}(t^{\prime})$ with ${t^{\prime}=\nu^{\prime}(x)}$; moreover,
${U_{i}(t)\in T_{\mathcal{N}^{\prime}}(D)}$ with ${t=\nu(x)}$. Now let
$v=v_{t}$ and $p=v_{t^{\prime}}$. Now ${U_{i}(t)\in
T_{\mathcal{N}^{\prime}}(D)}$ implies
$\mathsf{cls}((\mathbf{v}_{\lambda_{L}})_{i})=1$, and the above property
ensures
$(\mathbf{v}_{\lambda_{L}})_{i}\leq(\mathbf{p}_{\lambda_{L}^{\prime}})_{i}$;
since $\mathsf{cls}$ is a step function, we have
$\mathsf{cls}((\mathbf{p}_{\lambda_{L}^{\prime}})_{i})=1$. Hence,
$U_{i}(t^{\prime})\in T_{\mathcal{N}^{\prime}}(D^{\prime})$, as required. ∎

See 14

###### Proof.

We first prove the two items of the theorem, and then we prove that Algorithm
1 terminates.

First, recall that by condition (S4) of Lemma A.1, for each ${0\leq\ell\leq
L}$ and each $1\leq i\leq\delta_{\ell}$, set $\mathcal{X}_{\ell,i}$ is
contains exactly all the elements of $\mathcal{S}_{\ell,i}$. Furthermore,
since $\mathcal{S}_{\ell,i}$ is strictly monotonically increasing by condition
(S2) of Lemma A.1, its smallest element is its first element. Hence, the
smallest element of $\mathcal{X}_{\ell,i}$ is the first element of
$\mathcal{S}_{\ell,i}$. Furthermore, for any $\alpha\in\mathbb{R}$, let
$S_{{\ell,i}}^{>\alpha}$ be the subsequence of $\mathcal{S}_{\ell,i}$ which
contains all elements in $S_{{\ell,i}}^{>\alpha}$ greater than $\alpha$.
Clearly, $\mathcal{X}_{\ell,i}^{>\alpha}$ is identical to the set of elements
in $S_{{\ell,i}}^{>\alpha}$. Furthermore, since $\mathcal{S}_{\ell,i}$ is
strictly monotonically increasing, then either $S_{{\ell,i}}^{>\alpha}$ is
empty or it contains an element $s_{{\ell,i}}^{>\alpha}$ which appears in
$\mathcal{S}_{\ell,i}$ exactly once and satisfies the following conditions:

  1. (A1)

all elements that precede $s_{{\ell,i}}^{>\alpha}$ in $\mathcal{S}_{\ell,i}$
are smaller or equal to $\alpha$; and

  2. (A2)

all elements that follow $s_{{\ell,i}}^{>\alpha}$ in $\mathcal{S}_{\ell,i}$
are strictly greater than $s_{{\ell,i}}^{>\alpha}$.

In particular, condition (A2) ensures that if $S_{{\ell,i}}^{>\alpha}$ is not
empty, then $s_{{\ell,i}}^{>\alpha}$ is its smallest element. Hence, to show
the items of the theorem, it suffices to prove the following:

  * •

$\mathsf{Next}(\ell,i,{\vartriangleright})$ returns the first element of
$\mathcal{S}_{\ell,i}$, and

  * •

for each $\alpha\in\mathbb{R}$, $\mathsf{Next}(\ell,i,\alpha)$ returns
${\vartriangleleft}$ if $S_{{\ell,i}}^{>\alpha}$ is empty, and otherwise it
returns $s_{{\ell,i}}^{>\alpha}$.

We show both items simultaneously via induction over $0\leq\ell\leq L$.

For the base case $\ell=0$, consider an arbitrary $1\leq i\leq\delta_{0}$. To
see that $\mathsf{Next}(0,i,{\vartriangleright})$ returns the first element of
$\mathcal{S}_{0,i}$, simply note that line 2 of Algorithm 2 ensures that
$\mathsf{Next}(0,i,{\vartriangleright})=0$, which is precisely the smallest
element of $\mathcal{S}_{0,i}$. To prove the second item, consider an
arbitrary $\alpha\in\mathbb{R}$. If $S_{{0,i}}^{>\alpha}$ is empty then,
$\alpha\geq 1$, in which case line 4 of Algorithm 2 ensures
$\mathsf{Next}(0,i,\alpha)={\vartriangleleft}$, as expected. If
$S_{{0,i}}^{>\alpha}$ is not empty, we consider two possible cases: $\alpha<0$
or $0\leq\alpha<1$. If $\alpha<0$, then $S_{{0,i}}^{>\alpha}=(0,1)$, but
$\mathsf{Next}(0,i,\alpha)=0$ by line 2 of Algorithm 2, so the claim holds. If
$0\leq\alpha<1$, then $S_{{0,i}}^{>\alpha}=(1)$. But then, line 3 of Algorithm
2 ensures $\mathsf{Next}(0,i,\alpha)=1$.

For the induction step, consider some arbitrary $1\leq\ell\leq L$, and suppose
that both items above hold for $\ell-1$. Consider an arbitrary $1\leq
i\leq\delta_{\ell}$. We first show the first item. Observe that, the
definition of $\mathcal{S}_{\ell,i}$ ensures that its first element is
$\sigma(z)$ for
$z=\mathsf{Val}(\ell,i,\mathbf{s}_{\ell-1},\mathbf{Y}_{\emptyset})$. Recall
that $\mathbf{s}_{\ell-1}$ is defined as the vector of dimension
$\delta_{\ell-1}$ where $(\mathbf{s}_{\ell-1})_{j}$ is the first element of
$\mathcal{S}_{\ell-1,j}$, for each $1\leq j\leq\delta_{\ell-1}$. However, by
induction hypothesis,
$(\mathbf{s}_{\ell-1})_{j}=\mathsf{Next}(\ell-1,j,{\vartriangleright})$, and
so $\mathbf{s}_{\ell-1}=\mathsf{Start}(\ell)$. Then, lines 6 and 7 of
Algorithm 2 ensure that $\mathsf{Next}(\ell,i,{\vartriangleright})$ is
precisely $\sigma(z)$. We now show the second item. Consider an arbitrary
$\alpha\in\mathbb{R}$. We study the execution of
$\mathsf{Next}(\ell,i,\alpha)$. Since $\alpha\neq{\vartriangleright}$, $F$ is
initialised as stated in line 8 and so the loop starting in line 9 is
executed. We consider now the outcome of the loop’s execution. Let
$\mathcal{S}_{\ell,i}=q_{0},q_{1},\dots$. Let $N\geq 0$ be the smallest
natural number such that either $q_{N}$ is not defined or $q_{N}>\alpha$; such
$N$ must exist since $\mathcal{S}_{\ell,i}$ is either finite or it converges
to infinity, and furthermore it is strictly monotonically increasing. We next
show the following claim ($\ast$): for each $0\leq n\leq N$, the algorithm’s
loop reaches a state where $F=f_{n}$ after a finite number of iterations. We
prove this by induction on $n$.

The base case is straightforward since $F$ initially contains only the triple
$\langle\mathsf{Start}(\ell),\mathbf{Y}_{\emptyset},z\rangle$, where
$z=\mathsf{Val}(\ell,i,\mathsf{Start}(\ell),\mathbf{Y}_{\emptyset})$.
Furthermore, $f_{0}$ contains only the triple
$\langle\mathbf{s}_{\ell-1},\mathbf{Y}_{\emptyset},z^{\prime}\rangle$, for
$z^{\prime}=\mathsf{Val}(\ell,i,\mathbf{s}_{\ell-1},\mathbf{Y}_{\emptyset})$.
However, we have already shown that
$\mathsf{Start}(\ell)=\mathbf{s}_{\ell-1}$, so the initial state of $F$ is
identical to $f_{0}$. For the induction step, consider an arbitrary $0\leq
n<N$ and suppose that $F=f_{n}$ after a finite number of iterations of the
algorithm’s loop; we then show that $F=f_{n+1}$ holds after a finite number of
additional iterations. By definition, $f_{n}$ contains (at least) a triple of
the form $\langle\mathbf{x},\mathbf{Y},z\rangle$ with $\sigma(z)=q_{n}$, and
all other triples in $f_{n}$ are of the form
$\langle\mathbf{x}^{\prime},\mathbf{Y}^{\prime},z^{\prime}\rangle$ with