Because of its constant size, the complexity of evaluating a query over the
training database is constant and does not impact the asymptotic time
complexity of evaluating the query over the actual database using our
translation. There are two types of nondeterministic choices in our
algorithms:

  * •

Choosing some $X\leftarrow\mathcal{X}$ in a while-loop. As the while-loops
always update $\mathcal{X}$ with
$\mathcal{X}\coloneqq(\mathcal{X}\setminus\\{X\\})\cup f(X)$ for some $f$, the
order in which the elements of $\mathcal{X}$ are chosen does not matter.

  * •

Choosing a subset of queries $\overline{\mathcal{Q}}\subseteq\mathcal{Q}$ in
the function $\mathsf{sr2ranf}({Q},{\mathcal{Q}})$. Because
$\mathsf{sr2ranf}({Q},{\mathcal{Q}})$ yields a RANF query, we enumerate all
_minimal_ subsets (a subset $\overline{\mathcal{Q}}\subseteq\mathcal{Q}$ is
minimal if there exists no proper subset
$\overline{\mathcal{Q}}^{\prime}\subsetneq\overline{\mathcal{Q}}$ that could
be used instead of $\overline{\mathcal{Q}}$) and choose one that minimizes the
query cost of the RANF query.

  * •

Choosing a variable $x\in V$ and a set $\mathcal{G}$ such that
$\mathsf{cov}({x},{\tilde{Q}},{\mathcal{G}})$, where $\tilde{Q}$ is a query
with range-restricted bound variables and $V\subseteq\mathsf{fv}(\tilde{Q})$.
Observe that the measure $\mathsf{m}(Q)$ on queries, defined in Figure 8,
decreases for the queries in the premises of the rules for
$\mathsf{gen}({x},{\tilde{Q}},{\mathcal{G}})$ and
$\mathsf{cov}({x},{\tilde{Q}},{\mathcal{G}})$, defined in Figures 4 and 5.
Hence, deriving $\mathsf{gen}({x},{\tilde{Q}},{\mathcal{G}})$ and
$\mathsf{cov}({x},{\tilde{Q}},{\mathcal{G}})$ either succeeds or gets stuck
after at most $\mathsf{m}(\tilde{Q})$ steps. In particular, we can enumerate
all sets $\mathcal{G}$ such that $\mathsf{cov}({x},{\tilde{Q}},{\mathcal{G}})$
holds. Because we derive one additional query $\tilde{Q}[x\mapsto y]$ for
every $y\in\mathsf{eqs}({x},{\mathcal{G}})$ and a single query
$\tilde{Q}\land\mathsf{qps}^{\lor}({\mathcal{G}})$, we choose $x\in V$ and
$\mathcal{G}$ minimizing $\left|\mathsf{eqs}({x},{\mathcal{G}})\right|$ as the
first objective and
$\sum_{Q_{\mathit{qp}}\in\mathsf{qps}({\mathcal{G}})}\mathsf{cost}^{\mathcal{T}}(Q_{\mathit{qp}})$
as the second objective. Our particular choice of $\mathcal{G}$ with
$\mathsf{cov}({x},{\tilde{Q}},{\mathcal{G}})$ is merely a heuristic and does
not provide any additional guarantees compared to every other choice of
$\mathcal{G}$ with $\mathsf{cov}({x},{\tilde{Q}},{\mathcal{G}})$.

This process can be further improved by adopting query plan search heuristics
as is done by most of the existing database management systems.

##  7\. Data Golf Benchmark

input: An RC query $Q$ satisfying con, cst, var, rep, $\gamma\in\\{0,1\\}$.

output: Two sets of variables $\mathcal{V}^{+}$ and $\mathcal{V}^{-}$ whose
values must be equal in every tuple in ${\mathcal{T}^{+}_{\vec{v}}}$ and
${\mathcal{T}^{-}_{\vec{v}}}$ when computing a Data Golf structure.

1 function  _$\mathsf{dg}^{\approx}(Q,\gamma)$_ $\,=$

2 switch  _$Q$_ do

3 case  _$r(t_{1},\ldots,t_{\iota(r)})$_ do return
$(\varnothing,\varnothing)$;

4 case  _$x\approx y$_ do return $(\\{x,y\\},\varnothing)$;

5 case  _$\neg Q^{\prime}$_ do

6
$(\mathcal{V}^{+},\mathcal{V}^{-})\coloneqq\mathsf{dg}^{\approx}(Q^{\prime},\gamma)$;

7 return $(\mathcal{V}^{-},\mathcal{V}^{+})$;

8

9 case  _$Q_{1}^{\prime}\lor Q_{2}^{\prime}$ or $Q_{1}^{\prime}\land
Q_{2}^{\prime}$_ do

10
$(\mathcal{V}_{1}^{+},\mathcal{V}_{1}^{-})\coloneqq\mathsf{dg}^{\approx}(Q_{1}^{\prime},\gamma)$;

11
$(\mathcal{V}_{2}^{+},\mathcal{V}_{2}^{-})\coloneqq\mathsf{dg}^{\approx}(Q_{2}^{\prime},\gamma)$;

12 if  _$\gamma=0$_ then return
$(\mathcal{V}_{1}^{+}\cup\mathcal{V}_{2}^{+},\mathcal{V}_{1}^{-}\cup\mathcal{V}_{2}^{-})$;

13 else if  _$Q=Q_{1}^{\prime}\lor Q_{2}^{\prime}$_ then return
$(\mathcal{V}_{1}^{+}\cup\mathcal{V}_{2}^{-},\mathcal{V}_{1}^{-}\cup\mathcal{V}_{2}^{-})$;

14 else if  _$Q=Q_{1}^{\prime}\land Q_{2}^{\prime}$_ then return
$(\mathcal{V}_{1}^{+}\cup\mathcal{V}_{2}^{+},\mathcal{V}_{1}^{+}\cup\mathcal{V}_{2}^{-})$;

15

16 case  _$\exists y.\,Q_{y}$_ do return
$\mathsf{dg}^{\approx}(Q_{y},\gamma)$;

17

Algorithm 5 Computing sets of variables $\mathcal{V}^{+}$ and
$\mathcal{V}^{-}$ to reflect equalities in a query when computing a Data Golf
structure.

input: An RC query $Q$ satisfying con, cst, var, rep, a sequence of pairwise
distinct variables $\vec{v}$, $\mathsf{av}({Q})\subseteq\vec{v}$, sets of
tuples ${\mathcal{T}^{+}_{\vec{v}}}$ and ${\mathcal{T}^{-}_{\vec{v}}}$ over
$\vec{v}$ such that all values of variables from $\mathsf{av}({Q})$ in these
tuples are pairwise distinct (also across tuples) except that, in every tuple
in ${\mathcal{T}^{+}_{\vec{v}}}$ (${\mathcal{T}^{-}_{\vec{v}}}$), the
variables in $\mathcal{V}^{+}$ ($\mathcal{V}^{-}$) have the same value (which
is different across tuples), where
$\mathsf{dg}^{\approx}(Q,\gamma)=(\mathcal{V}^{+},\mathcal{V}^{-})$,
$\gamma\in\\{0,1\\}$.

output: A structure $\mathcal{S}$ such that
${\mathcal{T}^{+}_{\vec{v}}}[\vec{\mathsf{fv}}(Q)]\subseteq\left\llbracket{Q}\right\rrbracket$,
${\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q)]\cap\left\llbracket{Q}\right\rrbracket=\varnothing$,
and $\left\llbracket{Q^{\prime}}\right\rrbracket$ and $\left\llbracket{\neg
Q^{\prime}}\right\rrbracket$ contain at least
$\min\\{\left|{\mathcal{T}^{+}_{\vec{v}}}\right|,\left|{\mathcal{T}^{-}_{\vec{v}}}\right|\\}$
tuples, for every $Q^{\prime}\sqsubseteq Q$.

1 function
_$\mathsf{dg}(Q,\vec{v},{\mathcal{T}^{+}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}},\gamma)$_
$\,=$

2 switch  _$Q$_ do

3 case  _$r(t_{1},\ldots,t_{\iota(r)})$_ do return
$\\{r^{\mathcal{S}}\mapsto{\mathcal{T}^{+}_{\vec{v}}}[t_{1},\ldots,t_{\iota(r)}]\\}$;

4 case  _$x\approx y$_ do return $\varnothing$;

5 case  _$\neg Q^{\prime}$_ do return
$\mathsf{dg}(Q^{\prime},\vec{v},{\mathcal{T}^{-}_{\vec{v}}},{\mathcal{T}^{+}_{\vec{v}}},\gamma)$;

6 case  _$Q_{1}^{\prime}\lor Q_{2}^{\prime}$ or $Q_{1}^{\prime}\land
Q_{2}^{\prime}$_ do

7
$(\mathcal{V}_{1}^{+},\mathcal{V}_{1}^{-})\coloneqq\mathsf{dg}^{\approx}(Q_{1}^{\prime},\gamma)$;
$(\mathcal{V}_{2}^{+},\mathcal{V}_{2}^{-})\coloneqq\mathsf{dg}^{\approx}(Q_{2}^{\prime},\gamma)$;

8 if  _$\gamma=0$_ then
$(\mathcal{V}^{1},\mathcal{V}^{2})\coloneqq(\mathcal{V}_{1}^{+}\cup\mathcal{V}_{2}^{-},\mathcal{V}_{1}^{-}\cup\mathcal{V}_{2}^{+})$;

9 else if  _$Q=Q_{1}^{\prime}\land Q_{2}^{\prime}$_ then
$(\mathcal{V}^{1},\mathcal{V}^{2})\coloneqq(\mathcal{V}_{1}^{-}\cup\mathcal{V}_{2}^{-},\mathcal{V}_{1}^{-}\cup\mathcal{V}_{2}^{+})$;

10 else if  _$Q=Q_{1}^{\prime}\lor Q_{2}^{\prime}$_ then
$(\mathcal{V}^{1},\mathcal{V}^{2})\coloneqq(\mathcal{V}_{1}^{+}\cup\mathcal{V}_{2}^{+},\mathcal{V}_{1}^{-}\cup\mathcal{V}_{2}^{+})$;

11
$({\mathcal{T}^{1}_{\vec{v}}},{\mathcal{T}^{2}_{\vec{v}}})\leftarrow\\{({\mathcal{T}^{1}_{\vec{v}}},{\mathcal{T}^{2}_{\vec{v}}})\mid\left|{\mathcal{T}^{1}_{\vec{v}}}\right|=\left|{\mathcal{T}^{2}_{\vec{v}}}\right|=\min\\{\left|{\mathcal{T}^{+}_{\vec{v}}}\right|,\left|{\mathcal{T}^{-}_{\vec{v}}}\right|\\},\
\text{all values in tuples
in}\allowbreak{\mathcal{T}^{+}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}},{\mathcal{T}^{1}_{\vec{v}}},{\mathcal{T}^{2}_{\vec{v}}}\text{
are chosen to be pairwise distinct (also across tuples) except
that,}\allowbreak\text{in every tuple in }{\mathcal{T}^{1}_{\vec{v}}}\
({\mathcal{T}^{2}_{\vec{v}}}),\text{ the variables in }\mathcal{V}^{1}\
(\mathcal{V}^{2})\text{ have the same value}\allowbreak\text{(which is
different across tuples)}\\}$;

12 if  _$\gamma=0$_ then return
$\mathsf{dg}(Q_{1}^{\prime},\vec{v},{\mathcal{T}^{+}_{\vec{v}}}\cup{\mathcal{T}^{1}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}}\cup{\mathcal{T}^{2}_{\vec{v}}},\gamma)\cup\mathsf{dg}(Q_{2}^{\prime},\vec{v},{\mathcal{T}^{+}_{\vec{v}}}\cup{\mathcal{T}^{2}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}}\cup{\mathcal{T}^{1}_{\vec{v}}},\gamma)$;

13 else if  _$Q=Q_{1}^{\prime}\lor Q_{2}^{\prime}$_ then return
$\mathsf{dg}(Q_{1}^{\prime},\vec{v},{\mathcal{T}^{+}_{\vec{v}}}\cup{\mathcal{T}^{1}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}}\cup{\mathcal{T}^{2}_{\vec{v}}},\gamma)\cup\mathsf{dg}(Q_{2}^{\prime},\vec{v},{\mathcal{T}^{1}_{\vec{v}}}\cup{\mathcal{T}^{2}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}}\cup{\mathcal{T}^{+}_{\vec{v}}},\gamma)$;

14 else if  _$Q=Q_{1}^{\prime}\land Q_{2}^{\prime}$_ then return
$\mathsf{dg}(Q_{1}^{\prime},\vec{v},{\mathcal{T}^{+}_{\vec{v}}}\cup{\mathcal{T}^{-}_{\vec{v}}},{\mathcal{T}^{1}_{\vec{v}}}\cup{\mathcal{T}^{2}_{\vec{v}}},\gamma)\cup\mathsf{dg}(Q_{2}^{\prime},\vec{v},{\mathcal{T}^{+}_{\vec{v}}}\cup{\mathcal{T}^{2}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}}\cup{\mathcal{T}^{1}_{\vec{v}}},\gamma)$;

15

16 case  _$\exists y.\,Q_{y}$_ do return
$\mathsf{dg}(Q_{y},\vec{v},{\mathcal{T}^{+}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}},\gamma)$;

17

Algorithm 6 Computing the Data Golf structure.

In this section, we describe the _Data Golf_ benchmark, which we use to
generate structures (i.e., database instances) for our empirical evaluation.
The technical description of this benchmark is only needed to fully understand
the setup of our empirical evaluation (§8), but its details are independent of
our query translation (§4–6).

Given an RC query, we seek a structure that yields a nontrivial evaluation
result for the overall query and for all its subqueries. Intuitively, the
structure makes query evaluation potentially more challenging compared to the
case where some subquery evaluates to a trivial (e.g., empty) result. More
specifically, Data Golf has two objectives. The first resembles the _regex
golf_ game’s objective [Ell13] (hence the name) and aims to find a structure
on which the result of a given query contains a given _positive_ set of tuples
and does not contain any tuples from another given _negative_ set. The second
objective is to ensure that all the query’s subqueries evaluate to a non-
trivial result.

Formally, given a query $Q$ and two sets of tuples ${\mathcal{T}^{+}}$ and
${\mathcal{T}^{-}}$ over a fixed domain $\mathcal{D}$, representing
assignments of $\mathsf{av}({Q})$ and satisfying further assumptions on their
values, Data Golf produces a structure $\mathcal{S}$ (represented as a partial
mapping from predicate symbols to their interpretations) such that the
projections of tuples in ${\mathcal{T}^{+}}$ (${\mathcal{T}^{-}}$,
respectively) to $\vec{\mathsf{fv}}(Q)$ are in
$\left\llbracket{Q}\right\rrbracket$ (disjoint from
$\left\llbracket{Q}\right\rrbracket$, respectively) and
$\left|\left\llbracket{Q^{\prime}}\right\rrbracket\right|$ and
$\left|\left\llbracket{\neg Q^{\prime}}\right\rrbracket\right|$ are at least
$\min\\{\left|{\mathcal{T}^{+}}\right|,\left|{\mathcal{T}^{-}}\right|\\}$, for
every $Q^{\prime}\sqsubseteq Q$. To be able to produce such a structure
$\mathcal{S}$, we make the following assumptions on $Q$:

  1. (con)

for every subquery $\exists y.\,Q_{y}$ of $Q$ we have
$\mathsf{con}_{\mathsf{vgt}}({y},{Q_{y}},{\mathcal{A}})$ (Figure 11) for some
set of atomic predicates $\mathcal{A}$ and, moreover,
$\\{y\\}\subsetneq\mathsf{fv}(Q_{\mathit{ap}})$ holds for every
$Q_{\mathit{ap}}\in\mathcal{A}$; these conditions prevent subqueries like
$\exists y.\,\neg\mathsf{P}_{2}(x,y)$ and $\exists
y.\,(\mathsf{P}_{2}(x,y)\lor\mathsf{P}_{1}(y))$, respectively;

  2. (cst)

$Q$ contains no subquery of the form $x\approx\mathsf{c}$, which is satisfied
by exactly one tuple;

  3. (var)

$Q$ contains no closed subqueries, e.g., $\mathsf{P}_{1}(42)$, because a
closed subquery is either satisfied by all possible tuples or no tuple at all;
and

  4. (rep)

$Q$ contains no repeated predicate symbols and no equalities $x\approx y$ in
$Q$ share a variable; this avoids subqueries like
$\mathsf{P}_{1}(x)\land\neg\mathsf{P}_{1}(x)$ and $x\approx y\land\neg
x\approx y$.

Given a sequence of pairwise distinct variables $\vec{v}$ and a tuple
$\vec{d}$ of the same length, we may interpret the tuple $\vec{d}$ as a _tuple
over_ $\vec{v}$, denoted as $\vec{d}(\vec{v})$. Given a sequence
$t_{1},\ldots,t_{k}\in\vec{v}\cup\mathcal{C}$ of terms, we denote by
$\vec{d}(\vec{v})[t_{1},\ldots,t_{k}]$ the tuple obtained by evaluating the
terms $t_{1},\ldots,t_{k}$ over $\vec{d}(\vec{v})$. Formally, we define
$\vec{d}(\vec{v})[t_{1},\ldots,t_{k}]\coloneqq(d^{\prime}_{i})_{i=1}^{k}$,
where $d^{\prime}_{i}=\vec{d}_{j}$ if $t_{i}=\vec{v}_{j}$ and
$d^{\prime}_{i}=t_{i}$ if $t_{i}\in\mathcal{C}$. We lift this notion to sets
of tuples over $\vec{v}$ in the standard way.

Data Golf is formalized by the function
$\mathsf{dg}(Q,\vec{v},{\mathcal{T}^{+}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}},\gamma)$,
defined in Figure 6, where $\vec{v}$ is a sequence of pairwise distinct
variables containing all variables in $Q$, i.e.,
$\mathsf{av}({Q})\subseteq\vec{v}$, ${\mathcal{T}^{+}_{\vec{v}}}$ and
${\mathcal{T}^{-}_{\vec{v}}}$ are sets of tuples over $\vec{v}$, and
$\gamma\in\\{0,1\\}$ is a _strategy_. To reflect $Q$’s equalities in the sets
${\mathcal{T}^{+}_{\vec{v}}}$ and ${\mathcal{T}^{-}_{\vec{v}}}$, given a
strategy $\gamma$, we define the function
$\mathsf{dg}^{\approx}(Q,\gamma)=(\mathcal{V}^{+},\mathcal{V}^{-})$ (Figure 5)
that computes two sets of variables $\mathcal{V}^{+}$ and $\mathcal{V}^{-}$
whose values must be equal in every tuple in ${\mathcal{T}^{+}_{\vec{v}}}$ and
${\mathcal{T}^{-}_{\vec{v}}}$, respectively. The values of the remaining
variables ($\vec{v}\setminus\mathcal{V}^{+}$ and
$\vec{v}\setminus\mathcal{V}^{-}$, respectively) must be pairwise distinct and
also different from the value of the variables in $\mathcal{V}^{+}$ and
$\mathcal{V}^{-}$, respectively. In the case of a conjunction or a
disjunction, we add disjoint sets ${\mathcal{T}^{1}_{\vec{v}}}$,
${\mathcal{T}^{2}_{\vec{v}}}$ of tuples over $\vec{v}$ to
${\mathcal{T}^{+}_{\vec{v}}}$, ${\mathcal{T}^{-}_{\vec{v}}}$ so that the
intermediate results for the subqueries are neither equal nor disjoint. We
implement two strategies (parameter $\gamma$) to choose these sets
${\mathcal{T}^{1}_{\vec{v}}}$, ${\mathcal{T}^{2}_{\vec{v}}}$.

Let $\mathcal{S}$ be a Data Golf structure computed by
$\mathsf{dg}(Q,\vec{v},{\mathcal{T}^{+}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}},\gamma)$.
We justify why $\mathcal{S}$ satisfies
${\mathcal{T}^{+}_{\vec{v}}}[\vec{\mathsf{fv}}(Q)]\subseteq\left\llbracket{Q}\right\rrbracket$
and
${\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q)]\cap\left\llbracket{Q}\right\rrbracket=\varnothing$.
We proceed by induction on the query $Q$. Because of (rep), the Data Golf
structures for the subqueries $Q_{1}$, $Q_{2}$ of a binary query $Q_{1}\lor
Q_{2}$ or $Q_{1}\land Q_{2}$ can be combined using the union operator. The
only case that does not follow immediately is that
${\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q)]\cap\left\llbracket{Q}\right\rrbracket=\varnothing$
for a query $Q$ of the form $\exists y.\,Q_{y}$. We prove this case by
contradiction. Without loss of generality we assume that
$\vec{\mathsf{fv}}(Q_{y})=\vec{\mathsf{fv}}(Q)\cdot y$. Suppose that
$\vec{d}\in{\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q)]$ and
$\vec{d}\in\left\llbracket{Q}\right\rrbracket$. Because
$\vec{d}\in{\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q)]$, there exists
some $d$ such that $\vec{d}\cdot
d\in{\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q_{y})]$. Because
$\vec{d}\in\left\llbracket{Q}\right\rrbracket$, there exists some $d^{\prime}$
such that $\vec{d}\cdot d^{\prime}\in\left\llbracket{Q_{y}}\right\rrbracket$.
By the induction hypothesis, $\vec{d}\cdot
d\notin\left\llbracket{Q_{y}}\right\rrbracket$ and $\vec{d}\cdot
d^{\prime}\notin{\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q_{y})]$.
Because $\mathsf{con}_{\mathsf{vgt}}({y},{Q_{y}},{\mathcal{A}})$ holds for
some $\mathcal{A}$ satisfying (con), the query $Q_{y}$ is equivalent to
$(Q_{y}\land{\textstyle\bigvee_{Q_{\mathit{ap}}\in\mathcal{A}}}\;Q_{\mathit{ap}})\lor
Q_{y}[y/\bot]$. We have $\vec{d}\cdot
d^{\prime}\in\left\llbracket{Q_{y}}\right\rrbracket$. If the tuple
$\vec{d}\cdot d^{\prime}$ satisfies $Q_{y}[y/\bot]$, then $\vec{d}\cdot
d\in\left\llbracket{Q_{y}}\right\rrbracket$ (contradiction) because the
variable $y$ does not occur in the query $Q_{y}[y/\bot]$ and thus its
assignment in $\vec{d}\cdot d^{\prime}$ can be arbitrarily changed. Otherwise,
the tuple $\vec{d}\cdot d^{\prime}$ satisfies some atomic predicate
$Q_{\mathit{ap}}\in\mathcal{A}$ and (con) implies
$\\{y\\}\subsetneq\mathsf{fv}(Q_{\mathit{ap}})$. Hence, the tuples
$\vec{d}\cdot d$ and $\vec{d}\cdot d^{\prime}$ agree on the assignment of a
variable $x\in\mathsf{fv}(Q_{\mathit{ap}})\setminus\\{y\\}$. Let
${\overline{\mathcal{T}}^{+}_{\vec{v}}}$ and
${\overline{\mathcal{T}}^{-}_{\vec{v}}}$ be the sets in the recursive call of
$\mathsf{dg}$ on the atomic predicate from $Q_{\mathit{ap}}$. Because
$\vec{d}\cdot d\in{\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q_{y})]$ and
${\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q_{y})]\subseteq{\overline{\mathcal{T}}^{+}_{\vec{v}}}[\vec{\mathsf{fv}}(Q_{y})]\cup{\overline{\mathcal{T}}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q_{y})]$,
the tuple $\vec{d}\cdot d$ is in
${\overline{\mathcal{T}}^{+}_{\vec{v}}}[\vec{\mathsf{fv}}(Q_{y})]\cup{\overline{\mathcal{T}}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q_{y})]$.
Because $\vec{d}\cdot d^{\prime}$ satisfies the quantified predicate
$Q_{\mathit{ap}}$, the tuple $\vec{d}\cdot d^{\prime}$ is in
${\overline{\mathcal{T}}^{+}_{\vec{v}}}[\vec{\mathsf{fv}}(Q_{y})]$. Next we
observe that the assignments of every variable (in particular, $x$) in the
tuples from the sets ${\overline{\mathcal{T}}^{+}_{\vec{v}}}$,
${\overline{\mathcal{T}}^{-}_{\vec{v}}}$ are pairwise distinct (there can only
be equal values of variables within a single tuple). Because the tuples
$\vec{d}\cdot d$ and $\vec{d}\cdot d^{\prime}$ agree on the assignment of $x$,
they must be equal, i.e., $\vec{d}\cdot d=\vec{d}\cdot d^{\prime}$
(contradiction).

The sets ${\mathcal{T}^{+}_{\vec{v}}}$, ${\mathcal{T}^{-}_{\vec{v}}}$ only
grow in $\mathsf{dg}$’s recursion and the properties (con), (cst), (var), and
(rep) imply that $Q$ has no closed subquery. Hence,
${\mathcal{T}^{+}_{\vec{v}}}[\vec{\mathsf{fv}}(Q)]\subseteq\left\llbracket{Q}\right\rrbracket$
and
${\mathcal{T}^{-}_{\vec{v}}}[\vec{\mathsf{fv}}(Q)]\cap\left\llbracket{Q}\right\rrbracket=\varnothing$
imply that $\left|\left\llbracket{Q^{\prime}}\right\rrbracket\right|$ and
$\left|\left\llbracket{\neg Q^{\prime}}\right\rrbracket\right|$ contain at
least
$\min\\{\left|{\mathcal{T}^{+}_{\vec{v}}}\right|,\left|{\mathcal{T}^{-}_{\vec{v}}}\right|\\}$
tuples, for every $Q^{\prime}\sqsubseteq Q$.

######  Example .

Consider the query $Q\coloneqq\neg\exists
y.\,\mathsf{P}_{2}(x,y)\land\neg\mathsf{P}_{3}(x,y,z)$. This query $Q$
satisfies (con), (cst), (var), and (rep). In particular,
$\mathsf{con}_{\mathsf{vgt}}({y},{\mathsf{P}_{2}(x,y)\land\neg\mathsf{P}_{3}(x,y,z)},{\mathcal{A}})$
holds for $\mathcal{A}=\\{\mathsf{P}_{2}(x,y)\\}$ with
$\\{y\\}\subsetneq\mathsf{fv}(\mathsf{P}_{2}(x,y))$. We choose
$\vec{v}=(x,z,y)$,
${\mathcal{T}^{+}_{\vec{v}}}=\\{(0,4,8),\allowbreak(2,6,10)\\}$, and
${\mathcal{T}^{-}_{\vec{v}}}=\\{(12,16,20),(14,18,22)\\}$. The function
$\mathsf{dg}(Q,\vec{v},{\mathcal{T}^{+}_{\vec{v}}},{\mathcal{T}^{-}_{\vec{v}}},\gamma)$
first flips ${\mathcal{T}^{+}_{\vec{v}}}$ and ${\mathcal{T}^{-}_{\vec{v}}}$
because $Q$’s main connective is negation.

For conjunction (a binary operator), two additional sets of tuples are
computed: ${\mathcal{T}^{1}_{\vec{v}}}=\\{(24,28,32),(26,30,34)\\}$ and
${\mathcal{T}^{2}_{\vec{v}}}=\\{(36,40,44),(38,42,46)\\}$. Depending on the
strategy ($\gamma=0$ or $\gamma=1$), one of the following structures is
computed:
$\mathcal{S}_{0}=\\{\mathsf{P}_{2}\mapsto\\{(12,20),(14,22),\allowbreak(24,32),(26,34)\\},\mathsf{P}_{3}\mapsto{\mathcal{T}^{+}_{xyz}}\\}$,
or
$\mathcal{S}_{1}=\\{\mathsf{P}_{2}\mapsto\\{(12,20),(14,22),(0,8),(2,10)\\},\mathsf{P}_{3}\mapsto{\mathcal{T}^{+}_{xyz}}\\}$,
where
${\mathcal{T}^{+}_{xyz}}=\\{(0,8,4),\allowbreak(2,10,6),(24,32,28),(26,34,30)\\}$.

The query $\mathsf{P}_{1}(x)\land Q$ is satisfied by the finite set of tuples
${\mathcal{T}^{+}_{\vec{v}}}[x,z]$ under the structure
$\mathcal{S}_{1}\cup\\{\mathsf{P}_{1}\mapsto\\{(0),(2)\\}\\}$ obtained by
extending $\mathcal{S}_{1}$ ($\gamma=1$). In contrast, the same query
$\mathsf{P}_{1}(x)\land Q$ is satisfied by an infinite set of tuples including
${\mathcal{T}^{+}_{\vec{v}}}[x,z]$ and disjoint from
${\mathcal{T}^{-}_{\vec{v}}}[x,z]$ under the structure
$\mathcal{S}_{0}\cup\\{\mathsf{P}_{1}\mapsto\\{(0),(2)\\}\\}$ obtained by
extending $\mathcal{S}_{0}$ ($\gamma=0$).

##  8\. Empirical Evaluation

We empirically validate the evaluation performance of the queries output by
$\mathsf{RC2SQL}$. We also assess $\mathsf{RC2SQL}$’s translation time, the
average-case time complexity of query evaluation, scalability to large
databases, and DBMS interoperability. To this end, we answer the following
research questions:

  1. (1)

How does $\mathsf{RC2SQL}$’s query evaluation perform compared to the state-
of-the-art tools on both domain-independent and domain-dependent queries?

  2. (2)

How does $\mathsf{RC2SQL}$’s query evaluation scale on large synthetic
databases?

  3. (3)

How does $\mathsf{RC2SQL}$’s query evaluation perform on real-world databases?

  4. (4)

How does the count aggregation optimization impact $\mathsf{RC2SQL}$’s
performance?

  5. (5)

Can $\mathsf{RC2SQL}$ use different DBMSs for query evaluation?

  6. (6)

How long does $\mathsf{RC2SQL}$ take to translate different queries (without
query evaluation)?

We organize our evaluation into five experiments. Four experiments (Small,
Medium, Large, and Real) focus on the type and size of the structures we use
for query evaluation. The fifth experiment (Infinite) focuses on the
evaluation of non-evaluable (i.e., domain-dependent) queries that may
potentially produce infinite evaluation results.

To answer 1, we compare our tool with the translation-based approach by Van
Gelder and Topor [GT91] ($\mathsf{VGT}$), the structure reduction approach by
Ailamazyan et al. [AGSS86], and the $\mathsf{DDD}$ [MLAH99, Møl02],
$\mathsf{LDD}$ [CGS09], and $\mathsf{MonPoly}^{\mathsf{REG}}$ [BKMZ15] tools
that evaluate RC queries directly using infinite relations encoded as binary
decision diagrams. We could not find a publicly available implementation of
Van Gelder and Topor’s translation. Therefore, the tool $\mathsf{VGT}$ for
evaluable RC queries is derived from our implementation by modifying the
function $\mathsf{rb}(\cdot)$ in Figure 1 to use the relation
$\mathsf{con}_{\mathsf{vgt}}({x},{Q},{\mathcal{A}})$ (Appendix A, Figure 11)
instead of $\mathsf{cov}({x},{Q},{\mathcal{G}})$ (Figure 5) and to use the
generator
${\textstyle\bigvee_{Q_{\mathit{ap}}\in\mathcal{A}}}\exists\vec{\mathsf{fv}}(Q)\setminus\\{x\\}.\,Q_{\mathit{ap}}$
instead of $\mathsf{qps}^{\lor}({\mathcal{G}})$. Evaluable queries $Q$ are
always translated into $(Q_{\mathit{fin}},\bot)$ by $\mathsf{rw}({\cdot})$
because all of $Q$’s free variables are range restricted. We exclude
$\mathsf{VGT}$ from the comparison on non-evaluable queries (experiment
Infinite). Similarly, the implementation of Ailamazyan et al.’s approach was
not available; hence we used our formally-verified implementation [Ras22]. The
implementations of the remaining tools were publicly available.

We use Data Golf structures of growing size (experiments Small, Medium, and
Large) to answer 2. In contrast, to answer 3, we use real-world structures
obtained from the Amazon review dataset [NLM19] (experiment Real).

To answer 4, we also consider variants of the translation-based approaches
without the step that uses count aggregation optimization
$\mathsf{optcnt}(\cdot)$, superscripted with a minus (-).

SQL queries computed by the translations are evaluated using the
$\mathsf{PostgreSQL}$ and $\mathsf{MySQL}$ DBMS (5). We superscript the tool
names with P and M accordingly. In the Large experiment, we only use
$\mathsf{PostgreSQL}$ because it consistently performed better than
$\mathsf{MySQL}$ in the Medium experiment. In all our experiments, the
translation-based tools used a Data Golf structure with
$\left|{\mathcal{T}^{+}}\right|=\left|{\mathcal{T}^{-}}\right|=2$ as the
training database. We run our experiments on an AMD Ryzen 7 PRO 4750U computer
with 32 GB RAM. The relations in $\mathsf{PostgreSQL}$ and $\mathsf{MySQL}$
are recreated before each invocation to prevent optimizations based on caching
recent query evaluation results. We measure the query evaluation times of all
the tools and the translation time of our $\mathsf{RC2SQL}$ tool (6). We
provide all our experiments in an easily reproducible and publicly available
artifact [RBKT22a].

Experiments: | Small | Medium | Large | Infinite | Real
---|---|---|---|---|---
$\mathsf{RC2SQL}$ | ✓ | ✓ | ✓ | ✓∗ | ✓
$\mathsf{VGT}$ | ✓ | ✓ | TO | N/A | ✓
$\mathsf{DDD}$ | ✓ | TO | TO | ✓ | ✓
$\mathsf{LDD}$ | ✓ | TO | TO | ✓ | ✓
$\mathsf{MonPoly}^{\mathsf{REG}}$ | ✓ | TO | TO | ✓ | ✓
Ailamazyan et al. | TO | TO | TO | TO | TO
$*$ Only states that the result is infinite.
Table 1. Applicability and performance of all the tools on all the
experiments. TO = Timeout of 300s on all experiment runs, N/A = Not applicable

In the Small, Medium, and Large experiments, we generate ten pseudorandom
queries (denoted as $Q_{i},1\leq i\leq 10$, see Appendix C) with a fixed size
$14$ and Data Golf structures $\mathcal{S}$ (strategy $\gamma=1$). The queries
satisfy the Data Golf assumptions along with a few additional ones: the
queries are not safe range, every bound variable actually occurs in its scope,
disjunction only appears at the top-level, and only pairwise distinct
variables appear as terms in predicates. The queries have $2$ free variables
and every subquery has at most $4$ free variables. We control the size of the
Data Golf structure $\mathcal{S}$ in our experiments using a parameter
$n=\left|{\mathcal{T}^{+}}\right|=\left|{\mathcal{T}^{-}}\right|$. Because the
sets ${\mathcal{T}^{+}}$ and ${\mathcal{T}^{-}}$ grow in the recursion on
subqueries, relations in a Data Golf structure typically have more than $n$
tuples. The values of the parameter $n$ for Data Golf structures are
summarized in Figure 9.

The Infinite experiment consists of five pseudorandom queries $Q^{I}_{i},1\leq
i\leq 5$ (Appendix C) that are _not_ evaluable and
$\mathsf{rw}({Q^{I}_{i}})=(Q_{i,fin},Q_{i,inf})$, where $Q_{i,inf}\neq\bot$.
Specifically, the queries are of the form $Q_{1}\land\forall
x,y.\;Q_{2}\longrightarrow Q_{3}$, where $Q_{1},Q_{2}$, and $Q_{3}$ are either
atomic predicates or equalities. We choose the queries so that the number of
their satisfying tuples is not too high, e.g., quadratic in the parameter $n$,
because no tool can possibly enumerate so many tuples within the timeout. For
each $1\leq i\leq 5$, we compare the performance of our tool to tools that
directly evaluate $Q^{I}_{i}$ on structures generated by the two Data Golf
strategies (parameter $\gamma$), which trigger infinite or finite evaluation
results on the considered queries. For infinite results, our tool outputs this
fact (by evaluating $Q_{i,inf}$), whereas the other tools also output a finite
representation of the infinite result. For finite results, all tools produce
the same output.

Query | $Q_{1}$ | $Q_{2}$ | $Q_{3}$ | $Q_{4}$ | $Q_{5}$ | $Q_{6}$ | $Q_{7}$ | $Q_{8}$ | $Q_{9}$ | $Q_{10}$
---|---|---|---|---|---|---|---|---|---|---
Experiment Small, Evaluable pseudorandom queries $Q$,
$\left|\mathsf{sub}(Q)\right|=14$, $n=500$:
Translation time | 0.6 | 0.0 | 0.1 | 0.0 | 0.0 | 0.0 | 0.0 | 0.1 | 0.0 | 0.0
$\mathsf{RC2SQL}$P | 0.2 | 0.2 | 0.3 | 0.2 | 0.2 | 0.2 | 0.2 | 0.1 | 0.2 | 0.1
$\mathsf{RC2SQL}$M | 0.3 | 0.2 | 0.3 | 0.2 | 0.2 | 0.2 | 0.1 | 0.2 | 0.3 | 0.2
$\mathsf{RC2SQL}^{-}$P | 0.2 | 0.1 | 0.2 | 0.2 | 0.1 | 0.2 | 0.1 | 0.1 | 0.2 | 0.1
$\mathsf{RC2SQL}^{-}$M | 0.2 | 0.1 | 0.3 | 0.2 | 0.1 | 0.2 | 0.1 | 0.1 | 0.4 | 0.3
$\mathsf{VGT}$P | 1.5 | 0.2 | 1.8 | 1.3 | 1.9 | 8.6 | 2.5 | 1.5 | 15.6 | 4.8
$\mathsf{VGT}$M | 0.3 | 0.2 | 0.3 | 0.1 | 0.2 | 56.3 | 6.1 | 0.2 | 155.7 | 13.5
$\mathsf{VGT}^{-}$P | 16.4 | 6.0 | 10.7 | 6.3 | TO | 6.2 | 3.1 | 2.3 | 48.0 | 8.8
$\mathsf{VGT}^{-}$M | 129.1 | 73.7 | 97.3 | 66.8 | TO | 52.1 | 19.1 | 12.8 | TO | 61.1
$\mathsf{DDD}$ | 3.8 | 2.4 | 5.5 | RE | 1.2 | 3.7 | 4.7 | 2.2 | 17.9 | 5.3
$\mathsf{LDD}$ | 35.9 | 16.0 | 46.2 | 15.6 | 9.0 | 28.3 | 12.9 | 17.4 | 206.0 | 32.6
$\mathsf{MonPoly}^{\mathsf{REG}}$ | 31.3 | 11.2 | 29.7 | 10.5 | 10.2 | 31.2 | 10.7 | 21.0 | 103.3 | 24.0
Experiment Medium, Evaluable pseudorandom queries $Q$,
$\left|\mathsf{sub}(Q)\right|=14$, $n=20000$:
$\mathsf{RC2SQL}$P | 2.1 | 1.1 | 2.2 | 1.2 | 1.1 | 1.2 | 0.5 | 0.9 | 1.8 | 1.0
$\mathsf{RC2SQL}$M | 6.2 | 2.6 | 6.6 | 2.7 | 2.4 | 4.4 | 1.6 | 2.7 | 9.0 | 3.3
$\mathsf{RC2SQL}^{-}$P | 1.4 | 0.8 | 1.4 | 0.8 | 0.8 | 1.0 | 0.5 | 0.6 | 1.7 | 1.0
$\mathsf{RC2SQL}^{-}$M | 4.3 | 1.9 | 5.0 | 1.8 | 1.9 | 3.3 | 1.6 | 2.2 | 8.3 | 3.2
$\mathsf{VGT}$P | 2.9 | 1.0 | 3.0 | 2.2 | 2.8 | TO | TO | 2.3 | TO | TO
$\mathsf{VGT}$M | 4.6 | 2.4 | 5.2 | 2.6 | 2.7 | TO | TO | 3.0 | TO | TO
$\mathsf{VGT}^{-}$P | TO | TO | TO | TO | TO | TO | TO | TO | TO | TO
$\mathsf{VGT}^{-}$M | TO | TO | TO | TO | TO | TO | TO | TO | TO | TO
Experiment Large, Evaluable pseudorandom queries $Q$,
$\left|\mathsf{sub}(Q)\right|=14$, tool = $\mathsf{RC2SQL}$P:
$n=40000$ | 4.5 | 2.3 | 4.4 | 2.3 | 2.2 | 2.5 | 1.0 | 1.7 | 3.7 | 1.8
$n=80000$ | 8.8 | 4.5 | 8.7 | 4.8 | 4.5 | 5.0 | 1.8 | 3.3 | 7.2 | 3.7
$n=120000$ | 14.1 | 6.8 | 12.8 | 7.2 | 7.0 | 7.1 | 2.8 | 5.1 | 10.8 | 4.9
Query | $Q^{I}_{1}$ | $Q^{I}_{2}$ | $Q^{I}_{3}$ | $Q^{I}_{4}$ | $Q^{I}_{5}$ | $Q^{I}_{1}$ | $Q^{I}_{2}$ | $Q^{I}_{3}$ | $Q^{I}_{4}$ | $Q^{I}_{5}$
Experiment Infinite, Non-evaluable pseudorandom queries $Q$,
$\left|\mathsf{sub}(Q)\right|=7$, $n=4000$:
| Infinite results ($\gamma=0$) | Finite results ($\gamma=1$)
Translation time | 0.0 | 0.0 | 0.0 | 0.0 | 0.0 | 0.0 | 0.0 | 0.0 | 0.0 | 0.0
$\mathsf{RC2SQL}$P | 0.5 | 0.5 | 0.5 | 0.5 | 0.5 | 0.5 | 1.5 | 0.7 | 0.7 | 1.4
$\mathsf{RC2SQL}$M | 0.3 | 0.5 | 0.3 | 0.5 | 0.5 | 0.4 | 0.7 | 0.4 | 0.6 | 0.6
$\mathsf{RC2SQL}^{-}$P | 0.3 | 0.3 | 0.3 | 0.3 | 0.3 | 0.4 | TO | 0.3 | 0.5 | TO
$\mathsf{RC2SQL}^{-}$M | 0.4 | 1.0 | 0.5 | 0.7 | 0.9 | 0.6 | TO | 0.6 | 0.6 | TO
$\mathsf{DDD}$ | 32.4 | 81.0 | 32.7 | 60.9 | 81.6 | 32.1 | 68.6 | 31.9 | 59.4 | 68.2
$\mathsf{LDD}$ | TO | TO | TO | TO | TO | 288.5 | TO | TO | TO | TO
$\mathsf{MonPoly}^{\mathsf{REG}}$ | 175.0 | TO | 175.4 | TO | TO | 160.3 | 299.1 | 160.0 | TO | TO
Figure 9. Experiments Small, Medium, Large, and Infinite. We use the following
abbreviations: TO = Timeout of 300s, RE = Runtime Error. Reported translation
time for $\mathsf{RC2SQL}$.

Figure 9 shows the empirical evaluation results for the experiments Small,
Medium, Large, and Infinite. All entries are execution times in seconds, TO is
a timeout, and RE is a runtime error. In the experiments Small, Medium, and
Large, the columns correspond to ten unique pseudorandom queries (the same
queries are used in all the three experiments). In the Infinite experiment, we
use five unique pseudorandom queries and two Data Golf strategies. The time it
takes for our translation $\mathsf{RC2SQL}$ to translate each query is shown
in the first line for the experiments Small and Infinite because the queries
in the experiments Medium and Large are the same as in Small. The remaining
lines show evaluation times with the lowest time for a query typeset in bold.
We omit the rows for tools that time out or crash on all queries of an
experiment, e.g., Ailamazyan et al. [AGSS86]. Table 1 summarizes which tools
were used in which experiment. We conclude that our translation
$\mathsf{RC2SQL}$ significantly outperforms all other tools on all queries (1)
(except $\mathsf{VGT}$ on the fourth query, but on the smallest structure) and
scales well to higher values of $n$, i.e., larger relations in the Data Golf
structures, on all queries (2). The count aggregation optimization (4)
provides no conclusive benefit for our translation, while it consistently
improves $\mathsf{VGT}$’s performance, especially in the Medium experiment.

Query | $Q^{\mathit{susp}}$ | $Q^{\mathit{susp}}_{\mathit{user}}$ | ${Q^{\mathit{susp}}_{\mathit{text}}}$ |  | $Q^{\mathit{susp}}$ | $Q^{\mathit{susp}}_{\mathit{user}}$ | ${Q^{\mathit{susp}}_{\mathit{text}}}$
---|---|---|---|---|---|---|---
Param. $n$ | $10^{3}$ | $10^{4}$ | $10^{3}$ | $10^{4}$ | $10^{3}$ | $10^{4}$ | Dataset | GC | MI | GC | MI | GC | MI
Translation time | 0.0 | 0.0 | 0.3 |  | 0.0 | 0.0 | 0.3
$\mathsf{RC2SQL}$P | 1.2 | 1.4 | 1.8 | 2.2 | 3.5 | 4.1 |  | 1.6 | 8.4 | 2.5 | 11.9 | 4.9 | 51.3
$\mathsf{RC2SQL}$M | 0.3 | 1.1 | 0.3 | 1.4 | 0.5 | 2.6 |  | 1.9 | 54.2 | 2.4 | 71.0 | 4.5 | TO
$\mathsf{RC2SQL}^{-}$P | 28.1 | TO | 28.6 | TO | 228.6 | TO |  | 132.9 | TO | 131.8 | TO | TO | TO
$\mathsf{RC2SQL}^{-}$M | TO | TO | TO | TO | TO | TO |  | TO | TO | TO | TO | TO | TO
$\mathsf{VGT}$P | 1.5 | 1.7 | $-$ | $-$ | 204.3 | TO |  | 1.9 | 10.0 | $-$ | $-$ | TO | TO
$\mathsf{VGT}$M | 0.3 | 1.4 | $-$ | $-$ | TO | TO |  | 1.7 | 60.9 | $-$ | $-$ | TO | TO
$\mathsf{VGT}^{-}$P | TO | TO | $-$ | $-$ | TO | TO |  | TO | TO | $-$ | $-$ | TO | TO
$\mathsf{VGT}^{-}$M | TO | TO | $-$ | $-$ | TO | TO |  | TO | TO | $-$ | $-$ | TO | TO
$\mathsf{DDD}$ | 4.0 | TO | 4.1 | TO | 18.6 | TO |  | 61.3 | TO | 61.0 | TO | 126.7 | TO
$\mathsf{LDD}$ | 22.3 | TO | 22.2 | TO | 148.5 | TO |  | TO | TO | TO | TO | TO | TO
$\mathsf{MonPoly}^{\mathsf{REG}}$ | 22.4 | TO | 22.6 | TO | 84.1 | TO |  | TO | TO | TO | TO | TO | TO
Figure 10. Experiment Real with the queries $Q^{\mathit{susp}}$,
$Q^{\mathit{susp}}_{\mathit{user}}$, ${Q^{\mathit{susp}}_{\mathit{text}}}$. We
use the following abbreviations: GC = Gift Cards, MI = Musical Instruments, TO
= Timeout of 300s. Reported translation time for $\mathsf{RC2SQL}$.

We also evaluate the tools on the queries $Q^{\mathit{susp}}$ and
$Q^{\mathit{susp}}_{\mathit{user}}$ from the introduction and on the more
challenging query
${Q^{\mathit{susp}}_{\mathit{text}}}\coloneqq\mathsf{B}(b)\land\exists
u,s,t.\;\forall
p.\;\mathsf{P}(b,p)\longrightarrow\mathsf{S}(p,u,s)\lor\mathsf{T}(p,u,t)$ with
an additional relation $\mathsf{T}$ that relates user’s review text (variable
$t$) to a product. The query ${Q^{\mathit{susp}}_{\mathit{text}}}$ computes
all brands for which there is a user, a score, and a review text such that all
the brand’s products were reviewed by that user with that score or by that
user with that text. We use both Data Golf structures (strategy $\gamma=1$)
and real-world structures obtained from the Amazon review dataset [NLM19]. The
real-world relations $\mathsf{P}$, $\mathsf{S}$, and $\mathsf{T}$ are obtained
by projecting the respective tables from the Amazon review dataset for two
chosen product categories: gift cards (abbreviated GC) consisting of 147 194
reviews of 1 548 products and musical instruments (MI) consisting of 1 512 530
reviews of 120 400 products. The relation $\mathsf{B}$ contains all brands
from $\mathsf{P}$ that have at least three products. Because the tool by
Ailamazyan et al., $\mathsf{DDD}$, $\mathsf{LDD}$, and
$\mathsf{MonPoly}^{\mathsf{REG}}$ only support integer data, we injectively
remap the string and floating-point values from the Amazon review dataset to
integers.

Figure 10 shows the empirical evaluation results: the time it takes for our
translation $\mathsf{RC2SQL}$ to translate each query is shown in the first
line and the execution times on Data Golf structures (left) and on structures
derived from the real-world dataset for two specific product categories
(right) are shown in the remaining lines. We remark that $\mathsf{VGT}$ cannot
handle the query $Q^{\mathit{susp}}_{\mathit{user}}$ as it is not evaluable
[GT91], hence we mark the correspond cells in Figure 10 with $-$. Our
translation $\mathsf{RC2SQL}$ significantly outperforms all other tools
(except $\mathsf{VGT}$ on $Q^{\mathit{susp}}$, where $\mathsf{RC2SQL}$ and
$\mathsf{VGT}$ have similar performance) on both Data Golf and real-world
structures (3). $\mathsf{VGT}^{-}$ translates $Q^{\mathit{susp}}$ into a RANF
query with a higher query cost than $\mathsf{RC2SQL}^{-}$. However, the
optimization $\mathsf{optcnt}(\cdot)$ manages to rectify this inefficiency (4)
and thus $\mathsf{VGT}$ exhibits a comparable performance as
$\mathsf{RC2SQL}$. Specifically, the factor of $80\times$ in query cost
between $\mathsf{VGT}^{-}$ and $\mathsf{RC2SQL}^{-}$ improves to $1.1\times$
in query cost between $\mathsf{VGT}$ and $\mathsf{RC2SQL}$ on a Data Golf
structure with $n=20$ [RBKT22a]. Nevertheless, $\mathsf{VGT}$ does not finish
evaluating the query ${Q^{\mathit{susp}}_{\mathit{text}}}$ on GC and MI
datasets within 5 minutes, unlike $\mathsf{RC2SQL}$. Finally,
$\mathsf{RC2SQL}$’s translation took less than 1 second on all the queries
(6).

##  9\. Conclusion

We presented a translation-based approach to evaluating arbitrary relational
calculus queries over an infinite domain with improved time complexity over
existing approaches. This contribution is an important milestone towards
making the relational calculus a viable query language for practical
databases. In future work, we plan to integrate into our base language
features that database practitioners love, such as inequalities, bag
semantics, and aggregations.

## References

  * [AGSS86] Alfred K. Ailamazyan, Mikhail M. Gilula, Alexei P. Stolboushkin, and Grigorii F. Schwartz.  Reduction of a relational model with infinite domains to the case of finite domains.  Doklady Akademii Nauk SSSR, 286(2):308–311, 1986.  URL: http://mi.mathnet.ru/dan47310.
  * [AH91] Arnon Avron and Yoram Hirshfeld.  On first order database query languages.  In LICS 1991, pages 226–231. IEEE Computer Society, 1991.  doi:10.1109/LICS.1991.151647.
  * [AHV95] Serge Abiteboul, Richard Hull, and Victor Vianu.  Foundations of Databases.  Addison-Wesley, 1995.  URL: http://webdam.inria.fr/Alice/.
  * [BG04] Achim Blumensath and Erich Grädel.  Finite presentations of infinite structures: Automata and interpretations.  Theory Comput. Syst., 37(6):641–674, 2004.  doi:10.1007/s00224-004-1133-y.
  * [BKMZ15] David Basin, Felix Klaedtke, Samuel Müller, and Eugen Zălinescu.  Monitoring metric first-order temporal properties.  J. ACM, 62(2):15:1–15:45, 2015.  doi:10.1145/2699444.
  * [BL00] Michael Benedikt and Leonid Libkin.  Relational queries over interpreted structures.  J. ACM, 47(4):644–680, 2000.  doi:10.1145/347476.347477.
  * [CGS09] Sagar Chaki, Arie Gurfinkel, and Ofer Strichman.  Decision diagrams for linear arithmetic.  In FMCAD 2009, pages 53–60. IEEE, 2009.  doi:10.1109/FMCAD.2009.5351143.
  * [CKMP97] Jens Claußen, Alfons Kemper, Guido Moerkotte, and Klaus Peithner.  Optimizing queries with universal quantification in object-oriented and object-relational databases.  In Matthias Jarke, Michael J. Carey, Klaus R. Dittrich, Frederick H. Lochovsky, Pericles Loucopoulos, and Manfred A. Jeusfeld, editors, VLDB 1997, pages 286–295. Morgan Kaufmann, 1997.  URL: http://www.vldb.org/conf/1997/P286.PDF.
  * [Cod72] E. F. Codd.  Relational completeness of data base sublanguages.  Research Report / RJ / IBM / San Jose, California, RJ987, 1972\.
  * [CT95] Jan Chomicki and David Toman.  Implementing temporal integrity constraints using an active DBMS.  IEEE Trans. Knowl. Data Eng., 7(4):566–582, 1995.  doi:10.1109/69.404030.
  * [EHJ93] Martha Escobar-Molano, Richard Hull, and Dean Jacobs.  Safety and translation of calculus queries with scalar functions.  In Catriel Beeri, editor, PODS 1993, pages 253–264. ACM Press, 1993.  doi:10.1145/153850.153909.
  * [Ell13] Erling Ellingsen.  Regex golf, 2013.  URL: https://alf.nu/RegexGolf.
  * [GT87] Allen Van Gelder and Rodney W. Topor.  Safety and correct translation of relational calculus formulas.  In Moshe Y. Vardi, editor, PODS 1987, pages 313–327. ACM, 1987\.  doi:10.1145/28659.28693.
  * [GT91] Allen Van Gelder and Rodney W. Topor.  Safety and translation of relational calculus queries.  ACM Trans. Database Syst., 16(2):235–278, 1991.  doi:10.1145/114325.103712.
  * [HS94] Richard Hull and Jianwen Su.  Domain independence and the relational calculus.  Acta Informatica, 31(6):513–524, 1994.  doi:10.1007/BF01213204.
  * [Kif88] Michael Kifer.  On safety, domain independence, and capturability of database queries (preliminary report).  In Catriel Beeri, Joachim W. Schmidt, and Umeshwar Dayal, editors, JCDKB 1988, pages 405–415. Morgan Kaufmann, 1988.  doi:10.1016/b978-1-4832-1313-2.50037-8.
  * [KM01] Nils Klarlund and Anders Møller.  MONA v1.4 User Manual.  BRICS, Department of Computer Science, University of Aarhus, 2001.  URL: http://www.brics.dk/mona/.
  * [KNR16] Mahmoud Abo Khamis, Hung Q. Ngo, and Atri Rudra.  FAQ: questions asked frequently.  In Tova Milo and Wang-Chiew Tan, editors, PODS 2016, pages 13–28. ACM, 2016.  doi:10.1145/2902251.2902280.
  * [Lib04] Leonid Libkin.  Elements of Finite Model Theory.  Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004\.  doi:10.1007/978-3-662-07003-1.
  * [LYL08] Hong-Cheu Liu, Jeffrey Xu Yu, and Weifa Liang.  Safety, domain independence and translation of complex value database queries.  Inf. Sci., 178(12):2507–2533, 2008.  doi:10.1016/j.ins.2008.02.005.
  * [MLAH99] Jesper B. Møller, Jakob Lichtenberg, Henrik Reif Andersen, and Henrik Hulgaard.  Difference decision diagrams.  In Jörg Flum and Mario Rodríguez-Artalejo, editors, CSL 1999, volume 1683 of LNCS, pages 111–125. Springer, 1999.  doi:10.1007/3-540-48168-0_9.
  * [Møl02] Jesper B. Møller.  DDDLIB: A library for solving quantified difference inequalities.  In Andrei Voronkov, editor, CADE 2002, volume 2392 of LNCS, pages 129–133. Springer, 2002.  doi:10.1007/3-540-45620-1_9.
  * [NLM19] Jianmo Ni, Jiacheng Li, and Julian J. McAuley.  Justifying recommendations using distantly-labeled reviews and fine-grained aspects.  In Kentaro Inui, Jing Jiang, Vincent Ng, and Xiaojun Wan, editors, EMNLP 2019, pages 188–197. Association for Computational Linguistics, 2019.  doi:10.18653/v1/D19-1018.
  * [NRR13] Hung Q. Ngo, Christopher Ré, and Atri Rudra.  Skew strikes back: new developments in the theory of join algorithms.  SIGMOD Rec., 42(4):5–16, 2013.  doi:10.1145/2590989.2590991.
  * [OS16] Dan Olteanu and Maximilian Schleich.  Factorized databases.  SIGMOD Rec., 45(2):5–16, 2016.  doi:10.1145/3003665.3003667.
  * [Pao69] Robert A. Di Paola.  The recursive unsolvability of the decision problem for the class of definite formulas.  J. ACM, 16(2):324–327, 1969.  doi:10.1145/321510.321524.
  * [Ras22] Martin Raszyk.  First-order query evaluation.  Archive of Formal Proofs, 2022.  Formal proof development.  URL: https://www.isa-afp.org/entries/Eval_FO.html.
  * [RBKT22a] Martin Raszyk, David Basin, Srđan Krstić, and Dmitriy Traytel.  Implementation and empirical evaluation associated with this article, 2022\.  URL: https://github.com/mraszyk/rc2sql/tree/lmcs22.
  * [RBKT22b] Martin Raszyk, David Basin, Srđan Krstić, and Dmitriy Traytel.  Practical relational calculus query evaluation.  In Dan Olteanu and Nils Vortmeier, editors, ICDT 2022, volume 220 of LIPIcs, pages 11:1–11:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.  doi:10.4230/LIPIcs.ICDT.2022.11.
  * [Rev02] Peter Z. Revesz.  Introduction to Constraint Databases.  Texts in Computer Science. Springer, 2002.  doi:10.1007/b97430.
  * [RT22] Martin Raszyk and Dmitriy Traytel.  Making arbitrary relational calculus queries safe-range.  Archive of Formal Proofs, 2022.  Formal proof development.  URL: https://www.isa-afp.org/entries/Safe_Range_RC.html.
  * [Tra50] Boris A. Trakhtenbrot.  Impossibility of an algorithm for the decision problem in finite classes.  Doklady Akademii Nauk SSSR, 70(4):569–572, 1950.
  * [Var81] Moshe Y. Vardi.  The decision problem for database dependencies.  Inf. Process. Lett., 12(5):251–254, 1981.  doi:10.1016/0020-0190(81)90025-9.
  * [Var82] Moshe Y. Vardi.  The complexity of relational query languages (extended abstract).  In Harry R. Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber, editors, STOC 1982, pages 137–146. ACM, 1982\.  doi:10.1145/800070.802186.
  * [Yan19] Jun Yang.  radb, 2019.  URL: https://github.com/junyang/radb.

##  Appendix A Evaluable Queries

The classes of _evaluable_ queries [GT91, Definition 5.2] and _allowed_
queries [GT91, Definition 5.3] are decidable subsets of domain-independent RC
queries. The evaluable queries characterize exactly the domain-independent
queries with no repeated predicate symbols [GT91, Theorem 10.5]. Every
evaluable query can be translated to an equivalent allowed query [GT91,
Theorem 8.6] and every allowed query can be translated to an equivalent RANF
query [GT91, Theorem 9.6].

$\begin{array}[]{@{}l@{\;\;}c@{\;\;}l@{}}\mathsf{gen}_{\mathsf{vgt}}({x},{Q},{\\{Q\\}})&\text{if}&\mathsf{ap}(Q)\,\text{and}\,{x}\in\mathsf{fv}(Q);\\\
\mathsf{gen}_{\mathsf{vgt}}({x},{\neg\neg
Q},{\mathcal{A}})&\text{if}&\mathsf{gen}_{\mathsf{vgt}}({x},{Q},{\mathcal{A}});\\\
\mathsf{gen}_{\mathsf{vgt}}({x},{\neg(Q_{1}\lor
Q_{2})},{\mathcal{A}})&\text{if}&\mathsf{gen}_{\mathsf{vgt}}({x},{(\neg
Q_{1})\land(\neg Q_{2})},{\mathcal{A}});\\\
\mathsf{gen}_{\mathsf{vgt}}({x},{\neg(Q_{1}\land
Q_{2})},{\mathcal{A}})&\text{if}&\mathsf{gen}_{\mathsf{vgt}}({x},{(\neg
Q_{1})\lor(\neg Q_{2})},{\mathcal{A}});\\\
\mathsf{gen}_{\mathsf{vgt}}({x},{\neg\exists
y.\,Q_{y}},{\mathcal{A}})&\text{if}&x\neq
y\,\text{and}\,\mathsf{gen}_{\mathsf{vgt}}({x},{\neg Q_{y}},{\mathcal{A}});\\\
\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{1}\lor
Q_{2}},{\mathcal{A}_{1}\cup\mathcal{A}_{2}})&\text{if}&\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{1}},{\mathcal{A}_{1}})\,\text{and}\,\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{2}},{\mathcal{A}_{2}});\\\
\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{1}\land
Q_{2}},{\mathcal{A}})&\text{if}&\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{1}},{\mathcal{A}});\\\
\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{1}\land
Q_{2}},{\mathcal{A}})&\text{if}&\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{2}},{\mathcal{A}});\\\
\mathsf{gen}_{\mathsf{vgt}}({x},{\exists
y.\,Q_{y}},{\mathcal{A}})&\text{if}&x\neq
y\,\text{and}\,\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{y}},{\mathcal{A}});\\\\[10.0pt]
\mathsf{con}_{\mathsf{vgt}}({x},{Q},{\varnothing})&\text{if}&{x}\notin\mathsf{fv}(Q);\\\
\mathsf{con}_{\mathsf{vgt}}({x},{Q},{\\{Q\\}})&\text{if}&\mathsf{ap}(Q)\,\text{and}\,{x}\in\mathsf{fv}(Q);\\\
\mathsf{con}_{\mathsf{vgt}}({x},{\neg\neg
Q},{\mathcal{A}})&\text{if}&\mathsf{con}_{\mathsf{vgt}}({x},{Q},{\mathcal{A}});\\\
\mathsf{con}_{\mathsf{vgt}}({x},{\neg(Q_{1}\lor
Q_{2})},{\mathcal{A}})&\text{if}&\mathsf{con}_{\mathsf{vgt}}({x},{(\neg
Q_{1})\,\text{and}\,(\neg Q_{2})},{\mathcal{A}});\\\
\mathsf{con}_{\mathsf{vgt}}({x},{\neg(Q_{1}\land
Q_{2})},{\mathcal{A}})&\text{if}&\mathsf{con}_{\mathsf{vgt}}({x},{(\neg
Q_{1})\lor(\neg Q_{2})},{\mathcal{A}});\\\
\mathsf{con}_{\mathsf{vgt}}({x},{\neg\exists
y.\,Q_{y}},{\mathcal{A}})&\text{if}&x\neq
y\,\text{and}\,\mathsf{con}_{\mathsf{vgt}}({x},{\neg Q_{y}},{\mathcal{A}});\\\
\mathsf{con}_{\mathsf{vgt}}({x},{Q_{1}\lor
Q_{2}},{\mathcal{A}_{1}\cup\mathcal{A}_{2}})&\text{if}&\mathsf{con}_{\mathsf{vgt}}({x},{Q_{1}},{\mathcal{A}_{1}})\,\text{and}\,\mathsf{con}_{\mathsf{vgt}}({x},{Q_{2}},{\mathcal{A}_{2}});\\\
\mathsf{con}_{\mathsf{vgt}}({x},{Q_{1}\land
Q_{2}},{\mathcal{A}})&\text{if}&\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{1}},{\mathcal{A}});\\\
\mathsf{con}_{\mathsf{vgt}}({x},{Q_{1}\land
Q_{2}},{\mathcal{A}})&\text{if}&\mathsf{gen}_{\mathsf{vgt}}({x},{Q_{2}},{\mathcal{A}});\\\
\mathsf{con}_{\mathsf{vgt}}({x},{Q_{1}\land
Q_{2}},{\mathcal{A}_{1}\cup\mathcal{A}_{2}})&\text{if}&\mathsf{con}_{\mathsf{vgt}}({x},{Q_{1}},{\mathcal{A}_{1}})\,\text{and}\,\mathsf{con}_{\mathsf{vgt}}({x},{Q_{2}},{\mathcal{A}_{2}});\\\
\mathsf{con}_{\mathsf{vgt}}({x},{\exists
y.\,Q_{y}},{\mathcal{A}})&\text{if}&x\neq
y\,\text{and}\,\mathsf{con}_{\mathsf{vgt}}({x},{Q_{y}},{\mathcal{A}}).\\\
\end{array}$
Figure 11. The relations $\mathsf{gen}_{\mathsf{vgt}}({x},{Q},{\mathcal{A}})$
and $\mathsf{con}_{\mathsf{vgt}}({x},{Q},{\mathcal{A}})$ [GT91].

######  Definition .

A query $Q$ is called _evaluable_ if

  * •

every variable $x\in\mathsf{fv}(Q)$ satisfies
$\mathsf{gen}_{\mathsf{vgt}}({x},{Q})$ and

  * •

the bound variable $y$ in every subquery $\exists y.\,Q_{y}$ of $Q$ satisfies
$\mathsf{con}_{\mathsf{vgt}}({y},{Q_{y}})$.

A query $Q$ is called _allowed_ if

  * •

every variable $x\in\mathsf{fv}(Q)$ satisfies
$\mathsf{gen}_{\mathsf{vgt}}({x},{Q})$ and

  * •

the bound variable $y$ in every subquery $\exists y.\,Q_{y}$ of $Q$ satisfies
$\mathsf{gen}_{\mathsf{vgt}}({y},{Q_{y}})$,

where the relation $\mathsf{gen}_{\mathsf{vgt}}({x},{Q})$ is defined to hold
iff there exists a set of atomic predicates $\mathcal{A}$ such that
$\mathsf{gen}_{\mathsf{vgt}}({x},{Q},{\mathcal{A}})$ and the relation
$\mathsf{con}_{\mathsf{vgt}}({x},{Q})$ is defined to hold iff there exists a
set of atomic predicates $\mathcal{A}$ such that
$\mathsf{con}_{\mathsf{vgt}}({x},{Q},{\mathcal{A}})$, respectively. The
relations $\mathsf{gen}_{\mathsf{vgt}}({x},{Q},{\mathcal{A}})$ and
$\mathsf{con}_{\mathsf{vgt}}({x},{Q},{\mathcal{A}})$ are defined in Figure 11.

The termination of the rules in Figure 11 follow using the measure
$\mathsf{m}(Q)$ (Figure 8). We now relate the definitions from Figure 4 and
Figure 11 with the following lemmas.

######  Lemma .

Let $x$ and $y$ be free variables in a query $Q$ such that
$\mathsf{gen}_{\mathsf{vgt}}({x},{\neg Q})$ and
$\mathsf{gen}_{\mathsf{vgt}}({y},{Q})$ hold. Then we get a contradiction.

###### Proof.

This is proved by induction on the query $Q$ using the measure $\mathsf{m}(Q)$
on queries defined in Figure 8, which decreases in every case of the
definition in Figure 11. ∎

######  Lemma .

Let $Q$ be a query such that $\mathsf{gen}_{\mathsf{vgt}}({y},{Q_{y}})$ holds
for the bound variable $y$ in every subquery $\exists y.\,Q_{y}$ of $Q$.
Suppose that $\mathsf{gen}_{\mathsf{vgt}}({x},{Q})$ holds for a free variable
$x\in\mathsf{fv}(Q)$. Then $\mathsf{gen}({x},{Q})$ holds.

###### Proof.

This is proved by induction on the query $Q$ using the measure $\mathsf{m}(Q)$
on queries defined in Figure 8, which decreases in every case of the
definition in Figure 11.

Lemma A and the assumption that $\mathsf{gen}_{\mathsf{vgt}}({y},{Q_{y}})$
holds for the bound variable $y$ in every subquery $\exists y.\,Q_{y}$ of $Q$
imply that $\mathsf{gen}_{\mathsf{vgt}}({x},{Q})$ cannot be derived using the
rule $\mathsf{gen}_{\mathsf{vgt}}({x},{\neg\exists y.\,Q_{y}})$, i.e., $Q$
cannot be of the form $\neg\exists y.\,Q_{y}$. Every other case in the
definition of $\mathsf{gen}_{\mathsf{vgt}}({x},{Q})$ has a corresponding case
in the definition of $\mathsf{gen}({x},{Q})$. ∎

######  Lemma .

Let $Q$ be an _allowed_ query, i.e., $\mathsf{gen}_{\mathsf{vgt}}({x},{Q})$
holds for every free variable $x\in\mathsf{fv}(Q)$ and
$\mathsf{gen}_{\mathsf{vgt}}({y},{Q_{y}})$ holds for the bound variable $y$ in
every subquery $\exists y.\,Q_{y}$ of $Q$. Then $Q$ is a safe-range query,
i.e., $\mathsf{gen}({x},{Q})$ holds for every free variable
$x\in\mathsf{fv}(Q)$ and $\mathsf{gen}({y},{Q_{y}})$ holds for the bound
variable $y$ in every subquery $\exists y.\,Q_{y}$ of $Q$.

###### Proof.

The lemma is proved by applying Lemma A to every free variable of $Q$ and to
the bound variable $y$ in every subquery of $Q$ of the form $\exists
y.\,Q_{y}$. ∎

Lemma A shows that every allowed query is safe range. But there exist safe-
range queries that are not allowed, e.g., $\mathsf{B}(x)\land x\approx y$.

##  Appendix B Existential Normal Form

Recall that our translation uses a standard approach to obtain RANF queries
from safe-range queries via SRNF [AHV95]. In this section we introduce
existential normal form (ENF), an alternative normal form to SRNF that can
also be used to translate safe-range queries to RANF queries, and we discuss
why we opt for using SRNF instead.

Safe-range
RCSRNFENFRANF$\mathsf{srnf}(Q)$$\mathsf{sr2ranf}({Q_{\mathit{srnf}}},{\varnothing})$$\mathsf{enf}(Q)$$\mathsf{sr2ranf}({Q_{\mathit{enf}}},{\varnothing})$$\mathsf{sr2ranf}({Q})$
Figure 12. Alternative translation from safe-range RC to RANF query via ENF.

Figure 12 shows an overview of the RC fragments and query normal forms (nodes)
and the functions we use to translate between them (edges). The dashed edge
shows the translation of a safe-range query to RANF we opt for in this
article. It is the composition of the two translations from safe-range RC to
SRNF and from SRNF to RANF, respectively. In the rest of this section we
introduce ENF and the corresponding translations to RANF.

ENF was introduced by Van Gelder and Topor [GT91] to translate an allowed
query [GT91] into an equivalent RANF query. Given a safe-range query in ENF,
the rules $(R1)\text{--}(R3)$ from §3.4 can be applied to obtain an equivalent
RANF query [EHJ93, Lemma 7.8]. We remark that the rules $(R1)\text{--}(R3)$
are not sufficient to yield an equivalent RANF query for the original
definition of ENF [GT91]. This issue has been identified and fixed by Escobar-
Molano et al. [EHJ93]. Unlike SRNF, a query in ENF can have a subquery of the
form $\neg(Q_{1}\land Q_{2})$, but no subquery of the form $\neg Q_{1}\lor
Q_{2}$ or $Q_{1}\lor\neg Q_{2}$. A function $\mathsf{enf}(Q)$ that yields an
ENF query equivalent to $Q$ can be defined in terms of subquery rewriting
using the rules in [EHJ93, Figure 2].

Analogously to [EHJ93, Lemma 7.4], if a query $Q$ is safe range, then
$\mathsf{enf}(Q)$ is also safe range. Next we prove the following lemma that
we could use as a precondition for translating safe-range queries in ENF to
queries in RANF.

######  Lemma .

Let $Q_{\mathit{enf}}$ be a query in ENF. Then $\mathsf{gen}({x},{\neg
Q^{\prime}})$ does not hold for any variable $x$ and subquery $\neg
Q^{\prime}$ of $Q_{\mathit{enf}}$.

###### Proof.

Assume that $\mathsf{gen}({x},{\neg Q^{\prime}})$ holds for a variable $x$ in
a subquery $\neg Q^{\prime}$ of $Q_{\mathit{enf}}$. We derive a contradiction
by induction on $\mathsf{m}(Q_{\mathit{enf}})$. According to Figure 4 and by
definition of ENF, $\mathsf{gen}({x},{\neg Q^{\prime}})$ can only hold if
$Q^{\prime}$ is a conjunction. Then $\mathsf{gen}({x},{\neg Q^{\prime}})$
implies $\mathsf{gen}({x},{\neg Q_{1}})$ for some query
$Q_{1}\in\mathsf{flat}^{\land}(Q^{\prime})$ that is not a negation (by
definition of ENF) or conjunction (by definition of
$\mathsf{flat}^{\land}(\cdot)$), i.e., $Q_{1}$ is a disjunction (according to
Figure 4). Then $\mathsf{gen}({x},{\neg Q_{1}})$ implies
$\mathsf{gen}({x},{\neg Q_{2}})$ for some query
$Q_{2}\in\mathsf{flat}^{\lor}(Q_{1})$ that is not a negation (by definition of
ENF) or disjunction (by definition of $\mathsf{flat}^{\lor}(\cdot)$), i.e.,
$Q_{2}$ is a conjunction (according to Figure 4). Next we observe that $\neg
Q_{2}$ is in ENF because $Q_{2}$ is a subquery of the ENF query
$Q_{\mathit{enf}}$, $Q_{2}$ is a conjunction, and $Q_{2}$ is a subquery of a
disjunction ($Q_{1}$) in $Q_{\mathit{enf}}$. Moreover, $\mathsf{m}(\neg
Q_{2})<\mathsf{m}(Q_{1})<\mathsf{m}(Q^{\prime})<\mathsf{m}(Q_{\mathit{enf}})$.
This allows us to apply the induction hypothesis to the ENF query $\neg Q_{2}$
and its subquery $\neg Q_{2}$ (note that a query is a subquery of itself) and
derive that $\mathsf{gen}({x},{\neg Q_{2}})$ does not hold, which is a
contradiction. ∎

Although applying the rules $(R1)\text{--}(R3)$ to $\mathsf{enf}(Q)$ instead
of $\mathsf{srnf}(Q)$ may result in a RANF query with fewer subqueries, the
query cost, i.e., the time complexity of query evaluation, can be arbitrarily
larger. We illustrate this in the following example that is also included in
our artifact [RBKT22a]. We thus opt for using SRNF instead of ENF for
translating safe-range queries into RANF.

######  Example .

The safe-range query
$Q_{\mathit{enf}}\coloneqq\mathsf{P}_{2}(x,y)\land\neg(\mathsf{P}_{1}(x)\land\mathsf{P}_{1}(y))$
is in ENF and RANF, but not SRNF. Applying the rule $(R1)$ to
$\mathsf{srnf}(Q_{\mathit{enf}})$ yields the RANF query
$Q_{\mathit{srnf}}\coloneqq(\mathsf{P}_{2}(x,y)\land\neg\mathsf{P}_{1}(x))\lor(\mathsf{P}_{2}(x,y)\land\neg\mathsf{P}_{1}(y))$
that is equivalent to $Q_{\mathit{enf}}$. The costs of the two queries over a
structure $\mathcal{S}$ are
$\mathsf{cost}^{\mathcal{S}}(Q_{\mathit{enf}})=2\cdot\left|\left\llbracket{\mathsf{P}_{2}(x,y)}\right\rrbracket\right|+\allowbreak\left|\left\llbracket{\mathsf{P}_{1}(x)}\right\rrbracket\right|+\allowbreak\left|\left\llbracket{\mathsf{P}_{1}(y)}\right\rrbracket\right|+\allowbreak
2\cdot\left|\left\llbracket{\mathsf{P}_{1}(x)\land\mathsf{P}_{1}(y)}\right\rrbracket\right|+\allowbreak
2\cdot\left|\left\llbracket{Q_{\mathit{enf}}}\right\rrbracket\right|$ and
$\mathsf{cost}^{\mathcal{S}}(Q_{\mathit{srnf}})=2\cdot\left|\left\llbracket{\mathsf{P}_{2}(x,y)}\right\rrbracket\right|+\allowbreak\left|\left\llbracket{\mathsf{P}_{1}(x)}\right\rrbracket\right|+\allowbreak
2\cdot\left|\left\llbracket{\mathsf{P}_{2}(x,y)}\right\rrbracket\right|+\allowbreak\left|\left\llbracket{\mathsf{P}_{1}(y)}\right\rrbracket\right|+\allowbreak
2\cdot\left|\left\llbracket{\mathsf{P}_{2}(x,y)\land\neg\mathsf{P}_{1}(x)}\right\rrbracket\right|+\allowbreak
2\cdot\left|\left\llbracket{\mathsf{P}_{2}(x,y)\land\neg\mathsf{P}_{1}(y)}\right\rrbracket\right|+\allowbreak
2\cdot\left|\left\llbracket{Q_{\mathit{srnf}}}\right\rrbracket\right|$,
respectively. Note that the cost of $Q_{\mathit{enf}}$ can be arbitrarily
larger if $\mathsf{P}_{1}(x)\land\mathsf{P}_{1}(y)$ evaluates to a large
intermediate result, i.e.,
$\left|\left\llbracket{\mathsf{P}_{1}(x)\land\mathsf{P}_{1}(y)}\right\rrbracket\right|\gg\left|\left\llbracket{\mathsf{P}_{2}(x,y)}\right\rrbracket\right|$.
In contrast, the cost of $Q_{\mathit{srnf}}$ can only be larger by a constant
factor.

##  Appendix C Queries used in the evaluation

$Q_{1}\coloneqq\,$ | $\neg(\exists x_{2}.\,\neg(\exists x_{3}.\,((\mathsf{P}_{3}(x_{1},x_{0},x_{3}))\land(\neg(\exists x_{4}.\,\mathsf{P}_{4}(x_{1},x_{3},x_{4},x_{2}))))\land(\exists x_{4}.\,\mathsf{P}_{2}(x_{1},x_{4}))))\lor(\mathsf{Q}_{2}(x_{1},x_{0}))$
---|---
$Q_{2}\coloneqq\,$ | $\neg(\exists x_{2}.\,\neg(\exists x_{3}.\,(\neg(\mathsf{P}_{4}(x_{1},x_{0},x_{2},x_{3})))\land(\mathsf{P}_{3}(x_{1},x_{3},x_{0}))))\land(\exists x_{2}.\,\exists x_{3}.\,(x_{1}=x_{2})\land(\mathsf{Q}_{3}(x_{0},x_{2},x_{3})))$
$Q_{3}\coloneqq\,$ | $(\exists x_{2}.\,\neg(\exists x_{3}.\,((\mathsf{P}_{3}(x_{1},x_{0},x_{3}))\land(\mathsf{P}_{1}(x_{0})))\land((x_{0}=x_{1})\land(\neg(\mathsf{P}_{4}(x_{1},x_{2},x_{3},x_{0}))))))\land(\exists x_{2}.\,\mathsf{Q}_{3}(x_{1},x_{2},x_{0}))$
$Q_{4}\coloneqq\,$ | $(\exists x_{2}.\,\mathsf{P}_{3}(x_{1},x_{2},x_{0}))\land(\neg(x_{0}=x_{1}))\land(\neg(\exists x_{2}.\,\neg(\exists x_{3}.\,(\mathsf{P}_{2}(x_{0},x_{3}))\land(\neg(\mathsf{P}_{4}(x_{1},x_{3},x_{2},x_{0}))))))$
$Q_{5}\coloneqq\,$ | $(\exists x_{2}.\,\exists x_{3}.\,\neg(\exists x_{4}.\,(\exists x_{5}.\,\mathsf{P}_{3}(x_{0},x_{5},x_{4}))\land(\neg(\mathsf{P}_{4}(x_{0},x_{4},x_{2},x_{3})))))\land((\neg(x_{0}=x_{1}))\land(\mathsf{P}_{2}(x_{0},x_{1})))$
$Q_{6}\coloneqq\,$ | $(\exists x_{2}.\,\neg(\exists x_{3}.\,((\neg(\exists x_{4}.\,\mathsf{P}_{3}(x_{0},x_{3},x_{4})))\land(\mathsf{Q}_{3}(x_{0},x_{1},x_{3})))\land(\neg(\mathsf{R}_{3}(x_{0},x_{2},x_{1})))))\land(\exists x_{2}.\,\mathsf{S}_{3}(x_{0},x_{1},x_{2}))$
$Q_{7}\coloneqq\,$ | $(\exists x_{2}.\,(\mathsf{P}_{3}(x_{0},x_{2},x_{1}))\land(x_{0}=x_{2}))\land(\exists x_{2}.\,\neg(\exists x_{3}.\,(\neg(\exists x_{4}.\,\exists x_{5}.\,\mathsf{P}_{4}(x_{0},x_{2},x_{5},x_{4})))\land(\mathsf{P}_{2}(x_{1},x_{3}))))$
$Q_{8}\coloneqq\,$ | $\neg(\exists x_{2}.\,\neg(\exists x_{3}.\,(\exists x_{4}.\,(\mathsf{P}_{3}(x_{0},x_{3},x_{1}))\land((\mathsf{P}_{4}(x_{0},x_{3},x_{1},x_{4}))\land(x_{3}=x_{4})))\land(\neg(\exists x_{4}.\,\mathsf{Q}_{4}(x_{0},x_{4},x_{3},x_{2})))))$
$Q_{9}\coloneqq\,$ | $\mathsf{P}_{2}(x_{1},x_{0})\land(\exists x_{2}.\,\neg(\exists x_{3}.\,((\neg(\mathsf{P}_{4}(x_{1},x_{3},x_{2},x_{0})))\land(\mathsf{P}_{3}(x_{0},x_{3},x_{1})))\land(\neg(\mathsf{Q}_{2}(x_{0},x_{3})))))\land(x_{0}=x_{1})$
$Q_{10}\coloneqq\,$ | $(\exists x_{2}.\,\mathsf{P}_{3}(x_{1},x_{2},x_{0}))\lor(\neg(\exists x_{2}.\,\neg(\exists x_{3}.\,(\neg(\mathsf{P}_{2}(x_{1},x_{2})))\land(\exists x_{4}.\,(\mathsf{P}_{1}(x_{0}))\land(\mathsf{P}_{4}(x_{0},x_{3},x_{1},x_{4}))))))$
$Q^{I}_{1}\coloneqq\,$ | $\mathsf{P}_{1}(x_{0})\land\neg(\exists x_{2}.\,\exists x_{3}.\,(\mathsf{P}_{3}(x_{0},x_{2},x_{3})\land\neg(x_{0}=x_{1})))$
$Q^{I}_{2}\coloneqq\,$ | $\mathsf{P}_{1}(x_{0})\land\neg(\exists x_{2}.\,\exists x_{3}.\,(\mathsf{P}_{3}(x_{0},x_{2},x_{3})\land\neg\mathsf{P}_{2}(x_{1},x_{3})))$
$Q^{I}_{3}\coloneqq\,$ | $\mathsf{P}_{1}(x_{0})\land\neg(\exists x_{2}.\,\exists x_{3}.\,(\mathsf{P}_{3}(x_{0},x_{3},x_{2})\land\neg(x_{1}=x_{2})))$
$Q^{I}_{4}\coloneqq\,$ | $\mathsf{P}_{1}(x_{1})\land\neg(\exists x_{2}.\,\exists x_{3}.\,(\mathsf{P}_{3}(x_{1},x_{3},x_{2})\land\neg\mathsf{P}_{4}(x_{1},x_{0},x_{3},x_{2})))$
$Q^{I}_{5}\coloneqq\,$ | $\mathsf{P}_{1}(x_{0})\land\neg(\exists x_{2}.\,\exists x_{3}.\,(\mathsf{P}_{3}(x_{0},x_{2},x_{3})\land\neg\mathsf{Q}_{3}(x_{1},x_{2},x_{3})))$
Figure 13. Randomly generated queries.

Figure 13 shows the randomly generated queries that we use in our evaluation.
The index of each predicate indicates the predicate’s arity.