All-Instances Restricted Chase Termination

TL;DR

This paper investigates the problem of whether the restricted chase procedure terminates for all databases given certain classes of dependencies, showing that for guarded and sticky single-head TGDs, this problem is decidable.

Contribution

It proves that all-instances restricted chase termination is decidable for guarded and sticky single-head TGDs, extending understanding beyond the oblivious chase.

Findings

Decidability of all-instances restricted chase termination for guarded TGDs

Decidability of all-instances restricted chase termination for sticky TGDs

Extension of chase termination results to the standard (restricted) chase

Abstract

The chase procedure is a fundamental algorithmic tool in database theory with a variety of applications. A key problem concerning the chase procedure is all-instances termination: for a given set of tuple-generating dependencies (TGDs), is it the case that the chase terminates for every input database? In view of the fact that this problem is undecidable, it is natural to ask whether known well-behaved classes of TGDs ensure decidability. We consider here the main paradigms that led to robust TGD-based formalisms, that is, guardedness and stickiness. Although all-instances termination is well-understood for the oblivious version of the chase, the more subtle case of the restricted (a.k.a. the standard) chase is rather unexplored. We show that all-instances restricted chase termination for guarded and sticky single-head TGDs is decidable.

Equations

$$\displaystyle v(x)\ =\ \left\{\begin{array}[]{ll}h(x)&\text{if }x\in\mathsf{fr}(\sigma),\\ &\\ c_{\sigma,h}^{x}&\text{otherwise.}\end{array}\right.$$

$$J=I\cup \{\mathsf{result}(\sigma ,h)\},$$

$${\sigma }_1:P(x,y)\to R(x,y)$$

$${\sigma }_2:P(x,y)\to S(x)$$

$$\{P(a,b),R(a,b),S(a),R(a,c)\},$$

$$\begin{array}[]{rcl}\mathbb{CT}_{\forall\forall}^{\mathsf{res}}&=&\left\{{\mathcal{T}}\ :\begin{array}[]{l}\text{ for {\em every} database }D,\\ \text{ {\em every} valid restricted chase derivation}\\ \text{ of }D\text{ w.r.t.~{}}{\mathcal{T}}\text{ is finite}.\end{array}\right\}\end{array}$$

$$\displaystyle I_{i}^{n+1}\ =\ \left\{\begin{array}[]{ll}I_{i}^{n}&0\leq i\leq\ell\\ &\\ I_{i-1}^{n}\cup\{\mathsf{result}(\sigma,h)\}&i>\ell\end{array}\right.$$

$$\{⟨\alpha ,\beta ⟩:\alpha \in D\text{ and }\beta \in \mathsf{ochase}(D,\mathcal{T})\setminus D\}\cup {\prec }_p\cup {\prec }_s^{-1},$$

$$\{{\alpha }^{\infty }\}\cup \{R(t_1,\dots ,t_n)\in D:t_1,\dots ,t_n\text{ occur in }{\alpha }^{\infty }\}.$$

$${\sigma }_1$$

$${\sigma }_2$$

$${\sigma }_3$$

$${\Lambda }_{\mathcal{T}}=\mathsf{sch}(\mathcal{T})\times (\{F\}\cup \mathcal{T})\times {\mathcal{EQ}}_{\mathcal{T}}$$

$${\prec }_b=\{⟨x,y⟩:x,y\in V,\mathsf{org}(x)=F\text{ and }\mathsf{org}(y)\ne F\}\cup {\prec }_p\cup {\prec }_s^{-1}.$$

$$\displaystyle\mathsf{rank}(c)\ =\ \left\{\begin{array}[]{ll}0&\text{if }c\in\mathsf{dom}(D),\\ &\\ 1+\max\{\mathsf{rank}(c^{\prime}):c^{\prime}\prec_{p}^{\mathit{t}}c\}&\text{otherwise.}\end{array}\right.$$

$$R\left(c_{[(\alpha ,1){]}_{{\simeq }_{L^{♠}\cup B^{♠}}^{\ast }}},\dots ,c_{[(\alpha ,n){]}_{{\simeq }_{L^{♠}\cup B^{♠}}^{\ast }}}\right),$$

$$R(x,y,y)\to \exists zR(x,z,y),R(z,y,y)R(x,y,z)\to R(z,z,z).$$

$$\{⟨v,u⟩:v{\prec }_{p}u\text{ and, with }\tau (u)=(\sigma ,h),h(\mathsf{guard}(\sigma ))=\lambda (v)\}.$$

$$\{{\alpha }^{\infty }\}\cup \{\beta \in D:\beta {\subseteq }_{\pi }{\alpha }^{\infty }\text{ for some sideatom type }\pi \}.$$

$$K^{\prime }=K\cup \{\mathsf{result}(\sigma ,h):(\sigma ,h)\in S\},$$

$$K_i\cup \{\mathsf{result}({\sigma }_i^{\mathcal{I}},h):({\sigma }_i^{\mathcal{I}},h)\in S_i\},$$

$$\{(i,j):i\ge 0\text{ and }0\le j<|K_{i+1}\setminus K_i|\}.$$

$${\varphi }_{fin}(A)$$

$${\varphi }_{\pi }(x,y)$$

$${\varphi }_b(x,y)$$

$$\forall x\forall A(\forall y({\varphi }_b(y,x)\leftrightarrow y\in A)\to {\varphi }_{fin}(A))$$

$$\forall x\forall y\left(x\text{Yleft}y\wedge \mathsf{org}(y)=\sigma \to \underset{i\in \{1,\dots ,k\}}{\bigwedge }\exists z{\varphi }_{{\pi }_i}(z,y)\right)$$

$$\forall x\neg {\varphi }_b(x,x)$$

$${\mathcal{A}}_{\mathcal{T}}=\bigcup _{(e,\Pi )\in {\mathsf{etp}}_{\mathcal{T}}}{\mathcal{A}}_{e,\Pi }.$$

$$\displaystyle=\ \left\{\begin{array}[]{ll}\mathit{reject}&\text{ if }\alpha_{i}^{\diamondsuit}\prec_{s}\alpha_{j}^{\diamondsuit}\text{ for some }i<j,\\ &\\ (\Theta_{j+1},\mathsf{et}(\alpha_{j+1}^{\diamondsuit}))&\text{otherwise.}\end{array}\right.$$

$$\{i\in \{1,\dots ,\mathsf{ar}(\mathcal{T})\}:\text{ there is }j\in \Pi \text{ such that }\gamma [j]=\mathsf{head}(\sigma )[i]\}.$$

$$\begin{gathered} \{\alpha \in L^{♢}:\text{ there exists }j>0\text{ such that } \\ \mathsf{result}({\sigma }_j^{♢},h_j^{♢})\in B_i^{♢},\text{ and }\alpha \in h_j^{♢}(\mathsf{body}({\sigma }_j^{♢}))\}, \end{gathered}$$

Full text

1. Introduction

The chase procedure (or simply chase) is a fundamental algorithmic tool that has been applied to several database problems such as computing data exchange solutions (Fagin et al., 2005), and query answering and containment under constraints (Calì et al., 2013; Aho et al., 1979), to name a few. The chase takes as input a database $D$ and a set ${\mathcal{T}}$ of constraints – which, for this work, are tuple-generating dependencies (TGDs) of the form $\forall\bar{x}\forall\bar{y}\left(\phi(\bar{x},\bar{y})\rightarrow\exists\bar{z}\,\psi(\bar{x},\bar{z})\right)$ with $\phi$ and $\psi$ being conjunctions of atoms – and, if it terminates, its result is a finite instance $D_{\mathcal{T}}$ that is a universal model of $D$ and ${\mathcal{T}}$, i.e., a model that can be homomorphically embedded into every other model of $D$ and ${\mathcal{T}}$. This is the reason for the ubiquity of the chase as discussed in (Deutsch et al., 2008). Indeed, many central database problems, which involve reasoning with TGDs, can be solved by simply exhibiting a universal model. And this is not only in theory. Despite the fact that the instance constructed by the chase can be very large, efficient implementations of the chase procedure have been successfully applied during the last few years in many different contexts (Benedikt et al., 2017; Krötzsch et al., 2019; Nenov et al., 2015; Urbani et al., 2018).

The Chase In a Nutshell.

Roughly speaking, the chase adds new tuples to the database $D$ (possibly involving null values that act as witnesses for the existentially quantified variables), as dictated by the TGDs of ${\mathcal{T}}$, and it keeps doing this until all the TGDs of ${\mathcal{T}}$ are satisfied. There are, in principle, two different ways for formalizing this simple idea, which lead to different versions of the chase procedure. The first one, which gives rise to the oblivious chase, is as follows: for each pair $\bar{t},\bar{u}$ of tuples of terms from the instance $I$ constructed so far, trigger a TGD $\forall\bar{x}\forall\bar{y}\left(\phi(\bar{x},\bar{y})\rightarrow\exists\bar{z}\,\psi(\bar{x},\bar{z})\right)$ if $\phi(\bar{t},\bar{u})\subseteq I$, and add to $I$ the set of atoms $\psi(\bar{t},\bar{v})$, where $\bar{v}$ is a tuple of new terms not occurring in $I$. The second way, which leads to the restricted (a.k.a. standard) chase, is a refinement of the above with the additional condition that, for a pair $\bar{t},\bar{u}$ of tuples of terms, a TGD $\forall\bar{x}\forall\bar{y}\left(\phi(\bar{x},\bar{y})\rightarrow\exists\bar{z}\,\psi(\bar{x},\bar{z})\right)$ is triggered not only if $\phi(\bar{t},\bar{u})\subseteq I$, but also if there is no tuple $\bar{v}$ of terms from $I$ such that $\psi(\bar{t},\bar{v})\subseteq I$, i.e., if the TGD is not already satisfied. Thus, the key difference between the oblivious and restricted versions of the chase is that the former triggers a TGD whenever the left-hand side of the implication is satisfied, while the latter triggers a TGD only if it is violated.

It should be clear that the restricted chase, in general, builds much smaller instances than the oblivious one. Actually, it is very easy to devise an example where, according to the restricted chase, none of the TGDs should be triggered, while the oblivious chase builds an infinite instance. Consider, e.g., the database $D=\{R(a,b)\}$ and the TGD $\forall x\forall y(R(x,y)\rightarrow\exists z\,R(x,z))$. The restricted chase will detect that the database already satisfies the TGD, while the oblivious chase will build the infinite instance $\{R(a,b),R(a,\nu_{1}),R(a,\nu_{2}),\ldots\}$, where $\nu_{1},\nu_{2},\ldots$ are (labeled) nulls. Consequently, the restricted chase has a clear advantage over the oblivious chase when it comes to the size of the result. But, of course, this advantage does not come for free: at each step, the restricted chase has to check that there is no way to satisfy the right-hand side of the TGD at hand, and this is costly. However, as it has been recently observed, the benefit from producing much smaller instances can justify the effort of checking whether a TGD is already satisfied; see, e.g., (Benedikt et al., 2017; Krötzsch et al., 2019).

1.1. The Challenge of Non-termination

As said above, there are nowadays efficient implementations of the restricted chase that allows us to solve central database problems by adopting a materialization-based approach (Benedikt et al., 2017; Krötzsch et al., 2019; Nenov et al., 2015; Urbani et al., 2018). But, of course, for this to be feasible in practice we need a guarantee that the restricted chase terminates, which is not always the case. This fact motivated a long line of research on identifying fragments of TGDs that ensure the termination of the restricted chase, for every input database. A prime example is the class of weakly-acyclic TGDs (Fagin et al., 2005), which is the standard language for data exchange purposes. A similar formalism, called constraints with stratified-witness, has been proposed in (Deutsch and Tannen, 2003). Many other sufficient conditions for the termination of the restricted chase can be found in the literature; see, e.g., (Deutsch et al., 2008; Deutsch and Tannen, 2003; Grau et al., 2013; Greco et al., 2011; Marnette, 2009; Meier et al., 2009) – this list is by no means exhaustive, and we refer the reader to (Greco et al., 2012) for a comprehensive survey.

With so much effort spent on identifying sufficient conditions for the termination of the restricted chase, the question that comes up is whether a sufficient condition that is also necessary exists. In other words, given a set ${\mathcal{T}}$ of TGDs, is it possible to decide whether, for every database $D$, the restricted chase on $D$ and ${\mathcal{T}}$ terminates? This has been addressed in (Gogacz and Marcinkowski, 2014), where it is shown that the answer is negative, even for the oblivious chase.

The undecidability proof in (Gogacz and Marcinkowski, 2014) constructs a sophisticated set of TGDs that goes beyond existing well-behaved classes of TGDs that enjoy certain syntactic properties, which in turn ensure favorable model-theoretic properties. Such well-behaved classes of TGDs have been proposed in the context of ontological reasoning. The two main paradigms that led to robust TGD-based formalisms, without forcing the restricted chase to terminate, are guardedness (Baget et al., 2011; Calì et al., 2013, 2012a) and stickiness (Calì et al., 2012b). A TGD is guarded if the left-hand side of the implication, known as the body of the TGD, has an atom that contains (or “guards”) all the universally quantified variables. On the other hand, sticky sets of TGDs are inherently unguarded, and their main goal is to express joins among relations that cannot be expressed via guarded TGDs (details are given in Section 2).

The fact that the set of TGDs given in the undecidability proof of (Gogacz and Marcinkowski, 2014) is far from being guarded or sticky brings us to the following question: is the restricted chase termination problem, as described above, decidable for guarded or sticky TGDs? This question is rather well-understood for the oblivious chase. In the case of guarded TGDs, the problem is 2EXPTIME-complete, and becomes PSPACE-complete for linear (one body-atom) TGDs (Calautti et al., 2015). The sticky case has been recently addressed in (Calautti and Pieris, 2019), where it is shown that the problem is PSPACE-complete. However, despite its clear advantage over the oblivious chase, we know very little about the restricted chase. It has been shown, independently of our work, that the problem is decidable for single-head (one atom in the head) linear TGDs (Leclère et al., 2019). However, nothing so far was known about guarded or sticky TGDs.

1.2. Research Challenges

We concentrate on guarded and sticky TGDs (in fact, single-head TGDs), and study the restricted chase termination problem. More precisely, we study the following: given a set ${\mathcal{T}}$ of single-head guarded or sticky TGDs, is it the case that for every database $D$, every restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$ is finite? It might be the case that some derivations are finite and some others are not, depending on the order that TGDs are triggered, which is not the case for the oblivious chase. The reason for this non-deterministic behavior is the fact that the restricted chase applies a TGD only if it is necessary (recall the restricted vs. oblivious chase discussion above). On the other hand, the oblivious chase applies TGDs whenever the body is satisfied, which ensures a deterministic behavior. Our ultimate goal is to show that the problem in question is decidable. Towards this direction, one has to overcome a couple of non-trivial technical issues, which were not so difficult in the case of the oblivious chase.

Dealing with Fairness.

The fairness condition is crucial in the definition of the chase in order to ensure that the result is indeed a model of the input database and set of TGDs. It states that each TGD that is violated at some point of the execution of the chase eventually will be satisfied. One of the main difficulties underlying our problem is to ensure fairness. In other words, focussing on the complement of our problem, it is not enough to simply check whether there exists a database that leads to an infinite derivation w.r.t. the set of TGDs, but we have to ensure that it is also fair.

As shown in (Calautti et al., 2015), for the oblivious chase, the existence of a (possibly unfair) infinite chase derivation implies the existence of a fair one, which in turn implies that we can completely neglect the fairness condition. The question that comes up is whether we can establish the same for the restricted chase, which will crucially simplify our task. Actually, this question has been already posed by Jan Van den Bussche some years ago in a different context (den Bussche, 2015). Showing such a result for the restricted chase is significantly more difficult than showing it for the oblivious chase. Note that the recent work (Leclère et al., 2019), which considers the restricted chase, establishes such a result, but only for single-head linear TGDs. Generalizing this to single-head guarded or sticky TGDs, or ideally to arbitrary single-head TGDs, is a non-trivial task. As we shall see, here is the place where we need the TGDs to be single-head.

Existence of a Critical Database.

It would be extremely useful to have a special database $D^{*}$ in place, let us call it critical, of a very simple form, that ensures the following: given a set ${\mathcal{T}}$ of TGDs, if there is a database that leads to an infinite chase derivation w.r.t. ${\mathcal{T}}$, then already $D^{*}$ does. With such a critical database in place, one can focus on the complement of our problem, and check whether $D^{*}$ leads to an infinite chase derivation w.r.t. the given TGDs.

For the oblivious chase such a critical database exists: it simply collects all the atoms of the form $R(c,\ldots,c)$, where $R$ is a relation that occurs in the given set of TGDs (Marnette, 2009), and $c$ an arbitrary constant. All the known decidability results about the oblivious chase heavily rely on the critical database $D^{*}$ (Calautti et al., 2015; Calautti and Pieris, 2019). It is an easy exercise, however, to show that $D^{*}$, as defined above, does not serve as a critical database in the case of the restricted chase. This brings us to the other technical challenge that we need to overcome, that is, the lack of an obvious database that can serve as a critical database. Let us say that (Leclère et al., 2019), which considers the restricted chase, follows the critical database approach. However, it is easy to see that for single-head linear TGDs (the main concern of (Leclère et al., 2019)) such a critical database is simply a database consisting of a single atom. This is far from being true for single-head guarded or sticky TGDs.

1.3. Summary of Contributions

Our main results (Theorem 5.1 and Theorem 6.1) state that, for a set ${\mathcal{T}}$ of single-head guarded or sticky TGDs, checking whether, for every database $D$, every restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$ is finite, is decidable in elementary time. To show these results, we had to establish a series of auxiliary results, related to the technical challenges discussed above. Our main contributions follow:

In Section 4, we establish the Fairness Theorem, which essentially states that, for single-head (not necessarily guarded or sticky) TGDs, we can neglect the fairness condition. This overcomes the first challenge raised in the previous subsection. Let us stress that this result does not hold once we go beyond single-head TGDs, which means that our decision to focus on single-head TGDs is not for simplicity, but it might be crucial for the validity of our main results. This has been also observed, independently of our work, in (Leclère et al., 2019).

In Section 5, we focus on guarded TGDs. We first characterize the existence of an infinite (possibly unfair) restricted chase derivation of a database $D$ w.r.t. a set ${\mathcal{T}}$ of single-head (not necessarily guarded) TGDs via the existence of an infinite subset $S$, called chaseable, of the instance $C_{D,{\mathcal{T}}}$ constructed by applying a variant of the oblivious chase on $D$ using ${\mathcal{T}}$. Such a chaseable set $S$ enjoys certain properties that allow us to convert it into an infinite restricted chase derivation of $D$ w.r.t.${\mathcal{T}}$. We then show that, for a set ${\mathcal{T}}$ of single-head guarded TGDs, the problem of deciding whether there is a database $D$ such that an infinite chaseable subset of $C_{D,{\mathcal{T}}}$ exists can be reduced to the satisfiability problem of Monadic Second-Order Logic (MSOL) over infinite trees of bounded degree. The correctness of this reduction relies on another key result of independent interest: if there is a database that leads to a (possibly unfair) infinite chase derivation w.r.t. ${\mathcal{T}}$, then there is an acyclic one with the same property.

Finally, in Section 6, we concentrate on sticky TGDs. Given a set ${\mathcal{T}}$ of sticky TGDs, we reduce the problem of deciding whether there exists a database $D$ such that an infinite (possibly unfair) restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$ exists to the emptiness problem of deterministic Büchi automata. This reduction relies on another key result of independent interest: there exists a database $D$ such that an infinite (possibly unfair) restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$ exists iff a so-called finitary caterpillar for ${\mathcal{T}}$ exists. The latter is essentially an infinite “path-like” restricted chase derivation of some database w.r.t. ${\mathcal{T}}$, and is precisely the existence of such an object that we check via a deterministic Büchi automaton.

2. Preliminaries

We consider the disjoint countably infinite sets $\mathbf{C}$, $\mathbf{N}$, and $\mathbf{V}$ of constants, (labeled) nulls, and variables (used in dependencies), respectively. We refer to constants, nulls and variables as terms. For an integer $n>0$, we may write $[n]$ for the set $\{1,\ldots,n\}$.

Relational Databases.

A schema $\mathbf{S}$ is a finite set of relation symbols (or predicates) with associated arity. We write $R/n$ to denote that $R$ has arity $n>0$; we may also write $\mathsf{ar}(R)$ for $n$. A position of $\mathbf{S}$ is a pair $(R,i)$, where $R/n\in\mathbf{S}$ and $i\in[n]$, that essentially identifies the $i$-th argument of $R$. An atom over $\mathbf{S}$ is an expression of the form $R(\bar{t})$, where $R/n\in\mathbf{S}$ and $\bar{t}$ is an $n$-tuple of terms. A fact is an atom whose arguments consist only of constants. We write $R(\bar{t})[i]$ for the term of $R(\bar{t})$ at position $(R,i)$, i.e., the $i$-th element of $\bar{t}$. For brevity, we may refer to the position $(R,i)$ in $R(\bar{t})$ simply as the $i$-th position of $R(\bar{t})$ and write $(R(\bar{t}),i)$. Moreover, for a variable $x$ in $\bar{t}$, let $\mathsf{pos}(R(\bar{t}),x)=\{(R,i):R(\bar{t})[i]=x\}$, i.e., is the set of positions at which $x$ occurs according to $R(\bar{t})$. An instance over $\mathbf{S}$ is a (possibly infinite) set of atoms over $\mathbf{S}$ that contain constants and nulls, while a database over $\mathbf{S}$ is a finite set of facts over $\mathbf{S}$. The active domain of an instance $I$, denoted $\mathsf{dom}(I)$, is the set of all terms in $I$.

Substitutions and Homomorphisms.

A substitution from a set of terms $T$ to a set of terms $T^{\prime}$ is a function $h:T\rightarrow T^{\prime}$ defined as follows: $\emptyset$ is a substitution, and if $h$ is a substitution, then $h\cup\{t\mapsto t^{\prime}\}$, where $t\in T$ and $t^{\prime}\in T^{\prime}$, is a substitution. The restriction of $h$ to $S\subseteq T$ is denoted $h_{|S}$. 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$ such that (i) $t\in\mathbf{C}$ implies $h(t)=t$, and (ii) $R(t_{1},\ldots,t_{n})\in A$ implies $h(R(t_{1},\ldots,t_{n}))=R(h(t_{1}),\ldots,h(t_{n}))\in B$.

Single-Head Tuple-Generating Dependencies.

A single-head tuple-generating dependency $\sigma$ is a constant-free first-order sentence $\forall\bar{x}\forall\bar{y}\left(\phi(\bar{x},\bar{y})\rightarrow\exists\bar{z}\,R(\bar{x},\bar{z})\right)$, where $\bar{x},\bar{y},\bar{z}$ are tuples of variables of $\mathbf{V}$, $\phi(\bar{x},\bar{y})$ is a conjunction of atoms, and $R(\bar{x},\bar{z})$ is a single atom. For brevity, we write $\sigma$ as $\phi(\bar{x},\bar{y})\rightarrow\exists\bar{z}\,R(\bar{x},\bar{z})$, and use comma instead of $\wedge$ for joining atoms. We refer to $\phi(\bar{x},\bar{y})$ and $R(\bar{x},\bar{z})$ as the body and head of $\sigma$, denoted $\mathsf{body}(\sigma)$ and $\mathsf{head}(\sigma)$, respectively. Henceforth, we simply say tuple-generating dependency (TGD) instead of single-head TGD. The frontier of the TGD $\sigma$, denoted $\mathsf{fr}(\sigma)$, is the set of variables $\bar{x}$, i.e., the variables that appear both in the body and the head of $\sigma$. The schema of a set ${\mathcal{T}}$ of TGDs, denoted $\mathsf{sch}({\mathcal{T}})$, is the set of predicates in ${\mathcal{T}}$, and we write $\mathsf{ar}({\mathcal{T}})$ for the maximum arity over all those predicates. An instance $I$ satisfies a TGD $\sigma$ as the one above, written $I\models\sigma$, if the following holds: whenever there exists a homomorphism $h$ such that $h(\phi(\bar{x},\bar{y}))\subseteq I$, then there exists $h^{\prime}\supseteq h_{|\bar{x}}$ such that $h^{\prime}(R(\bar{x},\bar{z}))\in I$. Note that, by abuse of notation, we sometimes treat a tuple of variables as a set of variables, and a conjunction of atoms as a set of atoms. The instance $I$ satisfies a set ${\mathcal{T}}$ of TGDs, written $I\models{\mathcal{T}}$, if $I\models\sigma$ for each $\sigma\in{\mathcal{T}}$.

Guardedness.

A TGD $\sigma$ is guarded if there exists an atom $\alpha$ in its body that contains all the variables occurring in $\mathsf{body}(\sigma)$ (Calì et al., 2013). The atom $\alpha$ is the guard of $\sigma$. In case there are more than one atoms that can serve as the guard of $\sigma$, then we fix the left-most such atom in $\mathsf{body}(\sigma)$ as the guard. We write $\mathsf{guard}(\sigma)$ for the guard of $\sigma$. The class of guarded TGDs, denoted $\mathbb{G}$, is defined as the family of all possible finite sets of guarded single-head TGDs.

Stickiness.

The goal of stickiness is to capture joins that are not expressible via guarded TGDs (Calì et al., 2012b). The key property is that variables occurring more than once in the body of a TGD should be inductively propagated (or “stick”) to the head-atom as follows

where the first set of TGDs is sticky, while the second is not. The formal definition is based on an inductive procedure that marks the variables that may violate the above property. Roughly, the base step marks a body-variable that does occur in the head. Then, the marking is inductively propagated from head to body as follows

Stickiness requires every marked variable to appear only once in the body of a TGD. The formal definition follows.

Consider a set ${\mathcal{T}}$ of single-head TGDs; we assume, w.l.o.g., that the TGDs in ${\mathcal{T}}$ do not share variables. Let $\sigma\in{\mathcal{T}}$ and $x$ a variable in $\mathsf{body}(\sigma)$. We inductively define when $x$* is marked in ${\mathcal{T}}$*:

1. (1)

if $x$ does not occur in $\mathsf{head}(\sigma)$, then $x$ is marked in ${\mathcal{T}}$, and 2. (2)

assuming that $\mathsf{head}(\sigma)=R(\bar{t})$ and $x\in\bar{t}$, if there is $\sigma^{\prime}\in{\mathcal{T}}$ with $R(\bar{t}^{\prime})$ in its body, and each variable in $R(\bar{t}^{\prime})$ at a position of $\mathsf{pos}(R(\bar{t}),x)$ is marked in ${\mathcal{T}}$, then $x$ is marked in ${\mathcal{T}}$.

The set ${\mathcal{T}}$ is sticky if there is no TGD with two occurrences of a variable that is marked in ${\mathcal{T}}$. Let $\mathbb{S}$ be the corresponding class.

3. The Chase Procedure

The chase procedure accepts as input a database $D$ and a set ${\mathcal{T}}$ of TGDs, and constructs an instance that contains $D$ and satisfies ${\mathcal{T}}$. Central notions in this context are the notion of trigger, and the notion of trigger application (see, e.g., (Grahne and Onet, 2018)).

Definition 3.1.

A trigger for a set ${\mathcal{T}}$ of TGDs on an instance $I$ is a pair $(\sigma,h)$, where $\sigma\in{\mathcal{T}}$ and $h$ is a homomorphism from $\mathsf{body}(\sigma)$ to $I$. We call $(\sigma,h)$ active if there is no extension $h^{\prime}$ of $h_{|\mathsf{fr}(\sigma)}$ such that $h^{\prime}(\mathsf{head}(\sigma))\in I$. We denote by $\mathsf{result}(\sigma,h)$ the atom $v(\mathsf{head}(\sigma))$, where $v$ is a mapping from the variables of $\mathsf{head}(\sigma)$ to $\mathbf{N}$ defined as

[TABLE]

An application of $(\sigma,h)$ to $I$ returns the instance

[TABLE]

and such an application is denoted as $I\langle\sigma,h\rangle J$.

In the definition of $\mathsf{result}(\sigma,h)$, each existentially quantified variable $x$ occurring in $\mathsf{head}(\sigma)$ is mapped by $v$ to a “fresh” null value of $\mathbf{N}$ whose name is uniquely determined by the trigger $(\sigma,h)$ and $x$ itself. Thus, given a trigger $(\sigma,h)$, we can unambiguously write down the atom $\mathsf{result}(\sigma,h)$. In our analysis, it would be useful to be able to refer to the terms in $\mathsf{result}(\sigma,h)$ that have been propagated (not invented) during the application of $(\sigma,h)$. Formally, the frontier of $\mathsf{result}(\sigma,h)$, denoted $\mathsf{fr}(\mathsf{result}(\sigma,h))$, are the terms of $\mathsf{result}(\sigma,h)$ that occur at the positions of $\bigcup_{x\in\mathsf{fr}(\sigma)}\mathsf{pos}(\mathsf{head}(\sigma),x)$.

3.1. The Real Oblivious Chase

Although this work is about the termination of the restricted chase, we use a variant of the oblivious chase, which we introduce below, as an auxiliary tool. The oblivious chase of a database $D$ w.r.t. a set ${\mathcal{T}}$ of TGDs is essentially the $\subseteq$-minimal instance $I_{D,{\mathcal{T}}}$ that contains $D$ and is closed under trigger applications, i.e., for every trigger $(\sigma,h)$ for ${\mathcal{T}}$ on $I_{D,{\mathcal{T}}}$, $\mathsf{result}(\sigma,h)\in I_{D,{\mathcal{T}}}$. It is well-known that it can be realized by starting from the database $D$, and applying (active or non-active) triggers, which have not been applied before, for the given set ${\mathcal{T}}$ of TGDs on the instance constructed so far, and keep doing this until a fixpoint is reached. It is also well-known that $I_{D,{\mathcal{T}}}$ is unique since it does not depend on the order in which we apply the triggers; for more details see, e.g., (Calautti and Pieris, 2019; Grahne and Onet, 2018).

Our intention is to use the (unique) oblivious chase of $D$ w.r.t. ${\mathcal{T}}$ as a predefined instance in which all the restricted chase derivations live (the formal definition of the restricted chase is given below). Thus, our task will be essentially to search in this instance for an infinite restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$. To this end, we need the parent relation over the oblivious chase, which essentially gives us the atoms that were involved in the trigger application that produced a certain atom. However, as the following simple example shows, this relation is, in general, not unique:

Example 3.2.

Consider the set ${\mathcal{T}}$ of TGDs consisting of:

[TABLE]

The oblivious chase of $D=\{P(a,b)\}$ w.r.t. ${\mathcal{T}}$ is the instance

[TABLE]

where $c$ is a null. However, its atoms could have been produced in different ways: by applying $\sigma_{1},\sigma_{2},\sigma_{4}$, or by applying $\sigma_{1},\sigma_{3},\sigma_{4}$. In the first case, the parent of $S(a)$ is $P(a,b)$, while, in the second case, is the atom $R(a,b)$. Thus, although the oblivious chase is unique, its ambiguous which atom is the parent of $S(a)$.

As the above example illustrates, if we want to know in an unambiguous way who are the parents of a certain atom by simply inspecting the oblivious chase, we need to rely on a more refined structure. This is the purpose of the so-called real oblivious chase.

Definition 3.3.

The real oblivious chase of a database $D$ w.r.t. a set ${\mathcal{T}}$ of TGDs is the smallest labeled directed graph $\mathsf{ochase}(D,{\mathcal{T}})=\langle V,\prec_{p},\lambda,\tau\rangle$, where $\lambda$ and $\tau$ assign atoms over $\mathsf{sch}({\mathcal{T}})$ and TGD-mapping pairs (including the empty pair $\bot$) to nodes, such that:

• •

For each atom $\alpha\in D$, there is a node $v\in V$ with $\lambda(v)=\alpha$, $\tau(v)=\bot$, and, for each $u\prec_{p}w$, $w\neq v$.

• •

For each TGD $\sigma\in{\mathcal{T}}$, with $\mathsf{body}(\sigma)=\{\gamma_{1},\ldots,\gamma_{m}\}$, for each mapping $h$ from the variables in $\mathsf{body}(\sigma)$ to $\mathbf{C}\cup\mathbf{N}$, and for each $(v_{1},\ldots v_{m})\in V^{m}$, if $h(\gamma_{1})=\lambda(v_{1}),\ldots,h(\gamma_{m})=\lambda(v_{m})$, then there exists $v\in V$ such that $v_{1}\prec_{p}v,\ldots,v_{m}\prec_{p}v$, $\lambda(v)=\mathsf{result}(\sigma,h)$, and $\tau(v)=(\sigma,h)$.

The elements of $\{\lambda(v):v\in V\}$ are the atoms of $\mathsf{ochase}(D,{\mathcal{T}})$, and the relation $\prec_{p}$ is the parent relation of $\mathsf{ochase}(D,{\mathcal{T}})$.

Here is a simple example that illustrates the real oblivious chase:

Example 3.4.

Let $D$ and ${\mathcal{T}}$ be the database and the set of TGDs from Example 3.2. Then, $\mathsf{ochase}(D,{\mathcal{T}})$ is the following directed graph (for clarity, the homomorphisms are omitted)

where $c$ is the null determined by the trigger $(\sigma_{4},\{x\mapsto a\})$.

Strictly speaking, $\prec_{p}$ is a relation over the node set of the real oblivious chase of $D$ w.r.t. ${\mathcal{T}}$. However, for notational convenience, from now on we will usually identify $\mathsf{ochase}(D,{\mathcal{T}})$ with its atoms, which clearly form a multiset, and we will see $\prec_{p}$ as a relation over this multiset of atoms. Let us also clarify that, although the real oblivious chase may generate several copies of the same atom, it will never produce an atom that is not generated by the oblivious chase, i.e., the oblivious chase coincides with the set consisting of the atoms of the real oblivious chase. The advantage of the real oblivious chase is that it provides a unique multiset instance where all the different restricted chase derivations live, and at the same time we can unambiguously refer to the parents of a certain atom.

Remark. The name “real oblivious” reflects the fact that an atom is generated and added to the instance under construction even if its already present. On the other hand, the oblivious chase, since it builds a set (not a multiset) of atoms, it implicitly checks, before applying a trigger $(\sigma,h)$, whether the atom $\mathsf{result}(\sigma,h)$ is already present. This somehow tells us that what we normally call oblivious chase is not completely oblivious, unlike the real oblivious one, which generates an atom no matter if it has been generated before.

Stop Relation.

Before we proceed further, let us introduce one more basic relation, in addition to the parent relation, which will be heavily used throughout the paper. This is the “stop” relation $\prec_{s}$ over $\mathsf{ochase}(D,{\mathcal{T}})$. Intuitively, $\alpha\prec_{s}\beta$ means that in the presence of $\alpha$ the atom $\beta$ is superfluous in the sense that the trigger $(\sigma,h)$ for ${\mathcal{T}}$ on an instance that contains $\alpha$, with $\beta=\mathsf{result}(\sigma,h)$, is not active due to the presence of $\alpha$. Formally, given two vertices $v,u$ of $\mathsf{ochase}(D,{\mathcal{T}})$ such that $\tau(u)=(\sigma,h)$, we say that $\lambda(v)$ stops $\lambda(u)$, denoted $\lambda(v)\prec_{s}\lambda(u)$, if there exists a homomorphism $h^{\prime}$ such that (i) $h^{\prime}(\lambda(u))=\lambda(v)$, and (ii) $h^{\prime}(h(x))=h(x)$ for every $x\in\mathsf{fr}(\sigma)$. Notice that two copies of the same atom in the real oblivious chase always stop each other. It is also easy to verify that the following holds, which relates the notion of active trigger with $\prec_{s}$:

Fact 3.5.

Let $I\subseteq\mathsf{ochase}(D,{\mathcal{T}})$, and $(\sigma,h)$ a trigger for ${\mathcal{T}}$ on $I$. Then, $(\sigma,h)$ is active iff there is no $\alpha\in I$ such that $\alpha\prec_{s}\mathsf{result}(\sigma,h)$.

3.2. The Restricted Chase

We now come to the main object of our study, that is, the restricted (a.k.a. standard) chase. Similarly to the oblivious chase, the main idea of the restricted chase is, starting from a database $D$, to apply triggers for the given set ${\mathcal{T}}$ of TGDs on the instance constructed so far, and keep doing this until a fixpoint is reached. However, unlike the oblivious chase, it only applies active triggers. This is formalized as follows. Consider a database $D$ and a set ${\mathcal{T}}$ of TGDs. We distinguish the two cases where the chase is terminating or not:

• •

A finite sequence $(I_{i})_{0\leq i\leq n}$ of instances, with $D=I_{0}$ and $n\geq 0$, is a restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$ if: for each $0\leq i<n$, there is an active trigger $(\sigma,h)$ for ${\mathcal{T}}$ on $I_{i}$ with $I_{i}\langle\sigma,h\rangle I_{i+1}$, and there is no active trigger $(\sigma,h)$ for ${\mathcal{T}}$ on $I_{n}$.

• •

An infinite sequence $(I_{i})_{i\geq 0}$ of instances, with $D=I_{0}$, is a restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$ if, for each $i\geq 0$, there exists an active trigger $(\sigma,h)$ for ${\mathcal{T}}$ on $I_{i}$ such that $I_{i}\langle\sigma,h\rangle I_{i+1}$. Moreover, $(I_{i})_{i\geq 0}$ is called fair if, for each $i\geq 0$, and every active trigger $(\sigma,h)$ for ${\mathcal{T}}$ on $I_{i}$, there exists $j>i$ such that $(\sigma,h)$ is a non-active trigger for ${\mathcal{T}}$ on $I_{j}$. Notice that in a fair derivation all the active triggers will eventually be deactivated, which is not true for unfair derivations.

A restricted chase derivation is called valid if it is finite, or infinite and fair. Infinite but unfair restricted chase derivations are not valid since they do not serve the main purpose of the chase procedure, i.e., build an instance that satisfies the given set of TGDs.

Restricted Chase Termination Problem

It is well-known that even for simple databases and sets of TGDs, we may have infinite chase derivations. The key question is, given a set ${\mathcal{T}}$ of TGDs, can we check whether, for every database $D$, every valid chase derivation of $D$ w.r.t. ${\mathcal{T}}$ is finite? Before formalizing this problem, let us recall a central class of TGDs:

[TABLE]

The superscript $\mathsf{res}$ in $\mathbb{CT}_{\forall\forall}^{\mathsf{res}}$ indicates that we concentrate on restricted chase derivations. The main problem tackled in this work is defined as follows, where $\mathbb{C}$ is a class of TGDs:

PROBLEM : $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{C})$

INPUT : A set ${\mathcal{T}}\in\mathbb{C}$ of TGDs.

QUESTION : Is it the case that ${\mathcal{T}}\in\mathbb{CT}_{\forall\forall}^{\mathsf{res}}$?

The above decision problem is, in general, undecidable. In fact, assuming that $\mathbb{TGD}$ is the class of arbitrary (single-head) TGDs:

Theorem 3.6 ((Gogacz and

Marcinkowski, 2014)).

$\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{TGD})$* is undecidable, even if we focus on binary and ternary predicates.*

But what about $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{G})$ and $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{S})$? These are non-trivial problems, and showing that are decidable is our main contribution.

4. The Fairness Theorem

As one might expect, to establish the decidability of the problem $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{C})$, for $\mathbb{C}\in\{\mathbb{G},\mathbb{S}\}$, we focus on its complement and show that, for a set ${\mathcal{T}}\in\mathbb{C}$ of TGDs, we can decide whether there is a database $D$ such that there exists a fair infinite chase derivation of $D$ w.r.t. ${\mathcal{T}}$. However, as observed in (Calautti et al., 2015), where the same problem for the simpler case of the oblivious chase is studied, one of the main difficulties is to ensure fairness. For the oblivious chase, the existence of an (unfair) infinite chase derivation of $D$ w.r.t. ${\mathcal{T}}$ implies the existence of a fair one (Calautti et al., 2015). Does the same hold for the restricted chase? This is a non-trivial question that is affirmatively answered by the following result dubbed Fairness Theorem:

Theorem 4.1 (Fairness).

Consider a database $D$ and a set ${\mathcal{T}}$ of single-head TGDs. If there exists an infinite restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$, then there exists a fair one.

Note that, to our surprise, the above theorem does not hold for multi-head TGDs, i.e., TGDs where the head is an arbitrary conjunction of atoms; a counterexample can be found in the appendix.111This has been also observed, independently of our work, in the recent paper (Leclère et al., 2019) that concentrates on single-head linear TGDs. This reveals the subtlety of the restricted chase, and explains that our decision to focus on single-head TGDs is not just for simplicity, but it is crucial for our results. The decidability status of $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{G})$ and $\mathsf{CT}_{\forall\exists}^{\mathsf{res}}(\mathbb{S})$ for multi-head TGDs are challenging open problems.

We now proceed to show the Fairness Theorem. By hypothesis, there exists an infinite restricted chase derivation $(I_{i})_{i\geq 0}$ of $D$ w.r.t. ${\mathcal{T}}$. By exploiting $(I_{i})_{i\geq 0}$, we are going to construct an infinite sequence $s_{D,{\mathcal{T}}}=((I_{i}^{j})_{i\geq 0})_{j\geq 0}$ of chase derivations of $D$ w.r.t. ${\mathcal{T}}$ such that $(I_{i}^{i})_{i\geq 0}$ is fair. In other words, $s_{D,{\mathcal{T}}}$ can be seen as an infinite matrix $M$, where the $j$-th row is the chase derivation $(I_{i}^{j})_{i\geq 0}$, while the diagonal is a fair chase derivation of $D$ w.r.t. ${\mathcal{T}}$.

The Diagonal Property.

We start by first exposing a crucial property that $s_{D,{\mathcal{T}}}$ should enjoy:

Definition 4.2.

A sequence $((J_{i}^{j})_{i\geq 0})_{j\geq 0}$ of infinite restricted chase derivations of $D$ w.r.t. ${\mathcal{T}}$ enjoys the diagonal property if, for each $i,j,k\geq 0$, $i\leq j$ and $i\leq k$ implies that $J_{i}^{j}=J_{i}^{k}$.

In other words, by saying that the sequence $s_{D,{\mathcal{T}}}$ enjoys the diagonal property, we simply mean that on the $i$-th column of the matrix $M$, all instances below the diagonal element $I_{i}^{i}$ coincide with $I_{i}^{i}$ (hence the name diagonal property). This allows us to show that the diagonal gives rise to an infinite chase derivation of $D$ w.r.t. ${\mathcal{T}}$:

Lemma 4.3.

Consider a sequence $((J_{i}^{j})_{i\geq 0})_{j\geq 0}$ of infinite restricted chase derivations of $D$ w.r.t. ${\mathcal{T}}$ that enjoys the diagonal property. Then, $(J_{i}^{i})_{i\geq 0}$ is a restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$

Of course, the diagonal property alone does not guarantee that the chase derivation $(I_{i}^{i})_{i\geq 0}$ is fair. Thus, our main task is to construct $s_{D,{\mathcal{T}}}=((I_{i}^{j})_{i\geq 0})_{j\geq 0}$ in such a way that (i) it enjoys the diagonal property, and (ii) $(I_{i}^{i})_{i\geq 0}$ is a fair chase derivation.

The Construction of $s_{D,{\mathcal{T}}}$.

The high-level idea is as follows. The sequence $(I_{i}^{0})_{i\geq 0}$ is defined as $(I_{i})_{i\geq 0}$, which exists by hypothesis. Now, our intention is to obtain $(I_{i}^{n+1})_{i\geq 0}$ from $(I_{i}^{n})_{i\geq 0}$. To this end, we carefully choose a large enough index $\ell>0$ and (i) we define $(I_{i}^{n+1})_{0\leq i\leq\ell}$ as $(I_{i}^{n})_{0\leq i\leq\ell}$, i.e., by simply copying the first $\ell+1$ instances of $(I_{i}^{n})_{i\geq 0}$, (ii) we obtain $I_{\ell+1}^{n+1}$ from $I_{\ell}^{n+1}=I_{\ell}^{n}$ by deactivating one of the early active triggers due to which $(I_{i}^{n})_{i\geq 0}$ is not fair, and (iii) we obtain $(I_{i}^{n+1})_{i\geq\ell+2}$ by mimicking $(I_{i}^{n})_{i\geq\ell+1}$. The formal construction of $s_{D,{\mathcal{T}}}$ follows.

As said above, $(I_{i}^{0})_{i\geq 0}$ is defined as $(I_{i})_{i\geq 0}$. Assume now that $(I_{i}^{n})_{i\geq 0}$ has been defined for some $n\geq 0$. We are going to define $(I_{i}^{n+1})_{i\geq 0}$. Let $m\geq 0$ be the smallest index such that there exists an active trigger $(\sigma,h)$ for ${\mathcal{T}}$ on $I_{m}^{n}$ that remains active forever in $(I_{i}^{n})_{i\geq 0}$. (Notice that if such an $m\geq 0$ does not exist, then $(I_{i}^{n})_{i\geq 0}$ is fair and we are done.) Assume that $I_{i+1}^{n}$ is obtained from $I_{i}^{n}$ via the trigger $(\sigma_{i},h_{i})$. Let $A=\{i\geq 0:\mathsf{result}(\sigma,h)\prec_{s}\mathsf{result}(\sigma_{i},h_{i})\}$. By exploiting the properties of $\prec_{s}$, it is not difficult to show that:

Lemma 4.4.

The set $A$ is finite.

Let $\ell$ be an integer greater than all the elements of $\{n,m\}\cup A$, which exists by Lemma 4.4. We define:

[TABLE]

We can show the following; the proof is in the appendix:

Lemma 4.5.

$(I_{i}^{n+1})_{i\geq 0}$* is a restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$.*

Finalizing the Proof.

Lemma 4.5 implies that indeed $s_{D,{\mathcal{T}}}=((I_{i}^{j})_{i\geq 0})_{j\geq 0}$ is an infinite sequence of chase derivations of $D$ w.r.t. ${\mathcal{T}}$. The fact that in the definition of $(I_{i}^{n+1})_{i\geq 0}$ above we choose the integer $\ell$ to be greater than $n$ ensures that $s_{D,{\mathcal{T}}}$ enjoys the diagonal property. Therefore, by Lemma 4.3, we conclude that $(I_{i}^{i})_{i\geq 0}$ is an infinite chase derivation of $D$ w.r.t. ${\mathcal{T}}$. Moreover, since there are only finitely many active triggers for ${\mathcal{T}}$ on an instance $I_{i}^{j}$ since $I_{i}^{j}$ is finite, it follows from the construction of $s_{D,{\mathcal{T}}}$ that $(I_{i}^{i})_{i\geq 0}$ is fair. Hence, $(I_{i}^{i})_{i\geq 0}$ is a fair infinite chase derivation of $D$ w.r.t. ${\mathcal{T}}$.

5. Chase Termination & Guardedness

We now concentrate on guarded TGDs, and show that:

Theorem 5.1.

$\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{G})$* is decidable in elementary time.*

By Theorem 4.1, to establish the above result it suffices to show that, for a set ${\mathcal{T}}\in\mathbb{G}$ of TGDs, we can decide in elementary time whether there is a database $D$ such that there exists an infinite (possibly unfair) restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$. To this end, we first characterize the existence of an infinite (possibly unfair) restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$ via the existence of an infinite subset of $\mathsf{ochase}(D,{\mathcal{T}})$, called chaseable, that enjoys certain properties. We then show that the problem of deciding whether there is a database $D$ such that an infinite chaseable subset of $\mathsf{ochase}(D,{\mathcal{T}})$ exists can be reduced to the satisfiability problem of Monadic Second-Order Logic (MSOL) over infinite trees of bounded degree, which in turn implies that $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{G})$ is decidable. At first glance, such a reduction looks unfeasible since the above statement talks about arbitrary databases $D$, and thus $\mathsf{ochase}(D,{\mathcal{T}})$ can be structurally very complex, i.e., not close to a tree. Nevertheless, we can show that it suffices to concentrate on acyclic databases $D$, which in turn implies (due to the fact that we consider single-head guarded TGDs) that $\mathsf{ochase}(D,{\mathcal{T}})$ is acyclic.

5.1. Non-Termination via Chaseable Sets

We proceed to introduce the notion of chaseable set for a database $D$ and a set ${\mathcal{T}}$ of TGDs. The key idea is to isolate certain properties of an infinite subset of $\mathsf{ochase}(D,{\mathcal{T}})$ that allow us to convert it into an infinite restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$. To this end, we need the “before” relation $\prec_{b}$ over $\mathsf{ochase}(D,{\mathcal{T}})$. Intuitively, $\alpha\prec_{b}\beta$ means that, if the atoms $\alpha$ and $\beta$ have been generated by some restricted chase derivation $\delta$, then necessarily $\alpha$ has been generated before $\beta$; otherwise, $\delta$ is not a restricted chase derivation. Given a sequence of instances $I_{0},I_{1},\ldots$, where each $I_{i}$ is a subset of $\mathsf{ochase}(D,{\mathcal{T}})$, there are essentially three reasons why it is not, or it cannot be converted (by merging some of the initial instances) into a restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$: there are atoms $\alpha\in I_{i}\setminus I_{i-1}$ and $\beta\in I_{j}\setminus I_{j-1}$ such that:

1. (1)

$\alpha\in D$, $\beta\not\in D$ and $j<i$, i.e., $\alpha$ is generated after $\beta$. 2. (2)

$\alpha\prec_{p}\beta$ but $j<i$, i.e., the parent of $\beta$ is generated after $\beta$. 3. (3)

$\alpha\prec_{s}\beta$ but $i<j$, i.e., $\beta$ is generated after $\alpha$, while $\alpha$ stops $\beta$.

The goal of the relation $\prec_{b}$ is to ensure that none of the above holds. Having the parent relation $\prec_{p}$, and the stop relation $\prec_{s}$ (together with Fact 3.5), it should be clear that the before relation $\prec_{b}$ is

[TABLE]

where $\prec_{s}^{-1}$ refers to the inverse relation of $\prec_{s}$. We write $\prec_{b}^{+}$ for the transitive closure of $\prec_{b}$. The notion of chaseable set follows.

Definition 5.2.

Consider a database $D$, and a set ${\mathcal{T}}$ of TGDs. A set $A\subseteq\mathsf{ochase}(D,{\mathcal{T}})$ is called chaseable if the following hold:

1. (1)

For each $\alpha\in A$, the set $\{\beta\in A:\beta\prec_{b}^{+}\alpha\}$ is finite. 2. (2)

For each $\alpha\in A$ and $\beta\in\mathsf{ochase}(D,{\mathcal{T}})$, $\beta\prec_{p}\alpha$ implies $\beta\in A$. 3. (3)

$\{\langle\alpha,\beta\rangle:\alpha,\beta\in A\text{ and }\alpha\prec_{b}\beta\}$ is a directed acyclic graph, i.e., there are no cycles in the relation $\prec_{b}$ over $A$.

The first condition states that, for each $\alpha\in A$, only finitely many atoms of $A$ should come before $\alpha$. The second condition says that the parent of an atom $\alpha\in A$ should be in $A$. Finally, the third condition states that, for every pair of distinct atoms $\alpha,\beta\in A$, either $\alpha$ should come before $\beta$, or $\beta$ should come before $\alpha$. It is not difficult to show that indeed the existence of an infinite chaseable set characterizes the existence of an infinite restricted chase derivation.

Theorem 5.3.

Consider a database $D$ and a set ${\mathcal{T}}$ of TGDs. The following are equivalent:

1. (1)

There exists an infinite restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$. 2. (2)

There exists an infinite set $A\subseteq\mathsf{ochase}(D,{\mathcal{T}})$ that is chaseable.

Let us clarify that Theorem 5.3 holds for arbitrary, not necessarily guarded TGDs. The importance of guardedness is revealed in the next section, where we show that we can focus on acyclic databases.

5.2. The Treeification Theorem

We first need to recall the standard notion of acyclicity for instances. Intuitively, an instance $I$ is acyclic if its atoms can be rearranged in a tree $T$ in such a way that, for each term $t\in\mathsf{dom}(I)$, the set of atoms that mention $t$ induces a connected subtree of $T$.

Definition 5.4.

A join tree of an instance $I$ is a pair $(T,\lambda)$, where $T=(V,E)$ is a tree, and $\lambda$ is the labeling function $V\rightarrow I$, such that:

1. (1)

For each $\alpha\in I$, there exists $v\in V$ with $\lambda(v)=\alpha$. 2. (2)

For each term $t\in\mathsf{dom}(I)$, the set $\{v\in V:t\text{ occurs in }\lambda(v)\}$ induces a connected subtree of $T$.

We say that $I$ is acyclic if it admits a joint tree.

We then show the following result dubbed Treeification Theorem:

Theorem 5.5 (Treeification).

Let ${\mathcal{T}}\in\mathbb{G}$. If there exists a database $D$ such that there is an infinite restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$, then there is an acyclic database with the same property.

This is a rather involved result and its proof can be found in the appendix. In what follows, we give the high-level idea underlying the construction of the desired acyclic database. By hypothesis, there exists an infinite restricted chase derivation $(I_{i})_{i\geq 0}$ of some database $D$ w.r.t. ${\mathcal{T}}$. From $\mathsf{ochase}(D,{\mathcal{T}})=(V,\prec_{p},\lambda,\tau)$ we can naturally obtain the guard-parent (resp., side-parent) relation $\prec_{\mathit{gp}}$ (resp., $\prec_{\mathit{sp}}$) over $V$ as the subrelation of $\prec_{p}$ by keeping only the pairs of nodes $(v,u)$ where $v$ corresponds to the guard atom (resp., to a side atom, i.e., an atom other than the guard) of the TGD in $\tau(u)$. Let $\prec_{\mathit{gp}}^{+}$ be the transitive closure of $\prec_{\mathit{gp}}$. Observe that, due to guardedness, $\mathsf{ochase}(D,{\mathcal{T}})$ can be seen as a forest w.r.t. $\prec_{\mathit{gp}}$, where the nodes of $V$ labeled with atoms of $D$ are the roots of the trees, and all the other nodes are the non-root nodes. As with $\prec_{p}$, for convenience, we will usually see $\prec_{\mathit{gp}}$ and $\prec_{\mathit{sp}}$ as relations over the multiset consisting of the atoms of $\mathsf{ochase}(D,{\mathcal{T}})$.

Let $\mathcal{I}=\bigcup_{i\geq 0}I_{i}$. For an atom $\beta\in\mathcal{I}$, we define $\mathcal{I}_{\beta}$ as the set $\{\alpha\in\mathcal{I}:\beta\prec_{\mathit{gp}}^{+}\alpha\}$. Since $D$ is finite, while $\mathcal{I}$ is infinite, we can conclude that there exists an atom $\alpha^{\infty}\in D$ such that the set $\mathcal{I}_{\alpha^{\infty}}$ is infinite. At this point, one may think that the desired acyclic database consists of the atom $\alpha^{\infty}$ together with the atoms of $D$ that can serve as its side atoms, i.e., the database

[TABLE]

Unfortunately, as shown below, this is not the case:

Example 5.6.

Assume that ${\mathcal{T}}$ consists of the TGDs

[TABLE]

It is clear that there exists an infinite restricted chase derivation of $\{R(a,b),S(b,c)\}$ w.r.t. ${\mathcal{T}}$: first apply $\sigma_{1}$ and obtain $T(b)$, then apply $\sigma_{2}$ and obtain $P(a,b)$, and then apply $\sigma_{3}$ infinitely many times. Observe that the key atom $\alpha^{\infty}$ is $R(a,b)$. However, there is no infinite restricted chase derivation of $\{R(a,b)\}$ w.r.t ${\mathcal{T}}$. In fact, there are no active triggers for ${\mathcal{T}}$ on $\{R(a,b)\}$

As it can be seen from the above example, the reason why $\alpha^{\infty}$, together with its potential side atoms from $D$, do not give rise to an infinite restricted chase derivation is the need of what we call here remote side-parents. In particular, referring to Example 5.6, we have an infinite restricted chase derivation of $\{R(a,b),S(b,c)\}$ w.r.t. ${\mathcal{T}}$ due to the atom $P(a,b)$, which has as a guard-parent the atom $\alpha^{\infty}=R(a,b)$, and as a side-parent the atom $T(b)$. However, $T(b)$ is not a database atom, but is obtained due to the database atom $S(b,c)$, which cannot serve as a side atom of $R(a,b)$. So, somehow, the atom $S(b,c)$ is a remote side-parent of $P(a,b)$. This situation can be formalized as follows.

Definition 5.7.

Consider two distinct atoms $\alpha,\beta\in D$, and two atoms $\alpha^{\prime},\beta^{\prime}\in\mathcal{I}$. The tuple $\langle\alpha,\alpha^{\prime},\beta,\beta^{\prime}\rangle$ is a remote-side-parent situation if the following hold: $\alpha\prec_{\mathit{gp}}^{+}\alpha^{\prime}$, $\beta\prec_{\mathit{gp}}^{+}\beta^{\prime}$, and $\beta^{\prime}\prec_{\mathit{sp}}\alpha^{\prime}$. If this is the case, then we say that $\alpha$ longs for $\beta$.

It is now not difficult to show that there exists a natural number $\ell_{\infty}$ such that, if $\langle\alpha^{\infty},\alpha^{\prime},\beta,\beta^{\prime}\rangle$ is a remote-side-parent situation, then $\beta^{\prime}\in I_{\ell_{\infty}}$. In fact, if $\langle\alpha^{\infty},\alpha^{\prime},\beta,\beta^{\prime}\rangle$ is a remote-side-parent situation, then, due to guardedness, all the terms occurring in $\beta^{\prime}$ occur also in $\alpha^{\infty}$ and $\beta$. This implies that there are only finitely many pairs of atoms $(\beta,\beta^{\prime})$, where $\beta\in D$ and $\beta^{\prime}\in\mathcal{I}$, such that, for some $\alpha^{\prime}\in\mathcal{I}$ with $\alpha^{\infty}\prec_{\mathit{gp}}^{+}\alpha^{\prime}$, $\langle\alpha^{\infty},\alpha^{\prime},\beta,\beta^{\prime}\rangle$ is a remote-side-parent situation. The latter implies the existence of $\ell_{\infty}$ claimed above, which is crucial in the construction of the desired acyclic database. We can now give the intuition underlying this construction.

Our intention is to explicitly construct from $D$ a join tree $(T_{\mathit{ac}},\lambda)$, where $T_{\mathit{ac}}=(V,E)$, and the desired acyclic database $D_{\mathit{ac}}$ will be the set of atoms $\{\lambda(v):v\in V\}$. Imagine $D$ as a directed multigraph: the atoms of $D$ are the vertices of this graph, while the edge-relation is “longs for”. Now, $T_{\mathit{ac}}$ is the set of all directed paths in this directed graph, starting from $\alpha^{\infty}$, of length at most $\ell_{\infty}$. There is a natural tree ordering on such a set of paths, and this is exactly the ordering $E$ of $T_{\mathit{ac}}$. Every path is labelled with an isomorphic copy of the atom being its end-point, but in a particular way: if $x$ and $y$ are two vertices of $T_{\mathit{ac}}$, with $(x,y)\in E$, which means that $x$ comes from some $\alpha\in D$ and $y$ comes from some $\beta\in D$ such that $\alpha$ longs for $\beta$, then, if $\alpha,\beta$ share a term, then $\lambda(x)$ and $\lambda(y)$ share the respective terms. Thanks to that, we are able to show that (the offspring of) $\lambda(y)$ can offer to (the offspring of) $\lambda(x)$ the same service in $D_{\mathit{ac}}$ as (the offspring of) $\beta$ provides to (the offspring of) $\alpha$ in $D$.

5.3. Deciding $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{G})$ via MSOL

By Theorems 4.1,5.3 and 5.5, given a set ${\mathcal{T}}\in\mathbb{G}$, deciding whether ${\mathcal{T}}\not\in\mathbb{CT}_{\forall\forall}^{\mathsf{res}}$ is equivalent to the problem of checking whether there is an acyclic database $D$ such that an infinite chaseable subset of $\mathsf{ochase}(D,{\mathcal{T}})$ exists. Our goal is to reduce the latter to the satisfiability problem of Monadic Second-Order Logic (MSOL) over infinite trees of bounded degree, which is decidable in $k$-ExpTime, where $k$ is the number of quantifier alternations.

We need to devise an MSOL sentence $\phi_{\mathcal{T}}$ such that the following statements are equivalent:

1. (1)

There is an acyclic database $D$ such that an infinite chaseable subset of $\mathsf{ochase}(D,{\mathcal{T}})$ exists. 2. (2)

$\phi_{\mathcal{T}}$ is satisfiable over $\Lambda_{\mathcal{T}}$-labeled infinite trees of bounded degree, where $\Lambda_{\mathcal{T}}$ is a finite alphabet that depends on ${\mathcal{T}}$.

Abstract Join Trees

Whenever ${\mathcal{T}}$ consists of single-head guarded TGDs and $D$ is acyclic, then $\mathsf{ochase}(D,{\mathcal{T}})$ is also acyclic, which means that it has a join tree (Barceló et al., 2016). Thus, one may think that this join tree is a natural candidate for a tree that our MSOL formula could talk about. But this is not going to work for the simple reason that the codomain of the labeling function $\lambda$ of such a join tree is infinite. We therefore need to invent something similar to a join tree, i.e., a structure that encodes an instance as a labeled tree, but much more parsimonious with respect to the labeling function. This is precisely the purpose of what we call abstract join trees.

We define the finite alphabet $\Lambda_{\mathcal{T}}$ as a set of triples

[TABLE]

that encode atoms. Here is the idea underlying this encoding:

• •

The first element of each triple is a predicate; it simply tells us the predicate of the atom in question.

• •

Concerning the second element, $F$ stands for “database fact”, and indicates that the encoded atom is an atom from the original database. If an atom does not come from the database, then the second element of the triple tells us which TGD of ${\mathcal{T}}$ was used to generate it.

• •

Concerning the third element, we define ${\mathcal{E}Q}_{\mathcal{T}}$ as the set of all equivalence relations on $\{f,m\}\times\{1,2,\ldots\mathsf{ar}({\mathcal{T}})\}$, where $f$ and $m$ stand for “father” and “me”. The idea is that, for example, the pair $[[m,i],[m,j]]$ says that the encoded atom has the same term at its $i$-th and $j$-th position, while the pair $[[m,i],[f,j]]$ says that the term at the $i$-th position in the atom in question equals to the term at the $j$-th position of its father (with respect to the tree relation).

In what follows, for brevity, given a node $v$ that is labeled by the triple $\langle x,y,z\rangle$, we write $\mathsf{pr}(v)$ for the predicate $x$, $\mathsf{org}(v)$ for $y$, i.e., the origin of the encoded atom, and $\mathsf{eq}(v)$ for the equivalence relation $z$. Recall also that, for an atom $\alpha$, we write $\alpha[i]$ for its $i$-th term. We are now ready to formally define abstract join trees.

Definition 5.8.

An *abstract join tree * for a set ${\mathcal{T}}\in\mathbb{G}$ of TGDs is a (finite or infinite) $\Lambda_{\mathcal{T}}$-labeled rooted tree $T=\langle V,\Yleft\rangle$, of degree at most $\max\{\mathsf{ar}({\mathcal{T}}),|{\mathcal{T}}|\}$, that satisfies the following conditions:

1. (1)

The set $\{x\in V:\mathsf{org}(x)=F\}$ is non-empty but finite. 2. (2)

If $x\Yleft y$ and $\mathsf{org}(y)=F$, then $\mathsf{org}(x)=F$. 3. (3)

If $x\Yleft y$ and $\mathsf{org}(y)=\sigma$, then $\mathsf{pr}(x)$ is the predicate of $\mathsf{guard}(\sigma)$ and $\mathsf{pr}(y)$ is the predicate of $\mathsf{head}(\sigma)$. 4. (4)

If $x\Yleft y$, then $[[m,i],[m,j]]\in\mathsf{eq}(x)$ iff $[[f,i],[f,j]]\in\mathsf{eq}(y)$. 5. (5)

If $x\Yleft y$ and $\mathsf{org}(y)=\sigma$, for some $\sigma\in{\mathcal{T}}$ with $\alpha=\mathsf{guard}(\sigma)$ and $\beta=\mathsf{head}(\sigma)$, then:

1. (a)

$\alpha[i]=\beta[j]$ implies $[[f,i],[m,j]]\in\mathsf{eq}(y)$, 2. (b)

$\alpha[i]=\alpha[j]$ implies $[[f,i],[f,j]]\in\mathsf{eq}(y)$, and 3. (c)

if $\beta[j]$ is an existentially quantified variable in $\sigma$, then $[[m,i],[m,j]]\in\mathsf{eq}(y)$ iff $\beta[j]=\beta[i]$.

We now need to explain how an abstract join tree is transformed into an instance. Consider an abstract join tree $T=\langle V,\Yleft\rangle$ for a set ${\mathcal{T}}\in\mathbb{G}$. We define $\mathsf{Eq}_{T}\subseteq(V\times\{1,\ldots,\mathsf{ar}({\mathcal{T}})\})\times(V\times\{1,\ldots,\mathsf{ar}({\mathcal{T}})\})$ as the smallest equivalence relation such that, for every edge $x\Yleft y$, if $[[m,i],[m,j]]\in\mathsf{eq}(x)$ then $[[x,i],[x,j]]\in\mathsf{Eq}_{T}$, and if $[[f,i],[m,j]]\in\mathsf{eq}(y)$ then $[[x,i],[y,j]]\in\mathsf{Eq}_{T}$. The instance $\Delta(T)$ is defined as the set of atoms $\{\delta(x):x\in V\}$, where (i) for each $x\in V$, the predicate of $\delta(x)$ is $\mathsf{pr}(x)$, and (ii) for each $x,y\in V$, $\delta(x)[i]=\delta(y)[j]$ iff $[[x,i],[y,j]]\in\mathsf{Eq}_{T}$.

For an abstract join tree $T$, we write $T_{|F}$ for the restriction of $T$ to its nodes that are labeled with a label of the form $\langle\cdot,F,\cdot\rangle$. Then, it is not hard to see that the following equivalence holds:

Lemma 5.9.

For a set ${\mathcal{T}}\in\mathbb{G}$, and an acyclic database $D$, the following are equivalent:

1. (1)

There exists an infinite chaseable subset of $\mathsf{ochase}(D,{\mathcal{T}})$. 2. (2)

There exists an abstract join tree $T$ such that $\Delta(T_{|F})$ and $D$ are isomorphic, and $\Delta(T)$ is an infinite and chaseable subset of $\mathsf{ochase}(\Delta(T_{|F}),{\mathcal{T}})$.

Therefore, in order to prove Theorem 5.1, it is now enough to construct, for a given ${\mathcal{T}}$, an MSOL formula $\phi_{\mathcal{T}}$ such that, for any abstract join tree $T$, it holds that: $T\models\phi_{\mathcal{T}}$ iff ($\star$) $\Delta(T)$ is an infinite and chaseable subset of $\mathsf{ochase}(\Delta(T_{|F}),{\mathcal{T}})$.

Chaseable Abstract Join Trees

Our MSOL formula $\phi_{\mathcal{T}}$ (under construction) is supposed to express some property of $\Delta(T)$, for a given abstract join tree $T$, namely the property ($\star$). But, it does not see $\Delta(T)$. It can only talk about $T$. Moreover, talking about nodes, let say $x$ and $y$, of $T$, and relations between these nodes, it must actually mean the atoms $\delta(x)$ and $\delta(y)$, and relations among those atoms. Thus, it will be convenient to have a language to talk about the nodes of $T$ but to mean atoms of $\Delta(T)$. We now define such a language, allowing ourselves to slightly abuse the notation and overload the symbols $\prec_{p}$, $\prec_{s}$ and $\prec_{b}$.

First, we need a way to say that an atom $\alpha\in\Delta(T)$ can act as a side atom for some other atom $\beta\in\Delta(T)$, and also to specify which terms of $\beta$ occur in $\alpha$ and at which positions. This can be achieved via the notion of sideatom type. A sideatom type $\pi$ (w.r.t ${\mathcal{T}}$) is a triple $\langle P,m,\xi\rangle$, where $P/n\in\mathsf{sch}({\mathcal{T}})$, $m\leq\mathsf{ar}({\mathcal{T}})$ is a natural number, called the arity of $\pi$, and $\xi:[n]\rightarrow[m]$. Given two atoms $\alpha$ and $\beta$, we say that $\alpha$ is a $\pi$-sideatom of $\beta$, denoted $\alpha\subseteq_{\pi}\beta$, if the predicate of $\alpha$ is $P$, the predicate of $\beta$ has arity $m$, and $\alpha[i]=\beta(\xi(i))$ for each $i\in[n]$. For example, the atom $\alpha=P(a,b,c)$ is a $\pi$-sideatom of $\beta=R(a,d,c,b)$ with $\pi=\langle P,4,\{1\mapsto 1,2\mapsto 4,3\mapsto 3\}\rangle$. In what follows, it would be convenient to represent a guarded body by directly using sideatom types. More precisely, for a guarded TGD $\sigma$, where $\mathsf{body}(\sigma)=\gamma,\gamma_{1},\ldots,\gamma_{m}$ with $\gamma=\mathsf{guard}(\sigma)$, its body can be represented in the obvious way as $\gamma,\pi_{1},\ldots\pi_{m}$, where $\pi_{1},\ldots,\pi_{m}$ are sideatom types of arity equal to the arity of the predicate of $\gamma$.

Parent Relation.

Consider an abstract join tree $T=\langle V,\Yleft\rangle$ for a set ${\mathcal{T}}$ of guarded TGDs. The parent relation is defined as follows:

• •

Given an edge $x\Yleft y$ in $T$, with $\mathsf{org}(y)=\sigma$, for some $\sigma\in{\mathcal{T}}$ such that $\mathsf{body}(\sigma)=\gamma,\pi_{1},\ldots,\pi_{m}$, we say that a node $z\in V$ is a $\pi_{i}$-side-parent of $y$, denoted $z\prec_{sp}^{\pi_{i}}y$, if $\delta(z)\subseteq_{\pi_{i}}\delta(x)$.

• •

Given two nodes $x,y\in V$, $x$ is a parent of $y$, denoted $x\prec_{p}y$, if $x\Yleft y$, or $x\prec_{sp}^{\pi}y$ for some sideatom type $\pi$.

Stop Relation.

Consider two nodes $x,y\in V$, with $\mathsf{org}(y)=\sigma$. We say that $x$ stops y, denoted $x\prec_{s}y$, if there exists a homomorphism $h$ such that $h(\delta(y))=\delta(x)$, and, for each term $t$ in $\delta(y)$ that occurs at a position of $\bigcup_{x\in\mathsf{fr}(\sigma)}\mathsf{pos}(\mathsf{head}(\sigma),x)$, $h(t)=t$.

Before Relation.

The before relation is defined as expected:

[TABLE]

We write $\prec_{b}^{+}$ for the transitive closure of $\prec_{b}$.

Having the above relations in place, we can now define the notion of chaseable abstract join tree:

Definition 5.10.

Consider an abstract join tree $T=\langle V,\Yleft\rangle$ for a set ${\mathcal{T}}\in\mathbb{G}$. We say that $T$ is chaseable if the following hold:

1. (1)

For each $x\in V$, the set $\{y\in V:y\prec_{b}^{+}x\}$ is finite. 2. (2)

For each edge $x\Yleft y$, where $\mathsf{org}(y)=\sigma$ for some $\sigma\in{\mathcal{T}}$ with $\mathsf{body}(\sigma)=\gamma,\pi_{1},\ldots,\pi_{m}$, there exists $z\in V$ such that $z\prec_{sp}^{\pi_{i}}y$ for each $i\in[m]$. 3. (3)

$\{\langle x,y\rangle:x,y\in V\text{ and }x\prec_{b}y\}$ is a directed acyclic graph, i.e., there are no cycles in the relation $\prec_{b}$ over $V$.

It follows, by construction, that for a set ${\mathcal{T}}$ of guarded TGDs, and an abstract join tree $T$ for ${\mathcal{T}}$, $\Delta(T)$ is an infinite chaseable subset of $\mathsf{ochase}(\Delta(T_{|F}),{\mathcal{T}})$ iff there exists an infinite chaseable abstract join tree $\hat{T}$ for ${\mathcal{T}}$ such that $\Delta(T_{|F})$ is isomorphic to $\Delta(\hat{T}_{|F})$. Then:

Lemma 5.11.

For a set ${\mathcal{T}}\in\mathbb{G}$, the following are equivalent:

1. (1)

There exists an abstract join tree $T$ for ${\mathcal{T}}$ such that $\Delta(T)$ is an infinite chaseable subset of $\mathsf{ochase}(\Delta(T_{|F}),{\mathcal{T}})$. 2. (2)

There exists an infinite chaseable abstract join tree for ${\mathcal{T}}$.

Chaseable Abstract Join Trees are MSOL-definable

The last task is to show the following:

Lemma 5.12.

Consider a set ${\mathcal{T}}\in\mathbb{G}$. There is an MSOL sentence $\phi_{\mathcal{T}}$ such that, for a $\Lambda_{\mathcal{T}}$-labeled tree $T$ of degree at most $\max\{\mathsf{ar}({\mathcal{T}}),|{\mathcal{T}}|\}$, it holds that $T\models\phi_{\mathcal{T}}$ iff $T$ is a chaseable abstract join tree for ${\mathcal{T}}$.

The sentence $\phi_{\mathcal{T}}$ has to check whether a tree is an abstract join tree, and also whether the three conditions of Definition 5.10 are satisfied. Since, given an abstract join tree $T=\langle V,\Yleft\rangle$, for each term $t$ in $\Delta(T)$, $\{x\in V:t\text{ occurs in }\delta(x)\}$ induces a connected subtree of $T$, it should be evident that indeed the above conditions can be checked via an MSOL sentence. More details concerning the MSOL sentence $\phi_{\mathcal{T}}$ can be found in the appendix.

Having Lemmas 5.9, 5.11 and 5.12, we get that $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{G})$ is decidable in elementary time, and Theorem 5.1 follows.

6. Chase Termination & Stickiness

We now concentrate on sticky sets of TGDs, and show that:

Theorem 6.1.

$\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{S})$* is decidable in elementary time.*

As in the case of guarded TGDs, to establish the above result we are going to show that the complement of $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{S})$ is decidable in elementary time. In fact, our ultimate goal is to reduce the complement of $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{S})$ to the emptiness problem of deterministic Büchi automata, which is feasible in linear time in the size of the automaton. To this end, given a set ${\mathcal{T}}\in\mathbb{S}$, we characterize the existence of a database $D$ such that there is an infinite restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$ via the existence of a finitary caterpillar for ${\mathcal{T}}$. The latter is essentially an infinite “path-like” restricted chase derivation of some database w.r.t. ${\mathcal{T}}$, and, as we shall see, its existence can be checked via a deterministic Büchi automaton.

6.1. Non-Termination via Caterpillars

To formally introduce the notion of finitary caterpillar, we first need the notion of proto-caterpillar.

Definition 6.2.

Consider a set ${\mathcal{T}}$ of TGDs. A proto-caterpillar for ${\mathcal{T}}$ is a tuple $\diamondsuit=(L^{\diamondsuit},B^{\diamondsuit},T^{\diamondsuit},G^{\diamondsuit})$, where:

• •

$L^{\diamondsuit}$ is a (possibly infinite) instance over $\mathsf{sch}({\mathcal{T}})$, the legs of $\diamondsuit$,

• •

$B^{\diamondsuit}=(\alpha_{i}^{\diamondsuit})_{i\geq 0}$ is a sequence of atoms over $\mathsf{sch}({\mathcal{T}})$ with constants and nulls (no variables), the body of $\diamondsuit$,222By abuse of notation, we may sometimes treat $B^{\diamondsuit}$ as the set of atoms $\{\alpha_{i}^{\diamondsuit}\}_{i\geq 0}$.

• •

$T^{\diamondsuit}=(\sigma_{i}^{\diamondsuit},h_{i}^{\diamondsuit})_{i>0}$ is a sequence of TGD-mapping pairs where $h_{i}^{\diamondsuit}$ maps the variables in $\mathsf{body}(\sigma_{i}^{\diamondsuit})$ to $\mathbf{C}\cup\mathbf{N}$, and

• •

$G^{\diamondsuit}=(\gamma_{i}^{\diamondsuit})_{i>0}$ is a sequence of atoms with $\gamma_{i}^{\diamondsuit}\in\mathsf{body}(\sigma_{i}^{\diamondsuit})$,

such that, for each $i\geq 0$, the following holds:

• (1)

$(\sigma_{i+1}^{\diamondsuit},h_{i+1}^{\diamondsuit})$ is a trigger for ${\mathcal{T}}$ on $L^{\diamondsuit}\cup\{\alpha_{i}^{\diamondsuit}\}$;

• (2)

$\alpha_{i}^{\diamondsuit}=h_{i+1}^{\diamondsuit}(\gamma_{i+1}^{\diamondsuit})$;

• (3)

$\alpha_{i+1}^{\diamondsuit}=\mathsf{result}(\sigma_{i+1}^{\diamondsuit},h_{i+1}^{\diamondsuit})$.

It should not be difficult to see that a proto-caterpillar $\diamondsuit$ for ${\mathcal{T}}$ as above encodes a “path-like” oblivious chase derivation (modulo repetition of triggers) of the (possibly infinite) instance $L^{\diamondsuit}\cup\{\alpha_{0}^{\diamondsuit}\}$ w.r.t. ${\mathcal{T}}$. Indeed, each atom $\alpha_{i}^{\diamondsuit}$, for $i>0$, of the sequence $B^{\diamondsuit}$ can be derived from $L^{\diamondsuit}\cup\{\alpha_{i-1}^{\diamondsuit}\}$, i.e., the previous atom on the sequence and atoms of $L^{\diamondsuit}$, via the trigger $(\sigma_{i}^{\diamondsuit},h_{i}^{\diamondsuit})$. In other words, the infinite sequence of instances $(I_{i})_{i\geq 0}$, where $I_{0}=L^{\diamondsuit}\cup\{\alpha_{0}^{\diamondsuit}\}$ and, for $i>0$, $I_{i}=I_{i-1}\cup\{\alpha_{i}^{\diamondsuit}\}$, is an oblivious chase derivation (modulo repetition of triggers) of $I_{0}$ w.r.t. ${\mathcal{T}}$. But, even if we remove the repeated triggers, there is no guarantee that it is a restricted chase derivation for the following two reasons: an atom from $L^{\diamondsuit}$ may stop an atom $\alpha_{i}^{\diamondsuit}$ for $i>0$, or an atom $\alpha_{i}^{\diamondsuit}$ may stop an atom $\alpha_{j}^{\diamondsuit}$ for $j>i$. This brings us to the notion of caterpillar, which is essentially a proto-caterpillar with the guarantee that the above two cases are excluded.

Definition 6.3.

Consider a set ${\mathcal{T}}$ of TGDs. A caterpillar for ${\mathcal{T}}$ is a proto-caterpillar $\diamondsuit=(L^{\diamondsuit},(\alpha_{i}^{\diamondsuit})_{i\geq 0},\cdot,\cdot)$ for ${\mathcal{T}}$ such that:

1. (1)

for each $\beta\in L^{\diamondsuit}$ and $i>0$, $\beta\not\prec_{s}\alpha_{i}^{\diamondsuit}$, and 2. (2)

for each $0\leq i<j$, $\alpha_{i}^{\diamondsuit}\not\prec_{s}\alpha_{j}^{\diamondsuit}$.

It is an easy task to verify that a caterpillar $\diamondsuit$ for ${\mathcal{T}}$ as above encodes a “path-like” restricted chase derivation of the (possibly infinite) instance $L^{\diamondsuit}\cup\{\alpha_{0}^{\diamondsuit}\}$ w.r.t. ${\mathcal{T}}$. However, it should not be forgotten that we are interested on finite databases. This brings us to the central notion of finitary caterpillar.

Definition 6.4.

Consider a set ${\mathcal{T}}$ of TGDs. A finitary caterpillar for ${\mathcal{T}}$ is a caterpillar $(L^{\diamondsuit},\cdot,\cdot,\cdot)$ for ${\mathcal{T}}$ such that $L^{\diamondsuit}$ is finite.

Our goal is to characterize the existence of a database that gives rise to an infinite restricted chase derivation w.r.t. a sticky set ${\mathcal{T}}$ of TGDs via the existence of a finitary caterpillar for it.

Theorem 6.5.

Let ${\mathcal{T}}\in\mathbb{S}$. The following are equivalent:

1. (1)

There exists a database $D$ such that there is an infinite restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$. 2. (2)

There exists a finitary caterpillar for ${\mathcal{T}}$.

The fact that $(2)\Rightarrow(1)$ follows by definition, and holds for every set of TGDs, not necessarily sticky. The interesting direction is $(1)\Rightarrow(2)$, which relies on stickiness. To this end, we are going to introduce refined variants of caterpillars, which will eventually lead to finitary caterpillars. In particular, we are going to introduce the notions of (uniformly) connected caterpillar, and free caterpillar, and establish the following chain of implications:

• there exists a database $D$ such that there is an infinite restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$
• $\Rightarrow$

there exists a free connected caterpillar for ${\mathcal{T}}$

• $\Rightarrow$

there exists a free uniformly connected caterpillar for ${\mathcal{T}}$

• $\Rightarrow$

there exists a finitary caterpillar for ${\mathcal{T}}$,

which shows that indeed $(1)\Rightarrow(2)$. In the rest of the section, let ${\mathcal{T}}$ be a sticky set of single-head TGDs. For brevity, we will usually say (proto-)caterpillar meaning (proto-)caterpillar for ${\mathcal{T}}$.

Variants of Caterpillars

We first need some auxiliary terminology. Let $\alpha\in\mathsf{ochase}(D,{\mathcal{T}})$, for some database $D$, and assume that $\alpha=\mathsf{result}(\sigma,h)$. Let $\gamma$ be an atom of $\mathsf{body}(\sigma)$, which means that $h(\gamma)\in\mathsf{ochase}(D,{\mathcal{T}})$ with $h(\gamma)\prec_{p}\alpha$. We say that the $i$-th position of $h(\gamma)$ and the $j$-th position of $\alpha$ are related, denoted as $(h(\gamma),i)\simeq(\alpha,j)$, if $\gamma[i]=\mathsf{head}(\sigma)[j]$. Moreover, the $i$-th and $j$-th positions of $\alpha$ are related, written as $(\alpha,i)\simeq(\alpha,j)$, if $\mathsf{head}(\sigma)[i]=\mathsf{head}(\sigma)[j]$. Now, for an instance ${\mathcal{I}}\subseteq\mathsf{ochase}(D,{\mathcal{T}})$, let $\Pi(\mathcal{I})=\{(R(\bar{t}),i):R(\bar{t})\in{\mathcal{I}}\text{ and }1\leq i\leq\mathsf{ar}(R)\}$. We denote by $\simeq^{*}_{\mathcal{I}}$ the smallest equivalence relation that contains $(\Pi(\mathcal{I}))^{2}\cap(\simeq)$. Intuitively, $(\alpha,i)\simeq^{*}_{\mathcal{I}}(\beta,j)$, for some atoms $\alpha,\beta\in\mathsf{ochase}(D,{\mathcal{T}})$, means that the terms $\alpha[i]$ and $\beta[j]$ are provably equal via a proof that uses only atoms of $\mathcal{I}$. Notice that $(\alpha,i)\simeq_{\mathcal{I}}^{*}(\beta,j)$ implies $\alpha[i]=\beta[j]$, but the opposite implication is not always true.

We also need the notion of the “birth atom” of a null value. Consider a parent-closed instance ${\mathcal{I}}\subseteq\mathsf{ochase}(D,{\mathcal{T}})$, and let $c\in\mathsf{dom}(\mathcal{I})$ be a null. We write $\beta^{B}(c)$ (which reads “the birth atom of $c$”) for the atom of $\mathcal{I}$ such that: (1) $c$ occurs in $\beta^{B}(c)$, and (2) for every $\alpha\in\mathcal{I}$ with $\alpha\prec_{p}\beta^{B}(c)$, $c$ does not occur in $\alpha$. It is clear that there is only one birth atom of $c$. Notice also that for an atom $\beta\in\mathcal{I}$ such that $\beta[j]=c$, it holds that $\beta$ is the birth atom of $c$ iff for each parent $\alpha$ of $\beta$ and each position $i$ of $\alpha$, $(\alpha,i)\not\simeq(\beta,j)$.

We finally need to introduce the notion of immortal position, which relies on the marking procedure used in the definition of stickiness; see Section 2. Let $\alpha\in\mathsf{ochase}(D,{\mathcal{T}})$, for some database $D$, with $\alpha=\mathsf{result}(\sigma,h)$. The $i$-th position of $\alpha$ is immortal (w.r.t. ${\mathcal{T}}$) if the variable at the $i$-th position of $\mathsf{head}(\sigma)$ is not marked in ${\mathcal{T}}$. The name “immortal” reflects the fact that $\alpha[i]$ will be propagated forever, i.e., for every $\beta$ such that $\alpha\prec_{p}\beta$, $\alpha[i]\in\mathsf{fr}(\beta)$.

We are now ready to introduce the first variant of caterpillars.

Definition 6.6.

A caterpillar (or proto-caterpillar) $\diamondsuit=(\cdot,B^{\diamondsuit},\cdot,\cdot)$, where $B^{\diamondsuit}=(\alpha_{i}^{\diamondsuit})_{i\geq 0}$, is connected if there exist an infinite sequence $({\mathfrak{c}}_{i})_{i\geq 0}$ of terms, called the relay terms of $\diamondsuit$, an infinite sequence $(b_{i})_{i>0}$ of integers with $b_{1}<b_{2}<b_{3}<\cdots$, called the pass-on points of $\diamondsuit$, and infinite sequences $(p_{i})_{i>0}$ and $(m_{i})_{i\geq 0}$ ($p$ for “parent” and $m$ for “me”) of integers from $[\mathsf{ar}({\mathcal{T}})]$, such that, for each $k\geq 0$:

1. (1)

${\mathfrak{c}}_{0}$ occurs in $\alpha_{0}^{\diamondsuit}$; 2. (2)

$\alpha_{b_{k}}^{\diamondsuit}=\beta^{B}({\mathfrak{c}}_{k})$; 3. (3)

${\mathfrak{c}}_{k}=\alpha_{b_{k}}^{\diamondsuit}[m_{k}]$ and $\left(\alpha_{b_{k}}^{\diamondsuit},m_{k}\right)\simeq_{B^{\diamondsuit}}^{*}\left(\alpha_{b_{k+1}}^{\diamondsuit},p_{k+1}\right)$; 4. (4)

$\alpha_{j}^{\diamondsuit}[i]={\mathfrak{c}}_{k}$, for $i>0$, $j\geq 0$, implies $\left(\alpha_{j}^{\diamondsuit},i\right)$ is not immortal.

The above definition is indeed a bit technical. Intuitively, we can imagine the sequence of terms ${\mathfrak{c}}_{0},{\mathfrak{c}}_{1},{\mathfrak{c}}_{2},\ldots$ as an infinite relay race, where the ${\mathfrak{c}}_{i}$’s are mortal runners, and their birth atoms are the batton passing points. In other words, connectedness ensures the continuous propagation of a new null in the underlying “path-like” chase derivation. However, the distance between two consecutive pass-on points can be arbitrarily large, i.e., there is no uniform bound. As we shall see later, having such a uniform bound is crucial for going from connected caterpillars to finitary caterpillars. This brings us to the next refined variant of caterpillars.

Definition 6.7.

A caterpillar $\diamondsuit$ is uniformly connected if it is connected and, with $(b_{i})_{i>0}$ being its pass-on points, there exists an integer $d\geq 0$ such that, for each $k\geq 0$, $b_{k+1}-b_{k}<d$.

Let us now introduce the last variant of caterpillars that we need, namely free caterpillars. Recall that $(\alpha,i)\simeq^{*}_{L^{\diamondsuit}\cup B^{\diamondsuit}}(\beta,j)$, for $\alpha,\beta\in\mathsf{ochase}(L^{\diamondsuit}\cup B^{\diamondsuit},{\mathcal{T}})$, means that $\alpha[i]$ and $\beta[j]$ are provably equal via a proof that uses only atoms of $L^{\diamondsuit}\cup B^{\diamondsuit}$. It would be very useful to ensure that also the other direction holds.

Definition 6.8.

A (proto-)caterpillar $\diamondsuit=(L^{\diamondsuit},B^{\diamondsuit},\cdot,\cdot)$ is free if, for each $(\alpha,i),(\beta,j)\in\Pi(L^{\diamondsuit}\cup B^{\diamondsuit})$, $\alpha[i]=\beta[j]$ iff $(\alpha,i)\simeq_{L^{\diamondsuit}\cup B^{\diamondsuit}}^{*}(\beta,j)$.

6.2. Implication 1: Extracting a Free Connected Caterpillar

We are now ready to establish the chain of implications discussed above, immediately after Theorem 6.5. We first focus on the first implication that states the following: if there exists a database $D$ such that there is an infinite restricted chase derivation of $D$ w.r.t. ${\mathcal{T}}$, then there exists a free connected caterpillar for ${\mathcal{T}}$. Suppose $(I_{i})_{i\geq 0}$ is an infinite restricted chase derivation of some database $D$ w.r.t. ${\mathcal{T}}$, and let ${\mathcal{I}}=\bigcup_{i\geq 0}I_{i}$. We are going to extract from $(I_{i})_{i\geq 0}$ a free connected caterpillar. The construction proceeds in three steps:

1. (1)

First, we are going to construct a proto-caterpillar $\clubsuit$. 2. (2)

Then, we will convert $\clubsuit$ into a connected proto-caterpillar $\spadesuit$. 3. (3)

Finally, from $\spadesuit$ we will get a free connected caterpillar $\heartsuit$.

Step 1: Construct a Proto-Caterpillar

We proceed to extract from $(I_{i})_{i\geq 0}$ a proto-caterpillar $\clubsuit$ that is “almost connected”. Given a term (constant or null) $c$ and a null $c^{\prime}$, both in $\mathsf{dom}(\mathcal{I})$, we say that $c$ is a parent term of $c^{\prime}$ (w.r.t. $\mathcal{I}$), denoted $c\prec_{p}^{\mathit{t}}c^{\prime}$, if $c$ occurs in $\mathsf{fr}(\beta^{B}(c^{\prime}))$. Notice that, for $c$ to be a parent term of $c^{\prime}$ it is not enough to be in one of the parent atoms of the birth atom of $c^{\prime}$, but it needs to be propagated, via a frontier variable, during the application of the trigger that generates the birth atom of $c^{\prime}$. Now, for each term $c$ occurring in $\mathcal{I}$, we inductively define the rank of $c$ (w.r.t. $\mathcal{I}$) as follows:

[TABLE]

For a term $c\in\mathsf{dom}(\mathcal{I})$ with $\mathsf{rank}(c)>0$, select a term $c^{\prime}\in\mathsf{dom}(\mathcal{I})$ such that $\mathsf{rank}(c^{\prime})=\mathsf{rank}(c)-1$ and $c^{\prime}\prec_{p}^{\mathit{t}}c$. We call $c^{\prime}$ the favourite parent of $c$, and we write $c^{\prime}\prec_{\mathit{fp}}^{\mathit{t}}c$.333We assume that there exists some fixed mechanism that selects $c^{\prime}$. For example, $c^{\prime}$ can be the lexicographically first element of $\{c^{\prime\prime}:\mathsf{rank}(c^{\prime\prime})=\mathsf{rank}(c)-1\text{ and }c^{\prime\prime}\prec_{p}^{\mathit{t}}c\}$.

It should be clear that the binary relation $\prec_{\mathit{fp}}^{\mathit{t}}$ over $\mathsf{dom}(\mathcal{I})$ forms an infinite forest $F$ consisting of a finite number of trees, where the roots are terms from $\mathsf{dom}(D)$ of rank [math]. But what about the out-degree of each node of $F$? We can show that, for each $i\geq 0$, the set $\{c\in\mathsf{dom}(\mathcal{I}):\mathsf{rank}(c)=i\}$ is finite. This can be shown by induction on $i\geq 0$, while the key fact is that only finitely many triggers can be formed due to which a null with rank $i+1$ is generated (since, by induction hypothesis, the set of terms with rank at most $i$ is finite). Thus, the nodes of $F$ have finite out-degree. By applying König’s Lemma444König’s Lemma is a well-known result from graph theory: for an infinite directed rooted graph, if every node is reachable from the root, and every node has finite out-degree, then there exists an infinite directed simple path from the root. on $F$, we get that $F$ contains an infinite simple path starting from a root node; let ${\mathfrak{c}}_{0},{\mathfrak{c}}_{1},{\mathfrak{c}}_{2},\ldots$ be such a path.

By construction, for each $i\geq 0$, ${\mathfrak{c}}_{i}$ occurs in the birth atom of ${\mathfrak{c}}_{i+1}$. Moreover, there exists a sequence of atoms $\beta^{i}_{0},\beta^{i}_{1},\beta^{i}_{2},\ldots,\beta^{i}_{m_{i}}=\beta^{B}({\mathfrak{c}}_{i+1})$, where $\beta^{i}_{0}\in D$ if $i=0$ and $\beta^{i}_{0}=\beta^{B}({\mathfrak{c}}_{i})$ if $i>0$, such that $\beta^{i}_{k}\prec_{p}\beta^{i}_{k+1}$, for each $0\leq k<m_{i}$, and there are positions $j$ in $\beta^{B}({\mathfrak{c}}_{i})$ and $j^{\prime}$ in $\beta^{B}({\mathfrak{c}}_{i+1})$ such that $(\beta^{B}({\mathfrak{c}}_{i}),j)\simeq^{*}_{P_{i}}(\beta^{B}({\mathfrak{c}}_{i+1}),j^{\prime})$, where $P_{i}$ is the set of atoms $\{\beta^{i}_{0},\beta^{i}_{1},\ldots\beta^{i}_{m_{i}}\}$.

We are now ready to define $\clubsuit$. For brevity, let $P$ be the infinite set of atoms $\bigcup_{i\geq 0}P_{i}$. Let $\clubsuit=(L^{\clubsuit},B^{\clubsuit},T^{\clubsuit},G^{\clubsuit})$, where

• •

$L^{\clubsuit}=\{\alpha\in{\mathcal{I}}\setminus P:\text{ there is }\beta\in P\text{ such that }\alpha\prec_{p}\beta\}$,

• •

$B^{\clubsuit}=(\alpha_{i}^{\clubsuit})_{i\geq 0}$ with $\alpha^{\clubsuit}_{0},\alpha^{\clubsuit}_{1},\alpha^{\clubsuit}_{2},\ldots$ being the enumeration of the atoms of $P$ such that $\alpha^{\clubsuit}_{i}\prec_{p}\alpha^{\clubsuit}_{i+1}$, for each $i\geq 0$,

• •

$T^{\clubsuit}=(\sigma_{i}^{\clubsuit},h_{i}^{\clubsuit})_{i>0}$ with $(\sigma_{i}^{\clubsuit},h_{i}^{\clubsuit})$, for $i>0$, being the trigger for ${\mathcal{T}}$ on $B^{\clubsuit}\cup\{\alpha_{i-1}^{\clubsuit}\}$ such that $\alpha_{i}^{\clubsuit}=\mathsf{result}(\sigma_{i}^{\clubsuit},h_{i}^{\clubsuit})$, and

• •

$G^{\clubsuit}=(\gamma_{i}^{\clubsuit})_{i>0}$ with $\gamma^{\clubsuit}_{i}\in\mathsf{body}(\sigma_{i}^{\clubsuit})$ and $\alpha_{i-1}^{\clubsuit}=h_{i}^{\clubsuit}(\gamma_{i}^{\clubsuit})$.

It should be clear, from the above construction, that the sequence of triggers $(\sigma_{i}^{\clubsuit},h_{i}^{\clubsuit})_{i>0}$ exists, and thus, $\clubsuit$ is well-defined. Then:

Lemma 6.9.

$\clubsuit$* is a proto-caterpillar for ${\mathcal{T}}$.*

As said at the beginning of Step 1, the goal was to extract from $(I_{i})_{i\geq 0}$ a proto-caterpillar that is “almost connected”. It is easy to verify that the proto-caterpillar $\clubsuit$ is “almost connected” in the sense that all the conditions of Definition 6.6 are satisfied, with ${\mathfrak{c}}_{0},{\mathfrak{c}}_{1},\ldots$ playing the role of the relay terms, apart from (4). Indeed, there is no guarantee that ${\mathfrak{c}}_{0},{\mathfrak{c}}_{1},\ldots$ do not occur at immortal positions. Can we convert $\clubsuit$ into a connected proto-caterpillar that satisfies also condition (4)? This is the goal of the next step.

Step 2: Construct a Connected Proto-Caterpillar

It is clear that if a term ${\mathfrak{c}}_{i}$, for $i\geq 0$, occurs in an immortal position in some atom $\alpha^{\clubsuit}_{j}$, then it occurs in every $\alpha^{\clubsuit}_{k}$ for $k>j$. Since $\mathsf{ar}({\mathcal{T}})$ is finite, we can have only finitely many integers $i\geq 0$ such that the term ${\mathfrak{c}}_{i}$ occurs at an immortal position. Let $i_{0}$ be an integer greater than all such numbers $i$, which means that ${\mathfrak{c}}_{i_{0}},{\mathfrak{c}}_{i_{0}+1},{\mathfrak{c}}_{i_{0}+2},\ldots$ do not occur at immortal positions. Let $n$ be such that $\alpha_{n}^{\clubsuit}=\beta^{B}({\mathfrak{c}}_{i_{0}})$, i.e., is the birth atom of ${\mathfrak{c}}_{i_{0}}$. It should be now clear how $\clubsuit$ can be converted into a connected proto-caterpillar $\spadesuit$. For brevity, let $P$ be the set of atoms $\left\{\alpha_{k+n}^{\clubsuit}:k\geq 0\right\}$. Let $\spadesuit=(L^{\spadesuit},B^{\spadesuit},T^{\spadesuit},G^{\spadesuit})$, where

• •

$L^{\spadesuit}=\{\alpha\in{\mathcal{I}}\setminus P:\text{ there is }\beta\in P\text{ such that }\alpha\prec_{p}\beta\}$,

• •

$B^{\spadesuit}=(\alpha_{i}^{\spadesuit})_{i\geq 0}$ with $\alpha^{\spadesuit}_{i}=\alpha^{\clubsuit}_{i+n}$ for each $i\geq 0$,

• •

$T^{\spadesuit}=(\sigma_{i}^{\spadesuit},h_{i}^{\spadesuit})_{i>0}$ with $(\sigma_{i}^{\spadesuit},h_{i}^{\spadesuit})=(\sigma_{i+n}^{\clubsuit},h_{i+n}^{\clubsuit})$ for $i>0$, and

• •

$G^{\spadesuit}=(\gamma_{i}^{\spadesuit})_{i>0}$ with $\gamma_{i}^{\spadesuit}=\gamma^{\clubsuit}_{i+n}$ for each $i>0$.

Since, by Lemma 6.9, $\clubsuit$ is a proto-caterpillar for ${\mathcal{T}}$, we can conclude that $\spadesuit$ is also a proto-caterpillar. It also follows by construction that $\spadesuit$ is connected with ${\mathfrak{c}}_{i_{0}},{\mathfrak{c}}_{i_{0}+1},{\mathfrak{c}}_{i_{0}+2},\ldots$ being its relay terms. Then:

Lemma 6.10.

$\spadesuit$* is a connected proto-caterpillar for ${\mathcal{T}}$.*

Observe that there is no guarantee that $\spadesuit$ is a caterpillar since the two conditions in Definition 6.3 might be violated. Moreover, there is no guarantee that $\spadesuit$ is free, or, equivalently, that, for each $(\alpha,i),(\beta,j)\in\Pi(L^{\spadesuit}\cup B^{\spadesuit})$, $\alpha[i]=\beta[j]$ implies $(\alpha,i)\simeq_{L^{\spadesuit}\cup B^{\spadesuit}}^{*}(\beta,j)$; recall that the other direction holds trivially. Can we convert $\spadesuit$ into a free connected caterpillar? This is the goal of the next step.

Step 3: Construct a Free Connected Caterpillar

To achieve our goal, we are going to carefully replace each term occurring in $L^{\spadesuit}\cup B^{\spadesuit}$ at a certain position $\pi\in\Pi(L^{\spadesuit}\cup B^{\spadesuit})$ with a new constant that only depends on the equivalence class of $\pi$ w.r.t. the equivalence relation $\simeq_{L^{\spadesuit}\cup B^{\spadesuit}}^{*}$. As usual, we write $[\pi]_{\simeq_{L^{\spadesuit}\cup B^{\spadesuit}}^{*}}$ for the equivalence class of $\pi$ w.r.t. $\simeq_{L^{\spadesuit}\cup B^{\spadesuit}}^{*}$. Let $\bar{h}$ be a function that maps each atom $\alpha=R(t_{1},\ldots,t_{n})\in L^{\spadesuit}\cup B^{\spadesuit}$ to the atom

[TABLE]

where, for each $1\leq i\leq n$, $c_{[(\alpha,i)]_{\simeq_{L^{\spadesuit}\cup B^{\spadesuit}}^{*}}}$ is a constant from $\mathbf{C}$.

Having the function $\bar{h}$ in place, it is not difficult to see how $\spadesuit$ can be converted into the desired free connected caterpillar $\heartsuit$. In particular, $\heartsuit=(L^{\heartsuit},B^{\heartsuit},T^{\heartsuit},G^{\heartsuit})$, where

• •

$L^{\heartsuit}=\{\bar{h}(\alpha):\alpha\in L^{\spadesuit}\}$,

• •

$B^{\heartsuit}=(\alpha_{i}^{\heartsuit})_{i\geq 0}$ with $\alpha^{\heartsuit}_{i}=\bar{h}(\alpha^{\spadesuit}_{i})$ for each $i\geq 0$,

• •

$T^{\heartsuit}=(\sigma_{i}^{\heartsuit},h_{i}^{\heartsuit})_{i>0}$ with $\sigma_{i}^{\heartsuit}=\sigma_{i}^{\spadesuit}$ and $h_{i}^{\heartsuit}=\bar{h}\circ h_{i}^{\spadesuit}$, for $i>0$,

• •

$G^{\heartsuit}=(\gamma_{i}^{\heartsuit})_{i>0}$ with $\gamma_{i}^{\heartsuit}=\gamma_{i}^{\spadesuit}$ for each $i>0$.

Stickiness allows us to show the following, which concludes the proof of the first implication; for the details see the appendix:

Lemma 6.11.

$\heartsuit$* is a free connected caterpillar for ${\mathcal{T}}$.*

6.3. Implication 2: From a Free Connected Caterpillar to a Uniformly Connected One

Let us now concentrate on the second implication. The proof relies on the fact that we can check whether a free connected caterpillar exists via a deterministic Büchi automaton. As usual, for an automaton $\mathcal{A}$, we write $L({\mathcal{A}})$ for its language. Then:

Lemma 6.12.

We can construct a deterministic Büchi automaton ${\mathcal{A}}_{\mathcal{T}}$ where $L({\mathcal{A}}_{\mathcal{T}})\neq\emptyset$ iff there is a free connected caterpillar for ${\mathcal{T}}$.

Let us stress that the purpose of the automaton ${\mathcal{A}}_{\mathcal{T}}$ provided by Lemma 6.12 is twofold: it is used here, together with a pumping argument, for establishing the second implication, and it will be also used in Section 6.5 for showing that the problem of deciding whether a finitary caterpillar exists is decidable in elementary time. We proceed to give some details concerning ${\mathcal{A}}_{\mathcal{T}}$ that allow us to intuitively explain how we get the second implication, while the detailed construction can be found in the appendix. It should not be surprising that this is the place where freeness plays a role.

The automaton ${\mathcal{A}}_{\mathcal{T}}$ operates on what we call caterpillar words over a finite alphabet $\Lambda_{\mathcal{T}}$ consisting of triples of the form $(\sigma,\gamma,P)$, where $\sigma\in{\mathcal{T}}$, $\gamma\in\mathsf{body}(\sigma)$, and, with $R$ being the predicate of $\mathsf{head}(\sigma)$, $P\subseteq[\mathsf{ar}(R)]$. Intuitively, a caterpillar word $\mathbf{w}=w_{1}w_{2},\cdots$, with $w_{i}=(\sigma_{i},\gamma_{i},P_{i})$, is a candidate symbolic representation of a free connected caterpillar, where $w_{i}$ marks a pass-on point iff $P_{i}$ is non-empty. In fact, $P_{i}$ indicates at which positions of $\mathsf{head}(\sigma_{i})$ the new relay term appears. Roughly, ${\mathcal{A}}_{\mathcal{T}}$ accepts $\mathbf{w}$ iff $\mathbf{w}$ encodes a free connected caterpillar, while it enters an accepting state only when it reads a symbol $w_{i}$ that marks a pass-on point.

We get the second implication from the following observation, which can be shown by an obvious pumping argument:

Observation 1.

Let $\mathcal{A}$ be a deterministic Büchi automaton with $n_{\mathcal{A}}$ states. If $L(\mathcal{A})\neq\emptyset$, then there is $\mathbf{w}\in L(\mathcal{A})$ s.t. among each $n_{\mathcal{A}}$ consecutive states visited by $\mathcal{A}$ on input $\mathbf{w}$, at least one is accepting.

Suppose now that there exists a free connected caterpillar. By Lemma 6.12, $L({\mathcal{A}}_{\mathcal{T}})\neq\emptyset$. By applying the above observation to the automaton ${\mathcal{A}}_{\mathcal{T}}$, we get a word $\mathbf{w}$ that encodes a free connected caterpillar $\diamondsuit$ such that the distance between two consecutive pass-on points is bounded by the number of states of ${\mathcal{A}}_{\mathcal{T}}$. Thus, $\diamondsuit$ is a free uniformly connected caterpillar, as needed.

6.4. Implication 3: From a Free Uniformly Connected Caterpillar to a Finitary One

We now proceed with the last implication. Consider a free uniformly connected caterpillar $\diamondsuit=(L^{\diamondsuit},B^{\diamondsuit},T^{\diamondsuit},G^{\diamondsuit})$, where $B^{\diamondsuit}=(\alpha_{i}^{\diamondsuit})_{i\geq 0}$, $T^{\diamondsuit}=(\sigma_{i}^{\diamondsuit},h_{i}^{\diamondsuit})_{i>0}$, and $G^{\diamondsuit}=(\gamma_{i}^{\diamondsuit})_{i>0})$. Our intention is to obtain from $\diamondsuit$ a finitary caterpillar by unifying some terms of $\mathsf{dom}(L^{\diamondsuit})$ in order to make $L^{\diamondsuit}$ finite, while the rest remains a valid caterpillar. This can be done via what we call a unifying function.

A unifying function for $\diamondsuit$ is a function $h:{\mathfrak{V}}\rightarrow{\mathfrak{T}}$, where ${\mathfrak{V}}\subseteq\mathsf{dom}(L^{\diamondsuit})$, and ${\mathfrak{T}}$ a set of new terms not occurring in $L^{\diamondsuit}\cup B^{\diamondsuit}$; it is called unifying since it essentially unifies the terms of ${\mathfrak{V}}$. Let $h(\diamondsuit)=\left(h(L^{\diamondsuit}),(h(\alpha_{i}^{\diamondsuit}))_{i\geq 0},(\sigma_{i},h\circ h_{i}^{\diamondsuit})_{i>0},(\gamma_{i}^{\diamondsuit})_{i>0}\right)$. Then:

Lemma 6.13.

There exists a unifying function $h$ for $\diamondsuit$ such that $h(\diamondsuit)$ is a finitary caterpillar for ${\mathcal{T}}$.

It is not difficult to show that no matter how a unifying function $h$ for $\diamondsuit$ is defined, $h(\diamondsuit)$ is a proto-caterpillar that satisfies condition (1) of Definition 6.3. The non-trivial task is to define $h$ is such a way that $h(L^{\diamondsuit})$ is finite, and $h(\diamondsuit)$ satisfies condition (2) of Definition 6.3. The key here is, by exploiting uniformity, which provides a bound on the distance between two consecutive pass-on points, to define a sufficiently large finite set of new terms to which infinitely many carefully chosen terms of $\mathsf{dom}(L^{\diamondsuit})$ are mapped to; the details can be found in the appendix. This completes the proof of Theorem 6.5.

6.5. Deciding $\mathsf{CT}_{\forall\forall}^{\mathsf{res}}(\mathbb{S})$ via Büchi Automata

By Theorems 4.1 and 6.5, given a set ${\mathcal{T}}\in\mathbb{S}$, deciding whether ${\mathcal{T}}\not\in\mathbb{CT}_{\forall\forall}^{\mathsf{res}}$ is equivalent to the problem of checking whether there exists a finitary caterpillar for ${\mathcal{T}}$. By exploiting the Büchi automaton provided by Lemma 6.12, we can easily show that:

Lemma 6.14.

The problem of deciding whether there exists a finitary caterpillar for ${\mathcal{T}}$ is decidable in elementary time.

Since the emptiness problem of deterministic Büchi automata is feasible in linear time in the size of the automaton, and since the automaton provided by Lemma 6.12 can be constructed in elementary time, checking whether a free connected caterpillar for ${\mathcal{T}}$ exists is feasible in elementary time. Now, observe that the three implications established above, together with the $(2)\Rightarrow(1)$ direction of Theorem 6.5, imply that there exists a free connected caterpillar iff there exists a finitary caterpillar, and Lemma 6.14 follows.

7. Future Work

Here are some non-trivial questions that beg for an answer: (1) What about the exact complexity of our problems? (2) What about restricted chase termination for guarded or sticky sets of multi-head TGDs? (3) What about the more liberal version of the problem that asks whether there is a finite restricted chase derivation?

Appendix A Additional Notions

An equality type over a schema $\mathbf{S}$ is a pair $(R,E)$, where $R\in\mathbf{S}$ and $E$ is a partition of $\{1,\ldots,\mathsf{ar}(R)\}$ (which we see as a set of subsets of $\{1,\ldots,\mathsf{ar}(R)\}$). Let $\mathsf{etypes}(\mathbf{S})$ be the set of all possible equality types over $\mathbf{S}$, which is clearly finite. Given an atom $\alpha=R(t_{1},\ldots,t_{n})$ over $\mathbf{S}$, its equality type, denoted $\mathsf{et}(\alpha)$, is the equality type $(R,E)\in\mathsf{etypes}(\mathbf{S})$ such that $t_{i}=t_{j}$ iff $i,j$ coexist in a set of $E$. A homomorphism from a set of atoms $A$ to a set of atoms $B$ is an isomorphism from $A$ to $B$ if it is 1-1, and its inverse $h^{-1}$ is a homomorphism from $B$ to $A$.

Appendix B Proofs from Section 4

B.1. Fairness Theorem and Multi-head TGDs

Here is an example showing that the Fairness Theorem (Theorem 4.1) does not hold for multi-head TGDs:

Example B.1.

Consider the set ${\mathcal{T}}$ of TGDs consisting of

[TABLE]

It should be clear that there exists an infinite restricted chase derivation of $\{R(a,b,b)\}$ w.r.t. ${\mathcal{T}}$; apply only the first TGD. However, every valid restricted chase derivation of $\{R(a,b,b)\}$ w.r.t. ${\mathcal{T}}$ is finite.

Let us say that the recent paper (Leclère et al., 2019), which studies the restricted chase termination problem for linear TGDs, provides an example that refutes Theorem 4.1 even if we use only binary predicates.

B.2. Proof of Lemma 4.3

Clearly, $J_{0}^{0}=D$ since $(J_{i}^{0})_{i\geq 0}$ is a chase derivation of $D$ w.r.t. ${\mathcal{T}}$. It remains to show that, for $k\geq 0$, there is an active trigger $(\sigma,h)$ for ${\mathcal{T}}$ on $J_{k}^{k}$ such that $J_{k}^{k}\langle\sigma,h\rangle J_{k+1}^{k+1}$. Note that $J_{k}^{k}=J_{k}^{k+1}$ by the diagonal property. Thus, it suffices to show that there exists an active trigger $(\sigma,h)$ for ${\mathcal{T}}$ on $J_{k}^{k+1}$ such that $J_{k}^{k+1}\langle\sigma,h\rangle J_{k+1}^{k+1}$. This holds since $(J_{i}^{k+1})_{i\geq 0}$ is a chase derivation of $D$ w.r.t. ${\mathcal{T}}$.

B.3. Proof of Lemma 4.4

Let $\mathcal{I}^{n}=\bigcup_{i\geq 0}I_{i}^{n}$. Since ${\mathcal{T}}$ is finite, it suffices to show that, for each TGD $\hat{\sigma}\in{\mathcal{T}}$, the set of atoms $B_{\hat{\sigma}}$ that collects all the atoms of $\mathcal{I}^{n}$ that are stopped by $\mathsf{result}(\sigma,h)$ and are generated by a trigger that involves $\hat{\sigma}$, is finite. Indeed, $B_{\hat{\sigma}}$ is finite implies $A$ is finite, since the cardinality of $B_{\hat{\sigma}}$ coincides with the cardinality of $\{i\geq 0:\mathsf{result}(\sigma,h)\prec_{s}\mathsf{result}(\sigma_{i},h_{i})\text{ and }\sigma_{i}=\hat{\sigma}\}$.

Since all the atoms of $B_{\hat{\sigma}}$ have been created by the same TGD, and they are all stopped by $\mathsf{result}(\sigma,h)$, we can conclude that they are equal when restricted to their frontier. Towards a contradiction, assume that two atoms $\alpha,\beta\in B_{\hat{\sigma}}$ have the same equality type. This implies that $\alpha\prec_{s}\beta$ and $\beta\prec_{s}\alpha$, which contradicts the fact that $\alpha$ and $\beta$ belong to the result of a restricted chase derivation. Thus, for every two distinct atoms $\alpha,\beta\in B_{\hat{\sigma}}$, $\alpha$ and $\beta$ have different equality types. Since there are only finitely many equality types over $\mathsf{sch}({\mathcal{T}})$, we conclude that $B_{\hat{\sigma}}$ is finite, as needed.

B.4. Proof of Lemma 4.5

By construction, $I_{0}^{n+1}=I_{0}^{n}=D$. It remains to show that, for $i\geq 0$, there is an active trigger $(\sigma_{i},h_{i})$ for ${\mathcal{T}}$ on $I_{i}^{n+1}$ such that $I_{i}^{n+1}\langle\sigma_{i},h_{i}\rangle I_{i+1}^{n+1}$. We proceed by considering the following cases:

Case 1.

For $0\leq i\leq\ell$, the claim is trivial since $(I_{i}^{n+1})_{0\leq i\leq\ell}=(I_{i}^{n})_{0\leq i\leq\ell}$, while $(I_{i}^{n})_{i\geq 0}$ is a chase derivation of $D$ w.r.t. ${\mathcal{T}}$.

Case 2.

For $i=\ell+1$, the claim holds since $(\sigma,h)$ is an active trigger for ${\mathcal{T}}$ on $I_{\ell}^{n}=I_{\ell}^{n+1}$ and $I_{i}^{n+1}=I_{i-1}^{n+1}\cup\{\mathsf{result}(\sigma,h)\}$.

Case 3.

Finally, assume that $i\geq\ell+2$. Recall that $I_{i-1}^{n}$ is obtained from $I_{i-2}^{n}$ by applying the active trigger $(\sigma_{i-2},h_{i-2})$. We are going to show that $I_{i-1}^{n+1}\langle\sigma_{i-2},h_{i-2}\rangle I_{i}^{n+1}$. Clearly, $I_{i}^{n+1}=I_{i-1}^{n+1}\cup\{\mathsf{result}(\sigma_{i-2},h_{i-2})\}$ since $I_{i-1}^{n}=I_{i-2}^{n}\cup\{\mathsf{result}(\sigma_{i-2},h_{i-2})\}$. It is also clear that $(\sigma_{i-2},h_{i-2})$ is a trigger for ${\mathcal{T}}$ on $I_{i-1}^{n+1}$. It remains to show that it is also active. Assume that this is not the case. Fact 3.5 implies that there is an atom $\alpha\in I_{i-1}^{n+1}$ such that $\alpha\prec_{s}\mathsf{result}(\sigma_{i-2},h_{i-2})$. Recall that $I_{i-1}^{n+1}=I_{i-2}^{n}\cup\{\mathsf{result}(\sigma,h)\}$. Since $(\sigma_{i-2},h_{i-2})$ is an active trigger for ${\mathcal{T}}$ on $I_{i-2}^{n}$, we conclude that $\alpha\not\in I_{i-2}^{n}$. Moreover, since $i-2$ is greater that all the elements of $A$, we get that $\mathsf{result}(\sigma,h)$ does not stop $\mathsf{result}(\sigma_{i-2},h_{i-1})$, which implies that $\alpha\neq\mathsf{result}(\sigma_{i-2},h_{i-1})$. Hence, $\alpha\not\in I_{i-1}^{n+1}$, which is a contradiction.

Appendix C Proofs from Section 5

C.1. Proof of Theorem 5.3

The fact that $(1)\Rightarrow(2)$ is easy: simply define $A$ as the set $\bigcup_{i\geq 0}I_{i}$, where $(I_{i})_{i\geq 0}$ is the infinite restricted chase derivation of $D$ w.r.t.${\mathcal{T}}$ that exists by hypothesis. For the other direction, by exploiting $A$, we are going to inductively construct an infinite restricted chase derivation $(I_{i})_{i\geq 0}$ of $D$ w.r.t ${\mathcal{T}}$. Clearly, $I_{0}$ is defined as $D$. Suppose that we have already constructed $(I_{i})_{1\leq i\leq n-1}$, for some natural number $n>1$. Due to condition (1) of Definition 5.2, there exists an atom $\alpha\in A\setminus B$, where $B=\bigcup_{0\leq i<n}I_{i}$, that is minimal w.r.t. $\prec_{b}$, i.e., for every $\beta\in A\setminus B$, $\alpha\prec_{b}\beta$. We define $I_{n}$ as the instance $B\cup\{\alpha\}$. It remains to show that there exists an active trigger $(\sigma,h)$ for ${\mathcal{T}}$ on $B$ such that $\alpha=\mathsf{result}(\sigma,h)$. By condition (2) of Definition 5.2, we get that all the parents of $\alpha$ occur in $B$, and thus $(\sigma,h)$ is a trigger for ${\mathcal{T}}$ on $B$. To show that $(\sigma,h)$ is active, by Fact 3.5, we need to show that there is no $\beta\in B$ such that $\beta\prec_{s}\alpha$. Towards a contradiction, assume that such $\beta$ exists. This implies that $\alpha\prec_{b}\beta$ (recall that $\prec_{s}^{-1}\subseteq\prec_{b})$. But this implies that $\prec_{b}$ over $B$ contains a cycle, which is a contradiction due to the third condition of Definition 5.2, and the claim follows.

C.2. Proof of Theorem 5.5

In the rest of the subsection, let ${\mathcal{T}}$ be a set of single-head guarded TGDs. As it is common when studying guarded TGDs, we need a refined version of the parent relation over the real oblivious chase that distinguishes between guard- and side-parents.

Guard- and Side-Parent Relation.

Consider the real oblivious chase $\mathsf{ochase}(D,{\mathcal{T}})=\langle V,\prec_{p},\lambda,\tau\rangle$ of a database $D$ w.r.t. ${\mathcal{T}}$. We can naturally define the guard-parent relation $\prec_{\mathit{gp}}$ over $V$ as the subrelation of $\prec_{p}$ by keeping only the pairs of nodes $(v,u)$ where $v$ corresponds to the guard atom of the TGD in $\tau(u)$. Formally, the guard-parent relation $\prec_{\mathit{gp}}$ (over $V$) is defined as

[TABLE]

For a node $u$, we may write $\mathit{gp}(u)$ for its guard-parent, i.e., if $v\prec_{\mathit{gp}}u$, then $\mathit{gp}(u)=v$. We denote by $\prec_{\mathit{gp}}^{+}$ the transitive closure of $\prec_{\mathit{gp}}$. Observe that, due to guardedness, $\mathsf{ochase}(D,{\mathcal{T}})$ can be seen as a forest w.r.t. $\prec_{\mathit{gp}}$, with the nodes of $V$ labeled with atoms of $D$ being the roots of the trees, and all the other nodes are the non-root nodes. It would be conceptually useful to have this forest in mind.

Regarding the side-parents, it is not enough to simply keep the pairs $v\prec_{p}u$ where $v$ corresponds to a side atom (i.e., an atom different than the guard) of the TGD in $\tau(u)$. In addition, we need to know which terms of the atom $\lambda(\mathit{gp}(u))$ occur in $\lambda(v)$ and at which positions.555For the discussion in the main body of the paper, the simple side-parent relation $\prec_{sp}$ was enough. However, for the formal proof we need this additional information. This can be achieved via the notion of sideatom type.666Note that this notion has been also introduced and used in Section 5.3 where we talk about chaseable abstract join trees. We repeat it here for the sake of readability. A sideatom type $\pi$ (w.r.t ${\mathcal{T}}$) is a triple $\langle P,m,\xi\rangle$, where $P/n\in\mathsf{sch}({\mathcal{T}})$, $m\leq\mathsf{ar}({\mathcal{T}})$ is a natural number, called the arity of $\pi$, and $\xi:[n]\rightarrow[m]$. Given two atoms $\beta$ and $\gamma$, we say that $\beta$ is a $\pi$-sideatom of $\gamma$, denoted $\beta\subseteq_{\pi}\gamma$, if the predicate of $\beta$ is $P$, the predicate of $\gamma$ has arity $m$, and $\beta[i]=\gamma(\xi(i))$ for each $i\in[n]$. For example, the atom $\beta=P(a,b,c)$ is a $\pi$-sideatom of $\gamma=R(a,d,c,b)$ with $\pi=\langle P,4,\{1\mapsto 1,2\mapsto 4,3\mapsto 3\}\rangle$. Consider now a node $u\in V$ such that $v\prec_{p}u$, $v_{1}\prec_{p}u$, …, $v_{m}\prec_{p}u$, $\tau(u)=(\sigma,h)$, where $\mathsf{body}(\sigma)=\gamma,\gamma_{1},\ldots,\gamma_{m}$ with $\gamma=\mathsf{guard}(\sigma)$, and $h(\gamma)=\lambda(v)$, $h(\gamma_{1})=\lambda(v_{1})$, …, $h(\gamma_{m})=\lambda(v_{m})$. Let $\pi_{1},\ldots,\pi_{m}$ be sideatom types such that, for each $i\in[m]$, $\lambda(v_{i})\subseteq_{\pi_{i}}\lambda(v)$ (or $\lambda(v_{i})\subseteq_{\pi_{i}}\lambda(\mathit{gp}(u))$). Then, for each $i\in[m]$, we say that $v_{i}$ is a $\pi_{i}$-side-parent of $u$, written $v_{i}\prec_{\mathit{sp}}^{\pi_{i}}u$.

As for the relation $\prec_{p}$, notice that, strictly speaking, $\prec_{\mathit{gp}}$ and $\prec_{\mathit{sp}}^{\pi}$, for some sideatom type $\pi$, are relations over the node set $V$ of $\mathsf{ochase}(D,{\mathcal{T}})$. However, for convenience, we will usually see these relations as relations over the set multiset consisting of the atoms of $\mathsf{ochase}(D,{\mathcal{T}})$. Thus, we will directly refer to the guard-parent of an atom $\alpha$ of $\mathsf{ochase}(D,{\mathcal{T}})$ and write $\mathit{gp}(\alpha)$.

Let us now proceed with the proof of Theorem 5.5. By hypothesis, there exists an infinite restricted chase derivation $(I_{i})_{i\geq 0}$ of $D$ w.r.t. ${\mathcal{T}}$. The proof proceeds in three main steps:

1. (1)

We first construct from $D$ an acyclic database $D_{\mathit{ac}}$. In fact, we explicitly construct a join tree $(T_{\mathit{ac}},\lambda)$, where $T_{\mathit{ac}}=(V,E)$, and the database $D_{\mathit{ac}}$ is defined as $\{\lambda(v):v\in V\}$. 2. (2)

We then show that there is an auxiliary infinite sequence of instances $(K_{i})_{i\geq 0}$, where $K_{0}=D_{\mathit{ac}}$, which somehow mimics the infinite restricted chase derivation $(I_{i})_{i\geq 0}$ of $D$ w.r.t. ${\mathcal{T}}$. 3. (3)

Finally, by exploiting the sequence $(K_{i})_{i\geq 0}$, we construct an infinite restricted chase derivation $(J_{i})_{i\geq 0}$ of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$.

We proceed to give more details for each of the above steps. But first we need to fix some notation. Let $\mathcal{I}=\bigcup_{i\geq 0}I_{i}$. We write $(\sigma_{i}^{\mathcal{I}},h_{i}^{\mathcal{I}})$ for the trigger such that $I_{i}\langle\sigma_{i}^{\mathcal{I}},h_{i}^{\mathcal{I}}\rangle I_{i+1}$. For brevity, we write $\beta^{\mathcal{I}}_{i}$ for the atom $\mathsf{result}(\sigma_{i}^{\mathcal{I}},h_{i}^{\mathcal{I}})$, and $\gamma^{\mathcal{I}}_{i}$ for $\mathsf{guard}(\sigma^{\mathcal{I}}_{i})$. Given an atom $\beta\in\mathcal{I}$, we define $\mathcal{I}_{\beta}$ as the set $\{\alpha\in\mathcal{I}:\beta\prec_{\mathit{gp}}^{+}\alpha\}$.

Step 1: The Acyclic Database $D_{\mathit{ac}}$

Since $D$ is finite, while $\mathcal{I}$ is infinite, we can conclude that there exists an atom $\alpha^{\infty}\in D$ such that the set $\mathcal{I}_{\alpha^{\infty}}$ is infinite. One may think that the acyclic database $D_{\mathit{ac}}$ consists of the atom $\alpha^{\infty}$ together with the atoms of $D$ that can serve as its side atoms, i.e., the database

[TABLE]

However, as explained in the main body of the paper (see Example 5.6), this is not the case due to what we call remote side-parents:

Definition C.1.

Consider two distinct atoms $\alpha,\beta\in D$, and two atoms $\alpha^{\prime},\beta^{\prime}\in\mathcal{I}$. The tuple $\langle\alpha,\alpha^{\prime},\beta,\beta^{\prime}\rangle$ is a remote-side-parent situation if $\alpha\prec_{\mathit{gp}}^{+}\alpha^{\prime}$, $\beta\prec_{\mathit{gp}}^{+}\beta^{\prime}$, and $\beta^{\prime}\prec_{\mathit{sp}}^{\pi}\alpha^{\prime}$ for some sideatom type $\pi$. If this is the case, then we say that $\alpha$ longs for $\beta$.

The following easy lemma collects a couple of useful facts about the notion of remote-side-parent situation, which would be crucial for the construction of the acyclic database $D_{\mathit{ac}}$.

Lemma C.2.

1. (1)

If $\langle\alpha,\alpha^{\prime},\beta,\beta^{\prime}\rangle$ is a remote-side-parent situation, then $\beta^{\prime}\subseteq_{\pi}\alpha$ and $\beta^{\prime}\subseteq_{\pi^{\prime}}\beta$ for some types $\pi$ and $\pi^{\prime}$. 2. (2)

There exists a natural number $\ell_{\infty}$ such that, if $\langle\alpha^{\infty},\alpha^{\prime},\beta,\beta^{\prime}\rangle$ is a remote-side-parent situation, then $\beta^{\prime}\in I_{\ell_{\infty}}$.

Proof.

It is easy to verify that claim (1) holds due to guardedness. For claim (2) it suffices to observe that the following holds, which is a consequence of (1): for an atom $\alpha\in D$, there are only finitely many pairs of atoms $\beta,\beta^{\prime}$ such that, for some atom $\alpha^{\prime}$ with $\alpha\prec_{\mathit{gp}}^{+}\alpha^{\prime}$, $\langle\alpha,\alpha^{\prime},\beta,\beta^{\prime}\rangle$ is a remote-side-parent situation.

The Construction of $D_{\mathit{ac}}$.

Let us now formally define the acyclic database $D_{\mathit{ac}}$. We will construct, via simultaneous induction:

1. (1)

A labeled tree $(T_{\mathit{ac}},\lambda)$, where $T_{\mathit{ac}}=(V,E)$ and $\lambda$ is a labeling function from $V$ to $\{R([t_{1}]_{v},\ldots,[t_{n}]_{v}):R/n\in\mathsf{sch}({\mathcal{T}}),t_{i}\in\mathsf{dom}(D)\text{ and }v\in V\}$, i.e., the set of atoms that can be formed using predicates of $\mathsf{sch}({\mathcal{T}})$ and constants from the set $\{[t]_{v}:t\in\mathsf{dom}(D)\text{ and }v\in V\}$. 2. (2)

A mapping $h_{\mathit{ac}}$ from $\{\lambda(v):v\in V\}$ to $D$. 3. (3)

A function $\mathsf{depth}$ from $\{\lambda(v):v\in V\}$ to $\mathbb{N}$.

The constants of the form $[t]_{v}$ used above provide us with a simple mechanism for uniformly renaming a constant $t\in\mathsf{dom}(D)$ into a fresh constant, while this renaming step is performed with respect to a certain node $v$ of $T_{\mathit{ac}}$. This allows us to break the connection among occurrences of the same constant that are semantically different; this will be made clear in a while. The construction follows:

Base Case. Let $v\in V$ be the root node of $T_{\mathit{ac}}$. Then, $\lambda(v)=\alpha^{\infty}$, $h_{\mathit{ac}}(\lambda(v))=\alpha^{\infty}$, and $\mathsf{depth}(\lambda(v))=0$.

Inductive Step. Assume that $v\in V$ is such that $h_{\mathit{ac}}(\lambda(v))=\alpha$, for some $\alpha\in D$, with $\mathsf{depth}(\lambda(v))<\ell_{\infty}$. Then, for each $\beta\in D$ such that $\alpha$ longs for $\beta$, we add a new node $u$ to $V$, and the edge $(v,u)$ to $E$, in such a way that:

• •

the atom $\lambda(u)$ is of the following form:

• –

it has the same predicate as the atom $\beta$,

• –

$\lambda(u)[i]=\lambda(u)[j]$ iff $\beta[i]=\beta[j]$,

• –

$\lambda(u)[i]=\lambda(v)[j]$ iff $\beta[i]=\alpha[j]$,

• –

if $\lambda(u)[i]$ does not occur in $\lambda(v)$, then $\lambda(u)[i]=[\beta[i]]_{u}$.

• •

$h_{\mathit{ac}}(\lambda(u))=\beta$, and

• •

$\mathsf{depth}(\lambda(u))=\mathsf{depth}(\lambda(v))+1$.

This completes the construction of $(T_{\mathit{ac}},\lambda)$, $h_{\mathit{ac}}$ and $\mathsf{depth}$. Having $(T_{\mathit{ac}},\lambda)$ in place, we define $D_{\mathit{ac}}$ as $\{\lambda(v):v\in V\}$.

Before we proceed any further, it is important to observe that different nodes $v,u$ of $T_{\mathit{ac}}$ (possibly of different depths) may have the same label, i.e. it may happen that $\lambda(v)=\lambda(u)$. In this case, we treat them as two different atoms since, although syntactically the same, they are present in $T_{\mathit{ac}}$ for different reasons. Therefore, strictly speaking, $D_{\mathit{ac}}$ is a multiset database, i.e., it can hold many occurrences of the same atom, which are treated as different atoms. Let us clarify that the notion of acyclicity given in Definition 5.4 can be directly applied to multiset instances, i.e., a multiset instance is acyclic iff it admits a join tree.

Lemma C.3.

1. (1)

$D_{\mathit{ac}}$* is an acyclic multiset database.* 2. (2)

The mapping $h_{\mathit{ac}}$ is a homomorphism from $D_{\mathit{ac}}$ to $D$. 3. (3)

For each two vertices $u,v\in T_{\mathit{ac}}$, the mapping $h_{\mathit{ac}}$ is an isomorphism from $\{\lambda(u),\lambda(v)\}$ to $\{h_{\mathit{ac}}(\lambda(u)),h_{\mathit{ac}}(\lambda(v))\}$

Proof.

For (1) it suffices to show that $T_{\mathit{ac}}$ is finite, and that it enjoys the connectedness condition (condition (2) of Definition 5.4). By Lemma C.2(1), for $\alpha\in D$, there are only finitely many pairs of atoms $\beta,\beta^{\prime}$ such that $\langle\alpha,\alpha^{\prime},\beta,\beta^{\prime}\rangle$ is a remote-side-parent situation for some $\alpha^{\prime}$. Thus, by construction, the branching degree of $T_{\mathit{ac}}$ is finite. Since the depth of $T_{\mathit{ac}}$ is bounded by $\ell_{\infty}$, $T_{\mathit{ac}}$ is finite. The fact that $T_{\mathit{ac}}$ enjoys the connectedness condition follows by construction; here, the renaming of the constants $t$ of $\mathsf{dom}(D)$ to $[t]_{v}$ is crucial. Claims (2) and (3) also follow by construction.

It remains to show that there exists an infinite restricted chase derivation of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$. Indeed, by showing the latter statement for the multiset database $D_{\mathit{ac}}$, we can conclude that there exists an infinite restricted chase derivation of the acyclic database obtained from $D_{\mathit{ac}}$ by keeping only one occurrence of each atom w.r.t. ${\mathcal{T}}$.

Step 2: An Auxiliary Infinite Sequence of Instances

As we already explained, $D_{\mathit{ac}}$ consists of several (slightly modified) copies of atoms of $D$. It is like seeing the atoms of $D$ through several distorting mirrors, where the mirror images are atoms of $D_{\mathit{ac}}$. Imagine now that we watch the restricted chase derivation $(I_{i})_{i\geq 0}$ through those mirrors. Although during a restricted chase step only one atom, let us say $\alpha$, is generated, in the mirrors we see the generation of several atoms, which are the distorted images of $\alpha$. In order to formalize this phenomenon, we define a variant of the restricted chase, called weakly restricted chase.

Weakly Restricted Chase.

Our intention is to define a variant of chase that allows us to apply several active triggers at the same time, and operates on multiset instances, i.e., multisets of atoms. The reason why we need to consider multisets is because two different mirror images may be syntactically the same.

Definition C.4.

Consider a multiset instance $K$, and let $S$ be a set of active triggers for ${\mathcal{T}}$ on $K$. An application of $S$ to $K$, called weakly restricted chase step, returns the multiset instance

[TABLE]

and is denoted as $K\langle S\rangle K^{\prime}$. A sequence of multiset instances $(K_{i})_{i\geq 0}$, where $K_{0}$ is the database $D^{\prime}$, is a weakly restricted chase derivation of $D^{\prime}$ w.r.t. ${\mathcal{T}}$ if, for each $i\geq 0$, there exists a set $S$ of active triggers for ${\mathcal{T}}$ on $K_{i}$ such that $K_{i}\langle S\rangle K_{i+1}$.

The auxiliary infinite sequence of instances that we are looking for, which will eventually lead to an infinite restricted chase derivation of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$, is an infinite weakly restricted chase derivation of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$. This is essentially (modulo some condition, called the depth condition, given below) the infinite restricted chase derivation $(I_{i})_{i\geq 0}$ seen through the mirrors discussed above.

The Auxiliary Sequence $(K_{i})_{i\geq 0}$.

We now inductively construct a sequence of multiset instances $(K_{i})_{i\geq 0}$, together with a mapping $\bar{h}$ from $\bigcup_{i\geq 0}K_{i}$ to $\mathcal{I}$:

Base Case. Let $K_{0}=D_{\mathit{ac}}$, and for each $\alpha\in K_{0}$, $\bar{h}(\alpha)=h_{\mathit{ac}}(\alpha)$. Recall that $h_{\mathit{ac}}$ is the mapping from $D_{\mathit{ac}}$ to $D$ provided by Lemma C.3.

Inductive Step. Suppose now that $K_{i}$ and $\bar{h}:K_{i}\rightarrow\mathcal{I}$ have been already defined, for $i>0$. Let $S_{i}$ be the set of all active triggers for ${\mathcal{T}}$ on $K_{i}$ of the form $(\sigma^{\mathcal{I}}_{i},h)$, i.e., they use the same TGD $\sigma^{\mathcal{I}}_{i}$ that has been used in $(I_{i})_{i\geq 0}$ to generate the atom $\beta^{\mathcal{I}}_{i}$, such that:

1. (1)

$\bar{h}(h(\gamma_{i}^{\mathcal{I}}))=\mathit{gp}(\beta^{\mathcal{I}}_{i})$, which simply states that the atom of $K_{i}$ that is now about to become a guard-parent must be a mirror image of the guard-parent of the atom $\beta^{\mathcal{I}}_{i}$ in $\mathcal{I}$. 2. (2)

(Depth Condition) $\alpha\prec_{\mathit{gp}}^{+}h(\gamma_{i}^{\mathcal{I}})$, for some atom $\alpha\in D_{\mathit{ac}}$ such that $\alpha=\alpha^{\infty}$, or $\mathsf{depth}(\alpha)<\ell_{\infty}-i$.

We define $K_{i+1}$ as the multiset instance

[TABLE]

i.e., $K_{i}\langle S_{i}\rangle K_{i+1}$. Furthermore, for each $\alpha\in K_{i+1}\setminus K_{i}$, let $\bar{h}(\alpha)=\beta^{\mathcal{I}}_{i}$. This completes the definition of $(K_{i})_{i\geq 0}$.

The Structure of the Auxiliary Sequence.

By construction, $(K_{i})_{i\geq 0}$ is a weakly restricted chase derivation of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$. What is not immediately clear is that $(K_{i})_{i\geq 0}$ is infinite. Our goal, in the rest of this subsection, is to understand how $\mathcal{K}=\bigcup_{i\geq 0}K_{i}$ relates to $\mathcal{I}$. This analysis will give us useful information about the structure of $\mathcal{K}$, which will be crucial later, and also it will allow us to conclude that $\mathcal{K}$ is infinite.

For an atom $\beta\in\mathcal{K}$, we define $\mathcal{K}_{\beta}$ as the set $\{\alpha\in\mathcal{K}:\beta\prec_{\mathit{gp}}^{+}\alpha\}$. The main technical lemma that we need to show follows:

Lemma C.5.

For each $i\geq 0$, the following statements hold:

1. (1)

For each $\alpha\in D_{\mathit{ac}}$ such that $\alpha\neq{\alpha^{\infty}}$, $\bar{h}$ is an isomorphism from $\mathcal{K}_{\alpha}\cap K_{i}$ to $\mathcal{I}_{\bar{h}(\alpha)}\cap I_{k}$, where $k=\min\{i,\ell_{\infty}-\mathsf{depth}(\alpha)\}$. 2. (2)

The mapping $\bar{h}$ is an isomorphism from $\mathcal{K}_{\alpha^{\infty}}\cap K_{i}$ to $\mathcal{I}_{\alpha^{\infty}}\cap I_{i}$.

Proof.

For $\alpha\in D_{\mathit{ac}}$, we define $T^{K}_{i}(\alpha)={\mathcal{K}}_{\alpha}\cap K_{i}$ and $T^{I}_{i}(\alpha)={\mathcal{I}}_{\bar{h}(\alpha)}\cap I_{k}$, where $k=\min\{i,\ell_{\infty}-\mathsf{depth}(\alpha)\}$ if $\mathsf{depth}(\alpha)>0$, and $k=i$ otherwise. Let also ${\alpha^{I}_{i}}$ be an atom of $D$ such that $\alpha^{I}_{i}\prec_{gp}^{+}\beta^{I}_{i}$.

The lemma says that, for $i\geq 0$ and $\alpha\in D_{\mathit{ac}}$, $\bar{h}$ is an isomorphism from $T^{K}_{i}(\alpha)$ to $T^{I}_{i}(\alpha)$. We proceed by induction on $i$. The lemma holds for $i=0$, since $I_{0}=D$ and $K_{0}=D_{\mathit{ac}}$. Assume now that it is also true for some $i\geq 0$.

First observe that, if $\mathsf{depth}(\alpha)>0$ and $\mathsf{depth}(\alpha)\geq\ell_{\infty}-i$, for $\alpha\in D_{\mathit{ac}}$, then $T^{K}_{i}(\alpha)=T^{K}_{i+1}(\alpha)$ (this follows from the Depth Condition), and $T^{I}_{i}(\alpha)=T^{I}_{i+1}(\alpha)$. Thus, for such $\alpha$, the claim directly follows from the hypothesis.

It of course follows from the hypothesis (the part where it tells us something about $\bar{h}$) that, if $\beta\prec_{gp}^{+}\beta^{\prime}$, for some $\beta,\beta^{\prime}\in K_{i}$, then also $\bar{h}(\beta)\prec_{gp}^{+}\bar{h}(\beta^{\prime})$. In other words, if $\beta\in T_{i}^{K}(\alpha)$, then $\bar{h}(\beta)\in T_{i}^{K}(\bar{h}(\alpha))$. This means that, if $\bar{h}(\alpha)\neq\alpha^{I}_{i}$, then $T^{K}_{i}(\alpha)=T^{K}_{i+1}(\alpha)$. In this case, we also have that $T^{I}_{i}(\alpha)=T^{I}_{i+1}(\alpha)$. Hence, again, for such $\alpha$ our claim directly follows from the hypothesis.

Let us now concentrate on the only interesting case, where $\alpha$ is not too deep and is a mirror image of $\alpha^{I}_{i}$ (and, therefore, ${\mathcal{K}}_{\alpha}$ is a mirror image of ${\mathcal{I}}_{\alpha^{I}_{i}}$), which, formally speaking, means that $\bar{h}(\alpha)=\alpha^{I}_{i}$ and $\mathsf{depth}(\alpha)=0$ or $\mathsf{depth}(\alpha)<\ell_{\infty}-i$.

Clearly, for such $\alpha$, there exists exactly one atom which is in $T^{I}_{i+1}(\alpha)$ but not in $T^{I}_{i}(\alpha)$. This atom is $\beta^{I}_{i}$. It is also easy to see that $gp(\beta^{I}_{i})$ (or, $\beta_{gp}$, for short) is somewhere in $T^{I}_{i}(\alpha)$, and, by hypothesis, there is an atom $\kappa_{gp}$ somewhere in $T^{K}_{i}(\alpha)$ such that $\bar{h}(\kappa_{gp})=\beta_{gp}$.

Now, suppose there is an active trigger $(\sigma^{I}_{i},h)$ on $K_{i}$ such that $h(\gamma_{i})=\kappa_{gp}$. Then the atom, call it $\kappa_{new}$, will appear in $K_{i+1}$ as the result of this trigger, with $\bar{h}(\kappa_{new})=\beta^{I}_{i}$, and it is an easy exercise to verify that the new function $\bar{h}$ will be indeed an isomorphism between $T^{K}_{i+1}(\alpha)$ and $T^{I}_{i+1}(\alpha)$.

Thus, the only thing that remains to be shown is that such an active trigger indeed exists. For that we need to show:

(A) All the sideatoms of $\kappa_{gp}$ required by $\sigma_{i}^{\mathcal{I}}$ occur in ${K}_{i}$.

(B) The trigger $(\sigma_{i}^{\mathcal{I}},h)$ for ${\mathcal{T}}$ on $K_{i}$ is active.

For (A), suppose that $\pi$ is a sideatom type of $\gamma_{i}^{\mathcal{I}}$ required by $\sigma_{i}^{\mathcal{I}}$. We know that there is $\beta^{\pi}\in{I}_{i}$ such that $\beta^{\pi}\prec_{sp}^{\pi}\beta_{gp}$. If $\beta^{\pi}\in{\mathcal{I}}_{\alpha^{I}_{i}}={\mathcal{I}}_{\bar{h}(\alpha)}$, then, by induction hypothesis, there is $\kappa^{\pi}\in{\mathcal{K}}_{\alpha}\cap K_{i}$ such that $\kappa^{\pi}\prec_{sp}^{\pi}\kappa$. But what if $\beta^{\pi}$ is a remote side-parent?

Here is where the essence of the construction of $D_{\mathit{ac}}$, and of the Depth Condition, reveals itself. If $\beta^{\pi}\not\in{\mathcal{I}}_{\alpha^{I}_{i}}$, then there exists $\alpha^{\prime}\in D$ such that $\langle\alpha^{I}_{i},\beta^{I}_{i},\alpha^{\prime},\beta^{\pi}\rangle$ is a remote-side-parent situation, and $\beta^{\pi}=\beta^{\mathcal{I}}_{j}$ for some $j<i$. Thus, in $(T_{\mathit{ac}},\lambda)$ there is an edge $(v,u)$ such that $\lambda(v)=\alpha$ and $\lambda(u)=\kappa^{\prime}$, for some $\kappa^{\prime}$ with $\bar{h}(\kappa^{\prime})=\alpha^{\prime}$, as postulated in the Inductive Step of the construction of $D_{\mathit{ac}}$.

We know that either $\mathsf{depth}(\alpha)\leq\ell_{\infty}-i$ or $\mathsf{depth}(\alpha)>\ell_{\infty}-i$ but $\alpha=\alpha^{\infty}$. In both cases, by induction hypothesis, $\bar{h}$ is an isomorphism from $T^{K}_{i}(\kappa^{\prime})$ to $T^{I}_{i}(\kappa^{\prime})$. Let now $\kappa^{\pi}$ be an element of $T^{K}_{i}(\kappa^{\prime})$ such that $\bar{h}(\kappa^{\pi})=\beta^{\pi}$. It follows from the fact that $\bar{h}$ is an isomorphism from $T^{K}_{i}(\alpha)$ and $T^{I}_{i}(\alpha)$, and from Lemma C.3(3), that $\bar{h}$ is also an isomorphism from $T^{K}_{i}(\alpha)\cup T^{K}_{i}(\kappa^{\prime})$ to $T^{I}_{i}(\alpha)\cup T^{I}_{i}(\kappa^{\prime})$ (notice that guardedness is crucial here). Hence, $\kappa^{\pi}\prec_{sp}^{\pi}\kappa_{gp}$.

For (B), assume that the trigger $(\sigma_{i}^{\mathcal{I}},h)$ for ${\mathcal{T}}$ on $K_{i}$ is not active. Thus, there is $\alpha_{\mathit{bad}}\in K_{i}$ such that $\alpha_{\mathit{bad}}\prec_{s}\mathsf{result}(\sigma_{i}^{\mathcal{I}},h)$. We can then conclude that $\bar{h}(\alpha_{\mathit{bad}})\prec_{s}\bar{h}(\mathsf{result}(\sigma_{i}^{\mathcal{I}},h))$. This follows from the fact that, by claim (2) of Lemma C.3, $\bar{h}$ is a homomorphism from $\mathcal{K}$ to $\mathcal{I}$, and thus, if terms are equal in $\alpha_{\mathit{bad}}$ and $\mathsf{result}(\sigma_{i}^{\mathcal{I}},h)$, then they are not less equal in $\bar{h}(\alpha_{\mathit{bad}})$ and $\bar{h}(\mathsf{result}(\sigma_{i}^{\mathcal{I}},h))$. But then $(\sigma_{i}^{\mathcal{I}},h)$ for ${\mathcal{T}}$ on $I_{i}$ is not active due to the atom $\bar{h}(\alpha_{\mathit{bad}})\in I_{i}$, which is a contradiction. This concludes the proof of Lemma C.5.

Let us try to intuitively explain the above complicated lemma. Clearly, both $\mathcal{I}$ and $\mathcal{K}$ are forests (with $\prec_{\mathit{gp}}$ being the tree relation). The roots of the trees in $\mathcal{I}$ are atoms of $D$, while the roots of the trees in $\mathcal{K}$ are atoms of $D_{\mathit{ac}}$. Each atom in $D_{\mathit{ac}}$ has its original atom in $D$, and $\bar{h}$ tells us which is this atom. Now, the second claim of the lemma (which looks simpler) states the following: at every stage of the construction of $\mathcal{K}$, the tree that has been constructed up to this point over the root $\alpha^{\infty}\in D_{\mathit{ac}}$, it is isomorphic to the tree that has been built over $\alpha^{\infty}$ up to the same point of the construction of $\mathcal{I}$. This is actually expected since the construction of $\mathcal{K}$ is exactly the construction of $\mathcal{I}$, but seen in a room full of distorting mirrors, and imagining that $\alpha^{\infty}$ is the only element of $D_{\mathit{ac}}$ that is not a mirror image, but the real atom. Regarding the first claim, as long as $i$ is small enough, the situation is similar to the one in (2). The tree constructed in $\mathcal{K}$, until stage $i$, over the root $\alpha\in D_{\mathit{ac}}$ is isomorphic to the tree constructed in $\mathcal{I}$ until the same point in time over the root $\bar{h}(\alpha)\in D$. For some time we can see a faithful image of the construction, despite the fact that many mirror reflections are needed. But, when $i$ is too large (compared to $\mathsf{depth}(\alpha)$) we can no longer see anything new. Notice that, in particular, if $\mathsf{depth}(\alpha)=\ell_{\infty}$, the lemma states that no tree at all will be built over the root $\alpha$.

Let us now state a useful corollary, which directly follows from Lemma C.5; for the proof of claim (2) recall that ${\mathcal{I}}_{\alpha^{\infty}}$ is infinite, while the proof of claim (5) uses claims (3) and (4).

Corollary C.6.

1. (1)

$\bar{h}$* is an isomorphism from $\mathcal{K}_{\alpha^{\infty}}$ to $\mathcal{I}_{\alpha^{\infty}}$.* 2. (2)

The weakly restricted chase derivation $(K_{i})_{i\geq 0}$ is infinite. 3. (3)

For each atom $\alpha\in D_{\mathit{ac}}$ such that $\alpha\neq{\alpha^{\infty}}$, the mapping $\bar{h}$ is an isomorphism from $\mathcal{K}_{\alpha}$ to $\mathcal{I}_{\bar{h}(\alpha)}\cap I_{\ell_{\infty}-\mathsf{depth}(\alpha)}$. 4. (4)

For $\alpha,\alpha^{\prime}\in D_{\mathit{ac}}$ with $\bar{h}(\alpha)=\bar{h}(\alpha^{\prime})$ and $\mathsf{depth}(\alpha)\leq\mathsf{depth}(\alpha^{\prime})$, there is a 1-1 homomorphism $g$ from ${\mathcal{K}}_{\alpha^{\prime}}$ to ${\mathcal{K}}_{\alpha}$ and $g(\alpha)=\alpha^{\prime}$. 5. (5)

Let $\beta,\beta^{\prime}\in D_{\mathit{ac}}$ such that $\mathsf{depth}(\beta)\leq\mathsf{depth}(\beta^{\prime})$. For each $\alpha\in{\mathcal{K}}_{\beta}$ and $\alpha^{\prime}\in{\mathcal{K}}_{\beta^{\prime}}$ such that $\bar{h}(\alpha)=\bar{h}(\alpha^{\prime})$, there exists a 1-1 homomorphism $g$ from ${\mathcal{K}}_{\alpha^{\prime}}$ to ${\mathcal{K}}_{\alpha}$ and $g(\alpha)=\alpha^{\prime}$.

Step 3: An Infinite Restricted Chase Derivation

In this last step of the proof of the Treeification Theorem, our task is to extract from the infinite weakly restricted chase derivation of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$ constructed above, an infinite restricted chase derivation $(J_{i})_{i\geq 0}$ of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$. For this, we first need to a fix a notation allowing us to directly address the atoms of $\mathcal{K}$.

Let $\mathcal{N}$ be the set of pairs of natural numbers defined as

[TABLE]

By $\leq$ and $<$ we denote the lexicographic ordering on $\mathcal{N}$. Note that $\langle{\mathcal{N}},<\rangle$ and $\langle{\mathbb{N}},<\rangle$ are isomorphic. Now, let $(\kappa_{w})_{w\in{\mathcal{N}}}$ be an enumeration of all the atoms of $\mathcal{K}$ such that:

• •

$\kappa_{[i,j]}\in K_{i+1}\setminus K_{i}$, and

• •

if $\kappa_{[i,j]}\in\mathcal{K}_{\alpha}$ and $\kappa_{[i,j^{\prime}]}\in\mathcal{K}_{\beta}$, for some $j\leq j^{\prime}$ and $\alpha,\beta\in D_{\mathit{ac}}$, then $\mathsf{depth}(\alpha)\leq\mathsf{depth}(\beta)$.

We now present a simple (not necessarily terminating) procedure, dubbed $\mathsf{Extract}(\mathcal{K},{\mathcal{T}})$, that extracts from $\mathcal{K}$ an infinite restricted chase derivation $(J_{i})_{i\geq 0}$ of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$. This algorithm is depicted in the box above. It is clear that each time the while-loop is entered it holds that $J_{m}=\mathit{Born}$. It also follows by construction that:

Lemma C.7.

The sequence of instances $(J_{i})_{i\geq 0}$ produced by $\mathsf{Extract}(\mathcal{K},{\mathcal{T}})$ is a restricted chase derivation of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$.

The crucial question is whether this sequence is infinite. A positive answer to this question will conclude the proof of the treeification theorem. The rest of the section is devoted to showing that:

Lemma C.8.

The sequence of instances $(J_{i})_{i\geq 0}$ produced by $\mathsf{Extract}(\mathcal{K},{\mathcal{T}})$ is infinite.

We first show the following loop invariant lemma, that intuitively states the following: at each point of the execution of our iterative procedure, if an atom is not stopped, then there is a whole tuple of candidates that can act as its side-parents that are also not stopped.

Lemma C.9 (Loop Invariant).

Consider two atoms $\alpha,\beta\in\mathcal{K}$ such that $\beta\prec_{sp}^{\pi}\alpha$, for some sideatom type $\pi$. If $\alpha\in\mathit{Born}\cup\mathit{Pending}$, then there exists $\beta^{\prime}\in\mathit{Born}\cup\mathit{Pending}$ such that $\beta^{\prime}\prec_{sp}^{\pi}\alpha$.

Proof.

We proceed by induction on the number of iterations of $\mathsf{Extract}(\mathcal{K},{\mathcal{T}})$. Clearly, the loop invariant holds at the beginning of the execution. Suppose now that it holds at some point of the execution when we enter the while-loop. Let $\kappa_{[i,j]}$ be the current atom, i.e., the $\leq$-smallest atom of the set $\mathit{Pending}$.

It is easy to see that the guard-parent of $\kappa_{[i,j]}$ necessarily belongs to $\mathit{Born}$: it cannot be in $\mathit{Pending}$ because then $\kappa_{[i,j]}$ would not be minimal in $\mathit{Pending}$, and it cannot be in $\mathit{Stopped}$ because in such a case $\kappa_{[i,j]}$ would be in $\mathit{Stopped}$ too. It is clear that, if there exists an active trigger for ${\mathcal{T}}$ on $J_{m}$ that produces $\kappa_{[i,j]}$, then the set $\mathit{Born}\cup\mathit{Pending}$ remains unchanged since the algorithm will simply remove $\kappa_{[i,j]}$ from $\mathit{Pending}$ and add it to $\mathit{Born}$. Thus, in this case the loop invariant holds.

Assume now that there is no such an active trigger. There are only two cases in which this can happen:

Case 1.

Some of the side-parents $\kappa_{[i,j]}$ needs are not in $\mathit{Born}$. Assume that $\pi^{\prime}$ is a sideatom type required by the TGD $\sigma_{i}^{\mathcal{I}}$, due to which $\kappa_{[i,j]}$ has been generated in $\mathcal{K}$, and let $\kappa_{[i^{\prime},j^{\prime}]}$ be any candidate from $\mathcal{K}$ such that $\kappa_{[i^{\prime},j^{\prime}]}\prec_{sp}^{\pi^{\prime}}\kappa_{[i,j]}$. It should be clear that $i^{\prime}<i$. By construction, $\kappa_{[i^{\prime},j^{\prime}]}\in\mathit{Born}\cup\mathit{Stopped}$ (since $\kappa_{[i,j]}$ is minimal in $\mathit{Pending}$). By induction hypothesis, there is, among these candidates, at least one that belongs to $\mathit{Born}\cup\mathit{Pending}$. Hence, there must be at least one of those candidates in $\mathit{Born}$. This implies that this first case does not apply.

Case 2.

There is an atom $\kappa_{[i^{\prime},j^{\prime}]}\in J_{m}$ such that $\kappa_{[i^{\prime},j^{\prime}]}\prec_{s}\kappa_{[i,j]}$. By an argument similar to that for statement (B) in the proof of Lemma C.5 above, we can show that in such a case it would be $\bar{h}(\kappa_{[i^{\prime},j^{\prime}]})\prec_{s}\bar{h}(\kappa_{[i,j]})$. Since $(I_{i})_{i\geq 0}$ is a restricted chase derivation, we get that $i^{\prime}\geq i$. But since $\kappa_{[i^{\prime},j^{\prime}]}\in J_{m}$, we get that $i^{\prime}=i$, and thus, $j^{\prime}<j$. This means that $\bar{h}(\kappa_{[i,j]})=\bar{h}(\kappa_{[i^{\prime},j^{\prime}]})$, and $\kappa_{[i,j]}\in{\mathcal{K}}_{\beta}$ and $\kappa_{[i^{\prime},j^{\prime}]}\in{\mathcal{K}}_{\beta^{\prime}}$ for some $\beta,\beta^{\prime}\in D_{\mathit{ac}}$ such that $\mathsf{depth}(\beta^{\prime})\leq\mathsf{depth}(\beta)$. By Corollary C.6, ${\mathcal{K}}_{\kappa_{[i,j]}}$ is isomorphic to a subset of ${\mathcal{K}}_{\kappa_{[i^{\prime},j^{\prime}]}}$ via an isomorphism, let us say $g$, such that $g(\kappa_{[i,j]})=\kappa_{[i^{\prime},j^{\prime}]}$. Assume now that there are $\kappa,\kappa_{\pi}\in\mathit{Born}\cup\mathit{Pending}$ such that $\kappa_{\pi}\prec_{sp}^{\pi}\kappa$. We need to show that, after $\kappa_{[i,j]}$ gets stopped, together with all its $\prec_{\mathit{gp}}^{+}$-descendants, the loop invariant will still hold. Observe that if $\kappa_{\pi}\not\in{\mathcal{K}}_{\kappa_{[i,j]}}$, then it is not affected by the removal of atoms of ${\mathcal{K}}_{\kappa_{[i,j]}}$. Moreover, if $\kappa\in{\mathcal{K}}_{\kappa_{[i,j]}}$, then it gets stopped, and there is nothing to show about its side-parents. Thus, the only case that we need to worry about is when $\kappa\not\in{\mathcal{K}}_{\kappa_{[i,j]}}$ and $\kappa_{\pi}\in{\mathcal{K}}_{\kappa_{[i,j]}}$. In this case all the terms in $\kappa_{\pi}$ occur in $\mathsf{fr}(\kappa_{[i,j]})$. Furthermore, since $\kappa_{[i^{\prime},j^{\prime}]}\prec_{s}\kappa_{[i,j]}$, $\mathsf{fr}(\kappa_{[i,j]})=\mathsf{fr}(\kappa_{[i^{\prime},j^{\prime}]})$. Hence, the atom $g(\kappa_{\pi})$, which is in ${\mathcal{K}}_{\kappa_{[i,j]}}$, and thus in $\mathit{Born}\cup\mathit{Pending}$ after the current iteration, is such that $g(\kappa_{\pi})\prec_{sp}^{\pi}\kappa$, and the claim follows.

In order to understand the meaning of this lemma, recall that $\mathcal{K}$, since it was produced by a weakly restricted chase, is a multiset, and there can be many atoms $\beta\in\mathcal{K}$ such that $\beta\prec_{sp}^{\pi}\alpha$. This is a phenomenon that never happens in a normal restricted chase. By exploiting the loop invariant lemma, we can show that none of the atoms of $\mathcal{K}_{\alpha^{\infty}}$ is stopped during our iterative procedure.

Lemma C.10.

For each $\alpha\in\mathcal{K}$, if $\alpha\in\mathcal{K}_{\alpha^{\infty}}$, then $\alpha$ occurs in an instance of the sequence $(J_{i})_{i\geq 0}$ produced by $\mathsf{Extract}(\mathcal{K},{\mathcal{T}})$.

Proof.

We need to show that $\alpha\not\in\mathit{Stopped}$ for any $\alpha\in\mathcal{K}_{\alpha^{\infty}}$. Assume that there exists an atom of $\mathcal{K}_{\alpha^{\infty}}$ that belongs to $\mathit{Stopped}$; let $\hat{\alpha}$ be the $<$-smallest such atom. The loop invariant lemma (Lemma C.9) ensures that $\hat{\alpha}$ belongs to $\mathit{Stopped}$ not because some of its side-parents are missing, but for a different reason; in fact, for one of the following two reasons:

1. (1)

There exists an atom $\beta\in\mathit{Stopped}$ such that $\beta\prec_{\mathit{gp}}^{+}\hat{\alpha}$. Clearly, $\beta\in\mathcal{K}_{\alpha^{\infty}}$ and also $\beta<\hat{\alpha}$. But this contradicts the fact that $\hat{\alpha}$ is the $<$-smallest atom of $\mathcal{K}_{\alpha^{\infty}}$ that has been stopped. Thus, this reason does not apply. 2. (2)

There is $\beta\in\mathit{Born}$, with $\beta<\hat{\alpha}$ and $\beta\prec_{s}\hat{\alpha}$. Let $\beta=\kappa_{[i^{\prime},j^{\prime}]}$ and $\hat{\alpha}=\kappa_{[i,0]}$; it follows from the definition of $(\kappa_{w})_{w\in\mathcal{N}}$ that $\kappa_{[i,j]}\in\mathcal{K}_{\alpha^{\infty}}$ implies $j=0$. Clearly, $[i^{\prime},j^{\prime}]<[i,0]$. However, since $\kappa_{[i^{\prime},j^{\prime}]}\prec_{s}\kappa_{[i,0]}$, we get that $i^{\prime}\geq i$. Thus, $j<0$, which is not possible. Hence, also this reason does not apply.

Since none of the above cases apply, the claim follows.

Having Lemma C.10, it is clear that Lemma C.8 follows. Indeed, since $\mathcal{K}_{\alpha^{\infty}}$ is infinite (Corollary  C.6), and since each restricted chase step generates just one atom, we immediately get that the sequence $(J_{i})_{i\geq 0}$ of instances produced by $\mathsf{Extract}(\mathcal{K},{\mathcal{T}})$ is infinite. Therefore, $(J_{i})_{i\geq 0}$ is an infinite restricted chase derivation of $D_{\mathit{ac}}$ w.r.t. ${\mathcal{T}}$. This completes the proof of the Treeification Theorem.

C.3. Proof of Lemma 5.12

Let us assume, for the moment, that we have available the following auxiliary MSOL formulas (more details are given below); as usual, we use lower-case letters $x,y,\ldots$ for first-order variables, and upper-case letters $A,B,\ldots$ for second-order variables:

[TABLE]

By exploiting the above formulas, we can easily define $\phi_{\mathcal{T}}$ as the conjunction of the following four sentences:

1. (1)

$\phi_{\mathit{jt}}$ checks whether $T$ is an abstract join tree. It is easy to verify that all the conditions in the definition of abstract join trees (see Definition 5.8) are first-order expressible, apart from the first one, which states that the set $\{x\in V:\mathsf{org}(x)=F\}$ is finite. For this check we exploit the MSOL formula $\phi_{\mathit{fin}}$. 2. (2)

$\phi_{1}$ checks for the first condition of Definition 5.10 as follows:

[TABLE] 3. (3)

$\phi_{2}$ checks for the second condition; in what follows, we assume that $\sigma$ has body $\alpha,\pi_{1},\ldots,\pi_{k}$:

[TABLE]

Notice that $\mathsf{org}(y)=\sigma$ is an abbreviation of a big disjunction that checks, via monadic predicates $M_{\tau}$, where $\tau\in\Lambda_{\mathcal{T}}$, whether the label of $y$ is of the form $\langle\cdot,\sigma,\cdot\rangle$. 4. (4)

$\phi_{3}$ checks for the third condition as follows:

[TABLE]

We proceed to give more details about the auxiliary formulas used in $\phi_{\mathcal{T}}$. The formal definitions are omitted since they are long and tedious, but we give enough evidence that the formulas are indeed expressible in MSOL. Note that the following discussion heavily relies on the obvious fact below, which we will silently use:

Fact C.11.

Let $T=\langle V,\Yleft\rangle$ be an abstract join tree. For each term $t$ in $\Delta(T)$, $\{x\in V:t\text{ occurs in }\delta(x)\}$ induces a connected subtree of $T$.

Formula $\phi_{\mathit{fin}}(A)$.

This formula comes from the general MSOL toolbox. It states that every infinite directed path $B$ in $T$, starting from the root node of $T$, has an infinite directed sub-path, starting from some non-root element of $B$, which is disjoint with $A$.

Formula $\phi_{=}^{i,j}(x,y)$, for each $i,j\in\{1,\ldots,\mathsf{ar}({\mathcal{T}})\}$.

Notice that these formulas have not been explicitly used above. However, they are needed for defining $\phi_{\pi}$ and $\phi_{b}$. The formula $\phi_{=}^{i,j}(x,y)$ says that the term in $\delta(x)$ at position $i$ is equal to the term in $\delta(y)$ at position $j$. This can be expressed in MSOL as follows: there is a set $A\subseteq V$ such that (i) $A$ is a path with $x$ and $y$ being its ends, i.e., $A$ is finite, $x,y$ have exactly one neighbor in $A$, and any other node in $A$ has exactly two neighbors, and (ii) $A$ is a disjoint union of $A_{1},\ldots,A_{\mathsf{ar}({\mathcal{T}})}$ such that $x\in A_{i}$, $y\in A_{j}$, and, for all pairs $z,w\in A$ such that $z\Yleft w$, $z\in A_{k}$, $w\in A_{\ell}$ it holds that $[[f,k],[m,\ell]]\in\mathsf{eq}(w)$.

Formula $\phi_{\pi}(x,y)$.

The formula says that $\delta(x)\subseteq_{\pi}\delta(y)$. It should be clear that it can be easily expressed by exploiting the formulas $\phi_{=}^{i,j}$ given above for checking whether terms in atoms are equal.

Formula $\phi_{b}(x,y)$.

We first devise a formula $\psi_{b}(x,y)$, which states that $x\prec_{b}y$. Such a formula can be defined by using $\phi_{\pi}$ above, and also the formula $\phi_{s}(x,y)\equiv x\prec_{s}y$, which can be in turn defined by exploiting the formulas $\phi_{=}^{i,j}(x,y)$, for $i,j\in\{1,\ldots,\mathsf{ar}({\mathcal{T}})\}$.

Having $\psi_{b}$ we can then devise a formula $\phi_{\mathit{cl}}(A)$, which states that $A$ is $\prec_{b}$-downward closed, i.e., for each $x,y\in V$, with $x\prec_{b}y$ and $y\in A$ there is also $x\in A$.

Finally, $\phi_{b}(x,y)$ simply says that, for every $\prec_{b}$-downward closed set $A$ it holds that $y\in A$ implies $x\in A$.

Appendix D Proofs from Section 6

D.1. Proof of Lemma 6.11

Let us first establish an auxiliary claim, which essentially states that every free connected proto-caterpillar trivially satisfies condition (2) of Definition 6.3:

Lemma D.1.

Consider a free connected proto-caterpillar $\diamondsuit=(L^{\diamondsuit},(\alpha_{i}^{\diamondsuit})_{i\geq 0},(\sigma_{i}^{\diamondsuit},h_{i}^{\diamondsuit})_{i>0},(\gamma_{i}^{\diamondsuit})_{i>0})$. For $\beta\in L^{\diamondsuit}$ and $i>0$, $\beta\not\prec_{s}\alpha_{i}^{\diamondsuit}$.

Proof.

Towards a contradiction, assume that there exists $\beta\in L^{\diamondsuit}$ and $i>0$ such that $\beta\prec_{s}\alpha_{i}^{\diamondsuit}$. This implies that there exists a relay term ${\mathfrak{c}}$ of $\heartsuit$ occurring in $\mathsf{fr}(\alpha_{i}^{\diamondsuit})$ that occurs also in $\beta$. Let $\alpha_{j}^{\diamondsuit}$, for $j<i$, be the birth atom of ${\mathfrak{c}}$. In the special case where ${\mathfrak{c}}$ is the first relay term of $\diamondsuit$, then $j=0$. Assuming that ${\mathfrak{c}}^{\prime}$ is the next relay term of $\diamondsuit$ after ${\mathfrak{c}}$, let $k>i$ be such that $\alpha_{k}^{\diamondsuit}$ is the birth atom of ${\mathfrak{c}}^{\prime}$. By connectedness, ${\mathfrak{c}}$ occurs in $\mathsf{fr}(\alpha_{\ell}^{\diamondsuit})$ for every $j<\ell\leq k$. Moreover, we know that there exists $j\leq\ell\leq k$ such that $\beta\prec_{p}\alpha_{\ell}^{\diamondsuit}$. Since $\beta\neq\alpha_{\ell-1}^{\diamondsuit}$ and $\diamondsuit$ is free, we can conclude that the TGD $\sigma_{\ell}^{\diamondsuit}$ (recall that the trigger $(\sigma_{\ell}^{\diamondsuit},h_{\ell}^{\diamondsuit})$ generates $\alpha_{\ell}^{\diamondsuit}$), apart from the atom $\gamma_{\ell}^{\diamondsuit}$, which is mapped by $h_{\ell}^{\diamondsuit}$ to $\alpha_{\ell-1}^{\diamondsuit}$, has another atom in its body that is mapped by $h_{\ell}^{\diamondsuit}$ to $\beta$, while it shares a variable $x$ with $\gamma_{\ell}^{\diamondsuit}$ and $h_{\ell}^{\diamondsuit}(x)={\mathfrak{c}}$. Since ${\mathcal{T}}$ is a sticky set of TGDs, we conclude that ${\mathfrak{c}}$ occurs at an immortal position, which contradicts the fact that $\diamondsuit$ is connected.

We are now ready to give the proof of Lemma 6.11.

Proof of Lemma 6.11.

The fact that $\heartsuit$ is a connected proto-caterpillar follows from the fact that $\spadesuit$ is a connected proto-caterpillar (Lemma 6.10). In particular, by applying $\bar{h}$ on the atoms occurring in $\spadesuit$, there is no way to violate the conditions (1) - (3) of Definition 6.2, or the connectedness condition as defined in Definition 6.6. Moreover, it follows by construction that, for each $(\alpha,i),(\beta,j)\in\Pi(L^{\heartsuit}\cup B^{\heartsuit})$, $\alpha[i]=\beta[j]$ implies $(\alpha,i)\simeq_{L^{\heartsuit}\cup B^{\heartsuit}}^{*}(\beta,j)$, and thus, $\heartsuit$ is free. It remains to show that $\heartsuit$ enjoys the two conditions of Definition 6.3, which we recall here:

1. (1)

for each $\beta\in L^{\heartsuit}$ and $i>0$, $\beta\not\prec_{s}\alpha_{i}^{\heartsuit}$, and 2. (2)

for each $0\leq i<j$, $\alpha_{i}^{\heartsuit}\not\prec_{s}\alpha_{j}^{\heartsuit}$.

Since $\heartsuit$ is a free conected proto-caterpillar, (1) immediately follows from Lemma D.1.

For (2), towards a contradiction, assume that $\alpha_{i}^{\heartsuit}\prec_{s}\alpha_{j}^{\heartsuit}$ for some $0\leq i<j$. Since we know that, if a term in $\alpha_{i}^{\heartsuit}$ is equal to a term in $\alpha_{j}^{\heartsuit}$, then the terms at the same positions in $\alpha_{i}^{\spadesuit}$ and $\alpha_{j}^{\spadesuit}$ are also equal, we get that $\alpha_{i}^{\spadesuit}\prec_{s}\alpha_{j}^{\spadesuit}$. This implies that $\alpha_{i+n}^{\clubsuit}\prec_{s}\alpha_{j+n}^{\clubsuit}$; recall, from the construction of $\spadesuit$, that $n$ is such that $\alpha_{n}^{\clubsuit}$ is the birth atom of the relay term ${\mathfrak{c}}_{i_{0}}$. Therefore, there are atoms $\beta,\beta^{\prime}\in\mathcal{I}$ such that $\beta\prec_{p}^{+}\beta^{\prime}$ and $\beta\prec_{s}\beta^{\prime}$. But this contradicts the fact that $\beta\not\prec_{s}\beta^{\prime}$ since $(I_{i})_{i\geq 0}$ is a restricted chase derivation.

D.2. Proof of Lemma 6.12

The high-level idea of the construction is as follows. We first show that for an equality type $e=(R,E)$ from $\mathsf{etypes}(\mathsf{sch}({\mathcal{T}}))$, and a set of positions $\Pi\subseteq\{1,\ldots,\mathsf{ar}(R)\}$, we can build a deterministic Büchi automaton ${\mathcal{A}}_{e,\Pi}$ such that $L({\mathcal{A}}_{e,\Pi})\neq\emptyset$ iff there exists a free connected caterpillar such that its body starts with an atom of equality type $e$, and its first relay term occurs at positions $\Pi$ of this atom. This means that a word $\mathbf{w}$ (which we will call caterpillar word and its over a finite alphabet $\Lambda_{\mathcal{T}}$) accepted by ${\mathcal{A}}_{e,\Pi}$ is actually a symbolic representation of a free connected caterpillar as the one above. Observe now that there are finitely many pairs $(e,\Pi)$, where $e=(R,E)$ is an equality type of $\mathsf{etypes}(\mathsf{sch}({\mathcal{T}}))$, and $\Pi\subseteq\{1,\ldots,\mathsf{ar}(R)\}$; let $\mathsf{etp}_{\mathcal{T}}$ be the set of all such pairs. Since Büchi automata are closed under union, i.e., given two Büchi automata ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$, we can construct a Büchi automaton, denoted ${\mathcal{A}}_{1}\cup{\mathcal{A}}_{2}$, that recognizes the language $L({\mathcal{A}}_{1})\cup L({\mathcal{A}}_{2})$, the desired automaton is defined as the deterministic Büchi automaton

[TABLE]

Thus, our main task in the remainder of the section is, for a pair $(e,\Pi)\in\mathsf{etp}_{\mathcal{T}}$, to construct the Büchi automaton ${\mathcal{A}}_{e,\Pi}$.

Caterpillar Words and Automata

It is easy to see that a free proto-caterpillar is fully described (up to isomorphism, of course) by the equality type of the first atom $\alpha_{0}$ of its body, and an infinite sequence of TGD-atom pairs $(\sigma_{i},\gamma_{i})_{i>0}$, which tells us which TGD of ${\mathcal{T}}$ should be used to produce the next atom of the proto-caterpillar’s body, and which atom of the body of this TGD must match with the previous atom of the proto-caterpillar’s body. The remaining atoms of the body of the TGD tell us which are the leg atoms of the proto-caterpillar.777Notice that here we silently assume, w.l.o.g., that the proto-caterpillar is minimal in the sense that all the leg atoms participate in the generation of a body atom. Of course, not each such sequence translates to a free proto-caterpillar (as it may happen that some $\gamma_{i+1}$ does not match with the $i$-the atom according to $\alpha_{0}$ and the sequence $(\sigma_{1},\gamma_{1}),(\sigma_{2},\gamma_{2}),\ldots,(\sigma_{i},\gamma_{i})$), but if it does then the free proto-caterpillar is unique. However, there is no guarantee that this unique free proto-caterpillar is a connected caterpillar. In order to fully describe a free connected caterpillar we also need somehow to mark the pass-on points. This brings us to the notion of the caterpillar word (for ${\mathcal{T}}$).

We first define the finite alphabet $\Lambda_{\mathcal{T}}$, which consists of triples of the form $(\sigma,\gamma,P)$, where $\sigma\in{\mathcal{T}}$, $\gamma\in\mathsf{body}(\sigma)$, and, assuming that $R$ is the predicate of $\mathsf{head}(\sigma)$, $P\subseteq\{1,\ldots,\mathsf{ar}(R)\}$ is such that $P\neq\emptyset$ implies there exists $i\in\{1,\ldots,\mathsf{ar}(R)\}$ with $\mathsf{head}(\sigma)[i]\not\in\mathsf{fr}(\sigma)$ and $P=\{j:\mathsf{head}(\sigma)[i]=\mathsf{head}(\sigma)[j]\}$. Then:

Definition D.2.

A caterpillar word (for ${\mathcal{T}}$) is an infinite word $\mathbf{w}=w_{1}w_{2}\cdots$ such that, for each $i\geq 1$, $w_{i}\in\Lambda_{\mathcal{T}}$.

Intuitively, a caterpillar word $\mathbf{w}=w_{1}w_{2},\cdots$, with $w_{i}=(\sigma_{i},\gamma_{i},P_{i})$, is a candidate symbolic representation of a free connected caterpillar, where $w_{i}$ marks a pass-on point iff $P_{i}$ is non-empty. In fact, $P_{i}$ indicates at which positions of $\mathsf{head}(\sigma_{i})$ the new relay term appears. Now, given a pair $(e_{0},\Pi_{0})\in\mathsf{etp}_{\mathcal{T}}$, we say that $\mathbf{w}$ encodes a free connected caterpillar starting at $(e_{0},\Pi_{0})$888We keep this definition semi-formal as the formal one is very tedious and it does not add any technical value to the proof. if the sequence of TGD-atom pairs $(\sigma_{i},\gamma_{i})_{i>0}$ translates to a free connected caterpillar $\diamondsuit=(L^{\diamondsuit},(\alpha_{i}^{\diamondsuit})_{i\geq 0},(\sigma_{i}^{\diamondsuit},h_{i}^{\diamondsuit})_{i>0},(\gamma_{i}^{\diamondsuit})_{i>0})$, where (i) $\mathsf{et}(\alpha_{0}^{\diamondsuit})=e_{0}$, and the first relay term of $\diamondsuit$ occurs in $\alpha_{0}^{\diamondsuit}$ at positions $\Pi_{0}$, (ii) $\sigma_{i}=\sigma_{i}^{\diamondsuit}$ and $\gamma_{i}=\gamma_{i}^{\diamondsuit}$, for each $i>0$, and (iii) assuming that $b_{1}<b_{2}<\cdots$ are the pass-on points of $\diamondsuit$, $P_{i}\neq\emptyset$ iff $i\in\{b_{1},b_{2},\ldots\}$, and the $k$-th relay term of $\diamondsuit$ occurs in $\alpha_{b_{k}}^{\diamondsuit}$ at positions $P_{k}$.

Recall that our goal is to construct a deterministic Büchi automaton ${\mathcal{A}}_{e_{0},\Pi_{0}}$, with $\Lambda_{\mathcal{T}}$ being its alphabet, such that $L({\mathcal{A}}_{e_{0},\Pi_{0}})$ is exactly the set of caterpillar words that encode a free connected caterpillar starting at $(e_{0},\Pi_{0})$. The automaton ${\mathcal{A}}_{e_{0},\Pi_{0}}$ is defined as the (almost) cartesian product of three automata:

• •

${\mathcal{A}}_{\mathit{pc}}$ that checks whether a caterpillar word $\mathbf{w}$ encodes a free proto-caterpillar such that $e_{0}$ is the equality type of the first atom of its body. Note that the set $\Pi_{0}$ does not play any role here. In fact, this automaton will only read the first two elements of each letter of $\mathbf{w}$.

• •

${\mathcal{A}}_{\mathit{qc}}$ that checks whether a caterpillar word $\mathbf{w}$ that encodes a free proto-caterpillar $\diamondsuit$ is such that $\diamondsuit$ is a quasi-caterpillar, i.e., it satisfies condition (2) of Definition 6.3, that is, assuming that $(\alpha_{i}^{\diamondsuit})_{i\geq 0}$ is the body of $\diamondsuit$, $\alpha_{i}^{\diamondsuit}\not\prec_{s}\alpha_{j}^{\diamondsuit}$ for each $0\leq i<j$. This automaton is quite involved, and as ${\mathcal{A}}_{\mathit{pc}}$ above, it will read only the first two elements of each letter of $\mathbf{w}$.

• •

${\mathcal{A}}_{\mathit{cc}}$ that checks whether a caterpillar word $\mathbf{w}$ that encodes a free quasi-caterpillar $\diamondsuit$ is such that $\diamondsuit$ is connected. Since, by Lemma D.1, a free connected quasi-caterpillar is a caterpillar, ${\mathcal{A}}_{\mathit{cc}}$ essentially checks whether $\diamondsuit$ is a free connected caterpillar, i.e., condition (1) of Definition 6.3 comes for free.

By “almost cartesian product” we mean that the states of ${\mathcal{A}}_{e_{0},\Pi_{0}}$ will be triples, consisting of the states of ${\mathcal{A}}_{\mathit{pc}}$, ${\mathcal{A}}_{\mathit{qc}}$, and ${\mathcal{A}}_{\mathit{cc}}$. The transition functions of ${\mathcal{A}}_{\mathit{pc}}$ and ${\mathcal{A}}_{\mathit{cc}}$ will only depend on the current symbol of the word $\bf w$ and of the current state of the respective automaton. However, the transition function of ${\mathcal{A}}_{\mathit{qc}}$ will also use the current state of ${\mathcal{A}}_{\mathit{pc}}$ as part of its argument. Regarding the acceptance, each of the three automata will have a designated $\mathit{reject}$ state. If any of them is ever encountered, then we assume that ${\mathcal{A}}_{e_{0},\Pi_{0}}$ immediately rejects the input word $\mathbf{w}$. Apart from the $\mathit{reject}$ state, ${\mathcal{A}}_{cc}$ will have an accepting state. The automaton ${\mathcal{A}}_{e_{0},\Pi_{0}}$, which, as we said, is a Büchi automaton, will accept if ${\mathcal{A}}_{\mathit{cc}}$ will encounter this accepting state infinitely many times while reading the word $\bf w$. We can now describe the three automata in question.

The Automaton ${\mathcal{A}}_{\mathit{pc}}$

Since we are building a finite automaton, and there are infinitely many atoms in a caterpillar’s body, there is no hope the automaton, after reading the symbol $w_{i}$ of the input caterpillar word ${\bf w}=w_{1}w_{2}\cdots$, could “know” the $i$-th atom of the body of the proto-caterpillar encoded by $\bf w$. But it can know its equality type. We define the function $\delta_{\mathsf{et}}:\mathsf{etypes}(\mathsf{sch}({\mathcal{T}}))\times\Lambda_{\mathcal{T}}\rightarrow\mathsf{etypes}(\mathsf{sch}({\mathcal{T}}))\cup\{\mathit{reject}\}$ as follows: for each $e\in\mathsf{etypes}(\mathsf{sch}({\mathcal{T}}))$ and $(\sigma,\gamma,\cdot)\in\Lambda_{\mathcal{T}}$,

• •

if there is a homomorphism $h$ that maps $\gamma$ to $R(\star_{1},\ldots,\star_{n})$, with $\star_{i}=\star_{j}$ iff $i,j$ coexist in a set of $E$, then $\delta_{\mathsf{et}}(e,(\sigma,\gamma,\cdot))=\mathsf{et}(\bar{h}(\mathsf{head}(\sigma)))$, where $\bar{h}$ is an extension of $h$ that maps each existentially quantified variable in $\sigma$ to a distinct symbol;

• •

otherwise, $\delta_{\mathsf{et}}(e,(\sigma,\gamma,\cdot))=\mathit{reject}$.

Let ${\mathcal{A}}_{\mathit{pc}}$ be a Büchi automaton with

• •

$\mathsf{etypes}(\mathsf{sch}({\mathcal{T}}))\cup\{\mathit{reject}\}$ its set of states,

• •

$\Lambda_{\mathcal{T}}$ its alphabet,

• •

$\delta_{\mathsf{et}}$ its transition function, and

• •

$e_{0}$ its initial state.

Clearly, for a caterpillar word $\mathbf{w}$, ${\mathcal{A}}_{\mathit{pc}}$ does not reject $\bf w$ iff $\bf w$ encodes a free proto-caterpillar $\diamondsuit=(\cdot,(\alpha_{i}^{\diamondsuit})_{i\geq 0},\cdot,\cdot)$ such that $\mathsf{et}(\alpha_{0}^{\diamondsuit})=e_{0}$; and if it does, then $\delta_{\mathsf{et}}(\mathsf{et}(\alpha_{i-1}^{\diamondsuit}),w_{i})=\mathsf{et}(\alpha_{i}^{\diamondsuit})$, for each $i>0$.

The Automaton ${\mathcal{A}}_{\mathit{qc}}$

From now on we assume that an input caterpillar word $\bf w$ encodes a free proto-caterpillar $\diamondsuit=(\cdot,(\alpha_{i}^{\diamondsuit})_{i\geq 0},\cdot,\cdot)$ such that the first atom of its body has equality type $e_{0}$ (in case it does not encode such a free proto-caterpillar, ${\mathcal{A}}_{\mathit{pc}}$ will take care of it), and proceed towards checking whether $\diamondsuit$ is a quasi-caterpillar, i.e., whether it satisfies condition (2) of Definition 6.3, that is, $\alpha_{i}^{\diamondsuit}\not\prec_{s}\alpha_{j}^{\diamondsuit}$ for each $0\leq i<j$.

Given a finite set $\mathfrak{T}$ of terms, a $\mathfrak{T}$-equality type over a schema $\mathbf{S}$ is essentially an equality type $(R,E)$ over $\mathbf{S}$ where, in addition, some of the sets of $E$ are labeled with distinct terms of $\mathfrak{T}$ indicating that a term $t\in\mathfrak{T}$ should occur at certain positions. Formally, a $\mathfrak{T}$-equality type over $\mathbf{S}$ is a triple $(R,E,\lambda)$, where $(R,E)\in\mathsf{etypes}(\mathbf{S})$, and $\lambda$ is a partial injective function from $E$ to $\mathfrak{T}$. It is clear that there are only finitely many $\mathfrak{T}$-equality types over $\mathbf{S}$. The $\mathfrak{T}$-equality type of an atom $\alpha$, denoted $\mathsf{et}_{\mathfrak{T}}(\alpha)$, as well as the canonical atom of a $\mathfrak{T}$-equality type $e$, denoted $\mathsf{can}(e)$, are defined in the expected way.

Now, for brevity, let ${\mathfrak{T}}_{j}$ be the set of terms occurring in $\alpha_{j}^{\diamondsuit}$. We can easily show the following useful lemma:

Lemma D.3.

Suppose $i<j<k$ for some $i,j,k\geq 0$. It holds that $\alpha_{i}^{\diamondsuit}\prec_{s}\alpha_{k}^{\diamondsuit}$ iff $\mathsf{can}(\mathsf{et}_{{\mathfrak{T}}_{j}}(\alpha_{i}^{\diamondsuit}))\prec_{s}\alpha_{k}^{\diamondsuit}$.

Proof.

First, for each set of terms ${\mathfrak{T}}$ that contains all the terms occurring both in $\alpha_{i}^{\diamondsuit}$ and $\alpha_{k}^{\diamondsuit}$, it is easy to show that $\alpha_{i}^{\diamondsuit}\prec_{s}\alpha_{k}^{\diamondsuit}$ iff $\mathsf{can}(\mathsf{et}_{{\mathfrak{T}}}(\alpha_{i}^{\diamondsuit}))\prec_{s}\alpha_{k}^{\diamondsuit}$. Now, since $\diamondsuit$ is free, if some term occurs in $\alpha_{i}^{\diamondsuit}$ and $\alpha_{k}^{\diamondsuit}$, then it must also occur in $\alpha_{j}^{\diamondsuit}$. This implies that ${\mathfrak{T}}_{j}$ contains all the terms occurring both in $\alpha_{i}^{\diamondsuit}$ and $\alpha_{k}^{\diamondsuit}$, and the claim follows.

For each $j\geq 0$, let $\Theta_{j}=\{\mathsf{et}_{{\mathfrak{T}}}(\alpha_{i}^{\diamondsuit}):0\leq i\leq j\}$. Of course, $\Theta_{j}$ is a finite set, for each $j\geq 0$. Moreover, if we just know $\mathsf{et}(\alpha_{j}^{\diamondsuit})$, then the number of possible candidates for $\Theta_{j}$ is finite, and uniformly bounded, so $\Theta_{j}$ can be seen as a finite piece of information, or as (part of) a state of a finite automaton. It is possible to construct $\Theta_{j+1}$ only knowing $\Theta_{j}$, $\mathsf{et}(\alpha_{j}^{\diamondsuit})$ and the $(j+1)$-th symbol $w_{j+1}$ of $\mathbf{w}$. Furthermore, knowing $\Theta_{j}$ and $\mathsf{et}(\alpha_{j}^{\diamondsuit})$, we can check whether there is $0\leq i<j$ such that $\alpha_{i}^{\diamondsuit}\prec_{s}\alpha_{j}^{\diamondsuit}$; the latter is a consequence of Lemma D.3. Thus, we can define a function $\delta_{\Theta}$ such that:

$\delta_{\Theta}\left((\Theta_{j},\mathsf{et}(\alpha_{j}^{\diamondsuit})),(\sigma_{j+1},\gamma_{j+1},\cdot)\right)$

[TABLE]

Let ${\mathcal{A}}_{\mathit{qc}}$ be a Büchi automaton with

• •

its set of states consisting of pairs of the form $(\Theta,e)$ as above, and the $\mathit{reject}$ state,

• •

$\Lambda_{\mathcal{T}}$ its alphabet,

• •

$\delta_{\Theta}$ its transition function, and

• •

$(\emptyset,e_{0})$ its initial state.

By construction, for a caterpillar word $\mathbf{w}$, ${\mathcal{A}}_{\mathit{qc}}$ does not reject $\bf w$ iff $\bf w$ encodes a free proto-caterpillar $\diamondsuit$ that satisfies condition (2) of Definition 6.3, i.e., $\diamondsuit$ is a quasi-caterpillar.

The Automaton ${\mathcal{A}}_{\mathit{cc}}$

First, we need to define a function $\delta_{\mathit{pos}}$ that will let the automaton remember some terms. Given $\Pi\subseteq\{1,\ldots,\mathsf{ar}({\mathcal{T}})\}$ and $w=(\sigma,\gamma,P)\in\Lambda_{\mathcal{T}}$, let $\delta_{\mathit{pos}}(\Pi,w)$ be the set of integers

[TABLE]

The purpose of $\delta_{\mathit{pos}}$ will be made clear in a while.

The states of ${\mathcal{A}}_{\mathit{cc}}$ will be tuples $(\Pi_{1},\Pi_{2},q)$, where $\Pi_{1},\Pi_{2}\subseteq\{1,\ldots\mathsf{ar}({\mathcal{T}})\}$ and $q\in\{\top,\bot\}$. Roughly, $\Pi_{1}$ will remember the positions where the current relay term appears (we need this information since we must make sure that the current relay term survives until the next pass-on point), and $\Pi_{2}$ will remember the positions where all the relay terms, current and older ones, live at the given moment (we need this to make sure that they will never appear at an immortal position).

We proceed to define the function $\delta_{\mathit{cc}}$ as follows: given a state-symbol pair $(s,w)$ with $s=(\Pi_{1},\Pi_{2},q)$ and $w=(\sigma,\gamma,P)$:

• •

if $\delta_{\mathit{pos}}(\Pi_{1},w)=\emptyset$, or there exists $i\in\delta_{\mathit{pos}}(\Pi_{2},w)$ such that $\mathsf{head}(\sigma)[i]$ is not marked in ${\mathcal{T}}$, then $\delta_{\mathit{cc}}(s,w)=\mathit{reject}$;

• •

otherwise, $\delta_{cc}(s,w)=(\delta_{\mathit{pos}}(\Pi_{1},w),\delta_{\mathit{pos}}(\Pi_{2},w),\bot)$ if $P=\emptyset$, and $\delta_{\mathit{cc}}(s,w)=(P,\delta_{\mathit{pos}}(\Pi_{1},w)\cup\delta_{\mathit{pos}}(\Pi_{2},w),\top)$ if $P\neq\emptyset$.

Intuitively, this means that if we are not at a pass-on point ($P=\emptyset$), then keep track of the positions occupied by the current and the old relay terms. On the other hand, if we are at a pass-on point ($P\neq\emptyset$), then forget the positions occupied by the old relay terms and remember the positions at which the new one occurs. But do not forget them completely; simply add them to the set of positions where all the relay terms appear.

Let ${\mathcal{A}}_{\mathit{cc}}$ be a Büchi automaton with

• •

its set of states consisting of triples as described above, and the $\mathit{reject}$ state,

• •

$\Lambda_{\mathcal{T}}$ its alphabet,

• •

$\delta_{\mathit{cc}}$ its transition function,

• •

$(\Pi_{0},\emptyset,e_{0})$ its initial state, and

• •

all the states of the form $(\cdot,\cdot,\top)$ being accepting.

D.3. Proof of Lemma 6.13

Let $\diamondsuit=(L^{\diamondsuit},B^{\diamondsuit},T^{\diamondsuit},G^{\diamondsuit})$ be a free uniformly connected caterpillar, where $B^{\diamondsuit}=(\alpha_{i}^{\diamondsuit})_{i\geq 0}$, $T^{\diamondsuit}=(\sigma_{i}^{\diamondsuit},h_{i}^{\diamondsuit})_{i>0}$, and $G^{\diamondsuit}=(\gamma_{i}^{\diamondsuit})_{i>0})$. Let ${\mathfrak{c}}_{0},{\mathfrak{c}}_{1},\ldots$ be the relay terms of $\diamondsuit$. Moreover, assuming that $(b_{i})_{i>0}$ are the pass-on points of $\diamondsuit$, let $d\geq 0$ be such that $b_{k+1}-b_{k}<d$, for each $k\geq 0$. Our goal is to define a unifying function $h$ for $\diamondsuit$ such that $h(\diamondsuit)$ is a finitary caterpillar, which means that $h(L^{\diamondsuit})$ is finite.

We first observe that no matter how a unifying function $h$ for $\diamondsuit$ is defined, $h(\diamondsuit)$ is a proto-caterpillar that satisfies condition (1) of Definition 6.3. This is what the next lemma tells us:

Lemma D.4.

*Consider a unifying function $h$ for $\diamondsuit$. Then: *

1. (1)

$h(\diamondsuit)$* is a proto-caterpillar, and* 2. (2)

for each $\beta\in h(L^{\diamondsuit})$ and $i>0$, $\beta\not\prec_{s}h(\alpha_{i}^{\diamondsuit})$.

Proof.

It is clear that there is no way to violate the conditions given in Definition 6.2 by unifying terms in the legs of a proto-caterpillar. Since, by hypothesis, $\diamondsuit$ is a proto-caterpillar, we get that $h(\diamondsuit)$ is a proto-caterpillar, and (1) follows.

Concerning (2), the claim follows by the fact that none of the relay terms ${\mathfrak{c}}_{0},{\mathfrak{c}}_{1},\ldots$ of $\diamondsuit$ occurs in $L^{\diamondsuit}$. This implies that none of the terms ${\mathfrak{c}}_{0},{\mathfrak{c}}_{1},\ldots$ occurs in $h(L^{\diamondsuit})$, while, for each $i\geq 0$, $\mathsf{fr}(h(\alpha^{\diamondsuit}_{i}))$ contains a term from ${\mathfrak{c}}_{0},{\mathfrak{c}}_{1},\ldots$. Therefore, none of the atoms of $h(L^{\diamondsuit})$ can stop an atom of $(h(\alpha_{i}^{\diamondsuit}))_{i>0}$, and the claim follows.

Having the above lemma in place, it is clear that to establish Lemma 6.13 it remains to construct a unifying function $h$ for $\diamondsuit$ such that $h(L^{\diamondsuit})$ is finite, and $h(\diamondsuit)$ satisfies condition (2) of Definition 6.3. The rest of the section is devoted to constructing such a function.

We first define the domain of the desired function as the set of terms ${\mathfrak{V}}\subseteq\mathsf{dom}(L^{\diamondsuit})$ that occur at a position $(\alpha,i)$, for some atom $\alpha\in L^{\diamondsuit}$, that is not related to any immortal position $(\beta,j)$, where $\beta\in B^{\diamondsuit}$. Notice that none of the relay terms of $\diamondsuit$ occur in ${\mathfrak{V}}$. It would be useful to be able to refer to the terms of ${\mathfrak{V}}$ that participate in the generation of the atoms between the first body atom and the first pass-on point, as well as the atoms between two consecutive pass-on points. Let $B_{0}^{\diamondsuit}=\{\alpha_{j}^{\diamondsuit}:0<j\leq b_{1}\}\subseteq B^{\diamondsuit}$, that is, the set of atoms between $\alpha_{0}^{\diamondsuit}$ and the birth atom of ${\mathfrak{c}}_{1}$. Moreover, for each $i>0$, let $B_{i}^{\diamondsuit}=\{\alpha_{j}^{\diamondsuit}:b_{i}<j\leq b_{i+1}\}\subseteq B^{\diamondsuit}$, that is, the set of atoms between the birth atom of ${\mathfrak{c}}_{i}$ and the birth atom of ${\mathfrak{c}}_{i+1}$. We also define, for each $i\geq 0$, $L_{i}^{\diamondsuit}$ as the set of atoms

[TABLE]

which are essentially the atoms that are needed to generate $B_{i}^{\diamondsuit}$. Then, we let ${\mathfrak{V}}_{i}={\mathfrak{V}}\cap\mathsf{dom}(L_{i}^{\diamondsuit})$.

For the codomain we need a sufficiently large finite set of new terms. Let $m_{0}\geq 0$ be greater than the maximal number of variables in a TGD of ${\mathcal{T}}$ and $m=(d+1)\cdot m_{0}$; recall that $d$ is the uniform distance between two consecutive pass-on points of $\diamondsuit$. We define $\mathfrak{T}$, which will be the codomain of the desired function, as a set of terms such that $|\mathfrak{T}|=2m$ and $\mathfrak{T}\cap\mathsf{dom}(L^{\diamondsuit}\cup B^{\diamondsuit})=\emptyset$, i.e., $\mathfrak{T}$ collects $m$ new terms that do not occur in $L^{\diamondsuit}\cup B^{\diamondsuit}$. We can then show the following key technical lemma:

Lemma D.5.

There exists a unifying function $\hbar:{\mathfrak{V}}\rightarrow\mathfrak{T}$ such that, for each $i\geq 0$, the unifying function $\hbar_{|{\mathfrak{V}}_{i}}$ is 1-1.

Proof.

We first observe that:

1. (*)

for each $i\geq 0$, $|{\mathfrak{V}}_{i}|\leq m$ – this is a consequence of the definition of $m$; 2. (**)

for each $i>0$, ${\mathfrak{V}}_{i}\cap\bigcup_{j<i}{\mathfrak{V}}_{j}\subseteq{\mathfrak{V}}_{i-1}$ – since all the terms that occur both in $\bigcup_{j<i}{\mathfrak{V}}_{j}$ and in ${\mathfrak{V}}_{i}$ must also occur in $\alpha_{b_{i}}^{\diamondsuit}$.

We are going to build an ascending sequence $(\hbar_{i})_{i\geq 0}$ of functions, where $\hbar_{i}:\bigcup_{j\leq i}{\mathfrak{V}}_{j}\rightarrow\mathfrak{T}$, such that, for each $i\geq 0$, the function ${\hbar_{i}}_{|{\mathfrak{V}}_{i}}$ is 1-1. Then, $\hbar$ will be defined as $\bigcup_{i\geq 0}\hbar_{i}$.

Let $\hbar_{0}$ be an 1-1 function of the form ${\mathfrak{V}}_{0}\rightarrow\mathfrak{T}$. Notice that such a function exists since, by definition, $\mathfrak{T}$ is sufficiently large. Suppose now that $\hbar_{i-1}$, as specified above, has been defined. In order to define $\hbar_{i}$ we need to extend $\hbar_{i-1}$ to the terms in ${\mathfrak{V}}_{i}\setminus\bigcup_{j<i}{\mathfrak{V}}_{j}$ in such a way that the newly defined function is 1-1 on ${\mathfrak{V}}_{i}$. From (**) we know that ${\mathfrak{V}}_{i}\setminus\bigcup_{j<i}{\mathfrak{V}}_{j}={\mathfrak{V}}_{i}\setminus{\mathfrak{V}}_{i-1}$, and, by assumption, ${\hbar_{i-1}}_{|{\mathfrak{V}}_{i-1}}$ is 1-1. This means that on the subset of ${\mathfrak{V}}_{i}$ where $\hbar_{i}$ is already defined (since $\hbar_{i-1}$ is defined) it is 1-1. Now, to be able to extend it to an 1-1 function on the entire set ${\mathfrak{V}}_{i}$ we need to have enough terms in the codomain, which is guaranteed by (*).

Let $\hbar$ be the unifying function for $\diamondsuit$ provided by Lemma D.5. We proceed to show that:

Lemma D.6.

1. (1)

The instance $\hbar(L^{\diamondsuit})$ is finite. 2. (2)

For each $0\leq i<j$, $\hbar(\alpha_{i}^{\diamondsuit})\not\prec_{s}\hbar(\alpha_{j}^{\diamondsuit})$.

Proof.

For (1), since $\mathfrak{V}$ collects all the terms of $\mathsf{dom}(L^{\diamondsuit})$ that occur at a position $(\alpha,i)$, for some $\alpha\in L^{\diamondsuit}$, that is not related to any immortal position $(\beta,j)$, where $\beta\in B^{\diamondsuit}$, we can conclude that $\mathsf{dom}(L^{\diamondsuit})\setminus\mathfrak{V}$ is finite. Therefore, $\mathsf{dom}(\hbar(L^{\diamondsuit}))$ is finite, which in turn implies that $\hbar(L^{\diamondsuit})$ is finite, as needed.

For (2), we proceed by considering the following two cases:

• •

$i\leq b_{k}<j$ for some $k>0$. In this case, there exists $\ell\geq k$ such that the relay term ${\mathfrak{c}}_{\ell}$ occurs in $\mathsf{fr}(\alpha_{j}^{\diamondsuit})$ but not in $\mathsf{fr}(\alpha_{i}^{\diamondsuit})$. Since none of the relay terms of $\diamondsuit$ occurs in the domain or the codomain of $\hbar$, we conclude that ${\mathfrak{c}}_{\ell}$ occurs in $\mathsf{fr}(\hbar(\alpha_{j}^{\diamondsuit}))$ but not in $\mathsf{fr}(\hbar(\alpha_{i}^{\diamondsuit}))$, which implies that $\hbar(\alpha_{i}^{\diamondsuit})\not\prec_{s}\hbar(\alpha_{j}^{\diamondsuit})$.

• •

$b_{k}\leq i<j\leq b_{k+1}$ for some $k\geq 0$ (with $b_{0}=0$.) Since, by hypothesis, $\diamondsuit$ is a caterpillar, we get that $\alpha_{i}^{\diamondsuit}\not\prec_{s}\alpha_{j}^{\diamondsuit}$. The fact that $\hbar$ is an 1-1 function over ${\mathfrak{V}}_{k}$ allows us to conclude that $\{\alpha_{i}^{\diamondsuit},\alpha_{j}^{\diamondsuit}\}$ is isomorphic to $\{\hbar(\alpha_{i}^{\diamondsuit}),\hbar(\alpha_{j}^{\diamondsuit})\}$. Therefore, $\hbar(\alpha_{i}^{\diamondsuit})\not\prec_{s}\hbar(\alpha_{j}^{\diamondsuit})$, and the claim follows.

This completes the proof of the lemma.

By Lemma D.4 and D.6, we immediately get Lemma 6.13.