Piotr Ostropolski-Nalewaja

Jerzy Marcinkowski

David Carral

Sebastian Rudolph

A Journey to the Frontiers of Query Rewritability (Extended Technical Report)

We consider (first-order) query rewritability in the context of theorymediated query answering. The starting point of our journey is the FUS/FES conjecture, which states that any theory that is a finite expansion set (FES) and admits query rewriting (BDD, FUS) must be uniformly bounded. We show that this conjecture holds for a large class of BDD theories, which we call "local". Upon investigating how "non-local" BDD theories can actually get, we discover unexpected phenomena that, we think, are at odds with prevailing intuitions about BDD theories.

INTRODUCTION

The scenario we consider in this paper has been studied extensively both in database theory and in knowledge representation: consider a database instance D (also called fact set, or structure) and a theory T (or rule set) that consists of tuple generating dependencies (or rules). For a given conjunctive query 𝜙, we ask if D and T together logically entail 𝜙, written: D, T |= 𝜙. This problem is also referred to as ontology-mediated query answering. The chase. The notion of the chase is fundamental in this context. It denotes a structure obtained from D via the chase procedure, which iteratively adds new terms and atoms in order to satisfy the constraints from T , producing a growing sequence of structures D=𝐶ℎ 0 (D, T ), 𝐶ℎ 1 (D, T ), 𝐶ℎ 2 (D, T ), . . .. The chase 𝐶ℎ(D, T ) is then obtained as the corresponding fixpoint 𝑖 ∈N 𝐶ℎ 𝑖 (D, T ).

It is known [START_REF] Deutsch | The chase revisited[END_REF] that a conjunctive query is entailed if and only if it holds in the corresponding chase, which allows for reducing entailment to model checking:

∀T ∀D ∀𝜙 𝐶ℎ(D, T ) |= 𝜙 ⇔ D, T |= 𝜙 .
Finite expansion sets. We say T enjoys the finite expansion set property [START_REF] Baget | On rules with existential variables: Walking the decidability line[END_REF] (or simply is FES) if, for every D, all conjunctive queries satisfied in 𝐶ℎ(D, T ) are already jointly satisfied after finitely many chase steps. More precisely, T is FES if:

∀D ∃𝑖 ∈ N ∀𝜙 𝐶ℎ(D, T ) |= 𝜙 ⇔ 𝐶ℎ 𝑖 (D, T ) |= 𝜙 (FES)
This is an important property, since 𝐶ℎ(D, T ) is typically an infinite structure, only existing as an abstract mathematical object, and impossible to query, whereas 𝐶ℎ 𝑖 (D, T ) is always finite and so in principle it can be computed and queried. Bounded derivation depth. An arguably even more beneficial property a theory can enjoy in this context is the following: We say T has the bounded derivation depth property (or is BDD) if which means that, in order to evaluate 𝜙, it is enough to run only the first 𝑖 steps of the chase, with 𝑖 depending on 𝜙 but not on D.

As it turns out, BDD is equivalent [START_REF] Calì | Datalog ± : a unified approach to ontologies and integrity constraints[END_REF] to FUS (finite unification set) [START_REF] Baget | On rules with existential variables: Walking the decidability line[END_REF]. FUS is the class ensuring that conjunctive queries always rewrite: for each 𝜙 one can compute a query 𝜙 T , being a union of conjunctive queries, such that for each D we have that 𝐶ℎ(D, T ) |= 𝜙 exactly if D |= 𝜙 T -this is known to be equivalent to the existence of an arbitrary first-order rewriting [START_REF] König | Sound, complete and minimal UCQ-rewriting for existential rules[END_REF].

Behold the extreme usefulness of this property: instead of querying 𝐶ℎ(D, T ), an elusive infinite structure, we can equivalently query D, the only structure we have immediate access to.

No wonder the BDD/FUS property has been considered in literally hundreds of papers. Numerous classes of BDD theories have been identified and intensively studied, among them subclasses with decidable membership like: • linear theories, where rules have at most one body atom; • guarded BDD theories (while not all guarded theories are BDD, it is decidable to determine if a guarded theory is BDD [START_REF] Barceló | First-order rewritability of frontierguarded ontology-mediated queries[END_REF][START_REF] Civili | On the first-order rewritability of conjunctive queries over binary guarded existential rules[END_REF]), generalizing linear theories; • sticky theories, defined by a reasonably natural syntactic restriction on the use of joins [START_REF] Calì | Advanced processing for ontological queries[END_REF].

Apart from the decidable subclasses of BDD, there are also natural undecidable subclasses: • bounded Datalog theories, already studied decades before the class BDD itself was discovered [START_REF] Gaifman | Undecidable optimization problems for database logic programs[END_REF]; • binary BDD theories, where the arity of relation symbols is at most 2 (also studied in the context of description logics [START_REF] Artale | The DL-Lite family and relations[END_REF]); • backward shy theories [START_REF] Thomazo | Conjunctive Query Answering Under Existential Rules -Decidability, Complexity, and Algorithms[END_REF], a superclass of sticky theories.

As we expose in this paper, despite this extensive body of work, we still understand very little about the deeper mathematical properties of BDD theories. In particular, we are going to show that the intuition of BDD theories as being "local", "only depending on the small pieces of D", and "unable to look too far" while (more or less) correct for all aforementioned classes of BDD theories is blatantly incorrect for BDD theories in general.

The FUS/FES conjecture. There is a striking similarity between formulas (BDD) and (FES), inspiring a natural conjecture, which we call the FUS/FES conjecture: For any BDD theory that is also FES, it should be possible to choose the number 𝑖 in a uniform way, independently from both D and 𝜙. In other words, the conjecture says that if T is both BDD and FES then:

∃𝑖 ∈ N ∀𝜙 ∀D 𝐶ℎ(D, T ) |= 𝜙 ⇔ 𝐶ℎ 𝑖 (D, T ) |= 𝜙 (UBDD)
This conjecture was studied earlier [START_REF] Delivorias | On the k-boundedness for existential rules[END_REF] and a proof was proposed, which however turned out to be incorrect and was later withdrawn.

Later, it was shown that the conjecture would hold if the assumption that T is FES were replaced by a stronger property [START_REF] Bourhis | Oblivious and semi-oblivious boundedness for existential rules[END_REF].

Main results. We identify the new, generic class of local BDD theories. Informally, such theories enforce that the creation of every chase atom depends only on a constant number of facts from the database. Importantly, this new class not only includes most of the aforementioned subclasses of BDD (with sticky and backward shy being notable exceptions) but also all BDD theories over signatures with a maximum predicate arity of 2.

With this new class of theories defined (and the above inclusions proved), we present our three main results: First that the FUS/FES conjecture holds for local theories (Theorem 2). Second that the conjecture holds for every BDD theory over a binary signature (Corollary 1) -an immediate consequence of the fact that such theories are local (Theorem 1).

Yet, as least as interesting as these insights we find our third result (reflected in Theorem 3): the discovery of very much nonlocal (and not even what we call bounded-degree local) theories that are still BDD. Such theories not only defy many of the popular intuitions about the BDD class, but also shows that all previous investigations into that class have probably barely scratched its surface and that there is a lot of room for new decidable/syntactic classes of BDD theories, richer than all hitherto considered. One plausible reason why this new world exhibits counterintuitive phenomena and has gone entirely unnoticed is that it requires theories of arity higher than 2. Binary theories are much easier to imagine and they are mainly responsible for shaping our intuitions.

Summarizing, the main message of this paper is: even if a (finite) counterexample to the FUS/FES conjecture should exist, it is going to be found nowhere near the familiar avenues of the BDD class. But we also show that the known avenues only reach a small part of the BDD class and there is a lot of uncharted territory left. Organisation of this paper. Apart from its preliminary sections (Sections 2-7), the paper is organized as follows:

In Section 8 we define local theories. Later we state our first result Theorem 1 and present a brief insight into its proof.

In Section 9 we state our second result -that the FUS/FES conjecture holds for local theories (Theorem 2) -and prove it. Also we note that the conjecture holds for theories over binary signatures (Corollary 1).

In Section 10, we notice that sticky theories, while BDD, are not always local. We define another, weaker, notion, of bounded-degreelocal theories (or bd-local) and note that it covers sticky. Later we discuss properties of this newly defined class.

In Section 11 we examine the intuition that "BDD theories are unable to look too far". We define the notion of distancing theories, and show that if a theory is local then it is also distancing. We also notice that backward shy theories are distancing, so that most of the previously known examples of BDD theories are indeed distancing. We show however, that there exists a BDD theory T 𝑑 that is not distancing. As a corollary we get that, for this BDD theory, the rewriting 𝜙 T 𝑑 (which is a disjunction of conjunctive queries) of a query 𝜙 can require disjuncts of exponential size with respect to the size of 𝜙. This is in stark contrast to any BDD theories previously considered.

Finally in Section 12, we conclude and discuss future work.

This is an extended technical report of an article with the same title published at PODS 2022. It includes the complete formal proofs for all results in the appendix.

PRELIMINARIES

Queries and TGDs. A conjunctive query (CQ) is a formula 𝜓 ( ȳ) = ∃ x 𝛽 ( x, ȳ) with 𝛽 being a non-empty conjunction of atomic formulas over some signature (or schema) Σ (which is a finite set of relation symbols) and over some set of variables and set of constants. So, for example ∃𝑥 𝑆𝑖𝑏𝑙𝑖𝑛𝑔𝑠 (𝐴𝑏𝑒𝑙, 𝑥), 𝐹𝑒𝑚𝑎𝑙𝑒 (𝑥) is a CQ.

A boolean CQ (short: BCQ) is a CQ with all variables quantified (as in the preceding example). We refer to 𝛽 as the body of 𝜓 ( ȳ). By a union of conjunctive queries (UCQ) we mean a formula being a disjunction of CQs. By the size of a CQ, denoted |𝜓 ( ȳ)|, we mean the number of atomic formulas it is built of. By the width of a UCQ we will mean the size of its greatest disjunct. Also, we will sometimes treat UCQs as sets of CQs.

A theory or a rule set is a finite set of tuple generating dependencies (TGDs, often just referred to as rules). A rule is a first-order logic formula of the form ∀x, ȳ 𝛽 ( x, ȳ) ⇒ ∃ w 𝛼 ( ȳ, w) , where x, ȳ and w are pairwise disjoint lists of variables, 𝛽 ( x, ȳ) (the rule's body) is a conjunction of atomic formulas and 𝛼 ( ȳ, w) (the rule's head) is an atomic formula. The frontier ȳ of a rule 𝜌, denoted fr (𝜌), is the set of all variables that occur both in the body and the head of the rule. We omit universal quantifiers when writing rules and treat conjunctions of atoms (such as 𝛽) as sets of atoms.

Note that, in database theory terminology, our rules are "single head" TGDs. This is the only reasonable choice in this context, since we want to talk about theories over a binary signature: if we allowed rule heads to comprise several atoms, then rules with predicates of any arity could be easily simulated using only arity 2 predicates. On the other hand, this does not restrict our results in the cases where we do not assume that the signature is binary, since every multi-head theory can be rewritten into a single-head one, using higher-arity auxiliary predicates, and this rewriting does not affect the property of being FUS or FES. Structures and entailment. A database instance (or structure or fact set) is a set of facts -atomic formulas over Σ. For a structure F over Σ we let 𝑑𝑜𝑚(F) denote its active domain -the set of all terms that appear in the facts of F. For 𝑐, 𝑐 ′ ∈ 𝑑𝑜𝑚(F), we let 𝑑𝑖𝑠𝑡 F (𝑐, 𝑐 ′ ) denote the distance between 𝑐 and 𝑐 ′ in the Gaifman graph of F: the vertices of this graph are elements of 𝑑𝑜𝑚(F) and two vertices are connected by an edge if and only if they appear in the same fact. We define the degree of F as the degree of F's Gaifman graph.

F is a model of T (written: Homomorphisms and query containment. For structures D, F, a homomorphism from D to F is a function ℎ : 𝑑𝑜𝑚(D) → 𝑑𝑜𝑚(F) such that 𝐴(ℎ( ì 𝑥)) ∈ F for each fact 𝐴( ì 𝑥) ∈ D and that ℎ(𝑎) = 𝑎 for any constant 𝑎 ∈ 𝑑𝑜𝑚(D). Given a fact 𝛼 = 𝐴( ì 𝑥) ∈ D, we will use ℎ(𝛼) to denote 𝐴(ℎ( ì 𝑥)). For two CQs 𝜙 ( ȳ) and 𝜓 ( ȳ), with the same set of free variables, we say that 𝜙 ( ȳ) contains 𝜓 ( ȳ) if for every structure D and for every tuple ā ∈ 𝑑𝑜𝑚(D) | ȳ | if D |= 𝜓 ( ā) than also D |= 𝜙 ( ā). It is well known that 𝜙 ( ȳ) contains 𝜓 ( ȳ) if and only if there is a homomorphism 1 from 𝜙 ( ȳ) to 𝜓 ( ȳ) that is the identity on ȳ. Core of a structure. A substructure H of a finite structure G is a core of G (see [START_REF] Hell | The core of a graph[END_REF]) if there exists a homomorphism ℎ : G → H but there is no homomorphism from G to H ′ where H ′ is a proper substructure of H. Note that the definition of homomorphisms ensures that ℎ(𝑎) = 𝑎 for every constant 𝑎 ∈ 𝑑𝑜𝑚(G).

F |= T ) if F
It is well known that [START_REF] Hell | The core of a graph[END_REF]:

(1) Every finite structure has a core.

(2) Cores of a finite structure are unique up to isomorphism.

(3) If H is a core (of any structure) then it is a core of itself.

Given a (finite) structure G, we let 𝐶𝑜𝑟𝑒 (G) denote a function that returns some induced substructure of G that is a core. Connected queries, rules and theories. For a CQ, one can define its Gaifman graph in the natural way: Variables are the vertices of this graph and two variables are connected by an edge if and only if they both appear in the same atomic formula. A conjunctive query is connected if its Gaifman graph is connected. A TGD is connected if its body is. A theory is connected if each of its rules is.

All the theories we consider in this paper are connected with the important exception of theories over a binary signature. Forcing theories to be connected will help us to better express the nuances of the BDD class in Sections 10-11. This assumption does not reduce the expressive power of such theories due to the following trivial trick: add a fresh variable as an additional, first variable in all the atoms appearing in the rules of the theory. This will make the theory connected, and it will obviously preserve its BDD and FES status. But it will increase the arity -so if we care about the arity we do not get connectivity for free.

Note that after applying the trivial trick to an instance F the distance between each 𝑐 and 𝑐 ′ from 𝑑𝑜𝑚(F) will be at most 2. Also, applying this trick turns any instance with a Gaifman graph of a low (bounded) degree into one with a high degree Gaifman graph.

THE SKOLEM CHASE.

The chase procedure is a standard algorithm, studied in a plethora of papers. It can be used to semi-decide whether T , D |= 𝜙 ( ā) for given theory T , instance D, CQ 𝜙 ( ȳ) and tuple ā ∈ 𝑑𝑜𝑚(D) | ȳ | . In fact the algorithm comes in many variants and flavors. The best way to present our results is by using a variant of the the semi-oblivious Skolem chase, which we define in this section.

We say that two CQs have the same isomorphism type when one can be obtained from the other by means of bijective renaming of variables. For a CQ Φ define 𝜏 (Φ) as the isomorphism type of Φ.

For each possible isomorphism type 𝜏 = 𝜏 (𝜙 ( ȳ)) of some atomic conjunctive query 𝜙 ( ȳ), and for each natural number 1 ≤ 𝑖 ≤ 𝑎𝑟𝑖𝑡𝑦 (𝐸), where 𝐸 is the relation symbol of 𝜙 ( ȳ), let 𝑓 𝜏 𝑖 be a function symbol, with arity equal to | ȳ|, that is the number of free variables in 𝜙 ( ȳ).

Definition 2 (Skolemization). For a given TGD 𝜌, of the form 𝛽 ( x, ȳ) ⇒ ∃ w 𝛼 ( x, w) by sh(𝜌) we denote the Skolemization of the head of 𝜌, that is the atom 𝛼 ( x, w), with each variable 𝑤 ∈ w replaced by the term 𝑓 𝜏 𝑖 ( x), where 𝑖 is the earliest position in 𝛼 ( x, w) where the variable 𝑤 occurs.

Let, for example 𝜌 be 𝐸 (𝑥, 𝑦, 𝑧), 𝑃 (𝑥) ⇒ ∃𝑣 𝑅(𝑦, 𝑣, 𝑧, 𝑣). Then sh(𝜌) will be the atom 𝑅(𝑦, 𝑓 𝜏 2 (𝑦, 𝑧), 𝑧, 𝑓 𝜏 2 (𝑦, 𝑧)) where 𝜏 is the isomorphism type of ∃𝑣 𝑅(𝑦, 𝑣, 𝑧, 𝑣). Notice that sh(𝜌) does not depend on the body of 𝜌, only on its head. In particular it does not depend on the non-frontier variables 2 of the body of 𝜌.

Now we can define the procedure of rule application. Parameters of this procedure are an instance F, a rule 𝜌, and a mapping 𝜎 assigning elements of the active domain of F to the variables that occur in the body of 𝜌: Definition 3 (Rule application). Let 𝜌 be a rule of the form 𝛽 ( x, ȳ) ⇒ ∃ w 𝛼 ( ȳ, w), and let F be a fact set.

• Define H𝑜𝑚(𝜌, F) as the set of all mappings 𝜎 from variables in x ∪ ȳ to 𝑑𝑜𝑚(F) such that 𝜎 (𝛽 ( x, ȳ)) ⊆ F (which means that all the atoms from 𝛽 are in F after we apply 𝜎 to them). • For 𝜎 ∈ H𝑜𝑚(𝜌, F), define 𝑎𝑝𝑝𝑙 (𝜌, 𝜎) = 𝜎 (sh(𝜌)).

With these notions in place, we can now define the chase procedure as a whole. Given an instance D and a theory T , it produces a sequence (Ch 𝑖 (T , D)) 𝑖 ∈N of instances and the structure Ch(T , D), according to the following definition. It is well known that Ch(T , D) is a universal model for T and D (i.e., a model that can be homomorphically mapped into any other model). Thus, this structure can be used to solve CQ entailment: for any theory T , CQ 𝜙 ( ȳ), instance D and ā ∈ 𝑑𝑜𝑚(D) | ȳ | , we have:

𝐶ℎ(T , D) |= 𝜙 ( ā) ⇔ D, T |= 𝜙 ( ā)
Example 5. Let T 𝑎 and D 𝑎 be as in Example 1, then

• Ch 0 (T 𝑎 , D 𝑎 ) = D 𝑎 = {𝐻𝑢𝑚𝑎𝑛(𝐴𝑏𝑒𝑙)}, • Ch 1 (T 𝑎 , D 𝑎 ) = Ch 0 (T 𝑎 , D 𝑎 ) ∪ {𝑀𝑜𝑡ℎ𝑒𝑟 (𝐴𝑏𝑒𝑙, 𝑚𝑢𝑚(𝐴𝑏𝑒𝑙))}, • Ch 2 (T 𝑎 , D 𝑎 ) = Ch 1 (T 𝑎 , D 𝑎 ) ∪ {𝑀𝑜𝑡ℎ𝑒𝑟 (𝑚𝑢𝑚(𝐴𝑏𝑒𝑙), 𝑚𝑢𝑚(𝑚𝑢𝑚(𝐴𝑏𝑒𝑙))
)}, and so on (we use the function symbol "mum" as an alias for the ugly Skolem function symbol from Definition 2). Now note that there is nothing in Definition 4 that could prevent us from taking D = Ch 2 (T 𝑎 , D 𝑎 ) and running the chase for such D. It is easy to see that in that case we obtain Ch(T 𝑎 , D) = Ch(T 𝑎 , D 𝑎 ). This leads to the following easy insight: Observation 6. If D ⊆ F ⊆ Ch(T, D) then Ch(T, F) = Ch(T, D). 2 Including non-frontier variables as arguments of the functions 𝑓 𝜏 𝑖 (like 𝑥 in the current example) would lead to the oblivious chase. Also note that the names of the terms do not identify 𝜌 (their "rule of origin"). This is going to be important in the proof of Theorem 1.

Note that that equality in Observation 6 is to be understood literally (rather than "up to isomorphism"). This is crucial for our treatise and it constitutes the main reason why we use the Skolem naming convention.

Finally, let us state another property of the chase -a direct consequence of the fact that Ch(T , D) is a universal model. Property 7. Let T be a theory and let D and F be fact sets satisfying D ⊆ F ⊆ Ch(T , D) as well as F |= T . Then there exists a homomorphism from Ch(T , D) to F that is the identity on 𝑑𝑜𝑚(F).

Frontier and birth atoms. Let 𝛼 be an atom from 𝐶ℎ(T , D) \ D, created as 𝑎𝑝𝑝𝑙 (𝜌, 𝜎) for some 𝜌 ∈ T and 𝜎 ∈ 𝐻𝑜𝑚(𝜌, D). We let the frontier of 𝛼 (written: fr (𝛼)) denote the set of terms 𝜎 (fr (𝜌)). Notice that there may be more than one rule application creating the same atom 𝛼, but: Observation 8. For every 𝜌, 𝜌 ′ ∈ T and every 𝜎 ∈ 𝐻𝑜𝑚(𝜌, D) if 𝑎𝑝𝑝𝑙 (𝜌, 𝜎) = 𝑎𝑝𝑝𝑙 (𝜌 ′ , 𝜎 ′ ) then heads of 𝜌 and 𝜌 ′ when treated as CQs have the same isomorphism type.

Clearly, for each 𝑡 ∈ 𝑑𝑜𝑚(𝐶ℎ(T , D)) either 𝑡 ∈ 𝑑𝑜𝑚(D) or 𝑡 was created by the chase procedure as a Skolem term. Notice that, despite the name of the rule of T that created 𝑡 not being indicated in the name of 𝑡 (as per our Skolem naming convention), the following still holds: Observation 9. Suppose 𝑡 ∈ 𝑑𝑜𝑚(𝐶ℎ(T , D)) \ 𝑑𝑜𝑚(D). Then there exists exactly one atom 𝛼 ∈ 𝐶ℎ(T , D) such that 𝑡 appears in 𝛼, but 𝑡 ∉ fr (𝛼).

We will refer to such an atom 𝛼 as the birth atom of 𝑡. For the proof of the last observation notice that one can uniquely reconstruct 𝛼 using only 𝑡. This is because 𝑡 contains both the isomorphism type of 𝛼 (so that one can reconstruct 𝛼 up to bijective renaming of its terms) and its frontier terms.

THE THREE CLASSES

For a theory T , an instance D, a natural number 𝑛 and a conjunctive query 𝜙 (𝑦) we will write 𝐸𝑛𝑜𝑢𝑔ℎ(𝑛, 𝜙 (𝑦), D, T ) as a shorthand for:

∀ā ∈ 𝑑𝑜𝑚(D) | ȳ | 𝐶ℎ(T , D) |= 𝜙 ( ā) ⇔ 𝐶ℎ 𝑛 (T , D) |= 𝜙 ( ā) .
Meaning that "it is enough to run 𝑛 steps of the T -chase on D to fully evaluate 𝜙". Now we will provide definitions for three separate classes: BDD, FES, and UBDD [START_REF] Baget | On rules with existential variables: Walking the decidability line[END_REF][START_REF] Calì | A general datalog-based framework for tractable query answering over ontologies[END_REF].

Definition 10 (BDD). A theory T has the bounded derivation depth property if:

∀Φ ∃𝑛 Φ ∀D 𝐸𝑛𝑜𝑢𝑔ℎ(𝑛 Φ , Φ, D, T )

Definition 11 (FES). A theory T has the finite expansion set property if:

∀D ∃𝑛 D ∀Φ 𝐸𝑛𝑜𝑢𝑔ℎ(𝑛 D , Φ, D, T )

Definition 12 (UBDD). Theory T is uniformly BDD if: ∃𝑐 T ∀D ∀Φ 𝐸𝑛𝑜𝑢𝑔ℎ(𝑐 T , Φ, D, T )
Notice the striking similarity between the above expressions. Connections between those classes will be discussed later in Section 7, but before we need to explore BDD and FES in greater detail.

BDD AND FINITE UNIFICATION SETS

As with many important notions, it happens that the same concept is defined by multiple communities using different properties. This is exactly the case with finite unification set property [START_REF] Baget | On rules with existential variables: Walking the decidability line[END_REF] and BDD. Definition 13 (FUS). A theory T has the finite unification set property if every conjunctive query 𝜓 ( ȳ) has a rewriting -a UCQ, denoted 𝜓 rew ( ȳ), such that the following holds: For each instance D and each tuple ā ∈ 𝑑𝑜𝑚(D)

| ȳ | we have 𝐶ℎ(T , D), ā |= 𝜓 ( ȳ) ⇐⇒ D, ā |= 𝑟𝑒𝑤 (𝜓 ( ȳ)).
It is well known that T is BDD if and only if it is FUS [START_REF] Calì | Datalog ± : a unified approach to ontologies and integrity constraints[END_REF], so we will use the two terms interchangeably. For simplicity of our arguments and without loss of generality, we will require the set 𝑟𝑒𝑤 (𝜓 ( ȳ)) to be minimal:

If 𝜙 ( ȳ) ≠ 𝜙 ′ ( ȳ) are two elements of 𝑟𝑒𝑤 (𝜓 ( ȳ)) then 𝜙 ( ȳ) is not contained in 𝜙 ′ ( ȳ).
The BDD/FUS class admits several interesting properties. The following will be used later: facts about terms are produced by the chase soon after the terms are created (with only a constant delay). Observation 14. There exists a natural number 𝑛 𝑎𝑡 (depending only on T ) such that for any instance D, for any 𝑖 ∈ N, for any tuple t of domain elements from 𝑑𝑜𝑚(𝐶ℎ 𝑖 (T , D)) and for any 𝑅 ∈ Σ,

𝐶ℎ(T , D) |= 𝑅( t) implies 𝐶ℎ 𝑖+𝑛 𝑎𝑡 (T , D) |= 𝑅( t).
Proof (sketch). For any query 𝜙, let 𝑛 𝜙 denote the constant from Definition 10. Note, that there is only a finite number of non-isomorphic atomic queries. Therefore, we can obtain 𝑛 𝑎𝑡 as max({𝑛 𝜙 | 𝜙 is an atomic query}). □

The BDD property -exercises. Now, we would like to encourage the reader to solve a few exercises. While they are not part of the actual proofs, we believe they might provide valuable insights.

Exercise 15. Consider the theory T 𝑝 over schema {𝐸} consisting of just one rule 𝐸 (𝑥, 𝑦) ⇒ ∃𝑧 𝐸 (𝑦, 𝑧). Show that this theory is BDD.

Comment: This can be easily generalized: it is well known that all linear theories are BDD [START_REF] Calì | A general datalog-based framework for tractable query answering over ontologies[END_REF] (a theory is linear if each rule only has one atom in its body).

Exercise 16. Show that, if T is BDD and connected then there exists some 𝑑 ∈ N such that for each D and for each two terms

𝑐, 𝑐 ′ of 𝑑𝑜𝑚(D), if 𝑑𝑖𝑠𝑡 𝐶ℎ ( T,D) (𝑐, 𝑐 ′ ) = 1 then 𝑑𝑖𝑠𝑡 D (𝑐, 𝑐 ′ ) ≤ 𝑑.
Comment: the didactic purpose of Exercise 16 is to evoke or reinforce the intuition of BDD as a "locality" property: if terms from 𝑑𝑜𝑚(D) appear in one atom somewhere in 𝐶ℎ(T , D) then they could not possibly be far away from each other already in D.

FES AND CORE TERMINATION

FES theories always (regardless of the initial structure D) produce all the positive information present in 𝐶ℎ(T , D) already after a finite number of chase steps (this number can depend on D though). This is, as well, the case with the core termination [1, 2]: Definition 17. A theory T is core-terminating if for each fact set D there exists a 𝑘 ∈ N such that for each 𝑖 ≥ 𝑘:

𝐶𝑜𝑟𝑒 (Ch 𝑖 (T , D)) is isomorphic to 𝐶𝑜𝑟𝑒 (Ch 𝑖+1 (T , D)).
It is well known that T is core-terminating if and only if it is FES [START_REF] Baget | Revisiting chase termination for existential rules and their extension to nonmonotonic negation[END_REF], so we will use the two terms interchangeably. Moreover, the smallest numbers 𝑛 D and 𝑘 satisfying Definitions 11 and 17 (respectively) are equal; from now on this number will be denoted with 𝑐 T,D . It is also known [START_REF] Deutsch | The chase revisited[END_REF] that 𝐶𝑜𝑟𝑒 (Ch 𝑐 T,D (T , D)) |= T , D.

Definition 18. Given a FES theory T and an instance D, we let 𝐶𝑜𝑟𝑒 (T , D) denote 𝐶𝑜𝑟𝑒 (Ch 𝑐 T,D (T , D)).

Exercises Also this section comes with a few exercises. Again, we expect them to provide valuable insight, but they are not required for our subsequent proofs.

Exercise 19. Show that the theory from Exercise 15 is not FES.

Exercise 20. Show that the theory consisting of two rules 𝐸 (𝑥, 𝑦) ⇒ ∃𝑧 𝐸 (𝑦, 𝑧) and 𝐸 (𝑥, 𝑥 ′ ) ⇒ 𝐸 (𝑥, 𝑥) is FES.

THE FUS/FES CONJECTURE

It is very easy to produce examples of BDD theories that are not UBDD (see Exercise 15). However, all examples we could produce are not core-terminating. Likewise, it is easy to produce examples of core-terminating theories that are not UBDD, but they are not BDD either (all unbounded Datalog theories will be very happy to serve as examples). This gives rise to the following conjecture.

Conjecture 1 (The FUS/FES conjecture). Any theory that is both FUS and FES is also UBDD.

This conjecture was studied in [START_REF] Delivorias | On the k-boundedness for existential rules[END_REF] where an incorrect proof was proposed, and in [START_REF] Bourhis | Oblivious and semi-oblivious boundedness for existential rules[END_REF] where it was proved that it would hold true if the assumption that T is FES was replaced by the significantly stronger assumption that it is all-instances Skolem chase terminating. Note that the conjecture would be false if infinite theories, over infinite (yet just binary) schemas were allowed:

Example 21. Suppose a relation symbol 𝐸 𝑖 for every 𝑖 ∈ N. Let the theory T ∞ consist of all rules of the form 𝐸 𝑖 (𝑥, 𝑦) ⇒ ∃𝑧 𝐸 𝑖-1 (𝑦, 𝑧) for 𝑖 ∈ N + . Then T ∞ is BDD and core-terminating, but it is not UBDD. To see why this is the case, notice that only facts from a finite number of relations can appear in every given finite instance.

LOCAL THEORIES.

We are now ready to introduce the central notion of local theories. As it will turn out, not only the FUS/FES conjecture holds for these (Theorem 2) but they also subsume all BDD theories over binary signatures (Theorem 1). Notwithstanding, as we will argue near the end of the paper, there exists an untapped potential within the BDD class beyond the veils of locality (Theorem 3). Definition 22. A theory T is local if there exists some number 𝑙 T ∈ N such that for every instance D the following holds:

Ch(T , D) = F⊆D, |F| ≤𝑙 T Ch(T , F)
Note that the Skolem naming convention is important here. Without it, it would be unclear or at least ambiguous what a union of chases is supposed to mean. Importantly, we obtain that locality implies the BDD property. The detailed proof will be presented in Appendix A. Here, we just outline the proof idea. We start by observing that the atoms created in the chase by rules that contain existentially quantified variables form a forest. This is a crucial property of single-head rule sets over binary signatures as any such rule must have a frontier of size ≤1. (Obviously, this property ceases to hold for signatures of higher arities.) Essentially, as the chase progresses, the existential atoms (those produced through "proper" existential rules) are created further and further away from the instance. If we were able to bound the number of each such atom's ancestors -the atom set required for its creation -then we could finish the proof by slightly extending Observation 14. The forest shape, however, is not immediately sufficient to bound the ancestors of its atoms. To overcome this issue, we propose a normalization technique, that, given a BDD theory T over binary signature, produces a new theory T 𝑁 𝐹 , which might no longer be BDD but admits two important properties: First, the sets of existential atoms produced by T and by T 𝑁 𝐹 on any instance coincide (Lemma 48). Second, it is straightforward to find the mentioned bound on the number of ancestors for every atom produced by T 𝑁 𝐹 (Lemma 57). These two properties grant us Theorem 1. But how does such a normalization work? In simple words, it relies on the fact that T is BDD. In the absence of both disconnected and Datalog rules, the normalization would be rather simple: we could take any existential rule 𝛽 ⇒ 𝛼 ∈ T and replace it with rules 𝛾 ⇒ 𝛼 for all 𝛾 ∈ 𝑟𝑒𝑤 (𝛽). Dealing with disconnected bodies and Datalog rules complicates matters somewhat.

We are very confident that our proof can be generalized to all frontier-guarded BDD theories. As this is not yet spelled out in full detail, we prefer to be cautious and formulate it as conjecture.

Conjecture 2. Every frontier-guarded BDD theory is local.

THE FUS/FES CONJECTURE IS TRUE FOR LOCAL THEORIES

We proceed by presenting the second of our three main results.

Theorem 2. If a theory T is FES and local then it is UBDD.

This means that the FUS/FES conjecture holds for local theories. Before we start our proof, let us note that by Theorem 1 and Theorem 2, we can immediately conclude that Conjecture 1 holds for theories over binary signatures: Corollary 1. If a theory T over a binary signature is both FES and BDD then it is UBDD. Also, Theorem 1 implies that any counterexample to the conjecture -should it exist -would have to be outside the realm of local classes. We explore this uncharted lands in Section 11.

Proof of Theorem 2

As any UBDD theory is core-terminating as well, it is easy to see that a theory T is UBDD if and only if there exists some 𝑐 T ∈ N such that 𝐶𝑜𝑟𝑒 (T , D) ⊆ Ch 𝑐 T (T , D) holds for any instance D. Note that the numbers 𝑐 T here and in Definition 12 are equal. Thus we can reformulate Theorem 2 as follows:

Theorem 2 (alternative). Let T be a core-terminating local theory. Then there exists a 𝑐 T ∈ N such that 𝐶𝑜𝑟𝑒 (T , D) ⊆ Ch 𝑐 T (T , D) holds for any instance D .

Until the end of this section, we will consider T a fixed theory that is both core-terminating and local (so also BDD). To simplify notation, Ch(T , D) will be shortened to Ch(D).

Definition 24. For an instance D define I D as the family of sets

{F | F ⊆ D, |F| ≤ 𝑙 T }. Define C D = F∈I D 𝐶𝑜𝑟𝑒 (T , F).
Lemma 25. There exists a 𝑘 T ∈ N depending only on T (but not on D), such that C D ⊆ Ch 𝑘 T (D).

Proof. The set

A = {F | |F| ≤ 𝑙 T } of all instances (over Σ) of size at most 𝑙 T is finite (up to isomorphisms). Recall that T is core-terminating and let 𝑘 T = max{𝑐 T,D | D ∈ A}. □
If we were able able to find a homomorphism hD from 𝐶ℎ(D) to C D , the alternative formulation of Theorem 2 would be proved. Also, since T is core-terminating, we know that for each F ∈ I D there exists a homomorphism ℎ F from 𝐶ℎ(F) to C D and we know that F∈I D 𝐶ℎ(F) = 𝐶ℎ(D). So can't we just define hD = F∈I D ℎ F ? Unfortunately not, because the domains of ℎ F and ℎ F ′ may overlap (for some F ≠ F ′ ) and there is no guarantee that ℎ F and ℎ F ′ will agree on the terms that are in both domains. If hD could be produced this way, C D |= T would always hold. Yet, we found an example (not included here) of a pair D, T for which C D ̸ |= T .

Luckily, the idea to build a global homomorphism hD using the local homomorphisms ℎ F can be put to use in a different way, and the set of facts C D will indeed prove very useful in this context. The following lemma will be crucial in this endeavor: Lemma 26. For any instance D there exists a homomorphism hD from 𝐶ℎ(D) to 𝐶ℎ(D) such that for each 𝑡 ∈ 𝑑𝑜𝑚(𝐶ℎ(D)) there is

hD (𝑡) ∈ 𝑑𝑜𝑚(C D ).
Let us first discuss how Theorem 2 can be concluded from Lemma 26. Suppose some D is fixed and hD is a homomorphism as in Lemma 26. We know that 𝑡 ∈ 𝑑𝑜𝑚(𝐶ℎ(D)) implies hD (𝑡) ∈ 𝑑𝑜𝑚(C D ) and we know that C D ⊆ 𝐶ℎ 𝑘 T (D). So one might be tempted to immediately conclude hD (Ch(D)) ⊆ 𝐶ℎ 𝑘 T (D). But it is not quite that simple. Admittedly, Lemma 26 tells us that all the terms of hD (Ch(D)) will indeed appear in 𝐶ℎ 𝑘 T (D). But it says nothing like that about the atoms of hD (Ch(D)). Rather, it might be that there are atoms in hD (Ch(D)) that, despite having all their terms in 𝑑𝑜𝑚(C D ) are not themselves in C D . To overcome this little problem, we recall Observation 14 and let 𝑐 T = 𝑘 T +𝑛 𝑎𝑡 . Then hD (Ch(D)) ⊆ 𝐶ℎ 𝑐 T (D) follows as desired.

This means what remains to be presented in this section is the proof of Lemma 26: Definition 27. Let D be a set of facts and let F ⊆ D. We let 𝑀 F denote3 the substructure of Ch(D) induced by the set of terms 𝑑𝑜𝑚(Ch(D)) \ 𝑑𝑜𝑚(Ch(F)) \ 𝑑𝑜𝑚(𝐶𝑜𝑟𝑒 (T , F)) .

In the following, the terms of 𝑑𝑜𝑚(Ch(F)) \ 𝑑𝑜𝑚(𝐶𝑜𝑟𝑒 (T , F) will be referred to as banned terms. In the following, the atom 𝑎𝑝𝑝𝑙 (𝜌, 𝜎) will be mentioned often enough to deserve a shorter name, so we will call it 𝛼.

It is now sufficient (and necessary) to prove that there exists a homomorphism from 𝛼 to some atom 𝛼 ′ ∈ 𝑀 F , that is the identity on fr (𝛼). In other words, we need to show that if the body of the rule 𝜌 matches 𝑀 F (via mapping 𝜎), then we can find an atom in 𝑀 F that witnesses satisfaction of 𝜌. Such an 𝛼 ′ needs to have the same terms as 𝛼 in the frontier positions and may have arbitrary terms in the positions of the existentially quantified variables in ℎ𝑒𝑎𝑑 (𝜌), except that if 𝛼 had equal terms on two such positions then the respective terms in 𝛼 ′ must also be equal.

If 𝛼 ∈ 𝑀 F then of course we pick 𝛼 ′ = 𝛼. So, for the rest of the proof, assume 𝛼 ∉ 𝑀 F . Note that the only reason for 𝛼 to be in Ch(D) but not in 𝑀 F is that 𝛼 contains some banned term 𝑡.

But 𝜎 (𝑏𝑜𝑑𝑦 (𝜌)) ⊆ 𝑀 F . Thus fr (𝛼) ⊆ 𝑑𝑜𝑚(𝑀 F ) and so 𝑡 ∉ fr (𝛼). At this point, we can be sure that 𝜌 is not a Datalog rule -atoms derived via a Datalog rule do not have non-frontier terms.

Term 𝑡 being a non-frontier term of 𝛼 means that 𝛼 is the birth atom of 𝑡 in Ch(D). But 𝑡 ∈ 𝑑𝑜𝑚(Ch(F)) so from Observation 9, we know that 𝛼 is the birth atom of 𝑡 in Ch(F) and thus 𝛼 ∈ Ch(F).

Note This means that one can compose such homomorphisms, and the resulting function will also be a homomorphism from Ch(D) to Ch(D) (and it will be the identity on 𝑑𝑜𝑚(D), since each ℎ 𝑀 F is). Now the rabbit is going to be pulled out of the hat: let us compose all homomorphisms ℎ 𝑀 F ∈ H D , in any order. Call the resulting ("global") homomorphism hD . Now recall that the proof of Lemma 26 (and thus also of Theorem 2) will be finished once we can show that hD (𝑡) ∈ 𝑑𝑜𝑚(C D ) does indeed hold for each term 𝑡 ∈ 𝑑𝑜𝑚(𝐶ℎ(D)).

Recall our notion of banned terms. Now F is no longer fixed, i.e., for each F ∈ I D there is a set 𝑏𝑎𝑛 F of terms that occur somewhere in Ch(F) but not in 𝐶𝑜𝑟𝑒 (T , F). Each ℎ * 𝑀 F ∈ H D is the identity on all terms except those of 𝑏𝑎𝑛 F , and maps the terms from 𝑏𝑎𝑛 F into 𝑑𝑜𝑚(𝐶𝑜𝑟𝑒 (T , F)), which means into 𝑑𝑜𝑚(C D ).

Now suppose we apply hD to any 𝑡 ∈ 𝑑𝑜𝑚(𝐶ℎ(D)). If there is any ℎ

* 𝑀 F ∈ H D with ℎ * 𝑀 F (𝑡) ≠ 𝑡 then of course hD (𝑡) ∈ 𝑑𝑜𝑚(C D ). In case ℎ * 𝑀 F (𝑡) = 𝑡 for each ℎ * 𝑀 F , consider any F 𝑡 ∈ I D for which 𝑡 ∈ 𝑑𝑜𝑚(𝐶ℎ(F 𝑡 )). Then 𝑡 ∈ 𝑑𝑜𝑚(𝐶𝑜𝑟𝑒 (T , F 𝑡 )) ⊆ 𝑑𝑜𝑚(C D ).

SLIGHTLY BEYOND LOCALITY: STICKY THEORIES

Unfortunately, our notion of locality fails to characterize the entire BDD class, as demonstrated in the following example.

Example 30. Let 𝐸 be a relation of arity 4 and 𝑅 one of arity 2. Read 𝐸 (𝑎, 𝑏, 𝑏 ′ , 𝑐) as "𝑎 sees an edge from 𝑏 to 𝑏 ′ colored with color 𝑐" and 𝑅(𝑎, 𝑐) as "𝑎 considers 𝑐 a color". The following one-rule sticky theory T is not local: 𝐸 (𝑥, 𝑦, 𝑦 ′ , 𝑡), 𝑅(𝑥, 𝑡 ′ ) ⇒ ∃𝑦 ′′ 𝐸 (𝑥, 𝑦 ′ , 𝑦 ′′ , 𝑡 ′ ) (meaning "if 𝑥 sees an edge from 𝑦 to 𝑦 ′ and considers 𝑡 ′ a color, then 𝑥 must also see another edge from 𝑦 ′ to some 𝑦 ′′ of color 𝑡 ′ ").

To see that it is indeed not local, suppose it were and let 𝑙 T be the corresponding constant as in Definition 22. Now take an instance D consisting of 𝑙 T +1 atoms: one atom 𝐸 (𝑎, 𝑏 1 , 𝑏 2 , 𝑐 1 ) and atoms 𝑅(𝑎, 𝑐 𝑖 ) for 1 ≤ 𝑖 ≤ 𝑙 T . It is not hard to see that there are atoms in 𝐶ℎ(T , D) that require all the atoms from D to be produced.

The only reason, however, for connected sticky theories to be non-local are high-degree vertices, like the 𝑎 in the example. This leads to a natural generalization of the notion of locality: Definition 31. A theory T will be called bounded-degree local (or bd-local) if for any 𝑘 ∈ N there exists a constant 𝑙 T (𝑘) such that for every instance D having degree at most 𝑘, the following holds:

F⊆D, |F | ≤𝑙 T (𝑘) Ch(T , F) = Ch(T , D)
As of yet, we have been unable to show that the FUS/FES conjecture holds for bounded-degree local theories, but we believe that with some additional effort, the ideas from Section 9 could probably be adapted to work also for such theories. And of course they do work if only instances of fixed degree are considered.

It is not hard to show that sticky theories are indeed bd-local (cf. Appendix E). Hence, in view of Conjecture 2, it seems that most known decidable BDD classes are bounded-degree local. Perhaps surprisingly, unlike local theories, not all bounded-degree local theories are BDD:

Example 32. It is easy to see that the following single-rule theory is bounded-degree local but not BDD: 𝐸 (𝑥, 𝑦, 𝑧), 𝑅(𝑥, 𝑧) ⇒ 𝑅(𝑦, 𝑧).

But even if not all bd-local theories are BDD, it is not straightforward to come up with a BDD theory that is not bd-local. So a natural question arises: are there BDD theories that are not local in this generalized sense? We found it quite surprising to realize that the answer is positive:

Example 33. The following BDD theory T 𝑐 is not bd-local:

𝐸 (𝑥, 𝑦) ⇒ ∃𝑥 ′ , 𝑦 ′ 𝑅(𝑥, 𝑦, 𝑥 ′ , 𝑦 ′ ) 𝑅(𝑥, 𝑦, 𝑥 ′ , 𝑦 ′ ), 𝐸 (𝑦, 𝑧) ⇒ ∃𝑧 ′ 𝑅(𝑦, 𝑧, 𝑦 ′ , 𝑧 ′ )
To prove that it is BDD one can notice that if T 𝑐 , D |= 𝜙 ( ā), for some D and some ā ∈ 𝑑𝑜𝑚(D) | ā | then 𝐶ℎ |𝜙 ( ȳ) | |= 𝜙 ( ā). In order to prove that it is not bd-local consider, for each 𝑛 ∈ N, the instance D 𝑛 consisting of atoms 𝐸 (𝑎 1 , 𝑎 2 ), 𝐸 (𝑎 2 , 𝑎 3 ) . . ., 𝐸 (𝑎 𝑛 , 𝑎 1 ). The degree of this instance is 2. And there are atoms in 𝐶ℎ 𝑛 (T 𝑐 , D 𝑛 ) that are not in 𝐶ℎ 𝑛 (T 𝑐 , F) for any proper subset F of D 𝑛 .

We were, however, not able to find an example of a theory that would be hereditary BDD -a BDD theory such that every its subsets is BDD as well -but not bd-local. We think it reasonable to conjecture that there are no such theories.

FAR BEYOND LOCALITY: BDD THEORIES WITHOUT SMALL REWRITINGS

As we know, any local theory is also BDD. Additionally, local theories admit rewritings of linear width:

Observation 34. For each local theory T and for each CQ Ψ, the size of the greatest disjunct in the rewriting is at most 𝑙 T |Ψ|.

Clearly, the linear bound on the width of 𝑟𝑒𝑤 (Ψ) gives us an immediate exponential upper bound on the number of its disjuncts. A matching lower bound is trivial to obtain: Observation 35. Let T consist of the two rules: 𝐸 (𝑥, 𝑦) ⇒ 𝑅(𝑥, 𝑦) and 𝐸 ′ (𝑥, 𝑦) ⇒ 𝑅(𝑥, 𝑦). Then T is BDD and the number of disjuncts in 𝑟𝑒𝑤 (Ψ) can be exponential in the size of Ψ.

Recall the notion of backwards shy theories [START_REF] Thomazo | Conjunctive Query Answering Under Existential Rules -Decidability, Complexity, and Algorithms[END_REF] -these are BDD theories such that, for every query 𝜓 ( ȳ) if 𝜙 ( ȳ) ∈ 𝑟𝑒𝑤 (𝜓 ( ȳ)) then only variables from ȳ can occur more than once in 𝜙 ( ȳ). Sticky theories are backward shy. It is easy to see that backward shy theories admit rewritings of linear width as well and, in consequence, also all sticky theories do. This is related to another notion of locality: Definition 36. We call a theory T distancing if there is a 𝑑 T ∈ N such that for any instance D, any 𝑐, 𝑐 ′ ∈ 𝑑𝑜𝑚(D), and any 𝑛 ∈ N if

𝑑𝑖𝑠𝑡 𝐶ℎ ( T,D) (𝑐, 𝑐 ′ ) ≤ 𝑛 then 𝑑𝑖𝑠𝑡 D (𝑐, 𝑐 ′ ) ≤ 𝑑 T 𝑛.
Is every BDD theory distancing? It might seem that this can be shown using Exercise 16. However, this is not the case, since the path from 𝑐 to 𝑐 ′ in 𝐶ℎ(T , D) might lead through atoms not containing any constants from the original D. What can be proven is the following correspondency: Observation 37. If a BDD theory admits rewritings of linear width, then it is distancing.

Assuming Conjecture 2, this implies that all theories from previously known BDD classes are distancing. The converse of Observation 37 does not hold, and such theories can be easily found: Observation 38. The theory consisting of the single Datalog rule 𝐴(𝑥), 𝐸 (𝑥, 𝑦) ⇒ 𝐴(𝑦) is distancing but not BDD.

So do there exist non-distancing BDD theories at all? Do there exist BDD theories that do not admit rewritings of linear width? The answer is given by Theorem 3, which constitutes the third main result of this paper: Theorem 3. There exists a BDD theory that is non-distancing and does not even admit rewritings of polynomial width.

To see how this is possible, consider the following theory: Definition 39. Consider a signature with two binary predicates 𝑅 and 𝐺. Let the theory T 𝑑 consist of the following rules: (loop) 𝑡𝑟𝑢𝑒 ⇒ ∃𝑥 𝑅(𝑥, 𝑥), 𝐺 (𝑥, 𝑥) (pins) ∀𝑥 (𝑡𝑟𝑢𝑒 ⇒ ∃𝑧, 𝑧 ′ 𝑅(𝑥, 𝑧), 𝐺 (𝑥, 𝑧 ′ )) (grid) 𝑅(𝑥, 𝑥 ′ ), 𝐺 (𝑥, 𝑢), 𝐺 (𝑢, 𝑢 ′ ) ⇒ ∃𝑧 𝑅(𝑢 ′ , 𝑧), 𝐺 (𝑥 ′ , 𝑧)

Note that the rules of T 𝑑 are not single-head and some of them have empty bodies. One could easily reformulate them to avoid this at the cost of readability (see Appendix D). We will think of instances over our signature (and of bodies of queries) as graphs with edges colored in red or green. For 𝑛 ∈ N, let 𝐺 𝑛 (𝑥 0 , 𝑥 𝑛 ) denote the CQ ∃𝑥 1 . . . 𝑥 𝑛-1 𝐺 (𝑥 0 , 𝑥 1 ), . . . , 𝐺 (𝑥 𝑛-1 , 𝑥 𝑛 ) and 𝑅 𝑛 (𝑥 0 , 𝑥 𝑛 ) likewise. Define conjunctive queries 𝜙 𝑛 𝑅 (𝑥, 𝑦) by ∃𝑥 ′ , 𝑦 ′ 𝑅 𝑛 (𝑥, 𝑥 ′ ), 𝑅 𝑛 (𝑦, 𝑦 ′ ), 𝐺 (𝑥 ′ , 𝑦 ′ ) and let G 𝑛 (𝑎, 𝑏) be a path of 𝑛 green edges, with 𝑎 as the first vertex and 𝑏 as the last.

The following technical lemma substantiates Theorem 3:

Lemma 40. (A) The theory T 𝑑 is BDD. (B) 𝐺 2 𝑛 (𝑥, 𝑦) ∈ 𝑟𝑒𝑤 T 𝑑 (𝜙 𝑛
𝑅 (𝑥, 𝑦)) holds for every 𝑛 ∈ N. Let us first prove claim (B) of the theorem, which implies that T 𝑑 is not distancing. The claim follows once we notice that: (i) Ch(T 𝑑 , G 2 𝑛 (𝑎, 𝑏)) |= 𝜙 𝑛 𝑅 (𝑎, 𝑏) and (ii) if D is a proper subset of G 2 𝑛 (𝑎, 𝑏) then 𝐶ℎ(T 𝑑 , D) ̸ |= 𝜙 𝑛 𝑅 (𝑎, 𝑏). Establishing (i) is immediate, as exemplified in Fig. 1 displaying the case 𝑛 = 3. To show (ii), we note that if D is a proper subset of G 2 𝑛 (𝑎, 𝑏) then 𝑎 and 𝑏 are in two different connected components of D and, since T 𝑑 is connected, they are in two different connected components of 𝐶ℎ(T 𝑑 , D). The proof of claim (A) is much harder (see Appendix B). It defines a rewriting procedure in the spirit of [START_REF] König | Sound, complete and minimal UCQ-rewriting for existential rules[END_REF][START_REF] Gottlob | Query rewriting and optimization for ontological databases[END_REF], whose termination for any given query 𝜙 (𝑦) is shown, via an invariant defined by a complicated multiset ordering.

As our final exercise illustrates, the reasons why T 𝑑 is BDD are quite subtle indeed: Exercise 41. Show that without rule (loop), T 𝑑 would not be BDD. Hint: Consider the CQ ∃𝑥, 𝑦 𝑅(𝑥, 𝑦), 𝐺 (𝑥, 𝑦).

A remark on Theorem 3. A folklore belief seems to be that the existence of BDD theories that enforce rewritings of unbounded width is a consequence of the the fact that it is undecidable to check if a theory is BDD (see e.g. a recent stackexchange post [START_REF] Krötzsch | What is first-order rewritable (and fo-query)?[END_REF]). Our results call this belief into question, because being BDD is undecidable for theories with a binary signature, and yet such theories, if BDD, are local and thus admit rewritings of linear width. Remark on distancing and linear width rewritings. One may ask whether distancing is the same as admitting rewritings of linear width. The answer is no. While Observation 37 shows one implication, the converse is not true. Consider theory T 𝑑 from Definition 39, but with every predicate's arity increased by one, and the new variable 𝑟 occurring in the last position in every atom. Then the new theory is distancing (unlike T 𝑑 ), but it still requires exponential size rewritings (and, of course, it will remain BDD).

CONCLUSIONS AND FUTURE WORK

Our major motivation to embark on this journey was the pending status of the FUS/FES conjecture. On our way, we realized that any progress in that direction requires to significantly advance our understanding of the BDD class, seperating folklore beliefs from hard facts. To this end, we introduced several new notions, characterizing specific properties of theories, and investigated their correspondencies. Most notably, we defined local theories, a BDD subclass. Our major results are the following:

• We show that the FUS/FES conjecture holds for all local theories (Theorem 2), which include all theories over binary signatures (Corollary 1). If the conjecture holds in the general case, then our work may provide the basis for a complete proof. If it does not, we now know that we must look for counter-examples of higher arity to disprove it. • We show that there are BDD theories that are non-distancing and even necessitate rewritings of exponential width (Theorem 3). This result highlights the limitations of existing BDD classes [START_REF] Calì | Advanced processing for ontological queries[END_REF][START_REF] Artale | The DL-Lite family and relations[END_REF][START_REF] Thomazo | Conjunctive Query Answering Under Existential Rules -Decidability, Complexity, and Algorithms[END_REF], which can only characterise rule sets that admit rewritings of polynomial width. As for future work, we intend to explore the following:

• Study the relation between distancing and bd-local. More precisely, find out if there are theories that are BDD and bd-local but are not distancing.

Appendices Appendix A PROOF OF THEOREM 1

Let us now fix a binary signature Σ and a BDD theory T over Σ. By T 𝐷𝐿 we will denote the Datalog rules of T and by T ∃ its proper existential rules.

First we will need to distinguish, among all elements of T ∃ , detached 4 rules that are of the form 𝜙 ( x) → ∃𝑦, 𝑧𝜓 (𝑦, 𝑧) or 𝜙 ( x) → ∃𝑦𝜓 (𝑦), that is, rules having empty frontier. Note that when firing a detached rule, the newly created atom, has no common terms with the rest of the chase. Notice that, since we only consider binary schemas, the non-empty frontier of an existential rule always consists of exactly one variable 5 . Rules from T ∃ which are not detached will be called sensible Clearly, whatever fact set D we consider, the structure Ch(T , D) is a disjoint union of three sets of atoms. One set consists of the original facts from D. Second contains existential atoms, that is facts created in the process of the chase, by rules of T ∃ . The third set consists of atoms that are created by the rules of T 𝐷𝐿 which be called Datalog atoms. We will denote the set of existential atoms of Ch(T , D) together with atoms of D with Ch ∃ (T , D).

Let us now concentrate on the structure of Ch ∃ (T , D). Notice that there are again two kinds of atoms there: detached atoms, created by detached rules and sensible atoms, created by sensible rules. Notice also that our taxonomy of atoms implies a taxonomy of the terms of Ch ∃ (T , D) (that is the elements of 𝑑𝑜𝑚(Ch(T , D)) \ 𝑑𝑜𝑚(D)): there are sensible terms, created by sensible rules and detached terms, created by detached rules. The set of detached terms will be called 𝑑𝑒𝑡 (Ch(T , D)).

Observation 42. The graph whose vertices are the terms from 𝑑𝑜𝑚(Ch(T , D)) and whose edges are sensible atoms of Ch ∃ (T , D) is a forest. The set of the roots of the trees of this forest is equal to 𝑑𝑜𝑚(D) ∪ 𝑑𝑒𝑡 (Ch(T , D)). The number of children of any of the vertices of this forest is bounded by the number of existential rules in T .

For any 𝑎 ∈ 𝑑𝑜𝑚(D) ∪ 𝑑𝑒𝑡 (Ch(T , D)) let S(𝑎) be the set of all atoms of Ch ∃ (T , D) which are edges of the tree rooted in 𝑎. Following the naming convention, we call trees that are rooted in detached terms detached trees.

A.1 First (failed) attempt at the Crucial Lemma

For any given set of facts D let a parent function 𝑝𝑎𝑟 T be any function from Ch(T , D) \ D to the power set of Ch(T , D) such that for any atom 𝛼 ∈ Ch(T , D) there exists a rule 𝜌 and a mapping 𝜎 satisfying:

• 𝛼 = 𝑎𝑝𝑝𝑙 (𝜌, 𝜎),

• 𝜎 (𝑏𝑜𝑑𝑦 (𝜌)) = 𝑝𝑎𝑟 T (𝛼).

The parent function points to some (arbitrarily chosen) set of atoms that leads to the creation of 𝛼. Note that there may be more than one such function as 𝛼 could be created in more than one way during the chase.

Let D be any set of facts and let 𝑝𝑎𝑟 T be some parent function. Then we define an ancestor function 𝑎𝑛𝑐 T as follows:

• 𝑎𝑛𝑐 T (𝛼) = {𝛼 } for an atom 𝛼 ∈ D,

• 𝑎𝑛𝑐 T (𝛼) = 𝛼 ′ ∈𝑝𝑎𝑟 T (𝛼) 𝑎𝑛𝑐 T (𝛼 ′ ) for atoms of Ch(T , D) \ D. Intuitively the set 𝑎𝑛𝑐 T (𝛼) consists of facts from D which were used during the chase, to prove 𝛼. Of course there might be more than one ancestor function for any given set of facts as that function is strictly associated with a particular parent function. This freedom in taking parents, and so in picking ancestors, leads to some problems, as we will soon discover.

We would be one step from proving Theorem 1 if we had:

Lemma 43 (Crucial Lemma, first attempt, false). There is a natural number 𝑀, depending on the rule set T but not on the fact set D, such that for every ancestor function 𝑎𝑛𝑐 T , for each constant and any detached term 𝑡 in Ch(T , D) holds:

𝛼 ∈S(𝑡 ) 𝑎𝑛𝑐 T (𝛼) ≤ 𝑀
But that lemma is unfortunately not true. For a counterexample see:

Example 44. Let T consist of two rules:

• 𝐸 (𝑥, 𝑦), 𝑅(𝑧, 𝑦) → ∃𝑣 𝐸 (𝑦, 𝑣) • 𝐸 (𝑥, 𝑦), 𝑃 (𝑧) → 𝑅(𝑧, 𝑦) Suppose that 𝑀 as in the lemma exists and that D consists of atom 𝐸 (𝑎 0 , 𝑎 1 ) and atoms 𝑃 (𝑏 𝑖 ) for each 1 ≤ 𝑖 ≤ 𝑀.

Then Ch(T , D) will consist of an infinite number of new facts 𝐸 (𝑎 1 , 𝑎 2 ), 𝐸 (𝑎 2 , 𝑎 3 ),𝐸 (𝑎 3 , 𝑎 4 ) . . .. In order to build them, however, some facts about relation 𝑅 will need to be proven by the second rule using a number of 𝑃 atoms from D. And it might happen (Skolem/semioblivious chase is non-deterministic in that aspect) that the proven 𝑅-facts will be 𝑅(𝑏 1 , 𝑎 1 ), 𝑅(𝑏 2 , 𝑎 2 ), . . . 𝑅(𝑏 𝑀 , 𝑎 𝑀 ), meaning that S(𝑎 1 ) uses during its creation all the 𝑀 + 1 facts of D. But of course this is for irrelevant reasons: the same chase could be built if 𝑃 (𝑏 1 ) was used each time some 𝑃 was needed.

A.2 The normalization of T

In order to circumvent the problems highlighted by Example 44, we will now transform the rule set T into another rule set T 𝑁 𝐹 which, apart from some other useful properties, will satisfy the equality

( * ) Ch ∃ (T 𝑁 𝐹 , D) = Ch ∃ (T , D).
First we will define the signature of T 𝑁 𝐹 . Let us take a fresh set of nullary predicates M = {𝑀 𝜙 | 𝜙 is a boolean CQ over Σ}. Then our new signature 6 Σ ′ is Σ ∪ M.

Two procedures will be used during the normalization: body rewriting and body separation.

Definition 45 (Body rewriting). Let 𝜌 be some rule with body 𝛽 ( x, ȳ) over Σ and a head 𝛾 ( ȳ) which is an atom from Σ ′ possibly preceded with the existential quantifier (or two). Then by 𝑅𝑒𝑤 (𝜌) we denote the set: 6 We briefly forget here about our promise that signatures would be finite.

{𝛽 ′ ( x, ȳ) ⇒ 𝛾 ( ȳ) : 𝛽 ′ ( x, ȳ) ∈ 𝑟𝑒𝑤 T (∃ x 𝛽 ( x, ȳ))}
While body rewriting can be applied both to existential rules and Datalog rules, the second procedure will only be applied to existential rules. It separates the disconnected fragment of body of given existential rule and "encapsulates" that fragment in a single nullary predicate from M. That is, given a rule, the procedure returns a pair of rules. One being almost the original rule, but with its body changed to consist of nullary predicate and a connected conjunction of atoms. The second being a rule whose job is to prove the aforementioned nullary predicate.

Definition 46 (Body separation). If 𝜌 is an existential rule of the form 𝛽 ( x, ȳ) ∧ 𝜙 ( z) ⇒ ∃ ū𝛾 ( ȳ, ū) such that:

• ( x ∪ ȳ) ∩ z = ∅, • 𝛽 ( x, ȳ) is connected, then • 𝑠𝑒𝑝 𝑐𝑐 (𝜌) = 𝛽 ( x, ȳ) ∧ 𝑀 𝜙 ⇒ ∃ ū 𝛾 ( ȳ, ū) • 𝑠𝑒𝑝 𝑀 (𝜌) = 𝜙 ( z) ⇒ 𝑀 𝜙
If the body of 𝜌 is connected, we assume that 𝜙 ( z) is empty. And we have a nullary predicate 𝑀 ∅ ∈ Σ ′ for this occasion.

The normalization algorithm is performed in three steps:

Normalization Algorithm

Step One:

T 𝐼 = 𝜌 ∈T ∃ 𝑅𝑒𝑤 (𝜌)
Step two:

T 𝐼 𝐼 = {𝑠𝑒𝑝 𝑐𝑐 (𝜌) : 𝜌 ∈ T 𝐼 }
Step three: T 𝐼 𝐼 𝐼 = 𝜌 ∈T 𝐼 𝑅𝑒𝑤 (𝑠𝑒𝑝 𝑀 (𝜌))

Return: T 𝑁 𝐹 = T 𝐼 𝐼 ∪ T 𝐼 𝐼 𝐼
The normalization allows us to attack the source of the problem highlighted in the previous section by separating the "disconnected ancestors" required by existential rules and encapsulating those ancestors within rules producing nullary predicates.

Observation 47. Let 𝜌 be a rule that creates a detached atom in Ch(T 𝑁 𝐹 , D) for some fact set D. Then 𝜌 is a rule from T 𝐼 𝐼 and its body consists of a single nullary atom.

Lemma 48. For any set of facts D over Σ:

Ch ∃ (T , D) = Ch ∃ (T 𝑁 𝐹 , D)
Here, our choice of the Skolem naming convention can be explained. We want to show equality of the structures in Lemma 48 and so if we choose our Skolem naming convention to be dependent on rule names then Lemma 48 would obviously be false.

A.3 Proof of Lemma 48

This entire subsection is devoted to the proof of Lemma 48, which will follow directly from Lemma 52 and Lemma 55. But first, as a warm-up, notice that: Exercise 51. Suppose (∃ t, ū 𝜙 ( t, ȳ) ∧ 𝛾 ( ū)) ∈ 𝑟𝑒𝑤 T (∃ x𝛽 ( x, ȳ)) for some CQs 𝜙, 𝛾 and 𝛽, where the tuples of variables t ∪ ȳ and ū are disjoint. And suppose ∃v 𝜁 ( v) ∈ 𝑟𝑒𝑤 T (∃ ū 𝛾 ( ū)). Then there exists a query ∃z 𝜚 ( z, ȳ)

∈ 𝑟𝑒𝑤 T (∃ x𝛽 ( x, ȳ)) which is contained in (∃ t, v 𝜙 ( t, ȳ) ∧ 𝜁 ( v)). Hint: Let database D be a frozen body of ∃ t, v 𝜙 ( t, ȳ) ∧ 𝜁 ( v) and observe that D |= 𝑟𝑒𝑤 T (∃ x 𝛽 ( x, ȳ))
Notice that the only existential rules in T 𝑁 𝐹 are the ones in T 𝐼 𝐼 . Notice also that the only Datalog rules in T 𝑁 𝐹 are the ones in T 𝐼 𝐼 𝐼 and hence the only atoms which are in Ch(T 𝑁 𝐹 , D) but not in Ch ∃ (T 𝑁 𝐹 , D) are the nullary atoms from the set M.

By Ch 𝑖,∃ (T , D) we denote the intersection of Ch 𝑖 (T , D) and Ch ∃ (T , D).

Lemma 52. For each fact set D over Σ and each 𝑘 ∈ N:

Ch 𝑘,∃ (T 𝑁 𝐹 , D) ⊆ Ch ∃ (T , D).
Proof. We will show this by induction on 𝑘. The case for 𝑘 = 0 is trivial. Assume the claim is true for some 𝑘 ∈ N. We are going to show that it is also true for 𝑘 + 1.

Let 𝛼 be an atom from Ch 𝑘+1,∃ (T 𝑁 𝐹 , D), which is not in Ch 𝑘,∃ (T 𝑁 𝐹 , D). Then 𝛼 = 𝑎𝑝𝑝𝑙 (𝜌 𝛼 , 𝜎 𝛼 ) for some:

-𝜌 𝛼 ∈ T 𝐼 𝐼 , the rule which actually created 𝛼, of the form 𝜙 ( t, ȳ) ∧ 𝑀 𝛾 ⇒ ∃z 𝛼 0 ( ȳ, z), -𝜎 𝛼 such that 𝜎 𝛼 (𝜙 ( t, ȳ)) ⊆ Ch 𝑘,∃ (T 𝑁 𝐹 , D), (♥) -𝑀 𝛾 such that Ch 𝑘,∃ (T 𝑁 𝐹 , D) |= 𝑀 𝛾 .

It follows from the construction of T 𝑁 𝐹 that there must exist:

(1) A rule 𝜌 ′ ∈ T 𝐼 of the form:

𝜙 ( t, ȳ) ∧ 𝛾 ( ū) ⇒ ∃z 𝛼 0 ( ȳ, z) which, by
Step II of the normalization algorithm, led to the creation of 𝜌 𝛼 , such that the tuple ū of variables is disjoint with ȳ and with t, and that 𝜙 ( t, ȳ) is a connected query.

(2) A rule 𝜌 ∈ T ∃ of the form:

𝛽 ( x, ȳ) ⇒ ∃z 𝛼 0 ( ȳ, z)
which, by Step I of the normalization algorithm, led to the creation of 𝜌 ′ , such that:

(∃ t, ū 𝜙 ( t, ȳ) ∧ 𝛾 ( ū)) ∈ 𝑟𝑒𝑤 T (∃ x 𝛽 ( x, ȳ)) (♣) (3) A rule 𝜌 𝑀 𝛾 in T 𝐼 𝐼 𝐼 of the form 𝜁 ( ū) ⇒ 𝑀 𝛾 such that ∃ ū 𝜁 ( ū) ∈ 𝑟𝑒𝑤 T (∃ ū 𝛾 ( ū)
) and a substitution 𝜎 𝜁 from the variables in ū to 𝑑𝑜𝑚(Ch 𝑘-1,∃ (T 𝑁 𝐹 , D)) such that 𝜎 𝜁 (𝜁 ( ū)) ⊆ Ch 𝑘-1,∃ (T 𝑁 𝐹 , D). This is because, for 𝜌 𝛼 to be applicable in Ch 𝑘,∃ (T 𝑁 𝐹 , D), there must be Ch 𝑘,∃ (T 𝑁 𝐹 , D) |= 𝑀 𝛾 , and since D ̸ |= 𝑀 𝛾 , a rule able to produce 𝑀 𝛾 must have earlier been applied.

In order to complete the induction step, we need to show that 𝛼 ∈ Ch ∃ (T , D). Since 𝜌 is a rule of T this claim will follow once we can prove that:

Ch ∃ (T , D) |= ∃ x 𝛽 ( x, 𝜎 𝛼 ( ȳ)) (♦)
And (♦) will follow (using Exercise 49) once we can show that for some query 𝜚 ( ȳ) ∈ 𝑟𝑒𝑤 T (∃ x 𝛽 ( x, ȳ)) there is:

Ch ∃ (T , D) |= 𝜚 (𝜎 𝛼 ( ȳ)) (♠)
Recall that from (♥) we know that:

Ch 𝑘,∃ (T 𝑁 𝐹 , D) |= ∃ t 𝜙 ( t, 𝜎 𝛼 ( ȳ)).
By hypothesis this implies that:

Ch ∃ (T , D) |= ∃ t 𝜙 ( t, 𝜎 𝛼 ( ȳ)).
The claim (♠) would be now proven, using (♣), if we could also show that:

Ch ∃ (T , D) |= ∃ ū 𝛾 ( ū),
But this may not be the case. All we know is that:

Ch 𝑘,∃ (T 𝑁 𝐹 , D) |= ∃ ū 𝜁 ( ū)
and therefore (using the hypothesis again) that:

Ch ∃ (T , D) |= ∃ ū 𝜁 ( ū).
So we get that Ch ∃ (T , D) |= ∃s, t 𝜙 ( t, 𝜎 𝛼 ( ȳ)) ∧ 𝜁 (s). Now use Exercise 51 to get (♠). □

The proof of the following lemma seems overly complicated. Why doesn't it just follow from Exercise 50? This is because, while we assume that T is BDD, we never proved that T 𝑁 𝐹 is BDD too. Lemma 53. Suppose Ch(T 𝑁 𝐹 , D) |= 𝑀 𝜙 for some nullary fact 𝑀 𝜙 . Then 𝐶ℎ 1 (T 𝑁 𝐹 , D) |= 𝑀 𝜙 .

Proof. Suppose Ch(T 𝑁 𝐹 , D) |= 𝑀 𝜙 and let 𝛽 ( x) be the body of the rule from T 𝐼 𝐼 𝐼 that created 𝑀 𝜙 .

Recall that 𝛽 ( x) does not contain nullary predicates and that T 𝑁 𝐹 consists only of existential rules (from T 𝐼 𝐼 ) and of Datalog rules that prove nullary facts (from T 𝐼 𝐼 𝐼 ). This means that Ch ∃ (T 𝑁 𝐹 , D) |= ∃ x 𝛽 ( x). Now we can use Lemma 52 and get: Ch ∃ (T , D) |= ∃ x 𝛽 ( x). Now recall that ∃ x 𝛽 ( x) ∈ 𝑟𝑒𝑤 T (𝜙). From Exercise 50 we get that there exists another boolean query 𝛽 0 such that 𝛽 0 ∈ 𝑟𝑒𝑤 T (𝜙) and that D |= 𝛽 0 . And from this we can immediately conclude that Ch Let 𝛼 be an atom produced by an existential rule during the 𝑖 + 1-th step of Ch(T , D). Let a rule 𝜌 ∈ T and a mapping 𝜎 be such that 𝛼 = 𝑎𝑝𝑝𝑙 (𝜌, 𝜎) and let 𝛾 ( x, ȳ) be a body of 𝜌 where ȳ are the frontier variables.

While we know that Ch 𝑖 (T , D) |= 𝜎 (𝛾 ( x, ȳ)) we are not sure if Ch 𝑖,∃ (T , D) |= 𝜎 (𝛾 ( x, ȳ)): some of the atoms in 𝜎 (𝛾 ( x, ȳ)) could be produced by Datalog rules of T .

But 𝐶ℎ(T , D) = 𝐶ℎ(T , Ch 𝑖,∃ (T , D)), so if Ch 𝑖 (T , D) |= 𝜎 (𝛾 ( x, ȳ)) then we can be sure that there exists a query ∃z𝛽 ( z, ȳ) ∈ 𝑟𝑒𝑤 T (∃ x𝛾 ( x, ȳ)) such that Ch 𝑖,∃ (T , D) |= ∃z𝛽 ( z, σ (𝑦)) or, in other words, Ch 𝑖,∃ (T , D) |= 𝛽 (𝜎 𝛽 ( z), σ ( ȳ)) for some substitution 𝜎 𝛽 .

Observe that from the induction hypothesis we know that Ch 𝑖+2,∃ (T 𝑁 𝐹 , D) |= 𝛽 (𝜎 𝛽 ( z), σ ( ȳ)).

Let now 𝜌 ′ be the rule from T 𝑁 𝐹 (or, to be more precise, from T 𝐼 𝐼 ), such that ℎ𝑒𝑎𝑑 (𝜌 ′ ) = ℎ𝑒𝑎𝑑 (𝜌) and that the body of 𝜌 ′ is of the form 𝛽 0 ( ū, ȳ) ∧ 𝑀 𝜙 , where 𝛽 ( z, ȳ) = 𝛽 0 ( ū, ȳ) ∧ 𝜙 ( v) for some v disjoint from ū ∪ ȳ. It follows from the construction of T 𝑁 𝐹 that such a 𝜌 ′ exits.

Let us consider the second case. Note that Ch 𝑖+2,∃ (T 𝑁 𝐹 , D) |= 𝜎 𝛽 (𝛽 ′ ( x, ȳ)) and so all we need to show in order to complete our induction step is that Ch 𝑖+2 (T 𝑁 𝐹 , D) |= 𝑀 𝜙 .

Clearly Ch 𝑖+2,∃ (T 𝑁 𝐹 , D) |= ∃z𝜙 ( z) as we know that 𝜙 ⊆ 𝛽. From this we can conclude that D |= 𝑟𝑒𝑤 T (𝜙) and thus 𝑀 𝜙 ∈ Ch 2,∃ (T 𝑁 𝐹 , D).

This ends the proof of Lemma 55 and therefore of Lemma 48. □ Note that this implies that the sensible and non-nullary atoms of Ch(T 𝑁 𝐹 , D) form a set of trees having a tree S(𝑡) for each term 𝑡 that is a constant of D or detached term of Ch ∃ (T 𝑁 𝐹 , D). And that this set of trees is exactly this same set of trees as in the case of rule set T . Also, note that having Lemma 48 we get a very important: A. [START_REF] König | Sound, complete and minimal UCQ-rewriting for existential rules[END_REF] The Crucial Lemma

In this section, we state and prove the Crucial Lemma. Recall, that we want to prove, that for any term 𝑡 being a constant of D or a detached term of Ch ∃ (T 𝑁 𝐹 , D), the tree S(𝑡) rooted in 𝑡 and consisting of sensible atoms of Ch ∃ (T 𝑁 𝐹 , D) requires only a small subset of D to be built by the chase Ch(T 𝑁 𝐹 , D). First let us distinguish, among the parents and ancestors of some atom in Ch(T 𝑁 𝐹 , D), its connected parents and connected ancestors: given some parent function 𝑝𝑎𝑟 T 𝑁 𝐹 for Ch(T 𝑁 𝐹 , D) and an atom 𝛼 of Ch(T 𝑁 𝐹 , D) we define the set of connected parents 𝑐𝑝𝑎𝑟 (𝛼) as the set of all the non-nullary atoms of 𝑝𝑎𝑟 T 𝑁 𝐹 (𝛼). Then for atoms of Ch(T 𝑁 𝐹 , D) we define their respective sets of connected ancestors as follows:

• 𝑐𝑎𝑛𝑐 (𝛼) = {𝛼 } for an atom 𝛼 ∈ D,

• 𝑐𝑎𝑛𝑐 (𝛼) = 𝛼 ′ ∈𝑐𝑝𝑎𝑟 (𝛼) 𝑐𝑎𝑛𝑐 (𝛼 ′ ), otherwise.

Before proceeding, let us define a number of measures, depending on T 𝑁 𝐹 .

• Let 𝑘 be the number of nullary predicates in T 𝑁 𝐹 .

• Let ℎ be the maximal number of atoms in the body of a rule from T 𝑁 𝐹 . • Let 𝑛 be the number of rules in T 𝑁 𝐹 .

• Let 𝑁 be the number of elements of a full 𝑛-ary tree of depth ℎ.

• Let 𝑀 = 𝑁ℎ + 𝑘ℎ Now having prepared everything we are going to prove the Crucial Lemma: Lemma 57 (crucial). For every set of facts D, every term 𝑡 that is constant of D or detached term of Ch ∃ (T 𝑁 𝐹 , D) and every ancestor function 𝑎𝑛𝑐 T 𝑁 𝐹 :

𝛼 ∈S(𝑡 ) 𝑎𝑛𝑐 T 𝑁 𝐹 (𝛼) ≤ 𝑀 Notice that we now count ancestors with respect to T 𝑁 𝐹 instead of ancestors with respect to T . This is, in fact, the only difference between this lemma and the (false) Lemma 43.

Proof. The atoms of S(𝑡) are all produced by the rules of T 𝐼 𝐼 . Recall that bodies of those rules consist of one connected 𝐶𝑄 and one nullary atom. The number of atoms that are ancestors of nullary atoms can easily be bounded by 𝑘ℎ using Lemma 53.

What is left to be bound is the number of connected ancestors of S(𝑡). Recall that for 𝑡 ∈ 𝑑𝑜𝑚(D) ∪ 𝑑𝑒𝑡 (Ch(T 𝑁 𝐹 , D)) the set of facts S(𝑡) is a tree with 𝑡 as its root. This gives us a natural notion of depth of atoms in S(𝑡), with atoms containing 𝑡 being at depth one.

First we will consider the easier case when 𝑡 ∈ 𝑑𝑒𝑡 (Ch(T , D)). Then S(𝑡) is a detached tree, not connected by atoms of Ch(T 𝑁 𝐹 , D)) to D. Moreover the connected parents and connected ancestors are defined in such a way that every atom is in one connected component of Ch(T 𝑁 𝐹 , D)) with all its connected ancestors. So, no atom in S(𝑡) has any connected ancestors, and thus the entire S(𝑡) has in total at most 𝑘ℎ ancestors.

Let us now move to the case when 𝑡 ∈ 𝑑𝑜𝑚(D). Clearly, to be a connected ancestor of someone in S(𝑡) an atom in D must be a connected parent of someone in S(𝑡): Observe that, if an application of an existential rule 𝜌 created an atom at depth greater than ℎ then the connected part of the body 𝜌, of size at most ℎ, could not "reach" the atoms of D. From this we get 𝑁ℎ as bound for the number of connected ancestors of S(𝑡) which implies that 𝑀 is a bound on the number of ancestors of S(𝑡) for any 𝑡. Proof. From Observation 14 the size of D ′ can easily be bounded by ℎ 𝑛 𝑎𝑡 where ℎ is the maximal number of atoms in a rule of T and 𝑛 𝑎𝑡 is the constant from Observation 14. □ Thus 𝑀𝑑 T is a locality constant for Datalog atoms of Ch(T , D). This concludes the proof of Theorem 1.

It follows from the above lemma that each S 𝑖 satisfies Condition (♠). What we still need to show is that the process terminates: at some point we will get S 𝑖 without live queries. To this end, we are going to use ranks.

B.2 High-level proof of claim (A).

Termination.

For a marked query 𝑄 and an atom 𝛼 ∈ 𝑄 G the edge rank 𝑒𝑟𝑘 (𝛼, 𝑄) will be defined (Definition 75) as some natural number, reflecting "the minimal cost of hiking from a marked variable to 𝛼". Then we will prove that:

Lemma 66. Suppose a marked query 𝑄 ′ is returned as a result of applying one of the five operations to 𝑄. Then:

(i) If the operation is cut-red or fuse-red then |𝑄 R | > |𝑄 ′ R |. (ii) If the operation is cut-green then |𝑄 R | = |𝑄 ′ R | and for each 𝛼 ∈ 𝑄 G there is 𝑒𝑟𝑘 (𝛼, 𝑄) ≥ 𝑒𝑟𝑘 (𝛼, 𝑄 ′ ). (iii) If the operation is fuse-green then |𝑄 R | > |𝑄 ′ R | or |𝑄 R | ≥ |𝑄 ′ R | and 𝑒𝑟𝑘 (𝛼, 𝑄) ≥ 𝑒𝑟𝑘 (𝛼, 𝑄 ′ ) for each 𝛼 ∈ 𝑄 G .
(iv) If the operation is reduce and if 𝛼 ∈ 𝑄 G is the green atom removed by the operation and if 𝛼 ′ ∈ 𝑞(𝑄 ′ ) is any of the two green atoms added by the operation then:

(a) |𝑄 R | = |𝑄 ′ R |; (b) 𝑒𝑟𝑘 (𝛼 ′ , 𝑄 ′ ) < 𝑒𝑟𝑘 (𝛼, 𝑄); (c) if 𝛽 ∈ 𝑄 G ∩ 𝑄 ′ G then 𝑒𝑟𝑘 (𝛽, 𝑄 ′ ) ≤ 𝑒𝑟𝑘 (𝛽, 𝑄).
Recall that all the operations except for reduce will decrease the number of variables and of atoms in 𝑄. Multisets. Using Lemma 66 we are going to prove that our process indeed terminates. To this end we borrow a technique from the term rewriting community. We will use the notation {. . .} 𝑚 to denote a multiset. 𝑀 (𝐴) will denote the family of all finite multisets with elements from 𝐴. By < 𝑚 we will denote the (strict) mutiset ordering on 𝑀 (N). By R we will mean the set of all possible pairs ⟨𝑘, 𝐴⟩ where 𝑘 ∈ N and 𝐴 ∈ 𝑀 (N). For ⟨𝑘, 𝐴⟩, ⟨𝑘 ′ , 𝐴 ′ ⟩ ∈ R define ⟨𝑘, 𝐴⟩ < R ⟨𝑘 ′ , 𝐴 ′ ⟩ if 𝑘 < 𝑘 ′ , or 𝑘 = 𝑘 ′ and 𝐴 < 𝑚 𝐴 ′ . Finally, let < 𝑀 be the (strict) multiset ordering on 𝑀 (R). It is well known ( [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF]) that (♥) if 𝐴 is well-ordered then the multiset ordering on 𝑀 (𝐴) is also a well-ordering. So < 𝑚 is a well-ordering. In consequence < R , which is the lexicographic ordering on the Cartesian product of two well-ordered sets is a well-ordering too. And, again using (♥), we get that < 𝑀 is a well-ordering. Definition 67.

• For a marked query 𝑄 define its rank

𝑞𝑟𝑘 (𝑄) ∈ R as ⟨|𝑄 R |, {𝑒𝑟𝑘 (𝛼, 𝑄) : 𝛼 ∈ 𝑄 G } 𝑚 ⟩.
• For a set of marked queries S define its rank 𝑠𝑟𝑘 (S) ∈ 𝑀 (R)

as the multiset {𝑞𝑟𝑘 (𝑄) : 𝑄 ∈ S} 𝑚 . Now, since the set 𝑀 (R) is well-ordered by < 𝑀 , to prove termination of our process it is enough to show that whenever it produces two subsequent sets S 𝑖 and S 𝑖+1 there must be ( * ) 𝑠𝑟𝑘 (S 𝑖+1 ) < 𝑀 𝑠𝑟𝑘 (S 𝑖 ). But recall that S 𝑖+1 is S 𝑖 with one marked query, call it 𝑄, replaced by one of the five operations, with a set Q consisting of one or several marked queries. So (this is how the multiset ordering works) in order to show ( * ) it is enough to show that for each 𝑄 ′ ∈ Q we have 𝑄 ′ < R 𝑄.

But this follows immediately from Lemma 66, from the definition of the lexicographic ordering < R (if the operation in question is cut-red or fuse-red) and from the definition of the multiset ordering < 𝑚 (for the remaining three operations).

B.3 Proof of Lemma 40 (A).

Five operations. As promised, now we can define the five operations. Suppose 𝑄 = ⟨𝜙 ( ȳ), 𝑉 ⟩ is a live query and 𝑥 ∈ 𝑣𝑎𝑟 (𝑄).

Definition 69 (cut-red). Suppose 𝑥 is as in Lemma 68(i), with 𝐸 = 𝑅. Define cut-red(𝑄, 𝑥) as ⟨𝜙 ′ ( ȳ), 𝑉 (𝑄)⟩ where 𝜙 ′ ( ȳ) is created from 𝜙 ( ȳ) by removing the sole atom containing 𝑥.

Operation cut-green is defined in an analogous way.

Definition 70 (fuse-red). Let 𝑥, 𝑧 and 𝑧 ′ be as in Lemma 68 (iii), with 𝐸 = 𝑅. Then fuse-red(𝑄, 𝑥, 𝑧, 𝑧 ′ ) = ⟨𝜙 ′ ( ȳ), 𝑉 ⟩ where 𝜙 ′ ( ȳ) is 𝜙 ( ȳ) with all occurences of 𝑧 ′ renamed7 as 𝑧.

Operation fuse-green is defined in an analogous way.

Definition 71 (reduce). Suppose 𝑥 is as in Lemma 68 (ii). Let 𝜙 ′ ( ȳ) be a query obtained from 𝜙 ( ȳ) by removing atoms 𝑅(𝑥 𝑟 , 𝑥) and 𝐺 (𝑥 𝑔 , 𝑥) and replacing them with atoms 𝐺 (𝑥 ′ , 𝑥 ′′ ), 𝐺 (𝑥 ′′ , 𝑥 𝑟 ), 𝑅(𝑥 ′ , 𝑥 𝑔 ) where 𝑥 ′ and 𝑥 ′′ are fresh variables. Then define reduce(𝑄, 𝑥) as the set of four marked queries ⟨𝜙 ′ ( ȳ), 𝑉 (𝑄)⟩, ⟨𝜙 ′ ( ȳ), 𝑉 (𝑄) ∪ {𝑥 ′ }⟩, ⟨𝜙 ′ ( ȳ), 𝑉 (𝑄) ∪ {𝑥 ′ , 𝑥 ′′ }⟩ and ⟨𝜙 ′ ( ȳ), 𝑉 (𝑄) ∪ {𝑥 ′′ }⟩8 . Now, Lemma 64 easily follows from Lemma 68 and from Definitions 69-71.

The next thing left to be proven in this section is Lemma 66. Notice that claim (i) of the Lemma is now obvious: cut-red just removes a single red edge and fuse-red merges two red edges into one. In order to prove claims (ii)-(iv) however one needs to work a little bit harder.

Ranks. We are now going to define the rank 𝑒𝑟𝑘 (𝛼, 𝑄) for a live query 𝑄 and an atom 𝛼 ∈ 𝑄 G . To this end we consider paths, from some marked variable to 𝛼, traversing edges of 𝑞(𝑄) (in both directions). To be more precise: Definition 72. Given a live query 𝑄 an 𝑅-path is a finite sequence 𝑃 such that: • each of the elements of 𝑃 is either 𝐸 (𝑡, 𝑧) or 𝐸 -1 (𝑧, 𝑡) for some 𝐸 (𝑡, 𝑧) from 𝑞(𝑄), where 𝐸 ∈ {𝐺, 𝑅} (obviously, 𝐸 -1 (𝑧, 𝑡) means that we traverse 𝐸 (𝑡, 𝑧) backwards);

• if 𝐸 (𝑠, 𝑡) and 𝐸 ′ (𝑢, 𝑧) are two consecutive elements of 𝑃 then 𝑡 = 𝑢 (where 𝐸, 𝐸 ′ ∈ {𝐺, 𝑅, 𝐺 -1 , 𝑅 -1 }); (★) if 𝑅(𝑡, 𝑧) is an atom of 𝑞(𝑄) then only one of 𝑅(𝑡, 𝑧) or 𝑅 -1 (𝑧, 𝑡) can appear in 𝑃 and it can appear at most once.

Notice that an atom 𝐺 (𝑡, 𝑧) of 𝑞(𝑄), as well as 𝐺 -1 (𝑧, 𝑡), can appear any number of times in a 𝑅-path. Each 𝑅-path has its elevation and its cost9 : Definition 73 (elevation and cost). For an empty 𝑅-path ∅ we define 𝑐𝑜𝑠𝑡 (∅) = 0 and 𝑒𝑙𝑒𝑣 (∅) = 3 |𝑄 R | . For a path 𝑃 = 𝑃 ′ 𝐸 (𝑥, 𝑧) we define:

• 𝑒𝑙𝑒𝑣 (𝑃) = 𝑒𝑙𝑒𝑣 (𝑃 ′ ) if 𝐸 ∉ {𝑅, 𝑅 -1 } • 𝑒𝑙𝑒𝑣 (𝑃) = 3 • 𝑒𝑙𝑒𝑣 (𝑃 ′ ) if 𝐸 = 𝑅 • 𝑒𝑙𝑒𝑣 (𝑃) = 1 3 • 𝑒𝑙𝑒𝑣 (𝑃 ′ ) if 𝐸 = 𝑅 -1 • 𝑐𝑜𝑠𝑡 (𝑃) = 𝑐𝑜𝑠𝑡 (𝑃 ′ ) + 𝑒𝑙𝑒𝑣 (𝑃 ′ ) if 𝐸 ∈ {𝐺, 𝐺 -1 } • 𝑐𝑜𝑠𝑡 (𝑃) = 𝑐𝑜𝑠𝑡 (𝑃 ′ ) if 𝐸 ∉ {𝐺, 𝐺 -1 }
Notice that it follows from condition (★) of Definition 72 that 𝑒𝑙𝑒𝑣 (𝑃) is always a positive natural number. Definition 74. For an atom 𝛼 = 𝐺 (𝑢, 𝑢 ′ ) in 𝑞(𝑄) by an 𝛼-hike we mean an 𝑅-path such that: • if 𝐸 (𝑡, 𝑧) or 𝐸 -1 (𝑡, 𝑧) is the first atom of 𝑃 then 𝑡 ∈ 𝑉 (𝑄);

• the last element of 𝑃 is either 𝐺 (𝑢, 𝑢 ′ ) or 𝐺 -1 (𝑢 ′ , 𝑢).

For 𝛼 ∈ 𝑄 G we denote the set of all 𝛼-hikes as ℎ𝑖𝑘𝑒𝑠 (𝛼, 𝑄).

Definition 75. For an atom 𝛼 ∈ 𝑄 G its rank is defined as: 𝑒𝑟𝑘 (𝛼, 𝑄) = 𝑚𝑖𝑛({𝑐𝑜𝑠𝑡 (𝑃) : 𝑃 ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼, 𝑄)}).

It is easy to see that: Observation 76. For a marked query 𝑄 and for 𝛼 = 𝐺 (𝑢, 𝑢 ′ ) in 𝑄 G , if 𝑃 ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼, 𝑄) and 𝑐𝑜𝑠𝑡 (𝑃) = 𝑒𝑟𝑘 (𝛼, 𝑄) then any of 𝛼 or 𝐺 -1 (𝑢 ′ , 𝑢) can occur only as the last atom of 𝑃. Now we can finally prove Lemma 66. Proof of Lemma 66 (ii). Let 𝑄 ′ = cut-green(𝑄, 𝑥). It follows directly from the construction that |𝑄 R | = |𝑄 ′ R |. Now take any 𝛼 ∈ 𝑄 ′ G . We need to show that 𝑒𝑟𝑘 (𝛼, 𝑄) ≥ 𝑒𝑟𝑘 (𝛼, 𝑄 ′ ). Let 𝑧 ∈ 𝑣𝑎𝑟 (𝑄) be such that 𝐺 (𝑧, 𝑥) is an atom of 𝑞(𝑄). Consider any 𝑃 ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼, 𝑄). Let 𝑃 ′ be a path obtained from 𝑃 by deleting each occurrence of 𝐺 (𝑧, 𝑥) and 𝐺 -1 (𝑥, 𝑧). Then 𝑃 ′ ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼, 𝑄 ′ ) and 𝑐𝑜𝑠𝑡 (𝑃 ′ ) ≤ 𝑐𝑜𝑠𝑡 (𝑃). □

Proof of Lemma 66 (iii). Let 𝑄 ′ = fuse-green(𝑄, 𝑥, 𝑧, 𝑧 ′ ). If ( * ) there exists a variable 𝑢 ∈ 𝑣𝑎𝑟 (𝑄) such that atoms 𝑅(𝑧, 𝑢) and 𝑅(𝑧 ′ , 𝑢) are in 𝑞(𝑄), or that 𝑅(𝑢, 𝑧) and 𝑅(𝑢, 𝑧 ′ ) are in 𝑞(𝑄), then the two red edges merge in 𝑞(𝑄 ′ ) and |𝑄 R | > |𝑄 ′ R |. Also, if ( * * ) at least two of the atoms 𝑅(𝑧, 𝑧 ′ ), 𝑅(𝑧 ′ , 𝑧), 𝑅(𝑧, 𝑧), and 𝑅(𝑧 ′ , 𝑧 ′ ) are in 𝑞(𝑄) then |𝑄 R | > |𝑄 ′ R |. So suppose there is neither ( * ) nor ( * * ). Take any 𝛼 ∈ 𝑄 ′ G and 𝑃 ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼, 𝑄). Consider path 𝑃 ′ obtained from 𝑃 by replacing each occurrence of 𝑧 ′ in 𝑃 with 𝑧. Obviously, 𝑐𝑜𝑠𝑡 (𝑃) = 𝑐𝑜𝑠𝑡 (𝑃 ′ ). We now will show that 𝑃 ′ ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼, 𝑄 ′ ). Clearly, one only needs to worry if condition (★) of Definition 72 holds. Suppose towards contradiction that it does not. It can only happen when there exist 𝑠, 𝑡 ∈ 𝑣𝑎𝑟 (𝑄 ′ ) such that two atoms from {𝑅(𝑠, 𝑡), 𝑅 -1 (𝑡, 𝑠)} appear in 𝑃.

Let us assume that 𝑅(𝑠, 𝑡) (other cases are analogous) appears twice in 𝑃 ′ . But of course 𝑅(𝑠, 𝑡) could not appear twice in 𝑃, which is an 𝑅-path. So at least one occurrence of 𝑅(𝑠, 𝑡) in 𝑃 ′ results from the unification of 𝑧 and 𝑧 ′ .

There are two cases: either (a) 𝑠 = 𝑡 = 𝑧 or (b) exactly one of 𝑠, 𝑡 equals 𝑧. So suppose (b) happened and without loss of generality assume that 𝑠 = 𝑧. We know that there was 𝑅(𝑧, 𝑡) and 𝑅(𝑧 ′ , 𝑡) in 𝑃 and they both unified to 𝑅(𝑧, 𝑡) in 𝑃 ′ . But this would imply ( * ), leading to a contradiction. The remaining case (a) is that 𝑅(𝑧, 𝑧) occurs twice in 𝑃 ′ . But this would need ( * * ) to be true, which is a contradiction again.

So Let us first show claim (c). Take some 𝛽 ∈ 𝑄 G ∩ 𝑄 ′ G and 𝑃 ∈ ℎ𝑖𝑘𝑒𝑠 (𝛽, 𝑄) such that 𝑐𝑜𝑠𝑡 (𝑃) = 𝑒𝑟𝑘 (𝛽, 𝑄). Our goal is to find 𝑃 ′ ∈ ℎ𝑖𝑘𝑒𝑠 (𝛽, 𝑄 ′ ) such that 𝑐𝑜𝑠𝑡 (𝑃 ′ ) ≤ 𝑐𝑜𝑠𝑡 (𝑃).

Obviously, one can assume that 𝑃 does not contain, as a connected subsequence, 𝐺 (𝑥 𝑔 , 𝑥)𝐺 -1 (𝑥, 𝑥 𝑔 ). If it did, we could remove such subsequence to get a new 𝑃 with lower cost. And, as an R-path, 𝑃 does not contain subsequence 𝑅(𝑥 𝑟 , 𝑥)𝑅 -1 (𝑥, 𝑥 𝑟 ) either.

If no atom of 𝑃 contains 𝑥 then 𝑃 ∈ ℎ𝑖𝑘𝑒𝑠 (𝛽, 𝑄 ′ ) and thus we set 𝑃 ′ = 𝑃. Otherwise it contains exactly one of 𝑅(𝑥 𝑟 , 𝑥)𝐺 -1 (𝑥, 𝑥 𝑔 ) or 𝐺 (𝑥 𝑔 , 𝑥)𝑅 -1 (𝑥, 𝑥 𝑟 ) as a connected subsequence. Suppose 𝑃 = 𝑃 0 𝑅(𝑥 𝑟 , 𝑥)𝐺 -1 (𝑥, 𝑥 𝑔 )𝑃 1 . Let 𝐴 = 𝐺 -1 (𝑥 𝑟 , 𝑥 ′′ )𝐺 -1 (𝑥 ′′ , 𝑥 ′ )𝑅(𝑥 ′ , 𝑥 𝑔 ) and consider path 𝑃 ′ = 𝑃 0 𝐴𝑃 1 . Note that 𝑃 ′ ∈ ℎ𝑖𝑘𝑒𝑠 (𝛽, 𝑄). Now we need to show that 𝑐𝑜𝑠𝑡 (𝑃) > 𝑐𝑜𝑠𝑡 (𝑃 ′ ). But: The case when 𝑃 = 𝑃 0 𝐺 (𝑥 𝑔 , 𝑥)𝑅 -1 (𝑥, 𝑥 𝑟 )𝑃 1 , is similar.

Let us now move to claim (b). Take 𝑃 ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼, 𝑄) such that 𝑐𝑜𝑠𝑡 (𝑃) = 𝑒𝑟𝑘 (𝛼, 𝑄). We are going to build a path 𝑃 ′ ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼 ′ , 𝑄 ′ ) such that 𝑐𝑜𝑠𝑡 (𝑃 ′ ) < 𝑐𝑜𝑠𝑡 (𝑃).

There are two cases depending on the last atom of 𝑃:

In the first case 𝑃 is 𝑃 0 𝐺 (𝑥 𝑔 , 𝑥). Let then 𝑃 ′ be 𝑃 0 𝑅 -1 (𝑥 𝑔 , 𝑥 ′ )𝐺 (𝑥 ′ , 𝑥 ′′ ) or 𝑃 0 𝑅 -1 (𝑥 𝑔 , 𝑥 ′ )𝐺 (𝑥 ′ , 𝑥 ′′ )𝐺 (𝑥 ′′ , 𝑥 𝑟 ) (depending on whether 𝛼 ′ is 𝐺 (𝑥 ′ , 𝑥 ′′ ) or 𝐺 (𝑥 ′′ , 𝑥 𝑟 )). Then of course 𝑃 ′ ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼 ′ , 𝑄) and 𝑐𝑜𝑠𝑡 (𝑃) = 𝑐𝑜𝑠𝑡 (𝑃 0 ) + 𝑒𝑙𝑒𝑣 (𝑃 0 ) while 𝑐𝑜𝑠𝑡 (𝑃 ′ ) ≤ 𝑐𝑜𝑠𝑡 (𝑃 0 ) + 2 3 • 𝑒𝑙𝑒𝑣 (𝑃 0 ). The second case is that 𝑃 = 𝑃 0 𝑅(𝑥 𝑟 , 𝑥)𝐺 -1 (𝑥, 𝑥 𝑔 ). Here the argument is similar. Now we take 𝑃 ′ = 𝑃 0 𝐺 -1 (𝑥 𝑟 , 𝑥 ′′ ) or 𝑃 ′ = 𝑃 0 𝐺 -1 (𝑥 𝑟 , 𝑥 ′′ )𝐺 -1 (𝑥 ′′ , 𝑥 ′ ) (again depending on whether 𝛼 ′ is 𝐺 (𝑥 ′ , 𝑥 ′′ ) or 𝐺 (𝑥 ′′ , 𝑥 𝑟 )). Then 𝑃 ′ ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼 ′ , 𝑄) and 𝑐𝑜𝑠𝑡 (𝑃) = 𝑐𝑜𝑠𝑡 (𝑃 0 ) + 3 • 𝑒𝑙𝑒𝑣 (𝑃 0 ) while 𝑐𝑜𝑠𝑡 (𝑃 ′ ) ≤ 𝑐𝑜𝑠𝑡 (𝑃 0 ) + 2 • 𝑒𝑙𝑒𝑣 (𝑃 0 ) . □

B.4 Proof of Lemma 65

Let 𝑄 = ⟨𝜙 ( ȳ), 𝑉 ⟩ be any live marked query.

Lemma 65 will follow directly from Lemmas 77-79:

Lemma 77. For any set of facts D, tuple ā ∈ 𝑑𝑜𝑚(D) | ȳ | and 𝑥 such that 𝑄 ′ = cut-green(𝑄, 𝑥) (or 𝑄 ′ = cut-red(𝑄, 𝑥)) the following

  ∀𝜙 ∃𝑖 ∈ N ∀D 𝐶ℎ (D, T) |= 𝜙 ⇔ 𝐶ℎ 𝑖 (D, T) |= 𝜙 , (BDD)

Example 1 .

 1 satisfies all TGDs from T . For a pair T , D, a CQ 𝜙 ( ȳ), and a tuple ā ∈ 𝑑𝑜𝑚(D) | ȳ | , we write T , D |= 𝜙 ( ā) (or T , D, ā |= 𝜙 ( ȳ)) to indicate that T and D jointly entail 𝜙 ( ā), which means that 𝜙 ( ā) holds in each structure F satisfying F |= T , D, which serves as a shortcut for F |= T ∧ D ⊆ F. Consider the instance D 𝑎 = {𝐻𝑢𝑚𝑎𝑛(𝐴𝑏𝑒𝑙)} and the theory T 𝑎 consisting of the following two rules: 𝐻𝑢𝑚𝑎𝑛(𝑦) ⇒ ∃𝑧 𝑀𝑜𝑡ℎ𝑒𝑟 (𝑦, 𝑧) 𝑀𝑜𝑡ℎ𝑒𝑟 (𝑥, 𝑦) ⇒ 𝐻𝑢𝑚𝑎𝑛(𝑦) Then T 𝑎 , D 𝑎 |= ∃𝑦, 𝑧 𝑀𝑜𝑡ℎ𝑒𝑟 (𝐴𝑏𝑒𝑙, 𝑦), 𝑀𝑜𝑡ℎ𝑒𝑟 (𝑦, 𝑧).

Definition 4 (

 4 Semi-oblivious Skolem chase procedure). • Ch 0 (T , D) = D, • Ch 𝑖+1 (T , D) = Ch 𝑖 (T , D) ∪ {𝑎𝑝𝑝𝑙 (𝜌, 𝜎) | 𝜌 ∈ T , 𝜎 ∈ H𝑜𝑚(𝜌, Ch 𝑖 (T , D))}, • Ch(T , D) = 𝑖 ∈N Ch 𝑖 (T , D).

Observation 23 .

 23 If a theory is local then it is BDD. Proof (sketch). Given a local theory T and a CQ Φ, we show that there exists a natural number 𝑛 Φ satisfying Definition 10. Due to T being local, we can, for every F with F |= Φ, identify some D ⊆ F with D |= Φ and |D| ≤ 𝑙 T |Φ|. Therefore, we let F = {D | Ch(T , D) |= Φ ∧ |D| ≤ 𝑙 T |Φ|}. For any D ∈ F , define 𝑛 D as the minimal natural number such that Ch 𝑛 D (T , D) |= Φ. As F contains just a finite number of non-isomorphic instances, picking 𝑛 Φ = max{𝑛 D | D ∈ F } witnesses that Definition 10 applies. □ We defer any further discussion about locality until later sections. And now, let us state our first result. Theorem 1. Every BDD theory over binary signature is local.

Lemma 28 .

 28 For any instance D and for any F ⊆ D, the structure 𝑀 F is a model of T and D. Proof. Clearly 𝑀 F |= D. In order to prove 𝑀 F |= T , consider any 𝜌 ∈ T and any 𝜎 ∈ H𝑜𝑚(𝜌, 𝑀 F ). Of course, 𝑎𝑝𝑝𝑙 (𝜌, 𝜎) ∈ Ch(D), since Ch(D) is by definition closed under rule applications.

  that fr (𝛼) ⊆ 𝑑𝑜𝑚(𝐶𝑜𝑟𝑒 (T , F)) ( * ), as fr (𝛼) ⊆ 𝑑𝑜𝑚(Ch(F)) and none of the terms in fr (𝛼) are banned. Now let ℎ * F : Ch(F) → 𝐶𝑜𝑟𝑒 (T , F) be a homomorphism as in Property 7. Since 𝛼 ∈ Ch(F), we obtain ℎ * F (𝛼) ∈ 𝐶𝑜𝑟𝑒 (T , F) and thus ℎ * F (𝛼) ∈ 𝑀 F . As ℎ * F is a retraction, ℎ * F (fr (𝛼)) = fr (𝛼) follows from ( * ). Hence, ℎ * F (𝛼) can serve as our 𝛼 ′ , concluding the proof. □ Lemma 29. For any instance D and any F ⊆ D there exists a homomorphism ℎ * 𝑀 F from Ch(D) to itself that maps all terms to 𝑑𝑜𝑚(𝑀 F ) and is the identity on 𝑑𝑜𝑚(𝑀 F ). Proof. Note that 𝑀 F |= T (Lemma 28) and D ⊆ 𝑀 F . Then Property 7 ensures the existence of the claimed homomorphism. □ Let H D be the set of all homomorphisms ℎ * 𝑀 F for F ∈ I D . Each ℎ * 𝑀 F ∈ H D has as its domain the set 𝑑𝑜𝑚(Ch(𝑀 F )), that is equal to 𝑑𝑜𝑚(Ch(D)), and has as its image a subset of this domain.

Figure 1 :

 1 Figure 1: Fragment of 𝐶ℎ(T 𝑑 , G 8 (𝑎 0 , 𝑎 8 )) (print in colors!)

Exercise 49 .

 49 Let D be any instance and let ā ∈ 𝑑𝑜𝑚(𝐶ℎ(T , D)) | ȳ | . Let 𝜙 ( ȳ) ∈ 𝑟𝑒𝑤 (𝜓 ( ȳ)) (where𝜓 ( ȳ) is some CQ) and suppose 𝐶ℎ(T , D) |= 𝜙 ( ā). Then 𝐶ℎ(T , D) |= 𝜓 ( ā). Hint: Recall that 𝐶ℎ(T , 𝐶ℎ(T , D)) = 𝐶ℎ(T , D). Exercise 50. Let 𝜓 ( ȳ) be any CQ and 𝜙 ( ȳ) ∈ 𝑟𝑒𝑤 (𝜓 ( ȳ)). Let D be any instance and ā ∈ 𝑑𝑜𝑚(D) | ȳ | . Suppose 𝐶ℎ(T , D) |= 𝜙 ( ā). Then there exists query 𝜙 ′ ( ȳ) ∈ 𝑟𝑒𝑤 (𝜓 ( ȳ)) such that D |= 𝜙 ′ ( ā). Hint: Notice that 𝐶ℎ(T , 𝐶ℎ(T , D)) = 𝐶ℎ(T , D).

  1 (T 𝑁 𝐹 , D) |= 𝑀 𝜙 . □ Combining Lemma 53 and Observation 47 we get: Corollary 54. If Ch(T 𝑁 𝐹 , D) |= 𝛼 for some detached atom 𝛼 then 𝐶ℎ 2 (T 𝑁 𝐹 , D) |= 𝛼. The last lemma we need for the proof of Lemma 48 is: Lemma 55. Ch 𝑖,∃ (T , D) ⊆ Ch 𝑖+2,∃ (T 𝑁 𝐹 , D) Proof. The induction base D ⊆ Ch 2,∃ (T 𝑁 𝐹 , D) is clearly true. And so let us move to the induction step.

Corollary 56 .

 56 For any set of facts D: Ch(T 𝐷𝐿 , Ch ∃ (T 𝑁 𝐹 , D) ∪ D) = Ch(T , D)

𝛼

  ∈S(𝑡 ) 𝑐𝑎𝑛𝑐 (𝛼) = 𝛼 ∈S(𝑡 ) 𝑐𝑝𝑎𝑟 (𝛼) ∩ D. Using the above equality, one can bound the number of ancestors of atoms in the connected ancestors of someone in S(𝑡) in the following way: 𝛼 ∈S(𝑡 ) 𝑐𝑝𝑎𝑟 (𝛼) ∩ D ≤ 𝛼 ∈S(𝑡 ) |𝑐𝑝𝑎𝑟 (𝛼) ∩ D| . Now, we can easily bound |𝑐𝑝𝑎𝑟 (𝛼) ∩ D| with ℎ for any atom 𝛼 of Ch(T 𝑁 𝐹 , D). Finally we are going to show that only a finite (and bounded) number of atoms of S(𝑡) have any connected parents in D.

□ A.5 Proving Theorem 1

 1 Now we can finally prove Theorem 1. The following is an easy corollary of Lemma 57 and Corollary 56: Corollary 58. For any term 𝑡 ∈ 𝑑𝑜𝑚(D) ∪ 𝑑𝑒𝑡 (Ch(T 𝑁 𝐹 , D)) there exists a subset D ′ of D of size at most 𝑀 such that S(𝑡) ⊆ Ch(T , D ′ ).This is almost Theorem 1, but only for existential atoms of Ch(T , D). However, observe that:Observation 59. There exists a constant 𝑑 T such that for any set of facts D and for any atom 𝛼 of Ch(T 𝐷𝐿 , D) there exists a subset D ′ of D such that |D ′ | < 𝑑 T and 𝛼 ∈ Ch(T , D ′ ).

  𝑐𝑜𝑠𝑡 (𝑃) = 𝑐𝑜𝑠𝑡 (𝑃 0 ) + 3 • 𝑒𝑙𝑒𝑣 (𝑃 0 ) + 3 • 𝑒𝑙𝑒𝑣 (𝑃 0 ) • 𝑐𝑜𝑠𝑡 (𝑃 1 ) 𝑐𝑜𝑠𝑡 (𝑃 ′ ) = 𝑐𝑜𝑠𝑡 (𝑃 0 ) + 2 • 𝑒𝑙𝑒𝑣 (𝑃 0 ) + 3 • 𝑒𝑙𝑒𝑣 (𝑃 0 ) • 𝑐𝑜𝑠𝑡 (𝑃 1 )

•

  Extend the proof of Theorem 1 to show Conjecture 2, i.e., that all BDD frontier-guarded theories[START_REF] Baget | On rules with existential variables: Walking the decidability line[END_REF] are local and thus the FUS/FES conjecture holds for them. Also, show if the FUS/FES conjecture holds for bd-local theories and then, of course, try to show the conjecture in the general case! • Define a class of BDD theories that contains rule sets such as the one from Definition 39. Also, define an expressive class that captures the intuitive notion of locality, contains all known BDD classes, and implies BDD membership. • Even though we extend Theorem 3 in the appendix (see Lemma 40), we wonder if there is a theory that does not admit an elementary bound on the width of its rewritings. Acknowledgements. Ostropolski-Nalewaja and Marcinkowski were supported by the Polish National Science Centre (NCN) grant 2016/23/B/ST6/01438. Carral was supported by the ANR project CQFD (ANR-18-CE23-0003), the DFG project 389792660 (TRR 248, Center for Perspicuous Systems) and by the BMBF in the Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI). Rudolph was supported by the European Research Council through the ERC Consolidator Grant DeciGUT (project number 771779).

  It easily follows from Observation 63 that for every live query 𝑄 there must exist a maximal variable 𝑥 ∈ 𝑣𝑎𝑟 (𝑄). By this we mean that 𝑥 ∉ 𝑉 and that no atom of the form 𝐸 (𝑥, 𝑧) occurs in 𝑞(𝑄) for 𝐸 ∈ {𝐺, 𝑅}. Note that: Lemma 68. Let 𝑥 be a maximal variable of a live query ⟨𝜙 ( ȳ), 𝑉 ⟩. Then one of the following condition holds:(i) 𝑥 occurs in exactly one atom 𝐸 (𝑧, 𝑥), with 𝐸 ∈ {𝐺, 𝑅};(ii) 𝑥 occurs in exactly two atoms 𝑅(𝑥 𝑟 , 𝑥) and 𝐺 (𝑥 𝑔 , 𝑥) for some 𝑥 𝑟 , 𝑥 𝑔 ; (iii) there exist at least two vertices 𝑧 ≠ 𝑧 ′ and 𝐸 ∈ {𝐺, 𝑅} such that 𝐸 (𝑧, 𝑥) and 𝐸 (𝑧 ′ , 𝑥) are atoms of 𝜙 ( ȳ).

  𝑃 ′ ∈ ℎ𝑖𝑘𝑒𝑠 (𝛼, 𝑄 ′ ) and 𝑒𝑟𝑘 (𝛼, 𝑄) ≥ 𝑒𝑟𝑘 (𝛼, 𝑄 ′ ). □ Proof of Lemma 66 (iv). Let 𝑄 ′ be any of the marked queries in reduce(𝑄, 𝑥). Let 𝑥 𝑟 and 𝑥 𝑔 be variables of 𝑄 such that 𝐺 (𝑥 𝑔 , 𝑥) and 𝑅(𝑥 𝑟 , 𝑥) are atoms of 𝑞(𝑄). Recall that 𝑥 ′ , 𝑥 ′′ ∈ 𝑣𝑎𝑟 (𝑄 ′ ) are two new variables added by reduce.Clearly, |𝑄 ′ R | = |𝑄 R |, since when creating 𝑞(𝑄 ′ ) from 𝑞(𝑄) we have just replaced one red edge with another.

The queries 𝜙 ( ȳ) and 𝜓 ( ȳ) are seen as structures here: the active domains of these structures are the sets of variables of 𝜙 ( ȳ) and 𝜓 ( ȳ).

To be precise we should call this new structure 𝑀 D,F , but D will be fixed and clear from the context.

Such rules are called disconnected in[START_REF] Baget | Extending decidable cases for rules with existential variables[END_REF], however we think that calling those rules detached might help the reader to distinguish those from rules that have disconnected bodies.

Actually, the assumption we really use in the proof of Theorem 1 is not that relations are at most binary, but that the existential rules are "frontier one".

One could wonder what happens if one of the two variables we unify is in 𝑉 and the other is not in 𝑉 . But this is prohibited by Observation 63 (iii).

Note that ⟨𝜙 ′ ( ȳ), 𝑉 (𝑄) ∪ {𝑥 ′′ }⟩ is not properly marked, and thus not live, and it will in no way contribute to our process any more.

The cost of making a step depends on the current elevation. Current elevation depends on the difference between the total ascent and total descent.

Appendix B PROOF OF LEMMA 40 (A).

THE HIGH-LEVEL VIEW.

Since T 𝑑 is fixed, we will use the notation 𝐶ℎ(F) instead of 𝐶ℎ(T 𝑑 , F) Clearly, to prove that T 𝑑 is BDD, it is enough to consider only connected queries, since a bound for any non-connected query can be derived from bounds of its connected components. Additionally, notice that due to the rule (loop), if 𝜙 is a boolean query and if D is any instance then 𝐶ℎ 1 (D) |= 𝜙. So for the rest of the proof of Lemma 40 (A) we will consider only connected non-boolean queries. Let us start with: Definition 60 (Marked qery). We define a marked query as a pair ⟨𝜙 ( ȳ), 𝑉 ⟩ where 𝜙 ( ȳ) = ∃ x𝛽 ( x, ȳ) is a CQ and 𝑉 is a subset of variables of 𝜙 ( ȳ) such that ȳ ⊆ 𝑉 ⊆ ȳ ∪ x.

We say that the variables in 𝑉 are marked. It will often be more convenient to refer to a marked query without (or before) specifying its components. The letter 𝑄 will be used for that. If 𝑄 = ⟨𝜙 ( ȳ), 𝑉 ⟩ then by 𝑉 (𝑄) we mean 𝑉 , and 𝑞(𝑄) denotes 𝜙 ( ȳ). By 𝑣𝑎𝑟 (𝑄) we mean the set of all variables of 𝑞(𝑄), and 𝑄 R (𝑄 G ) is the set of red (green) atoms in 𝑞(𝑄).

For a marked query 𝑄 the intention behind the set of marked variables 𝑉 (𝑄) is that the variables of 𝑉 (𝑄) should not be mapped onto the chase-produced Skolem terms: Definition 61. For a marked query 𝑄 = ⟨𝜙 ( ȳ), 𝑉 ⟩, a fact set D, and ā ∈ 𝑑𝑜𝑚(D) | ȳ | we say that 𝐶ℎ(D) |= 𝑄 ( ā) if there exists a homomorphism ℎ : 𝑣𝑎𝑟 (𝑄) → 𝑑𝑜𝑚(𝐶ℎ(D)) witnessing 𝐶ℎ(D) |= 𝜙 ( ā) such that for every 𝑣 there is ℎ(𝑣) ∈ 𝑑𝑜𝑚(D) if and only if 𝑣 ∈ 𝑉 . Some marked queries are false -it follows directly from Definition 39 that they cannot be satisfied in any 𝐶ℎ(D): Marked queries satisfying conditions (i)-(iii) of Observation 63 will be called properly marked. Marked queries whose all variables are marked will be called totally marked. Properly marked queries that are not totally marked will be called live. Notice that for a totally marked query ⟨𝜙 ( ā), 𝑉 ⟩, an instance D and a tuple ā ∈ 𝑑𝑜𝑚(D) | ȳ | there is 𝐶ℎ(D) |= ⟨𝜙 ( ā), 𝑉 ⟩ if and only if D |= 𝜙 ( ā).

B.1 High-level proof of claim (A). The process.

Now we get some conjunctive query 𝜙 ( ȳ), that will be fixed till the end of this proof, and we want to show that there exists a rewriting of 𝜙, i.e. a finite set 𝑟𝑒𝑤 (𝜙 ( ȳ)) of CQs such that for each D and ā ∈ 𝑑𝑜𝑚(D) | ȳ | there is 𝐶ℎ(D) |= 𝜙 ( ā) if and only if there exists a 𝜓 ( ȳ) ∈ 𝑟𝑒𝑤 (𝜙 ( ȳ)) such that D |= 𝜓 ( ā).

Notice that 𝑟𝑒𝑤 (𝜙 ( ȳ)) will be constructed if we can produce a finite set S of marked queries, such that: S will be constructed as the result of some process. As the starting point of this process let S 0 = {𝑄 : 𝑞(𝑄) = 𝜙 ( ȳ)}, the set of all possible markings of 𝜙 ( ȳ). One can easily see that S 0 satisfies Condition (♠) above, but there is no reason to think that it also satisfies Condition (♣). Now, the plan is as follows. Five operations are going to be defined in Appendix B.3, called cut-red, cut-green, fuse-red, fuse-green, and reduce. Each of them will:

• take, as an input, some marked query 𝑄;

• remove from 𝑞(𝑄), one variable and some atoms (operation reduce will remove one red atom and one green) ; • keep the marking of the surviving variables unchanged; • in one case (of operation reduce) add two new variables, one red atom, and two green atoms); • return the resulting marked query (except for operation reduce which will return four marked queries: one for each of the four possible markings of the two new variables).

It will be shown in Appendix B.3 that:

Lemma 64 (Completness). If a query is live then at least one of the five operations can be applied to it.

At this point we can define our process, which is supposed to ultimately create S. Start from S 0 . Once S 𝑖 is defined, which does not satisfy condition (♣), take any live query 𝑄 ∈ S 𝑖 , apply one of the five operations to this query, and define S 𝑖+1 as S 𝑖 with 𝑄 replaced by the query (or queries) resulting from this application. Clearly, for the process to make sense we will need to prove (in Appendix B. Proof. Let 𝑥 ′ , 𝑥 ′′ , 𝑥 𝑟 , and 𝑥 𝑔 be variables of 𝑞(𝑄) such that 𝑅(𝑥 𝑟 , 𝑥), 𝐺 (𝑥 𝑔 , 𝑥) ∈ 𝑞(𝑄) and that 𝑅(𝑥 ′ , 𝑥 𝑔 ), 𝐺 (𝑥 ′ , 𝑥 ′′ ), 𝐺 (𝑥 ′′ , 𝑥 𝑟 ) ∈ 𝑞(𝑄 ′ ).

(⇐). Let 𝑄 ′ ∈ Q be such that Ch(T 𝑑 , D) |= 𝑄 ′ ( ā) and let ℎ ′ be a homomorphism witnessing that. We need to show that there exists a homomorphism ℎ witnessing Ch(T 𝑑 , D) |= 𝑄 ( ā).

Since 𝑅(𝑥 ′ , 𝑥 𝑔 ), 𝐺 (𝑥 ′ , 𝑥 ′′ ), 𝐺 (𝑥 ′′ , 𝑥 𝑟 ) are atoms of 𝑞(𝑄), and ℎ ′ is a homomorphism, we know that 𝑅(ℎ ′ (𝑥 𝑔 ), ℎ ′ (𝑥 ′ )), 𝐺 (ℎ ′ (𝑥 ′ ), ℎ ′ (𝑥 ′′ )) and 𝐺 (ℎ ′ (𝑥 ′′ ), ℎ ′ (𝑥 𝑟 )) are atoms of Ch(T 𝑑 , D). But, since (𝑔𝑟𝑖𝑑) is a rule of T 𝑑 , this implies that there exists an element 𝑡 ∈ Ch(T 𝑑 , D), such that 𝐺 (ℎ ′ (𝑥 𝑔 ), ℎ ′ (𝑡)) and 𝑅(ℎ ′ (𝑥 𝑟 ), ℎ ′ (𝑡)) are also in Ch(T 𝑑 , D).

Define ℎ by: • ℎ(𝑢) = ℎ ′ (𝑢) for 𝑢 ∈ 𝑣𝑎𝑟 (𝑄) \ {𝑥 }.

• ℎ(𝑥) = 𝑡. (⇒). Let ℎ be a homomorphism witnessing that Ch(T 𝑑 , D) |= 𝑄 ( ā). We will show that there exist 𝑄 ′ ∈ Q and a homomorphism ℎ ′ such that ℎ ′ is witnessing Ch(T 𝑑 , D) |= 𝑄 ′ ( ā). Again recall that 𝑥 is an unmarked variable and so let us find parents of ℎ(𝑥) in Ch(T 𝑑 , D). Note that ℎ(𝑥) could be created only by rule (𝑔𝑟𝑖𝑑) as it has an in-degree of two. Let 𝜎 be such that 𝑎𝑝𝑝𝑙 ((𝑔𝑟𝑖𝑑), 𝜎) = 𝑅(ℎ(𝑥 𝑟 ), ℎ(𝑥)), 𝐺 (ℎ(𝑥 𝑔 ), ℎ(𝑥)). We set:

There are four possible picks for 𝑄 ′ from Q. While homomorphism ℎ ′ works for any of them as elements of Q differ only by markings, we need to make sure that the marking of 𝑄 ′ agrees with ℎ ′ . Obviously for every variable of 𝑄 this is the case. However we have two new variables to consider, namely 𝑥 ′ and 𝑥 ′′ . Thus we need to take 𝑄 ′ such that it satisfies:

This is trivially possible due to Definition 71. □

Appendix C GENERALIZATION OF LEMMA 40

For 𝐾 ∈ N define T 𝐾 𝑑 as the theory, over Σ 𝐾 = {𝐼 𝐾 , 𝐼 𝐾-1 , . . . 𝐼 1 } (each 𝐼 𝑘 is a binary relation symbol), comprising, for each 1 ≤ 𝑖 < 𝐾 and each 1 ≤ 𝑘 ≤ 𝐾 the following 2𝐾 + 1 rules:

Using the ideas from Appendix B one can now show that:

Lemma 80. For each 𝐾 ∈ N: A. theory T 𝐾 𝑑 is BDD; B. there is a query 𝜓 (𝑦, 𝑦 ′ ) such that 𝑟𝑒𝑤 T 𝐾 𝑑 (𝜓 (𝑦, 𝑦 ′ )) contains a CQ of size (𝐾-1)-fold exponential in the size of 𝜓 .

Like in the case of Lemma 40, claim B of Lemma 80 is relatively easy to prove.

For the proof of claim A, properly marked queries first need to be slightly redefined (but let us skip it here). Then the five operations need to be generalized in the natural way: we will now have 𝐾 cut operations, 𝐾 fuse operations, and 𝐾-1 reduce operations.

The non-obvious part is how to modify the ranks 𝑒𝑟𝑘 and 𝑞𝑟𝑘 so that they do their job correctly in the new circumstances. For that 𝐼 𝑖 -paths need to be defined (for 1 ≤ 𝑖 < 𝐾), analogous to 𝑅-paths in Definition 72. But now the condition (★) will apply to atoms of the relation 𝐼 𝑖 (including 𝐼 -1 𝑖 ). Then 𝑖-elevation (𝑒𝑙𝑒𝑣 𝑖 ) will be defined, like in Definition 73. And finally, we will need 𝑐𝑜𝑠𝑡 𝑖 of a path, calculated almost like the cost of the path in Definition 73: for a path 𝑃 = 𝑃 ′ 𝐸 (𝑥, 𝑧) we have 𝑐𝑜𝑠𝑡 𝑖 (𝑃) = 𝑐𝑜𝑠𝑡 (𝑃 ′ ) + 𝑒𝑙𝑒𝑣 𝑖 (𝑃 ′ ) if 𝐸 = 𝐼 𝑖-1 or 𝐼 -1 𝑖-1 and 𝑐𝑜𝑠𝑡 𝑖 (𝑃) = 𝑐𝑜𝑠𝑡 (𝑃 ′ ) otherwise. Notice that 𝐼 𝑖 is the new red and 𝐼 𝑖-1 is the new green. Note also that we have a new situation: 𝐸 may now very well be neither "green" nor "red". And that is fine, in such case it neither contributes to the elevation nor to the cost of the path.

Having the function 𝑐𝑜𝑠𝑡 𝑖 , rank 𝑒𝑟𝑘 (𝛼) of an atom 𝛼 of the relation 𝐼 𝑖-1 is (like in Appendix B.3) defined as minimal 𝑐𝑜𝑠𝑡 𝑖 of an 𝐼 𝑖 -path from some marked variable to 𝛼, and rank 𝑞𝑟𝑘 𝑖 (𝑄) is the multiset of all ranks 𝑒𝑟𝑘 (𝛼) of all atoms 𝛼 of 𝐼 𝑖-1 in 𝑄. Finally, 𝑞𝑟𝑘 (𝑄) is the tuple:

where |𝑄 𝑖 | is the number of the atoms of the relation 𝐼 𝑖 in 𝑄. Clearly, the lexicographic ordering on the set of such ranks is a well ordering. Now, a careful case inspection shows that each of the 3𝐾-1 operations decreases the rank of a query.

Appendix D REMARKS ON T 𝑑

There are two technical problems one needs to deal with here:

A Journey to the Frontiers of Query Rewritability (Extended Technical Report)

(1) There are conjunctions in the heads of rules (loop) and (grid) (notice that the rule (pins) can be simply split into two singlehead rules).

(2) we have predicate "true" in the bodies of rules (loop) and (pins) To deal with the first problem we could introduce a new ternary predicate 𝑇 , and rewrite the rules as:

(𝑙𝑜𝑜𝑝) 𝑡𝑟𝑢𝑒 ⇒ ∃𝑥𝑇 (𝑥, 𝑥, 𝑥) (𝑔𝑟𝑖𝑑) 𝑅(𝑥, 𝑥 ′ ), 𝐺 (𝑥, 𝑢), 𝐺 (𝑢, 𝑢 ′ ) ⇒ ∃𝑧𝑇 (𝑢 ′ , 𝑥 ′ , 𝑧)

Then add Datalog rules: 𝑇 (𝑥, 𝑦, 𝑧) ⇒ 𝑅(𝑥, 𝑧) 𝑇 (𝑥, 𝑦, 𝑧) ⇒ 𝐺 (𝑦, 𝑧) 𝑅(𝑥, 𝑧), 𝐺 (𝑦, 𝑧) ⇒ 𝑇 (𝑥, 𝑦, 𝑧) In this way 𝑇 (𝑥, 𝑦, 𝑧) is just a macro for 𝑅(𝑥, 𝑧) and 𝐺 (𝑦, 𝑧) and clearly the transformation does not change the BDD status of the theory.

To deal with the second problem we need to replace the predicate "true" with something like "if anything at all exists". For rule (loop) it would mean that it should be replaced with three rules: 𝑅(𝑦, 𝑧) ⇒ ∃𝑥𝑇 (𝑥, 𝑥, 𝑥) 𝐺 (𝑦, 𝑧) ⇒ ∃𝑥𝑇 (𝑥, 𝑥, 𝑥) 𝑇 (𝑡, 𝑦, 𝑧) ⇒ ∃𝑥𝑇 (𝑥, 𝑥, 𝑥) This transformation leads to a theory which is equivalent to our T 𝑑 on all nonempty instances, but this is of course good enough.

An analogous (albeit slightly more complicated) trick works for (pins).

Appendix E STICKY AND BD-LOCAL

Here we prove the following observation: Observation 81. Every connected sticky theory is bd-local Proof. Let T be a connected sticky theory and D be any instance with 𝑘 being its degree. Let 𝐴( ì 𝑎) be an atom of Ch(T , D) and F be the minimal subset of D such that 𝐴( ì 𝑎) ∈ Ch(T , F). We show that |F| depends only on T and 𝑘. As T is connected and sticky we know that if |F| > 1 then every fact of F needs to contain some term of ì 𝑎. From this we conclude that |F| ≤ | ì 𝑎|𝑘, thus we know that T is local. □