# On the BDD/FC Conjecture

Tomasz Gogacz

Jerzy Marcinkowski

Institute of Computer Science  University of Wroclaw  Poland
<EMAIL_ADDRESS>Institute of Computer Science  University of Wroclaw
Poland<EMAIL_ADDRESS>
(30 July 1999)

###### Abstract

Bounded Derivation Depth property (BDD) and Finite Controllability (FC) are
two properties of sets of datalog rules and tuple generating dependencies
(known as Datalog∃ programs), which recently attracted some attention. We
conjecture that the first of these properties implies the second, and support
this conjecture by some evidence proving, among other results, that it holds
true for all theories over binary signature.

###### category:

F.4.1 Theory of Computation Mathematical Logic and Formal Languages:

###### category:

H.2.4 Database Management Systems - Relational databases

###### keywords:

Bounded Derivation Depth, Tuple Generating Dependencies, Finite
Controllability

††titlenote: Supported by Polish Ministry of Science and Higher Education NCN
grant N N206 371339.

Mathematical Logic rule-based databases, query processing

##  1 Introduction

Tuple generating dependencies (TGDs), recently known also as Datalog∃ rules,
are studied in various areas, from database theory to description logics, and
in various contexts. The context we are interested in here, is computing
certain answers to queries in the situation when some semantical information
about the database is known, and represented by some theory $\cal T$ (or a
Datalog∃ program), consisting of existential TGDs and plain datalog rules, but
it is assumed that our knowledge of the database facts is incomplete (this is
known as the open-world assumption).

In this paradigm, for a database instance $D$ (understood here as a set of
facts – atomic formulas), the semantics of $D$, in presence of $\cal T$ is
defined as the (*) set of all the database instances $\bar{D}$ which are
supersets of $D$ and satisfy $\cal T$. In other words, we are interested
whether, for a given query111Whenever we say ”query” in this paper we mean a
conjunctive query without negation. Whenever we say ”TGD” we mean a single-
head tuple generating dependency. $\Phi$, it holds that ${\cal
T},D\models\Phi$.

The problem is of course undecidable in general, so some restricted classes of
theories are being studied. For example Linear Datalog∃ programs, which
consist of TGDs which, as the body, have a single atomic formula, were studied
in [8], Guarded Datalog∃, being an extension of Linear (see Section 5.6 for
more details) was analyzed in [1] and Sticky Datalog∃ programs were introduced
(in two flavors) in [4] and [5].

As it turns out, decidability of query answering is not that hard to prove for
theories from these classes. But there are good reasons why we would like to
have more than just decidability. The desired properties of $\cal T$ are
(among others) Bounded Derivation Depth property (BDD) and Finite
Controllability (FC).

The theory $\cal T$ has the Finite Controllability property (for short: "$\cal
T$ is FC"), if the expression "the set of all database instances" in the
definition (*) above can be equivalently replaced by, more natural from the
database point of view, "the set of all finite database instances". To be more
precise:

######  Definition 1.

$\cal T$ is FC if for each database instance $D$ and each query $\Phi$, if
${\cal T},D\not\models\Phi$ then there exists a database instance $\cal M$
such that ${\cal M}\models D,\cal T$ but ${\cal M}\not\models\Phi$.

The difficult technical results in [8] (solving an old problem stated in [7])
and in [1] concern Finite Controllability of, respectively, Linear and Guarded
Datalog∃. (Actually, the result in [8] is stated in terms of Inclusion
Dependencies rather than TGDs, which, in this context, is another language to
talk about the same thing.) The question if the Sticky Datalog∃ programs are
FC was left as an open problem in [4] and was solved, positively, in [6].

The theory $\cal T$ has the Bounded Derivation Depth property (or just: "$\cal
T$ is BDD") if it admits positive first order query rewriting. In other words:

######  Definition 2.

$\cal T$ is BDD if for each query $\Phi$ there exists a union of conjunctive
queries $\Phi^{\prime}$ such that for every database instance $D$ the
equivalence : ${\cal T},D\models\Phi$ if and only if $D\models\Phi^{\prime}$
holds. (This is the definition we actually need here, but not the standard
one. See Section 1.1 for an equivalent, more standard definition. )

This means that instead of computing the answer to $\Phi$ over the infinite
set of databases having $D$ as their subset (or instead of computing the
answer to $\Phi$ over the infinite database $Chase(D,{\cal T})$ – see Section
1.1) it is enough to compute the answer to $\Phi^{\prime}$ over the known
finite database $D$. There is no need to explain how desirable in the database
context BDD is, so many of the good classes of Datalog∃ programs (including
Linear Datalog∃ and Sticky Datalog∃) are tailored to have this property. It is
worth mentioning that, while of course BDD is an undecidable property of $\cal
T$, still in all practical situations we know about, proving the statement
"all the programs from class $\cal C$ are BDD" is an easy exercise (if it is
true). This is in sharp contrast to Finite Controllability which is, as we
mentioned above, typically quite hard to prove.

BDD is typically easy to prove. FC is hard to prove. But each time we had a
class of BDD theories, finally we were able to show that this class is also
FC. This leads to a conjecture we would like to state here:

######  Conjecture 1 (The BDD/FC conjecture).

If some theory $\cal T$, being a set of existential TGDs and plain datalog
rules, is BDD then it is also FC.

The evidence we support our conjecture with is:

######  Theorem 1 (The main result of this paper).

Conjecture 1 is true for programs over binary signature.

The proof of Theorem 1 is the main technical contribution of this paper and
is, as we believe, quite difficult. It is presented in Section 3 but relies on
a system of tools developed in Sections 2 and 4.

Finally, in Section 5 we discuss the possible applications of our tools and
their limitations, In subsection 5.1 we show that Theorem 1 can be extended
also to quite a wide class of non-binary theories (see Theorem 3). In
subsection 5.4 we explain however, why our techniques do not seem to extend to
the proof of Conjecture 1 in general. In subsection 5.6 we show how Guarded
Datalog∃ programs can be seen as binary programs, and how our techniques can
be easily applied in this context.

###  1.1 TGDs and Chase – preliminaries

Let us remind the reader that a TGD is a formula of the form
$\forall\bar{x}\;(\Phi(\bar{x})\Rightarrow\exists y\;Q(y,\bar{y}))$ where
$\Phi$ is a conjunctive query, $Q$ is a relation symbol, $\bar{x},\bar{y}$ are
tuples of variables and $\bar{y}\subseteq\bar{x}$ (see Section 5.3 for a
comment on the multi-head TGDs). The universal quantifier in front of the
formula is usually omitted.

Finite sets consisting of existential TGDs and plain datalog rules will be
called theories.

For a theory $\cal T$ and a database instance $D$ we denote by
$Chase^{1}(D,{\cal T})$ the result of the following operation. For each tuple
$\bar{x}$ in $D$ satisfying a body of an rule
$t_{i}=\forall\bar{x}\;(\Phi(\bar{x})\Rightarrow\exists y\;Q(y,\bar{y}))$ form
$\cal T$, such that there is no $y\in D$ satisfying $D\models Q(y,\bar{y}))$,
we simultaneously add new constant $c_{t_{i},\bar{x}}$ into database and an
atom $Q(c_{t_{i},\bar{x}},\bar{y})$.

Then define $Chase^{i+1}(D,\cal T)$ as $Chase^{1}(Chase^{i}(D,\cal T),\cal T)$
and by Chase denote $\bigcup_{i}Chase^{i}(D,\cal T)$, which is the least
fixpoint of the $Chase^{1}$ operator.

Clearly, we have $Chase(D,{\cal T})\models D,\cal T$, but there is no reason
to think that $Chase^{i}(D,{\cal T})\models\cal T$ for any $i\in\mathbb{N}$.
Note that the chase we consider in this paper is the non-oblivious one – new
elements are only created if needed, as opposed to the blind Chase, which
creates a new witness each time it is demanded.

Since $Chase(D,{\cal T})$ is a ”free structure”, it is very easy to see that
for any query $\Phi$ (being a UCQ – a union of positive conjunctive queries)
$D,{\cal T}\models\Phi$ (which reads as ”$\Phi$ is certainly true in $D$, in
presence of $\cal T$”), if and only if $Chase(D,{\cal T})\models\Phi$.

A set $\cal T$ of TGDs is usually said to have Bounded Derivation Depth
property if for each query $\Psi$, there is a constant
$k_{\Psi}\in\mathbb{N}$, such that for each database instance $D$ if
$Chase(D,{\cal T})\models\Psi$ then $Chase^{k_{\Psi}}(D,{\cal T})\models\Psi$.
It is easy to see ([2]) that this definition of the BDD property is equivalent
to Definition 2.

Notations. When we say that ${\cal C}$ is a structure we may mean both, the
set of elements and the set of atoms of ${\cal C}$. If we feel this may cause
confusion we write $\operatorname{Dom}({\cal C})$ for the set of elements of
${\cal C}$. By ${\cal C}\models R$ (or ${\cal C}\models\psi$) we mean that an
atom $R$ (or a formula $\psi$) is true in ${\cal C}$. By ${\cal
C}_{1}\models{\cal C}_{2}$ we mean that each atom of ${\cal C}_{2}$ is an atom
of ${\cal C}_{1}$. For a structure ${\cal C}$ and a set $A$ (or a signature
$\Sigma$) by ${\cal C}\upharpoonright A$ (resp. by ${\cal
C}\upharpoonright\Sigma$) we mean the structure consisting of such atoms
$R(\bar{a})$ that ${\cal C}\models R(\bar{a})$ and $\bar{a}\subseteq A$ (resp.
$R\in\Sigma$). For a structure ${\cal C}$ over some signature $\Sigma$ by
${\cal C}_{con}$ we mean, depending on context, the set of elements of ${\cal
C}$ which are interpretations of constants from $\Sigma$ or the structure
${\cal C}\upharpoonright{\cal C}_{con}$. Similarly, by ${\cal C}_{non}$ we
mean the set of elements of ${\cal C}$ which are not incarnations of constants
from $\Sigma$ or the structure ${\cal C}\upharpoonright{\cal C}_{non}$.

In paper we consider only Boolean conjunctive queries. Sometimes free
variables are omitted to keep the notation light. In such cases one should
treat them as existentially quantified. (For example, for a query
$\Phi(\bar{x})$ the term $M\models\Phi$ should be read as
$M\models\exists\bar{x}\;\Phi(\bar{x})$).

##  2 Types and projections

###  2.1 The main ideas and
the structure of the proof

In order to prove Theorem 1 we need to construct, for a given BDD theory
${\cal T}$ over a binary signature, for a conjunctive query $Q(\bar{x})$ and
for a finite structure $D$, such that $Chase(D,{\cal
T})\not\models\exists\bar{x}\;Q(\bar{x})$, a new finite structure $M$, such
that $M\models D,{\cal T}$ but $M\not\models\exists\bar{x}\;Q(\bar{x})$.

Such $M$ will always contain a substructure $M^{\prime}$ being a homomorphic
image of $Chase(D,{\cal T})$. This $M^{\prime}$ is easy to construct inside
$M$ (if we had $M$): start from $D$, which is a substructure of both $M$ and
$Chase(D,{\cal T})$, and then mimic, inside $M$, all the applications of rules
that led to the construction of $Chase(D,{\cal T})$.

Isn’t $M^{\prime}$ itself always the finite model we are looking for? No,
because it may very well happen that by identifying elements of $Chase(D,{\cal
T})$ the homomorphism (call it $q$) created new instances of the bodies of the
rules of $\cal T$ in $M^{\prime}$, leading to the situation when applications
of rules is possible that were not applied in $Chase(D,{\cal T})$. For example
suppose that $E(x,y),R(y,z)\Rightarrow U(y)$ is a rule of $\cal T$ and
$Chase(D,{\cal T})\models E(a,b),R(b^{\prime},c)$, but $Chase(D,{\cal
T})\not\models U(b)$ and $Chase(D,{\cal T})\not\models U(b^{\prime})$. Suppose
also that $q(b)=q(b^{\prime})$. Then the fact $U(q(b))$, which may not be
homomorphic image of any fact in $Chase(D,{\cal T})$, is provable in $M$. This
can lead to a process in which an answer to $Q$ is built in $M$, something we
need to avoid. This can also lead to infinite chase, while we want $M$ to be a
finite structure. Let us illustrate this problem with one more example:

######  Example 1.

Let $\cal T$ be a theory consisting of three rules:

$E(x,y)\Rightarrow\exists z\;E(y,z)$

$E(x,y),E(y,z),E(z,x)\Rightarrow\exists t\;U(x,t)$

$U(x,y)\Rightarrow\exists z\;U(y,z)$

and a database instance $D=\\{E(a,b)\\}$.

Then $Chase(D,{\cal T})$ is an infinite $E-chain$, beginning with $a$ and $b$.
Consider $M^{\prime}$ consisting of elements $a,b$ and $c$ and atoms $E(a,b)$,
$E(b,c)$ and $E(c,a)$. Then $M^{\prime}$ is a homomorphic image of
$Chase(D,{\cal T})$, but is not itself a model of $\cal T$ – the last rule,
which was never triggered when $Chase(D,{\cal T})$ was built, can be used in
$M^{\prime}$. Moreover, it is easy to see that $Chase(M^{\prime},{\cal T})$ is
an infinite structure.

The idea of the construction we present in this paper is to make sure that
some sort of first order type of each $a$ in $Chase(D,{\cal T})$ is always the
same as the type of its image $q(a)$ in the homomorphic image of
$Chase(D,{\cal T})$. The definition of the type should be tailored in such a
way that such preservation of types implies that no harmful new applications
of rules from $\cal T$ for $q(a)$ exist in $M$.

In Section 2 we develop a sort of theory of positive types and their
preservation. We built a framework in which the Main Lemma (Lemma 2) can be
expressed. In Section 3 this Main Lemma is used to prove Theorem 1. In Section
4 we prove the Main Lemma. Sections 3 and 4 are independent and can be read in
any order.

The two most important technical tricks of the paper can be found in proofs of
Lemma 5 (in Section 3) and Lemma 11 (in Section 4). In the proof of Lemma 5 we
show how the assumption that the theory $\cal T$ is BDD can be used. The trick
in the proof of Lemma 11 relies on the construction, presented already in
Section 2.3, where we construct not just one finite structure, but an infinite
sequence of finite structures $M_{n}$ that in some sense converge to
$Chase(D,{\cal T})$. Then the idea is that if some query $\Psi$ is true in
$M_{n+1}$ (which we do not like, as we do not want too many queries to be true
in the finite structures we construct) then a query $\Phi$, being a ”one-step
normalized” version of $\Psi$ may not be true in $M_{n+1}$ but it will be true
in $M_{n}$. This then implies that if $\Psi$ is true in all $M_{n}$ then its
”normal form” also is. This ”converging to the Chase” trick is also used in
our another paper [6] and we believe it can have further applications.

###  2.2 Positive types

######  Definition 3.

Let $\cal C$ be a relational structure over signature $\Theta$. Let
$e\in\cal{\cal C}$ and let $n$ be a natural number. We define $ptp_{n}({\cal
C},e,\Theta)$ (which reads "positive n-type of $e$ in $\cal C$ over $\Theta$”)
as the set of all such conjunctive queries $\Psi(\bar{x},y)$ that:

  * •

$|\bar{x}|<n$,

  * •

all relations (and constants) used in $\Psi$ are in $\Theta$

  * •

${\cal C}\models\Psi(\bar{x},e)$.

We assume that equality belongs to each $\Theta$, which means that atoms of
the form $x=c$ (but not of the form $x\neq c$), where $x$ is a variable and
$c$ is a constant from $\Theta$, are allowed in the queries.

######  Example 2.

Let $\cal T$, $D$ and $M^{\prime}$ be like in Example 1, and let $\Theta$
consist of $E$ and $U$. Then $ptp_{2}(Chase(D,{\cal T})),a,\Theta)$ equals
$ptp_{2}(M^{\prime},a,\Theta)$, and each of them consists of the same two
queries: $E(x,y)$ and $E(y,x)$. But $ptp_{3}(Chase(D,{\cal T})),a,\Theta)$
does not equal $ptp_{3}(M^{\prime},a,\Theta)$: the query $E(y,x_{1})\wedge
E(x_{1},x_{2})$ $\wedge E(x_{2},y)$ belongs to the second of those two types
but not to the first one.

######  Remark 1.

Notice that if $c$ is a constant222Strictly speaking, we mean a value of this
constant in ${\cal C}$, but we are not always going to make this distinction.
from $\Theta$, and if $a\neq c$ is any other element of ${\cal C}$, then
$ptp_{n}({\cal C},c,\Theta)\neq ptp_{n}({\cal C},a,\Theta)$ for each $n\geq
1$. This is because we allowed a query of the form $y=c$, which belongs to
$ptp_{1}({\cal C},c,\Theta)$, but not to $ptp_{1}({\cal C},a,\Theta)$.

All the signatures under consideration are finite, so the number of possible
conjunctive queries with at most $n$ variables is finite. In consequence the
number of positive $n$-types is finite, for a given $n$.

Let us remark here that our positive $n$-types carry much less information
than the standard first order types (in the sense of Geifman or Hanf). Take
for example a structure $\cal C$, over the signature $\Theta=\\{R,E\\}$,
consisting of elements $a$,$b$,$c$,$d$,$e$, and atoms $R(a,b)$, $R(a,c)$,
$E(a,c)$, $E(d,e)$, $R(d,e)$. Then $ptp_{2}({\cal C},a,\Theta)=$
$ptp_{2}({\cal C},e,\Theta)$. But the first order 2-types of $a$ and $e$
differ: consider for example the formula: $\psi(x)=\exists z,y\;R(x,y)\wedge
E(x,z)\wedge y\neq z$. Then ${\cal C}\models\psi(a)$ but ${\cal
C}\not\models\psi(d)$.

###  2.3 How the finite structures are born

######  Definition 4.

Let $d$ and $e$ be two elements of $\cal C$. We define $d\equiv_{n}e$ if and
only if $ptp_{n}({\cal C},d,\Theta)=ptp_{n}({\cal C},e,\Theta)$.

Notice that both the relation $\equiv_{n}$ and the structures $M_{n}({\cal
C})$ (as defined below) depend on $\Theta$, and the signature should be added
as a parameter in Definitions 4 and 5. We will try to avoid confusion while
keeping the notation light, but when really needed we will include the
parameter, writing $M_{n}^{\Theta}({\cal C})$ instead of $M_{n}({\cal C})$.

######  Definition 5.

For a relational structure ${\cal C}$ define $M_{n}({\cal C})$ as a relational
structure whose set of elements is ${\cal C}/\equiv_{n}$, and such that
$M_{n}({\cal C})\models R(<[a_{i}]_{\equiv_{n}}>_{i})$ iff $\forall
i~{}\exists b_{i}\in[a_{i}]_{\equiv_{n}}$ such that ${\cal C}\models
R(<b_{i}>_{i})$.

In other words, the relations in $M_{n}({\cal C})$ are defined in the natural
way, as minimal (with respect to inclusion) relations such that the quotient
mapping $q_{n}:{\cal C}\longrightarrow M_{n}({\cal C})$ is a homomorphism.

We usually imagine $q_{n}$ as a projection333”Projection” in the geometric
sense not the database sense., so that the atoms in $M_{n}({\cal C})$ are
projections of atoms in ${\cal C}$.

Clearly each $M_{n}({\cal C})$ is a finite structure.

######  Lemma 1.

If $q_{n}(d)=q_{n}(e)$ then $q_{n-1}(d)=q_{n-1}(e)$. The structure
$M_{n-1}({\cal C})$ is a homomorphic image of $M_{n}({\cal C})$.

For the proof of the first claim notice that it follows from Definition 3 that
if the positive $n$-types of two elements are equal then their positive
$(n-1)$-types are also equal. The second is an easy exercise in basic
universal algebra.

###### ($\spadesuit$ 1

) The function $q_{n}$, as defined above, has ${\cal C}$ as its domain. It
will however be convenient to be able to write $q_{n}(a)$ also for $a\in
M_{n+1}({\cal C})$. In such a case $q_{n}(a)$ will be defined as $q_{n}(b)$,
where $b\in{\cal C}$ is any element such that $q_{n+1}(b)=a$. It follows from
Lemma 1 that the value of $q_{n}(a)$ does not depend on the choice of $b$.

We defined a canonical way of building finite structures. But is there any
chance that they really resemble the original infinite structure? What we are
particularly interested in is what happens to the positive $m$-types of
elements of ${\cal C}$. Are they preserved by $q_{n}$? It is easy to see that
we always have $ptp_{m}({\cal C},e,\Theta)\subseteq ptp_{m}(M_{n}({\cal
C}),q_{n}(e),\Theta)$. But can the inclusion be replaced with equality? Is the
positive $m$-type of $e\in{\cal C}$ always the same as the positive $m$-type
of $q_{n}(e)$?444Notice that we use two natural numbers here: $n$, which we
imagine is big – the bigger it is the more similar $M_{n}({\cal C})$ and
${\cal C}$ are, and $m$ – the smaller it is the easier it is preserve the
positive $m$-types. Unfortunately this is not yet the case:

######  Example 3.

Let $\Sigma=\\{E\\}$ and let ${\cal C}$ be the set $\\{a_{0},a_{1},a_{2}$
$\ldots\\}$ with $E(a_{i},a_{i+1})$ for each $i$. Notice that the names of the
elements $a_{i}$ are not part of $\Sigma$, so they are invisible for the
inhabitants of the structure, and the positive $n$-types of elements $a_{i}$
and $a_{j}$, with $i\neq j$, are equal if and only if $i,j\geq n$. (Actually,
not only the positive types of $a_{i}$ and $a_{j}$ are equal, but even their
$n$-Gaifman neighborhood are isomorphic.) So $M_{n}^{\Sigma}({\cal C})$ is a
structure with elements $\\{b_{0},b_{1},b_{2},\ldots b_{n}\\}$, with
$E(b_{i},b_{i+1})$ for each $i<n$ and with $E(b_{n},b_{n})$. Clearly,
$q_{n}(a_{n})=b_{n}$. But the positive 1-type of $b_{n}$ in $M_{n}({\cal C})$
contains the query $\exists yR(y,y)$, which is not in the positive 1-type of
$a_{n}$ in ${\cal C}$.

###  2.4 Colored structures

We are not quite happy with the quotient structure we got in Example 3. Too
many elements of ${\cal C}$ are identified, and even a very small conjunctive
query can easily see the difference between ${\cal C}$ and $M_{n}({\cal C})$.
But consider another example:

######  Example 4.

Let $\Sigma$ and ${\cal C}$ be like in Example 3. Let
$\bar{\Sigma}=\Sigma\cup\\{K_{0},K_{1},\ldots K_{m}\\}$, where
$K_{0},K_{1},\ldots K_{m}$ are unary predicates (colors) and let $\bar{{\cal
C}}$ be like ${\cal C}$, but with each $a_{i}$ satisfying also
$K_{i\mod(m+1)}$.

Let $n>m$. Then the positive $n$-types of elements $a_{i}$ and $a_{j}$, with
$i\neq j$, are equal if and only if $i,j\geq n$ and $i=j\mod{m+1}$. So
$M_{n}^{\bar{\Sigma}}(\bar{\cal C})$ will be a structure with elements
$\\{b_{0},b_{1},b_{2},\ldots b_{n+m}\\}$, with $E(b_{i},b_{i+1})$ for each
$i<n+m$ and with $E(b_{n+m},b_{n})$. It is not hard to see that now
$ptp_{m}({\bar{\cal C}},a,\Sigma)=$ $ptp_{m}(M_{n}^{\bar{\Sigma}}(\bar{\cal
C}),q_{n}(a),\Sigma)$ for each element $a\in\bar{\cal C}$. The positive
$m$-types of the elements of ${\cal C}$ are preserved by the quotient
operation.

Notice however that the positive $(m+1)$-types are not preserved. This is
because, unlike ${\cal C}$, the structure $M_{n}^{\bar{\Sigma}}(\bar{\cal C})$
contains a cycle of length $m+1$, which is easy to detect with a query with
$m+1$ variables. If we want to preserve positive $m$-types for bigger numbers
$m$ we need to use more colors.

Notice also that if we took $n<m$ then we would get $ptp_{m}({\bar{\cal
C}},a_{n},\Sigma)\neq$ $ptp_{m}(M_{n}^{\bar{\Sigma}}(\bar{\cal
C}),q_{n}(a_{n}),\Sigma)$. This is because $a_{n}$ would then be identified
with all the elements $a_{n+k{m+1}}$ for $k\in\mathbb{N}$, and therefore the
query
$\exists x_{1}\ldots x_{m-1}E(x_{1},x_{2})\wedge
E(x_{2},x_{3})\wedge\ldots\wedge E(x_{m-1},q_{n}(a_{n}))$
would be satisfied in $M_{n}^{\bar{\Sigma}}(\bar{\cal C})$, while the query
$\exists x_{1}\ldots x_{m-1}E(x_{1},x_{2})\wedge
E(x_{2},x_{3})\wedge\ldots\wedge E(x_{m-1},a_{n})$
is not satisfied in $\bar{\cal C}$.

The last example motivates the following definitions:

######  Definition 6.

Each of the unary predicates $K_{h}^{l}$ for some $h,l\in\mathbb{N}$ will be
called a color, with the number $h$ being called the hue of the color and the
number $l$ being called its lightness. The set of all colors will be denoted
as $\cal K$.

So far we just defined an infinite set of unary predicates (with strange
names, that we will need much later). Now a definition of coloring. A natural
one:

######  Definition 7.

For a structure ${\cal C}$ over a signature $\Sigma$ by a coloring of ${\cal
C}$ we will mean a structure $\bar{\cal C}$ over some finite signature
$\bar{\Sigma}$ such that:

  1. 1.

$\Sigma\subset\bar{\Sigma}\subset\Sigma\cup\cal K$

  2. 2.

$\bar{\cal C}\upharpoonright\Sigma={\cal C}$

  3. 3.

for each $a\in\bar{\cal C}$ there is exactly one color $K\in\cal K$ such that
$\bar{\cal C}\models K(a)$.

where $\bar{\cal C}\upharpoonright\Sigma$ is the structure $\bar{\cal C}$
restricted to the signature $\Sigma$.

###  2.5 Conservative structures

######  Definition 8.

Let ${\cal C}$ be a structure and let $m,n\in\mathbb{N}$. We will say that a
coloring $\bar{\cal C}$ of ${\cal C}$ is $n$-conservative up to size $m$ if:

###### ($\spadesuit$ 2

) $\;ptp_{m}({\cal C},e,\Sigma)=ptp_{m}(M_{n}^{\bar{\Sigma}}(\bar{\cal
C}),q_{n}(e),\Sigma)$ for each $e\in{\cal C}$, where $\Sigma$ and
$\bar{\Sigma}$ are like in Definition 7.

Being $n$-conservative up to size $m$ means that the positive $m$-types (with
respect to the signature $\Sigma$) of elements of $\bar{\cal C}$ are preserved
by the quotient mapping $q_{n}$ leading to the structure
$M_{n}^{\bar{\Sigma}}(\bar{\cal C})$. So, for example, the coloring $\bar{\cal
C}$ from Example 4 is $n$-conservative up to size $m$, if only $n>m$, but is
not $n$-conservative up to size $m+1$ for any $n$.

######  Definition 9.

A structure ${\cal C}$ is ptp-conservative if for each $m\in\mathbb{N}$ there
exist $n\in\mathbb{N}$ and a coloring $\bar{\cal C}$ of ${\cal C}$, such that
$\bar{\cal C}$ is $n$-conservative up to size $m$.

The following remark will be useful in Section 4

######  Remark 2.

Consider a coloring $\bar{\cal C}$ of ${\cal C}$ and a number $m$. Suppose
there is no such $n$ that $\bar{\cal C}$ is $n$-conservative up to size $m$.
This means that for each $n\in\mathbb{N}$ there is a query
$\exists\bar{x}\Psi_{n}(\bar{x},y)$, with at most $m$ variables, and an
element $e\in{\cal C}$ such that $M_{n}(\bar{\cal
C})\models\exists\bar{x}\Psi_{n}(\bar{x},q_{n}(e))$ but ${\cal
C}\not\models\exists\bar{x}\Psi_{n}(\bar{x},e)$.

But since there are only finitely many queries of at most $m$ variables, this
implies that there is a query $\Psi$ which is $\Psi_{n}$ for infinitely many
numbers $n$.

Notice also that if $n^{\prime}<n$ and $M_{n}(\bar{\cal
C})\models\exists\bar{x}\Psi(\bar{x},q_{n}(e))$ then $M_{n^{\prime}}(\bar{\cal
C})\models\exists\bar{x}\Psi(\bar{x},q_{n^{\prime}}(e))$.

So, if there is no such $n$ that $\bar{\cal C}$ is $n$-conservative up to size
$m$ then it must exist a single query $\Psi(\bar{x},y)$, with $|x|<m$, such
that for every $n$ there is an element $e$ of ${\cal C}$ such that
$M_{n}(\bar{\cal C})\models\exists\bar{x}\Psi(\bar{x},q_{n}(e))$ but ${\cal
C}\not\models\exists\bar{x}\Psi(\bar{x},e)$.

###  2.6 Further examples and remarks

######  Example 5.

It is very easy to see that the structure ${\cal C}$ from Examples 3 and 4 is
ptp-conservative. Given $m$ one just needs to define the coloring $\bar{\cal
C}$ using $m+1$ colors, like in Example 4, and take $n=m+2$. Then $\bar{\cal
C}$ will be $n$-conservative up to size $m$.

######  Example 6.

Let ${\cal C}$ be any infinite set with a total (irreflexive) order $E$. Then
it is easy to see that ${\cal C}$ is not ptp-conservative. Actually, it is
impossible to find a coloring $\bar{\cal C}$ of ${\cal C}$ and a number $n$
such that $\bar{\cal C}$ is $n$-conservative up to size 1: whatever the
coloring, there would be an element $e$ in ${\cal C}$ such that
$M_{n}^{\bar{\Sigma}}(\bar{\cal C})\models E(q_{n}(e),q_{n}(e))$.

######  Remark 3.

It is very important to see the role of the element $e$ in Definition 8.
Condition ($\spadesuit$ 2.), which says that each element of ${\cal C}$ keeps
its positive type after the quotient operation, is strictly stronger than:

###### ($\spadesuit$ 3

) for each conjunctive query $\Psi$ over $\Sigma$, with at most $m$ variables,
${\cal C}\models\Psi$ if and only if $M_{n}^{\bar{\Sigma}}(\bar{\cal
C})\models\Psi$.

which says that no new positive $m$-types appear in
$M_{n}^{\bar{\Sigma}}{\bar{\cal C}}$.

To see that, consider a theory $\cal T$ consisting of the rules:

$E(x,y)\Rightarrow\exists z\;E(y,z)$

$E(x,y),E(y,z)\Rightarrow E(x,z)$

and a database instance $D=\\{E(a,a),E(b,c)\\}$.

Let ${\cal C}=Chase(D,{\cal T})$. Then ${\cal C}$ satisfies condition
($\spadesuit$ 3.) (since, due to the presence of the atom $E(a,a)$, all
possible queries are true in ${\cal C}$), but is not ptp-conservative as it
contains an infinite irreflexive total order (see Example 6).

Next remark explains what Definition 9 is good for:

######  Remark 4.

Imagine that we have some theory $\cal T$ over a binary signature $\Sigma$,
and there is a existential TGD $\Psi$ in $\cal T$ of the form
$\psi(\bar{x},y)\Rightarrow\exists z\;R(y,z)$, where $m$ is the number of
variables in $x$. Let ${\cal C}=Chase(D,{\cal T})$. Clearly ${\cal
C}\models\Psi$, so if for some $e\in{\cal C}$ it holds that
$\exists\bar{x}\psi(\bar{x},y)\in ptp_{m}({\cal C},e,\Sigma)$, then there
exists $d\in{\cal C}$ such that ${\cal C}\models R(e,d)$.

Suppose we now color ${\cal C}$ and project it, using $q_{n}$, creating some
finite structure $M_{n}(\bar{\cal C})$. We would like to be sure that
$M_{n}({\cal C})$ is still a model (or at least some sort of pre-model) of
$\cal T$. So in particular we would like to be sure that $M_{n}({\cal
C})\models\Psi$.

But if $\bar{\cal C}$ was $n$-conservative up to size $m$, then we can be sure
that whenever we have an element $a=q_{n}(e)$ in $M_{n}(\bar{\cal C})$, such
that $M_{n}(\bar{\cal C})\models\exists\bar{x}\psi(\bar{x},a)$ then also
${\cal C}\models\exists\bar{x}\psi(\bar{x},e)$, which implies that ${\cal
C}\models\exists z\;R(e,z)$, which implies that $M_{n}(\bar{\cal C})$
$\models\exists z\;R(a,z)$ (notice that what we use here is really Condition
($\spadesuit$ 2.) and that Condition ($\spadesuit$ 3.) would not be strong
enough)

So, if $\bar{\cal C}$ was $n$-conservative up to size $m$, then
$M_{n}(\bar{\cal C})$ is a model of $\Psi$, and if ${\cal C}$ is ptp-
conservative then we can choose $m$ greater than the maximal size of the body
of a existential TGD rule in $\cal T$ and be sure that there exists a
coloring, and number $n$, leading to $M_{n}(\bar{\cal C})$ in which all the
existential TGDs of $\cal T$ are satisfied.

We now know how to turn a ptp-conservative Chase ${\cal C}$ of $\cal T$ into a
finite structure $M_{n}(\bar{\cal C})$ satisfying all the existential TGDs in
$\cal T$. But does it mean that $M_{n}(\bar{\cal C})\models{\cal T}$ then? As
the following example shows, not necessarily, even if $\cal T$ is BDD:

######  Example 7.

Consider the following BDD theory $\cal T$:

$E(x,y)\Rightarrow\exists z\;E(y,z)$

$E(x,y),E(x^{\prime},y)\Rightarrow R(x,x^{\prime})$

and a database instance $D=\\{E(a,b)\\}$.

Let ${\cal C}=Chase(D,{\cal T})$. Clearly, ${\cal C}$ is an infinite
$E$-chain, with an atom $R(e,e)$ true for each $e\in{\cal C}$. Whatever
coloring we now use, the only $R$ atoms in $M_{n}(\bar{\cal C})$ will be the
ones of the form $R(e,e)$. And whatever the coloring, there must be a triple
of elements $a,b,c$ in $M_{n}(\bar{\cal C})$ such that $a\neq b$ and
$M_{n}(\bar{\cal C})\models E(a,c),E(b,c)$, which shows that $M_{n}(\bar{\cal
C})$ is not a model of the plain datalog rule from $\cal T$.

Of course all the above definitions – of types, of $\equiv_{n}$, of $M_{n}$
and of conservativity, make sense also when we consider any signatures, not
just binary. But Remark 4 is not valid any more for such signatures, which
means that it is very hard to make sure that $M_{n}$ will actually resemble a
model of $\cal T$. We will be back to this point in Section 5.4.

###  2.7 Very Treelike DAGs and the Main Lemma

Most of the notions we defined so far apply to structures over any signature.
But what we are really interested in in this paper are binary signatures. They
consist of some binary relations, some unary relations and constants.
Structures over such signatures can be in a natural way seen as directed
graphs with edges, and vertices, labeled with some finite number of labels
(i.e. the names of the relations). Thanks to that we can use the language of
graphs – for example our infinite structures are usually (directed) trees or
DAGs.

We will concentrate on Very Treelike DAGs:

######  Definition 10.

For an element $e\in{\cal C}$ we define ${\cal P}(e)=\\{e\\}$ if $e\in{\cal
C}_{con}$ and ${\cal P}(e)=\\{e\\}\cup\\{x\in{\cal C}_{non}:{\cal C}\models
R(x,e)$ for some $R\in\Sigma\;\\}$ if $e\in{\cal C}_{non}$

######  Definition 11.

A structure ${\cal C}$ is called a Very Treelike DAG (VTDAG) if ${\cal
C}_{non}$ is a DAG and:

  * •

for each binary relation $R$ and each $e\in{\cal C}_{non}$ there is at most
one $d\in{\cal C}_{non}$ such that $R(d,e)$;

  * •

for each $e\in{\cal C}_{non}$ if $d,d^{\prime}\in{\cal P}(e)$ then $d\in{\cal
P}(d^{\prime})$ or $d^{\prime}\in{\cal P}(d)$.

The first condition says that each non-constant $e$ has at most one non-
constant ”direct predecessor” in each binary relation. The second says that
the set of ”direct predecessors” of $e$ is a (directed) clique.

Each tree is trivially a VTDAG. In order to prove Theorem 1 it is enough to
restrict the attention to trees only. VTDAGs which are not trees will not be
considered before Section 5.

The main tool in the proof of Theorem 1 is:

######  Lemma 2.

[The Main Lemma]
Each VTDAG is ptp-conservative.

In Section 3 we use Lemma 2 to prove Theorem 1. Then, in Section 4, we present
a proof of Lemma 2. Sections 3 and 4 are independent and can be read in any
order.

##  3 From the Main Lemma to Theorem 2

###  3.1 Hiding the query inside the theory

Nothing complicated happens in this subsection. We are just making some
simplifying (although without loss of generality) assumptions about the BDD
theory under consideration. This will help us to keep the notations simpler in
the rest of Section 3

For a binary BDD theory ${\cal T}_{0}$ and a conjunctive query $Q(\bar{x},y)$
define a new theory ${\cal T}$ as ${\cal T}_{0}$ enriched with a new TGD:

###### ($\spadesuit$ 4

) $Q(\bar{x},y)\Rightarrow\exists z\;F(y,z)$

where $F$ is a new predicate symbol. It is now easy to see that, for any
database instance $D$ such that $F$ does not occur in $D$, a finite structure
${\cal M}$ such that ${\cal M}\models{\cal T}_{0},D,\neg Q$ exists if and only
if a finite structure ${\cal M}$ such that ${\cal M}\models{\cal T},D,\neg F$
exists. This means that, in order to prove Theorem 1 it is enough to show:

######  Theorem 2.

For a binary BDD theory $\cal T$, containing a rule of the form ($\spadesuit$
4.), with predicate $F$ not occurring anywhere else in $\cal T$, and for each
database instance $D$, if $F$ does not occur in $Chase(D,{\cal T})$ then there
exists a finite structure $\cal M$ such that ${\cal M}\models D,{\cal T}$,
without any atom of predicate $F$ occurring in $\cal M$.

From now on we assume that $\cal T$ is like in the assumptions of the above
Theorem. We also assume, in order to keep the notations simple, that:

###### ($\spadesuit$ 5

)

  * •

the head of each existential TGD in $\cal T$ is of the form $\exists
z\;R(y,z)$, which means that the witness, whose existence is demanded by the
TGD, is the second argument of the predicate in the head;

  * •

if the predicate $R$ occurs as the head of some existential TGD in $\cal T$
then it does not occur as the head of any datalog rule in $\cal T$. We call
such predicates TGPs – tuple generating predicates.

We leave it for the readers as an exercise to see that every $\cal T$ can be
easily modified to satisfy ($\spadesuit$ 5.), for the cost of some additional
predicates and datalog rules, and this modification neither changes the BDD
status of the theory nor its FC status.

Hint: For each predicate $R$ in the signature introduce two new predicates
$R^{\prime}$ and $R^{\prime\prime}$. Add to theory datalog rules
$R^{\prime}(x,y)\rightarrow R(x,y)$ and $R^{\prime\prime}(x,y)\rightarrow
R(y,x)$. Replace each head of an existential TGD which is of the form $\exists
z\;R(y,z)$ by $\exists z\;R^{\prime}(y,z)$ and each head of the form $\exists
z\;R(z,y)$ by $\exists z\;R^{\prime\prime}(y,z)$.

###  3.2 The structure ${{\cal S}}(D,{\cal T})$

Let now $D$ be a database instance without atoms of $F$ and let $\Theta$ be
the signature of $D$ and $\cal T$. Define $\Sigma\supseteq\Theta$ as a new
signature which contains, apart from the relations and constants from
$\Theta$, a name for each element in $D$. Why do we prefer the elements of $D$
to be named? Because we want to be sure that their positive types in
$Chase(D,{\cal T})$ differ, and, in consequence, that they remain distinct
after a quotient operation (see Remark 1).

Now we are going to define the structure to which the techniques of Section 2
will be applied. Since we want to make use of Lemma 2, this structure must be
a tree (or at least a VTDAG). And of course we cannot expect $Chase(D,{\cal
T})$ to be a VTDAG.

######  Definition 12.

By ${\cal S}(D,{\cal T})$ (or just ${\cal S}$, as the context is always clear)
we mean the substructure of $Chase(D,{\cal T})$ consisting of all the elements
of $Chase(D,{\cal T})$, all the atoms in $D$ and all the atoms of the TGPs. We
understand that ${\cal S}$ is a structure over the signature $\Sigma$.

We will call the atoms in ${\cal S}$ skeleton atoms, as we imagine ${\cal S}$
as a sort of a skeleton of $Chase(D,{\cal T})$. The atoms of $Chase(D,{\cal
T})$ which are not in ${\cal S}$ will be called flesh atoms. So the flesh
atoms are the ones created in the process of chase by the datalog rules.

It follows easily from ($\spadesuit$ 5.) that:

######  Lemma 3.

  1. (i)

The graph ${\cal S}_{non}$ is acyclic;

  2. (ii)

the in-degree of any element of ${\cal S}_{non}$ is 1;

  3. (iii)

${\cal S}_{non}$ is a forest;

  4. (iv)

the degree of the elements of ${\cal S}_{non}$ is bounded by $|\Sigma|+1$;

Remember that all the elements of $D$ are constants from $\Sigma$, so they are
not in ${\cal C}_{non}$.

###### Proof.

For the proof of (i) and (ii) notice that the only way a TGP atom $R(a,b)$ can
be created is to be created together with a new element $b$. Acyclicity
follows from the fact that $b$ is always a "younger" element of $Chase(D,{\cal
T})$ than $a$. The claim (iii) follows from (i) and (ii). Finally, (iv)
follows from the fact, that the chase we consider is a non-oblivious one, so
for any fixed $a\in{\cal S}$ and for any TGP $R$ from $\Sigma$ at most one
$b\in{\cal S}$ can exist such that ${\cal S}\models R(a,b)$. $\Box$

Let us now think of ${\cal S}$ as of a new database instance:

######  Lemma 4.

$Chase(D,{\cal T})\models Chase({\cal S},{\cal T})$. In particular,
$\operatorname{Dom}(Chase({\cal S},{\cal T}))=\operatorname{Dom}(Chase(D,{\cal
T}))=\operatorname{Dom}({\cal S})$

Proof:

It is an easy lemma. It is enough to show, by induction, that for each natural
$n$:

###### ($\spadesuit$ 6

) $Chase(D,{\cal T})\models Chase^{n}({\cal S},{\cal T})$.

Clearly, $Chase(D,{\cal T})\models Chase^{0}({\cal S},{\cal T})$, by our
definition of ${\cal S}$. Suppose that ($\spadesuit$ 6.) is true for some
$n\in\mathbb{N}$, and

###### ($\spadesuit$ 7

) let $R(b,b^{\prime})$ be an atom which is not true in $Chase^{n}({\cal
S},{\cal T})$

but true in $Chase^{n+1}({\cal S},{\cal T})$. In order to prove that this
implies $Chase(D,{\cal T})\models R(b,b^{\prime})$ notice that one of the
following two possibilities must hold:

###### ($\spadesuit$ 8

) there is a datalog rule of the form $\Psi(\bar{x},y,z)\Rightarrow R(y,z)$ in
$\cal T$ and $Chase^{n}({\cal S},{\cal T})\models\Psi(\bar{a},b,b^{\prime})$
for some elements $\bar{a},b,b^{\prime}$, or

###### ($\spadesuit$ 9

) there is TGD of the form $\Psi(\bar{x},y)\Rightarrow\exists z\;R(y,z)$ in
$\cal T$ and $Chase^{n}({\cal S},{\cal T})\models\Psi(\bar{a},b)$ for some
elements $\bar{a},b$.

In both cases it follows from the inductive assumption that $Chase(D,{\cal
T})\models\Psi(\bar{a},b,b^{\prime})$ (resp. $\Psi(\bar{a},b)$). Now, if
($\spadesuit$ 8.) then $Chase(D,{\cal T})\models R(b,b^{\prime})$ follows
simply from the fact that all the rules of $\cal T$ are satisfied in
$Chase(D,{\cal T})$. Similarly, if ($\spadesuit$ 9.) then there exists
$b^{\prime}$ such that $Chase(D,{\cal T})\models R(b,b^{\prime})$. By the
definition of ${\cal S}$, we have that ${\cal S}\models R(b,b^{\prime})$, so
also $Chase^{n}({\cal S},{\cal T})\models R(b,b^{\prime})$, which contradicts
($\spadesuit$ 7.) $\Box$

It is very easy to see that also $Chase({\cal S},{\cal T})\models
Chase(D,{\cal T})$, so we get that $Chase(D,{\cal T})=Chase({\cal S},{\cal
T})$.

The idea behind the Lemma is that while ${\cal S}$ is a simple structure –
simple enough to be ptp-conservative – still not only it contains all elements
of $Chase(D,{\cal T})$ but also the complete information about the relations
between elements of $Chase(D,{\cal T})$ that need a witness and the needed
witnesses. Thanks to that $Chase(D,{\cal T})$ can be rebuilt, starting from
the skeleton ${\cal S}$, in a process of a (non-oblivious) chase that only
triggers datalog rules, but never the existential TGDs. Notice that this would
no longer be true if a single atom $R(a,a^{\prime})$ was removed from ${\cal
S}$ (even if the elements $a$,$a^{\prime}$ were kept, as arguments of some
other atoms). This is because at some point a TGD with the head $\exists
x\;R(a,x)$ would be triggered, and a new element $a^{\prime\prime}$ would be
created.

###  3.3 Proof of Theorem 2

Recall that for a BDD theory $\cal T$ and query $\Psi$ by $\Psi^{\prime}$ we
mean the positive first order rewriting of $\Psi$, which means that
$\Psi^{\prime}$ is such a query (a union of conjunctive queries), that for
each database instance $D$ it holds that $Chase(D,{\cal
T})\models\Psi\;\Leftrightarrow\;D\models\Psi^{\prime}$.

Let $\kappa=\max\\{|Var(\Psi^{\prime})|:\Psi\Rightarrow\psi$ is a rule in
${\cal T}\\}$. In other words, $\kappa$ is the maximal number of variables in
a query being a positive first order rewriting of a body of some rule of the
theory $\cal T$. By Lemma 2 there exists a coloring $\bar{\cal S}$ of ${\cal
S}$ and $\eta\in\mathbb{N}$ such that $\bar{\cal S}$ is $\eta$-ptp
conservative up to the size $\kappa$, which means that the elements of
$M^{\bar{\Sigma}}_{\eta}(\bar{\cal S})$ have the same positive $\kappa$-types
over $\Sigma$ as their counter-images in ${\cal S}$.

Now there are five structures one should imagine:

  * (i)

${\cal S}$

  * (ii)

Chase$(D,{\cal T})$ = $Chase({\cal S},{\cal T})$

  * (iii)

$M_{\eta}^{\bar{\Sigma}}(\bar{\cal S})$

  * (iv)

Chase$(M_{\eta}^{\bar{\Sigma}}(\bar{\cal S}),{\cal T})$

  * (v)

$q_{\eta}($Chase$(D,{\cal T}))$

The first two of them were already introduced in this Section. The third is
the result of the quotient operation applied to $\bar{\cal S}$ – something we
discussed in Section 2. Since $\bar{\cal S}$ is $\eta$-ptp conservative up to
the size $\kappa$, we know that $M_{\eta}^{\bar{\Sigma}}(\bar{\cal S})$ is a
model for all existential TGDs in $\cal T$ (see Remark 4). But, as we saw in
Example 7, we cannot be sure that $M_{\eta}^{\bar{\Sigma}}(\bar{\cal
S})\models{\cal T}$, as some datalog rules from $\cal T$ may be false in
$M_{\eta}^{\bar{\Sigma}}(\bar{\cal S})$. So to get a model of $\cal T$ we
apply chase to $M_{\eta}^{\bar{\Sigma}}(\bar{\cal S})$, which leads to our
fourth structure, Chase$(M_{\eta}^{\bar{\Sigma}}(\bar{\cal S}),{\cal T})$. So
far we know nothing about this structure, in particular we do not even know
whether Chase$(M_{\eta}^{\bar{\Sigma}}(\bar{\cal S}),{\cal T})$ is finite.

The fifth structure, $q_{\eta}($Chase$(D,{\cal T}))$ is only needed in example
8 which we hope explains some issues concerning
Chase$(M_{\eta}^{\bar{\Sigma}}(\bar{\cal S}),{\cal T})$. If you feel you not
need more explanations go directly to Lemma 5. $q_{\eta}($Chase$(D,{\cal T}))$
is defined as:

  * •

$\operatorname{Dom}(q_{\eta}($Chase$(D,{\cal
T})))=\operatorname{Dom}(M_{\eta}^{\bar{\Sigma}}(\bar{\cal S}))$;

  * •

relations are defined in $q_{\eta}($Chase$(D,{\cal T}))$ as the minimal
relations such that $q_{\eta}$, understood as a mapping from Chase$(D,{\cal
T})$ to $q_{\eta}($Chase$(D,{\cal T}))$, is a homomorphism.

So while the relations $M_{\eta}^{\bar{\Sigma}}(\bar{\cal S})$ are defined as
projections of the skeleton relations, the relations $q_{\eta}($Chase$(D,{\cal
T}))$ are projections of both, the skeleton and the flesh atoms.

One can see that Chase$(M_{\eta}^{\bar{\Sigma}}(\bar{\cal S}),{\cal T})\models
q_{\eta}($Chase$(D,{\cal T}))$. Indeed, any atom in $q_{\eta}($Chase$(D,{\cal
T}))$ which is not in $M_{\eta}^{\bar{\Sigma}}(\bar{\cal S})$ is a projection
of some flesh atom in Chase$(D,{\cal T})$. This last atom must have been
proved by some derivation in Chase$(D,{\cal T})$. But a projection of a valid
derivation from Chase$(D,{\cal T})$ is a valid derivation in
Chase$(M_{\eta}^{\bar{\Sigma}}(\bar{\cal S}),{\cal T})$.

At this point it would be reasonable to conjecture that maybe
$q_{\eta}($Chase$(D,{\cal T}))=$ Chase$(M_{\eta}^{\bar{\Sigma}}(\bar{\cal
S}),{\cal T})$. But this is not always the case, as the following example
shows:

######  Example 8.

Let $\cal T$ and $D$ be like in Example 7. Let ${\cal C}=Chase({\cal T},D)$.
Now ${\cal S}$ is the structure ${\cal C}$ from Example 4. Let $m$ be the
number of colors, $n>m$ and let $\bar{\cal S}$ be a coloring of ${\cal S}$,
like in Example 4. Now, the only $R$ atoms in
$q_{n}(M_{n}^{\bar{\Sigma}}(\bar{\cal S}))$ are atoms of the form $R(a,a)$ for
some $a\in M_{n}^{\bar{\Sigma}}$. But it is easy to see that
Chase$(M_{n}^{\bar{\Sigma}},T)\models R(b_{n-1},b_{n+m})$ (where $b_{n-1}$,
$b_{n+m}$ are again like in Example 4).

In the last example an atom was derived in
Chase$(M_{\eta}^{\bar{\Sigma}}(\bar{\cal S}),$ ${\cal T})$, which was not a
projection of any flesh atom. The meaning of the next lemma is that while, in
the process on chase on $M_{\eta}^{\bar{\Sigma}}(\bar{\cal S})$, some datalog
derivations can arise not being projections of datalog derivations in chase on
${\cal S}$, still (like in Lemma 4) no existential TGDs will be used, and no
new elements will be created. To be more precise:

######  Lemma 5.

$\operatorname{Dom}($Chase$(M_{\eta}(\bar{\cal S}),{\cal
T}))=\operatorname{Dom}(M_{\eta}(\bar{\cal S}))$

This proof is not very long but we believe it is quite tricky. It is here
where things really happen: Lemma 2 meets the assumption that $\cal T$ is BDD.

Proof of Lemma 5:

Suppose $\operatorname{Dom}(Chase(M_{\eta}(\bar{\cal S}),{\cal
T}))\not\subseteq\operatorname{Dom}(M_{\eta}(\bar{\cal S}))$

and let $j$ be the smallest natural number such that

$\operatorname{Dom}(Chase^{j+1}(M_{\eta}(\bar{\cal S}),{\cal
T}))\not\subseteq\operatorname{Dom}(M_{\eta}(\bar{\cal S}))$.

This means that there is a rule $\Psi(\bar{x},y)\Rightarrow\exists z\;R(y,z)$
in $\cal T$ and elements $\bar{a},b$ of $Chase^{j}(M_{\eta}(\bar{\cal
S}),{\cal T})$ such that

$Chase^{j}(M_{\eta}(\bar{\cal S}),{\cal T})\models\Psi(\bar{a},b)$, but

###### ($\spadesuit$ 10

) $Chase^{j}(M_{\eta}(\bar{\cal S}),{\cal T})\not\models\exists z\;R(b,z)$.

But if $Chase^{j}(M_{\eta}(\bar{\cal S}),{\cal T})\models\Psi(\bar{a},b)$ then
of course also
$Chase(M_{\eta}(\bar{\cal S}),{\cal T})\models\Psi(\bar{a},b)$. Since all of
$\bar{a}$ and $b$ are elements of $M_{\eta}(\bar{\cal S})$ we get (using the
fact that $\Psi^{\prime}$ is the positive first order rewriting of $\Psi$)
that $M_{\eta}(\bar{\cal S})\models\Psi^{\prime}(\bar{a},b)$ or, in other
words, $M_{\eta}(\bar{\cal S})\models\Psi^{\prime}(\bar{x},b)$. Let $c$ be any
such element of ${\cal S}$ that $q_{\kappa}(c)=b$. Since the size of
$\Psi^{\prime}$ is at most $\kappa$, by Lemma 2 we get that ${\cal
S}\models\Psi^{\prime}(\bar{x},c)$. Using again the fact that $\Psi^{\prime}$
is the positive first order rewriting of $\Psi$ we get that $Chase({\cal
S},{\cal T})\models\Psi(\bar{x},c)$.

$Chase({\cal S},{\cal T})$ is of course a model of $\cal T$, so there must be
an element $d$ such that $Chase({\cal S},{\cal T})\models R(c,d)$. It follows
from Lemma 4 that $d\in{\cal S}$ and, in consequence, $e=q_{\eta}(d)\in
M_{\eta}(\bar{\cal S})$. But this implies that $M_{\eta}(\bar{\cal S})\models
R(b,d)$ which contradicts ($\spadesuit$ 10.). $\Box$

As we show in Section 5.4, there is no hope to have anything similar to Lemma
5 in the general (non-binary) case.

We are ready to present the proof of Theorem 2:

In order to prove Theorem 2 (and, in consequence, Theorem 1) we need to show a
finite model of $D$ and $\cal T$ without any atom of the predicate symbol $F$.
The structure $Chase(M_{\eta}(\bar{\cal S}),{\cal T})$ is clearly a model of
$D,\cal T$. It follows from the Lemma 5 that its domain is exactly the domain
of $M_{\eta}(\bar{\cal S})$, so it is finite.

Since no atom of the relation $F$ occurs in ${\cal S}$ there is also no such
atom in $M_{\eta}(\bar{\cal S})$. So the only way any such atom could appear
in $Chase(M_{\eta}(\bar{\cal S}),{\cal T})$ would be to derive it in the
process of chase. But the only rule that derives $F$ is a existential TGD
which demands a new element, and no such rule could have been used, due to
Lemma 5. $\Box$

##  4 Proof of the Main Lemma

Fix a VTDAG ${\cal C}$ and a natural number $m$. Let $\Sigma$ be the signature
of ${\cal C}$. To prove Lemma 2 we need to find $n\in\mathbb{N}$ and a
coloring $\bar{\cal C}$ of ${\cal C}$ such that $\bar{\cal C}$ is
$n$-conservative up to the size $m$.

First let us define the coloring:

######  Definition 13.

For $e\in{\cal C}$ let ${\cal P}(e)$ be like in Definition 10.

  * •

For $e\in{\cal C}_{non}$ let ${\cal P}_{0}(e)={\cal P}(e)$.

  * •

For $e\in{\cal C}_{non}$ let ${\cal P}_{k}(e)=\bigcup_{a\in{\cal
P}_{k-1}(e)}P(a)$

######  Definition 14.

A coloring $\bar{\cal C}$ of ${\cal C}$ will be called natural if it satisfies
the following conditions:

  * •

if $e,e^{\prime}\in{\cal C}$ are such that $e^{\prime}\in{\cal P}_{m}(e)$ and
if
$\bar{\cal C}\models K^{l}_{h}(e),K^{l^{\prime}}_{h^{\prime}}(e^{\prime})$
then $h\neq h^{\prime}$;

  * •

if $e,e^{\prime}\in{\cal C}$ are such that $\bar{\cal C}\models
K^{l}_{h}(e),K^{l}_{h^{\prime}}(e^{\prime})$ then
${\cal C}\upharpoonright({\cal P}(e)\cup{\cal C}_{con})$ and ${\cal
C}\upharpoonright({\cal P}(e^{\prime})\cup{\cal C}_{con})$ are isomorphic.

It is easy to see that for each VTDAG ${\cal C}$ there exists a natural
coloring $\bar{\cal C}$. From now on by $\bar{\cal C}$ we will mean a fixed
natural coloring of ${\cal C}$.

By Remark 2 the proof of Lemma 2 will be finished when we show:

######  Lemma 6.

For each query $\Phi(\bar{x},y)$ over $\Sigma$, with $|\bar{x}|<m$, there
exists $n\in\mathbb{N}$ such that for each element $e\in{\cal C}$:

$M_{n}(\bar{\cal C})\models\exists\bar{x}\Phi(\bar{x},q_{n}(e))$ if and only
if ${\cal C}\models\exists\bar{x}\Phi(\bar{x},e)$

Proof of Lemma 6 begins here.

It will take till the end of Section 4 to finish.

First of all notice that if the Lemma 6 was false, then there would exists a
counterexample – a conjunctive query $\Phi(\bar{x},y)$ such that:

($\clubsuit$) for each $n\in\mathbb{N}$ there exists an element $e_{n}^{\Phi}$
of ${\cal C}$ and a valuation $\sigma_{n}^{\Phi}:Var(\Phi)\rightarrow
M_{n}(\bar{\cal C})$, with $\sigma_{n}^{\Phi}(y)=q_{n}(e_{n}^{\Phi})$, such
that $M_{n}(\bar{\cal C})\models\sigma_{n}^{\Phi}(\Phi)$ and ${\cal
C}\not\models\exists\bar{x}\Phi(\bar{x},e_{n}^{\Phi})$.

Each time we will say that query $\Phi$ is a counterexample we will think that
is satisfies condition ($\clubsuit$).

By a colors statement we will mean a query of the form:

$\bigwedge_{z\in Var(\Phi)}K_{h_{z}}^{l_{z}}$

where $K_{h_{z}}^{l_{z}}$ is any of the possible colors from $\cal K$. By a
color closure of $\Phi$ we will mean any query of the form
$\Phi\wedge\Upsilon$, where $\Upsilon$ is a colors statement. Of course there
are finitely many colors statements, and so there are finitely many possible
color closures of $\Phi$. A query which is a color closure of some other query
will be called color closed.

######  Lemma 7.

  * (i)

Let $\Phi$ be a counterexample. Then for each $n$ there is a query $\Phi_{c}$,
being a color closure of $\Phi$, such that $M_{n}(\bar{\cal
C})\models\sigma_{n}^{\Phi}(\Phi_{c})$ and $\bar{\cal
C}\not\models\exists\bar{x}\Phi_{c}(\bar{x},e_{n}^{\Phi})$.

  * (ii)

For each counterexample $\Phi$ there exists a color closure $\bar{\Phi}$ of
$\Phi$, which also is a counterexample.

  * (iii)

If there exists a query $\Phi$ being a color closed counter-example, then
there also exists another color closed counterexample $\Psi$ such that for
each constant $c$ from $\Sigma$, for each variable $z\in Var(\Psi)$ and for
each $n\in\mathbb{N}$ there is $\sigma^{\Psi}_{n}(z)\neq c$, where
$\sigma_{n}^{\Psi}$ is as $(\clubsuit)$. We will say that counterexample
$\Psi$ avoids constants.

###### Proof.

(i) The elements $\sigma_{n}^{\Phi}(z)$, where $z\in Var(\Phi)$ have some
colors. Adding to $\Phi$ a statement asserting that they have the colors they
really have will not make the new query $\sigma_{n}(\Phi_{C})$ less true in
$M_{n}(\bar{\cal C})$ than $\sigma_{n}^{\Phi}(\Phi)$ was.

On the other hand, $\exists\bar{x}\Phi(\bar{x},e_{n})$ was false in ${\cal C}$
already before the color statement was added and adding more constraints never
makes a query more true.

(ii) Use (i) and an argument like in Remark 2.

(iii) Suppose $\Phi$ is a color closed counterexample and
$\sigma^{\Phi}_{n}(z)$ $=c$ for some constant $c\in\Sigma$, some variable
$z\in Var(\Psi)$ and some $n\in\mathbb{N}$. By the definition of natural
coloring, the color of $c$ is unique in ${\cal C}_{con}$ and thus the equality
$\sigma^{\Phi}_{n}(z)=c$ must hold for each $n$, and thus $\Psi$ being the
result of replacing each occurrence of $z$ in $\Phi$ by $c$ is also a
counterexample. $\Box$

We are now going to view queries as graphs. What we mean here is a sort of
Gaifman graphs, where vertices are the variables in the query and the edges
are the atoms of the query. As we only have binary and unary atoms, we can in
a natural way see each query as a directed (labeled) graph. Concerning the
constants in the query, they are not understood to be vertices in the graph,
and it is good to think that an atom of the form $R(a,x)$ in a query, where
$a$ is a constant and $x$ is a variable, is just a unary predicate, telling us
something about $x$ alone. Notice that atoms of the form $R(a,b)$ in a query,
where both $a$ and $b$ are constants, are irrelevant from the point of view of
Lemma 6, as the part of ${\cal C}$ consisting of the constants remains
unchanged after our projections.

Now our plan of the proof of Lemma 6 is as follows. We want to show that no
query is an avoiding constants color closed counterexample. So first we will
notice (Lemma 8 and Lemma 9) that neither a query being an undirected tree,
nor a query containing a directed cycle can ever be a counterexample. At this
point we will know that if there is any avoiding constants color closed
counterexample $\Phi$ then $\Phi$ must contain an undirected cycle (but not a
directed one). But then, in Lemma 10 we show that if such a $\Phi$ existed,
then also another counterexample would exist, being a tree or containing a
directed cycle. That would however contradict Lemma 8 and Lemma 9.

Proofs of Lemma 8 and Lemma 9 are easy. Proof of Lemma 10, where we deal with
queries containing an undirected cycle, is much more complicated. A technique
of normalization of queries is used there, which we find to be the deepest
idea of this paper (we also employ this technique, in different context, in
[6], where it is called second little trick). Why are the undirected cycles in
the query so much harder to deal with than directed ones? The answer is in:

######  Example 9.

Let a theory $\cal T$ consist of the rules:

$F(x,y)\Rightarrow\exists z\;F(y,z)$ $F(x,y)\Rightarrow\exists z\;G(y,z)$

$G(x,y)\Rightarrow\exists z\;F(y,z)$ $G(x,y)\Rightarrow\exists z\;G(y,z)$

Let $D=\\{F(a,b)\\}$ and let ${\cal C}$ be $Chase(D,{\cal T})$, which means
that ${\cal C}$ is an infinite tree, where each element has exactly two
successors. Or, in other words, ${\cal C}$ consists, except from $a$ and $b$,
of all the elements $w(b)$, where $w\in\\{f,g\\}^{*}$. Let $\bar{\cal C}$ be a
natural coloring of ${\cal C}$.

Let $e_{1},e_{2}$ be two elements of ${\cal C}$ of the form $e_{1}=vfw(b)$,
$e_{2}=vgw(b)$, where $v,w\in\\{f,g\\}^{*}$ and where $|v|=n-1$.

Then $a_{1}=q_{n}(e_{1})\neq q_{n}(e_{2})=a_{2}$ are two distinct elements of
$M_{n}(\bar{\cal C})$ – the length of $v$ is not big enough to hide the slight
difference in the positive types of $e_{1}$ and $e_{2}$. Of course also
$a_{3}=q_{n}(f(e_{1}))\neq q_{n}(g(e_{1}))=a_{4}$ are two distinct elements
(each of them distinct than $a_{1}$ and $a_{2}$). But $a_{3}=q_{n}(f(e_{2}))$
and $a_{4}=q_{n}(g(e_{2}))$. This means that the atoms
$F(a_{1},a_{3}),F(a_{2},a_{3}),G(a_{2},a_{4}),G(a_{1},a_{4})$ are all true in
$M_{n}(\bar{\cal C})$, and so there is an undirected cycle in $M_{n}(\bar{\cal
C})$ consisting of 4 distinct elements.

As we saw in Example 4, by using coloring we can easily make sure that there
are no small directed cycles in $M_{n}({\bar{\cal C}})$. But we cannot rule
out small undirected new (not present in $\bar{\cal C}$) cycles in
$M_{n}({\bar{\cal C}})$. So we need to prove that, while the new cycles exist,
no small query can actually notice them.

######  Lemma 8.

Let $n\geq m$. Then for each element $e\in{\cal C}$ and each query
$\Psi(\bar{x},y)$, which is an undirected tree:
$\Psi\in ptp_{m}({\bar{\cal C}},e,\bar{\Sigma})$ if and only if $\Psi\in
ptp_{m}(M_{n}({\bar{\cal C}}),q_{n}(e),\bar{\Sigma})$.

It of course follows from the lemma that no query being an undirected tree can
be a counterexample.

######  Lemma 9.

Let $n\geq m$. Suppose $\Phi$ is a query containing a directed cycle, by which
we mean a sub-query of the form:
$R_{1}(x_{1},x_{2}),R_{2}(x_{2},x_{3}),\ldots
R_{k-1}(x_{k-1},x_{k}),R_{k}(x_{k},x_{1})$
where $k<m$ and $R_{i}$ are relation symbols from $\Sigma$. Then
$M_{n}({\bar{\cal C}})\not\models\Phi$.

Clearly, as being a counterexample means, among other conditions, being true
in $M_{n}(\bar{\cal C})$, the lemma implies that $\Phi$, containing a directed
cycle, never is a counterexample.

Proof of Lemma 8:

Call a query bad, if it is a counterexample555This is because the word
”counterexample” is already being used in another context, and we want to
avoid confusion to Lemma 8.

Suppose there exist bad queries and consider the smallest (with respect to the
number of variables) of them. Call this query $\Psi$.

First notice that $y$ occurs only in one binary atom in $\Psi$. Otherwise
(since $\Psi$ is a tree) $\Psi$ could be seen as a conjunction of smaller
queries sharing only the variable $y$, and one of those queries would need to
be a smaller bad query.

This means that the query $\Psi$ is either $(i)$ of the form $Q(x,y)$, where
$Q(x,y)=R(x,y)\wedge\tau(x)\wedge\tau^{\prime}(y)$ or
$Q(x,y)=R(y,x)\wedge\tau(x)\wedge\tau^{\prime}(y)$ for some relation symbol
$R$ and unary queries $\tau$,$\tau^{\prime}$, or $(ii)$ of the form
$Q(y,x_{1})\wedge\Psi_{0}(x_{1},\bar{z})$, where $Q$ is as above and $\bar{z}$
contains all the variables in $\bar{x}$ except from $x_{1}$. Notice that
$\Psi_{0}$ is smaller than $\Psi$.

The case $(i)$ is of course very easy. Remember that only elements of
$\bar{\cal C}$ the same unary type can be identified by our quotient
operations. So if $M_{n}(\bar{\cal C})\models Q(x,q_{n}(e))$ then there must
exist $d^{\prime},e^{\prime}\in{\cal C}$, such that ${\cal C}\models
Q(d^{\prime},e^{\prime})$ and $e\equiv_{n}e^{\prime}$. But that implies, by
definition of the relation $\equiv_{n}$, that there exists $d\in{\cal C}$ such
that ${\cal C}\models Q(d,e)$.

For the case (ii) suppose that $M_{n}(\bar{\cal C})\models
Q(q_{n}(e),x_{1})\wedge\Psi_{0}(x_{1},\bar{z})$, and let
$\sigma:\bar{x}\rightarrow M_{n}$ be the satisfying valuation.

$M_{n}(\bar{\cal C})\models Q(q_{n}(e),\sigma_{n}(x_{1}))$ means that there
exist elements $e^{\prime},d^{\prime}\in{\cal C}$ such that
$e\equiv_{n}e^{\prime}$, $q_{n}(d^{\prime})=\sigma(x_{1})$ and ${\cal
C}\models Q(e^{\prime},d^{\prime})$.

Notice that $M_{n}(\bar{\cal C})\models\Psi_{0}(q_{n}(d^{\prime}),\bar{z})$.
Since $\Psi_{0}$ is smaller than $\Psi$ it cannot be bad. So we get that
$\bar{\cal C}\models\Psi_{0}(d^{\prime},\bar{z})$. But that implies that
$\bar{\cal C}\models\Psi(e^{\prime},\bar{x})$. Now, since
$e\equiv_{n}e^{\prime}$ and $m\leq n$, we get $\bar{\cal
C}\models\Psi(e,\bar{x})$, but this contradicts the assumption that query
$\Psi$ was bad. $\Box$

Proof of Lemma 9:

Suppose $\Phi$ is like in the Lemma and $M_{n}({\bar{\cal C}})\models\Phi$.
This means that there exist elements $b_{1},a_{2}$, $b_{2},a_{3}\ldots
b_{k},a_{1}$ of $\bar{\cal C}$ such that $a_{i}\equiv_{n}b_{i}$ and $\bar{\cal
C}\models R_{i}(b_{i},a_{i+1})$ for each $i$. Let $c_{1}=b_{1}$. Suppose
$c_{i}$ is already defined, and $c_{i}\equiv_{n-i+1}b_{i}$. There exists a
non-constant element of $\bar{\cal C}$, namely $a_{i+1}$ such that $\bar{\cal
C}\models R_{i}(b_{i},a_{i+1})$. Since $c_{i}\equiv_{n-i+1}b_{i}$ and
$n-i+1>0$, there exists (a unique) element $c_{i+1}\in\bar{\cal C}$ such that
$R_{i}(c_{i},c_{i+1})$. By Lemma 12 we get that $c_{i+1}\equiv_{n-i}b_{i+1}$.

But that means that $c_{k}\equiv_{1}b_{k}$, which implies that there must be
an element $d\in\bar{\cal C}$ such that $\bar{\cal C}\models R_{k}(c_{k},d)$,
where the color of $d$ is the same as the color of $c_{1}$, so
$c_{1},c_{2},\ldots d$ form a directed path in $\bar{\cal C}$, of length not
greater than $m$, joining two elements of the same color. This contradicts the
definition of natural coloring. $\Box$

Now, Lemma 6 follows from Lemma 7, Lemma 8, Lemma 9 and from the following:

######  Lemma 10.

If there exists a color closed counterexample $\Phi$ which avoids constants
and which contains an undirected cycle then there exists also a counterexample
being a tree or a counterexample containing a directed cycle.

###  4.1 Proof of Lemma 10

Consider a query $\Psi(\bar{x},y)$ which contains an undirected cycle, which
is not a directed cycle. Then $\Psi$ must be of the form:

($\heartsuit$) $R_{1}(z^{\prime},z)\wedge
R_{2}(z^{\prime\prime},z)\wedge\psi(\bar{x},y)$

for some relations $R_{1},R_{2}\in\Sigma$ and some
$z,z^{\prime},z^{\prime\prime}$$\in Var(\Psi)$.

######  Lemma 11 (Normalization of queries).

If any color closed, avoiding constants, query $\Psi(\bar{x},y)$ of the form
$(\heartsuit)$ is a counterexample, then there is a binary relation
$P\in\Sigma$ such that one of the following queries is also a color closed,
avoiding constants, counterexample:

  * •

$\psi(\bar{x},y)\wedge R_{1}(z^{\prime},z)\wedge z^{\prime}=z^{\prime\prime}$

  * •

$\psi(\bar{x},y)\wedge R_{1}(z^{\prime},z)\wedge
P(z^{\prime\prime},z^{\prime})$

  * •

$\psi(\bar{x},y)\wedge R_{2}(z^{\prime\prime},z)\wedge
P(z^{\prime},z^{\prime\prime})$

To see how Lemma 11 implies Lemma 10, while $\Psi$ is a counterexample of the
form ($\heartsuit$) do replace it with another counterexample, the one whose
existence is assured by Lemma 11. The only way to leave the while-loop is to
produce a counterexample which is a tree or contains a directed cycle. So it
is enough to prove that the while-loop indeed terminates.

If the first possibility from the Lemma is used as the replacement, then the
new query has less variables than the old one (since adding an equivalence of
variables is the same as unifying the variables). But the last two
possibilities do not decrease the number of variables. So aren’t they going to
be applied forever? Consider the following measure of the size of a query:

Measure($\Phi$)= $\Sigma_{x\in Var(\Psi)}\;occ(x)smaller(x)$

where $occ(x)$ is the number of the occurrences of variable $x$ in $\Psi$ and
$smaller(x)$ is the number of variables from which $x$ is reachable by a
directed path in the graph of the query. It is easy to see that
Measure($\Psi)$ is a natural number which decreases each time Lemma 11 is
applied.

Before we prove Lemma 11 notice that the first condition in Definition 11
implies:

######  Lemma 12.

Suppose $a,b,c,d$ are non-constant elements of $\bar{\cal C}$, such that
$\bar{\cal C}\models R(a,b),R(c,d)$ for some relation $R\in\Sigma$. Then
$b\equiv_{n}d$ implies $a\equiv_{n-1}c$.

###### Proof.

Suppose there was a query $\psi(\bar{x},y)$, with $|\bar{x}|<n-1$, such that
$\bar{\cal C}\models\exists\bar{x}\psi(\bar{x},a)$ but $\bar{\cal
C}\not\models\exists\bar{x}\psi(\bar{x},c)$. Then $\bar{\cal
C}\models\exists\bar{x}x^{\prime}\psi(\bar{x},x^{\prime})\wedge
R(x^{\prime},b)$ but $\bar{\cal C}\not\models\psi(\bar{x},x^{\prime})\wedge
R(x^{\prime},d)$. But this would mean that $b\not\equiv_{n}d$. Notice that the
assumption that ${\cal C}$ is a VTDAG was used here. $\Box$

Proof of Lemma 11 Suppose $\Psi$ is a color closed counterexample of the form
($\heartsuit$). Consider the color of $z$ (call it color($z$)). More
precisely, color($z$) is the color that is enforced by $\Psi$ on any valuation
of $z$ that satisfies $\Psi$ . What we are interested in is not really the
full information about color($z$), but its lightness – the information about
the isomorphic type of ${\cal P}(e)$ for any $e\in\bar{\cal C}$ having the
color that $\Psi$ enforces on $z$.

Now please be ready for the most complicated argument of this paper. Let $e$
be like in the previous paragraph. The set ${\cal P}(e)$ contains some
elements $e^{\prime}$ and $e^{\prime\prime}$ such that
$R_{1}(e^{\prime},e)\wedge R_{2}(e^{\prime\prime},e)$ are true in $\bar{\cal
C}$. It follows from Definition 11 that in such case there must be an atom
$Q(e^{\prime},e^{\prime\prime})$ true in $\bar{\cal C}$, where
$Q(e^{\prime},e^{\prime\prime})$ is either $P(e^{\prime},e^{\prime\prime})$ or
$P(e^{\prime\prime},e^{\prime})$ for some relation $P\in\Sigma$, or
$e^{\prime}=e^{\prime\prime}$ (this happens when $R_{1}=R_{2}$). Notice that
the atom $Q$ only depends on the color of $z$ not on the choice of $e$.
Suppose $Q$ is $P(e^{\prime},e^{\prime\prime})$, the other two possibilities
are analogous. Now, we claim that $\Phi=\psi(\bar{x},y)\wedge
R_{2}(z^{\prime\prime},z)\wedge P(z^{\prime},z^{\prime\prime})$ is also a
counterexample, with $\sigma_{n}^{\Phi}=q_{n}\circ\sigma_{n+1}^{\Psi}$,
$e_{n}^{\Phi}=e_{n+1}^{\Psi}$ and $\sigma_{n}$.

Notice that we use the notation $q_{n}$ here in the sense defined in
($\spadesuit$ 1.): $\sigma_{n+1}^{\Psi}$, for an argument being a variable of
$\Psi$ (or $\Phi$ – they have the same set of variables) returns an element of
$M_{n+1}(\bar{\cal C})$ and $q_{n}$ for an argument from $M_{n+1}(\bar{\cal
C})$ returns an element of $M_{n}(\bar{\cal C})$.

We need to show that the conditions from $(\clubsuit)$ are now satisfied. It
is easy to see that
$\sigma_{n}^{\Phi}(y)=q_{n}\circ\sigma_{n+1}^{\Psi}(y)=q_{n}(e_{n+1}^{\Psi})=q_{n}(e_{n}^{\Phi})$.

What remains to be shown is that for each $n\in\mathbb{N}$:

(*) $M_{n}(\bar{\cal C})\models\sigma_{n}^{\Phi}(\Phi)$ and (**) $\bar{\cal
C}\not\models\exists\bar{x}\Phi(\bar{x},e_{n}^{\Phi})$.

Let us begin with (**), which is easier. Suppose $\bar{\cal
C}\models\Phi(\bar{x},e_{n}^{\Phi})$. So there exists a valuation
$\gamma:Var(\Phi)\rightarrow\bar{\cal C}$, with $\gamma(y)=e_{n}^{\Phi}$, such
that $\bar{\cal C}\models\gamma(\Phi)$. Notice that
$\gamma(y)=e_{n+1}^{\Psi}$. We claim that $\bar{\cal C}\models\gamma(\Psi)$
and this will be in contradiction with what we assumed about $\Psi$ and
$e_{n+1}^{\Psi}$.

For the proof of the last claim it is enough to show that $\bar{\cal C}\models
R_{1}(\gamma(z^{\prime}),\gamma(z))$, as this is the only atom of $\Psi$
missing in $\Phi$. But this follows from what we know about the isomorphic
type of $\gamma(z)$, from the fact that $\bar{\cal C}\models
P(\gamma(z^{\prime}),\gamma(z^{\prime\prime}))\wedge
R_{2}(\gamma(z^{\prime\prime}),\gamma(z))$ and from the assumption that the
in-degree of each of the relations in $\bar{\cal C}$ is at most 1 (first
condition in Definition 11).

Now we are going to prove (*). We know that $M_{n+1}(\bar{\cal
C})\models\sigma_{n+1}^{\Psi}(\Psi)$, so also $M_{n}(\bar{\cal C})\models
q_{n}\circ\sigma_{n+1}^{\Psi}(\Psi)$. What remains to be proved is that

(*) $M_{n}(\bar{\cal C})\models
P(q_{n}\sigma_{n+1}^{\Psi}(z^{\prime}),q_{n}\sigma_{n+1}^{\Psi}(z^{\prime\prime})).$

We know that $M_{n}(\bar{\cal C})\models
R_{1}(\sigma_{n+1}^{\Psi}(z^{\prime}),\sigma_{n+1}^{\Psi}(z))$ and that
$M_{n}(\bar{\cal C})\models
R_{2}(\sigma_{n+1}^{\Psi}(z^{\prime\prime}),\sigma_{n+1}^{\Psi}(z))$. This
means that there are elements $a^{\prime},a,b^{\prime\prime},b$ of $\bar{\cal
C}$ such that: $q_{n+1}(a)=q_{n+1}(b)=\sigma_{n+1}^{\Psi}(z)$,
$q_{n+1}(a^{\prime})=\sigma_{n+1}^{\Psi}(z^{\prime})$,
$q_{n+1}(a^{\prime\prime})=\sigma_{n+1}^{\Psi}(z^{\prime\prime})$ and
$\bar{\cal C}\models R_{1}(a^{\prime},a)\wedge R_{2}(b^{\prime\prime},b)$. The
color of $a$ and of $b$ is the color of $z$, so the isomorphic type of ${\cal
P}(a)$ is the same as the isomorphic type of ${\cal P}(b)$, and the same as
the isomorphic type of ${\cal P}(e)$, where $e$ is as in the beginning of
Lemma 11. This means that there is an element $a^{\prime\prime}\in\bar{\cal
C}$ such that $\bar{\cal C}\models R_{2}(a^{\prime\prime},a)$ and $\bar{\cal
C}\models P(a^{\prime\prime},a^{\prime})$. There is no reason to think that
$a^{\prime\prime}\equiv_{n+1}b^{\prime\prime}$. But from Lemma 12 we get that
$a^{\prime\prime}\equiv_{n}b^{\prime\prime}$. So $a^{\prime\prime}$ and $a$
are two elements of $\bar{\cal C}$ such that $\bar{\cal C}\models
R_{2}(a^{\prime\prime},a)$, that $q_{n}(a)=q_{n}\sigma_{n+1}^{\Psi}(z)$ and
that $q_{n}(a^{\prime\prime})=q_{n}\sigma_{n+1}^{\Psi}(z^{\prime\prime})$.
$\Box$

This ends the proofs of Lemmas 10,11 , 6 and 2.

##  5 Discussion

###  5.1 Beyond the binary case (slightly)

As a careful reader might already have noticed, our proof of Theorem 2 can
also be read as a proof of:

######  Theorem 3.

Let $\cal T$ be a set of existential TGDs and plain datalog rules, with each
of its existential TGDs of the form:
$\Psi(\bar{x},y)\Rightarrow\exists\bar{z}\;\Phi(y,\bar{z})$. Then, if $\cal T$
is BDD, then it is also FC.

It is because in the proof of Theorem 2 we only used the binarity assumption
for heads of existential TGDs.

Notice that we can rewrite existential TGDs from Theorem 3 into conjunction of
existential TGDs with binary heads and some arbitrary datalog rules. Hence the
whole proof of Theorem 2 survives.

Hint: For each TGD $\Psi(\bar{x},y)\Rightarrow\exists\bar{z}\;\Phi(y,\bar{z})$
we add new relational symbols $R^{1}_{\Phi}(y,z_{1})\ldots
R^{n}_{\Phi}(y,z_{n})$ where $n=|\bar{z}|$. We add to the theory rules
$\Psi(\bar{x},y)\Rightarrow\exists\bar{z}\;R^{i}_{\Phi}(y,z_{i})$ and datalog
rules $R^{1}_{\Phi}(y,z_{1})\wedge\ldots\wedge
R^{n}_{\Phi}(y,z_{n})\rightarrow\Phi(y,\bar{z})$.

###  5.2 The ternary case

Usually, once we know that some property holds for binary signatures, it is
easy to prove, by some sort of reduction, that it remains true in the general
case. This rule does not seem to be valid for the BDD/FC conjecture. What we
can however easily show is:

######  Theorem 4.

If the BDD/FC conjecture for ternary signatures is true then it is true in the
general case.

Instead of presenting a detailed proof of the theorem, which would be boring,
let us show an example of how the reduction works. Suppose we have a theory
$\cal T$ with a rule like:

(*) $P(x,y,z,x)\Rightarrow\exists t\;R(x,y,z,t)$

then rewrite it into the following three rules:

$P(x,y,z,x)\Rightarrow\exists w_{1}\;R_{1}(x,y,w_{1})$

$P(x,y,z,x)\wedge R_{1}(x,y,w_{1})\Rightarrow\exists
w_{2}\;R_{2}(w_{1},z,w_{2})$

$P(x,y,z,x)\wedge R_{1}(x,y,r)\wedge R_{2}(r,z,s)\Rightarrow\exists
t\;R^{\prime}(s,t)$

The idea is here that using ternary predicates we can give names to lists of
variables, in the good old Prolog way. We appear to still have non-ternary
predicates in the bodies of the rules. But just don’t think of them as of
predicates any more! The $P$ in the body of (*) is just a view over the real
predicates $P_{1}$, $P_{2}$ and $P^{\prime}$ now, which relate to $P$ in the
same was as $R_{1}$, $R_{2}$ and $R^{\prime}$ relate to $R$.

In this way we constructed a new, ternary theory, call it ${\cal T}^{\prime}$.
What we would now need to show (if it was a real detailed proof) would be that
(i) if $\cal T$ is BDD then ${\cal T}^{\prime}$ also is, and (ii) if ${\cal
T}^{\prime}$ is FC then $\cal T$ also is. To see how (ii) works take a
database instance $D$ and query $Q$. Rewrite $D$ and $Q$ into $D^{\prime}$ and
$Q^{\prime}$ in the new ternary language (possibly adding some new elements to
denote lists of elements of $D$). Of course if $Chase({\cal T},D)\not\models
Q$ then also $Chase(D^{\prime},{\cal T}^{\prime})\not\models Q^{\prime}$. So,
if ${\cal T}^{\prime}$ is FC, there exists a finite ${\cal M}^{\prime}$ being
a model of ${\cal T}^{\prime}$ and $D^{\prime}$ such that ${\cal
M}^{\prime}\not\models Q^{\prime}$. Now, to finish the proof of (i), define
the relations of $\cal M$ as views over respective relations in ${\cal
M}^{\prime}$.

Showing (i) is not really hard either.

###  5.3 Multi-head TGDs

The TGDs we consider in this paper are assumed to be single-head. Of course if
the arity is not restricted, then the validity of the BDD/FC conjecture does
not depend on this assumption, as every multi-head TGD $\Psi$ can be replaced
by a single-head TGD having, as its head, the join of all the atoms in the
head of $\Psi$, and by some datalog rules splitting this join back into
smaller atoms. But such a simple transformation is not possible for binary
signatures. It is actually easy to see that the BDD/FC conjecture for multi-
head TGDs over binary signatures is already equivalent to the full conjecture,
as any ternary Datalog∃ program can be encoded in this format. For example the
rule:

$P_{1}(x,y,z)\wedge P_{2}(x,y,z^{\prime})\Rightarrow\exists w\;P(x,z,w)$

can be encoded as (read $A^{i}(t,x)$ as ”$x$ is the $i$’th argument in the
atom $t$”):

$A_{P_{1}}^{1}(t_{1},x)\wedge A_{P_{1}}^{2}(t_{1},y)\wedge
A_{P_{1}}^{3}(t_{1},z)\wedge$ $A_{P_{2}}^{1}(t_{2},x)\wedge
A_{P_{2}}^{2}(t_{2},y)\wedge A_{P_{2}}^{3}(t_{2},z^{\prime})\Rightarrow$
$\exists t\;A_{P}^{1}(t,x)\wedge A_{P}^{2}(t,y)$

and $A_{P}^{1}(t,x)\wedge A_{P}^{2}(t,y)\Rightarrow\exists w\;A_{P}^{3}(t,w)$.

###  5.4 Why $M_{n}$ are too poor to be models
(in the non-binary case)

The main idea of our proof of Theorem 1 was first to find, for a BDD theory
$\cal T$ and a database instance $D$ the skeleton ${\cal S}$ which is a
substructure of $Chase(D,{\cal T})$ on one hand being simple enough to be ptp-
conservative, but on the other hand not only containing all the elements of
$Chase(D,{\cal T})$, but also sufficient information about the relations
between elements which require a witness and the witnesses. Then the idea was
to prove (Lemma 5) that the finite model $M_{n}$ constructed from this simple
structure by a quotient operation can be saturated, using the datalog rules
from $\cal T$, to a model of $\cal T$, without adding any new elements being
necessary.

The first reason this line of reasoning cannot be used in the general (non-
binary) case is that the distinction between existential TGDs and plain
datalog rules makes then no sense any more: each datalog rule can be turned
into a TGD by adding a new (existentially quantified) dummy variable to the
atom on the right hand side of the query. But what we view as an even more
serious obstacle is that, as the following example shows, it is hard to
imagine how anything analogous to Lemma 5 could be true in the general case:

Let the rules of $\cal T$ be: $R(x,x^{\prime},y,z)\Rightarrow E(y,z)$

and $E(x,y),E(t,y)\Rightarrow\exists z\;R(x,t,y,z)$

and let a database instance $D$ be $\\{E(a,b)\\}$.

Clearly, $\cal T$ is BDD. And ${\cal C}=Chase(D,{\cal T})$ is a very simple
structure: an infinite $E$-chain, with additional atom $R(x,x,y,z)$ for each
three consecutive elements $x$, $y$, $z$ of this chain. But whenever any two
elements of ${\cal C}$ are identified by a quotient operation, a new tuple
satisfying the body of the (only) TGD form $\cal T$ emerges (something we have
already seen in Example 7), and a new witness $z$ is required for this tuple.
Since the new witness is a function of the whole tuple, not just of (the
element substituted for) $y$, the (already existing) element $t$ of
$M_{n}(\bar{\cal C})$ such that $E(y,t)$ cannot be used now, and a new one
must be created. If there was just one element this would be something we
could live with – our main goal is just to keep the structure finite. But
notice that once the new witness $z$, with $E(y,z)$ is created, it enforces a
new infinite $E$-chain to be built.

###  5.5 Beyond BDD. The dead end of the ordering conjecture.

Anyone asked to give some examples of theories which are not FC will begin
from the most natural one – the infinite total ordering from Remark 3.

And it is not immediately clear how to come out with something really
different. For quite some time, we believed that the following conjecture
could be true:

######  Conjecture 2 (False).

$\cal T$ is not FC if and only if $\cal T$ defines an ordering, by which we
mean that there exists a database instance $D$, an infinite set $A\subseteq
Chase(D,{\cal T})$ and a query $\Phi(x,y)$, which is a conjunctive query with
projections, with two free variables, such that $Chase(D,{\cal
T})\not\models\exists\bar{x}\Phi(x,x)$ and $\Phi$ defines a strict total
ordering on $A$.

Notice how beautiful it would be. Even if our BDD/FC conjecture is true (which
we believe it is) it does not give a full explanation of the phenomenon of
Finite Controllability, as they are many theories (for example guarded) which
are FC but not BDD. Had Conjecture 2 be true, it would have given a sort of
such explanation, and a very elegant one, since the above property of
”defining an ordering” is very close to (the negation of) the standard, and
very important, model-theoretic notion of stability [10]. Besides, it could
give the BDD/FC conjecture as a corollary, if we only could prove that a BDD
theory never defines an ordering, which we believe should not be very hard.

Clearly, the ”if” implication of the conjecture holds true: if $D$, $A$ and
$\Phi$ like in the conjecture existed, then $\exists x\Phi(x,x)$ would be a
query false in $Chase(D,{\cal T})$ but true in each finite model of ${\cal
T},D$ (as each such finite model must contain a homomorphic image of
$Chase(D,{\cal T})$, and some two elements of $A$ must be mapped, by this
homomorphism, to the same element of the finite structure)

However, as the following notorious example shows, the opposite implication is
not true. Let $\cal T$ be:

$E(x,y)\Rightarrow\exists z\;E(y,z)$

$R(x,y),E(x,x^{\prime}),E(y,z),E(z,y^{\prime})\Rightarrow
R(x^{\prime},y^{\prime})$

It is not hard to see that $\cal T$ does not define an ordering. We are going
to show that $\cal T$ is not FC. Let $D$ consist of the atoms $E(a_{0},a_{1})$
and $R(a_{0},a_{0})$.

Then ${\cal C}=Chase(D,{\cal T})$ is an infinite $E$-chain like in Example 3,
but with additional atoms $R(a_{i},a_{2i})$ for each $i$. Let
$\Phi(x,y)=E(x,y)\wedge R(y,y)$. Clearly, ${\cal C}\not\models\Phi$ – the only
element $a_{0}$ of ${\cal C}$ which satisfies $R(y,y)$ has no $E$-predecessor.
But, as we are going to prove, if $\cal M$ is any finite model of ${\cal T},D$
then ${\cal M}\models\Phi$.

Indeed, whatever the structure $\cal M$ is, it must contain a sequence
$a_{0},a_{1},\ldots a_{m}\ldots a_{m+n}$ of elements such that $a_{m}=a_{m+n}$
and ${\cal M}\models E(a_{i},a_{i+1})$ for each $i<m+n$. The datalog rule form
$\cal T$ can then prove that ${\cal M}\models R(a_{m},a_{m+(m\mod n)})$, and
then that ${\cal M}\models R(a_{m+l\mod n},a_{m+(m+2l\mod n)})$. Let $l=-m\mod
n$. Now take $y=a_{m+l\mod n}$ and $x=a_{m+l-1\mod n}$ to get $R(y,y)$.

It is worth mentioning that the structure ${\cal C}$ from the above example is
ptp-conservative. As the degree of the elements of ${\cal C}$ is bounded by 4,
this follows from:

######  Lemma 13.

Each binary structure of bounded degree is ptp-conservative.

Proof (hint): For a given number $m$, color the structure in such a way, that
each neighborhood of radius $m$ consists of elements whose colors are pairwise
different. Then mimic the reasoning from Section 4. $\Box$

This shows ptp-conservativity of $Chase$, which – as explained in Remark 4 –
guarantees that, if only $n$ is big enough, $M_{n}(\overline{Chase})$ will be
a model for all the existential TGDs from the theory, does not buy us much
more: the devil can very well be in the plain datalog rules. Notice however,
that not all datalog rules are troublemakers:

######  Remark 5.

Suppose $\bar{\cal C}$ is $n$-conservative up to the size $m$. Let
$\Psi\Rightarrow Q(x)$ be a datalog rule with at most $m$ variables and with a
unary predicate in the head. If this true in $\bar{\cal C}$ then it is also
true in $M_{n}(\bar{\cal C})$. Proof: positive $m$-types of $x$ and of
$q_{n}(x)$ are the same.

###  5.6 Guarded TGDs

Guarded Datalog∃ programs, proved to be FC in [1], consist of guarded rules
(datalog rules and TGDs) which have an atom in the body, called the guard,
containing all the variables that occur in the body of this rule. There is no
restriction on the arity, in particular on the arity of the predicates in the
heads of TGDs.

The witness generated by a guarded TGD appears to depend on all the variables
in the head of the rule, and in consequence such a rule seems to be inherently
non-binary, not even in the broad sense of Section 5.1. But, as it turns out,
Guarded Datalog∃ programs are binary in disguise. And, while they are not BDD,
still nothing beyond the techniques developed in Sections 2 and 4 is needed to
prove they are FC.

To be more precise, suppose there exists a Guarded Program $\cal T$, a
database instance $D$ and a query $\Phi$ which are a counterexample for FC. Of
course $D$ can be also hardwired into $\cal T$ so we can assume it is empty.

Now we will show how to rewrite $\cal T$ and $\Phi$ into a binary signature,
without changing their status of a counterexample. Then we will use the
toolkit from Sections 2 and 4 to show very easily that the resulting binary
program is FC.

(i) First step is similar to the one in the end of Section 3.1 – we want the
predicates which are in the heads of TGDs (the TGPs) to be distinct that the
ones in the heads of datalog rules. We also want the rules to respect the
order of variables in atoms – if $x$ is left of $y$ in some atom in the rule
then $x$ never can be right of $y$ in any atom of the same rule. This can be
done by remembering the order of arguments as a part of the name of each
predicate. Of course $\Phi$ must be rewritten – each new predicate is now a
disjunction of the old predicates. Notice that guardedness implies that if
$\cal T$ respects the order of variables, if $Chase({\cal T})\models
R(\bar{a},c)$ for some TGP $R$ and if $Chase({\cal T})\models P(\bar{b},c)$
then $\bar{b}\subseteq\bar{a}$. The elements in $\bar{a}$ are "parents of
$c$", who were present in the atom $R$ when $c$ was born, and no rule can add
anything else left of $c$ in any atom.

Rename the variables in each rule in such a way, that the rightmost variable
of the guard of each rule is $y$. Call this $y$ the leading variable of the
rule.

(ii) We want the elements to know their parents by name. If $R(x_{1},\ldots
x_{k},y)$ is a TGP in $\cal T$ we add to $T$ new rules:
$R(x_{1},\ldots x_{k},y)\Rightarrow F_{i}(x_{i},y)$
for each $i\leq k$, where $F_{i}$ are new binary predicates.

(iii) Replace each TGD of the form $\Psi\Rightarrow\phi$, with the leading
variable $y$, with all possible rules of the form:

###### ($\spadesuit$ 11

) $\Psi\wedge F_{i_{1}}(x_{1},y)\wedge\ldots\wedge
F_{i_{k}}(x_{k},y)\Rightarrow\phi$

where $x_{1},\ldots x_{k}$ are all the non-leading variables in $\Psi$ and
$i_{1},\ldots i_{k}\leq K$, where $K$ is the maximal arity of the predicates
in $\cal T$. This changes nothing, as the elements to be substituted for
$x_{i}$ must have been some parents of $y$ anyway.

(iv) Now, again in the manner of Section 3.1 rewrite the current $\cal T$ and
$\Phi$ in such a way, that each TGP only occurs in one rule head (this can be
easily done for the cost of some renaming datalog rules).

(v) Now perform step (iii) for the datalog rules of the current program.

At some point in Section 5.1 we wrote: All we need in the proof in Section 3
is that (…) the witness generated by the rule only depends on one element in
the body (the $y$), while the additional elements in the body are just needed
to make sure that $y$ has a positive type which allows it to demand a witness.
Notice that this is exactly the case with our program now: all rules are in
the form ($\spadesuit$ 11.) and the elements of $Chase({\cal T})$ that can
possibly be substituted for elements of $\bar{x}$ in the body of such rule are
themselves functions of $y$. So $t$ is just a function of $y$, not of all the
elements of $\bar{x}$! The only reason why non-binary predicates could be
necessary does not exist any more. Let us get rid of them.

Since the original $\cal T$ was guarded, each atom $P(\bar{a})$ in
$Chase({\cal T})$ was contained in some TGP atom $R(\bar{b},c)$. Our idea is
that full information about $P(\bar{a})$ will be remembered, without
materializing $P(\bar{a})$, in a monadic way, by the element $c$. It will need
to remember which of its parents are involved in each predicate. Of course it
also needs to remember the links to its parents – this is why the relations
$F_{i}$ were introduced.

(vi) Replace each TGD of the form: $\Psi\Rightarrow\exists z\;R(x_{1},\ldots
x_{k},$ $z)$ ($x_{k}$ may, or may not, by equal to $y$) by the following
rules: $\Psi\Rightarrow\exists z\;E^{R}(y,z)$ and $\Psi\wedge
E^{R}(y,z)\Rightarrow R^{m}(z)$ where $E^{R}$ is a new binary predicate.
$E^{R}(y,z)$ means something like "the (unique) rule which derives $R$ was
applied to a tuple led by $y$ and a witness $z$ was created". The newly
created element $z$ must also learn who its parents are. For each
$i\in\\{1,\ldots k\\}$, if $F_{j}(x_{i},y)$ was an atom in $\Psi$, add to the
current $\cal T$ the rule:

($\diamondsuit$) $F_{j}(x_{i},y)\wedge E^{R}(y,z)\Rightarrow F_{i}(x_{i},z)$

and replace each TGP atom $R(x_{1},\ldots x_{k},z)$ in the body of any rule
by:
$F_{1}(x_{1},z)\wedge\ldots F_{k}(x_{k},z)\wedge R^{m}(z)$

Now the program does not have TGPs of arity higher than 2 any more. Notice
that for each variable $x\neq y$ in any rule, there exists $i$ such that the
atom $F_{i}(x,y)$ is in the body of this rule. We are ready to get rid also of
the non-TGPs:

(vii) In each rule, with the atoms $F_{i_{1}}(w_{1},y),\ldots
F_{i_{1}}(w_{l},y)$ in its body, replace each occurrence of a non-TGP atom
$Q(w_{1},\ldots w_{l})$ with $Q_{i_{1}i_{2}\ldots i_{l}}(y)$, where
$Q_{i_{1}i_{2}\ldots i_{l}}(y)$ is a new monadic predicate (in which $y$
remembers what his parents with numbers $i_{1},i_{2},\ldots i_{l}$ are
involved in). For each two monadic predicates of the form $Q_{i_{1}i_{2}\ldots
i_{l}}(y)$ and $Q_{j_{1}j_{2}\ldots j_{l}}$ add to the program all possible
rules of the form:

$F_{i_{1}}(x_{1},y)\ldots\wedge F_{i_{l}}(x_{l},y)\wedge
F_{j_{1}}(x_{1},z)\ldots\wedge F_{j_{l}}(x_{l},z)\wedge$
$\wedge Q_{i_{1}i_{2}\ldots i_{l}}(y)\Rightarrow Q_{j_{1}j_{2}\ldots
j_{l}}(z)$

The role of the last rule is to make sure that, once an atom of the predicate
$Q$, involving $x_{1}\ldots$ $x_{l}$ is derived, all the elements that have
$x_{1}\ldots$ $x_{l}$ among their parents are aware of that and ready to use
this fact in further derivations.

We now have a new program over a binary signature, call it ${\cal
T}^{\prime}$. It follows from the construction that ${\cal C}=Chase({\cal
T}^{\prime})$ is almost the same structure as $Chase({\cal T})$ (where $\cal
T$ is the original guarded program). They both have the same elements, and the
predicates of each of them can be seen as views over the predicates of the
other one. But notice that $Chase({\cal T}^{\prime})$ is a binary structure
satisfying the assumptions of of Lemma 2. So it is ptp-conservative. This
means that if $n$ is big enough then $M_{n}(\bar{\cal C})$ is a model for all
the existential TGDs in ${\cal T}^{\prime}$ and that $M_{n}(\bar{\cal
C})\not\models\Phi^{\prime}$ (where $\Phi^{\prime}$ is the original query
$\Phi$ after all the rewritings). To finish the proof of FC for Guarded
Datalog∃ programs we only need to show that $M_{n}(\bar{\cal C})$ is also a
model of all the datalog rules in ${\cal T}^{\prime}$. All the datalog rules
except from the rules of the form ($\diamondsuit$) have a unary atom in the
head, so (by Remark 5) we do not need to bother about them at all. What
remains to be seen is that the rules of the form ($\diamondsuit$) also remain
true in $M_{n}(\bar{\cal C})$. So suppose $M_{n}(\bar{\cal C})\models
F_{j}(a,b)\wedge E^{R}(b,c)$ for some $a,b,c$. This means that there exist
$a^{\prime},b^{\prime},b^{\prime\prime},c^{\prime\prime}$ in $\bar{\cal C}$
such that $\bar{\cal C}\models F_{j}(a^{\prime},b^{\prime})$, $\bar{\cal
C}\models E^{R}(b^{\prime\prime},c^{\prime\prime})$, $q_{n}(a^{\prime})=a$,
$q_{n}(b^{\prime})=q_{n}(b^{\prime\prime})=b$ and $q_{n}(c^{\prime})=c$. But
$\bar{\cal C}$ can be seen as a Chase of the guarded theory $\cal T$ with the
natural coloring, so the types of successors of an element only depend on the
type of this element, and it is easy to see that if
$b^{\prime}\equiv_{n}b^{\prime\prime}$ and $\bar{\cal C}\models
E^{R}(b^{\prime\prime},c^{\prime\prime})$ then there must exist
$c^{\prime}\equiv_{n}c^{\prime\prime}$ such that $\bar{\cal C}\models
E^{R}(b^{\prime},c^{\prime})$. Since the rule ($\diamondsuit$) was true in
$\bar{\cal C}$ we get that $\bar{\cal C}\models F_{i}(a^{\prime},c^{\prime})$
which implies that $M_{n}(\bar{\cal C})\models F_{i}(a,c)$. We proved that
$\diamondsuit$ remains true in $M_{n}(\bar{\cal C})$.

## References

  * [1] V. Barany, G. Gottlob, and M. Otto. Querying the guarded fragment; Proc. of the 25th IEEE Symposium on Logic in Computer Science, LICS 2010, Edinburgh, UK, pp. 1-10, 2010;
  * [2] A. Cali, G. Gottlob, and T. Lukasiewicz; A general datalog-based framework for tractable query answering over ontologies; in Proc. of PODS, 2009;
  * [3] A. Cali, G. Gottlob, and T. Lukasiewicz; A general datalog-based framework for tractable query answering over ontologies; J. Web Sem. 14, 2012, 57-83
  * [4] A. Cali, G. Gottlob, and A. Pieris; Advanced processing for ontological queries; Proc. VLDB-10, 3(1):554-565, 2010;
  * [5] A. Cali, G. Gottlob, and A. Pieris; Query Answering under Non-guarded Rules in Datalog+/- ; Web Reasoning and Rule Systems Lecture Notes in Computer Science, 2010, Volume 6333, pp 1-17;
  * [6] T. Gogacz, J. Marcinkowski; Converging to the Chase and Some Finite. Controllability Results; Proc. of the 28th IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, USA, to appear;
  * [7] D. S. Johnson and A. C. Klug. Testing containment of conjunctive queries under functional and inclusion dependencies; JCSS 28(1):167-189, 1984;
  * [8] R. Rosati; On the decidability and finite controllability of query processing in databases with incomplete information; in Proc. PODS 2006, pp. 356–365;
  * [9] R. Rosati; On the decidability and finite controllability of query processing in databases with incomplete information; J. Comput. Syst. Sci. 77(3),2011, pp. 572-594
  * [10] S. Shelah; (1969), Stable theories; Israel J. Math. 7 (3): 187-202.