[labelstyle=]

# Optimizing Recursive Queries with Program Synthesis

Yisu Remy Wang University of Washington relationalAI USA ,  Mahmoud Abo Khamis
relationalAI USA ,  Hung Q. Ngo relationalAI USA ,  Reinhard Pichler TU Wien
Austria and  Dan Suciu University of Washington relationalAI USA

(2021)

###### Abstract.

Most work on query optimization has concentrated on loop-free queries.
However, data science and machine learning workloads today typically involve
recursive or iterative computation. In this work, we propose a novel framework
for optimizing recursive queries using methods from program synthesis. In
particular, we introduce a simple yet powerful optimization rule called the
“FGH-rule” which aims to find a faster way to evaluate a recursive program.
The solution is found by making use of powerful tools, such as a program
synthesizer, an SMT-solver, and an equality saturation system. We demonstrate
the strength of the optimization by showing that the FGH-rule can lead to
speedups up to 4 orders of magnitude on three, already optimized Datalog
systems.

††copyright: acmcopyright††journalyear: 2021††doi: 10.1145/1122445.1122456

##  1\. Introduction

Most database systems are designed to support primarily non-recursive (loop-
free) queries. Their optimizers are based on the rule-driven, cost-based
Volcano architecture, designed specifically for optimizing non-recursive query
plans. However, most data science and machine learning workloads today involve
some form of recursion or iteration. Examples include finding the connected
components of a graph, computing the page rank, computing the network
centrality, minimizing an objective function using gradient descent, etc. The
importance of supporting recursive queries has been noted by system designers.
Some modern data analytics systems, like Spark or Tensorflow, support for-
loops. The SQL standard defines a limited form of recursive queries, using the
with construct, and some popular engines, like Postgres or SQLite, do support
this restricted form of recursion.

Datalog is a language designed specifically for recursive queries, and it is
gaining in popularity (Alvaro et al., 2010; Roscoe and Loo, 2018; Vianu, 2021;
Huang et al., 2011; Shkapsky et al., 2016a; Fan et al., 2019; Seo et al.,
2015; Wang et al., 2015; Francis-Landau et al., 2020). But the optimization
problem for recursive queries is much less studied. A datalog program consists
of multiple rules, defining several, mutually recursive relations, and one
distinguished relation name which is the output of the program. The effect of
the program consist of repeatedly applying the rules, sometimes called the
body of the program, until a fixpoint is reached, then it returns the output
relation. Datalog engines typically optimize the loop body, without optimizing
the actual loop. The few systems that do (for example Soufflé) apply only
limited optimization techniques, like magic set optimization and semi-naive
evaluation, which are mainly restricted to positive Datalog queries.

In this paper we describe a new query optimization framework for recursive
queries. Our framework replaces a recursive program with another, equivalent
recursive program, whose body may be quite different, and thus focuses on
optimizing the recursive program as a whole, not on optimizing its body in
isolation; the latter can be done separately, using standard query
optimization techniques. Our optimization is based on a novel rewrite rule for
recursive programs, called the FGH-rule, which we implement using program
synthesis, a technique developed in the programming languages and verification
communities. We introduce a new method for inferring loop invariants, which
extends the reach of the FGH-rule, and also show how to use global constraints
on the data for semantic optimizations using the FGH-rule. We explain these
points in some details next.

The FGH-Rule At the core of our approach is a novel, yet very simple rewrite
rule, called the FGH-rule (pronounced fig-rule), which can be used to prove
that two recursive programs are equivalent, even when their loop bodies are
quite different. We show that the FGH-rule can express previously known
optimizations for Datalog, including magic sets and semi-naive evaluation, and
also a wide range of new optimizations. The optimized program is often
significantly more efficient than the original program, and sometimes can have
a strictly lower asymptotic complexity. We implemented a source-to-source
optimizer using the FGH-rule, evaluated its effectiveness on several Datalog
systems, and observed speedups of up to $4$ orders of magnitude (Sec. 8).

For a taste of the FGH-optimization, consider the following example, from
(Zaniolo et al., 2017, 2018): compute the connected components of an
undirected graph $E(x,y)$. The Datalog program in Fig. 1 (a) achieves this by
first computing the transitive closure relation $TC(x,y)$, then computing a
$\min$-aggregate query assigning to every node $x$ the smallest label $L[y]$
of all nodes $y$ reachable from $x$. In contrast, the optimized program in
Fig. 1 (b) computes directly the CC label of every node $x$ as the minimum of
its own label and the smallest CC label of its neighbors, using a single
recursive rule with $\min$-aggregation. The space complexity of the transitive
closure is $O(n^{2})$, which, in practice, is prohibitively expensive on large
graphs. On the other hand, the optimized query has space complexity $O(n)$.

$\displaystyle TC(x,y)\text{ :- }$ $\displaystyle[x=y]\vee\exists
z(E(x,z)\wedge TC(z,y))$ $\displaystyle CC[x]\text{ :- }$
$\displaystyle\min_{y}\\{{L[y]}\mid{TC(x,y)}\\}$
(a)

$\displaystyle CC[x]\text{ :- }$
$\displaystyle\min(L[x],\min_{y}\\{{CC[y]}\mid{E(x,y)}\\})$
(b)

Figure 1. Unoptimized (a) and optimized (b) Datalog program for the connected
components of an undirected graph.

Pattern Matching vs. Query Synthesis Applying the FGH-rule is an instance of
query rewriting using views. In that problem we are given a set of view
expressions and a query, and the task is to rewrite the query to use the view
expressions rather than the base relations. This problem has been extensively
studied in the literature (Halevy, 2001), and today’s database systems perform
it using pattern matching (Goldstein and Larson, 2001). This is a form of
transformational synthesis, where every candidate query rewriting is
guaranteed to be correct, because it is obtained by applying a limited set of
manually crafted rules (patterns), which are guaranteed to be correct.
However, the FGH-rule often requires exploring a very large space, which
cannot be covered by a limited set of rules. In this paper we propose to use
counterexample-guided inductive synthesis (CEGIS) for this purpose, which is a
technique designed for program sketching (Solar-Lezama et al., 2006; Torlak
and Jackson, 2007). When applied to our context, we call this technique query
synthesis. Unlike pattern matching, query synthesis explores a much larger
space, by examining rewritings that are not necessarily correct, and need to
be checked for correctness by a verifier (z3 in our system). The verifier also
produces a small counterexample database for each rejected candidate, and
these counterexamples are collected by the synthesizer and used to produce
only candidate rewritings that pass all the previous counterexamples, which
significantly prunes the search space of the synthesizer. We report in Sec. 8
synthesis times of less than 1 second, even for complex queries that use
global constraints and require inferring loop invariants.

Monotone Queries and Semiring Semantics Datalog is, by definition, restricted
to monotone queries. This ensures that every query has a well-defined
semantics, namely the least fixpoint of its immediate consequence operator.
Existing optimizations for Datalog, like semi-naive evaluation and magic set
rewriting, apply mainly to monotone queries. Even stratified negation can (if
at all) only be handled by imposing appropriate restrictions (Tekle and Liu,
2019). But queries that contain aggregates or negation (expressed in SQL via
subqueries) are not monotone, and most systems that support recursion prohibit
the combination of aggregates and recursion. This has two shortcomings: it
limits what kind of queries the user can express, and also prevents many of
our FGH-rewritings. For example, the simple computation of connected
components in Fig. 1 (a) can be expressed in PostgreSQL, or in SQLite, or in
Soufflé, because the first rule uses only recursion and the second rule uses
only aggregation. However, none of these systems accepts the query in Fig. 1
(b), because it combines recursion and aggregation.111Prior work (Ganguly et
al., 1991; Seo et al., 2015) has proposed extending Datalog with $\min$ and
$\max$ aggregates by explicitly re-defining the semantics of recursive rules
with aggregates. Our approach keeps the standard least fixpoint semantics, but
generalizes the semiring. In order to express such queries, in this paper we
propose an extension of Datalog, following the approach in (Green et al.,
2007), where the relations are interpreted over ordered semirings.

A semiring is an algebraic structure with two operations, $\oplus,\otimes$.
Traditional Datalog corresponds to the Boolean semiring, where these two
operators are $\vee,\wedge$, while the query in Fig. 1 (b) is over the
Tropical semiring, where the two operators are $\min,+$ (reviewed in Sec. 2).
We call this extension of Datalog to ordered semirings $\text{\sf
Datalog}^{\circ}$, pronounced “Datalogo”, where the circle represents the
semiring. In $\text{\sf Datalog}^{\circ}$ recursion is still restricted to
monotone222This monotonicity is over the partial order from the ordered
semiring. queries, but monotone queries in $\text{\sf Datalog}^{\circ}$
include queries with aggregates, over an appropriate semiring. The query in
Fig. 1 (b) is monotone over the (ordered) tropical semiring.

Loop Invariants One difficulty in reasoning about loops in programming
languages is the need to discover loop invariants. Some (but not all)
applications of the FGH-rule also require the discovery of loop invariants. We
describe a novel technique for inferring loop invariants for $\text{\sf
Datalog}^{\circ}$ programs, by combining symbolic execution with equality
saturation, and using a verifier. We execute symbolically the recursive
program for a very small number of iterations (five in our system), obtain
query expressions for the IDBs (the recursive predicates), and construct all
identities satisfied by the IDBs. Then, we retain only candidates that hold at
each iteration, and check each candidate for correctness using the SMT solver.
By inferring and using loop invariants we show that we can significantly
improve some instances of magic-set optimizations from the literature: we call
the new optimization beyond magic.

Constraints and Semantic Optimizations Optimizations that are conditioned on
certain constraints on the database are known as semantic optimizations
(Ramakrishnan and Srivastava, 1994). SQL optimizers routinely use key
constraints and foreign key constraints to optimize queries. More powerful
optimizations can be performed using the chase and back-chase framework
(Deutsch et al., 1999; Popa et al., 2000), and these include optimizations
under inclusion constraints, or conditional functional dependencies, or tuple
generating constraints. However, all constraints that are useful for
optimizing non-recursive queries are local. In contrast, the FGH-rule
optimizes recursive queries, and therefore it can also exploit global
constraints. For example, suppose the database represents a graph, and the
global constraint states that the graph is a tree. This global constraint does
not help optimize non-recursive queries, but can be used to great advantage to
optimize some recursive queries; we give details in Sec. 3.3.

Equality Saturation Systems Throughout our optimizer we need to manage
symbolic expressions of queries, and their equivalence classes, as defined by
a set of rules. We uses for this purpose a state-of-the-art Equality
Saturation System (EQSAT), EGG (Willsey et al., 2021). We show how to use
EQSAT for checking equality under constraints, inferring loop invariants, and
“denormalization” (which is essentially query rewriting using views).

Related Work Our work was partially inspired by the PreM condition, described
by Zaniolo et al. (Zaniolo et al., 2017), which, as we shall explain, is a
special case of the FGH-rule. Unlike our system, their implementation required
the programmer to check the PreM manually, then perform the corresponding
optimization. Seveal prior systems leveraged SMT-solvers to reason about query
languages (Veanes et al., 2009; Chu et al., 2017; Grossman et al., 2017;
Schlaipfer et al., 2017; Wang et al., 2018); but none of these consider
recursive queries. Datalog synthesizers have been described in (Albarghouthi
et al., 2017; Si et al., 2018; Si et al., 2019; Wang et al., 2020b;
Raghothaman et al., 2020). Their setting is different from ours: the
specification is given by input-output examples, and the synthesizer needs to
produce a program that matches all examples. A design choice that we made, and
which sets us further aside from the previous systems, is to use an existing
CEGIS system, Rosette; thus, we do not aim to improve the CEGIS system itself,
but optimize the way we use it.

Contributions In summary, the main contribution of this paper consists of a
new, principled and powerful method for optimizing recursive queries. We make
the following specific contributions:

  * •

We introduce a simple optimization rule for recursive queries, called the FGH-
rule (Sec. 3).

  * •

We show how the FGH-rule captures known optimizations (magic sets, PreM, semi-
naive), (Sec. 3.1), some new optimizations (Sec. 3.2), and optimizations under
global constraints (Sec. 3.3).

  * •

We present our novel framework for query optimization via the FGH-rule (Sec.
4).

  * •

We describe how an SMT solver (Sec. 5) and a CEGIS system (Sec. 6) can be
profitably integrated into our FGH-optimizer.

  * •

We describe how to use an EQSAT system for various tasks in the FGH optimizer:
loop-invariant inference, denormalization, and checking equivalence under
constraints (Sec. 7).

##  2\. Background

Datalog A relation of arity $k$ is a finite subset of $D^{k}$, where $D$ is a
fixed domain. The abbreviations EDB and IDB stand for Extensional Database and
Intensional Database, and represent the base relations and the computed
relations respectively. A Datalog rule has the form:

$\displaystyle R_{0}(\texttt{vars})\text{ :- }$ $\displaystyle
R_{1}(\texttt{vars}_{1})\wedge\cdots\wedge R_{m}(\texttt{vars}_{m})$

where $R_{0}$ is an IDB, and $R_{1},\ldots,R_{m}$ are IDBs or EDBs. The rule
is safe if every variable occurs in at least some predicate in the body, and
the rule is linear if its body contains at most one IDB. A Datalog program
consists of a set of possibly mutually recursive rules. Usually, only a subset
of the IDB predicates are returned to the user, and we will call them the
answer IDBs. The Immediate Consequence Operator, ICO, is the mapping on the
IDB predicates that consists of one application of all the Datalog rules. The
semantics of a Datalog program is given by the least fixpoint of its ICO. The
naive evaluation algorithm consists of repeatedly applying the ICO until the
IDBs no longer change.

In this paper we will combine multiple rules with the same head into a single
rule by OR-ing their bodies, and writing explicitly all existential
quantifiers. This is a common convention used in the literature, see e.g.,
(Fitting, 1991). For example the following datalog program, which computes the
transitive closure of a relation $E$,

$\displaystyle TC(x,y)\text{ :- }$ $\displaystyle E(x,y)$ $\displaystyle
TC(x,y)\text{ :- }$ $\displaystyle E(x,z)\wedge TC(z,y)$

becomes $TC(x,y)\text{ :- }E(x,y)\vee\exists z(E(x,z)\wedge TC(z,y))$.

(Pre-)Semirings A pre-semiring is a tuple
$\bm{S}=(S,\oplus,\otimes,\bar{0},\bar{1})$ where $\oplus$ is commutative,
both $\oplus,\otimes$ are associative, have identities $\bar{0}$ and $\bar{1}$
respectively, and $\otimes$ distributes over $\oplus$. When $\otimes$ is
commutative, then we call $\bm{S}$ a commutative pre-semiring. All pre-
semirings in this paper are commutative, and we will simply refer to them as
pre-semirings. When the equality $x\otimes\bar{0}=\bar{0}$ holds for all $x$,
then it is called a semiring. An ordered pre-semiring is a pre-semiring with a
partial order $\preceq$, where both $\oplus,\otimes$ are monotone operations.
When the partial order is defined by $x\preceq y$ iff $\exists z,x\oplus z=y$
then it is called the natural order. Examples of ordered (pre-)semirings are
the Booleans $\mathbb{B}=(\\{0,1\\},\vee,\wedge,0,1)$, the closed natural
numbers $\mathbb{N}^{\infty}=(\mathbb{N}\cup\\{\infty\\},+,*,0,1)$, the
tropical semiring $\text{\sf
Trop}=(\mathbb{N}\cup\\{\infty\\},\min,+,\infty,0)$, the reversed tropical
semiring $\text{\sf Trop}^{r}=(\mathbb{N},\max,+,0,0)$, the lifted naturals
and lifted reals $\mathbb{N}_{\bot}=(\mathbb{N}\cup\\{\bot\\},+,*,0,1)$,
$\mathbb{R}_{\bot}=(\mathbb{R}\cup\\{\bot\\},+,*,0,1)$, where
$\bot+x=\bot*x=\bot$. The structures $\mathbb{B},\mathbb{N}^{\infty},\text{\sf
Trop}$ are semirings, the others are pre-semirings. $\mathbb{B}$,
$\mathbb{N}^{\infty},\text{\sf Trop}$, and $\text{\sf Trop}^{r}$ are naturally
ordered. Confusingly (!!), the order relation on Trop is the reverse one:
$\infty$ is the smallest, and $0$ is the largest element. The order relation
in $\mathbb{N}_{\bot}$ and $\mathbb{R}_{\bot}$ is given by $\bot\preceq x$ for
all $x$: they are ordered pre-semirings but not naturally ordered.333Note that
we define Trop and $\text{\sf Trop}^{r}$ over the natural numbers rather than
the reals. The motivation for this slight deviation from the standard
definition of these semirings will become clear in Section 5: the support of
integer theories by the SMT-solver z3.

$\bm{S}$-relations An $\bm{S}$-relation $R$ is a function that associates to
each tuple $t\in D^{k}$ a value in the semiring, $R[t]\in\bm{S}$. In this
context, $\bm{S}$ is called the value space of the relation $R$, while the
domain $D$ of its attributes is called the key space. $\bm{S}$-relations were
first introduced444Under the name $K$-relations. by Green et al. (Green et
al., 2007) in order to model data provenance. A $\mathbb{B}$-relation is a
set, an $\mathbb{N}^{\infty}$-relation is a bag (with possibly infinite
multiplicities), an $\mathbb{R}_{\bot}$-relation is a tensor (with possibly
undefined entries).

Queries Consider a relational schema $R_{1},R_{2},\ldots$ over a pre-semiring
$\bm{S}$. A positive (relational algebra) query is a relational algebra
expression using selections, projections, joins, and unions (no difference
operator in the positive fragment). The most common definition of the
relational algebra restricts the predicates used in selections to equality
predicates, $x=y$. In this paper we follow (Green et al., 2007) and allow
arbitrary predicates $p(x,y,\ldots)$ over the value space, including
disequality $x\neq y$, inequality $x<y$, or any other interpreted predicate.
Green (Green et al., 2007) showed that positive relational algebra extends
naturally to an arbitrary semiring $\bm{S}$. When $\bm{S}$ is the Boolean
semiring, then this coincides with the set semantics of relational algebra,
and when $\bm{S}$ is the semiring of natural numbers, then it coincides with
bag semantics.

Normal Forms Alternatively, a query can be described using rules, as follows.
A sum-product query is an expression

(1) $\displaystyle T(x_{1},\ldots,x_{k})$ $\displaystyle\text{ :-
}\bigoplus_{x_{k+1},\ldots,x_{p}\in D}A_{1}\otimes\cdots\otimes A_{m}$

where each $A_{u}$ is a relational atom of the form
$R_{i}(x_{t_{1_{i}}},\ldots,x_{t_{k_{i}}})$, or some interpreted predicate
such as $x_{i}>5x_{j}+3$. The variables $x_{1},\ldots,x_{k}$ are called free
variables, or head variables, and the others are called bound variables. A
sum-sum-product query has the form:

(2) $\displaystyle Q(x_{1},\ldots,x_{k})$ $\displaystyle\text{ :-
}T_{1}(x_{1},\ldots,x_{k})\oplus\cdots\oplus T_{q}(x_{1},\ldots,x_{k})$

where $T_{1},T_{2},\ldots,T_{q}$ are sum-product expressions with the same
head variables $x_{1},\ldots,x_{k}$. When the semiring is
$\mathbb{B},\mathbb{N}^{\infty}$ and the interpreted predicates are restricted
to equality predicates, then these queries are (Unions of) Conjunctive Queries
(UCQs) under set semantics, or under bag semantics; when the semiring is
$\mathbb{R}_{\bot}$, then the sum-products are tensor expressions, sometimes
called Einsum expressions (Rocktäschel, [n.d.]). Every positive relational
algebra query $Q$ can be converted into a sum-sum-product expression, which we
call the normal form of $Q$.

Datalogo Let $\bm{S}$ be an ordered pre-semiring. A $\text{\sf
Datalog}^{\circ}$ program consists of a set of (possibly recursive) sum-sum-
product rules (2) over $\bm{S}$-relations. We allow two extensions to the
expressions (1) and (2): the summation in (1) may be restricted by some
Boolean predicate, and we also allow an atom $A$ in (1) to be an interpreted
function. One important interpreted function is the cast operator
$[-]_{\bar{0}}^{\bar{1}}:\mathbb{B}\rightarrow\bm{S}$, which maps $0$ to
$\bar{0}$ and $1$ to $\bar{1}$ and therefore, for any predicate $P$,
$[P]_{\bar{0}}^{\bar{1}}$ is an atom in the pre-semiring $\bm{S}$. For
example, $[x<y]_{\bar{0}}^{\bar{1}}$ is $\bar{0}\in\bm{S}$ when $x\geq y$ and
$\bar{1}\in\bm{S}$ when $x<y$; when $\bar{0},\bar{1}$ are clear from the
context, we drop them and write simply $[x<y]$. We treat interpreted functions
in a similar way to negation in standard Datalog, and require a program to be
stratified, such that the interpreted functions are applied only to EDBs or to
IDBs defined in earlier strata. This implies that the ICO of that stratum is a
monotone function in the IDBs defined by that stratum, and its semantics is
defined as its least fixpoint. Abo Khamis et al. (Khamis et al., 2021) proved
that any $\text{\sf Datalog}^{\circ}$ program over the semirings discussed in
this section (except for $\mathbb{N}^{\infty}$ and $\text{\sf Trop}^{r}$)
converges in polynomial time in the size of the input database.

###### Example 2.1.

Consider the body of the rule in Fig. 1(b). The relations $L,CC$ are over the
tropical semiring, while $E$ is over the Boolean semiring. Formally, its body
is a sum-sum-product expression, with a Boolean predicate:

$\displaystyle L[x]\oplus\bigoplus_{y}\\{{CC[y]}\mid{E(x,y)}\\}$

Here the summation $\bigoplus_{y}$ is restricted to those values $y$ that
satisfy the predicate $E(x,y)$. Equivalently, we can rephrase it as:

$\displaystyle
L[x]\oplus\bigoplus_{y}\left(CC[y]\otimes[E(x,y)]_{\infty}^{0}\right)$

where $[-]_{\infty}^{0}$ is the cast operator from $\mathbb{B}$ to Trop; it
maps $0,1$ to $\infty,0$ respectively. Alternatively, suppose that we
represent a label $v=L[x]$ using a standard, Boolean-valued relation $L(x,v)$,
where $x$ is a key, and $v$ is the numerical value (label). Then, instead of
the atom $L[x]$ we would write $\bigoplus_{v}\\{{v}\mid{L(x,v)}\\}$, or
$\bigoplus_{v}\left(v\otimes[L(x,v)]_{\infty}^{0}\right)$. Here $v$ is
considered to be an atom.

##  3\. The FGH-Rule

In this section we introduce a simple rewrite rule that allows us to rewrite
an iterative program to another, possibly more efficient program. Then, we
illustrate how this rule, when applied to $\text{\sf Datalog}^{\circ}$
programs, can express several known optimizations in the literature, as well
as some new ones.

Consider an iterative program that repeatedly applies a function $F$ until
some termination condition is satisfied, then applies a function $G$ that
returns the final answer $Y$:

$\displaystyle X\leftarrow X_{0}$ (3) $\displaystyle\texttt{loop }X\leftarrow
F(X)\texttt{ end loop}$ $\displaystyle Y\leftarrow G(X)$

We call this an FG-program. The FGH-rule (pronounced FIG-rule) provides a
sufficient condition for the final answer $Y$ to be computed by the
alternative program, called the GH-program:

$\displaystyle Y\leftarrow G(X_{0})$ (4) $\displaystyle\texttt{loop
}Y\leftarrow H(Y)\texttt{ end loop}$

###### Theorem 3.1 (The FGH-Rule).

If the following identity holds:

(5) $\displaystyle G(F(X))=$ $\displaystyle\ H(G(X))$

then the FG-program (3) is equivalent to the GH-program (4).

###### Proof.

Let $X_{0},X_{1},X_{2},\ldots$ denote the intermediate values of the FG-
program, and $Y_{0},Y_{1},Y_{2},\ldots$ those of the GH-program. By the FGH-
rule, the following diagram commutes, proving the claim:

${{X_{0}}}$${{X_{1}}}$${{X_{2}}}$${\cdots}$${{X_{n}}}$${{Y_{0}}}$${{Y_{1}}}$${{Y_{2}}}$${\cdots}$${{Y_{n}}}$$\scriptstyle{F}$$\scriptstyle{G}$$\scriptstyle{H}$$\scriptstyle{G}$$\scriptstyle{F}$$\scriptstyle{H}$$\scriptstyle{G}$$\scriptstyle{F}$$\scriptstyle{H}$$\scriptstyle{G}$$\scriptstyle{F}$$\scriptstyle{H}$

∎

In this paper we will apply the FGH-rule to optimize $\text{\sf
Datalog}^{\circ}$ programs. In this context, $F$ is the ICO of the $\text{\sf
Datalog}^{\circ}$ program, $X$ is the tuple of all its IDB predicates, and $Y$
are the answer-IDB predicates. We will also make the natural assumption that
$G$ maps the initial state $X_{0}$ of the IDBs of the program (3) to the
initial state $Y_{0}$ of (4). For example, if both programs are traditional
Datalog programs, then the initial state consists of all IDBs being the empty
set, which we denote, with some abuse, by $X_{0}=\emptyset$, even when $X$
consists of several mutually recursive IDBs. Similarly, $Y_{0}=\emptyset$.
Typically, $G$ is a conjunctive query, which maps $\emptyset$ to $\emptyset$,
and in that case the theorem implies that, if Eq. (5) holds, then the
following $\text{\sf Datalog}^{\circ}$ programs $\Pi_{1},\Pi_{2}$ return the
same answer $Y$:

$\displaystyle\Pi_{1}:$ $\displaystyle X\text{ :- }$ $\displaystyle F(X)$
$\displaystyle\Pi_{2}:$ $\displaystyle Y\text{ :- }$ $\displaystyle H(Y)$ (6)
$\displaystyle Y\text{ :- }$ $\displaystyle G(X)$

More generally, however, the theorem does not care about the termination
condition of the FG-programs (3). It only assumes that the GH-program is
executed the same number of iterations as the FG-program. However, it follows
immediately that, if $F$ reaches a fixpoint, then so does $H$:

###### Corollary 3.2.

If the FG-program reaches a fixpoint after $n$ steps (meaning:
$X_{n}=X_{n+1}$) then the GH-program also reaches a fixpoint after $n$ steps
($Y_{n}=Y_{n+1}$). The converse fails: the GH-program may converge much faster
than the FG-program.

In summary, the optimization proceeds as follows. Given an FG-program defined
by the query expressions $F$ and $G$, find a new query expression $H$ such
that the identity $G\circ F=H\circ G$ holds, then replace the FG-program with
the GH-program. We will describe this process in detail in Sec. 4. In the
remainder of this section we present several examples showing that the FGH-
rule can express several known optimizations, like magic set rewriting, and
new optimizations, like semantic optimizations using global constraints.

###  3.1. Simple Examples

###### Example 3.3 (Connected Components).

Consider the computation of the connected components of a graph, which is a
well-known target of query optimization in the literature, see e.g., (Zaniolo
et al., 2018). The program is given in Fig. 1 (a), and its optimized version
in Fig. 1 (b). The three transformations $F,G,H$ are as follows:

$\displaystyle F(TC)\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle
TC^{\prime}$ where $\displaystyle
TC^{\prime}(x,y)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle[x=y]\vee\exists z(E(x,z)\wedge TC(z,y))$ $\displaystyle
G(TC)\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle CC$ where
$\displaystyle CC[x]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\min_{y}\\{{L[y]}\mid{TC(x,y)}\\}$ $\displaystyle
H(CC)\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle CC^{\prime}$
where $\displaystyle CC^{\prime}[x]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\min(L[x],\min_{y}\\{{CC[y]}\mid{E(x,y)}\\})$

To check the FGH-rule, we compute
$CC_{1}\stackrel{{\scriptstyle\text{def}}}{{=}}G(F(TC))=G(TC^{\prime})$, then
compute $CC_{2}\stackrel{{\scriptstyle\text{def}}}{{=}}H(G(TC))=H(CC)$, both
shown in Fig. 2, and observe that it becomes identical to $CC_{1}$ after
renaming the variables $y^{\prime},y$ to $y,z$ respectively.

$\displaystyle CC_{1}[x]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\min_{y}\\{{L[y]}\mid{TC^{\prime}(x,y)}\\}$ $\displaystyle=$
$\displaystyle\min_{y}\\{{L[y]}\mid{[x=y]\vee\exists z(E(x,z)\wedge
TC(z,y))}\\}$ $\displaystyle=$
$\displaystyle\min(L[x],\min_{y}\\{{L[y]}\mid{\exists z(E(x,z)\wedge
TC(z,y))}\\})$ $\displaystyle=$
$\displaystyle\min(L[x],\min_{y,z}\\{{L[y]}\mid{E(x,z)\wedge TC(z,y)}\\})$
$\displaystyle CC_{2}[x]\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\min(L[x],\min_{y}\\{{CC[y]}\mid{E(x,y)}\\})$ $\displaystyle=$
$\displaystyle\min(L[x],\min_{y}\\{{\min_{y^{\prime}}\\{{L[y^{\prime}]}\mid{TC(y,y^{\prime})}\\}}\mid{E(x,y)}\\})$
$\displaystyle=$
$\displaystyle\min(L[x],\min_{y^{\prime},y}\\{{L[y^{\prime}]}\mid{E(x,y)\wedge
TC(y,y^{\prime})}\\})$

Figure 2. Computing $CC_{1}$ and $CC_{2}$ from Example 3.3.

###### Example 3.4 (PreM Property).

Zaniolo et al. (Zaniolo et al., 2017) define the Pre-mappability rule (PreM),
and prove that, under this rule, one Datalog program with ICO $F$ is
equivalent to another program with a simpler ICO. The PreM property is a
restricted form of the FGH-rule, more precisely it asserts that the identity
$G(F(X))=G(F(G(X)))$ holds. In this case one can simply define $H$ as
$H(X)=G(F(X))$, and the FGH-rule holds. The PreM rule is more restricted than
the FGH-rule, in two ways. First, the types of the IDBs of the F-program and
the H-program must be the same. Second, the new query $H$ is uniquely defined,
namely $H\stackrel{{\scriptstyle\text{def}}}{{=}}G\circ F$. While this
simplifies the optimizer significantly, it also limits the type of
optimizations that are possible under PreM.

###### Example 3.5 (Simple Magic).

The simplest application of magic set optimization (Bancilhon et al., 1986;
Mumick and Pirahesh, 1994; Mumick et al., 1990) converts transitive closure to
reachability. More precisely, it rewrites this program:

$\displaystyle\Pi_{1}:$ $\displaystyle TC(x,y)\text{ :- }$
$\displaystyle[x=y]\vee\exists z(TC(x,z)\wedge E(z,y))$ (7) $\displaystyle
Q(y)\text{ :- }$ $\displaystyle TC(a,y)$

where $a$ is some constant, into this program:

(8) $\displaystyle\Pi_{2}:$ $\displaystyle Q(y)\text{ :- }$
$\displaystyle[y=a]\vee\exists z(Q(z)\wedge E(z,y))$

This is a powerful optimization, because it reduces the run time from
$O(n^{2})$ to $O(n)$. Several Datalog systems support some form of magic set
optimizations. We check that (7) is equivalent to (8) by verifying the FGH-
rule. The functions $F,G,H$ are shown in Fig. 3. One can verify that
$G(F(TC))=H(G(TC))$, for any relation $TC$. Indeed, after converting both
expressions to normal form, we obtain $G(F(TC))=H(G(TC))=P$, where:

$\displaystyle P(y)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle[y=a]\vee\exists z(TC(a,z)\wedge E(z,y))$

We prove in the full version of this paper that, given a sideways information
passing strategy (SIPS) (Beeri and Ramakrishnan, 1991) every magic set
optimization (Balbin et al., 1991) over a Datalog program can be proven
correct using a sequence of applications of the FGH-rule.

$\displaystyle F(TC)\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle
TC^{\prime}$ where $\displaystyle
TC^{\prime}(x,y)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle[x=y]\vee\exists z(TC(x,z)\wedge E(z,y))$ $\displaystyle
G(TC)\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle Q$ where
$\displaystyle Q(y)\stackrel{{\scriptstyle\text{def}}}{{=}}$ $\displaystyle
TC(a,y)$ $\displaystyle H(Q)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle Q^{\prime}$ where $\displaystyle
Q^{\prime}(y)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle[y=a]\vee\exists z(Q(z)\wedge E(z,y))$

Figure 3. Expressions $F,G,H$ in Example 3.5.

###### Example 3.6 (Generalized Semi-Naive Evaluation).

The naïve evaluation algorithm for (positive) Datalog re-discovers each fact
from step $t$ again at steps $t+1,t+2,\ldots$ The semi-naive algorithm aims at
avoiding this, by computing only the new facts. We generalize the semi-naive
evaluation from the Boolean semiring to any ordered pre-semiring $\bm{S}$, and
prove its correctness using the FGH-rule. We require $\bm{S}$ to be a complete
distributive lattice and $\oplus$ to be idempotent, and define the “minus”
operation as: $b\ominus
a\stackrel{{\scriptstyle\text{def}}}{{=}}\bigwedge\\{{c}\mid{b\preceq a\oplus
c}\\}$, then prove using the FGH-rule that the following two programs are
equivalent:

$\displaystyle\begin{array}[]{ll|lll}\Pi_{1}:&&\Pi_{2}:&&\\\
&X_{0}:=\emptyset;&&Y_{0}:=\emptyset;&\Delta_{0}:=F(\emptyset)\ominus\emptyset;\
\ \ \ //=F(\emptyset)\\\ &\texttt{loop }X_{t}:=F(X_{t-1});&&\texttt{loop
}&Y_{t}:=Y_{t-1}\oplus\Delta_{t-1};\\\ &&&&\Delta_{t}:=F(Y_{t})\ominus
Y_{t};\end{array}$

To prove their equivalence, we define
$G(X)\stackrel{{\scriptstyle\text{def}}}{{=}}(X,F(X)\ominus X)$,
$H(X,\Delta)\stackrel{{\scriptstyle\text{def}}}{{=}}(X\oplus\Delta,F(X\oplus\Delta)\ominus(X\oplus\Delta))$,
and then we prove that $G(F(X))=H(G(X))$ by exploiting the fact that $\bm{S}$
is a complete distributive lattice. In practice, we compute the difference
$\Delta_{t}=F(Y_{t})\ominus Y_{t}=F(Y_{t-1}\oplus\Delta_{t-1})\ominus
F(Y_{t-1})$ using an efficient differential rule that computes $\delta
F(Y_{t-1},\Delta_{t-1})=F(Y_{t-1}\oplus\Delta_{t-1})\ominus F(Y_{t-1})$, where
$\delta F$ is an incremental update query for $F$, i.e., it satisfies the
identity $F(Y)\oplus\delta F(Y,\Delta)=F(Y\oplus\Delta)$.

Thus, semi-naive query evaluation generalizes from standard Datalog over the
Booleans to $\text{\sf Datalog}^{\circ}$ over any complete distributive
lattice with idempotent $\oplus$, and, moreover, is a special case of the FGH-
rule. However, the semi-naive program (more precisely, function $H$) is no
longer monotone, while our synthesizer (described in Sec. 6) is currently
restricted to infer only monotone functions $H$. For that reason we do not
synthesize the semi-naive algorithm; instead we apply it using pattern-
matching as the last optimization step.

###  3.2. Loop Invariants

More advanced uses of the FGH-rule require a loop-invariant, $\phi(X)$. By
refining Theorem 3.1 with a loop invariant we obtain the following corollary:

###### Corollary 3.7.

Let $\phi(X)$ be any predicate satisfying the following three conditions:

(9) $\displaystyle\phi(X_{0})$ (10)
$\displaystyle\phi(X)\Rightarrow\phi(F(X))$ (11)
$\displaystyle\phi(X)\Rightarrow\left(G(F(X))=H(G(X))\right)$

then the FG-program (3) is equivalent to the GH-program (4).

To prove the corollary, we consider the restriction of the function $F$ to
values $X$ that satisfy $\phi$. Conditions (9) and (10) state that $\phi$ is a
loop invariant for the FG-program (3), while condition (11) is the FGH-rule
applied to the restriction of $F$ to $\phi$.

###### Example 3.8 (Beyond Magic).

By using loop-invariants, we can perform optimizations that are more powerful
than standard magic set rewritings. For a simple illustration, consider the
following program:

(12) $\displaystyle\Pi_{1}:$ $\displaystyle TC(x,y)\text{ :- }$
$\displaystyle[x=y]\vee\exists z(E(x,z)\wedge TC(z,y))$ $\displaystyle
Q(y)\text{ :- }$ $\displaystyle TC(a,y)$

which we want to optimize to:

(13) $\displaystyle\Pi_{2}:$ $\displaystyle Q(y)\text{ :- }$
$\displaystyle[y=a]\vee\exists z(Q(z)\wedge E(z,y))$

Unlike the simple magic program in Example 3.5, here rule (12) is right-
recursive. As shown in (Beeri and Ramakrishnan, 1991), the magic set
optimization using the standard sideways information passing optimization
(Abiteboul et al., 1995) yields a program that is more complicated than our
program (13). Indeed, consider a graph that is simply a directed path
$a_{0}\rightarrow a_{1}\rightarrow\dots\rightarrow a_{n}$ with $a=a_{0}$.
Then, even with magic set optimization, the right-recursive rule (12) needs to
derive quadratically many facts of the form $T(a_{i},a_{j})$ for $i\leq j$,
whereas the optimized program (13) can be evaluated in linear time. Note also
that the FGH-rule cannot be applied directly to prove that the program (12) is
equivalent to (13). To see this, denote by
$P_{1}\stackrel{{\scriptstyle\text{def}}}{{=}}G(F(TC))$ and
$P_{2}\stackrel{{\scriptstyle\text{def}}}{{=}}H(G(TC))$, and observe that
$P_{1},P_{2}$ are defined as:

$\displaystyle P_{1}(y)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle[y=a]\vee\exists z(E(a,z)\wedge TC(z,y))$ $\displaystyle
P_{2}(y)\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle[y=a]\vee\exists z(TC(a,z)\wedge E(z,y))$

In general, $P_{1}\neq P_{2}$. The problem is that the FGH-rule requires that
$G(F(TC))=H(G(TC))$ for every input $TC$, not just the transitive closure of
$E$. However, the FGH-rule does hold if we restrict $TC$ to relations that
satisfy the following loop-invariant $\phi(TC)$:

(14) $\displaystyle\exists z_{1}(E(x,z_{1})\wedge
TC(z_{1},y))\Leftrightarrow\exists z_{2}(TC(x,z_{2})\wedge E(z_{2},y))$

If $TC$ satisfies this predicate, then it follows immediately that
$P_{1}=P_{2}$, allowing us to optimize the program (12) to (13). It remains to
prove that $\phi$ is indeed an invariant for the function $F$. The base case
(9) holds because both sides of (14) are empty when $TC=\emptyset$. It remains
to check $\phi(TC)\Rightarrow\phi(F(TC))$. Let us denote
$TC^{\prime}\stackrel{{\scriptstyle\text{def}}}{{=}}F(TC)$, then we need to
check that, if (14) holds, then the predicate
$\Psi_{1}(x,y)\stackrel{{\scriptstyle\text{def}}}{{=}}\exists
z_{1}(E(x,z_{1})\wedge TC^{\prime}(z_{1},y))$ is equivalent to the predicate
$\Psi_{2}(x,y)\stackrel{{\scriptstyle\text{def}}}{{=}}\exists
z_{2}(TC^{\prime}(x,z_{2})\wedge E(z_{2},y))$. We expand both predicates in
Fig. 4, where we renamed $z$ to $z_{2}$ in the last line of $\Psi_{1}$, and
renamed $z$ to $z_{1}$ in $\Psi_{2}$. Their equivalence follows from the
assumption (14).

$\displaystyle\Psi_{1}(x,y)\equiv$ $\displaystyle\exists
z_{1}\left(E(x,z_{1})\wedge\left([z_{1}=y]\vee\exists z(E(z_{1},z)\wedge
TC(z,y))\right)\right)$ $\displaystyle\equiv$ $\displaystyle\exists
z_{1}\left(E(x,z_{1})\wedge[z_{1}=y]\vee E(x,z_{1})\wedge\exists
z(E(z_{1},z)\wedge TC(z,y))\right)$ $\displaystyle\equiv$ $\displaystyle
E(x,y)\vee\exists z_{1}(E(x,z_{1})\wedge\exists z(E(z_{1},z)\wedge TC(z,y)))$
$\displaystyle\equiv$ $\displaystyle E(x,y)\vee\exists
z_{1}(E(x,z_{1})\wedge\exists z_{2}(E(z_{1},z_{2})\wedge TC(z_{2},y)))$
$\displaystyle\Psi_{2}(x,y)\equiv$ $\displaystyle\exists
z_{2}\left(\left([x=z_{2}]\vee\exists z(E(x,z)\wedge TC(z,z_{2}))\right)\wedge
E(z_{2},y)\right)$ $\displaystyle\equiv$ $\displaystyle E(x,y)\vee\exists
z,z_{2}(E(x,z)\wedge TC(z,z_{2})\wedge E(z_{2},y))$ $\displaystyle\equiv$
$\displaystyle E(x,y)\vee\exists z(E(x,z)\wedge\exists z_{2}(TC(z,z_{2})\wedge
E(z_{2},y)))$ $\displaystyle\equiv$ $\displaystyle E(x,y)\vee\exists
z_{1}(E(x,z_{1})\wedge\exists z_{2}(TC(z_{1},z_{2})\wedge E(z_{2},y)))$

Figure 4. Predicates $\Psi_{1}$ and $\Psi_{2}$ from Example 3.8.

###  3.3. Semantic Optimization Under Constraints

Semantic optimization refers to optimization rules that hold when the database
satisfies certain constraints (Ramakrishnan and Srivastava, 1994). For
example, most database systems today can optimize key/foreign-key joins by
simply removing the join when the table containing the key is not used
anywhere else in the query.

A priori knowledge on the structure of the underlying data may often provide
additional potential for optimization. For instance, in (Bancilhon et al.,
1986), the counting and reverse counting methods are presented to further
optimize the same-generation program if it is known that the underlying graph
is acyclic. We present a principled way of exploiting such a priori knowledge.
As we show here, recursive queries have the potential to use global
constraints on the data during semantic optimization; for example, the query
optimizer may exploit the fact that the graph is a tree, or the graph is
connected.

Let $\Gamma$ denote a set of constraints on the EDBs. Then, the FGH-rule (5)
needs to be be checked only for EDBs that satisfy $\Gamma$. We illustrate this
with an example:

###### Example 3.9 (Semantic Optimization).

Consider a hierarchy of subparts consisting of two relations:
$\texttt{SubPart}(x,y)$ indicates that $y$ is a subpart of $x$, and
$\texttt{Cost}[x]\in\mathbb{N}$ represents the cost of the part $x$. We want
to compute, for each $x$, the total cost $Q[x]$ of all its subparts, sub-
subparts, etc. Since the hierarchy can, in general, be a DAG, we first need to
compute the transitive closure, before summing up the costs of all subparts,
sub-subparts, etc:

(15) $\displaystyle\Pi_{1}:$ $\displaystyle S(x,y)\text{ :- }$
$\displaystyle[x=y]\vee\exists
z\left(S(x,z)\wedge\texttt{SubPart}(z,y)\right)$ $\displaystyle Q[x]\text{ :-
}$ $\displaystyle\sum_{y}\\{{\texttt{Cost}[y]}\mid{S(x,y)}\\}$

The first rule, defining the $S$ predicate, is over the $\mathbb{B}$ semiring,
while the second rule, defining $Q$, is over the $\mathbb{N}_{\bot}$ semiring.
Consider now the case when our subpart hierarchy is a tree. Then, we can
compute the total cost much more efficiently, using the following program:

(16) $\displaystyle\Pi_{2}:$ $\displaystyle Q[x]\text{ :- }$
$\displaystyle\texttt{Cost}[x]+\sum_{z}\\{{Q[z]}\mid{\texttt{SubPart}(x,z)}\\}$

Optimizing the program (15) to (16) is an instance of semantic optimization,
since this only holds if the database instance is a tree. We do this in three
steps. We define the constraint $\Gamma$ stating that the data is a tree;
using $\Gamma$ we infer a loop-invariant $\Phi$ of the program $\Pi_{1}$;
using $\Gamma$ and $\Phi$ we prove the FGH-rule, concluding that $\Pi_{1}$ is
equivalent to $\Pi_{2}$.

The constraint $\Gamma$ is the conjunction of the following statements:

(17) $\displaystyle\forall
x_{1},x_{2},y\left(\texttt{SubPart}(x_{1},y)\wedge\texttt{SubPart}(x_{2},y)\Rightarrow
x_{1}=x_{2}\right)$ (18) $\displaystyle\forall
x,y\left(\texttt{SubPart}(x,y)\Rightarrow T(x,y)\right)$ (19)
$\displaystyle\forall x,y,z\left(T(x,z)\wedge\texttt{SubPart}(z,y)\Rightarrow
T(x,y)\right)$ (20) $\displaystyle\forall x,y\left(T(x,y)\Rightarrow x\neq
y\right)$

The first asserts that $y$ is a key in $\texttt{SubPart}(x,y)$. The last three
are an Existential Second Order Logic (ESO) statement: they assert that there
exists some relation $T(x,y)$ that contains SubPart, is transitively closed,
and irreflexive. Next, we infer the following loop-invariant of the program
$\Pi_{1}$:

(21) $\displaystyle\Phi:S(x,y)\Rightarrow[x=y]\vee T(x,y)$

Finally, we check the FGH-rule, under the assumptions $\Gamma,\Phi$. Denote by
$P_{1}\stackrel{{\scriptstyle\text{def}}}{{=}}G(F(S))$ and
$P_{2}\stackrel{{\scriptstyle\text{def}}}{{=}}H(G(S))$. To prove $P_{1}=P_{2}$
we simplify $P_{1}$ using the assumptions $\Gamma,\Phi$, as shown in Fig. 5.
We explain each step. Line 2-3 are inclusion/exclusion. Line 4 uses the fact
that the term on line 3 is $=0$, because the loop invariant implies:

$\displaystyle S(x,z)\wedge\texttt{SubPart}(z,y)$
$\displaystyle\Rightarrow([x=z]\vee T(x,z))\wedge\texttt{SubPart}(z,y)$ by
(21)
$\displaystyle\equiv\texttt{SubPart}(x,y)\vee(T(x,z)\wedge\texttt{SubPart}(z,y))$
$\displaystyle\Rightarrow T(x,y)\vee T(x,y)$ by (19) $\displaystyle\equiv
T(x,y)$ $\displaystyle\Rightarrow x\neq y$ by (20)

Line 5 follows from the fact that $y$ is a key in $\texttt{SubPart}(z,y)$. A
direct calculation of $P_{2}=H(G(S))$ results in the same expression as line 5
of Fig. 5, proving that $P_{1}=P_{2}$.

$\displaystyle P_{1}[x]=$
$\displaystyle\sum_{y}\\{{\texttt{Cost}[y]}\mid{[x=y]\vee\exists
z\left(S(x,z)\wedge\texttt{SubPart}(z,y)\right)}\\}$ $\displaystyle=$
$\displaystyle\texttt{Cost}[x]+\sum_{y}\\{{\texttt{Cost}[y]}\mid{\exists
z\left(S(x,z)\wedge\texttt{SubPart}(z,y)\right)}\\}$ $\displaystyle\ \ \
-\sum_{y}\\{{\texttt{Cost}[y]}\mid{[x=y]\wedge\exists
z\left(S(x,z)\wedge\texttt{SubPart}(z,y)\right)}\\}$ $\displaystyle=$
$\displaystyle\texttt{Cost}[x]+\sum_{y}\\{{\texttt{Cost}[y]}\mid{\exists
z\left(S(x,z)\wedge\texttt{SubPart}(z,y)\right)}\\}$ $\displaystyle=$
$\displaystyle\texttt{Cost}[x]+\sum_{y}\sum_{z}\\{{\texttt{Cost}[y]}\mid{\left(S(x,z)\wedge\texttt{SubPart}(z,y)\right)}\\}$

Figure 5. Transformation of
$P_{1}\stackrel{{\scriptstyle\text{def}}}{{=}}G(F(S))$ in Example 3.9.

##  4\. Architecture of FGH-Optimization

Figure 6. The architecture of the FGH-optimizer. The input is the unoptimized
program $\Pi_{1}$, consisting of the functions $F,G$ and the database
constraint $\Gamma$. The output consists of the optimized program $\Pi_{2}$,
see Eq. (6). Blue boxes are described in Section 6 and the green boxes in
Section 7. The yellow box (generalized semi-naive optimization) is described
in Section 3.1. The red boxes represent three state-of-the-art systems:
Rosette is a CEGIS system (Solar-Lezama et al., 2006; Torlak and Jackson,
2007; Torlak and Bodík, 2013), z3 is an SMT solver (de Moura and Bjørner,
2008), and EGG is an EQSAT system (Willsey et al., 2021).

In the rest of the paper we describe our synthesis-based FGH-optimizer, whose
architecture is shown in Fig. 6. We optimize one stratum at a time. We denote
by $\Pi_{1}$ one stratum of the input program, denote by $X$ its recursive
IDBs, by $Y$ its output IDBs, and by $F,G$ the ICO and the output operator
respectively; see Eq. (6). The optimizer also takes as input a database
constraint, $\Gamma$. The optimizer starts by inferring the loop invariant
$\Phi$; this is discussed in Sec. 7. Next, the optimizer needs to find $H$
such that $\Gamma\wedge\Phi\models\left(G(F(X))=H(G(X))\right)$. To reduce
clutter we will often abbreviate this to
$\Gamma\models\left(G(F(X))=H(G(X))\right)$, assuming that $\Gamma$
incorporates $\Phi$. The optimizer makes two attempts at synthesizing $H$: it
first tries using a simpler rule-based synthesizer, and, if that fails, then
it tries the state-of-the-art Counterexample-Guided Inductive Synthesis
(CEGIS). This is described in Sec. 6. Finally, $H$ (or the original program if
the FGH-optimization failed) is further transformed using generalized semi-
naive optimization, as we already described in Sec. 3.1. Notice that
stratification ensures that no interpreted functions are applied to the IDBs
$X$; they can still be applied to the EDBs, or occur in predicates.

The FGH-optimization is an instance of query rewriting using views (Halevy,
2001; Goldstein and Larson, 2001). Denoting by
$Q\stackrel{{\scriptstyle\text{def}}}{{=}}G(F(X))$ and
$V\stackrel{{\scriptstyle\text{def}}}{{=}}G(X)$, one has to rewrite the query
$Q$ using the view(s) $V$, in other words $Q=H(V)$. This is a total rewriting,
in the sense that $H$ is no longer allowed to refer to the IDBs $X$. This
problem is NP-complete for UCQs with set semantics (Levy et al., 1995), in NP
for UCQs with bag semantics555This follows from the fact that, under bag
semantics, two UCQ queries are equivalent iff they are isomorphic. (Green,
2009; Wang et al., 2020a)., and undecidable for realistic SQL queries that
include aggregates and arithmetic (Goldstein and Larson, 2001). Systems that
support query rewriting using views are rule-based, and apply a set of hand
crafted, predefined patterns; our first attempt to synthesize $H$ is also
rule-based. Such synthesizers usually cannot take advantage of database
constraints, but we will show in Sec. 7 how to exploit the constraint $\Gamma$
in the rule-based synthesizer. However, rule-based rewriting explores a
limited space, which is insufficient for many FGH-optimizations. In a seminal
paper (Solar-Lezama et al., 2006) Solar-Lezama proposed an alternative to
rule-based transformation, called Counterexample-Guided Inductive Synthesis,
CEGIS: the synthesizer produces potentially incorrect candidates, and an SMT
solver verifies their correctness. In the FGH-optimizer we use a program
synthesizer, Rosette (Torlak and Bodík, 2013), to synthesize $H$.

At a conceptual level, program synthesis has two abstract steps: generate $H$,
and verify $G(F(X))=H(G(X))$. While the verifier is not used explicitly, it is
used implicitly in the synthesizer, and we describe it in Sec. 5. Then we
describe the synthesizer in Sec. 6.

##  5\. Verification

We introduced the FGH-rule in Sec. 3 and showed several examples. In order to
apply the rule, one needs to check the identity (5), $F(G(X))=G(H(X))$. In
this section we describe how we verify this identity. This step is implicit in
both boxes Rule-based Synthesis and CEGIS in Fig 6. The identity can be
checked in one of two ways: by applying a predefined set of identity rules (as
currently done by most query optimizers), or by using an SMT solver.

###  5.1. Rule-based Test

Let $P_{1}=G(F(X))$, $P_{2}=H(G(X))$. To check $P_{1}=P_{2}$, the rule-based
test first normalizes both expressions into a sum-sum-product expression (Eq.
(2)) via the semiring axioms, then checks if the expressions are isomorphic:
if yes, then $P_{1}=P_{2}$, otherwise we assume $P_{1}\neq P_{2}$. The
treatment of a constraint $\Gamma$ will be discussed in Sec. 7. This test can
be visualized as follows:

(22) $\displaystyle
P_{1}\xrightarrow[]{\text{axioms}}\text{normalize}(P_{1})\simeq\text{normalize}(P_{2})\xleftarrow[]{\text{axioms}}P_{2}$

where $\simeq$ denotes isomorphism. The Rule-based test is sound. When both
$P_{1},P_{2}$ are over the $\mathbb{N}^{\infty}$ semiring and have no
interpreted functions then it is also complete (Green, 2009; Wang et al.,
2020a). This simple test motivates the need for a complete set of axioms that
allows any semiring expression to be normalized. The axioms include standard
semiring axioms, and axioms about summations and free variables fv. For
example, in order to prove $CC_{1}=CC_{2}$ in Example 3.3 (with semiring
notation in Figure 7) one needs all three axioms below:

(23) $\displaystyle\bigoplus_{x}\bigoplus_{y}\left(\cdots\right)=\ $
$\displaystyle\bigoplus_{x,y}\left(\cdots\right)$ (24) $\displaystyle
A\otimes\bigoplus_{x}B=\ $ $\displaystyle\bigoplus_{x}A\otimes B\text{ when
}x\not\in\texttt{fv}(A)$ (25)
$\displaystyle\bigoplus_{x}\left(A(x)\otimes[x=y]\right)=\ $ $\displaystyle
A(y)$

$\displaystyle CC_{1}[x]$
$\displaystyle=\bigoplus_{y}L[y]\otimes\big{(}[x=y]_{\infty}^{0}\oplus\bigoplus_{z}[E(x,z)]_{\infty}^{0}\otimes[TC(z,y)]_{\infty}^{0}\big{)}$
$\displaystyle CC_{2}[x]$
$\displaystyle=L[x]\oplus\bigoplus_{y}\big{(}\bigoplus_{y^{\prime}}L[y^{\prime}]\otimes[TC(y,y^{\prime})]_{\infty}^{0}\big{)}\otimes[E(x,y)]_{\infty}^{0}$

Figure 7. $CC_{1}$ and $CC_{2}$ in semiring notation; their normal forms are
isomorphic.

###  5.2. SMT Test

When the expressions $P_{1},P_{2}$ are over a semiring other than
$\mathbb{N}^{\infty}$, or they contain interpreted functions, then the rule-
based test is insufficient and we use an SMT solver for our verifier. We still
normalize the expressions using our axioms, because today’s solvers cannot
reason about bound/free variables (as needed in axioms (23)-(25)). The SMT
test is captured by the following figure:

(26) $\displaystyle
P_{1}\xrightarrow[]{\text{axioms}}\text{normalize}(P_{1})\xleftrightarrow{\text{SMT}}$
$\displaystyle\text{normalize}(P_{2})\xleftarrow[]{\text{axioms}}P_{2}$

###### Example 5.1 (APSP100).

Consider a labeled graph $E$ where $E[x,y]$ represents the cost of the edge
$x,y$. The following query over Trop computes the all-pairs shortest path up
to length of 100:

$\displaystyle D[x,y]\text{ :- }$ $\displaystyle\texttt{if }x=y\texttt{ then
}0\texttt{ else }\min_{z}\left(D[x,z]+E[z,y]\right)$ (27) $\displaystyle
Q[x,y]\text{ :- }$ $\displaystyle\min(D[x,y],100)$

The program is inefficient because it first computes the full path length,
only to cap it later to 100. By using the FGH-rule we get:

(28) $\displaystyle Q[x,y]\text{ :- }$ $\displaystyle\texttt{if }x=y\texttt{
then }0\texttt{ else }\min\left(\min_{z}\left(Q[x,z]+E[z,y]\right),100\right)$

We show how to verify that (28) is equivalent to (27). Denote by
$P_{1}\stackrel{{\scriptstyle\text{def}}}{{=}}G(F(D))$ and
$P_{2}\stackrel{{\scriptstyle\text{def}}}{{=}}H(G(D))$ (where $F,G,H$ are the
obvious functions in the two programs defining $Q$). After we de-sugar,
convert to semiring expressions, and normalize, they become:

$\displaystyle P_{1}[x,y]$
$\displaystyle=\left(0\otimes[x=y]_{\infty}^{0}\right)\oplus\left(\bigoplus_{z}D[x,z]\otimes
E[z,y]\right)\oplus 100$ $\displaystyle P_{2}[x,y]$
$\displaystyle=\left(0\otimes[x=y]_{\infty}^{0}\right)\oplus\left(\bigoplus_{z}D[x,z]\otimes
E[z,y]\right)\oplus\left(100\otimes\bigoplus_{z}E[z,y]\right)\oplus 100$

In the normalized expressions we push the summations past the joins, i.e., we
apply rule (24) from right to left, thus we write
$100\otimes\bigoplus(\cdots)$ instead of $\bigoplus(100\otimes\cdots)$: we
give the rationale below. At this point, the normalized $P_{1}$ and $P_{2}$
are not isomorphic, yet they are equivalent if they are interpreted in Trop.
We explain below in detail how the solver can check that. In this particular
semiring, the identity $100=\left(100\otimes\bigoplus_{z}E[z,y]\right)\oplus
100$ holds since it becomes $100=\min(100+\min_{z}E[z,y],100)$ with
$E[z,y]\geq 0$, once we replace the uninterpreted operators $\oplus,\otimes$
with $\min,+$.

Implementation We describe how we implemented the SMT test $\Gamma\models
P_{1}=P_{2}$ using a solver, now also taking the database constraint $\Gamma$
into account, where $P_{1},P_{2}$ are the expressions $G\circ F$ and $H\circ
G$. We used the z3 solver (de Moura and Bjørner, 2008), but our discussion
applies to other solvers as well. We need to normalize $P_{1},P_{2}$ before
using the solver, because solvers require all axioms to be expressed in First
Order Logic. They cannot encode the axioms (23)-(25), because they are
referring to free variables, which is a meta-logical condition not expressible
in First Order Logic. Once normalized, we encode the equality as a first-order
logic formula, and assert its negation, asking the solver to check if
$\Gamma\wedge\left(P_{1}\neq P_{2}\right)$ is satisfiable. The solver returns
UNSAT, a counterexample, or UNKNOWN. UNSAT means the identity holds. When it
returns a counterexample, then the identity fails, and the counterexample is
given as input to the synthesizer (Sec. 6). UNKNOWN means that it could
neither prove nor disprove the equivalence and we assume $P_{1}\neq P_{2}$.
For the theory of reals with $+,*$, despite its decidability, z3 often timed
out in our experiments. We therefore used the theory of integers, and z3 never
timed out or returned UNKNOWN in our experiments.

We encode every $\bm{S}$-relation $R(x_{1},\dots,x_{n})$ as an uninterpreted
function $R:\mathbb{N}\times\cdots\times\mathbb{N}\rightarrow\bm{S}$, where
$\bm{S}$ is the interpreted semiring, i.e., $\mathbb{B}$, Trop,
$\mathbb{N}^{\infty}$, etc. We represent natural numbers as integers with
nonnegativity assertions, and represent the sets
$\mathbb{N}^{\infty},\mathbb{N}_{\bot},\mathbb{R}_{\bot}$ as union types.
Operators supported by the solver, like $+,*,\min,-$, are entered unchanged;
we treat other operators as uninterpreted functions. Unbounded aggregation,
like $\bigoplus_{x}e(x)$, poses a challenge: there is no such operation in any
SMT theory. Here we use the fact that $P_{1}$ and $P_{2}$ are normalized sum-
sum-product expressions:

$\displaystyle P_{1}=$
$\displaystyle\left(\bigoplus_{x_{1}}e_{1}\right)\oplus\left(\bigoplus_{x_{2}}e_{2}\right)\oplus\cdots$
$\displaystyle P_{2}=$
$\displaystyle\left(\bigoplus_{x_{1}^{\prime}}e_{1}^{\prime}\right)\oplus\left(\bigoplus_{x_{2}^{\prime}}e_{2}^{\prime}\right)\oplus\cdots$

Assume first that each $x_{i}$ is a single variable. We ensure that all the
variables $x_{1},x_{2},\ldots$ in $P_{1}$ are distinct, by renaming them if
necessary. Next, we replace each expression $\bigoplus_{x_{i}}e_{i}$ with
$u(x_{i},e_{i})$ where $u$ is an uninterpreted function. Finally, we ask the
solver to check

$\displaystyle\Gamma\models\left(u(x_{1},e_{1})\oplus
u(x_{2},e_{2})\oplus\cdots=u(x_{1}^{\prime},e_{1}^{\prime})\oplus
u(x_{2}^{\prime},e_{2}^{\prime})\oplus\cdots\right)$

This procedure is sound, because if the identity
$u(x,e)=u(x^{\prime},e^{\prime})$ holds, then $x=x^{\prime}$ (they are the
same variable) and $e=e^{\prime}$, which means that
$\bigoplus_{x}e=\bigoplus_{x^{\prime}}e^{\prime}$. Moreover, when synthesizing
$P_{2}$, we will ensure that the generator includes the variables
$x_{1},x_{2},\ldots$ present in $P_{1}$ to achieve a limited form of
completeness, see Sec. 6. Finally, if a summation is over multiple variables,
we simply nest the uninterpreted function, i.e., write $\bigoplus_{x,y}e$ as
$u(x,u(y,e))$.

###### Example 5.2.

We now finish Example 5.1. After introducing the uninterpreted functions
described above, we obtain:

$\displaystyle P_{1}=$ $\displaystyle\min(0+w(x,y),u(z,D[x,z]+E[z,y]),100)$
$\displaystyle P_{2}=$
$\displaystyle\min(0+w(x,y),u(z,D[x,z]+E[z,y]),100+u(z,E[z,y]),100)$

where $w(x,y)$ is an uninterpreted function representing $[x=y]_{\infty}^{0}$,
and $u$ is our uninterpreted function encoding summation. The solver proves
that the two expressions are equal, given that $w\geq 0$ and $u\geq 0$. Notice
that it was critical to factorize the term 100: had we not done that, then the
expression $100+u(z,E[z,y])$ would be $u(z,100+E[z,y])$ and the identity
$P_{1}=P_{2}$ no longer holds.

Discussion Readers unfamiliar with First Order Logic may be puzzled by our
statement that the identity $u(x,e)=u(x^{\prime},e^{\prime})$ holds iff
$x=x^{\prime}$ and $e=e^{\prime}$. In order to explain this, it helps to first
review the basic definitions of validity and satisfiability in logic. A
statement is “valid” if it is true for all interpretations of its
uninterpreted symbols. For example, the equality $f(x)+y=y+f(x)$ is valid over
integers, because it holds for all function $f$ and all values of $x$ and $y$.
A statement is “satisfiable” if there exists interpretations of its
uninterpreted symbols that make the statement true. A statement is valid iff
its negation is not satisfiable. In our case, the statement
$u(x,e)=u(x^{\prime},e^{\prime})$ is valid if the equality is true for all
possible interpretations of $u,x,x^{\prime}$. For example, suppose we asked
the solver to check whether $u(x,2(x+1))=u(y,2y+2)$ is valid. To answer this
question, we negate the statement and ask the z3 solver whether the negation
is satisfiable: $u(x,2(x+1))\neq u(y,2y+2)$. One can easily satisfy this with
pen and paper, e.g., $x=1,y=2,u(a,b)=a+b$, then $u(x,2(x+1))=5$,
$u(y,2y+2)=8$. z3 also answers “yes”, and provides the following example for
the inequality666Please refer to the documentation of z3 for how models for
uninterpreted functions are constructed.:

$x=0,y=38,u(a,b)=\text{if }a=38\wedge b=78\text{ then }6\text{ else }4$

Therefore, the identity $u(x,2(x+1))=u(y,2y+2)$ is not valid. In contrast,
suppose we asked the solver whether $u(x,2(x+1))=u(x,2x+2)$ is valid. Its
negation is $u(x,2(x+1))\neq u(x,2x+2)$, and z3 returns UNSAT, which means
that the identity is valid. In general, the identity
$u(x,e)=u(x^{\prime},e^{\prime})$ is valid iff $x=x^{\prime}$ and
$e=e^{\prime}$.

##  6\. Synthesis

We have seen in Sec. 5 how to use an SMT solver to check the identity
$G(F(X))=H(G(X))$. We are now ready to discuss the core of the FGH-optimizer:
given only the query expressions $F,G$, find an expression $H$ such that the
identity $G(F(X))=H(G(X))$ holds; recall that we denote these expressions by
$P_{1},P_{2}$. As for verification, this can be done by using only rewriting,
or using program synthesis with an SMT solver. We are also given a database
constraint $\Gamma$, and we assume that we have already added to it the loop
invariant $\Phi$.

###  6.1. Rule-based Synthesis

The optimizer first attempts to synthesize $H$ using rule-based rewriting.
This process is akin to our initial verifier that relies only on normalization
and isomorphism checking.

(29) $\displaystyle
P_{1}\xrightarrow[]{\text{axioms}}\text{normalize}(P_{1})\xrightarrow[]{\text{axioms}}P_{2}$

There is no obvious way to “denormalize” an expression, since many expressions
can share the same normal form. We used for this purpose an equality
saturation system (EQSAT), which we also used for multiple tasks of the FGH-
optimizer, see Fig 6. We describe EQSAT in Sec. 7.

###  6.2. Counterexample-based Synthesis

The rule-based synthesis (29) explores only correct rewritings $P_{2}$, but
its space is limited by the hand-written axioms. The alternative approach,
pioneered in the programming language community (Solar-Lezama et al., 2006),
is to synthesize candidate programs $P_{2}$ from a much larger space, then
using an SMT solver to verify their correctness. This technique, called
Counterexample-Guided Inductive Synthesis, or CEGIS, can find rewritings
$P_{2}$ even in the presence of interpreted functions, because it exploits the
theory of the underlying domain. As a first attempt it can be described as
follows (we will revise it below):

(30) $\displaystyle
P_{1}\xrightarrow[]{\text{axioms}}\text{normalize}(P_{1})\xrightarrow[]{\textsf{CEGIS}}P_{2}$

####  6.2.1. Brief Overview of CEGIS

We give a brief overview of the CEGIS system, Rosette (Torlak and Jackson,
2007; Torlak and Bodík, 2013), that we used in our optimizer. Understanding
its working is important in order to optimize its usage for FGH-optimization.
The input to Rosette consists of a specification and a grammar, and the goal
is to synthesize a program defined by the grammar and that satisfies the
specification. The main loop is implemented with a pair of dueling SMT-
solvers, the generator and the checker. In our setting, the inputs are the
query $P_{1}$, the database constraint $\Gamma$, and a small grammar $\Sigma$
(described below). The specification is $\Gamma\models(P_{1}=P_{2})$, where
$P_{2}$ is defined by the grammar $\Sigma$. The generator generates
syntactically correct programs $P_{2}$, and the verifier checks
$\Gamma\models(P_{1}=P_{2})$. In the most naive attempt, the generator could
blindly generate candidates
$P_{2},P_{2}^{\prime},P_{2}^{\prime\prime},\ldots$, until one is found that
the verifier accepts. This is hopelessly inefficient. The first optimization
in CEGIS is that the verifier returns a small counterexample database instance
$D$ for each unsuccessful candidate $P_{2}$, i.e., $P_{1}(D)\neq P_{2}(D)$.
When considering a new candidate $P_{2}$, the generator checks that
$P_{1}(D_{i})=P_{2}(D_{i})$ holds for all previous counterexamples
$D_{1},D_{2},\ldots$, by simply evaluating the queries $P_{1},P_{2}$ on the
small instance $D_{i}$. This significantly reduces the search space of the
generator.

CEGIS applies a second optimization, where it uses the SMT solver itself to
generate the next candidate $P_{2}$, as follows. It requires a fixed recursion
depth for the grammar $\Sigma$; in other words we can assume w.l.o.g. that
$\Sigma$ is non-recursive. Then it associates a symbolic Boolean variable
$b_{1},b_{2},\ldots$ to each choice of the grammar. The grammar $\Sigma$ can
be viewed now as a BDD (binary decision diagram) where each node is labeled by
a choice variable $b_{j}$, and each leaf by a completely specified program
$P_{2}$. The search space of the generator is now completely defined by the
choice variables $b_{j}$, and Rosette uses the SMT solver to generate values
for these Boolean variables such that the corresponding program $P_{2}$
satisfies $P_{1}(D_{i})=P_{2}(D_{i})$, for all counterexample instances
$D_{i}$. This significantly speeds up the choice of the next candidate
$P_{2}$.

####  6.2.2. Using Rosette

To use Rosette, we need to define the specification and the grammar. A first
attempt is to simply define some grammar for $H$, with the specification
$\Gamma\models\left(G(F(X))=H(G(X))\right)$. This does not work, since Rosette
uses the SMT solver to check the identity: as explained in Sec. 5.2, modern
SMT solvers have limitations that require us to first normalize $G(F(X))$ and
$H(G(X))$ before checking their equivalence. Even if we modify Rosette to
normalize $H(G(X))$ during verification, there is still no obvious way to
incorporate normalization into the program generator driven by the SMT solver.
Instead, we define a grammar $\Sigma$ for $\text{normalize}(H(G(X)))$ rather
than for $H$, and then specify:

$\Gamma\models\text{normalize}(G(F(X)))=\text{normalize}(H(G(X)))$

Then, we denormalize the result returned by Rosette, in order to extract $H$,
using the denormalization module in Fig. 6, described in Sec. 7. In summary,
our CEGIS-approach for FGH-optimization can be visualized as follows:

(31) $\displaystyle
P_{1}\xrightarrow[]{\text{axioms}}\text{normalize}(P_{1})\xrightarrow[]{\textsf{CEGIS}}\text{normalize}(P_{2})\xrightarrow[]{\text{axioms}}P_{2}$

The choice of the grammar $\Sigma$ is critical for the FGH-optimizer. If it is
too restricted, then the optimizer will be limited too, if it is too general,
then the optimizer will take a prohibitive amount of time to explore the
entire space. We briefly describe our design at a high level. Recall that $X$
denotes multiple IDBs, and the query $G(X)$ may also return multiple
intermediate relations. In our system $G(X)$ is restricted to return a single
relation, so we will assume that $Y=G(X)$ is a single IDB. The expression $G$
is known to us, and is a sum-sum-product expression, see Eq. (2),

$\displaystyle G(X)=$ $\displaystyle G_{1}(X)\oplus\cdots\oplus G_{m}(X)$

where each $G_{i}(X)$ is a sum-product expression, Eq. (1), using the IDBs $X$
and/or the EDBs.

To generate $\texttt{normalize}(H(G(X)))$, we group its sum-products by the
number of occurrences of $Y$:

$\displaystyle\texttt{normalize}(H(Y))=$ $\displaystyle H^{(0)}\oplus
H^{(1)}(Y)\oplus\cdots\oplus H^{(k_{\max})}(Y)$

where $H^{(k)}$ is a sum-sum-product $H^{(k)}=Q_{1}\oplus Q_{2}\oplus\cdots$
s.t. each $Q_{i}$ contains exactly $k$ occurrences of $Y$, and an arbitrary
number of EDBs (it may not contain the IDBs $X$). We choose $k_{\max}$ as the
largest number of recursive IDBs $X$ that occur in any rule of the original
program $F(X)$, e.g., if the original program was linear, then
$k_{\max}\stackrel{{\scriptstyle\text{def}}}{{=}}1$. We obtain:

$\displaystyle\texttt{normalize}(H(G(X)))=$ $\displaystyle\ \ \ \
H^{(0)}\oplus\texttt{normalize}(H^{(1)}(G(X)))\oplus\cdots\oplus\texttt{normalize}(H^{(k_{\max})}(G(X)))$

The grammar $\Sigma$ is shown in Fig. 8. The start symbol, $A$, generates a
sum matching the expression above. $A_{0}$ generates $H^{(0)}$, which is a sum
of sum-product terms without any occurrence of $Y$. Recall from Sec. 5.2 that
the expression $u(z,Q)$ denotes $\bigoplus_{z}Q$. $E$ is one of the EDBs, and
$Z$ is a non-terminal for which we define rules $Z\rightarrow
z_{1}|z_{2}|\cdots|z_{m}|z_{1}^{\prime}|z_{2}^{\prime}\cdots$ where
$z_{1},\ldots,z_{m}$ are variables that already occur in
$\texttt{normalize}(G(F(X)))$, and $z_{1}^{\prime},z_{2}^{\prime},\ldots$ is
some fixed set of fresh variable names. $A_{k}$ generates
$\texttt{normalize}(H^{(k)}(G(X)))$, which is a sum of sum-products, each with
exactly $k$ occurrence of $Y$. As stated in Fig. 8, the rules for $A_{k}$ are
incorrect. For example consider $A_{1}$: the $m$ non-terminals
$A_{11},\ldots,A_{1m}$ should have identical derivations, instead of being
expanded independently. For example, assume $G=G_{1}\oplus G_{2}$ (thus $m=2$)
and we want $H$ to be one of $E_{1}\otimes Y$ or $E_{2}\otimes Y$ or
$E_{3}\otimes Y$. Then, $\texttt{normalize}(H(G(X)))$ can be one of the
following three expressions $E_{1}\otimes G_{1}\oplus E_{1}\otimes G_{2}$ or
$E_{2}\otimes G_{1}\oplus E_{2}\otimes G_{2}$ or $E_{3}\otimes G_{1}\oplus
E_{3}\otimes G_{2}$. However, the grammar $A_{1}\rightarrow A_{11}\oplus
A_{12}$ also generates incorrect expressions $E_{1}\otimes G_{1}\oplus
E_{2}\otimes G_{2}$, because $A_{11},A_{12}$ can choose independently the IDB
$E_{1},E_{2}$, or $E_{3}$. We fix this by exploiting the choice variables in
Rosette: we simply use the same variables in $A_{11},A_{12},\ldots$ ensuring
that all these non-terminals make exactly the same choices. We note that our
current system is restricted to linear programs, hence $k_{\max}=1$.

$\displaystyle A\rightarrow\ $ $A_{0}\oplus A_{1}\oplus\cdots\oplus
A_{k_{\max}},$ $\displaystyle A_{0}\rightarrow\ $ $Q_{0}\mid Q_{0}\oplus
A_{0},\ \ Q_{0}\rightarrow\ u(Z,Q_{0})\mid Q_{0}\otimes Q_{0}\mid
E(Z,Z,\cdots,Z),$ $\displaystyle A_{1}\rightarrow$ $A_{11}\oplus\cdots\oplus
A_{1m},\ \ A_{2}\rightarrow\ A_{211}\oplus\cdots\oplus A_{2mm},\ \
A_{3}\rightarrow A_{3111}\oplus\ldots$ $\displaystyle A_{1i}\rightarrow\ $
$\displaystyle Q_{1i}\mid Q_{1i}\oplus A_{1i},$ $\displaystyle
Q_{1i}\rightarrow\ $ $\displaystyle u(Z,Q_{1i})\mid Q_{1i}\otimes Q_{0}\mid
G_{i}(X),$ $\displaystyle i=$ $\displaystyle 1,m$ $\displaystyle
A_{2ij}\rightarrow\ $ $\displaystyle Q_{2ij}\oplus A_{2ij},$ $\displaystyle
Q_{2ij}\rightarrow\ $ $\displaystyle u(Z,Q_{2ij})\mid Q_{1i}\otimes G_{j}(X),$
$\displaystyle i,j=$ $\displaystyle 1,m$ $\displaystyle
A_{3ij\ell}\rightarrow\ $ $\displaystyle Q_{3ij\ell}\oplus A_{3ij\ell},$
$\displaystyle Q_{3ij\ell}\rightarrow\ $ $\displaystyle u(Z,Q_{3ij\ell})\mid
Q_{2ij}\otimes G_{\ell}(X),$ $\displaystyle i,j,\ell=$ $\displaystyle 1,m$

Figure 8. Grammar $\Sigma$ for $\texttt{normalize}(H(G(X)))$, for
$k_{\max}=3$.

####  6.2.3. Discussion

Even though our grammar is restricted to $k_{\max}=1$, it is more complex than
Fig 8, in order to further reduce the search space. We use more non-terminals
to better control which variables $z$ can be used where, and we also consider
the choice of including entire subexpressions that occur in the original
program $P_{1}$, since they are often reused in the optimized program. The
synthesizer would require many trials to find them, had we not included them
explicitly.

##  7\. Equality Saturation

Figure 9. Example e-graph.

Throughout the FGH-optimizer we need to manipulate expressions, apply rules,
and manage equivalent expressions. This problem is common to all query
optimizers. Instead of implementing our own expression manager, we adopt a
state-of-the-art rewriting system dubbed Equality Saturation (EQSAT).
Specifically, we used EGG (Willsey et al., 2021) to implement the green boxes
in the architecture shown in Fig. 6.

An EQSAT system maintains a data structure called an e-graph that compactly
represents a set of expressions, together with an equivalence relation over
this set. Each e-graph consists of a set of e-classes, each e-class consists
of a set of e-nodes, and each e-node is a function symbol with e-classes as
children. Figure 9 shows an e-graph representing the two expressions in Eq.
(24), their subexpressions, and other equivalent expressions. Each e-class
(dotted box) represents a class of equivalent expressions. For example e-class
5 represents $A\otimes B$ and $B\otimes A$, which are equivalent by
commutativity. e-class 6 represents four equivalent expressions (including the
two choices in e-class 5).

The EQSAT system maintains separately a collection of rules, each represented
by a pair of patterns. For example, one rule may state that $\otimes$ is
commutative: $x\otimes y=y\otimes x$. The e-graph can efficiently add a new
expression to its collection, insert a new rule, and match a given expression
against the e-graph.

We describe how we use EGG in the FGH-optimizer. First, we use it to extend
the Rule-based test (Sec. 5.1) to account for a constraint $\Gamma$. By
design, the e-graph makes it easy to infer the equivalence $P_{1}=P_{2}$ from
a set of rules. Suppose we want to check such an equivalence conditioned on
$\Gamma$. We may assume w.l.o.g. that $\Gamma$ is a logical implication,
$\Delta\Rightarrow\Theta$ since all database constraints are expressed this
way. We convert it into an equivalence $\Delta\wedge\Theta=\Delta$, and insert
it into the e-graph, then check for equivalence $P_{1}=P_{2}$.

Second, we use the e-graph to denormalize an expression. More precisely,
recall from Sec. 6.1 that we attempt to synthesize $H$ by denormalizing
$P_{1}\stackrel{{\scriptstyle\text{def}}}{{=}}\text{normalize}(F(G(X)))$, in
other words, writing it in the form $H(G(X))$. For that we add $G(X)$ to the
e-graph, observe in which e-class it is inserted, and replace that e-class
with a new node $Y$. The root of the new e-graph represents many equivalent
expressions, and each of them is a candidate for $H$. We choose the expression
$H$ that has the smallest AST and does not have any occurrence of the IDBs
$X$.

Finally, we use the e-graph to infer the loop invariants. We do this by
symbolically executing the recursive program $F$ for up to 5 iterations, and
compute the symbolic expressions of the IDBs $X$: $X_{0},X_{1},\ldots$ Using
an e-graph we represent all identities satisfied by these (distinct!)
expressions. The identities that are satisfied by every $X_{i}$ are candidate
loop invariants: for each of them we use the SMT solver to check if they
satisfy Eq. (10) from Sec. 3.2.

Program | Synthesis Type | Constraint? | Invariant? | Dataset | Size (# ops)
---|---|---|---|---|---
Beyond Magic (BM) | rule-based | No | Yes | twitter, epinions, wiki | 6
Connected Components (CC) | rule-based | No | No | twitter, epinions, wiki | 6
Single Source Shortest Path (SSSP) | rule-based | No | No | twitter, epinions, wiki | 17
Sliding Window Sum (WS) | CEGIS | No | Yes | Vector of Numbers | 15
Betweenness Centrality (BC) | CEGIS | No | No | Erdős–Rényi Graphs | 43
Graph Radius (R) | CEGIS | Yes | Yes | Random Recursive Trees | 12
Multi-level Marketing (MLM) | CEGIS | Yes | Yes | Random Recursive Trees | 6
Figure 10. Experimental Setup

Figure 11. Speedup of the optimized v.s. original program; higher is better;
t.o. means the original program timed out after 3 hours, in which case we
report the speedup against 3 hours; o.o.m. means the original program ran out
of memory. Figure 12. Runtime increase as a function of the data size; lower
is better.

Program | BM | CC | SSSP | R | MLM | BC | WS
---|---|---|---|---|---|---|---
Invariance inference | 0.092 | 0 | 0 | 0.129 | 0.132 | 0 | 0
Synthesis | 0.004 | 0.005 | 0.004 | 0.284 | 0.299 | 1.2 | 0.821
Total | 0.096 | 0.005 | 0.004 | 0.413 | 0.431 | 1.2 | 0.821
Opt. / Exec. (max-min) | .82% - .16% | .04%-.01% | .24%-.002% | .41%-.07% | .76%-.09% | 6.3%-.51% | 7.4%-.66%

Program | R | MLM | BC | WS
---|---|---|---|---
Search space | 10 | 20 | 132 | 94

Figure 13. Optimization time in seconds, optimization time over execution
time, and size of the search space.

##  8\. Evaluation

We implemented a source-to-source FGH-optimizer, based on Fig. 6. The input is
a program $\Pi_{1}$, given by $F,G$, and a database constraint $\Gamma$, and
the output is an optimized program $H$. We evaluated it on three Datalog
systems, and several programs from benchmarks proposed by prior research
(Shkapsky et al., 2016a; Fan et al., 2019); we also propose new benchmarks
that perform standard data analysis tasks. We did not modify any of the three
Datalog engines. We asked two major questions:

  1. (1)

How effective is our source-to-source optimization, given that each system
already supports a range of optimizations?

  2. (2)

How much time does the actual FGH optimization take?

###  8.1. Setup

There is a great number of commercial and open-source Datalog engines in the
wild, but only a few support aggregates in recursion. We were able to identify
five major systems with such support: SociaLite (Seo et al., 2015), Myria
(Wang et al., 2015), the DeALS family of systems (DeALS (Shkapsky et al.,
2015), BigDatalog (Shkapsky et al., 2016b), and RaDlog (Gu et al., 2019)),
RecStep (Fan et al., 2019), and Dyna (Francis-Landau et al., 2020). Prior work
(Shkapsky et al., 2016a) reports SociaLite and Myria are consistently slower
than newer systems, so we do not include them in our experiments. Dyna is
designed to experiment with novel language semantics and not for data
analytics, and we were not able to run our benchmarks without errors using it.
Systems in the DeALS family are similar to each other; we pick BigDatalog
because it is open source and runs our benchmarks without errors; we include
RecStep for the same reasons. Both BigDatalog and RecStep are multi-core
systems. Finally, we run experiments on an unreleased commercial system X,
which is single core. As we shall discuss, X is the only one that supports all
features for our benchmarks.

We conducted all experiments on a server running CentOS 8.3.2011. The server
has a total of 1008GB memory, and 4 Intel Xeon CPU E7-4890 v2 2.80GHz CPUs,
each with 15 cores and 30 threads. We ran seven benchmarks, shown in Fig 10.
BM and CC are Examples 3.8 and 3.3; MLM is basically Example 3.9. CC, SSSP and
MLM are from (Shkapsky et al., 2016a), the others are designed by us. R and
MLM require a database constraint stating that the data is a tree. BM, R, and
MLM each have a non-trivial loop invariant that is inferred by the optimizer.
Our optimizer requires each program to consist of two rules, one each for $F$
and $G$, and so a meaningful metric for program size is the number of semiring
operations. These numbers are listed in the last column of Fig 10. Our
benchmark programs are comparable in size to those used in prior work
(Shkapsky et al., 2016a; Fan et al., 2019). All programs are available in our
git repository. The real-world datasets twitter (McAuley and Leskovec, 2012),
epinions (Richardson et al., 2003), and wiki (Leskovec et al., 2010) are from
the popular SNAP collection (Leskovec and Krevl, 2014). We follow the setting
in (Shkapsky et al., 2016a; Fan et al., 2019) when generating the synthetic
graphs. We additionally generate random recursive trees with an exponential
decay, modeling the decay of association in multi-level marketing (Emek et
al., 2011). For WS, we input the vector $[1,\ldots,n]$, since the values of
the entries do not affect run time. In general, we used smaller datasets than
(Shkapsky et al., 2016a; Fan et al., 2019) because some of our experiments run
single-threaded.

###  8.2. Run Time Measurement

For each program-dataset pair, we measure the run times of three programs:
original, with the FGH-optimization, and with the FGH-optimization and the
generalized semi-naive (GSN, for short) transformation. We report only the
speedups relative to the original program in Fig. 11 and 12. In some cases the
original program timed out our preset limit of 3 hours, where we report the
speedup against the 3 hours mark. In some other cases the original program ran
out of memory and we mark them with “o.o.m.” in the figure. The absolute
runtimes are irrelevant for our discussion, since we want to report the effect
of adding our optimizations. (We also do not have permission to report the
runtimes of X.) All three systems already perform semi-naive evaluation on the
original program, since that is expressed over the Boolean semiring. But the
FGH-optimized program is over a different semiring (except for BM), and GSN
has non-stratifiable rules with negation, which are supported only by system
X; we report GSN only for system X. While the benchmarks in Fig. 11 were on
real datasets, those in Fig. 12 use synthetic data, for multiple reasons: we
did not have access to a good tree dataset needed in the R and MLM benchmarks,
BC timed out on our real data (BC is computationally expensive), and WS uses
only a simple array. A benefit of synthetic data is that we can report how the
optimizations scale with the data size. Unfortunately, the FGH-optimized
programs in Fig. 12 require recursion with SUM aggregation, which is not
supported by BigDatalog or RecStep; this is in contrast with those in Fig. 11,
which require recursion with MIN aggregation which is supported by all
systems.

####  8.2.1. Findings

Figure 11 shows the results of the first group of benchmarks optimized by the
rule-based synthesizer. Overall, we observe our optimizer provides consistent
and significant (up to 4 orders of magnitude) speedup across systems and
datasets. Only a few datapoints indicate the optimization has little effect:
BM and CC on wiki under BigDatalog, and SSSP on wiki under X. This is due to
the small size of the wiki dataset: both the optimized and unoptimized
programs finish very quickly, so the run time is dominated by system overhead
which cannot be optimized away. We also note that (under X) GSN speeds up SSSP
but slows down CC (note the log scale). The latter occurs because the
$\Delta$-relations for CC are very large, and as a result the semi-naive
evaluation has the same complexity as the naive evaluation; but the semi-naive
program is more complex and incurs a constant slowdown. GSN has no effect on
BM because the program is in the boolean semiring, and X already implements
the standard semi-naive evaluation. Optimizing BM with FGH on BigDatalog sees
a significant speedup even though the systems already implements magic set
rewrite, because the optimization depends on a loop invariant.777 BigDatalog
can optimize the left-recursive version of BM (7) to obtain similar speedup,
via the classic magic set rewrite. Overall, both the semi-naive and naive
versions of the optimized program are significantly faster than the
unoptimized program.

Figure 12 shows the results of the second group of benchmarks, which required
CEGIS. Since we used synthetic data, we examined here the asymptotic behavior
of the optimization as a function of the data size. The most advanced
optimization was for BC, which leads essentially to Brandes’ algorithm
(Brandes, 2001): its effect is dramatic. R and MLM rely on semantic
optimization for a tree. We generated two synthetic trees, a random recursive
tree with expected depth of $O(\log n)$ and one with exponential decay with
expected depth of $O(n)$. Since the benefit of the optimization depends on the
depth, we see a much better asymptotic behavior in the second case. Here, too,
the optimizations were always improving the runtime.

###  8.3. Optimization Time and the Size of the Search Space

CEGIS can quickly become very expensive if its search space is large, and, for
that reason, we have designed the grammar generator carefully to reduce the
search space without losing generality. Fig. 13 reports the runtime of the
synthesizer (in seconds) for both rule-based synthesis and CEGIS, and the size
of the search space. The rule-based synthesizer runs in milliseconds, while
CEGIS took over 1s for BC (our hardest benchmark). These numbers are close to
those demanded by modern query optimizers, and represent only a tiny portion
of the total runtime of the optimized query. Optimization time takes less than
1% of the query run time for all benchmarks except for BC and WS on the
smallest input data. To our surprise, our grammar managed to narrow the search
space considerably, to no more than 132 candidates, which (in hindsight)
explains the low optimization times. The search space can grow rapidly, and
even exponentially, as the size of the input program grows. Our optimizer
optimizes a single stratum at a time, focusing on improving critical “basic
blocks” of a program. Our benchmark programs demonstrate a wide range of data
analysis computation can be expressed succinctly using just a few semiring
operations, and optimization can have a dramatic impact on performance.

###  8.4. Summary

We conclude that our optimizer can significantly speedup already optimized
Datalog systems, either single-core or multi-core. GSN can, sometimes, further
improve the runtime. We achieved this using a rather small search space, which
led to fast optimization.

##  9\. Conclusion

We have presented a new optimization method for recursive queries, which
generalizes many previous optimizations described in the literature. We
implemented it using a CEGIS and an EQSAT system. Our experiments have shown
that this optimization is beneficial, regardless of what other optimizations a
Datalog system supports. We discuss here some limitations and future work.

Our current implementation is restricted to linear programs, but our
techniques apply to nonlinear programs as well. Non-linear programs require a
more complex grammar $\Sigma$; this is likely to increase the search space,
and possibly increase the optimization time. We leave this exploration to
future work.

Our current optimizer is heuristic-based, and future work needs to integrate
it with a cost model. This, however, will be challenging, because very little
work exists for estimating the cost of recursive queries. This paper applies a
simple cost-model. We use the arity of the IDB predicate as a proxy for a
simple asymptotic cost model, because $N^{\text{arity}}$ is the size bound of
the output, when $N$ is the size of the active domain. This simple cost-model
is currently used by the commercial DB system mentioned in the paper. If the
optimized program reduces the arity, then it is assessed to have lower cost.

Two limitations of our current implementation are the fact that we currently
do not “invent” new IDBs for the optimized query, and do not apply the FGH-
optimizer repeatedly. Both would be required in order to support more advanced
instances of magic set optimizations.

Our initial motivation for this work came from a real application, which
consists of a few hundred Datalog rules that were computationally very
expensive, and required a significant amount of manual optimizations. Upon
close examination, at a very high level, the manual optimization that we
performed could be described, abstractly, as a sliding window optimization (WS
in Fig. 10), which is one of the simplest instantiations of the FGH-rule. Yet,
our current system is far from able to optimize automatically programs with
hundreds of rules: we leave that for future work.

###### Acknowledgements.

Suciu and Wang were partially supported by NSF IIS 1907997 and NSF IIS
1954222. Pichler was supported by the Austrian Science Fund (FWF):P30930.

## References

  * (1)
  * Abiteboul et al. (1995) Serge Abiteboul, Richard Hull, and Victor Vianu. 1995\.  _Foundations of Databases_.  Addison-Wesley.  http://webdam.inria.fr/Alice/
  * Albarghouthi et al. (2017) Aws Albarghouthi, Paraschos Koutris, Mayur Naik, and Calvin Smith. 2017.  Constraint-Based Synthesis of Datalog Programs. In _Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings_ _(Lecture Notes in Computer Science, Vol. 10416)_ , J. Christopher Beck (Ed.). Springer, 689–706.  https://doi.org/10.1007/978-3-319-66158-2_44
  * Alvaro et al. (2010) Peter Alvaro, William R. Marczak, Neil Conway, Joseph M. Hellerstein, David Maier, and Russell Sears. 2010.  Dedalus: Datalog in Time and Space. In _Datalog Reloaded - First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010. Revised Selected Papers_ _(Lecture Notes in Computer Science, Vol. 6702)_ , Oege de Moor, Georg Gottlob, Tim Furche, and Andrew Jon Sellers (Eds.). Springer, 262–281.  https://doi.org/10.1007/978-3-642-24206-9_16
  * Balbin et al. (1991) Isaac Balbin, Graeme S. Port, Kotagiri Ramamohanarao, and Krishnamurthy Meenakshi. 1991.  Efficient Bottom-UP Computation of Queries on Stratified Databases.  _J. Log. Program._ 11, 3&4 (1991), 295–344.  https://doi.org/10.1016/0743-1066(91)90030-S
  * Bancilhon et al. (1986) François Bancilhon, David Maier, Yehoshua Sagiv, and Jeffrey D. Ullman. 1986.  Magic Sets and Other Strange Ways to Implement Logic Programs. In _Proceedings of the Fifth ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, March 24-26, 1986, Cambridge, Massachusetts, USA_ , Avi Silberschatz (Ed.). ACM, 1–15.  https://doi.org/10.1145/6012.15399
  * Beeri and Ramakrishnan (1991) Catriel Beeri and Raghu Ramakrishnan. 1991.  On the Power of Magic.  _J. Log. Program._ 10, 3&4 (1991), 255–299.  https://doi.org/10.1016/0743-1066(91)90038-Q
  * Brandes (2001) Ulrik Brandes. 2001\.  A faster algorithm for betweenness centrality.  _Journal of mathematical sociology_ 25, 2 (2001), 163–177.
  * Chu et al. (2017) Shumo Chu, Chenglong Wang, Konstantin Weitz, and Alvin Cheung. 2017.  Cosette: An Automated Prover for SQL. In _8th Biennial Conference on Innovative Data Systems Research, CIDR 2017, Chaminade, CA, USA, January 8-11, 2017, Online Proceedings_. www.cidrdb.org.  http://cidrdb.org/cidr2017/papers/p51-chu-cidr17.pdf
  * de Moura and Bjørner (2008) Leonardo de Moura and Nikolaj Bjørner. 2008.  Z3: An Efficient SMT Solver. In _Tools and Algorithms for the Construction and Analysis of Systems_ , C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340.
  * Deutsch et al. (1999) Alin Deutsch, Lucian Popa, and Val Tannen. 1999.  Physical Data Independence, Constraints, and Optimization with Universal Plans. In _VLDB’99, Proceedings of 25th International Conference on Very Large Data Bases, September 7-10, 1999, Edinburgh, Scotland, UK_ , Malcolm P. Atkinson, Maria E. Orlowska, Patrick Valduriez, Stanley B. Zdonik, and Michael L. Brodie (Eds.). Morgan Kaufmann, 459–470.  http://www.vldb.org/conf/1999/P44.pdf
  * Emek et al. (2011) Yuval Emek, Ron Karidi, Moshe Tennenholtz, and Aviv Zohar. 2011\.  Mechanisms for multi-level marketing. In _Proceedings of the 12th ACM conference on Electronic commerce_. 209–218.
  * Fan et al. (2019) Zhiwei Fan, Jianqiao Zhu, Zuyu Zhang, Aws Albarghouthi, Paraschos Koutris, and Jignesh M. Patel. 2019.  Scaling-Up In-Memory Datalog Processing: Observations and Techniques.  _Proc. VLDB Endow._ 12, 6 (2019), 695–708.  https://doi.org/10.14778/3311880.3311886
  * Fitting (1991) Melvin Fitting. 1991\.  Bilattices and the Semantics of Logic Programming.  _J. Log. Program._ 11, 1&2 (1991), 91–116.  https://doi.org/10.1016/0743-1066(91)90014-G
  * Francis-Landau et al. (2020) Matthew Francis-Landau, Tim Vieira, and Jason Eisner. 2020\.  Evaluation of Logic Programs with Built-Ins and Aggregation: A Calculus for Bag Relations. In _13th International Workshop on Rewriting Logic and Its Applications_. 49–63.
  * Ganguly et al. (1991) Sumit Ganguly, Sergio Greco, and Carlo Zaniolo. 1991\.  Minimum and Maximum Predicates in Logic Programming. In _Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 29-31, 1991, Denver, Colorado, USA_ , Daniel J. Rosenkrantz (Ed.). ACM Press, 154–163.  https://doi.org/10.1145/113413.113427
  * Goldstein and Larson (2001) Jonathan Goldstein and Per-Åke Larson. 2001.  Optimizing Queries Using Materialized Views: A practical, scalable solution. In _Proceedings of the 2001 ACM SIGMOD international conference on Management of data, Santa Barbara, CA, USA, May 21-24, 2001_ , Sharad Mehrotra and Timos K. Sellis (Eds.). ACM, 331–342.  https://doi.org/10.1145/375663.375706
  * Green (2009) Todd J. Green. 2009\.  Containment of conjunctive queries on annotated relations. In _Database Theory - ICDT 2009, 12th International Conference, St. Petersburg, Russia, March 23-25, 2009, Proceedings_ _(ACM International Conference Proceeding Series, Vol. 361)_ , Ronald Fagin (Ed.). ACM, 296–309.  https://doi.org/10.1145/1514894.1514930
  * Green et al. (2007) Todd J. Green, Gregory Karvounarakis, and Val Tannen. 2007\.  Provenance semirings. In _Proceedings of the Twenty-Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 11-13, 2007, Beijing, China_ , Leonid Libkin (Ed.). ACM, 31–40.  https://doi.org/10.1145/1265530.1265535
  * Grossman et al. (2017) Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, and Mooly Sagiv. 2017.  Verifying Equivalence of Spark Programs. In _Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II_ _(Lecture Notes in Computer Science, Vol. 10427)_ , Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 282–300.  https://doi.org/10.1007/978-3-319-63390-9_15
  * Gu et al. (2019) Jiaqi Gu, Yugo H. Watanabe, William A. Mazza, Alexander Shkapsky, Mohan Yang, Ling Ding, and Carlo Zaniolo. 2019.  RaSQL: Greater Power and Performance for Big Data Analytics with Recursive-aggregate-SQL on Spark. In _Proceedings of the 2019 International Conference on Management of Data, SIGMOD Conference 2019, Amsterdam, The Netherlands, June 30 - July 5, 2019_ , Peter A. Boncz, Stefan Manegold, Anastasia Ailamaki, Amol Deshpande, and Tim Kraska (Eds.). ACM, 467–484.  https://doi.org/10.1145/3299869.3324959
  * Halevy (2001) Alon Y. Halevy. 2001\.  Answering queries using views: A survey.  _VLDB J._ 10, 4 (2001), 270–294.  https://doi.org/10.1007/s007780100054
  * Huang et al. (2011) Shan Shan Huang, Todd Jeffrey Green, and Boon Thau Loo. 2011\.  Datalog and Emerging Applications: An Interactive Tutorial. In _Proceedings of the 2011 ACM SIGMOD International Conference on Management of Data_ (Athens, Greece) _(SIGMOD ’11)_. Association for Computing Machinery, New York, NY, USA, 1213–1216.  https://doi.org/10.1145/1989323.1989456
  * Khamis et al. (2021) Mahmoud Abo Khamis, Hung Q. Ngo, Reinhard Pichler, Dan Suciu, and Yisu Remy Wang. 2021\.  _Convergence of Datalog over (Pre-) Semirings_.  arXiv:2105.14435v1 [cs.DB]
  * Leskovec et al. (2010) Jure Leskovec, Daniel Huttenlocher, and Jon Kleinberg. 2010\.  Signed networks in social media. In _Proceedings of the SIGCHI conference on human factors in computing systems_. 1361–1370.
  * Leskovec and Krevl (2014) Jure Leskovec and Andrej Krevl. 2014.  SNAP Datasets: Stanford Large Network Dataset Collection.  http://snap.stanford.edu/data.
  * Levy et al. (1995) Alon Y. Levy, Alberto O. Mendelzon, Yehoshua Sagiv, and Divesh Srivastava. 1995.  Answering Queries Using Views. In _Proceedings of the Fourteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 22-25, 1995, San Jose, California, USA_ , Mihalis Yannakakis and Serge Abiteboul (Eds.). ACM Press, 95–104.  https://doi.org/10.1145/212433.220198
  * Mascellani and Pedreschi (2002) Paolo Mascellani and Dino Pedreschi. 2002.  The Declarative Side of Magic. In _Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert A. Kowalski, Part II_ _(Lecture Notes in Computer Science, Vol. 2408)_ , Antonis C. Kakas and Fariba Sadri (Eds.). Springer, 83–108.  https://doi.org/10.1007/3-540-45632-5_4
  * McAuley and Leskovec (2012) Julian J McAuley and Jure Leskovec. 2012.  Learning to discover social circles in ego networks.. In _NIPS_ , Vol. 2012. Citeseer, 548–56.
  * Mumick et al. (1990) Inderpal Singh Mumick, Sheldon J. Finkelstein, Hamid Pirahesh, and Raghu Ramakrishnan. 1990.  Magic is Relevant. In _Proceedings of the 1990 ACM SIGMOD International Conference on Management of Data, Atlantic City, NJ, USA, May 23-25, 1990_ , Hector Garcia-Molina and H. V. Jagadish (Eds.). ACM Press, 247–258.  https://doi.org/10.1145/93597.98734
  * Mumick and Pirahesh (1994) Inderpal Singh Mumick and Hamid Pirahesh. 1994.  Implementation of Magic-sets in a Relational Database System. In _Proceedings of the 1994 ACM SIGMOD International Conference on Management of Data, Minneapolis, Minnesota, USA, May 24-27, 1994_ , Richard T. Snodgrass and Marianne Winslett (Eds.). ACM Press, 103–114.  https://doi.org/10.1145/191839.191860
  * Popa et al. (2000) Lucian Popa, Alin Deutsch, Arnaud Sahuguet, and Val Tannen. 2000.  A Chase Too Far?. In _Proceedings of the 2000 ACM SIGMOD International Conference on Management of Data, May 16-18, 2000, Dallas, Texas, USA_ , Weidong Chen, Jeffrey F. Naughton, and Philip A. Bernstein (Eds.). ACM, 273–284.  https://doi.org/10.1145/342009.335421
  * Raghothaman et al. (2020) Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, and Bernhard Scholz. 2020\.  Provenance-guided synthesis of Datalog programs.  _Proc. ACM Program. Lang._ 4, POPL (2020), 62:1–62:27.  https://doi.org/10.1145/3371130
  * Ramakrishnan and Srivastava (1994) Raghu Ramakrishnan and Divesh Srivastava. 1994.  Semantics and Optimization of Constraint Queries in Databases.  _IEEE Data Eng. Bull._ 17, 2 (1994), 14–17.  http://sites.computer.org/debull/94JUN-CD.pdf
  * Richardson et al. (2003) Matthew Richardson, Rakesh Agrawal, and Pedro Domingos. 2003\.  Trust management for the semantic web. In _International semantic Web conference_. Springer, 351–368.
  * Rocktäschel ([n.d.]) Tim Rocktäschel. [n.d.].  Einsum is all you need - Einstein summation in deep learning.  https://rockt.github.io/2018/04/30/einsum.
  * Roscoe and Loo (2018) Timothy Roscoe and Boon Thau Loo. 2018.  Declarative Networking.  In _Encyclopedia of Database Systems, Second Edition_ , Ling Liu and M. Tamer Özsu (Eds.). Springer.  https://doi.org/10.1007/978-1-4614-8265-9_1220
  * Schlaipfer et al. (2017) Matthias Schlaipfer, Kaushik Rajan, Akash Lal, and Malavika Samak. 2017.  Optimizing Big-Data Queries Using Program Synthesis. In _Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, October 28-31, 2017_. ACM, 631–646.  https://doi.org/10.1145/3132747.3132773
  * Seo et al. (2015) Jiwon Seo, Stephen Guo, and Monica S. Lam. 2015.  SociaLite: An Efficient Graph Query Language Based on Datalog.  _IEEE Trans. Knowl. Data Eng._ 27, 7 (2015), 1824–1837.  https://doi.org/10.1109/TKDE.2015.2405562
  * Shkapsky et al. (2016a) Alexander Shkapsky, Mohan Yang, Matteo Interlandi, Hsuan Chiu, Tyson Condie, and Carlo Zaniolo. 2016a.  Big Data Analytics with Datalog Queries on Spark. In _Proceedings of the 2016 International Conference on Management of Data_ (San Francisco, California, USA) _(SIGMOD ’16)_. Association for Computing Machinery, New York, NY, USA, 1135–1149.  https://doi.org/10.1145/2882903.2915229
  * Shkapsky et al. (2016b) Alexander Shkapsky, Mohan Yang, Matteo Interlandi, Hsuan Chiu, Tyson Condie, and Carlo Zaniolo. 2016b.  Big Data Analytics with Datalog Queries on Spark. In _Proceedings of the 2016 International Conference on Management of Data, SIGMOD Conference 2016, San Francisco, CA, USA, June 26 - July 01, 2016_ , Fatma Özcan, Georgia Koutrika, and Sam Madden (Eds.). ACM, 1135–1149.  https://doi.org/10.1145/2882903.2915229
  * Shkapsky et al. (2015) Alexander Shkapsky, Mohan Yang, and Carlo Zaniolo. 2015\.  Optimizing recursive queries with monotonic aggregates in DeALS. In _31st IEEE International Conference on Data Engineering, ICDE 2015, Seoul, South Korea, April 13-17, 2015_ , Johannes Gehrke, Wolfgang Lehner, Kyuseok Shim, Sang Kyun Cha, and Guy M. Lohman (Eds.). IEEE Computer Society, 867–878.  https://doi.org/10.1109/ICDE.2015.7113340
  * Si et al. (2018) Xujie Si, Woosuk Lee, Richard Zhang, Aws Albarghouthi, Paraschos Koutris, and Mayur Naik. 2018\.  Syntax-guided synthesis of Datalog programs. In _Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018_ , Gary T. Leavens, Alessandro Garcia, and Corina S. Pasareanu (Eds.). ACM, 515–527.  https://doi.org/10.1145/3236024.3236034
  * Si et al. (2019) Xujie Si, Mukund Raghothaman, Kihong Heo, and Mayur Naik. 2019.  Synthesizing Datalog Programs using Numerical Relaxation. In _Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019_ , Sarit Kraus (Ed.). ijcai.org, 6117–6124.  https://doi.org/10.24963/ijcai.2019/847
  * Solar-Lezama et al. (2006) Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, and Vijay A. Saraswat. 2006.  Combinatorial sketching for finite programs. In _Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, October 21-25, 2006_ , John Paul Shen and Margaret Martonosi (Eds.). ACM, 404–415.  https://doi.org/10.1145/1168857.1168907
  * Tekle and Liu (2019) K. Tuncay Tekle and Yanhong A. Liu. 2019.  Extended Magic for Negation: Efficient Demand-Driven Evaluation of Stratified Datalog with Precise Complexity Guarantees. In _Proceedings 35th International Conference on Logic Programming (Technical Communications), ICLP 2019 Technical Communications, Las Cruces, NM, USA, September 20-25, 2019_ _(EPTCS, Vol. 306)_ , Bart Bogaerts, Esra Erdem, Paul Fodor, Andrea Formisano, Giovambattista Ianni, Daniela Inclezan, Germán Vidal, Alicia Villanueva, Marina De Vos, and Fangkai Yang (Eds.). 241–254.  https://doi.org/10.4204/EPTCS.306.28
  * Torlak and Bodík (2013) Emina Torlak and Rastislav Bodík. 2013.  Growing solver-aided languages with rosette. In _ACM Symposium on New Ideas in Programming and Reflections on Software, Onward! 2013, part of SPLASH ’13, Indianapolis, IN, USA, October 26-31, 2013_ , Antony L. Hosking, Patrick Th. Eugster, and Robert Hirschfeld (Eds.). ACM, 135–152.  https://doi.org/10.1145/2509578.2509586
  * Torlak and Jackson (2007) Emina Torlak and Daniel Jackson. 2007.  Kodkod: A Relational Model Finder. In _Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings_ _(Lecture Notes in Computer Science, Vol. 4424)_ , Orna Grumberg and Michael Huth (Eds.). Springer, 632–647.  https://doi.org/10.1007/978-3-540-71209-1_49
  * Veanes et al. (2009) Margus Veanes, Pavel Grigorenko, Peli de Halleux, and Nikolai Tillmann. 2009.  Symbolic Query Exploration. In _Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings_ _(Lecture Notes in Computer Science, Vol. 5885)_ , Karin K. Breitman and Ana Cavalcanti (Eds.). Springer, 49–68.  https://doi.org/10.1007/978-3-642-10373-5_3
  * Vianu (2021) Victor Vianu. 2021\.  Datalog Unchained. In _Proceedings of the 40th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems_ (Virtual Event, China) _(PODS’21)_. Association for Computing Machinery, New York, NY, USA, 57–69.  https://doi.org/10.1145/3452021.3458815
  * Wang et al. (2015) Jingjing Wang, Magdalena Balazinska, and Daniel Halperin. 2015\.  Asynchronous and Fault-Tolerant Recursive Datalog Evaluation in Shared-Nothing Engines.  _Proc. VLDB Endow._ 8, 12 (Aug. 2015), 1542–1553.  https://doi.org/10.14778/2824032.2824052
  * Wang et al. (2018) Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. 2018.  Verifying equivalence of database-driven applications.  _Proc. ACM Program. Lang._ 2, POPL (2018), 56:1–56:29.  https://doi.org/10.1145/3158144
  * Wang et al. (2020b) Yuepeng Wang, Rushi Shah, Abby Criswell, Rong Pan, and Isil Dillig. 2020b.  Data Migration using Datalog Program Synthesis.  _Proc. VLDB Endow._ 13, 7 (2020), 1006–1019.  https://doi.org/10.14778/3384345.3384350
  * Wang et al. (2020a) Yisu Remy Wang, Shana Hutchison, Dan Suciu, Bill Howe, and Jonathan Leang. 2020a.  SPORES: Sum-Product Optimization via Relational Equality Saturation for Large Scale Linear Algebra.  _Proc. VLDB Endow._ 13, 11 (2020), 1919–1932.  http://www.vldb.org/pvldb/vol13/p1919-wang.pdf
  * Willsey et al. (2021) Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021\.  egg: Fast and extensible equality saturation.  _Proc. ACM Program. Lang._ 5, POPL (2021), 1–29.  https://doi.org/10.1145/3434304
  * Zaniolo et al. (2017) Carlo Zaniolo, Mohan Yang, Ariyam Das, Alexander Shkapsky, Tyson Condie, and Matteo Interlandi. 2017\.  Fixpoint semantics and optimization of recursive Datalog programs with aggregates.  _Theory Pract. Log. Program._ 17, 5-6 (2017), 1048–1065.  https://doi.org/10.1017/S1471068417000436
  * Zaniolo et al. (2018) Carlo Zaniolo, Mohan Yang, Matteo Interlandi, Ariyam Das, Alexander Shkapsky, and Tyson Condie. 2018\.  Declarative BigData Algorithms via Aggregates and Relational Database Dependencies. In _Proceedings of the 12th Alberto Mendelzon International Workshop on Foundations of Data Management, Cali, Colombia, May 21-25, 2018_ _(CEUR Workshop Proceedings, Vol. 2100)_ , Dan Olteanu and Barbara Poblete (Eds.). CEUR-WS.org.  http://ceur-ws.org/Vol-2100/paper2.pdf

##  Appendix A Grammar Refinements

As discussed in Section 6.2.3, we implement further refinements of the grammar
in Figure 8 to limit the search space. First, we allow the user to specify a
type for each attribute of a relation. For example, a weighted edge relation
$E(x:\text{ID},y:\text{ID},z:\text{int})$ has 2 attributes of type ID and the
last attribute typed int. Although they all share the same concrete type
(think “machine type”), the abstract types help guide the synthesizer to never
use the same variables for attributes of different types. Second, we allow the
user to define helper functions. One example is the definition of $D$ in
Figure 18 which computes the distance between two vertices. $D$ is used
repeatedly in the remaining definition in Figure 18, and it is a common
practice for programmers to abstract out such recurring patterns. We leverage
good practice like this to aid synthesis: if a user defines a helper function
with head relation $R$, we will include $R$ as a base relation in our grammar
because it is likely that the helper function is also helpful in the optimized
query. When generating a candidate, we simply inline the definition of the
helper function, thereby including an entire sub-expression of the original
query. Concretely, the refinements augment the grammar in Figure 8 with types
and adds the following cases to the production rule of $Q_{0}$:

$Q_{0}\rightarrow\cdots\mid Z_{int}\mid F(Z,Z,\ldots,Z)$

where $Z_{int}$ are variables of type int and $F$ is a user-defined helper
function.

##  Appendix B Benchmark Programs

Figures 17, 18, 20, 19, 14, 15 and 16 contain the benchmark queries used in
the experiments. In each query, $V$ is the set of input vertices and $E$ the
set of input edges. A binary edge relation is unweighted, and a ternary edge
relation is weighted with the weight in the third position. The domain of all
relations is integers. Each query outputs the head relation of the last rule.

$\displaystyle TC(x,y)$ $\displaystyle=V(x)\wedge[x=y]\vee\exists
t(TC(x,t)\wedge E(t,y))$ $\displaystyle R(y)$ $\displaystyle=TC(\texttt{a},y)$
Figure 14. Beyond Magic (BM). a is a constant vertex ID, chosen uniformly at
random during experiments. $\displaystyle TC(x,y)$
$\displaystyle=V(x)\wedge[x=y]\vee\exists t(TC(x,t)\wedge E(t,y))$
$\displaystyle SCC[x]$ $\displaystyle=\min_{v}\\{{v}\mid{TC(x,v)}\\}$
Figure 15. Connected Components (CC). Note the vertex ID itself is used as the
label for that vertex, instead of $L(v)$ in fig. 1. $\displaystyle D(x,d)$
$\displaystyle=[x=\texttt{a}]\wedge[d=0]$
$\displaystyle\vee\exists(y,d_{1},d_{2}:D(y,d_{1})\wedge
E(y,x,d_{2})\wedge[d=d_{1}+d_{2}])$ $\displaystyle SP[x]$
$\displaystyle=\min_{d}\\{{d}\mid{D(x,d)}\\}$
Figure 16. Single-source Shortest Paths (SSSP). a is a constant vertex ID,
chosen uniformly at random during experiments. $\displaystyle W(t,j,w)$
$\displaystyle=A(j,w)\wedge[t=j]$ $\displaystyle\vee\exists(s:[t=s+1]\wedge
W(s,j,w)\wedge[1\leq j<t])$ $\displaystyle P[t]$
$\displaystyle=\sum_{j,w}\\{{w}\mid{W(t,j,w)}\\}$ $\displaystyle S[t]$
$\displaystyle=P[t]-P[t-10]$
Figure 17. Window Sum (WS) with a window size of 10. $A$ is an array, and
$A(i,v)$ is true when $A$ holds $v$ at index $i$, and arrays are 1-indexed.
$\displaystyle D(s,t,k)$ $\displaystyle=V(x)\wedge[s=t]\wedge[k=0]$
$\displaystyle\vee[k=1+\min_{v,l}\\{{l}\mid{E(v,t)\wedge[s\neq t]\wedge
D(s,v,l)}\\}]$ $\displaystyle\sigma(s,t,n)$
$\displaystyle=V(s)\wedge[s=t]\wedge[n=1]$ $\displaystyle\vee E(v,t)\wedge
D(s,v,d_{sv})\wedge D(s,t,d_{st})$
$\displaystyle\wedge[d_{sv}=d_{st}+1]\wedge[s\neq t]\wedge\sigma(s,v,m)$
$\displaystyle B[v]$
$\displaystyle=\sum_{s,t,b}\\{\sigma_{sv}\times\sigma_{vt}/\sigma_{st}\mid[s\neq
t]\wedge[s\neq v]\wedge[t\neq v]$ $\displaystyle\wedge D(s,t,d_{st})\wedge
D(s,v,d_{sv})\wedge D(v,t,d_{vt})\wedge[d_{st}=d_{sv}+d_{vt}]$
$\displaystyle\wedge\sigma(s,v,\sigma_{sv})\wedge\sigma(v,t,\sigma_{vt})\wedge\sigma(s,t,\sigma_{st})\\}$
Figure 18. Betweenness Centrality (BC). Intuitively, $D$ computes the distance
between two vertices, and $\sigma$ computes the number of shortest paths
between two vertices. $\displaystyle TC(x,y,w)$
$\displaystyle=V(x)\wedge[x=y]\wedge[w=0]$
$\displaystyle\vee\exists(z,w_{1}:TC(x,z,w_{1})\wedge
E(z,y)\wedge[w=w_{1}+1])$ $\displaystyle SP[x,y]$
$\displaystyle=\min_{w}\\{{w}\mid{TC(x,y,w)}\\}$ $\displaystyle R[x]$
$\displaystyle=\max_{y}\\{{SP[x,y]}\mid{}\\}$
Figure 19. Graph Radius (R). $R[x]$ computes the length of the longest
shortest-path between $x$ and any other vertex in the graph. Intuitively, it
is the diameter with one vertex fixed. $\displaystyle TC(x,y)$
$\displaystyle=V(x)\wedge[x=y]\vee\exists(z:TC(x,z)\wedge E(z,y))$
$\displaystyle M[x]$ $\displaystyle=\sum_{v}\\{{v}\mid{TC(x,v)}\\}$
Figure 20. Multi-level Marketing (MLM). Intuitively, each vertex $v$
represents a participant who makes $v$ amount of profit; the query $M[x]$
computes the total profit of the sub-network under participant $x$.

##  Appendix C Magic Set Optimization

We describe here a general form of magic set optimization and show that its
correctness can be proven by a verifier using only three rules: the FGH rule,
the Stratification Rule, and the Fixpoint rule, described below. Each of the
rewrite rules can be proven by our verifier, but our synthesizer cannot
synthesize the magic rewritings in general; it is currently restricted to
relatively simple rewritings, like those illustrated earlier in the paper.

##### Notations

In this section we restrict the discussion to the Boolean semiring and
monotone functions. When we write $F(X)$ we assume that $X$ is a tuple of IDB
relations, e.g. $X=(R,S,T)$, and $F(X)$ returns a tuple of relations of the
same arities. A datalog program has the form $X\text{ :- }F(X)$, and we denote
by $\bar{X}$ its least fixpoint. Given two tuples of relations $X,Y$ of the
same type, i.e. the same number of relations and of the same arities, we write
$X\Rightarrow Y$ to mean component-wise set inclusion. For example, if
$X=(R_{1},S_{1},T_{1})$ and $Y=(R_{2},S_{2},T_{2})$ then $X\Rightarrow Y$
means $R_{1}\subseteq R_{2}$, $S_{1}\subseteq S_{2}$, $T_{1}\subseteq T_{2}$.

###  C.1. The Three Rules

##### Simplified FGH Rule

We consider the following simplified version of the FGH rule. Given two
datalog programs:

$\displaystyle\Pi_{1}:\ X\text{ :- }$ $\displaystyle F(X)$
$\displaystyle\Pi_{2}:\ Y\text{ :- }H(Y)$

a homomorphism from $\Pi_{1}$ to $\Pi_{2}$ is a function $G$ satisfying
$G(\emptyset)=\emptyset$ and $G(F(X))=H(G(X))$ for all $X$. If such a
homomorphism exists, then the FGH-rule in Theorem 3.1 implies the following:

(32) $\displaystyle G(\bar{X})=$ $\displaystyle\bar{Y}$

The only difference from the FGH-rule in Theorem 3.1 is that we do not ask for
$\Pi_{1}$ to return $G(X)$.

##### Stratification Rule

Assume $K(Z),F(Z,X)$ are two monotone functions over tuples of relations, such
that the output of $K$ has the same type as $Z$, and the output of $F$ has the
same type as $X$. Then the following two programs are equivalent:

$\displaystyle\begin{array}[t]{rrl}\Pi:&Z\text{ :- }&K(Z)\\\ &X\text{ :-
}&F(Z,X)\end{array}$ $\displaystyle\begin{array}[t]{rrll}\Pi^{\prime}:&Z\text{
:- }&K(Z)&\mbox{// Stratum 0: let $\bar{Z}$ be its fixpoint}\\\
\cline{2-3}\cr&X\text{ :- }&F(\bar{Z},X)&\mbox{// Stratum 1: note the use of
$\bar{Z}$}\end{array}$

The program $\Pi$ computes both sets of rules $K,F$ in a single stratum.
Program $\Pi^{\prime}$ separates them into two strata: first it computes the
fixpoint $\bar{Z}$ of $K$, then uses it as an EDB to compute the fixpoint of
$F(\bar{Z},X)$. This stratification rule is well known for monotone datalog,
and we omit the proof. A formal statement asserts that, for any
$\omega$-continuous functions $K$, $F$, denoting
$L(Z,X)\stackrel{{\scriptstyle\text{def}}}{{=}}(K(Z),F(Z,X))$, we have
$\text{\sf lfp}(L)=(\text{\sf lfp}(K),\text{\sf lfp}(\lambda X.F(\text{\sf
lfp}(K),X)))$.

##### Fixpoint Rule

Consider a datalog program, and suppose that its stratum $s$ is the following:

$\displaystyle X\text{ :- }$ $\displaystyle F(X)$

Let $\bar{X}$ be the fixpoint of stratum $s$. Then the following constraint
holds in all strata $s^{\prime}>s$:

(33) $\displaystyle F(\bar{X})\Rightarrow$ $\displaystyle\bar{X}$

###  C.2. Running Example

Throughout this section we will illustrate using the following example.

###### Example C.1.

We show below a program $\Pi$ and its magic set optimized program $\Pi_{O}$.

$\displaystyle\begin{array}[b]{rrl}\Pi:&R(x)\text{ :- }&V(x)\\\ &R(x)\text{ :-
}&T(x,y,z)\wedge R(y)\wedge R(z)\\\ &Q(x)\text{ :- }&G(x)\wedge
R(x)\end{array}$
$\displaystyle\begin{array}[b]{rrl}\Pi_{O}:&Q_{0}^{\prime}()\text{ :- }&\\\
&R^{\prime}_{O}(y)\text{ :- }&R^{\prime}_{O}(x)\wedge T(x,y,z)\\\
&R^{\prime}_{O}(z)\text{ :- }&R^{\prime}_{O}(x)\wedge T(x,y,z)\wedge
R_{O}(y)\\\ &R_{O}^{\prime}(x)\text{ :- }&Q^{\prime}_{O}()\wedge G(x)\\\
&R_{O}(x)\text{ :- }&R^{\prime}_{O}(x)\wedge V(x)\\\ &R_{O}(x)\text{ :-
}&R^{\prime}_{O}(x)\wedge T(x,y,z)\wedge R(y)\wedge R(z)\\\ &Q_{O}(x)\text{ :-
}&Q^{\prime}_{O}()\wedge G(x)\wedge R_{O}(x)\end{array}$

$\Pi$ computes an IDB $R(x)$, then returns $Q(x)$ which is a restriction of
$R$. The optimized program $\Pi_{O}$ computes the IDB $R_{O}(x)$ only on a
subset of the nodes $x$ that are sufficient to answer $Q$, namely the set
defined by $R^{\prime}_{O}(x)$. The predicate $R^{\prime}_{O}(x)$ is called
the magic predicate.

###  C.3. Definition of Magic Set Rewriting

We use the elegant definition of magic set rewriting by Mascellani and
Pedreschi (Mascellani and Pedreschi, 2002).

##### Notation

An atom $A$ is a predicate symbol followed by variables and/or constants, e.g.
$A$ can be $R(^{\prime}a^{\prime},^{\prime}b^{\prime},x,y)$. Single atoms are
denoted $A,B,\dots$ and sequences (possibly empty) of atoms by
$\mathbf{A},\mathbf{B},\dots$ Each datalog rule has the form $A\text{ :-
}\mathbf{A}$. Following the convention used in (Abiteboul et al., 1995), a
query is given by a datalog program $\Pi$ and a query predicate $Q$ not
occurring in $\Pi$, such that $Q$ is defined by a single rule $r_{Q}$ of the
form $r_{Q}:Q(\mathbf{v})\text{ :- }\mathbf{A}$, where $\mathbf{A}$ does not
contain the predicate $Q$.

##### Modes

For an $n$-ary relation symbol $R$, a mode is a string $\\{+,-\\}^{n}$.
Intuitively a $+$ represents an input, and a $-$ represents an output. Given a
datalog program $\Pi$, we fix a moding for each relational symbol $R$. The
moding can be arbitrary, with a single restriction: the mode of the output
predicate $Q$ must be $(-,-,\cdots,-)$, i.e. all its positions are output
positions. To simplify the notations, we will assume w.l.o.g. that, for each
relational symbol $R$ the input positions precede the output positions, i.e.
its mode is $+\cdots+-\cdots-$. Hence, an atom $A$ of the form
$R(\mathbf{u},\mathbf{v})$ has input arguments $\mathbf{u}$ and output
arguments $\mathbf{v}$.

##### Magic set transformation

To each relational symbol $R$ we associate two new symbols. A magic symbol
$R^{\prime}_{O}$, whose arity is the number of input positions in the mode of
$R$, and an optimized symbol $R_{O}$, of the same arity as $R$. If $A$ is the
atom $R(\mathbf{u},\mathbf{v})$, then we denote by
$A^{\prime}_{O}\stackrel{{\scriptstyle\text{def}}}{{=}}R^{\prime}(\mathbf{u})$
and $A_{O}\stackrel{{\scriptstyle\text{def}}}{{=}}R_{O}(\bm{u},\bm{v})$ the
atoms with the corresponding symbols $R^{\prime}_{O}$ and $R_{O}$
respectively. Similarly, if $\bm{A}$ is a sequence of atoms, then we denote by
$\bm{A}^{\prime}_{O}$ and $\bm{A}_{O}$ the corresponding sequences of atoms.
If $R$ is an EDB, then we define $R_{O}$ to be the same EDB, and we will often
remove the subscript $O$.

###### Definition C.2.

(Mascellani and Pedreschi, 2002, Definition 3) Let $\Pi$ be a datalog program
with an output predicate $Q$. The magic set transformation is the program
$\Pi_{O}$ obtained from $\Pi$ by the following transformation steps:

  1. (1)

For every rule in $\Pi$ fix an order of the atoms in its body, i.e. the rule
becomes:

$\displaystyle r\colon\ A\text{ :- }$ $\displaystyle B_{1}\wedge
B_{2}\wedge\cdots\wedge B_{k}$

For every atom $B_{\ell}$ above add the new rule:

(34) $\displaystyle r^{\prime}_{\ell}\colon\ B^{\prime}_{\ell,O}\text{ :- }$
$\displaystyle A^{\prime}_{O}\wedge B_{1,O}\wedge\cdots\wedge B_{\ell-1,O}$

  2. (2)

Add the following rule with an empty body (i.e. the body is true):
$Q^{\prime}_{O}()\text{ :- }$.

  3. (3)

Replace each original rule $A\text{ :- }\mathbf{A}$ in $\Pi$ by the new rule
$A_{O}\text{ :- }A^{\prime}_{O},\mathbf{A}_{O}$.

###### Example C.3.

In Example C.1 we use the modes $R(+)$, and $Q(-)$. We associate to the atoms
$R(x),Q(x)$ the magic atoms $R_{O}^{\prime}(x),Q_{O}^{\prime}()$ and the
optimized atoms $R_{O}(x),Q_{O}(x)$. The modes for the EDBs $V,T,G$ can be
arbitrary, since the magic symbols
$V^{\prime}_{O},T^{\prime}_{O},G^{\prime}_{O}$ are never used in any rule, and
hence they were omitted from $\Pi_{O}$; they are useful for us only to
simplify the statement of Lemma C.6 below, and for that reason we illustrate
them here, assuming that their modes are $-,-,-$. Then, according to item 1 of
Def. C.2, the optimized program should include these rules:

$\displaystyle V^{\prime}_{O}()\text{ :- }$ $\displaystyle R^{\prime}_{O}(x)$
$\displaystyle T^{\prime}_{O}()\text{ :- }$ $\displaystyle R^{\prime}_{O}(x)$
$\displaystyle G^{\prime}_{O}()\text{ :- }$ $\displaystyle Q^{\prime}()$

If we add these rules to the program $\Pi_{O}$ in Example C.1, then we observe
that, at fixpoint, $\bar{R}_{O}^{\prime}\neq\emptyset$ (assuming
$G\neq\emptyset$), and therefore,
$\bar{V}^{\prime}_{O}()=\bar{T}^{\prime}_{O}()=\bar{G}^{\prime}_{O}()=\texttt{true}$.

##### Correctness

We restate here the theorem from (Mascellani and Pedreschi, 2002, Theorem 4):

###### Theorem C.4.

Let $\Pi$ be a datalog program with query predicate $Q$. Fix any moding of its
symbols, and let $\Pi_{O}$, be the corresponding magic program. Then, at
fixpoint, the IDB $\bar{Q}$ computed by $\Pi$ equals the IDB $\bar{Q}_{O}$
computed by $\Pi_{O}$.

We will re-prove the theorem by showing, importantly, that the equivalence of
the two programs follows from the three rules, FGH, Stratification, and
Fixpoint, and therefore can be checked automatically by a verifier.

###  C.4. Property B

To prove the equivalence of $\Pi$ and $\Pi_{O}$ we only need one property of
the optimized program, which we call Property B. We prove here that the
specific rewriting in Def. C.2 ensures that the resulting program $\Pi_{0}$
satisfies Property B; later we will show that any program $\Pi_{O}$ satisfying
Property B is equivalent to $\Pi$. Our proof here consists of several
applications of the chase procedure, which we briefly review here.

##### The Chase

Suppose that the following constraint holds: $\forall
x(\Phi(x)\Rightarrow\Psi(x))$. Then the following equivalence holds:

$\displaystyle\forall x(\Phi(x)\wedge\Gamma(x)\equiv$
$\displaystyle\Phi(x)\wedge\Psi(x)\wedge\Gamma(x))$

By “applying the chase” we mean rewriting the formula $\Phi(x)\wedge\Gamma(x)$
to $\Phi(x)\wedge\Psi(x)\wedge\Gamma(x)$. The “back-chase” proceeds in
reverse, i.e. it removes $\Psi(x)$. Both the chase and the back-chase can be
encoded in an EQSAT system (see Sec. 7), and therefore proofs based on
chase/back-chase can be derived and checked automatically.

Consider a program $\Pi$ and its magic-set rewriting $\Pi_{O}$ in Definition
C.2. Consider the least fixpoint of $\Pi_{O}$; as usual we denote by
$\bar{R}_{O}^{\prime},\bar{R}_{O}$ the instances in this least fixpoint; this
notation extends to the case when $R$ is an EDB symbol, then simply
$\bar{R}_{O}\stackrel{{\scriptstyle\text{def}}}{{=}}R$.

###### Definition C.5 (Boundedness).

Let $R$ be an IDB symbol occurring in the program $\Pi$. We say that an
instance $R$ is bounded w.r.t. $\Pi_{O}$ if it satisfies:

(35) $\displaystyle\forall u\forall v(\bar{R}^{\prime}_{O}(u)\wedge
R(u,v)\Rightarrow$ $\displaystyle\bar{R}_{O}(u,v))$

This definition holds trivially for each EDB relation $R$: each such relation
is bounded, because $\bar{R}_{O}=R$ by definition.

###### Lemma C.6 (Property B).

Consider an instance of all IDBs of the program $\Pi$ that is bounded w.r.t.
$\Pi_{O}$. Then, for every rule $r$ in the original program $\Pi$:

$\displaystyle r:\ A\text{ :- }$ $\displaystyle\bm{B}$

the following equivalence holds:

(36) $\displaystyle\bar{A}^{\prime}_{O}\wedge\bm{B}\equiv$
$\displaystyle\bar{A}^{\prime}_{O}\wedge\bar{\bm{B}}_{O}^{\prime}\wedge\bm{B}$

To help the reader parsing Eq. (36), we note that the atoms in the sequence
$\bm{B}$ refer to the bounded relational instance (the symbols appearing in
$\Pi$), while the atoms $\bar{A}^{\prime}_{O}$ and $\bar{\bm{B}}_{O}^{\prime}$
refer to the fixpoint of the program $\Pi_{O}$.

###### Proof.

This proof is the place where we use the magic rule (34) in item 1 of
Definition C.2. Specifically, we write $\bm{B}=B_{1}\wedge\cdots\wedge B_{k}$,
where the order of the atoms is that chosen in Def. C.2 item 1. At fixpoint,
for each $\ell=1,k$, the magic rule (34) becomes the following implication by
the Fixpoint rule (see Eq. (33)):

(37)
$\displaystyle\bar{A}^{\prime}_{O}\wedge\bigwedge_{i=1,\ell-1}\bar{B}_{i,O}\Rightarrow$
$\displaystyle\bar{B}_{\ell,O}^{\prime}$

We will chase repeatedly the LHS of (36) with the implications (37) and (35)
to arrive at the RHS.

For each $\ell=0,k$, denote by $\Phi_{\ell}$ the following sentence:

$\displaystyle\Phi_{\ell}\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle\bar{A}^{\prime}\wedge\bigwedge_{i=1,\ell}\left(\bar{B}_{i,O}^{\prime}\wedge
B_{i}\right)\wedge\bigwedge_{i=\ell+1,k}B_{i}$

Eq. (36) asserts that $\Phi_{0}\equiv\Phi_{k}$, and we prove it by showing
that, for every $\ell=1,k$, the following holds:

$\displaystyle\Phi_{\ell-1}\equiv$ $\displaystyle\Phi_{\ell}$

This follows from the following chase steps:

$\displaystyle\bar{A}^{\prime}_{O}\wedge\bigwedge_{i=1,\ell-1}\left(\bar{B}_{i,O}^{\prime}\wedge
B_{i}\right)\wedge B_{\ell}\equiv$
$\displaystyle\bar{A}^{\prime}_{O}\wedge\bigwedge_{i=1,\ell-1}\left(\bar{B}_{i,O}^{\prime}\wedge\bar{B}_{i,O}\wedge
B_{i}\right)\wedge B_{\ell}$ Chase with (35) $\displaystyle\equiv$
$\displaystyle\bar{A}^{\prime}_{O}\wedge\bigwedge_{i=1,\ell-1}\left(\bar{B}_{i,O}^{\prime}\wedge\bar{B}_{i,O}\wedge
B_{i}\right)\wedge\bar{B}_{\ell,O}^{\prime}\wedge B_{\ell}$ Chase with (37)
$\displaystyle\equiv$
$\displaystyle\bar{A}^{\prime}_{O}\wedge\bigwedge_{i=1,\ell}\left(\bar{B}_{i,O}^{\prime}\wedge
B_{i}\right)$ Back-chase with (35)

By conjoining both sides of the equivalence above with
$\bigwedge_{i=\ell+1,k}B_{i}$ we obtain $\Phi_{\ell-1}\equiv\Phi_{\ell}$, as
required. ∎

###### Example C.7.

We describe the Property B for the running Example C.1. Let
$\bar{R}_{O}^{\prime},\bar{Q}_{O}^{\prime}$ be the outputs of the magic
predicates of the program $\Pi_{O}$. Notice that
$Q_{O}^{\prime}()\equiv\texttt{true}$. The Property B asserts the following:
if $R,Q$ are two bounded instances, meaning that they satisfy:

(38) $\displaystyle\forall x(\bar{R}_{O}^{\prime}(x)\wedge R(x)\Rightarrow$
$\displaystyle\bar{R}_{O}(x))$ $\displaystyle\forall
x(\bar{Q}_{O}^{\prime}()\wedge Q(x)\Rightarrow$ $\displaystyle\bar{Q}_{O}(x))$

then the following holds (one constraint for each of the 3 rules of $\Pi$):

$\displaystyle\forall x(\bar{R}^{\prime}_{O}(x)\wedge V(x)\equiv$
$\displaystyle\bar{R}^{\prime}_{O}(x)\wedge\bar{V}^{\prime}_{O}()\wedge V(x))$
$\displaystyle\forall x(\bar{R}^{\prime}_{O}(x)\wedge T(x,y,z)\wedge
R(y)\wedge R(z)\equiv$
$\displaystyle\bar{R}^{\prime}_{O}(x)\wedge\bar{T}_{O}^{\prime}()\wedge
T(x,y,z)\wedge\bar{R}_{O}^{\prime}(y)\wedge
R(y)\wedge\bar{R}^{\prime}_{O}(z)\wedge R(z))$ $\displaystyle\forall
x(\bar{Q}_{O}^{\prime}()\wedge G(x)\wedge R(x)\equiv$
$\displaystyle\bar{Q}_{O}^{\prime}()\wedge\bar{G}_{O}^{\prime}()\wedge
G(x)\wedge\bar{R}_{O}^{\prime}(x)\wedge R(x))$

We saw in Example C.3 that
$\bar{V}^{\prime}_{O}()\equiv\bar{T}^{\prime}_{O}()\equiv\bar{G}^{\prime}_{O}()\equiv\texttt{true}$,
hence to check Property B it suffices to check only two equivalences:

$\displaystyle\forall x(\bar{R}^{\prime}_{O}(x)\wedge T(x,y,z)\wedge
R(y)\wedge R(z)\equiv$ $\displaystyle\bar{R}^{\prime}_{O}(x)\wedge
T(x,y,z)\wedge\bar{R}_{O}^{\prime}(y)\wedge
R(y)\wedge\bar{R}^{\prime}_{O}(z)\wedge R(z))$ $\displaystyle\forall
x(\bar{Q}_{O}^{\prime}()\wedge G(x)\wedge R(x)\equiv$
$\displaystyle\bar{Q}_{O}^{\prime}()\wedge
G(x)\wedge\bar{R}_{O}^{\prime}(x)\wedge R(x))$

We leave it up to the reader to check that both constraints can be derived by
repeated chase and back-chase using the constraints (38) and the following
constraints derived from the property of the fixpoint of $\Pi_{O}$ (see Eq.
(33)):

$\displaystyle\forall x(\bar{R}_{O}^{\prime}(x)\wedge T(x,y,z)\Rightarrow$
$\displaystyle\bar{R}_{O}^{\prime}(y))$ $\displaystyle\forall
x(\bar{R}_{O}^{\prime}(x)\wedge T(x,y,z)\wedge\bar{R}_{O}(y)\Rightarrow$
$\displaystyle\bar{R}_{O}^{\prime}(z))$

###  C.5. Correctness Proof of Magic Set Rewriting

We prove a stronger claim than Theorem C.4: we prove the correctness of magic
set rewriting using only the FGH, the Stratification, and the Fixpoint rules.
While at a high level our proof is inspired by Mascellani and Pedreschi
(Mascellani and Pedreschi, 2002), it differs in that we use the least fixpoint
semantics of a datalog program rather than the minimal model semantics. This
allows us to prove the equivalence $\Pi\equiv\Pi_{O}$ using only the three
rules, FGH, Stratification, and Fixpoint. Moreover, our proof here is
independent of the particular definition of the magic set rewriting used to
define $\Pi_{O}$ (Def. C.2), and, instead, applies to any program $\Pi_{O}$
that satisfies Property B.

Let $X$ denote the tuple of IDBs of the original program $\Pi$, and fix a
moding. Then we let $X^{\prime}$ denote the tuple of the magic IDBs, in other
words:

$\displaystyle X=$
$\displaystyle(R_{1}(\bm{u}_{1},\bm{v}_{1}),R_{2}(\bm{u}_{2},\bm{v}_{2}),\ldots)$
$\displaystyle X^{\prime}=$
$\displaystyle(R^{\prime}_{1}(\bm{u}_{1}),R^{\prime}_{2}(\bm{u}_{2}),\ldots)$

We denote by $X^{\prime}\wedge X$ their pairwise conjunction:

$\displaystyle X^{\prime}\wedge X\stackrel{{\scriptstyle\text{def}}}{{=}}$
$\displaystyle(R^{\prime}_{1}(\bm{u}_{1})\wedge
R_{1}(\bm{u}_{1},\bm{v}_{1}),R^{\prime}_{2}(\bm{u}_{2})\wedge
R_{2}(\bm{u}_{2},\bm{v}_{2}),\ldots)$

Consider two programs $\Pi$ and $\Pi_{O}$:

(39) $\displaystyle\Pi:\ X\text{ :- }$ $\displaystyle F(X)$