All-Instances Oblivious Chase Termination is Undecidable for Single-Head Binary TGDs

1 Introduction

The chase [Maier et al., 1979] is a fundamental family of algorithms used to solve issues involving the tuple-generating dependencies [Fagin, 2018] TGDs, e.g., checking query containment under constraints [Beeri and Vardi, 1984; Maier et al., 1979], computing data-exchange solutions [Fagin et al., 2005], querying databases with views [Halevy, 2001] or querying probabilistic databases [Olteanu et al., 2009]. Moreover, the chase is intensively used in ontological modelling and knowledge representation [Baget et al., 2011; Cal`ı et al., 2010; Grau et al., 2013], especially for answering conjunctive queries over ontologies formulated with TGDs: see e.g. [Benedikt et al., 2017; Urbani et al., 2018] for practical implementations and benchmarks. The main idea behind the chase is fairly simple: given a database D and a set of TGDs T the chase computes a universal model of D and T i.e., a possibly infinite extension of D, which is self-sufficient to determine query entailment. Whilst TGDs have a precise definition i.e., they are first-order sentences of the form ∀x ∀y α(x, y) → ∃z β(y, z), where both α and β are positive conjunctions of atoms, the way how the chase constructs a universal model can be formalized in various ways. It results in several versions of the chase, developed during the last decade: the Oblivious Chase [Cal`ı et al., 2013], the Skolem Chase [Marnette, 2009], the SemiOblivious Chase [Marnette, 2009], the Standard Chase [Fagin et al., 2005]. In this paper however, we focus on the Oblivious Chase, which is an eager (or a naive) version of the chase. Roughly speaking, for each TGD ∀x ∀y α(x, y) → ∃z β(y, z) from a set T the Oblivious T -Chase extends an initial database D with fresh elements z witnessing β(y, z) whenever it is possible to find tuples x, y witnessing α(x, y). The chasing process continues until a fix point is reached. If such fix-point structure is finite, we say that the chase is terminating.

∗B. Bednarczyk was supported by ERC Consolidator Grant 771779 (DeciGUT). P. Ostropolski-Nalewaja was supported by the Polish National Science Centre (NCN) grant 2016/23/B/ST6/01438.

A natural question arising from chase termination is the All-Instances Chase Termination Problem (AICTP): a static analysis variant of chase termination, where we ask whether for a given set T of TGDs the T -Chase terminates on all possible databases D [Grahne and Onet, 2018]. The problem was recently shown to be undecidable in [Gogacz and Marcinkowski, 2014] for sets of ternary rules, no matter what version of the chase we choose. Since the TGDs used in their undecidability proof are far from any well-known and wellbehaved rule classes, researchers started looking on AICTP for rule-sets under some shape restrictions [Calautti et al., 2015]. Recently the decidability of AICTP has been shown for sets of linear TGDs [Lecl`ere et al., 2019], sets of single-head guarded TGDs [Gogacz et al., 2020], and for sets of sticky TGDs [Calautti and Pieris, 2019].

1.1 Our Contribution

In this work, we consider the All-Instances Chase Termination Problem for the class of TGDs under two restrictions: first, the allowed arity of relations in TGDs is at most two and second, all rules contain at most one atom in their heads. Such restrictions are very natural, e.g. for ontologies from the Horn fragment of OWL [Hitzler et al., 2009]. More precisely we are going to prove the following theorem:

Theorem 1.1. All-Instances Oblivious Chase Termination is undecidable for sets of binary single-head TGDs.

Our result significantly improves the exponential space lower bound provided in [Gogacz and Marcinkowski, 2014]. Moreover, by arguing along the lines of [Gogacz and Marcinkowski, 2014, Sec. 3.5] our proofs can be extended to the undecidability proof of AICTP for binary single-head TGDs for both Standard and Semi-Oblivious Chases.

2 Preliminaries

We consider a set of terms T, defined as the union of three countably-infinite mutually-disjoint sets of constants C, of nulls N, and of variables V. A schema S is a finite set of relational symbols. For each relational symbol R ∈ S we denote its arity with ar(R). An atom over S is an expression of the form R(t), where t is a ar(R)-tuple of terms. A fact is simply an atom R(t), where t consists only of constants. An instance I over S is a (possibly infinite) set of atoms, whereas a database D is a finite set of facts. The active domain adom(I) of an instance I is the set of all domain elements from relations of I, i.e., both constants and nulls. Since databases and instances are structures in a sense of mathematical logic, we use satisfaction relation |= to indicate that a structure satisfies a given formula. Moreover, we note here that in Section 3 we work on schemata containing relational symbols of arity at most two only. Thus we often refer to binary relations simply as edges and to domain elements of instances as nodes or vertices.

A tuple-generating dependency (TGD) is a sentence of the form ϕ = ∀xy α(x, y) → ∃z β(y, z), where x, y, z are tuples of variables from V and both the body α(x, y) and the head β(y, z) of ϕ (denoted with body(ϕ) and head(ϕ) respectively) are positive conjunctions of atoms. For the sake of readability, we often omit quantifiers in TGDs. We say that a TGD ϕ is: n-ary if all relations appearing in ϕ are of arity at most n, single-head if head(ϕ) contains at most one atom, existential if ϕ contains an existential quantifier, and datalog if ϕ does not contain an existential quantifier.

A substitution is a partial function defined over T. A homomorphism from a set of atoms A to a set of atoms B is a substitution h from the terms of A to the terms of B, which additionally satisfies conditions: (i) h(t) = t for each t ∈ C, and (ii) R(h(t1), . . . , h(tn)) ∈ B for all R(t1, . . . , tn) ∈ A.

An instance I is contained in I′ , (written I ⊆ I′ ), when there exists a injective homomorphism from I to I′ . For two instances I and I′ and schemata S′ ⊆ S we write I ≡S′ I′ when I and I′ are isomorphic when restricted to relations from S′ .

2.1 The Chase

For a given set T of TGDs and an input instance I, the Oblivious T -Chase (or simply T -Chase from now on) produces the universal model of T and I, i.e., a model that can be homomorphically embedded in any other model of T and I. The construction is done by exhaustively applying so-called triggers on the intermediate instances constructed so far.

A T -trigger on an instance I is a pair (ϕ, h) composed of a TGD ϕ from T and a homomorphism h : body(ϕ)→I. An application of a trigger (ϕ, h) to I returns a fresh instance 1 I′ = I ∪ {h′ (head(ϕ))}, where the homomorphism h′ ⊇ h maps each existentially quantified variable from head(ϕ) to a fresh null from N. An application of such trigger is denoted with I(ϕ, h)I′ .

We say that a (possibly infinite) sequence of instances I0, I1, . . . (called intermediate instances) is a T - chase sequence whenever it satisfies:

1 Note that we identify formulae with structures and vice versa.

• for each index i there exists a T -trigger (ϕi, hi) such that Ii(ϕi, hi)Ii+1 holds, and
• for all indices i < j once the trigger applications Ii(ϕi, hi)Ii+1 and Ij(ϕj, hj)Ij+1 are given, the inequality (ϕi, hi) ̸= (ϕj , hj) holds, and
• for each i if there exists a trigger (ϕ, h) on instance Ii then there exists j such that (ϕj , hj) = (ϕ, h).

Given a T -Chase sequence I0, I1, . . . we define its result as a union ⋃∞i=0 Ii. It is well-known [Grahne and Onet, 2018] that the order of application of triggers does not matter in Oblivious Chase: it leads eventually to the same structure (finite or not), up to renaming of the nulls. Henceforth, we denote with Ch(T , D) the result of the T -Chase procedure on D (which is equal to the result of any T -Chase sequence that is starting from D). We say that the T -Chase on D is terminating when the resulting instance is finite.

2.2 Undecidability of AIOCTP

In the All-Instances Oblivious Chase Termination Problem (abbreviated as AIOCTP) we ask if, for given set of TGDs T , the T -Chase terminates on all possible databases D. It was recently shown in [Gogacz and Marcinkowski, 2014]:

Theorem 2.1. The AIOCTP is undecidable.

Theorem 2.2. The AIOCTP for the class of binary singlehead TGDs is EXPSPACE-hard.

Moreover, it was observed by Marnette [Marnette, 2009] that to decide all-instance termination for the oblivious T - Chase, it is sufficient to restrict the problem to the termination on a very specific database called the critical instance. For a given schema S, the critical instance IScr is simply a database containing a single constant s, called the source, and all atoms of the form R(s, s, . . . , s) where R ∈ S. The main property of the critical instance is presented below:

Lemma 2.3 ([Marnette, 2009]). For any set of TGDs T over a schema S, the T -Chase terminates on all databases D if and only if the T -Chase terminates on the critical instance IScr .

The Conway function g : N → N is defined as:

Now we present the main undecidable problem used in our reduction, namely the boundedness of Conway functions. Fix a natural number n ∈ N. Let πn be a product of n prime numbers and let q0, q1, . . . , qπn-1, r0, r1, . . . , rπn-1 be natural numbers such that for every m ∈ N congruent to j modulo πn the fraction m · qj rj is a natural number.

The Conway set G is defined as {gi (2) : i ∈ N}, i.e., the smallest set containing 2 and closed under applications of g. It is known that checking if G is bounded is undecidable [Gogacz and Marcinkowski, 2014, Sec. 3.2-3.3].

Lemma 2.4. For a given natural numbers n, πn and qi, ri for i ∈ [0, πn), the problem of deciding finiteness of G is undecidable.

Without losing undecidability status of the above problem, we may assume that the sequence g(2), g2 (2), g3 (2), . . . is non-decreasing. It implies that for a finite Conway set G the sequence gn (2) will eventually be constant.

3 Undecidability Proof

This section is entirely devoted to the proof of the main theorem in our paper, namely:

Theorem 1.1 (restated). All-Instances Oblivious Chase Termination is undecidable for sets of binary single-head TGDs.

The proof of Theorem 1.1 is done by a reduction from the boundedness of Conway functions. We recall that n, πn, g and G = {gn (2): n ∈ N} are fixed and defined as in Section 2.2. Note that by applying Lemma 2.3 and Lemma 2.4, one can conclude that in order to show the main result it is sufficient to find a set Tall of TGDs such that:

Lemma 3.1. The Tall-chase terminates on the critical instance Icr iff the Conway set G is bounded.

Constructing such set of TGDs, even when there is no restriction on the arity of relations, is no easy feat. It can already be seen in [Gogacz and Marcinkowski, 2014] that working with the critical instance is a tedious fight. As our reduction shares some of the ideas with the mentioned work, it needs to overcome the same (and even a few more) problems. We briefly discuss our main ideas in the context of the existing works of Gogacz and Marcinkowski.

The TGDs used in the undecidability proof in [Gogacz and Marcinkowski, 2014] build a path starting from a critical instance. For every vertex v on such a path the chase computes a "private" Conway set Gv of v, where the numbers in Gv are implicitly represented as the distances between v and the other vertices from the path. When the source "gets" into the Conway set Gv then v is allowed to give birth to the next node on the path. The machinery required for computing Gv in their work employed multiplication and hence it lead to seemingly inherent ternarity of their construction: to say that one segment is c times longer than the other one they need to name two such segments in a single relation and thus the presence of three vertices in one atom were required.

In our construction, instead of just building a path, we build a whole binary tree. The beauty of the construction is that it allows us to uniquely identify the L∗R-ancestor of each node in a tree. Moreover, it grants us the ability to specify that a certain condition holds for nodes u, v and "the unique ancestor of u" rather to quantify over triples of elements. Continuing the idea from Gogacz et al., each node v in a tree also computes its own Conway set Gv and gives birth to two new children if v "reaches" the source via Gv. It means that if the G is unbounded then the new vertices will be created indefinitely.

3.1 Schema and Treelike Instances

We define a schema S composed of the following relations:

• Src(x) a unary relation used to distinguish the source from other nodes (no TGD will use Src in its head).

L(x, y) "left" successor relation.

• R(x, y) "right" successor relation. Relations L and R are used to construct the set of edges in treelike instances defined later.

E(x, y) a binary relation denoting "left or right" successor.

• Rei(x, y) for any i ∈ [0, πn-1] is a binary relation denoting that the distance between x and y modulo πn is equal to i.

Sp(x, y) a binary relation stating that x is on the side path of y. This relation along with the next one is the main building block used in encoding multiplication in treelike structures.

Lvl(x, y) a binary relation connecting relevant vertices on equal "depth".

Multi(x, y) for any i ∈ [0, πn - 1] is a binary relation that works closely with the Sp relation to encode multiplication.

G(x, y) a binary relation denoting that the distance between x and y is in G.

Families of Treelike Instances

Analyzing the intermediate instances produced by the chase is a tedious task. To make such reasoning significantly easier, one can define a family of instances having some "neat" properties, i.e., satisfying the following: when G is bounded, rather than showing that the chase terminates, we can observe that all intermediate instances are contained in some finite structure from such family; otherwise, intermediate instances will contain bigger and bigger members of this family. Hence, analysing the chase boils down to analysing such family. In this section, we present three such families. Before we follow, let us stress that all paths in instances from T go up toward the source (rather than go down as usual in computer science).

Let us move to the definition of the first family of instances. We encourage the reader to take a look at Figure 1.

Definition 3.2 (family T). For any i ∈ N let Ti be a full binary tree of depth i with successor relations L and R such that:

• the root is replaced with the source and
• if x is a node from Ti and xl (resp. xr) is its left (resp. right) child, then Ti |= L(xl, x) (resp.Ti |= R(xr, x)) holds.

The family T is defined as a set {Ti | i ∈ N}.

Observe that the instance T0 is equivalent to the critical instance IScr Note that due to the treelike nature of the family T we can distinguish leafs and the root in instances from T.

Paths. Let I be an instance over S and let x and y be two of its nodes. If x is connected to y by a directed path p composed of relations from some S′ ⊆ S we say that the path p is an S′ -restricted path. Also, for a regular language L over S a path p is L-restricted if there exists a word from L that is a naturally corresponding to relations used by p. For a path p we denote its length with |p|.

Distances. We discuss the notion of the distance in the instances from T family. Henceforth let us fix a natural number i and an instance I ≡{L,R} Ti. Let x, y be nodes from I. Contrary to what was expected here, we cannot simply define the distance between nodes x and y as the length of the {L, R}- restricted path between those nodes. When the source is the endpoint of a path it warps the natural notion of distance due to its L and R loops. Hence, we employ a more complicated definition using a set-based approach. With dist(x, y) we denote the set of all |p| for p being a {L,R}-restricted path from x to y, i.e. the set of all possible "distances" from x to y. Note that there are only three possible cardinalities of the distance set: 0, 1 or ∞. If nodes x, y are not connected by a directed {L,R}-restricted path then |dist(x, y)| = 0, if x and y are connected and y is not the root then |dist(x, y)| = 1 and otherwise |dist(x, y)| = ∞. While this definition is a bit confusing it is quite important one as the construction would not work properly with L and R absent from the source.

Side paths. The notion of a side path plays an instrumental role in our construction. Let us fix an instance I ≡{L,R} Ti. For any given node y ∈ I the side path of y is the set of nodes x s.t. there is a (L∗R)-restricted path from x to y. Moreover for any x from the side path of y, we say that y is the side parent of x. We stress that every node from I has a unique side parent.

As a next step, we define the family Tbuilt .

Definition 3.3 (family Tbuilt ). For any natural number i the instance Tbuilt i is defined as the minimal instance satisfying Ti ≡{L,R} Tbuilt i such that all following conditions hold for any two nodes x, y ∈ Tbuilt i :

• Tbuilt i |= E(x, y) holds if and only if Tbuilt i |= L(x, y) holds or Tbuilt i |= R(x, y) holds.
• Tbuilt i |= Rej(x, y) if and only if there exists a {L,R}- restricted path of length k connecting x and y such that k is congruent to j (modulo πn).
• Tbuilt i |= Sp(x, y) if and only if there is a (L∗R)- restricted path from x to y.
• Tbuilt i |= Lvl (x, y) if and only if there exists a node z ∈ Tbuilt i and a natural number k such that Tbuilt i |= Sp(y, z) ∧ Ek (x, z) ∧ Ek (y, z) holds.
• Tbuilt i |= Multj(x, y) if and only if there exists a node z witnessing Sp(x, z) such that all values v ∈ dist(x, z) satisfy qj rj · v ∈ dist(x, y).

The family Tbuilt is defined as a set {Tbuilt i | i ∈ N}.

z

x

Figure 4: The relation Multj. Observe that the third vertex y is uniquely defined as a side parent of x.

One may wonder about the purpose of instances from Tbuilt family. Those instances are simply nodes from the previously defined family T equipped with a framework for computing the Conway set G. On the other hand, looking somewhat further ahead, the instance Tbuilt i is exactly the result of starting the Tbuild-chase on Ti, where the set of TGDs Tbuild is going to be defined soon. We postpone the definition of the TGDs until Section 3.2, as we believe that it is easier to grasp the meaning of relations from S and hence the proof, by understanding those "declarative" definitions first.

Most of the properties of Tbuilt family are easy to understand, except the property of relations Multj. Along those lines lies the essence of our proof as the binary relation Sp neatly stores (with a help from side paths) the ternary relation responsible for multiplication. We strongly encourage the reader to take more time in visualising the family Tbuilt and taking a look at the Figures 2-4.

Finally, we define the last family of tree-like instances required in our undecidability proof. Similarly to the previous case, one may think that those instances are constructed by the chase on Tbuilt i . One can also view Tcomp i as an instance Tbuilt i after computation of Conway set G reaches a fixed point due to the limited depth of the instance.

Definition 3.4 (family Tcomp i ). For any natural number i the instance Tcomp i is defined as a minimal instance satisfying Tcomp i ≡S\{G} Tbuilt i such that for any two nodes x and y from Tcomp i , the condition Tcomp i |= G(x, y) holds iff there exists k ∈ dist(x, y) which also belongs to the Conway set G. The family Tcomp is defined as the set {Tcomp i | i ∈ N}.

3.2 Tuple Generating Dependencies

Now, once the intended meaning of all relations is known, we define the set of TGDs Tall containing fourteen TGDs. Whilst this number may seem overwhelming, this set can be easily divided into three parts having a coherent and hopefully easy to grasp meaning. We divide the set Tall as follows: TGDs from 1 to 10 are denoted with Tbuild, TGDs from 11 to 12 are denoted with Tcomp and the set of the last two TGDs is denoted with Tgrow. We also note that the TGDs 4, 9, 10 and 12 are actually sets of TGDs (having one TGD per each i ∈ [0, πn-1]) rather than just single rules. Note that TGDs from Tcomp and Tbuild are datalog, while TGDs from Tgrow are existential.

The first two TGDs are responsible for building the relation E over the relations L and R so that E can act as the disjunction L ∨ R in the TGDs appearing later. Also, to simplify the forthcoming TGDs, for the relation L (and analogously for R and E) we use Li (x0, xi) as a syntactic sugar for L(x0, x1) ∧ L(x1, x2) ∧ . . . ∧ L(xi-1, xi).

TGDs 3-4 construct the relation Rei such that Rei(x, y) holds for nodes x and y if the distance from x to y is equal to i modulo πn.

The sole purpose of TGDs 5-8 is to build relations Sp and Lvl (see also Figures 2 and 3).

The TGDs above are responsible for constructing the relationMulti which serves as a way (along with the Lvl relation) to simulate multiplication in our construction (see Figure 4). The set Tbuild of TGDs (i.e., TGDs from 1 to 10) serves as a building mechanism. This mechanism is meant to be able to extend a number of relations over some treelike instances (more precisely the instance Ti from Definition 3.2).

The computation of a Conway set is done with the TGDs 11 and 12, defined above. The TGD 12 may look complicated, but it is a crucial element of our proof as the body of that rule is able to extract a "hidden" ternary information. Figures 5-8 might shed some light onto these TGDs.

The last two TGDs (denoted with Tgrow) are the only existential rules in Tall. Those TGDs are used to enlarge instances and to make them look similar to the full binary trees. Notice connection between those two rules and a family of treelike instances T.

The following observation about TGDs 13-14 will prove useful later:

Observation 3.5. Every node of Ch(Tall, Icr), except the source, has at most one child connected by L and at most one connected by R.

3.3 FromUnboundedness to Nontermination

In this section we show that if the Conway set G is infinite then the Tall-chase does not terminate on the critical instance IScr . Let us, for the rest of this section, define I as the set of all intermediate instances of the Tall-chase run on IScr .

Lemma 3.6. If G is not finite then the Tall-chase does not terminate on the critical instance IScr .

Note that a single step of the chase can increase the structure only by a single atom. Hence it is sufficient to show that the sequence of intermediate instances from the Tall-chase run on IScr (= T0) contains arbitrarily large instances:

Lemma 3.7. If G is infinite then for every natural number i there exists an intermediate instance I ∈ I such that Ti ⊆ I.

To show Lemma 3.7 we employ an inductive reasoning in which the following lemma plays the central role:

Lemma 3.8. If G is infinite then for every natural number i:

• if there exists an instance I ∈ I containing Tbuilt i then there exists an instance I′ ∈ I containing Tcomp i
• if there exists an instance I ∈ I containing Ti then there exists an instance I′ ∈ I containing Tbuilt i
• if there exists an instance I ∈ I containing Tcomp i then there exists an instance I′ ∈ I containing Ti+1

Proof. Therein we present only the second claimed property. We believe that it is both the most essential and the most difficult bit of our construction. Let us define Ibuild as the restriction of the instance I to the image of the injective homomorphism witnessing Tbuilt i ⊆ I. Observe that from the definition of the family Tcomp i , it is sufficient to show that for every natural number k and any vertices x, y ∈ Ibuild the following implication holds: if gk (2) ∈ dist(x, y) then Ch(Tall, T0) |= G(x, y). We prove it by induction over k. In the proof the only TGDs in use are TGDs 11-12 hence it might be helpful to take a look at Figures 5-8. The base of the induction is trivially satisfied as TGD 11 ensures that any two vertices connected by a path of length 2 in Ibuild are connected by the G edge in Ch(Tall, T0).

Let us pick a pair of nodes x and z from Ibuild that are connected by a {L, R}-restricted path of length gk+1 (2). We will show that there exists a trigger in the instance Ibuild for TGD 12 such that its head is mapped to vertices x and z. Let y be a node on {L,R}-restricted path from x to z such that gk (2) ∈ dist(x, y). Thus from the induction hypothesis we infer that Ibuild |= G(x, y). If y is the source then y = z and from the fact that Ibuild |= G(x, y) we conclude that Ibuild |= G(x, z). Let us consider the case when u is not the source. Let x′ ∈ Ibuild be the node such that Ibuild |= Sp(x′ , y) holds and x′ satisfies gk (2) ∈ dist(x′ , y). Notice that by the definition of Tbuilt i we know that Lvl connects x and x′ in Ibuild. Observe that Rej(x, y) holds in Ibuild for j ≡ gk (2) mod πn. Finally, we need to show that Multj(x′ , z) holds in Ibuild. By employing the definition of Tbuilt i , it is sufficient to show that every v ∈ dist(x′ , y) satisfies qj rj · v ∈ dist(x′ , z). We know that y is not the source so set dist(x′ , y) contains only gk (2). See that the following holds:

We know gk+1 (2) ∈ dist(x, z) = dist(x′ , z), which implies the satisfaction of Ibuild |= Mult i(x′ , z). Hence we conclude that there is the required trigger for the TGD 12 in Ibuild, which when applied, connects x and z by the relation G. From the definition of the chase sequence we know that each trigger is eventually applied, which guarantees the existence of the demanded instance.

3.4 FromBoundedness to Termination

It remains to prove that if the Conway set G is bounded then the Tall-chase terminates on the critical instance IScr . Here we really reap the benefits of our declarative definitions from Section 3.1 and avoid the tedious work with the ever-expanding chase. The following observations come from the definition of the family Tcomp .

Observation 3.9. For every i the instance Ch(Tbuild ∪ Tcomp, Tcomp i ) is isomorphic to Tcomp i .

Observation 3.10. If G is bounded then in Tcomp max(G)+1 no leaf is connected by a G-edge with the source.

We employ these two observations to prove the following: Lemma 3.11. If G is finite then the Tall-chase terminates on the critical instance.

Proof. We will show that every intermediate instance of Tallchase on the critical instance IScr is contained within a finite instance Tcomp max(G)+1 (existing due to fact that G is bounded) and thus the chase terminates. First observe that IScr is trivially contained in Tcomp max(G)+1 . Let us take a trigger (ϕ, h) and any pair of intermediate instances I and I′ from Tall-chase run on IScr such that I(ϕ, h)I′ holds. Suppose that I ⊆ Tcomp max(G)+1 holds and we will prove that I′ ⊆ Tcomp max(G)+1 holds. Let λ be an injective homomorphism witnessing the fact that I ⊆ Tcomp max(G)+1 holds. If a TGD ϕ belongs to Tbuild ∪ Tcomp then trivially from Observation 3.9 we infer I′ ⊆ Tcomp max(G)+1 . Otherwise ϕ is contained in Tgrow. W.l.o.g suppose that ϕ is the TGD 13. When the TGD ϕ was fired, it created the "left" child of some node. From Observation 3.5 we can immediately conclude that ϕ was applied to a node v ∈ I not having a left child, such that I |= G(v, s) holds (where s is the source). By Observation 3.10 we infer that v corresponds through λ to a non-leaf node in Tcomp max(G)+1 but then it is easy to extend λ to also witness I′ ⊆ Tcomp max(G)+1 as follows: let u be a freshly created node and λ(u) be equal to the left child of λ(v).

The above lemma, together with Lemma 3.6 from the previous section, allows us to conclude the correctness of Lemma 3.1 and thus the correctness of the main theorem.

4 Conclusions

In this paper, we have shown that the All-Instance Oblivious Chase Termination Problem for the class of single-head binary TGDs is undecidable. By arguing along the lines of (Subsection 3.5 in [Gogacz and Marcinkowski, 2014]) we may also conclude undecidability of All-Instances Termination for the Standard chase and for the Semi-Oblivious chase. It is fair to say that the presented proof is quite technical. We encoded the boundedness problem of Conway functions in the growing structure of the chase executed on the critical instance. The main obstacle was to encode the multiplication function, which is inherently ternary and was used e.g. in [Gogacz and Marcinkowski, 2014]. To avoid ternarity we force the structure generated by the chase to be a binary tree and employ the idea of the side paths to uniquely identify certain elements.

A natural direction for further investigation could be as follows: is there any non-trivial and well-known class of TGDs of arbitrary arity, which also causes undecidability of All-Instances chase Termination? Natural candidates are classes of weakly sticky-join [Cal`ı et al., 2010], glut-frontierguarded [Kr¨otzsch and Rudolph, 2011] or model faithfulacyclic [Grau et al., 2013] TGDs, since they are the most expressive among other TGD classes.