By construction of $I_{i+1}$, there is a non-unary fact $R(\bar{c})\in
I_{i+1}$ such that $I_{i+1}$ is the restriction of $I$ to ${\sf
adom}(I_{i})\cup\bar{c}$. For every $k>i$, there is thus a $u_{k}\in V$ with
$R(h_{k}(\bar{c}))\in B(u)$. In fact, each $u_{k}$ is unique by definition of
instance trees. By skipping homomorphisms from $h_{i+1},h_{i+2},\dots$ along
with the associated functions $f_{i,i+1},f_{i,i+2},\dots$ and isomorphisms
$\iota_{i,i+1},\iota_{i,i+2},\dots$, we can achieve that one of the following
two cases applies:

  1. 1.

$u_{k}$ is in the range of $f_{i,k}$ for all $k>i$, or

  2. 2.

$u_{k}$ is not in the range of $f_{i,k}$ for all $k>i$.

In Case 1, since $V_{i}$ is finite we can once more skip homomorphisms and
achieve that there is some $v\in V_{i}$ such that $f_{i,k}(v)=u_{k}$, for all
$k>i$. For every $k>i$, by Property 3 of embeddings we may define

$\bar{d}_{k}=\iota_{i,k}^{-}(h_{k}(\bar{c})).$

The choice of $v$ and Property 1 of embeddings yield $\bar{d}_{k}\subseteq{\sf
adom}(B_{i}(v))$ for all $k>i$. Since ${\sf adom}(B_{i}(v))$ is finite, there
are only finitely many possible choices for the $\bar{d}_{k}$. By skipping
homomorphism, we may thus achieve that they are all identical. Extend
$g_{i+1}$ by setting $g_{i+1}(c)=\iota_{i,k}^{-}(h_{k}(c))$ for some
(equivalently: all) $k>i$, for every $c\in\bar{c}$ such that $g_{i+1}(c)$ is
not yet defined. Define $f_{i+1,j}=f_{i,j}$ and $\iota_{i+1,j}=\iota_{i,j}$
for all $j>i$. One may verify that $(\dagger)$ is satisfied.

We argue that, as required, $g_{i+1}$ is a homomorphism from $I_{i+1}$ to
$I_{\mathcal{T}\xspace_{i+1}}$. Take any fact $S(\bar{e})\in I_{i+1}$. The
definition of $g_{i+1}$ and ($\dagger$) yield
$g_{i+1}(c)=\iota_{i,i+1}^{-}(h_{i+1}(c))$ for all $c\in\bar{e}$. It remains
to note that $h_{i+1}$ is a homomorphism from $I_{i+1}$ to
${\mathsf{chase}}_{T_{1}}(\widehat{t})$, thus
$S(h_{i+1})\in{\mathsf{chase}}_{T_{1}}(\widehat{t})$, and $\iota_{i,i+1}^{-}$
is an isomorphism.

We consider now Case 2, that is, $u_{k}$ is not in the range of $f_{i,k}$, for
all $k>i$. Now, observe that since $I_{i+1}$ is connected, there is some
$d\in\bar{c}\cap{\sf adom}(I_{i})$, and thus $g_{i}(d)$ is already defined.
Choose $v\in V_{i}$ with $g_{i}(d)\in{\sf adom}(B(v))$ and consider the
sequence

$w_{k}=f_{i,k}(v),\quad k>i.$

Since $u_{k}$ is not in the range of $f_{i,k}$, we have $u_{k}\neq w_{k}$, for
all $k$. However, $h_{k}(d)\in{\sf adom}(B(w_{k}))\cap{\sf adom}(B(u_{k}))$.
Due to Property 1 from the definition of instance trees, we can skip
homomorphisms to reach one of the following situations:

  1. (a)

$u_{k}$ is the predecessor of $w_{k}$, for all $k>i$,

  2. (b)

$u_{k}$ is a successor of $w_{k}$, for all $k>i$, or

  3. (c)

$u_{k},w_{k}$ are siblings, for all $k>i$.

In all cases, we start as follows. Similarly to the induction start, consider
the sequence

$(B_{i+1},\lambda_{i+1},\bar{d}_{i+1}),(B_{i+2},\lambda_{i+2},\bar{d}_{i+2}),\dots$

with $(B_{k},\lambda_{k},\bar{d}_{k})=(B(u_{k}),\mu(u_{k}),h_{k}(\bar{c}))$,
for all $k>i$. Since the width of $\mathcal{T}$is bounded, there are only
finitely many isomorphism types of these triples. Thus we may choose an
isomorphism type that occurs infinitely often. By skipping homomorphisms, we
can achieve that all $(B_{k},\lambda_{k},\bar{d}_{k})$ are of the same type.
We further select a triple $(B,\lambda,\bar{d})$ that is of the same
isomorphism type to be used as a bag in the tree $\mathcal{T}\xspace_{i+1}$.
We make this choice such that $g_{i}(d)\in{\sf adom}(B)$ and ${\sf
adom}(B)\setminus\\{g_{i}(d)\\}$ consists only of fresh constants, that is,
constants not used in $I_{\mathcal{T}\xspace_{i}}$. Define $\tau_{k}$ to be an
isomorphism that witnesses that $(B,\lambda,\bar{d})$ and
$(B_{k},\lambda_{k},\bar{d}_{k})$ have the same isomorphism type, for all
$k>i$.

We now extend $\mathcal{T}\xspace_{i+1},g_{i+1}$ distinguishing Cases (a)–(c).

In Case (a), let us first argue that $v$ is the root of
$\mathcal{T}\xspace_{i}$. If not, then $f_{i,k}$ maps the predecessor
$v^{\prime}$ to $u_{k}$, for all $k>i$, in contradiction to the fact that
$u_{k}$ is not in the range of $f_{i,k}$. Then, add a predecessor $v^{\prime}$
of $v$ to $\mathcal{T}\xspace_{i+1}$, set

$B_{i+1}(v^{\prime})=B,\quad\mu_{i+1}=\mu_{i+1}\cup\lambda,$

and set, for all $c\in{\sf adom}(I_{i+1})$ such that $g_{i+1}(c)$ is not yet
defined, $g_{i+1}(c)=\iota_{i+1,k}^{-}(h_{k}(c))$, for some (equivalently:
all) $k>i$. It can be verified that setting, for all $j>i$,

$\displaystyle f_{i+1,j}$
$\displaystyle=f_{i,j}\cup\\{(v^{\prime},u_{j})\\},\text{ and}$
$\displaystyle\iota_{i+1,j}$ $\displaystyle=\iota_{i,j}\cup\tau_{j}$

witnesses $(\dagger)$ for $i+1$.

In Case (b), we do exactly the same as in Case (a) with $v^{\prime}$ a fresh
_successor_ of $v$ (instead of predecessor).

In Case (c), we make a final case distinction. If $v$ has a predecessor
$v_{0}$ in $\mathcal{T}\xspace_{i}$, then proceed exactly as in Case (a), but
make $v^{\prime}$ a fresh successor of $v_{0}$. Otherwise, let
$u_{k}^{\prime}$ be the predecessor of $u_{k}$, for all $k>i$, and consider
the sequence

$(B_{i+1}^{\prime},\lambda_{i+1}^{\prime},d_{i+1}),(B_{i+2}^{\prime},\lambda_{i+2}^{\prime},d_{i+2}),\dots$

with
$(B_{k}^{\prime},\lambda_{k}^{\prime},d_{k})=(B(u_{k}^{\prime}),\mu(u_{k}^{\prime}),h_{k}(d))$,
for all $k>i$ (recall that we fixed $d$ in the beginning of Case 2). We can
again skip homomorphisms and achieve that all the
$(B_{k}^{\prime},\lambda_{k}^{\prime},d_{k})$ are of the same isomorphism
type. We further select a triple $(B^{\prime},\lambda^{\prime},d^{\prime})$
that is of the same isomorphism type to be used as a bag in the tree
$\mathcal{T}\xspace_{i+1}$. We make this choice such that $g_{i}(d)\in{\sf
adom}(B^{\prime})$ and ${\sf adom}(B^{\prime})\setminus\\{g_{i}(d)\\}$
consists only of fresh constants, that is, constants not used in
$I_{\mathcal{T}\xspace_{i}}$. Define $\tau_{k}^{\prime}$ to be an isomorphism
that witnesses that $(B^{\prime},\lambda^{\prime},d^{\prime})$ and
$(B_{k}^{\prime},\lambda_{k}^{\prime},d_{k})$ have the same isomorphism type,
for all $k>i$. Then, add a predecessor $v^{\prime}$ of $v$ and a fresh
successor $v^{\prime\prime}$ of $v^{\prime}$ to $\mathcal{T}\xspace_{i+1}$,
set

$B_{i+1}(v^{\prime})=B^{\prime},\quad
B_{i+1}(v^{\prime\prime})=B,\quad\mu_{i+1}=\mu_{i+1}\cup\lambda\cup\lambda^{\prime},$

and set, for all $c\in{\sf adom}(I_{i+1})$ such that $g_{i+1}(c)$ is not yet
defined, $g_{i+1}(c)=\iota_{i+1,k}^{-}(h_{k}(c))$, for some (equivalently:
all) $k>i$. It can be verified that setting, for all $j>i$,

$\displaystyle f_{i+1,j}$
$\displaystyle=f_{i,j}\cup\\{(v^{\prime},u_{j}^{\prime}),(v^{\prime\prime},u_{j})\\},\text{
and}$ $\displaystyle\iota_{i+1,j}$
$\displaystyle=\iota_{i,j}\cup\tau_{j}\cup\tau_{j}^{\prime}$

witnesses $(\dagger)$ for $i+1$.

This finishes the construction of the sequences
$\mathcal{T}\xspace_{0},\mathcal{T}\xspace_{1},\dots$ and $g_{0},g_{1},\dots$.
Recall that both the $\mathcal{T}\xspace_{i}$ and the $g_{i}$ are
monotonically growing and that we are interested in the limits
$\widehat{}\mathcal{T}\xspace$ and $g$ of the sequences, that is,

$\widehat{}\mathcal{T}\xspace=\left(\bigcup_{i\geq 0}V_{i},\bigcup_{i\geq
0}E_{i},\bigcup_{i\geq 0}B_{i},\bigcup_{i\geq 0}\mu_{i}\right)$

and

$g=\bigcup_{i\geq 0}g_{i}.$

Since each $g_{i}$ is a homomorphism from $I_{i}$ to
$I_{\mathcal{T}\xspace_{i}}$, it is clear that $g$ is a homomorphism from $I$
to $I_{\widehat{}\mathcal{T}\xspace}$. Moreover,
$\widehat{}\mathcal{T}\xspace$ is $\widehat{t}$-proper since each
$\mathcal{T}\xspace_{i}$ is. ∎

##  Appendix F Proofs for Section 6: Decision Procedures

We prove the decidability results from Section 6 using the characterizations
provided in that section and tree automata. More precisely, to prove the
3ExpTimeupper bounds for hom-conservativity and CQ-conservativity in Theorem
5, we show how to construct, given sets $T_{1},T_{2}$ of frontier-one TGDs and
signatures ${\Sigma_{D}}$and ${\Sigma_{Q}}$, a tree automaton
$\mathfrak{A}$such that $L(\mathfrak{A}\xspace)\neq\emptyset$ iff
$T_{1}\not\models_{{\Sigma_{D}}\xspace,{\Sigma_{Q}}\xspace}^{\textup{hom}}T_{2}$
resp.
$T_{1}\not\models_{{\Sigma_{D}}\xspace,{\Sigma_{Q}}\xspace}^{\textup{CQ}}T_{2}$.
The use of tree automata is sanctioned by the characterizations of hom-
conservativity and CQ-conservativity in terms of tree-shaped witnesses
provided by Theorem 6 and Theorem 9.

We start with giving the necessary details on tree automata.

###  F.1 Tree Automata

A _tree_ is a non-empty (and potentially infinite) set of words
$W\subseteq(\mathbbm{N}\setminus 0)^{*}$ closed under prefixes. We assume that
trees are finitely branching, that is, for every $w\in W$, the set $\\{i>0\mid
w\cdot i\in W\\}$ is finite. For $w\in(\mathbbm{N}\setminus 0)^{*}$, set
$w\cdot 0:=w$. For $w=n_{0}n_{1}\cdots n_{k}$, $k>0$, set
$w\cdot-1:=n_{0}\cdots n_{k-1}$, and call $w$ a _successor_ of $w\cdot-1$ and
$w\cdot-1$ a _predecessor_ of $w$. For an alphabet $\Theta$, a _$\Theta$
-labeled tree_ is a pair $(W,L)$ with $W$ a tree and $L:W\rightarrow\Theta$ a
node labeling function.

A _two-way alternating tree automaton ( 2ATA)_ is a tuple
$\mathfrak{A}\xspace=(Q,\Theta,q_{0},\delta,\Theta)$ where $Q$ is a finite set
of states, $\Theta$ is the input alphabet, $q_{0}\in Q$ is the initial state,
$\delta$ is a transition function, and $\Theta:Q\to\mathbb{N}$ is a priority
function. The transition function $\delta$ maps every state $q$ and input
letter $a\in\Theta$ to a positive Boolean formula $\delta(q,a)$ over the truth
constants ${\mathsf{true}}$ and ${\mathsf{false}}$ and _transition atoms_ of
the form $q$, $\Diamond^{-}q$, $\Box^{-}q$, $\Diamond q$ and $\Box q$. A
transition $q$ expresses that a copy of $\mathfrak{A}$is sent to the current
node in state $q$; $\Diamond^{-}q$ means that a copy is sent in state $q$ to
the predecessor node, which is required to exist; $\Box^{-}q$ means the same
except that the predecessor node is not required to exist; $\Diamond q$ means
that a copy of $q$ is sent to some successor and $\Box q$ means that a copy of
$q$ is sent to all successors. The semantics of 2ATAis given in terms of runs
as usual.

Let $(W,L)$ be a $\Theta$-labeled tree and
$\mathfrak{A}\xspace=(Q,\Theta,q_{0},\delta,\Omega)$ a 2ATA. A run of
$\mathfrak{A}$over $(W,L)$ is a $W\times Q$-labeled tree $(W_{r},r)$ such that
$\varepsilon\in W_{r}$, $r(\varepsilon)=(\varepsilon,q_{0})$, and for all
$y\in W_{r}$ with $r(y)=(x,q)$ and $\delta(q,V(x))=\theta$, there is an
assignment $v$ of truth values to the transition atoms in $\theta$ such that
$v$ satisfies $\theta$ and:

  * •

if $v(q^{\prime})=1$, then $r(y^{\prime})=(x,q^{\prime})$ for some successor
$y^{\prime}$ of $y$ in $W_{r}$;

  * •

if $v(\Diamond^{-}q^{\prime})=1$, then $x\neq\varepsilon$ and
$r(y^{\prime})=(x\cdot-1,q^{\prime})$ for some successor $y^{\prime}$ of $y$
in $W_{r}$;

  * •

if $v(\Box^{-}q^{\prime})=1$, then $x=\varepsilon$ or
$r(y^{\prime})=(x\cdot-1,q^{\prime})$ for some successor $y^{\prime}$ of $y$
in $W_{r}$;

  * •

if $v(\Diamond q^{\prime})=1$, then there is some $j$ and a successor
$y^{\prime}$ of $y$ in $W_{r}$ with $r(y^{\prime})=(x\cdot j,q^{\prime})$;

  * •

if $v(\Box q^{\prime})=1$, then for all successors $x^{\prime}$ of $x$, there
is a successor $y^{\prime}$ of $y$ in $W_{r}$ with
$r(y^{\prime})=(x^{\prime},q^{\prime})$.

Let $\gamma=i_{0}i_{1}\cdots$ be an infinite path in $W_{r}$ and denote, for
all $j\geq 0$, with $q_{j}$ the state such that $r(i_{j})=(x,q_{j})$. The path
$\gamma$ is accepting if the largest number $m$ such that $\Omega(q_{j})=m$
for infinitely many $j$ is even. A run $(W_{r},r)$ is accepting, if all
infinite paths in $W_{r}$ are accepting. $\mathfrak{A}$accepts a tree if
$\mathfrak{A}$has an accepting run over it. We use $L(\mathfrak{A}\xspace)$ to
denote the set of $\Theta$-labeled trees accepted by $\mathfrak{A}\xspace$.

It is not hard to show that 2ATAare closed under intersection and that the
intersection automaton can be constructed in polynomial time, see for example
(?). The _emptiness problem_ for 2ATAmeans to decide, given a 2ATA
$\mathfrak{A}$, whether $L(\mathfrak{A}\xspace)=\emptyset$. Emptiness of 2ATA
can be solved in time single exponential in the number of states and the
maximal priority, and polynomial in all other components. This was proved for
2ATAs on ranked trees in (?) and it was shown in (?) that the result carries
over to the particular version of 2ATAs used here, which run on trees of
arbitrary finite degree.

###  F.2 Upper Bound for Hom-Conservativity

To decide hom-conservativity via Theorem 6 it suffices to devise a
2ATA$\mathfrak{A}$such that

  * $(\ast_{\mathfrak{A}}\xspace)$

$\mathfrak{A}\xspace$ accepts all tree-like instances $I$ of width
$\max(k,\ell)$ that are models of $T_{1}$ and some tree-like
${\Sigma_{Q}}\xspace$-databases $D$ of width $k$ such that ${\sf
chase}_{T_{2}}(D)\not\rightarrow_{{\Sigma_{Q}}\xspace}I$, where $k$ and $\ell$
are the body and head width of $T_{1}$.

However, 2ATAs cannot run directly on tree-like databases or instances because
the potential labels of the underlying trees (the bags) may use any number of
constants and do not constitute a finite alphabet. We therefore use an
appropriate encoding of tree-like databases that reuses constants so that we
can make do with finitely many constants overall, similar to what has been
done, for example, in (?).

##### Encoding of tree-like instances.

Let $m=\max(k,\ell)$ with $k$ the body width and $\ell$ the head width of
$T_{1}$. Fix a set $\Delta$ of $2m$ constants and define $\Theta_{0}$ to be
the set of all $\Sigma\xspace$-databases $B$ with ${\sf
adom}(B)\subseteq\Delta$ and $|{\sf adom}(B)|\leq m$, where $\Sigma\xspace$ is
the union of ${\Sigma_{D}}\xspace$ and ${\mathsf{sig}}(T_{1})$, that is, all
relation symbols that occur in $T_{1}$.

Let $(W,L)$ be a $\Theta_{0}$-labeled tree. For convenience, we use $B_{w}$ to
refer to the database $L(w)$ at node $w$. For a constant $c\in\Delta$, we say
that $v,w\in W$ are _$c$ -equivalent_ if $c\in{\sf adom}(B_{u})$ for all $u$
on the unique shortest path from $v$ to $w$. Informally, this means that $c$
represents the same constant in $B_{v}$ and in $B_{w}$. In case that $c\in{\sf
adom}(B_{w})$, we use $[w]_{c}$ to denote the set of all $v$ that are
$c$-equivalent to $w$. We call $(W,L)$ _well-formed_ if it satisfies the
following counterparts of Conditions 1 and 2 of instance trees:

  1. 1′.

for every $w\in W$ and every $c\in{\sf adom}(B_{w})$, the restriction of $W$
to $[w]_{c}$ is a tree of depth at most $1$;

  2. 2′.

for every $w\in W$ and successor $v$ of $w$, ${\sf adom}(B_{w})\cap{\sf
adom}(B_{v})$ contains at most one constant.

Each well-formed $\Theta_{0}$-labeled tree $(W,L)$ _represents_ a
$\Sigma\xspace$-instance tree $\mathcal{T}\xspace_{W,L}=(V,E,B)$ as follows.
The underlying tree $(V,E)$ is the tree (described by) $W$. The active domain
of $I_{\mathcal{T}\xspace_{W,L}}$ is the set of all equivalence classes
$[w]_{c}$ with $w\in W$ and $c\in{\sf adom}(B_{w})$ and the labeling $B$ is
defined by taking

$R([w]_{c_{1}},\ldots,[w]_{c_{k}})\in B(w)\quad\text{ iff
\quad}R(c_{1},\ldots,c_{k})\in B_{w},$

for all $w\in W$ and $c\in{\sf adom}(B_{w})$. As a shorthand, we use $I_{W,L}$
to denote the instance $I_{\mathcal{T}\xspace_{W,L}}$.

Conversely, for every ${\Sigma_{D}}\xspace$-instance $I$ such that
$I=I_{\mathcal{T}}\xspace$ for a instance tree $\mathcal{T}\xspace=(V,E,B)$ of
width $m$, we can find a $\Theta_{0}$-labeled tree $(W,L)$ that represents $I$
in the sense that $I_{W,L}$ is isomorphic to $I$. Since $\Delta$ is of size
$2m$, it is possible to select a mapping $\pi:{\sf adom}(D)\to\Delta$ such
that for each $(v,w)\in E$ and each $d,e\in{\sf adom}(B(w))\cup{\sf
adom}(B(v))$, we have $\pi(d)=\pi(e)$ iff $d=e$. Define the
$\Theta_{0}$-labeled tree $(W,L)$ by setting $W=(V,E)$, and for all $w\in W$,
$B_{w}$ to the image of $B(w)$ under $\pi$. Clearly, $(W,L)$ satisfies the
desired properties.

##### Automata Constructions

We construct a 2ATA $\mathfrak{A}$that satisfies
$(\ast_{\mathfrak{A}}\xspace)$, for given
$T_{1},T_{2},{\Sigma_{D}}\xspace,{\Sigma_{Q}}\xspace$. We may assume without
loss of generality that all symbols from ${\Sigma_{D}}$and ${\Sigma_{Q}}$occur
in $T_{1}$. The desired 2ATA runs over $\Theta$-labeled trees with
$\Theta=\Theta_{0}\times\Theta_{0}\times\Theta_{1}$ where $\Theta_{0}$ is
defined as above, and $\Theta_{1}$ is the set of all mappings
$\mu:\Delta^{\prime}\to{\sf TP}(T_{2})$ for some
$\Delta^{\prime}\subseteq\Delta$ with $|\Delta^{\prime}|\leq m$. Intuitively,
the first component will represent a ${\Sigma_{D}}\xspace$-database $D$, the
second component will represent a model $I$ of $T_{1}$ and $D$, and the last
component will represent the $T_{2}$ chase of $D$, restricted to ${\sf
adom}(D)$.

For a $\Theta$-labeled tree $(W,L)$, we set
$L(w)=(L_{0}(w),L_{1}(w),L_{2}(w))$ for all $w\in W$ and thus may use
$L_{i}(w)$ to refer to the $i$-th component of the label of $w$, for
$i\in\\{0,1,2\\}$. For the sake of readability, we may use $\mu_{w}$ to denote
$L_{2}(w)$. A $\Theta$-labeled tree $(W,L)$ is called _well-typed_ if, for all
$w\in W$:

  1. 1.

the domain of $\mu_{w}$ is ${\sf adom}(L_{0}(w))$ and

  2. 2.

for every successor $v$ of $w$ and every $c\in{\sf adom}(L_{0}(w))\cap{\sf
adom}(L_{0}(v))$, we have $\mu_{w}(c)=\mu_{v}(c)$.

The desired 2ATA$\mathfrak{A}$is constructed as the intersection of the five
2ATAs
$\mathfrak{A}\xspace_{0},\mathfrak{A}\xspace_{1},\mathfrak{A}\xspace_{2},\mathfrak{A}\xspace_{3},\mathfrak{A}\xspace_{4}$
provided by the following lemma.

######  Lemma 22.

There are 2ATAs
$\mathfrak{A}\xspace_{0},\mathfrak{A}\xspace_{1},\mathfrak{A}\xspace_{2},\mathfrak{A}\xspace_{3},\mathfrak{A}\xspace_{4}$
such that:

  * –

$\mathfrak{A}\xspace_{0}$ accepts $(W,L)$ iff it is well-typed and $(W,L_{0})$
and $(W,L_{1})$ are well-formed;

  * –

$\mathfrak{A}\xspace_{1}$ accepts $(W,L)$ iff $I_{W,L_{0}}$ is a
${\Sigma_{D}}\xspace$-database of width $k$;

  * –

$\mathfrak{A}\xspace_{2}$ accepts $(W,L)$ iff $I_{W,L_{1}}$ is a model of
$I_{W,L_{0}}$ and $T_{1}$;

  * –

$\mathfrak{A}\xspace_{3}$ accepts $(W,L)$ iff for every $w\in W$ and every
$c\in{\sf adom}(L_{0}(w))$,

$\mu_{w}(c)={\sf tp}_{T_{2}}({\sf chase}_{T_{2}}(I_{W,L_{0}}),[w]_{c}).$

  * –

$\mathfrak{A}\xspace_{4}$ accepts $(W,L)$ iff
${\mathsf{chase}}_{T_{2}}(I_{W,L_{1}})\not\rightarrow I_{W,L_{1}}$.

The number of states of

  * –

$\mathfrak{A}\xspace_{0}$ is exponential in $||T_{1}||$ (and independent of
$T_{2}$);

  * –

$\mathfrak{A}\xspace_{1}$ does not depend on the input;

  * –

$\mathfrak{A}\xspace_{2}$ is exponential in $||T_{1}||$ (and independent of
$T_{2}$);

  * –

$\mathfrak{A}\xspace_{3}$ is exponential in $||T_{2}||$ (and independent of
$T_{1}$);

  * –

$\mathfrak{A}\xspace_{4}$ is double exponential in $||T_{2}||$ (and
independent of $T_{1}$).

All automata can be constructed in time triple exponential in
$||T_{1}||+||T_{2}||$ and have maximum priority one.

It can be verified that $\mathcal{A}$satisfies ($\ast_{\mathfrak{A}}\xspace$)
and thus $L(\mathfrak{A}\xspace)\neq\emptyset$ iff
$T_{1}\not\models_{{\Sigma_{D}}\xspace,{\Sigma_{Q}}\xspace}^{\textup{hom}}T_{2}$.
The rest of this section is devoted to proving Lemma 22.

#### Automaton $\mathfrak{A}\xspace_{0}$.

This automaton is straightforward to construct.

#### Automaton $\mathfrak{A}\xspace_{1}$.

This automaton simply verifies that all databases $L_{0}(w)$ use only symbols
from ${\Sigma_{D}}\xspace$ and at most $k$ constants, and that on every path
there are only finitely many non-empty databases. Constantly many states
suffice for this purpose.

#### Automaton $\mathfrak{A}\xspace_{2}$.

First note that $I_{W,L_{1}}$ is a model of $I_{W,L_{0}}$ iff $L_{0}(w)$ is a
subset of $L_{1}(w)$, for every $w\in W$. This check can easily be done by a
2ATAwith constantly many states. In order to verify that $I_{W,L_{1}}$ is a
model of $T_{1}$, it is essential to realize that the employed encoding allows
a 2ATAto do the following:

  * $(\dagger)$

given some $w\in W$ and $c\in{\sf adom}(L_{1}(w))$, and a unary CQ $q(x)$,
verify that there is a homomorphism $h$ from $q$ to $I_{W,L_{1}}$ with
$h(x)=[w]_{c}$.

Since (parts of) 2ATAs can easily be complemented by dualization, they are
also able to verify that there is no such homomorphism. The
2ATA$\mathfrak{A}\xspace_{2}$ may thus visit all $w\in W$ and all $c\in{\sf
adom}(L_{1}(w))$ and verify that, for every TGD
$\phi(x,\bar{y})\to\exists\bar{z}\,\psi(x,\bar{z})$ in $T_{1}$, there is no
homomorphism $h$ from $q_{\phi}(x)$ to $I_{W,L_{1}}$ with $h(x)=[w]_{c}$ or
there is a homomorphism $g$ from $q_{\psi}(x)$ to $I_{W,L_{1}}$ with
$g(x)=[w]_{c}$.

Informally, a 2ATAcan achieve $(\dagger)$ by memorizing (in its state) a CQ
$p$ for which it still has to check the existence of a homomorphism, plus the
target constant of the free variable of $p$ (if any). If the automaton visits
a given node $w\in W$ in such a state, it guesses the variables
$y_{1},\ldots,y_{n}$ that the homomorphism will map to ${\sf adom}(L_{1}(w))$
and also the corresponding homomorphism targets $e_{1},\ldots,e_{n}\in{\sf
adom}(L_{1}(w))$. It verifies that the guess indeed give rise to a partial
homomorphism to database $L_{1}(w)$ and proceeds with the parts of $p$ that
have not been mapped to the current database $L_{1}(w)$.

To formalize this idea, we use _instantiated CQs_ in which all answer
variables are replaced with constants, writing $q(\bar{c})$ to indicate that
$\bar{c}$ are precisely the constants that occur in $q$ and that all variables
are quantified. We will mostly drop the word ‘instantiated’ and only speak of
CQs.

Let $q(\bar{c})$ be an (instantiated) CQ. A _$\Delta$ -splitting_ of
$q(\bar{c})$ is obtained by first replacing any number of variables in
$q(\bar{c})$ with constants777Different variables may be replaced with the
same constant. from $\Delta$ and then partitioning the (atoms of the)
resulting CQ into CQs
$q_{0}(\bar{c}_{0}),q_{1}(\bar{c}_{1}),\ldots,q_{n}(\bar{c}_{n})$ such that:

  1. 1.

$q_{0}$ has no quantified variables;

  2. 2.

for all $i>0$, $\bar{c}_{i}$ is empty or a single constant from $\bar{c}_{0}$;

  3. 3.

for all $j>i>0$, $q_{i}$ and $q_{j}$ share no variables.

For a set $T$ of frontier-one TGDs, the _$\Delta$ -closure
${\mathsf{cls}}(T,\Delta)$ of $T$_ is the smallest set of CQs such that:

  * •

For every TGD $\phi(x,\bar{y})\to\exists\bar{z}\,\psi(x,\bar{z})\in T$ and
every $c\in\Delta$, the CQs $q_{\phi}(c)$ and $q_{\psi}(c)$ are contained in
${\mathsf{cls}}(T,\Delta)$;

  * •

if $q(\bar{c})\in{\mathsf{cls}}(T,\Delta)$ and
$q_{0}(\bar{c}_{0}),q_{1}(\bar{c}_{1}),\ldots,q_{n}(\bar{c}_{n})$ is a
$\Delta$-splitting of $q(\bar{c})$, then
$q_{1}(\bar{c}_{1}),\ldots,q_{k}(\bar{c}_{k})\in{\mathsf{cls}}(T,\Delta)$.

It is important to note that:

######  Lemma 23.

The cardinality of ${\mathsf{cls}}(T,\Delta)$ is bounded by $|T|\cdot
2^{m}\cdot(|\Delta|+1)^{m}$, with $m$ the maximum of body and head width of
$T$.

###### Proof.

Every query in ${\mathsf{cls}}(T,\Delta)$ can be obtained by starting with a
Boolean CQ $q()\leftarrow\exists x\,q_{\psi}(x,\bar{z})$ or
$q()\leftarrow\exists x\,q_{\phi}(x,\bar{y})$ for some TGD
$\phi(x,\bar{y})\to\exists\bar{z}\,\psi(x,\bar{z})\in T$, restricting it to
some subset of its variables, and then possibly replacing any number of
variables with constants from $\Delta$. ∎

We can now describe the 2ATAachieving $(\dagger)$ more formally. It uses all
members of ${\mathsf{cls}}(T_{1},\Delta)$ as states. If it visits $w\in W$ in
state $q(\bar{c})$, it non-deterministically chooses a ${\sf
adom}(L_{1}(w))$-splitting
$q_{0}(\bar{c}_{0}),q_{1}(\bar{c}_{1}),\ldots,q_{n}(\bar{c}_{n})$ of
$q(\bar{c})$, verifies that $q_{0}(\bar{c})$ (viewed as a database) is
contained in $L_{1}(w)$ and, for each $i$ with $1\leq i\leq n$:

  * •

if $q_{i}(\bar{c}_{i})$ is unary and $\bar{c}_{i}=c$, then the 2ATAsends a
copy in state $q_{i}(\bar{c}_{i})$ to some $v\in[w]_{c}$;

  * •

if $q_{i}(\bar{c}_{i})$ is Boolean, then the 2ATAsends a copy in state
$q_{i}(\bar{c}_{i})$ to some $v\in W$.

Using the priorities we can make sure that the process terminates, that is, at
some point the splitting takes the form of $q_{0}(\bar{c}_{0})=q(\bar{c})$.
Using Lemma 23 we can verify that $\mathfrak{A}\xspace_{2}$ uses exponentially
many states.

#### Automaton $\mathfrak{A}\xspace_{3}$.

Before we can describe the idea, we need to establish some necessary
preliminaries. A TGD
$\phi(\bar{x},\bar{y})\to\exists\bar{z}\,\psi(\bar{x},\bar{z})$ is _full_ if
$\bar{z}$ is empty. A _monadic datalog program_ is a set of full frontier-one
TGDs. In such programs, however, we also admit nullary relation symbols and
empty frontiers.

Let $T$ be a set of frontier-one TGDs. We construct from $T$ a monadic datalog
program $T^{\prime}$ as follows. Recall that all CQs in
$q\in{\mathsf{bodyCQ}}\xspace(T)$ are Boolean or unary. For every CQ
$q(\bar{x})\in{\mathsf{bodyCQ}}\xspace(T)$, introduce a relation symbol
$A_{q(\bar{x})}$ of arity $|\bar{x}|$. With ${\mathsf{bodyCQ}}\xspace^{+}(T)$,
we denote the set of (Boolean or unary) CQs that can be obtained from a CQ
$q\in{\mathsf{bodyCQ}}\xspace(T)$ by adding any number of atoms
$A_{p(\bar{x})}(\bar{y})$ with $p(\bar{x})\in{\mathsf{bodyCQ}}\xspace(T)$ and
$\bar{y}$ a tuple of variables from $q$ of length $|\bar{x}|$.

Given a CQ $q\in{\mathsf{bodyCQ}}\xspace^{+}(T)$, we denote with
$q^{\downarrow}$ the CQ obtained from $q$ by replacing every nullary atom
$A_{p(\bar{x})}$ with a copy $p^{\prime}(\bar{x})$ of $p(\bar{x})$ that uses
only fresh variable names. In addition, if $\bar{x}=x$ is non-empty, the copy
of $x$ in $p^{\prime}(\bar{x})$ is identified with $x$. Now, $T^{\prime}$
consists of all rules

  1. (i)

$q(\bar{x})\to A_{p(\bar{x})}(\bar{x})$ such that
$q(\bar{x})\in{\mathsf{bodyCQ}}\xspace^{+}(T)$ and
$p(\bar{x})\in{\mathsf{bodyCQ}}\xspace(T)$ have the same arity and
$D_{q^{\downarrow}},T\models p(\bar{x})$,

  2. (ii)

$q(x)\to A_{p(\bar{x})}(\bar{x})$ such that
$p(\bar{x})\in{\mathsf{bodyCQ}}\xspace(T)$ and $q$ is a conjunction of nullary
atoms $A_{p^{\prime}}$ and unary atoms $A_{p^{\prime}}(x)$,
$p^{\prime}\in{\mathsf{bodyCQ}}\xspace(T)$, such that
$D_{q^{\downarrow}},T\models p(\bar{x})$.

######  Lemma 24.

Let $T$ be a set of frontier-one TGDs and $T^{\prime}$ the corresponding
monadic datalog program. Then, for every database $D$,
$q(\bar{x})\in{\mathsf{bodyCQ}}\xspace(T)$, and every $\bar{c}\in{\sf
adom}(D)^{|\bar{x}|}$,

$D,T\models q(\bar{c})\quad\text{iff}\quad D,T^{\prime}\models
A_{q(\bar{x})}(\bar{c}).$

###### Proof.

For the “if”-direction, suppose that $D,T\not\models q(\bar{c})$, for some
database $D$, $q(\bar{x})\in{\mathsf{bodyCQ}}\xspace(T)$, and $\bar{c}\in{\sf
adom}(D)^{|\bar{x}|}$, that is, $\bar{c}\notin q({\sf chase}_{T}(D))$. Obtain
an instance $I$ from ${\sf chase}_{T}(D)$ by interpreting the fresh symbols
$A_{p(\bar{y})}$ in the expected way, that is, for all
$p(\bar{y})\in{\mathsf{bodyCQ}}\xspace(T)$, and $\bar{d}\in{\sf adom}({\sf
chase}_{T}(D))^{|\bar{y}|}$, we have:

$A_{p(\bar{y})}(\bar{d})\in I\quad\text{ iff }\quad\bar{d}\in p({\sf
chase}_{T}(D)).$

It is readily verified that $I$ is a model of $D$ and $T^{\prime}$. But since
$\bar{c}\notin q({\sf chase}_{T}(D))$, we have $A_{q(\bar{x})}(\bar{c})\notin
I$ and thus $D,T^{\prime}\not\models A_{q(\bar{x})}(\bar{c})$.

For the “only if”-direction, let $D,T^{\prime}\not\models
A_{q(\bar{x})}(\bar{c})$, for some database $D$,
$q(\bar{x})\in{\mathsf{bodyCQ}}\xspace(T)$, and $\bar{c}\in{\sf
adom}(D)^{|\bar{x}|}$, that is, $A_{q(\bar{x})}(\bar{c})\notin I$ for some
model $I$ of $D$ and $T^{\prime}$. We associate with every $d\in{\sf adom}(I)$
a $T$-type $t_{d}$ by taking:

$\displaystyle t_{d}=~{}{}$
$\displaystyle\\{p(x)\in{\mathsf{bodyCQ}}\xspace(T)\mid A_{p(x)}(d)\in
I\\}\cup{}$ $\displaystyle\\{p()\in{\mathsf{bodyCQ}}\xspace(T)\mid A_{p()}\in
I\\}.$

Now obtain an instance $I^{\prime}$ from $I$ by adding, for every $d\in{\sf
adom}(I)$ a disjoint copy of ${\sf chase}_{T}(t_{d})$ identifying its root
with $d$. It remains to show that $I^{\prime}$ is a model of $T$ and that
$\bar{c}\notin q(I^{\prime})$. For both statements, we will need the following
auxiliary claim.

Claim 1. For all $p(\bar{x})\in{\mathsf{bodyCQ}}\xspace(T)$ and all
$\bar{d}\in{\sf adom}(I)^{|\bar{x}|}$, we have

$\bar{d}\in p(I^{\prime})\quad\text{ iff }\quad A_{p(x)}(\bar{d})\in I.$

Proof of Claim 1. The “if”-direction is immediate from the construction of
$I^{\prime}$, so we concentrate on “only if”. The proof is by induction on the
number of variables in $p$.

Let $\bar{d}\in p(I^{\prime})$, that is, there is a homomorphism $h$ from $p$
to $I^{\prime}$ with $h(\bar{x})=\bar{d}$. Let us define $h^{\downarrow}(x)=e$
in case $h(x)$ is in the copy of ${\sf chase}_{T}(t_{e})$, for all variables
$x$ in $p$. Set $H^{\downarrow}=\\{h^{\downarrow}(x)\mid\text{ $x$ variable in
$p$}\\}$. We decompose $p$ guided by $h$ into queries $p_{0}$, $p_{e}$ with
$e\in H^{\downarrow}$ as follows:

  * •

For every $e\in H^{\downarrow}$, $p_{e}$ is the restriction of $p$ to all
variables $y$ in $p$ with $h^{\downarrow}(y)=e$.

  * •

$p_{0}$ consists of the remaining atoms and has answer variable $x$ in case
$p$ has an answer variable $x$.

Note that all obtained queries are contained in ${\mathsf{bodyCQ}}\xspace(T)$.
We distinguish three cases. Observe that Case 1 applies if $p$ contains at
most one variable and thus establishes the induction base.

Case 1: $p_{e}=p$, for some $e\in H^{\downarrow}$. If $p$ is Boolean, then
there is a homomorphism $g$ from $p$ to ${\sf chase}_{T}(t_{e})$. If $p$ has
answer variable $x$, then $\bar{d}=e$ and $g(x)$ is the constant corresponding
to the free variable of $t_{e}$. Thus, $t_{e},T\models p(\bar{x})$ and we find
in $T^{\prime}$ the rule $\widehat{q}(x)\to A_{p(\bar{x})}(\bar{x})$ where
$\widehat{q}$ is the conjunction of all $A_{p^{\prime}(x)}(x)$ with
$A_{p^{\prime}(x)}(e)\in I$ and all $A_{p^{\prime}(x)}\in I$. By definition of
$\widehat{q}$, $e\in\widehat{q}(I)$ and hence $A_{p(\bar{x})}(\bar{d})\in I$.

Case 2: $p_{0}=p$. Then $h$ witnesses that $\bar{d}\in p(I)$. Since trivially
$D_{p^{\downarrow}},T\models p(\bar{x})$, $T^{\prime}$ contains the rule
$p(\bar{x})\to A_{p(\bar{x})}(\bar{x})$. This implies that
$A_{p(\bar{x})}(\bar{d})\in I$.

Case 3: Otherwise. Then all obtained queries $p_{0}$, $p_{e}$ have less
variables than $p$. We obtain a CQ $\widehat{p}$ from $p_{0}$ by doing the
following, for every $e\in H^{\downarrow}$:

  * •

if $p_{0}$ and $p_{e}$ do not share any variable, then add the nullary atom
$A_{p_{e}}$, and

  * •

if $p_{0}$ and $p_{e}$ share a variable, then pick such a variable $x_{e}$,
make it an answer variable in $p_{e}$, and add the unary atom
$A_{p_{e}(x_{e})}(x_{e})$.

Observe that $h$ witnesses that $\bar{d}\in\widehat{p}(I)$ since $\bar{d}\in
p_{0}(I)$ and, for all $e\in H^{\downarrow}$, we have:

  * •

If $\widehat{p}$ contains $A_{p_{e}}$, then $h$ witnesses that $()\in
p_{e}(I^{\prime})$, and thus, by induction, $A_{p_{e}}\in I$.

  * •

If $\widehat{p}$ contains $A_{p_{e}(x_{e})}(x_{e})$, then $h$ witnesses that
$h(x_{e})\in p_{e}(I^{\prime})$, and thus, by induction,
$A_{p_{e}(x_{e})}(h(x_{e}))\in I$.

Moreover, it should be clear that $D_{\widehat{p}^{\downarrow}},T\models
p(\bar{x})$, and thus we find the rule $\widehat{p}(\bar{x})\to
A_{p(\bar{x})}(\bar{x})$ in $T^{\prime}$, hence $A_{p(\bar{x})}(\bar{d})\in
I$.

This finishes the proof of Claim 1. Claim 1 immediately implies that
$\vec{c}\notin q(I^{\prime})$ since $A_{q(\bar{x})}(\bar{c})\notin I$. It
remains to verify the following.

Claim 2. $I^{\prime}$ is a model of $T$.

Proof of Claim 2. To see that $I^{\prime}$ is a model of $T$ let
$\vartheta=\phi(x,\bar{y})\to\exists\bar{z}\,\psi(x,\bar{z})$ be a TGD in $T$
and suppose that $d\in q_{\phi}(I^{\prime})$, that is, there is a homomorphism
$h$ from $q_{\phi}$ to $I^{\prime}$ with $h(x)=d$. We show that $d\in
q_{\psi}(I^{\prime})$. We distinguish cases.

Case 1: $d\in{\sf adom}(I)$. In this case, Claim 1 implies that
$A_{q_{\phi}}(d)\in I$, and hence $q_{\phi}(x)\in t_{d}$. Since ${\sf
chase}_{T}(t_{d})$ is a model of both $q_{\phi}(x)$ and $\vartheta$, we have
that $x\in q_{\psi}({\sf chase}_{T}(t_{d}))$. The construction of $I^{\prime}$
ensures that $x\in q_{\psi}(I^{\prime})$.

Case 2: $d\notin{\sf adom}(I)$. Then $d$ is in the copy of ${\sf
chase}_{T}(t_{e})$, for some $e\in{\sf adom}(I)$. We obtain CQs $q_{1},q_{2}$
from $q_{\phi}$ as follows:

  * •

$q_{1}$ is the restriction of $q_{\phi}$ to all variables $y$ such that $h(y)$
is in the copy of ${\sf chase}_{T}(t_{e})$.

  * •

$q_{2}$ is obtained by starting from the remaining atoms and then identifying
all variables shared with $q_{1}$. (Note that every such variable $y$
satisfies $h(y)=e$.) If there is none such variable, then $q_{2}$ is Boolean.
Otherwise, the variable obtained in the identification process is the answer
variable.

The homomorphism $h$ witnesses that $e\in q_{2}(I^{\prime})$ if $q_{2}$ is
unary and $()\in q_{2}(I^{\prime})$ otherwise. If $q_{2}$ is unary, Claim 1
yields that $A_{q_{2}(y)}(e)\in I$ and thus $q_{2}(x)\in t_{e}$. Otherwise,
Claim 1 yields that $A_{q_{2}}\in I$ and thus $q_{2}\in t_{e}$. By definition
of ${\sf chase}_{T}(t_{e})$ we find a homomorphism $g$ from $q_{2}$ to ${\sf
chase}_{T}(t_{e})$ that maps the answer variable of $q_{2}$ (if any) to the
constant corresponding to the free variable of $t_{e}$. Let $h^{\prime}$ be
the copy of $h$ that maps $q_{1}$ to ${\sf chase}_{T}(t_{e})$ (instead of the
copy of ${\sf chase}_{T}(t_{e})$ in $I^{\prime}$). But then $g\cup h^{\prime}$
is a homomorphism from $q_{\phi}$ to ${\sf chase}_{T}(t_{e})$, and hence
$d^{\prime}\in q_{\phi}({\sf chase}_{T}(t_{e}))$ where $d^{\prime}$ is the
copy of $d$ in ${\sf chase}_{T}(t_{e})$. Since ${\sf chase}_{T}(t_{e})$ is a
model of $\vartheta$, we have $d^{\prime}\in q_{\psi}({\sf chase}_{T}(t_{e}))$
and thus $d\in q_{\psi}(I^{\prime})$. This finishes the proof of Claim 2. ∎

######  Lemma 25.

Let $T$ be a set of frontier-one TGDs of body width $k$. Then, $T^{\prime}$
consists of:

  * •

at most exponentially many rules of type (i), and

  * •

at most double exponentially many rules of type (ii).

Moreover, rules of type (i) have at most $k$ variables and rules of type (ii)
have only one variable. $T^{\prime}$ can be computed in time triple
exponential in $||T||$.

###### Proof.

First note that there are at most exponentially many queries in
${\mathsf{bodyCQ}}\xspace^{+}(T)$. Indeed, by construction, there are only
exponentially many queries in ${\mathsf{bodyCQ}}\xspace(T)$, and each query
has at most $k$ variables, $k$ the body width of $T$. These at most $k$
variables are now labeled with the fresh concept names $A_{\psi(\bar{x})}$
with $\psi(\bar{x})$ in ${\mathsf{bodyCQ}}\xspace(T)$. It follows that there
are at most exponentially many queries in ${\mathsf{bodyCQ}}\xspace^{+}(T)$.
Overall, there are at most exponentially many candidates for rules of type (i)
and at most double exponentially many candidates for rules of type (ii) in
$T^{\prime}$.

Also note that, for each query $q(\bar{x})$ that can occur in a rule body in
(i) or (ii), the query $q^{\downarrow}$ is a $T$-type, and thus of size
exponential in $||T||$. Moreover, note that the checks
$D_{q^{\downarrow}},T\models p(\bar{x})$ that have to be made in oder to
decide whether a candidate rule is included in $T^{\prime}$ are instances of
query evaluation w.r.t. frontier-one TGDs. Since query evaluation w.r.t.
frontier-one TGDs is 2ExpTime-complete (?), all these checks can be made in
triple exponential time. ∎

We are now in a position to describe the automaton $\mathfrak{A}\xspace_{3}$.
Let $T_{2}^{\prime}$ be the monadic datalog program obtained from $T_{2}$. The
automaton uses $T_{2}^{\prime}$ to verify the correctness of the labeling
$\mu_{w}$ by visiting every node $w\in W$ and doing the following for every
$c\in{\sf adom}(L_{0}(w))$ and every
$q(\bar{x})\in{\mathsf{bodyCQ}}\xspace(T_{2})$:

  1. 1.

if $q(x)\in\mu_{w}(c)$ is unary, then verify that
$I_{W,L_{0}},T_{2}\models\mathcal{A}\xspace_{q(x)}([w]_{c})$;

  2. 2.

if $q\in\mu_{w}(c)$ is Boolean, then verify that
$I_{W,L_{0}},T_{2}\models\mathcal{A}\xspace_{q}$;

  3. 3.

if $q(x)\notin\mu_{w}(c)$ is unary, then verify that
$I_{W,L_{0}},T_{2}\not\models\mathcal{A}\xspace_{q(x)}([w]_{c})$;

  4. 4.

if $q\notin\mu_{w}(c)$ is Boolean, then verify that
$I_{W,L_{0}},T_{2}\not\models\mathcal{A}\xspace_{q}$.

By Lemma 24, the automaton may use $T^{\prime}_{2}$ in place of $T_{2}$. For
Points 1 and 2, the automaton guesses a _derivation_ , as commonly used to
define the semantics of datalog; for details, we refer to (?). For Points 3
and 4, it needs to verify that there is no derivation, which is easy by
dualizing the subautomaton for Points 1 and 2. We thus concentrate on Points 1
and 2.

To verify that $I_{W,L_{0}},T_{2}^{\prime}\models A_{q(x)}([w]_{c})$ (resp.,
$I_{W,L_{0}},T_{2}^{\prime}\models A_{q}$), the automaton non-
deterministically chooses a derivation of $A_{q(\bar{x})}([w]_{c})$ (resp.,
$A_{q}$) in $I_{W,L_{0}}$ under $T_{2}^{\prime}$. For doing so, it uses states
from ${\mathsf{cls}}(T_{2}^{\prime\prime},\Delta)$ where
$T_{2}^{\prime\prime}$ is the fragment of $T_{2}^{\prime}$ consisting only of
the rules of type (i) and where ${\mathsf{cls}}$ defined as in the description
of $\mathfrak{A}\xspace_{2}$. It starts in state $A_{q(\bar{x})}(c)$ (resp.,
$A_{q}$). (Recall that in world $w$, the element $[w]_{c}$ of $I_{W,L_{0}}$ is
represented by constant $c$.)

Intuitively, if the automaton visits $w\in W$ in a state $q(\bar{c})$, then
this represents the obligation to find a derivation for $q(\widehat{c})$ in
$I_{W,L_{0}}$ under $T_{2}^{\prime}$, where $\widehat{c}=[w]_{c}$ if
$\bar{c}=c$ consists of a single constant and $\widehat{c}$ is empty
otherwise. We distinguish cases depending on the shape of $q(\bar{c})$.

Case (1) If $q(\bar{c})$ is of shape $A_{p(\bar{x})}(\bar{c})$, then the
automaton non-deterministically does one of the following:

  * •

non-deterministically choose a rule $q^{\prime}(\bar{x})\to
A_{p(\bar{x})}(\bar{x})$ of type (i) in $T_{2}^{\prime}$ and proceed in state
$q^{\prime}(\bar{c})$, or

  * •

non-deterministically choose a rule $q^{\prime}(x)\to A_{p(\bar{x})}(\bar{x})$
of type (ii) in $T_{2}^{\prime}$ and:

    * –

if $\bar{c}=c$ is a single constant, then (using alternation) the automaton
proceeds in states $A_{p^{\prime}}(c)$, for all unary atoms
$A_{p^{\prime}}(x)$ that occur in $q^{\prime}$, and in $A_{p^{\prime}}$, for
all nullary atoms $A_{p^{\prime}}$ that occur in $q^{\prime}$;

    * –

if $\bar{c}$ is empty, the automaton navigates (non-deterministically) to some
$w\in W$, picks a constant $c\in{\sf adom}(L_{0}(w))$ and proceeds as in the
previous item (again using alternation).

Case (2) If $q(\bar{c})$ is not of shape $A_{p(\bar{x})}(\bar{c})$, then the
automaton non-deterministically chooses an ${\mathsf{adom}}(B(w))$-splitting
$q_{0}(\bar{c}_{0}),q_{1}(\bar{c}_{1}),\ldots,q_{n}(\bar{c}_{n})$ of
$q(\widehat{c})$. It then obtains $q_{0}^{\prime}(\bar{c}_{0})$ from
$q_{0}(\bar{c}_{0})$ by dropping all atoms of the form $A_{p(x)}(x)$ and
$A_{p}$ and proceeds to verify that $q_{0}^{\prime}(\bar{c})$ (viewed as a
database) is contained in $L_{0}(w)$. Additionally, for each $i$ with $1\leq
i\leq n$:

  * •

if $q_{i}(\bar{c}_{i})$ is unary with $\bar{c}_{i}=c$, then the 2ATAsends a
copy in state $q_{i}(\bar{c}_{i})$ to some $v\in[w]_{c}$;

  * •

if $q_{i}(\bar{c}_{i})$ is Boolean, then the 2ATAsends a copy in state
$q_{i}(\bar{c}_{i})$ to some $v\in W$.

Finally, the dropped atoms are processed as follows.

  * •

if $A_{p}(c)$ is a unary atom in $q_{0}(\bar{c}_{0})$, the automaton sends a
copy in state $A_{p}(c)$ to $w$;

  * •

if $A_{p}$ is a Boolean atom in $q_{0}(\bar{c}_{0})$, the automaton sends a
copy in state $A_{p}$ to $w$.

Using the priorities, we can make sure that the process terminates. Combining
Lemma 23 and Lemma 25, one can verify that
${\mathsf{cls}}(T_{2}^{\prime\prime},\Delta)$ (recall that
$T_{2}^{\prime\prime}$ is the subset of $T_{2}^{\prime}$ consisting only of
rules of type (i)) contains exponentially many queries and thus
$\mathfrak{A}\xspace_{3}$ uses at most exponentially many states. By Lemma 25,
$\mathfrak{A}\xspace_{3}$ can be computed in triple exponential time.

#### Automaton $\mathfrak{A}\xspace_{4}$.

To construct automaton $\mathfrak{A}\xspace_{4}$, first note that
${\mathsf{chase}}_{T_{2}}(I_{W,L_{1}})\not\rightarrow I_{W,L_{1}}$ if for some
$w\in W$ and some $c\in{\sf adom}(L_{0}(w))$, there is no
${\Sigma_{Q}}\xspace$-homomorphism $h$ from ${\sf chase}_{T_{2}}(\mu_{w}(c))$
to $I_{W,L_{1}}$ with $h(x)=[w]_{c}$. It thus suffices to check the latter.

For convenience, we concentrate on the complement and build an automaton that
is capable of verifying that, given $w\in W$ and $c\in{\sf adom}(L_{0}(w))$,

  * $(\dagger)$

there is a ${\Sigma_{Q}}\xspace$-homomorphism $h$ from ${\sf
chase}_{T_{2}}(\mu_{w}(c))$ to $I_{W,L_{1}}$ with $h(x)=[w]_{c}$.

The automaton $\mathfrak{A}\xspace_{4}$ then non-deterministically guesses a
$w\in W$ and a $c\in{\sf adom}(L_{0}(w))$ and uses the complement/dualization
of the automaton that verifies $(\dagger)$.

We rely on the representation of ${\sf chase}_{T_{2}}(\mu_{w}(c))$ as a
(rooted!) $\mu_{w}(c)$-proper $T_{2}$-labeled instance tree
$\mathcal{T}\xspace=(V,E,B,\mu)$, see the discussion that preceeds Lemma 8. It
is important to realize that the instance $B(v)$ at some node $v\in V$
together with the labeling $\mu_{v}$ of ${\sf adom}(B(v))$ with $T_{2}$-types
completely determine the successors $v^{\prime}$ of $v$ and their labeling
$B(v^{\prime})$ and $\mu_{v^{\prime}}$. More precisely, the type $\mu(c)$ of a
constant $c\in{\sf adom}(B(v))$ determines all successors $v^{\prime}$ of $v$
that have $c$ in their domain ${\sf adom}(B(v^{\prime}))$. Moreover, $v$ has a
successor with label $B(v^{\prime}),\mu_{v^{\prime}}$ iff
$\mu_{v}(c),T_{2}\models q_{(B(v^{\prime}),\mu_{v^{\prime}})}^{c}(x)$ (c.f.
Condition 2 of properness). Since query evaluation w.r.t. frontier-one TGDs is
2ExpTime-complete (?) and the size of the input is exponential in $||T||$,
this check is possible in triple exponential time. Hence, all possible
successors can be computed in triple exponential time.

For achieving $(\dagger)$, the automaton proceeds as follows. It memorizes (in
its states) the database $B(v)$ at the current node $v\in V$ of
$\mathcal{T}\xspace$ and the type labeling $\mu_{v}$. It then guesses a
partial $\Sigma_{Q}$-homomorphism from $B(v)$ to the currently visited node
$w\in W$. Each variable that is mapped to the current state gives rise to
successors $v^{\prime}$ of $v$ with associated $B(v^{\prime})$ and
$\mu_{v^{\prime}}$ labelings, and the automaton spawns copies of itself that
generate these successor (as states), moves to neighboring nodes in the input
tree, and proceeds there. As in the encoding of $\mathcal{T}\xspace$ as a
labeled tree, it remaps the constants in the instances $B(\cdot)$ to ensure
that only finitely many states are used; this is possible since every instance
$B(v)$ is isomorphic to the head of some TGD in $T_{2}$.

More formally, the automaton uses as states pairs $\langle
q(\bar{c}),\mu\rangle$ where:

  * •

$q(\bar{c})$ is an element of ${\mathsf{cls}}(T_{2},\Delta)$, and

  * •

$\mu$ assigns a $T_{2}$-type to every variable in $q(\bar{c})$.

When the automaton visits a node $w\in W$ in state $\langle
q(\bar{c}),\mu\rangle$, this represents the obligation to verify that there is
a ${\Sigma_{Q}}\xspace$-homomorphism $h$ from $q$ to $I_{W,L_{1}}$ such that:

  * •

for every constant $c\in\bar{c}$, $h(c)=[w]_{c}$, and

  * •

for every variable $x$ in $q$, there is a ${\Sigma_{Q}}\xspace$-homomorphism
$g$ from ${\sf chase}_{T_{2}}(\mu(x))$ to $I_{W,L_{1}}$ with $g(x)=h(x)$.

For doing so, the automaton non-deterministically chooses an
${\mathsf{adom}}(B(w))$-splitting
$q_{0}(\bar{c}_{0}),\ldots,q_{n}(\bar{c}_{n})$ of $q(\bar{c})$ and proceeds as
follows:

  * •

it verifies that the ${\Sigma_{Q}}\xspace$-restriction of $q_{0}(\bar{c}_{0})$
is a subset of $L_{1}(w)$;

  * •

for every $i$ with $1\leq i\leq n$, we let $\mu_{i}$ be the restriction of
$\mu$ to the variables in $q_{i}$, then

    * –

if $q_{i}(\bar{c}_{i})$ is unary with $\bar{c}_{i}=c$, then the 2ATAsends a
copy in state $\langle q_{i}(\bar{c}_{i}),\mu_{i}\rangle$ to some
$v\in[w]_{c}$.

    * –

if $q_{i}(\bar{c}_{i})$ is Boolean, then the 2ATAsends a copy in state
$\langle q_{i}(\bar{c}_{i}),\mu_{i}\rangle$ to some $v\in W$.

  * •

for every variable $x$ in $q$ that was replaced by a constant $d$ in the
splitting, consider any node $v$ in $\mathcal{T}$and any
$e\in{\mathsf{adom}}(B(v))$ with $\mu_{v}(e)=\mu(x)$,888Choosing different $v$
and $e$ leads to exactly the same result provided that $\mu_{v}(e)=\mu(x)$.
and all successors $v^{\prime}$ of $v$ with
${\mathsf{adom}}(B(v))\cap{\mathsf{adom}}(B(v^{\prime}))\subseteq\\{e\\}$. Let
$q^{\prime}$ be $B(v^{\prime})$ viewed as a CQ which is Boolean with $e$
viewed as the answer variable if $e\in{\mathsf{adom}}(B(v^{\prime}))$ and
Boolean otherwise. Further let $\mu^{\prime}=\mu_{v^{\prime}}$. The automaton
does the following:

    * –

if $q^{\prime}$ is unary, then it sends a copy in state $\langle
q^{\prime}(d),\mu^{\prime}\rangle$ to some $w^{\prime}\in[w]_{d}$;

    * –

if $q^{\prime}$ is Boolean, then it sends a copy in state $\langle
q^{\prime},\mu^{\prime}\rangle$ to some $w^{\prime}\in W$.

Overall, one can verify that the number of states is at most double
exponential in $||T_{2}||$. There are doubly exponentially many types and, by
Lemma 23, the size of ${\mathsf{cls}}(T_{2},\Delta)$ is bounded exponentially
in the size of $||T_{2}||$. Since all queries in
${\mathsf{cls}}(T_{2},\Delta)$ have at most $||T_{2}||$ variables, the triple
exponential bound follows. As argued, the automaton can be computed in time
triple exponential in $||T_{2}||$.

###  F.3 Upper Bounds for CQ-Conservativity

We actually work with a refinement of the characterization given in Theorem 9;
its proof is based on Lemma 7. The formulation of this refinement is somewhat
more technical than the formulation of Theorem 9, and in fact we decided to go
in these two steps for didactic reasons.

######  Theorem 11.

Let $T_{1}$ and $T_{2}$ be sets of frontier-one TGDs, ${\Sigma_{D}}\xspace$
and ${\Sigma_{Q}}\xspace$ schemas, and $k$ the body width of $T_{1}$. Then
$T_{1}\models^{\text{CQ}}_{{\Sigma_{D}}\xspace,{\Sigma_{Q}}\xspace}T_{2}$ iff
for all tree-like ${\Sigma_{D}}\xspace$-databases $D$ of width at most $k$ and
all tree-like models $I$ of $T_{1}$ and $D$ of width $\max(k,\ell)$, the
following holds:

  1. 1.

${\sf chase}_{T_{2}}(D)|^{\sf
con}_{{\Sigma_{Q}}\xspace}\rightarrow_{{\Sigma_{Q}}\xspace}I$;

  2. 2.

for every labeled ${\Sigma_{Q}}\xspace$-head fragment $A=(F,\mu)$ of $T_{2}$
with ${\sf chase}_{T_{2}}(D)\models q_{A}$, one of the following holds:

    1. (a)

${\sf chase}_{T_{2}}(D_{A})|^{\sf
con}_{{\Sigma_{Q}}\xspace}\rightarrow_{{\Sigma_{Q}}\xspace}I$;

    2. (b)

${\sf chase}_{T_{2}}(D_{A})|^{\sf con}_{{\Sigma_{Q}}\xspace}\rightarrow^{{\sf
lim}}_{{\Sigma_{Q}}\xspace}{\sf chase}_{T_{1}}({\sf tp}_{T_{1}}(I,c))$ for
some $c\in{\sf adom}(D)$.

_Proof._ It suffices to show that for every tree-like
${\Sigma_{D}}\xspace$-database $D$ of width $k$, Conditions 1 and 2 of Theorem
9 are satisfied if and only if for all tree-like models $I$ of $T_{1}$ and $D$
of width $\max(k,\ell)$, Conditions 1 and 2 above are satisfied.

First assume that for all tree-like models $I$ of $T_{1}$ and $D$ of width
$\max(k,\ell)$, Conditions 1 and 2 above are satisfied. Since
${\mathsf{chase}}_{T_{1}}(D)$ is such a model, Condition 1 of Theorem 9 is
also satisfied. Now for Condition 2. By Lemma 7, for all maximally
${\Sigma_{Q}}$-connected components $J$ of ${\sf
chase}_{T_{2}}(D)\setminus{\sf chase}_{T_{2}}(D)|^{\sf
con}_{\Sigma_{Q}}\xspace$, Condition 2(a) or 2(b) above is satisfied when
${\sf chase}_{T_{2}}(D_{A})|^{\sf con}_{{\Sigma_{Q}}\xspace}$ is replaced by
$J$. In the former case, also Condition 2(a) of Theorem 9 is satisfied. In the
latter case, it follows that $J\rightarrow^{{\sf
lim}}_{{\Sigma_{Q}}\xspace}{\sf chase}_{T_{1}}(D)$. One can then show exactly
as in the proof of Theorem 9 that either Condition 2(a) or 2(b) of that
theorem is satisfied.

Conversely, suppose that Conditions 1 and 2 of Theorem 9 are satisfied for
$D$. Since ${\mathsf{chase}}_{T_{1}}(D)\rightarrow I$ for every model $I$ of
$T_{1}$ and $D$, Condition 1 of Theorem 9 implies that for all tree-like
models $I$ of $T_{1}$ and $D$ of width $\max(k,\ell)$, Condition 1 above is
satisfied. It remains to argue that Condition 2 above is satisfied. Assume to
the contrary that is is not. Then there is some tree-like model $I$ of $T_{1}$
and $D$ of width $\max(k,\ell)$ and some labeled ${\Sigma_{Q}}\xspace$-head
fragment $A=(F,\mu)$ of $T_{2}$ such that both 2(a) and 2(b) above are
violated. Since ${\mathsf{chase}}_{T_{1}}(D)\rightarrow I$, these conditions
are still violated when $I$ is replaced by ${\mathsf{chase}}_{T_{1}}(D)$.

We distinguish the following cases:

  * •

${\sf chase}_{T_{2}}(D_{A})|^{\sf con}_{{\Sigma_{Q}}\xspace}\not\to{\sf
chase}_{T_{2}}(D)|^{\sf con}_{{\Sigma_{Q}}\xspace}$.

Then ${\sf chase}_{T_{2}}(D_{A})|^{\sf con}_{{\Sigma_{Q}}\xspace}$ is an
induced subinstance of a maximally ${\Sigma_{Q}}\xspace$-connected component
$I$ of ${\sf chase}_{T_{2}}(D)\setminus{\sf chase}_{T_{2}}(D)|^{\sf
con}_{{\Sigma_{Q}}\xspace}$. Thus, ${\sf chase}_{T_{2}}(D_{A})|^{\sf
con}_{{\Sigma_{Q}}\xspace}\not\to_{{\Sigma_{Q}}\xspace}{\sf chase}_{T_{1}}(D)$
implies $I\not\to_{{\Sigma_{Q}}\xspace}{\sf chase}_{T_{1}}(D)$ and Condition
2(a) of Theorem 9 is not satisfied. Moreover, ${\sf
chase}_{T_{2}}(D_{A})|^{\sf con}_{{\Sigma_{Q}}\xspace}\not\to^{\sf
lim}_{{\Sigma_{Q}}\xspace}{\sf chase}_{T_{1}}({\sf tp}_{T_{1}}({\sf
chase}_{T_{1}}(D),c))$ for all $c\in{\sf adom}(D)$ implies $I\not\to^{\sf
lim}_{{\Sigma_{Q}}\xspace}{\sf chase}_{T_{1}}(D)|^{\downarrow}_{c}$, for all
$c\in{\sf adom}(D)$. This is because ${\sf chase}_{T_{2}}(D_{A})|^{\sf
con}_{{\Sigma_{Q}}\xspace}$ is a subinstance of $I$ and, due to Lemma 6, ${\sf
chase}_{T_{1}}(D)|^{\downarrow}_{c}$ is a subinstance of ${\sf
chase}_{T_{1}}({\sf tp}_{T_{1}}({\sf chase}_{T_{1}}(D),c))$. Thus, both
Condition 2(a) and 2(b) of Theorem 9 are violated, a contradiction.

  * •

${\sf chase}_{T_{2}}(D_{A})|^{\sf con}_{{\Sigma_{Q}}\xspace}\to{\sf
chase}_{T_{2}}(D)|^{\sf con}_{{\Sigma_{Q}}\xspace}$.

Then ${\sf chase}_{T_{2}}(D_{A})|^{\sf
con}_{{\Sigma_{Q}}\xspace}\not\rightarrow_{{\Sigma_{Q}}\xspace}{\sf
chase}_{T_{1}}(D)$ implies ${\sf chase}_{T_{2}}(D)|^{\sf
con}_{{\Sigma_{Q}}\xspace}\not\rightarrow_{{\Sigma_{Q}}\xspace}{\sf
chase}_{T_{1}}(D)$. Hence, Condition 1 of Theorem 9 is not satisfied, which is
again a contradiction. $\Box$

Let $T_{1},T_{2},{\Sigma_{D}}\xspace,{\Sigma_{Q}}\xspace$ be given. We may
again assume without loss of generality that all symbols from
${\Sigma_{D}}$and ${\Sigma_{Q}}$occur in $T_{1}$. Let $k$ and $\ell$ be the
body and head width of $T_{1}$. It suffices to devise a 2ATA$\mathfrak{B}$such
that

  * $(\ast_{\mathfrak{B}}\xspace)$

$\mathfrak{B}\xspace$ accepts all tree-like instances $I$ of width
$\max(k,\ell)$ that are a model of $T_{1}$ and of some tree-like
${\Sigma_{Q}}\xspace$-database $D$ of width $k$ such that Condition 1 and
Condition 2 of Theorem 11 are violated.

In order to represent tree-like instances of bounded width as the input to
2ATAs, we use exactly the same encoding of infinite instances as for hom-
conservativity, and in fact, the constructed automata run over the same
alphabet $\Theta=\Theta_{0}\times\Theta_{0}\times\Theta_{1}$. Recall that an
input tree over this alphabet represents a ${\Sigma_{D}}\xspace$-database $D$
in the first component, a model $I$ of $T_{1}$ and $D$ in the second
component, and the chase of $D$ with $T_{2}$, restricted to ${\sf adom}(D)$,
in the last component.

The desired 2ATA$\mathfrak{B}$is constructed as the intersection of 2ATAs
$\mathfrak{B}\xspace_{0},\mathfrak{B}\xspace_{1},\mathfrak{B}\xspace_{2},\mathfrak{B}\xspace_{3}$,
and $\mathfrak{B}$’ where $\mathfrak{B}$’ in turn is the union of 2ATAs
$\mathfrak{B}\xspace_{4}$ and $\mathfrak{B}\xspace_{5}$, all of them provided
by the following lemma.

######  Lemma 26.

There are 2ATAs
$\mathfrak{B}\xspace_{0},\mathfrak{B}\xspace_{1},\mathfrak{B}\xspace_{2},\mathfrak{B}\xspace_{3},\mathfrak{B}\xspace_{4}$
such that:

  * –

$\mathfrak{B}\xspace_{0}$ accepts $(W,L)$ iff it is well-typed and $(W,L_{0})$
and $(W,L_{1})$ are well-formed;

  * –

$\mathfrak{B}\xspace_{1}$ accepts $(W,L)$ iff $I_{W,L_{0}}$ is a
${\Sigma_{D}}\xspace$-database of width $k$;

  * –

$\mathfrak{B}\xspace_{2}$ accepts $(W,L)$ iff $I_{W,L_{1}}$ is a model of
$I_{W,L_{0}}$ and $T_{1}$;

  * –

$\mathfrak{B}\xspace_{3}$ accepts $(W,L)$ iff for every $w\in W$ and every
$c\in{\sf adom}(L_{0}(w))$,

$\mu_{w}(c)={\sf tp}_{T_{2}}({\sf chase}_{T_{2}}(I_{W,L_{0}}),[w]_{c}).$

  * –

$\mathfrak{B}\xspace_{4}$ accepts $(W,L)$ iff Condition 1 of Theorem 11 is
violated; with ‘$I$’ replaced with ‘$I_{W,L_{1}}$’ is violated;

  * –

$\mathfrak{B}\xspace_{5}$ accepts $(W,L)$ iff Condition 2 of Theorem 11 with
‘$I$’ and ‘$D$’ replaced with ‘$I_{W,L_{1}}$’ and ‘$I_{W,L_{0}}$’,
respectively, is violated;

The number of states

  * –

of $\mathfrak{B}\xspace_{0}$ is exponential in $||T_{1}||$ (and independent of
$T_{2}$);

  * –

of $\mathfrak{B}\xspace_{1}$ does not depend on the input;

  * –

of $\mathfrak{B}\xspace_{2}$ is exponential in $||T_{1}||$ (and independent of
$T_{2}$);

  * –

of $\mathfrak{B}\xspace_{3}$ is exponential in $||T_{2}||$ (and independent of
$T_{1}$);

  * –

of $\mathfrak{B}\xspace_{4}$ is exponential in $||T_{2}||$ (and independent of
$T_{1}$);

  * –

of $\mathfrak{B}\xspace_{5}$ is double exponential in both $||T_{1}||$ and
$||T_{2}||$.

All automata can be constructed in time triple exponential in
$||T_{1}||+||T_{2}||$ and have maximum priority one.

It can be verified that $\mathfrak{B}$satisfies ($\ast_{\mathfrak{B}}\xspace$)
and thus $L(\mathfrak{B}\xspace)\neq\emptyset$ iff
$T_{1}\not\models_{{\Sigma_{D}}\xspace,{\Sigma_{Q}}\xspace}^{\textup{CQ}}T_{2}$.
The rest of this section is devoted to proving Lemma 26. Automata
$\mathfrak{B}\xspace_{0},\mathfrak{B}\xspace_{1},\mathfrak{B}\xspace_{2},\mathfrak{B}\xspace_{3}$
are exactly as
$\mathfrak{A}\xspace_{0},\mathfrak{A}\xspace_{1},\mathfrak{A}\xspace_{2},\mathfrak{A}\xspace_{3}$
in Lemma 22, so we concentrate on $\mathfrak{B}\xspace_{4}$ and
$\mathfrak{B}\xspace_{5}$.

#### Automaton $\mathfrak{B}\xspace_{4}$.

The task of $\mathfrak{B}\xspace_{4}$ is to verify ${\sf
chase}_{T_{2}}(I_{W,L_{0}})|^{\sf
con}_{{\Sigma_{Q}}\xspace}\not\rightarrow_{{\Sigma_{Q}}\xspace}I_{W,L_{1}}$.
Note that this is very similar to what is achieved by automaton
$\mathfrak{A}\xspace_{4}$ from Lemma 22, which verifies that ${\sf
chase}_{T_{2}}(I_{W,L_{0}})\not\rightarrow_{{\Sigma_{Q}}\xspace}I_{W,L_{1}}$.
In fact, it can be solved using essentially the same construction and thus has
the same size and can be computed in the same time as
$\mathfrak{A}\xspace_{4}$. More precisely, the gist of the construction of
$\mathfrak{A}\xspace_{4}$ is to find an automaton that verifies, given $w\in
W$ and $c\in{\sf adom}(L_{0}(w))$, that there is a
${\Sigma_{Q}}\xspace$-homomorphism $h$ from ${\sf chase}_{T_{2}}(\mu_{w}(c))$
to $I_{W,L_{1}}$ with $h(x)=[w]_{c}$. This is done by constructing ${\sf
chase}_{T_{2}}(\mu_{w}(c))$ ‘in the states’. $\mathfrak{B}\xspace_{4}$ does
exactly the same, but disregards $\Sigma_{Q}$-disconnected parts of ${\sf
chase}_{T_{2}}(\mu_{w}(c))$.

#### Automaton $\mathfrak{B}\xspace_{5}$.

The task of $\mathfrak{B}\xspace_{5}$ is to verify that for all
${\Sigma_{Q}}\xspace$-labeled head fragments $A=(F,\mu)$ of $T_{2}$ such that
${\sf chase}_{T_{2}}(I_{W,L_{0}})\models q_{A}$, the following hold:

  1. 1.

${\sf chase}_{T_{2}}(D_{A})|^{\sf
con}_{{\Sigma_{Q}}\xspace}\not\rightarrow_{{\Sigma_{Q}}\xspace}I_{W,L_{1}}$;

  2. 2.

${\sf chase}_{T_{2}}(D_{A})|^{\sf
con}_{{\Sigma_{Q}}\xspace}\not\rightarrow^{{\sf
lim}}_{{\Sigma_{Q}}\xspace}{\sf
chase}_{T_{1}}({\mathsf{tp}}_{T_{1}}(I_{W,L_{0}},[w]_{c}))$ for all
$[w]_{c}\in{\sf adom}(I_{W,L_{0}})$.

Note that the condition ${\sf chase}_{T_{2}}(I_{W,L_{0}})\models q_{A}$ is
satisfied iff for some $[w]_{c}\in{\sf adom}(I_{W,L_{0}})$, the type $t={\sf
tp}_{T_{2}}({\sf chase}_{T_{2}}(I_{W,L_{0}},[w]_{c}))$ satisfies
$t,T_{2}\models q_{A}$. Since we are considering the intersection with
$\mathfrak{B}\xspace_{3}$, we can assume that $\mu_{w}(c)={\sf
tp}_{T_{2}}({\sf chase}_{T_{2}}(I_{W,L_{0}},[w]_{c}))$ and thus, the latter
condition is satisfied iff $\mu_{w}(c),T_{2}\models q_{A}$ for some $w\in W$
and $c\in{\sf adom}(L_{0}(w))$.

Thus, the automaton can identify all relevant labeled
${\Sigma_{Q}}\xspace$-head fragments $A=(F,\mu)$ of $T_{2}$ by visiting all
$w\in W$, all $c\in{\sf adom}(L_{0}(w))$, and testing for each whether
$\mu_{w}(c),T_{2}\models q_{A}$ is satisfied. The result of all possible such
tests can be computed in time triple exponential in $||T_{2}||$ already during
the construction of $\mathfrak{B}\xspace_{5}$, since query evaluation w.r.t.
frontier-one TGDs is 2ExpTime-complete (?).

If the test $\mu_{w}(c),T_{2}\models q_{A}$ is succesfull, the automaton has
to verify Points 1 and 2 above for ${\sf chase}_{T_{2}}(D_{A})|^{\sf
con}_{{\Sigma_{Q}}\xspace}$. There is once more a lot of similarity between
Point 1 and what is achieved by automaton $\mathfrak{A}\xspace_{4}$ from Lemma
22. Constructing an automaton that verifies Point 1 is thus another variation
of the construction of $\mathfrak{A}\xspace_{4}$, the main difference being
that instead of chasing a single type we chase $D_{A}$ with $T_{2}$ in the
states of the automaton. In particular, the automaton starts in state $\langle
q_{F},\mu\rangle$ (note that $q_{F}\in{\mathsf{cls}}(T_{2},\Delta)$).

For Point 2, we invoke Theorem 10 for every labeled ${\Sigma_{Q}}\xspace$-head
fragment $A=(F,\mu)$ of $T_{2}$ identified above. The automaton memorizes $A$
in its states and visits (again) all $w\in W$, and all $c\in{\sf
adom}(I_{W,L_{0}})$ in order to verify that

${\sf chase}_{T_{2}}(D_{A})|^{\sf
con}_{{\Sigma_{Q}}\xspace}\not\rightarrow^{{\sf
lim}}_{{\Sigma_{Q}}\xspace}{\sf chase}_{T_{1}}({\sf
tp}_{T_{1}}(I_{W,L_{1}},[w]_{c})).$

Recall that these tests have been precomputed via Theorem 10. Hence, all the
automaton has to do at this point is to guess999Recall that the $T_{1}$-type
is not represented in the input. the $T_{1}$-type $t$ of $[w]_{c}$ in
$I_{W,L_{1}}$, verify that it is the correct type using the monadic datalog
rewriting $T_{1}^{\prime}$ of $T_{1}$ as in automaton
$\mathfrak{A}\xspace_{3}$ of Lemma 22, and lookup the result of ${\sf
chase}_{T_{2}}(D_{A})|^{\sf con}_{\Sigma_{Q}}\xspace\rightarrow^{{\sf
lim}}_{{\Sigma_{Q}}\xspace}{\sf chase}_{T_{1}}(t)$ in the precomputated table.

Overall, the resulting automaton is of size double exponential in both
$||T_{2}||$ (for Point 1) and $||T_{1}||$ (for guessing a $T_{1}$-type and
verifying it in Point 2). It can be computed in triple exponential time. In
particular, the computation of the lookup table for Point 2 is possible in
triple exponential time, by Theorem 10.

###  F.4 Proof of Theorem 10

We prove Theorem 10 via the characterization of bounded homomorphisms in terms
of standard (unbounded) homomorphisms given by Lemma 8. Let two sets of
frontier-one TGDs $T_{1},T_{2}$, a schema $\Sigma$, a labeled $\Sigma$-head
fragment $A=(D,\mu)$ of $T_{2}$, and a $T_{1}$-type $\widehat{t}$ be given. It
suffices to devise a 2ATA$\mathfrak{C}\xspace$ such that:

  * $(\ast_{\mathfrak{C}}\xspace)$

$\mathfrak{C}$accepts all encodings of $\widehat{t}$-proper $T_{1}$-labeled
instance trees $\mathcal{T}\xspace$ of width $m$ such that ${\sf
chase}_{T_{2}}(D_{A})|_{\Sigma}^{\sf con}\to I_{\mathcal{T}}\xspace$.

Here we need to work with possibly non-rooted instance trees, and thus we
slightly modify our encoding of instance trees as input to the 2ATA. The input
alphabet is
$\Theta^{\prime}=\Theta_{0}\times\\{0,1\\}\times\Theta_{1}^{\prime}$ where
$\Theta_{0}$ is defined as above and $\Theta^{\prime}_{1}$ is the set of all
mappings $\mu:\Delta^{\prime}\to{\sf TP}(T_{1})$ for some
$\Delta^{\prime}\subseteq\Delta$ with $|\Delta^{\prime}|\leq m$. Note that, in
contrast to the alphabet $\Theta_{1}$ employed before, here we use
$T_{1}$-types in place of $T_{2}$-types. For a $\Theta^{\prime}$-labeled tree
$(W,L)$ and $w\in W$ with $L(w)=(B,i,\mu)$, we use $L_{0}(w)$ to denote $B$,
$i_{w}$ to denote $i$, and $\mu_{w}$ to denote $\mu$. Our aim is that every
$\Theta^{\prime}$-labeled tree $(W,L)$ represents a $T_{1}$-labeled instance
tree $\mathcal{T}\xspace=(V,E,B,\mu)$ where the $(V,E,B)$-part is represented
by $(W,L_{0})$ as before and the $\mu$-part is represented by $(W,\mu_{w})$.

The additional labeling with the 0/1-marker $i_{w}$ is necessary because
$T_{1}$-labeled instance trees need not have a root and thus may contain an
infinite predecessor path. This path will be represented as a _downward_ path
in the (rooted!) $\Theta^{\prime}$-labeled trees, but marked with a 1-marker
for identification purposes.

A $\Theta^{\prime}$-labeled tree $(W,L)$ is _well-typed_ if, for all $w\in W$,
the domain of $\mu_{w}$ is ${\sf adom}(L(w))$, and for all successors $v$ of
$w$, and all $d\in{\sf adom}(L_{0}(w))\cap{\sf adom}(L_{0}(v))$, we have
$\mu_{w}(d)=\mu_{v}(d)$. It is _well-formed_ if $(W,L_{0})$ satisfies the two
conditions of well-formedness for $\Theta_{0}$-labeled trees from the automata
constructions above plus the following additional condition:

  * •

there is a finite or infinite (and non-empty) path
$\Pi=w_{0},w_{1},w_{2},\ldots$ in $W$ that starts at the root such that all
nodes $w\in W$ with $i_{w}=1$ lie on this path.

Every well-typed and well-formed $\Theta^{\prime}$-labeled tree $(W,L)$ gives
rise to a $\Sigma\xspace$-instance tree $(V,E,B)$ and an associated instance
$I_{W,L}$ as follows.

  * •

the set of nodes $V$ is $W$;

  * •

the set of edges $E$ is defined as follows:

    * –

if $w^{\prime}$ is a successor of $w$ and $i_{w^{\prime}}=0$, then
$(w,w^{\prime})\in E$;

    * –

if $w^{\prime}$ is a successor of $w$ and $i_{w^{\prime}}=1$, then (both
$w,w^{\prime}$ lie on the path $\Pi$) and $(w^{\prime},w)\in E$.

That is, the successor relation on the path $\Pi$ becomes the predecessor
relation; the remaining successor relations stay the same. The definition of
the labeling $B$ and consequently also of $I_{W,L}$ is exactly as in the
preceeding encoding. Setting $\mu=\bigcup_{w\in W}\mu_{w}$, this extends to a
$T_{1}$-labeled instance tree $\mathcal{T}\xspace_{W,L}=(V,E,B,\mu)$.

Conversely, for every $T_{1}$-labeled instance tree
$\mathcal{T}\xspace=(V,E,B,\mu)$ of width at most $m$, we can find a
$\Theta^{\prime}$-labeled tree $(W,L)$ that represents $\mathcal{T}\xspace$ in
the sense that $\mathcal{T}\xspace_{W,L}$ is isomorphic to
$\mathcal{T}\xspace$. Since $\Delta$ is of size $2m$, it is possible to select
a mapping $\pi:{\sf adom}(I_{\mathcal{T}}\xspace)\to\Delta$ such that for each
edge $(v,w)\in E$ and all constants $c,c^{\prime}\in{\sf adom}(B(w))\cup{\sf
adom}(B(v))$, we have $\pi(c)=\pi(c^{\prime})$ iff $c=c^{\prime}$. Define the
$\Theta^{\prime}$-labeled tree $(W,L)$ as follows:

  * •

If $(V,E)$ has a root, then $W=(V,E)$. Otherwise, there is an infinite path
$v_{0},v_{1},\ldots$ in $(V,E)$ such that $v_{i+1}$ is a predecessor of
$v_{i}$, for all $i\geq 0$. We make this path the infinite _successor_ path
$\Pi$ starting from $v_{0}$ (and leave all other successor relations
untouched).

  * •

For all $w\in W$, $L(w)=(B(w),0,\mu_{w})$ if $w\notin\Pi$ and
$B_{w}=(B(w),1,\mu_{w})$, if $w\in\Pi$.

Clearly, $(W,L)$ satisfies the desired properties.

The automaton $\mathfrak{C}\xspace$ is the intersection of the three 2ATAs
$\mathfrak{C}\xspace_{0},\mathfrak{C}\xspace_{1},\mathfrak{C}\xspace_{2}$
provided by the following lemma.

######  Lemma 27.

There are 2ATAs
$\mathfrak{C}\xspace_{0},\mathfrak{C}\xspace_{1},\mathfrak{C}\xspace_{2}$ such
that:

  * –

$\mathfrak{C}\xspace_{0}$ accepts $(W,L)$ iff $(W,L)$ is well-typed and well-
formed;

  * –

$\mathfrak{C}\xspace_{1}$ accepts $(W,L)$ iff the $T_{1}$-labeled instance
tree $\mathcal{T}\xspace_{W,L}$ is $\widehat{t}$-proper;

  * –

$\mathfrak{C}\xspace_{2}$ accepts $(W,L)$ iff ${\sf
chase}_{T_{2}}(D_{2})|_{\Sigma}^{\sf con}\to I_{W,L}$.

The number of states of

  * –

$\mathfrak{C}\xspace_{0}$ is exponential in $||T_{1}||$ (and independent of
$T_{2}$);

  * –

$\mathfrak{C}\xspace_{1}$ is linear in $||T_{1}||$ (and independent of
$T_{2}$);

  * –

$\mathfrak{C}\xspace_{2}$ is double exponential in $||T_{2}||$ (and
independent of $T_{1}$).

All automata can be constructed in time triple exponential in
$||T_{1}||+||T_{2}||$ and have maximum priority one.

It can be verified that $\mathfrak{C}$satisfies
$(\ast_{\mathfrak{C}}\xspace)$, and thus $L(\mathfrak{C}\xspace)\neq\emptyset$
iff there is some $\widehat{t}$-proper $T_{1}$-labeled instance tree
$\mathcal{T}\xspace$ with ${\sf chase}_{T_{2}}(D_{A})|_{\Sigma}^{\sf con}\to
I_{\mathcal{T}}\xspace$. The automaton $\mathfrak{C}\xspace_{0}$ is
straightforward.

#### Automaton $\mathfrak{C}\xspace_{1}$.

The automaton simply visits every node $w\in W$ in the input tree $(W,L)$ and
verifies locally at each node that Conditions 1 and 2 of properness are
satisfied. For Condition 1, we have to check whether the labeling $L_{1}(w)$
of the current node $w$ satisfies Condition 1 of Properness. Condition 1(a) is
a simple lookup and for Condition 1(b), one has to decide (during the
construction of the automaton) whether $\widehat{t},T_{1}\models
q_{(B(v),\mu_{v})}$ for all possible labelings $(B(v),\mu(v))$. This is
possible in time triple exponential in $||T_{1}||$, since query evaluation
w.r.t. frontier-one TGDs is 2ExpTime-complete (?). For Condition 2 of
properness, the automaton needs to memorize the constant $c$ (if any) that is
shared between neighboring nodes in $W$. The condition
$\mu_{u}(c),T_{1}\models q^{c}_{(B(w),\mu_{v})}(x)$ that is part of Condition
2 of properness can then be checked, again in triple exponential time in
$||T_{1}||$. Thus, $\mathfrak{C}\xspace_{1}$ can be computed in triple
exponential time.

#### Automaton $\mathfrak{C}\xspace_{2}$.

The check ${\sf chase}_{T_{2}}(D_{A})|_{\Sigma}^{\sf con}\to I_{W,L}$ is
similar to what $\mathfrak{A}\xspace_{4}$ in Lemma 22 achieves and, in fact,
exactly what the sub-automaton for Point 1 of $\mathfrak{B}\xspace_{5}$ in
Lemma 26 achieves. We repeat it here for the sake of convenience. The
2ATA$\mathfrak{C}\xspace_{2}$ behaves exactly as $\mathfrak{A}\xspace_{4}$,
but starts in state $\langle q_{F},\mu\rangle$. Recall that $A=(F,\mu)$, that
$q_{F}$ is $F$ viewed as Boolean CQ, and that
$q_{F}\in{\mathsf{cls}}(T_{2},\Delta)$ and so $\langle q_{F},\mu\rangle$ is a
state in $\mathfrak{A}\xspace_{4}$.